RTLtyping: now performed entirely in Coq, no need for an external Caml oracle + a validator.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2157 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

2 files changed, 713 insertions, 371 deletions

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index f8dbfe4..a1f9518 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -12,6 +12,7 @@
 
 (** Typing rules and a type inference algorithm for RTL. *)
 
+Require Import Recdef.
 Require Import Coqlib.
 Require Import Errors.
 Require Import Maps.
@@ -160,266 +161,777 @@ Definition wt_program (p: program): Prop :=
 
 (** * Type inference *)
 
-(** There are several ways to ensure that RTL code is well-typed and
-  to obtain the typing environment (type assignment for pseudo-registers)
-  needed for register allocation.  One is to start with well-typed Cminor
-  code and show type preservation for RTL generation and RTL optimizations.
-  Another is to start with untyped RTL and run a type inference algorithm
-  that reconstructs the typing environment, determining the type of
-  each pseudo-register from its uses in the code.  We follow the second
-  approach.
+Section INFERENCE.
 
-  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. *)
+Local Open Scope error_monad_scope.
 
-Parameter infer_type_environment:
-  function -> list (node * instruction) -> option regenv.
+Variable f: function.
 
-(** ** Algorithm to check the correctness of a type environment *)
+(** The type inference engine operates over a state that has two components:
+- [te_typ]: a partial map from pseudoregisters to types, for
+  pseudoregs whose types are already determined from their uses;
+- [te_eqs]: a list of pairs [(r1,r2)] of pseudoregisters, indicating that
+  [r1] and [r2] must have the same type because they are involved in a move
+  [r1 := r2] or [r2 := r1], but this type is not yet determined.
+*)
 
-Section TYPECHECKING.
+Record typenv : Type := Typenv {
+  te_typ: PTree.t typ;            (**r mapping reg -> known type *)
+  te_eqs: list (reg * reg)        (**r pairs of regs that must have same type *)
+}.
 
-Variable funct: function.
-Variable env: regenv.
+(** Determine that [r] must have type [ty]. *)
 
-Definition check_reg (r: reg) (ty: typ): bool :=
-  if typ_eq (env r) ty then true else false.
+Definition type_reg (e: typenv) (r: reg) (ty: typ) : res typenv :=
+  match e.(te_typ)!r with
+  | None => OK {| te_typ := PTree.set r ty e.(te_typ); te_eqs := e.(te_eqs) |}
+  | Some ty' => if typ_eq ty ty' then OK e else Error (MSG "bad type for variable " :: POS r :: nil)
+  end.
 
-Fixpoint check_regs (rl: list reg) (tyl: list typ) {struct rl}: bool :=
+Fixpoint type_regs (e: typenv) (rl: list reg) (tyl: list typ) {struct rl}: res typenv :=
   match rl, tyl with
-  | nil, nil => true
-  | r1::rs, ty::tys => check_reg r1 ty && check_regs rs tys
-  | _, _ => false
+  | nil, nil => OK e
+  | r1::rs, ty1::tys => do e1 <- type_reg e r1 ty1; type_regs e1 rs tys
+  | _, _ => Error (msg "arity mismatch")
+  end.
+
+Definition type_ros (e: typenv) (ros: reg + ident) : res typenv :=
+  match ros with
+  | inl r => type_reg e r Tint
+  | inr s => OK e
+  end.
+
+(** Determine that [r1] and [r2] must have the same type.  If none of
+  [r1] and [r2] has known type, just record an equality constraint.
+  The boolean result is [true] if one of the types of [r1] and [r2]
+  was previously unknown and could be determined because the other type is
+  known.  Otherwise, [te_typ] does not change and [false] is returned. *)
+
+Function type_move (e: typenv) (r1 r2: reg) : res (bool * typenv) :=
+  match e.(te_typ)!r1, e.(te_typ)!r2 with
+  | None, None =>
+      OK (false, {| te_typ := e.(te_typ); te_eqs := (r1, r2) :: e.(te_eqs) |})
+  | Some ty1, None =>
+      OK (true, {| te_typ := PTree.set r2 ty1 e.(te_typ); te_eqs := e.(te_eqs) |})
+  | None, Some ty2 =>
+      OK (true, {| te_typ := PTree.set r1 ty2 e.(te_typ); te_eqs := e.(te_eqs) |})
+  | Some ty1, Some ty2 =>
+      if typ_eq ty1 ty2
+      then OK (false, e)
+      else Error(MSG "ill-typed move between " :: POS r1 :: MSG " and " :: POS r2 :: nil)
+  end.
+
+(** Checking the validity of successor nodes. *)
+
+Definition check_successor (s: node): res unit :=
+  match f.(fn_code)!s with
+  | None => Error (MSG "bad successor " :: POS s :: nil)
+  | Some i => OK tt
+  end.
+
+Fixpoint check_successors (sl: list node): res unit :=
+  match sl with
+  | nil => OK tt
+  | s1 :: sl' => do x <- check_successor s1; check_successors sl'
   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 is_move (op: operation) : bool :=
+  match op with Omove => true | _ => false end.
 
-Definition check_successor (s: node) : bool :=
-  match funct.(fn_code)!s with None => false | Some i => true end.
+(** First pass: check structural constraints and process all type constraints
+  of the form [typeof(r) = ty] arising from the RTL instructions.
+  Simultaneously, record equations [typeof(r1) = typeof(r2)] arising
+  from move instructions that cannot be immediately resolved. *)
 
-Definition check_instr (i: instruction) : bool :=
+Definition type_instr (e: typenv) (i: instruction) : res typenv :=
   match i with
   | Inop s =>
-      check_successor s
-  | Iop Omove (arg::nil) res s =>
-      if typ_eq (env arg) (env res) 
-      then check_successor s
-      else false
-  | Iop Omove args res s =>
-      false
+      do x <- check_successor s; OK e
   | Iop op args res s =>
