From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 4 Sep 2006 15:08:29 +0000
Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S
 dans les semantiques - Ajout constructions switch et allocation dynamique -
 Initialisation des variables globales - Portage Coq 8.1 beta Debut
 d'integration du front-end C: - Traduction Clight -> Csharpminor dans
 cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/RTLtyping.v | 1230 ++++++++++-----------------------------------------
 1 file changed, 227 insertions(+), 1003 deletions(-)

(limited to 'backend/RTLtyping.v')

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index d15dbb88..33338d37 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -6,7 +6,7 @@ Require Import AST.
 Require Import Op.
 Require Import Registers.
 Require Import RTL.
-Require Import union_find.
+Require Conventions.
 
 (** * The type system *)
 
@@ -38,7 +38,7 @@ Definition regenv := reg -> typ.
 Section WT_INSTR.
 
 Variable env: regenv.
-Variable funct: function.
+Variable funsig: signature.
 
 Inductive wt_instr : instruction -> Prop :=
   | wt_Inop:
@@ -72,13 +72,17 @@ Inductive wt_instr : instruction -> Prop :=
       List.map env args = sig.(sig_args) ->
       env res = match sig.(sig_res) with None => Tint | Some ty => ty end ->
       wt_instr (Icall sig ros args res s)
+  | wt_Ialloc:
+      forall arg res s,
+      env arg = Tint -> env res = Tint ->
+      wt_instr (Ialloc arg res s)
   | wt_Icond:
       forall cond args s1 s2,
       List.map env args = type_of_condition cond ->
       wt_instr (Icond cond args s1 s2)
   | wt_Ireturn: 
       forall optres,
-      option_map env optres = funct.(fn_sig).(sig_res) ->
+      option_map env optres = funsig.(sig_res) ->
       wt_instr (Ireturn optres).
 
 End WT_INSTR.
@@ -88,15 +92,27 @@ End WT_INSTR.
    parameters agree in types with the function signature, and
    names of parameters are pairwise distinct. *)
 
-Record wt_function (env: regenv) (f: function) : Prop :=
+Record wt_function (f: function) (env: regenv): Prop :=
   mk_wt_function {
     wt_params:
       List.map env f.(fn_params) = f.(fn_sig).(sig_args);
     wt_norepet:
       list_norepet f.(fn_params);
     wt_instrs:
-      forall pc instr, f.(fn_code)!pc = Some instr -> wt_instr env f instr
-  }.
+      forall pc instr, 
+      f.(fn_code)!pc = Some instr -> wt_instr env f.(fn_sig) instr
+}.
+
+Inductive wt_fundef: fundef -> Prop :=
+  | wt_fundef_external: forall ef,
+      Conventions.sig_external_ok ef.(ef_sig) ->
+      wt_fundef (External ef)
+  | wt_function_internal: forall f env,
+      wt_function f env ->
+      wt_fundef (Internal f).
+
+Definition wt_program (p: program): Prop :=
+  forall i f, In (i, f) (prog_funct p) -> wt_fundef f.
 
 (** * Type inference *)
 
@@ -109,1022 +125,221 @@ Record wt_function (env: regenv) (f: function) : Prop :=
   each pseudo-register from its uses in the code.  We follow the second
   approach.
 
-  The algorithm and its correctness proof in this section were
-  contributed by Damien Doligez. *)
+  We delegate the task of determining the type of each pseudo-register
+  to an external ``oracle'': a function written in Caml and not
+  proved correct.  We verify the returned type environment using
+  the following Coq code, which we will prove correct. *)
 
-(** ** Type inference algorithm *)
+Parameter infer_type_environment:
+  function -> list (node * instruction) -> option regenv.
 
-Set Implicit Arguments.
+(** ** Algorithm to check the correctness of a type environment *)
 
-(** Type inference for RTL is similar to that for simply-typed 
-  lambda-calculus: we use type variables to represent the types
-  of registers that have not yet been determined to be [Tint] or [Tfloat]
-  based on their uses.  We need exactly one type variable per pseudo-register,
-  therefore type variables can be conveniently equated with registers.
-  The type of a register during inference is therefore either
-  [tTy t] (with [t = Tint] or [t = Tfloat]) for a known type,
-  or [tReg r] to mean ``the same type as that of register [r]''. *)
+Section TYPECHECKING.
 
-Inductive myT : Set :=
-  | tTy : typ -> myT
-  | tReg : reg -> myT.
+Variable funct: function.
+Variable env: regenv.
 
-(** The algorithm proceeds by unification of the currently inferred
-  type for a pseudo-register with the type dictated by its uses.
-  Unification builds on a ``union-find'' data structure representing
-  equivalence classes of types (see module [Union_find]).
-*)
+Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
+Proof. decide equality. Qed.
 
-Module myreg.
-  Definition T := myT.
-  Definition eq : forall (x y : T), {x=y}+{x<>y}.
-  Proof.
-    destruct x; destruct y; auto;
-    try (apply right; discriminate); try (apply left; discriminate).
-    destruct t; destruct t0;
-    try (apply right; congruence); try (apply left; congruence).
-    elim (peq r r0); intros.
-    rewrite a; apply left; apply refl_equal.
-    apply right; congruence.
-  Defined.
-End myreg.
-
-Module mymap.
-  Definition elt := myreg.T.
-  Definition encode (t : myreg.T) : positive :=
-    match t with
-    | tTy Tint => xH
-    | tTy Tfloat => xI xH
-    | tReg r => xO r
-    end.
-  Definition decode (p : positive) : elt :=
-    match p with
-    | xH => tTy Tint
-    | xI _ => tTy Tfloat
-    | xO r => tReg r
-    end.
-
-  Lemma encode_decode : forall x : myreg.T, decode (encode x) = x.
-  Proof.
-    destruct x; try destruct t; simpl; auto.
-  Qed.
-
-  Lemma encode_injective :
-    forall (x y : myreg.T), encode x = encode y -> x = y.
-  Proof.
-    intros.
-    unfold encode in H. destruct x; destruct y; try congruence;
-    try destruct t; try destruct t0; congruence.
-  Qed.
-
-  Definition T := PTree.t positive.
-  Definition empty := PTree.empty positive.
-  Definition get (adr : elt) (t : T) :=
-    option_map decode (PTree.get (encode adr) t).
-  Definition add (adr dat : elt) (t : T) :=
-    PTree.set (encode adr) (encode dat) t.
-
-  Theorem get_empty : forall (x : elt), get x empty = None.
-  Proof.
-    intro.
-    unfold get. unfold empty.
-    rewrite PTree.gempty.
-    simpl; auto.
-  Qed.
-  Theorem get_add_1 :
-    forall (x y : elt) (m : T), get x (add x y m) = Some y.
-  Proof.
-    intros.
-    unfold add. unfold get.
-    rewrite PTree.gss.
-    simpl; rewrite encode_decode; auto.
-  Qed.
-  Theorem get_add_2 :
-    forall (x y z : elt) (m : T), z <> x -> get z (add x y m) = get z m.
-  Proof.
-    intros.
-    unfold get. unfold add.
-    rewrite PTree.gso; auto.
-    intro. apply H. apply encode_injective. auto.
-  Qed.
-End mymap.
-
-Module Uf := Unionfind (myreg) (mymap).
-
-Definition error := Uf.identify Uf.empty (tTy Tint) (tTy Tfloat).
-
-Fixpoint fold2 (A B : Set) (f : Uf.T -> A -> B -> Uf.T)
-               (init : Uf.T) (la : list A) (lb : list B) {struct la}
-               : Uf.T :=
-  match la, lb with
-  | ha::ta, hb::tb => fold2 f (f init ha hb) ta tb
-  | nil, nil => init
-  | _, _ => error
-  end.
+Definition check_reg (r: reg) (ty: typ): bool :=
+  if typ_eq (env r) ty then true else false.
 
