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

9 files changed, 75 insertions, 136 deletions

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: