Coloringaux: make identifiers unique; special treatment of precolored

  nodes a la Appel and George.
Maps: in PTree.combine, compress useless subtrees.
Lattice: more efficient implementation of LPMap.
Makefile: build profiling version


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

3 files changed, 129 insertions, 65 deletions

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index c7abdcc..436583f 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -127,3 +127,13 @@ let print_timers () =
 
 let _ = at_exit print_timers
 *)
+
+(* Heap profiling facility *)
+
+(*
+let heap_info msg =
+  Gc.full_major();
+  let s = Gc.stat() in
+  Printf.printf "%s: size %d live %d\n " msg s.Gc.heap_words s.Gc.live_words;
+  flush stdout
+*)
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 390f49d..a185c43 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -80,23 +80,31 @@ Definition get (p: positive) (x: t) : L.t :=
 Definition set (p: positive) (v: L.t) (x: t) : t :=
   match x with
   | Bot_except m =>
-      Bot_except (PTree.set p v m)
+      Bot_except (if L.beq v L.bot then PTree.remove p m else PTree.set p v m)
   | Top_except m =>
-      Top_except (PTree.set p v m)
+      Top_except (if L.beq v L.top then PTree.remove p m else PTree.set p v m)
   end.
 
 Lemma gss:
   forall p v x,
-  get p (set p v x) = v.
+  L.eq (get p (set p v x)) v.
 Proof.
-  intros. destruct x; simpl; rewrite PTree.gss; auto.
+  intros. destruct x; simpl. 
+  case_eq (L.beq v L.bot); intros.
+  rewrite PTree.grs. apply L.eq_sym. apply L.beq_correct; auto. 
+  rewrite PTree.gss. apply L.eq_refl.
+  case_eq (L.beq v L.top); intros.
+  rewrite PTree.grs. apply L.eq_sym. apply L.beq_correct; auto. 
+  rewrite PTree.gss. apply L.eq_refl.
 Qed.
 
 Lemma gso:
   forall p q v x,
   p <> q -> get p (set q v x) = get p x.
 Proof.
-  intros. destruct x; simpl; rewrite PTree.gso; auto.
+  intros. destruct x; simpl.
+  destruct (L.beq v L.bot). rewrite PTree.gro; auto. rewrite PTree.gso; auto.
+  destruct (L.beq v L.top). rewrite PTree.gro; auto. rewrite PTree.gso; auto.
 Qed.
 
 Definition eq (x y: t) : Prop :=
@@ -177,6 +185,10 @@ Proof.
   unfold ge; intros. rewrite get_top. apply L.ge_top.
 Qed.
 
+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.
+
 Definition lub (x y: t) : t :=
   match x, y with
   | Bot_except m, Bot_except n =>
