From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- cparser/validator/Alphabet.v | 4 +-- cparser/validator/Automaton.v | 4 +-- cparser/validator/Grammar.v | 12 ++++----- cparser/validator/Interpreter.v | 2 +- cparser/validator/Interpreter_complete.v | 42 ++++++++++++++++---------------- cparser/validator/Interpreter_correct.v | 6 ++--- cparser/validator/Validator_complete.v | 2 +- cparser/validator/Validator_safe.v | 2 +- 8 files changed, 37 insertions(+), 37 deletions(-) (limited to 'cparser/validator') 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. -- cgit