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

3 files changed, 445 insertions, 314 deletions

diff --git a/common/AST.v b/common/AST.v
index 1342bef..673f1d8 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 036fd8f..ccb7b03 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 95dc4e6..f472ec3 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.