-Definition option_fold2 (A B : Set) (f : Uf.T -> A -> B -> Uf.T)
-                        (init : Uf.T) (oa : option A) (ob : option B)
-                        : Uf.T :=
-  match oa, ob with
-  | Some a, Some b => f init a b
-  | None, None => init
-  | _, _ => error
-  end.
-
-Definition teq (ty1 ty2 : typ) : bool :=
-  match ty1, ty2 with
-  | Tint, Tint => true
-  | Tfloat, Tfloat => true
+Fixpoint check_regs (rl: list reg) (tyl: list typ) {struct rl}: bool :=
+  match rl, tyl with
+  | nil, nil => true
+  | r1::rs, ty::tys => check_reg r1 ty && check_regs rs tys
   | _, _ => false
   end.
 
-Definition type_rtl_arg (u : Uf.T) (r : reg) (t : typ) :=
-  Uf.identify u (tReg r) (tTy t).
-
-Definition type_rtl_ros (u : Uf.T) (ros : reg+ident) :=
-  match ros with
-  | inl r => Uf.identify u (tReg r) (tTy Tint)
-  | inr s => u
-  end.
+Definition check_op (op: operation) (args: list reg) (res: reg): bool :=
+  let (targs, tres) := type_of_operation op in
+  check_regs args targs && check_reg res tres.
 
-Definition type_of_sig_res (sig : signature) :=
-  match sig.(sig_res) with None => Tint | Some ty => ty end.
-
-(** This is the core type inference function.  The [u] argument is
-  the current substitution / equivalence classes between types.
-  An updated set of equivalence classes, reflecting unifications
-  possibly performed during the type-checking of [i], is returned.
-  Note that [type_rtl_instr] never fails explicitly.  However,
-  in case of type error (e.g. applying the [Oadd] integer operation
-  to float registers), the equivalence relation returned will
-  put [tTy Tint] and [tTy Tfloat] in the same equivalence class.
-  This fact will propagate through type inference for other instructions,
-  and be detected at the end of type inference, indicating a typing failure.
-*)
-
-Definition type_rtl_instr (rtyp : option typ)
-    (u : Uf.T) (_ : positive) (i : instruction) :=
+Definition check_instr (i: instruction) : bool :=
   match i with
-  | Inop _ => u
-  | Iop Omove (r1 :: nil) r0 _ => Uf.identify u (tReg r0) (tReg r1)
-  | Iop Omove _ _ _ => error
-  | Iop Oundef nil _ _ => u
-  | Iop Oundef _ _ _ => error
-  | Iop op args r0 _ =>
-      let (argtyp, restyp) := type_of_operation op in
-      let u1 := type_rtl_arg u r0 restyp in
-      fold2 type_rtl_arg u1 args argtyp
-  | Iload chunk addr args r0 _ =>  
-      let u1 := type_rtl_arg u r0 (type_of_chunk chunk) in
-      fold2 type_rtl_arg u1 args (type_of_addressing addr)
-  | Istore chunk addr args r0 _ =>
-      let u1 := type_rtl_arg u r0 (type_of_chunk chunk) in
-      fold2 type_rtl_arg u1 args (type_of_addressing addr)
-  | Icall sign ros args r0 _ =>
-      let u1 := type_rtl_ros u ros in
-      let u2 := type_rtl_arg u1 r0 (type_of_sig_res sign) in
-      fold2 type_rtl_arg u2 args sign.(sig_args)
+  | Inop _ =>
+      true
+  | Iop Omove (arg::nil) res _ =>
+      if typ_eq (env arg) (env res) then true else false
+  | Iop Omove args res _ =>
+      false
+  | Iop Oundef nil res _ =>
+      true
+  | Iop Oundef args res _ =>
+      false
+  | Iop op args res _ =>
+      check_op op args res
+  | Iload chunk addr args dst _ =>
+      check_regs args (type_of_addressing addr)
+      && check_reg dst (type_of_chunk chunk)
+  | Istore chunk addr args src _ =>
+      check_regs args (type_of_addressing addr)
+      && check_reg src (type_of_chunk chunk)
+  | Icall sig ros args res _ =>
+      match ros with inl r => check_reg r Tint | inr s => true end
+      && check_regs args sig.(sig_args)
+      && check_reg res (match sig.(sig_res) with None => Tint | Some ty => ty end)
+  | Ialloc arg res _ =>
+      check_reg arg Tint && check_reg res Tint
   | Icond cond args _ _ =>
-      fold2 type_rtl_arg u args (type_of_condition cond)
-  | Ireturn o => option_fold2 type_rtl_arg u o rtyp
+      check_regs args (type_of_condition cond)
+  | Ireturn optres =>
+      match optres, funct.(fn_sig).(sig_res) with
+      | None, None => true
+      | Some r, Some t => check_reg r t
+      | _, _ => false
+      end
   end.
 
-Definition mk_env (u : Uf.T) (r : reg) :=
-  if myreg.eq (Uf.repr u (tReg r)) (Uf.repr u (tTy Tfloat))
-  then Tfloat
-  else Tint.
+Definition check_params_norepet (params: list reg): bool :=
+  if list_norepet_dec Reg.eq params then true else false.
 
-Fixpoint member (x : reg) (l : list reg) {struct l} : bool :=
-  match l with
-  | nil => false
-  | y :: rest => if peq x y then true else member x rest
+Fixpoint check_instrs (instrs: list (node * instruction)) : bool :=
+  match instrs with
+  | nil => true
+  | (pc, i) :: rem => check_instr i && check_instrs rem
   end.
 
-Fixpoint repet (l : list reg) : bool :=
-  match l with
-  | nil => false
-  | x :: rest => member x rest || repet rest
-  end.
+(** ** Correctness of the type-checking algorithm *)
 
