Merge of the float32 branch:

- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86


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

6 files changed, 967 insertions, 43 deletions

diff --git a/common/AST.v b/common/AST.v
index fba5354..1b1e872 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -35,17 +35,19 @@ Definition ident_eq := peq.
 
 Parameter ident_of_string : String.string -> ident.
 
-(** The intermediate languages are weakly typed, using only three
+(** The intermediate languages are weakly typed, using only four
   types: [Tint] for 32-bit integers and pointers, [Tfloat] for 64-bit
-  floating-point numbers, [Tlong] for 64-bit integers. *)
+  floating-point numbers, [Tlong] for 64-bit integers, [Tsingle]
+  for 32-bit floating-point numbers. *)
 
 Inductive typ : Type :=
   | Tint
   | Tfloat
-  | Tlong.
+  | Tlong
+  | Tsingle.
 
 Definition typesize (ty: typ) : Z :=
-  match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 end.
+  match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 | Tsingle => 4 end.
 
 Lemma typesize_pos: forall ty, typesize ty > 0.
 Proof. destruct ty; simpl; omega. Qed.
@@ -60,6 +62,26 @@ Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}
 Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
                      := list_eq_dec typ_eq.
 
+(** All values of type [Tsingle] are also of type [Tfloat].  This
+  corresponds to the following subtyping relation over types. *)
+
+Definition subtype (ty1 ty2: typ) : bool :=
+  match ty1, ty2 with
+  | Tint, Tint => true
+  | Tlong, Tlong => true
+  | Tfloat, Tfloat => true
+  | Tsingle, Tsingle => true
+  | Tsingle, Tfloat => true
+  | _, _ => false
+  end.
+
+Fixpoint subtype_list (tyl1 tyl2: list typ) : bool :=
+  match tyl1, tyl2 with
+  | nil, nil => true
+  | ty1::tys1, ty2::tys2 => subtype ty1 ty2 && subtype_list tys1 tys2
+  | _, _ => false
+  end.
+
 (** Additionally, function definitions and function calls are annotated
   by function signatures indicating the number and types of arguments,
   as well as the type of the returned value if any.  These signatures
@@ -110,6 +132,19 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
   | Mint16unsigned => Tint
   | Mint32 => Tint
   | Mint64 => Tlong
+  | Mfloat32 => Tsingle
+  | Mfloat64 => Tfloat
+  | Mfloat64al32 => Tfloat
+  end.
+
+Definition type_of_chunk_use (c: memory_chunk) : typ :=
+  match c with
+  | Mint8signed => Tint
+  | Mint8unsigned => Tint
+  | Mint16signed => Tint
+  | Mint16unsigned => Tint
+  | Mint32 => Tint
+  | Mint64 => Tlong
   | Mfloat32 => Tfloat
   | Mfloat64 => Tfloat
   | Mfloat64al32 => Tfloat
@@ -123,6 +158,7 @@ Definition chunk_of_type (ty: typ) :=
   | Tint => Mint32
   | Tfloat => Mfloat64al32
   | Tlong => Mint64
+  | Tsingle => Mfloat32
   end.
 
 (** Initialization data for global variables. *)
@@ -283,6 +319,25 @@ Proof.
   exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto.
 Qed.
 
+Lemma transform_partial_program2_succeeds:
+  forall p tp i g,
+  transform_partial_program2 p = OK tp ->
+  In (i, g) p.(prog_defs) ->
+  match g with
+  | Gfun fd => exists tfd, transf_fun fd = OK tfd
+  | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv
+  end.
+Proof.
+  intros. monadInv H. 
+  revert x EQ H0. induction (prog_defs p); simpl; intros.
+  contradiction.
+  destruct a as [id1 g1]. destruct g1.
+  destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. 
+  destruct H0. inv H. econstructor; eauto. eapply IHl; eauto.
+  destruct (transf_globvar v) eqn:TV; try discriminate. monadInv EQ.
+  destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto.
+Qed.
+
 Lemma transform_partial_program2_main:
   forall p tp,
   transform_partial_program2 p = OK tp ->
@@ -353,6 +408,16 @@ Proof.
   apply transform_partial_program2_function. 
 Qed.
 
+Lemma transform_partial_program_succeeds:
+  forall p tp i fd,
+  transform_partial_program p = OK tp ->
+  In (i, Gfun fd) p.(prog_defs) ->
+  exists tfd, transf_partial fd = OK tfd.
+Proof.
+  unfold transform_partial_program; intros. 
+  exploit transform_partial_program2_succeeds; eauto. 
+Qed.
+
 End TRANSF_PARTIAL_PROGRAM.
 
 Lemma transform_program_partial_program:
diff --git a/common/Events.v b/common/Events.v
index f342799..be1915a 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -57,6 +57,7 @@ Inductive eventval: Type :=
   | EVint: int -> eventval
   | EVlong: int64 -> eventval
   | EVfloat: float -> eventval
+  | EVfloatsingle: float -> eventval
   | EVptr_global: ident -> int -> eventval.
 
 Inductive event: Type :=
@@ -272,6 +273,9 @@ Inductive eventval_match: eventval -> typ -> val -> Prop :=
       eventval_match (EVlong i) Tlong (Vlong i)
   | ev_match_float: forall f,
       eventval_match (EVfloat f) Tfloat (Vfloat f)
+  | ev_match_single: forall f,
+      Float.is_single f ->
+      eventval_match (EVfloatsingle f) Tsingle (Vfloat f)
   | ev_match_ptr: forall id b ofs,
       Genv.find_symbol ge id = Some b ->
       eventval_match (EVptr_global id ofs) Tint (Vptr b ofs).
@@ -291,7 +295,7 @@ Lemma eventval_match_type:
   forall ev ty v,
   eventval_match ev ty v -> Val.has_type v ty.
 Proof.
-  intros. inv H; constructor.
+  intros. inv H; simpl; auto. 
 Qed.
 
 Lemma eventval_list_match_length:
@@ -330,7 +334,7 @@ Lemma eventval_match_inject:
   forall ev ty v1 v2,
   eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2.
 Proof.
-  intros. inv H; inv H0; try constructor.
+  intros. inv H; inv H0; try constructor; auto.
   destruct glob_pres as [A [B C]].
   exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ.
   rewrite Int.add_zero. econstructor; eauto. 
@@ -384,6 +388,7 @@ Definition eventval_valid (ev: eventval) : Prop :=
   | EVint _ => True
   | EVlong _ => True
   | EVfloat _ => True
+  | EVfloatsingle f => Float.is_single f
   | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b
   end.
 
@@ -392,25 +397,37 @@ Definition eventval_type (ev: eventval) : typ :=
   | EVint _ => Tint
   | EVlong _ => Tlong
   | EVfloat _ => Tfloat
+  | EVfloatsingle _ => Tsingle
   | EVptr_global id ofs => Tint
   end.
 
-Lemma eventval_valid_match:
-  forall ev ty,
-  eventval_valid ev -> eventval_type ev = ty -> exists v, eventval_match ev ty v.
-Proof.
-  intros. subst ty. destruct ev; simpl in *.
+Lemma eventval_match_receptive:
+  forall ev1 ty v1 ev2,
+  eventval_match ev1 ty v1 ->
+  eventval_valid ev1 -> eventval_valid ev2 -> eventval_type ev1 = eventval_type ev2 ->
+  exists v2, eventval_match ev2 ty v2.
+Proof.
+  intros. inv H; destruct ev2; simpl in H2; try discriminate.
+  exists (Vint i0); constructor.
+  destruct H1 as [b EQ]. exists (Vptr b i1); constructor; auto.
+  exists (Vlong i0); constructor.
+  exists (Vfloat f1); constructor.
+  exists (Vfloat f1); constructor; auto.
   exists (Vint i); constructor.
-  exists (Vlong i); constructor.
-  exists (Vfloat f0); constructor.
-  destruct H as [b A]. exists (Vptr b i0); constructor; auto.
+  destruct H1 as [b' EQ]. exists (Vptr b' i0); constructor; auto.
 Qed.
 
 Lemma eventval_match_valid:
-  forall ev ty v,
-  eventval_match ev ty v -> eventval_valid ev /\ eventval_type ev = ty.
+  forall ev ty v, eventval_match ev ty v -> eventval_valid ev.
 Proof.
-  induction 1; simpl; auto. split; auto. exists b; auto.
+  destruct 1; simpl; auto. exists b; auto.
+Qed.
+
+Lemma eventval_match_same_type:
+  forall ev1 ty v1 ev2 v2,
+  eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 -> eventval_type ev1 = eventval_type ev2.
+Proof.
+  destruct 1; intros EV; inv EV; auto. 
 Qed.
 
 End EVENTVAL.
@@ -430,7 +447,7 @@ Lemma eventval_match_preserved:
   forall ev ty v,
   eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v.
 Proof.
-  induction 1; constructor. rewrite symbols_preserved; auto. 
+  induction 1; constructor; auto. rewrite symbols_preserved; auto. 
 Qed.
 
 Lemma eventval_list_match_preserved:
@@ -753,9 +770,8 @@ Lemma volatile_load_receptive:
   exists v2, volatile_load ge chunk m b ofs t2 v2.
 Proof.
   intros. inv H; inv H0.
-  exploit eventval_match_valid; eauto. intros [A B]. 
-  exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. 
-  intros [v' EVM]. exists (Val.load_result chunk v'). constructor; auto.
+  exploit eventval_match_receptive; eauto. intros [v' EM].
+  exists (Val.load_result chunk v'). constructor; auto.
   exists v1; constructor; auto.
 Qed.
 
@@ -766,8 +782,7 @@ Lemma volatile_load_ok:
 Proof.
   intros; constructor; intros.
 (* well typed *)
-  unfold proj_sig_res; simpl. inv H. inv H0.
-  destruct chunk; destruct v; simpl; constructor.
+  unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. 
   eapply Mem.load_type; eauto. 
 (* arity *)
   inv H; inv H0; auto.
@@ -796,15 +811,17 @@ Proof.
 (* determ *)
   inv H; inv H0. inv H1; inv H7; try congruence.
   assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0.
-  exploit eventval_match_valid. eexact H2. intros [V1 T1].
-  exploit eventval_match_valid. eexact H4. intros [V2 T2].
-  split. constructor; auto. congruence.
+  split. constructor. 
+  eapply eventval_match_valid; eauto.
+  eapply eventval_match_valid; eauto.
+  eapply eventval_match_same_type; eauto.
   intros EQ; inv EQ. 
   assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0.
   auto.
   split. constructor. intuition congruence.
 Qed.
 
+
 Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int)
                                    (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
@@ -830,8 +847,7 @@ Lemma volatile_load_global_ok:
 Proof.
   intros; constructor; intros.
 (* well typed *)
-  unfold proj_sig_res; simpl. inv H. inv H1.
-  destruct chunk; destruct v; simpl; constructor.
+  unfold proj_sig_res; simpl. inv H. inv H1. apply Val.load_result_type.
   eapply Mem.load_type; eauto. 
 (* arity *)
   inv H; inv H1; auto.
@@ -1450,15 +1466,15 @@ Proof.
   inv H; simpl; omega.
 (* receptive *)
   inv H; inv H0.
-  exploit eventval_match_valid; eauto. intros [A B]. 
-  exploit eventval_valid_match. eexact H7. rewrite <- H8; eauto. 
-  intros [v' EVM]. exists v'; exists m1. econstructor; eauto. 
+  exploit eventval_match_receptive; eauto. intros [v' EVM].
+  exists v'; exists m1. econstructor; eauto. 
 (* determ *)
   inv H; inv H0.
   assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0.
-  exploit eventval_match_valid. eexact H2. intros [V1 T1].
-  exploit eventval_match_valid. eexact H3. intros [V2 T2].
-  split. constructor; auto. congruence.
+  split. constructor.
+  eapply eventval_match_valid; eauto.
+  eapply eventval_match_valid; eauto.
+  eapply eventval_match_same_type; eauto.
   intros EQ; inv EQ. split; auto. eapply eventval_match_determ_1; eauto.
 Qed.
 
diff --git a/common/Memdata.v b/common/Memdata.v
index c62ba99..47f8471 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -473,7 +473,7 @@ Lemma decode_val_type:
 Proof.
   intros. unfold decode_val. 
   destruct (proj_bytes cl). 
-  destruct chunk; simpl; auto. 
+  destruct chunk; simpl; auto. apply Float.single_of_bits_is_single.
   destruct chunk; simpl; auto.
   unfold proj_pointer. destruct cl; try (exact I).
   destruct m; try (exact I).
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index c18b09d..9768447 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -16,7 +16,11 @@ open Printf
 open Camlcoq
 open AST
 
-let name_of_type = function Tint -> "int" | Tfloat -> "float" | Tlong -> "long"
+let name_of_type = function
+  | Tint -> "int"
+  | Tfloat -> "float"
+  | Tlong -> "long"
+  | Tsingle -> "single"
 
 let name_of_chunk = function
   | Mint8signed -> "int8signed"
diff --git a/common/Subtyping.v b/common/Subtyping.v
new file mode 100644
index 0000000..e1bf61a
--- /dev/null
+++ b/common/Subtyping.v
@@ -0,0 +1,808 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* A solver for subtyping constraints. *)
+
+Require Import Recdef Coqlib Maps Errors.
+
+Local Open Scope nat_scope.
+Local Open Scope error_monad_scope.
+
+(** This module provides a solver for sets of subtyping constraints of the
+  following kinds: [base-type <: T(x)] or [T(x) <: base-type] or [T(x) <: T(y)].
+  The unknowns are the types [T(x)] of every identifier [x]. *)
+
+(** The interface for base types and the subtyping relation. *)
+
+Module Type TYPE_ALGEBRA.
+
+(** Type expressions *)
+
+Variable t: Type.
+Variable eq: forall (x y: t), {x=y} + {x<>y}.
+Variable default: t.
+
+(** Subtyping *)
+
+Variable sub: t -> t -> Prop.
+Hypothesis sub_refl: forall x, sub x x.
+Hypothesis sub_trans: forall x y z, sub x y -> sub y z -> sub x z.
+Variable sub_dec: forall x y, {sub x y} + {~sub x y}.
+
+(** Least upper bounds. [lub x y] is specified only when [x] and [y] have
+  a common supertype; it can be arbitrary otherwise. *)
+
+Variable lub: t -> t -> t.
+Hypothesis lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y).
+Hypothesis lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y).
+Hypothesis lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z.
+
+(** Greater lower bounds. [glb x y] is specified only when [x] and [y] have
+  a common subtype; it can be arbitrary otherwise.*)
+
+Variable glb: t -> t -> t.
+Hypothesis glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x.
+Hypothesis glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y.
+Hypothesis glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y).
+
+(** Low and high bounds for a given type. *)
+Variable low_bound: t -> t.
+Variable high_bound: t -> t.
+Hypothesis low_bound_sub: forall t, sub (low_bound t) t.
+Hypothesis low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x.
+Hypothesis high_bound_sub: forall t, sub t (high_bound t).
+Hypothesis high_bound_majorant: forall x y, sub x y -> sub y (high_bound x).
+
+(** Measure over types *)
+
+Variable weight: t -> nat.
+Variable max_weight: nat.
+Hypothesis weight_range: forall t, weight t <= max_weight.
+Hypothesis weight_sub: forall x y, sub x y -> weight x <= weight y.
+Hypothesis weight_sub_strict: forall x y, sub x y -> x <> y -> weight x < weight y.
+
+End TYPE_ALGEBRA.
+
+(** The constraint solver. *)
+
+Module SubSolver (T: TYPE_ALGEBRA).
+
+(* The current set of constraints is represented by a record with two components:
+- [te_typ]: a partial map from variables to pairs [tlo, thi]
+  of types, representing the low and high bounds for this variable.
+- [te_sub]: a list of pairs [(x,y)] of variables, indicating that
+  the type of [x] must be a subtype of the type of [y].
+*)
+
+Inductive bounds : Type := B (lo: T.t) (hi: T.t) (SUB: T.sub lo hi).
+
+Definition constraint : Type := (positive * positive)%type.
+
+Record typenv : Type := Typenv {
+  te_typ: PTree.t bounds;    (**r mapping var -> low & high bounds *)
+  te_sub: list constraint    (**r additional subtyping constraints *)
+}.
+
+Definition initial : typenv := {| te_typ := PTree.empty _; te_sub := nil |}.
+
+(** Add the constraint [ty <: T(x)]. *)
+
+Definition type_def (e: typenv) (x: positive) (ty: T.t) : res typenv :=
+  match e.(te_typ)!x with
+  | None =>
+      let b := B ty (T.high_bound ty) (T.high_bound_sub ty) in
+      OK {| te_typ := PTree.set x b e.(te_typ);
+            te_sub := e.(te_sub) |}
+  | Some(B lo hi s1) =>
+      match T.sub_dec ty hi with
+      | left s2 =>
+          let lo' := T.lub lo ty in
+          if T.eq lo lo' then OK e else
+            let b := B lo' hi (T.lub_min lo ty hi s1 s2) in
+            OK {| te_typ := PTree.set x b e.(te_typ);
+                  te_sub := e.(te_sub) |}
+      | right _ =>
+          Error (MSG "bad definition of variable " :: POS x :: nil)
+      end
+  end.
+
+Fixpoint type_defs (e: typenv) (rl: list positive) (tyl: list T.t) {struct rl}: res typenv :=
+  match rl, tyl with
+  | nil, nil => OK e
+  | r1::rs, ty1::tys => do e1 <- type_def e r1 ty1; type_defs e1 rs tys
+  | _, _ => Error (msg "arity mismatch")
+  end.
+
+(** Add the constraint [T(x) <: ty]. *)
+
+Definition type_use (e: typenv) (x: positive) (ty: T.t) : res typenv :=
+  match e.(te_typ)!x with
+  | None =>
+      let b := B (T.low_bound ty) ty (T.low_bound_sub ty) in
+      OK {| te_typ := PTree.set x b e.(te_typ);
+            te_sub := e.(te_sub) |}
+  | Some(B lo hi s1) =>
+      match T.sub_dec lo ty with
+      | left s2 =>
+          let hi' := T.glb hi ty in
+          if T.eq hi hi' then OK e else
+            let b := B lo hi' (T.glb_max hi ty lo s1 s2) in
+            OK {| te_typ := PTree.set x b e.(te_typ);
+                  te_sub := e.(te_sub) |}
+      | right _ =>
+          Error (MSG "bad use of variable " :: POS x :: nil)
+      end
+  end.
+
+Fixpoint type_uses (e: typenv) (rl: list positive) (tyl: list T.t) {struct rl}: res typenv :=
+  match rl, tyl with
+  | nil, nil => OK e
+  | r1::rs, ty1::tys => do e1 <- type_use e r1 ty1; type_uses e1 rs tys
+  | _, _ => Error (msg "arity mismatch")
+  end.
+
+(** Add the constraint [T(x) <: T(y)].
+    The boolean result is [true] if the types of [r1] and [r2] could be
+    made more precise.  Otherwise, [te_typ] does not change and
+    [false] is returned. *)
+
+Definition type_move (e: typenv) (r1 r2: positive) : res (bool * typenv) :=
+  if peq r1 r2 then OK (false, e) else
+  match e.(te_typ)!r1, e.(te_typ)!r2 with
+  | None, None =>
+      OK (false, {| te_typ := e.(te_typ); te_sub := (r1, r2) :: e.(te_sub) |})
+  | Some(B lo1 hi1 s1), None =>
+      let b2 := B lo1 (T.high_bound lo1) (T.high_bound_sub lo1) in
+      OK (true, {| te_typ := PTree.set r2 b2 e.(te_typ);
+                   te_sub := if T.sub_dec hi1 lo1 then e.(te_sub)
+                             else (r1, r2) :: e.(te_sub) |})
+  | None, Some(B lo2 hi2 s2) =>
+      let b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2) in
+      OK (true, {| te_typ := PTree.set r1 b1 e.(te_typ);
+                   te_sub := if T.sub_dec hi2 lo2 then e.(te_sub)
+                             else (r1, r2) :: e.(te_sub) |})
+  | Some(B lo1 hi1 s1), Some(B lo2 hi2 s2) =>
+      if T.sub_dec hi1 lo2 then
+        (* The constraint is always true, don't record it *)
+        OK (false, e)
+      else match T.sub_dec lo1 hi2 with
+      | left s =>
+          (* Tighten the bounds on [r1] and [r2] when possible and record
+             the constraint. *)
+          let lo2' := T.lub lo1 lo2 in
+          let hi1' := T.glb hi1 hi2 in
+          let b1 := B lo1 hi1' (T.glb_max hi1 hi2 lo1 s1 s) in
+          let b2 := B lo2' hi2 (T.lub_min lo1 lo2 hi2 s s2) in
+          if T.eq lo2 lo2' then
+            if T.eq hi1 hi1' then
+              OK (false, {| te_typ := e.(te_typ);
+                            te_sub := (r1, r2) :: e.(te_sub) |})
+            else
+              OK (true, {| te_typ := PTree.set r1 b1 e.(te_typ);
+                           te_sub := (r1, r2) :: e.(te_sub) |})
+          else
+            if T.eq hi1 hi1' then
+              OK (true, {| te_typ := PTree.set r2 b2 e.(te_typ);
+                           te_sub := (r1, r2) :: e.(te_sub) |})
+            else
+              OK (true, {| te_typ := PTree.set r2 b2 (PTree.set r1 b1 e.(te_typ));
+                           te_sub := (r1, r2) :: e.(te_sub) |})
+      | right _ =>
+          Error(MSG "ill-typed move from " :: POS r1 :: MSG " to " :: POS r2 :: nil)
+      end
+  end.
+
+(** Solve the remaining subtyping constraints by iteration. *)
+
+Fixpoint solve_rec (e: typenv) (changed: bool) (q: list constraint) : 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.
+
+(** Measuring the state *)
+
+Definition weight_bounds (ob: option bounds) : nat :=
+  match ob with None => T.max_weight + 1 | Some(B lo hi s) => T.weight hi - T.weight lo end.
+
+Lemma weight_bounds_1:
+  forall lo hi s, weight_bounds (Some (B lo hi s)) < weight_bounds None.
+Proof.
+  intros; simpl. generalize (T.weight_range hi); omega. 
+Qed.
+
+Lemma weight_bounds_2:
+  forall lo1 hi1 s1 lo2 hi2 s2,
+  T.sub lo2 lo1 -> T.sub hi1 hi2 -> lo1 <> lo2 \/ hi1 <> hi2 ->
+  weight_bounds (Some (B lo1 hi1 s1)) < weight_bounds (Some (B lo2 hi2 s2)).
+Proof.
+  intros; simpl. 
+  generalize (T.weight_sub _ _ s1) (T.weight_sub _ _ s2) (T.weight_sub _ _ H) (T.weight_sub _ _ H0); intros.
+  destruct H1.
+  assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). omega.
+  assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). omega.
+Qed.
+
+Hint Resolve T.sub_refl: ty.
+
+Lemma weight_type_move:
+  forall e r1 r2 changed e',
+  type_move e r1 r2 = OK(changed, e') ->
+  (e'.(te_sub) = e.(te_sub) \/ e'.(te_sub) = (r1, r2) :: e.(te_sub))
+  /\ (forall r, weight_bounds e'.(te_typ)!r <= weight_bounds e.(te_typ)!r)
+  /\ (changed = true ->
+        weight_bounds e'.(te_typ)!r1 + weight_bounds e'.(te_typ)!r2 
+        < weight_bounds e.(te_typ)!r1 + weight_bounds e.(te_typ)!r2).
+Proof.
+  unfold type_move; intros.
+  destruct (peq r1 r2).
+  inv H. split; auto. split; intros. omega. discriminate.
+  destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
+  destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
+- destruct (T.sub_dec hi1 lo2).
+  inv H. split; auto. split; intros. omega. discriminate.
+  destruct (T.sub_dec lo1 hi2); try discriminate.
+  set (lo2' := T.lub lo1 lo2) in *.
+  set (hi1' := T.glb hi1 hi2) in *.
+  assert (S1': T.sub hi1' hi1) by (eapply T.glb_left; eauto).
+  assert (S2': T.sub lo2 lo2') by (eapply T.lub_right; eauto).
+  set (b1 := B lo1 hi1' (T.glb_max hi1 hi2 lo1 s1 s)) in *.
+  set (b2 := B lo2' hi2 (T.lub_min lo1 lo2 hi2 s s2)) in *.
+Local Opaque weight_bounds.
+  destruct (T.eq lo2 lo2'); destruct (T.eq hi1 hi1'); inversion H; clear H; subst changed e'; simpl.
++ split; auto. split; intros. omega. discriminate.
++ assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1)))
+  by (apply weight_bounds_2; auto with ty).
+  split; auto. split; intros. 
+  rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. omega. omega.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. 
++ assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2)))
+  by (apply weight_bounds_2; auto with ty).
+  split; auto. split; intros. 
+  rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. omega.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega.
++ assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1)))
+  by (apply weight_bounds_2; auto with ty).
+  assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2)))
+  by (apply weight_bounds_2; auto with ty).
+  split; auto. split; intros. 
+  rewrite ! PTree.gsspec.
+  destruct (peq r r2). subst r. rewrite E2. omega.
+  destruct (peq r r1). subst r. rewrite E1. omega. 
+  omega.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. omega.
+
+- set (b2 := B lo1 (T.high_bound lo1) (T.high_bound_sub lo1)) in *.
+  assert (weight_bounds (Some b2) < weight_bounds None) by (apply weight_bounds_1).
+  inv H; simpl.
+  split. destruct (T.sub_dec hi1 lo1); auto.
+  split; intros. 
+  rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; omega. omega.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. 
+
+- set (b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2)) in *.
+  assert (weight_bounds (Some b1) < weight_bounds None) by (apply weight_bounds_1).
+  inv H; simpl.
+  split. destruct (T.sub_dec hi2 lo2); auto.
+  split; intros. 
+  rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; omega. omega.
+  rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega.
+
+- inv H. split; auto. simpl; split; intros. omega. congruence.
+Qed.
+
+Definition weight_constraints (b: PTree.t bounds) (cstr: list constraint) : nat :=
+  List.fold_right (fun xy n => n + weight_bounds b!(fst xy) + weight_bounds b!(snd xy)) 0 cstr.
+
+Remark weight_constraints_tighter:
+  forall b1 b2, (forall r, weight_bounds b1!r <= weight_bounds b2!r) ->
+  forall q, weight_constraints b1 q <= weight_constraints b2 q.
+Proof.
+  induction q; simpl. omega. generalize (H (fst a)) (H (snd a)); omega.
+Qed.
+
+Lemma weight_solve_rec:
+  forall q e changed e' changed',
+  solve_rec e changed q = OK(e', changed') ->
+  (forall r, weight_bounds e'.(te_typ)!r <= weight_bounds e.(te_typ)!r) /\
+  weight_constraints e'.(te_typ) e'.(te_sub) + (if changed' && negb changed then 1 else 0)
+     <= weight_constraints e.(te_typ) e.(te_sub) + weight_constraints e.(te_typ) q.
+Proof.
+  induction q; simpl; intros.
+- inv H. split. intros; omega. replace (changed' && negb changed') with false. 
+  omega. destruct changed'; auto.
+- destruct a as [r1 r2]; monadInv H; simpl.
+  rename x into changed1. rename x0 into e1.
+  exploit weight_type_move; eauto. intros [A [B C]].
+  exploit IHq; eauto. intros [D E].
+  split. intros. eapply le_trans. eapply D. eapply B.
+  assert (P: weight_constraints (te_typ e1) (te_sub e) <=
+             weight_constraints (te_typ e) (te_sub e))
+  by (apply weight_constraints_tighter; auto).
+  assert (Q: weight_constraints (te_typ e1) (te_sub e1) <=
+             weight_constraints (te_typ e1) (te_sub e) + 
+             weight_bounds (te_typ e1)!r1 + weight_bounds (te_typ e1)!r2).
+  { destruct A as [Q|Q]; rewrite Q. omega. simpl. omega. }
+  assert (R: weight_constraints (te_typ e1) q <= weight_constraints (te_typ e) q)
+  by (apply weight_constraints_tighter; auto).
+  set (ch1 := if changed' && negb (changed || changed1) then 1 else 0) in *.
+  set (ch2 := if changed' && negb changed then 1 else 0) in *.
+  destruct changed1.
+  assert (ch2 <= ch1 + 1). 
+  { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r. 
+    destruct (changed' && negb changed); omega. }
+  exploit C; eauto. omega.
+  assert (ch2 <= ch1).
+  { unfold ch2, ch1. rewrite orb_false_r. omega. }
+  generalize (B r1) (B r2); omega.  
+Qed.
+
+Definition weight_typenv (e: typenv) : nat := 
+  weight_constraints e.(te_typ) e.(te_sub).
+
+(** Iterative solving of the remaining constraints *)
+
+Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv :=
+  match solve_rec {| te_typ := e.(te_typ); te_sub := nil |} false e.(te_sub) with
+  | OK(e', false) => OK e                   (**r no more changes, fixpoint reached *)
+  | OK(e', true)  => solve_constraints e'   (**r one more iteration *)
+  | Error msg => Error msg
+  end.
+Proof.
+  intros. exploit weight_solve_rec; eauto. simpl. intros [A B].
+  unfold weight_typenv. omega. 
+Qed.
+
+Definition typassign := positive -> T.t.
+
+Definition makeassign (e: typenv) : typassign :=
+  fun x => match e.(te_typ)!x with Some(B lo hi s) => lo | None => T.default end.
+
+Definition solve (e: typenv) : res typassign :=
+  do e' <- solve_constraints e; OK(makeassign e').
+
+(** What it means to be a solution *)
+
+Definition satisf (te: typassign) (e: typenv) : Prop :=
+   (forall x lo hi s, e.(te_typ)!x = Some(B lo hi s) -> T.sub lo (te x) /\ T.sub (te x) hi)
+/\ (forall x y, In (x, y) e.(te_sub) -> T.sub (te x) (te y)).
+
+Lemma satisf_initial: forall te, satisf te initial.
+Proof.
+  unfold initial; intros; split; simpl; intros. 
+  rewrite PTree.gempty in H; discriminate.
+  contradiction.
+Qed.
+
+(** Soundness proof *)
+
+Lemma type_def_incr:
+  forall te x ty e e', type_def e x ty = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  unfold type_def; intros. destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
+- destruct (T.sub_dec ty hi); try discriminate.
+  destruct (T.eq lo (T.lub lo ty)); monadInv H.
+  subst e'; auto.
+  destruct H0 as [P Q]; split; auto; intros.
+  destruct (peq x x0). 
+  + subst x0. rewrite E in H; inv H.
+    exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. 
+    apply T.sub_trans with (T.lub lo0 ty); auto. eapply T.lub_left; eauto. 
+  + eapply P; simpl. rewrite PTree.gso; eauto. 
+- inv H. destruct H0 as [P Q]; split; auto; intros.
+  eapply P; simpl. rewrite PTree.gso; eauto. congruence.
+Qed.
+
+Hint Resolve type_def_incr: ty.
+
+Lemma type_def_sound:
+  forall te x ty e e', type_def e x ty = OK e' -> satisf te e' -> T.sub ty (te x).
+Proof.
+  unfold type_def; intros. destruct H0 as [P Q].
+  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
+- destruct (T.sub_dec ty hi); try discriminate.
+  destruct (T.eq lo (T.lub lo ty)); monadInv H.
+  + subst e'. apply T.sub_trans with lo. 
+    rewrite e0. eapply T.lub_right; eauto. eapply P; eauto.
+  + apply T.sub_trans with (T.lub lo ty). 
+    eapply T.lub_right; eauto. 
+    eapply (P x). simpl. rewrite PTree.gss; eauto. 
+- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. 
+Qed.
+
+Lemma type_defs_incr:
+  forall te xl tyl e e', type_defs e xl tyl = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty.
+Qed.
+
+Hint Resolve type_defs_incr: ty.
+
+Lemma type_defs_sound:
+  forall te xl tyl e e', type_defs e xl tyl = OK e' -> satisf te e' -> list_forall2 T.sub tyl (map te xl).
+Proof.
+  induction xl; destruct tyl; simpl; intros; monadInv H.
+  constructor.
+  constructor; eauto. eapply type_def_sound; eauto with ty.
+Qed.
+
+Lemma type_use_incr:
+  forall te x ty e e', type_use e x ty = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  unfold type_use; intros. destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
+- destruct (T.sub_dec lo ty); try discriminate.
+  destruct (T.eq hi (T.glb hi ty)); monadInv H.
+  subst e'; auto.
+  destruct H0 as [P Q]; split; auto; intros.
+  destruct (peq x x0). 
+  + subst x0. rewrite E in H; inv H.
+    exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. 
+    apply T.sub_trans with (T.glb hi0 ty); auto. eapply T.glb_left; eauto. 
+  + eapply P; simpl. rewrite PTree.gso; eauto. 
+- inv H. destruct H0 as [P Q]; split; auto; intros.
+  eapply P; simpl. rewrite PTree.gso; eauto. congruence.
+Qed.
+
+Hint Resolve type_use_incr: ty.
+
+Lemma type_use_sound:
+  forall te x ty e e', type_use e x ty = OK e' -> satisf te e' -> T.sub (te x) ty.
+Proof.
+  unfold type_use; intros. destruct H0 as [P Q].
+  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E.
+- destruct (T.sub_dec lo ty); try discriminate.
+  destruct (T.eq hi (T.glb hi ty)); monadInv H.
+  + subst e'. apply T.sub_trans with hi. 
+    eapply P; eauto. rewrite e0. eapply T.glb_right; eauto. 
+  + apply T.sub_trans with (T.glb hi ty). 
+    eapply (P x). simpl. rewrite PTree.gss; eauto. 
+    eapply T.glb_right; eauto. 
+- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. 
+Qed.
+
+Lemma type_uses_incr:
+  forall te xl tyl e e', type_uses e xl tyl = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty.
+Qed.
+
+Hint Resolve type_uses_incr: ty.
+
+Lemma type_uses_sound:
+  forall te xl tyl e e', type_uses e xl tyl = OK e' -> satisf te e' -> list_forall2 T.sub (map te xl) tyl.
+Proof.
+  induction xl; destruct tyl; simpl; intros; monadInv H.
+  constructor.
+  constructor; eauto. eapply type_use_sound; eauto with ty.
+Qed.
+
+Lemma type_move_incr:
+  forall te e r1 r2 e' changed,
+  type_move e r1 r2 = OK(changed, e') -> satisf te e' -> satisf te e.
+Proof.
+  unfold type_move; intros. destruct H0 as [P Q].
+  destruct (peq r1 r2). inv H; split; auto.
+  destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
+  destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
+- destruct (T.sub_dec hi1 lo2). inv H; split; auto.
+  destruct (T.sub_dec lo1 hi2); try discriminate.
+  set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *.
+  destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *.
+  + subst e'; simpl in *. split; auto. 
+  + subst e'; simpl in *. split; auto. intros. destruct (peq x r1).
+    subst x. 
+    rewrite E1 in H. injection H; intros; subst lo0 hi0. 
+    exploit (P r1). rewrite PTree.gss; eauto. intuition. 
+    apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto.
+    eapply P. rewrite PTree.gso; eauto.
+  + subst e'; simpl in *. split; auto. intros. destruct (peq x r2).
+    subst x. 
+    rewrite E2 in H. injection H; intros; subst lo0 hi0. 
+    exploit (P r2). rewrite PTree.gss; eauto. intuition. 
+    apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto.
+    eapply P. rewrite PTree.gso; eauto.
+  + split; auto. intros. 
+    destruct (peq x r1). subst x. 
+    rewrite E1 in H. injection H; intros; subst lo0 hi0. 
+    exploit (P r1). rewrite PTree.gso; eauto. rewrite PTree.gss; eauto. intuition. 
+    apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto.
+    destruct (peq x r2). subst x. 
+    rewrite E2 in H. injection H; intros; subst lo0 hi0. 
+    exploit (P r2). rewrite PTree.gss; eauto. intuition. 
+    apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto.
+    eapply P. rewrite ! PTree.gso; eauto.
+- inv H; simpl in *. split; intros.
+  eapply P. rewrite PTree.gso; eauto. congruence.
+  apply Q.   destruct (T.sub_dec hi1 lo1); auto with coqlib.
+- inv H; simpl in *. split; intros.
+  eapply P. rewrite PTree.gso; eauto. congruence.
+  apply Q.   destruct (T.sub_dec hi2 lo2); auto with coqlib.
+- inv H; simpl in *. split; auto. 
+Qed.
+
+Hint Resolve type_move_incr: ty.
+
+Lemma type_move_sound:
+  forall te e r1 r2 e' changed,
+  type_move e r1 r2 = OK(changed, e') -> satisf te e' -> T.sub (te r1) (te r2).
+Proof.
+  unfold type_move; intros. destruct H0 as [P Q].
+  destruct (peq r1 r2). subst r2. apply T.sub_refl.
+  destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
+  destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
+- destruct (T.sub_dec hi1 lo2). 
+  inv H. apply T.sub_trans with hi1. eapply P; eauto. apply T.sub_trans with lo2; auto. eapply P; eauto.
+  destruct (T.sub_dec lo1 hi2); try discriminate.
+  set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *.
+  destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *.
+  + subst e'; simpl in *. apply Q; auto.
+  + subst e'; simpl in *. apply Q; auto. 
+  + subst e'; simpl in *. apply Q; auto. 
+  + apply Q; auto.
+- inv H; simpl in *. destruct (T.sub_dec hi1 lo1).
+  + apply T.sub_trans with hi1. eapply P; eauto. rewrite PTree.gso; eauto. 
+    apply T.sub_trans with lo1; auto. eapply P. rewrite PTree.gss; eauto. 
+  + auto with coqlib.
+- inv H; simpl in *. destruct (T.sub_dec hi2 lo2).
+  + apply T.sub_trans with hi2. eapply P. rewrite PTree.gss; eauto. 
+    apply T.sub_trans with lo2; auto. eapply P. rewrite PTree.gso; eauto. 
+  + auto with coqlib.
+- inv H. simpl in Q; auto. 
+Qed.
+
+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.
+
+Lemma solve_rec_sound:
+  forall te r1 r2 q e changed e' changed',
+  solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' -> 
+  T.sub (te r1) (te r2).
+Proof.
+  induction q; simpl; intros.
+- contradiction.
+- destruct a as [r3 r4]; monadInv H. destruct H0. 
+  + inv H. eapply type_move_sound; eauto. eapply solve_rec_incr; eauto.
+  + eapply IHq; eauto with ty.
+Qed.
+
+Lemma type_move_false:
+  forall e r1 r2 e',
+  type_move e r1 r2 = OK(false, e') ->
+  te_typ e' = te_typ e /\ T.sub (makeassign e r1) (makeassign e r2).
+Proof.
+  unfold type_move; intros. 
+  destruct (peq r1 r2). inv H. split; auto. apply T.sub_refl.
+  unfold makeassign;
+  destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
+  destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
+- destruct (T.sub_dec hi1 lo2). 
+  inv H. split; auto. eapply T.sub_trans; eauto.
+  destruct (T.sub_dec lo1 hi2); try discriminate.
+  set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *.
+  destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); try discriminate.
+  monadInv H. split; auto. rewrite e0. unfold lo. eapply T.lub_left; eauto.
+- discriminate.
+- discriminate.
+- inv H. split; auto. apply T.sub_refl.
+Qed.
+
+Lemma solve_rec_false:
+  forall r1 r2 q e changed e',
+  solve_rec e changed q = OK(e', false) ->
+  changed = false /\ 
+  (In (r1, r2) q -> T.sub (makeassign e r1) (makeassign e r2)).
+Proof.
+  induction q; simpl; intros.
+- inv H. tauto. 
+- destruct a as [r3 r4]; monadInv H.
+  exploit IHq; eauto. intros [P Q].
+  destruct changed; try discriminate. destruct x; try discriminate.
+  exploit type_move_false; eauto. intros [U V].
+  split. auto. intros [A|A]. inv A. auto. exploit Q; auto. 
+  unfold makeassign; rewrite U; auto.    
+Qed.
+
+Lemma solve_constraints_incr:
+  forall te e e', solve_constraints e = OK e' -> satisf te e' -> satisf te e.
+Proof.
+  intros te e; functional induction (solve_constraints e); intros.
+- inv H. auto.
+- exploit solve_rec_incr; eauto. intros [A B].
+  split; auto. intros; eapply solve_rec_sound; eauto.
+- discriminate.
+Qed.
+
+Lemma solve_constraints_sound:
+  forall e e', solve_constraints e = OK e' -> satisf (makeassign e') e'.
+Proof.
+  intros e0; functional induction (solve_constraints e0); intros.
+- inv H. split; intros.
+  unfold makeassign; rewrite H. split; auto with ty.
+  exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto. 
+- eauto.
+- discriminate.
+Qed.
+
+Theorem solve_sound:
+  forall e te, solve e = OK te -> satisf te e.
+Proof.
+  unfold solve; intros. monadInv H. 
+  eapply solve_constraints_incr. eauto. eapply solve_constraints_sound; eauto.
+Qed.
+
+(** Completeness proof *)
+
+Lemma type_def_complete:
+  forall te e x ty,
+  satisf te e -> T.sub ty (te x) -> exists e', type_def e x ty = OK e' /\ satisf te e'.
+Proof.
+  unfold type_def; intros. destruct H as [P Q].
+  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. 
+- destruct (T.sub_dec ty hi). 
+  destruct (T.eq lo (T.lub lo ty)).
+  exists e; split; auto. split; auto.
+  econstructor; split; eauto. split; simpl; auto; intros. 
+  rewrite PTree.gsspec in H. destruct (peq x0 x). 
+  inv H. exploit P; eauto. intuition. eapply T.lub_min; eauto. 
+  eapply P; eauto.
+  elim n. apply T.sub_trans with (te x); auto. eapply P; eauto.
+- econstructor; split; eauto. split; simpl; auto; intros.
+  rewrite PTree.gsspec in H. destruct (peq x0 x). 
+  inv H. split; auto. apply T.high_bound_majorant; auto.
+  eapply P; eauto.
+Qed.
+
+Lemma type_defs_complete:
+  forall te xl tyl e,
+  satisf te e -> list_forall2 T.sub tyl (map te xl) ->
+  exists e', type_defs e xl tyl = OK e' /\ satisf te e'.
+Proof.
+  induction xl; intros; inv H0; simpl.
+  econstructor; eauto.
+  exploit (type_def_complete te e a a1); auto. intros (e1 & P & Q).
+  exploit (IHxl al e1); auto. intros (e2 & U & V).
+  exists e2; split; auto. rewrite P; auto.
+Qed.
+
+Lemma type_use_complete:
+  forall te e x ty,
+  satisf te e -> T.sub (te x) ty -> exists e', type_use e x ty = OK e' /\ satisf te e'.
+Proof.
+  unfold type_use; intros. destruct H as [P Q].
+  destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. 
+- destruct (T.sub_dec lo ty). 
+  destruct (T.eq hi (T.glb hi ty)).
+  exists e; split; auto. split; auto.
+  econstructor; split; eauto. split; simpl; auto; intros. 
+  rewrite PTree.gsspec in H. destruct (peq x0 x). 
+  inv H. exploit P; eauto. intuition. eapply T.glb_max; eauto. 
+  eapply P; eauto.
+  elim n. apply T.sub_trans with (te x); auto. eapply P; eauto.
+- econstructor; split; eauto. split; simpl; auto; intros.
+  rewrite PTree.gsspec in H. destruct (peq x0 x). 
+  inv H. split; auto. apply T.low_bound_minorant; auto.
+  eapply P; eauto.
+Qed.
+
+Lemma type_uses_complete:
+  forall te xl tyl e,
+  satisf te e -> list_forall2 T.sub (map te xl) tyl ->
+  exists e', type_uses e xl tyl = OK e' /\ satisf te e'.
+Proof.
+  induction xl; intros; inv H0; simpl.
+  econstructor; eauto.
+  exploit (type_use_complete te e a b1); auto. intros (e1 & P & Q).
+  exploit (IHxl bl e1); auto. intros (e2 & U & V).
+  exists e2; split; auto. rewrite P; auto.
+Qed.
+
+Lemma type_move_complete:
+  forall te e r1 r2,
+  satisf te e -> T.sub (te r1) (te r2) ->
+  exists changed e', type_move e r1 r2 = OK(changed, e') /\ satisf te e'.
+Proof.
+  unfold type_move; intros. elim H; intros P Q.
+  assert (Q': forall x y, In (x, y) ((r1, r2) :: te_sub e) -> T.sub (te x) (te y)).
+  { intros. destruct H1; auto. congruence. }
+  destruct (peq r1 r2). econstructor; econstructor; eauto.
+  destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1;
+  destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2.
+- exploit (P r1); eauto. intros [L1 U1].
+  exploit (P r2); eauto. intros [L2 U2].
+  destruct (T.sub_dec hi1 lo2). econstructor; econstructor; eauto.
+  destruct (T.sub_dec lo1 hi2). 
+  destruct (T.eq lo2 (T.lub lo1 lo2)); destruct (T.eq hi1 (T.glb hi1 hi2));
+  econstructor; econstructor; split; eauto; split; auto; simpl; intros.
+  + rewrite PTree.gsspec in H1. destruct (peq x r1). 
+    clear e0. inv H1. split; auto.  
+    apply T.glb_max. auto. apply T.sub_trans with (te r2); auto.
+    eapply P; eauto.
+  + rewrite PTree.gsspec in H1. destruct (peq x r2). 
+    clear e0. inv H1. split; auto.  
+    apply T.lub_min. apply T.sub_trans with (te r1); auto. auto.
+    eapply P; eauto.
+  + rewrite ! PTree.gsspec in H1. destruct (peq x r2).
+    inv H1. split; auto. apply T.lub_min; auto. apply T.sub_trans with (te r1); auto.
+    destruct (peq x r1).
+    inv H1. split; auto. apply T.glb_max; auto. apply T.sub_trans with (te r2); auto.
+    eapply P; eauto.
+  + elim n1. apply T.sub_trans with (te r1); auto. 
+    apply T.sub_trans with (te r2); auto. 
+- econstructor; econstructor; split; eauto; split.
+  + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r2).
+    inv H1. exploit P; eauto. intuition. 
+    apply T.sub_trans with (te r1); auto.
+    apply T.high_bound_majorant. apply T.sub_trans with (te r1); auto.
+    eapply P; eauto.
+  + destruct (T.sub_dec hi1 lo1); auto.
+- econstructor; econstructor; split; eauto; split.
+  + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r1).
+    inv H1. exploit P; eauto. intuition. 
+    apply T.low_bound_minorant. apply T.sub_trans with (te r2); auto.
+    apply T.sub_trans with (te r2); auto.
+    eapply P; eauto.
+  + destruct (T.sub_dec hi2 lo2); auto.
+- econstructor; econstructor; split; eauto; split; auto.
+Qed.
+
+Lemma solve_rec_complete:
+  forall te q e changed,
+  satisf te e ->
+  (forall r1 r2, In (r1, r2) q -> T.sub (te r1) (te r2)) ->
+  exists e' changed', solve_rec e changed q = OK(e', changed') /\ satisf te e'.
+Proof.
+  induction q; simpl; intros.
+- econstructor; econstructor; eauto.
+- destruct a as [r1 r2]. 
+  exploit (type_move_complete te e r1 r2); auto. intros (changed1 & e1 & A & B).
+  exploit (IHq e1 (changed || changed1)); auto. intros (e' & changed' & C & D).
+  exists e'; exists changed'. rewrite A; simpl; rewrite C; auto.
+Qed.
+
+Lemma solve_constraints_complete:
+  forall te e, satisf te e -> exists e', solve_constraints e = OK e' /\ satisf te e'.
+Proof.
+  intros te e. functional induction (solve_constraints e); intros. 
+- exists e; auto.
+- exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false).
+  destruct H; split; auto. simpl; tauto.
+  destruct H; auto.
+  intros (e1 & changed1 & P & Q). 
+  apply IHr. congruence. 
+- exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false).
+  destruct H; split; auto. simpl; tauto.
+  destruct H; auto.
+  intros (e1 & changed1 & P & Q). 
+  congruence.
+Qed.
+
+Lemma solve_complete:
+  forall te e, satisf te e -> exists te', solve e = OK te'.
+Proof.
+  intros. unfold solve. 
+  destruct (solve_constraints_complete te e H) as (e' & P & Q). 
+  econstructor. rewrite P. simpl. eauto. 
+Qed.
+
+End SubSolver.
+
diff --git a/common/Values.v b/common/Values.v
index 76fb230..bb97cdc 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -61,6 +61,7 @@ Definition has_type (v: val) (t: typ) : Prop :=
   | Vint _, Tint => True
   | Vlong _, Tlong => True
   | Vfloat _, Tfloat => True
+  | Vfloat f, Tsingle => Float.is_single f
   | Vptr _ _, Tint => True
   | _, _ => False
   end.
@@ -78,6 +79,23 @@ Definition has_opttype (v: val) (ot: option typ) : Prop :=
   | Some t => has_type v t
   end.
 
+Lemma has_subtype:
+  forall ty1 ty2 v,
+  subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2.
+Proof.
+  intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac.
+  unfold has_type in *. destruct v; auto. 
+Qed.
+
+Lemma has_subtype_list:
+  forall tyl1 tyl2 vl,
+  subtype_list tyl1 tyl2 = true -> has_type_list vl tyl1 -> has_type_list vl tyl2.
+Proof.
+  induction tyl1; intros; destruct tyl2; try discriminate; destruct vl; try contradiction.
+  red; auto.
+  simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto.
+Qed.
+
 (** Truth values.  Pointers and non-zero integers are treated as [True].
   The integer 0 (also used to represent the null pointer) is [False].
   [Vundef] and floats are neither true nor false. *)
@@ -603,14 +621,14 @@ Definition cmplu (c: comparison) (v1 v2: val): option val :=
 
 End COMPARISONS.
 
-(** [load_result] is used in the memory model (library [Mem])
-  to post-process the results of a memory read.  For instance,
-  consider storing the integer value [0xFFF] on 1 byte at a
-  given address, and reading it back.  If it is read back with
+(** [load_result] reflects the effect of storing a value with a given
+  memory chunk, then reading it back with the same chunk.  Depending
+  on the chunk and the type of the value, some normalization occurs.
+  For instance, consider storing the integer value [0xFFF] on 1 byte
+  at a given address, and reading it back.  If it is read back with
   chunk [Mint8unsigned], zero-extension must be performed, resulting
-  in [0xFF].  If it is read back as a [Mint8signed], sign-extension
-  is performed and [0xFFFFFFFF] is returned.   Type mismatches
-  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
+  in [0xFF].  If it is read back as a [Mint8signed], sign-extension is
+  performed and [0xFFFFFFFF] is returned. *)
 
 Definition load_result (chunk: memory_chunk) (v: val) :=
   match chunk, v with
@@ -626,6 +644,19 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
   | _, _ => Vundef
   end.
 
+Lemma load_result_type:
+  forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk).
+Proof.
+  intros. destruct chunk; destruct v; simpl; auto. apply Float.singleoffloat_is_single.
+Qed.
+
+Lemma load_result_same:
+  forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v.
+Proof.
+  unfold has_type; intros. destruct v; destruct ty; try contradiction; auto.
+  simpl. rewrite Float.singleoffloat_of_single; auto. 
+Qed.
+
 (** Theorems on arithmetic operations. *)
 
 Theorem cast8unsigned_and: