Revu traitement des variables globales dans AST.program et dans Globalenvs.

Adaptation frontend, backend en consequence.
Integration passe C -> C#minor dans common/Main.v.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 222 insertions, 158 deletions

diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 036fd8f6..ccb7b03e 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -35,10 +35,10 @@ Module Type GENV.
    (** The type of global environments.  The parameter [F] is the type
        of function descriptions. *)
 
-  Variable globalenv: forall (F: Set), program F -> t F.
+  Variable globalenv: forall (F V: Set), program F V -> t F.
    (** Return the global environment for the given program. *)
 
-  Variable init_mem: forall (F: Set), program F -> mem.
+  Variable init_mem: forall (F V: Set), program F V -> mem.
    (** Return the initial memory state for the given program. *)
 
   Variable find_funct_ptr: forall (F: Set), t F -> block -> option F.
@@ -61,83 +61,110 @@ Module Type GENV.
     forall (F: Set) (ge: t F) (b: block),
     find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b.    
   Hypothesis find_funct_ptr_prop:
-    forall (F: Set) (P: F -> Prop) (p: program F) (b: block) (f: F),
+    forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
     (forall id f, In (id, f) (prog_funct p) -> P f) ->
     find_funct_ptr (globalenv p) b = Some f ->
     P f.
   Hypothesis find_funct_prop:
-    forall (F: Set) (P: F -> Prop) (p: program F) (v: val) (f: F),
+    forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F),
     (forall id f, In (id, f) (prog_funct p) -> P f) ->
     find_funct (globalenv p) v = Some f ->
     P f.
   Hypothesis find_funct_ptr_symbol_inversion:
-    forall (F: Set) (p: program F) (id: ident) (b: block) (f: F),
+    forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F),
     find_symbol (globalenv p) id = Some b ->
     find_funct_ptr (globalenv p) b = Some f ->
     In (id, f) p.(prog_funct).
 
   Hypothesis initmem_nullptr:
-    forall (F: Set) (p: program F),
+    forall (F V: Set) (p: program F V),
     let m := init_mem p in
     valid_block m nullptr /\
     m.(blocks) nullptr = empty_block 0 0.
   Hypothesis initmem_block_init:
-    forall (F: Set) (p: program F) (b: block),
+    forall (F V: Set) (p: program F V) (b: block),
     exists id, (init_mem p).(blocks) b = block_init_data id.
   Hypothesis find_funct_ptr_inv:
-    forall (F: Set) (p: program F) (b: block) (f: F),
+    forall (F V: Set) (p: program F V) (b: block) (f: F),
     find_funct_ptr (globalenv p) b = Some f -> b < 0.
   Hypothesis find_symbol_inv:
-    forall (F: Set) (p: program F) (id: ident) (b: block),
+    forall (F V: Set) (p: program F V) (id: ident) (b: block),
     find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p).
 
 (** Commutation properties between program transformations
   and operations over global environments. *)
 
   Hypothesis find_funct_ptr_transf:
-    forall (A B: Set) (transf: A -> B) (p: program A) (b: block) (f: A),
+    forall (A B V: Set) (transf: A -> B) (p: program A V) (b: block) (f: A),
     find_funct_ptr (globalenv p) b = Some f ->
     find_funct_ptr (globalenv (transform_program transf p)) b = Some (transf f).
   Hypothesis find_funct_transf:
-    forall (A B: Set) (transf: A -> B) (p: program A) (v: val) (f: A),
+    forall (A B V: Set) (transf: A -> B) (p: program A V) (v: val) (f: A),
     find_funct (globalenv p) v = Some f ->
     find_funct (globalenv (transform_program transf p)) v = Some (transf f).
   Hypothesis find_symbol_transf:
-    forall (A B: Set) (transf: A -> B) (p: program A) (s: ident),
+    forall (A B V: Set) (transf: A -> B) (p: program A V) (s: ident),
     find_symbol (globalenv (transform_program transf p)) s =
     find_symbol (globalenv p) s.
   Hypothesis init_mem_transf:
-    forall (A B: Set) (transf: A -> B) (p: program A),
+    forall (A B V: Set) (transf: A -> B) (p: program A V),
     init_mem (transform_program transf p) = init_mem p.
 
 (** Commutation properties between partial program transformations
   and operations over global environments. *)
 
   Hypothesis find_funct_ptr_transf_partial:
-    forall (A B: Set) (transf: A -> option B)
-           (p: program A) (p': program B),
+    forall (A B V: Set) (transf: A -> option B)
+           (p: program A V) (p': program B V),
     transform_partial_program transf p = Some p' ->
     forall (b: block) (f: A),
     find_funct_ptr (globalenv p) b = Some f ->
     find_funct_ptr (globalenv p') b = transf f /\ transf f <> None.
   Hypothesis find_funct_transf_partial:
-    forall (A B: Set) (transf: A -> option B)
-           (p: program A) (p': program B),
+    forall (A B V: Set) (transf: A -> option B)
+           (p: program A V) (p': program B V),
     transform_partial_program transf p = Some p' ->
     forall (v: val) (f: A),
     find_funct (globalenv p) v = Some f ->
     find_funct (globalenv p') v = transf f /\ transf f <> None.
   Hypothesis find_symbol_transf_partial:
-    forall (A B: Set) (transf: A -> option B)
-           (p: program A) (p': program B),
+    forall (A B V: Set) (transf: A -> option B)
+           (p: program A V) (p': program B V),
     transform_partial_program transf p = Some p' ->
     forall (s: ident),
     find_symbol (globalenv p') s = find_symbol (globalenv p) s.
   Hypothesis init_mem_transf_partial:
-    forall (A B: Set) (transf: A -> option B)
-           (p: program A) (p': program B),
+    forall (A B V: Set) (transf: A -> option B)
+           (p: program A V) (p': program B V),
     transform_partial_program transf p = Some p' ->
     init_mem p' = init_mem p.
+
+  Hypothesis find_funct_ptr_transf_partial2:
+    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+           (p: program A V) (p': program B W),
+    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    forall (b: block) (f: A),
+    find_funct_ptr (globalenv p) b = Some f ->
+    find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None.
+  Hypothesis find_funct_transf_partial2:
+    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+           (p: program A V) (p': program B W),
+    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    forall (v: val) (f: A),
+    find_funct (globalenv p) v = Some f ->
+    find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None.
+  Hypothesis find_symbol_transf_partial2:
+    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+           (p: program A V) (p': program B W),
+    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    forall (s: ident),
+    find_symbol (globalenv p') s = find_symbol (globalenv p) s.
+  Hypothesis init_mem_transf_partial2:
+    forall (A B V W: Set) (transf_fun: A -> option B) (transf_var: V -> option W)
+           (p: program A V) (p': program B W),
+    transform_partial_program2 transf_fun transf_var p = Some p' ->
+    init_mem p' = init_mem p.
+
 End GENV.
 
 (** The rest of this library is a straightforward implementation of
@@ -147,17 +174,18 @@ Module Genv: GENV.
 
 Section GENV.
 
-Variable funct: Set.                    (* The type of functions *)
+Variable F: Set.                    (* The type of functions *)
+Variable V: Set.                    (* The type of information over variables *)
 
 Record genv : Set := mkgenv {
-  functions: ZMap.t (option funct);     (* mapping function ptr -> function *)
+  functions: ZMap.t (option F);     (* mapping function ptr -> function *)
   nextfunction: Z;
   symbols: PTree.t block                (* mapping symbol -> block *)
 }.
 
 Definition t := genv.
 
-Definition add_funct (name_fun: (ident * funct)) (g: genv) : genv :=
+Definition add_funct (name_fun: (ident * F)) (g: genv) : genv :=
   let b := g.(nextfunction) in
   mkgenv (ZMap.set b (Some (snd name_fun)) g.(functions))
          (Zpred b)
@@ -168,10 +196,10 @@ Definition add_symbol (name: ident) (b: block) (g: genv) : genv :=
          g.(nextfunction)
          (PTree.set name b g.(symbols)).
 
-Definition find_funct_ptr (g: genv) (b: block) : option funct :=
+Definition find_funct_ptr (g: genv) (b: block) : option F :=
   ZMap.get b g.(functions).
 
-Definition find_funct (g: genv) (v: val) : option funct :=
+Definition find_funct (g: genv) (v: val) : option F :=
   match v with
   | Vptr b ofs =>
       if Int.eq ofs Int.zero then find_funct_ptr g b else None
@@ -183,7 +211,7 @@ Definition find_symbol (g: genv) (symb: ident) : option block :=
   PTree.get symb g.(symbols).
 
 Lemma find_funct_inv:
-  forall (ge: t) (v: val) (f: funct),
+  forall (ge: t) (v: val) (f: F),
   find_funct ge v = Some f -> exists b, v = Vptr b Int.zero.
 Proof.
   intros until f. unfold find_funct. destruct v; try (intros; discriminate).
@@ -207,38 +235,40 @@ Qed.
 Definition empty : genv :=
   mkgenv (ZMap.init None) (-1) (PTree.empty block).
 
-Definition add_functs (init: genv) (fns: list (ident * funct)) : genv :=
+Definition add_functs (init: genv) (fns: list (ident * F)) : genv :=
   List.fold_right add_funct init fns.
 
 Definition add_globals 
-        (init: genv * mem) (vars: list (ident * list init_data)) : genv * mem :=
+       (init: genv * mem) (vars: list (ident * list init_data * V))
+       : genv * mem :=
   List.fold_right
-    (fun (id_init: ident * list init_data) (g_st: genv * mem) =>
-       let (id, init) := id_init in
-       let (g, st) := g_st in
-       let (st', b) := Mem.alloc_init_data st init in
-       (add_symbol id b g, st'))
+    (fun (id_init: ident * list init_data * V) (g_st: genv * mem) =>
+       match id_init, g_st with
+       | ((id, init), info), (g, st) =>
+           let (st', b) := Mem.alloc_init_data st init in
+           (add_symbol id b g, st')
+       end)
     init vars.
 
-Definition globalenv_initmem (p: program funct) : (genv * mem) :=
+Definition globalenv_initmem (p: program F V) : (genv * mem) :=
   add_globals
     (add_functs empty p.(prog_funct), Mem.empty)
     p.(prog_vars).
 
-Definition globalenv (p: program funct) : genv :=
+Definition globalenv (p: program F V) : genv :=
   fst (globalenv_initmem p).
-Definition init_mem  (p: program funct) : mem :=
+Definition init_mem  (p: program F V) : mem :=
   snd (globalenv_initmem p).
 
 Lemma functions_globalenv:
-  forall (p: program funct),
+  forall (p: program F V),
   functions (globalenv p) = functions (add_functs empty p.(prog_funct)).
 Proof.
   assert (forall init vars,
      functions (fst (add_globals init vars)) = functions (fst init)).
   induction vars; simpl.
   reflexivity.
-  destruct a. destruct (add_globals init vars).
+  destruct a as [[id1 init1] info1]. destruct (add_globals init vars).
   simpl. exact IHvars. 
 
   unfold add_globals; simpl. 
@@ -247,34 +277,28 @@ Proof.
 Qed.
 
 Lemma initmem_nullptr:
-  forall (p: program funct),
+  forall (p: program F V),
   let m := init_mem p in
   valid_block m nullptr /\
   m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0).
 Proof.
-  assert
-   (forall init,
-    let m1 := snd init in
-    0 < m1.(nextblock) ->
-    m1.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0) ->
-    forall vars,
-    let m2 := snd (add_globals init vars) in
-    0 < m2.(nextblock) /\
-    m2.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0)).
+  pose (P := fun m => valid_block m nullptr /\
+        m.(blocks) nullptr = mkblock 0 0 (fun y => Undef) (undef_undef_outside 0 0)).
+  assert (forall init, P (snd init) -> forall vars, P (snd (add_globals init vars))).
   induction vars; simpl; intros.
-  tauto.
-  destruct a. 
-  caseEq (add_globals init vars). intros g m2 EQ. 
-  rewrite EQ in IHvars. simpl in IHvars. elim IHvars; intros.
-  simpl. split. omega. 
-  rewrite update_o. auto. apply sym_not_equal. apply Zlt_not_eq. exact H1.
-
-  intro. unfold init_mem. unfold globalenv_initmem. 
-  unfold valid_block. apply H. simpl. omega. reflexivity.
+  auto.
+  destruct a as [[id1 in1] inf1]. 
+  destruct (add_globals init vars) as [g st]. 
+  simpl in *. destruct IHvars. split.
+  red; simpl. red in H0. omega.
+  simpl. rewrite update_o. auto. unfold block. red in H0. omega. 
+
+  intro. unfold init_mem, globalenv_initmem. apply H. 
+  red; simpl. split. compute. auto. reflexivity.
 Qed. 
 
 Lemma initmem_block_init:
-  forall (p: program funct) (b: block),
+  forall (p: program F V) (b: block),
   exists id, (init_mem p).(blocks) b = block_init_data id.
 Proof.
   assert (forall g0 vars g1 m b,
@@ -283,11 +307,12 @@ Proof.
   induction vars; simpl.
   intros. inversion H. unfold Mem.empty; simpl. 
   exists (@nil init_data). symmetry. apply Mem.block_init_data_empty.
-  destruct a. caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. 
+  destruct a as [[id1 init1] info1]. 
+  caseEq (add_globals (g0, Mem.empty) vars). intros g1 m1 EQ. 
   intros g m b EQ1. injection EQ1; intros EQ2 EQ3; clear EQ1.
   rewrite <- EQ2; simpl. unfold update.
   case (zeq b (nextblock m1)); intro.
-  exists l; auto.
+  exists init1; auto.
   eauto.
   intros. caseEq (globalenv_initmem p). 
   intros g m EQ. unfold init_mem; rewrite EQ; simpl. 
@@ -301,7 +326,7 @@ Proof.
 Qed.
 
 Theorem find_funct_ptr_inv:
-  forall (p: program funct) (b: block) (f: funct),
+  forall (p: program F V) (b: block) (f: F),
   find_funct_ptr (globalenv p) b = Some f -> b < 0.
 Proof.
   intros until f.
@@ -316,7 +341,7 @@ Proof.
 Qed.
 
 Theorem find_symbol_inv:
-  forall (p: program funct) (id: ident) (b: block),
+  forall (p: program F V) (id: ident) (b: block),
   find_symbol (globalenv p) id = Some b -> b < nextblock (init_mem p).
 Proof.
   assert (forall fns s b,
@@ -333,9 +358,10 @@ Proof.
   induction vars; simpl; intros until b.
   intros. inversion H0. subst g m. simpl. 
   generalize (H fns s b H1). omega.
-  destruct a. caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
+  destruct a as [[id1 init1] info1]. 
+  caseEq (add_globals (add_functs empty fns, Mem.empty) vars).
   intros g1 m1 ADG EQ. inversion EQ; subst g m; clear EQ.
-  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s i); intro.
+  unfold add_symbol; simpl. rewrite PTree.gsspec. case (peq s id1); intro.
   intro EQ; inversion EQ. omega.
   intro. generalize (IHvars _ _ _ _ ADG H0). omega.
   intros until b. unfold find_symbol, globalenv, init_mem, globalenv_initmem; simpl.
@@ -348,7 +374,7 @@ End GENV.
 
 (* Invariants on functions *)
 Lemma find_funct_ptr_prop:
-  forall (F: Set) (P: F -> Prop) (p: program F) (b: block) (f: F),
+  forall (F V: Set) (P: F -> Prop) (p: program F V) (b: block) (f: F),
   (forall id f, In (id, f) (prog_funct p) -> P f) ->
   find_funct_ptr (globalenv p) b = Some f ->
   P f.
@@ -364,7 +390,7 @@ Proof.
 Qed.
 
 Lemma find_funct_prop:
-  forall (F: Set) (P: F -> Prop) (p: program F) (v: val) (f: F),
+  forall (F V: Set) (P: F -> Prop) (p: program F V) (v: val) (f: F),
   (forall id f, In (id, f) (prog_funct p) -> P f) ->
   find_funct (globalenv p) v = Some f ->
   P f.
@@ -376,7 +402,7 @@ Proof.
 Qed.
 
 Lemma find_funct_ptr_symbol_inversion:
-  forall (F: Set) (p: program F) (id: ident) (b: block) (f: F),
+  forall (F V: Set) (p: program F V) (id: ident) (b: block) (f: F),
   find_symbol (globalenv p) id = Some b ->
   find_funct_ptr (globalenv p) b = Some f ->
   In (id, f) p.(prog_funct).
@@ -407,15 +433,15 @@ Proof.
     generalize (H _ H0). fold g. unfold block. omega.
   assert (forall g0 m0, b < 0 ->
           forall vars g m,
-          @add_globals F (g0, m0) vars = (g, m) ->
+          @add_globals F V (g0, m0) vars = (g, m) ->
           PTree.get id g.(symbols) = Some b ->
           PTree.get id g0.(symbols) = Some b).
     induction vars; simpl.
     intros. inversion H2. auto.
-    destruct a. caseEq (add_globals (g0, m0) vars). 
+    destruct a as [[id1 init1] info1]. caseEq (add_globals (g0, m0) vars). 
     intros g1 m1 EQ g m EQ1. injection EQ1; simpl; clear EQ1.
     unfold add_symbol; intros A B. rewrite <- B. simpl. 
-    rewrite PTree.gsspec. case (peq id i); intros.
+    rewrite PTree.gsspec. case (peq id id1); intros.
     assert (b > 0). injection H2; intros. rewrite <- H3. apply nextblock_pos. 
     omegaContradiction.
     eauto. 
@@ -430,24 +456,26 @@ Qed.
 
 (* Global environments and program transformations. *)
 
-Section TRANSF_PROGRAM_PARTIAL.
+Section TRANSF_PROGRAM_PARTIAL2.
 
-Variable A B: Set.
-Variable transf: A -> option B.
-Variable p: program A.
-Variable p': program B.
-Hypothesis transf_OK: transform_partial_program transf p = Some p'.
+Variable A B V W: Set.
+Variable transf_fun: A -> option B.
+Variable transf_var: V -> option W.
+Variable p: program A V.
+Variable p': program B W.
+Hypothesis transf_OK:
+  transform_partial_program2 transf_fun transf_var p = Some p'.
 
 Lemma add_functs_transf:
   forall (fns: list (ident * A)) (tfns: list (ident * B)),
-  transf_partial_program transf fns = Some tfns ->
+  map_partial transf_fun fns = Some tfns ->
   let r := add_functs (empty A) fns in
   let tr := add_functs (empty B) tfns in
   nextfunction tr = nextfunction r /\
   symbols tr = symbols r /\
   forall (b: block) (f: A),
   ZMap.get b (functions r) = Some f ->
-  ZMap.get b (functions tr) = transf f /\ transf f <> None.
+  ZMap.get b (functions tr) = transf_fun f /\ transf_fun f <> None.
 Proof.
   induction fns; simpl.
 
@@ -455,8 +483,8 @@ Proof.
   simpl. split. reflexivity. split. reflexivity.
   intros b f; repeat (rewrite ZMap.gi). intros; discriminate.
 
-  intro tfns. destruct a. caseEq (transf a). intros a' TA. 
-  caseEq (transf_partial_program transf fns). intros l TPP EQ.
+  intro tfns. destruct a. caseEq (transf_fun a). intros a' TA. 
+  caseEq (map_partial transf_fun fns). intros l TPP EQ.
   injection EQ; intro; subst tfns.
   clear EQ. simpl. 
   generalize (IHfns l TPP).
@@ -476,32 +504,49 @@ Proof.
 Qed.
 
 Lemma mem_add_globals_transf:
-  forall (g1: genv A) (g2: genv B) (m: mem) (vars: list (ident * list init_data)),
-  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) vars).
+  forall (g1: genv A) (g2: genv B) (m: mem) 
+         (vars: list (ident * list init_data * V))
+         (tvars: list (ident * list init_data * W)),
+  map_partial transf_var vars = Some tvars ->
+  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
 Proof.
   induction vars; simpl.
-  reflexivity.
-  destruct a. destruct (add_globals (g1, m) vars).
-  destruct (add_globals (g2, m) vars).
-  simpl in IHvars. subst m1. reflexivity. 
-Qed. 
+  intros. inversion H. reflexivity.
+  intro. destruct a as [[id1 init1] info1]. 
+  caseEq (transf_var info1); try congruence.
+  intros tinfo1 EQ1.
+  caseEq (map_partial transf_var vars); try congruence.
+  intros tvars' EQ2 EQ3. 
+  inversion EQ3. simpl. 
+  generalize (IHvars _ EQ2). 
+  destruct (add_globals (g1, m) vars).
+  destruct (add_globals (g2, m) tvars').
+  simpl. intro. subst m1. auto.
+Qed.
 
 Lemma symbols_add_globals_transf:
   forall (g1: genv A) (g2: genv B) (m: mem),
   symbols g1 = symbols g2 ->
-  forall (vars: list (ident * list init_data)),
+  forall (vars: list (ident * list init_data * V))
+         (tvars: list (ident * list init_data * W)),
+  map_partial transf_var vars = Some tvars ->
   symbols (fst (add_globals (g1, m) vars)) =
-  symbols (fst (add_globals (g2, m) vars)).
+  symbols (fst (add_globals (g2, m) tvars)).
 Proof.
   induction vars; simpl.
-  assumption.
-  generalize (mem_add_globals_transf g1 g2 m vars); intro.
-  destruct a. destruct (add_globals (g1, m) vars).
-  destruct (add_globals (g2, m) vars).
-  simpl. simpl in IHvars. simpl in H0. 
-  rewrite H0; rewrite IHvars. reflexivity.
+  intros. inversion H0. assumption.
+  intro. destruct a as [[id1 init1] info1]. 
+  caseEq (transf_var info1); try congruence. intros tinfo1 EQ1.
+  caseEq (map_partial transf_var vars); try congruence.
+  intros tvars' EQ2 EQ3. inversion EQ3; simpl. 
+  generalize (IHvars _ EQ2). 
+  generalize (mem_add_globals_transf g1 g2 m vars EQ2).
+  destruct (add_globals (g1, m) vars).
+  destruct (add_globals (g2, m) tvars').
+  simpl. intros. congruence.
 Qed.
 
+(*
 Lemma prog_funct_transf_OK:
   transf_partial_program transf p.(prog_funct) = Some p'.(prog_funct).
 Proof.
@@ -510,94 +555,118 @@ Proof.
   injection transf_OK0; intros; subst p'. reflexivity.
   discriminate.
 Qed.
+*)
 
-Theorem find_funct_ptr_transf_partial:
+Theorem find_funct_ptr_transf_partial2:
   forall (b: block) (f: A),
   find_funct_ptr (globalenv p) b = Some f ->
-  find_funct_ptr (globalenv p') b = transf f /\ transf f <> None.
+  find_funct_ptr (globalenv p') b = transf_fun f /\ transf_fun f <> None.
 Proof.
-  intros until f. 
-  generalize (add_functs_transf p.(prog_funct) prog_funct_transf_OK).
-  intros [X [Y Z]].
-  unfold find_funct_ptr. 
-  repeat (rewrite functions_globalenv). 
-  apply Z. 
+  intros until f. functional inversion transf_OK. 
+  destruct (add_functs_transf _ H0) as [P [Q R]]. 
+  unfold find_funct_ptr. repeat rewrite functions_globalenv. simpl. 
+  auto.
 Qed.
 
-Theorem find_funct_transf_partial:
+Theorem find_funct_transf_partial2:
   forall (v: val) (f: A),
   find_funct (globalenv p) v = Some f ->
-  find_funct (globalenv p') v = transf f /\ transf f <> None.
+  find_funct (globalenv p') v = transf_fun f /\ transf_fun f <> None.
 Proof.
   intros until f. unfold find_funct. 
   case v; try (intros; discriminate).
   intros b ofs.
   case (Int.eq ofs Int.zero); try (intros; discriminate).
-  apply find_funct_ptr_transf_partial. 
+  apply find_funct_ptr_transf_partial2. 
 Qed.
 
-Lemma symbols_init_transf:
+Lemma symbols_init_transf2:
   symbols (globalenv p') = symbols (globalenv p).
 Proof.
   unfold globalenv. unfold globalenv_initmem.
-  generalize (add_functs_transf p.(prog_funct) prog_funct_transf_OK).
-  intros [X [Y Z]].
-  generalize transf_OK.
-  unfold transform_partial_program.
-  case (transf_partial_program transf (prog_funct p)).
-  intros. injection transf_OK0; intro; subst p'; simpl.
-  symmetry. apply symbols_add_globals_transf.
-  symmetry. exact Y. 
-  intros; discriminate.
+  functional inversion transf_OK.
+  destruct (add_functs_transf _ H0) as [P [Q R]]. 
+  simpl. symmetry. apply symbols_add_globals_transf. auto. auto.
 Qed.
 
-Theorem find_symbol_transf_partial:
+Theorem find_symbol_transf_partial2:
   forall (s: ident),
   find_symbol (globalenv p') s = find_symbol (globalenv p) s.
 Proof.
   intros. unfold find_symbol. 
-  rewrite symbols_init_transf. auto.
+  rewrite symbols_init_transf2. auto.
 Qed.
 
-Theorem init_mem_transf_partial:
+Theorem init_mem_transf_partial2:
   init_mem p' = init_mem p.
 Proof.
   unfold init_mem. unfold globalenv_initmem. 
-  generalize transf_OK.
-  unfold transform_partial_program.
-  case (transf_partial_program transf (prog_funct p)).
-  intros. injection transf_OK0; intro; subst p'; simpl.
-  symmetry. apply mem_add_globals_transf. 
-  intros; discriminate.
+  functional inversion transf_OK.
+  simpl. symmetry. apply mem_add_globals_transf. auto.
 Qed.
 
-End TRANSF_PROGRAM_PARTIAL.
+End TRANSF_PROGRAM_PARTIAL2.
 
-Section TRANSF_PROGRAM.
 
-Variable A B: Set.
-Variable transf: A -> B.
-Variable p: program A.
-Let tp := transform_program transf p.
+Section TRANSF_PROGRAM_PARTIAL.
 
-Definition transf_partial (x: A) : option B := Some (transf x).
+Variable A B V: Set.
+Variable transf: A -> option B.
+Variable p: program A V.
+Variable p': program B V.
+Hypothesis transf_OK: transform_partial_program transf p = Some p'.
 
-Lemma transf_program_transf_partial_program:
-  forall (fns: list (ident * A)),
-  transf_partial_program transf_partial fns =
-  Some (transf_program transf fns).
+Remark transf2_OK:
+  transform_partial_program2 transf (fun x => Some x) p = Some p'.
 Proof.
-  induction fns; simpl.
-   reflexivity.
-   destruct a. rewrite IHfns. reflexivity.
+  rewrite <- transf_OK. unfold transform_partial_program2, transform_partial_program.
+  destruct (map_partial transf (prog_funct p)); auto.
+  rewrite map_partial_identity; auto. 
+Qed.
+
+Theorem find_funct_ptr_transf_partial:
+  forall (b: block) (f: A),
+  find_funct_ptr (globalenv p) b = Some f ->
+  find_funct_ptr (globalenv p') b = transf f /\ transf f <> None.
+Proof.
+  exact (@find_funct_ptr_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
 Qed.
 
-Lemma transform_program_transform_partial_program:
-  transform_partial_program transf_partial p = Some tp.
+Theorem find_funct_transf_partial:
+  forall (v: val) (f: A),
+  find_funct (globalenv p) v = Some f ->
+  find_funct (globalenv p') v = transf f /\ transf f <> None.
 Proof.
-  unfold tp. unfold transform_partial_program, transform_program.
-  rewrite transf_program_transf_partial_program.
-  reflexivity.
+  exact (@find_funct_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+Qed.
+
+Theorem find_symbol_transf_partial:
+  forall (s: ident),
+  find_symbol (globalenv p') s = find_symbol (globalenv p) s.
+Proof.
+  exact (@find_symbol_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+Qed.
+
+Theorem init_mem_transf_partial:
+  init_mem p' = init_mem p.
+Proof.
+  exact (@init_mem_transf_partial2 _ _ _ _ _ _ _ _ transf2_OK).
+Qed.
+
+End TRANSF_PROGRAM_PARTIAL.
+
+Section TRANSF_PROGRAM.
+
+Variable A B V: Set.
+Variable transf: A -> B.
+Variable p: program A V.
+Let tp := transform_program transf p.
+
+Remark transf_OK:
+  transform_partial_program (fun x => Some (transf x)) p = Some tp.
+Proof.
+  unfold tp, transform_program, transform_partial_program.
+  rewrite map_partial_total. reflexivity.
 Qed.
 
 Theorem find_funct_ptr_transf:
@@ -605,10 +674,9 @@ Theorem find_funct_ptr_transf:
   find_funct_ptr (globalenv p) b = Some f ->
   find_funct_ptr (globalenv tp) b = Some (transf f).
 Proof.
-  intros.
-  generalize (find_funct_ptr_transf_partial transf_partial p
-                  transform_program_transform_partial_program).
-  intros. elim (H0 b f H). intros. exact H1.
+  intros. 
+  destruct (@find_funct_ptr_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
+  as [X Y]. auto.
 Qed.
 
 Theorem find_funct_transf:
@@ -616,26 +684,22 @@ Theorem find_funct_transf:
   find_funct (globalenv p) v = Some f ->
   find_funct (globalenv tp) v = Some (transf f).
 Proof.
-  intros.
-  generalize (find_funct_transf_partial transf_partial p
-                  transform_program_transform_partial_program).
-  intros. elim (H0 v f H). intros. exact H1.
+  intros. 
+  destruct (@find_funct_transf_partial _ _ _ _ _ _ transf_OK _ _ H)
+  as [X Y]. auto.
 Qed.
 
 Theorem find_symbol_transf:
   forall (s: ident),
   find_symbol (globalenv tp) s = find_symbol (globalenv p) s.
 Proof.
-  intros.
-  apply find_symbol_transf_partial with transf_partial.
-  apply transform_program_transform_partial_program.
+  exact (@find_symbol_transf_partial _ _ _ _ _ _ transf_OK).
 Qed.
 
 Theorem init_mem_transf:
   init_mem tp = init_mem p.
 Proof.
-  apply init_mem_transf_partial with transf_partial.
-  apply transform_program_transform_partial_program.
+  exact (@init_mem_transf_partial _ _ _ _ _ _ transf_OK).
 Qed.
 
 End TRANSF_PROGRAM.