From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- common/AST.v | 74 ++++++++++++++++++++++++++++++------------------------------ 1 file changed, 37 insertions(+), 37 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index c62b0091..16673c47 100644 --- a/common/AST.v +++ b/common/AST.v @@ -121,7 +121,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. @@ -255,14 +255,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. *) @@ -289,18 +289,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 *) Local Open Scope error_monad_scope. @@ -338,7 +338,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' => @@ -369,12 +369,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. @@ -387,12 +387,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. @@ -407,7 +407,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]]. @@ -429,7 +429,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]]. @@ -451,11 +451,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. @@ -470,11 +470,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. @@ -621,7 +621,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: @@ -630,7 +630,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: @@ -639,8 +639,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: @@ -649,8 +649,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. @@ -663,7 +663,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. @@ -679,7 +679,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. @@ -687,11 +687,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. *) @@ -723,24 +723,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. @@ -890,7 +890,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) @@ -948,7 +948,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. @@ -956,7 +956,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