@@ -194,7 +206,7 @@ Definition lub (x y: t) : t :=
         (PTree.combine
            (fun a b =>
               match a, b with
-              | Some u, Some v => Some (L.lub u v)
+              | Some u, Some v => opt_lub u v
               | None, _ => b
               | _, None => None
               end)
@@ -204,7 +216,7 @@ Definition lub (x y: t) : t :=
         (PTree.combine
            (fun a b =>
               match a, b with
-              | Some u, Some v => Some (L.lub u v)
+              | Some u, Some v => opt_lub u v
               | None, _ => None
               | _, None => a
               end)
@@ -214,7 +226,7 @@ Definition lub (x y: t) : t :=
         (PTree.combine 
            (fun a b =>
               match a, b with
-              | Some u, Some v => Some (L.lub u v)
+              | Some u, Some v => opt_lub u v
               | _, _ => None
               end)
            m n)
@@ -223,37 +235,65 @@ Definition lub (x y: t) : t :=
 Lemma lub_commut:
   forall x y, eq (lub x y) (lub y x).
 Proof.
-  intros x y p. 
+  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;
-  try apply L.eq_refl; try apply L.lub_commut.
+  auto; apply L.eq_refl || apply L.lub_commut.
 Qed.
 
 Lemma ge_lub_left:
   forall x y, ge (lub x y) x.
 Proof.
+  assert (forall u v,
+    L.ge (match opt_lub u v with Some x => x | None => L.top end) u).
+  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.
 
-  rewrite PTree.gcombine. 
-  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
+  rewrite PTree.gcombine; auto.
+  destruct t0!p; destruct t1!p.
+  apply L.ge_lub_left.
   apply L.ge_refl. apply L.eq_refl. 
-  destruct t1!p. apply L.ge_bot. apply L.ge_refl. apply L.eq_refl.
-  auto.
+  apply L.ge_bot.
+  apply L.ge_refl. apply L.eq_refl.
 
-  rewrite PTree.gcombine. 
-  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
-  apply L.ge_top. destruct t1!p. apply L.ge_bot. apply L.ge_bot.
+  rewrite PTree.gcombine; auto.
+  destruct t0!p; destruct t1!p.
   auto.
+  apply L.ge_top.
+  apply L.ge_bot.
+  apply L.ge_top.
 
-  rewrite PTree.gcombine. 
-  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
-  apply L.ge_refl. apply L.eq_refl. apply L.ge_refl. apply L.eq_refl. auto.
+  rewrite PTree.gcombine; auto.
+  destruct t0!p; destruct t1!p.
+  auto.
+  apply L.ge_refl. apply L.eq_refl.
+  apply L.ge_top.
+  apply L.ge_top.
 
-  rewrite PTree.gcombine. 
-  destruct t0!p. destruct t1!p. apply L.ge_lub_left.
-  apply L.ge_top. apply L.ge_refl. apply L.eq_refl.
+  rewrite PTree.gcombine; auto.
+  destruct t0!p; destruct t1!p.
   auto.
+  apply L.ge_top.
+  apply L.ge_top.
+  apply L.ge_top.
 Qed.
 
 End LPMap.
diff --git a/lib/Maps.v b/lib/Maps.v
index b607d24..4c0bd50 100644
--- a/lib/Maps.v
+++ b/lib/Maps.v
@@ -102,9 +102,9 @@ Module Type TREE.
   Variable combine:
     forall (A: Type), (option A -> option A -> option A) -> t A -> t A -> t A.
   Hypothesis gcombine:
-    forall (A: Type) (f: option A -> option A -> option A)
-           (m1 m2: t A) (i: elt),
+    forall (A: Type) (f: option A -> option A -> option A),
     f None None = None ->
+    forall (m1 m2: t A) (i: elt),
     get i (combine f m1 m2) = f (get i m1) (get i m2).
   Hypothesis combine_commut:
     forall (A: Type) (f g: option A -> option A -> option A),
@@ -481,70 +481,84 @@ Module PTree <: TREE.
     rewrite append_neutral_l; auto.
   Qed.
 
-    Fixpoint xcombine_l (A : Type) (f : option A -> option A -> option A)
-                       (m : t A) {struct m} : t A :=
+  Definition Node' (A: Type) (l: t A) (x: option A) (r: t A): t A :=
+    match l, x, r with
+    | Leaf, None, Leaf => Leaf
+    | _, _, _ => Node l x r
+    end.
+
+  Lemma gnode':
+    forall (A: Type) (l r: t A) (x: option A) (i: positive),
+    get i (Node' l x r) = get i (Node l x r).
+  Proof.
+    intros. unfold Node'. 
+    destruct l; destruct x; destruct r; auto.
+    destruct i; simpl; auto; rewrite gleaf; auto.
+  Qed.
+
+  Section COMBINE.
+
+  Variable A: Type.
+  Variable f: option A -> option A -> option A.
+  Hypothesis f_none_none: f None None = None.
+
+  Fixpoint xcombine_l (m : t A) {struct m} : t A :=
       match m with
       | Leaf => Leaf
-      | Node l o r => Node (xcombine_l f l) (f o None) (xcombine_l f r)
+      | Node l o r => Node' (xcombine_l l) (f o None) (xcombine_l r)
       end.
 
-    Lemma xgcombine_l :
-          forall (A : Type) (f : option A -> option A -> option A)
-                 (i : positive) (m : t A),
-          f None None = None -> get i (xcombine_l f m) = f (get i m) None.
+  Lemma xgcombine_l :
+          forall (m: t A) (i : positive),
+          get i (xcombine_l m) = f (get i m) None.
     Proof.
-      induction i; intros; destruct m; simpl; auto.
+      induction m; intros; simpl.
+      repeat rewrite gleaf. auto.
+      rewrite gnode'. destruct i; simpl; auto.
     Qed.
 
-    Fixpoint xcombine_r (A : Type) (f : option A -> option A -> option A)
-                       (m : t A) {struct m} : t A :=
+  Fixpoint xcombine_r (m : t A) {struct m} : t A :=
       match m with
       | Leaf => Leaf
-      | Node l o r => Node (xcombine_r f l) (f None o) (xcombine_r f r)
+      | Node l o r => Node' (xcombine_r l) (f None o) (xcombine_r r)
       end.
 
-    Lemma xgcombine_r :
-          forall (A : Type) (f : option A -> option A -> option A)
-                 (i : positive) (m : t A),
-          f None None = None -> get i (xcombine_r f m) = f None (get i m).
+  Lemma xgcombine_r :
+          forall (m: t A) (i : positive),
+          get i (xcombine_r m) = f None (get i m).
     Proof.
-      induction i; intros; destruct m; simpl; auto.
+      induction m; intros; simpl.
+      repeat rewrite gleaf. auto.
+      rewrite gnode'. destruct i; simpl; auto.
     Qed.
 
-  Fixpoint combine (A : Type) (f : option A -> option A -> option A)
-                   (m1 m2 : t A) {struct m1} : t A :=
+  Fixpoint combine (m1 m2 : t A) {struct m1} : t A :=
     match m1 with
-    | Leaf => xcombine_r f m2
+    | Leaf => xcombine_r m2
     | Node l1 o1 r1 =>
         match m2 with
-        | Leaf => xcombine_l f m1
-        | Node l2 o2 r2 => Node (combine f l1 l2) (f o1 o2) (combine f r1 r2)
+        | Leaf => xcombine_l m1
+        | Node l2 o2 r2 => Node' (combine l1 l2) (f o1 o2) (combine r1 r2)
         end
     end.
 
-    Lemma xgcombine:
-      forall (A: Type) (f: option A -> option A -> option A) (i: positive)
-             (m1 m2: t A),
-      f None None = None ->
-      get i (combine f m1 m2) = f (get i m1) (get i m2).
-    Proof.
-      induction i; intros; destruct m1; destruct m2; simpl; auto;
-      try apply xgcombine_r; try apply xgcombine_l; auto.
-    Qed.
-
   Theorem gcombine:
-    forall (A: Type) (f: option A -> option A -> option A)
-           (m1 m2: t A) (i: positive),
-    f None None = None ->
-    get i (combine f m1 m2) = f (get i m1) (get i m2).
+      forall (m1 m2: t A) (i: positive),
+      get i (combine m1 m2) = f (get i m1) (get i m2).
   Proof.
-    intros A f m1 m2 i H; exact (xgcombine f i m1 m2 H).
+    induction m1; intros; simpl.
+    rewrite gleaf. apply xgcombine_r.
+    destruct m2; simpl.
+    rewrite gleaf. rewrite <- xgcombine_l. auto. 
+    repeat rewrite gnode'. destruct i; simpl; auto.
   Qed.
 
-    Lemma xcombine_lr :
-      forall (A : Type) (f g : option A -> option A -> option A) (m : t A),
-      (forall (i j : option A), f i j = g j i) ->
-      xcombine_l f m = xcombine_r g m.
+  End COMBINE.
+
+  Lemma xcombine_lr :
+    forall (A : Type) (f g : option A -> option A -> option A) (m : t A),
+    (forall (i j : option A), f i j = g j i) ->
+    xcombine_l f m = xcombine_r g m.
     Proof.
       induction m; intros; simpl; auto.
       rewrite IHm1; auto.