diff options
Diffstat (limited to 'MenhirLib')
| -rw-r--r-- | MenhirLib/Alphabet.v | 247 | ||||
| -rw-r--r-- | MenhirLib/Automaton.v | 164 | ||||
| -rw-r--r-- | MenhirLib/Grammar.v | 162 | ||||
| -rw-r--r-- | MenhirLib/Interpreter.v | 453 | ||||
| -rw-r--r-- | MenhirLib/Interpreter_complete.v | 825 | ||||
| -rw-r--r-- | MenhirLib/Interpreter_correct.v | 175 | ||||
| -rw-r--r-- | MenhirLib/Main.v | 79 | ||||
| -rw-r--r-- | MenhirLib/Validator_classes.v | 74 | ||||
| -rw-r--r-- | MenhirLib/Validator_complete.v | 394 | ||||
| -rw-r--r-- | MenhirLib/Validator_safe.v | 234 |
10 files changed, 2807 insertions, 0 deletions
diff --git a/MenhirLib/Alphabet.v b/MenhirLib/Alphabet.v new file mode 100644 index 00000000..29070e3d --- /dev/null +++ b/MenhirLib/Alphabet.v @@ -0,0 +1,247 @@ +(****************************************************************************) +(* *) +(* 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 Omega List Syntax Relations RelationClasses. + +Local Obligation Tactic := intros. + +(** A comparable type is equiped with a [compare] function, that define an order + relation. **) +Class Comparable (A:Type) := { + compare : A -> A -> comparison; + compare_antisym : forall x y, CompOpp (compare x y) = compare y x; + compare_trans : forall x y z c, + (compare x y) = c -> (compare y z) = c -> (compare x z) = c +}. + +Theorem compare_refl {A:Type} (C: Comparable A) : + forall x, compare x x = Eq. +Proof. +intros. +pose proof (compare_antisym x x). +destruct (compare x x); intuition; try discriminate. +Qed. + +(** The corresponding order is a strict order. **) +Definition comparableLt {A:Type} (C: Comparable A) : relation A := + fun x y => compare x y = Lt. + +Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) : + StrictOrder (comparableLt C). +Proof. +apply Build_StrictOrder. +unfold Irreflexive, Reflexive, complement, comparableLt. +intros. +pose proof H. +rewrite <- compare_antisym in H. +rewrite H0 in H. +discriminate H. +unfold Transitive, comparableLt. +intros x y z. +apply compare_trans. +Qed. + +(** nat is comparable. **) +Program Instance natComparable : Comparable nat := + { compare := Nat.compare }. +Next Obligation. +symmetry. +destruct (Nat.compare x y) as [] eqn:?. +rewrite Nat.compare_eq_iff in Heqc. +destruct Heqc. +rewrite Nat.compare_eq_iff. +trivial. +rewrite <- nat_compare_lt in *. +rewrite <- nat_compare_gt in *. +trivial. +rewrite <- nat_compare_lt in *. +rewrite <- nat_compare_gt in *. +trivial. +Qed. +Next Obligation. +destruct c. +rewrite Nat.compare_eq_iff in *; destruct H; assumption. +rewrite <- nat_compare_lt in *. +apply (Nat.lt_trans _ _ _ H H0). +rewrite <- nat_compare_gt in *. +apply (gt_trans _ _ _ H H0). +Qed. + +(** A pair of comparable is comparable. **) +Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) : + Comparable (A*B) := + { compare := fun x y => + let (xa, xb) := x in let (ya, yb) := y in + match compare xa ya return comparison with + | Eq => compare xb yb + | x => x + end }. +Next Obligation. +destruct x, y. +rewrite <- (compare_antisym a a0). +rewrite <- (compare_antisym b b0). +destruct (compare a a0); intuition. +Qed. +Next Obligation. +destruct x, y, z. +destruct (compare a a0) as [] eqn:?, (compare a0 a1) as [] eqn:?; +try (rewrite <- H0 in H; discriminate); +try (destruct (compare a a1) as [] eqn:?; + try (rewrite <- compare_antisym in Heqc0; + rewrite CompOpp_iff in Heqc0; + rewrite (compare_trans _ _ _ _ Heqc0 Heqc2) in Heqc1; + discriminate); + try (rewrite <- compare_antisym in Heqc1; + rewrite CompOpp_iff in Heqc1; + rewrite (compare_trans _ _ _ _ Heqc2 Heqc1) in Heqc0; + discriminate); + assumption); +rewrite (compare_trans _ _ _ _ Heqc0 Heqc1); +try assumption. +apply (compare_trans _ _ _ _ H H0). +Qed. + +(** Special case of comparable, where equality is Leibniz equality. **) +Class ComparableLeibnizEq {A:Type} (C: Comparable A) := + compare_eq : forall x y, compare x y = Eq -> x = y. + +(** Boolean equality for a [Comparable]. **) +Definition compare_eqb {A:Type} {C:Comparable A} (x y:A) := + match compare x y with + | Eq => true + | _ => false + end. + +Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableLeibnizEq C} : + forall x y, compare_eqb x y = true <-> x = y. +Proof. +unfold compare_eqb. +intuition. +apply compare_eq. +destruct (compare x y); intuition; discriminate. +destruct H. +rewrite compare_refl; intuition. +Qed. + +Instance NComparableLeibnizEq : ComparableLeibnizEq natComparable := Nat.compare_eq. + +(** A pair of ComparableLeibnizEq is ComparableLeibnizEq **) +Instance PairComparableLeibnizEq + {A:Type} {CA:Comparable A} (UA:ComparableLeibnizEq CA) + {B:Type} {CB:Comparable B} (UB:ComparableLeibnizEq CB) : + ComparableLeibnizEq (PairComparable CA CB). +Proof. +intros x y; destruct x, y; simpl. +pose proof (compare_eq a a0); pose proof (compare_eq b b0). +destruct (compare a a0); try discriminate. +intuition. +destruct H2, H0. +reflexivity. +Qed. + +(** An [Finite] type is a type with the list of all elements. **) +Class Finite (A:Type) := { + all_list : list A; + all_list_forall : forall x:A, In x all_list +}. + +(** An alphabet is both [ComparableLeibnizEq] and [Finite]. **) +Class Alphabet (A:Type) := { + AlphabetComparable :> Comparable A; + AlphabetComparableLeibnizEq :> ComparableLeibnizEq AlphabetComparable; + AlphabetFinite :> Finite A +}. + +(** The [Numbered] class provides a conveniant way to build [Alphabet] instances, + with a good computationnal complexity. It is mainly a injection from it to + [positive] **) +Class Numbered (A:Type) := { + inj : A -> positive; + surj : positive -> A; + surj_inj_compat : forall x, surj (inj x) = x; + inj_bound : positive; + inj_bound_spec : forall x, (inj x < Pos.succ inj_bound)%positive +}. + +Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A := + { AlphabetComparable := {| compare := fun x y => Pos.compare (inj x) (inj y) |}; + AlphabetFinite := + {| all_list := fst (Pos.iter + (fun '(l, p) => (surj p::l, Pos.succ p)) + ([], 1%positive) inj_bound) |} }. +Next Obligation. simpl. now rewrite <- Pos.compare_antisym. Qed. +Next Obligation. + match goal with c : comparison |- _ => destruct c end. + - rewrite Pos.compare_eq_iff in *. congruence. + - rewrite Pos.compare_lt_iff in *. eauto using Pos.lt_trans. + - rewrite Pos.compare_gt_iff in *. eauto using Pos.lt_trans. +Qed. +Next Obligation. + intros x y. unfold compare. intros Hxy. + assert (Hxy' : inj x = inj y). + (* We do not use [Pos.compare_eq_iff] directly to make sure the + proof is executable. *) + { destruct (Pos.eq_dec (inj x) (inj y)) as [|[]]; [now auto|]. + now apply Pos.compare_eq_iff. } + (* Using rewrite here leads to non-executable proofs. *) + transitivity (surj (inj x)). + { apply eq_sym, surj_inj_compat. } + transitivity (surj (inj y)); cycle 1. + { apply surj_inj_compat. } + apply f_equal, Hxy'. +Defined. +Next Obligation. + rewrite <-(surj_inj_compat x). + generalize (inj_bound_spec x). generalize (inj x). clear x. intros x. + match goal with |- ?Hx -> In ?s (fst ?p) => + assert ((Hx -> In s (fst p)) /\ snd p = Pos.succ inj_bound); [|now intuition] end. + rewrite Pos.lt_succ_r. + induction inj_bound as [|y [IH1 IH2]] using Pos.peano_ind; + (split; [intros Hx|]); simpl. + - rewrite (Pos.le_antisym _ _ Hx); auto using Pos.le_1_l. + - auto. + - rewrite Pos.iter_succ. destruct Pos.iter; simpl in *. subst. + rewrite Pos.le_lteq in Hx. destruct Hx as [?%Pos.lt_succ_r| ->]; now auto. + - rewrite Pos.iter_succ. destruct Pos.iter. simpl in IH2. subst. reflexivity. +Qed. + +(** Definitions of [FSet]/[FMap] from [Comparable] **) +Require Import OrderedTypeAlt. +Require FSetAVL. +Require FMapAVL. +Import OrderedType. + +Module Type ComparableM. + Parameter t : Type. + Declare Instance tComparable : Comparable t. +End ComparableM. + +Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt. + Definition t := C.t. + Definition compare : t -> t -> comparison := compare. + + Infix "?=" := compare (at level 70, no associativity). + + Lemma compare_sym x y : (y?=x) = CompOpp (x?=y). + Proof. exact (Logic.eq_sym (compare_antisym x y)). Qed. + Lemma compare_trans c x y z : + (x?=y) = c -> (y?=z) = c -> (x?=z) = c. + Proof. + apply compare_trans. + Qed. +End OrderedTypeAlt_from_ComparableM. + +Module OrderedType_from_ComparableM (C:ComparableM) <: OrderedType. + Module Alt := OrderedTypeAlt_from_ComparableM C. + Include (OrderedType_from_Alt Alt). +End OrderedType_from_ComparableM. diff --git a/MenhirLib/Automaton.v b/MenhirLib/Automaton.v new file mode 100644 index 00000000..c310fc61 --- /dev/null +++ b/MenhirLib/Automaton.v @@ -0,0 +1,164 @@ +(****************************************************************************) +(* *) +(* 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. *) +(* *) +(****************************************************************************) + +Require Grammar. +Require Export Alphabet. +From Coq Require Import Orders. +From Coq Require Export List Syntax. + +Module Type AutInit. + (** The grammar of the automaton. **) + Declare Module Gram:Grammar.T. + Export Gram. + + (** The set of non initial state is considered as an alphabet. **) + Parameter noninitstate : Type. + Declare Instance NonInitStateAlph : Alphabet noninitstate. + + Parameter initstate : Type. + Declare Instance InitStateAlph : Alphabet initstate. + + (** When we are at this state, we know that this symbol is the top of the + stack. **) + Parameter last_symb_of_non_init_state: noninitstate -> symbol. +End AutInit. + +Module Types(Import Init:AutInit). + (** In many ways, the behaviour of the initial state is different from the + behaviour of the other states. So we have chosen to explicitaly separate + them: the user has to provide the type of non initial states. **) + Inductive state := + | Init: initstate -> state + | Ninit: noninitstate -> state. + + Program Instance StateAlph : Alphabet state := + { AlphabetComparable := {| compare := fun x y => + match x, y return comparison with + | Init _, Ninit _ => Lt + | Init x, Init y => compare x y + | Ninit _, Init _ => Gt + | Ninit x, Ninit y => compare x y + end |}; + AlphabetFinite := {| all_list := map Init all_list ++ map Ninit all_list |} }. + Local Obligation Tactic := intros. + Next Obligation. + destruct x, y; intuition; apply compare_antisym. + Qed. + Next Obligation. + destruct x, y, z; intuition. + apply (compare_trans _ i0); intuition. + congruence. + congruence. + apply (compare_trans _ n0); intuition. + Qed. + Next Obligation. + intros x y. + destruct x, y; intuition; try discriminate. + rewrite (compare_eq i i0); intuition. + rewrite (compare_eq n n0); intuition. + Qed. + Next Obligation. + apply in_or_app; destruct x; intuition; + [left|right]; apply in_map; apply all_list_forall. + Qed. + + Coercion Ninit : noninitstate >-> state. + Coercion Init : initstate >-> state. + + (** For an LR automaton, there are four kind of actions that can be done at a + given state: + - Shifting, that is reading a token and putting it into the stack, + - Reducing a production, that is popping the right hand side of the + production from the stack, and pushing the left hand side, + - Failing + - Accepting the word (special case of reduction) + + As in the menhir parser generator, we do not want our parser to read after + the end of stream. That means that once the parser has read a word in the + grammar language, it should stop without peeking the input stream. So, for + the automaton to be complete, the grammar must be particular: if a word is + in its language, then it is not a prefix of an other word of the language + (otherwise, menhir reports an end of stream conflict). + + As a consequence of that, there is two notions of action: the first one is + an action performed before having read the stream, the second one is after + **) + + Inductive lookahead_action (term:terminal) := + | Shift_act: forall s:noninitstate, + T term = last_symb_of_non_init_state s -> lookahead_action term + | Reduce_act: production -> lookahead_action term + | Fail_act: lookahead_action term. + Arguments Shift_act [term]. + Arguments Reduce_act [term]. + Arguments Fail_act [term]. + + Inductive action := + | Default_reduce_act: production -> action + | Lookahead_act : (forall term:terminal, lookahead_action term) -> action. + + (** Types used for the annotations of the automaton. **) + + (** An item is a part of the annotations given to the validator. + It is acually a set of LR(1) items sharing the same core. It is needed + to validate completeness. **) + Record item := { + (** The pseudo-production of the item. **) + prod_item: production; + + (** The position of the dot. **) + dot_pos_item: nat; + + (** The lookahead symbol of the item. We are using a list, so we can store + together multiple LR(1) items sharing the same core. **) + lookaheads_item: list terminal + }. +End Types. + +Module Type T. + Include AutInit <+ Types. + Module Export GramDefs := Grammar.Defs Gram. + + (** For each initial state, the non terminal it recognizes. **) + Parameter start_nt: initstate -> nonterminal. + + (** The action table maps a state to either a map terminal -> action. **) + Parameter action_table: + state -> action. + (** The goto table of an LR(1) automaton. **) + Parameter goto_table: state -> forall nt:nonterminal, + option { s:noninitstate | NT nt = last_symb_of_non_init_state s }. + + (** Some annotations on the automaton to help the validation. **) + + (** When we are at this state, we know that these symbols are just below + the top of the stack. The list is ordered such that the head correspond + to the (almost) top of the stack. **) + Parameter past_symb_of_non_init_state: noninitstate -> list symbol. + + (** When we are at this state, the (strictly) previous states verify these + predicates. **) + Parameter past_state_of_non_init_state: noninitstate -> list (state -> bool). + + (** The items of the state. **) + Parameter items_of_state: state -> list item. + + (** The nullable predicate for non terminals : + true if and only if the symbol produces the empty string **) + Parameter nullable_nterm: nonterminal -> bool. + + (** The first predicates for non terminals, symbols or words of symbols. A + terminal is in the returned list if, and only if the parameter produces a + word that begins with the given terminal **) + Parameter first_nterm: nonterminal -> list terminal. +End T. diff --git a/MenhirLib/Grammar.v b/MenhirLib/Grammar.v new file mode 100644 index 00000000..a371318b --- /dev/null +++ b/MenhirLib/Grammar.v @@ -0,0 +1,162 @@ +(****************************************************************************) +(* *) +(* 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 Orders. +Require Import Alphabet. + +(** The terminal non-terminal alphabets of the grammar. **) +Module Type Alphs. + Parameters terminal nonterminal : Type. + Declare Instance TerminalAlph: Alphabet terminal. + Declare Instance NonTerminalAlph: Alphabet nonterminal. +End Alphs. + +(** Definition of the alphabet of symbols, given the alphabet of terminals + and the alphabet of non terminals **) +Module Symbol(Import A:Alphs). + + Inductive symbol := + | T: terminal -> symbol + | NT: nonterminal -> symbol. + + Program Instance SymbolAlph : Alphabet symbol := + { AlphabetComparable := {| compare := fun x y => + match x, y return comparison with + | T _, NT _ => Gt + | NT _, T _ => Lt + | T x, T y => compare x y + | NT x, NT y => compare x y + end |}; + AlphabetFinite := {| all_list := + map T all_list++map NT all_list |} }. + Next Obligation. + destruct x; destruct y; intuition; apply compare_antisym. + Qed. + Next Obligation. + destruct x; destruct y; destruct z; intuition; try discriminate. + apply (compare_trans _ t0); intuition. + apply (compare_trans _ n0); intuition. + Qed. + Next Obligation. + intros x y. + destruct x; destruct y; try discriminate; intros. + rewrite (compare_eq t t0); now intuition. + rewrite (compare_eq n n0); now intuition. + Defined. + Next Obligation. + rewrite in_app_iff. + destruct x; [left | right]; apply in_map; apply all_list_forall. + Qed. + +End Symbol. + +(** A curryfied function with multiple parameters **) +Definition arrows_right: Type -> list Type -> Type := + fold_right (fun A B => A -> B). + +Module Type T. + Include Alphs <+ Symbol. + + (** [symbol_semantic_type] maps a symbols to the type of its semantic + values. **) + Parameter symbol_semantic_type: symbol -> Type. + + (** The type of productions identifiers **) + Parameter production : Type. + Declare Instance ProductionAlph : Alphabet production. + + (** Accessors for productions: left hand side, right hand side, + and semantic action. The semantic actions are given in the form + of curryfied functions, that take arguments in the reverse order. **) + Parameter prod_lhs: production -> nonterminal. + (* The RHS of a production is given in reversed order, so that symbols *) + Parameter prod_rhs_rev: production -> list symbol. + Parameter prod_action: + forall p:production, + arrows_right + (symbol_semantic_type (NT (prod_lhs p))) + (map symbol_semantic_type (prod_rhs_rev p)). + + (** Tokens are the atomic elements of the input stream: they contain + a terminal and a semantic value of the type corresponding to this + terminal. *) + Parameter token : Type. + Parameter token_term : token -> terminal. + Parameter token_sem : + forall tok : token, symbol_semantic_type (T (token_term tok)). +End T. + +Module Defs(Import G:T). + + (** The semantics of a grammar is defined in two stages. First, we + define the notion of parse tree, which represents one way of + recognizing a word with a head symbol. Semantic values are stored + at the leaves. + + This notion is defined in two mutually recursive flavours: + either for a single head symbol, or for a list of head symbols. *) + Inductive parse_tree: + forall (head_symbol:symbol) (word:list token), Type := + + (** Parse tree for a terminal symbol. *) + | Terminal_pt: + forall (tok:token), parse_tree (T (token_term tok)) [tok] + + (** Parse tree for a non-terminal symbol. *) + | Non_terminal_pt: + forall (prod:production) {word:list token}, + parse_tree_list (prod_rhs_rev prod) word -> + parse_tree (NT (prod_lhs prod)) word + + (* Note : the list head_symbols_rev is reversed. *) + with parse_tree_list: + forall (head_symbols_rev:list symbol) (word:list token), Type := + + | Nil_ptl: parse_tree_list [] [] + + | Cons_ptl: + forall {head_symbolsq:list symbol} {wordq:list token}, + parse_tree_list head_symbolsq wordq -> + + forall {head_symbolt:symbol} {wordt:list token}, + parse_tree head_symbolt wordt -> + + parse_tree_list (head_symbolt::head_symbolsq) (wordq++wordt). + + (** We can now finish the definition of the semantics of a grammar, + by giving the semantic value assotiated with a parse tree. *) + Fixpoint pt_sem {head_symbol word} (tree:parse_tree head_symbol word) : + symbol_semantic_type head_symbol := + match tree with + | Terminal_pt tok => token_sem tok + | Non_terminal_pt prod ptl => ptl_sem ptl (prod_action prod) + end + with ptl_sem {A head_symbols word} (tree:parse_tree_list head_symbols word) : + arrows_right A (map symbol_semantic_type head_symbols) -> A := + match tree with + | Nil_ptl => fun act => act + | Cons_ptl q t => fun act => ptl_sem q (act (pt_sem t)) + end. + + Fixpoint pt_size {head_symbol word} (tree:parse_tree head_symbol word) := + match tree with + | Terminal_pt _ => 1 + | Non_terminal_pt _ l => S (ptl_size l) + end + with ptl_size {head_symbols word} (tree:parse_tree_list head_symbols word) := + match tree with + | Nil_ptl => 0 + | Cons_ptl q t => + pt_size t + ptl_size q + end. +End Defs. diff --git a/MenhirLib/Interpreter.v b/MenhirLib/Interpreter.v new file mode 100644 index 00000000..568597ba --- /dev/null +++ b/MenhirLib/Interpreter.v @@ -0,0 +1,453 @@ +(****************************************************************************) +(* *) +(* 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. +From Coq.ssr Require Import ssreflect. +Require Automaton. +Require Import Alphabet Grammar Validator_safe. + +Module Make(Import A:Automaton.T). +Module Import ValidSafe := Validator_safe.Make A. + +(** A few helpers for dependent types. *) + +(** Decidable propositions. *) +Class Decidable (P : Prop) := decide : {P} + {~P}. +Arguments decide _ {_}. + +(** A [Comparable] type has decidable equality. *) +Instance comparable_decidable_eq T `{ComparableLeibnizEq T} (x y : T) : + Decidable (x = y). +Proof. + unfold Decidable. + destruct (compare x y) eqn:EQ; [left; apply compare_eq; intuition | ..]; + right; intros ->; by rewrite compare_refl in EQ. +Defined. + +Instance list_decidable_eq T : + (forall x y : T, Decidable (x = y)) -> + (forall l1 l2 : list T, Decidable (l1 = l2)). +Proof. unfold Decidable. decide equality. Defined. + +Ltac subst_existT := + repeat + match goal with + | _ => progress subst + | H : @existT ?A ?P ?x ?y1 = @existT ?A ?P ?x ?y2 |- _ => + let DEC := fresh in + assert (DEC : forall u1 u2 : A, Decidable (u1 = u2)) by apply _; + apply Eqdep_dec.inj_pair2_eq_dec in H; [|by apply DEC]; + clear DEC + end. + +(** The interpreter is written using dependent types. In order to + avoid reducing proof terms while executing the parser, we thunk all + the propositions behind an arrow. + Note that thunkP is still in Prop so that it is erased by + extraction. + *) +Definition thunkP (P : Prop) : Prop := True -> P. + +(** Sometimes, we actually need a reduced proof in a program (for + example when using an equality to cast a value). In that case, + instead of reducing the proof we already have, we reprove the + assertion by using decidability. *) +Definition reprove {P} `{Decidable P} (p : thunkP P) : P := + match decide P with + | left p => p + | right np => False_ind _ (np (p I)) + end. + +(** Combination of reprove with eq_rect. *) +Definition cast {T : Type} (F : T -> Type) {x y : T} (eq : thunkP (x = y)) + {DEC : unit -> Decidable (x = y)}: + F x -> F y := + fun a => eq_rect x F a y (@reprove _ (DEC ()) eq). + +Lemma cast_eq T F (x : T) (eq : thunkP (x = x)) `{forall x y, Decidable (x = y)} a : + cast F eq a = a. +Proof. by rewrite /cast -Eqdep_dec.eq_rect_eq_dec. Qed. + +(** Input buffers and operations on them. **) +CoInductive buffer : Type := + Buf_cons { buf_head : token; buf_tail : buffer }. + +Delimit Scope buffer_scope with buf. +Bind Scope buffer_scope with buffer. + +Infix "::" := Buf_cons (at level 60, right associativity) : buffer_scope. + +(** Concatenation of a list and an input buffer **) +Fixpoint app_buf (l:list token) (buf:buffer) := + match l with + | nil => buf + | cons t q => (t :: app_buf q buf)%buf + end. +Infix "++" := app_buf (at level 60, right associativity) : buffer_scope. + +Lemma app_buf_assoc (l1 l2:list token) (buf:buffer) : + (l1 ++ (l2 ++ buf) = (l1 ++ l2) ++ buf)%buf. +Proof. induction l1 as [|?? IH]=>//=. rewrite IH //. Qed. + +(** The type of a non initial state: the type of semantic values associated + with the last symbol of this state. *) +Definition noninitstate_type state := + symbol_semantic_type (last_symb_of_non_init_state state). + +(** The stack of the automaton : it can be either nil or contains a non + initial state, a semantic value for the symbol associted with this state, + and a nested stack. **) +Definition stack := list (sigT noninitstate_type). (* eg. list {state & state_type state} *) + +Section Interpreter. + +Hypothesis safe: safe. + +(* Properties of the automaton deduced from safety validation. *) +Proposition shift_head_symbs: shift_head_symbs. +Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed. +Proposition goto_head_symbs: goto_head_symbs. +Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed. +Proposition shift_past_state: shift_past_state. +Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed. +Proposition goto_past_state: goto_past_state. +Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed. +Proposition reduce_ok: reduce_ok. +Proof. pose proof safe; unfold ValidSafe.safe in H; intuition. Qed. + +Variable init : initstate. + +(** The top state of a stack **) +Definition state_of_stack (stack:stack): state := + match stack with + | [] => init + | existT _ s _::_ => s + end. + +(** The stack of states of an automaton stack **) +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. + +(** The stack of symbols of an automaton stack **) +Definition symb_stack_of_stack (stack:stack) := + List.map + (fun cell:sigT noninitstate_type => last_symb_of_non_init_state (projT1 cell)) + stack. + +(** The stack invariant : it basically states that the assumptions on the + states are true. **) +Inductive stack_invariant: stack -> Prop := + | stack_invariant_constr: + forall stack, + prefix (head_symbs_of_state (state_of_stack stack)) + (symb_stack_of_stack stack) -> + prefix_pred (head_states_of_state (state_of_stack 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). + +(** [pop] pops some symbols from the stack. It returns the popped semantic + values using [sem_popped] as an accumulator and discards the popped + states.**) +Fixpoint pop (symbols_to_pop:list symbol) {A:Type} (stk:stack) : + thunkP (prefix symbols_to_pop (symb_stack_of_stack stk)) -> + forall (action:arrows_right A (map symbol_semantic_type symbols_to_pop)), + stack * A. +unshelve refine + (match symbols_to_pop + return + (thunkP (prefix symbols_to_pop (symb_stack_of_stack stk))) -> + forall (action:arrows_right A (map _ symbols_to_pop)), stack * A + with + | [] => fun _ action => (stk, action) + | t::q => fun Hp action => + match stk + return thunkP (prefix (t::q) (symb_stack_of_stack stk)) -> stack * A + with + | existT _ state_cur sem::stack_rec => fun Hp => + let sem_conv := cast symbol_semantic_type _ sem in + pop q _ stack_rec _ (action sem_conv) + | [] => fun Hp => False_rect _ _ + end Hp + end). +Proof. + - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp). + - clear -Hp. abstract (specialize (Hp I); now inversion Hp). + - simpl in Hp. clear -Hp. abstract (intros _ ; specialize (Hp I); now inversion Hp). +Defined. + +(* Equivalent declarative specification for pop, so that we avoid + (part of) the dependent types nightmare. *) +Inductive pop_spec {A:Type} : + forall (symbols_to_pop:list symbol) (stk : stack) + (action : arrows_right A (map symbol_semantic_type symbols_to_pop)) + (stk' : stack) (sem : A), + Prop := + | Nil_pop_spec stk sem : pop_spec [] stk sem stk sem + | Cons_pop_spec symbols_to_pop st stk action sem stk' res : + pop_spec symbols_to_pop stk (action sem) stk' res -> + pop_spec (last_symb_of_non_init_state st::symbols_to_pop) + (existT _ st sem :: stk) action stk' res. + +Lemma pop_spec_ok {A:Type} symbols_to_pop stk Hp action stk' res: + pop symbols_to_pop stk Hp action = (stk', res) <-> + pop_spec (A:=A) symbols_to_pop stk action stk' res. +Proof. + revert stk Hp action. + induction symbols_to_pop as [|t symbols_to_pop IH]=>stk Hp action /=. + - split. + + intros [= <- <-]. constructor. + + intros H. inversion H. by subst_existT. + - destruct stk as [|[st sem]]=>/=; [by destruct pop_subproof0|]. + remember (pop_subproof t symbols_to_pop stk st Hp) as EQ eqn:eq. clear eq. + generalize EQ. revert Hp action. rewrite <-(EQ I)=>Hp action ?. + rewrite cast_eq. rewrite IH. split. + + intros. by constructor. + + intros H. inversion H. by subst_existT. +Qed. + + +Lemma pop_preserves_invariant symbols_to_pop stk Hp A action : + stack_invariant stk -> + stack_invariant (fst (pop symbols_to_pop stk Hp (A:=A) action)). +Proof. + revert stk Hp A action. induction symbols_to_pop as [|t q IH]=>//=. + intros stk Hp A action Hi. + destruct Hi as [stack Hp' Hpp [|state st stk']]. + - destruct pop_subproof0. + - now apply IH. +Qed. + +Lemma pop_state_valid symbols_to_pop stk Hp A action lpred : + prefix_pred lpred (state_stack_of_stack stk) -> + let stk' := fst (pop symbols_to_pop stk Hp (A:=A) action) in + state_valid_after_pop (state_of_stack stk') symbols_to_pop lpred. +Proof. + revert stk Hp A action lpred. induction symbols_to_pop as [|t q IH]=>/=. + - intros stk Hp A a lpred Hpp. destruct lpred as [|pred lpred]; constructor. + inversion Hpp as [|? lpred' ? pred' Himpl Hpp' eq1 eq2]; subst. + specialize (Himpl (state_of_stack stk)). + destruct (pred' (state_of_stack stk)) as [] eqn:Heqpred'=>//. + destruct stk as [|[]]; simpl in *. + + inversion eq2; subst; clear eq2. + unfold singleton_state_pred in Heqpred'. + now rewrite compare_refl in Heqpred'; discriminate. + + inversion eq2; subst; clear eq2. + unfold singleton_state_pred in Heqpred'. + now rewrite compare_refl in Heqpred'; discriminate. + - intros stk Hp A a lpred Hpp. destruct stk as [|[] stk]=>//=. + + destruct pop_subproof0. + + destruct lpred as [|pred lpred]; [by constructor|]. + constructor. apply IH. by inversion Hpp. +Qed. + +(** [step_result] represents the result of one step of the automaton : it can + fail, accept or progress. [Fail_sr] means that the input is incorrect. + [Accept_sr] means that this is the last step of the automaton, and it + returns the semantic value of the input word. [Progress_sr] means that + some progress has been made, but new steps are needed in order to accept + a word. + + For [Accept_sr] and [Progress_sr], the result contains the new input buffer. + + [Fail_sr] means that the input word is rejected by the automaton. It is + different to [Err] (from the error monad), which mean that the automaton is + bogus and has perfomed a forbidden action. **) +Inductive step_result := + | Fail_sr: step_result + | Accept_sr: symbol_semantic_type (NT (start_nt init)) -> buffer -> step_result + | Progress_sr: stack -> buffer -> step_result. + +(** [reduce_step] does a reduce action : + - pops some elements from the stack + - execute the action of the production + - follows the goto for the produced non terminal symbol **) +Definition reduce_step stk prod (buffer : buffer) + (Hval : thunkP (valid_for_reduce (state_of_stack stk) prod)) + (Hi : thunkP (stack_invariant stk)) + : step_result. +refine + ((let '(stk', sem) as ss := pop (prod_rhs_rev prod) stk _ (prod_action prod) + return thunkP (state_valid_after_pop (state_of_stack (fst ss)) _ + (head_states_of_state (state_of_stack stk))) -> _ + in fun Hval' => + match goto_table (state_of_stack stk') (prod_lhs prod) as goto + return (thunkP (goto = None -> + match state_of_stack stk' with + | Init i => prod_lhs prod = start_nt i + | Ninit _ => False + end)) -> _ + with + | Some (exist _ state_new e) => fun _ => + let sem := eq_rect _ _ sem _ e in + Progress_sr (existT noninitstate_type state_new sem::stk') buffer + | None => fun Hval => + let sem := cast symbol_semantic_type _ sem in + Accept_sr sem buffer + end (fun _ => _)) + (fun _ => pop_state_valid _ _ _ _ _ _ _)). +Proof. + - clear -Hi Hval. + abstract (intros _; destruct Hi=>//; eapply prefix_trans; [by apply Hval|eassumption]). + - clear -Hval. + abstract (intros _; f_equal; specialize (Hval I eq_refl); destruct stk' as [|[]]=>//). + - simpl in Hval'. clear -Hval Hval'. + abstract (move : Hval => /(_ I) [_ /(_ _ (Hval' I))] Hval2 Hgoto; by rewrite Hgoto in Hval2). + - clear -Hi. abstract by destruct Hi. +Defined. + +Lemma reduce_step_stack_invariant_preserved stk prod buffer Hv Hi stk' buffer': + reduce_step stk prod buffer Hv Hi = Progress_sr stk' buffer' -> + stack_invariant stk'. +Proof. + unfold reduce_step. + match goal with + | |- context [pop ?symbols_to_pop stk ?Hp ?action] => + assert (Hi':=pop_preserves_invariant symbols_to_pop stk Hp _ action (Hi I)); + generalize (pop_state_valid symbols_to_pop stk Hp _ action) + end. + destruct pop as [stk0 sem]=>/=. simpl in Hi'. intros Hv'. + assert (Hgoto1:=goto_head_symbs (state_of_stack stk0) (prod_lhs prod)). + assert (Hgoto2:=goto_past_state (state_of_stack stk0) (prod_lhs prod)). + match goal with | |- context [fun _ : True => ?X] => generalize X end. + destruct goto_table as [[state_new e]|] eqn:EQgoto=>//. + intros _ [= <- <-]. constructor=>/=. + - constructor. eapply prefix_trans. apply Hgoto1. by destruct Hi'. + - unfold state_stack_of_stack; simpl; constructor. + + intros ?. by destruct singleton_state_pred. + + eapply prefix_pred_trans. apply Hgoto2. by destruct Hi'. + - by constructor. +Qed. + +(** One step of parsing. **) +Definition step stk buffer (Hi : thunkP (stack_invariant stk)): step_result := + match action_table (state_of_stack stk) as a return + thunkP + match a return Prop with + | Default_reduce_act prod => _ + | Lookahead_act awt => forall t : terminal, + match awt t with + | Reduce_act p => _ + | _ => True + end + end -> _ + with + | Default_reduce_act prod => fun Hv => + reduce_step stk prod buffer Hv Hi + | Lookahead_act awt => fun Hv => + match buf_head buffer with + | tok => + match awt (token_term tok) as a return + thunkP match a return Prop with Reduce_act p => _ | _ => _ end -> _ + with + | Shift_act state_new e => fun _ => + let sem_conv := eq_rect _ symbol_semantic_type (token_sem tok) _ e in + Progress_sr (existT noninitstate_type state_new sem_conv::stk) + (buf_tail buffer) + | Reduce_act prod => fun Hv => + reduce_step stk prod buffer Hv Hi + | Fail_act => fun _ => + Fail_sr + end (fun _ => Hv I (token_term tok)) + end + end (fun _ => reduce_ok _). + +Lemma step_stack_invariant_preserved stk buffer Hi stk' buffer': + step stk buffer Hi = Progress_sr stk' buffer' -> + stack_invariant stk'. +Proof. + unfold step. + generalize (reduce_ok (state_of_stack stk))=>Hred. + assert (Hshift1 := shift_head_symbs (state_of_stack stk)). + assert (Hshift2 := shift_past_state (state_of_stack stk)). + destruct action_table as [prod|awt]=>/=. + - eauto using reduce_step_stack_invariant_preserved. + - set (term := token_term (buf_head buffer)). + generalize (Hred term). clear Hred. intros Hred. + specialize (Hshift1 term). specialize (Hshift2 term). + destruct (awt term) as [state_new e|prod|]=>//. + + intros [= <- <-]. constructor=>/=. + * constructor. eapply prefix_trans. apply Hshift1. by destruct Hi. + * unfold state_stack_of_stack; simpl; constructor. + -- intros ?. by destruct singleton_state_pred. + -- eapply prefix_pred_trans. apply Hshift2. by destruct Hi. + * constructor; by apply Hi. + + eauto using reduce_step_stack_invariant_preserved. +Qed. + +(** The parsing use a [nat] fuel parameter [log_n_steps], so that we + do not have to prove terminaison, which is difficult. + + Note that [log_n_steps] is *not* the fuel in the conventionnal + sense: this parameter contains the logarithm (in base 2) of the + number of steps to perform. Hence, a value of, e.g., 50 will + usually be enough to ensure termination. *) +Fixpoint parse_fix stk buffer (log_n_steps : nat) (Hi : thunkP (stack_invariant stk)): + { sr : step_result | + forall stk' buffer', sr = Progress_sr stk' buffer' -> stack_invariant stk' } := + match log_n_steps with + | O => exist _ (step stk buffer Hi) + (step_stack_invariant_preserved _ _ Hi) + | S log_n_steps => + match parse_fix stk buffer log_n_steps Hi with + | exist _ (Progress_sr stk buffer) Hi' => + parse_fix stk buffer log_n_steps (fun _ => Hi' _ buffer eq_refl) + | sr => sr + end + end. + +(** The final result of a parsing is either a failure (the automaton + has rejected the input word), either a timeout (the automaton has + spent all the given [2^log_n_steps]), either a parsed semantic value + with a rest of the input buffer. + + Note that we do not make parse_result depend on start_nt for the + result type, so that this inductive is extracted without the use + of Obj.t in OCaml. **) +Inductive parse_result {A : Type} := + | Fail_pr: parse_result + | Timeout_pr: parse_result + | Parsed_pr: A -> buffer -> parse_result. +Global Arguments parse_result _ : clear implicits. + +Definition parse (buffer : buffer) (log_n_steps : nat): + parse_result (symbol_semantic_type (NT (start_nt init))). +refine (match proj1_sig (parse_fix [] buffer log_n_steps _) with + | Fail_sr => Fail_pr + | Accept_sr sem buffer' => Parsed_pr sem buffer' + | Progress_sr _ _ => Timeout_pr + end). +Proof. + abstract (repeat constructor; intros; by destruct singleton_state_pred). +Defined. + +End Interpreter. + +Arguments Fail_sr {init}. +Arguments Accept_sr {init} _ _. +Arguments Progress_sr {init} _ _. + +End Make. + +Module Type T(A:Automaton.T). + Include (Make A). +End T. 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. diff --git a/MenhirLib/Interpreter_correct.v b/MenhirLib/Interpreter_correct.v new file mode 100644 index 00000000..1325f610 --- /dev/null +++ b/MenhirLib/Interpreter_correct.v @@ -0,0 +1,175 @@ +(****************************************************************************) +(* *) +(* 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. +Require Import Alphabet. +Require Grammar Automaton Interpreter. +From Coq.ssr Require Import ssreflect. + +Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A). + +(** * Correctness of the interpreter **) + +(** We prove that, in any case, if the interpreter accepts returning a + semantic value, then this is a semantic value of the input **) + +Section Init. + +Variable init:initstate. + +(** [word_has_stack_semantics] relates a word with a stack, stating that the + word is a concatenation of words that have the semantic values stored in + the stack. **) +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) + (pt:parse_tree (last_symb_of_non_init_state s) wordt), + + word_has_stack_semantics + (wordq++wordt) (existT noninitstate_type s (pt_sem pt)::stackq). + +(** [pop] preserves the invariant **) +Lemma pop_spec_ptl A symbols_to_pop action word_stk stk (res : A) stk' : + pop_spec symbols_to_pop stk action stk' res -> + word_has_stack_semantics word_stk stk -> + exists word_stk' word_res (ptl:parse_tree_list symbols_to_pop word_res), + (word_stk' ++ word_res = word_stk)%list /\ + word_has_stack_semantics word_stk' stk' /\ + ptl_sem ptl action = res. +Proof. + intros Hspec. revert word_stk. + induction Hspec as [stk sem|symbols_to_pop st stk action sem stk' res Hspec IH]; + intros word_stk Hword_stk. + - exists word_stk, [], Nil_ptl. rewrite -app_nil_end. eauto. + - inversion Hword_stk. subst_existT. + edestruct IH as (word_stk' & word_res & ptl & ? & Hword_stk'' & ?); [eassumption|]. + subst. eexists word_stk', (word_res ++ _)%list, (Cons_ptl ptl _). + split; [|split]=>//. rewrite app_assoc //. +Qed. + +(** [reduce_step] preserves the invariant **) +Lemma reduce_step_invariant (stk:stack) (prod:production) Hv Hi word buffer : + word_has_stack_semantics word stk -> + match reduce_step init stk prod buffer Hv Hi with + | Accept_sr sem buffer_new => + exists pt : parse_tree (NT (start_nt init)) word, + buffer = buffer_new /\ pt_sem pt = sem + | Progress_sr stk' buffer_new => + buffer = buffer_new /\ word_has_stack_semantics word stk' + | Fail_sr => True + end. +Proof. + intros Hword_stk. unfold reduce_step. + match goal with + | |- context [pop_state_valid init ?stp stk ?x1 ?x2 ?x3 ?x4 ?x5] => + generalize (pop_state_valid init stp stk x1 x2 x3 x4 x5) + end. + destruct pop as [stk' sem] eqn:Hpop=>/= Hv'. + apply pop_spec_ok in Hpop. apply pop_spec_ptl with (word_stk := word) in Hpop=>//. + destruct Hpop as (word1 & word2 & ptl & <- & Hword1 & <-). + generalize (reduce_step_subproof1 init stk prod Hv stk' (fun _ : True => Hv')). + destruct goto_table as [[st' EQ]|]. + - intros _. split=>//. + change (ptl_sem ptl (prod_action prod)) with (pt_sem (Non_terminal_pt prod ptl)). + generalize (Non_terminal_pt prod ptl). rewrite ->EQ. intros pt. by constructor. + - intros Hstk'. destruct Hword1; [|by destruct Hstk']. + generalize (reduce_step_subproof0 init prod [] (fun _ : True => Hstk')). + simpl in Hstk'. rewrite -Hstk' // => EQ. rewrite cast_eq. + exists (Non_terminal_pt prod ptl). by split. +Qed. + +(** [step] preserves the invariant **) +Lemma step_invariant stk word buffer safe Hi : + word_has_stack_semantics word stk -> + match step safe init stk buffer Hi with + | Accept_sr sem buffer_new => + exists word_new (pt:parse_tree (NT (start_nt init)) word_new), + (word ++ buffer = word_new ++ buffer_new)%buf /\ + pt_sem pt = sem + | Progress_sr stk_new buffer_new => + exists word_new, + (word ++ buffer = word_new ++ buffer_new)%buf /\ + word_has_stack_semantics word_new stk_new + | Fail_sr => True + end. +Proof. + intros Hword_stk. unfold step. + generalize (reduce_ok safe (state_of_stack init stk)). + destruct action_table as [prod|awt]. + - intros Hv. + apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word buffer) in Hword_stk. + destruct reduce_step=>//. + + destruct Hword_stk as (pt & <- & <-); eauto. + + destruct Hword_stk as [<- ?]; eauto. + - destruct buffer as [tok buffer]=>/=. + move=> /(_ (token_term tok)) Hv. destruct (awt (token_term tok)) as [st EQ|prod|]=>//. + + eexists _. split; [by apply app_buf_assoc with (l2 := [_])|]. + change (token_sem tok) with (pt_sem (Terminal_pt tok)). + generalize (Terminal_pt tok). generalize [tok]. + rewrite -> EQ=>word' pt /=. by constructor. + + apply (reduce_step_invariant stk prod (fun _ => Hv) Hi word (tok::buffer)) + in Hword_stk. + destruct reduce_step=>//. + * destruct Hword_stk as (pt & <- & <-); eauto. + * destruct Hword_stk as [<- ?]; eauto. +Qed. + +(** [step] preserves the invariant **) +Lemma parse_fix_invariant stk word buffer safe log_n_steps Hi : + word_has_stack_semantics word stk -> + match proj1_sig (parse_fix safe init stk buffer log_n_steps Hi) with + | Accept_sr sem buffer_new => + exists word_new (pt:parse_tree (NT (start_nt init)) word_new), + (word ++ buffer = word_new ++ buffer_new)%buf /\ + pt_sem pt = sem + | Progress_sr stk_new buffer_new => + exists word_new, + (word ++ buffer = word_new ++ buffer_new)%buf /\ + word_has_stack_semantics word_new stk_new + | Fail_sr => True + end. +Proof. + revert stk word buffer Hi. + induction log_n_steps as [|log_n_steps IH]=>/= stk word buffer Hi Hstk; + [by apply step_invariant|]. + assert (IH1 := IH stk word buffer Hi Hstk). + destruct parse_fix as [[] Hi']=>/=; try by apply IH1. + destruct IH1 as (word' & -> & Hstk')=>//. by apply IH. +Qed. + +(** The interpreter is correct : if it returns a semantic value, then the input + word has this semantic value. +**) +Theorem parse_correct safe buffer log_n_steps: + match parse safe init buffer log_n_steps with + | Parsed_pr sem buffer_new => + exists word_new (pt:parse_tree (NT (start_nt init)) word_new), + buffer = (word_new ++ buffer_new)%buf /\ + pt_sem pt = sem + | _ => True + end. +Proof. + unfold parse. + assert (Hparse := parse_fix_invariant [] [] buffer safe log_n_steps + (parse_subproof init)). + destruct proj1_sig=>//. apply Hparse. constructor. +Qed. + +End Init. + +End Make. diff --git a/MenhirLib/Main.v b/MenhirLib/Main.v new file mode 100644 index 00000000..f6158074 --- /dev/null +++ b/MenhirLib/Main.v @@ -0,0 +1,79 @@ +(****************************************************************************) +(* *) +(* 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. *) +(* *) +(****************************************************************************) + +Require Grammar Automaton Interpreter_correct Interpreter_complete. +From Coq Require Import Syntax Arith. + +Module Make(Export Aut:Automaton.T). +Export Aut.Gram. +Export Aut.GramDefs. + +Module Import Inter := Interpreter.Make Aut. +Module Correct := Interpreter_correct.Make Aut Inter. +Module Complete := Interpreter_complete.Make Aut Inter. + +Definition complete_validator:unit->bool := Complete.Valid.is_complete. +Definition safe_validator:unit->bool := ValidSafe.is_safe. +Definition parse (safe:safe_validator ()=true) init log_n_steps buffer : + parse_result (symbol_semantic_type (NT (start_nt init))):= + parse (ValidSafe.safe_is_validator safe) init buffer log_n_steps. + +(** Correction theorem. **) +Theorem parse_correct + (safe:safe_validator ()= true) init log_n_steps buffer: + match parse safe init log_n_steps buffer with + | Parsed_pr sem buffer_new => + exists word (pt : parse_tree (NT (start_nt init)) word), + buffer = (word ++ buffer_new)%buf /\ + pt_sem pt = sem + | _ => True + end. +Proof. apply Correct.parse_correct. Qed. + +(** Completeness theorem. **) +Theorem parse_complete + (safe:safe_validator () = true) init log_n_steps word buffer_end: + complete_validator () = true -> + forall tree:parse_tree (NT (start_nt init)) word, + match parse safe init log_n_steps (word ++ buffer_end) with + | Fail_pr => False + | Parsed_pr sem_res buffer_end_res => + sem_res = pt_sem tree /\ buffer_end_res = buffer_end /\ + pt_size tree <= 2^log_n_steps + | Timeout_pr => 2^log_n_steps < pt_size tree + end. +Proof. + intros. now apply Complete.parse_complete, Complete.Valid.complete_is_validator. +Qed. + +(** Unambiguity theorem. **) +Theorem unambiguity: + safe_validator () = true -> complete_validator () = true -> inhabited token -> + forall init word, + forall (tree1 tree2:parse_tree (NT (start_nt init)) word), + pt_sem tree1 = pt_sem tree2. +Proof. + intros Hsafe Hcomp [tok] init word tree1 tree2. + pose (buf_end := cofix buf_end := (tok :: buf_end)%buf). + assert (Hcomp1 := parse_complete Hsafe init (pt_size tree1) word buf_end + Hcomp tree1). + assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word buf_end + Hcomp tree2). + destruct parse. + - destruct Hcomp1. + - exfalso. eapply PeanoNat.Nat.lt_irrefl. etransitivity; [|apply Hcomp1]. + eapply Nat.pow_gt_lin_r. constructor. + - destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity. +Qed. + +End Make. diff --git a/MenhirLib/Validator_classes.v b/MenhirLib/Validator_classes.v new file mode 100644 index 00000000..c043cb73 --- /dev/null +++ b/MenhirLib/Validator_classes.v @@ -0,0 +1,74 @@ +(****************************************************************************) +(* *) +(* 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. +From Coq.ssr Require Import ssreflect. +Require Import Alphabet. + +Class IsValidator (P : Prop) (b : bool) := + is_validator : b = true -> P. +Hint Mode IsValidator + -. + +Instance is_validator_true : IsValidator True true. +Proof. done. Qed. + +Instance is_validator_false : IsValidator False false. +Proof. done. Qed. + +Instance is_validator_eq_true b : + IsValidator (b = true) b. +Proof. done. Qed. + +Instance is_validator_and P1 b1 P2 b2 `{IsValidator P1 b1} `{IsValidator P2 b2}: + IsValidator (P1 /\ P2) (if b1 then b2 else false). +Proof. split; destruct b1, b2; auto using is_validator. Qed. + +Instance is_validator_comparable_leibniz_eq A (C:Comparable A) (x y : A) : + ComparableLeibnizEq C -> + IsValidator (x = y) (compare_eqb x y). +Proof. intros ??. by apply compare_eqb_iff. Qed. + +Instance is_validator_comparable_eq_impl A `(Comparable A) (x y : A) P b : + IsValidator P b -> + IsValidator (x = y -> P) (if compare_eqb x y then b else true). +Proof. + intros Hval Val ->. rewrite /compare_eqb compare_refl in Val. auto. +Qed. + +Lemma is_validator_forall_finite A P b `(Finite A) : + (forall (x : A), IsValidator (P x) (b x)) -> + IsValidator (forall (x : A), P x) (forallb b all_list). +Proof. + move=> ? /forallb_forall. + auto using all_list_forall, is_validator, forallb_forall. +Qed. +(* We do not use an instance directly here, because we need somehow to + force Coq to instantiate b with a lambda. *) +Hint Extern 2 (IsValidator (forall x : ?A, _) _) => + eapply (is_validator_forall_finite _ _ (fun (x:A) => _)) + : typeclass_instances. + +(* Hint for synthetizing pattern-matching. *) +Hint Extern 2 (IsValidator (match ?u with _ => _ end) ?b0) => + let b := fresh "b" in + unshelve notypeclasses refine (let b : bool := _ in _); + [destruct u; intros; shelve|]; (* Synthetize `match .. with` in the validator. *) + unify b b0; + unfold b; destruct u; clear b + : typeclass_instances. + +(* Hint for unfolding definitions. This is necessary because many + hints for IsValidator use [Hint Extern], which do not automatically + unfold identifiers. *) +Hint Extern 100 (IsValidator ?X _) => unfold X + : typeclass_instances. diff --git a/MenhirLib/Validator_complete.v b/MenhirLib/Validator_complete.v new file mode 100644 index 00000000..ebb74500 --- /dev/null +++ b/MenhirLib/Validator_complete.v @@ -0,0 +1,394 @@ +(****************************************************************************) +(* *) +(* 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 Derive. +From Coq.ssr Require Import ssreflect. +Require Automaton. +Require Import Alphabet Validator_classes. + +Module Make(Import A:Automaton.T). + +(** We instantiate some sets/map. **) +Module TerminalComparableM <: ComparableM. + Definition t := terminal. + Instance tComparable : Comparable t := _. +End TerminalComparableM. +Module TerminalOrderedType := OrderedType_from_ComparableM TerminalComparableM. +Module StateProdPosComparableM <: ComparableM. + Definition t := (state*production*nat)%type. + Instance tComparable : Comparable t := _. +End StateProdPosComparableM. +Module StateProdPosOrderedType := + OrderedType_from_ComparableM StateProdPosComparableM. + +Module TerminalSet := FSetAVL.Make TerminalOrderedType. +Module StateProdPosMap := FMapAVL.Make StateProdPosOrderedType. + +(** Nullable predicate for symbols and list of symbols. **) +Definition nullable_symb (symbol:symbol) := + match symbol with + | NT nt => nullable_nterm nt + | _ => false + end. + +Definition nullable_word (word:list symbol) := + forallb nullable_symb word. + +(** First predicate for non terminal, symbols and list of symbols, given as FSets. **) +Definition first_nterm_set (nterm:nonterminal) := + fold_left (fun acc t => TerminalSet.add t acc) + (first_nterm nterm) TerminalSet.empty. + +Definition first_symb_set (symbol:symbol) := + match symbol with + | NT nt => first_nterm_set nt + | T t => TerminalSet.singleton t + end. + +Fixpoint first_word_set (word:list symbol) := + match word with + | [] => TerminalSet.empty + | t::q => + if nullable_symb t then + TerminalSet.union (first_symb_set t) (first_word_set q) + else + first_symb_set t + end. + +(** Small helper for finding the part of an item that is after the dot. **) +Definition future_of_prod prod dot_pos : list symbol := + (fix loop n lst := + match n with + | O => lst + | S x => match loop x lst with [] => [] | _::q => q end + end) + dot_pos (rev' (prod_rhs_rev prod)). + +(** We build a fast map to store all the items of all the states. **) +Definition items_map (_:unit): StateProdPosMap.t TerminalSet.t := + fold_left (fun acc state => + fold_left (fun acc item => + let key := (state, prod_item item, dot_pos_item item) in + let data := fold_left (fun acc t => TerminalSet.add t acc) + (lookaheads_item item) TerminalSet.empty + in + let old := + match StateProdPosMap.find key acc with + | Some x => x | None => TerminalSet.empty + end + in + StateProdPosMap.add key (TerminalSet.union data old) acc + ) (items_of_state state) acc + ) all_list (StateProdPosMap.empty TerminalSet.t). + +(** We need to avoid computing items_map each time we need it. To that + purpose, we declare a typeclass specifying that some map is equal to + items_map. *) +Class IsItemsMap m := is_items_map : m = items_map (). + +(** Accessor. **) +Definition find_items_map items_map state prod dot_pos : TerminalSet.t := + match StateProdPosMap.find (state, prod, dot_pos) items_map with + | None => TerminalSet.empty + | Some x => x + end. + +Definition state_has_future state prod (fut:list symbol) (lookahead:terminal) := + exists dot_pos:nat, + fut = future_of_prod prod dot_pos /\ + TerminalSet.In lookahead (find_items_map (items_map ()) state prod dot_pos). + +(** Iterator over items. **) +Definition forallb_items items_map (P:state -> production -> nat -> TerminalSet.t -> bool): bool:= + StateProdPosMap.fold (fun key set acc => + match key with (st, p, pos) => (acc && P st p pos set)%bool end + ) items_map true. + +(** Typeclass instances for synthetizing the validator. *) + +Instance is_validator_subset S1 S2 : + IsValidator (TerminalSet.Subset S1 S2) (TerminalSet.subset S1 S2). +Proof. intros ?. by apply TerminalSet.subset_2. Qed. + +(* While the specification of the validator always quantify over + possible lookahead tokens individually, the validator usually + handles lookahead sets directly instead, for better performances. + + For instance, the validator for [state_has_future], which speaks + about one single lookahead token is a subset operation: +*) +Lemma is_validator_state_has_future_subset st prod pos lookahead lset im fut : + TerminalSet.In lookahead lset -> + fut = future_of_prod prod pos -> + IsItemsMap im -> + IsValidator (state_has_future st prod fut lookahead) + (TerminalSet.subset lset (find_items_map im st prod pos)). +Proof. + intros ? -> -> HSS%TerminalSet.subset_2. exists pos. split=>//. by apply HSS. +Qed. +(* We do not declare this lemma as an instance, and use [Hint Extern] + instead, because the typeclass mechanism has trouble instantiating + some evars if we do not explicitely call [eassumption]. *) +Hint Extern 2 (IsValidator (state_has_future _ _ _ _) _) => + eapply is_validator_state_has_future_subset; [eassumption|eassumption || reflexivity|] +: typeclass_instances. + +(* As said previously, we manipulate lookahead terminal sets instead of + lookahead individually. Hence, when we quantify over a lookahead set + in the specification, we do not do anything in the executable + validator. + + This instance is used for [non_terminal_closed]. *) +Instance is_validator_forall_lookahead_set lset P b: + (forall lookahead, TerminalSet.In lookahead lset -> IsValidator (P lookahead) b) -> + IsValidator (forall lookahead, TerminalSet.In lookahead lset -> P lookahead) b. +Proof. unfold IsValidator. firstorder. Qed. + + +(* Dually, we sometimes still need to explicitelly iterate over a + lookahead set. This is what this lemma allows. + Used only in [end_reduce]. *) +Lemma is_validator_iterate_lset P b lookahead lset : + TerminalSet.In lookahead lset -> + IsValidator P (b lookahead) -> + IsValidator P (TerminalSet.fold (fun lookahead acc => + if acc then b lookahead else false) lset true). +Proof. + intros Hlset%TerminalSet.elements_1 Hval Val. apply Hval. + revert Val. rewrite TerminalSet.fold_1. generalize true at 1. clear -Hlset. + induction Hlset as [? l <-%compare_eq|? l ? IH]=> /= b' Val. + - destruct (b lookahead). by destruct b'. exfalso. by induction l; destruct b'. + - eauto. +Qed. +Hint Extern 100 (IsValidator _ _) => + match goal with + | H : TerminalSet.In ?lookahead ?lset |- _ => + eapply (is_validator_iterate_lset _ (fun lookahead => _) _ _ H); clear H + end +: typeclass_instances. + +(* We often quantify over all the items of all the states of the + automaton. This lemma and the accompanying [Hint Resolve] + declaration allow generating the corresponding executable + validator. + + Note that it turns out that, in all the uses of this pattern, the + first thing we do for each item is pattern-matching over the + future. This lemma also embbed this pattern-matching, which makes + it possible to get the hypothesis [fut' = future_of_prod prod (S pos)] + in the non-nil branch. + + Moreover, note, again, that while the specification quantifies over + lookahead terminals individually, the code provides lookahead sets + instead. *) +Lemma is_validator_forall_items P1 b1 P2 b2 im : + IsItemsMap im -> + + (forall st prod lookahead lset pos, + TerminalSet.In lookahead lset -> + [] = future_of_prod prod pos -> + IsValidator (P1 st prod lookahead) (b1 st prod pos lset)) -> + + (forall st prod pos lookahead lset s fut', + TerminalSet.In lookahead lset -> + fut' = future_of_prod prod (S pos) -> + IsValidator (P2 st prod lookahead s fut') (b2 st prod pos lset s fut')) -> + + IsValidator (forall st prod fut lookahead, + state_has_future st prod fut lookahead -> + match fut with + | [] => P1 st prod lookahead + | s :: fut' => P2 st prod lookahead s fut' + end) + (forallb_items im (fun st prod pos lset => + match future_of_prod prod pos with + | [] => b1 st prod pos lset + | s :: fut' => b2 st prod pos lset s fut' + end)). +Proof. + intros -> Hval1 Hval2 Val st prod fut lookahead (pos & -> & Hlookahead). + rewrite /forallb_items StateProdPosMap.fold_1 in Val. + assert (match future_of_prod prod pos with + | [] => b1 st prod pos (find_items_map (items_map ()) st prod pos) + | s :: fut' => b2 st prod pos (find_items_map (items_map ()) st prod pos) s fut' + end = true). + - unfold find_items_map in *. + assert (Hfind := @StateProdPosMap.find_2 _ (items_map ()) (st, prod, pos)). + destruct StateProdPosMap.find as [lset|]; [|by edestruct (TerminalSet.empty_1); eauto]. + specialize (Hfind _ eq_refl). apply StateProdPosMap.elements_1 in Hfind. + revert Val. generalize true at 1. + induction Hfind as [[? ?] l [?%compare_eq ?]|??? IH]=>?. + + simpl in *; subst. + match goal with |- _ -> ?X = true => destruct X end; [done|]. + rewrite Bool.andb_false_r. clear. induction l as [|[[[??]?]?] l IH]=>//. + + apply IH. + - destruct future_of_prod eqn:EQ. by eapply Hval1; eauto. + eapply Hval2 with (pos := pos); eauto; []. + revert EQ. unfold future_of_prod=>-> //. +Qed. +(* We need a hint for expplicitely instantiating b1 and b2 with lambdas. *) +Hint Extern 0 (IsValidator + (forall st prod fut lookahead, + state_has_future st prod fut lookahead -> _) + _) => + eapply (is_validator_forall_items _ (fun st prod pos lset => _) + _ (fun st prod pos lset s fut' => _)) + : typeclass_instances. + +(* Used in [start_future] only. *) +Instance is_validator_forall_state_has_future im st prod : + IsItemsMap im -> + IsValidator + (forall look, state_has_future st prod (rev' (prod_rhs_rev prod)) look) + (let lookaheads := find_items_map im st prod 0 in + forallb (fun t => TerminalSet.mem t lookaheads) all_list). +Proof. + move=> -> /forallb_forall Val look. + specialize (Val look (all_list_forall _)). exists 0. split=>//. + by apply TerminalSet.mem_2. +Qed. + +(** * Validation for completeness **) + +(** The nullable predicate is a fixpoint : it is correct. **) +Definition nullable_stable := + forall p:production, + if nullable_word (prod_rhs_rev p) then + nullable_nterm (prod_lhs p) = true + else True. + +(** The first predicate is a fixpoint : it is correct. **) +Definition first_stable:= + forall (p:production), + TerminalSet.Subset (first_word_set (rev' (prod_rhs_rev p))) + (first_nterm_set (prod_lhs p)). + +(** The initial state has all the S=>.u items, where S is the start non-terminal **) +Definition start_future := + forall (init:initstate) (p:production), + prod_lhs p = start_nt init -> + forall (t:terminal), + state_has_future init p (rev' (prod_rhs_rev p)) t. + +(** If a state contains an item of the form A->_.av[[b]], where a is a + terminal, then reading an a does a [Shift_act], to a state containing + an item of the form A->_.v[[b]]. **) +Definition terminal_shift := + forall (s1:state) prod fut lookahead, + state_has_future s1 prod fut lookahead -> + match fut with + | T t::q => + match action_table s1 with + | Lookahead_act awp => + match awp t with + | Shift_act s2 _ => + state_has_future s2 prod q lookahead + | _ => False + end + | _ => False + end + | _ => True + end. + +(** If a state contains an item of the form A->_.[[a]], then either we do a + [Default_reduce_act] of the corresponding production, either a is a + terminal (ie. there is a lookahead terminal), and reading a does a + [Reduce_act] of the corresponding production. **) +Definition end_reduce := + forall (s:state) prod fut lookahead, + state_has_future s prod fut lookahead -> + match fut with + | [] => + match action_table s with + | Default_reduce_act p => p = prod + | Lookahead_act awt => + match awt lookahead with + | Reduce_act p => p = prod + | _ => False + end + end + | _ => True + end. + +Definition is_end_reduce items_map := + forallb_items items_map (fun s prod pos lset => + match future_of_prod prod pos with + | [] => + match action_table s with + | Default_reduce_act p => compare_eqb p prod + | Lookahead_act awt => + TerminalSet.fold (fun lookahead acc => + match awt lookahead with + | Reduce_act p => (acc && compare_eqb p prod)%bool + | _ => false + end) lset true + end + | _ => true + end). + +(** If a state contains an item of the form A->_.Bv[[b]], where B is a + non terminal, then the goto table says we have to go to a state containing + an item of the form A->_.v[[b]]. **) +Definition non_terminal_goto := + forall (s1:state) prod fut lookahead, + state_has_future s1 prod fut lookahead -> + match fut with + | NT nt::q => + match goto_table s1 nt with + | Some (exist _ s2 _) => + state_has_future s2 prod q lookahead + | None => False + end + | _ => True + end. + +Definition start_goto := + forall (init:initstate), + match goto_table init (start_nt init) with + | None => True + | Some _ => False + end. + +(** Closure property of item sets : if a state contains an item of the form + A->_.Bv[[b]], then for each production B->u and each terminal a of + first(vb), the state contains an item of the form B->_.u[[a]] **) +Definition non_terminal_closed := + forall s1 prod fut lookahead, + state_has_future s1 prod fut lookahead -> + match fut with + | NT nt::q => + forall p, prod_lhs p = nt -> + (if nullable_word q then + state_has_future s1 p (future_of_prod p 0) lookahead + else True) /\ + (forall lookahead2, + TerminalSet.In lookahead2 (first_word_set q) -> + state_has_future s1 p (future_of_prod p 0) lookahead2) + | _ => True + end. + +(** The automaton is complete **) +Definition complete := + nullable_stable /\ first_stable /\ start_future /\ terminal_shift + /\ end_reduce /\ non_terminal_goto /\ start_goto /\ non_terminal_closed. + +Derive is_complete_0 +SuchThat (forall im, IsItemsMap im -> IsValidator complete (is_complete_0 im)) +As complete_0_is_validator. +Proof. intros im. subst is_complete_0. instantiate (1:=fun im => _). apply _. Qed. + +Definition is_complete (_:unit) := is_complete_0 (items_map ()). +Lemma complete_is_validator : IsValidator complete (is_complete ()). +Proof. by apply complete_0_is_validator. Qed. + +End Make. diff --git a/MenhirLib/Validator_safe.v b/MenhirLib/Validator_safe.v new file mode 100644 index 00000000..2d2ea4b3 --- /dev/null +++ b/MenhirLib/Validator_safe.v @@ -0,0 +1,234 @@ +(****************************************************************************) +(* *) +(* 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 Derive. +From Coq.ssr Require Import ssreflect. +Require Automaton. +Require Import Alphabet Validator_classes. + +Module Make(Import A:Automaton.T). + +(** The singleton predicate for states **) +Definition singleton_state_pred (state:state) := + (fun state' => match compare state state' with Eq => true |_ => false end). + +(** [past_state_of_non_init_state], extended for all states. **) +Definition past_state_of_state (state:state) := + match state with + | Init _ => [] + | Ninit nis => past_state_of_non_init_state nis + end. + +(** Concatenations of last and past **) +Definition head_symbs_of_state (state:state) := + match state with + | Init _ => [] + | Ninit s => + last_symb_of_non_init_state s::past_symb_of_non_init_state s + end. +Definition head_states_of_state (state:state) := + singleton_state_pred state::past_state_of_state state. + +(** * Validation for correctness **) + +(** Prefix predicate between two lists of symbols. **) +Inductive prefix: list symbol -> list symbol -> Prop := +| prefix_nil: forall l, prefix [] l +| prefix_cons: forall l1 l2 x, prefix l1 l2 -> prefix (x::l1) (x::l2). + +(** [prefix] is transitive **) +Lemma prefix_trans: + forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3. +Proof. + intros l1 l2 l3 H1 H2. revert l3 H2. + induction H1; [now constructor|]. inversion 1. subst. constructor. eauto. +Qed. + +Fixpoint is_prefix (l1 l2:list symbol) := + match l1, l2 with + | [], _ => true + | t1::q1, t2::q2 => (compare_eqb t1 t2 && is_prefix q1 q2)%bool + | _::_, [] => false + end. + +Instance prefix_is_validator l1 l2 : IsValidator (prefix l1 l2) (is_prefix l1 l2). +Proof. + revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref. + - constructor. + - destruct l2 as [|x2 l2]=>//. + move: Hpref=> /andb_prop [/compare_eqb_iff -> /IH ?]. by constructor. +Qed. + +(** If we shift, then the known top symbols of the destination state is + a prefix of the known top symbols of the source state, with the new + symbol added. **) +Definition shift_head_symbs := + forall s, + match action_table s with + | Lookahead_act awp => forall t, + match awp t with + | Shift_act s2 _ => + prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) + | _ => True + end + | _ => True + end. + +(** When a goto happens, then the known top symbols of the destination state + is a prefix of the known top symbols of the source state, with the new + symbol added. **) +Definition goto_head_symbs := + forall s nt, + match goto_table s nt with + | Some (exist _ s2 _) => + prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) + | None => True + end. + +(** We have to say the same kind of checks for the assumptions about the + states stack. However, theses assumptions are predicates. So we define + a notion of "prefix" over predicates lists, that means, basically, that + an assumption entails another **) +Inductive prefix_pred: list (state->bool) -> list (state->bool) -> Prop := + | prefix_pred_nil: forall l, prefix_pred [] l + | prefix_pred_cons: forall l1 l2 f1 f2, + (forall x, implb (f2 x) (f1 x) = true) -> + prefix_pred l1 l2 -> prefix_pred (f1::l1) (f2::l2). + +(** [prefix_pred] is transitive **) +Lemma prefix_pred_trans: + forall (l1 l2 l3:list (state->bool)), + prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3. +Proof. + intros l1 l2 l3 H1 H2. revert l3 H2. + induction H1 as [|l1 l2 f1 f2 Hf2f1]; [now constructor|]. + intros l3. inversion 1 as [|??? f3 Hf3f2]. subst. constructor; [|now eauto]. + intros x. specialize (Hf3f2 x). specialize (Hf2f1 x). + repeat destruct (_ x); auto. +Qed. + +Fixpoint is_prefix_pred (l1 l2:list (state->bool)) := + match l1, l2 with + | [], _ => true + | f1::q1, f2::q2 => + (forallb (fun x => implb (f2 x) (f1 x)) all_list + && is_prefix_pred q1 q2)%bool + | _::_, [] => false + end. + +Instance prefix_pred_is_validator l1 l2 : + IsValidator (prefix_pred l1 l2) (is_prefix_pred l1 l2). +Proof. + revert l2. induction l1 as [|x1 l1 IH]=>l2 Hpref. + - constructor. + - destruct l2 as [|x2 l2]=>//. + move: Hpref=> /andb_prop [/forallb_forall ? /IH ?]. + constructor; auto using all_list_forall. +Qed. + +(** The assumptions about state stack is conserved when we shift **) +Definition shift_past_state := + forall s, + match action_table s with + | Lookahead_act awp => forall t, + match awp t with + | Shift_act s2 _ => + prefix_pred (past_state_of_non_init_state s2) + (head_states_of_state s) + | _ => True + end + | _ => True + end. + +(** The assumptions about state stack is conserved when we do a goto **) +Definition goto_past_state := + forall s nt, + match goto_table s nt with + | Some (exist _ s2 _) => + prefix_pred (past_state_of_non_init_state s2) + (head_states_of_state s) + | None => True + end. + +(** What states are possible after having popped these symbols from the + stack, given the annotation of the current state ? **) +Inductive state_valid_after_pop (s:state): + list symbol -> list (state -> bool) -> Prop := + | state_valid_after_pop_nil1: + forall p pl, p s = true -> state_valid_after_pop s [] (p::pl) + | state_valid_after_pop_nil2: + forall sl, state_valid_after_pop s sl [] + | state_valid_after_pop_cons: + forall st sq p pl, state_valid_after_pop s sq pl -> + state_valid_after_pop s (st::sq) (p::pl). + +Fixpoint is_state_valid_after_pop (state:state) (to_pop:list symbol) annot := + match annot, to_pop with + | [], _ => true + | p::_, [] => p state + | p::pl, s::sl => is_state_valid_after_pop state sl pl + end. + +Instance impl_is_state_valid_after_pop_is_validator state sl pl P b : + IsValidator P b -> + IsValidator (state_valid_after_pop state sl pl -> P) + (if is_state_valid_after_pop state sl pl then b else true). +Proof. + destruct (is_state_valid_after_pop state0 sl pl) eqn:EQ. + - intros ??. auto using is_validator. + - intros _ _ Hsvap. exfalso. induction Hsvap=>//; [simpl in EQ; congruence|]. + by destruct sl. +Qed. + +(** A state is valid for reducing a production when : + - The assumptions on the state are such that we will find the right hand + side of the production on the stack. + - We will be able to do a goto after having popped the right hand side. +**) +Definition valid_for_reduce (state:state) prod := + prefix (prod_rhs_rev prod) (head_symbs_of_state state) /\ + forall state_new, + state_valid_after_pop state_new + (prod_rhs_rev prod) (head_states_of_state state) -> + match goto_table state_new (prod_lhs prod) with + | None => + match state_new with + | Init i => prod_lhs prod = start_nt i + | Ninit _ => False + end + | _ => True + end. + +(** All the states that does a reduce are valid for reduction **) +Definition reduce_ok := + forall s, + match action_table s with + | Lookahead_act awp => + forall t, match awp t with + | Reduce_act p => valid_for_reduce s p + | _ => True + end + | Default_reduce_act p => valid_for_reduce s p + end. + +(** The automaton is safe **) +Definition safe := + shift_head_symbs /\ goto_head_symbs /\ shift_past_state /\ + goto_past_state /\ reduce_ok. + +Derive is_safe +SuchThat (IsValidator safe (is_safe ())) +As safe_is_validator. +Proof. subst is_safe. instantiate (1:=fun _ => _). apply _. Qed. + +End Make. |