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

23 files changed, 538 insertions, 468 deletions

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 4420269e..79657c55 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -765,13 +765,13 @@ Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_transf _ _ transf_fundef prog).
+Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog).
 
 Lemma funct_ptr_translated:
   forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   Genv.find_funct_ptr tge b = Some (transf_fundef f).
-Proof (@Genv.find_funct_ptr_transf _ _ transf_fundef prog).
+Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog).
 
 Lemma sig_translated:
   forall (f: RTL.fundef),
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 9eed0091..6fdf6028 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -80,7 +80,7 @@ Record function : Set := mkfunction {
 }.
 
 Definition fundef := AST.fundef function.
-Definition program := AST.program fundef.
+Definition program := AST.program fundef unit.
 
 Definition funsig (fd: fundef) :=
   match fd with
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 38ba38b8..ee241873 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -653,13 +653,13 @@ Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_transf _ _ transf_fundef prog).
+Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog).
 
 Lemma function_ptr_translated:
   forall (v: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge v = Some f ->
   Genv.find_funct_ptr tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_ptr_transf _ _ transf_fundef prog).
+Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog).
 
 Lemma sig_translated:
   forall (f: RTL.fundef),
diff --git a/backend/LTL.v b/backend/LTL.v
index f20ba3fc..0dc97020 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -64,7 +64,7 @@ Record function: Set := mkfunction {
 
 Definition fundef := AST.fundef function.
 
-Definition program := AST.program fundef.
+Definition program := AST.program fundef unit.
 
 Definition funsig (fd: fundef) :=
   match fd with
diff --git a/backend/Linear.v b/backend/Linear.v
index 2520f5bf..0f1a31f2 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -54,7 +54,7 @@ Record function: Set := mkfunction {
 
 Definition fundef := AST.fundef function.
 
-Definition program := AST.program fundef.
+Definition program := AST.program fundef unit.
 
 Definition funsig (fd: fundef) :=
   match fd with
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 22bf19c0..5937fc34 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -27,18 +27,18 @@ Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_transf _ _ transf_fundef prog).
+Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog).
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   Genv.find_funct_ptr tge v = Some (transf_fundef f).
-Proof (@Genv.find_funct_ptr_transf _ _ transf_fundef prog).
+Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog).
 
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (@Genv.find_symbol_transf _ _ transf_fundef prog).
+Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog).
 
 Lemma sig_preserved:
   forall f, funsig (transf_fundef f) = LTL.funsig f.
diff --git a/backend/Mach.v b/backend/Mach.v
index 1a9a94ae..75b5baa8 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -61,7 +61,7 @@ Record function: Set := mkfunction
 
 Definition fundef := AST.fundef function.
 
-Definition program := AST.program fundef.
+Definition program := AST.program fundef unit.
 
 Definition funsig (fd: fundef) :=
   match fd with
diff --git a/backend/PPC.v b/backend/PPC.v
index 37f882b3..3aa4ec4f 100644
--- a/backend/PPC.v
+++ b/backend/PPC.v
@@ -286,7 +286,7 @@ lbl:    .long   0x43300000, 0x00000000
 
 Definition code := list instruction.
 Definition fundef := AST.fundef code.
-Definition program := AST.program fundef.
+Definition program := AST.program fundef unit.
 
 (** * Operational semantics *)
 
