diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cminorgen.v | 10 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 28 | ||||
-rw-r--r-- | cfrontend/Csem.v | 10 | ||||
-rw-r--r-- | cfrontend/Csharpminor.v | 20 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 21 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof1.v | 40 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof3.v | 57 | ||||
-rw-r--r-- | cfrontend/Csyntax.v | 17 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 8 |
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: |