How to parse a string into a list of lists in Coq?

Question

I was trying to parse a string with double newlines into a list of lists of int in Coq but I'm not able to make it work as expected.

Example string:

1
2

3
4
5

The above string needs to be parsed into [[1; 2]; [3; 4; 5]]. I followed a similar example for parsing but I think I'm using the wrong parsing levels.

Here's my faulty code:

From Coq Require Export List NArith.

#[global] Open Scope N.
Import ListNotations.

Declare Custom Entry elfEntry.
Declare Custom Entry elfEntry1.

Notation "'input' elf1 .. elfN" :=
    (cons elf1 .. (cons elfN nil) ..)
  (at level 200, elf1 custom elfEntry, only parsing).

Notation "cal1 .. calN" := (cons cal1 .. (cons calN nil) ..)
  (in custom elfEntry at level 1, cal1 custom elfEntry1).

Notation "cal1" := cal1
  (in custom elfEntry1 at level 1, cal1 constr at level 1).

Definition example := input
1
2

3
4
5
.

Print example.

Answer 1

I am afraid you need to have an explicit separator

Notation "'input' elf1 ';' .. ';' elfN" :=
    (cons elf1 .. (cons elfN nil) ..)
  (at level 200, elf1 custom elfEntry, only parsing).

Notation "cal1 .. calN" := (cons cal1 .. (cons calN nil) ..)
  (in custom elfEntry at level 1, cal1 custom elfEntry1).

Notation "cal1" := cal1
  (in custom elfEntry1 at level 1, cal1 constr at level 1).

Definition example := input
1
2
;
3
4
.

Print example.