Require Import Streams.
Require Import ProofIrrelevance.
Require Import Equality.
Require Import List.
Require Import Syntax.
Require Import Alphabet.
Require Import Arith.
Require Grammar.
Require Automaton.
Require Interpreter.
Require Validator_complete.

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

Completeness Proof *

Section Completeness_Proof.

Hypothesis complete: complete.

Proposition nullable_stable: nullable_stable.
Proposition first_stable: first_stable.
Proposition start_future: start_future.
Proposition terminal_shift: terminal_shift.
Proposition end_reduce: end_reduce.
Proposition start_goto: start_goto.
Proposition non_terminal_goto: non_terminal_goto.
Proposition non_terminal_closed: non_terminal_closed.

Lemma nullable_correct:
  forall head sem word, word = [] ->
    parse_tree head word sem -> nullable_symb head = true
with nullable_correct_list:
  forall heads sems word, word = [] ->
    parse_tree_list heads word sems -> nullable_word heads = true.

Lemma first_correct:
  forall head sem word t q, word = t::q ->
  parse_tree head word sem ->
  TerminalSet.In (projT1 t) (first_symb_set head)
with first_correct_list:
  forall heads sems word t q, word = t::q ->
  parse_tree_list heads word sems ->
  TerminalSet.In (projT1 t) (first_word_set heads).

Variable init: initstate.
Variable full_word: list token.
Variable buffer_end: Stream token.
Variable full_sem: symbol_semantic_type (NT (start_nt init)).

Inductive pt_zipper:
  forall (hole_symb:symbol) (hole_word:list token)
         (hole_sem:symbol_semantic_type hole_symb), Type :=
| Top_ptz:
  pt_zipper (NT (start_nt init)) (full_word) (full_sem)
| Cons_ptl_ptz:
  forall {head_symbolt:symbol}
    {wordt:list token}
    {semantic_valuet:symbol_semantic_type head_symbolt},

  forall {head_symbolsq:list symbol}
    {wordq:list token}
    {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)},
    parse_tree_list head_symbolsq wordq semantic_valuesq ->

    ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq)
      (semantic_valuet,semantic_valuesq) ->

    pt_zipper head_symbolt wordt semantic_valuet
with ptl_zipper:
  forall (hole_symbs:list symbol) (hole_word:list token)
         (hole_sems:tuple (map symbol_semantic_type hole_symbs)), Type :=
| Non_terminal_pt_ptlz:
  forall {p:production} {word:list token}
    {semantic_values:tuple (map symbol_semantic_type (rev (prod_rhs_rev p)))},
    pt_zipper (NT (prod_lhs p)) word (uncurry (prod_action p) semantic_values) ->
    ptl_zipper (rev (prod_rhs_rev p)) word semantic_values

| Cons_ptl_ptlz:
  forall {head_symbolt:symbol}
    {wordt:list token}
    {semantic_valuet:symbol_semantic_type head_symbolt},
    parse_tree head_symbolt wordt semantic_valuet ->

  forall {head_symbolsq:list symbol}
    {wordq:list token}
    {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)},

  ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq)
    (semantic_valuet,semantic_valuesq) ->

  ptl_zipper head_symbolsq wordq semantic_valuesq.

Fixpoint ptlz_cost {hole_symbs hole_word hole_sems}
  (ptlz:ptl_zipper hole_symbs hole_word hole_sems) :=
  match ptlz with
    | Non_terminal_pt_ptlz ptz =>
      ptz_cost ptz
    | Cons_ptl_ptlz pt ptlz' =>
      ptlz_cost ptlz'
  end
with ptz_cost {hole_symb hole_word hole_sem}
  (ptz:pt_zipper hole_symb hole_word hole_sem) :=
  match ptz with
    | Top_ptz => 0
    | Cons_ptl_ptz ptl ptlz' =>
      1 + ptl_size ptl + ptlz_cost ptlz'
  end.

Inductive pt_dot: Type :=
| Reduce_ptd: ptl_zipper [] [] () -> pt_dot
| Shift_ptd:
  forall (term:terminal) (sem: symbol_semantic_type (T term))
    {symbolsq wordq semsq},
    parse_tree_list symbolsq wordq semsq ->
    ptl_zipper (T term::symbolsq) (existT (fun t => symbol_semantic_type (T t)) term sem::wordq) (sem, semsq) ->
    pt_dot.

Definition ptd_cost (ptd:pt_dot) :=
  match ptd with
    | Reduce_ptd ptlz => ptlz_cost ptlz
    | Shift_ptd _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz
  end.

Fixpoint ptlz_buffer {hole_symbs hole_word hole_sems}
  (ptlz:ptl_zipper hole_symbs hole_word hole_sems): Stream token :=
  match ptlz with
    | Non_terminal_pt_ptlz ptz =>
      ptz_buffer ptz
    | Cons_ptl_ptlz _ ptlz' =>
      ptlz_buffer ptlz'
  end
with ptz_buffer {hole_symb hole_word hole_sem}
  (ptz:pt_zipper hole_symb hole_word hole_sem): Stream token :=
  match ptz with
    | Top_ptz => buffer_end
    | @Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' =>
      wordq++ptlz_buffer ptlz'
  end.

Definition ptd_buffer (ptd:pt_dot) :=
  match ptd with
    | Reduce_ptd ptlz => ptlz_buffer ptlz
    | @Shift_ptd term sem _ wordq _ _ ptlz =>
      Cons (existT (fun t => symbol_semantic_type (T t)) term sem)
           (wordq ++ ptlz_buffer ptlz)
  end.

Fixpoint ptlz_prod {hole_symbs hole_word hole_sems}
  (ptlz:ptl_zipper hole_symbs hole_word hole_sems): production :=
  match ptlz with
    | @Non_terminal_pt_ptlz prod _ _ _ => prod
    | Cons_ptl_ptlz _ ptlz' =>
      ptlz_prod ptlz'
  end.

Fixpoint ptlz_past {hole_symbs hole_word hole_sems}
  (ptlz:ptl_zipper hole_symbs hole_word hole_sems): list symbol :=
  match ptlz with
    | Non_terminal_pt_ptlz _ => []
    | @Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz'
  end.

Lemma ptlz_past_ptlz_prod:
  forall hole_symbs hole_word hole_sems
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
  rev_append hole_symbs (ptlz_past ptlz) = prod_rhs_rev (ptlz_prod ptlz).