-Definition type_rtl_function (f : function) :=
-  let u1 := PTree.fold (type_rtl_instr f.(fn_sig).(sig_res))
-                       f.(fn_code) Uf.empty in
-  let u2 := fold2 type_rtl_arg u1 f.(fn_params) f.(fn_sig).(sig_args) in
-  if repet f.(fn_params) then
-    None
-  else
-    if myreg.eq (Uf.repr u2 (tTy Tint)) (Uf.repr u2 (tTy Tfloat))
-    then None
-    else Some (mk_env u2).
-
-Unset Implicit Arguments.
-
-(** ** Correctness proof for type inference *)
-
-(** General properties of the type equivalence relation. *)
-
-Definition consistent (u : Uf.T) :=
-  Uf.repr u (tTy Tint) <> Uf.repr u (tTy Tfloat).
-
-Lemma consistent_not_eq : forall (u : Uf.T) (A : Type) (x y : A),
-  consistent u ->
-  (if myreg.eq (Uf.repr u (tTy Tint)) (Uf.repr u (tTy Tfloat)) then x else y)
-  = y.
-  Proof.
-    intros.
-    unfold consistent in H.
-    destruct (myreg.eq (Uf.repr u (tTy Tint)) (Uf.repr u (tTy Tfloat)));
-    congruence.
-  Qed.
-
-Lemma equal_eq : forall (t : myT) (A : Type) (x y : A),
-  (if myreg.eq t t then x else y) = x.
-  Proof.
-    intros.
-    destruct (myreg.eq t t); congruence.
-  Qed.
-
-Lemma error_inconsistent : forall (A : Prop), consistent error -> A.
-  Proof.
-    intros.
-    absurd (consistent error); auto.
-    intro.
-    unfold error in H.  unfold consistent in H.
-    rewrite Uf.sameclass_identify_1 in H.
-    congruence.
-  Qed.
-
-Lemma teq_correct : forall (t1 t2 : typ), teq t1 t2 = true -> t1 = t2.
-  Proof.
-    intros; destruct t1; destruct t2; try simpl in H; congruence.
-  Qed.
-
-Definition included (u1 u2 : Uf.T) : Prop :=
-  forall (e1 e2: myT),
-    Uf.repr u1 e1 = Uf.repr u1 e2 -> Uf.repr u2 e1 = Uf.repr u2 e2.
-
-Lemma included_refl :
-  forall (e : Uf.T), included e e.
-  Proof.
-    unfold included. auto.
-  Qed.
-
-Lemma included_trans :
-  forall (e1 e2 e3 : Uf.T),
-  included e3 e2 -> included e2 e1 -> included e3 e1.
-  Proof.
-    unfold included. auto.
-  Qed.
-
-Lemma included_consistent :
-  forall (u1 u2 : Uf.T),
-  included u1 u2 -> consistent u2 -> consistent u1.
-  Proof.
-    unfold consistent. unfold included.
-    intros.
-    intro. apply H0. apply H.
-    auto.
-  Qed.
-
-Lemma included_identify :
-  forall (u : Uf.T) (t1 t2 : myT), included u (Uf.identify u t1 t2).
-  Proof.
-  unfold included.
-  intros.
-  apply Uf.sameclass_identify_2; auto.
-  Qed.
-
-Lemma type_arg_correct_1 :
-  forall (u : Uf.T) (r : reg) (t : typ),
-  consistent (type_rtl_arg u r t)
-  -> Uf.repr (type_rtl_arg u r t) (tReg r)
-     = Uf.repr (type_rtl_arg u r t) (tTy t).
-  Proof.
-    intros.
-    unfold type_rtl_arg.
-    rewrite Uf.sameclass_identify_1.
-    auto.
-  Qed.
-
-Lemma type_arg_correct :
-  forall (u : Uf.T) (r : reg) (t : typ),
-  consistent (type_rtl_arg u r t) -> mk_env (type_rtl_arg u r t) r = t.
-  Proof.
-    intros.
-    unfold mk_env. 
-    rewrite type_arg_correct_1.
-    destruct t.
-    apply consistent_not_eq; auto.
-    destruct (myreg.eq (Uf.repr (type_rtl_arg u r Tfloat) (tTy Tfloat)));
-    congruence.
-    auto.
-  Qed.
-
-Lemma type_arg_included :
-  forall (u : Uf.T) (r : reg) (t : typ), included u (type_rtl_arg u r t).
-  Proof.
-    intros.
-    unfold type_rtl_arg.
-    apply included_identify.
-  Qed.
-
-Lemma type_arg_extends :
-  forall (u : Uf.T) (r : reg) (t : typ),
-  consistent (type_rtl_arg u r t) -> consistent u.
-  Proof.
-    intros.
-    apply included_consistent with (u2 := type_rtl_arg u r t).
-    apply type_arg_included.
-    auto.
-  Qed.
-
-Lemma type_args_included :
-  forall (l1 : list reg) (l2 : list typ) (u : Uf.T),
-  consistent (fold2 type_rtl_arg u l1 l2)
-  -> included u (fold2 type_rtl_arg u l1 l2).
-  Proof.
-    induction l1; intros; destruct l2.
-    simpl in H; simpl; apply included_refl.
-    simpl in H. apply error_inconsistent. auto.
-    simpl in H. apply error_inconsistent. auto.
-    simpl.
-    simpl in H.
-    apply included_trans with (e2 := type_rtl_arg u a t).
-    apply type_arg_included.
-    apply IHl1.
-    auto.
-  Qed.
-
-Lemma type_args_extends :
-  forall (l1 : list reg) (l2 : list typ) (u : Uf.T),
-  consistent (fold2 type_rtl_arg u l1 l2) -> consistent u.
-  Proof.
-    intros.
-    apply (included_consistent _ _ (type_args_included l1 l2 u H)).
-    auto.
-  Qed.
-
-Lemma type_args_correct :
-  forall (l1 : list reg) (l2 : list typ) (u : Uf.T),
-  consistent (fold2 type_rtl_arg u l1 l2)
-  -> map (mk_env (fold2 type_rtl_arg u l1 l2)) l1 = l2.
-  Proof.
-    induction l1.
-    intros.
-    destruct l2.
-    unfold map; simpl; auto.
-    simpl in H; apply error_inconsistent; auto.
-    intros.
-    destruct l2.
-    simpl in H; apply error_inconsistent; auto.
-    simpl.
-    simpl in H.
-    rewrite (IHl1 l2 (type_rtl_arg u a t) H).
-    unfold mk_env.
-    destruct t.
-    rewrite (type_args_included _ _ _ H (tReg a) (tTy Tint)).
-    rewrite consistent_not_eq; auto.
-    apply type_arg_correct_1.
-    apply type_args_extends with (l1 := l1) (l2 := l2); auto.
-    rewrite (type_args_included _ _ _ H (tReg a) (tTy Tfloat)).
-    rewrite equal_eq; auto.
-    apply type_arg_correct_1.
-    apply type_args_extends with (l1 := l1) (l2 := l2); auto.
-  Qed.
-
-(** Correctness of [wt_params]. *)
-
-Lemma type_rtl_function_params :
-  forall (f: function) (env: regenv),
-  type_rtl_function f = Some env
-  -> List.map env f.(fn_params) = f.(fn_sig).(sig_args).
-  Proof.
-    destruct f; unfold type_rtl_function; simpl.
-    destruct (repet fn_params); simpl; intros; try congruence.
-    pose (u := PTree.fold (type_rtl_instr (sig_res fn_sig)) fn_code Uf.empty).
-    fold u in H.
-    cut (consistent (fold2 type_rtl_arg u fn_params (sig_args fn_sig))).
-    intro.
-    pose (R := Uf.repr (fold2 type_rtl_arg u fn_params (sig_args fn_sig))).
-    fold R in H.
-    destruct (myreg.eq (R (tTy Tint)) (R (tTy Tfloat))).
-    congruence.
-    injection H.
-    intro.
-    rewrite <- H1.
-    apply type_args_correct.
-    auto.
-    intro.
-    rewrite H0 in H.
-    rewrite equal_eq in H.
-    congruence.
-  Qed.
-
-(** Correctness of [wt_norepet]. *)
-
-Lemma member_correct :
-  forall (l : list reg) (a : reg), member a l = false -> ~In a l.
-  Proof.
-    induction l; simpl; intros; try tauto.
-    destruct (peq a0 a); simpl; try congruence.
-    intro. destruct H0; try congruence.
-    generalize H0; apply IHl; auto.
-  Qed.
-
-Lemma repet_correct :
-  forall (l : list reg), repet l = false -> list_norepet l.
-  Proof.
-    induction l; simpl; intros.
-     exact (list_norepet_nil reg).
-     elim (orb_false_elim (member a l) (repet l) H); intros.
-     apply list_norepet_cons.
-      apply member_correct; auto.
-      apply IHl; auto.
-  Qed.
-
-Lemma type_rtl_function_norepet :
-  forall (f: function) (env: regenv),
-  type_rtl_function f = Some env
-  -> list_norepet f.(fn_params).
-  Proof.
-    destruct f; unfold type_rtl_function; simpl.
-    intros. cut (repet fn_params = false).
-     intro. apply repet_correct. auto.
-     destruct (repet fn_params); congruence.
-  Qed.
-
-(** Correctness of [wt_instrs]. *)
-
-Lemma step1 :
-  forall (f : function) (env : regenv),
-  type_rtl_function f = Some env
-  -> exists u2 : Uf.T,
-       included (PTree.fold (type_rtl_instr f.(fn_sig).(sig_res))
-                            f.(fn_code) Uf.empty)
-                u2
-       /\ env = mk_env u2
-       /\ consistent u2.
-  Proof.
-    intros f env.
-    pose (u1 := (PTree.fold (type_rtl_instr f.(fn_sig).(sig_res))
-                            f.(fn_code) Uf.empty)).
-    fold u1.
-    unfold type_rtl_function.
-    intros.
-    destruct (repet f.(fn_params)).
-    congruence.
-    fold u1 in H.
-    pose (u2 := (fold2 type_rtl_arg u1 f.(fn_params) f.(fn_sig).(sig_args))).
-    fold u2 in H.
-    exists u2.
-    caseEq (myreg.eq (Uf.repr u2 (tTy Tint)) (Uf.repr u2 (tTy Tfloat))).
-    intros.
-    rewrite e in H.
-    rewrite equal_eq in H.
-    congruence.
-    intros.
-    rewrite consistent_not_eq in H.
-    apply conj.
-    unfold u2.
-    apply type_args_included.
-    auto.
-    apply conj; auto.
-    congruence.
-    auto.
-  Qed.
-
-Lemma let_fold_args_res :
-  forall (u : Uf.T) (l : list reg) (r : reg) (e : list typ * typ),
-  (let (argtyp, restyp) := e in
-   fold2 type_rtl_arg (type_rtl_arg u r restyp) l argtyp)
-  = fold2 type_rtl_arg (type_rtl_arg u r (snd e)) l (fst e).
-  Proof.
-    intros. rewrite (surjective_pairing e). simpl. auto.
-  Qed.
-
-Lemma type_args_res_included :
-  forall (l1 : list reg) (l2 : list typ) (u : Uf.T) (r : reg) (t : typ),
-  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) l1 l2)
-  -> included u (fold2 type_rtl_arg (type_rtl_arg u r t) l1 l2).
-  Proof.
-  intros.
-  apply included_trans with (e2 := type_rtl_arg u r t).
-  apply type_arg_included.
-  apply type_args_included; auto.
-  Qed.
-
-Lemma type_args_res_ros_included :
-  forall (l1 : list reg) (l2 : list typ) (u : Uf.T) (r : reg) (t : typ)
-         (ros : reg+ident),
-  consistent (fold2 type_rtl_arg (type_rtl_arg (type_rtl_ros u ros) r t) l1 l2)
-  -> included u (fold2 type_rtl_arg (type_rtl_arg (type_rtl_ros u ros) r t) l1 l2).
+Lemma check_reg_correct:
+  forall r ty, check_reg r ty = true -> env r = ty.
 Proof.
