The parsing challenge in Idris

ParsingChallenge.idr

module ParsingChallenge

-- The objective is the 'recognize' -function, on earley parsing style.
--Grammar : Type -> Type
--Generates : Grammar s -> s -> List s -> Type
--recognize : (g:Grammar s) -> (i:s) -> (s:List s) -> Dec (Generates g i s)

infixl 10 ::=
data Rule : Type -> Type where
  (::=) : s -> (xs:List s) -> {auto nonempty:NonEmpty xs} -> Rule s
data Grammar s = G (List (Rule s))

lhs : Rule s -> s
lhs (x ::= xs) = x

rhs : Rule s -> List s
rhs (x ::= xs) = xs

data InGrammar : (s:Type) -> Rule s -> Grammar s -> Type where
  GHead : (r:Rule s) -> InGrammar s r (G (r :: rs))
  GTail : InGrammar s r (G rs) -> InGrammar s r (G (r2 :: rs))

mutual
  data Generates : Grammar s -> s -> List s -> Type where
    Trivial : Generates g s [s]
    Derive : InGrammar s r g -> Seq g (rhs r) ys -> Generates g (lhs r) ys

  data Seq : Grammar s -> List s -> List s -> Type where
    Nil  : Seq g [] []
    (::) : Generates g s xs -> Seq g ss ys -> Seq g (s::ss) (xs ++ ys)

-- Test grammar, with some symbols
data Symbol = A | B | C | S

test_grammar : Grammar Symbol
test_grammar = G [
  S ::= [A,B,C],
  S ::= [B,C] ]

generates_abc : Generates Parsing.test_grammar S [A,B,C]
generates_abc = Derive (GHead (S ::= [A,B,C])) [Trivial, Trivial, Trivial]

-- Just try do this.
does_not_generate_empty : Generates g s [] -> Void

-- If you succeed, try prove this next
does_not_generate_aaa : Generates Parsing.test_grammar u [A,A,A] -> Void