diff --git a/backend/RTL.v b/backend/RTL.v
index 4a3f8e8c..8b46a7db 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -92,7 +92,7 @@ Record function: Set := mkfunction {
 
 Definition fundef := AST.fundef function.
 
-Definition program := AST.program fundef.
+Definition program := AST.program fundef unit.
 
 Definition funsig (fd: fundef) :=
   match fd with
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 33338d37..449e837a 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -466,10 +466,10 @@ Proof.
   apply wt_regset_assign. auto. rewrite H11. rewrite <- H1.
   assert (wt_fundef f).
     destruct ros; simpl in H0.
-    pattern f. apply Genv.find_funct_prop with fundef p (rs#r).
+    pattern f. apply Genv.find_funct_prop with fundef unit p (rs#r).
     exact wt_p. exact H0. 
     caseEq (Genv.find_symbol ge i); intros; rewrite H12 in H0.
-    pattern f. apply Genv.find_funct_ptr_prop with fundef p b.
+    pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b.
     exact wt_p. exact H0.
     discriminate.
   eapply H3. auto. rewrite H1. rewrite <- H10.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 88547e76..eae53cac 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -84,18 +84,18 @@ Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
   Genv.find_funct tge v = Some (tunnel_fundef f).
-Proof (@Genv.find_funct_transf _ _ tunnel_fundef p).
+Proof (@Genv.find_funct_transf _ _ _ tunnel_fundef p).
 
 Lemma function_ptr_translated:
   forall v f,
   Genv.find_funct_ptr ge v = Some f ->
   Genv.find_funct_ptr tge v = Some (tunnel_fundef f).
-Proof (@Genv.find_funct_ptr_transf _ _ tunnel_fundef p).
+Proof (@Genv.find_funct_ptr_transf _ _ _ tunnel_fundef p).
 
 Lemma symbols_preserved:
   forall id,
   Genv.find_symbol tge id = Genv.find_symbol ge id.
-Proof (@Genv.find_symbol_transf _ _ tunnel_fundef p).
+Proof (@Genv.find_symbol_transf _ _ _ tunnel_fundef p).
 
 Lemma sig_preserved:
   forall f, funsig (tunnel_fundef f) = funsig f.
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 4c611b44..30832e84 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -375,10 +375,10 @@ Definition build_compilenv
     (globenv, 0).
 
 Definition assign_global_variable
-     (ce: compilenv) (info: ident * var_kind * list init_data) : compilenv :=
+     (ce: compilenv) (info: ident * list init_data * var_kind) : compilenv :=
   match info with
-  | (id, Vscalar chunk, _) => PMap.set id (Var_global_scalar chunk) ce
-  | (id, Varray _, _) => PMap.set id Var_global_array ce
+  | (id, _, Vscalar chunk) => PMap.set id (Var_global_scalar chunk) ce
+  | (id, _, Varray _) => PMap.set id Var_global_array ce
   end.
 
 Definition build_global_compilenv (p: Csharpminor.program) : compilenv :=
@@ -428,6 +428,8 @@ Definition transl_function
 Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): option fundef :=
   transf_partial_fundef (transl_function gce) f.
 
+Definition transl_globvar (vk: var_kind) := Some tt.
+
 Definition transl_program (p: Csharpminor.program) : option program :=
   let gce := build_global_compilenv p in
-  transform_partial_program (transl_fundef gce) (program_of_program p).
+  transform_partial_program2 (transl_fundef gce) transl_globvar p.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 7820095a..66d0efff 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -22,7 +22,7 @@ Section TRANSLATION.
 Variable prog: Csharpminor.program.
 Variable tprog: program.
 Hypothesis TRANSL: transl_program prog = Some tprog.
-Let ge : Csharpminor.genv := Genv.globalenv (program_of_program prog).
+Let ge : Csharpminor.genv := Genv.globalenv prog.
 Let tge: genv := Genv.globalenv tprog.
 Let gce : compilenv := build_global_compilenv prog.
 
@@ -30,7 +30,7 @@ Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
   intro. unfold ge, tge. 
-  apply Genv.find_symbol_transf_partial with (transl_fundef gce).
+  apply Genv.find_symbol_transf_partial2 with (transl_fundef gce) transl_globvar.
   exact TRANSL.
 Qed.
 
@@ -42,7 +42,7 @@ Lemma function_ptr_translated:
 Proof.
   intros. 
   generalize 
-   (Genv.find_funct_ptr_transf_partial (transl_fundef gce) TRANSL H).
+   (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar TRANSL H).
   case (transl_fundef gce f).
   intros tf [A B]. exists tf. tauto.
   intros [A B]. elim B. reflexivity.
@@ -56,7 +56,7 @@ Lemma functions_translated:
 Proof.
   intros. 
   generalize 
-   (Genv.find_funct_transf_partial (transl_fundef gce) TRANSL H).
+   (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL H).
   case (transl_fundef gce f).
   intros tf [A B]. exists tf. tauto.
   intros [A B]. elim B. reflexivity.
@@ -86,9 +86,9 @@ Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop :=
 Lemma global_compilenv_charact:
   global_compilenv_match gce (global_var_env prog).
 Proof.
-  set (mkgve := fun gv (vars: list (ident * var_kind * list init_data)) =>
+  set (mkgve := fun gv (vars: list (ident * list init_data * var_kind)) =>
          List.fold_left
-          (fun gve x => match x with (id, k, init) => PTree.set id k gve end)
+          (fun gve x => match x with (id, init, k) => PTree.set id k gve end)
           vars gv).
   assert (forall vars gv ce,
             global_compilenv_match ce gv ->
@@ -97,11 +97,11 @@ Proof.
   induction vars; simpl; intros.
   auto.
   apply IHvars. intro id1. unfold assign_global_variable.
-  destruct a as [[id2 lv2] init2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec.
+  destruct a as [[id2 init2] lv2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec.
   case (peq id1 id2); intro. auto. apply H. 
   case (peq id1 id2); intro. auto. apply H.
 
-  change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(Csharpminor.prog_vars)).
+  change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(prog_vars)).
   unfold gce, build_global_compilenv. apply H. 
   intro. rewrite PMap.gi. auto.
 Qed.
@@ -2534,7 +2534,7 @@ Proof
   of the source program and the transformed program. *)
 
 Lemma match_globalenvs_init:
-  let m := Genv.init_mem (program_of_program prog) in
+  let m := Genv.init_mem prog in
   let tm := Genv.init_mem tprog in
   let f := fun b => if zlt b m.(nextblock) then Some(b, 0) else None in
   match_globalenvs f.
@@ -2560,7 +2560,7 @@ Theorem transl_program_correct:
 Proof.
   intros t n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]].
   elim (function_ptr_translated _ _ FINDF). intros tfn [TFIND TR].
-  set (m0 := Genv.init_mem (program_of_program prog)) in *.
+  set (m0 := Genv.init_mem prog) in *.
   set (f := fun b => if zlt b m0.(nextblock) then Some(b, 0) else None).
   assert (MINJ0: mem_inject f m0 m0).
     unfold f; constructor; intros.
@@ -2570,7 +2570,7 @@ Proof.
     split. auto. 
     constructor. compute. split; congruence. left; auto. 
     intros; omega. 
-    generalize (Genv.initmem_block_init (program_of_program prog) b0). fold m0. intros [idata EQ].
+    generalize (Genv.initmem_block_init prog b0). fold m0. intros [idata EQ].
     rewrite EQ. simpl. apply Mem.contents_init_data_inject. 
     destruct (zlt b1 (nextblock m0)); try discriminate.
     destruct (zlt b2 (nextblock m0)); try discriminate.
@@ -2583,12 +2583,10 @@ Proof.
   exists b; exists tfn; exists tm1.
   split. fold tge. rewrite <- FINDS. 
   replace (prog_main prog) with (AST.prog_main tprog). fold ge. apply symbols_preserved.
-  transitivity (AST.prog_main (program_of_program prog)).
-  apply transform_partial_program_main with (transl_fundef gce). assumption.
-  reflexivity.
+  apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption.
   split. assumption.
   split. rewrite <- SIG. apply sig_preserved; auto.
-  rewrite (Genv.init_mem_transf_partial (transl_fundef gce) _ TRANSL).
+  rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL).
   inversion VINJ; subst tres. assumption. 
 Qed.
 
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index b73e83cc..ed5a1b4c 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -367,12 +367,6 @@ Inductive cast : val -> type -> type -> val -> Prop :=
 
 Definition genv := Genv.t fundef.
 
-Definition globalenv (p: program) : genv :=
-  Genv.globalenv (program_of_program p).
-
-Definition init_mem (p: program) : mem :=  
-  Genv.init_mem (program_of_program p).
-
 (** Local environment *)
 
 Definition env := PTree.t block. (* map variable -> location *)
@@ -743,8 +737,8 @@ End RELSEM.
 (** Execution of a whole program *)
 
 Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