-      check_op op args res && check_successor s
+      do x <- check_successor s;
+      if is_move op then
+        match args with
+        | arg :: nil => do (changed, e') <- type_move e arg res; OK e'
+        | _ => Error (msg "ill-formed move")
+        end
+      else
+       (let (targs, tres) := type_of_operation op in
+        do e1 <- type_regs e args targs; type_reg e1 res tres)
   | Iload chunk addr args dst s =>
-      check_regs args (type_of_addressing addr)
-      && check_reg dst (type_of_chunk chunk)
-      && check_successor s
+      do x <- check_successor s;
+      do e1 <- type_regs e args (type_of_addressing addr);
+      type_reg e1 dst (type_of_chunk chunk)
   | Istore chunk addr args src s =>
-      check_regs args (type_of_addressing addr)
-      && check_reg src (type_of_chunk chunk)
-      && check_successor s
+      do x <- check_successor s;
+      do e1 <- type_regs e args (type_of_addressing addr);
+      type_reg e1 src (type_of_chunk chunk)
   | Icall sig ros args res s =>
-      match ros with inl r => check_reg r Tint | inr s => true end
-      && check_regs args sig.(sig_args)
-      && check_reg res (proj_sig_res sig)
-      && check_successor s
+      do x <- check_successor s;
+      do e1 <- type_ros e ros;
+      do e2 <- type_regs e1 args sig.(sig_args);
+      type_reg e2 res (proj_sig_res sig)
   | Itailcall sig ros args =>
-      match ros with inl r => check_reg r Tint | inr s => true end
-      && check_regs args sig.(sig_args)
-      && opt_typ_eq sig.(sig_res) funct.(fn_sig).(sig_res)
-      && tailcall_is_possible sig
+      do e1 <- type_ros e ros;
+      do e2 <- type_regs e1 args sig.(sig_args);
+      if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then
+        if tailcall_is_possible sig
+        then OK e2
+        else Error(msg "tailcall not possible")
+      else Error(msg "bad return type in tailcall")
   | Ibuiltin ef args res s =>
-      check_regs args (ef_sig ef).(sig_args)
-      && check_reg res (proj_sig_res (ef_sig ef))
-      && (if ef_reloads ef then arity_ok (ef_sig ef).(sig_args) else true)
-      && check_successor s
+      let sig := ef_sig ef in
+      do x <- check_successor s;
+      do e1 <- type_regs e args sig.(sig_args);
+      do e2 <- type_reg e1 res (proj_sig_res sig);
+      if (negb (ef_reloads ef)) || arity_ok sig.(sig_args)
+      then OK e2
+      else Error(msg "cannot reload builtin")
   | Icond cond args s1 s2 =>
-      check_regs args (type_of_condition cond)
-      && check_successor s1
-      && check_successor s2
+      do x1 <- check_successor s1;
+      do x2 <- check_successor s2;
+      type_regs e args (type_of_condition cond)
   | Ijumptable arg tbl =>
-      check_reg arg Tint
-      && List.forallb check_successor tbl
-      && zle (list_length_z tbl * 4) Int.max_unsigned
+      do x <- check_successors tbl;
+      do e1 <- type_reg e arg Tint;
+      if zle (list_length_z tbl * 4) Int.max_unsigned then OK e1 else Error(msg "jumptable too big")
   | Ireturn optres =>
-      match optres, funct.(fn_sig).(sig_res) with
-      | None, None => true
-      | Some r, Some t => check_reg r t
-      | _, _ => false
+      match optres, f.(fn_sig).(sig_res) with
+      | None, None => OK e
+      | Some r, Some t => type_reg e r t
+      | _, _ => Error(msg "bad return")
       end
   end.
 
-Definition check_params_norepet (params: list reg): bool :=
-  if list_norepet_dec Reg.eq params then true else false.
+Definition type_code (e: typenv): res typenv :=
+  PTree.fold
+    (fun re pc i =>
+       match re with
+       | Error _ => re
+       | OK e =>
+           match type_instr e i with
+           | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg)
+           | OK e' => OK e'
+           end
+       end)
+    f.(fn_code) (OK e).
+
+(** Second pass: iteratively process the remaining equality constraints
+    arising out of "move" instructions *)
 
-Fixpoint check_instrs (instrs: list (node * instruction)) : bool :=
-  match instrs with
-  | nil => true
-  | (pc, i) :: rem => check_instr i && check_instrs rem
+Definition equations := list (reg * reg).
+
+Fixpoint solve_rec (e: typenv) (changed: bool) (q: equations) : res (typenv * bool) :=
+  match q with 
+  | nil =>
+      OK (e, changed)
+  | (r1, r2) :: q' =>
+      do (changed1, e1) <- type_move e r1 r2; solve_rec e1 (changed || changed1) q'
   end.
 