-  intros.
-  apply included_trans with (e2 := type_rtl_ros u ros).
-  unfold type_rtl_ros; destruct ros.
-  apply included_identify.
-  apply included_refl.
-  apply type_args_res_included; auto.
+  unfold check_reg; intros.
+  destruct (typ_eq (env r) ty). auto. discriminate.
 Qed.
 
-Lemma type_instr_included :
-  forall (p : positive) (i : instruction) (u : Uf.T) (res_ty : option typ),
-  consistent (type_rtl_instr res_ty u p i)
-  -> included u (type_rtl_instr res_ty u p i).
-  Proof.
-    intros.
-    destruct i; simpl; simpl in H; try apply type_args_res_included; auto.
-    apply included_refl; auto.
-    destruct o; simpl; simpl in H; try apply type_args_res_included; auto.
-    destruct l; simpl; simpl in H; auto.
-    apply error_inconsistent; auto.
-    destruct l; simpl; simpl in H; auto.
-    apply included_identify.
-    apply error_inconsistent; auto.
-    destruct l; simpl; simpl in H; auto.
-    apply included_refl.
-    apply error_inconsistent; auto.
-    apply type_args_res_ros_included; auto.
-    apply type_args_included; auto.
-    destruct res_ty; destruct o; simpl; simpl in H;
-      try (apply error_inconsistent; auto; fail).
-    apply type_arg_included.
-    apply included_refl.
-   Qed.
-
-Lemma type_instrs_extends :
-  forall (l : list (positive * instruction)) (u : Uf.T) (res_ty : option typ),
-  consistent
-      (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u)
-  -> consistent u.
+Lemma check_regs_correct:
+  forall rl tyl, check_regs rl tyl = true -> List.map env rl = tyl.
 Proof.
-  induction l; simpl; intros.
-  auto.
-  apply included_consistent
-     with (u2 := (type_rtl_instr res_ty u (fst a) (snd a))).
-  apply type_instr_included.
-  apply IHl with (res_ty := res_ty); auto.
-  apply IHl with (res_ty := res_ty); auto.
+  induction rl; destruct tyl; simpl; intros.
+  auto. discriminate. discriminate.
+  elim (andb_prop _ _ H); intros. 
+  rewrite (check_reg_correct _ _ H0). rewrite (IHrl tyl H1). auto.
 Qed.
 
