Agda: parsing nested lists

Question

I am trying to parse nested lists in Agda. I searched on google and the closest I have found is parsing addressed in Haskell, but usually libraries like "parsec" are used that are not available in Agda.

So I would like to parse "((1,2,3),(4,5,6))" with a result type of (List (List Nat)).

And further nested lists should be supported (up to depth 5), e.g., depth 3 would be (List (List (List Nat))).

My code is very long and cumbersome, and it only works for (List (List Nat)) but not for further nested lists. I didn't make any progress on my own.

If helpful, I would like to reuse splitBy from the first answer of one of my older posts.

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 **

Connor's talk at ICFP is online -- the title is "Agda-curious?".
It is from two days ago. Check it out!!
.
See the video:
http://www.youtube.com/watch?v=XGyJ519RY6Y

--
EDIT2:
I found a link that seems to be almost the code I need for my parsing.
There is a tokenize function provided:
https://github.com/fkettelhoit/agda-prelude/blob/master/Examples/PrefixCalculator.agda

--
EDIT3:
I finally found a simple combinator library that should be fast enough. There are no examples included in the library so I still have to look how to solve the problem.
Here is the link:

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

There is more agda-code from Nicolas Pouillard online:
https://github.com/crypto-agda

Answer 1

I don't have access to an agda implementation right now, so I can't check syntax, but this is how I would address it.

First, NesList can be simplified.

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

Then you need a general-purpose list parsing function. Instead of Maybe you could use List to specify alternative parses. The return value is a successful parse and the remainder of the string.

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

This, given a parser routine for type x, parses a parenthesis-delineated comma-separated list of x.

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

This parses a general NesList.

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

Edit: As was pointed out in the comments, code using this kind of Parser won't pass agda's termination checker. I'm thinking that if you want to do parser combinators you need a Stream based setup.

Answer 2

I'm a bit late to the party but I am currently writing a total parser combinators library and I have a fairly compact solution re-using the neat NesList type suggested by @NovaDenizen.

I use difference lists but the basic ones would do too (we'd simply have to replace DList.toList with List.reverse because chainl1 aggregates values left to right).

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 ',')

All the test cases pass successfully. I have added the example to the (monolithic) poc file so you can check for yourself

_ : "((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 ∷ []) ∷ []) ∷ [] !