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的第一个答案。

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)

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

Answer 2

我参加聚会有点晚了，但我目前正在编写一个完整的解析器组合库，并且我有一个相当紧凑的解决方案，重新使用NesList@NovaDenizen 建议的简洁类型。

我使用差异列表，但基本列表也可以（我们只需替换DList.toList为，List.reverse因为chainl1从左到右聚合值）。

NList : Set → ℕ → Set
NList A zero    = A
NList A (suc n) = List (NList A n)

NList′ : {A : Set} → [ Parser A ] →
         (n : ℕ) → [ Parser (NList A n) ]
NList′ A zero    = A
NList′ A (suc n) = parens $ return $ DList.toList <$>
                   chainl1 (DList.[_] <$> NList′ A n)
                           (return $ DList._++_ <$ char ',')

所有测试用例都成功通过。我已将示例添加到（整体）poc 文件中，以便您自己检查

_ : "((1,2,3),(4,5,6))" ∈ NList′ decimal 2
_ = (1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ [] !

_ : "((1,2,3),(4,5,6),(7,8,9,10))" ∈ NList′ decimal 2
_ = (1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ (7 ∷ 8 ∷ 9 ∷ 10 ∷ []) ∷ [] !

_ : "((1),(2))" ∈ NList′ decimal 2
_ = (1 ∷ []) ∷ (2 ∷ []) ∷ [] !

_ : "((1,2))" ∈ NList′ decimal 2
_ = (1 ∷ 2 ∷ []) ∷ [] !

_ : "(((1,2),(3,4)),((5,6),(7,8)))" ∈ NList′ decimal 3
_ = ((1 ∷ 2 ∷ []) ∷ (3 ∷ 4 ∷ []) ∷ []) ∷
    ((5 ∷ 6 ∷ []) ∷ (7 ∷ 8 ∷ []) ∷ []) ∷ [] !

Answer 3

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

module NewParser where

-- dummy
open import Data.Maybe
open import Data.Bool

-- includes
open import Data.List hiding (map)

-- ***
-- WAS PRELUDE IMPORTS
open import StringHelpers using (charToℕ; stringToℕ)
open import Data.String hiding (_==_; _++_)
open import Data.Char
open import Function
open import Data.Nat
open import Data.Unit
open import Data.Maybe


-- https://github.com/crypto-agda/agda-nplib/tree/master/lib/Text
open import Text.Parser
open import ParserHelpers



--- ****
--- Lessons Learned, this is the key:
--- (was a basic error that tyeps where too specific, generalisation not possible)

-- parseList : {A : Set} → Parser (Maybe A) → Parser (Maybe A) → ℕ → Parser (List (Maybe A))
-- converted to
-- parseList : {A : Set} → Parser A → Parser A → ℕ → Parser (List A)



-- *****
-- General ... Normal List (depth 1)

parseList : {A : Set} → Parser A → Parser A → ℕ → Parser (List A)
parseList oneMatcher manyMatcher n = ⟪ _++_ · (map toL oneMatcher) · (many n manyMatcher) ⟫

parseBracketList : {A : Set} → Parser A → Parser A → ℕ → Parser (List A)
parseBracketList oneMatcher manyMatcher n = bracket '(' (parseList oneMatcher manyMatcher n) ')'

parseCommaListConvert : {A : Set} → (List Char → A) → (Parser (List Char)) → ℕ → Parser (List A)
parseCommaListConvert convert parser = parseBracketList (⟪ convert · parser ⟫) (⟪ convert · parseOne "," *> parser ⟫) 


-- For Numbers

number : Parser (List Char)
number = manyOneOf (toList "1234567890")

parseNumList : ℕ → Parser (List (Maybe ℕ))
parseNumList = parseCommaListConvert charsToℕ number


-- Nested List (depth 2)
--

parseListListNum : ℕ → Parser (List (List (Maybe ℕ)))
parseListListNum n = parseList (parseNumList n) ((parseOne ",") *> (parseNumList n)) n


parseManyLists : ℕ → Parser (List (List (Maybe ℕ)))
parseManyLists n = bracket '(' (parseListListNum n) ')'



-- Run the Parsers
--

open import MaybeEliminatorHelper

-- max number of terms is the number of characters in the string
-- this is for the termination checker
runParseList' : String → Maybe (List (Maybe ℕ))
runParseList' s = runParser (parseNumList (strLength s)) (toList s)

runParseList : String → Maybe (List ℕ)
runParseList = maybe-list-maybe-eliminate ∘ runParseList'

-- nested list
runParseNesList' : String → Maybe (List (List( Maybe ℕ)))
runParseNesList' s = runParser (parseManyLists (length (toList s))) (toList s)

runParseNesList : String → Maybe (List (List ℕ))
runParseNesList = maybe-list-list-maybe-eliminate ∘ runParseNesList' 

这是我的辅助功能：

module MaybeEliminatorHelper where

open import Data.Maybe
open import Category.Monad
open import Function

open import Data.List

open import Category.Functor


sequence-maybe : ∀ {a} {A : Set a} → List (Maybe A) → Maybe (List A)
sequence-maybe = sequence Data.Maybe.monad


join : {A : Set} → Maybe (Maybe A) → Maybe A
join m = m >>= id
  where 
    open RawMonad Data.Maybe.monad


maybe-list-elem : {A : Set} → Maybe (List (Maybe A)) → Maybe (List A)
maybe-list-elem mlm = join (sequence-maybe <$> mlm)
  where open RawFunctor functor

{-
sequence-maybe : [Maybe a] -> Maybe [a]

join :: Maybe (Maybe a) -> Maybe a


Maybe (List (List (Maybe A))
  Maybe.fmap (List.fmap sequenc-maybe)
Maybe (List (Maybe (List A))
  Maybe.fmap sequence-maybe
Maybe (Maybe (List (List A)))
  join
Maybe (List (List A))



join . Maybe.fmap sequence-maybe . Maybe.fmap (List.fmap sequenc-maybe)

join . Maybe.fmap (sequence-maybe . List.fmap sequenc-maybe)
(short form)

-}

maybe-list-elem2 : {A : Set} → Maybe (List (List (Maybe A))) → Maybe (List (List A)) 
maybe-list-elem2 = join ∘ Mfmap (sequence-maybe ∘ Lfmap sequence-maybe)
  where
    open RawMonad Data.Maybe.monad hiding (join) renaming (_<$>_ to Mfmap)
    open RawMonad Data.List.monad hiding (join) renaming (_<$>_ to Lfmap)


maybe-list-maybe-eliminate = maybe-list-elem

maybe-list-list-maybe-eliminate = maybe-list-elem2

其他辅助功能：

-- ***
-- WAS PRELUDE IMPORTS
open import StringHelpers using (charToℕ; stringToℕ)

open import Data.String hiding (_==_)
open import Data.Char
open import Function
open import Data.Nat
open import Data.Unit
open import Data.Maybe



open import Text.Parser

open import Data.List


-- mini helpers
--

parseOne : String → Parser Char
parseOne = oneOf ∘ toList 

strLength : String → ℕ
strLength = length ∘ toList 


-- misc helpers
--

charsToℕ : List Char → Maybe ℕ
charsToℕ [] = nothing
charsToℕ xs = stringToℕ (fromList xs)

toL : ∀ {a} {A : Set a} → A → List A
toL x = x ∷ []


-- test
l : List (Maybe ℕ)
l = (just 3) ∷ (just 3) ∷ []


-- Parser Helpers Nicolas
--
isSpace : Char → Bool
isSpace = (_==_ ' ')

spaces : Parser ⊤
spaces = manySat isSpace *> pure _

-- decide if seperator before after brackets is spaces
someSpaces : Parser ⊤
someSpaces = someSat isSpace *> pure _

tok : Char → Parser ⊤
tok c = spaces *> char c *> pure _

bracket : ∀ {A} → Char → Parser A → Char → Parser A
bracket start p stop = tok start *> p <* tok stop

还有一些测试用例：

tn09 : pList "12,13,,14" ≡ nothing
tn09 = refl

tn08 : pList "" ≡ nothing
tn08 = refl

tn07 : pList "12,13,14" ≡ nothing
tn07 = refl

-- not working tn06 : pList "(12,13,14,17)," ≡ nothing
-- not working tn06 = refl

tn05 : pList "aa,bb,cc" ≡ nothing
tn05 = refl

tn04 : pList "11" ≡ nothing 
tn04 = refl

tn03 : pList "(11,12,13)" ≡ just (11 ∷ 12 ∷ 13 ∷ [])
tn03 = refl


-- new testcases
tn11 : pList2 "((1,2,3),(4,5,6),(7,8,9))" ≡ just ((1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ (7 ∷ 8 ∷ 9 ∷ []) ∷ [])
tn11 = refl

-- old testcases
p1 : pList2 "((1,2,3),(4,5,6))" ≡ just ((1 ∷ 2 ∷ 3 ∷ []) ∷ (4 ∷ 5 ∷ 6 ∷ []) ∷ [])
p1 = refl


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

p3 : pList2 "((1),(2))" ≡ just ((1 ∷ []) ∷ (2 ∷ []) ∷ [])
p3 = refl

p4 : pList2 "((1,2))" ≡ just ((1 ∷ 2 ∷ []) ∷ [])
p4 = refl

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