-Lemma type_instrs_included :
-  forall (l : list (positive * instruction)) (u : Uf.T) (res_ty : option typ),
-  consistent
-      (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u)
-  -> included u
-         (fold_left (fun v p => type_rtl_instr res_ty v (fst p) (snd p)) l u).
-  Proof.
-    induction l; simpl; intros.
-    apply included_refl; auto.
-    apply included_trans with (e2 := (type_rtl_instr res_ty u (fst a) (snd a))).
-    apply type_instr_included.
-    apply type_instrs_extends with (res_ty := res_ty) (l := l); auto.
-    apply IHl; auto.
-  Qed.
-
-Lemma step2 :
-  forall (res_ty : option typ) (c : code) (u0 : Uf.T),
-  consistent (PTree.fold (type_rtl_instr res_ty) c u0) ->
-  forall (pc : positive) (i : instruction),
-  c!pc = Some i
-  -> exists u : Uf.T,
-        consistent (type_rtl_instr res_ty u pc i)
-     /\ included (type_rtl_instr res_ty u pc i)
-                    (PTree.fold (type_rtl_instr res_ty) c u0).
-  Proof.
-    intros.
-    rewrite PTree.fold_spec.
-    rewrite PTree.fold_spec in H.
-    pose (H1 := PTree.elements_correct _ _ H0).
-    generalize H. clear H.
-    generalize u0. clear u0.
-    generalize H1. clear H1.
-    induction (PTree.elements c).
-    intros.
-    absurd (In (pc, i) nil).
-    apply in_nil.
-    auto.
-    intros.
-    simpl in H.
-    elim H1.
-    intro.
-    rewrite H2 in H.
-    simpl in H.
-    rewrite H2. simpl.
-    exists u0.
-    apply conj.
-    apply type_instrs_extends with (res_ty := res_ty) (l := l).
-    auto.
-    apply type_instrs_included.
-    auto.
-    intro.
-    simpl.
-    apply IHl.
-    auto.
-    auto.
-  Qed.
-
-Definition mapped (u : Uf.T) (r : reg) :=
-  Uf.repr u (tReg r) = Uf.repr u (tTy Tfloat)
-  \/ Uf.repr u (tReg r) = Uf.repr u (tTy Tint).
-
-Definition definite (u : Uf.T) (i : instruction) :=
-  match i with
-  | Inop _ => True
-  | Iop Omove (r1 :: nil) r0 _ => Uf.repr u (tReg r1) = Uf.repr u (tReg r0)
-  | Iop Oundef _ _ _ => True
-  | Iop _ args r0 _ =>
-         mapped u r0 /\ forall r : reg, In r args -> mapped u r
-  | Iload _ _ args r0 _ =>
-         mapped u r0 /\ forall r : reg, In r args -> mapped u r
-  | Istore _ _ args r0 _ =>
-         mapped u r0 /\ forall r : reg, In r args -> mapped u r
-  | Icall _ ros args r0 _ =>
-      match ros with inl r => mapped u r | _ => True end
-      /\ mapped u r0 /\ forall r : reg, In r args -> mapped u r
-  | Icond _ args _ _ =>
-      forall r : reg, In r args -> mapped u r
-  | Ireturn None => True
-  | Ireturn (Some r) => mapped u r
-  end.
-
-Lemma type_arg_complete :
-  forall (u : Uf.T) (r : reg) (t : typ),
-  mapped (type_rtl_arg u r t) r.
-Proof.
-  intros.
-  unfold type_rtl_arg.
-  unfold mapped.
-  destruct t.
-  right; apply Uf.sameclass_identify_1.
-  left; apply Uf.sameclass_identify_1.
-Qed.
-
-Lemma type_arg_mapped :
-  forall (u : Uf.T) (r r0 : reg) (t : typ),
-  mapped u r0 -> mapped (type_rtl_arg u r t) r0.
-Proof.
-  unfold mapped.
-  unfold type_rtl_arg.
-  intros.
-  elim H; intros.
-  left; apply Uf.sameclass_identify_2; auto.
-  right; apply Uf.sameclass_identify_2; auto.
-Qed.
-
-Lemma type_args_mapped :
-  forall (lr : list reg) (lt : list typ) (u : Uf.T) (r : reg),
-  consistent (fold2 type_rtl_arg u lr lt) ->
-  mapped u r ->
-    mapped (fold2 type_rtl_arg u lr lt) r.
+Lemma check_op_correct:
+  forall op args res,
+  check_op op args res = true ->
+  (List.map env args, env res) = type_of_operation op.
 Proof.
-  induction lr; simpl; intros.
-  destruct lt; simpl; auto; try (apply error_inconsistent; auto; fail).
-  destruct lt; simpl; auto; try (apply error_inconsistent; auto; fail).
-  apply IHlr.
+  unfold check_op; intros.
+  destruct (type_of_operation op) as [targs tres]. 
+  elim (andb_prop _ _ H); intros.
+  rewrite (check_regs_correct _ _ H0).
+  rewrite (check_reg_correct _ _ H1).
   auto.
-  apply type_arg_mapped; auto.
-Qed.
-
-Lemma type_args_complete :
-  forall (lr : list reg) (lt : list typ) (u : Uf.T),
-  consistent (fold2 type_rtl_arg u lr lt)
-  -> forall r, (In r lr -> mapped (fold2 type_rtl_arg u lr lt) r).
-Proof.
-  induction lr; simpl; intros.
-  destruct lt; simpl; try tauto.
-  destruct lt; simpl.
-  apply error_inconsistent; auto.
-  elim H0; intros.
-  rewrite H1.
-  rewrite H1 in H.
-  apply type_args_mapped; auto.
-  apply type_arg_complete.
-  apply IHlr; auto.
-Qed.
-
-Lemma type_res_complete :
-  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ),
-  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt)
-  -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r.
-Proof.
-  intros.
-  apply type_args_mapped; auto.
-  apply type_arg_complete.
 Qed.
 
-Lemma type_args_res_complete :
-  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ),
-  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt)
-  -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r
-      /\ forall rr, (In rr lr -> mapped (fold2 type_rtl_arg (type_rtl_arg u r t)
-                                                            lr lt)
-                                        rr).
+Lemma check_instr_correct:
+  forall i, check_instr i = true -> wt_instr env funct.(fn_sig) i.
 Proof.
