aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/validator
diff options
context:
space:
mode:
Diffstat (limited to 'cparser/validator')
-rw-r--r--cparser/validator/Alphabet.v4
-rw-r--r--cparser/validator/Automaton.v4
-rw-r--r--cparser/validator/Grammar.v12
-rw-r--r--cparser/validator/Interpreter.v2
-rw-r--r--cparser/validator/Interpreter_complete.v42
-rw-r--r--cparser/validator/Interpreter_correct.v6
-rw-r--r--cparser/validator/Validator_complete.v2
-rw-r--r--cparser/validator/Validator_safe.v2
8 files changed, 37 insertions, 37 deletions
diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v
index 85a1689d..13718cd5 100644
--- a/cparser/validator/Alphabet.v
+++ b/cparser/validator/Alphabet.v
@@ -193,7 +193,7 @@ Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
{ AlphabetComparable :=
{| compare := fun x y => compare31 (inj x) (inj y) |};
AlphabetFinite :=
- {| all_list := fst (iter_int31 inj_bound _
+ {| all_list := fst (iter_int31 inj_bound _
(fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }.
Next Obligation. apply Zcompare_antisym. Qed.
Next Obligation.
@@ -229,7 +229,7 @@ rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; refle
replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega.
rewrite Z_mod_same_full in H0.
exfalso; omega.
-exfalso; inversion Heqp; subst;
+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.
diff --git a/cparser/validator/Automaton.v b/cparser/validator/Automaton.v
index b15f87d2..98ab1246 100644
--- a/cparser/validator/Automaton.v
+++ b/cparser/validator/Automaton.v
@@ -113,7 +113,7 @@ Module Types(Import Init:AutInit).
(** Types used for the annotations of the automaton. **)
(** An item is a part of the annotations given to the validator.
- It is acually a set of LR(1) items sharing the same core. It is needed
+ It is acually a set of LR(1) items sharing the same core. It is needed
to validate completeness. **)
Record item := {
(** The pseudo-production of the item. **)
@@ -136,7 +136,7 @@ Module Type T.
Parameter start_nt: initstate -> nonterminal.
(** The action table maps a state to either a map terminal -> action. **)
- Parameter action_table:
+ Parameter action_table:
state -> action.
(** The goto table of an LR(1) automaton. **)
Parameter goto_table: state -> forall nt:nonterminal,
diff --git a/cparser/validator/Grammar.v b/cparser/validator/Grammar.v
index d162892d..0768d647 100644
--- a/cparser/validator/Grammar.v
+++ b/cparser/validator/Grammar.v
@@ -96,8 +96,8 @@ Module Defs(Import G:T).
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
+ 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. **)
Inductive parse_tree:
forall (head_symbol:symbol) (word:list token)
@@ -110,9 +110,9 @@ Module Defs(Import G:T).
parse_tree (T t)
[existT (fun t => symbol_semantic_type (T t)) t sem] 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
+ (** 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.**)
| Non_terminal_pt:
forall {p:production} {word:list token}
@@ -152,7 +152,7 @@ Module Defs(Import G:T).
Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) :=
- match tree with
+ match tree with
| Terminal_pt _ _ => 1
| Non_terminal_pt _ _ _ l => S (ptl_size l)
end
diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v
index 16be3859..2242065c 100644
--- a/cparser/validator/Interpreter.v
+++ b/cparser/validator/Interpreter.v
@@ -98,7 +98,7 @@ Fixpoint pop (symbols_to_pop:list symbol) (stack_cur:stack):
result (stack * A) :=
match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), _ with
| [] => fun A action => OK (stack_cur, action)
- | t::q => fun A action =>
+ | t::q => fun A action =>
match stack_cur with
| existT state_cur sem::stack_rec =>
match compare_eqdec (last_symb_of_non_init_state state_cur) t with
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v
index 3b922f7d..3d564c11 100644
--- a/cparser/validator/Interpreter_complete.v
+++ b/cparser/validator/Interpreter_complete.v
@@ -102,7 +102,7 @@ Variable buffer_end: Stream token.
Variable full_sem: symbol_semantic_type (NT (start_nt init)).
Inductive pt_zipper:
- forall (hole_symb:symbol) (hole_word:list token)
+ forall (hole_symb:symbol) (hole_word:list token)
(hole_sem:symbol_semantic_type hole_symb), Type :=
| Top_ptz:
pt_zipper (NT (start_nt init)) (full_word) (full_sem)
@@ -115,7 +115,7 @@ Inductive pt_zipper:
{wordq:list token}
{semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)},
parse_tree_list head_symbolsq wordq semantic_valuesq ->
-
+
ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq)
(semantic_valuet,semantic_valuesq) ->
@@ -134,11 +134,11 @@ with ptl_zipper:
{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}
{semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)},
-
+
ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq)
(semantic_valuet,semantic_valuesq) ->
@@ -275,7 +275,7 @@ Fixpoint build_pt_dot {hole_symbs hole_word hole_sems}
(ptlz:ptl_zipper hole_symbs hole_word hole_sems)
:pt_dot :=
match ptl in parse_tree_list hole_symbs hole_word hole_sems
- return ptl_zipper hole_symbs hole_word hole_sems -> _
+ return ptl_zipper hole_symbs hole_word hole_sems -> _
with
| Nil_ptl => fun ptlz =>
Reduce_ptd ptlz
@@ -292,7 +292,7 @@ Fixpoint build_pt_dot {hole_symbs hole_word hole_sems}
end ptlz.
Lemma build_pt_dot_cost:
- forall hole_symbs hole_word hole_sems
+ 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),
ptd_cost (build_pt_dot ptl ptlz) = ptl_size ptl + ptlz_cost ptlz.
@@ -307,7 +307,7 @@ simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity.
Qed.
Lemma build_pt_dot_buffer:
- forall hole_symbs hole_word hole_sems
+ 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),
ptd_buffer (build_pt_dot ptl ptlz) = hole_word ++ ptlz_buffer ptlz.
@@ -321,7 +321,7 @@ simpl; rewrite build_pt_dot_buffer.
apply app_str_app_assoc.
Qed.
-Lemma ptd_stack_compat_build_pt_dot:
+Lemma ptd_stack_compat_build_pt_dot:
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)
@@ -354,8 +354,8 @@ Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems}
{ word:_ & { sem:_ &
(pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem *
parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } :=
- match ptlz in ptl_zipper hole_symbs hole_word hole_sems
- return parse_tree_list hole_symbs hole_word hole_sems ->
+ match ptlz in ptl_zipper hole_symbs hole_word hole_sems
+ return parse_tree_list hole_symbs hole_word hole_sems ->
{ word:_ & { sem:_ &
(pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem *
parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } }
@@ -368,7 +368,7 @@ Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems}
end ptl.
Lemma pop_ptlz_cost:
- forall hole_symbs hole_word hole_sems
+ 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
@@ -381,7 +381,7 @@ simpl; apply pop_ptlz_cost.
Qed.
Lemma pop_ptlz_buffer:
- forall hole_symbs hole_word hole_sems
+ 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
@@ -414,14 +414,14 @@ Lemma pop_ptlz_pop_stack_compat:
(stack:stack),
ptlz_stack_compat ptlz stack ->
-
- let action' :=
- eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _
+
+ let action' :=
+ 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
match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with
- | OK (stack', sem') =>
+ | OK (stack', sem') =>
ptz_stack_compat ptz stack' /\ sem = sem'
| Err => True
end.
@@ -503,8 +503,8 @@ pose proof (pop_ptlz_buffer _ _ _ Nil_ptl ptlz).
destruct (pop_ptlz Nil_ptl ptlz) as [word [sem [ptz pt]]].
rewrite H0; clear H0.
revert H.
-match goal with
- |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end =>
+match goal with
+ |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end =>
replace p1 with p2; [destruct p2 as [|[]]; intros|]
end.
assumption.
@@ -610,8 +610,8 @@ Qed.
Variable full_pt: parse_tree (NT (start_nt init)) full_word full_sem.
Definition init_ptd :=
- match full_pt in parse_tree head full_word full_sem return
- pt_zipper head full_word full_sem ->
+ match full_pt in parse_tree head full_word full_sem return
+ pt_zipper head full_word full_sem ->
match head return Type with | T _ => unit | NT _ => pt_dot end
with
| Terminal_pt _ _ => fun _ => ()
@@ -668,7 +668,7 @@ Qed.
Theorem parse_complete n_steps:
match parse init (full_word ++ buffer_end) n_steps with
| OK (Parsed_pr sem_res buffer_end_res) =>
- sem_res = full_sem /\ buffer_end_res = buffer_end /\
+ sem_res = full_sem /\ buffer_end_res = buffer_end /\
pt_size full_pt <= n_steps
| OK Fail_pr => False
| OK Timeout_pr => n_steps < pt_size full_pt
diff --git a/cparser/validator/Interpreter_correct.v b/cparser/validator/Interpreter_correct.v
index 095b26ca..3a285158 100644
--- a/cparser/validator/Interpreter_correct.v
+++ b/cparser/validator/Interpreter_correct.v
@@ -68,7 +68,7 @@ Qed.
Lemma pop_invariant:
forall (symbols_to_pop symbols_popped:list symbol)
(stack_cur:stack)
- (A:Type)
+ (A:Type)
(action:arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A),
forall word_stack word_popped,
forall sem_popped,
@@ -96,12 +96,12 @@ destruct e; simpl.
dependent destruction H.
destruct H0, H1. apply (Cons_ptl X), inhabits in X0.
specialize (IHsymbols_to_pop _ _ _ action0 _ _ _ H X0).
-match goal with
+match goal with
IHsymbols_to_pop:match ?p1 with Err => _ | OK _ => _ end |- match ?p2 with Err => _ | OK _ => _ end =>
replace p2 with p1; [destruct p1 as [|[]]|]; intuition
end.
destruct IHsymbols_to_pop as [word1res [word2res [sem_full []]]]; intuition; subst.
-exists word1res.
+exists word1res.
eexists.
exists sem_full.
intuition.
diff --git a/cparser/validator/Validator_complete.v b/cparser/validator/Validator_complete.v
index 98559305..90ab1b0c 100644
--- a/cparser/validator/Validator_complete.v
+++ b/cparser/validator/Validator_complete.v
@@ -497,7 +497,7 @@ Qed.
(** The automaton is complete **)
Definition complete :=
- nullable_stable /\ first_stable /\ start_future /\ terminal_shift
+ nullable_stable /\ first_stable /\ start_future /\ terminal_shift
/\ end_reduce /\ non_terminal_goto /\ start_goto /\ non_terminal_closed.
Definition is_complete (_:unit) :=
diff --git a/cparser/validator/Validator_safe.v b/cparser/validator/Validator_safe.v
index 119f7337..c5229ac9 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.
generated by cgit (git 2.34.1) at 2024-07-01 06:42:17 +0000