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})