Various algorithmic improvements that reduce compile times (thanks Alexandre Pilkiewicz):

- Lattice: preserve sharing in "combine" operation
- Kildall: use splay heaps (lib/Heaps.v) for node sets
- RTLgen: add a "nop" before loops so that natural enumeration of nodes
  coincides with (reverse) postorder
- Maps: add PTree.map1 operation, use it in RTL and LTL.
- Driver: increase minor heap size


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

19 files changed, 965 insertions, 141 deletions

diff --git a/.depend b/.depend
index 24ba8a7..ccafd5a 100644
--- a/.depend
+++ b/.depend
@@ -2,6 +2,7 @@ lib/Axioms.vo: lib/Axioms.v
 lib/Coqlib.vo: lib/Coqlib.v
 lib/Intv.vo: lib/Intv.v lib/Coqlib.vo
 lib/Maps.vo: lib/Maps.v lib/Coqlib.vo
+lib/Heaps.vo: lib/Heaps.v lib/Coqlib.vo lib/Ordered.vo
 lib/Lattice.vo: lib/Lattice.v lib/Coqlib.vo lib/Maps.vo
 lib/Ordered.vo: lib/Ordered.v lib/Coqlib.vo lib/Maps.vo lib/Integers.vo
 lib/Iteration.vo: lib/Iteration.v lib/Axioms.vo lib/Coqlib.vo
@@ -35,7 +36,7 @@ backend/RTLgenproof.vo: backend/RTLgenproof.v lib/Coqlib.vo lib/Maps.vo common/A
 backend/Tailcall.vo: backend/Tailcall.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Globalenvs.vo backend/Registers.vo $(ARCH)/Op.vo backend/RTL.vo backend/Conventions.vo
 backend/Tailcallproof.vo: backend/Tailcallproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo $(ARCH)/Op.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Registers.vo backend/RTL.vo backend/Conventions.vo backend/Tailcall.vo
 backend/RTLtyping.vo: backend/RTLtyping.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo $(ARCH)/Op.vo backend/Registers.vo common/Globalenvs.vo common/Values.vo common/Memory.vo lib/Integers.vo common/Events.vo common/Smallstep.vo backend/RTL.vo backend/Conventions.vo
-backend/Kildall.vo: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Ordered.vo
+backend/Kildall.vo: backend/Kildall.v lib/Coqlib.vo lib/Iteration.vo lib/Maps.vo lib/Lattice.vo lib/Heaps.vo
 backend/CastOptim.vo: backend/CastOptim.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo
 backend/CastOptimproof.vo: backend/CastOptimproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Events.vo common/Memory.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Registers.vo backend/RTL.vo lib/Lattice.vo backend/Kildall.vo backend/CastOptim.vo
 $(ARCH)/ConstpropOp.vo: $(ARCH)/ConstpropOp.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo $(ARCH)/Op.vo backend/Registers.vo
@@ -82,9 +83,9 @@ backend/Machconcr.vo: backend/Machconcr.v lib/Coqlib.vo lib/Maps.vo common/AST.v
 backend/Machabstr2concr.vo: backend/Machabstr2concr.v lib/Axioms.vo lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machtyping.vo backend/Machabstr.vo backend/Machconcr.vo backend/Conventions.vo $(ARCH)/Asmgenretaddr.vo
 $(ARCH)/Asm.vo: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo
 $(ARCH)/Asmgen.vo: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo
-$(ARCH)/Asmgenretaddr.vo: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo
-$(ARCH)/Asmgenproof1.vo: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
-$(ARCH)/Asmgenproof.vo: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo
+$(ARCH)/Asmgenretaddr.vo: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo
+$(ARCH)/Asmgenproof1.vo: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo
+$(ARCH)/Asmgenproof.vo: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machconcr.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo
 cfrontend/Csyntax.vo: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo
 cfrontend/Csem.vo: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo
 cfrontend/Cstrategy.vo: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo common/Determinism.vo cfrontend/Csyntax.vo cfrontend/Csem.vo
diff --git a/Makefile b/Makefile
index 752a8e6..6fea519 100644
--- a/Makefile
+++ b/Makefile
@@ -33,7 +33,7 @@ GPATH=$(DIRS)
 
 # General-purpose libraries (in lib/)
 
-LIB=Axioms.v Coqlib.v Intv.v Maps.v Lattice.v Ordered.v \
+LIB=Axioms.v Coqlib.v Intv.v Maps.v Heaps.v Lattice.v Ordered.v \
   Iteration.v Integers.v Floats.v Parmov.v UnionFind.v
 
 # Parts common to the front-ends and the back-end (in common/)
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 5a5e4c4..daa53e5 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -165,7 +165,7 @@ Proof.
   apply agree_increasing with (live!!n).
   eapply DS.fixpoint_solution. unfold analyze in H; eauto.
   unfold RTL.successors, Kildall.successors_list. 
-  rewrite PTree.gmap. rewrite H0. simpl. auto.
+  rewrite PTree.gmap1. rewrite H0. simpl. auto.
   auto.
 Qed.
 
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index c5670e8..275b9fd 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -695,7 +695,7 @@ Proof.
   intros res FIXPOINT WF AT SUCC.
   assert (Numbering.ge res!!pc' (transfer f pc res!!pc)).
     eapply Solver.fixpoint_solution; eauto.
-    unfold successors_list, successors. rewrite PTree.gmap.
+    unfold successors_list, successors. rewrite PTree.gmap1.
     rewrite AT. auto.
   apply H.
   intros. rewrite PMap.gi. apply empty_numbering_satisfiable.
diff --git a/backend/CastOptim.v b/backend/CastOptim.v
index 545564d..19d0065 100644
--- a/backend/CastOptim.v
+++ b/backend/CastOptim.v
@@ -136,12 +136,12 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     | Single, Single => Single
     | _, _ => Unknown
     end.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
+  Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
-    unfold lub, eq; intros.
-    destruct x; destruct y; auto.
+    unfold lub, ge; intros.
+    destruct x; destruct y; auto. 
   Qed.
-  Lemma ge_lub_left: forall x y, ge (lub x y) x.
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
   Proof.
     unfold lub, ge; intros.
     destruct x; destruct y; auto. 
diff --git a/backend/CastOptimproof.v b/backend/CastOptimproof.v
index d507609..b04e061 100644
--- a/backend/CastOptimproof.v
+++ b/backend/CastOptimproof.v
@@ -118,7 +118,7 @@ Proof.
   intros approxs; intros.
   apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
-  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
+  unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto.
   auto.
   intros. rewrite PMap.gi. apply regs_match_approx_top. 
 Qed.
diff --git a/backend/Constprop.v b/backend/Constprop.v
index 03966cd..47c40e3 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -87,12 +87,6 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     | _, Novalue => x
     | _, _ => Unknown
     end.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
-  Proof.
-    unfold lub, eq; intros.
-    case (eq_dec x y); case (eq_dec y x); intros; try congruence.
-    destruct x; destruct y; auto.
-  Qed.
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
     unfold lub; intros.
@@ -100,6 +94,13 @@ Module Approx <: SEMILATTICE_WITH_TOP.
     apply ge_refl. apply eq_refl.
     destruct x; destruct y; unfold ge; tauto.
   Qed.
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
+  Proof.
+    unfold lub; intros.
+    case (eq_dec x y); intro.
+    apply ge_refl. subst. apply eq_refl.
+    destruct x; destruct y; unfold ge; tauto.
+  Qed.
 End Approx.
 
 Module D := LPMap Approx.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 714468a..1dad518 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -106,7 +106,7 @@ Proof.
   intros approxs; intros.
   apply regs_match_approx_increasing with (transfer f pc approxs!!pc).
   eapply DS.fixpoint_solution; eauto.
-  unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto.
+  unfold successors_list, successors. rewrite PTree.gmap1. rewrite H0. auto.
   auto.
   intros. rewrite PMap.gi. apply regs_match_approx_top. 
 Qed.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index 83206f7..e1e6ea5 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -344,14 +344,12 @@ Proof.
            ((st_in st) !! n) (L.lub (st_in st) !! n out).
   split.
   eapply L.ge_trans. apply L.ge_refl. apply H; auto.
-  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
-  apply L.ge_lub_left. 
+  apply L.ge_lub_right. 
   auto.
 
   simpl. split.
   rewrite PMap.gss.
-  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
-  apply L.ge_lub_left. 
+  apply L.ge_lub_right.
   intros. rewrite PMap.gso; auto.
 Qed.
 
@@ -506,8 +504,7 @@ Proof.
   elim H.
   elim H; intros.
   subst a. rewrite PMap.gss.
-  eapply L.ge_compat. apply L.lub_commut. apply L.eq_refl. 
-  apply L.ge_lub_left.
+  apply L.ge_lub_right.
   destruct a. rewrite PMap.gsspec. case (peq n p); intro.
   subst p. apply L.ge_trans with (start_state_in ep)!!n.
   apply L.ge_lub_left. auto.
@@ -1168,49 +1165,41 @@ End BBlock_solver.
   greatest node in the working list.  For backward analysis,
   we will similarly pick the smallest node in the working list. *)
 
-Require Import FSets.
-Require Import FSetAVL.
-Require Import Ordered.
-
-Module PositiveSet := FSetAVL.Make(OrderedPositive).
-Module PositiveSetFacts := FSetFacts.Facts(PositiveSet).
+Require Import Heaps.
 
 Module NodeSetForward <: NODE_SET.
-  Definition t := PositiveSet.t.
-  Definition add (n: positive) (s: t) : t := PositiveSet.add n s.
+  Definition t := PHeap.t.
+  Definition add (n: positive) (s: t) : t := PHeap.insert n s.
   Definition pick (s: t) :=
-    match PositiveSet.max_elt s with
-    | Some n => Some(n, PositiveSet.remove n s)
+    match PHeap.findMax s with
+    | Some n => Some(n, PHeap.deleteMax s)
     | None => None
     end.
   Definition initial (successors: PTree.t (list positive)) :=
-    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
-  Definition In := PositiveSet.In.
+    PTree.fold (fun s pc scs => PHeap.insert pc s) successors PHeap.empty.
+  Definition In := PHeap.In.
 
   Lemma add_spec:
     forall n n' s, In n' (add n s) <-> n = n' \/ In n' s.
   Proof.
-    intros. exact (PositiveSetFacts.add_iff s n n').
+    intros. rewrite PHeap.In_insert. unfold In. intuition.
   Qed.
     
   Lemma pick_none:
     forall s n, pick s = None -> ~In n s.
   Proof.
-    intros until n; unfold pick. caseEq (PositiveSet.max_elt s); intros.
+    intros until n; unfold pick. caseEq (PHeap.findMax s); intros.
     congruence.
-    apply PositiveSet.max_elt_3. auto.
+    apply PHeap.findMax_empty. auto.
   Qed.
 
   Lemma pick_some:
     forall s n s', pick s = Some(n, s') ->
     forall n', In n' s <-> n = n' \/ In n' s'.
   Proof.
-    intros until s'; unfold pick. caseEq (PositiveSet.max_elt s); intros.
-    inversion H0; clear H0; subst. 
-    split; intros. 
-    destruct (peq n n'). auto. right. apply PositiveSet.remove_2; assumption.
-    elim H0; intro. subst n'. apply PositiveSet.max_elt_1. auto. 
-    apply PositiveSet.remove_3 with n; assumption.
+    intros until s'; unfold pick. caseEq (PHeap.findMax s); intros.
+    inv H0.
+    generalize (PHeap.In_deleteMax s n n' H). unfold In. intuition.
     congruence.
   Qed.
 
@@ -1233,39 +1222,36 @@ Module NodeSetForward <: NODE_SET.
 End NodeSetForward.
 
 Module NodeSetBackward <: NODE_SET.
-  Definition t := PositiveSet.t.
-  Definition add (n: positive) (s: t) : t := PositiveSet.add n s.
+  Definition t := PHeap.t.
+  Definition add (n: positive) (s: t) : t := PHeap.insert n s.
   Definition pick (s: t) :=
-    match PositiveSet.min_elt s with
-    | Some n => Some(n, PositiveSet.remove n s)
+    match PHeap.findMin s with
+    | Some n => Some(n, PHeap.deleteMin s)
     | None => None
     end.
   Definition initial (successors: PTree.t (list positive)) :=
-    PTree.fold (fun s pc scs => PositiveSet.add pc s) successors PositiveSet.empty.
-  Definition In := PositiveSet.In.
+    PTree.fold (fun s pc scs => PHeap.insert pc s) successors PHeap.empty.
+  Definition In := PHeap.In.
 
   Lemma add_spec:
     forall n n' s, In n' (add n s) <-> n = n' \/ In n' s.
   Proof NodeSetForward.add_spec.
-    
+
   Lemma pick_none:
     forall s n, pick s = None -> ~In n s.
   Proof.
-    intros until n; unfold pick. caseEq (PositiveSet.min_elt s); intros.
+    intros until n; unfold pick. caseEq (PHeap.findMin s); intros.
     congruence.
-    apply PositiveSet.min_elt_3. auto.
+    apply PHeap.findMin_empty. auto.
   Qed.
 
   Lemma pick_some:
     forall s n s', pick s = Some(n, s') ->
     forall n', In n' s <-> n = n' \/ In n' s'.
   Proof.
-    intros until s'; unfold pick. caseEq (PositiveSet.min_elt s); intros.
-    inversion H0; clear H0; subst. 
-    split; intros. 
-    destruct (peq n n'). auto. right. apply PositiveSet.remove_2; assumption.
-    elim H0; intro. subst n'. apply PositiveSet.min_elt_1. auto. 
-    apply PositiveSet.remove_3 with n; assumption.
+    intros until s'; unfold pick. caseEq (PHeap.findMin s); intros.
+    inv H0.
+    generalize (PHeap.In_deleteMin s n n' H). unfold In. intuition.
     congruence.
   Qed.
 
diff --git a/backend/LTL.v b/backend/LTL.v
index 2eff67c..a68352f 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -290,4 +290,4 @@ Definition successors_instr (i: instruction) : list node :=
   end.
 
 Definition successors (f: function): PTree.t (list node) :=
-  PTree.map (fun pc i => successors_instr i) f.(fn_code).
+  PTree.map1 successors_instr f.(fn_code).
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index df75000..abc497e 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -128,7 +128,7 @@ Proof.
   assert (LBoolean.ge reach!!pc' reach!!pc).
   change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)).
   eapply DS.fixpoint_solution. eexact H.
-  unfold Kildall.successors_list, successors. rewrite PTree.gmap.
+  unfold Kildall.successors_list, successors. rewrite PTree.gmap1.
   rewrite H0; auto.
   elim H3; intro. congruence. auto.
   intros. apply PMap.gi.
diff --git a/backend/RTL.v b/backend/RTL.v
index 1c309a0..208c7b1 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -368,7 +368,7 @@ Definition successors_instr (i: instruction) : list node :=
   end.
 
 Definition successors (f: function) : PTree.t (list node) :=
-  PTree.map (fun pc i => successors_instr i) f.(fn_code).
+  PTree.map1 successors_instr f.(fn_code).
 
 (** Transformation of a RTL function instruction by instruction.
   This applies a given transformation function to all instructions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index e918449..a9c8f97 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -591,7 +591,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do n1 <- reserve_instr;
       do n2 <- transl_stmt map sbody n1 nexits ngoto nret rret;
       do xx <- update_instr n1 (Inop n2);
-      ret n1
+      add_instr (Inop n2)
   | Sblock sbody =>
       transl_stmt map sbody nd (nd :: nexits) ngoto nret rret
   | Sexit n =>
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index b49b671..24f8c1a 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1069,7 +1069,7 @@ Proof.
   inv H2. eapply IHs2; eauto.
   (* loop *)
   intros. inversion H1; subst.
-  eapply IHs; eauto. econstructor; eauto.
+  eapply IHs; eauto. econstructor; eauto. econstructor; eauto.
   (* block *)
   intros. inv H1.
   eapply IHs; eauto. econstructor; eauto.
@@ -1216,6 +1216,7 @@ Proof.
   left. apply plus_one. eapply exec_Inop; eauto. 
   econstructor; eauto. 
   econstructor; eauto.
+  econstructor; eauto.
 
   (* block *)
   inv TS.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 44e7c41..9b2e63e 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -885,9 +885,10 @@ Inductive tr_stmt (c: code) (map: mapping):
      tr_stmt c map sfalse nfalse nd nexits ngoto nret rret ->
      tr_condition c map nil a ns ntrue nfalse ->
      tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret
-  | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop,
-     tr_stmt c map sbody nloop ns nexits ngoto nret rret ->
+  | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop nend,
+     tr_stmt c map sbody nloop nend nexits ngoto nret rret ->
      c!ns = Some(Inop nloop) ->
+     c!nend = Some(Inop nloop) ->
      tr_stmt c map (Sloop sbody) ns nd nexits ngoto nret rret
   | tr_Sblock: forall sbody ns nd nexits ngoto nret rret,
      tr_stmt c map sbody ns nd (nd :: nexits) ngoto nret rret ->
@@ -1294,7 +1295,7 @@ Proof.
   econstructor. 
   apply tr_stmt_incr with s1; auto. 
   eapply IHstmt; eauto with rtlg.
-  eauto with rtlg.
+  eauto with rtlg. eauto with rtlg. 
   (* Sblock *)
   econstructor. 
   eapply IHstmt; eauto with rtlg.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index fcdc335..d6d1868 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -356,6 +356,7 @@ let cmdline_actions =
   @ f_opt "madd" option_fmadd
 
 let _ =
+  Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 };
   Cparser.Machine.config := Cparser.Machine.ilp32ll64;
   Cparser.Builtins.set C2C.builtins;
   CPragmas.initialize();
diff --git a/lib/Heaps.v b/lib/Heaps.v
new file mode 100644
index 0000000..a5c0d61
--- /dev/null
+++ b/lib/Heaps.v
@@ -0,0 +1,570 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 heap data structure. *)
+
+(** The implementation uses splay heaps, following C. Okasaki,
+    "Purely functional data structures", section 5.4.
+    One difference: we eliminate duplicate elements.
+    (If an element is already in a heap, inserting it again does nothing.)
+*)
+
+Require Import Coqlib.
+Require Import FSets.
+Require Import Ordered.
+
+Module SplayHeapSet(E: OrderedType).
+
+(** "Raw" implementation.  The "is a binary search tree" invariant
+    is proved separately. *)
+
+Module R.
+
+Inductive heap: Type :=
+  | Empty
+  | Node (l: heap) (x: E.t) (r: heap).
+
+Function partition (pivot: E.t) (h: heap) { struct h } : heap * heap :=
+  match h with
+  | Empty => (Empty, Empty)
+  | Node a x b =>
+      match E.compare x pivot with
+      | EQ _ => (a, b)
+      | LT _ =>
+        match b with
+        | Empty => (h, Empty)
+        | Node b1 y b2 =>
+            match E.compare y pivot with
+            | EQ _ => (Node a x b1, b2)
+            | LT _ =>
+              let (small, big) := partition pivot b2
+              in (Node (Node a x b1) y small, big)
+            | GT _ =>
+              let (small, big) := partition pivot b1
+              in (Node a x small, Node big y b2)
+            end
+        end
+     | GT _ =>
+        match a with
+        | Empty => (Empty, h)
+        | Node a1 y a2 =>
+            match E.compare y pivot with
+            | EQ _ => (a1, Node a2 x b)
+            | LT _ =>
+              let (small, big) := partition pivot a2
+              in (Node a1 y small, Node big x b)
+            | GT _ =>
+              let (small, big) := partition pivot a1
+              in (small, Node big y (Node a2 x b))
+            end
+        end
+    end
+  end.
+
+Definition insert (x: E.t) (h: heap) : heap :=
+  let (a, b) := partition x h in Node a x b.
+
+Fixpoint findMin (h: heap) : option E.t :=
+  match h with
+  | Empty => None
+  | Node Empty x b => Some x
+  | Node a x b => findMin a
+  end.
+
+Function deleteMin (h: heap) : heap :=
+  match h with
+  | Empty => Empty
+  | Node Empty x b => b
+  | Node (Node Empty x b) y c => Node b y c
+  | Node (Node a x b) y c => Node (deleteMin a) x (Node b y c)
+  end.
+
+Fixpoint findMax (h: heap) : option E.t :=
+  match h with
+  | Empty => None
+  | Node a x Empty => Some x
+  | Node a x b => findMax b
+  end.
+
+Function deleteMax (h: heap) : heap :=
+  match h with
+  | Empty => Empty
+  | Node b x Empty => b
+  | Node b x (Node c y Empty) => Node b x c
+  | Node a x (Node b y c) => Node (Node a x b) y (deleteMax c)
+  end.
+
+(** Specification *)
+
+Fixpoint In (x: E.t) (h: heap) : Prop :=
+  match h with
+  | Empty => False
+  | Node a y b => In x a \/ E.eq x y \/ In x b
+  end.
+
+(** Invariants *)
+
+Fixpoint lt_heap (h: heap) (x: E.t) : Prop :=
+  match h with
+  | Empty => True
+  | Node a y b => lt_heap a x /\ E.lt y x /\ lt_heap b x
+  end.
+
+Fixpoint gt_heap (h: heap) (x: E.t) : Prop :=
+  match h with
+  | Empty => True
+  | Node a y b => gt_heap a x /\ E.lt x y /\ gt_heap b x
+  end.
+
+Fixpoint bst (h: heap) : Prop :=
+  match h with
+  | Empty => True
+  | Node a x b => bst a /\ bst b /\ lt_heap a x /\ gt_heap b x
+  end.
+
+Definition le (x y: E.t) := E.eq x y \/ E.lt x y.
+
+Lemma le_lt_trans:
+  forall x1 x2 x3, le x1 x2 -> E.lt x2 x3 -> E.lt x1 x3.
+Proof.
+  unfold le; intros; intuition.
+  destruct (E.compare x1 x3).
+    auto. 
+    elim (@E.lt_not_eq x2 x3). auto. apply E.eq_trans with x1. apply E.eq_sym; auto. auto.
+    elim (@E.lt_not_eq x2 x1). eapply E.lt_trans; eauto. apply E.eq_sym; auto.
+    eapply E.lt_trans; eauto.
+Qed.
+
+Lemma lt_le_trans:
+  forall x1 x2 x3, E.lt x1 x2 -> le x2 x3 -> E.lt x1 x3.
+Proof.
+  unfold le; intros; intuition.
+  destruct (E.compare x1 x3).
+    auto. 
+    elim (@E.lt_not_eq x1 x2). auto. apply E.eq_trans with x3. auto. apply E.eq_sym; auto.
+    elim (@E.lt_not_eq x3 x2). eapply E.lt_trans; eauto. apply E.eq_sym; auto.
+    eapply E.lt_trans; eauto.
+Qed.
+
+Lemma le_trans:
+  forall x1 x2 x3, le x1 x2 -> le x2 x3 -> le x1 x3.
+Proof.
+  intros. destruct H. destruct H0. red; left; eapply E.eq_trans; eauto. 
+  red. right. eapply le_lt_trans; eauto. red; auto.
+  red. right. eapply lt_le_trans; eauto.
+Qed.
+
+Lemma lt_heap_trans:
+  forall x y, le x y ->
+  forall h, lt_heap h x -> lt_heap h y.
+Proof.
+  induction h; simpl; intros. 
+  auto.
+  intuition. eapply lt_le_trans; eauto.
+Qed.
+
+Lemma gt_heap_trans:
+  forall x y, le y x ->
+  forall h, gt_heap h x -> gt_heap h y.
+Proof.
+  induction h; simpl; intros. 
+  auto.
+  intuition. eapply le_lt_trans; eauto.
+Qed.
+
+(** Properties of [partition] *)
+
+Lemma In_partition:
+  forall x pivot, ~E.eq x pivot ->
+  forall h, bst h -> (In x h <-> In x (fst (partition pivot h)) \/ In x (snd (partition pivot h))).
+Proof.
+  intros x pivot NEQ h0. functional induction (partition pivot h0); simpl; intros.
+  tauto.
+  intuition. elim NEQ. eapply E.eq_trans; eauto.
+  intuition.
+  intuition. elim NEQ. eapply E.eq_trans; eauto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+  intuition. 
+  intuition. elim NEQ. eapply E.eq_trans; eauto. 
+  rewrite e3 in IHp; simpl in IHp. intuition.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+Qed.
+
+Lemma partition_lt:
+  forall x pivot h,
+  lt_heap h x -> lt_heap (fst (partition pivot h)) x /\ lt_heap (snd (partition pivot h)) x.
+Proof.
+  intros x pivot h0. functional induction (partition pivot h0); simpl.
+  tauto.
+  tauto.
+  tauto.
+  tauto.
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+  tauto.
+  tauto.
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+Qed.
+ 
+Lemma partition_gt:
+  forall x pivot h,
+  gt_heap h x -> gt_heap (fst (partition pivot h)) x /\ gt_heap (snd (partition pivot h)) x.
+Proof.
+  intros x pivot h0. functional induction (partition pivot h0); simpl.
+  tauto.
+  tauto.
+  tauto.
+  tauto.
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+  tauto.
+  tauto.
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+  rewrite e3 in IHp; simpl in IHp. tauto. 
+Qed.
+
+Lemma partition_split:
+  forall pivot h,
+  bst h -> lt_heap (fst (partition pivot h)) pivot /\ gt_heap (snd (partition pivot h)) pivot.
+Proof.
+  intros pivot h0. functional induction (partition pivot h0); simpl.
+  tauto.
+  intuition. eapply lt_heap_trans; eauto. red; auto. eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto. 
+  intuition. eapply lt_heap_trans; eauto. red; auto.
+  intuition. eapply lt_heap_trans; eauto. red; auto. 
+    eapply lt_heap_trans; eauto. red; auto.
+    apply gt_heap_trans with y; auto. red. left; apply E.eq_sym; auto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+    eapply lt_heap_trans; eauto. red; auto.
+    eapply lt_heap_trans; eauto. red; auto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+    eapply lt_heap_trans; eauto. red; auto.
+    apply gt_heap_trans with y; eauto. red; auto.
+  intuition. eapply gt_heap_trans; eauto. red; auto.
+  intuition. apply lt_heap_trans with y; eauto. red; auto.
+    eapply gt_heap_trans; eauto. red; left; apply E.eq_sym; auto.
+    eapply gt_heap_trans; eauto. red; auto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+    apply lt_heap_trans with y; eauto. red; auto.
+    eapply gt_heap_trans; eauto. red; auto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+    apply gt_heap_trans with y; eauto. red; auto.
+    apply gt_heap_trans with x; eauto. red; auto.
+Qed.
+
+Lemma partition_bst:
+  forall pivot h,
+  bst h ->
+  bst (fst (partition pivot h)) /\ bst (snd (partition pivot h)).
+Proof.
+  intros pivot h0. functional induction (partition pivot h0); simpl.
+  tauto.
+  tauto.
+  tauto.
+  tauto.
+  rewrite e3 in IHp; simpl in IHp. intuition. 
+    apply lt_heap_trans with x; auto. red; auto.
+    generalize (partition_gt y pivot b2 H7). rewrite e3; simpl. tauto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+    generalize (partition_gt x pivot b1 H3). rewrite e3; simpl. tauto.
+    generalize (partition_lt y pivot b1 H4). rewrite e3; simpl. tauto.
+  tauto.
+  tauto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+    generalize (partition_gt y pivot a2 H6). rewrite e3; simpl. tauto.
+    generalize (partition_lt x pivot a2 H8). rewrite e3; simpl. tauto.
+  rewrite e3 in IHp; simpl in IHp. intuition.
+    generalize (partition_lt y pivot a1 H3). rewrite e3; simpl. tauto.
+    apply gt_heap_trans with x; auto. red. auto.
+Qed.
+
+(** Properties of [insert] *)
+
+Lemma insert_bst:
+  forall x h, bst h -> bst (insert x h).
+Proof.
+  intros. 
+  unfold insert. case_eq (partition x h). intros a b EQ; simpl. 
+  generalize (partition_bst x h H).
+  generalize (partition_split x h H).
+  rewrite EQ; simpl. tauto.
+Qed.
+
+Lemma In_insert:
+  forall x h y, bst h -> (In y (insert x h) <-> E.eq y x \/ In y h).
+Proof.
+  intros. unfold insert.
+  case_eq (partition x h). intros a b EQ; simpl. 
+  assert (E.eq y x \/ ~E.eq y x).
+    destruct (E.compare y x); auto.
+    right; red; intros. elim (E.lt_not_eq l). apply E.eq_sym; auto.
+  destruct H0.
+  tauto.
+  generalize (In_partition y x H0 h H). rewrite EQ; simpl. tauto. 
+Qed.
+
+(** Properties of [findMin] and [deleteMin] *)
+
+Lemma deleteMin_lt:
+  forall x h, lt_heap h x -> lt_heap (deleteMin h) x.
+Proof.
+  intros x h0. functional induction (deleteMin h0); simpl; intros.
+  auto.
+  tauto.
+  tauto. 
+  intuition. 
+Qed.
+
+Lemma deleteMin_bst:
+  forall h, bst h -> bst (deleteMin h).
+Proof.
+  intros h0. functional induction (deleteMin h0); simpl; intros.
+  auto.
+  tauto.
+  tauto.
+  intuition.
+    apply deleteMin_lt; auto. 
+    apply gt_heap_trans with y; auto. red; auto. 
+Qed.
+
+Lemma In_deleteMin:
+  forall y x h,
+  findMin h = Some x ->
+  (In y h <-> E.eq y x \/ In y (deleteMin h)).
+Proof.
+  intros y x h0. functional induction (deleteMin h0); simpl; intros.
+  congruence.
+  inv H. tauto.
+  inv H. tauto. 
+  destruct a. contradiction. tauto.
+Qed.
+
+Lemma gt_heap_In:
+  forall x y h, gt_heap h x -> In y h -> E.lt x y.
+Proof.
+  induction h; simpl; intros. 
+  contradiction.
+  intuition. apply lt_le_trans with x0; auto. red. left. apply E.eq_sym; auto.
+Qed.
+
+Lemma findMin_min:
+  forall x h, findMin h = Some x -> bst h -> forall y, In y h -> le x y.
+Proof.
+  induction h; simpl; intros.
+  contradiction.
+  destruct h1.
+  inv H. simpl in *. intuition.
+  red; left; apply E.eq_sym; auto.
+  red; right. eapply gt_heap_In; eauto.
+  assert (le x x1).
+    apply IHh1; auto. tauto. simpl. right; left; apply E.eq_refl.
+  intuition.
+  apply le_trans with x1. auto.  apply le_trans with x0. simpl in H4. red; tauto. 
+  red; left; apply E.eq_sym; auto.
+  apply le_trans with x1. auto. apply le_trans with x0. simpl in H4. red; tauto.
+  red; right. eapply gt_heap_In; eauto.
+Qed.
+
+Lemma findMin_empty:
+  forall h, h <> Empty -> findMin h <> None.
+Proof.
+  induction h; simpl; intros.
+  congruence.
+  destruct h1. congruence. apply IHh1. congruence.
+Qed.
+
+(** Properties of [findMax] and [deleteMax]. *)
+
+Lemma deleteMax_gt:
+  forall x h, gt_heap h x -> gt_heap (deleteMax h) x.
+Proof.
+  intros x h0. functional induction (deleteMax h0); simpl; intros.
+  auto.
+  tauto.
+  tauto. 
+  intuition. 
+Qed.
+
+Lemma deleteMax_bst:
+  forall h, bst h -> bst (deleteMax h).
+Proof.
+  intros h0. functional induction (deleteMax h0); simpl; intros.
+  auto.
+  tauto.
+  tauto.
+  intuition.
+    apply lt_heap_trans with x; auto. red; auto.
+    apply deleteMax_gt; auto.
+Qed.
+
+Lemma In_deleteMax:
+  forall y x h,
+  findMax h = Some x ->
+  (In y h <-> E.eq y x \/ In y (deleteMax h)).
+Proof.
+  intros y x h0. functional induction (deleteMax h0); simpl; intros.
+  congruence.
+  inv H. tauto.
+  inv H. tauto. 
+  destruct c. contradiction. tauto.
+Qed.
+
+Lemma lt_heap_In:
+  forall x y h, lt_heap h x -> In y h -> E.lt y x.
+Proof.
+  induction h; simpl; intros. 
+  contradiction.
+  intuition. apply le_lt_trans with x0; auto. red. left. apply E.eq_sym; auto.
+Qed.
+
+Lemma findMax_max:
+  forall x h, findMax h = Some x -> bst h -> forall y, In y h -> le y x.
+Proof.
+  induction h; simpl; intros.
+  contradiction.
+  destruct h2.
+  inv H. simpl in *. intuition.
+  red; right. eapply lt_heap_In; eauto.
+  red; left. auto.
+  assert (le x1 x).
+    apply IHh2; auto. tauto. simpl. right; left; apply E.eq_refl.
+  intuition.
+  apply le_trans with x1; auto.  apply le_trans with x0.
+  red; right. eapply lt_heap_In; eauto.
+  simpl in H6. red; tauto. 
+  apply le_trans with x1; auto. apply le_trans with x0.
+  red; auto.
+  simpl in H6. red; tauto.
+Qed.
+
+Lemma findMax_empty:
+  forall h, h <> Empty -> findMax h <> None.
+Proof.
+  induction h; simpl; intros.
+  congruence.
+  destruct h2. congruence. apply IHh2. congruence.
+Qed.
+
+End R.
+
+(** Wrapping in a dependent type *)
+
+Definition t := { h: R.heap | R.bst h }.
+
+(** Operations *)
+
+Program Definition empty : t := R.Empty.
+
+Program Definition insert (x: E.t) (h: t) : t := R.insert x h.
+Next Obligation. apply R.insert_bst. apply proj2_sig. Qed.
+
+Program Definition findMin (h: t) : option E.t := R.findMin h.
+
+Program Definition deleteMin (h: t) : t := R.deleteMin h.
+Next Obligation. apply R.deleteMin_bst. apply proj2_sig. Qed.
+
+Program Definition findMax (h: t) : option E.t := R.findMax h.
+
+Program Definition deleteMax (h: t) : t := R.deleteMax h.
+Next Obligation. apply R.deleteMax_bst. apply proj2_sig. Qed.
+
+(** Membership (for specification) *)
+
+Program Definition In (x: E.t) (h: t) : Prop := R.In x h.
+
+(** Properties of [empty] *)
+
+Lemma In_empty: forall x, ~In x empty.
+Proof.
+  intros; red; intros.
+  red in H. simpl in H. tauto.
+Qed.
+
+(** Properties of [insert] *)
+
+Lemma In_insert:
+  forall x h y,
+  In y (insert x h) <-> E.eq y x \/ In y h.
+Proof.
+  intros. unfold In, insert; simpl. apply R.In_insert. apply proj2_sig.
+Qed.
+
+(** Properties of [findMin] *)
+
+Lemma findMin_empty:
+  forall h y, findMin h = None -> ~In y h.
+Proof.
+  unfold findMin, In; intros; simpl. 
+  destruct (proj1_sig h). 
+  simpl. tauto.
+  exploit R.findMin_empty; eauto. congruence.
+Qed.
+
+Lemma findMin_min:
+  forall h x y, findMin h = Some x -> In y h -> E.eq x y \/ E.lt x y.
+Proof.
+  unfold findMin, In; simpl. intros.
+  change (R.le x y). eapply R.findMin_min; eauto. apply proj2_sig.
+Qed.
+
+(** Properties of [deleteMin]. *)
+
+Lemma In_deleteMin:
+  forall h x y,
+  findMin h = Some x ->
+  (In y h <-> E.eq y x \/ In y (deleteMin h)).
+Proof.
+  unfold findMin, In; simpl; intros.
+  apply R.In_deleteMin. auto.
+Qed.
+
+(** Properties of [findMax] *)
+
+Lemma findMax_empty:
+  forall h y, findMax h = None -> ~In y h.
+Proof.
+  unfold findMax, In; intros; simpl. 
+  destruct (proj1_sig h). 
+  simpl. tauto.
+  exploit R.findMax_empty; eauto. congruence.
+Qed.
+
+Lemma findMax_max:
+  forall h x y, findMax h = Some x -> In y h -> E.eq y x \/ E.lt y x.
+Proof.
+  unfold findMax, In; simpl. intros.
+  change (R.le y x). eapply R.findMax_max; eauto. apply proj2_sig.
+Qed.
+
+(** Properties of [deleteMax]. *)
+
+Lemma In_deleteMax:
+  forall h x y,
+  findMax h = Some x ->
+  (In y h <-> E.eq y x \/ In y (deleteMax h)).
+Proof.
+  unfold findMax, In; simpl; intros.
+  apply R.In_deleteMax. auto.
+Qed.
+
+End SplayHeapSet.
+
+(** Instantiation over type [positive] *)
+
+Module PHeap := SplayHeapSet(OrderedPositive).
+
+
diff --git a/lib/Lattice.v b/lib/Lattice.v
index a185c43..c200fc8 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -35,12 +35,11 @@ Module Type SEMILATTICE.
   Variable ge: t -> t -> Prop.
   Hypothesis ge_refl: forall x y, eq x y -> ge x y.
   Hypothesis ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
-  Hypothesis ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
   Variable bot: t.
   Hypothesis ge_bot: forall x, ge x bot.
   Variable lub: t -> t -> t.
-  Hypothesis lub_commut: forall x y, eq (lub x y) (lub y x).
   Hypothesis ge_lub_left: forall x y, ge (lub x y) x.
+  Hypothesis ge_lub_right: forall x y, ge (lub x y) y.
 
 End SEMILATTICE.
 
@@ -57,6 +56,8 @@ End SEMILATTICE_WITH_TOP.
 
 (** * Semi-lattice over maps *)
 
+Set Implicit Arguments.
+
 (** Given a semi-lattice with top [L], the following functor implements
   a semi-lattice structure over finite maps from positive numbers to [L.t].
   The default value for these maps is either [L.top] or [L.bot]. *)
@@ -156,11 +157,6 @@ Proof.
   unfold ge; intros. apply L.ge_trans with (get p y); auto.
 Qed.
 
-Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-Proof.
-  unfold eq,ge; intros. eapply L.ge_compat; eauto.
-Qed.
-
 Definition bot := Bot_except (PTree.empty L.t).
 
 Lemma get_bot: forall p, get p bot = L.bot.
@@ -185,6 +181,232 @@ Proof.
   unfold ge; intros. rewrite get_top. apply L.ge_top.
 Qed.
 
+(** A [combine] operation over the type [PTree.t L.t] that attempts
+  to share its result with its arguments. *)
+
+Section COMBINE.
+
+Variable f: option L.t -> option L.t -> option L.t.
+Hypothesis f_none_none: f None None = None.
+
+Definition opt_eq (ox oy: option L.t) : Prop :=
+  match ox, oy with
+  | None, None => True
+  | Some x, Some y => L.eq x y
+  | _, _ => False
+  end.
+
+Lemma opt_eq_refl: forall ox, opt_eq ox ox.
+Proof.
+  intros. unfold opt_eq. destruct ox. apply L.eq_refl. auto. 
+Qed.
+
+Lemma opt_eq_sym: forall ox oy, opt_eq ox oy -> opt_eq oy ox.
+Proof.
+  unfold opt_eq. destruct ox; destruct oy; auto. apply L.eq_sym. 
+Qed.
+
+Lemma opt_eq_trans: forall ox oy oz, opt_eq ox oy -> opt_eq oy oz -> opt_eq ox oz.
+Proof.
+  unfold opt_eq. destruct ox; destruct oy; destruct oz; intuition. 
+  eapply L.eq_trans; eauto.
+Qed.
+
+Definition opt_beq (ox oy: option L.t) : bool :=
+  match ox, oy with
+  | None, None => true
+  | Some x, Some y => L.beq x y
+  | _, _ => false
+  end.
+
+Lemma opt_beq_correct:
+  forall ox oy, opt_beq ox oy = true -> opt_eq ox oy.
+Proof.
+  unfold opt_beq, opt_eq. destruct ox; destruct oy; try congruence. 
+  intros. apply L.beq_correct; auto. 
+  auto.
+Qed.
+
+Definition tree_eq (m1 m2: PTree.t L.t) : Prop :=
+  forall i, opt_eq (PTree.get i m1) (PTree.get i m2).
+
+Lemma tree_eq_refl: forall m, tree_eq m m.
+Proof. intros; red; intros; apply opt_eq_refl. Qed.
+
+Lemma tree_eq_sym: forall m1 m2, tree_eq m1 m2 -> tree_eq m2 m1.
+Proof. intros; red; intros; apply opt_eq_sym; auto. Qed.
+
+Lemma tree_eq_trans: forall m1 m2 m3, tree_eq m1 m2 -> tree_eq m2 m3 -> tree_eq m1 m3.
+Proof. intros; red; intros; apply opt_eq_trans with (PTree.get i m2); auto. Qed.
+
+Lemma tree_eq_node: 
+  forall l1 o1 r1 l2 o2 r2,
+  tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
+  tree_eq (PTree.Node l1 o1 r1) (PTree.Node l2 o2 r2).
+Proof.
+  intros; red; intros. destruct i; simpl; auto.
+Qed.
+
+Lemma tree_eq_node': 
+  forall l1 o1 r1 l2 o2 r2,
+  tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
+  tree_eq (PTree.Node l1 o1 r1) (PTree.Node' l2 o2 r2).
+Proof.
+  intros; red; intros. rewrite PTree.gnode'. apply tree_eq_node; auto. 
+Qed.
+
+Lemma tree_eq_node'': 
+  forall l1 o1 r1 l2 o2 r2,
+  tree_eq l1 l2 -> tree_eq r1 r2 -> opt_eq o1 o2 ->
+  tree_eq (PTree.Node' l1 o1 r1) (PTree.Node' l2 o2 r2).
+Proof.
+  intros; red; intros. repeat rewrite PTree.gnode'. apply tree_eq_node; auto. 
+Qed.
+
+Hint Resolve opt_beq_correct opt_eq_refl opt_eq_sym 
+             tree_eq_refl tree_eq_sym
+             tree_eq_node tree_eq_node' tree_eq_node'' : combine.
+
+Inductive changed: Type := Unchanged | Changed (m: PTree.t L.t).
+
+Fixpoint combine_l (m : PTree.t L.t) {struct m} : changed :=
+  match m with
+  | PTree.Leaf =>
+      Unchanged
+  | PTree.Node l o r =>
+      let o' := f o None in
+      match combine_l l, combine_l r with
+      | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r)
+      | Unchanged, Changed r' => Changed (PTree.Node' l o' r')
+      | Changed l', Unchanged => Changed (PTree.Node' l' o' r)
+      | Changed l', Changed r' => Changed (PTree.Node' l' o' r')
+      end
+  end.
+
+Lemma combine_l_eq:
+  forall m,
+  tree_eq (match combine_l m with Unchanged => m | Changed m' => m' end)
+          (PTree.xcombine_l f m).
+Proof.
+  induction m; simpl.
+  auto with combine.
+  destruct (combine_l m1) as [ | l']; destruct (combine_l m2) as [ | r'];
+  auto with combine.
+  case_eq (opt_beq (f o None) o); auto with combine.
+Qed.
+
+Fixpoint combine_r (m : PTree.t L.t) {struct m} : changed :=
+  match m with
+  | PTree.Leaf =>
+      Unchanged
+  | PTree.Node l o r =>
+      let o' := f None o in
+      match combine_r l, combine_r r with
+      | Unchanged, Unchanged => if opt_beq o' o then Unchanged else Changed (PTree.Node' l o' r)
+      | Unchanged, Changed r' => Changed (PTree.Node' l o' r')
+      | Changed l', Unchanged => Changed (PTree.Node' l' o' r)
+      | Changed l', Changed r' => Changed (PTree.Node' l' o' r')
+      end
+  end.
+
+Lemma combine_r_eq:
+  forall m,
+  tree_eq (match combine_r m with Unchanged => m | Changed m' => m' end)
+          (PTree.xcombine_r f m).
+Proof.
+  induction m; simpl.
+  auto with combine.
+  destruct (combine_r m1) as [ | l']; destruct (combine_r m2) as [ | r'];
+  auto with combine.
+  case_eq (opt_beq (f None o) o); auto with combine.
+Qed.
+
+Inductive changed2 : Type :=
+  | Same
+  | Same1
+  | Same2
+  | CC(m: PTree.t L.t).
+
+Fixpoint xcombine (m1 m2 : PTree.t L.t) {struct m1} : changed2 :=
+    match m1, m2 with
+    | PTree.Leaf, PTree.Leaf => 
+        Same
+    | PTree.Leaf, _ =>
+        match combine_r m2 with
+        | Unchanged => Same2
+        | Changed m => CC m
+        end
+    | _, PTree.Leaf =>
+        match combine_l m1 with
+        | Unchanged => Same1
+        | Changed m => CC m
+        end
+    | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 =>
+        let o := f o1 o2 in
+        match xcombine l1 l2, xcombine r1 r2 with
+        | Same, Same =>
+            match opt_beq o o1, opt_beq o o2 with
+            | true, true => Same
+            | true, false => Same1
+            | false, true => Same2
+            | false, false => CC(PTree.Node' l1 o r1)
+            end
+        | Same1, Same | Same, Same1 | Same1, Same1 =>
+            if opt_beq o o1 then Same1 else CC(PTree.Node' l1 o r1)
+        | Same2, Same | Same, Same2 | Same2, Same2 =>
+            if opt_beq o o2 then Same2 else CC(PTree.Node' l2 o r2)
+        | Same1, Same2 => CC(PTree.Node' l1 o r2)
+        | (Same|Same1), CC r => CC(PTree.Node' l1 o r)
+        | Same2, Same1 => CC(PTree.Node' l2 o r1)
+        | Same2, CC r => CC(PTree.Node' l2 o r)
+        | CC l, (Same|Same1) => CC(PTree.Node' l o r1)
+        | CC l, Same2 => CC(PTree.Node' l o r2)
+        | CC l, CC r => CC(PTree.Node' l o r)
+        end
+    end.
+
+Lemma xcombine_eq:
+  forall m1 m2, 
+  match xcombine m1 m2 with
+  | Same => tree_eq m1 (PTree.combine f m1 m2) /\ tree_eq m2 (PTree.combine f m1 m2)
+  | Same1 => tree_eq m1 (PTree.combine f m1 m2)
+  | Same2 => tree_eq m2 (PTree.combine f m1 m2)
+  | CC m => tree_eq m (PTree.combine f m1 m2)
+  end.
+Proof.
+Opaque combine_l combine_r PTree.xcombine_l PTree.xcombine_r.
+  induction m1; destruct m2; simpl.
+  split; apply tree_eq_refl.
+  generalize (combine_r_eq (PTree.Node m2_1 o m2_2)).
+  destruct (combine_r (PTree.Node m2_1 o m2_2)); auto.
+  generalize (combine_l_eq (PTree.Node m1_1 o m1_2)).
+  destruct (combine_l (PTree.Node m1_1 o m1_2)); auto.
+  generalize (IHm1_1 m2_1) (IHm1_2 m2_2). 
+  destruct (xcombine m1_1 m2_1);
+  destruct (xcombine m1_2 m2_2); auto with combine;
+  intuition; case_eq (opt_beq (f o o0) o); case_eq (opt_beq (f o o0) o0); auto with combine.
+Qed.
+
+Definition combine (m1 m2: PTree.t L.t) : PTree.t L.t :=
+  match xcombine m1 m2 with
+  | Same|Same1 => m1
+  | Same2 => m2
+  | CC m => m
+  end.
+
+Lemma gcombine:
+  forall m1 m2 i, opt_eq (PTree.get i (combine m1 m2)) (f (PTree.get i m1) (PTree.get i m2)).
+Proof.
+  intros.
+  assert (tree_eq (combine m1 m2) (PTree.combine f m1 m2)).
+  unfold combine.
+  generalize (xcombine_eq m1 m2).
+  destruct (xcombine m1 m2); tauto.
+  eapply opt_eq_trans. apply H. rewrite PTree.gcombine; auto. apply opt_eq_refl.
+Qed.
+
+End COMBINE.
+
 Definition opt_lub (x y: L.t) : option L.t :=
   let z := L.lub x y in
   if L.beq z L.top then None else Some z.
@@ -193,7 +415,7 @@ Definition lub (x y: t) : t :=
   match x, y with
   | Bot_except m, Bot_except n =>
       Bot_except
-        (PTree.combine 
+        (combine
            (fun a b =>
               match a, b with
               | Some u, Some v => Some (L.lub u v)
@@ -203,7 +425,7 @@ Definition lub (x y: t) : t :=
            m n)
   | Bot_except m, Top_except n =>
       Top_except
-        (PTree.combine
+        (combine
            (fun a b =>
               match a, b with
               | Some u, Some v => opt_lub u v
@@ -213,7 +435,7 @@ Definition lub (x y: t) : t :=
         m n)             
   | Top_except m, Bot_except n =>
       Top_except
-        (PTree.combine
+        (combine
            (fun a b =>
               match a, b with
               | Some u, Some v => opt_lub u v
@@ -223,7 +445,7 @@ Definition lub (x y: t) : t :=
         m n)             
   | Top_except m, Top_except n =>
       Top_except
-        (PTree.combine 
+        (combine
            (fun a b =>
               match a, b with
               | Some u, Some v => opt_lub u v
@@ -232,29 +454,26 @@ Definition lub (x y: t) : t :=
            m n)
   end.
 
-Lemma lub_commut:
-  forall x y, eq (lub x y) (lub y x).
+Lemma gcombine_top:
+  forall f t1 t2 p,
+  f None None = None ->
+  L.eq (get p (Top_except (combine f t1 t2)))
+       (match f t1!p t2!p with Some x => x | None => L.top end).
 Proof.
-  intros x y p.
-  assert (forall u v,
-    L.eq (match opt_lub u v with
-          | Some x => x
-          | None => L.top end)
-         (match opt_lub v u with
-         | Some x => x
-         | None => L.top
-         end)).
-  intros. unfold opt_lub. 
-  case_eq (L.beq (L.lub u v) L.top);
-  case_eq (L.beq (L.lub v u) L.top); intros.
-  apply L.eq_refl.
-  eapply L.eq_trans. apply L.eq_sym. apply L.beq_correct; eauto. apply L.lub_commut.
-  eapply L.eq_trans. apply L.lub_commut. apply L.beq_correct; auto.
-  apply L.lub_commut.
-  destruct x; destruct y; simpl;
-  repeat rewrite PTree.gcombine; auto;
-  destruct t0!p; destruct t1!p;
-  auto; apply L.eq_refl || apply L.lub_commut.
+  intros. simpl. generalize (gcombine f H t1 t2 p). unfold opt_eq. 
+  destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p).
+  auto. contradiction. contradiction. intros; apply L.eq_refl.
+Qed.
+
+Lemma gcombine_bot:
+  forall f t1 t2 p,
+  f None None = None ->
+  L.eq (get p (Bot_except (combine f t1 t2)))
+       (match f t1!p t2!p with Some x => x | None => L.bot end).
+Proof.
+  intros. simpl. generalize (gcombine f H t1 t2 p). unfold opt_eq. 
+  destruct ((combine f t1 t2)!p); destruct (f t1!p t2!p).
+  auto. contradiction. contradiction. intros; apply L.eq_refl.
 Qed.
 
 Lemma ge_lub_left:
@@ -265,31 +484,70 @@ Proof.
   intros; unfold opt_lub. 
   case_eq (L.beq (L.lub u v) L.top); intros. apply L.ge_top. apply L.ge_lub_left.
 
-  unfold ge, get, lub; intros; destruct x; destruct y.
+  unfold ge, lub; intros. destruct x; destruct y.
 
-  rewrite PTree.gcombine; auto.
-  destruct t0!p; destruct t1!p.
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot. auto. 
+  simpl. destruct t0!p; destruct t1!p.
   apply L.ge_lub_left.
   apply L.ge_refl. apply L.eq_refl. 
   apply L.ge_bot.
   apply L.ge_refl. apply L.eq_refl.
 
-  rewrite PTree.gcombine; auto.
-  destruct t0!p; destruct t1!p.
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. 
+  simpl. destruct t0!p; destruct t1!p.
   auto.
   apply L.ge_top.
   apply L.ge_bot.
   apply L.ge_top.
 
-  rewrite PTree.gcombine; auto.
-  destruct t0!p; destruct t1!p.
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. 
+  simpl. destruct t0!p; destruct t1!p.
+  auto.
+  apply L.ge_refl. apply L.eq_refl.
+  apply L.ge_top.
+  apply L.ge_top.
+
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. 
+  simpl. destruct t0!p; destruct t1!p.
+  auto.
+  apply L.ge_top.
+  apply L.ge_top.
+  apply L.ge_top.
+Qed.
+
+Lemma ge_lub_right:
+  forall x y, ge (lub x y) y.
+Proof.
+  assert (forall u v,
+    L.ge (match opt_lub u v with Some x => x | None => L.top end) v).
+  intros; unfold opt_lub. 
+  case_eq (L.beq (L.lub u v) L.top); intros. apply L.ge_top. apply L.ge_lub_right.
+
+  unfold ge, lub; intros. destruct x; destruct y.
+
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_bot. auto. 
+  simpl. destruct t0!p; destruct t1!p.
+  apply L.ge_lub_right.
+  apply L.ge_bot.
+  apply L.ge_refl. apply L.eq_refl. 
+  apply L.ge_refl. apply L.eq_refl.
+
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. 
+  simpl. destruct t0!p; destruct t1!p.
   auto.
+  apply L.ge_top.
   apply L.ge_refl. apply L.eq_refl.
   apply L.ge_top.
+
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. 
+  simpl. destruct t0!p; destruct t1!p.
+  auto.
+  apply L.ge_bot.
+  apply L.ge_top.
   apply L.ge_top.
 
-  rewrite PTree.gcombine; auto.
-  destruct t0!p; destruct t1!p.
+  eapply L.ge_trans. apply L.ge_refl. apply gcombine_top. auto. 
+  simpl. destruct t0!p; destruct t1!p.
   auto.
   apply L.ge_top.
   apply L.ge_top.
@@ -303,7 +561,7 @@ End LPMap.
 (** Given a set [S: FSetInterface.S], the following functor
     implements a semi-lattice over these sets, ordered by inclusion. *)
 
-Module LFSet (S: FSetInterface.S) <: SEMILATTICE.
+Module LFSet (S: FSetInterface.WS) <: SEMILATTICE.
 
   Definition t := S.t.
 
@@ -323,10 +581,6 @@ Module LFSet (S: FSetInterface.S) <: SEMILATTICE.
   Proof.
     unfold ge, S.Subset; intros. eauto.
   Qed.
-  Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-  Proof.
-    unfold ge, eq, S.Subset, S.Equal; intros. firstorder.
-  Qed.
 
   Definition  bot: t := S.empty.
   Lemma ge_bot: forall x, ge x bot.
@@ -335,18 +589,17 @@ Module LFSet (S: FSetInterface.S) <: SEMILATTICE.
   Qed.
 
   Definition lub: t -> t -> t := S.union.
-  Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
-  Proof.
-    unfold lub, eq, S.Equal; intros. split; intro.
-    destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto.
-    destruct (S.union_1 H). apply S.union_3; auto. apply S.union_2; auto.
-  Qed.
 
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
     unfold lub, ge, S.Subset; intros. apply S.union_2; auto. 
   Qed.
 
+  Lemma ge_lub_right: forall x y, ge (lub x y) y.
+  Proof.
+    unfold lub, ge, S.Subset; intros. apply S.union_3; auto. 
+  Qed.
+
 End LFSet.
 
 (** * Flat semi-lattice *)
@@ -403,11 +656,6 @@ Proof.
   transitivity t1; auto.
 Qed.
 
-Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-Proof.
-  unfold eq; intros; congruence.
-Qed.
-
 Definition bot: t := Bot.
 
 Lemma ge_bot: forall x, ge x bot.
@@ -431,13 +679,13 @@ Definition lub (x y: t) : t :=
   | Inj a, Inj b => if X.eq a b then Inj a else Top
   end.
 
-Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
+Lemma ge_lub_left: forall x y, ge (lub x y) x.
 Proof.
-  unfold eq; destruct x; destruct y; simpl; auto.
-  case (X.eq t0 t1); case (X.eq t1 t0); intros; congruence.
+  destruct x; destruct y; simpl; auto.
+  case (X.eq t0 t1); simpl; auto.
 Qed.
 
-Lemma ge_lub_left: forall x y, ge (lub x y) x.
+Lemma ge_lub_right: forall x y, ge (lub x y) y.
 Proof.
   destruct x; destruct y; simpl; auto.
   case (X.eq t0 t1); simpl; auto.
@@ -472,11 +720,6 @@ Proof. unfold ge; tauto. Qed.
 Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
 Proof. unfold ge; intuition congruence. Qed.
 
-Lemma ge_compat: forall x x' y y', eq x x' -> eq y y' -> ge x y -> ge x' y'.
-Proof.
-  unfold eq; intros; congruence.
-Qed.
-
 Definition bot := false.
 
 Lemma ge_bot: forall x, ge x bot.
@@ -489,10 +732,10 @@ Proof. unfold ge, top; tauto. Qed.
 
 Definition lub (x y: t) := x || y.
 
-Lemma lub_commut: forall x y, eq (lub x y) (lub y x).
-Proof. intros; unfold eq, lub. apply orb_comm. Qed.
-
 Lemma ge_lub_left: forall x y, ge (lub x y) x.
 Proof. destruct x; destruct y; compute; tauto. Qed.
 
+Lemma ge_lub_right: forall x y, ge (lub x y) y.
+Proof. destruct x; destruct y; compute; tauto. Qed.
+
 End LBoolean.
diff --git a/lib/Maps.v b/lib/Maps.v
index cdee00c..793c223 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -98,6 +98,13 @@ Module Type TREE.
     forall (A B: Type) (f: elt -> A -> B) (i: elt) (m: t A),
     get i (map f m) = option_map (f i) (get i m).
 
+  (** Same as [map], but the function does not receive the [elt] argument. *)
+  Variable map1:
+    forall (A B: Type), (A -> B) -> t A -> t B.
+  Hypothesis gmap1:
+    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
+    get i (map1 f m) = option_map f (get i m).
+
   (** Applying a function pairwise to all data of two trees. *)
   Variable combine:
     forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A.
@@ -492,6 +499,19 @@ Module PTree <: TREE.
     rewrite append_neutral_l; auto.
   Qed.
 
+  Fixpoint map1 (A B: Type) (f: A -> B) (m: t A) {struct m} : t B :=
+    match m with
+    | Leaf => Leaf
+    | Node l o r => Node (map1 f l) (option_map f o) (map1 f r)
+    end.
+
+  Theorem gmap1:
+    forall (A B: Type) (f: A -> B) (i: elt) (m: t A),
+    get i (map1 f m) = option_map f (get i m).
+  Proof.
+    induction i; intros; destruct m; simpl; auto.
+  Qed.
+
   Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A :=
     match l, x, r with
     | Leaf, None, Leaf => Leaf
@@ -1091,13 +1111,13 @@ Module PMap <: MAP.
   Qed.
 
   Definition map (A B : Type) (f : A -> B) (m : t A) : t B :=
-    (f (fst m), PTree.map (fun _ => f) (snd m)).
+    (f (fst m), PTree.map1 f (snd m)).
 
   Theorem gmap:
     forall (A B: Type) (f: A -> B) (i: positive) (m: t A),
     get i (map f m) = f(get i m).
   Proof.
-    intros. unfold map. unfold get. simpl. rewrite PTree.gmap.
+    intros. unfold map. unfold get. simpl. rewrite PTree.gmap1.
     unfold option_map. destruct (PTree.get i (snd m)); auto.
   Qed.