From b8552c55a3c65a3f598d155aeb764e68841ba501 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Sun, 3 Jun 2018 18:26:33 +0200 Subject: Fix menhirLib namespaces, following changes in Menhir version 20180530 --- cparser/MenhirLib/Alphabet.v | 320 ++++++++++++++ cparser/MenhirLib/Automaton.v | 167 ++++++++ cparser/MenhirLib/Grammar.v | 166 ++++++++ cparser/MenhirLib/Interpreter.v | 228 ++++++++++ cparser/MenhirLib/Interpreter_complete.v | 686 +++++++++++++++++++++++++++++++ cparser/MenhirLib/Interpreter_correct.v | 228 ++++++++++ cparser/MenhirLib/Interpreter_safe.v | 275 +++++++++++++ cparser/MenhirLib/Main.v | 92 +++++ cparser/MenhirLib/Tuples.v | 49 +++ cparser/MenhirLib/Validator_complete.v | 542 ++++++++++++++++++++++++ cparser/MenhirLib/Validator_safe.v | 414 +++++++++++++++++++ cparser/validator/Alphabet.v | 320 -------------- cparser/validator/Automaton.v | 167 -------- cparser/validator/Grammar.v | 166 -------- cparser/validator/Interpreter.v | 228 ---------- cparser/validator/Interpreter_complete.v | 686 ------------------------------- cparser/validator/Interpreter_correct.v | 228 ---------- cparser/validator/Interpreter_safe.v | 275 ------------- cparser/validator/Main.v | 92 ----- cparser/validator/Tuples.v | 49 --- cparser/validator/Validator_complete.v | 542 ------------------------ cparser/validator/Validator_safe.v | 414 ------------------- 22 files changed, 3167 insertions(+), 3167 deletions(-) create mode 100644 cparser/MenhirLib/Alphabet.v create mode 100644 cparser/MenhirLib/Automaton.v create mode 100644 cparser/MenhirLib/Grammar.v create mode 100644 cparser/MenhirLib/Interpreter.v create mode 100644 cparser/MenhirLib/Interpreter_complete.v create mode 100644 cparser/MenhirLib/Interpreter_correct.v create mode 100644 cparser/MenhirLib/Interpreter_safe.v create mode 100644 cparser/MenhirLib/Main.v create mode 100644 cparser/MenhirLib/Tuples.v create mode 100644 cparser/MenhirLib/Validator_complete.v create mode 100644 cparser/MenhirLib/Validator_safe.v delete mode 100644 cparser/validator/Alphabet.v delete mode 100644 cparser/validator/Automaton.v delete mode 100644 cparser/validator/Grammar.v delete mode 100644 cparser/validator/Interpreter.v delete mode 100644 cparser/validator/Interpreter_complete.v delete mode 100644 cparser/validator/Interpreter_correct.v delete mode 100644 cparser/validator/Interpreter_safe.v delete mode 100644 cparser/validator/Main.v delete mode 100644 cparser/validator/Tuples.v delete mode 100644 cparser/validator/Validator_complete.v delete mode 100644 cparser/validator/Validator_safe.v (limited to 'cparser') diff --git a/cparser/MenhirLib/Alphabet.v b/cparser/MenhirLib/Alphabet.v new file mode 100644 index 00000000..a13f69b0 --- /dev/null +++ b/cparser/MenhirLib/Alphabet.v @@ -0,0 +1,320 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Int31. +Require Import Cyclic31. +Require Import Omega. +Require Import List. +Require Import Syntax. +Require Import Relations. +Require Import 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 usual equality. **) +Class ComparableUsualEq {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:ComparableUsualEq 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. + +(** [Comparable] provides a decidable equality. **) +Definition compare_eqdec {A:Type} {C:Comparable A} {U:ComparableUsualEq C} (x y:A): + {x = y} + {x <> y}. +Proof. +destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..]; + right; intro; destruct H; rewrite compare_refl in Heqc; discriminate. +Defined. + +Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq. + +(** A pair of ComparableUsualEq is ComparableUsualEq **) +Instance PairComparableUsualEq + {A:Type} {CA:Comparable A} (UA:ComparableUsualEq CA) + {B:Type} {CB:Comparable B} (UB:ComparableUsualEq CB) : + ComparableUsualEq (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 [ComparableUsualEq] and [Finite]. **) +Class Alphabet (A:Type) := { + AlphabetComparable :> Comparable A; + AlphabetComparableUsualEq :> ComparableUsualEq 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 + [Int31] **) +Class Numbered (A:Type) := { + inj : A -> int31; + surj : int31 -> A; + surj_inj_compat : forall x, surj (inj x) = x; + inj_bound : int31; + inj_bound_spec : forall x, (phi (inj x) < phi inj_bound)%Z +}. + +Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A := + { AlphabetComparable := + {| compare := fun x y => compare31 (inj x) (inj y) |}; + AlphabetFinite := + {| all_list := fst (iter_int31 inj_bound _ + (fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }. +Next Obligation. apply Zcompare_antisym. Qed. +Next Obligation. +destruct c. unfold compare31 in *. +rewrite Z.compare_eq_iff in *. congruence. +eapply Zcompare_Lt_trans. apply H. apply H0. +eapply Zcompare_Gt_trans. apply H. apply H0. +Qed. +Next Obligation. +intros x y H. unfold compare, compare31 in H. +rewrite Z.compare_eq_iff in *. +rewrite <- surj_inj_compat, <- phi_inv_phi with (inj y), <- H. +rewrite phi_inv_phi, surj_inj_compat; reflexivity. +Qed. +Next Obligation. +rewrite iter_int31_iter_nat. +pose proof (inj_bound_spec x). +match goal with |- In x (fst ?p) => destruct p as [] eqn:? end. +replace inj_bound with i in H. +revert l i Heqp x H. +induction (Z.abs_nat (phi inj_bound)); intros. +inversion Heqp; clear Heqp; subst. +rewrite spec_0 in H. pose proof (phi_bounded (inj x)). omega. +simpl in Heqp. +destruct nat_rect; specialize (IHn _ _ (eq_refl _) x); simpl in *. +inversion Heqp. subst. clear Heqp. +rewrite phi_incr in H. +pose proof (phi_bounded i0). +pose proof (phi_bounded (inj x)). +destruct (Z_lt_le_dec (Z.succ (phi i0)) (2 ^ Z.of_nat size)%Z). +rewrite Zmod_small in H by omega. +apply Zlt_succ_le, Zle_lt_or_eq in H. +destruct H; simpl; auto. left. +rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity. +replace (Z.succ (phi i0)) with (2 ^ Z.of_nat size)%Z in H by omega. +rewrite Z_mod_same_full in H. +exfalso; omega. +rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. +pose proof (phi_bounded inj_bound); pose proof (phi_bounded i). +rewrite <- Z.abs_eq with (phi i), <- Z.abs_eq with (phi inj_bound) by omega. +clear H H0 H1. +do 2 rewrite <- Zabs2Nat.id_abs. +f_equal. +revert l i Heqp. +assert (Z.abs_nat (phi inj_bound) < Z.abs_nat (2^31)). +apply Zabs_nat_lt, phi_bounded. +induction (Z.abs_nat (phi inj_bound)); intros. +inversion Heqp; reflexivity. +inversion Heqp; clear H1 H2 Heqp. +match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end. +pose proof (phi_bounded i0). +erewrite <- IHn, <- Zabs2Nat.inj_succ in H |- *; eauto; try omega. +rewrite phi_incr, Zmod_small; intuition; try omega. +apply inj_lt in H. +pose proof Z.le_le_succ_r. +do 2 rewrite Zabs2Nat.id_abs, Z.abs_eq in H; now eauto. +Qed. + +(** Previous class instances for [option A] **) +Program Instance OptionComparable {A:Type} (C:Comparable A) : Comparable (option A) := + { compare := fun x y => + match x, y return comparison with + | None, None => Eq + | None, Some _ => Lt + | Some _, None => Gt + | Some x, Some y => compare x y + end }. +Next Obligation. +destruct x, y; intuition. +apply compare_antisym. +Qed. +Next Obligation. +destruct x, y, z; try now intuition; +try (rewrite <- H in H0; discriminate). +apply (compare_trans _ _ _ _ H H0). +Qed. + +Instance OptionComparableUsualEq {A:Type} {C:Comparable A} (U:ComparableUsualEq C) : + ComparableUsualEq (OptionComparable C). +Proof. +intros x y. +destruct x, y; intuition; try discriminate. +rewrite (compare_eq a a0); intuition. +Qed. + +Program Instance OptionFinite {A:Type} (E:Finite A) : Finite (option A) := + { all_list := None :: map Some all_list }. +Next Obligation. +destruct x; intuition. +right. +apply in_map. +apply all_list_forall. +Defined. + +(** 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/cparser/MenhirLib/Automaton.v b/cparser/MenhirLib/Automaton.v new file mode 100644 index 00000000..fc995298 --- /dev/null +++ b/cparser/MenhirLib/Automaton.v @@ -0,0 +1,167 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Grammar. +Require Import Orders. +Require Export Alphabet. +Require Export List. +Require Export 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/cparser/MenhirLib/Grammar.v b/cparser/MenhirLib/Grammar.v new file mode 100644 index 00000000..8e427cd9 --- /dev/null +++ b/cparser/MenhirLib/Grammar.v @@ -0,0 +1,166 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import List. +Require Import Syntax. +Require Import Alphabet. +Require Import Orders. +Require Tuples. + +(** 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); intuition. + rewrite (compare_eq n n0); intuition. + Qed. + Next Obligation. + rewrite in_app_iff. + destruct x; [left | right]; apply in_map; apply all_list_forall. + Qed. + +End Symbol. + +Module Type T. + Export Tuples. + + 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. + Parameter prod_rhs_rev: production -> list symbol. + Parameter prod_action: + forall p:production, + arrows_left + (map symbol_semantic_type (rev (prod_rhs_rev p))) + (symbol_semantic_type (NT (prod_lhs p))). + +End T. + +Module Defs(Import G:T). + + (** A token is a terminal and a semantic value for this terminal. **) + Definition token := {t:terminal & symbol_semantic_type (T t)}. + + (** A grammar creates a relation between word of tokens and semantic values. + This relation is parametrized by the head symbol. It defines the + "semantics" of the grammar. This relation is defined by a notion of + parse tree. **) + Inductive parse_tree: + forall (head_symbol:symbol) (word:list token) + (semantic_value:symbol_semantic_type head_symbol), Type := + + (** A single token has its semantic value as semantic value, for the + corresponding terminal as head symbol. **) + | Terminal_pt: + forall (t:terminal) (sem:symbol_semantic_type (T t)), + parse_tree (T t) + [existT (fun t => symbol_semantic_type (T t)) t sem] sem + + (** Given a production, if a word has a list of semantic values for the + right hand side as head symbols, then this word has the semantic value + given by the semantic action of the production for the left hand side + as head symbol.**) + | Non_terminal_pt: + forall {p:production} {word:list token} + {semantic_values:tuple (map symbol_semantic_type (rev (prod_rhs_rev p)))}, + parse_tree_list (rev (prod_rhs_rev p)) word semantic_values -> + parse_tree (NT (prod_lhs p)) word (uncurry (prod_action p) semantic_values) + + (** Basically the same relation as before, but for list of head symbols (ie. + We are building a forest of syntax trees. It is mutually recursive with the + previous relation **) + with parse_tree_list: + forall (head_symbols:list symbol) (word:list token) + (semantic_values:tuple (map symbol_semantic_type head_symbols)), + Type := + + (** The empty word has [()] as semantic for [[]] as head symbols list **) + | Nil_ptl: parse_tree_list [] [] () + + (** The cons of the semantic value for one head symbol and for a list of head + symbols **) + | Cons_ptl: + (** The semantic for the head **) + forall {head_symbolt:symbol} {wordt:list token} + {semantic_valuet:symbol_semantic_type head_symbolt}, + parse_tree head_symbolt wordt semantic_valuet -> + + (** and the semantic for the tail **) + forall {head_symbolsq:list symbol} {wordq:list token} + {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, + parse_tree_list head_symbolsq wordq semantic_valuesq -> + + (** give the semantic of the cons **) + parse_tree_list + (head_symbolt::head_symbolsq) + (wordt++wordq) + (semantic_valuet, semantic_valuesq). + + + Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) := + match tree with + | Terminal_pt _ _ => 1 + | Non_terminal_pt l => S (ptl_size l) + end + with ptl_size {head_symbols word sems} (tree:parse_tree_list head_symbols word sems) := + match tree with + | Nil_ptl => 0 + | Cons_ptl t q => + pt_size t + ptl_size q + end. +End Defs. diff --git a/cparser/MenhirLib/Interpreter.v b/cparser/MenhirLib/Interpreter.v new file mode 100644 index 00000000..4ac02693 --- /dev/null +++ b/cparser/MenhirLib/Interpreter.v @@ -0,0 +1,228 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Streams. +Require Import List. +Require Import Syntax. +Require Automaton. +Require Import Alphabet. + +Module Make(Import A:Automaton.T). + +(** The error monad **) +Inductive result (A:Type) := + | Err: result A + | OK: A -> result A. + +Arguments Err [A]. +Arguments OK [A]. + +Definition bind {A B: Type} (f: result A) (g: A -> result B): result B := + match f with + | OK x => g x + | Err => Err + end. + +Definition bind2 {A B C: Type} (f: result (A * B)) (g: A -> B -> result C): + result C := + match f with + | OK (x, y) => g x y + | Err => Err + end. + +Notation "'do' X <- A ; B" := (bind A (fun X => B)) + (at level 200, X ident, A at level 100, B at level 200). + +Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) + (at level 200, X ident, Y ident, A at level 100, B at level 200). + +(** Some operations on streams **) + +(** Concatenation of a list and a stream **) +Fixpoint app_str {A:Type} (l:list A) (s:Stream A) := + match l with + | nil => s + | cons t q => Cons t (app_str q s) + end. + +Infix "++" := app_str (right associativity, at level 60). + +Lemma app_str_app_assoc {A:Type} (l1 l2:list A) (s:Stream A) : + l1 ++ (l2 ++ s) = (l1 ++ l2) ++ s. +Proof. +induction l1. +reflexivity. +simpl. +rewrite IHl1. +reflexivity. +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 Init. + +Variable init : initstate. + +(** The top state of a stack **) +Definition state_of_stack (stack:stack): state := + match stack with + | [] => init + | existT _ s _::_ => s + end. + +(** [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) (stack_cur:stack): + forall {A:Type} (action:arrows_right A (map symbol_semantic_type symbols_to_pop)), + result (stack * A) := + match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), result (stack * A) with + | [] => fun A action => OK (stack_cur, action) + | t::q => fun A action => + match stack_cur with + | existT _ state_cur sem::stack_rec => + match compare_eqdec (last_symb_of_non_init_state state_cur) t with + | left e => + let sem_conv := eq_rect _ symbol_semantic_type sem _ e in + pop q stack_rec (action sem_conv) + | right _ => Err + end + | [] => Err + end + end. + +(** [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)) -> Stream token -> step_result + | Progress_sr: stack -> Stream token -> step_result. + +Program Definition prod_action': + forall p, + arrows_right (symbol_semantic_type (NT (prod_lhs p))) + (map symbol_semantic_type (prod_rhs_rev p)):= + fun p => + eq_rect _ (fun x => x) (prod_action p) _ _. +Next Obligation. +unfold arrows_left, arrows_right; simpl. +rewrite <- fold_left_rev_right, <- map_rev, rev_involutive. +reflexivity. +Qed. + +(** [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 stack_cur production buffer: result step_result := + do (stack_new, sem) <- + pop (prod_rhs_rev production) stack_cur (prod_action' production); + match goto_table (state_of_stack stack_new) (prod_lhs production) with + | Some (exist _ state_new e) => + let sem := eq_rect _ _ sem _ e in + OK (Progress_sr (existT noninitstate_type state_new sem::stack_new) buffer) + | None => + match stack_new with + | [] => + match compare_eqdec (prod_lhs production) (start_nt init) with + | left e => + let sem := eq_rect _ (fun nt => symbol_semantic_type (NT nt)) sem _ e in + OK (Accept_sr sem buffer) + | right _ => Err + end + | _::_ => Err + end + end. + +(** One step of parsing. **) +Definition step stack_cur buffer: result step_result := + match action_table (state_of_stack stack_cur) with + | Default_reduce_act production => + reduce_step stack_cur production buffer + | Lookahead_act awt => + match Streams.hd buffer with + | existT _ term sem => + match awt term with + | Shift_act state_new e => + let sem_conv := eq_rect _ symbol_semantic_type sem _ e in + OK (Progress_sr (existT noninitstate_type state_new sem_conv::stack_cur) + (Streams.tl buffer)) + | Reduce_act production => + reduce_step stack_cur production buffer + | Fail_action => + OK Fail_sr + end + end + end. + +(** The parsing use a [nat] parameter [n_steps], so that we do not have to prove + terminaison, which is difficult. So the 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 [n_steps]), either a parsed semantic + value with a rest of the input buffer. +**) +Inductive parse_result := + | Fail_pr: parse_result + | Timeout_pr: parse_result + | Parsed_pr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> parse_result. + +Fixpoint parse_fix stack_cur buffer n_steps: result parse_result:= + match n_steps with + | O => OK Timeout_pr + | S it => + do r <- step stack_cur buffer; + match r with + | Fail_sr => OK Fail_pr + | Accept_sr t buffer_new => OK (Parsed_pr t buffer_new) + | Progress_sr s buffer_new => parse_fix s buffer_new it + end + end. + +Definition parse buffer n_steps: result parse_result := + parse_fix [] buffer n_steps. + +End Init. + +Arguments Fail_sr [init]. +Arguments Accept_sr [init] _ _. +Arguments Progress_sr [init] _ _. + +Arguments Fail_pr [init]. +Arguments Timeout_pr [init]. +Arguments Parsed_pr [init] _ _. + +End Make. + +Module Type T(A:Automaton.T). + Include (Make A). +End T. diff --git a/cparser/MenhirLib/Interpreter_complete.v b/cparser/MenhirLib/Interpreter_complete.v new file mode 100644 index 00000000..2e64b8da --- /dev/null +++ b/cparser/MenhirLib/Interpreter_complete.v @@ -0,0 +1,686 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Streams. +Require Import ProofIrrelevance. +Require Import Equality. +Require Import List. +Require Import Syntax. +Require Import Alphabet. +Require Import Arith. +Require Grammar. +Require Automaton. +Require Interpreter. +Require Validator_complete. + +Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A). +Module Import Valid := Validator_complete.Make A. + +(** * Completeness Proof **) + +Section Completeness_Proof. + +Hypothesis complete: complete. + +Proposition nullable_stable: nullable_stable. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition first_stable: first_stable. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition start_future: start_future. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition terminal_shift: terminal_shift. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition end_reduce: end_reduce. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition start_goto: start_goto. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition non_terminal_goto: non_terminal_goto. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. +Proposition non_terminal_closed: non_terminal_closed. +Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. + +(** If the nullable predicate has been validated, then it is correct. **) +Lemma nullable_correct: + forall head sem word, word = [] -> + parse_tree head word sem -> nullable_symb head = true +with nullable_correct_list: + forall heads sems word, word = [] -> + parse_tree_list heads word sems -> nullable_word heads = true. +Proof with eauto. +intros. +destruct X. +congruence. +apply nullable_stable... +intros. +destruct X; simpl... +apply andb_true_intro. +apply app_eq_nil in H; destruct H; split... +Qed. + +(** If the first predicate has been validated, then it is correct. **) +Lemma first_correct: + forall head sem word t q, word = t::q -> + parse_tree head word sem -> + TerminalSet.In (projT1 t) (first_symb_set head) +with first_correct_list: + forall heads sems word t q, word = t::q -> + parse_tree_list heads word sems -> + TerminalSet.In (projT1 t) (first_word_set heads). +Proof with eauto. +intros. +destruct X. +inversion H; subst. +apply TerminalSet.singleton_2, compare_refl... +apply first_stable... +intros. +destruct X. +congruence. +simpl. +case_eq wordt; intros. +erewrite nullable_correct... +apply TerminalSet.union_3. +subst... +rewrite H0 in *; inversion H; destruct H2. +destruct (nullable_symb head_symbolt)... +apply TerminalSet.union_2... +Qed. + +Variable init: initstate. +Variable full_word: list token. +Variable buffer_end: Stream token. +Variable full_sem: symbol_semantic_type (NT (start_nt init)). + +Inductive pt_zipper: + forall (hole_symb:symbol) (hole_word:list token) + (hole_sem:symbol_semantic_type hole_symb), Type := +| Top_ptz: + pt_zipper (NT (start_nt init)) (full_word) (full_sem) +| Cons_ptl_ptz: + forall {head_symbolt:symbol} + {wordt:list token} + {semantic_valuet:symbol_semantic_type head_symbolt}, + + forall {head_symbolsq:list symbol} + {wordq:list token} + {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, + parse_tree_list head_symbolsq wordq semantic_valuesq -> + + ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq) + (semantic_valuet,semantic_valuesq) -> + + pt_zipper head_symbolt wordt semantic_valuet +with ptl_zipper: + forall (hole_symbs:list symbol) (hole_word:list token) + (hole_sems:tuple (map symbol_semantic_type hole_symbs)), Type := +| Non_terminal_pt_ptlz: + forall {p:production} {word:list token} + {semantic_values:tuple (map symbol_semantic_type (rev (prod_rhs_rev p)))}, + pt_zipper (NT (prod_lhs p)) word (uncurry (prod_action p) semantic_values) -> + ptl_zipper (rev (prod_rhs_rev p)) word semantic_values + +| Cons_ptl_ptlz: + forall {head_symbolt:symbol} + {wordt:list token} + {semantic_valuet:symbol_semantic_type head_symbolt}, + parse_tree head_symbolt wordt semantic_valuet -> + + forall {head_symbolsq:list symbol} + {wordq:list token} + {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, + + ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq) + (semantic_valuet,semantic_valuesq) -> + + ptl_zipper head_symbolsq wordq semantic_valuesq. + +Fixpoint ptlz_cost {hole_symbs hole_word hole_sems} + (ptlz:ptl_zipper hole_symbs hole_word hole_sems) := + match ptlz with + | Non_terminal_pt_ptlz ptz => + ptz_cost ptz + | Cons_ptl_ptlz pt ptlz' => + ptlz_cost ptlz' + end +with ptz_cost {hole_symb hole_word hole_sem} + (ptz:pt_zipper hole_symb hole_word hole_sem) := + match ptz with + | Top_ptz => 0 + | Cons_ptl_ptz ptl ptlz' => + 1 + ptl_size ptl + ptlz_cost ptlz' + end. + +Inductive pt_dot: Type := +| Reduce_ptd: ptl_zipper [] [] () -> pt_dot +| Shift_ptd: + forall (term:terminal) (sem: symbol_semantic_type (T term)) + {symbolsq wordq semsq}, + parse_tree_list symbolsq wordq semsq -> + ptl_zipper (T term::symbolsq) (existT (fun t => symbol_semantic_type (T t)) term sem::wordq) (sem, semsq) -> + pt_dot. + +Definition ptd_cost (ptd:pt_dot) := + match ptd with + | Reduce_ptd ptlz => ptlz_cost ptlz + | Shift_ptd _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz + end. + +Fixpoint ptlz_buffer {hole_symbs hole_word hole_sems} + (ptlz:ptl_zipper hole_symbs hole_word hole_sems): Stream token := + match ptlz with + | Non_terminal_pt_ptlz ptz => + ptz_buffer ptz + | Cons_ptl_ptlz _ ptlz' => + ptlz_buffer ptlz' + end +with ptz_buffer {hole_symb hole_word hole_sem} + (ptz:pt_zipper hole_symb hole_word hole_sem): Stream token := + match ptz with + | Top_ptz => buffer_end + | @Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' => + wordq++ptlz_buffer ptlz' + end. + +Definition ptd_buffer (ptd:pt_dot) := + match ptd with + | Reduce_ptd ptlz => ptlz_buffer ptlz + | @Shift_ptd term sem _ wordq _ _ ptlz => + Cons (existT (fun t => symbol_semantic_type (T t)) term sem) + (wordq ++ ptlz_buffer ptlz) + end. + +Fixpoint ptlz_prod {hole_symbs hole_word hole_sems} + (ptlz:ptl_zipper hole_symbs hole_word hole_sems): production := + match ptlz with + | @Non_terminal_pt_ptlz prod _ _ _ => prod + | Cons_ptl_ptlz _ ptlz' => + ptlz_prod ptlz' + end. + +Fixpoint ptlz_past {hole_symbs hole_word hole_sems} + (ptlz:ptl_zipper hole_symbs hole_word hole_sems): list symbol := + match ptlz with + | Non_terminal_pt_ptlz _ => [] + | @Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz' + end. + +Lemma ptlz_past_ptlz_prod: + forall hole_symbs hole_word hole_sems + (ptlz:ptl_zipper hole_symbs hole_word hole_sems), + rev_append hole_symbs (ptlz_past ptlz) = prod_rhs_rev (ptlz_prod ptlz). +Proof. +fix ptlz_past_ptlz_prod 4. +destruct ptlz; simpl. +rewrite <- rev_alt, rev_involutive; reflexivity. +apply (ptlz_past_ptlz_prod _ _ _ ptlz). +Qed. + +Definition ptlz_state_compat {hole_symbs hole_word hole_sems} + (ptlz:ptl_zipper hole_symbs hole_word hole_sems) + (state:state): Prop := + state_has_future state (ptlz_prod ptlz) hole_symbs + (projT1 (Streams.hd (ptlz_buffer ptlz))). + +Fixpoint ptlz_stack_compat {hole_symbs hole_word hole_sems} + (ptlz:ptl_zipper hole_symbs hole_word hole_sems) + (stack:stack): Prop := + ptlz_state_compat ptlz (state_of_stack init stack) /\ + match ptlz with + | Non_terminal_pt_ptlz ptz => + ptz_stack_compat ptz stack + | @Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' => + match stack with + | [] => False + | existT _ _ sem'::stackq => + ptlz_stack_compat ptlz' stackq /\ + sem ~= sem' + end + end +with ptz_stack_compat {hole_symb hole_word hole_sem} + (ptz:pt_zipper hole_symb hole_word hole_sem) + (stack:stack): Prop := + match ptz with + | Top_ptz => stack = [] + | Cons_ptl_ptz _ ptlz' => + ptlz_stack_compat ptlz' stack + end. + +Lemma ptlz_stack_compat_ptlz_state_compat: + forall hole_symbs hole_word hole_sems + (ptlz:ptl_zipper hole_symbs hole_word hole_sems) + (stack:stack), + ptlz_stack_compat ptlz stack -> ptlz_state_compat ptlz (state_of_stack init stack). +Proof. +destruct ptlz; simpl; intuition. +Qed. + +Definition ptd_stack_compat (ptd:pt_dot) (stack:stack): Prop := + match ptd with + | Reduce_ptd ptlz => ptlz_stack_compat ptlz stack + | Shift_ptd _ _ _ ptlz => ptlz_stack_compat ptlz stack + end. + +Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems) + :pt_dot := + match ptl in parse_tree_list hole_symbs hole_word hole_sems + return ptl_zipper hole_symbs hole_word hole_sems -> _ + with + | Nil_ptl => fun ptlz => + Reduce_ptd ptlz + | Cons_ptl pt ptl' => + match pt in parse_tree hole_symb hole_word hole_sem + return ptl_zipper (hole_symb::_) (hole_word++_) (hole_sem,_) -> _ + with + | Terminal_pt term sem => fun ptlz => + Shift_ptd term sem ptl' ptlz + | Non_terminal_pt ptl'' => fun ptlz => + build_pt_dot ptl'' + (Non_terminal_pt_ptlz (Cons_ptl_ptz ptl' ptlz)) + end + end ptlz. + +Lemma build_pt_dot_cost: + forall hole_symbs hole_word hole_sems + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems), + ptd_cost (build_pt_dot ptl ptlz) = ptl_size ptl + ptlz_cost ptlz. +Proof. +fix build_pt_dot_cost 4. +destruct ptl; intros. +reflexivity. +destruct p. +reflexivity. +simpl; rewrite build_pt_dot_cost. +simpl; rewrite <- plus_n_Sm, Nat.add_assoc; reflexivity. +Qed. + +Lemma build_pt_dot_buffer: + forall hole_symbs hole_word hole_sems + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems), + ptd_buffer (build_pt_dot ptl ptlz) = hole_word ++ ptlz_buffer ptlz. +Proof. +fix build_pt_dot_buffer 4. +destruct ptl; intros. +reflexivity. +destruct p. +reflexivity. +simpl; rewrite build_pt_dot_buffer. +apply app_str_app_assoc. +Qed. + +Lemma ptd_stack_compat_build_pt_dot: + forall hole_symbs hole_word hole_sems + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems) + (stack:stack), + ptlz_stack_compat ptlz stack -> + ptd_stack_compat (build_pt_dot ptl ptlz) stack. +Proof. +fix ptd_stack_compat_build_pt_dot 4. +destruct ptl; intros. +eauto. +destruct p. +eauto. +simpl. +apply ptd_stack_compat_build_pt_dot. +split. +apply ptlz_stack_compat_ptlz_state_compat, non_terminal_closed in H. +apply H; clear H; eauto. +destruct wordq. +right; split. +eauto. +eapply nullable_correct_list; eauto. +left. +eapply first_correct_list; eauto. +eauto. +Qed. + +Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems} + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems): + { word:_ & { sem:_ & + (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * + parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } := + match ptlz in ptl_zipper hole_symbs hole_word hole_sems + return parse_tree_list hole_symbs hole_word hole_sems -> + { word:_ & { sem:_ & + (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * + parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } + with + | @Non_terminal_pt_ptlz prod word sem ptz => fun ptl => + let sem := uncurry (prod_action prod) sem in + existT _ word (existT _ sem (ptz, Non_terminal_pt ptl)) + | Cons_ptl_ptlz pt ptlz' => fun ptl => + pop_ptlz (Cons_ptl pt ptl) ptlz' + end ptl. + +Lemma pop_ptlz_cost: + forall hole_symbs hole_word hole_sems + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems), + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in + ptlz_cost ptlz = ptz_cost ptz. +Proof. +fix pop_ptlz_cost 5. +destruct ptlz. +reflexivity. +simpl; apply pop_ptlz_cost. +Qed. + +Lemma pop_ptlz_buffer: + forall hole_symbs hole_word hole_sems + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems), + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in + ptlz_buffer ptlz = ptz_buffer ptz. +Proof. +fix pop_ptlz_buffer 5. +destruct ptlz. +reflexivity. +simpl; apply pop_ptlz_buffer. +Qed. + +Lemma pop_ptlz_pop_stack_compat_converter: + forall A hole_symbs hole_word hole_sems (ptlz:ptl_zipper hole_symbs hole_word hole_sems), + arrows_left (map symbol_semantic_type (rev (prod_rhs_rev (ptlz_prod ptlz)))) A = + arrows_left (map symbol_semantic_type hole_symbs) + (arrows_right A (map symbol_semantic_type (ptlz_past ptlz))). +Proof. +intros. +rewrite <- ptlz_past_ptlz_prod. +unfold arrows_right, arrows_left. +rewrite rev_append_rev, map_rev, map_app, map_rev, <- fold_left_rev_right, rev_involutive, fold_right_app. +rewrite fold_left_rev_right. +reflexivity. +Qed. + +Lemma pop_ptlz_pop_stack_compat: + forall hole_symbs hole_word hole_sems + (ptl:parse_tree_list hole_symbs hole_word hole_sems) + (ptlz:ptl_zipper hole_symbs hole_word hole_sems) + (stack:stack), + + ptlz_stack_compat ptlz stack -> + + let action' := + eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _ + (pop_ptlz_pop_stack_compat_converter _ _ _ _ _) + in + let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in + match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with + | OK (stack', sem') => + ptz_stack_compat ptz stack' /\ sem = sem' + | Err => True + end. +Proof. +Opaque AlphabetComparable AlphabetComparableUsualEq. +fix pop_ptlz_pop_stack_compat 5. +destruct ptlz. intros; simpl. +split. +apply H. +eapply (f_equal (fun X => uncurry X semantic_values)). +apply JMeq_eq, JMeq_sym, JMeq_eqrect with (P:=fun x => x). +simpl; intros; destruct stack0. +destruct (proj2 H). +simpl in H; destruct H. +destruct s as (state, sem'). +destruct H0. +specialize (pop_ptlz_pop_stack_compat _ _ _ (Cons_ptl p ptl) ptlz _ H0). +destruct (pop_ptlz (Cons_ptl p ptl) ptlz) as [word [sem []]]. +destruct (compare_eqdec (last_symb_of_non_init_state state) head_symbolt); intuition. +eapply JMeq_sym, JMeq_trans, JMeq_sym, JMeq_eq in H1; [|apply JMeq_eqrect with (e:=e)]. +rewrite <- H1. +simpl in pop_ptlz_pop_stack_compat. +erewrite proof_irrelevance with (p1:=pop_ptlz_pop_stack_compat_converter _ _ _ _ _). +apply pop_ptlz_pop_stack_compat. +Transparent AlphabetComparable AlphabetComparableUsualEq. +Qed. + +Definition next_ptd (ptd:pt_dot): option pt_dot := + match ptd with + | Shift_ptd term sem ptl ptlz => + Some (build_pt_dot ptl (Cons_ptl_ptlz (Terminal_pt term sem) ptlz)) + | Reduce_ptd ptlz => + let 'existT _ _ (existT _ _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in + match ptz in pt_zipper sym _ _ return parse_tree sym _ _ -> _ with + | Top_ptz => fun pt => None + | Cons_ptl_ptz ptl ptlz' => + fun pt => Some (build_pt_dot ptl (Cons_ptl_ptlz pt ptlz')) + end pt + end. + +Lemma next_ptd_cost: + forall ptd, + match next_ptd ptd with + | None => ptd_cost ptd = 0 + | Some ptd' => ptd_cost ptd = S (ptd_cost ptd') + end. +Proof. +destruct ptd. unfold next_ptd. +pose proof (pop_ptlz_cost _ _ _ Nil_ptl p). +destruct (pop_ptlz Nil_ptl p) as [word[sem[[]]]]. +assumption. +rewrite build_pt_dot_cost. +assumption. +simpl; rewrite build_pt_dot_cost; reflexivity. +Qed. + +Lemma reduce_step_next_ptd: + forall (ptlz:ptl_zipper [] [] ()) (stack:stack), + ptlz_stack_compat ptlz stack -> + match reduce_step init stack (ptlz_prod ptlz) (ptlz_buffer ptlz) with + | OK Fail_sr => + False + | OK (Accept_sr sem buffer) => + sem = full_sem /\ buffer = buffer_end /\ next_ptd (Reduce_ptd ptlz) = None + | OK (Progress_sr stack buffer) => + match next_ptd (Reduce_ptd ptlz) with + | None => False + | Some ptd => + ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd + end + | Err => + True + end. +Proof. +intros. +unfold reduce_step, next_ptd. +apply pop_ptlz_pop_stack_compat with (ptl:=Nil_ptl) in H. +pose proof (pop_ptlz_buffer _ _ _ Nil_ptl ptlz). +destruct (pop_ptlz Nil_ptl ptlz) as [word [sem [ptz pt]]]. +rewrite H0; clear H0. +revert H. +match goal with + |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end => + replace p1 with p2; [destruct p2 as [|[]]; intros|] +end. +assumption. +simpl. +destruct H; subst. +generalize dependent s0. +generalize (prod_lhs (ptlz_prod ptlz)); clear ptlz stack0. +dependent destruction ptz; intros. +simpl in H; subst; simpl. +pose proof start_goto; unfold Valid.start_goto in H; rewrite H. +destruct (compare_eqdec (start_nt init) (start_nt init)); intuition. +apply JMeq_eq, JMeq_eqrect with (P:=fun nt => symbol_semantic_type (NT nt)). +pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). +apply non_terminal_goto in H0. +destruct (goto_table (state_of_stack init s) n) as [[]|]; intuition. +apply ptd_stack_compat_build_pt_dot; simpl; intuition. +symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type). +symmetry; apply build_pt_dot_buffer. +destruct s; intuition. +simpl in H; apply ptlz_stack_compat_ptlz_state_compat in H. +destruct (H0 _ _ _ H eq_refl). +generalize (pop_ptlz_pop_stack_compat_converter (symbol_semantic_type (NT (prod_lhs (ptlz_prod ptlz)))) _ _ _ ptlz). +pose proof (ptlz_past_ptlz_prod _ _ _ ptlz); simpl in H. +rewrite H; clear H. +intro; f_equal; simpl. +apply JMeq_eq. +etransitivity. +apply JMeq_eqrect with (P:=fun x => x). +symmetry. +apply JMeq_eqrect with (P:=fun x => x). +Qed. + +Lemma step_next_ptd: + forall (ptd:pt_dot) (stack:stack), + ptd_stack_compat ptd stack -> + match step init stack (ptd_buffer ptd) with + | OK Fail_sr => + False + | OK (Accept_sr sem buffer) => + sem = full_sem /\ buffer = buffer_end /\ next_ptd ptd = None + | OK (Progress_sr stack buffer) => + match next_ptd ptd with + | None => False + | Some ptd => + ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd + end + | Err => + True + end. +Proof. +intros. +destruct ptd. +pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). +apply end_reduce in H0. +unfold step. +destruct (action_table (state_of_stack init stack0)). +rewrite H0 by reflexivity. +apply reduce_step_next_ptd; assumption. +simpl; destruct (Streams.hd (ptlz_buffer p)); simpl in H0. +destruct (l x); intuition; rewrite H1. +apply reduce_step_next_ptd; assumption. +pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). +apply terminal_shift in H0. +unfold step. +destruct (action_table (state_of_stack init stack0)); intuition. +simpl; destruct (Streams.hd (ptlz_buffer p0)) as [] eqn:?. +destruct (l term); intuition. +apply ptd_stack_compat_build_pt_dot; simpl; intuition. +unfold ptlz_state_compat; simpl; destruct Heqt; assumption. +symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type). +rewrite build_pt_dot_buffer; reflexivity. +Qed. + +Lemma parse_fix_complete: + forall (ptd:pt_dot) (stack:stack) (n_steps:nat), + ptd_stack_compat ptd stack -> + match parse_fix init stack (ptd_buffer ptd) n_steps with + | OK (Parsed_pr sem_res buffer_end_res) => + sem_res = full_sem /\ buffer_end_res = buffer_end /\ + S (ptd_cost ptd) <= n_steps + | OK Fail_pr => False + | OK Timeout_pr => n_steps < S (ptd_cost ptd) + | Err => True + end. +Proof. +fix parse_fix_complete 3. +destruct n_steps; intros; simpl. +apply Nat.lt_0_succ. +apply step_next_ptd in H. +pose proof (next_ptd_cost ptd). +destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition. +rewrite H3 in H0; rewrite H0. +apply le_n_S, Nat.le_0_l. +destruct (next_ptd ptd); intuition; subst. +eapply parse_fix_complete with (n_steps:=n_steps) in H1. +rewrite H0. +destruct (parse_fix init s (ptd_buffer p) n_steps) as [|[]]; try assumption. +apply lt_n_S; assumption. +destruct H1 as [H1 []]; split; [|split]; try assumption. +apply le_n_S; assumption. +Qed. + +Variable full_pt: parse_tree (NT (start_nt init)) full_word full_sem. + +Definition init_ptd := + match full_pt in parse_tree head full_word full_sem return + pt_zipper head full_word full_sem -> + match head return Type with | T _ => unit | NT _ => pt_dot end + with + | Terminal_pt _ _ => fun _ => () + | Non_terminal_pt ptl => + fun top => build_pt_dot ptl (Non_terminal_pt_ptlz top) + end Top_ptz. + +Lemma init_ptd_compat: + ptd_stack_compat init_ptd []. +Proof. +unfold init_ptd. +assert (ptz_stack_compat Top_ptz []) by reflexivity. +pose proof (start_future init); revert H0. +generalize dependent Top_ptz. +generalize dependent full_word. +generalize full_sem. +generalize (start_nt init). +dependent destruction full_pt0. +intros. +apply ptd_stack_compat_build_pt_dot; simpl; intuition. +apply H0; reflexivity. +Qed. + +Lemma init_ptd_cost: + S (ptd_cost init_ptd) = pt_size full_pt. +Proof. +unfold init_ptd. +assert (ptz_cost Top_ptz = 0) by reflexivity. +generalize dependent Top_ptz. +generalize dependent full_word. +generalize full_sem. +generalize (start_nt init). +dependent destruction full_pt0. +intros. +rewrite build_pt_dot_cost; simpl. +rewrite H, Nat.add_0_r; reflexivity. +Qed. + +Lemma init_ptd_buffer: + ptd_buffer init_ptd = full_word ++ buffer_end. +Proof. +unfold init_ptd. +assert (ptz_buffer Top_ptz = buffer_end) by reflexivity. +generalize dependent Top_ptz. +generalize dependent full_word. +generalize full_sem. +generalize (start_nt init). +dependent destruction full_pt0. +intros. +rewrite build_pt_dot_buffer; simpl. +rewrite H; reflexivity. +Qed. + +Theorem parse_complete n_steps: + match parse init (full_word ++ buffer_end) n_steps with + | OK (Parsed_pr sem_res buffer_end_res) => + sem_res = full_sem /\ buffer_end_res = buffer_end /\ + pt_size full_pt <= n_steps + | OK Fail_pr => False + | OK Timeout_pr => n_steps < pt_size full_pt + | Err => True + end. +Proof. +pose proof (parse_fix_complete init_ptd [] n_steps init_ptd_compat). +rewrite init_ptd_buffer, init_ptd_cost in H. +apply H. +Qed. + +End Completeness_Proof. + +End Make. diff --git a/cparser/MenhirLib/Interpreter_correct.v b/cparser/MenhirLib/Interpreter_correct.v new file mode 100644 index 00000000..1263d4e3 --- /dev/null +++ b/cparser/MenhirLib/Interpreter_correct.v @@ -0,0 +1,228 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Streams. +Require Import List. +Require Import Syntax. +Require Import Equality. +Require Import Alphabet. +Require Grammar. +Require Automaton. +Require Interpreter. + +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 state, 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) + (semantic_valuet:_), + inhabited (parse_tree (last_symb_of_non_init_state s) wordt semantic_valuet) -> + + word_has_stack_semantics + (wordq++wordt) (existT noninitstate_type s semantic_valuet::stackq). + +Lemma pop_invariant_converter: + forall A symbols_to_pop symbols_popped, + arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A = + arrows_left (map symbol_semantic_type symbols_popped) + (arrows_right A (map symbol_semantic_type symbols_to_pop)). +Proof. +intros. +unfold arrows_right, arrows_left. +rewrite rev_append_rev, map_app, map_rev, fold_left_app. +apply f_equal. +rewrite <- fold_left_rev_right, rev_involutive. +reflexivity. +Qed. + +(** [pop] preserves the invariant **) +Lemma pop_invariant: + forall (symbols_to_pop symbols_popped:list symbol) + (stack_cur:stack) + (A:Type) + (action:arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A), + forall word_stack word_popped, + forall sem_popped, + word_has_stack_semantics word_stack stack_cur -> + inhabited (parse_tree_list symbols_popped word_popped sem_popped) -> + let action' := eq_rect _ (fun x=>x) action _ (pop_invariant_converter _ _ _) in + match pop symbols_to_pop stack_cur (uncurry action' sem_popped) with + | OK (stack_new, sem) => + exists word1res word2res sem_full, + (word_stack = word1res ++ word2res)%list /\ + word_has_stack_semantics word1res stack_new /\ + sem = uncurry action sem_full /\ + inhabited ( + parse_tree_list (rev_append symbols_to_pop symbols_popped) (word2res++word_popped) sem_full) + | Err => True + end. +Proof. +induction symbols_to_pop; intros; unfold pop; fold pop. +exists word_stack, ([]:list token), sem_popped; intuition. +f_equal. +apply JMeq_eq, JMeq_eqrect with (P:=(fun x => x)). +destruct stack_cur as [|[]]; eauto. +destruct (compare_eqdec (last_symb_of_non_init_state x) a); eauto. +destruct e; simpl. +dependent destruction H. +destruct H0, H1. apply (Cons_ptl X), inhabits in X0. +specialize (IHsymbols_to_pop _ _ _ action0 _ _ _ H X0). +match goal with + IHsymbols_to_pop:match ?p1 with Err => _ | OK _ => _ end |- match ?p2 with Err => _ | OK _ => _ end => + replace p2 with p1; [destruct p1 as [|[]]|]; intuition +end. +destruct IHsymbols_to_pop as [word1res [word2res [sem_full []]]]; intuition; subst. +exists word1res. +eexists. +exists sem_full. +intuition. +rewrite <- app_assoc; assumption. +simpl; f_equal; f_equal. +apply JMeq_eq. +etransitivity. +apply JMeq_eqrect with (P:=(fun x => x)). +symmetry. +apply JMeq_eqrect with (P:=(fun x => x)). +Qed. + +(** [reduce_step] preserves the invariant **) +Lemma reduce_step_invariant (stack:stack) (prod:production): + forall word buffer, word_has_stack_semantics word stack -> + match reduce_step init stack prod buffer with + | OK (Accept_sr sem buffer_new) => + buffer = buffer_new /\ + inhabited (parse_tree (NT (start_nt init)) word sem) + | OK (Progress_sr stack_new buffer_new) => + buffer = buffer_new /\ + word_has_stack_semantics word stack_new + | Err | OK Fail_sr => True + end. +Proof with eauto. +intros. +unfold reduce_step. +pose proof (pop_invariant (prod_rhs_rev prod) [] stack (symbol_semantic_type (NT (prod_lhs prod)))). +revert H0. +generalize (pop_invariant_converter (symbol_semantic_type (NT (prod_lhs prod))) (prod_rhs_rev prod) []). +rewrite <- rev_alt. +intros. +specialize (H0 (prod_action prod) _ [] () H (inhabits Nil_ptl)). +match goal with H0:let action' := ?a in _ |- _ => replace a with (prod_action' prod) in H0 end. +simpl in H0. +destruct (pop (prod_rhs_rev prod) stack (prod_action' prod)) as [|[]]; intuition. +destruct H0 as [word1res [word2res [sem_full]]]; intuition. +destruct H4; apply Non_terminal_pt, inhabits in X. +match goal with X:inhabited (parse_tree _ _ ?u) |- _ => replace u with s0 in X end. +clear sem_full H2. +simpl; destruct (goto_table (state_of_stack init s) (prod_lhs prod)) as [[]|]; intuition; subst. +rewrite app_nil_r in X; revert s0 X; rewrite e0; intro; simpl. +constructor... +destruct s; intuition. +destruct (compare_eqdec (prod_lhs prod) (start_nt init)); intuition. +rewrite app_nil_r in X. +rewrite <- e0. +inversion H0. +destruct X; constructor... +apply JMeq_eq. +etransitivity. +apply JMeq_eqrect with (P:=(fun x => x)). +symmetry. +apply JMeq_eqrect with (P:=(fun x => x)). +Qed. + +(** [step] preserves the invariant **) +Lemma step_invariant (stack:stack) (buffer:Stream token): + forall buffer_tmp, + (exists word_old, + buffer = word_old ++ buffer_tmp /\ + word_has_stack_semantics word_old stack) -> + match step init stack buffer_tmp with + | OK (Accept_sr sem buffer_new) => + exists word_new, + buffer = word_new ++ buffer_new /\ + inhabited (parse_tree (NT (start_nt init)) word_new sem) + | OK (Progress_sr stack_new buffer_new) => + exists word_new, + buffer = word_new ++ buffer_new /\ + word_has_stack_semantics word_new stack_new + | Err | OK Fail_sr => True + end. +Proof with eauto. +intros. +destruct H, H. +unfold step. +destruct (action_table (state_of_stack init stack)). +pose proof (reduce_step_invariant stack p x buffer_tmp). +destruct (reduce_step init stack p buffer_tmp) as [|[]]; intuition; subst... +destruct buffer_tmp. +unfold Streams.hd. +destruct t. +destruct (l x0); intuition. +exists (x ++ [existT (fun t => symbol_semantic_type (T t)) x0 s])%list. +split. +now rewrite <- app_str_app_assoc; intuition. +apply Cons_stack_whss; intuition. +destruct e; simpl. +now exact (inhabits (Terminal_pt _ _)). +match goal with |- (match reduce_step init stack p ?buff with Err => _ | OK _ => _ end) => + pose proof (reduce_step_invariant stack p x buff); + destruct (reduce_step init stack p buff) as [|[]]; intuition; subst +end... +Qed. + +(** The interpreter is correct : if it returns a semantic value, then the input + word has this semantic value. +**) +Theorem parse_correct buffer n_steps: + match parse init buffer n_steps with + | OK (Parsed_pr sem buffer_new) => + exists word_new, + buffer = word_new ++ buffer_new /\ + inhabited (parse_tree (NT (start_nt init)) word_new sem) + | _ => True + end. +Proof. +unfold parse. +assert (exists w, buffer = w ++ buffer /\ word_has_stack_semantics w []). +exists ([]:list token); intuition. +now apply Nil_stack_whss. +revert H. +generalize ([]:stack), buffer at 2 3. +induction n_steps; simpl; intuition. +pose proof (step_invariant _ _ _ H). +destruct (step init s buffer0); simpl; intuition. +destruct s0; intuition. +apply IHn_steps; intuition. +Qed. + +End Init. + +End Make. diff --git a/cparser/MenhirLib/Interpreter_safe.v b/cparser/MenhirLib/Interpreter_safe.v new file mode 100644 index 00000000..a1aa35b8 --- /dev/null +++ b/cparser/MenhirLib/Interpreter_safe.v @@ -0,0 +1,275 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import Streams. +Require Import Equality. +Require Import List. +Require Import Syntax. +Require Import Alphabet. +Require Grammar. +Require Automaton. +Require Validator_safe. +Require Interpreter. + +Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A). +Module Import Valid := Validator_safe.Make A. + +(** * A correct automaton does not crash **) + +Section Safety_proof. + +Hypothesis safe: safe. + +Proposition shift_head_symbs: shift_head_symbs. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition goto_head_symbs: goto_head_symbs. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition shift_past_state: shift_past_state. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition goto_past_state: goto_past_state. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. +Proposition reduce_ok: reduce_ok. +Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. + +(** We prove that a correct automaton won't crash : the interpreter will + not return [Err] **) + +Variable init : initstate. + +(** 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 init stack)) + (symb_stack_of_stack stack) -> + prefix_pred (head_states_of_state (state_of_stack init stack)) + (state_stack_of_stack stack) -> + stack_invariant_next stack -> + stack_invariant stack +with stack_invariant_next: stack -> Prop := + | stack_invariant_next_nil: + stack_invariant_next [] + | stack_invariant_next_cons: + forall state_cur st stack_rec, + stack_invariant stack_rec -> + stack_invariant_next (existT _ state_cur st::stack_rec). + +(** [pop] conserves the stack invariant and does not crash + under the assumption that we can pop at this place. + Moreover, after a pop, the top state of the stack is allowed. **) +Lemma pop_stack_invariant_conserved + (symbols_to_pop:list symbol) (stack_cur:stack) A action: + stack_invariant stack_cur -> + prefix symbols_to_pop (head_symbs_of_state (state_of_stack init stack_cur)) -> + match pop symbols_to_pop stack_cur (A:=A) action with + | OK (stack_new, _) => + stack_invariant stack_new /\ + state_valid_after_pop + (state_of_stack init stack_new) symbols_to_pop + (head_states_of_state (state_of_stack init stack_cur)) + | Err => False + end. +Proof with eauto. + intros. + pose proof H. + destruct H. + revert H H0 H1 H2 H3. + generalize (head_symbs_of_state (state_of_stack init stack0)). + generalize (head_states_of_state (state_of_stack init stack0)). + revert stack0 A action. + induction symbols_to_pop; intros. + - split... + destruct l; constructor. + inversion H2; subst. + specialize (H7 (state_of_stack init stack0)). + destruct (f2 (state_of_stack init stack0)) as [] eqn:? ... + destruct stack0 as [|[]]; simpl in *. + + inversion H6; subst. + unfold singleton_state_pred in Heqb0. + now rewrite compare_refl in Heqb0; discriminate. + + inversion H6; subst. + unfold singleton_state_pred in Heqb0. + now rewrite compare_refl in Heqb0; discriminate. + - destruct stack0 as [|[]]; unfold pop. + + inversion H0; subst. + now inversion H. + + fold pop. + destruct (compare_eqdec (last_symb_of_non_init_state x) a). + * inversion H0; subst. clear H0. + inversion H; subst. clear H. + dependent destruction H3; simpl. + assert (prefix_pred (List.tl l) (state_stack_of_stack stack0)). + unfold tl; destruct l; [constructor | inversion H2]... + pose proof H. destruct H3. + specialize (IHsymbols_to_pop stack0 A (action0 n) _ _ H4 H7 H H0 H6). + revert IHsymbols_to_pop. + fold (noninitstate_type x); generalize (pop symbols_to_pop stack0 (action0 n)). + destruct r as [|[]]; intuition... + destruct l; constructor... + * apply n0. + inversion H0; subst. + inversion H; subst... +Qed. + +(** [prefix] is associative **) +Lemma prefix_ass: + forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3. +Proof. +induction l1; intros. +constructor. +inversion H; subst. +inversion H0; subst. +constructor; eauto. +Qed. + +(** [prefix_pred] is associative **) +Lemma prefix_pred_ass: + forall (l1 l2 l3:list (state->bool)), + prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3. +Proof. +induction l1; intros. +constructor. +inversion H; subst. +inversion H0; subst. +constructor; eauto. +intro. +specialize (H3 x). +specialize (H4 x). +destruct (f0 x); simpl in *; intuition. +rewrite H4 in H3; intuition. +Qed. + +(** If we have the right to reduce at this state, then the stack invariant + is conserved by [reduce_step] and [reduce_step] does not crash. **) +Lemma reduce_step_stack_invariant_conserved stack prod buff: + stack_invariant stack -> + valid_for_reduce (state_of_stack init stack) prod -> + match reduce_step init stack prod buff with + | OK (Fail_sr | Accept_sr _ _) => True + | OK (Progress_sr stack_new _) => stack_invariant stack_new + | Err => False + end. +Proof with eauto. +unfold valid_for_reduce. +intuition. +unfold reduce_step. +pose proof (pop_stack_invariant_conserved (prod_rhs_rev prod) stack _ (prod_action' prod)). +destruct (pop (prod_rhs_rev prod) stack (prod_action' prod)) as [|[]]. +apply H0... +destruct H0... +pose proof (goto_head_symbs (state_of_stack init s) (prod_lhs prod)). +pose proof (goto_past_state (state_of_stack init s) (prod_lhs prod)). +unfold bind2. +destruct H0. +specialize (H2 _ H3)... +destruct (goto_table (state_of_stack init stack0) (prod_lhs prod)) as [[]|]. +constructor. +simpl. +constructor. +eapply prefix_ass... +unfold state_stack_of_stack; simpl; constructor. +intro; destruct (singleton_state_pred x x0); reflexivity. +eapply prefix_pred_ass... +constructor... +constructor... +destruct stack0 as [|[]]... +destruct (compare_eqdec (prod_lhs prod) (start_nt init))... +apply n, H2, eq_refl. +apply H2, eq_refl. +Qed. + +(** If the automaton is safe, then the stack invariant is conserved by + [step] and [step] does not crash. **) +Lemma step_stack_invariant_conserved (stack:stack) buffer: + stack_invariant stack -> + match step init stack buffer with + | OK (Fail_sr | Accept_sr _ _) => True + | OK (Progress_sr stack_new _) => stack_invariant stack_new + | Err => False + end. +Proof with eauto. +intro. +unfold step. +pose proof (shift_head_symbs (state_of_stack init stack)). +pose proof (shift_past_state (state_of_stack init stack)). +pose proof (reduce_ok (state_of_stack init stack)). +destruct (action_table (state_of_stack init stack)). +apply reduce_step_stack_invariant_conserved... +destruct buffer as [[]]; simpl. +specialize (H0 x); specialize (H1 x); specialize (H2 x). +destruct (l x)... +destruct H. +constructor. +unfold state_of_stack. +constructor. +eapply prefix_ass... +unfold state_stack_of_stack; simpl; constructor. +intro; destruct (singleton_state_pred s0 x0)... +eapply prefix_pred_ass... +constructor... +constructor... +apply reduce_step_stack_invariant_conserved... +Qed. + +(** If the automaton is safe, then it does not crash **) +Theorem parse_no_err buffer n_steps: + parse init buffer n_steps <> Err. +Proof with eauto. +unfold parse. +assert (stack_invariant []). +constructor. +constructor. +unfold state_stack_of_stack; simpl; constructor. +intro; destruct (singleton_state_pred init x)... +constructor. +constructor. +revert H. +generalize buffer ([]:stack). +induction n_steps; simpl. +now discriminate. +intros. +pose proof (step_stack_invariant_conserved s buffer0 H). +destruct (step init s buffer0) as [|[]]; simpl... +discriminate. +discriminate. +Qed. + +(** A version of [parse] that uses safeness in order to return a + [parse_result], and not a [result parse_result] : we have proven that + parsing does not return [Err]. **) +Definition parse_with_safe (buffer:Stream token) (n_steps:nat): + parse_result init. +Proof with eauto. +pose proof (parse_no_err buffer n_steps). +destruct (parse init buffer n_steps)... +congruence. +Defined. + +End Safety_proof. + +End Make. diff --git a/cparser/MenhirLib/Main.v b/cparser/MenhirLib/Main.v new file mode 100644 index 00000000..1a17e988 --- /dev/null +++ b/cparser/MenhirLib/Main.v @@ -0,0 +1,92 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Grammar. +Require Automaton. +Require Interpreter_safe. +Require Interpreter_correct. +Require Interpreter_complete. +Require Import Syntax. + +Module Make(Export Aut:Automaton.T). +Export Aut.Gram. +Export Aut.GramDefs. + +Module Import Inter := Interpreter.Make Aut. +Module Safe := Interpreter_safe.Make Aut Inter. +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 := Safe.Valid.is_safe. +Definition parse (safe:safe_validator ()=true) init n_steps buffer : parse_result init:= + Safe.parse_with_safe (Safe.Valid.is_safe_correct safe) init buffer n_steps. + +(** Correction theorem. **) +Theorem parse_correct + (safe:safe_validator ()= true) init n_steps buffer: + match parse safe init n_steps buffer with + | Parsed_pr sem buffer_new => + exists word, + buffer = word ++ buffer_new /\ inhabited (parse_tree (NT (start_nt init)) word sem) + | _ => True + end. +Proof. +unfold parse, Safe.parse_with_safe. +pose proof (Correct.parse_correct init buffer n_steps). +generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init buffer n_steps). +destruct (Inter.parse init buffer n_steps); intros. +now destruct (n (eq_refl _)). +now destruct p; trivial. +Qed. + +(** Completeness theorem. **) +Theorem parse_complete + (safe:safe_validator () = true) init n_steps word buffer_end sem: + complete_validator () = true -> + forall tree:parse_tree (NT (start_nt init)) word sem, + match parse safe init n_steps (word ++ buffer_end) with + | Fail_pr => False + | Parsed_pr sem_res buffer_end_res => + sem_res = sem /\ buffer_end_res = buffer_end /\ pt_size tree <= n_steps + | Timeout_pr => n_steps < pt_size tree + end. +Proof. +intros. +unfold parse, Safe.parse_with_safe. +pose proof (Complete.parse_complete (Complete.Valid.is_complete_correct H) init _ buffer_end _ tree n_steps). +generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init (word ++ buffer_end) n_steps). +destruct (Inter.parse init (word ++ buffer_end) n_steps); intros. +now destruct (n eq_refl). +now exact H0. +Qed. + +(** Unambiguity theorem. **) +Theorem unambiguity: + safe_validator () = true -> complete_validator () = true -> inhabited token -> + forall init word, + forall sem1 (tree1:parse_tree (NT (start_nt init)) word sem1), + forall sem2 (tree2:parse_tree (NT (start_nt init)) word sem2), + sem1 = sem2. +Proof. +intros. +destruct H1. +pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem1) H0 tree1. +pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem2) H0 tree2. +destruct (parse H init (pt_size tree1) (word ++ Streams.const X)); intuition. +rewrite <- H3, H1; reflexivity. +Qed. + +End Make. diff --git a/cparser/MenhirLib/Tuples.v b/cparser/MenhirLib/Tuples.v new file mode 100644 index 00000000..3fd2ec03 --- /dev/null +++ b/cparser/MenhirLib/Tuples.v @@ -0,0 +1,49 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Import List. +Require Import Coq.Program.Syntax. +Require Import Equality. + +(** A curryfied function with multiple parameters **) +Definition arrows_left: list Type -> Type -> Type := + fold_left (fun A B => B -> A). + +(** A curryfied function with multiple parameters **) +Definition arrows_right: Type -> list Type -> Type := + fold_right (fun A B => A -> B). + +(** A tuple is a heterogeneous list. For convenience, we use pairs. **) +Fixpoint tuple (types : list Type) : Type := + match types with + | nil => unit + | t::q => prod t (tuple q) + end. + +Fixpoint uncurry {args:list Type} {res:Type}: + arrows_left args res -> tuple args -> res := + match args return forall res, arrows_left args res -> tuple args -> res with + | [] => fun _ f _ => f + | t::q => fun res f p => let (d, t) := p in + (@uncurry q _ f t) d + end res. + +Lemma JMeq_eqrect: + forall (U:Type) (a b:U) (P:U -> Type) (x:P a) (e:a=b), + eq_rect a P x b e ~= x. +Proof. +destruct e. +reflexivity. +Qed. diff --git a/cparser/MenhirLib/Validator_complete.v b/cparser/MenhirLib/Validator_complete.v new file mode 100644 index 00000000..a9823278 --- /dev/null +++ b/cparser/MenhirLib/Validator_complete.v @@ -0,0 +1,542 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Automaton. +Require Import Alphabet. +Require Import List. +Require Import Syntax. + +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). + +(** 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. + +Lemma forallb_items_spec : + forall p, forallb_items (items_map ()) p = true -> + forall st prod fut lookahead, state_has_future st prod fut lookahead -> + forall P:state -> production -> list symbol -> terminal -> Prop, + (forall st prod pos set lookahead, + TerminalSet.In lookahead set -> p st prod pos set = true -> + P st prod (future_of_prod prod pos) lookahead) -> + P st prod fut lookahead. +Proof. +intros. +unfold forallb_items in H. +rewrite StateProdPosMap.fold_1 in H. +destruct H0; destruct H0. +specialize (H1 st prod x _ _ H2). +destruct H0. +apply H1. +unfold find_items_map in *. +pose proof (@StateProdPosMap.find_2 _ (items_map ()) (st, prod, x)). +destruct (StateProdPosMap.find (st, prod, x) (items_map ())); [ |destruct (TerminalSet.empty_1 H2)]. +specialize (H0 _ (eq_refl _)). +pose proof (StateProdPosMap.elements_1 H0). +revert H. +generalize true at 1. +induction H3. +destruct H. +destruct y. +simpl in H3; destruct H3. +pose proof (compare_eq (st, prod, x) k H). +destruct H3. +simpl. +generalize (p st prod x t). +induction l; simpl; intros. +rewrite Bool.andb_true_iff in H3. +intuition. +destruct a; destruct k; destruct p0. +simpl in H3. +replace (b0 && b && p s p0 n t0)%bool with (b0 && p s p0 n t0 && b)%bool in H3. +apply (IHl _ _ H3). +destruct b, b0, (p s p0 n t0); reflexivity. +intro. +apply IHInA. +Qed. + +(** * Validation for completeness **) + +(** The nullable predicate is a fixpoint : it is correct. **) +Definition nullable_stable:= + forall p:production, + nullable_word (rev (prod_rhs_rev p)) = true -> + nullable_nterm (prod_lhs p) = true. + +Definition is_nullable_stable (_:unit) := + forallb (fun p:production => + implb (nullable_word (rev' (prod_rhs_rev p))) (nullable_nterm (prod_lhs p))) + all_list. + +Property is_nullable_stable_correct : + is_nullable_stable () = true -> nullable_stable. +Proof. +unfold is_nullable_stable, nullable_stable. +intros. +rewrite forallb_forall in H. +specialize (H p (all_list_forall p)). +unfold rev' in H; rewrite <- rev_alt in H. +rewrite H0 in H; intuition. +Qed. + +(** 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)). + +Definition is_first_stable (_:unit) := + forallb (fun p:production => + TerminalSet.subset (first_word_set (rev' (prod_rhs_rev p))) + (first_nterm_set (prod_lhs p))) + all_list. + +Property is_first_stable_correct : + is_first_stable () = true -> first_stable. +Proof. +unfold is_first_stable, first_stable. +intros. +rewrite forallb_forall in H. +specialize (H p (all_list_forall p)). +unfold rev' in H; rewrite <- rev_alt in H. +apply TerminalSet.subset_2; intuition. +Qed. + +(** The initial state has all the S=>.u items, where S is the start non-terminal **) +Definition start_future := + forall (init:initstate) (t:terminal) (p:production), + prod_lhs p = start_nt init -> + state_has_future init p (rev (prod_rhs_rev p)) t. + +Definition is_start_future items_map := + forallb (fun init => + forallb (fun prod => + if compare_eqb (prod_lhs prod) (start_nt init) then + let lookaheads := find_items_map items_map init prod 0 in + forallb (fun t => TerminalSet.mem t lookaheads) all_list + else + true) all_list) all_list. + +Property is_start_future_correct : + is_start_future (items_map ()) = true -> start_future. +Proof. +unfold is_start_future, start_future. +intros. +rewrite forallb_forall in H. +specialize (H init (all_list_forall _)). +rewrite forallb_forall in H. +specialize (H p (all_list_forall _)). +rewrite <- compare_eqb_iff in H0. +rewrite H0 in H. +rewrite forallb_forall in H. +specialize (H t (all_list_forall _)). +exists 0. +split. +apply rev_alt. +apply TerminalSet.mem_2; eauto. +Qed. + +(** 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. + +Definition is_terminal_shift items_map := + forallb_items items_map (fun s1 prod pos lset => + match future_of_prod prod pos with + | T t::_ => + match action_table s1 with + | Lookahead_act awp => + match awp t with + | Shift_act s2 _ => + TerminalSet.subset lset (find_items_map items_map s2 prod (S pos)) + | _ => false + end + | _ => false + end + | _ => true + end). + +Property is_terminal_shift_correct : + is_terminal_shift (items_map ()) = true -> terminal_shift. +Proof. +unfold is_terminal_shift, terminal_shift. +intros. +apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ fut look => _)). +intros. +destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition. +destruct (action_table st); intuition. +destruct (l0 t); intuition. +exists (S pos). +split. +unfold future_of_prod in *. +rewrite Heql; reflexivity. +apply (TerminalSet.subset_2 H2); intuition. +Qed. + +(** 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 -> + fut = [] -> + 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. + +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). + +Property is_end_reduce_correct : + is_end_reduce (items_map ()) = true -> end_reduce. +Proof. +unfold is_end_reduce, end_reduce. +intros. +revert H1. +apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => _ -> + match action_table st with + | Default_reduce_act p => p = prod + | _ => _ + end)). +intros. +rewrite H3 in H2. +destruct (action_table st); intuition. +apply compare_eqb_iff; intuition. +rewrite TerminalSet.fold_1 in H2. +revert H2. +generalize true at 1. +pose proof (TerminalSet.elements_1 H1). +induction H2. +pose proof (compare_eq _ _ H2). +destruct H4. +simpl. +assert (fold_left + (fun (a : bool) (e : TerminalSet.elt) => + match l e with + | Shift_act _ _ => false + | Reduce_act p => (a && compare_eqb p prod0)%bool + | Fail_act => false + end) l0 false = true -> False). +induction l0; intuition. +apply IHl0. +simpl in H4. +destruct (l a); intuition. +destruct (l lookahead0); intuition. +apply compare_eqb_iff. +destruct (compare_eqb p prod0); intuition. +destruct b; intuition. +simpl; intros. +eapply IHInA; eauto. +Qed. + +(** 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 => + forall prod fut lookahead, + state_has_future s1 prod fut lookahead -> + match fut with + | NT nt'::_ => nt <> nt' + | _ => True + end + end + | _ => True + end. + +Definition is_non_terminal_goto items_map := + forallb_items items_map (fun s1 prod pos lset => + match future_of_prod prod pos with + | NT nt::_ => + match goto_table s1 nt with + | Some (exist _ s2 _) => + TerminalSet.subset lset (find_items_map items_map s2 prod (S pos)) + | None => forallb_items items_map (fun s1' prod' pos' _ => + (implb (compare_eqb s1 s1') + match future_of_prod prod' pos' with + | NT nt' :: _ => negb (compare_eqb nt nt') + | _ => true + end)%bool) + end + | _ => true + end). + +Property is_non_terminal_goto_correct : + is_non_terminal_goto (items_map ()) = true -> non_terminal_goto. +Proof. +unfold is_non_terminal_goto, non_terminal_goto. +intros. +apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => + match fut with + | NT nt :: q => + match goto_table st nt with + | Some _ => _ + | None => + forall p f l, state_has_future st p f l -> (_:Prop) + end + | _ => _ + end)). +intros. +destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition. +destruct (goto_table st n) as [[]|]. +exists (S pos). +split. +unfold future_of_prod in *. +rewrite Heql; reflexivity. +apply (TerminalSet.subset_2 H2); intuition. +intros. +remember st in H2; revert Heqs. +apply (forallb_items_spec _ H2 _ _ _ _ H3 (fun st' prod fut look => s = st' -> match fut return Prop with [] => _ | _ => _ end)); intros. +rewrite <- compare_eqb_iff in H6; rewrite H6 in H5. +destruct (future_of_prod prod1 pos0) as [|[]]; intuition. +rewrite <- compare_eqb_iff in H7; rewrite H7 in H5. +discriminate. +Qed. + +Definition start_goto := + forall (init:initstate), goto_table init (start_nt init) = None. + +Definition is_start_goto (_:unit) := + forallb (fun (init:initstate) => + match goto_table init (start_nt init) with + | Some _ => false + | None => true + end) all_list. + +Definition is_start_goto_correct: + is_start_goto () = true -> start_goto. +Proof. +unfold is_start_goto, start_goto. +rewrite forallb_forall. +intros. +specialize (H init (all_list_forall _)). +destruct (goto_table init (start_nt init)); congruence. +Qed. + +(** 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:state) prod fut lookahead, + state_has_future s1 prod fut lookahead -> + match fut with + | NT nt::q => + forall (p:production) (lookahead2:terminal), + prod_lhs p = nt -> + TerminalSet.In lookahead2 (first_word_set q) \/ + lookahead2 = lookahead /\ nullable_word q = true -> + state_has_future s1 p (rev (prod_rhs_rev p)) lookahead2 + | _ => True + end. + +Definition is_non_terminal_closed items_map := + forallb_items items_map (fun s1 prod pos lset => + match future_of_prod prod pos with + | NT nt::q => + forallb (fun p => + if compare_eqb (prod_lhs p) nt then + let lookaheads := find_items_map items_map s1 p 0 in + (implb (nullable_word q) (TerminalSet.subset lset lookaheads)) && + TerminalSet.subset (first_word_set q) lookaheads + else true + )%bool all_list + | _ => true + end). + +Property is_non_terminal_closed_correct: + is_non_terminal_closed (items_map ()) = true -> non_terminal_closed. +Proof. +unfold is_non_terminal_closed, non_terminal_closed. +intros. +apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => + match fut with + | NT nt :: q => forall p l, _ -> _ -> state_has_future st _ _ _ + | _ => _ + end)). +intros. +destruct (future_of_prod prod0 pos); intuition. +destruct s; eauto; intros. +rewrite forallb_forall in H2. +specialize (H2 p (all_list_forall p)). +rewrite <- compare_eqb_iff in H3. +rewrite H3 in H2. +rewrite Bool.andb_true_iff in H2. +destruct H2. +exists 0. +split. +apply rev_alt. +destruct H4 as [|[]]; subst. +apply (TerminalSet.subset_2 H5); intuition. +rewrite H6 in H2. +apply (TerminalSet.subset_2 H2); intuition. +Qed. + +(** The automaton is complete **) +Definition complete := + nullable_stable /\ first_stable /\ start_future /\ terminal_shift + /\ end_reduce /\ non_terminal_goto /\ start_goto /\ non_terminal_closed. + +Definition is_complete (_:unit) := + let items_map := items_map () in + (is_nullable_stable () && is_first_stable () && is_start_future items_map && + is_terminal_shift items_map && is_end_reduce items_map && is_start_goto () && + is_non_terminal_goto items_map && is_non_terminal_closed items_map)%bool. + +Property is_complete_correct: + is_complete () = true -> complete. +Proof. +unfold is_complete, complete. +repeat rewrite Bool.andb_true_iff. +intuition. +apply is_nullable_stable_correct; assumption. +apply is_first_stable_correct; assumption. +apply is_start_future_correct; assumption. +apply is_terminal_shift_correct; assumption. +apply is_end_reduce_correct; assumption. +apply is_non_terminal_goto_correct; assumption. +apply is_start_goto_correct; assumption. +apply is_non_terminal_closed_correct; assumption. +Qed. + +End Make. diff --git a/cparser/MenhirLib/Validator_safe.v b/cparser/MenhirLib/Validator_safe.v new file mode 100644 index 00000000..183d661b --- /dev/null +++ b/cparser/MenhirLib/Validator_safe.v @@ -0,0 +1,414 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +Require Automaton. +Require Import Alphabet. +Require Import List. +Require Import Syntax. + +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). + +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. + +Property is_prefix_correct (l1 l2:list symbol): + is_prefix l1 l2 = true -> prefix l1 l2. +Proof. +revert l2. +induction l1; intros. +apply prefix_nil. +unfold is_prefix in H. +destruct l2; intuition; try discriminate. +rewrite Bool.andb_true_iff in H. +destruct H. +rewrite compare_eqb_iff in H. +destruct H. +apply prefix_cons. +apply IHl1; intuition. +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. + +Definition is_shift_head_symbs (_:unit) := + forallb (fun s:state => + match action_table s with + | Lookahead_act awp => + forallb (fun t => + match awp t with + | Shift_act s2 _ => + is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) + | _ => true + end) + all_list + | _ => true + end) + all_list. + +Property is_shift_head_symbs_correct: + is_shift_head_symbs () = true -> shift_head_symbs. +Proof. +unfold is_shift_head_symbs, shift_head_symbs. +intros. +rewrite forallb_forall in H. +specialize (H s (all_list_forall s)). +destruct (action_table s); intuition. +rewrite forallb_forall in H. +specialize (H t (all_list_forall t)). +destruct (l t); intuition. +apply is_prefix_correct; intuition. +Qed. + +(** 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. + +Definition is_goto_head_symbs (_:unit) := + forallb (fun s:state => + forallb (fun nt => + match goto_table s nt with + | Some (exist _ s2 _) => + is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) + | None => true + end) + all_list) + all_list. + +Property is_goto_head_symbs_correct: + is_goto_head_symbs () = true -> goto_head_symbs. +Proof. +unfold is_goto_head_symbs, goto_head_symbs. +intros. +rewrite forallb_forall in H. +specialize (H s (all_list_forall s)). +rewrite forallb_forall in H. +specialize (H nt (all_list_forall nt)). +destruct (goto_table s nt); intuition. +destruct s0. +apply is_prefix_correct; intuition. +Qed. + +(** 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). + +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. + +Property is_prefix_pred_correct (l1 l2:list (state->bool)) : + is_prefix_pred l1 l2 = true -> prefix_pred l1 l2. +Proof. +revert l2. +induction l1. +intros. +apply prefix_pred_nil. +intros. +destruct l2; intuition; try discriminate. +unfold is_prefix_pred in H. +rewrite Bool.andb_true_iff in H. +rewrite forallb_forall in H. +apply prefix_pred_cons; intuition. +apply H0. +apply 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. + +Definition is_shift_past_state (_:unit) := + forallb (fun s:state => + match action_table s with + | Lookahead_act awp => + forallb (fun t => + match awp t with + | Shift_act s2 _ => + is_prefix_pred + (past_state_of_non_init_state s2) (head_states_of_state s) + | _ => true + end) + all_list + | _ => true + end) + all_list. + +Property is_shift_past_state_correct: + is_shift_past_state () = true -> shift_past_state. +Proof. +unfold is_shift_past_state, shift_past_state. +intros. +rewrite forallb_forall in H. +specialize (H s (all_list_forall s)). +destruct (action_table s); intuition. +rewrite forallb_forall in H. +specialize (H t (all_list_forall t)). +destruct (l t); intuition. +apply is_prefix_pred_correct; intuition. +Qed. + +(** 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. + +Definition is_goto_past_state (_:unit) := + forallb (fun s:state => + forallb (fun nt => + match goto_table s nt with + | Some (exist _ s2 _) => + is_prefix_pred + (past_state_of_non_init_state s2) (head_states_of_state s) + | None => true + end) + all_list) + all_list. + +Property is_goto_past_state_correct : + is_goto_past_state () = true -> goto_past_state. +Proof. +unfold is_goto_past_state, goto_past_state. +intros. +rewrite forallb_forall in H. +specialize (H s (all_list_forall s)). +rewrite forallb_forall in H. +specialize (H nt (all_list_forall nt)). +destruct (goto_table s nt); intuition. +destruct s0. +apply is_prefix_pred_correct; intuition. +Qed. + +(** 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. + +Property is_state_valid_after_pop_complete state sl pl : + state_valid_after_pop state sl pl -> is_state_valid_after_pop state sl pl = true. +Proof. +intro. +induction H; intuition. +destruct sl; intuition. +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) -> + goto_table state_new (prod_lhs prod) = None -> + match state_new with + | Init i => prod_lhs prod = start_nt i + | Ninit _ => False + end. + +Definition is_valid_for_reduce (state:state) prod:= + (is_prefix (prod_rhs_rev prod) (head_symbs_of_state state) && + forallb (fun state_new => + if is_state_valid_after_pop state_new (prod_rhs_rev prod) + (head_states_of_state state) then + match goto_table state_new (prod_lhs prod) with + | Some _ => true + | None => + match state_new with + | Init i => compare_eqb (prod_lhs prod) (start_nt i) + | Ninit _ => false + end + end + else + true) + all_list)%bool. + +Property is_valid_for_reduce_correct (state:state) prod: + is_valid_for_reduce state prod = true -> valid_for_reduce state prod. +Proof. +unfold is_valid_for_reduce, valid_for_reduce. +intros. +rewrite Bool.andb_true_iff in H. +split. +apply is_prefix_correct. +intuition. +intros. +rewrite forallb_forall in H. +destruct H. +specialize (H2 state_new (all_list_forall state_new)). +rewrite is_state_valid_after_pop_complete, H1 in H2. +destruct state_new; intuition. +rewrite compare_eqb_iff in H2; intuition. +intuition. +Qed. + +(** 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. + +Definition is_reduce_ok (_:unit) := + forallb (fun s => + match action_table s with + | Lookahead_act awp => + forallb (fun t => + match awp t with + | Reduce_act p => is_valid_for_reduce s p + | _ => true + end) + all_list + | Default_reduce_act p => is_valid_for_reduce s p + end) + all_list. + +Property is_reduce_ok_correct : + is_reduce_ok () = true -> reduce_ok. +Proof. +unfold is_reduce_ok, reduce_ok. +intros. +rewrite forallb_forall in H. +specialize (H s (all_list_forall s)). +destruct (action_table s). +apply is_valid_for_reduce_correct; intuition. +intro. +rewrite forallb_forall in H. +specialize (H t (all_list_forall t)). +destruct (l t); intuition. +apply is_valid_for_reduce_correct; intuition. +Qed. + +(** The automaton is safe **) +Definition safe := + shift_head_symbs /\ goto_head_symbs /\ shift_past_state /\ + goto_past_state /\ reduce_ok. + +Definition is_safe (_:unit) := + (is_shift_head_symbs () && is_goto_head_symbs () && is_shift_past_state () && + is_goto_past_state () && is_reduce_ok ())%bool. + +Property is_safe_correct: + is_safe () = true -> safe. +Proof. +unfold safe, is_safe. +repeat rewrite Bool.andb_true_iff. +intuition. +apply is_shift_head_symbs_correct; assumption. +apply is_goto_head_symbs_correct; assumption. +apply is_shift_past_state_correct; assumption. +apply is_goto_past_state_correct; assumption. +apply is_reduce_ok_correct; assumption. +Qed. + +End Make. diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v deleted file mode 100644 index a13f69b0..00000000 --- a/cparser/validator/Alphabet.v +++ /dev/null @@ -1,320 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import Int31. -Require Import Cyclic31. -Require Import Omega. -Require Import List. -Require Import Syntax. -Require Import Relations. -Require Import 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 usual equality. **) -Class ComparableUsualEq {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:ComparableUsualEq 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. - -(** [Comparable] provides a decidable equality. **) -Definition compare_eqdec {A:Type} {C:Comparable A} {U:ComparableUsualEq C} (x y:A): - {x = y} + {x <> y}. -Proof. -destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..]; - right; intro; destruct H; rewrite compare_refl in Heqc; discriminate. -Defined. - -Instance NComparableUsualEq : ComparableUsualEq natComparable := Nat.compare_eq. - -(** A pair of ComparableUsualEq is ComparableUsualEq **) -Instance PairComparableUsualEq - {A:Type} {CA:Comparable A} (UA:ComparableUsualEq CA) - {B:Type} {CB:Comparable B} (UB:ComparableUsualEq CB) : - ComparableUsualEq (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 [ComparableUsualEq] and [Finite]. **) -Class Alphabet (A:Type) := { - AlphabetComparable :> Comparable A; - AlphabetComparableUsualEq :> ComparableUsualEq 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 - [Int31] **) -Class Numbered (A:Type) := { - inj : A -> int31; - surj : int31 -> A; - surj_inj_compat : forall x, surj (inj x) = x; - inj_bound : int31; - inj_bound_spec : forall x, (phi (inj x) < phi inj_bound)%Z -}. - -Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A := - { AlphabetComparable := - {| compare := fun x y => compare31 (inj x) (inj y) |}; - AlphabetFinite := - {| all_list := fst (iter_int31 inj_bound _ - (fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }. -Next Obligation. apply Zcompare_antisym. Qed. -Next Obligation. -destruct c. unfold compare31 in *. -rewrite Z.compare_eq_iff in *. congruence. -eapply Zcompare_Lt_trans. apply H. apply H0. -eapply Zcompare_Gt_trans. apply H. apply H0. -Qed. -Next Obligation. -intros x y H. unfold compare, compare31 in H. -rewrite Z.compare_eq_iff in *. -rewrite <- surj_inj_compat, <- phi_inv_phi with (inj y), <- H. -rewrite phi_inv_phi, surj_inj_compat; reflexivity. -Qed. -Next Obligation. -rewrite iter_int31_iter_nat. -pose proof (inj_bound_spec x). -match goal with |- In x (fst ?p) => destruct p as [] eqn:? end. -replace inj_bound with i in H. -revert l i Heqp x H. -induction (Z.abs_nat (phi inj_bound)); intros. -inversion Heqp; clear Heqp; subst. -rewrite spec_0 in H. pose proof (phi_bounded (inj x)). omega. -simpl in Heqp. -destruct nat_rect; specialize (IHn _ _ (eq_refl _) x); simpl in *. -inversion Heqp. subst. clear Heqp. -rewrite phi_incr in H. -pose proof (phi_bounded i0). -pose proof (phi_bounded (inj x)). -destruct (Z_lt_le_dec (Z.succ (phi i0)) (2 ^ Z.of_nat size)%Z). -rewrite Zmod_small in H by omega. -apply Zlt_succ_le, Zle_lt_or_eq in H. -destruct H; simpl; auto. left. -rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity. -replace (Z.succ (phi i0)) with (2 ^ Z.of_nat size)%Z in H by omega. -rewrite Z_mod_same_full in H. -exfalso; omega. -rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal. -pose proof (phi_bounded inj_bound); pose proof (phi_bounded i). -rewrite <- Z.abs_eq with (phi i), <- Z.abs_eq with (phi inj_bound) by omega. -clear H H0 H1. -do 2 rewrite <- Zabs2Nat.id_abs. -f_equal. -revert l i Heqp. -assert (Z.abs_nat (phi inj_bound) < Z.abs_nat (2^31)). -apply Zabs_nat_lt, phi_bounded. -induction (Z.abs_nat (phi inj_bound)); intros. -inversion Heqp; reflexivity. -inversion Heqp; clear H1 H2 Heqp. -match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end. -pose proof (phi_bounded i0). -erewrite <- IHn, <- Zabs2Nat.inj_succ in H |- *; eauto; try omega. -rewrite phi_incr, Zmod_small; intuition; try omega. -apply inj_lt in H. -pose proof Z.le_le_succ_r. -do 2 rewrite Zabs2Nat.id_abs, Z.abs_eq in H; now eauto. -Qed. - -(** Previous class instances for [option A] **) -Program Instance OptionComparable {A:Type} (C:Comparable A) : Comparable (option A) := - { compare := fun x y => - match x, y return comparison with - | None, None => Eq - | None, Some _ => Lt - | Some _, None => Gt - | Some x, Some y => compare x y - end }. -Next Obligation. -destruct x, y; intuition. -apply compare_antisym. -Qed. -Next Obligation. -destruct x, y, z; try now intuition; -try (rewrite <- H in H0; discriminate). -apply (compare_trans _ _ _ _ H H0). -Qed. - -Instance OptionComparableUsualEq {A:Type} {C:Comparable A} (U:ComparableUsualEq C) : - ComparableUsualEq (OptionComparable C). -Proof. -intros x y. -destruct x, y; intuition; try discriminate. -rewrite (compare_eq a a0); intuition. -Qed. - -Program Instance OptionFinite {A:Type} (E:Finite A) : Finite (option A) := - { all_list := None :: map Some all_list }. -Next Obligation. -destruct x; intuition. -right. -apply in_map. -apply all_list_forall. -Defined. - -(** 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/cparser/validator/Automaton.v b/cparser/validator/Automaton.v deleted file mode 100644 index fc995298..00000000 --- a/cparser/validator/Automaton.v +++ /dev/null @@ -1,167 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Grammar. -Require Import Orders. -Require Export Alphabet. -Require Export List. -Require Export 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/cparser/validator/Grammar.v b/cparser/validator/Grammar.v deleted file mode 100644 index 8e427cd9..00000000 --- a/cparser/validator/Grammar.v +++ /dev/null @@ -1,166 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import List. -Require Import Syntax. -Require Import Alphabet. -Require Import Orders. -Require Tuples. - -(** 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); intuition. - rewrite (compare_eq n n0); intuition. - Qed. - Next Obligation. - rewrite in_app_iff. - destruct x; [left | right]; apply in_map; apply all_list_forall. - Qed. - -End Symbol. - -Module Type T. - Export Tuples. - - 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. - Parameter prod_rhs_rev: production -> list symbol. - Parameter prod_action: - forall p:production, - arrows_left - (map symbol_semantic_type (rev (prod_rhs_rev p))) - (symbol_semantic_type (NT (prod_lhs p))). - -End T. - -Module Defs(Import G:T). - - (** A token is a terminal and a semantic value for this terminal. **) - Definition token := {t:terminal & symbol_semantic_type (T t)}. - - (** A grammar creates a relation between word of tokens and semantic values. - This relation is parametrized by the head symbol. It defines the - "semantics" of the grammar. This relation is defined by a notion of - parse tree. **) - Inductive parse_tree: - forall (head_symbol:symbol) (word:list token) - (semantic_value:symbol_semantic_type head_symbol), Type := - - (** A single token has its semantic value as semantic value, for the - corresponding terminal as head symbol. **) - | Terminal_pt: - forall (t:terminal) (sem:symbol_semantic_type (T t)), - parse_tree (T t) - [existT (fun t => symbol_semantic_type (T t)) t sem] sem - - (** Given a production, if a word has a list of semantic values for the - right hand side as head symbols, then this word has the semantic value - given by the semantic action of the production for the left hand side - as head symbol.**) - | Non_terminal_pt: - forall {p:production} {word:list token} - {semantic_values:tuple (map symbol_semantic_type (rev (prod_rhs_rev p)))}, - parse_tree_list (rev (prod_rhs_rev p)) word semantic_values -> - parse_tree (NT (prod_lhs p)) word (uncurry (prod_action p) semantic_values) - - (** Basically the same relation as before, but for list of head symbols (ie. - We are building a forest of syntax trees. It is mutually recursive with the - previous relation **) - with parse_tree_list: - forall (head_symbols:list symbol) (word:list token) - (semantic_values:tuple (map symbol_semantic_type head_symbols)), - Type := - - (** The empty word has [()] as semantic for [[]] as head symbols list **) - | Nil_ptl: parse_tree_list [] [] () - - (** The cons of the semantic value for one head symbol and for a list of head - symbols **) - | Cons_ptl: - (** The semantic for the head **) - forall {head_symbolt:symbol} {wordt:list token} - {semantic_valuet:symbol_semantic_type head_symbolt}, - parse_tree head_symbolt wordt semantic_valuet -> - - (** and the semantic for the tail **) - forall {head_symbolsq:list symbol} {wordq:list token} - {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, - parse_tree_list head_symbolsq wordq semantic_valuesq -> - - (** give the semantic of the cons **) - parse_tree_list - (head_symbolt::head_symbolsq) - (wordt++wordq) - (semantic_valuet, semantic_valuesq). - - - Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) := - match tree with - | Terminal_pt _ _ => 1 - | Non_terminal_pt l => S (ptl_size l) - end - with ptl_size {head_symbols word sems} (tree:parse_tree_list head_symbols word sems) := - match tree with - | Nil_ptl => 0 - | Cons_ptl t q => - pt_size t + ptl_size q - end. -End Defs. diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v deleted file mode 100644 index 4ac02693..00000000 --- a/cparser/validator/Interpreter.v +++ /dev/null @@ -1,228 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import Streams. -Require Import List. -Require Import Syntax. -Require Automaton. -Require Import Alphabet. - -Module Make(Import A:Automaton.T). - -(** The error monad **) -Inductive result (A:Type) := - | Err: result A - | OK: A -> result A. - -Arguments Err [A]. -Arguments OK [A]. - -Definition bind {A B: Type} (f: result A) (g: A -> result B): result B := - match f with - | OK x => g x - | Err => Err - end. - -Definition bind2 {A B C: Type} (f: result (A * B)) (g: A -> B -> result C): - result C := - match f with - | OK (x, y) => g x y - | Err => Err - end. - -Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). - -Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) - (at level 200, X ident, Y ident, A at level 100, B at level 200). - -(** Some operations on streams **) - -(** Concatenation of a list and a stream **) -Fixpoint app_str {A:Type} (l:list A) (s:Stream A) := - match l with - | nil => s - | cons t q => Cons t (app_str q s) - end. - -Infix "++" := app_str (right associativity, at level 60). - -Lemma app_str_app_assoc {A:Type} (l1 l2:list A) (s:Stream A) : - l1 ++ (l2 ++ s) = (l1 ++ l2) ++ s. -Proof. -induction l1. -reflexivity. -simpl. -rewrite IHl1. -reflexivity. -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 Init. - -Variable init : initstate. - -(** The top state of a stack **) -Definition state_of_stack (stack:stack): state := - match stack with - | [] => init - | existT _ s _::_ => s - end. - -(** [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) (stack_cur:stack): - forall {A:Type} (action:arrows_right A (map symbol_semantic_type symbols_to_pop)), - result (stack * A) := - match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), result (stack * A) with - | [] => fun A action => OK (stack_cur, action) - | t::q => fun A action => - match stack_cur with - | existT _ state_cur sem::stack_rec => - match compare_eqdec (last_symb_of_non_init_state state_cur) t with - | left e => - let sem_conv := eq_rect _ symbol_semantic_type sem _ e in - pop q stack_rec (action sem_conv) - | right _ => Err - end - | [] => Err - end - end. - -(** [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)) -> Stream token -> step_result - | Progress_sr: stack -> Stream token -> step_result. - -Program Definition prod_action': - forall p, - arrows_right (symbol_semantic_type (NT (prod_lhs p))) - (map symbol_semantic_type (prod_rhs_rev p)):= - fun p => - eq_rect _ (fun x => x) (prod_action p) _ _. -Next Obligation. -unfold arrows_left, arrows_right; simpl. -rewrite <- fold_left_rev_right, <- map_rev, rev_involutive. -reflexivity. -Qed. - -(** [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 stack_cur production buffer: result step_result := - do (stack_new, sem) <- - pop (prod_rhs_rev production) stack_cur (prod_action' production); - match goto_table (state_of_stack stack_new) (prod_lhs production) with - | Some (exist _ state_new e) => - let sem := eq_rect _ _ sem _ e in - OK (Progress_sr (existT noninitstate_type state_new sem::stack_new) buffer) - | None => - match stack_new with - | [] => - match compare_eqdec (prod_lhs production) (start_nt init) with - | left e => - let sem := eq_rect _ (fun nt => symbol_semantic_type (NT nt)) sem _ e in - OK (Accept_sr sem buffer) - | right _ => Err - end - | _::_ => Err - end - end. - -(** One step of parsing. **) -Definition step stack_cur buffer: result step_result := - match action_table (state_of_stack stack_cur) with - | Default_reduce_act production => - reduce_step stack_cur production buffer - | Lookahead_act awt => - match Streams.hd buffer with - | existT _ term sem => - match awt term with - | Shift_act state_new e => - let sem_conv := eq_rect _ symbol_semantic_type sem _ e in - OK (Progress_sr (existT noninitstate_type state_new sem_conv::stack_cur) - (Streams.tl buffer)) - | Reduce_act production => - reduce_step stack_cur production buffer - | Fail_action => - OK Fail_sr - end - end - end. - -(** The parsing use a [nat] parameter [n_steps], so that we do not have to prove - terminaison, which is difficult. So the 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 [n_steps]), either a parsed semantic - value with a rest of the input buffer. -**) -Inductive parse_result := - | Fail_pr: parse_result - | Timeout_pr: parse_result - | Parsed_pr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> parse_result. - -Fixpoint parse_fix stack_cur buffer n_steps: result parse_result:= - match n_steps with - | O => OK Timeout_pr - | S it => - do r <- step stack_cur buffer; - match r with - | Fail_sr => OK Fail_pr - | Accept_sr t buffer_new => OK (Parsed_pr t buffer_new) - | Progress_sr s buffer_new => parse_fix s buffer_new it - end - end. - -Definition parse buffer n_steps: result parse_result := - parse_fix [] buffer n_steps. - -End Init. - -Arguments Fail_sr [init]. -Arguments Accept_sr [init] _ _. -Arguments Progress_sr [init] _ _. - -Arguments Fail_pr [init]. -Arguments Timeout_pr [init]. -Arguments Parsed_pr [init] _ _. - -End Make. - -Module Type T(A:Automaton.T). - Include (Make A). -End T. diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v deleted file mode 100644 index 2e64b8da..00000000 --- a/cparser/validator/Interpreter_complete.v +++ /dev/null @@ -1,686 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import Streams. -Require Import ProofIrrelevance. -Require Import Equality. -Require Import List. -Require Import Syntax. -Require Import Alphabet. -Require Import Arith. -Require Grammar. -Require Automaton. -Require Interpreter. -Require Validator_complete. - -Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A). -Module Import Valid := Validator_complete.Make A. - -(** * Completeness Proof **) - -Section Completeness_Proof. - -Hypothesis complete: complete. - -Proposition nullable_stable: nullable_stable. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. -Proposition first_stable: first_stable. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. -Proposition start_future: start_future. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. -Proposition terminal_shift: terminal_shift. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. -Proposition end_reduce: end_reduce. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. -Proposition start_goto: start_goto. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. -Proposition non_terminal_goto: non_terminal_goto. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. -Proposition non_terminal_closed: non_terminal_closed. -Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed. - -(** If the nullable predicate has been validated, then it is correct. **) -Lemma nullable_correct: - forall head sem word, word = [] -> - parse_tree head word sem -> nullable_symb head = true -with nullable_correct_list: - forall heads sems word, word = [] -> - parse_tree_list heads word sems -> nullable_word heads = true. -Proof with eauto. -intros. -destruct X. -congruence. -apply nullable_stable... -intros. -destruct X; simpl... -apply andb_true_intro. -apply app_eq_nil in H; destruct H; split... -Qed. - -(** If the first predicate has been validated, then it is correct. **) -Lemma first_correct: - forall head sem word t q, word = t::q -> - parse_tree head word sem -> - TerminalSet.In (projT1 t) (first_symb_set head) -with first_correct_list: - forall heads sems word t q, word = t::q -> - parse_tree_list heads word sems -> - TerminalSet.In (projT1 t) (first_word_set heads). -Proof with eauto. -intros. -destruct X. -inversion H; subst. -apply TerminalSet.singleton_2, compare_refl... -apply first_stable... -intros. -destruct X. -congruence. -simpl. -case_eq wordt; intros. -erewrite nullable_correct... -apply TerminalSet.union_3. -subst... -rewrite H0 in *; inversion H; destruct H2. -destruct (nullable_symb head_symbolt)... -apply TerminalSet.union_2... -Qed. - -Variable init: initstate. -Variable full_word: list token. -Variable buffer_end: Stream token. -Variable full_sem: symbol_semantic_type (NT (start_nt init)). - -Inductive pt_zipper: - forall (hole_symb:symbol) (hole_word:list token) - (hole_sem:symbol_semantic_type hole_symb), Type := -| Top_ptz: - pt_zipper (NT (start_nt init)) (full_word) (full_sem) -| Cons_ptl_ptz: - forall {head_symbolt:symbol} - {wordt:list token} - {semantic_valuet:symbol_semantic_type head_symbolt}, - - forall {head_symbolsq:list symbol} - {wordq:list token} - {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, - parse_tree_list head_symbolsq wordq semantic_valuesq -> - - ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq) - (semantic_valuet,semantic_valuesq) -> - - pt_zipper head_symbolt wordt semantic_valuet -with ptl_zipper: - forall (hole_symbs:list symbol) (hole_word:list token) - (hole_sems:tuple (map symbol_semantic_type hole_symbs)), Type := -| Non_terminal_pt_ptlz: - forall {p:production} {word:list token} - {semantic_values:tuple (map symbol_semantic_type (rev (prod_rhs_rev p)))}, - pt_zipper (NT (prod_lhs p)) word (uncurry (prod_action p) semantic_values) -> - ptl_zipper (rev (prod_rhs_rev p)) word semantic_values - -| Cons_ptl_ptlz: - forall {head_symbolt:symbol} - {wordt:list token} - {semantic_valuet:symbol_semantic_type head_symbolt}, - parse_tree head_symbolt wordt semantic_valuet -> - - forall {head_symbolsq:list symbol} - {wordq:list token} - {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)}, - - ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq) - (semantic_valuet,semantic_valuesq) -> - - ptl_zipper head_symbolsq wordq semantic_valuesq. - -Fixpoint ptlz_cost {hole_symbs hole_word hole_sems} - (ptlz:ptl_zipper hole_symbs hole_word hole_sems) := - match ptlz with - | Non_terminal_pt_ptlz ptz => - ptz_cost ptz - | Cons_ptl_ptlz pt ptlz' => - ptlz_cost ptlz' - end -with ptz_cost {hole_symb hole_word hole_sem} - (ptz:pt_zipper hole_symb hole_word hole_sem) := - match ptz with - | Top_ptz => 0 - | Cons_ptl_ptz ptl ptlz' => - 1 + ptl_size ptl + ptlz_cost ptlz' - end. - -Inductive pt_dot: Type := -| Reduce_ptd: ptl_zipper [] [] () -> pt_dot -| Shift_ptd: - forall (term:terminal) (sem: symbol_semantic_type (T term)) - {symbolsq wordq semsq}, - parse_tree_list symbolsq wordq semsq -> - ptl_zipper (T term::symbolsq) (existT (fun t => symbol_semantic_type (T t)) term sem::wordq) (sem, semsq) -> - pt_dot. - -Definition ptd_cost (ptd:pt_dot) := - match ptd with - | Reduce_ptd ptlz => ptlz_cost ptlz - | Shift_ptd _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz - end. - -Fixpoint ptlz_buffer {hole_symbs hole_word hole_sems} - (ptlz:ptl_zipper hole_symbs hole_word hole_sems): Stream token := - match ptlz with - | Non_terminal_pt_ptlz ptz => - ptz_buffer ptz - | Cons_ptl_ptlz _ ptlz' => - ptlz_buffer ptlz' - end -with ptz_buffer {hole_symb hole_word hole_sem} - (ptz:pt_zipper hole_symb hole_word hole_sem): Stream token := - match ptz with - | Top_ptz => buffer_end - | @Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' => - wordq++ptlz_buffer ptlz' - end. - -Definition ptd_buffer (ptd:pt_dot) := - match ptd with - | Reduce_ptd ptlz => ptlz_buffer ptlz - | @Shift_ptd term sem _ wordq _ _ ptlz => - Cons (existT (fun t => symbol_semantic_type (T t)) term sem) - (wordq ++ ptlz_buffer ptlz) - end. - -Fixpoint ptlz_prod {hole_symbs hole_word hole_sems} - (ptlz:ptl_zipper hole_symbs hole_word hole_sems): production := - match ptlz with - | @Non_terminal_pt_ptlz prod _ _ _ => prod - | Cons_ptl_ptlz _ ptlz' => - ptlz_prod ptlz' - end. - -Fixpoint ptlz_past {hole_symbs hole_word hole_sems} - (ptlz:ptl_zipper hole_symbs hole_word hole_sems): list symbol := - match ptlz with - | Non_terminal_pt_ptlz _ => [] - | @Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz' - end. - -Lemma ptlz_past_ptlz_prod: - forall hole_symbs hole_word hole_sems - (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - rev_append hole_symbs (ptlz_past ptlz) = prod_rhs_rev (ptlz_prod ptlz). -Proof. -fix ptlz_past_ptlz_prod 4. -destruct ptlz; simpl. -rewrite <- rev_alt, rev_involutive; reflexivity. -apply (ptlz_past_ptlz_prod _ _ _ ptlz). -Qed. - -Definition ptlz_state_compat {hole_symbs hole_word hole_sems} - (ptlz:ptl_zipper hole_symbs hole_word hole_sems) - (state:state): Prop := - state_has_future state (ptlz_prod ptlz) hole_symbs - (projT1 (Streams.hd (ptlz_buffer ptlz))). - -Fixpoint ptlz_stack_compat {hole_symbs hole_word hole_sems} - (ptlz:ptl_zipper hole_symbs hole_word hole_sems) - (stack:stack): Prop := - ptlz_state_compat ptlz (state_of_stack init stack) /\ - match ptlz with - | Non_terminal_pt_ptlz ptz => - ptz_stack_compat ptz stack - | @Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' => - match stack with - | [] => False - | existT _ _ sem'::stackq => - ptlz_stack_compat ptlz' stackq /\ - sem ~= sem' - end - end -with ptz_stack_compat {hole_symb hole_word hole_sem} - (ptz:pt_zipper hole_symb hole_word hole_sem) - (stack:stack): Prop := - match ptz with - | Top_ptz => stack = [] - | Cons_ptl_ptz _ ptlz' => - ptlz_stack_compat ptlz' stack - end. - -Lemma ptlz_stack_compat_ptlz_state_compat: - forall hole_symbs hole_word hole_sems - (ptlz:ptl_zipper hole_symbs hole_word hole_sems) - (stack:stack), - ptlz_stack_compat ptlz stack -> ptlz_state_compat ptlz (state_of_stack init stack). -Proof. -destruct ptlz; simpl; intuition. -Qed. - -Definition ptd_stack_compat (ptd:pt_dot) (stack:stack): Prop := - match ptd with - | Reduce_ptd ptlz => ptlz_stack_compat ptlz stack - | Shift_ptd _ _ _ ptlz => ptlz_stack_compat ptlz stack - end. - -Fixpoint build_pt_dot {hole_symbs hole_word hole_sems} - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems) - :pt_dot := - match ptl in parse_tree_list hole_symbs hole_word hole_sems - return ptl_zipper hole_symbs hole_word hole_sems -> _ - with - | Nil_ptl => fun ptlz => - Reduce_ptd ptlz - | Cons_ptl pt ptl' => - match pt in parse_tree hole_symb hole_word hole_sem - return ptl_zipper (hole_symb::_) (hole_word++_) (hole_sem,_) -> _ - with - | Terminal_pt term sem => fun ptlz => - Shift_ptd term sem ptl' ptlz - | Non_terminal_pt ptl'' => fun ptlz => - build_pt_dot ptl'' - (Non_terminal_pt_ptlz (Cons_ptl_ptz ptl' ptlz)) - end - end ptlz. - -Lemma build_pt_dot_cost: - forall hole_symbs hole_word hole_sems - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - ptd_cost (build_pt_dot ptl ptlz) = ptl_size ptl + ptlz_cost ptlz. -Proof. -fix build_pt_dot_cost 4. -destruct ptl; intros. -reflexivity. -destruct p. -reflexivity. -simpl; rewrite build_pt_dot_cost. -simpl; rewrite <- plus_n_Sm, Nat.add_assoc; reflexivity. -Qed. - -Lemma build_pt_dot_buffer: - forall hole_symbs hole_word hole_sems - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - ptd_buffer (build_pt_dot ptl ptlz) = hole_word ++ ptlz_buffer ptlz. -Proof. -fix build_pt_dot_buffer 4. -destruct ptl; intros. -reflexivity. -destruct p. -reflexivity. -simpl; rewrite build_pt_dot_buffer. -apply app_str_app_assoc. -Qed. - -Lemma ptd_stack_compat_build_pt_dot: - forall hole_symbs hole_word hole_sems - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems) - (stack:stack), - ptlz_stack_compat ptlz stack -> - ptd_stack_compat (build_pt_dot ptl ptlz) stack. -Proof. -fix ptd_stack_compat_build_pt_dot 4. -destruct ptl; intros. -eauto. -destruct p. -eauto. -simpl. -apply ptd_stack_compat_build_pt_dot. -split. -apply ptlz_stack_compat_ptlz_state_compat, non_terminal_closed in H. -apply H; clear H; eauto. -destruct wordq. -right; split. -eauto. -eapply nullable_correct_list; eauto. -left. -eapply first_correct_list; eauto. -eauto. -Qed. - -Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems} - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems): - { word:_ & { sem:_ & - (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * - parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } := - match ptlz in ptl_zipper hole_symbs hole_word hole_sems - return parse_tree_list hole_symbs hole_word hole_sems -> - { word:_ & { sem:_ & - (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem * - parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } - with - | @Non_terminal_pt_ptlz prod word sem ptz => fun ptl => - let sem := uncurry (prod_action prod) sem in - existT _ word (existT _ sem (ptz, Non_terminal_pt ptl)) - | Cons_ptl_ptlz pt ptlz' => fun ptl => - pop_ptlz (Cons_ptl pt ptl) ptlz' - end ptl. - -Lemma pop_ptlz_cost: - forall hole_symbs hole_word hole_sems - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in - ptlz_cost ptlz = ptz_cost ptz. -Proof. -fix pop_ptlz_cost 5. -destruct ptlz. -reflexivity. -simpl; apply pop_ptlz_cost. -Qed. - -Lemma pop_ptlz_buffer: - forall hole_symbs hole_word hole_sems - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in - ptlz_buffer ptlz = ptz_buffer ptz. -Proof. -fix pop_ptlz_buffer 5. -destruct ptlz. -reflexivity. -simpl; apply pop_ptlz_buffer. -Qed. - -Lemma pop_ptlz_pop_stack_compat_converter: - forall A hole_symbs hole_word hole_sems (ptlz:ptl_zipper hole_symbs hole_word hole_sems), - arrows_left (map symbol_semantic_type (rev (prod_rhs_rev (ptlz_prod ptlz)))) A = - arrows_left (map symbol_semantic_type hole_symbs) - (arrows_right A (map symbol_semantic_type (ptlz_past ptlz))). -Proof. -intros. -rewrite <- ptlz_past_ptlz_prod. -unfold arrows_right, arrows_left. -rewrite rev_append_rev, map_rev, map_app, map_rev, <- fold_left_rev_right, rev_involutive, fold_right_app. -rewrite fold_left_rev_right. -reflexivity. -Qed. - -Lemma pop_ptlz_pop_stack_compat: - forall hole_symbs hole_word hole_sems - (ptl:parse_tree_list hole_symbs hole_word hole_sems) - (ptlz:ptl_zipper hole_symbs hole_word hole_sems) - (stack:stack), - - ptlz_stack_compat ptlz stack -> - - let action' := - eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _ - (pop_ptlz_pop_stack_compat_converter _ _ _ _ _) - in - let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in - match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with - | OK (stack', sem') => - ptz_stack_compat ptz stack' /\ sem = sem' - | Err => True - end. -Proof. -Opaque AlphabetComparable AlphabetComparableUsualEq. -fix pop_ptlz_pop_stack_compat 5. -destruct ptlz. intros; simpl. -split. -apply H. -eapply (f_equal (fun X => uncurry X semantic_values)). -apply JMeq_eq, JMeq_sym, JMeq_eqrect with (P:=fun x => x). -simpl; intros; destruct stack0. -destruct (proj2 H). -simpl in H; destruct H. -destruct s as (state, sem'). -destruct H0. -specialize (pop_ptlz_pop_stack_compat _ _ _ (Cons_ptl p ptl) ptlz _ H0). -destruct (pop_ptlz (Cons_ptl p ptl) ptlz) as [word [sem []]]. -destruct (compare_eqdec (last_symb_of_non_init_state state) head_symbolt); intuition. -eapply JMeq_sym, JMeq_trans, JMeq_sym, JMeq_eq in H1; [|apply JMeq_eqrect with (e:=e)]. -rewrite <- H1. -simpl in pop_ptlz_pop_stack_compat. -erewrite proof_irrelevance with (p1:=pop_ptlz_pop_stack_compat_converter _ _ _ _ _). -apply pop_ptlz_pop_stack_compat. -Transparent AlphabetComparable AlphabetComparableUsualEq. -Qed. - -Definition next_ptd (ptd:pt_dot): option pt_dot := - match ptd with - | Shift_ptd term sem ptl ptlz => - Some (build_pt_dot ptl (Cons_ptl_ptlz (Terminal_pt term sem) ptlz)) - | Reduce_ptd ptlz => - let 'existT _ _ (existT _ _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in - match ptz in pt_zipper sym _ _ return parse_tree sym _ _ -> _ with - | Top_ptz => fun pt => None - | Cons_ptl_ptz ptl ptlz' => - fun pt => Some (build_pt_dot ptl (Cons_ptl_ptlz pt ptlz')) - end pt - end. - -Lemma next_ptd_cost: - forall ptd, - match next_ptd ptd with - | None => ptd_cost ptd = 0 - | Some ptd' => ptd_cost ptd = S (ptd_cost ptd') - end. -Proof. -destruct ptd. unfold next_ptd. -pose proof (pop_ptlz_cost _ _ _ Nil_ptl p). -destruct (pop_ptlz Nil_ptl p) as [word[sem[[]]]]. -assumption. -rewrite build_pt_dot_cost. -assumption. -simpl; rewrite build_pt_dot_cost; reflexivity. -Qed. - -Lemma reduce_step_next_ptd: - forall (ptlz:ptl_zipper [] [] ()) (stack:stack), - ptlz_stack_compat ptlz stack -> - match reduce_step init stack (ptlz_prod ptlz) (ptlz_buffer ptlz) with - | OK Fail_sr => - False - | OK (Accept_sr sem buffer) => - sem = full_sem /\ buffer = buffer_end /\ next_ptd (Reduce_ptd ptlz) = None - | OK (Progress_sr stack buffer) => - match next_ptd (Reduce_ptd ptlz) with - | None => False - | Some ptd => - ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd - end - | Err => - True - end. -Proof. -intros. -unfold reduce_step, next_ptd. -apply pop_ptlz_pop_stack_compat with (ptl:=Nil_ptl) in H. -pose proof (pop_ptlz_buffer _ _ _ Nil_ptl ptlz). -destruct (pop_ptlz Nil_ptl ptlz) as [word [sem [ptz pt]]]. -rewrite H0; clear H0. -revert H. -match goal with - |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end => - replace p1 with p2; [destruct p2 as [|[]]; intros|] -end. -assumption. -simpl. -destruct H; subst. -generalize dependent s0. -generalize (prod_lhs (ptlz_prod ptlz)); clear ptlz stack0. -dependent destruction ptz; intros. -simpl in H; subst; simpl. -pose proof start_goto; unfold Valid.start_goto in H; rewrite H. -destruct (compare_eqdec (start_nt init) (start_nt init)); intuition. -apply JMeq_eq, JMeq_eqrect with (P:=fun nt => symbol_semantic_type (NT nt)). -pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). -apply non_terminal_goto in H0. -destruct (goto_table (state_of_stack init s) n) as [[]|]; intuition. -apply ptd_stack_compat_build_pt_dot; simpl; intuition. -symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type). -symmetry; apply build_pt_dot_buffer. -destruct s; intuition. -simpl in H; apply ptlz_stack_compat_ptlz_state_compat in H. -destruct (H0 _ _ _ H eq_refl). -generalize (pop_ptlz_pop_stack_compat_converter (symbol_semantic_type (NT (prod_lhs (ptlz_prod ptlz)))) _ _ _ ptlz). -pose proof (ptlz_past_ptlz_prod _ _ _ ptlz); simpl in H. -rewrite H; clear H. -intro; f_equal; simpl. -apply JMeq_eq. -etransitivity. -apply JMeq_eqrect with (P:=fun x => x). -symmetry. -apply JMeq_eqrect with (P:=fun x => x). -Qed. - -Lemma step_next_ptd: - forall (ptd:pt_dot) (stack:stack), - ptd_stack_compat ptd stack -> - match step init stack (ptd_buffer ptd) with - | OK Fail_sr => - False - | OK (Accept_sr sem buffer) => - sem = full_sem /\ buffer = buffer_end /\ next_ptd ptd = None - | OK (Progress_sr stack buffer) => - match next_ptd ptd with - | None => False - | Some ptd => - ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd - end - | Err => - True - end. -Proof. -intros. -destruct ptd. -pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). -apply end_reduce in H0. -unfold step. -destruct (action_table (state_of_stack init stack0)). -rewrite H0 by reflexivity. -apply reduce_step_next_ptd; assumption. -simpl; destruct (Streams.hd (ptlz_buffer p)); simpl in H0. -destruct (l x); intuition; rewrite H1. -apply reduce_step_next_ptd; assumption. -pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H). -apply terminal_shift in H0. -unfold step. -destruct (action_table (state_of_stack init stack0)); intuition. -simpl; destruct (Streams.hd (ptlz_buffer p0)) as [] eqn:?. -destruct (l term); intuition. -apply ptd_stack_compat_build_pt_dot; simpl; intuition. -unfold ptlz_state_compat; simpl; destruct Heqt; assumption. -symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type). -rewrite build_pt_dot_buffer; reflexivity. -Qed. - -Lemma parse_fix_complete: - forall (ptd:pt_dot) (stack:stack) (n_steps:nat), - ptd_stack_compat ptd stack -> - match parse_fix init stack (ptd_buffer ptd) n_steps with - | OK (Parsed_pr sem_res buffer_end_res) => - sem_res = full_sem /\ buffer_end_res = buffer_end /\ - S (ptd_cost ptd) <= n_steps - | OK Fail_pr => False - | OK Timeout_pr => n_steps < S (ptd_cost ptd) - | Err => True - end. -Proof. -fix parse_fix_complete 3. -destruct n_steps; intros; simpl. -apply Nat.lt_0_succ. -apply step_next_ptd in H. -pose proof (next_ptd_cost ptd). -destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition. -rewrite H3 in H0; rewrite H0. -apply le_n_S, Nat.le_0_l. -destruct (next_ptd ptd); intuition; subst. -eapply parse_fix_complete with (n_steps:=n_steps) in H1. -rewrite H0. -destruct (parse_fix init s (ptd_buffer p) n_steps) as [|[]]; try assumption. -apply lt_n_S; assumption. -destruct H1 as [H1 []]; split; [|split]; try assumption. -apply le_n_S; assumption. -Qed. - -Variable full_pt: parse_tree (NT (start_nt init)) full_word full_sem. - -Definition init_ptd := - match full_pt in parse_tree head full_word full_sem return - pt_zipper head full_word full_sem -> - match head return Type with | T _ => unit | NT _ => pt_dot end - with - | Terminal_pt _ _ => fun _ => () - | Non_terminal_pt ptl => - fun top => build_pt_dot ptl (Non_terminal_pt_ptlz top) - end Top_ptz. - -Lemma init_ptd_compat: - ptd_stack_compat init_ptd []. -Proof. -unfold init_ptd. -assert (ptz_stack_compat Top_ptz []) by reflexivity. -pose proof (start_future init); revert H0. -generalize dependent Top_ptz. -generalize dependent full_word. -generalize full_sem. -generalize (start_nt init). -dependent destruction full_pt0. -intros. -apply ptd_stack_compat_build_pt_dot; simpl; intuition. -apply H0; reflexivity. -Qed. - -Lemma init_ptd_cost: - S (ptd_cost init_ptd) = pt_size full_pt. -Proof. -unfold init_ptd. -assert (ptz_cost Top_ptz = 0) by reflexivity. -generalize dependent Top_ptz. -generalize dependent full_word. -generalize full_sem. -generalize (start_nt init). -dependent destruction full_pt0. -intros. -rewrite build_pt_dot_cost; simpl. -rewrite H, Nat.add_0_r; reflexivity. -Qed. - -Lemma init_ptd_buffer: - ptd_buffer init_ptd = full_word ++ buffer_end. -Proof. -unfold init_ptd. -assert (ptz_buffer Top_ptz = buffer_end) by reflexivity. -generalize dependent Top_ptz. -generalize dependent full_word. -generalize full_sem. -generalize (start_nt init). -dependent destruction full_pt0. -intros. -rewrite build_pt_dot_buffer; simpl. -rewrite H; reflexivity. -Qed. - -Theorem parse_complete n_steps: - match parse init (full_word ++ buffer_end) n_steps with - | OK (Parsed_pr sem_res buffer_end_res) => - sem_res = full_sem /\ buffer_end_res = buffer_end /\ - pt_size full_pt <= n_steps - | OK Fail_pr => False - | OK Timeout_pr => n_steps < pt_size full_pt - | Err => True - end. -Proof. -pose proof (parse_fix_complete init_ptd [] n_steps init_ptd_compat). -rewrite init_ptd_buffer, init_ptd_cost in H. -apply H. -Qed. - -End Completeness_Proof. - -End Make. diff --git a/cparser/validator/Interpreter_correct.v b/cparser/validator/Interpreter_correct.v deleted file mode 100644 index 1263d4e3..00000000 --- a/cparser/validator/Interpreter_correct.v +++ /dev/null @@ -1,228 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import Streams. -Require Import List. -Require Import Syntax. -Require Import Equality. -Require Import Alphabet. -Require Grammar. -Require Automaton. -Require Interpreter. - -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 state, 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) - (semantic_valuet:_), - inhabited (parse_tree (last_symb_of_non_init_state s) wordt semantic_valuet) -> - - word_has_stack_semantics - (wordq++wordt) (existT noninitstate_type s semantic_valuet::stackq). - -Lemma pop_invariant_converter: - forall A symbols_to_pop symbols_popped, - arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A = - arrows_left (map symbol_semantic_type symbols_popped) - (arrows_right A (map symbol_semantic_type symbols_to_pop)). -Proof. -intros. -unfold arrows_right, arrows_left. -rewrite rev_append_rev, map_app, map_rev, fold_left_app. -apply f_equal. -rewrite <- fold_left_rev_right, rev_involutive. -reflexivity. -Qed. - -(** [pop] preserves the invariant **) -Lemma pop_invariant: - forall (symbols_to_pop symbols_popped:list symbol) - (stack_cur:stack) - (A:Type) - (action:arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A), - forall word_stack word_popped, - forall sem_popped, - word_has_stack_semantics word_stack stack_cur -> - inhabited (parse_tree_list symbols_popped word_popped sem_popped) -> - let action' := eq_rect _ (fun x=>x) action _ (pop_invariant_converter _ _ _) in - match pop symbols_to_pop stack_cur (uncurry action' sem_popped) with - | OK (stack_new, sem) => - exists word1res word2res sem_full, - (word_stack = word1res ++ word2res)%list /\ - word_has_stack_semantics word1res stack_new /\ - sem = uncurry action sem_full /\ - inhabited ( - parse_tree_list (rev_append symbols_to_pop symbols_popped) (word2res++word_popped) sem_full) - | Err => True - end. -Proof. -induction symbols_to_pop; intros; unfold pop; fold pop. -exists word_stack, ([]:list token), sem_popped; intuition. -f_equal. -apply JMeq_eq, JMeq_eqrect with (P:=(fun x => x)). -destruct stack_cur as [|[]]; eauto. -destruct (compare_eqdec (last_symb_of_non_init_state x) a); eauto. -destruct e; simpl. -dependent destruction H. -destruct H0, H1. apply (Cons_ptl X), inhabits in X0. -specialize (IHsymbols_to_pop _ _ _ action0 _ _ _ H X0). -match goal with - IHsymbols_to_pop:match ?p1 with Err => _ | OK _ => _ end |- match ?p2 with Err => _ | OK _ => _ end => - replace p2 with p1; [destruct p1 as [|[]]|]; intuition -end. -destruct IHsymbols_to_pop as [word1res [word2res [sem_full []]]]; intuition; subst. -exists word1res. -eexists. -exists sem_full. -intuition. -rewrite <- app_assoc; assumption. -simpl; f_equal; f_equal. -apply JMeq_eq. -etransitivity. -apply JMeq_eqrect with (P:=(fun x => x)). -symmetry. -apply JMeq_eqrect with (P:=(fun x => x)). -Qed. - -(** [reduce_step] preserves the invariant **) -Lemma reduce_step_invariant (stack:stack) (prod:production): - forall word buffer, word_has_stack_semantics word stack -> - match reduce_step init stack prod buffer with - | OK (Accept_sr sem buffer_new) => - buffer = buffer_new /\ - inhabited (parse_tree (NT (start_nt init)) word sem) - | OK (Progress_sr stack_new buffer_new) => - buffer = buffer_new /\ - word_has_stack_semantics word stack_new - | Err | OK Fail_sr => True - end. -Proof with eauto. -intros. -unfold reduce_step. -pose proof (pop_invariant (prod_rhs_rev prod) [] stack (symbol_semantic_type (NT (prod_lhs prod)))). -revert H0. -generalize (pop_invariant_converter (symbol_semantic_type (NT (prod_lhs prod))) (prod_rhs_rev prod) []). -rewrite <- rev_alt. -intros. -specialize (H0 (prod_action prod) _ [] () H (inhabits Nil_ptl)). -match goal with H0:let action' := ?a in _ |- _ => replace a with (prod_action' prod) in H0 end. -simpl in H0. -destruct (pop (prod_rhs_rev prod) stack (prod_action' prod)) as [|[]]; intuition. -destruct H0 as [word1res [word2res [sem_full]]]; intuition. -destruct H4; apply Non_terminal_pt, inhabits in X. -match goal with X:inhabited (parse_tree _ _ ?u) |- _ => replace u with s0 in X end. -clear sem_full H2. -simpl; destruct (goto_table (state_of_stack init s) (prod_lhs prod)) as [[]|]; intuition; subst. -rewrite app_nil_r in X; revert s0 X; rewrite e0; intro; simpl. -constructor... -destruct s; intuition. -destruct (compare_eqdec (prod_lhs prod) (start_nt init)); intuition. -rewrite app_nil_r in X. -rewrite <- e0. -inversion H0. -destruct X; constructor... -apply JMeq_eq. -etransitivity. -apply JMeq_eqrect with (P:=(fun x => x)). -symmetry. -apply JMeq_eqrect with (P:=(fun x => x)). -Qed. - -(** [step] preserves the invariant **) -Lemma step_invariant (stack:stack) (buffer:Stream token): - forall buffer_tmp, - (exists word_old, - buffer = word_old ++ buffer_tmp /\ - word_has_stack_semantics word_old stack) -> - match step init stack buffer_tmp with - | OK (Accept_sr sem buffer_new) => - exists word_new, - buffer = word_new ++ buffer_new /\ - inhabited (parse_tree (NT (start_nt init)) word_new sem) - | OK (Progress_sr stack_new buffer_new) => - exists word_new, - buffer = word_new ++ buffer_new /\ - word_has_stack_semantics word_new stack_new - | Err | OK Fail_sr => True - end. -Proof with eauto. -intros. -destruct H, H. -unfold step. -destruct (action_table (state_of_stack init stack)). -pose proof (reduce_step_invariant stack p x buffer_tmp). -destruct (reduce_step init stack p buffer_tmp) as [|[]]; intuition; subst... -destruct buffer_tmp. -unfold Streams.hd. -destruct t. -destruct (l x0); intuition. -exists (x ++ [existT (fun t => symbol_semantic_type (T t)) x0 s])%list. -split. -now rewrite <- app_str_app_assoc; intuition. -apply Cons_stack_whss; intuition. -destruct e; simpl. -now exact (inhabits (Terminal_pt _ _)). -match goal with |- (match reduce_step init stack p ?buff with Err => _ | OK _ => _ end) => - pose proof (reduce_step_invariant stack p x buff); - destruct (reduce_step init stack p buff) as [|[]]; intuition; subst -end... -Qed. - -(** The interpreter is correct : if it returns a semantic value, then the input - word has this semantic value. -**) -Theorem parse_correct buffer n_steps: - match parse init buffer n_steps with - | OK (Parsed_pr sem buffer_new) => - exists word_new, - buffer = word_new ++ buffer_new /\ - inhabited (parse_tree (NT (start_nt init)) word_new sem) - | _ => True - end. -Proof. -unfold parse. -assert (exists w, buffer = w ++ buffer /\ word_has_stack_semantics w []). -exists ([]:list token); intuition. -now apply Nil_stack_whss. -revert H. -generalize ([]:stack), buffer at 2 3. -induction n_steps; simpl; intuition. -pose proof (step_invariant _ _ _ H). -destruct (step init s buffer0); simpl; intuition. -destruct s0; intuition. -apply IHn_steps; intuition. -Qed. - -End Init. - -End Make. diff --git a/cparser/validator/Interpreter_safe.v b/cparser/validator/Interpreter_safe.v deleted file mode 100644 index a1aa35b8..00000000 --- a/cparser/validator/Interpreter_safe.v +++ /dev/null @@ -1,275 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import Streams. -Require Import Equality. -Require Import List. -Require Import Syntax. -Require Import Alphabet. -Require Grammar. -Require Automaton. -Require Validator_safe. -Require Interpreter. - -Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A). -Module Import Valid := Validator_safe.Make A. - -(** * A correct automaton does not crash **) - -Section Safety_proof. - -Hypothesis safe: safe. - -Proposition shift_head_symbs: shift_head_symbs. -Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. -Proposition goto_head_symbs: goto_head_symbs. -Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. -Proposition shift_past_state: shift_past_state. -Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. -Proposition goto_past_state: goto_past_state. -Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. -Proposition reduce_ok: reduce_ok. -Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed. - -(** We prove that a correct automaton won't crash : the interpreter will - not return [Err] **) - -Variable init : initstate. - -(** 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 init stack)) - (symb_stack_of_stack stack) -> - prefix_pred (head_states_of_state (state_of_stack init stack)) - (state_stack_of_stack stack) -> - stack_invariant_next stack -> - stack_invariant stack -with stack_invariant_next: stack -> Prop := - | stack_invariant_next_nil: - stack_invariant_next [] - | stack_invariant_next_cons: - forall state_cur st stack_rec, - stack_invariant stack_rec -> - stack_invariant_next (existT _ state_cur st::stack_rec). - -(** [pop] conserves the stack invariant and does not crash - under the assumption that we can pop at this place. - Moreover, after a pop, the top state of the stack is allowed. **) -Lemma pop_stack_invariant_conserved - (symbols_to_pop:list symbol) (stack_cur:stack) A action: - stack_invariant stack_cur -> - prefix symbols_to_pop (head_symbs_of_state (state_of_stack init stack_cur)) -> - match pop symbols_to_pop stack_cur (A:=A) action with - | OK (stack_new, _) => - stack_invariant stack_new /\ - state_valid_after_pop - (state_of_stack init stack_new) symbols_to_pop - (head_states_of_state (state_of_stack init stack_cur)) - | Err => False - end. -Proof with eauto. - intros. - pose proof H. - destruct H. - revert H H0 H1 H2 H3. - generalize (head_symbs_of_state (state_of_stack init stack0)). - generalize (head_states_of_state (state_of_stack init stack0)). - revert stack0 A action. - induction symbols_to_pop; intros. - - split... - destruct l; constructor. - inversion H2; subst. - specialize (H7 (state_of_stack init stack0)). - destruct (f2 (state_of_stack init stack0)) as [] eqn:? ... - destruct stack0 as [|[]]; simpl in *. - + inversion H6; subst. - unfold singleton_state_pred in Heqb0. - now rewrite compare_refl in Heqb0; discriminate. - + inversion H6; subst. - unfold singleton_state_pred in Heqb0. - now rewrite compare_refl in Heqb0; discriminate. - - destruct stack0 as [|[]]; unfold pop. - + inversion H0; subst. - now inversion H. - + fold pop. - destruct (compare_eqdec (last_symb_of_non_init_state x) a). - * inversion H0; subst. clear H0. - inversion H; subst. clear H. - dependent destruction H3; simpl. - assert (prefix_pred (List.tl l) (state_stack_of_stack stack0)). - unfold tl; destruct l; [constructor | inversion H2]... - pose proof H. destruct H3. - specialize (IHsymbols_to_pop stack0 A (action0 n) _ _ H4 H7 H H0 H6). - revert IHsymbols_to_pop. - fold (noninitstate_type x); generalize (pop symbols_to_pop stack0 (action0 n)). - destruct r as [|[]]; intuition... - destruct l; constructor... - * apply n0. - inversion H0; subst. - inversion H; subst... -Qed. - -(** [prefix] is associative **) -Lemma prefix_ass: - forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3. -Proof. -induction l1; intros. -constructor. -inversion H; subst. -inversion H0; subst. -constructor; eauto. -Qed. - -(** [prefix_pred] is associative **) -Lemma prefix_pred_ass: - forall (l1 l2 l3:list (state->bool)), - prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3. -Proof. -induction l1; intros. -constructor. -inversion H; subst. -inversion H0; subst. -constructor; eauto. -intro. -specialize (H3 x). -specialize (H4 x). -destruct (f0 x); simpl in *; intuition. -rewrite H4 in H3; intuition. -Qed. - -(** If we have the right to reduce at this state, then the stack invariant - is conserved by [reduce_step] and [reduce_step] does not crash. **) -Lemma reduce_step_stack_invariant_conserved stack prod buff: - stack_invariant stack -> - valid_for_reduce (state_of_stack init stack) prod -> - match reduce_step init stack prod buff with - | OK (Fail_sr | Accept_sr _ _) => True - | OK (Progress_sr stack_new _) => stack_invariant stack_new - | Err => False - end. -Proof with eauto. -unfold valid_for_reduce. -intuition. -unfold reduce_step. -pose proof (pop_stack_invariant_conserved (prod_rhs_rev prod) stack _ (prod_action' prod)). -destruct (pop (prod_rhs_rev prod) stack (prod_action' prod)) as [|[]]. -apply H0... -destruct H0... -pose proof (goto_head_symbs (state_of_stack init s) (prod_lhs prod)). -pose proof (goto_past_state (state_of_stack init s) (prod_lhs prod)). -unfold bind2. -destruct H0. -specialize (H2 _ H3)... -destruct (goto_table (state_of_stack init stack0) (prod_lhs prod)) as [[]|]. -constructor. -simpl. -constructor. -eapply prefix_ass... -unfold state_stack_of_stack; simpl; constructor. -intro; destruct (singleton_state_pred x x0); reflexivity. -eapply prefix_pred_ass... -constructor... -constructor... -destruct stack0 as [|[]]... -destruct (compare_eqdec (prod_lhs prod) (start_nt init))... -apply n, H2, eq_refl. -apply H2, eq_refl. -Qed. - -(** If the automaton is safe, then the stack invariant is conserved by - [step] and [step] does not crash. **) -Lemma step_stack_invariant_conserved (stack:stack) buffer: - stack_invariant stack -> - match step init stack buffer with - | OK (Fail_sr | Accept_sr _ _) => True - | OK (Progress_sr stack_new _) => stack_invariant stack_new - | Err => False - end. -Proof with eauto. -intro. -unfold step. -pose proof (shift_head_symbs (state_of_stack init stack)). -pose proof (shift_past_state (state_of_stack init stack)). -pose proof (reduce_ok (state_of_stack init stack)). -destruct (action_table (state_of_stack init stack)). -apply reduce_step_stack_invariant_conserved... -destruct buffer as [[]]; simpl. -specialize (H0 x); specialize (H1 x); specialize (H2 x). -destruct (l x)... -destruct H. -constructor. -unfold state_of_stack. -constructor. -eapply prefix_ass... -unfold state_stack_of_stack; simpl; constructor. -intro; destruct (singleton_state_pred s0 x0)... -eapply prefix_pred_ass... -constructor... -constructor... -apply reduce_step_stack_invariant_conserved... -Qed. - -(** If the automaton is safe, then it does not crash **) -Theorem parse_no_err buffer n_steps: - parse init buffer n_steps <> Err. -Proof with eauto. -unfold parse. -assert (stack_invariant []). -constructor. -constructor. -unfold state_stack_of_stack; simpl; constructor. -intro; destruct (singleton_state_pred init x)... -constructor. -constructor. -revert H. -generalize buffer ([]:stack). -induction n_steps; simpl. -now discriminate. -intros. -pose proof (step_stack_invariant_conserved s buffer0 H). -destruct (step init s buffer0) as [|[]]; simpl... -discriminate. -discriminate. -Qed. - -(** A version of [parse] that uses safeness in order to return a - [parse_result], and not a [result parse_result] : we have proven that - parsing does not return [Err]. **) -Definition parse_with_safe (buffer:Stream token) (n_steps:nat): - parse_result init. -Proof with eauto. -pose proof (parse_no_err buffer n_steps). -destruct (parse init buffer n_steps)... -congruence. -Defined. - -End Safety_proof. - -End Make. diff --git a/cparser/validator/Main.v b/cparser/validator/Main.v deleted file mode 100644 index 1a17e988..00000000 --- a/cparser/validator/Main.v +++ /dev/null @@ -1,92 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Grammar. -Require Automaton. -Require Interpreter_safe. -Require Interpreter_correct. -Require Interpreter_complete. -Require Import Syntax. - -Module Make(Export Aut:Automaton.T). -Export Aut.Gram. -Export Aut.GramDefs. - -Module Import Inter := Interpreter.Make Aut. -Module Safe := Interpreter_safe.Make Aut Inter. -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 := Safe.Valid.is_safe. -Definition parse (safe:safe_validator ()=true) init n_steps buffer : parse_result init:= - Safe.parse_with_safe (Safe.Valid.is_safe_correct safe) init buffer n_steps. - -(** Correction theorem. **) -Theorem parse_correct - (safe:safe_validator ()= true) init n_steps buffer: - match parse safe init n_steps buffer with - | Parsed_pr sem buffer_new => - exists word, - buffer = word ++ buffer_new /\ inhabited (parse_tree (NT (start_nt init)) word sem) - | _ => True - end. -Proof. -unfold parse, Safe.parse_with_safe. -pose proof (Correct.parse_correct init buffer n_steps). -generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init buffer n_steps). -destruct (Inter.parse init buffer n_steps); intros. -now destruct (n (eq_refl _)). -now destruct p; trivial. -Qed. - -(** Completeness theorem. **) -Theorem parse_complete - (safe:safe_validator () = true) init n_steps word buffer_end sem: - complete_validator () = true -> - forall tree:parse_tree (NT (start_nt init)) word sem, - match parse safe init n_steps (word ++ buffer_end) with - | Fail_pr => False - | Parsed_pr sem_res buffer_end_res => - sem_res = sem /\ buffer_end_res = buffer_end /\ pt_size tree <= n_steps - | Timeout_pr => n_steps < pt_size tree - end. -Proof. -intros. -unfold parse, Safe.parse_with_safe. -pose proof (Complete.parse_complete (Complete.Valid.is_complete_correct H) init _ buffer_end _ tree n_steps). -generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init (word ++ buffer_end) n_steps). -destruct (Inter.parse init (word ++ buffer_end) n_steps); intros. -now destruct (n eq_refl). -now exact H0. -Qed. - -(** Unambiguity theorem. **) -Theorem unambiguity: - safe_validator () = true -> complete_validator () = true -> inhabited token -> - forall init word, - forall sem1 (tree1:parse_tree (NT (start_nt init)) word sem1), - forall sem2 (tree2:parse_tree (NT (start_nt init)) word sem2), - sem1 = sem2. -Proof. -intros. -destruct H1. -pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem1) H0 tree1. -pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem2) H0 tree2. -destruct (parse H init (pt_size tree1) (word ++ Streams.const X)); intuition. -rewrite <- H3, H1; reflexivity. -Qed. - -End Make. diff --git a/cparser/validator/Tuples.v b/cparser/validator/Tuples.v deleted file mode 100644 index 3fd2ec03..00000000 --- a/cparser/validator/Tuples.v +++ /dev/null @@ -1,49 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import List. -Require Import Coq.Program.Syntax. -Require Import Equality. - -(** A curryfied function with multiple parameters **) -Definition arrows_left: list Type -> Type -> Type := - fold_left (fun A B => B -> A). - -(** A curryfied function with multiple parameters **) -Definition arrows_right: Type -> list Type -> Type := - fold_right (fun A B => A -> B). - -(** A tuple is a heterogeneous list. For convenience, we use pairs. **) -Fixpoint tuple (types : list Type) : Type := - match types with - | nil => unit - | t::q => prod t (tuple q) - end. - -Fixpoint uncurry {args:list Type} {res:Type}: - arrows_left args res -> tuple args -> res := - match args return forall res, arrows_left args res -> tuple args -> res with - | [] => fun _ f _ => f - | t::q => fun res f p => let (d, t) := p in - (@uncurry q _ f t) d - end res. - -Lemma JMeq_eqrect: - forall (U:Type) (a b:U) (P:U -> Type) (x:P a) (e:a=b), - eq_rect a P x b e ~= x. -Proof. -destruct e. -reflexivity. -Qed. diff --git a/cparser/validator/Validator_complete.v b/cparser/validator/Validator_complete.v deleted file mode 100644 index a9823278..00000000 --- a/cparser/validator/Validator_complete.v +++ /dev/null @@ -1,542 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Automaton. -Require Import Alphabet. -Require Import List. -Require Import Syntax. - -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). - -(** 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. - -Lemma forallb_items_spec : - forall p, forallb_items (items_map ()) p = true -> - forall st prod fut lookahead, state_has_future st prod fut lookahead -> - forall P:state -> production -> list symbol -> terminal -> Prop, - (forall st prod pos set lookahead, - TerminalSet.In lookahead set -> p st prod pos set = true -> - P st prod (future_of_prod prod pos) lookahead) -> - P st prod fut lookahead. -Proof. -intros. -unfold forallb_items in H. -rewrite StateProdPosMap.fold_1 in H. -destruct H0; destruct H0. -specialize (H1 st prod x _ _ H2). -destruct H0. -apply H1. -unfold find_items_map in *. -pose proof (@StateProdPosMap.find_2 _ (items_map ()) (st, prod, x)). -destruct (StateProdPosMap.find (st, prod, x) (items_map ())); [ |destruct (TerminalSet.empty_1 H2)]. -specialize (H0 _ (eq_refl _)). -pose proof (StateProdPosMap.elements_1 H0). -revert H. -generalize true at 1. -induction H3. -destruct H. -destruct y. -simpl in H3; destruct H3. -pose proof (compare_eq (st, prod, x) k H). -destruct H3. -simpl. -generalize (p st prod x t). -induction l; simpl; intros. -rewrite Bool.andb_true_iff in H3. -intuition. -destruct a; destruct k; destruct p0. -simpl in H3. -replace (b0 && b && p s p0 n t0)%bool with (b0 && p s p0 n t0 && b)%bool in H3. -apply (IHl _ _ H3). -destruct b, b0, (p s p0 n t0); reflexivity. -intro. -apply IHInA. -Qed. - -(** * Validation for completeness **) - -(** The nullable predicate is a fixpoint : it is correct. **) -Definition nullable_stable:= - forall p:production, - nullable_word (rev (prod_rhs_rev p)) = true -> - nullable_nterm (prod_lhs p) = true. - -Definition is_nullable_stable (_:unit) := - forallb (fun p:production => - implb (nullable_word (rev' (prod_rhs_rev p))) (nullable_nterm (prod_lhs p))) - all_list. - -Property is_nullable_stable_correct : - is_nullable_stable () = true -> nullable_stable. -Proof. -unfold is_nullable_stable, nullable_stable. -intros. -rewrite forallb_forall in H. -specialize (H p (all_list_forall p)). -unfold rev' in H; rewrite <- rev_alt in H. -rewrite H0 in H; intuition. -Qed. - -(** 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)). - -Definition is_first_stable (_:unit) := - forallb (fun p:production => - TerminalSet.subset (first_word_set (rev' (prod_rhs_rev p))) - (first_nterm_set (prod_lhs p))) - all_list. - -Property is_first_stable_correct : - is_first_stable () = true -> first_stable. -Proof. -unfold is_first_stable, first_stable. -intros. -rewrite forallb_forall in H. -specialize (H p (all_list_forall p)). -unfold rev' in H; rewrite <- rev_alt in H. -apply TerminalSet.subset_2; intuition. -Qed. - -(** The initial state has all the S=>.u items, where S is the start non-terminal **) -Definition start_future := - forall (init:initstate) (t:terminal) (p:production), - prod_lhs p = start_nt init -> - state_has_future init p (rev (prod_rhs_rev p)) t. - -Definition is_start_future items_map := - forallb (fun init => - forallb (fun prod => - if compare_eqb (prod_lhs prod) (start_nt init) then - let lookaheads := find_items_map items_map init prod 0 in - forallb (fun t => TerminalSet.mem t lookaheads) all_list - else - true) all_list) all_list. - -Property is_start_future_correct : - is_start_future (items_map ()) = true -> start_future. -Proof. -unfold is_start_future, start_future. -intros. -rewrite forallb_forall in H. -specialize (H init (all_list_forall _)). -rewrite forallb_forall in H. -specialize (H p (all_list_forall _)). -rewrite <- compare_eqb_iff in H0. -rewrite H0 in H. -rewrite forallb_forall in H. -specialize (H t (all_list_forall _)). -exists 0. -split. -apply rev_alt. -apply TerminalSet.mem_2; eauto. -Qed. - -(** 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. - -Definition is_terminal_shift items_map := - forallb_items items_map (fun s1 prod pos lset => - match future_of_prod prod pos with - | T t::_ => - match action_table s1 with - | Lookahead_act awp => - match awp t with - | Shift_act s2 _ => - TerminalSet.subset lset (find_items_map items_map s2 prod (S pos)) - | _ => false - end - | _ => false - end - | _ => true - end). - -Property is_terminal_shift_correct : - is_terminal_shift (items_map ()) = true -> terminal_shift. -Proof. -unfold is_terminal_shift, terminal_shift. -intros. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ fut look => _)). -intros. -destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition. -destruct (action_table st); intuition. -destruct (l0 t); intuition. -exists (S pos). -split. -unfold future_of_prod in *. -rewrite Heql; reflexivity. -apply (TerminalSet.subset_2 H2); intuition. -Qed. - -(** 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 -> - fut = [] -> - 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. - -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). - -Property is_end_reduce_correct : - is_end_reduce (items_map ()) = true -> end_reduce. -Proof. -unfold is_end_reduce, end_reduce. -intros. -revert H1. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => _ -> - match action_table st with - | Default_reduce_act p => p = prod - | _ => _ - end)). -intros. -rewrite H3 in H2. -destruct (action_table st); intuition. -apply compare_eqb_iff; intuition. -rewrite TerminalSet.fold_1 in H2. -revert H2. -generalize true at 1. -pose proof (TerminalSet.elements_1 H1). -induction H2. -pose proof (compare_eq _ _ H2). -destruct H4. -simpl. -assert (fold_left - (fun (a : bool) (e : TerminalSet.elt) => - match l e with - | Shift_act _ _ => false - | Reduce_act p => (a && compare_eqb p prod0)%bool - | Fail_act => false - end) l0 false = true -> False). -induction l0; intuition. -apply IHl0. -simpl in H4. -destruct (l a); intuition. -destruct (l lookahead0); intuition. -apply compare_eqb_iff. -destruct (compare_eqb p prod0); intuition. -destruct b; intuition. -simpl; intros. -eapply IHInA; eauto. -Qed. - -(** 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 => - forall prod fut lookahead, - state_has_future s1 prod fut lookahead -> - match fut with - | NT nt'::_ => nt <> nt' - | _ => True - end - end - | _ => True - end. - -Definition is_non_terminal_goto items_map := - forallb_items items_map (fun s1 prod pos lset => - match future_of_prod prod pos with - | NT nt::_ => - match goto_table s1 nt with - | Some (exist _ s2 _) => - TerminalSet.subset lset (find_items_map items_map s2 prod (S pos)) - | None => forallb_items items_map (fun s1' prod' pos' _ => - (implb (compare_eqb s1 s1') - match future_of_prod prod' pos' with - | NT nt' :: _ => negb (compare_eqb nt nt') - | _ => true - end)%bool) - end - | _ => true - end). - -Property is_non_terminal_goto_correct : - is_non_terminal_goto (items_map ()) = true -> non_terminal_goto. -Proof. -unfold is_non_terminal_goto, non_terminal_goto. -intros. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => - match fut with - | NT nt :: q => - match goto_table st nt with - | Some _ => _ - | None => - forall p f l, state_has_future st p f l -> (_:Prop) - end - | _ => _ - end)). -intros. -destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition. -destruct (goto_table st n) as [[]|]. -exists (S pos). -split. -unfold future_of_prod in *. -rewrite Heql; reflexivity. -apply (TerminalSet.subset_2 H2); intuition. -intros. -remember st in H2; revert Heqs. -apply (forallb_items_spec _ H2 _ _ _ _ H3 (fun st' prod fut look => s = st' -> match fut return Prop with [] => _ | _ => _ end)); intros. -rewrite <- compare_eqb_iff in H6; rewrite H6 in H5. -destruct (future_of_prod prod1 pos0) as [|[]]; intuition. -rewrite <- compare_eqb_iff in H7; rewrite H7 in H5. -discriminate. -Qed. - -Definition start_goto := - forall (init:initstate), goto_table init (start_nt init) = None. - -Definition is_start_goto (_:unit) := - forallb (fun (init:initstate) => - match goto_table init (start_nt init) with - | Some _ => false - | None => true - end) all_list. - -Definition is_start_goto_correct: - is_start_goto () = true -> start_goto. -Proof. -unfold is_start_goto, start_goto. -rewrite forallb_forall. -intros. -specialize (H init (all_list_forall _)). -destruct (goto_table init (start_nt init)); congruence. -Qed. - -(** 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:state) prod fut lookahead, - state_has_future s1 prod fut lookahead -> - match fut with - | NT nt::q => - forall (p:production) (lookahead2:terminal), - prod_lhs p = nt -> - TerminalSet.In lookahead2 (first_word_set q) \/ - lookahead2 = lookahead /\ nullable_word q = true -> - state_has_future s1 p (rev (prod_rhs_rev p)) lookahead2 - | _ => True - end. - -Definition is_non_terminal_closed items_map := - forallb_items items_map (fun s1 prod pos lset => - match future_of_prod prod pos with - | NT nt::q => - forallb (fun p => - if compare_eqb (prod_lhs p) nt then - let lookaheads := find_items_map items_map s1 p 0 in - (implb (nullable_word q) (TerminalSet.subset lset lookaheads)) && - TerminalSet.subset (first_word_set q) lookaheads - else true - )%bool all_list - | _ => true - end). - -Property is_non_terminal_closed_correct: - is_non_terminal_closed (items_map ()) = true -> non_terminal_closed. -Proof. -unfold is_non_terminal_closed, non_terminal_closed. -intros. -apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look => - match fut with - | NT nt :: q => forall p l, _ -> _ -> state_has_future st _ _ _ - | _ => _ - end)). -intros. -destruct (future_of_prod prod0 pos); intuition. -destruct s; eauto; intros. -rewrite forallb_forall in H2. -specialize (H2 p (all_list_forall p)). -rewrite <- compare_eqb_iff in H3. -rewrite H3 in H2. -rewrite Bool.andb_true_iff in H2. -destruct H2. -exists 0. -split. -apply rev_alt. -destruct H4 as [|[]]; subst. -apply (TerminalSet.subset_2 H5); intuition. -rewrite H6 in H2. -apply (TerminalSet.subset_2 H2); intuition. -Qed. - -(** The automaton is complete **) -Definition complete := - nullable_stable /\ first_stable /\ start_future /\ terminal_shift - /\ end_reduce /\ non_terminal_goto /\ start_goto /\ non_terminal_closed. - -Definition is_complete (_:unit) := - let items_map := items_map () in - (is_nullable_stable () && is_first_stable () && is_start_future items_map && - is_terminal_shift items_map && is_end_reduce items_map && is_start_goto () && - is_non_terminal_goto items_map && is_non_terminal_closed items_map)%bool. - -Property is_complete_correct: - is_complete () = true -> complete. -Proof. -unfold is_complete, complete. -repeat rewrite Bool.andb_true_iff. -intuition. -apply is_nullable_stable_correct; assumption. -apply is_first_stable_correct; assumption. -apply is_start_future_correct; assumption. -apply is_terminal_shift_correct; assumption. -apply is_end_reduce_correct; assumption. -apply is_non_terminal_goto_correct; assumption. -apply is_start_goto_correct; assumption. -apply is_non_terminal_closed_correct; assumption. -Qed. - -End Make. diff --git a/cparser/validator/Validator_safe.v b/cparser/validator/Validator_safe.v deleted file mode 100644 index 183d661b..00000000 --- a/cparser/validator/Validator_safe.v +++ /dev/null @@ -1,414 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Automaton. -Require Import Alphabet. -Require Import List. -Require Import Syntax. - -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). - -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. - -Property is_prefix_correct (l1 l2:list symbol): - is_prefix l1 l2 = true -> prefix l1 l2. -Proof. -revert l2. -induction l1; intros. -apply prefix_nil. -unfold is_prefix in H. -destruct l2; intuition; try discriminate. -rewrite Bool.andb_true_iff in H. -destruct H. -rewrite compare_eqb_iff in H. -destruct H. -apply prefix_cons. -apply IHl1; intuition. -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. - -Definition is_shift_head_symbs (_:unit) := - forallb (fun s:state => - match action_table s with - | Lookahead_act awp => - forallb (fun t => - match awp t with - | Shift_act s2 _ => - is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) - | _ => true - end) - all_list - | _ => true - end) - all_list. - -Property is_shift_head_symbs_correct: - is_shift_head_symbs () = true -> shift_head_symbs. -Proof. -unfold is_shift_head_symbs, shift_head_symbs. -intros. -rewrite forallb_forall in H. -specialize (H s (all_list_forall s)). -destruct (action_table s); intuition. -rewrite forallb_forall in H. -specialize (H t (all_list_forall t)). -destruct (l t); intuition. -apply is_prefix_correct; intuition. -Qed. - -(** 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. - -Definition is_goto_head_symbs (_:unit) := - forallb (fun s:state => - forallb (fun nt => - match goto_table s nt with - | Some (exist _ s2 _) => - is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s) - | None => true - end) - all_list) - all_list. - -Property is_goto_head_symbs_correct: - is_goto_head_symbs () = true -> goto_head_symbs. -Proof. -unfold is_goto_head_symbs, goto_head_symbs. -intros. -rewrite forallb_forall in H. -specialize (H s (all_list_forall s)). -rewrite forallb_forall in H. -specialize (H nt (all_list_forall nt)). -destruct (goto_table s nt); intuition. -destruct s0. -apply is_prefix_correct; intuition. -Qed. - -(** 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). - -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. - -Property is_prefix_pred_correct (l1 l2:list (state->bool)) : - is_prefix_pred l1 l2 = true -> prefix_pred l1 l2. -Proof. -revert l2. -induction l1. -intros. -apply prefix_pred_nil. -intros. -destruct l2; intuition; try discriminate. -unfold is_prefix_pred in H. -rewrite Bool.andb_true_iff in H. -rewrite forallb_forall in H. -apply prefix_pred_cons; intuition. -apply H0. -apply 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. - -Definition is_shift_past_state (_:unit) := - forallb (fun s:state => - match action_table s with - | Lookahead_act awp => - forallb (fun t => - match awp t with - | Shift_act s2 _ => - is_prefix_pred - (past_state_of_non_init_state s2) (head_states_of_state s) - | _ => true - end) - all_list - | _ => true - end) - all_list. - -Property is_shift_past_state_correct: - is_shift_past_state () = true -> shift_past_state. -Proof. -unfold is_shift_past_state, shift_past_state. -intros. -rewrite forallb_forall in H. -specialize (H s (all_list_forall s)). -destruct (action_table s); intuition. -rewrite forallb_forall in H. -specialize (H t (all_list_forall t)). -destruct (l t); intuition. -apply is_prefix_pred_correct; intuition. -Qed. - -(** 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. - -Definition is_goto_past_state (_:unit) := - forallb (fun s:state => - forallb (fun nt => - match goto_table s nt with - | Some (exist _ s2 _) => - is_prefix_pred - (past_state_of_non_init_state s2) (head_states_of_state s) - | None => true - end) - all_list) - all_list. - -Property is_goto_past_state_correct : - is_goto_past_state () = true -> goto_past_state. -Proof. -unfold is_goto_past_state, goto_past_state. -intros. -rewrite forallb_forall in H. -specialize (H s (all_list_forall s)). -rewrite forallb_forall in H. -specialize (H nt (all_list_forall nt)). -destruct (goto_table s nt); intuition. -destruct s0. -apply is_prefix_pred_correct; intuition. -Qed. - -(** 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. - -Property is_state_valid_after_pop_complete state sl pl : - state_valid_after_pop state sl pl -> is_state_valid_after_pop state sl pl = true. -Proof. -intro. -induction H; intuition. -destruct sl; intuition. -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) -> - goto_table state_new (prod_lhs prod) = None -> - match state_new with - | Init i => prod_lhs prod = start_nt i - | Ninit _ => False - end. - -Definition is_valid_for_reduce (state:state) prod:= - (is_prefix (prod_rhs_rev prod) (head_symbs_of_state state) && - forallb (fun state_new => - if is_state_valid_after_pop state_new (prod_rhs_rev prod) - (head_states_of_state state) then - match goto_table state_new (prod_lhs prod) with - | Some _ => true - | None => - match state_new with - | Init i => compare_eqb (prod_lhs prod) (start_nt i) - | Ninit _ => false - end - end - else - true) - all_list)%bool. - -Property is_valid_for_reduce_correct (state:state) prod: - is_valid_for_reduce state prod = true -> valid_for_reduce state prod. -Proof. -unfold is_valid_for_reduce, valid_for_reduce. -intros. -rewrite Bool.andb_true_iff in H. -split. -apply is_prefix_correct. -intuition. -intros. -rewrite forallb_forall in H. -destruct H. -specialize (H2 state_new (all_list_forall state_new)). -rewrite is_state_valid_after_pop_complete, H1 in H2. -destruct state_new; intuition. -rewrite compare_eqb_iff in H2; intuition. -intuition. -Qed. - -(** 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. - -Definition is_reduce_ok (_:unit) := - forallb (fun s => - match action_table s with - | Lookahead_act awp => - forallb (fun t => - match awp t with - | Reduce_act p => is_valid_for_reduce s p - | _ => true - end) - all_list - | Default_reduce_act p => is_valid_for_reduce s p - end) - all_list. - -Property is_reduce_ok_correct : - is_reduce_ok () = true -> reduce_ok. -Proof. -unfold is_reduce_ok, reduce_ok. -intros. -rewrite forallb_forall in H. -specialize (H s (all_list_forall s)). -destruct (action_table s). -apply is_valid_for_reduce_correct; intuition. -intro. -rewrite forallb_forall in H. -specialize (H t (all_list_forall t)). -destruct (l t); intuition. -apply is_valid_for_reduce_correct; intuition. -Qed. - -(** The automaton is safe **) -Definition safe := - shift_head_symbs /\ goto_head_symbs /\ shift_past_state /\ - goto_past_state /\ reduce_ok. - -Definition is_safe (_:unit) := - (is_shift_head_symbs () && is_goto_head_symbs () && is_shift_past_state () && - is_goto_past_state () && is_reduce_ok ())%bool. - -Property is_safe_correct: - is_safe () = true -> safe. -Proof. -unfold safe, is_safe. -repeat rewrite Bool.andb_true_iff. -intuition. -apply is_shift_head_symbs_correct; assumption. -apply is_goto_head_symbs_correct; assumption. -apply is_shift_past_state_correct; assumption. -apply is_goto_past_state_correct; assumption. -apply is_reduce_ok_correct; assumption. -Qed. - -End Make. -- cgit