module Parsing infixl 10 ::= data Rule : Type -> Type where (::=) : s -> (xs:List s) -> {auto nonempty:NonEmpty xs} -> Rule s total Grammar : Type -> Type Grammar s = List (Rule s) lhs : Rule s -> s lhs (x ::= xs) = x rhs : Rule s -> List s rhs (x ::= xs) = xs rhs_not_empty : (r:Rule s) -> NonEmpty (rhs r) rhs_not_empty ((::=) x xs {nonempty}) = nonempty rhs_head : Rule s -> s rhs_head (x ::= xs) = head xs data Indexer : (xs : List a) -> Type where Z : Indexer (x :: xs) S : Indexer xs -> Indexer (x :: xs) z_ndex : (list:List s) -> NonEmpty list -> Indexer list z_ndex (_ :: _) IsNonEmpty = Z rule_first_index : (r:Rule s) -> Indexer (rhs r) rule_first_index r = z_ndex (rhs r) (rhs_not_empty r) lemma_select : {p:List a} -> (i:List a) -> (Indexer i -> Indexer p) -> (Indexer p -> Maybe b) -> List b lemma_select [] _ _ = [] lemma_select (x :: xs) f g = let zs = lemma_select xs (f . S) g in case g (f Z) of Just z => z :: zs Nothing => zs select : (p:List a) -> (Indexer p -> Maybe b) -> List b select xs f = lemma_select xs (\a => a) f total ndex : {list:List a} -> Indexer list -> a ndex {list = []} Z impossible ndex {list = []} (S _) impossible ndex {list = (a :: _)} Z = a ndex {list = (_ :: xs)} (S x) = ndex {list=xs} x lemma_next_ndex : (xs:List a) -> (ys:List a) -> ((Indexer ys) -> Indexer xs) -> (Indexer ys) -> Maybe (Indexer xs) lemma_next_ndex xs (y::[]) f Z = Nothing lemma_next_ndex xs (y::(y2 :: ys)) f Z = Just (f (S Z)) lemma_next_ndex xs (y::ys) f (S s) = lemma_next_ndex xs ys (f . S) s next_ndex : Indexer xs -> Maybe (Indexer xs) next_ndex {xs} ix = lemma_next_ndex xs xs (\a => a) ix data Indexing : a -> List a -> Type where Ndex : (ix:Indexer list) -> Indexing (ndex ix) list -- Some two fun little auxiliary proofs. next_ndex_empty_tail : Dec (xs=[]) -> Dec (next_ndex (Z {xs=xs}) = Nothing) next_ndex_empty_tail (Yes Refl) = Yes Refl next_ndex_empty_tail {xs = []} (No contra) = Yes Refl next_ndex_empty_tail {xs = (x :: xs)} (No contra) = No (\assum => case assum of Refl impossible) next_ndex_is_next : (next_ndex (Z {xs=(x::(y::xs))}) = Just (S Z {xs=(x::(y::xs))})) next_ndex_is_next = Refl mutual data Generates : Grammar s -> s -> List s -> Type where Trivial : Generates g s [s] Derive : Indexing r g -> Seq g (rhs r) ys -> {auto zl:(lhs r = lhs_r)} -> 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 -> {auto zz:(xs ++ ys = zs)} -> Seq g (s::ss) zs -- 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] ] -- generates_abc : Generates Parsing.test_grammar D [A,B,C] -- generates_abc = Derive (Ndex Z) [Trivial, Trivial, Trivial] -- -- lemma_empty_lists : {xs:List s} -> {ys:List s} -> (xs ++ ys = []) -- -> (xs = [], ys = []) -- lemma_empty_lists {xs = []} {ys = []} prf = (Refl, Refl) -- lemma_empty_lists {xs = []} {ys = (_ :: _)} Refl impossible -- lemma_empty_lists {xs = (_ :: _)} {ys = []} Refl impossible -- lemma_empty_lists {xs = (_ :: _)} {ys = (_ :: _)} Refl impossible -- -- mutual -- total no_empty_seq : Seq g t [] -> NonEmpty t -> Void -- no_empty_seq [] IsNonEmpty impossible -- no_empty_seq ((::) x z {zz}) IsNonEmpty = let -- (Refl, Refl) = lemma_empty_lists zz in -- does_not_generate_empty x -- -- total does_not_generate_empty : {g:Grammar x} -> Generates g s [] -> Void -- does_not_generate_empty {g} (Derive {r} in_grammar y) = -- no_empty_seq y (rhs_not_empty r) -- -- b_must_be_b : Generates [D ::= [A, B, C], D ::= [B, C]] B xs -> (xs = [B]) -- b_must_be_b Trivial = Refl -- b_must_be_b (Derive (Ndex Z) y {zl=Refl}) impossible -- b_must_be_b (Derive (Ndex (S Z)) y {zl=Refl}) impossible -- -- s_abc_rule_lemma : Seq Parsing.test_grammar (rhs (index 0 Parsing.test_grammar)) [A, A, A] -> Void -- s_abc_rule_lemma ((::) Trivial ((::) x y {zz=ww}) {zz=Refl}) = case (b_must_be_b x, ww) of (Refl, Refl) impossible -- s_abc_rule_lemma ((Derive (Ndex Z) z {zl=Refl}) :: y) impossible -- s_abc_rule_lemma ((Derive (Ndex (S Z)) z {zl=Refl}) :: y) impossible -- -- s_bc_rule_lemma : Seq Parsing.test_grammar (rhs (index 1 Parsing.test_grammar)) [A, A, A] -> Void -- s_bc_rule_lemma ((::) Trivial _ {zz=Refl}) impossible -- s_bc_rule_lemma ((Derive (Ndex Z) z {zl=Refl}) :: y) impossible -- s_bc_rule_lemma ((Derive (Ndex (S Z)) z {zl=Refl}) :: y) impossible -- -- does_not_generate_aaa : Generates Parsing.test_grammar u [A,A,A] -> Void -- does_not_generate_aaa (Derive x y {r} {zl}) = case (x,zl) of -- (Ndex Z, Refl) => s_abc_rule_lemma y -- (Ndex (S Z), Refl) => s_bc_rule_lemma y -- Green slime -- -- Unification failures can be solved by expansion on parameters -- that fail to unify. data Item : (g:Grammar s) -> Bool -> Type where Completed : Nat -> Indexing r g -> Item g True Incomplete : Nat -> Indexing r g -> Indexer (rhs r) -> Item g False lemma_predict : DecEq s => {g:Grammar s} -> s -> (Indexer g) -> Maybe (s, Item g False) lemma_predict x ix = case decEq x (lhs$ndex ix) of (No contra) => Nothing (Yes _) => Just (rhs_head (ndex ix), Incomplete Z (Ndex ix) (rule_first_index (ndex ix))) predict : DecEq s => {g : Grammar s} -> s -> List (s, Item g False) predict {g} x = select g (lemma_predict x) lemma_shift : {g : Grammar s} -> Nat -> Item g False -> Either (Item g True) (s, Item g False) lemma_shift off (Incomplete k x y) = case (next_ndex y) of Nothing => Left (Completed (k+off) x) (Just y2) => Right (ndex y2, Incomplete (k+off) x y2) shift : DecEq s => {g : Grammar s} -> Nat -> s -> List (s, Item g False) -> (List (Item g True), List (s, Item g False)) shift k x [] = ([], []) shift k x ((a,item) :: xs) = let (c,p) = shift k x xs in case decEq x a of (Yes Refl) => case lemma_shift k item of (Left item) => (item :: c, p) (Right pitem) => (c, pitem :: p) (No contra) => (c,p) mark : DecEq s => s -> List s -> Maybe (List s) mark x [] = Just [x] mark x (y :: xs) = case decEq x y of (Yes prf) => Nothing (No contra) => mark x xs >>= Just . (y::) prediction : DecEq s => {g : Grammar s} -> (visited:List s) -> (completed:List s) -> List (s, Item g False) prediction visited [] = [] prediction visited (x :: xs) = case mark x visited of Nothing => prediction visited xs Just visited_x => let p = predict x in p ++ (prediction visited_x (map fst p ++ xs)) extractComplete : {g:Grammar s} -> Item g True -> (Nat, s) extractComplete (Completed ix _ {r}) = (ix, lhs r) lemma_completion : DecEq s => {g : Grammar s} -> (i:Nat) -> s -> (st:List (List (s, Item g False))) -> (List (Item g True), List (s, Item g False)) lemma_completion k x xs = case inBounds k xs of (Yes prf) => shift (S k) x (index k xs) (No contra) => ([],[]) -- For now handling the boundaries here. completion : DecEq s => {g : Grammar s} -> (st:List (List (s, Item g False))) -> (visited:List (Nat, s)) -> (completed:List (Nat, s)) -> (List (Nat, s), List (s, Item g False)) completion st visited [] = (visited, []) completion st visited (x :: xs) = case mark x visited of Nothing => completion st visited xs Just visited_x => let (c,p) = lemma_completion (fst x) (snd x) st (c2,p2) = completion st visited_x (map extractComplete c++xs) in (c2,p++p2) lemma_recognize : DecEq s => {g : Grammar s} -> s -> Nat -> (st : List (List (s, Item g False))) -> (input : List s) -> Bool lemma_recognize lhs i {g} st [] = False lemma_recognize lhs i {g} st (x :: []) = let (c,p) = completion st [] [(0, x)] in case mark (i,lhs) c of Nothing => True (Just _) => False lemma_recognize lhs i {g} st (x :: xs) = let (c,p) = completion st [] [(0, x)] p2 = prediction [] (map fst p) {g=g} in lemma_recognize lhs (S i) ((p ++ p2) :: st) xs {g=g} --recognize : (g : Grammar s) -> (lhs:s) -> (input:List s) -- -> Dec (Generates g lhs input) recognize : DecEq s => (g : Grammar s) -> (lhs:s) -> (input:List s) -> Bool recognize g lhs input = let ist = prediction [] [lhs] {g=g} in lemma_recognize lhs 1 [ist] input {g=g} accept : DecEq s => {g : Grammar s} -> (st:List (List (s, Item g False))) -> s -> (List (Nat, s), List (List (s, Item g False))) accept st x = let (c, p) = completion st [] [(0,x)] in (c, p :: st) step_0 : (List (Nat, Symbol), List (List (Symbol, Item Parsing.test_grammar False))) step_0 = ([], [predict D]) step_1 : (List (Nat, Symbol), List (List (Symbol, Item Parsing.test_grammar False))) step_1 = accept (snd step_0) A step_2 : (List (Nat, Symbol), List (List (Symbol, Item Parsing.test_grammar False))) step_2 = accept (snd step_1) B step_3 : (List (Nat, Symbol), List (List (Symbol, Item Parsing.test_grammar False))) step_3 = accept (snd step_2) C