Require Import Streams.
Require Import List.
Require Import Syntax.
Require Import Equality.
Require Import Alphabet.
Require Grammar.
Require Automaton.
Require Interpreter.

Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).

Section Init.

Variable init:initstate.

Inductive word_has_stack_semantics:
  forall (word:list token) (stack:stack), Prop :=
  | Nil_stack_whss: word_has_stack_semantics [] []
  | Cons_stack_whss:
    forall (wordq:list token) (stackq:stack),
      word_has_stack_semantics wordq stackq ->

    forall (wordt:list token) (s:noninitstate)
           (semantic_valuet:_),
      inhabited (parse_tree (last_symb_of_non_init_state s) wordt semantic_valuet) ->

    word_has_stack_semantics
       (wordq++wordt) (existT noninitstate_type s semantic_valuet::stackq).

Lemma pop_invariant_converter:
  forall A symbols_to_pop symbols_popped,
  arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A =
  arrows_left (map symbol_semantic_type symbols_popped)
    (arrows_right A (map symbol_semantic_type symbols_to_pop)).
Proof.
intros.
unfold arrows_right, arrows_left.
rewrite rev_append_rev, map_app, map_rev, fold_left_app.
f_equal.
rewrite <- fold_left_rev_right, rev_involutive.
reflexivity.
Qed.

Lemma pop_invariant:
  forall (symbols_to_pop symbols_popped:list symbol)
         (stack_cur:stack)
         (A:Type)
         (action:arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A),
  forall word_stack word_popped,
  forall sem_popped,
    word_has_stack_semantics word_stack stack_cur ->
    inhabited (parse_tree_list symbols_popped word_popped sem_popped) ->
    let action´ := eq_rect _ (fun x=>x) action _ (pop_invariant_converter _ _ _) in
    match pop symbols_to_pop stack_cur (uncurry action´ sem_popped) with
      | OK (stack_new, sem) =>
          exists word1res word2res sem_full,
            (word_stack = word1res ++ word2res)%list /\
            word_has_stack_semantics word1res stack_new /\
            sem = uncurry action sem_full /\
            inhabited (
              parse_tree_list (rev_append symbols_to_pop symbols_popped) (word2res++word_popped) sem_full)
      | Err => True
    end.
Proof.
induction symbols_to_pop; intros; unfold pop; fold pop.
exists word_stack ([]:list token) sem_popped; intuition.
f_equal.
apply JMeq_eq, JMeq_eqrect with (P:=(fun x => x)).
destruct stack_cur as [|[]]; eauto.
destruct (compare_eqdec (last_symb_of_non_init_state x) a); eauto.
destruct e; simpl.
dependent destruction H.
destruct H0, H1. apply (Cons_ptl X), inhabits in X0.
specialize (IHsymbols_to_pop _ _ _ action0 _ _ _ H X0).
match goal with
  IHsymbols_to_pop:match ?p1 with Err => _ | OK _ => _ end |- match ?p2 with Err => _ | OK _ => _ end =>
    replace p2 with p1; [destruct p1 as [|[]]|]; intuition
end.
destruct IHsymbols_to_pop as [word1res [word2res [sem_full []]]]; intuition; subst.
exists word1res.
eexists.
exists sem_full.
intuition.
rewrite <- app_assoc; assumption.
simpl; f_equal; f_equal.
apply JMeq_eq.
etransitivity.
apply JMeq_eqrect with (P:=(fun x => x)).
symmetry.
apply JMeq_eqrect with (P:=(fun x => x)).
Qed.

Lemma reduce_step_invariant (stack:stack) (prod:production):
  forall word buffer, word_has_stack_semantics word stack ->
  match reduce_step init stack prod buffer with
    | OK (Accept_sr sem buffer_new) =>
      buffer = buffer_new /\
      inhabited (parse_tree (NT (start_nt init)) word sem)
    | OK (Progress_sr stack_new buffer_new) =>
      buffer = buffer_new /\
      word_has_stack_semantics word stack_new
    | Err | OK Fail_sr => True
  end.