Definition ptlz_state_compat {hole_symbs hole_word hole_sems}
  (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
  (state:state): Prop :=
  state_has_future state (ptlz_prod ptlz) hole_symbs
    (projT1 (Streams.hd (ptlz_buffer ptlz))).

Fixpoint ptlz_stack_compat {hole_symbs hole_word hole_sems}
  (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
  (stack:stack): Prop :=
  ptlz_state_compat ptlz (state_of_stack init stack) /\
  match ptlz with
    | Non_terminal_pt_ptlz ptz =>
      ptz_stack_compat ptz stack
    | @Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' =>
      match stack with
        | [] => False
        | existT _ _ sem'::stackq =>
          ptlz_stack_compat ptlz' stackq /\
          sem ~= sem'
      end
  end
with ptz_stack_compat {hole_symb hole_word hole_sem}
  (ptz:pt_zipper hole_symb hole_word hole_sem)
  (stack:stack): Prop :=
  match ptz with
    | Top_ptz => stack = []
    | Cons_ptl_ptz _ ptlz' =>
      ptlz_stack_compat ptlz' stack
  end.

Lemma ptlz_stack_compat_ptlz_state_compat:
  forall hole_symbs hole_word hole_sems
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
    (stack:stack),
    ptlz_stack_compat ptlz stack -> ptlz_state_compat ptlz (state_of_stack init stack).

Definition ptd_stack_compat (ptd:pt_dot) (stack:stack): Prop :=
  match ptd with
    | Reduce_ptd ptlz => ptlz_stack_compat ptlz stack
    | Shift_ptd _ _ _ ptlz => ptlz_stack_compat ptlz stack
  end.

Fixpoint build_pt_dot {hole_symbs hole_word hole_sems}
    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
    :pt_dot :=
  match ptl in parse_tree_list hole_symbs hole_word hole_sems
    return ptl_zipper hole_symbs hole_word hole_sems -> _
  with
    | Nil_ptl => fun ptlz =>
      Reduce_ptd ptlz
    | Cons_ptl pt ptl' =>
      match pt in parse_tree hole_symb hole_word hole_sem
        return ptl_zipper (hole_symb::_) (hole_word++_) (hole_sem,_) -> _
      with
        | Terminal_pt term sem => fun ptlz =>
          Shift_ptd term sem ptl' ptlz
        | Non_terminal_pt ptl'' => fun ptlz =>
          build_pt_dot ptl''
            (Non_terminal_pt_ptlz (Cons_ptl_ptz ptl' ptlz))
      end
  end ptlz.

Lemma build_pt_dot_cost:
  forall hole_symbs hole_word hole_sems
    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
    ptd_cost (build_pt_dot ptl ptlz) = ptl_size ptl + ptlz_cost ptlz.

Lemma build_pt_dot_buffer:
  forall hole_symbs hole_word hole_sems
    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
    ptd_buffer (build_pt_dot ptl ptlz) = hole_word ++ ptlz_buffer ptlz.

Lemma ptd_stack_compat_build_pt_dot:
  forall hole_symbs hole_word hole_sems
    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
    (stack:stack),
  ptlz_stack_compat ptlz stack ->
  ptd_stack_compat (build_pt_dot ptl ptlz) stack.

Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems}
  (ptl:parse_tree_list hole_symbs hole_word hole_sems)
  (ptlz:ptl_zipper hole_symbs hole_word hole_sems):
    { word:_ & { sem:_ &
      (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem *
       parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } :=
  match ptlz in ptl_zipper hole_symbs hole_word hole_sems
    return parse_tree_list hole_symbs hole_word hole_sems ->
    { word:_ & { sem:_ &
      (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem *
       parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } }
  with
    | @Non_terminal_pt_ptlz prod word sem ptz => fun ptl =>
      let sem := uncurry (prod_action prod) sem in
      existT _ word (existT _ sem (ptz, Non_terminal_pt ptl))
    | Cons_ptl_ptlz pt ptlz' => fun ptl =>
      pop_ptlz (Cons_ptl pt ptl) ptlz'
  end ptl.

Lemma pop_ptlz_cost:
  forall hole_symbs hole_word hole_sems
    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
  let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in
  ptlz_cost ptlz = ptz_cost ptz.

Lemma pop_ptlz_buffer:
  forall hole_symbs hole_word hole_sems
    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
  let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in
  ptlz_buffer ptlz = ptz_buffer ptz.

Lemma pop_ptlz_pop_stack_compat_converter:
  forall A hole_symbs hole_word hole_sems (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
  arrows_left (map symbol_semantic_type (rev (prod_rhs_rev (ptlz_prod ptlz)))) A =
  arrows_left (map symbol_semantic_type hole_symbs)
    (arrows_right A (map symbol_semantic_type (ptlz_past ptlz))).

Lemma pop_ptlz_pop_stack_compat:
  forall hole_symbs hole_word hole_sems
    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
    (stack:stack),

    ptlz_stack_compat ptlz stack ->

    let action' :=
      eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _
      (pop_ptlz_pop_stack_compat_converter _ _ _ _ _)
    in
    let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in
      match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with
        | OK (stack', sem') =>
           ptz_stack_compat ptz stack' /\ sem = sem'
        | Err => True
      end.

Definition next_ptd (ptd:pt_dot): option pt_dot :=
  match ptd with
    | Shift_ptd term sem ptl ptlz =>
      Some (build_pt_dot ptl (Cons_ptl_ptlz (Terminal_pt term sem) ptlz))
    | Reduce_ptd ptlz =>
      let 'existT _ _ (existT _ _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in
      match ptz in pt_zipper sym _ _ return parse_tree sym _ _ -> _ with
        | Top_ptz => fun pt => None
        | Cons_ptl_ptz ptl ptlz' =>
          fun pt => Some (build_pt_dot ptl (Cons_ptl_ptlz pt ptlz'))
      end pt
  end.

Lemma next_ptd_cost:
  forall ptd,
    match next_ptd ptd with
      | None => ptd_cost ptd = 0
      | Some ptd' => ptd_cost ptd = S (ptd_cost ptd')
    end.

Lemma reduce_step_next_ptd:
  forall (ptlz:ptl_zipper [] [] ()) (stack:stack),
    ptlz_stack_compat ptlz stack ->
    match reduce_step init stack (ptlz_prod ptlz) (ptlz_buffer ptlz) with
      | OK Fail_sr =>
        False
      | OK (Accept_sr sem buffer) =>
        sem = full_sem /\ buffer = buffer_end /\ next_ptd (Reduce_ptd ptlz) = None
      | OK (Progress_sr stack buffer) =>
        match next_ptd (Reduce_ptd ptlz) with
          | None => False
          | Some ptd =>
            ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd
        end
      | Err =>
        True
    end.

Lemma step_next_ptd:
  forall (ptd:pt_dot) (stack:stack),
    ptd_stack_compat ptd stack ->
    match step init stack (ptd_buffer ptd) with
      | OK Fail_sr =>
        False
      | OK (Accept_sr sem buffer) =>
        sem = full_sem /\ buffer = buffer_end /\ next_ptd ptd = None
      | OK (Progress_sr stack buffer) =>
        match next_ptd ptd with
          | None => False
          | Some ptd =>
            ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd
        end
      | Err =>
        True
    end.

Lemma parse_fix_complete:
  forall (ptd:pt_dot) (stack:stack) (n_steps:nat),
    ptd_stack_compat ptd stack ->
    match parse_fix init stack (ptd_buffer ptd) n_steps with
      | OK (Parsed_pr sem_res buffer_end_res) =>
        sem_res = full_sem /\ buffer_end_res = buffer_end /\
         S (ptd_cost ptd) <= n_steps
      | OK Fail_pr => False
      | OK Timeout_pr => n_steps < S (ptd_cost ptd)
      | Err => True
    end.

Variable full_pt: parse_tree (NT (start_nt init)) full_word full_sem.

Definition init_ptd :=
  match full_pt in parse_tree head full_word full_sem return
    pt_zipper head full_word full_sem ->
    match head return Type with | T _ => unit | NT _ => pt_dot end
  with
    | Terminal_pt _ _ => fun _ => ()
    | Non_terminal_pt ptl =>
      fun top => build_pt_dot ptl (Non_terminal_pt_ptlz top)
  end Top_ptz.

Lemma init_ptd_compat:
  ptd_stack_compat init_ptd [].

Lemma init_ptd_cost:
  S (ptd_cost init_ptd) = pt_size full_pt.

Lemma init_ptd_buffer:
  ptd_buffer init_ptd = full_word ++ buffer_end.

Theorem parse_complete n_steps:
  match parse init (full_word ++ buffer_end) n_steps with
    | OK (Parsed_pr sem_res buffer_end_res) =>
      sem_res = full_sem /\ buffer_end_res = buffer_end /\
       pt_size full_pt <= n_steps
    | OK Fail_pr => False
    | OK Timeout_pr => n_steps < pt_size full_pt
    | Err => True
  end.

End Completeness_Proof.

End Make.