Commit ec31fb4f authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Safety is now proved on-the-fly in the interpreter with dependent types....

Safety is now proved on-the-fly in the interpreter with dependent types. parse_tree_lists are now reversed.
parent f0842e17
......@@ -78,13 +78,13 @@ Module Type T.
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.
(* The RHS of a production is given in reversed order, so that symbols *)
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))).
arrows_right
(symbol_semantic_type (NT (prod_lhs p)))
(map symbol_semantic_type (prod_rhs_rev p)).
End T.
Module Defs(Import G:T).
......@@ -92,71 +92,67 @@ 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. **)
(** The semantics of a grammar is defined in two stages. First, we
define the notion of parse tree, which represents one way of
recognizing a word with a head symbol. Semantic values are stored
at the leaves.
This notion is defined in two mutually recursive flavours:
either for a single head symbol, or for a list of head symbols. *)
Inductive parse_tree:
forall (head_symbol:symbol) (word:list token)
(semantic_value:symbol_semantic_type head_symbol), Type :=
forall (head_symbol:symbol) (word:list token), Type :=
(** A single token has its semantic value as semantic value, for the
corresponding terminal as head symbol. **)
(** Parse tree for a terminal 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
parse_tree (T t) [existT (fun t => symbol_semantic_type (T t)) t 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.**)
(** Parse tree for a non-terminal 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 **)
forall (prod:production) {word:list token},
parse_tree_list (prod_rhs_rev prod) word ->
parse_tree (NT (prod_lhs prod)) word
(* Note : the list head_symbols_rev is reversed. *)
with parse_tree_list:
forall (head_symbols:list symbol) (word:list token)
(semantic_values:tuple (map symbol_semantic_type head_symbols)),
Type :=
forall (head_symbols_rev:list symbol) (word:list token), Type :=
(** The empty word has [()] as semantic for [[]] as head symbols list **)
| Nil_ptl: parse_tree_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 ->
forall {head_symbolsq:list symbol} {wordq:list token},
parse_tree_list head_symbolsq wordq ->
(** 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 ->
forall {head_symbolt:symbol} {wordt:list token},
parse_tree head_symbolt wordt ->
(** give the semantic of the cons **)
parse_tree_list
(head_symbolt::head_symbolsq)
(wordt++wordq)
(semantic_valuet, semantic_valuesq).
parse_tree_list (head_symbolt::head_symbolsq) (wordq++wordt).
(** We can now finish the definition of the semantics of a grammar,
by giving the semantic value assotiated with a parse tree. *)
Fixpoint pt_sem {head_symbol word} (tree:parse_tree head_symbol word) :
symbol_semantic_type head_symbol :=
match tree with
| Terminal_pt _ sem => sem
| Non_terminal_pt prod ptl => ptl_sem ptl (prod_action prod)
end
with ptl_sem {A head_symbols word} (tree:parse_tree_list head_symbols word) :
arrows_right A (map symbol_semantic_type head_symbols) -> A :=
match tree with
| Nil_ptl => fun act => act
| Cons_ptl q t => fun act => ptl_sem q (act (pt_sem t))
end.
Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) :=
Fixpoint pt_size {head_symbol word} (tree:parse_tree head_symbol word) :=
match tree with
| Terminal_pt _ _ => 1
| Non_terminal_pt l => S (ptl_size l)
| Non_terminal_pt _ l => S (ptl_size l)
end
with ptl_size {head_symbols word sems} (tree:parse_tree_list head_symbols word sems) :=
with ptl_size {head_symbols word} (tree:parse_tree_list head_symbols word) :=
match tree with
| Nil_ptl => 0
| Cons_ptl t q =>
| Cons_ptl q t =>
pt_size t + ptl_size q
end.
End Defs.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(* *********************************************************************)
(* *)
(* Menhir *)
(* *)
(* 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 Lesser General Public License as *)
(* published by the Free Software Foundation, either version 3 of *)
(* the License, or (at your option) any later version. *)
(* *)
(* *********************************************************************)
From Coq Require Import Streams Equality List Syntax.
From MenhirLib Require Import Alphabet.
From MenhirLib Require Grammar Automaton Validator_safe 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.
......@@ -12,8 +12,7 @@
(* *)
(* *********************************************************************)
From MenhirLib Require Grammar Automaton Interpreter_safe
Interpreter_correct Interpreter_complete.
From MenhirLib Require Grammar Automaton Interpreter_correct Interpreter_complete.
From Coq Require Import Syntax.
Module Make(Export Aut:Automaton.T).
......@@ -21,68 +20,55 @@ 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 safe_validator:unit->bool := ValidSafe.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.
parse (ValidSafe.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)
exists word (pt : parse_tree (NT (start_nt init)) word),
buffer = word ++ buffer_new /\
pt_sem pt = 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.
Proof. apply Correct.parse_correct. Qed.
(** Completeness theorem. **)
Theorem parse_complete
(safe:safe_validator () = true) init n_steps word buffer_end sem:
(safe:safe_validator () = true) init n_steps word buffer_end:
complete_validator () = true ->
forall tree:parse_tree (NT (start_nt init)) word sem,
forall tree:parse_tree (NT (start_nt init)) word,
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
| Fail_pr => False
| Parsed_pr sem_res buffer_end_res =>
sem_res = pt_sem tree /\ 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.
intros. now apply Complete.parse_complete, Complete.Valid.is_complete_correct.
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.
forall (tree1 tree2:parse_tree (NT (start_nt init)) word),
pt_sem tree1 = pt_sem tree2.
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.
intros Hsafe Hcomp [tok] init word tree1 tree2.
assert (Hcomp1 := parse_complete Hsafe init (pt_size tree1) word (Streams.const tok)
Hcomp tree1).
assert (Hcomp2 := parse_complete Hsafe init (pt_size tree1) word (Streams.const tok)
Hcomp tree2).
destruct parse; auto with exfalso zarith.
destruct Hcomp1 as [-> _], Hcomp2 as [-> _]. reflexivity.
Qed.
End Make.
......@@ -37,6 +37,13 @@ Fixpoint uncurry {args:list Type} {res:Type}:
(@uncurry q _ f t) d
end res.
Lemma arrows_left_right_map_rev_append A B l1 l2 (f : B -> Type) :
arrows_left (map f (rev_append l1 l2)) A =
arrows_left (map f l2) (arrows_right A (map f l1)).
Proof.
revert l2. induction l1 as [|C l1 IH]; intros l2; [|simpl; rewrite IH]; reflexivity.
Qed.
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.
......
......@@ -61,8 +61,8 @@ Fixpoint first_word_set (word:list symbol) :=
| t::q =>
if nullable_symb t then
TerminalSet.union (first_symb_set t) (first_word_set q)
else
first_symb_set t
else
first_symb_set t
end.
(** Small helper for finding the part of an item that is after the dot. **)
......@@ -157,29 +157,28 @@ Qed.
(** The nullable predicate is a fixpoint : it is correct. **)
Definition nullable_stable:=
forall p:production,
nullable_word (rev (prod_rhs_rev p)) = true ->
nullable_word (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)))
implb (nullable_word (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.
unfold is_nullable_stable, nullable_stable.
intros.
rewrite forallb_forall in H.
specialize (H p (all_list_forall p)).
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)))
TerminalSet.Subset (first_word_set (rev' (prod_rhs_rev p)))
(first_nterm_set (prod_lhs p)).
Definition is_first_stable (_:unit) :=
......@@ -191,19 +190,18 @@ Definition is_first_stable (_:unit) :=
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.
unfold is_first_stable, first_stable.
intros.
rewrite forallb_forall in H.
specialize (H p (all_list_forall p)).
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.
state_has_future init p (rev' (prod_rhs_rev p)) t.
Definition is_start_future items_map :=
forallb (fun init =>
......@@ -217,20 +215,18 @@ Definition is_start_future items_map :=
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.
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; [now trivial|].
apply TerminalSet.mem_2; eauto.
Qed.
(** If a state contains an item of the form A->_.av[[b]], where a is a
......@@ -372,13 +368,7 @@ Definition non_terminal_goto :=
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
| None => False
end
| _ => True
end.
......@@ -390,12 +380,7 @@ Definition is_non_terminal_goto items_map :=
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)
| None => false
end
| _ => true
end).
......@@ -410,26 +395,18 @@ apply (forallb_items_spec _ H _ _ _ _ H0 (fun st prod fut look =>
| NT nt :: q =>
match goto_table st nt with
| Some _ => _
| None =>
forall p f l, state_has_future st p f l -> (_:Prop)
| None => False
end
| _ => _
end)).
intros.
destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition.
destruct (goto_table st n) as [[]|].
destruct (goto_table st n) as [[]|]; [|congruence].
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 :=
......@@ -464,7 +441,7 @@ Definition non_terminal_closed :=
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
state_has_future s1 p (rev' (prod_rhs_rev p)) lookahead2
| _ => True
end.
......@@ -485,29 +462,28 @@ Definition is_non_terminal_closed items_map :=
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)).