In case things crash somehow during upgrade, I stashed the whole Earley parser here for now.

Parsing.idr

module Parsing
import ParsingHelpers
--import Data.List.Quantifiers

data Transition : (a -> a -> Type) -> a -> a -> Type where
  IdTrans : (f x y) -> Transition f x y
  StepTrans : (f x y) -> Transition f y z -> Transition f x z

rhs_head_transitive_closure : DecEq s => Grammar s -> List s -> List (Rule s)
rhs_head_transitive_closure g vs = 
  transitive_closure check conv g vs
  where
    check : (v : s) -> Rule s -> Bool
    check v x = decAsBool (decEq v (lhs x))
    conv  : Rule s -> s
    conv = rhs_head

record Item (s:Type) where
  constructor Incomplete
  origin : Nat
  rule : Rule s
  dot_point : Index (rhs rule)

record CompleteItem (s:Type) where
  constructor Complete
  origin : Nat
  rule : Rule s

predict : DecEq s => Grammar s -> List s -> List (s, Item s)
predict g = map new_item . rhs_head_transitive_closure g
  where new_item : Rule s -> (s, Item s)
        new_item rule = (rhs_head rule, Incomplete Z rule rhs_head_index)

zeros : List (Nat, s) -> List (s)
zeros [] = []
zeros ((Z, x) :: xs) = x :: zeros xs
zeros ((S _, _) :: xs) = zeros xs

decr : List (Nat, s) -> List (Nat, s)
decr [] = []
decr ((Z,s) :: xs) = decr xs
decr ((S x,s) :: xs) = (x, s) :: decr xs

process : Nat -> List (s, Item s) ->
  (List (Nat, s), List (CompleteItem s), List (s, Item s))
process m [] = ([],[],[])
process m ((x, Incomplete n r dp) :: xs) = let (a,b,c) = process m xs
  in case nexth dp of
  Just dpn => (a, b, (nth dpn, Incomplete (n+m) r dpn)::c)
  Nothing => ((n, lhs r)::a, (Complete (n+m) r)::b, c) 

pitpull : DecEq s => List s -> List (s, Item s) -> List (s, Item s)
pitpull xs st = transitive_closure check conv st xs
  where check : s -> (s, Item s) -> Bool
        check x y = decAsBool (decEq x (fst y))
        conv : (s, Item s) -> s
        conv (x, Incomplete Z r dp) = case nexth dp of
          Just _ => x
          Nothing => lhs r
        conv (x, _) = x

shift : DecEq s => List (List (s, Item s))
  -> (List (Nat, s))
  -> {default (S Z) m : Nat}
  -> (List (CompleteItem s), List (s, Item s))
shift [] ss {m} = ([], [])
shift (st::sts) ss {m} = let
  (tt,c1,s1) = process m (pitpull (zeros ss) st)
  (c2,s2) = shift sts (decr $ tt ++ ss) {m=S m}
  in (c1++c2, s1++s2)

recognize : DecEq s => (g : Grammar s) -> (acc:s) -> (input:List s) -> Bool
recognize g acc input = step [predict g [acc]] input
  where step : List (List (s, Item s)) -> (List s) -> Bool
        step sts [] = False
        step ([]::_) _ = False
        step sts (x :: []) = let
          (c,_) = shift sts [(0, x)]
          m = (length sts)
          in any (\(Complete n r) => (m == n) && decAsBool(decEq acc (lhs r))) c
        step sts (x :: ys) = let
          (_,st) = shift sts [(0, x)]
          st2 = predict g (map fst st)
          in step ((st++st2)::sts) ys

mutual
  data Generates : Grammar s -> s -> List s -> Type where
    Put : Generates g s [s]
    Derive : (ir:Index g) -> Seq g (rhs (nth ir)) xs
      -> {auto x_is:lhs (nth ir) = x}
      -> Generates g x xs

  data Seq : Grammar s -> List s -> List s -> Type where
    Nil  : Seq g [] []
    (::) : Generates g s xs -> Seq g ss ys -> {auto zs_is:(xs ++ ys = zs)}
      -> Seq g (s::ss) zs

recognize_lemma : DecEq s => (Grammar s) -> (acc:s) -> (input:List s)
  -> (recognize g acc input = True) -> Generates g acc input
recognize_lemma g acc [] Refl impossible
recognize_lemma g acc (k::rest) prf = ?aaaaaa