-  let ge := globalenv p in 
-  let m0 := init_mem p in
+  let ge := Genv.globalenv p in 
+  let m0 := Genv.init_mem p in
   exists b, exists f, exists m1,
   Genv.find_symbol ge p.(prog_main) = Some b /\
   Genv.find_funct_ptr ge b = Some f /\
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index 246ebf53..016fab4d 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -122,11 +122,7 @@ Record function : Set := mkfunction {
 
 Definition fundef := AST.fundef function.
 
-Record program : Set := mkprogram {
-  prog_funct: list (ident * fundef);
-  prog_main: ident;
-  prog_vars: list (ident * var_kind * list init_data)
-}.
+Definition program : Set := AST.program fundef var_kind.
 
 Definition funsig (fd: fundef) :=
   match fd with
@@ -187,12 +183,6 @@ Definition sizeof (lv: var_kind) : Z :=
   | Varray sz => Zmax 0 sz
   end.
 
-Definition program_of_program (p: program): AST.program fundef :=
-  AST.mkprogram
-    p.(prog_funct)
-    p.(prog_main)
-    (List.map (fun x => match x with (id, k, init) => (id, init) end) p.(prog_vars)).
-
 Definition fn_variables (f: function) :=
   List.map
     (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) f.(fn_params)
@@ -206,7 +196,7 @@ Definition fn_vars_names (f: function) :=
 
 Definition global_var_env (p: program): gvarenv :=
   List.fold_left
-    (fun gve x => match x with (id, k, init) => PTree.set id k gve end)
+    (fun gve x => match x with (id, init, k) => PTree.set id k gve end)
     p.(prog_vars) (PTree.empty var_kind).
 
 (** Evaluation of operator applications. *)
@@ -316,7 +306,7 @@ Inductive bind_parameters: env ->
 Section RELSEM.
 
 Variable prg: program.
-Let ge := Genv.globalenv (program_of_program prg).
+Let ge := Genv.globalenv prg.
 
 (* Evaluation of the address of a variable: 
    [eval_var_addr prg ge e id b] states that variable [id] 
@@ -554,8 +544,8 @@ End RELSEM.
   in the initial memory state for [p] eventually returns value [r]. *)
 
 Definition exec_program (p: program) (t: trace) (r: val) : Prop :=
-  let ge := Genv.globalenv (program_of_program p) in
-  let m0 := Genv.init_mem (program_of_program p) in
+  let ge := Genv.globalenv p in
+  let m0 := Genv.init_mem p in
   exists b, exists f, exists m,
   Genv.find_symbol ge p.(prog_main) = Some b /\
   Genv.find_funct_ptr ge b = Some f /\
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 58c0bb8f..5585416b 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -562,8 +562,10 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt)
 
 (*** Translation of functions *)
 
-Definition transl_params := transf_partial_program chunk_of_type.
-Definition transl_vars := transf_partial_program var_kind_of_type.
+Definition transl_params (l: list (ident * type)) :=
+   AST.map_partial chunk_of_type l.
+Definition transl_vars (l: list (ident * type)) :=
+   AST.map_partial var_kind_of_type l.
 
 Definition transl_function (f: Csyntax.function) : option function :=
   do tparams <- transl_params (Csyntax.fn_params f);
@@ -581,18 +583,7 @@ Definition transl_fundef (f: Csyntax.fundef) : option fundef :=
 
 (** ** Translation of programs *)
 
-Fixpoint transl_global_vars
-      (vl: list (ident * type * list init_data)) :
-      option (list (ident * var_kind * list init_data)) :=
-  match vl with
-  | nil => Some nil
-  | (id, ty, init) :: rem =>
-      do vk <- var_kind_of_type ty;
-      do trem <- transl_global_vars rem;
-      Some ((id, vk, init) :: trem)
-  end.
+Definition transl_globvar (ty: type) := var_kind_of_type ty.
 
 Definition transl_program (p: Csyntax.program) : option program :=
-  do tfun <- transf_partial_program transl_fundef (Csyntax.prog_funct p);
-  do tvars <- transl_global_vars (Csyntax.prog_defs p);
-  Some (mkprogram tfun (Csyntax.prog_main p) tvars).
+  transform_partial_program2 transl_fundef transl_globvar p.
diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v
index 17f7aa92..bee07824 100644
--- a/cfrontend/Cshmgenproof1.v
+++ b/cfrontend/Cshmgenproof1.v
@@ -100,50 +100,32 @@ Proof.
   simpl; intro EQ; inversion EQ; subst vk; auto.
 Qed.
 
-(** Transformation of programs and functions *)
-
-Lemma transform_program_of_program:
-  forall prog tprog,
-  transl_program prog = Some tprog ->
-  transform_partial_program transl_fundef (Csyntax.program_of_program prog) =
-  Some (program_of_program tprog).
-Proof.
-  intros prog tprog TRANSL.  
-  monadInv TRANSL. rewrite <- H0. unfold program_of_program; simpl. 
-  unfold transform_partial_program, Csyntax.program_of_program; simpl.
-  rewrite EQ. decEq. decEq. 
-  generalize EQ0. generalize l0. generalize (prog_defs prog).
-  induction l1; simpl; intros. 
-  inversion EQ1; subst l1. reflexivity.
-  destruct a as [[id ty] init]. monadInv EQ1. subst l2. simpl. decEq. apply IHl1. auto. 
-Qed.
-
 (** ** Some properties of the translation functions *)
 
-Lemma transf_partial_program_names:
+Lemma map_partial_names:
   forall (A B: Set) (f: A -> option B)
          (l: list (ident * A)) (tl: list (ident * B)),
-  transf_partial_program f l = Some tl ->
+  map_partial f l = Some tl ->
   List.map (@fst ident B) tl = List.map (@fst ident A) l.
 Proof.
   induction l; simpl.
   intros. inversion H. reflexivity.
   intro tl. destruct a as [id x]. destruct (f x); try congruence.
-  caseEq (transf_partial_program f l); intros; try congruence.
+  caseEq (map_partial f l); intros; try congruence.
   inversion H0; subst tl. simpl. decEq. auto.
 Qed.
    
-Lemma transf_partial_program_append:
+Lemma map_partial_append:
   forall (A B: Set) (f: A -> option B)
          (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)),
-  transf_partial_program f l1 = Some tl1 ->
-  transf_partial_program f l2 = Some tl2 ->
-  transf_partial_program f (l1 ++ l2) = Some (tl1 ++ tl2).
+  map_partial f l1 = Some tl1 ->
+  map_partial f l2 = Some tl2 ->
+  map_partial f (l1 ++ l2) = Some (tl1 ++ tl2).
 Proof.
   induction l1; intros until tl2; simpl.
   intros. inversion H. simpl; auto.
   destruct a as [id x]. destruct (f x); try congruence.
-  caseEq (transf_partial_program f l1); intros; try congruence.
+  caseEq (map_partial f l1); intros; try congruence.
   inversion H0. rewrite (IHl1 _ _ _ H H1). auto.
 Qed.
  
@@ -152,7 +134,7 @@ Lemma transl_params_names:
   transl_params vars = Some tvars ->
   List.map (@fst ident memory_chunk) tvars = Ctyping.var_names vars.
 Proof.
-  exact (transf_partial_program_names _ _ chunk_of_type).
+  exact (map_partial_names _ _ chunk_of_type).
 Qed.
 
 Lemma transl_vars_names:
