From 0ba10d800ae221377bf76dc1e5f5b4351a95cf42 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 26 Aug 2009 12:57:11 +0000
Subject: 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
---
 Makefile               |   6 +-
 backend/Coloringaux.ml | 192 +++++++++++++++++++++++++++++++++----------------
 lib/Camlcoq.ml         |  10 +++
 lib/Lattice.v          |  86 ++++++++++++++++------
 lib/Maps.v             |  98 ++++++++++++++-----------
 5 files changed, 266 insertions(+), 126 deletions(-)

diff --git a/Makefile b/Makefile
index f9abb530..95eca7de 100644
--- a/Makefile
+++ b/Makefile
@@ -96,6 +96,10 @@ ccomp: driver/Configuration.ml
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.native \
         && rm -f ccomp && ln -s _build/driver/Driver.native ccomp
 
+ccomp.prof: driver/Configuration.ml
+	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.p.native \
+        && rm -f ccomp.prof && ln -s _build/driver/Driver.p.native ccomp.prof
+
 ccomp.byte: driver/Configuration.ml
 	$(OCAMLBUILD) $(OCB_OPTIONS) Driver.d.byte \
         && rm -f ccomp.byte && ln -s _build/driver/Driver.d.byte ccomp.byte
@@ -103,7 +107,7 @@ ccomp.byte: driver/Configuration.ml
 runtime:
 	$(MAKE) -C runtime
 
-.PHONY: proof extraction cil ccomp runtime
+.PHONY: proof extraction cil ccomp ccomp.prof ccomp.byte runtime
 
 all:
 	$(MAKE) proof
diff --git a/backend/Coloringaux.ml b/backend/Coloringaux.ml
index 7b61645e..9b657697 100644
--- a/backend/Coloringaux.ml
+++ b/backend/Coloringaux.ml
@@ -36,7 +36,7 @@ open Conventions
    follows. *)
 
 type node =
-  { ident: reg;                         (*r register identifier *)
+  { ident: int;                         (*r unique identifier *)
     typ: typ;                           (*r its type *)
     regclass: int;                      (*r identifier of register class *)
     mutable spillcost: float;           (*r estimated cost of spilling *)
@@ -93,7 +93,7 @@ module DLinkNode = struct
   type t = node
   let make state =
     let rec empty =
-      { ident = Coq_xH; typ = Tint; regclass = 0;
+      { ident = 0; typ = Tint; regclass = 0;
         adjlist = []; degree = 0; spillcost = 0.0;
         movelist = []; alias = None; color = None;
         nstate = state; nprev = empty; nnext = empty }
@@ -149,12 +149,33 @@ module DLinkMove = struct
     in fold dl.mnext accu
 end
 
+(* Auxiliary data structures *)
+
+module IntSet = Set.Make(struct
+  type t = int
+  let compare x y =
+    if x < y then -1 else if x > y then 1 else 0
+end)
+
+module IntPairSet = Set.Make(struct
+  type t = int * int
+  let compare (x1, y1) (x2, y2) =
+    if x1 < x2 then -1 else
+    if x1 > x2 then 1 else
+    if y1 < y2 then -1 else
+    if y1 > y2 then 1 else
+    0
+  end)
+
 (* \subsection{The George-Appel algorithm} *)
 
 (* Below is a straigthforward translation of the pseudo-code at the end
    of the TOPLAS article by George and Appel.  Two bugs were fixed
    and are marked as such.  Please refer to the article for explanations. *)
 
+(* The adjacency set  *)
+let adjSet = ref IntPairSet.empty
+
 (* Low-degree, non-move-related nodes *)
 let simplifyWorklist = DLinkNode.make SimplifyWorklist
 
@@ -182,9 +203,14 @@ let worklistMoves = DLinkMove.make WorklistMoves
 (* Moves not yet ready for coalescing *)
 let activeMoves = DLinkMove.make ActiveMoves
 
+(* To generate node identifiers *)
+let nextRegIdent = ref 0
+
 (* Initialization of all global data structures *)
 
 let init() =
+  adjSet := IntPairSet.empty;
+  nextRegIdent := 0;
   DLinkNode.clear simplifyWorklist;
   DLinkNode.clear freezeWorklist;
   DLinkNode.clear spillWorklist;
@@ -197,17 +223,25 @@ let init() =
 (* Determine if two nodes interfere *)
 
 let interfere n1 n2 =
-  if n1.degree < n2.degree
-  then List.memq n2 n1.adjlist
-  else List.memq n1 n2.adjlist
+  let i1 = n1.ident and i2 = n2.ident in
+  let p = if i1 < i2 then (i1, i2) else (i2, i1) in
+  IntPairSet.mem p !adjSet
 
 (* Add an edge to the graph.  Assume edge is not in graph already *)
 
 let addEdge n1 n2 =
-  n1.adjlist <- n2 :: n1.adjlist;
-  n1.degree  <- 1 + n1.degree;
-  n2.adjlist <- n1 :: n2.adjlist;
-  n2.degree  <- 1 + n2.degree
+  assert (n1 != n2 && not (interfere n1 n2));
+  let i1 = n1.ident and i2 = n2.ident in
+  let p = if i1 < i2 then (i1, i2) else (i2, i1) in
+  adjSet := IntPairSet.add p !adjSet;
+  if n1.nstate <> Colored then begin
+    n1.adjlist <- n2 :: n1.adjlist;
+    n1.degree  <- 1 + n1.degree
+  end;
+  if n2.nstate <> Colored then begin
+    n2.adjlist <- n1 :: n2.adjlist;
+    n2.degree  <- 1 + n2.degree
+  end
 
 (* Apply the given function to the relevant adjacent nodes of a node *)
 
@@ -234,31 +268,55 @@ let nodeMoves n =
 let moveRelated n =
   List.exists moveIsActiveOrWorklist n.movelist
 
+(* Register classes *)
+
+let class_of_type = function Tint -> 0 | Tfloat -> 1
+
+let num_register_classes = 2
+
+let caller_save_registers = [|
+  Array.of_list Conventions.int_caller_save_regs;
+  Array.of_list Conventions.float_caller_save_regs
+|]
+
+let callee_save_registers = [|
+  Array.of_list Conventions.int_callee_save_regs;
+  Array.of_list Conventions.float_callee_save_regs
+|]
+
+let num_available_registers = 
+  [| Array.length caller_save_registers.(0)
+           + Array.length callee_save_registers.(0);
+     Array.length caller_save_registers.(1)
+           + Array.length callee_save_registers.(1) |]
+
 (*i
 (* Check invariants *)
 
+let name_of_node n = string_of_int n.ident
+
 let degreeInvariant n =
   let c = ref 0 in
   iterAdjacent (fun n -> incr c) n;
   if !c <> n.degree then
-    fatal_error("degree invariant violated by " ^ name_of_node n)
+    failwith("degree invariant violated by " ^ name_of_node n)
 
 let simplifyWorklistInvariant n =
   if n.degree < num_available_registers.(n.regclass)
   && not (moveRelated n)
   then ()
-  else fatal_error("simplify worklist invariant violated by " ^ name_of_node n)
+  else failwith("simplify worklist invariant violated by " ^ name_of_node n)
 
 let freezeWorklistInvariant n =
   if n.degree < num_available_registers.(n.regclass)
   && moveRelated n
   then ()
-  else fatal_error("freeze worklist invariant violated by " ^ name_of_node n)
+  else failwith("freeze worklist invariant violated by " ^ name_of_node n)
 
 let spillWorklistInvariant n =
   if n.degree >= num_available_registers.(n.regclass)
   then ()
-  else fatal_error("spill worklist invariant violated by " ^ name_of_node n)
+  else failwith("spill worklist invariant violated by " ^ name_of_node n)
 
 let checkInvariants () =
   DLinkNode.iter
@@ -270,35 +328,14 @@ let checkInvariants () =
   DLinkNode.iter
     (fun n -> degreeInvariant n; spillWorklistInvariant n)
     spillWorklist
-i*)
-
-(* Register classes *)
-
-let class_of_type = function Tint -> 0 | Tfloat -> 1
-
-let num_register_classes = 2
-
-let caller_save_registers = [|
-  Array.of_list Conventions.int_caller_save_regs;
-  Array.of_list Conventions.float_caller_save_regs
-|]
-
-let callee_save_registers = [|
-  Array.of_list Conventions.int_callee_save_regs;
-  Array.of_list Conventions.float_callee_save_regs
-|]
-
-let num_available_registers = 
-  [| Array.length caller_save_registers.(0)
-           + Array.length callee_save_registers.(0);
-     Array.length caller_save_registers.(1)
-           + Array.length callee_save_registers.(1) |]
+*)
 
 (* Build the internal representation of the graph *)
 
 let nodeOfReg r typenv spillcosts =
   let ty = typenv r in
-  { ident = r; typ = ty; regclass = class_of_type ty;
+  incr nextRegIdent;
+  { ident = !nextRegIdent; typ = ty; regclass = class_of_type ty;
     spillcost = (try float(Hashtbl.find spillcosts r) with Not_found -> 0.0);
     adjlist = []; degree = 0; movelist = []; alias = None;
     color = None;
@@ -307,7 +344,8 @@ let nodeOfReg r typenv spillcosts =
 
 let nodeOfMreg mr =
   let ty = mreg_type mr in
-  { ident = Coq_xH; typ = ty; regclass = class_of_type ty;
+  incr nextRegIdent;
+  { ident = !nextRegIdent; typ = ty; regclass = class_of_type ty;
     spillcost = 0.0;
     adjlist = []; degree = 0; movelist = []; alias = None;
     color = Some (R mr);
@@ -332,7 +370,7 @@ let build g typenv spillcosts =
       let n = nodeOfMreg mr in
       Hashtbl.add mreg_mapping mr n;
       n in
-  (* Fill the adjacency lists and compute the degrees. *)
+  (* Fill the adjacency set and the adjacency lists; compute the degrees. *)
   SetRegReg.fold
     (fun (Coq_pair(r1, r2)) () ->
       addEdge (find_reg_node r1) (find_reg_node r2))
@@ -369,6 +407,7 @@ let build g typenv spillcosts =
       else
         DLinkNode.insert n simplifyWorklist)
     reg_mapping;
+  (* Return mapping from pseudo-registers to nodes *)
   reg_mapping
 
 (* Enable moves that have become low-degree related *)
@@ -389,11 +428,11 @@ let decrementDegree n =
   if d = k then begin
     enableMoves n;
     iterAdjacent enableMoves n;
-    if n.nstate <> Colored then begin
-      if moveRelated n
-      then DLinkNode.move n spillWorklist freezeWorklist
-      else DLinkNode.move n spillWorklist simplifyWorklist
-    end
+(*    if n.nstate <> Colored then begin *)
+    if moveRelated n
+    then DLinkNode.move n spillWorklist freezeWorklist
+    else DLinkNode.move n spillWorklist simplifyWorklist
+(*    end *)
   end
 
 (* Simulate the effect of combining nodes [n1] and [n3] on [n2],
@@ -402,11 +441,22 @@ let decrementDegree n =
 let combineEdge n1 n2 =
   assert (n1 != n2);
   if interfere n1 n2 then begin
+    (* The two edges n2--n3 and n2--n1 become one, so degree of n2 decreases *)
     decrementDegree n2
   end else begin
-    n1.adjlist <- n2 :: n1.adjlist;
-    n2.adjlist <- n1 :: n2.adjlist;
-    n1.degree  <- n1.degree + 1
+    (* Add new edge *)
+    let i1 = n1.ident and i2 = n2.ident in
+    let p = if i1 < i2 then (i1, i2) else (i2, i1) in
+    adjSet := IntPairSet.add p !adjSet;
+    if n1.nstate <> Colored then begin
+      n1.adjlist <- n2 :: n1.adjlist;
+      n1.degree  <- 1 + n1.degree
+    end;
+    if n2.nstate <> Colored then begin
+      n2.adjlist <- n1 :: n2.adjlist;
+      (* n2's degree stays the same because the old edge n2--n3 disappears
+         and becomes the new edge n2--n1 *)
+    end
   end
 
 (* Simplification of a low-degree node *)
@@ -420,18 +470,37 @@ let simplify () =
 
 (* Briggs' conservative coalescing criterion *)
 
-let canConservativelyCoalesce n1 n2 =
-  let seen = ref Regset.empty in
-  let k = num_available_registers.(n1.regclass) in
+let canConservativelyCoalesce u v =
+  let seen = ref IntSet.empty in
+  let k = num_available_registers.(u.regclass) in
   let c = ref 0 in
   let consider n =
-    if not (Regset.mem n.ident !seen) then begin
-      seen := Regset.add n.ident !seen;
-      if n.degree >= k || n.nstate = Colored then incr c
+    if not (IntSet.mem n.ident !seen) then begin
+      seen := IntSet.add n.ident !seen;
+      if n.degree >= k then begin
+        incr c;
+        if !c >= k then raise Exit
+      end
     end in
-  iterAdjacent consider n1;
-  iterAdjacent consider n2;
-  !c < k
+  try
+    iterAdjacent consider u;
+    iterAdjacent consider v;
+    true
+  with Exit ->
+    false
+
+(* The alternate criterion for precolored nodes *)
+
+let canCoalescePrecolored u v =
+  let k = num_available_registers.(u.regclass) in
+  let isOK t =
+    if t.degree < k || t.nstate = Colored || interfere t u
+    then ()
+    else raise Exit in
+  try
+    iterAdjacent isOK v; true
+  with Exit ->
+    false
 
 (* Update worklists after a move was processed *)
 
@@ -475,7 +544,9 @@ let coalesce () =
     DLinkMove.insert m constrainedMoves;
     addWorkList u;
     addWorkList v
-  end else if canConservativelyCoalesce u v then begin
+  end else if (if u.nstate = Colored 
+               then canCoalescePrecolored u v
+               else canConservativelyCoalesce u v) then begin
     DLinkMove.insert m coalescedMoves;
     combine u v;
     addWorkList u
@@ -486,10 +557,10 @@ let coalesce () =
 (* Freeze moves associated with node [u] *)
 
 let freezeMoves u =
-  let au = getAlias u in
+  let u' = getAlias u in
   let freeze m =
     let y = getAlias m.src in
-    let v = if y == au then getAlias m.dst else y in
+    let v = if y == u' then getAlias m.dst else y in
     DLinkMove.move m activeMoves frozenMoves;
     if not (moveRelated v)
     && v.degree < num_available_registers.(v.regclass)
@@ -530,7 +601,7 @@ let selectSpill () =
 (* Produce the order of nodes that we'll use for coloring *)
 
 let rec nodeOrder stack =
-  (*i checkInvariants(); i*)
+  (*i checkInvariants(); *)
   if DLinkNode.notempty simplifyWorklist then
     (let n = simplify() in nodeOrder (n :: stack))
   else if DLinkMove.notempty worklistMoves then
@@ -622,6 +693,7 @@ let graph_coloring (f: coq_function) (g: graph) (env: regenv) (regs: Regset.t)
   Array.fill start_points 0 num_register_classes 0;
   let mapping = build g env (spill_costs f) in
   List.iter assign_color (nodeOrder []);
+  init();
   fun r ->
     try location_of_node (getAlias (Hashtbl.find mapping r))
     with Not_found -> R IT1 (* any location *)
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index c7abdccd..436583f1 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 390f49dd..a185c43a 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 b607d241..4c0bd507 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.
-- 
cgit