diff options
Diffstat (limited to 'cparser/validator/Validator_complete.v')
| -rw-r--r-- | cparser/validator/Validator_complete.v | 525 |
1 files changed, 525 insertions, 0 deletions
diff --git a/cparser/validator/Validator_complete.v b/cparser/validator/Validator_complete.v new file mode 100644 index 0000000..9855930 --- /dev/null +++ b/cparser/validator/Validator_complete.v @@ -0,0 +1,525 @@ +(* *********************************************************************) +(* *) +(* 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 _ _ _ _ => _)). +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 _ _ _ _ => _)). +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 _ _ _ _ => _)). +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 _ _ _ _ => _)); intros. +rewrite <- compare_eqb_iff in Heqs; rewrite Heqs in H5. +destruct (future_of_prod prod2 pos0) as [|[]]; intuition. +rewrite <- compare_eqb_iff in H6; rewrite H6 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 _ _ _ _ => _)). +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. |