parsing - 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来自 first answer我的旧帖子之一。

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

编辑1 **

康纳在 ICFP 的演讲是在线的——标题是“Agda-curious?”。
这是两天前的事。一探究竟!!
.
看视频:
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 的在线代码:
https://github.com/crypto-agda

Answer 1

我现在无法访问 agda 实现，所以我无法检查语法，但这就是我要解决的问题。

首先，NesList 可以简化。

NesList 0 = ℕ
NesList (succ n) = List (NesList n)

然后你需要一个通用的列表解析函数。您可以使用 List 而不是 Maybe 来指定替代解析。返回值是一个成功的解析和字符串的剩余部分。

Parser : Set -> Set
Parser a = List Char -> Maybe (Pair a (List Char))

这给定类型 x 的解析器例程，解析 x 的括号描述的逗号分隔列表。

parseGeneralList : { a : Set } Parser a -> Parser (List a)
parseGeneralList = ...implement me!...

这会解析一个通用的 NesList。

parseNesList : (a : ℕ) -> Parser (NesList a)
parseNesList 0 = parseNat
parseNesList (succ n) = parseGeneralList (parseNesList n)

编辑:正如评论中指出的那样，使用这种 Parser 的代码不会通过 agda 的终止检查器。我在想，如果你想做解析器组合器，你需要一个基于 Stream 的设置。