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: [PATCH] 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 f9abb5301..95eca7ded 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 7b61645ed..9b6576977 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 c7abdccd1..436583f13 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 390f49ddb..a185c43a5 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 b607d2416..4c0bd5078 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.
--
GitLab