--x -- Some two fun little auxiliary proofs.
--x next_ndex_empty_tail : Dec (xs=[]) -> Dec (next_ndex (Z {xs=xs}) = Nothing)
--x next_ndex_empty_tail (Yes Refl) = Yes Refl
--x next_ndex_empty_tail {xs = []} (No contra) = Yes Refl
--x next_ndex_empty_tail {xs = (x :: xs)} (No contra) =
--x   No (\assum => case assum of Refl impossible)
--x 
--x next_ndex_is_next : (next_ndex (Z {xs=(x::(y::xs))}) = Just (S Z {xs=(x::(y::xs))}))
--x next_ndex_is_next = Refl

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

DecEq Symbol where
  decEq A A = Yes Refl
  decEq A B = No (\pf => case pf of Refl impossible)
  decEq A C = No (\pf => case pf of Refl impossible)
  decEq A D = No (\pf => case pf of Refl impossible)
  decEq B B = Yes Refl
  decEq B A = No (\pf => case pf of Refl impossible)
  decEq B C = No (\pf => case pf of Refl impossible)
  decEq B D = No (\pf => case pf of Refl impossible)
  decEq C C = Yes Refl
  decEq C A = No (\pf => case pf of Refl impossible)
  decEq C B = No (\pf => case pf of Refl impossible)
  decEq C D = No (\pf => case pf of Refl impossible)
  decEq D D = Yes Refl
  decEq D A = No (\pf => case pf of Refl impossible)
  decEq D B = No (\pf => case pf of Refl impossible)
  decEq D C = No (\pf => case pf of Refl impossible)

test_grammar : Grammar Symbol
test_grammar = [
  D ::= [A,B,C],
  D ::= [B,C],
  D ::= [B,C],
  B ::= [A,C],
  A ::= [B,C],
  B ::= [C] ]

leaf_a : SPPF Parsing.test_grammar (Sym A) [A]
leaf_a = Leaf
leaf_b : SPPF Parsing.test_grammar (Sym B) [B]
leaf_b = Leaf
leaf_c : SPPF Parsing.test_grammar (Sym C) [C]
leaf_c = Leaf
leaf_d : SPPF Parsing.test_grammar (Sym D) [D]
leaf_d = Leaf

generates_abc : SPPF Parsing.test_grammar (Sym D) [A,B,C]
generates_abc = Branch ab leaf_c {rule=Z} {dot=(S Z)}
  where ab : SPPF Parsing.test_grammar (Dot Z {rule=Z}) [A,B]
        ab = (Branch leaf_a leaf_b {rule=Z} {dot=Z})

ParsingHelpers.idr

module ParsingHelpers
%default total

public export
flip : (a = b) -> (b = a)
flip Refl = Refl

public export
plus_reduces_z : {m : Nat} -> plus Z m = m
plus_reduces_z = Refl

public export
plus_reduces_sk : {k, m : Nat} -> plus (S k) m = S (plus k m)
plus_reduces_sk = Refl

public export
plus_commutes_z : m = plus m 0
plus_commutes_z {m = Z} = Refl
plus_commutes_z {m = (S k)} = let rec = plus_commutes_z {m=k}
  in rewrite rec in Refl

public export
plus_commutes : (n, m : Nat) -> plus n m = plus m n
plus_commutes Z m = plus_commutes_z
plus_commutes (S k) Z = rewrite plus_commutes_z {m=k} in Refl
plus_commutes (S k) (S j) = let
  pk = plus_commutes k (S j)
  pj = plus_commutes (S k) j
  in rewrite pk in rewrite flip pj in cong {f=S . S} (flip$plus_commutes k j)

public export
plus_assoc : (n, m, p : Nat) -> plus n (plus m p) = plus (plus n m) p
plus_assoc Z m p = Refl
plus_assoc (S k) m p = let pa = plus_assoc k m p in cong pa

public export
data Index : (xs : List a) -> Type where
  Z : Index (x :: xs)
  S : Index xs -> Index (x :: xs)

public export
Uninhabited (Index []) where
  uninhabited (Z) impossible
  uninhabited (S _) impossible

public export
nth : {list:List a} -> Index list -> a
nth {list = []} Z impossible
nth {list = []} (S _) impossible
nth {list = (a :: _)} Z = a
nth {list = (_ :: xs)} (S x) = nth {list=xs} x

public export
nexth : Index xs -> Maybe (Index xs)
nexth {xs = []} Z impossible
nexth {xs = []} (S _) impossible
nexth {xs = (_ :: [])} Z = Nothing
nexth {xs = (_ :: (_ :: _))} Z = Just (S Z)
nexth {xs = (_ :: _)} (S j) = nexth j >>= (Just . S)

public export
last : Index (x::xs)
last {xs = []} = Z
last {xs = (_ :: xs)} = S last

public export
data Selected : (List a) -> (List a) -> (a -> Type) -> Type where
  IsSelected : {a:List t, b:List t}
    -> ((x:Index a) -> p (nth x) -> (y:Index b ** (nth x = nth y)))
    -> ((y:Index b) -> p (nth y))
    -> Selected b a p

