Commit b54721f5 authored by xleroy's avatar xleroy
Browse files

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
parent 63cc20f9
......@@ -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
......
......@@ -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/)
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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).
......@@ -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.
......
......@@ -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
......
......@@ -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 =>
......
......@@ -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.
......
......@@ -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.
......
......@@ -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();
......
(* *********************************************************************)
(* *)
(* 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.