diff options
Diffstat (limited to 'cparser/validator/Interpreter_complete.v')
| -rw-r--r-- | cparser/validator/Interpreter_complete.v | 685 |
1 files changed, 685 insertions, 0 deletions
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v new file mode 100644 index 0000000..3b922f7 --- /dev/null +++ b/cparser/validator/Interpreter_complete.v @@ -0,0 +1,685 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Streams. +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. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition first_stable: first_stable. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition start_future: start_future. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition terminal_shift: terminal_shift. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition end_reduce: end_reduce. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition start_goto: start_goto. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition non_terminal_goto: non_terminal_goto. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition non_terminal_closed: non_terminal_closed. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. + +(** If the nullable predicate has been validated, then it is correct. **) +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. +Proof with eauto. +intros. +destruct X. +congruence. +apply nullable_stable... +intros. +destruct X; simpl... +apply andb_true_intro. +apply app_eq_nil in H; destruct H; split... +Qed. + +(** If the first predicate has been validated, then it is correct. **) +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). +Proof with eauto. +intros. +destruct X. +inversion H; subst. +apply TerminalSet.singleton_2, compare_refl... +apply first_stable... +intros. +destruct X. +congruence. +simpl. +case_eq wordt; intros. +erewrite nullable_correct... +apply TerminalSet.union_3. +subst... +rewrite H0 in *; inversion H; destruct H2. +destruct (nullable_symb head_symbolt)... +apply TerminalSet.union_2... +Qed. + +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). +Proof. +fix 4. +destruct ptlz; simpl. +rewrite <- rev_alt, rev_involutive; reflexivity. +apply (ptlz_past_ptlz_prod _ _ _ ptlz). +Qed. + +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). +Proof. +destruct ptlz; simpl; intuition. +Qed. + +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. +Proof. +fix 4. +destruct ptl; intros. +reflexivity. +destruct p. +reflexivity. +simpl; rewrite build_pt_dot_cost. +simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity. +Qed. + +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. +Proof. +fix 4. +destruct ptl; intros. +reflexivity. +destruct p. +reflexivity. +simpl; rewrite build_pt_dot_buffer. +apply app_str_app_assoc. +Qed. + +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. +Proof. +fix 4. +destruct ptl; intros. +eauto. +destruct p. +eauto. +simpl. +apply ptd_stack_compat_build_pt_dot. +split. +apply ptlz_stack_compat_ptlz_state_compat, non_terminal_closed in H. +apply H; clear H; eauto. +destruct wordq. +right; split. +eauto. +eapply nullable_correct_list; eauto. +left. +eapply first_correct_list; eauto. +eauto. +Qed. + +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. +Proof. +fix 5. +destruct ptlz. +reflexivity. +simpl; apply pop_ptlz_cost. +Qed. + +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. +Proof. +fix 5. +destruct ptlz. +reflexivity. +simpl; apply pop_ptlz_buffer. +Qed. + +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))). +Proof. +intros. +rewrite <- ptlz_past_ptlz_prod. +unfold arrows_right, arrows_left. +rewrite rev_append_rev, map_rev, map_app, map_rev, <- fold_left_rev_right, rev_involutive, fold_right_app. +rewrite fold_left_rev_right. +reflexivity. +Qed. + +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. +Proof. +Opaque AlphabetComparable AlphabetComparableUsualEq. +fix 5. +destruct ptlz. intros; simpl. +split. +apply H. +f_equal. +apply JMeq_eq, JMeq_sym, JMeq_eqrect with (P:=fun x => x). +simpl; intros; destruct stack0. +destruct (proj2 H). +simpl in H; destruct H. +destruct s as (state, sem'). +destruct H0. +specialize (pop_ptlz_pop_stack_compat _ _ _ (Cons_ptl p ptl) ptlz _ H0). +destruct (pop_ptlz (Cons_ptl p ptl) ptlz) as [word [sem []]]. +destruct (compare_eqdec (last_symb_of_non_init_state state) head_symbolt); intuition. +eapply JMeq_sym, JMeq_trans, JMeq_sym, JMeq_eq in H1; [|apply JMeq_eqrect with (e:=e)]. +rewrite <- H1. +simpl in pop_ptlz_pop_stack_compat. +erewrite proof_irrelevance with (p1:=pop_ptlz_pop_stack_compat_converter _ _ _ _ _). +apply pop_ptlz_pop_stack_compat. +Transparent AlphabetComparable AlphabetComparableUsualEq. +Qed. + +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. +Proof. +destruct ptd. unfold next_ptd. +pose proof (pop_ptlz_cost _ _ _ Nil_ptl p). +destruct (pop_ptlz Nil_ptl p) as [word[sem[[]]]]. +assumption. +rewrite build_pt_dot_cost. +assumption. +simpl; rewrite build_pt_dot_cost; reflexivity. +Qed. + +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. +Proof. +intros. +unfold reduce_step, next_ptd. +apply pop_ptlz_pop_stack_compat with (ptl:=Nil_ptl) in H. +pose proof (pop_ptlz_buffer _ _ _ Nil_ptl ptlz). +destruct (pop_ptlz Nil_ptl ptlz) as [word [sem [ptz pt]]]. +rewrite H0; clear H0. +revert H. +match goal with + |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end => + replace p1 with p2; [destruct p2 as [|[]]; intros|] +end. +assumption. +simpl. +destruct H; subst. +generalize dependent s0. +generalize (prod_lhs (ptlz_prod ptlz)); clear ptlz stack0. +dependent destruction ptz; intros. +simpl in H; subst; simpl. +pose proof start_goto; unfold Valid.start_goto in H; rewrite H. +destruct (compare_eqdec (start_nt init) (start_nt init)); intuition. +apply JMeq_eq, JMeq_eqrect with (P:=fun nt => symbol_semantic_type (NT nt)). +pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). +apply non_terminal_goto in H0. +destruct (goto_table (state_of_stack init s) n) as [[]|]; intuition. +apply ptd_stack_compat_build_pt_dot; simpl; intuition. +symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type). +symmetry; apply build_pt_dot_buffer. +destruct s; intuition. +simpl in H; apply ptlz_stack_compat_ptlz_state_compat in H. +destruct (H0 _ _ _ H eq_refl). +generalize (pop_ptlz_pop_stack_compat_converter (symbol_semantic_type (NT (prod_lhs (ptlz_prod ptlz)))) _ _ _ ptlz). +pose proof (ptlz_past_ptlz_prod _ _ _ ptlz); simpl in H. +rewrite H; clear H. +intro; f_equal; simpl. +apply JMeq_eq. +etransitivity. +apply JMeq_eqrect with (P:=fun x => x). +symmetry. +apply JMeq_eqrect with (P:=fun x => x). +Qed. + +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. +Proof. +intros. +destruct ptd. +pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). +apply end_reduce in H0. +unfold step. +destruct (action_table (state_of_stack init stack0)). +rewrite H0 by reflexivity. +apply reduce_step_next_ptd; assumption. +simpl; destruct (Streams.hd (ptlz_buffer p)); simpl in H0. +destruct (l x); intuition; rewrite H1. +apply reduce_step_next_ptd; assumption. +pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). +apply terminal_shift in H0. +unfold step. +destruct (action_table (state_of_stack init stack0)); intuition. +simpl; destruct (Streams.hd (ptlz_buffer p0)) as [] eqn:?. +destruct (l term); intuition. +apply ptd_stack_compat_build_pt_dot; simpl; intuition. +unfold ptlz_state_compat; simpl; destruct Heqt; assumption. +symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type). +rewrite build_pt_dot_buffer; reflexivity. +Qed. + +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. +Proof. +fix 3. +destruct n_steps; intros; simpl. +apply lt_0_Sn. +apply step_next_ptd in H. +pose proof (next_ptd_cost ptd). +destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition. +rewrite H3 in H0; rewrite H0. +apply le_n_S, le_0_n. +destruct (next_ptd ptd); intuition; subst. +eapply parse_fix_complete with (n_steps:=n_steps) in H1. +rewrite H0. +destruct (parse_fix init s (ptd_buffer p) n_steps) as [|[]]; try assumption. +apply lt_n_S; assumption. +destruct H1 as [H1 []]; split; [|split]; try assumption. +apply le_n_S; assumption. +Qed. + +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 []. +Proof. +unfold init_ptd. +assert (ptz_stack_compat Top_ptz []) by reflexivity. +pose proof (start_future init); revert H0. +generalize dependent Top_ptz. +generalize dependent full_word. +generalize full_sem. +generalize (start_nt init). +dependent destruction full_pt0. +intros. +apply ptd_stack_compat_build_pt_dot; simpl; intuition. +apply H0; reflexivity. +Qed. + +Lemma init_ptd_cost: + S (ptd_cost init_ptd) = pt_size full_pt. +Proof. +unfold init_ptd. +assert (ptz_cost Top_ptz = 0) by reflexivity. +generalize dependent Top_ptz. +generalize dependent full_word. +generalize full_sem. +generalize (start_nt init). +dependent destruction full_pt0. +intros. +rewrite build_pt_dot_cost; simpl. +rewrite H, plus_0_r; reflexivity. +Qed. + +Lemma init_ptd_buffer: + ptd_buffer init_ptd = full_word ++ buffer_end. +Proof. +unfold init_ptd. +assert (ptz_buffer Top_ptz = buffer_end) by reflexivity. +generalize dependent Top_ptz. +generalize dependent full_word. +generalize full_sem. +generalize (start_nt init). +dependent destruction full_pt0. +intros. +rewrite build_pt_dot_buffer; simpl. +rewrite H; reflexivity. +Qed. + +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. +Proof. +pose proof (parse_fix_complete init_ptd [] n_steps init_ptd_compat). +rewrite init_ptd_buffer, init_ptd_cost in H. +apply H. +Qed. + +End Completeness_Proof. + +End Make. |