-  intros.
-  apply conj.
-  apply type_res_complete; auto.
-  apply type_args_complete; auto.
+  unfold check_instr; intros; destruct i.
+  (* nop *)
+  constructor.
+  (* op *)
+  destruct o;
+  try (apply wt_Iop; [congruence|congruence|apply check_op_correct;auto]).
+  destruct l; try discriminate. destruct l; try discriminate.
+  destruct (typ_eq (env r0) (env r)); try discriminate.
+  apply wt_Iopmove; auto.
+  destruct l; try discriminate.
+  apply wt_Iopundef.
+  (* load *)
+  elim (andb_prop _ _ H); intros.
+  constructor. apply check_regs_correct; auto. apply check_reg_correct; auto.
+  (* store *)
+  elim (andb_prop _ _ H); intros.
+  constructor. apply check_regs_correct; auto. apply check_reg_correct; auto.
+  (* call *)
+  elim (andb_prop _ _ H); clear H; intros.
+  elim (andb_prop _ _ H); clear H; intros.
+  constructor.
+  destruct s0; auto. apply check_reg_correct; auto.
+  apply check_regs_correct; auto.
+  apply check_reg_correct; auto.
+  (* alloc *)
+  elim (andb_prop _ _ H); intros.
+  constructor; apply check_reg_correct; auto.
+  (* cond *)
+  constructor. apply check_regs_correct; auto.
+  (* return *)
+  constructor. 
+  destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate.
+  rewrite (check_reg_correct _ _ H); auto.
+  auto.
 Qed.
 
-Lemma type_ros_complete :
-  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r r1 : reg) (t : typ),
-  consistent (fold2 type_rtl_arg (type_rtl_arg
-                                    (type_rtl_ros u (inl ident r1)) r t) lr lt)
-  ->
-  mapped (fold2 type_rtl_arg (type_rtl_arg
-                                (type_rtl_ros u (inl ident r1)) r t) lr lt) r1.
+Lemma check_instrs_correct:
+  forall instrs,
+  check_instrs instrs = true ->
+  forall pc i, In (pc, i) instrs -> wt_instr env funct.(fn_sig) i.
 Proof.
-  intros.
-  apply type_args_mapped; auto.
-  apply type_arg_mapped.
-  unfold type_rtl_ros.
-  unfold mapped.
-  right.
-  apply Uf.sameclass_identify_1; auto.
+  induction instrs; simpl; intros.
+  elim H0.
+  destruct a as [pc' i']. elim (andb_prop _ _ H); clear H; intros.
+  elim H0; intro.
+  inversion H2; subst pc' i'. apply check_instr_correct; auto.
+  eauto.
 Qed.
 
-Lemma type_res_correct :
-  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r : reg) (t : typ),
-  consistent (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt)
-  -> mk_env (fold2 type_rtl_arg (type_rtl_arg u r t) lr lt) r = t.
-Proof.
-  intros.
-  unfold mk_env.
-  rewrite (type_args_included _ _ _ H (tReg r) (tTy t)).
-  destruct t.
-  apply consistent_not_eq; auto.
-  apply equal_eq; auto.
-  unfold type_rtl_arg; apply Uf.sameclass_identify_1; auto.
-Qed.
+End TYPECHECKING.
 
-Lemma type_ros_correct :
-  forall (u : Uf.T) (lr : list reg) (lt : list typ) (r r1 : reg) (t : typ),
-  consistent (fold2 type_rtl_arg (type_rtl_arg
-                                    (type_rtl_ros u (inl ident r1)) r t) lr lt)
-  ->
-  mk_env (fold2 type_rtl_arg (type_rtl_arg
-                                (type_rtl_ros u (inl ident r1)) r t) lr lt) r1
-  = Tint.
-Proof.
-  intros.
-  unfold mk_env.
-  rewrite (type_args_included _ _ _ H (tReg r1) (tTy Tint)).
-  apply consistent_not_eq; auto.
-  rewrite (type_arg_included (type_rtl_ros u (inl ident r1)) r t (tReg r1) (tTy Tint)).
-  auto.
-  simpl.
-  apply Uf.sameclass_identify_1; auto.
-Qed.
-
-Lemma step3 :
-  forall (u : Uf.T) (f : function) (c : code) (i : instruction) (pc : positive),
-  c!pc = Some i ->
-  consistent (type_rtl_instr f.(fn_sig).(sig_res) u pc i)
-  ->    wt_instr (mk_env (type_rtl_instr f.(fn_sig).(sig_res) u pc i)) f i
-     /\ definite (type_rtl_instr f.(fn_sig).(sig_res) u pc i) i.
-  Proof.
-    Opaque type_rtl_arg.
-    intros.
-    destruct i; simpl in H0; simpl.
-     (* Inop *)
-     apply conj; auto. apply wt_Inop.
-     (* Iop *)
-     destruct o;
-       try (apply conj; [
-             apply wt_Iop; try congruence; simpl;
-               rewrite (type_args_correct _ _ _ H0);
-               rewrite (type_res_correct _ _ _ _ _ H0);
-               auto
-            |apply (type_args_res_complete _ _ _ _ _ H0)]).
-      (* Omove *)
-      destruct l; [apply error_inconsistent; auto | idtac].
-      destruct l; [idtac | apply error_inconsistent; auto].
-      apply conj.
-      apply wt_Iopmove.
-      simpl.
-      unfold mk_env.
-      rewrite Uf.sameclass_identify_1.
-      congruence.
-      simpl.
-      rewrite Uf.sameclass_identify_1; congruence.
-      (* Oundef *)
-      destruct l; [idtac | apply error_inconsistent; auto].
-      apply conj. apply wt_Iopundef.
-      unfold definite. auto.
-     (* Iload *)
-     apply conj.
-      apply wt_Iload.
-       rewrite (type_args_correct _ _ _ H0); auto.
-       rewrite (type_res_correct _ _ _ _ _ H0); auto.
-      simpl; apply (type_args_res_complete _ _ _ _ _ H0).
-     (* IStore *)
-     apply conj.
-      apply wt_Istore.
-       rewrite (type_args_correct _ _ _ H0); auto.
-       rewrite (type_res_correct _ _ _ _ _ H0); auto.
-      simpl; apply (type_args_res_complete _ _ _ _ _ H0).
-     (* Icall *)
-     apply conj.
-      apply wt_Icall.
-       destruct s0; auto. apply type_ros_correct. auto.
-       apply type_args_correct. auto.
-       fold (type_of_sig_res s). apply type_res_correct. auto.
-      destruct s0.
-       apply conj.
-        apply type_ros_complete. auto.
-        apply type_args_res_complete. auto.
-       apply conj; auto.
-         apply type_args_res_complete. auto.
-     (* Icond *) 
-     apply conj.
-      apply wt_Icond.
-       apply (type_args_correct _ _ _ H0).
-       simpl; apply (type_args_complete _ _ _ H0).
-     (* Ireturn *)
-     destruct o; simpl.
-      apply conj.
-       apply wt_Ireturn.
-         destruct f.(fn_sig).(sig_res); simpl; simpl in H0.
-          rewrite type_arg_correct; auto.
-          apply error_inconsistent; auto.
-       destruct f.(fn_sig).(sig_res); simpl; simpl in H0.
-          apply type_arg_complete.
-          apply error_inconsistent; auto.
-      apply conj; auto. apply wt_Ireturn.
-        destruct f.(fn_sig).(sig_res); simpl; simpl in H0.
-         apply error_inconsistent; auto.
-         congruence.
-    Transparent type_rtl_arg.
-  Qed.
-
-Lemma mapped_included_consistent :
-  forall (u1 u2 : Uf.T) (r : reg),
-  mapped u1 r ->
-  included u1 u2 ->
-  consistent u2 ->
-  mk_env u2 r = mk_env u1 r.
-Proof.
-  intros.
-  unfold mk_env.
-  unfold mapped in H.
-  elim H; intros; rewrite H2; rewrite (H0 _ _ H2).
-  rewrite equal_eq; rewrite equal_eq; auto.
-  rewrite (consistent_not_eq u2).
-  rewrite (consistent_not_eq u1).
-  auto.
-  apply included_consistent with (u2 := u2).
-  auto.
-  auto.
-  auto.
-Qed.
+(** ** The type inference function **)
 
