diff options
| -rw-r--r-- | .depend | 9 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | backend/Allocproof.v | 2 | ||||
| -rw-r--r-- | backend/CSEproof.v | 2 | ||||
| -rw-r--r-- | backend/CastOptim.v | 8 | ||||
| -rw-r--r-- | backend/CastOptimproof.v | 2 | ||||
| -rw-r--r-- | backend/Constprop.v | 13 | ||||
| -rw-r--r-- | backend/Constpropproof.v | 2 | ||||
| -rw-r--r-- | backend/Kildall.v | 70 | ||||
| -rw-r--r-- | backend/LTL.v | 2 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 2 | ||||
| -rw-r--r-- | backend/RTL.v | 2 | ||||
| -rw-r--r-- | backend/RTLgen.v | 2 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 3 | ||||
| -rw-r--r-- | backend/RTLgenspec.v | 7 | ||||
| -rw-r--r-- | driver/Driver.ml | 1 | ||||
| -rw-r--r-- | lib/Heaps.v | 570 | ||||
| -rw-r--r-- | lib/Lattice.v | 383 | ||||
| -rw-r--r-- | lib/Maps.v | 24 |
19 files changed, 965 insertions, 141 deletions
@@ -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/) 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. @@ -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. |