Library compcert.cparser.validator.Validator_complete
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.
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.
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.
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)).
(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).
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).
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.