-Lemma mapped_list_included :
-  forall (u1 u2 : Uf.T) (lr : list reg),
-  (forall r, In r lr -> mapped u1 r) ->
-  included u1 u2 ->
-  consistent u2 ->
-    map (mk_env u2) lr = map (mk_env u1) lr.
-Proof.
-  induction lr; simpl; intros.
-  auto.
-  rewrite (mapped_included_consistent u1 u2 a).
-  rewrite IHlr; auto.
-  apply (H a); intros.
-  left; auto.
-  auto.
-  auto.
-Qed.
+Definition type_function (f: function): option regenv :=
+  let instrs := PTree.elements f.(fn_code) in
+  match infer_type_environment f instrs with
+  | None => None
+  | Some env =>
+      if check_regs env f.(fn_params) f.(fn_sig).(sig_args)
+      && check_params_norepet f.(fn_params)
+      && check_instrs f env instrs
+      then Some env else None
+  end.
 
-Lemma included_mapped :
-  forall (u1 u2 : Uf.T) (r : reg),
-  included u1 u2 ->
-  mapped u1 r ->
-    mapped u2 r.
-Proof.
-  unfold mapped.
-  intros.
-  elim H0; intros.
-  left; rewrite (H _ _ H1); auto.
-  right; rewrite (H _ _ H1); auto.
-Qed.
+Definition type_external_function (ef: external_function): bool :=
+  List.fold_right
+    (fun l b => match l with Locations.S _ => false | Locations.R _ => b end)
+    true (Conventions.loc_arguments ef.(ef_sig)).
 
-Lemma included_mapped_forall :
-  forall (u1 u2 : Uf.T) (r : reg) (l : list reg),
-  included u1 u2 ->
-  mapped u1 r /\ (forall r, In r l -> mapped u1 r) ->
-    mapped u2 r /\ (forall r, In r l -> mapped u2 r).
+Lemma type_function_correct:
+  forall f env,
+  type_function f = Some env ->
+  wt_function f env.
 Proof.
