diff options
Diffstat (limited to 'cparser/MenhirLib/Validator_complete.v')
| -rw-r--r-- | cparser/MenhirLib/Validator_complete.v | 542 |
1 files changed, 0 insertions, 542 deletions
diff --git a/cparser/MenhirLib/Validator_complete.v b/cparser/MenhirLib/Validator_complete.v deleted file mode 100644 index a9823278..00000000 --- a/cparser/MenhirLib/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. |