Agda:解析嵌套列表

Question

我试图解析Agda中的嵌套列表.我在谷歌搜索,我发现最接近的是在Haskell中解析,但通常使用像"parsec"这样的库,这些库在Agda中不可用.

所以我想"((1,2,3),(4,5,6))"用结果类型解析(List (List Nat)).

并且应该支持进一步的嵌套列表(直到深度5),例如,深度3将是(List (List (List Nat))).

我的代码非常冗长和繁琐,它只适用于(List (List Nat))但不适用于其他嵌套列表.我自己没有取得任何进展.

如果有帮助,我想splitBy从我的一篇旧帖子的第一个答案中重复使用.

NesList : ? ? Set
NesList 0 = ? -- this case is easy
NesList 1 = List ? -- this case is easy
NesList 2 = List (List ?) 
NesList 3 = List (List (List ?))
NesList 4 = List (List (List (List ?)))
NesList 5 = List (List (List (List (List ?)))) -- I am only interested to list depth 5
NesList _ = ? -- this is a hack, but I think okay for now


-- My implementation is *not* shown here
--
--
-- (it's about 80 lines long and uses 3 different functions
parseList2 : List Char ? Maybe (List (List ?))
parseList2 _ = nothing -- dummy result


parseList : (dept : ?) ? String ? Maybe (NesList dept)
parseList 2 s = parseList2 (toList s)
parseList _ _ = nothing



-- Test Cases that are working (in my version)

p1 : parseList 2 "((1,2,3),(4,5,6))" ? just ((1 ? 2 ? 3 ? []) ? (4 ? 5 ? 6 ? []) ? [])
p1 = refl


p2 : parseList 2 "((1,2,3),(4,5,6),(7,8,9,10))" ? just ((1 ? 2 ? 3 ? []) ? (4 ? 5 ? 6 ? []) ? (7 ? 8 ? 9 ? 10 ? []) ? [])
p2 = refl

p3 : parseList 2 "((1),(2))" ? just ((1 ? []) ? (2 ? []) ? [])
p3 = refl

p4 : parseList 2 "((1,2))" ? just ((1 ? 2 ? []) ? [])
p4 = refl

-- Test Cases that are not working 
-- i.e., List (List (List Nat))

lp5 : parseList 3 "(((1,2),(3,4)),((5,6),(7,8)))" ? just (  ((1 ? 2 ? []) ? (3 ? 4 ? []) ? []) ? ((5 ? 6 ? []) ? (7 ? 8 ? []) ? []) ? [])
lp5 = refl

EDIT1**

康纳在ICFP的演讲是在线 - 标题是"Agda好奇吗？".
它是从两天前开始的.看看这个!!
.
观看视频:http:
//www.youtube.com/watch？v = XGyJ519RY6Y

-
EDIT2:
我发现一个链接似乎几乎是我解析所需的代码.提供
了一个tokenize功能:https:
//github.com/fkettelhoit/agda-prelude/blob/master/Examples/PrefixCalculator.agda

-
EDIT3:
我终于找到了一个应该足够快的简单组合库.库中没有包含示例,因此我仍然需要了解如何解决问题.
链接在这里:

https://github.com/crypto-agda/agda-nplib/blob/master/lib/Text/Parser.agda

来自Nicolas Pouillard的更多agda代码在线:https:
//github.com/crypto-agda

Answer 1

我在这里发布我使用解析器组合器的解决方案。\n它使用github 上的 agda-nplib 库。\n该代码远非最佳，但它可以工作。

\n\n

module NewParser where\n\n-- dummy\nopen import Data.Maybe\nopen import Data.Bool\n\n-- includes\nopen import Data.List hiding (map)\n\n-- ***\n-- WAS PRELUDE IMPORTS\nopen import StringHelpers using (charTo\xe2\x84\x95; stringTo\xe2\x84\x95)\nopen import Data.String hiding (_==_; _++_)\nopen import Data.Char\nopen import Function\nopen import Data.Nat\nopen import Data.Unit\nopen import Data.Maybe\n\n\n-- https://github.com/crypto-agda/agda-nplib/tree/master/lib/Text\nopen import Text.Parser\nopen import ParserHelpers\n\n\n\n--- ****\n--- Lessons Learned, this is the key:\n--- (was a basic error that tyeps where too specific, generalisation not possible)\n\n-- parseList : {A : Set} \xe2\x86\x92 Parser (Maybe A) \xe2\x86\x92 Parser (Maybe A) \xe2\x86\x92 \xe2\x84\x95 \xe2\x86\x92 Parser (List (Maybe A))\n-- converted to\n-- parseList : {A : Set} \xe2\x86\x92 Parser A \xe2\x86\x92 Parser A \xe2\x86\x92 \xe2\x84\x95 \xe2\x86\x92 Parser (List A)\n\n\n\n-- *****\n-- General ... Normal List (depth 1)\n\nparseList : {A : Set} \xe2\x86\x92 Parser A \xe2\x86\x92 Parser A \xe2\x86\x92 \xe2\x84\x95 \xe2\x86\x92 Parser (List A)\nparseList oneMatcher manyMatcher n = \xe2\x9f\xaa _++_ \xc2\xb7 (map toL oneMatcher) \xc2\xb7 (many n manyMatcher) \xe2\x9f\xab\n\nparseBracketList : {A : Set} \xe2\x86\x92 Parser A \xe2\x86\x92 Parser A \xe2\x86\x92 \xe2\x84\x95 \xe2\x86\x92 Parser (List A)\nparseBracketList oneMatcher manyMatcher n = bracket \'(\' (parseList oneMatcher manyMatcher n) \')\'\n\nparseCommaListConvert : {A : Set} \xe2\x86\x92 (List Char \xe2\x86\x92 A) \xe2\x86\x92 (Parser (List Char)) \xe2\x86\x92 \xe2\x84\x95 \xe2\x86\x92 Parser (List A)\nparseCommaListConvert convert parser = parseBracketList (\xe2\x9f\xaa convert \xc2\xb7 parser \xe2\x9f\xab) (\xe2\x9f\xaa convert \xc2\xb7 parseOne "," *> parser \xe2\x9f\xab) \n\n\n-- For Numbers\n\nnumber : Parser (List Char)\nnumber = manyOneOf (toList "1234567890")\n\nparseNumList : \xe2\x84\x95 \xe2\x86\x92 Parser (List (Maybe \xe2\x84\x95))\nparseNumList = parseCommaListConvert charsTo\xe2\x84\x95 number\n\n\n-- Nested List (depth 2)\n--\n\nparseListListNum : \xe2\x84\x95 \xe2\x86\x92 Parser (List (List (Maybe \xe2\x84\x95)))\nparseListListNum n = parseList (parseNumList n) ((parseOne ",") *> (parseNumList n)) n\n\n\nparseManyLists : \xe2\x84\x95 \xe2\x86\x92 Parser (List (List (Maybe \xe2\x84\x95)))\nparseManyLists n = bracket \'(\' (parseListListNum n) \')\'\n\n\n\n-- Run the Parsers\n--\n\nopen import MaybeEliminatorHelper\n\n-- max number of terms is the number of characters in the string\n-- this is for the termination checker\nrunParseList\' : String \xe2\x86\x92 Maybe (List (Maybe \xe2\x84\x95))\nrunParseList\' s = runParser (parseNumList (strLength s)) (toList s)\n\nrunParseList : String \xe2\x86\x92 Maybe (List \xe2\x84\x95)\nrunParseList = maybe-list-maybe-eliminate \xe2\x88\x98 runParseList\'\n\n-- nested list\nrunParseNesList\' : String \xe2\x86\x92 Maybe (List (List( Maybe \xe2\x84\x95)))\nrunParseNesList\' s = runParser (parseManyLists (length (toList s))) (toList s)\n\nrunParseNesList : String \xe2\x86\x92 Maybe (List (List \xe2\x84\x95))\nrunParseNesList = maybe-list-list-maybe-eliminate \xe2\x88\x98 runParseNesList\' \n

\n\n

这是我的辅助函数：

\n\n

module MaybeEliminatorHelper where\n\nopen import Data.Maybe\nopen import Category.Monad\nopen import Function\n\nopen import Data.List\n\nopen import Category.Functor\n\n\nsequence-maybe : \xe2\x88\x80 {a} {A : Set a} \xe2\x86\x92 List (Maybe A) \xe2\x86\x92 Maybe (List A)\nsequence-maybe = sequence Data.Maybe.monad\n\n\njoin : {A : Set} \xe2\x86\x92 Maybe (Maybe A) \xe2\x86\x92 Maybe A\njoin m = m >>= id\n  where \n    open RawMonad Data.Maybe.monad\n\n\nmaybe-list-elem : {A : Set} \xe2\x86\x92 Maybe (List (Maybe A)) \xe2\x86\x92 Maybe (List A)\nmaybe-list-elem mlm = join (sequence-maybe <$> mlm)\n  where open RawFunctor functor\n\n{-\nsequence-maybe : [Maybe a] -> Maybe [a]\n\njoin :: Maybe (Maybe a) -> Maybe a\n\n\nMaybe (List (List (Maybe A))\n  Maybe.fmap (List.fmap sequenc-maybe)\nMaybe (List (Maybe (List A))\n  Maybe.fmap sequence-maybe\nMaybe (Maybe (List (List A)))\n  join\nMaybe (List (List A))\n\n\n\njoin . Maybe.fmap sequence-maybe . Maybe.fmap (List.fmap sequenc-maybe)\n\njoin . Maybe.fmap (sequence-maybe . List.fmap sequenc-maybe)\n(short form)\n\n-}\n\nmaybe-list-elem2 : {A : Set} \xe2\x86\x92 Maybe (List (List (Maybe A))) \xe2\x86\x92 Maybe (List (List A)) \nmaybe-list-elem2 = join \xe2\x88\x98 Mfmap (sequence-maybe \xe2\x88\x98 Lfmap sequence-maybe)\n  where\n    open RawMonad Data.Maybe.monad hiding (join) renaming (_<$>_ to Mfmap)\n    open RawMonad Data.List.monad hiding (join) renaming (_<$>_ to Lfmap)\n\n\nmaybe-list-maybe-eliminate = maybe-list-elem\n\nmaybe-list-list-maybe-eliminate = maybe-list-elem2\n

\n\n

更多辅助功能：

\n\n

-- ***\n-- WAS PRELUDE IMPORTS\nopen import StringHelpers using (charTo\xe2\x84\x95; stringTo\xe2\x84\x95)\n\nopen import Data.String hiding (_==_)\nopen import Data.Char\nopen import Function\nopen import Data.Nat\nopen import Data.Unit\nopen import Data.Maybe\n\n\n\nopen import Text.Parser\n\nopen import Data.List\n\n\n-- mini helpers\n--\n\nparseOne : String \xe2\x86\x92 Parser Char\nparseOne = oneOf \xe2\x88\x98 toList \n\nstrLength : String \xe2\x86\x92 \xe2\x84\x95\nstrLength = length \xe2\x88\x98 toList \n\n\n-- misc helpers\n--\n\ncharsTo\xe2\x84\x95 : List Char \xe2\x86\x92 Maybe \xe2\x84\x95\ncharsTo\xe2\x84\x95 [] = nothing\ncharsTo\xe2\x84\x95 xs = stringTo\xe2\x84\x95 (fromList xs)\n\ntoL : \xe2\x88\x80 {a} {A : Set a} \xe2\x86\x92 A \xe2\x86\x92 List A\ntoL x = x \xe2\x88\xb7 []\n\n\n-- test\nl : List (Maybe \xe2\x84\x95)\nl = (just 3) \xe2\x88\xb7 (just 3) \xe2\x88\xb7 []\n\n\n-- Parser Helpers Nicolas\n--\nisSpace : Char \xe2\x86\x92 Bool\nisSpace = (_==_ \' \')\n\nspaces : Parser \xe2\x8a\xa4\nspaces = manySat isSpace *> pure _\n\n-- decide if seperator before after brackets is spaces\nsomeSpaces : Parser \xe2\x8a\xa4\nsomeSpaces = someSat isSpace *> pure _\n\ntok : Char \xe2\x86\x92 Parser \xe2\x8a\xa4\ntok c = spaces *> char c *> pure _\n\nbracket : \xe2\x88\x80 {A} \xe2\x86\x92 Char \xe2\x86\x92 Parser A \xe2\x86\x92 Char \xe2\x86\x92 Parser A\nbracket start p stop = tok start *> p <* tok stop\n

\n\n

以及一些测试用例：

\n\n

tn09 : pList "12,13,,14" \xe2\x89\xa1 nothing\ntn09 = refl\n\ntn08 : pList "" \xe2\x89\xa1 nothing\ntn08 = refl\n\ntn07 : pList "12,13,14" \xe2\x89\xa1 nothing\ntn07 = refl\n\n-- not working tn06 : pList "(12,13,14,17)," \xe2\x89\xa1 nothing\n-- not working tn06 = refl\n\ntn05 : pList "aa,bb,cc" \xe2\x89\xa1 nothing\ntn05 = refl\n\ntn04 : pList "11" \xe2\x89\xa1 nothing \ntn04 = refl\n\ntn03 : pList "(11,12,13)" \xe2\x89\xa1 just (11 \xe2\x88\xb7 12 \xe2\x88\xb7 13 \xe2\x88\xb7 [])\ntn03 = refl\n\n\n-- new testcases\ntn11 : pList2 "((1,2,3),(4,5,6),(7,8,9))" \xe2\x89\xa1 just ((1 \xe2\x88\xb7 2 \xe2\x88\xb7 3 \xe2\x88\xb7 []) \xe2\x88\xb7 (4 \xe2\x88\xb7 5 \xe2\x88\xb7 6 \xe2\x88\xb7 []) \xe2\x88\xb7 (7 \xe2\x88\xb7 8 \xe2\x88\xb7 9 \xe2\x88\xb7 []) \xe2\x88\xb7 [])\ntn11 = refl\n\n-- old testcases\np1 : pList2 "((1,2,3),(4,5,6))" \xe2\x89\xa1 just ((1 \xe2\x88\xb7 2 \xe2\x88\xb7 3 \xe2\x88\xb7 []) \xe2\x88\xb7 (4 \xe2\x88\xb7 5 \xe2\x88\xb7 6 \xe2\x88\xb7 []) \xe2\x88\xb7 [])\np1 = refl\n\n\np2 : pList2 "((1,2,3),(4,5,6),(7,8,9,10))" \xe2\x89\xa1 just ((1 \xe2\x88\xb7 2 \xe2\x88\xb7 3 \xe2\x88\xb7 []) \xe2\x88\xb7 (4 \xe2\x88\xb7 5 \xe2\x88\xb7 6 \xe2\x88\xb7 []) \xe2\x88\xb7 (7 \xe2\x88\xb7 8 \xe2\x88\xb7 9 \xe2\x88\xb7 10 \xe2\x88\xb7 []) \xe2\x88\xb7 [])\np2 = refl\n\np3 : pList2 "((1),(2))" \xe2\x89\xa1 just ((1 \xe2\x88\xb7 []) \xe2\x88\xb7 (2 \xe2\x88\xb7 []) \xe2\x88\xb7 [])\np3 = refl\n\np4 : pList2 "((1,2))" \xe2\x89\xa1 just ((1 \xe2\x88\xb7 2 \xe2\x88\xb7 []) \xe2\x88\xb7 [])\np4 = refl\n

\n\n

我愿意接受改进代码的建议。

\n