-  intros.
-  elim H0; intros.
-  apply conj.
-  apply (included_mapped _ _ r H); auto.
-  intros.
-  apply (included_mapped _ _ r0 H).
-  apply H2; auto.
+  unfold type_function; intros until env.
+  set (instrs := PTree.elements f.(fn_code)).
+  case (infer_type_environment f instrs).
+  intro env'. 
+  caseEq (check_regs env' f.(fn_params) f.(fn_sig).(sig_args)); intro; simpl; try congruence.
+  caseEq (check_params_norepet f.(fn_params)); intro; simpl; try congruence.
+  caseEq (check_instrs f env' instrs); intro; simpl; try congruence.
+  intro EQ; inversion EQ; subst env'.
+  constructor. 
+  apply check_regs_correct; auto.
+  unfold check_params_norepet in H0. 
+  destruct (list_norepet_dec Reg.eq (fn_params f)). auto. discriminate.
+  intros. eapply check_instrs_correct. eauto. 
+  unfold instrs. apply PTree.elements_correct. eauto.
+  congruence.
 Qed.
 
-Lemma definite_included :
-  forall (u1 u2 : Uf.T) (i : instruction),
-  included u1 u2 -> definite u1 i -> definite u2 i.
+Lemma type_external_function_correct:
+  forall ef,
+  type_external_function ef = true ->
+  Conventions.sig_external_ok ef.(ef_sig).
 Proof.
-  unfold definite.
-  intros.
-  destruct i; try apply (included_mapped_forall _ _ _ _ H H0); auto.
-  destruct o; try apply (included_mapped_forall _ _ _ _ H H0); auto.
-  destruct l; auto.
-  apply (included_mapped_forall _ _ _ _ H H0).
-  destruct l; auto.
-  apply (included_mapped_forall _ _ _ _ H H0).
-  destruct s0; auto.
-  elim H0; intros.
-  apply conj.
-  apply (included_mapped _ _ _ H H1).
-  apply (included_mapped_forall _ _ _ _ H H2).
-  elim H0; intros.
-  apply conj; auto.
-  apply (included_mapped_forall _ _ _ _ H H2).
-  intros.
-  apply (included_mapped _ _ _ H (H0 r H1)).
-  destruct o; auto.
-  apply (included_mapped _ _ _ H H0).
+  intro ef. unfold type_external_function, Conventions.sig_external_ok.
+  generalize (Conventions.loc_arguments (ef_sig ef)).
+  induction l; simpl.
+  tauto.
+  destruct a. intros. firstorder congruence.
+  congruence.
 Qed.
 
-Lemma step4 :
-  forall (f : function) (u1 u3 : Uf.T) (i : instruction),
-  included u3 u1 ->
-  wt_instr (mk_env u3) f i ->
-  definite u3 i ->
-  consistent u1 ->
-    wt_instr (mk_env u1) f i.
-  Proof.
-    intros f u1 u3 i H1 H H0 X.
-    destruct H; try simpl in H0; try (elim H0; intros).
-     apply wt_Inop.
-     apply wt_Iopmove. unfold mk_env. rewrite (H1 _ _ H0). auto.
-     apply wt_Iopundef.
-     apply wt_Iop; auto.
-       destruct op; try congruence; simpl; simpl in H3;
-       simpl in H0; elim H0; intros; rewrite (mapped_included_consistent _ _ _ H4 H1 X);
-       rewrite (mapped_list_included _ _ _ H5 H1); auto.
-     apply wt_Iload.
-      rewrite (mapped_list_included _ _ _ H4 H1); auto.
-      rewrite (mapped_included_consistent _ _ _ H3 H1 X). auto.
-     apply wt_Istore.
-      rewrite (mapped_list_included _ _ _ H4 H1); auto.
-      rewrite (mapped_included_consistent _ _ _ H3 H1 X). auto.
-     elim H5; intros; destruct ros; apply wt_Icall.
-      rewrite (mapped_included_consistent _ _ _ H4 H1 X); auto.
-      rewrite (mapped_list_included _ _ _ H7 H1); auto.
-      rewrite (mapped_included_consistent _ _ _ H6 H1 X); auto.
-      auto.
-      rewrite (mapped_list_included _ _ _ H7 H1); auto.
-      rewrite (mapped_included_consistent _ _ _ H6 H1 X); auto.
-     apply wt_Icond. rewrite (mapped_list_included _ _ _ H0 H1); auto.
-     apply wt_Ireturn.
-      destruct optres; destruct f.(fn_sig).(sig_res);
-        simpl in H; simpl; try congruence.
-        rewrite (mapped_included_consistent _ _ _ H0 H1 X); auto.
-  Qed.
-
-Lemma type_rtl_function_instrs :
-  forall (f: function) (env: regenv),
-  type_rtl_function f = Some env
-  -> forall pc i, f.(fn_code)!pc = Some i -> wt_instr env f i.
-  Proof.
-    intros.
-    elim (step1 _ _ H).
-    intros.
-    elim H1.
-    intros.
-    elim H3.
-    intros.
-    rewrite H4.
-    elim (step2 _ _ _ (included_consistent _ _ H2 H5) _ _ H0).
-    intros.
-    elim H6. intros.
-    elim (step3 x0 f _ _ _ H0); auto. intros.
-    apply (step4 f _ _ i H2); auto.
-    apply (step4 _ _ _ _ H8 H9 H10).
-    apply (included_consistent _ _ H2); auto.
-    apply (definite_included _ _ _ H8 H10); auto.
-  Qed.
-
-(** Combining the sub-proofs. *)
-
-Theorem type_rtl_function_correct:
-  forall (f: function) (env: regenv),
-  type_rtl_function f = Some env -> wt_function env f.
-  Proof.
-    intros.
-    exact (mk_wt_function env f (type_rtl_function_params f _ H)
-                                (type_rtl_function_norepet f _ H)
-                                (type_rtl_function_instrs f _ H)).
-  Qed.
-
-Definition wt_program (p: program) : Prop :=
-  forall i f, In (i, f) (prog_funct p) -> type_rtl_function f <> None.
-
 (** * Type preservation during evaluation *)
 
 (** The type system for RTL is not sound in that it does not guarantee
@@ -1143,6 +358,7 @@ Require Import Globalenvs.
 Require Import Values.
 Require Import Mem.
 Require Import Integers.
+Require Import Events.
 
 Definition wt_regset (env: regenv) (rs: regset) : Prop :=
   forall r, Val.has_type (rs#r) (env r).
@@ -1180,6 +396,14 @@ Proof.
   apply wt_regset_assign; auto.
 Qed.
 
+Lemma wt_event_match:
+  forall ef args t res,
+  event_match ef args t res ->
+  Val.has_type res (proj_sig_res ef.(ef_sig)).
+Proof.
+  induction 1. inversion H0; exact I.
+Qed.
+
 Section SUBJECT_REDUCTION.
 
 Variable p: program.
@@ -1190,26 +414,24 @@ Let ge := Genv.globalenv p.
 
 Definition exec_instr_subject_reduction
     (c: code) (sp: val)
-    (pc: node) (rs: regset) (m: mem)
+    (pc: node) (rs: regset) (m: mem) (t: trace)
     (pc': node) (rs': regset) (m': mem) : Prop :=
   forall env f
          (CODE: c = fn_code f)
-         (WT_FN: wt_function env f)
+         (WT_FN: wt_function f env)
          (WT_RS: wt_regset env rs),
   wt_regset env rs'.
 
 Definition exec_function_subject_reduction
-    (f: function) (args: list val) (m: mem) (res: val) (m': mem) : Prop :=
-  forall env,
-  wt_function env f ->  
-  Val.has_type_list args f.(fn_sig).(sig_args) ->
-  Val.has_type res
-    (match f.(fn_sig).(sig_res) with None => Tint | Some ty => ty end).
+    (f: fundef) (args: list val) (m: mem) (t: trace) (res: val) (m': mem) : Prop :=
+  wt_fundef f ->  
+  Val.has_type_list args (sig_args (funsig f)) ->
+  Val.has_type res (proj_sig_res (funsig f)).
 
 Lemma subject_reduction:
-  forall f args m res m',
-  exec_function ge f args m res m' ->
-  exec_function_subject_reduction f args m res m'.
+  forall f args m t res m',
+  exec_function ge f args m t res m' ->
+  exec_function_subject_reduction f args m t res m'.
 Proof.
   apply (exec_function_ind_3 ge
            exec_instr_subject_reduction
@@ -1217,7 +439,7 @@ Proof.
            exec_function_subject_reduction);
   intros; red; intros;
   try (rewrite CODE in H;
-       generalize (wt_instrs env _ WT_FN pc _ H);
+       generalize (wt_instrs _ _ WT_FN pc _ H);
        intro WT_INSTR;
        inversion WT_INSTR).
  
@@ -1233,7 +455,7 @@ Proof.
 
   apply wt_regset_assign. auto.
   replace (env res) with (snd (type_of_operation op)).
-  apply type_of_operation_sound with function ge rs##args sp; auto.
+  apply type_of_operation_sound with fundef ge rs##args sp; auto.
   rewrite <- H7. reflexivity.
 
   apply wt_regset_assign. auto. rewrite H8. 
@@ -1241,37 +463,39 @@ Proof.
 
   assumption.
 
-  apply wt_regset_assign. auto. rewrite H11. rewrite H1.
-  assert (type_rtl_function f <> None).
+  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 function p (rs#r).
+    pattern f. apply Genv.find_funct_prop with fundef 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 function p b.
+    pattern f. apply Genv.find_funct_ptr_prop with fundef p b.
     exact wt_p. exact H0.
     discriminate.
-  assert (exists env1, wt_function env1 f).
-    caseEq (type_rtl_function f); intros; try congruence.
-    exists t. apply type_rtl_function_correct; auto.
-  elim H13; intros env1 WT_FN1. 
-  eapply H3. eexact WT_FN1. rewrite <- H1. rewrite <- H10.
+  eapply H3. auto. rewrite H1. rewrite <- H10.
   apply wt_regset_list; auto. 
 
+  apply wt_regset_assign. auto. rewrite H6; exact I. 
+
   assumption.
   assumption.
   assumption.
   eauto.
   eauto.
 
+  inversion H4; subst f0.
   assert (WT_INIT: wt_regset env (init_regs args (fn_params f))).
-    apply wt_init_regs. rewrite (wt_params env f H4). assumption.
-  generalize (H1 env f (refl_equal (fn_code f)) H4 WT_INIT). 
+    apply wt_init_regs. rewrite (wt_params _ _ H7). assumption.
+  generalize (H1 env f (refl_equal (fn_code f)) H7 WT_INIT). 
   intro WT_RS.
-  generalize (wt_instrs env _ H4 pc _ H2).
+  generalize (wt_instrs _ _ H7 pc _ H2).
   intro WT_INSTR; inversion WT_INSTR.
-  destruct or; simpl in H3; simpl in H7; rewrite <- H7.
+  unfold proj_sig_res; simpl.
+  destruct or; simpl in H3; simpl in H8; rewrite <- H8.
   rewrite H3. apply WT_RS. 
   rewrite H3. simpl; auto.
+
+  simpl. eapply wt_event_match; eauto.
 Qed. 
 
 End SUBJECT_REDUCTION.
-- 
cgit