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 --- common/AST.v | 76 ++++++++++++++++++++++++++++++------------------------------ 1 file changed, 38 insertions(+), 38 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 4e02b3d4..4ecbaa8a 100644 --- a/common/AST.v +++ b/common/AST.v @@ -123,7 +123,7 @@ Definition proj_sig_res (s: signature) : typ := Definition signature_eq: forall (s1 s2: signature), {s1=s2} + {s1<>s2}. Proof. generalize opt_typ_eq, list_typ_eq; intros; decide equality. - generalize bool_dec; intros. decide equality. + generalize bool_dec; intros. decide equality. Defined. Global Opaque signature_eq. @@ -257,14 +257,14 @@ Lemma transform_program_function: exists f, In (i, Gfun f) p.(prog_defs) /\ transf f = tf. Proof. simpl. unfold transform_program. intros. - exploit list_in_map_inv; eauto. - intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. + exploit list_in_map_inv; eauto. + intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. exists f; auto. Qed. End TRANSF_PROGRAM. -(** General iterator over program that applies a given code transfomration +(** General iterator over program that applies a given code transfomration function to all function descriptions with their identifers and leaves teh other parts of the program unchanged. *) @@ -291,18 +291,18 @@ Lemma tranforma_program_function_ident: exists f, In (i, Gfun f) p.(prog_defs) /\ transf i f = tf. Proof. simpl. unfold transform_program_ident. intros. - exploit list_in_map_inv; eauto. - intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. + exploit list_in_map_inv; eauto. + intros [[i' gd] [EQ IN]]. simpl in EQ. destruct gd; inv EQ. exists f; auto. Qed. End TRANSF_PROGRAM_IDENT. -(** The following is a more general presentation of [transform_program] where +(** The following is a more general presentation of [transform_program] where global variable information can be transformed, in addition to function definitions. Moreover, the transformation functions can fail and return an error message. Also the transformation functions are defined - for the case the identifier of the function is passed as additional + for the case the identifier of the function is passed as additional argument *) Open Local Scope error_monad_scope. @@ -341,7 +341,7 @@ Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * gl end end. -Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := +Fixpoint transf_globdefs_ident (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := match l with | nil => OK nil | (id, Gfun f) :: l' => @@ -372,12 +372,12 @@ Lemma transform_partial_program2_function: In (i, Gfun tf) tp.(prog_defs) -> exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun f = OK tf. Proof. - intros. monadInv H. simpl in H0. + intros. monadInv H. simpl in H0. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. destruct (transf_fun f) as [tf1|msg] eqn:?; monadInv EQ. - simpl in H0; destruct H0. inv H. exists f; auto. + simpl in H0; destruct H0. inv H. exists f; auto. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. destruct (transf_globvar v) as [tv1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. @@ -390,12 +390,12 @@ Lemma transform_partial_ident_program2_function: In (i, Gfun tf) tp.(prog_defs) -> exists f, In (i, Gfun f) p.(prog_defs) /\ transf_fun_ident i f = OK tf. Proof. - intros. monadInv H. simpl in H0. + intros. monadInv H. simpl in H0. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. destruct (transf_fun_ident id f) as [tf1|msg] eqn:?; monadInv EQ. - simpl in H0; destruct H0. inv H. exists f; auto. + simpl in H0; destruct H0. inv H. exists f; auto. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. destruct (transf_globvar_ident id v) as [tv1|msg] eqn:?; monadInv EQ. simpl in H0; destruct H0. inv H. @@ -410,7 +410,7 @@ Lemma transform_partial_program2_variable: In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs) /\ transf_var v = OK tv.(gvar_info). Proof. - intros. monadInv H. simpl in H0. + intros. monadInv H. simpl in H0. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. @@ -432,7 +432,7 @@ Lemma transform_partial_ident_program2_variable: In (i, Gvar(mkglobvar v tv.(gvar_init) tv.(gvar_readonly) tv.(gvar_volatile))) p.(prog_defs) /\ transf_var_ident i v = OK tv.(gvar_info). Proof. - intros. monadInv H. simpl in H0. + intros. monadInv H. simpl in H0. revert x EQ H0. induction (prog_defs p); simpl; intros. inv EQ. contradiction. destruct a as [id [f|v]]. @@ -454,11 +454,11 @@ Lemma transform_partial_program2_succeeds: | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv end. Proof. - intros. monadInv H. + intros. monadInv H. revert x EQ H0. induction (prog_defs p); simpl; intros. contradiction. destruct a as [id1 g1]. destruct g1. - destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. + destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. destruct H0. inv H. econstructor; eauto. eapply IHl; eauto. destruct (transf_globvar v) eqn:TV; try discriminate. monadInv EQ. destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. @@ -473,11 +473,11 @@ Lemma transform_partial_ident_program2_succeeds: | Gvar gv => exists tv, transf_var_ident i gv.(gvar_info) = OK tv end. Proof. - intros. monadInv H. + intros. monadInv H. revert x EQ H0. induction (prog_defs p); simpl; intros. contradiction. destruct a as [id1 g1]. destruct g1. - destruct (transf_fun_ident id1 f) eqn:TF; try discriminate. monadInv EQ. + destruct (transf_fun_ident id1 f) eqn:TF; try discriminate. monadInv EQ. destruct H0. inv H. econstructor; eauto. eapply IHl; eauto. destruct (transf_globvar_ident id1 v) eqn:TV; try discriminate. monadInv EQ. destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. @@ -624,7 +624,7 @@ Lemma transform_partial_program_function: In (i, Gfun tf) tp.(prog_defs) -> exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial f = OK tf. Proof. - apply transform_partial_program2_function. + apply transform_partial_program2_function. Qed. Lemma transform_partial_ident_program_function: @@ -633,7 +633,7 @@ Lemma transform_partial_ident_program_function: In (i, Gfun tf) tp.(prog_defs) -> exists f, In (i, Gfun f) p.(prog_defs) /\ transf_partial_ident i f = OK tf. Proof. - apply transform_partial_ident_program2_function. + apply transform_partial_ident_program2_function. Qed. Lemma transform_partial_program_succeeds: @@ -642,8 +642,8 @@ Lemma transform_partial_program_succeeds: In (i, Gfun fd) p.(prog_defs) -> exists tfd, transf_partial fd = OK tfd. Proof. - unfold transform_partial_program; intros. - exploit transform_partial_program2_succeeds; eauto. + unfold transform_partial_program; intros. + exploit transform_partial_program2_succeeds; eauto. Qed. Lemma transform_partial_ident_program_succeeds: @@ -652,8 +652,8 @@ Lemma transform_partial_ident_program_succeeds: In (i, Gfun fd) p.(prog_defs) -> exists tfd, transf_partial_ident i fd = OK tfd. Proof. - unfold transform_partial_ident_program; intros. - exploit transform_partial_ident_program2_succeeds; eauto. + unfold transform_partial_ident_program; intros. + exploit transform_partial_ident_program2_succeeds; eauto. Qed. End TRANSF_PARTIAL_PROGRAM. @@ -666,7 +666,7 @@ Proof. unfold transform_partial_program, transform_partial_program2, transform_program; intros. replace (transf_globdefs (fun f => OK (transf f)) (fun v => OK v) p.(prog_defs)) with (OK (map (transform_program_globdef transf) p.(prog_defs))). - auto. + auto. induction (prog_defs p); simpl. auto. destruct a as [id [f|v]]; rewrite <- IHl. @@ -682,7 +682,7 @@ Proof. unfold transform_partial_ident_program, transform_partial_ident_program2, transform_program; intros. replace (transf_globdefs_ident (fun id f => OK (transf id f)) (fun _ v => OK v) p.(prog_defs)) with (OK (map (transform_program_globdef_ident transf) p.(prog_defs))). - auto. + auto. induction (prog_defs p); simpl. auto. destruct a as [id [f|v]]; rewrite <- IHl. @@ -690,11 +690,11 @@ Proof. destruct v; auto. Qed. -(** The following is a relational presentation of +(** The following is a relational presentation of [transform_partial_augment_preogram]. Given relations between function definitions and between variable information, it defines a relation between programs stating that the two programs have appropriately related - shapes (global names are preserved and possibly augmented, etc) + shapes (global names are preserved and possibly augmented, etc) and that identically-named function definitions and variable information are related. *) @@ -726,24 +726,24 @@ Lemma transform_partial_augment_program_match: forall (A B V W: Type) (transf_fun: A -> res B) (transf_var: V -> res W) - (p: program A V) + (p: program A V) (new_globs : list (ident * globdef B W)) (new_main : ident) (tp: program B W), transform_partial_augment_program transf_fun transf_var new_globs new_main p = OK tp -> - match_program + match_program (fun fd tfd => transf_fun fd = OK tfd) (fun info tinfo => transf_var info = OK tinfo) new_globs new_main p tp. Proof. - unfold transform_partial_augment_program; intros. monadInv H. + unfold transform_partial_augment_program; intros. monadInv H. red; simpl. split; auto. exists x; split; auto. revert x EQ. generalize (prog_defs p). induction l; simpl; intros. monadInv EQ. constructor. - destruct a as [id [f|v]]. + destruct a as [id [f|v]]. (* function *) - destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. + destruct (transf_fun f) as [tf|?] eqn:?; monadInv EQ. constructor; auto. constructor; auto. (* variable *) unfold transf_globvar in EQ. @@ -854,7 +854,7 @@ Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} Proof. generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. apply String.string_dec. + apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. @@ -894,7 +894,7 @@ End TRANSF_PARTIAL_FUNDEF. (** * Arguments and results to builtin functions *) -Set Contextual Implicit. +Set Contextual Implicit. Inductive builtin_arg (A: Type) : Type := | BA (x: A) @@ -952,7 +952,7 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar | BA_addrstack ofs => BA_addrstack ofs | BA_loadglobal chunk id ofs => BA_loadglobal chunk id ofs | BA_addrglobal id ofs => BA_addrglobal id ofs - | BA_splitlong hi lo => + | BA_splitlong hi lo => BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo) end. @@ -960,7 +960,7 @@ Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_re match a with | BR x => BR (f x) | BR_none => BR_none - | BR_splitlong hi lo => + | BR_splitlong hi lo => BR_splitlong (map_builtin_res f hi) (map_builtin_res f lo) end. -- cgit