Proof with eauto.
intros.
unfold reduce_step.
pose proof (pop_invariant (prod_rhs_rev prod) [] stack (symbol_semantic_type (NT (prod_lhs prod)))).
revert H0.
generalize (pop_invariant_converter (symbol_semantic_type (NT (prod_lhs prod))) (prod_rhs_rev prod) []).
rewrite <- rev_alt.
intros.
specialize (H0 (prod_action prod) _ [] () H (inhabits Nil_ptl)).
match goal with H0:let action´ := ?a in _ |- _ => replace a with (prod_action´ prod) in H0 end.
simpl in H0.
destruct (pop (prod_rhs_rev prod) stack (prod_action´ prod)) as [|[]]; intuition.
destruct H0 as [word1res [word2res [sem_full]]]; intuition.
destruct H4; apply Non_terminal_pt, inhabits in X.
match goal with X:inhabited (parse_tree _ _ ?u) |- _ => replace u with s0 in X end.
clear sem_full H2.
simpl; destruct (goto_table (state_of_stack init s) (prod_lhs prod)) as [[]|]; intuition; subst.
rewrite app_nil_r in X; revert s0 X; rewrite e0; intro; simpl.
constructor...
destruct s; intuition.
destruct (compare_eqdec (prod_lhs prod) (start_nt init)); intuition.
rewrite app_nil_r in X.
rewrite <- e0.
inversion H0.
destruct X; constructor...
apply JMeq_eq.
etransitivity.
apply JMeq_eqrect with (P:=(fun x => x)).
symmetry.
apply JMeq_eqrect with (P:=(fun x => x)).
Qed.

Lemma step_invariant (stack:stack) (buffer:Stream token):
  forall buffer_tmp,
  (exists word_old,
    buffer = word_old ++ buffer_tmp /\
    word_has_stack_semantics word_old stack) ->
  match step init stack buffer_tmp with
    | OK (Accept_sr sem buffer_new) =>
      exists word_new,
        buffer = word_new ++ buffer_new /\
        inhabited (parse_tree (NT (start_nt init)) word_new sem)
    | OK (Progress_sr stack_new buffer_new) =>
      exists word_new,
        buffer = word_new ++ buffer_new /\
        word_has_stack_semantics word_new stack_new
    | Err | OK Fail_sr => True
  end.
Proof with eauto.
intros.
destruct H, H.
unfold step.
destruct (action_table (state_of_stack init stack)).
pose proof (reduce_step_invariant stack p x buffer_tmp).
destruct (reduce_step init stack p buffer_tmp) as [|[]]; intuition; subst...
destruct buffer_tmp.
unfold Streams.hd.
destruct t.
destruct (l x0); intuition.
exists (x ++ [existT (fun t => symbol_semantic_type (T t)) x0 s])%list.
split.
now rewrite <- app_str_app_assoc; intuition.
apply Cons_stack_whss; intuition.
destruct e; simpl.
now exact (inhabits (Terminal_pt _ _)).
match goal with |- (match reduce_step init stack p ?buff with Err => _ | OK _ => _ end) =>
  pose proof (reduce_step_invariant stack p x buff);
  destruct (reduce_step init stack p buff) as [|[]]; intuition; subst
end...
Qed.

Theorem parse_correct buffer n_steps:
  match parse init buffer n_steps with
    | OK (Parsed_pr sem buffer_new) =>
      exists word_new,
        buffer = word_new ++ buffer_new /\
        inhabited (parse_tree (NT (start_nt init)) word_new sem)
    | _ => True
  end.
Proof.
unfold parse.
assert (exists w, buffer = w ++ buffer /\ word_has_stack_semantics w []).
exists ([]:list token); intuition.
now apply Nil_stack_whss.
revert H.
generalize ([]:stack), buffer at 2 3.
induction n_steps; simpl; intuition.
pose proof (step_invariant _ _ _ H).
destruct (step init s buffer0); simpl; intuition.
destruct s0; intuition.
apply IHn_steps; intuition.
Qed.

End Init.

End Make.