@@ -160,7 +142,7 @@ Lemma transl_vars_names:
   transl_vars vars = Some tvars ->
   List.map (@fst ident var_kind) tvars = Ctyping.var_names vars.
 Proof.
-  exact (transf_partial_program_names _ _ var_kind_of_type).
+  exact (map_partial_names _ _ var_kind_of_type).
 Qed.
 
 Lemma transl_names_norepet:
@@ -182,7 +164,7 @@ Lemma transl_vars_append:
   transl_vars l1 = Some tl1 -> transl_vars l2 = Some tl2 ->
   transl_vars (l1 ++ l2) = Some (tl1 ++ tl2).
 Proof.
-  exact (transf_partial_program_append _ _ var_kind_of_type).
+  exact (map_partial_append _ _ var_kind_of_type).
 Qed.
 
 Lemma transl_params_vars:
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v
index b33771b5..5037d43f 100644
--- a/cfrontend/Cshmgenproof3.v
+++ b/cfrontend/Cshmgenproof3.v
@@ -24,15 +24,15 @@ Variable tprog: Csharpminor.program.
 Hypothesis WTPROG: wt_program prog.
 Hypothesis TRANSL: transl_program prog = Some tprog.
 
-Let ge := Csem.globalenv prog.
-Let tge := Genv.globalenv (Csharpminor.program_of_program tprog).
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
-  intros. unfold ge, Csem.globalenv, tge. 
-  apply Genv.find_symbol_transf_partial with transl_fundef.
-  apply transform_program_of_program; auto.
+  intros. unfold ge, tge. 
+  apply Genv.find_symbol_transf_partial2 with transl_fundef transl_globvar.
+  auto.
 Qed.
 
 Lemma functions_translated:
@@ -41,7 +41,7 @@ Lemma functions_translated:
   exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = Some tf.
 Proof.
   intros. 
-  generalize (Genv.find_funct_transf_partial transl_fundef (transform_program_of_program _ _ TRANSL) H).
+  generalize (Genv.find_funct_transf_partial2 transl_fundef transl_globvar TRANSL H).
   intros [A B]. 
   destruct (transl_fundef f). exists f0; split. assumption. auto. congruence.
 Qed.
@@ -52,7 +52,7 @@ Lemma function_ptr_translated:
   exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Some tf.
 Proof.
   intros. 
-  generalize (Genv.find_funct_ptr_transf_partial transl_fundef (transform_program_of_program _ _ TRANSL) H).
+  generalize (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar TRANSL H).
   intros [A B]. 
   destruct (transl_fundef f). exists f0; split. assumption. auto. congruence.
 Qed.
@@ -63,8 +63,7 @@ Lemma functions_well_typed:
   wt_fundef (global_typenv prog) f.
 Proof.
   intros. inversion WTPROG. 
-  apply (@Genv.find_funct_prop _ (wt_fundef (global_typenv prog)) 
-                               (Csyntax.program_of_program prog) v f).
+  apply (@Genv.find_funct_prop _ _ (wt_fundef (global_typenv prog)) prog v f).
   intros. apply wt_program_funct with id. assumption.
   assumption.
 Qed.
@@ -75,8 +74,7 @@ Lemma function_ptr_well_typed:
   wt_fundef (global_typenv prog) f.
 Proof.
   intros. inversion WTPROG. 
-  apply (@Genv.find_funct_ptr_prop _ (wt_fundef (global_typenv prog)) 
-                               (Csyntax.program_of_program prog) b f).
+  apply (@Genv.find_funct_ptr_prop _ _ (wt_fundef (global_typenv prog)) prog b f).
   intros. apply wt_program_funct with id. assumption.
   assumption.
 Qed.
@@ -230,9 +228,9 @@ Qed.
 
 Definition globvarenv 
     (gv: gvarenv)
-    (vars: list (ident * var_kind * list init_data)) :=
+    (vars: list (ident * list init_data * var_kind)) :=
   List.fold_left
-    (fun gve x => match x with (id, k, init) => PTree.set id k gve end)
+    (fun gve x => match x with (id, init, k) => PTree.set id k gve end)
     vars gv.
 
 Definition type_not_by_value (ty: type) : Prop :=
@@ -259,14 +257,14 @@ Proof.
 Qed.
 
 Definition global_fun_typenv :=
-  add_global_funs (PTree.empty type) (Csyntax.prog_funct prog).
+  add_global_funs (PTree.empty type) prog.(prog_funct).
 
 Lemma add_global_funs_match_global_env:
   match_globalenv global_fun_typenv (PTree.empty var_kind).
 Proof.
   intros; red; intros.
   assert (type_not_by_value ty).
-    apply add_global_funs_charact with (Csyntax.prog_funct prog) (PTree.empty type) id.
+    apply add_global_funs_charact with (prog_funct prog) (PTree.empty type) id.
     intros until ty0. rewrite PTree.gempty. congruence.
     assumption.
   red in H1. rewrite H0 in H1. contradiction.
@@ -275,17 +273,21 @@ Qed.
 Lemma add_global_var_match_globalenv:
   forall vars tenv gv tvars,
   match_globalenv tenv gv ->
-  transl_global_vars vars = Some tvars ->
+  map_partial transl_globvar vars = Some tvars ->
   match_globalenv (add_global_vars tenv vars) (globvarenv gv tvars).
 Proof.
-  induction vars; intros; simpl.
-  simpl in H0. inversion H0. simpl. auto.
-  destruct a as [[id ty] init]. monadInv H0. subst tvars.
-  simpl. apply IHvars; auto.
+  induction vars; simpl.
+  intros. inversion H0. assumption.
+  destruct a as [[id init] ty]. intros until tvars; intro.
+  caseEq (transl_globvar ty); try congruence. intros vk VK. 
+  caseEq (map_partial transl_globvar vars); try congruence. intros tvars' EQ1 EQ2.
+  inversion EQ2; clear EQ2. simpl. 
+  apply IHvars; auto.
   red. intros until chunk. repeat rewrite PTree.gsspec. 
   destruct (peq id0 id); intros.
-  inversion H1; clear H1; subst id0 ty0. 
-  generalize (var_kind_by_value _ _ H2). congruence.
+  inversion H0; clear H0; subst id0 ty0. 
+  generalize (var_kind_by_value _ _ H2). 
+  unfold transl_globvar in VK. congruence.
   red in H. eauto. 
 Qed.
 
