diff options
Diffstat (limited to 'MenhirLib/Interpreter_complete.v')
| -rw-r--r-- | MenhirLib/Interpreter_complete.v | 825 |
1 files changed, 825 insertions, 0 deletions
diff --git a/MenhirLib/Interpreter_complete.v b/MenhirLib/Interpreter_complete.v new file mode 100644 index 00000000..ec69592b --- /dev/null +++ b/MenhirLib/Interpreter_complete.v @@ -0,0 +1,825 @@ +(****************************************************************************) +(* *) +(* Menhir *) +(* *) +(* Jacques-Henri Jourdan, CNRS, LRI, Université Paris Sud *) +(* *) +(* Copyright Inria. All rights reserved. This file is distributed under *) +(* the terms of the GNU Lesser General Public License as published by the *) +(* Free Software Foundation, either version 3 of the License, or (at your *) +(* option) any later version, as described in the file LICENSE. *) +(* *) +(****************************************************************************) + +From Coq Require Import List Syntax Arith. +From Coq.ssr Require Import ssreflect. +Require Import Alphabet Grammar. +Require Automaton Interpreter 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 safe: Inter.ValidSafe.safe. +Hypothesis complete: complete. + +(* Properties of the automaton deduced from completeness validation. *) +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 head word : + word = [] -> parse_tree head word -> nullable_symb head = true +with nullable_correct_list heads word : + word = [] -> + parse_tree_list heads word -> nullable_word heads = true. +Proof. + - destruct 2=>//. assert (Hnull := nullable_stable prod). + erewrite nullable_correct_list in Hnull; eauto. + - intros Hword. destruct 1=>//=. destruct (app_eq_nil _ _ Hword). + eauto using andb_true_intro. +Qed. + +(** Auxiliary lemma for first_correct. *) +Lemma first_word_set_app t word1 word2 : + TerminalSet.In t (first_word_set (word1 ++ word2)) <-> + TerminalSet.In t (first_word_set word1) \/ + TerminalSet.In t (first_word_set word2) /\ nullable_word (rev word1) = true. +Proof. + induction word1 as [|s word1 IH]=>/=. + - split; [tauto|]. move=>[/TerminalSet.empty_1 ?|[? _]]//. + - rewrite /nullable_word forallb_app /=. destruct nullable_symb=>/=. + + rewrite Bool.andb_true_r. split. + * move=>/TerminalSet.union_1. rewrite IH. + move=>[?|[?|[??]]]; auto using TerminalSet.union_2, TerminalSet.union_3. + * destruct IH. + move=>[/TerminalSet.union_1 [?|?]|[??]]; + auto using TerminalSet.union_2, TerminalSet.union_3. + + rewrite Bool.andb_false_r. by intuition. +Qed. + +(** If the first predicate has been validated, then it is correct. **) +Lemma first_correct head word t q : + word = t::q -> + parse_tree head word -> + TerminalSet.In (token_term t) (first_symb_set head) +with first_correct_list heads word t q : + word = t::q -> + parse_tree_list heads word -> + TerminalSet.In (token_term t) (first_word_set (rev' heads)). +Proof. + - intros Hword. destruct 1=>//. + + inversion Hword. subst. apply TerminalSet.singleton_2, compare_refl. + + eapply first_stable. eauto. + - intros Hword. destruct 1 as [|symq wordq ptl symt wordt pt]=>//=. + rewrite /rev' -rev_alt /= first_word_set_app /= rev_involutive rev_alt. + destruct wordq; [right|left]. + + destruct nullable_symb; eauto using TerminalSet.union_2, nullable_correct_list. + + inversion Hword. subst. fold (rev' symq). eauto. +Qed. + +(** A PTL is compatible with a stack if the top of the stack contains + data representing to this PTL. *) +Fixpoint ptl_stack_compat {symbs word} + (stk0 : stack) (ptl : parse_tree_list symbs word) (stk : stack) : Prop := + match ptl with + | Nil_ptl => stk0 = stk + | @Cons_ptl _ _ ptl sym _ pt => + match stk with + | [] => False + | existT _ _ sem::stk => + ptl_stack_compat stk0 ptl stk /\ + exists e, + sem = eq_rect _ symbol_semantic_type (pt_sem pt) _ e + end + end. + +(** .. and when a PTL is compatible with a stack, then calling the pop + function return the semantic value of this PTL. *) +Lemma pop_stack_compat_pop_spec {A symbs word} + (ptl:parse_tree_list symbs word) (stk:stack) (stk0:stack) action : + ptl_stack_compat stk0 ptl stk -> + pop_spec symbs stk action stk0 (ptl_sem (A:=A) ptl action). +Proof. + revert stk. induction ptl=>stk /= Hstk. + - subst. constructor. + - destruct stk as [|[st sem] stk]=>//. destruct Hstk as [Hstk [??]]. subst. + simpl. constructor. eauto. +Qed. + +Variable init: initstate. + +(** In order to prove compleness, we first fix a word to be parsed + together with the content of the parser at the end of the parsing. *) +Variable full_word: list token. +Variable buffer_end: buffer. + +(** Completeness is proved by following the traversal of the parse + tree which is performed by the parser. Each step of parsing + correspond to one step of traversal. In order to represent the state + of the traversal, we define the notion of "dotted" parse tree, which + is a parse tree with one dot on one of its node. The place of the + dot represents the place of the next action to be executed. + + Such a dotted parse tree is decomposed into two part: a "regular" + parse tree, which is the parse tree placed under the dot, and a + "parse tree zipper", which is the part of the parse tree placed + above the dot. Therefore, a parse tree zipper is a parse tree with a + hole. Moreover, for easier manipulation, a parse tree zipper is + represented "upside down". That is, the root of the parse tree is + actually a leaf of the zipper, while the root of the zipper is the + hole. + *) +Inductive pt_zipper: + forall (hole_symb:symbol) (hole_word:list token), Type := +| Top_ptz: + pt_zipper (NT (start_nt init)) full_word +| Cons_ptl_ptz: + forall {head_symbolsq:list symbol} {wordq:list token}, + parse_tree_list head_symbolsq wordq -> + + forall {head_symbolt:symbol} {wordt:list token}, + + ptl_zipper (head_symbolt::head_symbolsq) (wordq++wordt) -> + pt_zipper head_symbolt wordt +with ptl_zipper: + forall (hole_symbs:list symbol) (hole_word:list token), Type := +| Non_terminal_pt_ptlz: + forall {p:production} {word:list token}, + pt_zipper (NT (prod_lhs p)) word -> + ptl_zipper (prod_rhs_rev p) word + +| Cons_ptl_ptlz: + forall {head_symbolsq:list symbol} {wordq:list token}, + + forall {head_symbolt:symbol} {wordt:list token}, + parse_tree head_symbolt wordt -> + + ptl_zipper (head_symbolt::head_symbolsq) (wordq++wordt) -> + + ptl_zipper head_symbolsq wordq. + +(** A dotted parse tree is the combination of a parse tree zipper with + a parse tree. It can be intwo flavors, depending on which is the next + action to be executed (shift or reduce). *) +Inductive pt_dot: Type := +| Reduce_ptd: forall {prod word}, + parse_tree_list (prod_rhs_rev prod) word -> + pt_zipper (NT (prod_lhs prod)) word -> + pt_dot +| Shift_ptd: forall (tok : token) {symbolsq wordq}, + parse_tree_list symbolsq wordq -> + ptl_zipper (T (token_term tok)::symbolsq) (wordq++[tok]) -> + pt_dot. + +(** We can compute the full semantic value of a parse tree when + represented as a dotted ptd. *) + +Fixpoint ptlz_sem {hole_symbs hole_word} + (ptlz:ptl_zipper hole_symbs hole_word) : + (forall A, arrows_right A (map symbol_semantic_type hole_symbs) -> A) -> + (symbol_semantic_type (NT (start_nt init))) := + match ptlz with + | @Non_terminal_pt_ptlz prod _ ptz => + fun k => ptz_sem ptz (k _ (prod_action prod)) + | Cons_ptl_ptlz pt ptlz => + fun k => ptlz_sem ptlz (fun _ f => k _ (f (pt_sem pt))) + end +with ptz_sem {hole_symb hole_word} + (ptz:pt_zipper hole_symb hole_word): + symbol_semantic_type hole_symb -> symbol_semantic_type (NT (start_nt init)) := + match ptz with + | Top_ptz => fun sem => sem + | Cons_ptl_ptz ptl ptlz => + fun sem => ptlz_sem ptlz (fun _ f => ptl_sem ptl (f sem)) + end. + +Definition ptd_sem (ptd : pt_dot) := + match ptd with + | @Reduce_ptd prod _ ptl ptz => + ptz_sem ptz (ptl_sem ptl (prod_action prod)) + | Shift_ptd tok ptl ptlz => + ptlz_sem ptlz (fun _ f => ptl_sem ptl (f (token_sem tok))) + end. + +(** The buffer associated with a dotted parse tree corresponds to the + buffer left to be read by the parser when at the state represented + by the dotted parse tree. *) +Fixpoint ptlz_buffer {hole_symbs hole_word} + (ptlz:ptl_zipper hole_symbs hole_word): buffer := + match ptlz with + | Non_terminal_pt_ptlz ptz => + ptz_buffer ptz + | @Cons_ptl_ptlz _ _ _ wordt _ ptlz' => + wordt ++ ptlz_buffer ptlz' + end +with ptz_buffer {hole_symb hole_word} + (ptz:pt_zipper hole_symb hole_word): buffer := + match ptz with + | Top_ptz => buffer_end + | Cons_ptl_ptz _ ptlz => + ptlz_buffer ptlz + end. + +Definition ptd_buffer (ptd:pt_dot) := + match ptd with + | Reduce_ptd _ ptz => ptz_buffer ptz + | @Shift_ptd tok _ wordq _ ptlz => (tok::ptlz_buffer ptlz)%buf + end. + +(** We are now ready to define the main invariant of the proof of + completeness: we need to specify when a stack is compatible with a + dotted parse tree. Informally, a stack is compatible with a dotted + parse tree when it is the concatenation stack fragments which are + compatible with each of the partially recognized productions + appearing in the parse tree zipper. Moreover, the head of each of + these stack fragment contains a state which has an item predicted by + the corresponding zipper. + + More formally, the compatibility relation first needs the following + auxiliary definitions: *) +Fixpoint ptlz_prod {hole_symbs hole_word} + (ptlz:ptl_zipper hole_symbs hole_word): production := + match ptlz with + | @Non_terminal_pt_ptlz prod _ _ => prod + | Cons_ptl_ptlz _ ptlz' => ptlz_prod ptlz' + end. + +Fixpoint ptlz_future {hole_symbs hole_word} + (ptlz:ptl_zipper hole_symbs hole_word): list symbol := + match ptlz with + | Non_terminal_pt_ptlz _ => [] + | @Cons_ptl_ptlz _ _ s _ _ ptlz' => s::ptlz_future ptlz' + end. + +Fixpoint ptlz_lookahead {hole_symbs hole_word} + (ptlz:ptl_zipper hole_symbs hole_word) : terminal := + match ptlz with + | Non_terminal_pt_ptlz ptz => token_term (buf_head (ptz_buffer ptz)) + | Cons_ptl_ptlz _ ptlz' => ptlz_lookahead ptlz' + end. + +Fixpoint ptz_stack_compat {hole_symb hole_word} + (stk : stack) (ptz : pt_zipper hole_symb hole_word) : Prop := + match ptz with + | Top_ptz => stk = [] + | Cons_ptl_ptz ptl ptlz => + exists stk0, + state_has_future (state_of_stack init stk) (ptlz_prod ptlz) + (hole_symb::ptlz_future ptlz) (ptlz_lookahead ptlz) /\ + ptl_stack_compat stk0 ptl stk /\ + ptlz_stack_compat stk0 ptlz + end +with ptlz_stack_compat {hole_symbs hole_word} + (stk : stack) (ptlz : ptl_zipper hole_symbs hole_word) : Prop := + match ptlz with + | Non_terminal_pt_ptlz ptz => ptz_stack_compat stk ptz + | Cons_ptl_ptlz _ ptlz => ptlz_stack_compat stk ptlz + end. + +Definition ptd_stack_compat (ptd:pt_dot) (stk:stack): Prop := + match ptd with + | @Reduce_ptd prod _ ptl ptz => + exists stk0, + state_has_future (state_of_stack init stk) prod [] + (token_term (buf_head (ptz_buffer ptz))) /\ + ptl_stack_compat stk0 ptl stk /\ + ptz_stack_compat stk0 ptz + | Shift_ptd tok ptl ptlz => + exists stk0, + state_has_future (state_of_stack init stk) (ptlz_prod ptlz) + (T (token_term tok) :: ptlz_future ptlz) (ptlz_lookahead ptlz) /\ + ptl_stack_compat stk0 ptl stk /\ + ptlz_stack_compat stk0 ptlz + end. + +Lemma ptz_stack_compat_cons_state_has_future {symbsq wordq symbt wordt} stk + (ptl : parse_tree_list symbsq wordq) + (ptlz : ptl_zipper (symbt :: symbsq) (wordq ++ wordt)) : + ptz_stack_compat stk (Cons_ptl_ptz ptl ptlz) -> + state_has_future (state_of_stack init stk) (ptlz_prod ptlz) + (symbt::ptlz_future ptlz) (ptlz_lookahead ptlz). +Proof. move=>[stk0 [? [? ?]]] //. Qed. + +Lemma ptlz_future_ptlz_prod hole_symbs hole_word + (ptlz:ptl_zipper hole_symbs hole_word) : + rev_append (ptlz_future ptlz) hole_symbs = prod_rhs_rev (ptlz_prod ptlz). +Proof. induction ptlz=>//=. Qed. + +Lemma ptlz_future_first {symbs word} (ptlz : ptl_zipper symbs word) : + TerminalSet.In (token_term (buf_head (ptlz_buffer ptlz))) + (first_word_set (ptlz_future ptlz)) \/ + token_term (buf_head (ptlz_buffer ptlz)) = ptlz_lookahead ptlz /\ + nullable_word (ptlz_future ptlz) = true. +Proof. + induction ptlz as [|??? [|tok] pt ptlz IH]; [by auto| |]=>/=. + - rewrite (nullable_correct _ _ eq_refl pt). + destruct IH as [|[??]]; [left|right]=>/=; auto using TerminalSet.union_3. + - left. destruct nullable_symb; eauto using TerminalSet.union_2, first_correct. +Qed. + +(** We now want to define what is the next dotted parse tree which is + to be handled after one action. Such dotted parse is built in two + steps: Not only we have to perform the action by completing the + parse tree, but we also have to prepare for the following step by + moving the dot down to place it in front of the next action to be + performed. +*) +Fixpoint build_pt_dot_from_pt {symb word} + (pt : parse_tree symb word) (ptz : pt_zipper symb word) + : pt_dot := + match pt in parse_tree symb word + return pt_zipper symb word -> pt_dot + with + | Terminal_pt tok => + fun ptz => + let X := + match ptz in pt_zipper symb word + return match symb with T term => True | NT _ => False end -> + { symbsq : list symbol & + { wordq : list token & + (parse_tree_list symbsq wordq * + ptl_zipper (symb :: symbsq) (wordq ++ word))%type } } + with + | Top_ptz => fun F => False_rect _ F + | Cons_ptl_ptz ptl ptlz => fun _ => + existT _ _ (existT _ _ (ptl, ptlz)) + end I + in + Shift_ptd tok (fst (projT2 (projT2 X))) (snd (projT2 (projT2 X))) + | Non_terminal_pt prod ptl => fun ptz => + let is_notnil := + match ptl in parse_tree_list w _ + return option (match w return Prop with [] => False | _ => True end) + with + | Nil_ptl => None + | _ => Some I + end + in + match is_notnil with + | None => Reduce_ptd ptl ptz + | Some H => build_pt_dot_from_pt_rec ptl H (Non_terminal_pt_ptlz ptz) + end + end ptz +with build_pt_dot_from_pt_rec {symbs word} + (ptl : parse_tree_list symbs word) + (Hsymbs : match symbs with [] => False | _ => True end) + (ptlz : ptl_zipper symbs word) + : pt_dot := + match ptl in parse_tree_list symbs word + return match symbs with [] => False | _ => True end -> + ptl_zipper symbs word -> + pt_dot + with + | Nil_ptl => fun Hsymbs _ => False_rect _ Hsymbs + | Cons_ptl ptl' pt => fun _ => + match ptl' in parse_tree_list symbsq wordq + return parse_tree_list symbsq wordq -> + ptl_zipper (_ :: symbsq) (wordq ++ _) -> + pt_dot + with + | Nil_ptl => fun _ ptlz => + build_pt_dot_from_pt pt (Cons_ptl_ptz Nil_ptl ptlz) + | _ => fun ptl' ptlz => + build_pt_dot_from_pt_rec ptl' I (Cons_ptl_ptlz pt ptlz) + end ptl' + end Hsymbs ptlz. + +Definition build_pt_dot_from_ptl {symbs word} + (ptl : parse_tree_list symbs word) + (ptlz : ptl_zipper symbs word) + : pt_dot := + match ptlz in ptl_zipper symbs word + return parse_tree_list symbs word -> pt_dot + with + | Non_terminal_pt_ptlz ptz => fun ptl => + Reduce_ptd ptl ptz + | Cons_ptl_ptlz pt ptlz => fun ptl => + build_pt_dot_from_pt pt (Cons_ptl_ptz ptl ptlz) + end ptl. + +Definition next_ptd (ptd:pt_dot) : option pt_dot := + match ptd with + | Shift_ptd tok ptl ptlz => + Some (build_pt_dot_from_ptl (Cons_ptl ptl (Terminal_pt tok)) ptlz) + | Reduce_ptd ptl ptz => + match ptz in pt_zipper symb word + return parse_tree symb word -> _ + with + | Top_ptz => fun _ => None + | Cons_ptl_ptz ptl' ptlz => fun pt => + Some (build_pt_dot_from_ptl (Cons_ptl ptl' pt) ptlz) + end (Non_terminal_pt _ ptl) + end. + +Fixpoint next_ptd_iter (ptd:pt_dot) (log_n_steps:nat) : option pt_dot := + match log_n_steps with + | O => next_ptd ptd + | S log_n_steps => + match next_ptd_iter ptd log_n_steps with + | None => None + | Some ptd => next_ptd_iter ptd log_n_steps + end + end. + +(** We prove that these functions behave well w.r.t. semantic values. *) +Lemma sem_build_from_pt {symb word} + (pt : parse_tree symb word) (ptz : pt_zipper symb word) : + ptz_sem ptz (pt_sem pt) + = ptd_sem (build_pt_dot_from_pt pt ptz) +with sem_build_from_pt_rec {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) + Hsymbs : + ptlz_sem ptlz (fun _ f => ptl_sem ptl f) + = ptd_sem (build_pt_dot_from_pt_rec ptl Hsymbs ptlz). +Proof. + - destruct pt as [tok|prod word ptl]=>/=. + + revert ptz. generalize [tok]. + generalize (token_sem tok). generalize I. + change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1. + generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz. + + match goal with + | |- context [match ?X with Some H => _ | None => _ end] => destruct X=>// + end. + by rewrite -sem_build_from_pt_rec. + - destruct ptl; [contradiction|]. + specialize (sem_build_from_pt_rec _ _ ptl)=>/=. destruct ptl. + + by rewrite -sem_build_from_pt. + + by rewrite -sem_build_from_pt_rec. +Qed. + +Lemma sem_build_from_ptl {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) : + ptlz_sem ptlz (fun _ f => ptl_sem ptl f) + = ptd_sem (build_pt_dot_from_ptl ptl ptlz). +Proof. destruct ptlz=>//=. by rewrite -sem_build_from_pt. Qed. + +Lemma sem_next_ptd (ptd : pt_dot) : + match next_ptd ptd with + | None => True + | Some ptd' => ptd_sem ptd = ptd_sem ptd' + end. +Proof. + destruct ptd as [prod word ptl ptz|tok symbs word ptl ptlz] =>/=. + - change (ptl_sem ptl (prod_action prod)) + with (pt_sem (Non_terminal_pt prod ptl)). + generalize (Non_terminal_pt prod ptl). clear ptl. + destruct ptz as [|?? ptl ?? ptlz]=>// pt. by rewrite -sem_build_from_ptl. + - by rewrite -sem_build_from_ptl. +Qed. + +Lemma sem_next_ptd_iter (ptd : pt_dot) (log_n_steps : nat) : + match next_ptd_iter ptd log_n_steps with + | None => True + | Some ptd' => ptd_sem ptd = ptd_sem ptd' + end. +Proof. + revert ptd. + induction log_n_steps as [|log_n_steps IH]; [by apply sem_next_ptd|]=>/= ptd. + assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|]=>//. + specialize (IH ptd'). destruct next_ptd_iter=>//. congruence. +Qed. + +(** We prove that these functions behave well w.r.t. xxx_buffer. *) +Lemma ptd_buffer_build_from_pt {symb word} + (pt : parse_tree symb word) (ptz : pt_zipper symb word) : + (word ++ ptz_buffer ptz)%buf = ptd_buffer (build_pt_dot_from_pt pt ptz) +with ptd_buffer_build_from_pt_rec {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) + Hsymbs : + (word ++ ptlz_buffer ptlz)%buf = ptd_buffer (build_pt_dot_from_pt_rec ptl Hsymbs ptlz). +Proof. + - destruct pt as [tok|prod word ptl]=>/=. + + f_equal. revert ptz. generalize [tok]. + generalize (token_sem tok). generalize I. + change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1. + generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz. + + match goal with + | |- context [match ?X with Some H => _ | None => _ end] => destruct X eqn:EQ + end. + * by rewrite -ptd_buffer_build_from_pt_rec. + * rewrite [X in (X ++ _)%buf](_ : word = []) //. clear -EQ. by destruct ptl. + - destruct ptl as [|?? ptl ?? pt]; [contradiction|]. + specialize (ptd_buffer_build_from_pt_rec _ _ ptl). + destruct ptl. + + by rewrite /= -ptd_buffer_build_from_pt. + + by rewrite -ptd_buffer_build_from_pt_rec //= app_buf_assoc. +Qed. + +Lemma ptd_buffer_build_from_ptl {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) : + ptlz_buffer ptlz = ptd_buffer (build_pt_dot_from_ptl ptl ptlz). +Proof. + destruct ptlz as [|???? pt]=>//=. by rewrite -ptd_buffer_build_from_pt. +Qed. + +(** We prove that these functions behave well w.r.t. xxx_stack_compat. *) +Lemma ptd_stack_compat_build_from_pt {symb word} + (pt : parse_tree symb word) (ptz : pt_zipper symb word) + (stk: stack) : + ptz_stack_compat stk ptz -> + ptd_stack_compat (build_pt_dot_from_pt pt ptz) stk +with ptd_stack_compat_build_from_pt_rec {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) + (stk : stack) Hsymbs : + ptlz_stack_compat stk ptlz -> + state_has_future (state_of_stack init stk) (ptlz_prod ptlz) + (rev' (prod_rhs_rev (ptlz_prod ptlz))) (ptlz_lookahead ptlz) -> + ptd_stack_compat (build_pt_dot_from_pt_rec ptl Hsymbs ptlz) stk. +Proof. + - intros Hstk. destruct pt as [tok|prod word ptl]=>/=. + + revert ptz Hstk. generalize [tok]. generalize (token_sem tok). generalize I. + change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1. + generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz. + + assert (state_has_future (state_of_stack init stk) prod + (rev' (prod_rhs_rev prod)) (token_term (buf_head (ptz_buffer ptz)))). + { revert ptz Hstk. remember (NT (prod_lhs prod)) eqn:EQ=>ptz. + destruct ptz as [|?? ptl0 ?? ptlz0]. + - intros ->. apply start_future. congruence. + - subst. intros (stk0 & Hfut & _). apply non_terminal_closed in Hfut. + specialize (Hfut prod eq_refl). + destruct (ptlz_future_first ptlz0) as [Hfirst|[Hfirst Hnull]]. + + destruct Hfut as [_ Hfut]. auto. + + destruct Hfut as [Hfut _]. by rewrite Hnull -Hfirst in Hfut. } + match goal with + | |- context [match ?X with Some H => _ | None => _ end] => destruct X eqn:EQ + end. + * by apply ptd_stack_compat_build_from_pt_rec. + * exists stk. destruct ptl=>//. + - intros Hstk Hfut. destruct ptl as [|?? ptl ?? pt]; [contradiction|]. + specialize (ptd_stack_compat_build_from_pt_rec _ _ ptl). destruct ptl. + + eapply ptd_stack_compat_build_from_pt=>//. exists stk. + split; [|split]=>//; []. + by rewrite -ptlz_future_ptlz_prod rev_append_rev /rev' -rev_alt + rev_app_distr rev_involutive in Hfut. + + by apply ptd_stack_compat_build_from_pt_rec. +Qed. + +Lemma ptd_stack_compat_build_from_ptl {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) + (stk stk0: stack) : + ptlz_stack_compat stk0 ptlz -> + ptl_stack_compat stk0 ptl stk -> + state_has_future (state_of_stack init stk) (ptlz_prod ptlz) + (ptlz_future ptlz) (ptlz_lookahead ptlz) -> + ptd_stack_compat (build_pt_dot_from_ptl ptl ptlz) stk. +Proof. + intros Hstk0 Hstk Hfut. destruct ptlz=>/=. + - eauto. + - apply ptd_stack_compat_build_from_pt=>/=. eauto. +Qed. + +(** We can now proceed by proving that the invariant is preserved by + each step of parsing. We also prove that each step of parsing + follows next_ptd. + + We start with reduce steps: *) +Lemma reduce_step_next_ptd (prod : production) (word : list token) + (ptl : parse_tree_list (prod_rhs_rev prod) word) + (ptz : pt_zipper (NT (prod_lhs prod)) word) + (stk : stack) + Hval Hi : + ptd_stack_compat (Reduce_ptd ptl ptz) stk -> + match next_ptd (Reduce_ptd ptl ptz) with + | None => + reduce_step init stk prod (ptz_buffer ptz) Hval Hi = + Accept_sr (ptd_sem (Reduce_ptd ptl ptz)) buffer_end + | Some ptd => + exists stk', + reduce_step init stk prod (ptz_buffer ptz) Hval Hi = + Progress_sr stk' (ptd_buffer ptd) /\ + ptd_stack_compat ptd stk' + end. +Proof. + intros (stk0 & _ & Hstk & Hstk0). + apply pop_stack_compat_pop_spec with (action := prod_action prod) in Hstk. + rewrite <-pop_spec_ok with (Hp := reduce_step_subproof init stk prod Hval Hi) in Hstk. + unfold reduce_step. + match goal with + | |- context [pop_state_valid init ?A stk ?B ?C ?D ?E ?F] => + generalize (pop_state_valid init A stk B C D E F) + end. + rewrite Hstk /=. intros Hv. + generalize (reduce_step_subproof1 init stk prod Hval stk0 (fun _ : True => Hv)). + clear Hval Hstk Hi Hv stk. + assert (Hgoto := fun fut prod' => + non_terminal_goto (state_of_stack init stk0) prod' (NT (prod_lhs prod)::fut)). + simpl in Hgoto. + destruct goto_table as [[st Hst]|] eqn:Hgoto'. + - intros _. + assert (match ptz with Top_ptz => False | _ => True end). + { revert ptz Hst Hstk0 Hgoto'. + generalize (eq_refl (NT (prod_lhs prod))). + generalize (NT (prod_lhs prod)) at 1 3 5. + intros nt Hnt ptz. destruct ptz=>//. injection Hnt=> <- /= Hst -> /= Hg. + assert (Hsg := start_goto init). by rewrite Hg in Hsg. } + clear Hgoto'. + + change (ptl_sem ptl (prod_action prod)) + with (pt_sem (Non_terminal_pt prod ptl)). + generalize (Non_terminal_pt prod ptl). clear ptl. + destruct ptz as [|?? ptl ? ? ptlz]=>// pt. + + subst=>/=. eexists _. split. + + f_equal. apply ptd_buffer_build_from_ptl. + + destruct Hstk0 as (stk0' & Hfut & Hstk0' & Hstk0). + apply (ptd_stack_compat_build_from_ptl _ _ _ stk0'); auto; []. + split=>//. by exists eq_refl. + - intros Hv. generalize (reduce_step_subproof0 _ prod _ (fun _ => Hv)). + intros EQnt. clear Hv Hgoto'. + + change (ptl_sem ptl (prod_action prod)) + with (pt_sem (Non_terminal_pt prod ptl)). + generalize (Non_terminal_pt prod ptl). clear ptl. destruct ptz. + + intros pt. f_equal. by rewrite cast_eq. + + edestruct Hgoto. eapply ptz_stack_compat_cons_state_has_future, Hstk0. +Qed. + +Lemma step_next_ptd (ptd : pt_dot) (stk : stack) Hi : + ptd_stack_compat ptd stk -> + match next_ptd ptd with + | None => + step safe init stk (ptd_buffer ptd) Hi = + Accept_sr (ptd_sem ptd) buffer_end + | Some ptd' => + exists stk', + step safe init stk (ptd_buffer ptd) Hi = + Progress_sr stk' (ptd_buffer ptd') /\ + ptd_stack_compat ptd' stk' + end. +Proof. + intros Hstk. unfold step. + generalize (reduce_ok safe (state_of_stack init stk)). + destruct ptd as [prod word ptl ptz|tok symbs word ptl ptlz]. + - assert (Hfut : state_has_future (state_of_stack init stk) prod [] + (token_term (buf_head (ptz_buffer ptz)))). + { destruct Hstk as (? & ? & ?)=>//. } + assert (Hact := end_reduce _ _ _ _ Hfut). + destruct action_table as [?|awt]=>Hval /=. + + subst. by apply reduce_step_next_ptd. + + set (term := token_term (buf_head (ptz_buffer ptz))) in *. + generalize (Hval term). clear Hval. destruct (awt term)=>//. subst. + intros Hval. by apply reduce_step_next_ptd. + - destruct Hstk as (stk0 & Hfut & Hstk & Hstk0). + assert (Hact := terminal_shift _ _ _ _ Hfut). simpl in Hact. clear Hfut. + destruct action_table as [?|awt]=>//= /(_ (token_term tok)). + destruct awt as [st' EQ| |]=>// _. eexists. split. + + f_equal. rewrite -ptd_buffer_build_from_ptl //. + + apply (ptd_stack_compat_build_from_ptl _ _ _ stk0); simpl; eauto. +Qed. + +(** We prove the completeness of the parser main loop. *) +Lemma parse_fix_next_ptd_iter (ptd : pt_dot) (stk : stack) (log_n_steps : nat) Hi : + ptd_stack_compat ptd stk -> + match next_ptd_iter ptd log_n_steps with + | None => + proj1_sig (parse_fix safe init stk (ptd_buffer ptd) log_n_steps Hi) = + Accept_sr (ptd_sem ptd) buffer_end + | Some ptd' => + exists stk', + proj1_sig (parse_fix safe init stk (ptd_buffer ptd) log_n_steps Hi) = + Progress_sr stk' (ptd_buffer ptd') /\ + ptd_stack_compat ptd' stk' + end. +Proof. + revert ptd stk Hi. + induction log_n_steps as [|log_n_steps IH]; [by apply step_next_ptd|]. + move => /= ptd stk Hi Hstk. assert (IH1 := IH ptd stk Hi Hstk). + assert (EQsem := sem_next_ptd_iter ptd log_n_steps). + destruct parse_fix as [sr Hi']. simpl in IH1. + destruct next_ptd_iter as [ptd'|]. + - rewrite EQsem. destruct IH1 as (stk' & -> & Hstk'). by apply IH. + - by subst. +Qed. + +(** The parser is defined by recursion over a fuel parameter. In the + completeness proof, we need to predict how much fuel is going to be + needed in order to prove that enough fuel gives rise to a successful + parsing. + + To do so, of a dotted parse tree, which is the number of actions + left to be executed before complete parsing when the current state + is represented by the dotted parse tree. *) +Fixpoint ptlz_cost {hole_symbs hole_word} + (ptlz:ptl_zipper hole_symbs hole_word) := + match ptlz with + | Non_terminal_pt_ptlz ptz => ptz_cost ptz + | Cons_ptl_ptlz pt ptlz' => pt_size pt + ptlz_cost ptlz' + end +with ptz_cost {hole_symb hole_word} (ptz:pt_zipper hole_symb hole_word) := + match ptz with + | Top_ptz => 0 + | Cons_ptl_ptz ptl ptlz' => 1 + ptlz_cost ptlz' + end. + +Definition ptd_cost (ptd:pt_dot) := + match ptd with + | Reduce_ptd ptl ptz => ptz_cost ptz + | Shift_ptd _ ptl ptlz => 1 + ptlz_cost ptlz + end. + +Lemma ptd_cost_build_from_pt {symb word} + (pt : parse_tree symb word) (ptz : pt_zipper symb word) : + pt_size pt + ptz_cost ptz = S (ptd_cost (build_pt_dot_from_pt pt ptz)) +with ptd_cost_build_from_pt_rec {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) + Hsymbs : + ptl_size ptl + ptlz_cost ptlz = ptd_cost (build_pt_dot_from_pt_rec ptl Hsymbs ptlz). +Proof. + - destruct pt as [tok|prod word ptl']=>/=. + + revert ptz. generalize [tok]. generalize (token_sem tok). generalize I. + change True with (match T (token_term tok) with T _ => True | NT _ => False end) at 1. + generalize (T (token_term tok)) => symb HT sem word ptz. by destruct ptz. + + match goal with + | |- context [match ?X with Some H => _ | None => _ end] => destruct X eqn:EQ + end. + * rewrite -ptd_cost_build_from_pt_rec /= plus_n_Sm //. + * simpl. by destruct ptl'. + - destruct ptl as [|?? ptl ?? pt]; [contradiction|]. + specialize (ptd_cost_build_from_pt_rec _ _ ptl). destruct ptl. + + apply eq_add_S. rewrite -ptd_cost_build_from_pt /=. ring. + + rewrite -ptd_cost_build_from_pt_rec //=. ring. +Qed. + +Lemma ptd_cost_build_from_ptl {symbs word} + (ptl : parse_tree_list symbs word) (ptlz : ptl_zipper symbs word) : + ptlz_cost ptlz = ptd_cost (build_pt_dot_from_ptl ptl ptlz). +Proof. + destruct ptlz=>//. apply eq_add_S. rewrite -ptd_cost_build_from_pt /=. ring. +Qed. + +Lemma next_ptd_cost ptd: + match next_ptd ptd with + | None => ptd_cost ptd = 0 + | Some ptd' => ptd_cost ptd = S (ptd_cost ptd') + end. +Proof. + destruct ptd as [prod word ptl ptz|tok symbq wordq ptl ptlz] =>/=. + - generalize (Non_terminal_pt prod ptl). clear ptl. + destruct ptz as [|?? ptl ?? ptlz]=>// pt. by rewrite -ptd_cost_build_from_ptl. + - by rewrite -ptd_cost_build_from_ptl. +Qed. + +Lemma next_ptd_iter_cost ptd log_n_steps : + match next_ptd_iter ptd log_n_steps with + | None => ptd_cost ptd < 2^log_n_steps + | Some ptd' => ptd_cost ptd = 2^log_n_steps + ptd_cost ptd' + end. +Proof. + revert ptd. induction log_n_steps as [|log_n_steps IH]=>ptd /=. + - assert (Hptd := next_ptd_cost ptd). destruct next_ptd=>//. by rewrite Hptd. + - rewrite Nat.add_0_r. assert (IH1 := IH ptd). destruct next_ptd_iter as [ptd'|]. + + specialize (IH ptd'). destruct next_ptd_iter as [ptd''|]. + * by rewrite IH1 IH -!plus_assoc. + * rewrite IH1. by apply plus_lt_compat_l. + + by apply lt_plus_trans. +Qed. + +(** We now prove the top-level parsing function. The only thing that + is left to be done is the initialization. To do so, we define the + initial dotted parse tree, depending on a full (top-level) parse tree. *) + +Variable full_pt : parse_tree (NT (start_nt init)) full_word. + +Theorem parse_complete log_n_steps: + match parse safe init (full_word ++ buffer_end) log_n_steps with + | Parsed_pr sem buff => + sem = pt_sem full_pt /\ buff = buffer_end /\ pt_size full_pt <= 2^log_n_steps + | Timeout_pr => 2^log_n_steps < pt_size full_pt + | Fail_pr => False + end. +Proof. + assert (Hstk : ptd_stack_compat (build_pt_dot_from_pt full_pt Top_ptz) []) by + by apply ptd_stack_compat_build_from_pt. + unfold parse. + assert (Hparse := parse_fix_next_ptd_iter _ _ log_n_steps (parse_subproof init) Hstk). + rewrite -ptd_buffer_build_from_pt -sem_build_from_pt /= in Hparse. + assert (Hcost := next_ptd_iter_cost (build_pt_dot_from_pt full_pt Top_ptz) log_n_steps). + destruct next_ptd_iter. + - destruct Hparse as (? & -> & ?). apply (f_equal S) in Hcost. + rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost. rewrite Hcost. + apply le_lt_n_Sm, le_plus_l. + - rewrite Hparse. split; [|split]=>//. apply lt_le_S in Hcost. + by rewrite -ptd_cost_build_from_pt Nat.add_0_r in Hcost. +Qed. + +End Completeness_Proof. + +End Make. |