title: Agda: parsing nested lists
body: <p>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.</p>
  
  <p>So I would like to parse <code>"((1,2,3),(4,5,6))"</code> with a result type of <code>(List (List Nat))</code>. </p>
  
  <p>And further nested lists should be supported (up to depth 5), e.g., depth 3 would be <code>(List (List (List Nat)))</code>.</p>
  
  <p>My code is very long and cumbersome, and it only works for <code>(List (List Nat))</code> but not for further nested lists. I didn't make any progress on my own.</p>
  
  <p>If helpful, I would like to reuse <code>splitBy</code> from the <a href="https://stackoverflow.com/questions/11763639/agda-parse-a-string-with-numbers">first answer</a> of one of my older posts.</p>
  
  <pre><code>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
  </code></pre>
  
  <h2><strong><em>EDIT1</em></strong> **</h2>
  
  <p>Connor's talk at ICFP is online -- the title is "Agda-curious?".<br>
  It is from two days ago. Check it out!!<br>
  .<br>
  See the video:<br>
  <a href="http://www.youtube.com/watch?v=XGyJ519RY6Y" rel="nofollow noreferrer">http://www.youtube.com/watch?v=XGyJ519RY6Y</a>  </p>
  
  <p>--<br>
  <strong>EDIT2:</strong><br>
  I found a link that seems to be almost the code I need for my parsing.<br>
  There is a <code>tokenize</code> function provided:<br>
  <a href="https://github.com/fkettelhoit/agda-prelude/blob/master/Examples/PrefixCalculator.agda" rel="nofollow noreferrer">https://github.com/fkettelhoit/agda-prelude/blob/master/Examples/PrefixCalculator.agda</a></p>
  
  <p>--<br>
  <strong>EDIT3:</strong><br>
  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.<br>
  Here is the link:  </p>
  
  <h2><a href="https://github.com/crypto-agda/agda-nplib/blob/master/lib/Text/Parser.agda" rel="nofollow noreferrer">https://github.com/crypto-agda/agda-nplib/blob/master/lib/Text/Parser.agda</a></h2>
  
  <p>There is more agda-code from Nicolas Pouillard online:<br>
  <a href="https://github.com/crypto-agda" rel="nofollow noreferrer">https://github.com/crypto-agda</a></p>