@@ -297,7 +299,7 @@ Proof.
   unfold global_typenv.
   apply add_global_var_match_globalenv.
   apply add_global_funs_match_global_env. 
-  monadInv TRANSL. rewrite <- H0. reflexivity.
+  unfold transl_program in TRANSL. functional inversion TRANSL. auto.
 Qed.
 
 (** ** Variable accessors *)
@@ -1481,23 +1483,18 @@ Proof.
   
   assert (type_of_fundef f = Tfunction Tnil (Tint I32 Signed)).
     apply wt_program_main.
-    change (Csyntax.prog_funct prog)
-      with (AST.prog_funct (Csyntax.program_of_program prog)).
     eapply Genv.find_funct_ptr_symbol_inversion; eauto. 
   exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]].
   exists b; exists tf; exists m1.
   split. 
     rewrite (symbols_preserved _ _ TRANSL).
-    monadInv TRANSL. rewrite <- H1. simpl. auto.
+    rewrite (transform_partial_program2_main transl_fundef transl_globvar prog TRANSL). auto.
   split. auto.
   split. 
     generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD H). simpl; auto.
-  rewrite (@Genv.init_mem_transf_partial _ _ transl_fundef 
-             (Csyntax.program_of_program prog)
-             (Csharpminor.program_of_program tprog)).
+  rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL).
   generalize (transl_funcall_correct _ _ WT TRANSL _ _ _ _ _ _ EVAL).
   intro. eapply H0. 
   eapply function_ptr_well_typed; eauto.
   auto.
-  apply transform_program_of_program; auto.
 Qed.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index d3bd8d6f..979d0bca 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -130,11 +130,7 @@ Inductive fundef : Set :=
 
 (** Program *)
 
-Record program : Set := mkprogram {
-    prog_funct: list (ident * fundef);
-    prog_defs: list (ident * type * list init_data);
-    prog_main: ident
-}.
+Definition program : Set := AST.program fundef type.
 
 (** ** Operations over types *)
 
@@ -293,17 +289,6 @@ Definition access_mode (ty: type) : mode :=
   | Tunion fList => By_nothing
 end.
 
-(** Conversion of a Clight program into an AST program *)
-
-Definition extract_global_var (id_ty_init: ident * type * list init_data) :=
-  match id_ty_init with (id, ty, init) => (id, init) end.
-
-Definition program_of_program (p: program) : AST.program fundef :=
-  AST.mkprogram
-    p.(prog_funct)
-    p.(prog_main)
-    (List.map extract_global_var p.(prog_defs)).
-
 (** Classification of arithmetic operations and comparisons *)
 
 Inductive classify_add_cases : Set :=
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 8b2f90f2..7c6a3790 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -136,11 +136,11 @@ Inductive wt_fundef: typenv -> fundef -> Prop :=
       wt_fundef env (External id args res).
 
 Definition add_global_var
-     (env: typenv) (id_ty_init: ident * type * list init_data) : typenv :=
-  match id_ty_init with (id, ty, init) => PTree.set id ty env end.
+     (env: typenv) (id_ty_init: ident * list init_data * type) : typenv :=
+  match id_ty_init with (id, init, ty) => PTree.set id ty env end.
 
 Definition add_global_vars
-     (env: typenv) (vars: list(ident * type * list init_data)) : typenv :=
+     (env: typenv) (vars: list(ident * list init_data * type)) : typenv :=
   List.fold_left add_global_var vars env.
 
 Definition add_global_fun
@@ -152,7 +152,7 @@ Definition add_global_funs
   List.fold_left add_global_fun funs env.
 
 Definition global_typenv (p: program) :=
-  add_global_vars (add_global_funs (PTree.empty type) p.(prog_funct)) p.(prog_defs).
+  add_global_vars (add_global_funs (PTree.empty type) p.(prog_funct)) p.(prog_vars).
 
 Record wt_program (p: program) : Prop :=  mk_wt_program {
   wt_program_funct:
diff --git a/common/AST.v b/common/AST.v
index 1342bef1..673f1d81 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -67,16 +67,18 @@ Inductive init_data: Set :=
 (** Whole programs consist of:
 - a collection of function definitions (name and description);
 - the name of the ``main'' function that serves as entry point in the program;
-- a collection of global variable declarations (name and initializer).
+- a collection of global variable declarations, consisting of
+  a name, initialization data, and additional information.
 
-The type of function descriptions varies among the various intermediate
-languages and is taken as parameter to the [program] type.  The other parts
-of whole programs are common to all languages. *)
+The type of function descriptions and that of additional information
+for variables vary among the various intermediate languages and are
+taken as parameters to the [program] type.  The other parts of whole
+programs are common to all languages. *)
 