-(** ** Correctness of the type-checking algorithm *)
+Lemma type_move_length:
+  forall e r1 r2 changed e',
+  type_move e r1 r2 = OK (changed, e') ->
+  if changed 
+  then List.length e'.(te_eqs) = List.length e.(te_eqs)
+  else (List.length e'.(te_eqs) <= S (List.length e.(te_eqs)))%nat.
+Proof.
+  intros. functional inversion H; subst; simpl; omega.
+Qed.
+
+Lemma solve_rec_length:
+  forall q e changed e' changed',
+  solve_rec e changed q = OK (e', changed') ->
+  (List.length e'.(te_eqs) <= List.length e.(te_eqs) + List.length q)%nat.
+Proof.
+  induction q; simpl; intros. 
+- inv H. omega.
+- destruct a as [r1 r2]. monadInv H. 
+  assert (length (te_eqs x0) <= S (length (te_eqs e)))%nat.
+  {
+    exploit type_move_length; eauto. destruct x; omega. 
+  }
+  exploit IHq; eauto. 
+  omega.
+Qed.
 
-Ltac elimAndb :=
-  match goal with
-  | [ H: _ && _ = true |- _ ] =>
-      elim (andb_prop _ _ H); clear H; intros; elimAndb
-  | _ =>
-      idtac
+Lemma solve_rec_shorter:
+  forall q e e',
+  solve_rec e false q = OK (e', true) ->
+  (List.length e'.(te_eqs) < List.length e.(te_eqs) + List.length q)%nat.
+Proof.
+  induction q; simpl; intros.
+- discriminate.
+- destruct a as [r1 r2]; monadInv H.
+  exploit type_move_length; eauto. destruct x; intros. 
+  exploit solve_rec_length; eauto. omega.
+  exploit IHq; eauto. omega.
+Qed.
+
+Definition length_typenv (e: typenv) := length e.(te_eqs).
+
+Function solve_equations (e: typenv) {measure length_typenv e} : res typenv :=
+  match solve_rec {| te_typ := e.(te_typ); te_eqs := nil |} false e.(te_eqs) with
+  | OK (e', false) => OK e                    (**r no progress made: terminate *)
+  | OK (e', true) => solve_equations e'       (**r at least one type changed: iterate *)
+  | Error msg => Error msg
   end.
+Proof.
+  intros. exploit solve_rec_shorter; eauto. 
+Qed.
+
+(** The final type assignment aribtrarily gives type [Tint] to the 
+  pseudoregs that are still unconstrained at the end of type inference. *)
+
+Definition make_regenv (e: typenv) : regenv :=
+  fun r => match e.(te_typ)!r with Some ty => ty | None => Tint end.
+
+Definition check_params_norepet (params: list reg): res unit :=
+  if list_norepet_dec Reg.eq params then OK tt else Error(msg "duplicate parameters").
 
-Lemma check_reg_correct:
-  forall r ty, check_reg r ty = true -> env r = ty.
+Definition type_function : res regenv :=
+  do e1 <- type_code {| te_typ := PTree.empty typ; te_eqs := nil |};
+  do e2 <- type_regs e1 f.(fn_params) f.(fn_sig).(sig_args);
+  do e3 <- solve_equations e2;
+  do x1 <- check_params_norepet f.(fn_params);
+  do x2 <- check_successor f.(fn_entrypoint);
+  OK (make_regenv e3).
+
+(** ** Soundness proof *)
+
+(** What it means for a final type assignment [te] to satisfy the constraints
+  collected so far in the [e] state. *)
+
+Definition satisf (te: regenv) (e: typenv) : Prop :=
+     (forall r ty, e.(te_typ)!r = Some ty -> te r = ty)
+  /\ (forall r1 r2, In (r1, r2) e.(te_eqs) -> te r1 = te r2).
+
+Remark type_reg_incr:
+  forall e r ty e' te, type_reg e r ty = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  unfold type_reg; intros; destruct (e.(te_typ)!r) eqn:E.
+  destruct (typ_eq ty t); inv H. auto.
+  inv H. destruct H0 as [A B]. split; intros.
+  apply A. simpl. rewrite PTree.gso; auto. congruence. 
+  apply B. simpl; auto. 
+Qed.
+
+Hint Resolve type_reg_incr: ty.
+
+Remark type_regs_incr:
+  forall rl tyl e e' te, type_regs e rl tyl = OK e' -> satisf te e' -> satisf te e.
 Proof.
-  unfold check_reg; intros.
-  destruct (typ_eq (env r) ty). auto. discriminate.
+  induction rl; simpl; intros; destruct tyl; try discriminate.
+  inv H; eauto with ty.
+  monadInv H. eauto with ty.
 Qed.
 
-Lemma check_regs_correct:
-  forall rl tyl, check_regs rl tyl = true -> List.map env rl = tyl.
+Hint Resolve type_regs_incr: ty.
+
+Remark type_ros_incr:
+  forall e ros e' te, type_ros e ros = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  unfold type_ros; intros. destruct ros. eauto with ty. inv H; auto with ty.
+Qed.
+
+Hint Resolve type_ros_incr: ty.
+
+Remark type_move_incr:
+  forall e r1 r2 changed e' te,
+  type_move e r1 r2 = OK (changed, e') ->
+  satisf te e' -> satisf te e.
 Proof.
-  induction rl; destruct tyl; simpl; intros.
-  auto. discriminate. discriminate.
-  elimAndb.
-  rewrite (check_reg_correct _ _ H). rewrite (IHrl tyl H0). auto.
+  intros. destruct H0 as [A B]. functional inversion H; subst; simpl in *.
+- split; auto. 
+- split; intros. apply A. rewrite PTree.gso; auto. congruence. auto. 
+- split; intros. apply A. rewrite PTree.gso; auto. congruence. auto.
+- split; auto.
 Qed.
 
-Lemma check_op_correct:
-  forall op args res,
-  check_op op args res = true ->
-  (List.map env args, env res) = type_of_operation op.
+Hint Resolve type_move_incr: ty.
+
+Lemma type_reg_sound:
+  forall e r ty e' te, type_reg e r ty = OK e' -> satisf te e' -> te r = ty.
 Proof.
-  unfold check_op; intros.
-  destruct (type_of_operation op) as [targs tres].
-  elimAndb. 
-  rewrite (check_regs_correct _ _ H).
-  rewrite (check_reg_correct _ _ H0).
+  unfold type_reg; intros. destruct H0 as [A B]. 
+  destruct (e.(te_typ)!r) as [t|] eqn:E.
+  destruct (typ_eq ty t); inv H. apply A; auto.
+  inv H. apply A. simpl. apply PTree.gss.
+Qed.
+
+Lemma type_regs_sound:
+  forall rl tyl e e' te, type_regs e rl tyl = OK e' -> satisf te e' -> map te rl = tyl.
+Proof.
+  induction rl; simpl; intros; destruct tyl; try discriminate.
+- auto.
+- monadInv H. f_equal; eauto. eapply type_reg_sound. eauto. eauto with ty. 
+Qed.
+
+Lemma type_ros_sound:
+  forall e ros e' te, type_ros e ros = OK e' -> satisf te e' ->
+  match ros with inl r => te r = Tint | inr s => True end.
+Proof.
+  unfold type_ros; intros. destruct ros. 
+  eapply type_reg_sound; eauto.
   auto.
 Qed.
 
-Lemma check_successor_correct:
-  forall s,
-  check_successor s = true -> valid_successor funct s.
-Proof.
-  intro; unfold check_successor, valid_successor.
-  destruct (fn_code funct)!s; intro.
-  exists i; auto.
-  discriminate.
-Qed.
-
-Lemma check_instr_correct:
-  forall i, check_instr i = true -> wt_instr env funct i.
-Proof.
-  unfold check_instr; intros; destruct i; elimAndb.
-  (* nop *)
-  constructor. apply check_successor_correct; auto.
-  (* op *)
-  destruct o; elimAndb;
-  try (apply wt_Iop; [ congruence
-                     | apply check_op_correct; auto
-                     | apply check_successor_correct; auto ]).
-  destruct l; try discriminate. destruct l; try discriminate.
-  destruct (typ_eq (env r0) (env r)); try discriminate.
-  apply wt_Iopmove; auto. apply check_successor_correct; auto.
-  (* load *)
-  constructor. apply check_regs_correct; auto. apply check_reg_correct; auto.
-  apply check_successor_correct; auto.
-  (* store *)
-  constructor. apply check_regs_correct; auto. apply check_reg_correct; auto.
-  apply check_successor_correct; auto.
-  (* call *)
+Lemma type_move_sound:
+  forall e r1 r2 changed e' te,
+  type_move e r1 r2 = OK (changed, e') -> satisf te e' -> te r1 = te r2.
+Proof.
+  intros. destruct H0 as [A B]. functional inversion H; subst; simpl in *.
+- apply B; auto.
+- rewrite (A r1 ty1). rewrite (A r2 ty1). auto. 
+  apply PTree.gss. rewrite PTree.gso; auto. congruence.
+- rewrite (A r1 ty2). rewrite (A r2 ty2). auto. 
+  rewrite PTree.gso; auto. congruence. apply PTree.gss.
+- erewrite ! A; eauto. 
+Qed.
+
+Lemma check_successor_sound:
+  forall s x, check_successor s = OK x -> valid_successor f s.
+Proof.
+  unfold check_successor, valid_successor; intros. 
+  destruct (fn_code f)!s; inv H. exists i; auto.
+Qed.
+
+Hint Resolve check_successor_sound: ty.
+
+Lemma check_successors_sound:
+  forall sl x, check_successors sl = OK x -> forall s, In s sl -> valid_successor f s.
+Proof.
+  induction sl; simpl; intros. 
+  contradiction.
+  monadInv H. destruct H0. subst a; eauto with ty. eauto. 
+Qed.
+
+Lemma type_instr_incr:
+  forall e i e' te,
+  type_instr e i = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  intros; destruct i; try (monadInv H); eauto with ty.
+- (* op *)
+  destruct (is_move o) eqn:ISMOVE.
+  destruct l; try discriminate. destruct l; monadInv EQ0. eauto with ty.
+  destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. eauto with ty.
+- (* tailcall *)
+  destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
+  destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
+  eauto with ty.
+- (* builtin *)
+  destruct (negb (ef_reloads e0) || arity_ok (sig_args (ef_sig e0))) eqn:E; inv EQ3.
+  eauto with ty.
+- (* jumptable *)
+  destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2.
+  eauto with ty.
+- (* return *)
+  simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate.
+  eauto with ty.
+  inv H; auto with ty.
+Qed.
+
+Lemma type_instr_sound:
+  forall e i e' te,
+  type_instr e i = OK e' -> satisf te e' -> wt_instr te f i.
+Proof.
+  intros; destruct i; try (monadInv H); simpl.
+- (* nop *)
+  constructor; eauto with ty.
+- (* op *)
+  destruct (is_move o) eqn:ISMOVE.
+  (* move *)
+  + assert (o = Omove) by (unfold is_move in ISMOVE; destruct o; congruence).
+    subst o.
+    destruct l; try discriminate. destruct l; monadInv EQ0.
+    constructor. eapply type_move_sound; eauto. eauto with ty.
+  + destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0.
+    apply wt_Iop. 
+    unfold is_move in ISMOVE; destruct o; congruence.
+    rewrite TYOP. f_equal. eapply type_regs_sound; eauto with ty. eapply type_reg_sound; eauto.
+    eauto with ty.
+- (* load *)
   constructor.
-  destruct s0; auto. apply check_reg_correct; auto.
-  apply check_regs_correct; auto.
-  apply check_reg_correct; auto.
-  apply check_successor_correct; auto.
-  (* tailcall *)
+  eapply type_regs_sound; eauto with ty. eapply type_reg_sound; eauto.
+  eauto with ty.
+- (* store *)
   constructor.
-  destruct s0; auto. apply check_reg_correct; auto.
-  eapply proj_sumbool_true; eauto.
-  apply check_regs_correct; auto.
-  apply tailcall_is_possible_correct; auto.
-  (* builtin *)
+  eapply type_regs_sound; eauto with ty. eapply type_reg_sound; eauto.
+  eauto with ty.
+- (* call *)
+  constructor. 
+  eapply type_ros_sound; eauto with ty. 
+  eapply type_regs_sound; eauto with ty.
+  eapply type_reg_sound; eauto.
+  eauto with ty.
+- (* tailcall *)
+  destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
+  destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
   constructor.
-  apply check_regs_correct; auto.
-  apply check_reg_correct; auto.
+  eapply type_ros_sound; eauto with ty. 
   auto.
-  destruct (ef_reloads e); auto. 
-  apply check_successor_correct; auto.
-  (* cond *)
-  constructor. apply check_regs_correct; auto.
-  apply check_successor_correct; auto.
-  apply check_successor_correct; auto.
-  (* jumptable *)
-  constructor. apply check_reg_correct; auto.
-  rewrite List.forallb_forall in H1. intros. apply check_successor_correct; auto.
-  eapply proj_sumbool_true. eauto.  
-  (* return *)
-  constructor. 
-  destruct o; simpl; destruct funct.(fn_sig).(sig_res); try discriminate.
-  rewrite (check_reg_correct _ _ H); auto.
+  eapply type_regs_sound; eauto with ty.
+  apply tailcall_is_possible_correct; auto.
+- (* builtin *)
+  destruct (negb (ef_reloads e0) || arity_ok (sig_args (ef_sig e0))) eqn:E; inv EQ3.
+  constructor.
+  eapply type_regs_sound; eauto with ty.
+  eapply type_reg_sound; eauto.
+  destruct (ef_reloads e0); auto.
+  eauto with ty.
+- (* cond *)
+  constructor.
+  eapply type_regs_sound; eauto with ty.
+  eauto with ty.
+  eauto with ty.
+- (* jumptable *)
+  destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2.
+  constructor.
+  eapply type_reg_sound; eauto.
+  eapply check_successors_sound; eauto. 
   auto.
+- (* return *)
+  simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate.
+  constructor. simpl. rewrite RES. f_equal. eapply type_reg_sound; eauto.
+  inv H. constructor. rewrite RES; auto. 
 Qed.
 
-Lemma check_instrs_correct:
-  forall instrs,
-  check_instrs instrs = true ->
-  forall pc i, In (pc, i) instrs -> wt_instr env funct i.
+Lemma type_code_sound:
+  forall e e' te,
+  type_code e = OK e' ->
+  forall pc i, f.(fn_code)!pc = Some i -> satisf te e' -> wt_instr te f i.
 Proof.
-  induction instrs; simpl; intros.
-  elim H0.
-  destruct a as [pc' i']. elimAndb. 
-  elim H0; intro.
-  inversion H2; subst pc' i'. apply check_instr_correct; auto.
-  eauto.
+  intros e0 e1 te TCODE.
+  set (P := fun c opte =>
+         match opte with
+         | Error _ => True
+         | OK e' => forall pc i, c!pc = Some i -> satisf te e' -> wt_instr te f i
+         end).
+  assert (P f.(fn_code) (OK e1)).
+  {
+    rewrite <- TCODE. unfold type_code. apply PTree_Properties.fold_rec; unfold P; intros. 
+    - (* extensionality *)
+      destruct a; auto. intros. rewrite <- H in H1. eapply H0; eauto. 
+    - (* base case *)
+      rewrite PTree.gempty in H; discriminate.
+    - (* inductive case *)
+      destruct a as [e|?]; auto. 
+      destruct (type_instr e v) as [e'|?] eqn:TYINSTR; auto.
+      intros. rewrite PTree.gsspec in H2. destruct (peq pc k). 
+      inv H2. eapply type_instr_sound; eauto. 
+      eapply H1; eauto. eapply type_instr_incr; eauto. 
+  }
+  intros; eapply H; eauto. 
 Qed.
 
-End TYPECHECKING.
+Lemma solve_rec_incr:
+  forall te q e changed e' changed',
+  solve_rec e changed q = OK (e', changed') -> satisf te e' -> satisf te e.
+Proof.
+  induction q; simpl; intros.
+- inv H; auto.
+- destruct a as [r1 r2]; monadInv H. eauto with ty. 
+Qed.
 
-(** ** The type inference function **)
+Lemma solve_rec_sound:
+  forall r1 r2 te q e changed e' changed',
+  solve_rec e changed q = OK (e', changed') -> satisf te e' -> In (r1, r2) q -> te r1 = te r2.
+Proof.
+  induction q; simpl; intros.
+- contradiction. 
+- destruct a as [r3 r4]; monadInv H. destruct H1 as [A|A].
+  inv A. eapply type_move_sound; eauto. eapply solve_rec_incr; eauto. 
+  eapply IHq; eauto.
+Qed.
 
-Open Scope string_scope.
+Lemma solve_rec_false:
+  forall q e changed e',
+  solve_rec e changed q = OK (e', false) -> changed = false.
+Proof.
+  induction q; simpl; intros. 
+- inv H; auto.
+- destruct a as [r1 r2]; monadInv H. exploit IHq; eauto. rewrite orb_false_iff. tauto. 
+Qed.
 
-Definition type_function (f: function): res regenv :=
-  let instrs := PTree.elements f.(fn_code) in
-  match infer_type_environment f instrs with
-  | None => Error (msg "RTL type inference error")
-  | 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
-      && check_successor f f.(fn_entrypoint)
-      then OK env
-      else Error (msg "RTL type checking error")
-  end.
+Lemma solve_rec_solved:
+  forall r1 r2 q e changed e',
+  solve_rec e changed q = OK (e', false) ->
+  In (r1, r2) q -> make_regenv e r1 = make_regenv e r2.
+Proof.
+  induction q; simpl; intros.
+- contradiction.
+- destruct a as [r3 r4]; monadInv H.
+  assert (x = false). 
+  { exploit solve_rec_false; eauto. rewrite orb_false_iff. tauto. }
+  subst x. functional inversion EQ.
+  + destruct H0 as [A|A]. 
+    inv A. unfold make_regenv. rewrite H1; rewrite H2; auto.
+    subst x0. exploit IHq; eauto.
+  + destruct H0 as [A|A]. 
+    inv A. unfold make_regenv. rewrite H1; rewrite H2; auto.
+    subst x0. exploit IHq; eauto.
+Qed.
 
-Lemma type_function_correct:
-  forall f env,
-  type_function f = OK env ->
-  wt_function f env.
-Proof.
-  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.
-  caseEq (check_successor f (fn_entrypoint f)); 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.
-  apply check_successor_correct. auto.
+Lemma solve_equations_incr:
+  forall te e e', solve_equations e = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  intros te e0; functional induction (solve_equations e0); intros.
+- inv H. auto.
+- exploit solve_rec_incr; eauto. intros [A B]. split; intros.
+  apply A; auto.
+  eapply solve_rec_sound; eauto. 
+- discriminate.
+Qed.
+
+Lemma solve_equations_sound:
+  forall e e', solve_equations e = OK e' -> satisf (make_regenv e') e'.
+Proof.
+  intros e0; functional induction (solve_equations e0); intros.
+- inv H. split; intros. 
+  unfold make_regenv; rewrite H; auto. 
+  exploit solve_rec_solved; eauto.
+- eauto.
+- discriminate.
+Qed.
+
+Theorem type_function_correct:
+  forall env, type_function = OK env -> wt_function f env.
+Proof.
+  unfold type_function; intros. monadInv H. 
+  exploit solve_equations_sound; eauto. intros SAT1.
+  exploit solve_equations_incr; eauto. intros SAT0.
+  exploit type_regs_incr; eauto. intros SAT.
+  constructor.
+- (* type of parameters *)
+  eapply type_regs_sound; eauto.
+- (* parameters are unique *)
+  unfold check_params_norepet in EQ2. 
+  destruct (list_norepet_dec Reg.eq (fn_params f)); inv EQ2; auto. 
+- (* instructions are well typed *)
+  intros; eapply type_code_sound; eauto.
+- (* entry point is valid *)
+  eauto with ty. 
+Qed.
+
+(** ** Completeness proof *)
+
+Lemma type_reg_complete:
+  forall te e r ty,
+  satisf te e -> te r = ty -> exists e', type_reg e r ty = OK e' /\ satisf te e'.
+Proof.
+  intros. unfold type_reg. 
+  destruct ((te_typ e)!r) as [ty'|] eqn: E.
+  exists e; split; auto. replace ty' with ty. apply dec_eq_true.
+  exploit (proj1 H); eauto. congruence. 
+  econstructor; split. reflexivity. 
+  destruct H as [A B]; split; simpl; intros; auto. 
+  rewrite PTree.gsspec in H. destruct (peq r0 r); auto. congruence. 
+Qed.
+
+Lemma type_regs_complete:
+  forall te rl tyl e,
+  satisf te e -> map te rl = tyl -> exists e', type_regs e rl tyl = OK e' /\ satisf te e'.
+Proof.
+  induction rl; simpl; intros; subst tyl.
+  exists e; auto.
+  destruct (type_reg_complete te e a (te a)) as [e1 [A B]]; auto.
+  exploit IHrl; eauto. intros [e' [C D]]. 
+  exists e'; split; auto. rewrite A; simpl; rewrite C; auto.
+Qed.
+
+Lemma type_ros_complete:
+  forall te ros e,
+  satisf te e ->
+  match ros with inl r => te r = Tint | inr s => True end ->
+  exists e', type_ros e ros = OK e' /\ satisf te e'.
+Proof.
+  intros; destruct ros; simpl. 
+  eapply type_reg_complete; eauto.
+  exists e; auto.
+Qed.
+
+Lemma type_move_complete:
+  forall te r1 r2 e,
+  satisf te e ->
+  te r1 = te r2 ->
+  exists changed e', type_move e r1 r2 = OK (changed, e') /\ satisf te e'.
+Proof.
+  intros. functional induction (type_move e r1 r2). 
+- econstructor; econstructor; split; eauto. 
+  destruct H as [A B]; split; simpl; intros; auto. 
+  destruct H; auto. congruence.
+- econstructor; econstructor; split; eauto. 
+  destruct H as [A B]; split; simpl; intros; auto. 
+  rewrite PTree.gsspec in H. destruct (peq r r2); auto. 
+  subst. exploit A; eauto. congruence. 
+- econstructor; econstructor; split; eauto. 
+  destruct H as [A B]; split; simpl; intros; auto. 
+  rewrite PTree.gsspec in H. destruct (peq r r1); auto. 
+  subst. exploit A; eauto. congruence.
+- econstructor; econstructor; split; eauto.
+- destruct H as [A B]. apply A in e0. apply A in e1. congruence. 
+Qed.
+
+Lemma check_successor_complete:
+  forall s, valid_successor f s -> check_successor s = OK tt.
+Proof.
+  unfold valid_successor, check_successor; intros. 
+  destruct H as [i EQ]; rewrite EQ; auto.
+Qed.
+
+Lemma type_instr_complete:
+  forall te e i,
+  satisf te e ->
+  wt_instr te f i ->
+  exists e', type_instr e i = OK e' /\ satisf te e'.
+Proof.
+  induction 2; simpl.
+- (* nop *)
+  econstructor; split. rewrite check_successor_complete; simpl; eauto. auto.
+- (* move *)
+  exploit type_move_complete; eauto. intros (changed & e' & A & B).
+  exists e'; split. rewrite check_successor_complete by auto; simpl. rewrite A; auto. auto.
+- (* other op *)
+  destruct (type_of_operation op) as [targ tres]. injection H1; clear H1; intros. 
+  exploit type_regs_complete. eauto. eauto. intros [e1 [A B]].
+  exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]].
+  exists e2; split; auto.
+  rewrite check_successor_complete by auto; simpl. 
+  replace (is_move op) with false. rewrite A; simpl; rewrite C; auto.
+  destruct op; reflexivity || congruence.
+- (* load *)
+  exploit type_regs_complete. eauto. eauto. intros [e1 [A B]].
+  exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]].
+  exists e2; split; auto.
+  rewrite check_successor_complete by auto; simpl. 
+  rewrite A; simpl; rewrite C; auto.
+- (* store *)
+  exploit type_regs_complete. eauto. eauto. intros [e1 [A B]].
+  exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]].
+  exists e2; split; auto.
+  rewrite check_successor_complete by auto; simpl. 
+  rewrite A; simpl; rewrite C; auto.
+- (* call *)
+  exploit type_ros_complete. eauto. eauto. intros [e1 [A B]].
+  exploit type_regs_complete. eauto. eauto. intros [e2 [C D]].
+  exploit type_reg_complete. eexact D. eauto. intros [e3 [E F]].
+  exists e3; split; auto. 
+  rewrite check_successor_complete by auto; simpl. 
+  rewrite A; simpl; rewrite C; simpl; rewrite E; auto.
+- (* tailcall *)
+  exploit type_ros_complete. eauto. eauto. intros [e1 [A B]].
+  exploit type_regs_complete. eauto. eauto. intros [e2 [C D]].
+  exists e2; split; auto. 
+  rewrite A; simpl; rewrite C; simpl. 
+  rewrite H1; rewrite dec_eq_true. 
+  replace (tailcall_is_possible sig) with true; auto. 
+  revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig). 
+  induction l; simpl; intros. auto.
+  exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl.
+  intros; apply H3; auto. 
+- (* builtin *)
+  exploit type_regs_complete. eauto. eauto. intros [e1 [A B]].
+  exploit type_reg_complete. eexact B. eauto. intros [e2 [C D]].
+  exists e2; split; auto.
+  rewrite check_successor_complete by auto; simpl. 
+  rewrite A; simpl; rewrite C; simpl.
+  destruct H2; rewrite H2. 
+  rewrite orb_true_r. auto. 
+  auto. 
+- (* cond *)
+  exploit type_regs_complete. eauto. eauto. intros [e1 [A B]].
+  exists e1; split; auto.
+  rewrite check_successor_complete by auto; simpl. 
+  rewrite check_successor_complete by auto; simpl.
+  auto.
+- (* jumptbl *)
+  exploit type_reg_complete. eauto. eauto. intros [e1 [A B]].
+  exists e1; split; auto.
+  replace (check_successors tbl) with (OK tt). simpl. 
+  rewrite A; simpl. apply zle_true; auto. 
+  revert H1. generalize tbl. induction tbl0; simpl; intros. auto. 
+  rewrite check_successor_complete by auto; simpl.
+  apply IHtbl0; intros; auto.
+- (* return *)
+  rewrite <- H0. destruct optres; simpl.
+  apply type_reg_complete; auto.
+  exists e; auto.
+Qed.
+
+Lemma type_code_complete:
+  forall te e,
+  (forall pc instr, f.(fn_code)!pc = Some instr -> wt_instr te f instr) ->
+  satisf te e ->
+  exists e', type_code e = OK e' /\ satisf te e'.
+Proof.
+  intros te e0 WTC SAT0.
+  set (P := fun c res =>
+        (forall pc i, c!pc = Some i -> wt_instr te f i) ->
+        exists e', res = OK e' /\ satisf te e').
+  assert (P f.(fn_code) (type_code e0)).
+  {
+    unfold type_code. apply PTree_Properties.fold_rec; unfold P; intros.
+    - apply H0. intros. apply H1 with pc. rewrite <- H; auto. 
+    - exists e0; auto. 
+    - destruct H1 as [e [A B]]. 
+      intros. apply H2 with pc. rewrite PTree.gso; auto. congruence.
+      subst a. 
+      destruct (type_instr_complete te e v) as [e' [C D]].
+      auto. apply H2 with k. apply PTree.gss. 
+      exists e'; split; auto. rewrite C; auto. 
+  }
+  apply H; auto.
+Qed.
+
+Lemma solve_rec_complete:
+  forall te q e changed,
+  satisf te e ->
+  (forall r1 r2, In (r1, r2) q -> te r1 = te r2) ->
+  exists e' changed', solve_rec e changed q = OK(e', changed') /\ satisf te e'.
+Proof.
+  induction q; simpl; intros. 
+- exists e; exists changed; auto.
+- destruct a as [r3 r4]. 
+  exploit type_move_complete. eauto. apply H0. left; eauto. 
+  intros (changed1 & e1 & A & B).
+  destruct (IHq e1 (changed || changed1)) as (e2 & changed2 & C & D); auto.
+  exists e2; exists changed2; split; auto. rewrite A; simpl; rewrite C; auto.
+Qed.
+
+Lemma solve_equations_complete:
+  forall te e,
+  satisf te e ->
+  exists e', solve_equations e = OK e' /\ satisf te e'.
+Proof.
+  intros te e0. functional induction (solve_equations e0); intros.
+- exists e; auto. 
+- destruct (solve_rec_complete te (te_eqs e) {| te_typ := te_typ e; te_eqs := nil |} false)
+  as (e1 & changed1 & A & B). 
+  destruct H; split; intros. apply H; auto. contradiction.
+  exact (proj2 H). 
+  rewrite e0 in A. inv A. auto. 
+- destruct (solve_rec_complete te (te_eqs e) {| te_typ := te_typ e; te_eqs := nil |} false)
+  as (e1 & changed1 & A & B). 
+  destruct H; split; intros. apply H; auto. contradiction.
+  exact (proj2 H).
   congruence.
 Qed.
 
+Theorem type_function_complete:
+  forall te, wt_function f te -> exists te, type_function = OK te.
+Proof.
+  intros. destruct H. 
+  destruct (type_code_complete te {| te_typ := PTree.empty typ; te_eqs := nil |}) as (e1 & A & B).
+  auto. split; simpl; intros. rewrite PTree.gempty in H; congruence. contradiction.
+  destruct (type_regs_complete te f.(fn_params) f.(fn_sig).(sig_args) e1) as (e2 & C & D); auto.
+  destruct (solve_equations_complete te e2) as (e3 & E & F); auto.
+  exists (make_regenv e3); unfold type_function. 
+  rewrite A; simpl. rewrite C; simpl. rewrite E; simpl. 
+  unfold check_params_norepet. rewrite pred_dec_true; auto. simpl. 
+  rewrite check_successor_complete by auto. auto. 
+Qed.
+
+End INFERENCE.
+
 (** * Type preservation during evaluation *)
 
 (** The type system for RTL is not sound in that it does not guarantee
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
deleted file mode 100644
index 5935605..0000000
--- a/backend/RTLtypingaux.ml
+++ /dev/null
@@ -1,170 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Type inference for RTL *)
-
-open Datatypes
-open Camlcoq
-open Maps
-open AST
-open Memdata
-open Op
-open Registers
-open RTL
-open PrintAST
-
-exception Type_error of string
-
-let env = ref (PTree.empty : typ PTree.t)
-
-let set_type r ty =
-  match PTree.get r !env with
-  | None -> env := PTree.set r ty !env
-  | Some ty' -> if ty <> ty' then raise (Type_error "type mismatch")
-
-let rec set_types rl tyl =
-  match rl, tyl with
-  | [], [] -> ()
-  | r1 :: rs, ty1 :: tys -> set_type r1 ty1; set_types rs tys
-  | _, _ -> raise (Type_error "arity mismatch")
-
-(* First pass: process constraints of the form typeof(r) = ty *)
-
-let type_instr retty (pc, i) =
-  match i with
-  | Inop(_) ->
-      ()
-  | Iop(Omove, _, _, _) -> 
-      ()
-  | Iop(op, args, res, _) ->
-      if two_address_op op && List.length args >= 1 && List.hd args <> res
-      then raise (Type_error "two-address constraint violation");
-      let (targs, tres) = type_of_operation op in
-      set_types args targs; set_type res tres
-  | Iload(chunk, addr, args, dst, _) ->
-      set_types args (type_of_addressing addr);
-      set_type dst (type_of_chunk chunk)
-  | Istore(chunk, addr, args, src, _) ->
-      set_types args (type_of_addressing addr);
-      set_type src (type_of_chunk chunk)
-  | Icall(sg, ros, args, res, _) ->
-      begin try
-        begin match ros with
-        | Coq_inl r -> set_type r Tint
-        | Coq_inr _ -> ()
-        end;
-        set_types args sg.sig_args;
-        set_type res (match sg.sig_res with None -> Tint | Some ty -> ty)
-      with Type_error msg ->
-        let name =
-          match ros with
-          | Coq_inl _ -> "<reg>"
-          | Coq_inr id -> extern_atom id in
-        raise(Type_error (Printf.sprintf "type mismatch in Icall(%s): %s"
-                                         name msg))
-      end
-  | Itailcall(sg, ros, args) ->
-      begin try
-        begin match ros with
-        | Coq_inl r -> set_type r Tint
-        | Coq_inr _ -> ()
-        end;
-        set_types args sg.sig_args;
-        if sg.sig_res <> retty then
-          raise (Type_error "mismatch on return type")
-      with Type_error msg ->
-        let name =
-          match ros with
-          | Coq_inl _ -> "<reg>"
-          | Coq_inr id -> extern_atom id in
-        raise(Type_error (Printf.sprintf "type mismatch in Itailcall(%s): %s"
-                                         name msg))
-      end
-  | Ibuiltin(ef, args, res, _) ->
-      begin try
-        let sg = ef_sig ef in
-        set_types args sg.sig_args;
-        set_type res (match sg.sig_res with None -> Tint | Some ty -> ty);
-        if ef_reloads ef && not (Conventions.arity_ok sg.sig_args) then
-          raise(Type_error "wrong arity")
-      with Type_error msg ->
-        raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s"
-                                         (name_of_external ef) msg))
-      end
-  | Icond(cond, args, _, _) ->
-      set_types args (type_of_condition cond)
-  | Ijumptable(arg, _) ->
-      set_type arg Tint
-  | Ireturn(optres) ->
-      begin match optres, retty with
-      | None, None -> ()
-      | Some r, Some ty -> set_type r ty
-      | _, _ -> raise (Type_error "type mismatch in Ireturn")
-      end
-
-let type_pass1 retty instrs = 
-  List.iter (type_instr retty) instrs
-
-(* Second pass: extract move constraints typeof(r1) = typeof(r2)
-   and solve them iteratively *)
-
-let rec extract_moves = function
-  | [] -> []
-  | (pc, i) :: rem ->
-      match i with
-      | Iop(Omove, [r1], r2, _) ->
-          (r1, r2) :: extract_moves rem
-      | Iop(Omove, _, _, _) ->
-          raise (Type_error "wrong Omove")
-      | _ ->
-          extract_moves rem
-
-let changed = ref false
-
-let rec solve_moves = function
-  | [] -> []
-  | (r1, r2) :: rem ->
-      match (PTree.get r1 !env, PTree.get r2 !env) with
-      | Some ty1, Some ty2 ->
-          if ty1 = ty2 
-          then (changed := true; solve_moves rem)
-          else raise (Type_error "type mismatch in Omove")
-      | Some ty1, None ->
-          env := PTree.set r2 ty1 !env; changed := true; solve_moves rem
-      | None, Some ty2 ->
-          env := PTree.set r1 ty2 !env; changed := true; solve_moves rem
-      | None, None ->
-          (r1, r2) :: solve_moves rem
-
-let rec iter_solve_moves mvs =
-  changed := false;
-  let mvs' = solve_moves mvs in
-  if !changed then iter_solve_moves mvs'
-
-let type_pass2 instrs =
-  iter_solve_moves (extract_moves instrs)
-
-let typeof e r =
-  match PTree.get r e with Some ty -> ty | None -> Tint
-
-let infer_type_environment f instrs =
-  try
-    env := PTree.empty;
-    set_types f.fn_params f.fn_sig.sig_args;
-    type_pass1 f.fn_sig.sig_res instrs;
-    type_pass2 instrs;
-    let e = !env in
-    env := PTree.empty;
-    Some(typeof e)
-  with Type_error msg ->
-    Printf.eprintf "Error during RTL type inference: %s\n" msg;
-    None