From f0a5038b4e4220300637d3e9e918d9ec31623108 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Oct 2015 15:33:47 +0200 Subject: Added versions of the tranform_* functions in AST to work with functions taking the ident as argument. This functions are currently not used inside the proven part but it is nice to have them already there, when they are used by some future pass. They also come equiped with the corresponding proofs. --- common/AST.v | 217 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 216 insertions(+), 1 deletion(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 4d929f13..4e02b3d4 100644 --- a/common/AST.v +++ b/common/AST.v @@ -264,10 +264,46 @@ Qed. End TRANSF_PROGRAM. +(** 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. *) + +Section TRANSF_PROGRAM_IDENT. + +Variable A B V: Type. +Variable transf: ident -> A -> B. + +Definition transform_program_globdef_ident (idg: ident * globdef A V) : ident * globdef B V := + match idg with + | (id, Gfun f) => (id, Gfun (transf id f)) + | (id, Gvar v) => (id, Gvar v) + end. + +Definition transform_program_ident (p: program A V): program B V := + mkprogram + (List.map transform_program_globdef_ident p.(prog_defs)) + p.(prog_public) + p.(prog_main). + +Lemma tranforma_program_function_ident: + forall p i tf, + In (i, Gfun tf) (transform_program_ident p).(prog_defs) -> + 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. + exists f; auto. +Qed. + +End TRANSF_PROGRAM_IDENT. + (** 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. *) + return an error message. Also the transformation functions are defined + for the case the identifier of the function is passed as additional + argument *) Open Local Scope error_monad_scope. Open Local Scope string_scope. @@ -276,12 +312,18 @@ Section TRANSF_PROGRAM_GEN. Variables A B V W: Type. Variable transf_fun: A -> res B. +Variable transf_fun_ident: ident -> A -> res B. Variable transf_var: V -> res W. +Variable transf_var_ident: ident -> V -> res W. Definition transf_globvar (g: globvar V) : res (globvar W) := do info' <- transf_var g.(gvar_info); OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). +Definition transf_globvar_ident (i: ident) (g: globvar V) : res (globvar W) := + do info' <- transf_var_ident i g.(gvar_info); + OK (mkglobvar info' g.(gvar_init) g.(gvar_readonly) g.(gvar_volatile)). + Fixpoint transf_globdefs (l: list (ident * globdef A V)) : res (list (ident * globdef B W)) := match l with | nil => OK nil @@ -299,10 +341,31 @@ 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)) := + match l with + | nil => OK nil + | (id, Gfun f) :: l' => + match transf_fun_ident id f with + | Error msg => Error (MSG "In function " :: CTX id :: MSG ": " :: msg) + | OK tf => + do tl' <- transf_globdefs_ident l'; OK ((id, Gfun tf) :: tl') + end + | (id, Gvar v) :: l' => + match transf_globvar_ident id v with + | Error msg => Error (MSG "In variable " :: CTX id :: MSG ": " :: msg) + | OK tv => + do tl' <- transf_globdefs_ident l'; OK ((id, Gvar tv) :: tl') + end + end. + Definition transform_partial_program2 (p: program A V) : res (program B W) := do gl' <- transf_globdefs p.(prog_defs); OK (mkprogram gl' p.(prog_public) p.(prog_main)). +Definition transform_partial_ident_program2 (p: program A V) : res (program B W) := + do gl' <- transf_globdefs_ident p.(prog_defs); + OK (mkprogram gl' p.(prog_public) p.(prog_main)). + Lemma transform_partial_program2_function: forall p tp i tf, transform_partial_program2 p = OK tp -> @@ -321,6 +384,24 @@ Proof. exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. Qed. +Lemma transform_partial_ident_program2_function: + forall p tp i tf, + transform_partial_ident_program2 p = OK tp -> + 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. + 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. + 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. + exploit IHl; eauto. intros [f' [P Q]]; exists f'; auto. +Qed. + Lemma transform_partial_program2_variable: forall p tp i tv, transform_partial_program2 p = OK tp -> @@ -342,6 +423,28 @@ Proof. exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. Qed. + +Lemma transform_partial_ident_program2_variable: + forall p tp i tv, + transform_partial_ident_program2 p = OK tp -> + In (i, Gvar tv) tp.(prog_defs) -> + exists v, + 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. + 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. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. + destruct (transf_globvar_ident id v) as [tv1|msg] eqn:?; monadInv EQ. + simpl in H0; destruct H0. inv H. + monadInv Heqr. simpl. exists (gvar_info v). split. left. destruct v; auto. auto. + exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. +Qed. + Lemma transform_partial_program2_succeeds: forall p tp i g, transform_partial_program2 p = OK tp -> @@ -361,6 +464,25 @@ Proof. destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. Qed. +Lemma transform_partial_ident_program2_succeeds: + forall p tp i g, + transform_partial_ident_program2 p = OK tp -> + In (i, g) p.(prog_defs) -> + match g with + | Gfun fd => exists tfd, transf_fun_ident i fd = OK tfd + | Gvar gv => exists tv, transf_var_ident i gv.(gvar_info) = OK tv + end. +Proof. + 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 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. +Qed. + Lemma transform_partial_program2_main: forall p tp, transform_partial_program2 p = OK tp -> @@ -369,6 +491,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_ident_program2_main: + forall p tp, + transform_partial_ident_program2 p = OK tp -> + tp.(prog_main) = p.(prog_main). +Proof. + intros. monadInv H. reflexivity. +Qed. + Lemma transform_partial_program2_public: forall p tp, transform_partial_program2 p = OK tp -> @@ -377,6 +507,14 @@ Proof. intros. monadInv H. reflexivity. Qed. +Lemma transform_partial_ident_program2_public: + forall p tp, + transform_partial_ident_program2 p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + intros. monadInv H. reflexivity. +Qed. + (** Additionally, we can also "augment" the program with new global definitions and a different "main" function. *) @@ -397,6 +535,18 @@ Proof. intros. monadInv H. reflexivity. Qed. +Definition transform_partial_augment_ident_program (p: program A V) : res (program B W) := + do gl' <- transf_globdefs_ident p.(prog_defs); + OK(mkprogram (gl' ++ new_globs) p.(prog_public) new_main). + +Lemma transform_partial_augment_ident_program_main: + forall p tp, + transform_partial_augment_ident_program p = OK tp -> + tp.(prog_main) = new_main. +Proof. + intros. monadInv H. reflexivity. +Qed. + End AUGMENT. Remark transform_partial_program2_augment: @@ -409,6 +559,16 @@ Proof. simpl. f_equal. f_equal. rewrite <- app_nil_end. auto. Qed. +Remark transform_partial_ident_program2_augment: + forall p, + transform_partial_ident_program2 p = + transform_partial_augment_ident_program nil p.(prog_main) p. +Proof. + unfold transform_partial_ident_program2, transform_partial_augment_ident_program; intros. + destruct (transf_globdefs_ident (prog_defs p)); auto. + simpl. f_equal. f_equal. rewrite <- app_nil_end. auto. +Qed. + End TRANSF_PROGRAM_GEN. (** The following is a special case of [transform_partial_program2], @@ -418,10 +578,14 @@ Section TRANSF_PARTIAL_PROGRAM. Variable A B V: Type. Variable transf_partial: A -> res B. +Variable transf_partial_ident: ident -> A -> res B. Definition transform_partial_program (p: program A V) : res (program B V) := transform_partial_program2 transf_partial (fun v => OK v) p. +Definition transform_partial_ident_program (p: program A V) : res (program B V) := + transform_partial_ident_program2 transf_partial_ident (fun _ v => OK v) p. + Lemma transform_partial_program_main: forall p tp, transform_partial_program p = OK tp -> @@ -430,6 +594,14 @@ Proof. apply transform_partial_program2_main. Qed. +Lemma transform_partial_ident_program_main: + forall p tp, + transform_partial_ident_program p = OK tp -> + tp.(prog_main) = p.(prog_main). +Proof. + apply transform_partial_ident_program2_main. +Qed. + Lemma transform_partial_program_public: forall p tp, transform_partial_program p = OK tp -> @@ -438,6 +610,14 @@ Proof. apply transform_partial_program2_public. Qed. +Lemma transform_partial_ident_program_public: + forall p tp, + transform_partial_ident_program p = OK tp -> + tp.(prog_public) = p.(prog_public). +Proof. + apply transform_partial_ident_program2_public. +Qed. + Lemma transform_partial_program_function: forall p tp i tf, transform_partial_program p = OK tp -> @@ -447,6 +627,15 @@ Proof. apply transform_partial_program2_function. Qed. +Lemma transform_partial_ident_program_function: + forall p tp i tf, + transform_partial_ident_program p = OK tp -> + 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. +Qed. + Lemma transform_partial_program_succeeds: forall p tp i fd, transform_partial_program p = OK tp -> @@ -457,6 +646,16 @@ Proof. exploit transform_partial_program2_succeeds; eauto. Qed. +Lemma transform_partial_ident_program_succeeds: + forall p tp i fd, + transform_partial_ident_program p = OK tp -> + 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. +Qed. + End TRANSF_PARTIAL_PROGRAM. Lemma transform_program_partial_program: @@ -475,6 +674,22 @@ Proof. destruct v; auto. Qed. +Lemma transform_program_partial_ident_program: + forall (A B V: Type) (transf: ident -> A -> B) (p: program A V), + transform_partial_ident_program (fun id f => OK(transf id f)) p = OK(transform_program_ident transf p). +Proof. + intros. + 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. + induction (prog_defs p); simpl. + auto. + destruct a as [id [f|v]]; rewrite <- IHl. + auto. + destruct v; auto. +Qed. + (** The following is a relational presentation of [transform_partial_augment_preogram]. Given relations between function definitions and between variable information, it defines a relation -- cgit From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: Use Coq strings instead of idents to name external and builtin functions. The AST.ident type represents source-level identifiers as unique positive numbers. However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files. This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example: * in $ARCH/Machregs.v to define the register conventions for builtin functions; * in the VST program logic from Princeton to treat thread primitives specially. So far, we used AST.ident_of_string to recover the ident associated with a string. However, this function is defined in OCaml and doesn't execute within Coq. This is a problem both for VST and for future executability of CompCert within Coq. This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val. This provides stable names for externals and builtins, as needed. For inline asm and annotations, it's a matter of taste, but using strings feels more natural. EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables. --- common/AST.v | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 4e02b3d4..c62b0091 100644 --- a/common/AST.v +++ b/common/AST.v @@ -16,8 +16,8 @@ (** This file defines a number of data types and operations used in the abstract syntax trees of many of the intermediate languages. *) +Require Import String. Require Import Coqlib. -Require String. Require Import Errors. Require Import Integers. Require Import Floats. @@ -33,8 +33,6 @@ Definition ident := positive. Definition ident_eq := peq. -Parameter ident_of_string : String.string -> ident. - (** The intermediate languages are weakly typed, using the following types: *) Inductive typ : Type := @@ -305,8 +303,7 @@ End TRANSF_PROGRAM_IDENT. for the case the identifier of the function is passed as additional argument *) -Open Local Scope error_monad_scope. -Open Local Scope string_scope. +Local Open Scope error_monad_scope. Section TRANSF_PROGRAM_GEN. @@ -760,10 +757,10 @@ Qed. and associated operations. *) Inductive external_function : Type := - | EF_external (name: ident) (sg: signature) + | EF_external (name: string) (sg: signature) (** A system call or library function. Produces an event in the trace. *) - | EF_builtin (name: ident) (sg: signature) + | EF_builtin (name: string) (sg: signature) (** A compiler built-in function. Behaves like an external, but can be inlined by the compiler. *) | EF_vload (chunk: memory_chunk) @@ -786,15 +783,15 @@ Inductive external_function : Type := Produces no observable event. *) | EF_memcpy (sz: Z) (al: Z) (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *) - | EF_annot (text: ident) (targs: list typ) + | EF_annot (text: string) (targs: list typ) (** A programmer-supplied annotation. Takes zero, one or several arguments, produces an event carrying the text and the values of these arguments, and returns no value. *) - | EF_annot_val (text: ident) (targ: typ) + | EF_annot_val (text: string) (targ: typ) (** Another form of annotation that takes one argument, produces an event carrying the text and the value of this argument, and returns the value of the argument. *) - | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string) + | EF_inline_asm (text: string) (sg: signature) (clobbers: list string) (** Inline [asm] statements. Semantically, treated like an annotation with no parameters ([EF_annot text nil]). To be used with caution, as it can invalidate the semantic @@ -852,9 +849,8 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. + generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. apply String.string_dec. Defined. Global Opaque external_function_eq. -- cgit 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