public export
select : {p:a -> Type} -> ((x:a) -> Dec (p x))
  -> List a -> List a
select f = filter (\x => decAsBool (f x))

public export
lemma_cons : {xs:List a, ys:List a} -> (x :: xs = y :: ys) -> (x = y, xs = ys)
lemma_cons Refl = (Refl, Refl)

public export
select_theorem : {a:Type} -> (xs:List a) -> (ys:List a)
  -> (p:a -> Type)
  -> (f:(x:a) -> Dec (p x))
  -> ys = select f xs
  -> Selected ys xs p
select_theorem [] ys p f prf = IsSelected
  (\a => absurd a)
  (\a => case prf of Refl impossible)
select_theorem (x :: xs) ys p f prf with (f x)
  select_theorem (x :: xs) ys p f prf | (Yes y) with (ys)
    select_theorem (x :: xs) ys p f prf | (Yes y) | [] = absurd prf
    select_theorem (x :: xs) ys p f prf | (Yes y) | (z :: zs) with (lemma_cons prf)
      select_theorem (x :: xs) ys p f prf | (Yes y) | (x :: zs) | (Refl, prf2) with (select_theorem xs zs p f prf2)
        select_theorem (x :: xs) ys p f prf | (Yes y) | (x :: zs) | (Refl, prf2) | (IsSelected g z) = IsSelected
          (\ix => case ix of 
             Z => \_ => (Z ** Refl)
             (S x) => \px => let (foo**pf) = g x px in (S foo ** pf))
          (\yx => case yx of 
             Z => y
             (S x) => z x)
  select_theorem (x :: xs) ys p f prf | (No contra) with (select_theorem xs ys p f prf)
    select_theorem (x :: xs) ys p f prf | (No contra) | (IsSelected g y) = IsSelected
      (\ix => case ix of
        Z => (void . contra)
        (S x) => g x) y

-- https://gist.github.com/MarcelineVQ/5152c66371c047860157dad597144502
public export
data Singleton : (x : k) -> Type where
  With : (y : a) -> y = x -> Singleton x

public export
inspect : (x : a) -> Singleton x
inspect x = With x Refl

public export
bifndx : Bool -> a -> (List a, List a) -> (List a, List a)
bifndx c a (x, y) = if c then (x, a::y) else (a::x, y)

public export
bin : (a -> Bool) -> List a -> (List a, List a)
bin f [] = ([], [])
bin f (x :: xs) = bifndx (f x) x (bin f xs)

public export
pj1_thm : ((a,b) = c) -> (a = fst c)
pj1_thm x = cong {f=fst} x

public export
pj2_thm : ((a,b) = c) -> (b = snd c)
pj2_thm x = cong {f=snd} x

public export
zero_thm : (plus a 0) = a
zero_thm {a} = plus_commutes a Z

public export
comm : (a:Nat) -> (b:Nat) -> (plus a b) = (plus b a)
comm = plus_commutes

public export
plus_motion : (a:Nat) -> (b:Nat) -> (S (plus a b) = plus a (S b))
plus_motion Z b = Refl
plus_motion (S k) b = rewrite comm k (S b) in cong {f=S . S} (comm k b)

public export
bin_theorem : {i, j:List a}
  -> (f:a -> Bool) -> (i,j) = bin f k -> length i + length j = length k
bin_theorem {k = []} f Refl = Refl
bin_theorem {k = (x :: xs)} f prf = case (inspect(f x), inspect (bin f xs)) of
  (With False a, With (i,j) b) =>
         rewrite pj1_thm prf
      in rewrite pj2_thm prf
      in rewrite flip b
      in rewrite flip a
      in cong {f=S} (bin_theorem f b)
  (With True a, With (i,j) b) => 
         rewrite pj1_thm prf
      in rewrite pj2_thm prf
      in rewrite flip b
      in rewrite flip a
      in rewrite flip (plus_motion (length i) (length j))
      in cong {f=S} (bin_theorem f b)

public export
always_lte : LTE a (plus z a)
always_lte {a = Z} = LTEZero
always_lte {a = (S k)} {z = Z} = LTESucc (always_lte {a=k} {z=Z})
always_lte {a = (S k)} {z = (S j)} = let
  ll = always_lte {a=k} {z=S j}
  in rewrite plus_motion j (S k)
  in rewrite flip (plus_motion j (S k))
  in rewrite flip (plus_motion j k)
  in (LTESucc ll)

public export
bin_smaller : {i, j:List a}
  -> (f:a -> Bool) -> ((i,j) = bin f k) -> (size j = S z) -> Smaller i k
