aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
Diffstat (limited to 'cparser')
-rw-r--r--cparser/validator/Alphabet.v35
-rw-r--r--cparser/validator/Grammar.v7
-rw-r--r--cparser/validator/Interpreter.v28
-rw-r--r--cparser/validator/Interpreter_complete.v58
-rw-r--r--cparser/validator/Interpreter_correct.v4
-rw-r--r--cparser/validator/Interpreter_safe.v12
-rw-r--r--cparser/validator/Validator_complete.v35
-rw-r--r--cparser/validator/Validator_safe.v8
8 files changed, 106 insertions, 81 deletions
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v
index db850860..2d7f8ff9 100644
--- a/cparser/validator/Alphabet.v
+++ b/cparser/validator/Alphabet.v
@@ -199,7 +199,7 @@ Next Obligation. apply Zcompare_antisym. Qed.
Next Obligation.
destruct c. unfold compare31 in *.
rewrite Z.compare_eq_iff in *. congruence.
-eapply Zcompare_Lt_trans. apply H. apply H0.
+eapply Zcompare_Lt_trans. apply H. apply H0.
eapply Zcompare_Gt_trans. apply H. apply H0.
Qed.
Next Obligation.
@@ -214,28 +214,27 @@ pose proof (inj_bound_spec x).
match goal with |- In x (fst ?p) => destruct p as [] eqn:? end.
replace inj_bound with i in H.
revert l i Heqp x H.
-apply iter_nat_invariant; intros.
+induction (Z.abs_nat (phi inj_bound)); intros.
inversion Heqp; clear Heqp; subst.
-destruct x; specialize (H _ _ (eq_refl _) x0); simpl in *.
-rewrite phi_incr in H0.
-pose proof (phi_bounded i).
-pose proof (phi_bounded (inj x0)).
-destruct (Z_lt_le_dec (Zsucc (phi i)) (2 ^ Z_of_nat size)%Z).
-rewrite Zmod_small in H0 by omega.
-apply Zlt_succ_le, Zle_lt_or_eq in H0.
-destruct H0; eauto.
-left.
-rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; reflexivity.
-replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega.
-rewrite Z_mod_same_full in H0.
+rewrite spec_0 in H. pose proof (phi_bounded (inj x)). omega.
+simpl in Heqp.
+destruct nat_rect; specialize (IHn _ _ (eq_refl _) x); simpl in *.
+inversion Heqp. subst. clear Heqp.
+rewrite phi_incr in H.
+pose proof (phi_bounded i0).
+pose proof (phi_bounded (inj x)).
+destruct (Z_lt_le_dec (Zsucc (phi i0)) (2 ^ Z_of_nat size)%Z).
+rewrite Zmod_small in H by omega.
+apply Zlt_succ_le, Zle_lt_or_eq in H.
+destruct H; simpl; auto. left.
+rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x), H, phi_inv_phi; reflexivity.
+replace (Zsucc (phi i0)) with (2 ^ Z_of_nat size)%Z in H by omega.
+rewrite Z_mod_same_full in H.
exfalso; omega.
-exfalso; inversion Heqp; subst;
- pose proof (phi_bounded (inj x)); change (phi 0) with 0%Z in H; omega.
-clear H.
rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal.
pose proof (phi_bounded inj_bound); pose proof (phi_bounded i).
rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega.
-clear H H0.
+clear H H0 H1.
do 2 rewrite <- inj_Zabs_nat.
f_equal.
revert l i Heqp.
diff --git a/cparser/validator/Grammar.v b/cparser/validator/Grammar.v
index 0768d647..8e427cd9 100644
--- a/cparser/validator/Grammar.v
+++ b/cparser/validator/Grammar.v
@@ -17,6 +17,7 @@ Require Import List.
Require Import Syntax.
Require Import Alphabet.
Require Import Orders.
+Require Tuples.
(** The terminal non-terminal alphabets of the grammar. **)
Module Type Alphs.
@@ -65,7 +66,7 @@ Module Symbol(Import A:Alphs).
End Symbol.
Module Type T.
- Require Export Tuples.
+ Export Tuples.
Include Alphs <+ Symbol.
@@ -154,12 +155,12 @@ Module Defs(Import G:T).
Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) :=
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) :=
match tree with
| Nil_ptl => 0
- | Cons_ptl _ _ _ t _ _ _ q =>
+ | Cons_ptl t q =>
pt_size t + ptl_size q
end.
End Defs.
diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v
index 2242065c..a24362f8 100644
--- a/cparser/validator/Interpreter.v
+++ b/cparser/validator/Interpreter.v
@@ -87,7 +87,7 @@ Variable init : initstate.
Definition state_of_stack (stack:stack): state :=
match stack with
| [] => init
- | existT s _::_ => s
+ | existT _ s _::_ => s
end.
(** [pop] pops some symbols from the stack. It returns the popped semantic
@@ -96,15 +96,15 @@ Definition state_of_stack (stack:stack): state :=
Fixpoint pop (symbols_to_pop:list symbol) (stack_cur:stack):
forall {A:Type} (action:arrows_right A (map symbol_semantic_type symbols_to_pop)),
result (stack * A) :=
- match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), _ with
+ match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), result (stack * A) with
| [] => fun A action => OK (stack_cur, action)
| t::q => fun A action =>
match stack_cur with
- | existT state_cur sem::stack_rec =>
+ | existT _ state_cur sem::stack_rec =>
match compare_eqdec (last_symb_of_non_init_state state_cur) t with
| left e =>
let sem_conv := eq_rect _ symbol_semantic_type sem _ e in
- pop q stack_rec (action sem_conv)
+ pop q stack_rec (action sem_conv)
| right _ => Err
end
| [] => Err
@@ -147,16 +147,16 @@ Qed.
Definition reduce_step stack_cur production buffer: result step_result :=
do (stack_new, sem) <-
pop (prod_rhs_rev production) stack_cur (prod_action' production);
- match goto_table (state_of_stack stack_new) (prod_lhs production) return _ with
- | Some (exist state_new e) =>
+ match goto_table (state_of_stack stack_new) (prod_lhs production) with
+ | Some (exist _ state_new e) =>
let sem := eq_rect _ _ sem _ e in
OK (Progress_sr (existT noninitstate_type state_new sem::stack_new) buffer)
| None =>
- match stack_new return _ with
+ match stack_new with
| [] =>
- match compare_eqdec (prod_lhs production) (start_nt init) return _ with
+ match compare_eqdec (prod_lhs production) (start_nt init) with
| left e =>
- let sem := eq_rect _ (fun nt => _ (_ nt)) sem _ e in
+ let sem := eq_rect _ (fun nt => symbol_semantic_type (NT nt)) sem _ e in
OK (Accept_sr sem buffer)
| right _ => Err
end
@@ -171,7 +171,7 @@ Definition step stack_cur buffer: result step_result :=
reduce_step stack_cur production buffer
| Lookahead_act awt =>
match Streams.hd buffer with
- | existT term sem =>
+ | existT _ term sem =>
match awt term with
| Shift_act state_new e =>
let sem_conv := eq_rect _ symbol_semantic_type sem _ e in
@@ -213,6 +213,14 @@ Definition parse buffer n_steps: result parse_result :=
End Init.
+Arguments Fail_sr [init].
+Arguments Accept_sr [init] _ _.
+Arguments Progress_sr [init] _ _.
+
+Arguments Fail_pr [init].
+Arguments Timeout_pr [init].
+Arguments Parsed_pr [init] _ _.
+
End Make.
Module Type T(A:Automaton.T).
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v
index 3d564c11..eb407061 100644
--- a/cparser/validator/Interpreter_complete.v
+++ b/cparser/validator/Interpreter_complete.v
@@ -147,16 +147,16 @@ with ptl_zipper:
Fixpoint ptlz_cost {hole_symbs hole_word hole_sems}
(ptlz:ptl_zipper hole_symbs hole_word hole_sems) :=
match ptlz with
- | Non_terminal_pt_ptlz _ _ _ ptz =>
+ | Non_terminal_pt_ptlz ptz =>
ptz_cost ptz
- | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' =>
+ | Cons_ptl_ptlz pt ptlz' =>
ptlz_cost ptlz'
end
with ptz_cost {hole_symb hole_word hole_sem}
(ptz:pt_zipper hole_symb hole_word hole_sem) :=
match ptz with
| Top_ptz => 0
- | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' =>
+ | Cons_ptl_ptz ptl ptlz' =>
1 + ptl_size ptl + ptlz_cost ptlz'
end.
@@ -172,29 +172,29 @@ Inductive pt_dot: Type :=
Definition ptd_cost (ptd:pt_dot) :=
match ptd with
| Reduce_ptd ptlz => ptlz_cost ptlz
- | Shift_ptd _ _ _ _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz
+ | Shift_ptd _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz
end.
Fixpoint ptlz_buffer {hole_symbs hole_word hole_sems}
(ptlz:ptl_zipper hole_symbs hole_word hole_sems): Stream token :=
match ptlz with
- | Non_terminal_pt_ptlz _ _ _ ptz =>
+ | Non_terminal_pt_ptlz ptz =>
ptz_buffer ptz
- | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' =>
+ | Cons_ptl_ptlz _ ptlz' =>
ptlz_buffer ptlz'
end
with ptz_buffer {hole_symb hole_word hole_sem}
(ptz:pt_zipper hole_symb hole_word hole_sem): Stream token :=
match ptz with
| Top_ptz => buffer_end
- | Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' =>
+ | @Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' =>
wordq++ptlz_buffer ptlz'
end.
Definition ptd_buffer (ptd:pt_dot) :=
match ptd with
| Reduce_ptd ptlz => ptlz_buffer ptlz
- | Shift_ptd term sem _ wordq _ _ ptlz =>
+ | @Shift_ptd term sem _ wordq _ _ ptlz =>
Cons (existT (fun t => symbol_semantic_type (T t)) term sem)
(wordq ++ ptlz_buffer ptlz)
end.
@@ -202,16 +202,16 @@ Definition ptd_buffer (ptd:pt_dot) :=
Fixpoint ptlz_prod {hole_symbs hole_word hole_sems}
(ptlz:ptl_zipper hole_symbs hole_word hole_sems): production :=
match ptlz with
- | Non_terminal_pt_ptlz prod _ _ _ => prod
- | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' =>
+ | @Non_terminal_pt_ptlz prod _ _ _ => prod
+ | Cons_ptl_ptlz _ ptlz' =>
ptlz_prod ptlz'
end.
Fixpoint ptlz_past {hole_symbs hole_word hole_sems}
(ptlz:ptl_zipper hole_symbs hole_word hole_sems): list symbol :=
match ptlz with
- | Non_terminal_pt_ptlz _ _ _ _ => []
- | Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz'
+ | Non_terminal_pt_ptlz _ => []
+ | @Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz'
end.
Lemma ptlz_past_ptlz_prod:
@@ -236,12 +236,12 @@ Fixpoint ptlz_stack_compat {hole_symbs hole_word hole_sems}
(stack:stack): Prop :=
ptlz_state_compat ptlz (state_of_stack init stack) /\
match ptlz with
- | Non_terminal_pt_ptlz _ _ _ ptz =>
+ | Non_terminal_pt_ptlz ptz =>
ptz_stack_compat ptz stack
- | Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' =>
+ | @Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' =>
match stack with
| [] => False
- | existT _ sem'::stackq =>
+ | existT _ _ sem'::stackq =>
ptlz_stack_compat ptlz' stackq /\
sem ~= sem'
end
@@ -251,7 +251,7 @@ with ptz_stack_compat {hole_symb hole_word hole_sem}
(stack:stack): Prop :=
match ptz with
| Top_ptz => stack = []
- | Cons_ptl_ptz _ _ _ _ _ _ _ ptlz' =>
+ | Cons_ptl_ptz _ ptlz' =>
ptlz_stack_compat ptlz' stack
end.
@@ -267,7 +267,7 @@ Qed.
Definition ptd_stack_compat (ptd:pt_dot) (stack:stack): Prop :=
match ptd with
| Reduce_ptd ptlz => ptlz_stack_compat ptlz stack
- | Shift_ptd _ _ _ _ _ _ ptlz => ptlz_stack_compat ptlz stack
+ | Shift_ptd _ _ _ ptlz => ptlz_stack_compat ptlz stack
end.
Fixpoint build_pt_dot {hole_symbs hole_word hole_sems}
@@ -279,13 +279,13 @@ Fixpoint build_pt_dot {hole_symbs hole_word hole_sems}
with
| Nil_ptl => fun ptlz =>
Reduce_ptd ptlz
- | Cons_ptl _ _ _ pt _ _ _ ptl' =>
+ | Cons_ptl pt ptl' =>
match pt in parse_tree hole_symb hole_word hole_sem
return ptl_zipper (hole_symb::_) (hole_word++_) (hole_sem,_) -> _
with
| Terminal_pt term sem => fun ptlz =>
Shift_ptd term sem ptl' ptlz
- | Non_terminal_pt _ _ _ ptl'' => fun ptlz =>
+ | Non_terminal_pt ptl'' => fun ptlz =>
build_pt_dot ptl''
(Non_terminal_pt_ptlz (Cons_ptl_ptz ptl' ptlz))
end
@@ -360,10 +360,10 @@ Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems}
(pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem *
parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } }
with
- | Non_terminal_pt_ptlz prod word sem ptz => fun ptl =>
+ | @Non_terminal_pt_ptlz prod word sem ptz => fun ptl =>
let sem := uncurry (prod_action prod) sem in
existT _ word (existT _ sem (ptz, Non_terminal_pt ptl))
- | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' => fun ptl =>
+ | Cons_ptl_ptlz pt ptlz' => fun ptl =>
pop_ptlz (Cons_ptl pt ptl) ptlz'
end ptl.
@@ -371,7 +371,7 @@ Lemma pop_ptlz_cost:
forall hole_symbs hole_word hole_sems
(ptl:parse_tree_list hole_symbs hole_word hole_sems)
(ptlz:ptl_zipper hole_symbs hole_word hole_sems),
- let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in
+ let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in
ptlz_cost ptlz = ptz_cost ptz.
Proof.
fix 5.
@@ -384,7 +384,7 @@ Lemma pop_ptlz_buffer:
forall hole_symbs hole_word hole_sems
(ptl:parse_tree_list hole_symbs hole_word hole_sems)
(ptlz:ptl_zipper hole_symbs hole_word hole_sems),
- let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in
+ let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in
ptlz_buffer ptlz = ptz_buffer ptz.
Proof.
fix 5.
@@ -419,7 +419,7 @@ Lemma pop_ptlz_pop_stack_compat:
eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _
(pop_ptlz_pop_stack_compat_converter _ _ _ _ _)
in
- let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in
+ let 'existT _ word (existT _ sem (ptz, pt)) := pop_ptlz ptl ptlz in
match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with
| OK (stack', sem') =>
ptz_stack_compat ptz stack' /\ sem = sem'
@@ -431,7 +431,7 @@ fix 5.
destruct ptlz. intros; simpl.
split.
apply H.
-f_equal.
+eapply (f_equal (fun X => uncurry X semantic_values)).
apply JMeq_eq, JMeq_sym, JMeq_eqrect with (P:=fun x => x).
simpl; intros; destruct stack0.
destruct (proj2 H).
@@ -451,13 +451,13 @@ Qed.
Definition next_ptd (ptd:pt_dot): option pt_dot :=
match ptd with
- | Shift_ptd term sem _ _ _ ptl ptlz =>
+ | Shift_ptd term sem ptl ptlz =>
Some (build_pt_dot ptl (Cons_ptl_ptlz (Terminal_pt term sem) ptlz))
| Reduce_ptd ptlz =>
- let 'existT _ (existT _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in
+ let 'existT _ _ (existT _ _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in
match ptz in pt_zipper sym _ _ return parse_tree sym _ _ -> _ with
| Top_ptz => fun pt => None
- | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' =>
+ | Cons_ptl_ptz ptl ptlz' =>
fun pt => Some (build_pt_dot ptl (Cons_ptl_ptlz pt ptlz'))
end pt
end.
@@ -615,7 +615,7 @@ Definition init_ptd :=
match head return Type with | T _ => unit | NT _ => pt_dot end
with
| Terminal_pt _ _ => fun _ => ()
- | Non_terminal_pt _ _ _ ptl =>
+ | Non_terminal_pt ptl =>
fun top => build_pt_dot ptl (Non_terminal_pt_ptlz top)
end Top_ptz.
diff --git a/cparser/validator/Interpreter_correct.v b/cparser/validator/Interpreter_correct.v
index 3a285158..1263d4e3 100644
--- a/cparser/validator/Interpreter_correct.v
+++ b/cparser/validator/Interpreter_correct.v
@@ -59,7 +59,7 @@ Proof.
intros.
unfold arrows_right, arrows_left.
rewrite rev_append_rev, map_app, map_rev, fold_left_app.
-f_equal.
+apply f_equal.
rewrite <- fold_left_rev_right, rev_involutive.
reflexivity.
Qed.
@@ -87,7 +87,7 @@ Lemma pop_invariant:
end.
Proof.
induction symbols_to_pop; intros; unfold pop; fold pop.
-exists word_stack ([]:list token) sem_popped; intuition.
+exists word_stack, ([]:list token), sem_popped; intuition.
f_equal.
apply JMeq_eq, JMeq_eqrect with (P:=(fun x => x)).
destruct stack_cur as [|[]]; eauto.
diff --git a/cparser/validator/Interpreter_safe.v b/cparser/validator/Interpreter_safe.v
index f094ddce..a1aa35b8 100644
--- a/cparser/validator/Interpreter_safe.v
+++ b/cparser/validator/Interpreter_safe.v
@@ -69,15 +69,15 @@ Inductive stack_invariant: stack -> Prop :=
(symb_stack_of_stack stack) ->
prefix_pred (head_states_of_state (state_of_stack init stack))
(state_stack_of_stack stack) ->
- stack_invariant_rec stack ->
+ stack_invariant_next stack ->
stack_invariant stack
-with stack_invariant_rec: stack -> Prop :=
- | stack_invariant_rec_nil:
- stack_invariant_rec []
- | stack_invariant_rec_cons:
+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_rec (existT _ state_cur st::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.
diff --git a/cparser/validator/Validator_complete.v b/cparser/validator/Validator_complete.v
index 90ab1b0c..a9823278 100644
--- a/cparser/validator/Validator_complete.v
+++ b/cparser/validator/Validator_complete.v
@@ -276,7 +276,7 @@ Property is_terminal_shift_correct :
Proof.
unfold is_terminal_shift, terminal_shift.
intros.
-apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ fut look => _)).
intros.
destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition.
destruct (action_table st); intuition.
@@ -327,7 +327,11 @@ Proof.
unfold is_end_reduce, end_reduce.
intros.
revert H1.
-apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+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.
@@ -368,7 +372,7 @@ Definition non_terminal_goto :=
match fut with
| NT nt::q =>
match goto_table s1 nt with
- | Some (exist s2 _) =>
+ | Some (exist _ s2 _) =>
state_has_future s2 prod q lookahead
| None =>
forall prod fut lookahead,
@@ -386,7 +390,7 @@ Definition is_non_terminal_goto items_map :=
match future_of_prod prod pos with
| NT nt::_ =>
match goto_table s1 nt with
- | Some (exist s2 _) =>
+ | 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')
@@ -403,7 +407,16 @@ Property is_non_terminal_goto_correct :
Proof.
unfold is_non_terminal_goto, non_terminal_goto.
intros.
-apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+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 [[]|].
@@ -414,10 +427,10 @@ 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.
+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.
@@ -476,7 +489,11 @@ Property is_non_terminal_closed_correct:
Proof.
unfold is_non_terminal_closed, non_terminal_closed.
intros.
-apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+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.
diff --git a/cparser/validator/Validator_safe.v b/cparser/validator/Validator_safe.v
index c5229ac9..183d661b 100644
--- a/cparser/validator/Validator_safe.v
+++ b/cparser/validator/Validator_safe.v
@@ -121,7 +121,7 @@ Qed.
Definition goto_head_symbs :=
forall s nt,
match goto_table s nt with
- | Some (exist s2 _) =>
+ | Some (exist _ s2 _) =>
prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
| None => True
end.
@@ -130,7 +130,7 @@ Definition is_goto_head_symbs (_:unit) :=
forallb (fun s:state =>
forallb (fun nt =>
match goto_table s nt with
- | Some (exist s2 _) =>
+ | Some (exist _ s2 _) =>
is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
| None => true
end)
@@ -235,7 +235,7 @@ Qed.
Definition goto_past_state :=
forall s nt,
match goto_table s nt with
- | Some (exist s2 _) =>
+ | Some (exist _ s2 _) =>
prefix_pred (past_state_of_non_init_state s2)
(head_states_of_state s)
| None => True
@@ -245,7 +245,7 @@ Definition is_goto_past_state (_:unit) :=
forallb (fun s:state =>
forallb (fun nt =>
match goto_table s nt with
- | Some (exist s2 _) =>
+ | Some (exist _ s2 _) =>
is_prefix_pred
(past_state_of_non_init_state s2) (head_states_of_state s)
| None => true
generated by cgit (git 2.34.1) at 2024-06-29 11:39:07 +0000