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

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

A correct automaton does not crash *

Section Safety_proof.

Hypothesis safe: safe.

Proposition shift_head_symbs: shift_head_symbs.
Proposition goto_head_symbs: goto_head_symbs.
Proposition shift_past_state: shift_past_state.
Proposition goto_past_state: goto_past_state.
Proposition reduce_ok: reduce_ok.


Variable init : initstate.

Definition state_stack_of_stack (stack:stack) :=
  (List.map
    (fun cell:sigT noninitstate_type => singleton_state_pred (projT1 cell))
    stack ++ [singleton_state_pred init])%list.

Definition symb_stack_of_stack (stack:stack) :=
  List.map
    (fun cell:sigT noninitstate_type => last_symb_of_non_init_state (projT1 cell))
    stack.

Inductive stack_invariant: stack -> Prop :=
  | stack_invariant_constr:
    forall stack,
      prefix (head_symbs_of_state (state_of_stack init stack))
                  (symb_stack_of_stack stack) ->
      prefix_pred (head_states_of_state (state_of_stack init stack))
                  (state_stack_of_stack stack) ->
      stack_invariant_next stack ->
      stack_invariant stack
with stack_invariant_next: stack -> Prop :=
  | stack_invariant_next_nil:
      stack_invariant_next []
  | stack_invariant_next_cons:
    forall state_cur st stack_rec,
      stack_invariant stack_rec ->
      stack_invariant_next (existT _ state_cur st::stack_rec).

Lemma pop_stack_invariant_conserved
  (symbols_to_pop:list symbol) (stack_cur:stack) A action:
  stack_invariant stack_cur ->
  prefix symbols_to_pop (head_symbs_of_state (state_of_stack init stack_cur)) ->
  match pop symbols_to_pop stack_cur (A:=A) action with
    | OK (stack_new, _) =>
      stack_invariant stack_new /\
      state_valid_after_pop
        (state_of_stack init stack_new) symbols_to_pop
        (head_states_of_state (state_of_stack init stack_cur))
    | Err => False
  end.

Lemma prefix_ass:
  forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3.

Lemma prefix_pred_ass:
  forall (l1 l2 l3:list (state->bool)),
  prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3.

Lemma reduce_step_stack_invariant_conserved stack prod buff:
  stack_invariant stack ->
  valid_for_reduce (state_of_stack init stack) prod ->
  match reduce_step init stack prod buff with
    | OK (Fail_sr | Accept_sr _ _) => True
    | OK (Progress_sr stack_new _) => stack_invariant stack_new
    | Err => False
  end.

Lemma step_stack_invariant_conserved (stack:stack) buffer:
  stack_invariant stack ->
  match step init stack buffer with
    | OK (Fail_sr | Accept_sr _ _) => True
    | OK (Progress_sr stack_new _) => stack_invariant stack_new
    | Err => False
  end.

Theorem parse_no_err buffer n_steps:
  parse init buffer n_steps <> Err.

Definition parse_with_safe (buffer:Stream token) (n_steps:nat):
  parse_result init.

End Safety_proof.

End Make.