bin_smaller {k} {i} {z} f prf prf1 = let booboo = bin_theorem f prf {k=k}
  in rewrite flip booboo
  in rewrite prf1
  in rewrite (comm (length i) (S z))
  in LTESucc always_lte

public export
TCR : (s:Type) -> (w:Type) -> List w -> Type
TCR s w g = List s -> List w

public export
transitive_closure : (s -> w -> Bool) -> (w -> s)
  -> List w -> List s -> List w
transitive_closure {s} {w} ck conv g vs = let
  ind = sizeInd {a=List w} {P=TCR s w}
  in ind step g vs
  where step : (x : List w)
    -> ((y : List w) -> Smaller y x -> TCR s w y)
    -> TCR s w x
        step g rec [] = []
        step g rec (a::aa) = case inspect (bin (ck a) g) of
          (With (ll,rr) prf) => case inspect (length rr) of
            (With Z prf2) => step g rec aa
            (With (S z) prf2) => let
              ree = rec ll (bin_smaller (ck a) prf (flip prf2) {k=g})
              in rr ++ ree (map conv rr)

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

public export
total Grammar : Type -> Type
Grammar s = List (Rule s)

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

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

public export
rhs_head_index : {r:Rule s} -> Index (rhs r)
rhs_head_index {r = (x ::= [])} impossible
rhs_head_index {r = (x ::= (y :: xs))} = Z

public export
rhs_head : Rule s -> s
rhs_head (x ::= xs) = head xs

public export
rhs_tail : Rule s -> List s
rhs_tail (x ::= xs) = tail xs

public export
cut : {xs:List a} -> Index xs -> (List a, List a)
cut {xs=(x::xs)} Z = ([x], xs)
cut {xs=(x::xs)} (S k) = let rec = cut k in (x::fst rec, snd rec)

public export
concat_theorem : {auto nxs:NonEmpty xs} -> (k:Index (xs ++ ys) ** cut k = (xs, ys))
concat_theorem {nxs=IsNonEmpty} {xs=(x::[])} = (Z ** Refl)
concat_theorem {nxs=IsNonEmpty} {xs=(_::x::xs)} {ys} = let
  (k ** prf) = concat_theorem {xs=(x::xs)} {ys=ys}
  prf1 = pj1_thm (flip prf)
  prf2 = pj2_thm (flip prf)
  in (S k ** rewrite prf1 in rewrite prf2 in Refl)

public export
data SPPS : (s:Type) -> Grammar s -> Type where
  Sym : s -> SPPS s g
  Dot : {g:Grammar s} -> (rule:Index g) -> Index (rhs_tail (nth rule)) -> SPPS s g

public export
its_same : Index xs -> Index (x::xs)
its_same Z = Z
its_same (S y) = S (its_same y)

public export
prev_dot : (i:Index g) -> Index (rhs_tail (nth i)) -> SPPS s g
prev_dot i x = case read x of
    Just prev => Dot i prev
    Nothing   => Sym (rhs_head (nth i))
  where read : Index s -> Maybe (Index s)
        read Z = Nothing
        read (S y) = Just (its_same y)

public export
this_dot : (i:Index g) -> Index (rhs_tail (nth i)) -> SPPS s g
this_dot i x = case nexth x of
  Just _ => Dot i x
  Nothing => Sym (lhs (nth i))

-- https://www.sciencedirect.com/science/article/pii/S1571066108001497
-- SPPF-style parsing from Earley recognizers.
public export
data SPPF : (g:Grammar s) -> SPPS s g -> List s -> Type where
  Leaf : SPPF g (Sym s) [s]
  Short : (rule:Index g) -> SPPF g (Sym x) xs
    -> {auto short_rule:(rhs (nth rule) = [x])}
    -> {auto z_is:(lhs (nth rule) = z)}
    -> SPPF g (Sym z) xs
  Branch : SPPF g (prev_dot rule dot) xs -> SPPF g (Sym (nth dot)) ys
    -> {default concat_theorem ok:(k:Index zs ** cut k = (xs,ys))}
    -> {auto z_is:(this_dot rule dot = z)}
    -> SPPF g z zs
  DeepShort : (rule:Index g) -> SPPF g (Sym x) xs
    -> {auto short_rule:(rhs (nth rule) = [x])}
    -> {auto z_is:(lhs (nth rule) = z)}
    -> SPPF g (Sym z) xs
    -> SPPF g (Sym z) xs
  DeepBranch : SPPF g (prev_dot rule dot) xs -> SPPF g (Sym (nth dot)) ys
    -> {default concat_theorem ok:(k:Index zs ** cut k = (xs,ys))}
    -> {auto z_is:(this_dot rule dot = z)}
    -> SPPF g z zs
    -> SPPF g z zs