-Record program (funct: Set) : Set := mkprogram {
-  prog_funct: list (ident * funct);
+Record program (F V: Set) : Set := mkprogram {
+  prog_funct: list (ident * F);
   prog_main: ident;
-  prog_vars: list (ident * list init_data)
+  prog_vars: list (ident * list init_data * V)
 }.
 
 (** We now define a general iterator over programs that applies a given
@@ -85,40 +87,27 @@ Record program (funct: Set) : Set := mkprogram {
 
 Section TRANSF_PROGRAM.
 
-Variable A B: Set.
+Variable A B V: Set.
 Variable transf: A -> B.
 
-Fixpoint transf_program (l: list (ident * A)) : list (ident * B) :=
-  match l with
-  | nil => nil
-  | (id, fn) :: rem => (id, transf fn) :: transf_program rem
-  end.
+Definition transf_program (l: list (ident * A)) : list (ident * B) :=
+  List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l.
 
-Definition transform_program (p: program A) : program B :=
+Definition transform_program (p: program A V) : program B V :=
   mkprogram
     (transf_program p.(prog_funct))
     p.(prog_main)
     p.(prog_vars).
 
-Remark transf_program_functions:
-  forall fl i tf,
-  In (i, tf) (transf_program fl) ->
-  exists f, In (i, f) fl /\ transf f = tf.
-Proof.
-  induction fl; simpl.
-  tauto.
-  destruct a. simpl. intros.
-  elim H; intro. exists a. split. left. congruence. congruence.
-  generalize (IHfl _ _ H0). intros [f [IN TR]].
-  exists f. split. right. auto. auto.
-Qed.
-
 Lemma transform_program_function:
   forall p i tf,
   In (i, tf) (transform_program p).(prog_funct) ->
   exists f, In (i, f) p.(prog_funct) /\ transf f = tf.
 Proof.
-  simpl. intros. eapply transf_program_functions; eauto.
+  simpl. unfold transf_program. intros.
+  exploit list_in_map_inv; eauto. 
+  intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst. 
+  exists f; split; auto.
 Qed.
 
 End TRANSF_PROGRAM.
@@ -127,66 +116,83 @@ End TRANSF_PROGRAM.
   code transformation function can fail and therefore returns an
   option type. *)
 
-Section TRANSF_PARTIAL_PROGRAM.
+Section MAP_PARTIAL.
 
-Variable A B: Set.
-Variable transf_partial: A -> option B.
+Variable A B C: Set.
+Variable f: B -> option C.
 
-Fixpoint transf_partial_program
-            (l: list (ident * A)) : option (list (ident * B)) :=
+Fixpoint map_partial (l: list (A * B)) : option (list (A * C)) :=
   match l with
   | nil => Some nil
-  | (id, fn) :: rem =>
-      match transf_partial fn with
+  | (a, b) :: rem =>
+      match f b with
       | None => None
-      | Some fn' =>
-          match transf_partial_program rem with
+      | Some c =>
+          match map_partial rem with
           | None => None
-          | Some res => Some ((id, fn') :: res)
+          | Some res => Some ((a, c) :: res)
           end
       end
   end.
 
-Definition transform_partial_program (p: program A) : option (program B) :=
-  match transf_partial_program p.(prog_funct) with
-  | None => None
-  | Some fl => Some (mkprogram fl p.(prog_main) p.(prog_vars))
-  end.
+Remark In_map_partial:
+  forall l l' a c,
+  map_partial l = Some l' ->
+  In (a, c) l' ->
+  exists b, In (a, b) l /\ f b = Some c.
+Proof.
+  induction l; simpl.
+  intros. inversion H; subst. elim H0.
+  destruct a as [a1 b1]. intros until c.
+  caseEq (f b1); try congruence.
+  intros c1 EQ1. caseEq (map_partial l); try congruence.
+  intros res EQ2 EQ3 IN. inversion EQ3; clear EQ3; subst l'.
+  elim IN; intro. inversion H; subst. 
+  exists b1; auto.
+  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
+Qed.
 
-Remark transf_partial_program_functions:
-  forall fl tfl i tf,
-  transf_partial_program fl = Some tfl ->
-  In (i, tf) tfl ->
-  exists f, In (i, f) fl /\ transf_partial f = Some tf.
+End MAP_PARTIAL.
+
+Remark map_partial_total:
+  forall (A B C: Set) (f: B -> C) (l: list (A * B)),
+  map_partial (fun b => Some (f b)) l =
+  Some (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
+Proof.
+  induction l; simpl.
+  auto.
+  destruct a as [a1 b1]. rewrite IHl. reflexivity.
+Qed.
+
+Remark map_partial_identity:
+  forall (A B: Set) (l: list (A * B)),
+  map_partial (fun b => Some b) l = Some l.
 Proof.
-  induction fl; simpl.
-  intros; injection H; intro; subst tfl; contradiction.
-  case a; intros id fn. intros until tf.
-  caseEq (transf_partial fn).
-  intros tfn TFN.
-  caseEq (transf_partial_program fl).
-  intros tfl1 TFL1 EQ. injection EQ; intro; clear EQ; subst tfl.
-  simpl.  intros [EQ1|IN1].
-  exists fn. intuition congruence.
-  generalize (IHfl _ _ _ TFL1 IN1).
-  intros [f [X Y]].
-  exists f. intuition congruence.
-  intros; discriminate.
-  intros; discriminate.
+  induction l; simpl.
+  auto.
+  destruct a as [a1 b1]. rewrite IHl. reflexivity.
 Qed.
 
+Section TRANSF_PARTIAL_PROGRAM.
+
+Variable A B V: Set.
+Variable transf_partial: A -> option B.
+
+Function transform_partial_program (p: program A V) : option (program B V) :=
+  match map_partial transf_partial p.(prog_funct) with
+  | None => None
+  | Some fl => Some (mkprogram fl p.(prog_main) p.(prog_vars))
+  end.
+
 Lemma transform_partial_program_function:
   forall p tp i tf,
   transform_partial_program p = Some tp ->
   In (i, tf) tp.(prog_funct) ->
   exists f, In (i, f) p.(prog_funct) /\ transf_partial f = Some tf.
 Proof.
-  intros until tf.
-  unfold transform_partial_program.
-  caseEq (transf_partial_program (prog_funct p)).
-  intros. apply transf_partial_program_functions with l; auto.
-  injection H0; intros; subst tp. exact H1.
-  intros; discriminate.
+  intros. functional inversion H. 
+  apply In_map_partial with fl; auto. 
+  inversion H; subst tp; assumption.
 Qed.
 
 Lemma transform_partial_program_main:
@@ -194,14 +200,69 @@ Lemma transform_partial_program_main:
   transform_partial_program p = Some tp ->
   tp.(prog_main) = p.(prog_main).
 Proof.
-  intros p tp. unfold transform_partial_program.
-  destruct (transf_partial_program (prog_funct p)).
-  intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; reflexivity.
-  intro; discriminate.
+  intros. functional inversion H. reflexivity.
+Qed.
+
+Lemma transform_partial_program_vars:
+  forall p tp,
+  transform_partial_program p = Some tp ->
+  tp.(prog_vars) = p.(prog_vars).
+Proof.
+  intros. functional inversion H. reflexivity.
 Qed.
 
 End TRANSF_PARTIAL_PROGRAM.
 
+(** The following is a variant of [transform_program_partial] where
+  both the program functions and the additional variable information
+  are transformed by functions that can fail. *)
+
+Section TRANSF_PARTIAL_PROGRAM2.
+
+Variable A B V W: Set.
+Variable transf_partial_function: A -> option B.
+Variable transf_partial_variable: V -> option W.
+
+Function transform_partial_program2 (p: program A V) : option (program B W) :=
+  match map_partial transf_partial_function p.(prog_funct) with
+  | None => None
+  | Some fl =>
+      match map_partial transf_partial_variable p.(prog_vars) with
+      | None => None
+      | Some vl => Some (mkprogram fl p.(prog_main) vl)
+      end
+  end.
+
+Lemma transform_partial_program2_function:
+  forall p tp i tf,
+  transform_partial_program2 p = Some tp ->
+  In (i, tf) tp.(prog_funct) ->
+  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = Some tf.
+Proof.
+  intros. functional inversion H. 
+  apply In_map_partial with fl. auto. subst tp; assumption.
+Qed.
+
+Lemma transform_partial_program2_variable:
+  forall p tp i tv,
+  transform_partial_program2 p = Some tp ->
+  In (i, tv) tp.(prog_vars) ->
+  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = Some tv.
+Proof.
+  intros. functional inversion H. 
+  apply In_map_partial with vl. auto. subst tp; assumption.
+Qed.
+
+Lemma transform_partial_program2_main:
+  forall p tp,
+  transform_partial_program2 p = Some tp ->
+  tp.(prog_main) = p.(prog_main).
+Proof.
+  intros. functional inversion H. reflexivity.
+Qed.
+
+End TRANSF_PARTIAL_PROGRAM2.
+
 (** For most languages, the functions composing the program are either
   internal functions, defined within the language, or external functions
   (a.k.a. system calls) that emit an event when applied.  We define
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.
diff --git a/common/Main.v b/common/Main.v
index 95dc4e6c..f472ec3a 100644
--- a/common/Main.v
+++ b/common/Main.v
@@ -6,6 +6,8 @@ Require Import Maps.
 Require Import AST.
 Require Import Values.
 (** Languages (syntax and semantics). *)
+Require Csyntax.
+Require Csem.
 Require Csharpminor.
 Require Cminor.
 Require RTL.
@@ -14,6 +16,7 @@ Require Linear.
 Require Mach.
 Require PPC.
 (** Translation passes. *)
+Require Cshmgen.
 Require Cminorgen.
 Require RTLgen.
 Require Constprop.
@@ -24,11 +27,13 @@ Require Linearize.
 Require Stacking.
 Require PPCgen.
 (** Type systems. *)
+Require Ctyping.
 Require RTLtyping.
 Require LTLtyping.
 Require Lineartyping.
 Require Machtyping.
 (** Proofs of semantic preservation and typing preservation. *)
+Require Cshmgenproof3.
 Require Cminorgenproof.
 Require RTLgenproof.
 Require Constpropproof.
@@ -62,12 +67,9 @@ Notation "a @@ b" :=
    (apply_total _ _ a b) (at level 50, left associativity).
 
 (** We define two translation functions for whole programs: one starting with
-  a Csharpminor program, the other with a Cminor program.  Both
+  a C program, the other with a Cminor program.  Both
   translations produce PPC programs ready for pretty-printing and
-  assembling.  Some front-ends will prefer to generate Csharpminor
-  (e.g. a C front-end) while some others (e.g. an ML compiler) might
-  find it more convenient to generate Cminor directly, bypassing
-  Csharpminor.
+  assembling.  
 
   There are two ways to compose the compiler passes.  The first translates
   every function from the Cminor program from Cminor to RTL, then to LTL, etc,
@@ -89,24 +91,20 @@ Definition transf_cminor_fundef (f: Cminor.fundef) : option PPC.fundef :=
   @@@ Stacking.transf_fundef
   @@@ PPCgen.transf_fundef.
 
-(** And here is the translation for Csharpminor functions. *)
-
-Definition transf_csharpminor_fundef
-     (gce: Cminorgen.compilenv) (f: Csharpminor.fundef) : option PPC.fundef :=
-  Some f 
-  @@@ Cminorgen.transl_fundef gce
-  @@@ transf_cminor_fundef.
-
 (** The corresponding translations for whole program follow. *)
 
 Definition transf_cminor_program (p: Cminor.program) : option PPC.program :=
   transform_partial_program transf_cminor_fundef p.
 
-Definition transf_csharpminor_program (p: Csharpminor.program) : option PPC.program :=
-  let gce := Cminorgen.build_global_compilenv p in
-  transform_partial_program 
-    (transf_csharpminor_fundef gce)
-    (Csharpminor.program_of_program p).
+Definition transf_c_program (p: Csyntax.program) : option PPC.program :=
+  match Ctyping.typecheck_program p with
+  | false => None
+  | true =>
+      Some p 
+      @@@ Cshmgen.transl_program
+      @@@ Cminorgen.transl_program
+      @@@ transf_cminor_program
+  end.
 
 (** * Equivalence with whole program transformations *)
 
@@ -126,23 +124,18 @@ Definition transf_cminor_program2 (p: Cminor.program) : option PPC.program :=
   @@@ Stacking.transf_program
   @@@ PPCgen.transf_program.
 
-Definition transf_csharpminor_program2 (p: Csharpminor.program) : option PPC.program :=
-  Some p
-  @@@ Cminorgen.transl_program
-  @@@ transf_cminor_program2.
-
-Lemma transf_partial_program_compose:
-  forall (A B C: Set)
+Lemma map_partial_compose:
+  forall (X A B C: Set)
          (f1: A -> option B) (f2: B -> option C)
-         (p: list (ident * A)),
-  transf_partial_program f1 p @@@ transf_partial_program f2 =
-  transf_partial_program (fun f => f1 f @@@ f2) p.
+         (p: list (X * A)),
+  map_partial f1 p @@@ map_partial f2 =
+  map_partial (fun f => f1 f @@@ f2) p.
 Proof.
   induction p. simpl. auto.
   simpl. destruct a. destruct (f1 a). 
-  simpl. simpl in IHp. destruct (transf_partial_program f1 p).
+  simpl. simpl in IHp. destruct (map_partial f1 p).
   simpl. simpl in IHp. destruct (f2 b).
-  destruct (transf_partial_program f2 l). 
+  destruct (map_partial f2 l). 
   rewrite <- IHp. auto.
   rewrite <- IHp. auto.
   auto.
@@ -150,40 +143,67 @@ Proof.
   simpl. auto.
 Qed.
 
+(*
+Lemma transform_partial_program2_compose:
+  forall (A B C V W X: Set)
+         (f1: A -> option B) (g1: V -> option W)
+         (f2: B -> option C) (g2: W -> option X)
+         (p: program A V),
+  transform_partial_program2 f1 g1 p @@@
+                  (fun p' => transform_partial_program2 f2 g2 p') =
+  transform_partial_program2 (fun x => f1 x @@@ f2) (fun x => g1 x @@@ g2) p.
+Proof.
+  unfold transform_partial_program2; intros.
+  rewrite <- map_partial_compose; simpl.
+  rewrite <- map_partial_compose; simpl.
+  destruct (map_partial f1 (prog_funct p)); simpl; auto.
+  destruct (map_partial g1 (prog_vars p)); simpl; auto.
+  destruct (map_partial f2 l); auto.
+Qed.
+
+Lemma transform_program_partial2_partial:
+  forall (A B V: Set) (f: A -> option B) (p: program A V),
+  transform_partial_program f p =
+  transform_partial_program2 f (fun x => Some x) p.
+Proof.
+  intros. unfold transform_partial_program, transform_partial_program2.
+  rewrite map_partial_identity. auto.
+Qed.
+
+Lemma apply_partial_transf_program:
+  forall (A B V: Set) (f: A -> option B) (x: option (program A V)),
+  x @@@ (fun p => transform_partial_program f p) =
+  x @@@ (fun p => transform_partial_program2 f (fun x => Some x) p).
+Proof.
+  intros. unfold apply_partial. 
+  destruct x. apply transform_program_partial2_partial. auto.
+Qed.
+*)
 Lemma transform_partial_program_compose:
-  forall (A B C: Set)
+  forall (A B C V: Set)
          (f1: A -> option B) (f2: B -> option C)
-         (p: program A),
+         (p: program A V),
   transform_partial_program f1 p @@@
-                        (fun p' => transform_partial_program f2 p') =
+                       (fun p' => transform_partial_program f2 p') =
   transform_partial_program (fun f => f1 f @@@ f2) p.
 Proof.
   unfold transform_partial_program; intros.
-  rewrite <- transf_partial_program_compose. simpl. 
-  destruct (transf_partial_program f1 (prog_funct p)); simpl.
+  rewrite <- map_partial_compose. simpl. 
+  destruct (map_partial f1 (prog_funct p)); simpl.
   auto. auto. 
 Qed.
 
-Lemma transf_program_partial_total:
-  forall (A B: Set) (f: A -> B) (l: list (ident * A)),
-  Some (AST.transf_program f l) =
-    AST.transf_partial_program (fun x => Some (f x)) l.
-Proof.
-  induction l. simpl. auto.
-  simpl. destruct a. rewrite <- IHl. auto.
-Qed.
-
 Lemma transform_program_partial_total:
-  forall (A B: Set) (f: A -> B) (p: program A),
+  forall (A B V: Set) (f: A -> B) (p: program A V),
   Some (transform_program f p) =
     transform_partial_program (fun x => Some (f x)) p.
 Proof.
   intros. unfold transform_program, transform_partial_program.
-  rewrite <- transf_program_partial_total. auto.
+  rewrite map_partial_total. auto. 
 Qed.
 
 Lemma apply_total_transf_program:
-  forall (A B: Set) (f: A -> B) (x: option (program A)),
+  forall (A B V: Set) (f: A -> B) (x: option (program A V)),
   x @@ (fun p => transform_program f p) =
   x @@@ (fun p => transform_partial_program (fun x => Some (f x)) p).
 Proof.
@@ -219,6 +239,7 @@ Proof.
   reflexivity.
 Qed.
 
+(*
 Lemma transf_csharpminor_program_equiv:
   forall p, transf_csharpminor_program2 p = transf_csharpminor_program p.
 Proof.
@@ -227,22 +248,27 @@ Proof.
   simpl. 
   replace transf_cminor_program2 with transf_cminor_program.
   unfold transf_cminor_program, Cminorgen.transl_program, Cminor.program, PPC.program.
-  apply transform_partial_program_compose. 
+  rewrite apply_partial_transf_program.
+  rewrite transform_partial_program2_compose.
+  reflexivity.
   symmetry. apply extensionality. exact transf_cminor_program_equiv.
 Qed.
+*)
 
 (** * Semantic preservation *)
 
-(** We prove that the [transf_program2] translations preserve semantics.  The proof
-  composes the semantic preservation results for each pass. *)
+(** We prove that the [transf_program] translations preserve semantics.  The proof
+  composes the semantic preservation results for each pass.
+  This establishes the correctness of the whole compiler! *)
 
-Lemma transf_cminor_program2_correct:
+Theorem transf_cminor_program_correct:
   forall p tp t n,
-  transf_cminor_program2 p = Some tp ->
+  transf_cminor_program p = Some tp ->
   Cminor.exec_program p t (Vint n) ->
   PPC.exec_program tp t (Vint n).
 Proof.
   intros until n.
+  rewrite <- transf_cminor_program_equiv.
   unfold transf_cminor_program2.
   simpl. caseEq (RTLgen.transl_program p). intros p1 EQ1. 
   simpl. set (p2 := CSE.transf_program (Constprop.transf_program p1)).
@@ -273,39 +299,19 @@ Proof.
   simpl; intros; discriminate.
 Qed.
 
-Lemma transf_csharpminor_program2_correct:
-  forall p tp t n,
-  transf_csharpminor_program2 p = Some tp ->
-  Csharpminor.exec_program p t (Vint n) ->
-  PPC.exec_program tp t (Vint n).
-Proof.
-  intros until n; unfold transf_csharpminor_program2; simpl.
-  caseEq (Cminorgen.transl_program p).
-  simpl; intros p1 EQ1 EQ2 EXEC. 
-  apply transf_cminor_program2_correct with p1. auto. 
-  apply Cminorgenproof.transl_program_correct with p. auto.
-  assumption.
-  simpl; intros; discriminate.
-Qed.
-
-(** It follows that the whole compiler is semantic-preserving. *)
-
-Theorem transf_cminor_program_correct:
-  forall p tp t n,
-  transf_cminor_program p = Some tp ->
-  Cminor.exec_program p t (Vint n) ->
-  PPC.exec_program tp t (Vint n).
-Proof.
-  intros. apply transf_cminor_program2_correct with p. 
-  rewrite transf_cminor_program_equiv. assumption. assumption.
-Qed.
-
-Theorem transf_csharpminor_program_correct:
+Theorem transf_c_program_correct:
   forall p tp t n,
-  transf_csharpminor_program p = Some tp ->
-  Csharpminor.exec_program p t (Vint n) ->
+  transf_c_program p = Some tp ->
+  Csem.exec_program p t (Vint n) ->
   PPC.exec_program tp t (Vint n).
 Proof.
-  intros. apply transf_csharpminor_program2_correct with p. 
-  rewrite transf_csharpminor_program_equiv. assumption. assumption.
+  intros until n; unfold transf_c_program; simpl.
+  caseEq (Ctyping.typecheck_program p); try congruence; intro.
+  caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1.
+  caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. 
+  intros EQ3 SEM.
+  eapply transf_cminor_program_correct; eauto.
+  eapply Cminorgenproof.transl_program_correct; eauto. 
+  eapply Cshmgenproof3.transl_program_correct; eauto.
+  apply Ctyping.typecheck_program_correct; auto.
 Qed.