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.