diff options
-rw-r--r-- | backend/CSE2.v | 115 | ||||
-rw-r--r-- | driver/Compiler.v | 1 | ||||
-rw-r--r-- | lib/HashedSet.v | 12 | ||||
-rw-r--r-- | lib/Lattice.v | 33 |
4 files changed, 17 insertions, 144 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index be72405b..99ecc623 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -29,7 +29,7 @@ Proof. decide equality. Defined. -Module RELATION. +Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Definition t := (PTree.t sym_val). Definition eq (r1 r2 : t) := @@ -138,119 +138,6 @@ Qed. End RELATION. -Module Type SEMILATTICE_WITHOUT_BOTTOM. - - Parameter t: Type. - Parameter eq: t -> t -> Prop. - Axiom eq_refl: forall x, eq x x. - Axiom eq_sym: forall x y, eq x y -> eq y x. - Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Parameter beq: t -> t -> bool. - Axiom beq_correct: forall x y, beq x y = true -> eq x y. - Parameter ge: t -> t -> Prop. - Axiom ge_refl: forall x y, eq x y -> ge x y. - Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Parameter lub: t -> t -> t. - Axiom ge_lub_left: forall x y, ge (lub x y) x. - Axiom ge_lub_right: forall x y, ge (lub x y) y. - -End SEMILATTICE_WITHOUT_BOTTOM. - -Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). - Definition t := option L.t. - Definition eq (a b : t) := - match a, b with - | None, None => True - | Some x, Some y => L.eq x y - | Some _, None | None, Some _ => False - end. - - Lemma eq_refl: forall x, eq x x. - Proof. - unfold eq; destruct x; trivial. - apply L.eq_refl. - Qed. - - Lemma eq_sym: forall x y, eq x y -> eq y x. - Proof. - unfold eq; destruct x; destruct y; trivial. - apply L.eq_sym. - Qed. - - Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Proof. - unfold eq; destruct x; destruct y; destruct z; trivial. - - apply L.eq_trans. - - contradiction. - Qed. - - Definition beq (x y : t) := - match x, y with - | None, None => true - | Some x, Some y => L.beq x y - | Some _, None | None, Some _ => false - end. - - Lemma beq_correct: forall x y, beq x y = true -> eq x y. - Proof. - unfold beq, eq. - destruct x; destruct y; trivial; try congruence. - apply L.beq_correct. - Qed. - - Definition ge (x y : t) := - match x, y with - | None, Some _ => False - | _, None => True - | Some a, Some b => L.ge a b - end. - - Lemma ge_refl: forall x y, eq x y -> ge x y. - Proof. - unfold eq, ge. - destruct x; destruct y; trivial. - apply L.ge_refl. - Qed. - - Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Proof. - unfold ge. - destruct x; destruct y; destruct z; trivial; try contradiction. - apply L.ge_trans. - Qed. - - Definition bot: t := None. - Lemma ge_bot: forall x, ge x bot. - Proof. - unfold ge, bot. - destruct x; trivial. - Qed. - - Definition lub (a b : t) := - match a, b with - | None, _ => b - | _, None => a - | (Some x), (Some y) => Some (L.lub x y) - end. - - Lemma ge_lub_left: forall x y, ge (lub x y) x. - Proof. - unfold ge, lub. - destruct x; destruct y; trivial. - - apply L.ge_lub_left. - - apply L.ge_refl. - apply L.eq_refl. - Qed. - - Lemma ge_lub_right: forall x y, ge (lub x y) y. - Proof. - unfold ge, lub. - destruct x; destruct y; trivial. - - apply L.ge_lub_right. - - apply L.ge_refl. - apply L.eq_refl. - Qed. -End ADD_BOTTOM. Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..294aad1f 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -43,6 +43,7 @@ Require Constprop. Require CSE. Require ForwardMoves. Require CSE2. +Require CSE3. Require Deadcode. Require Unusedglob. Require Allnontrap. diff --git a/lib/HashedSet.v b/lib/HashedSet.v index 6130ba17..2a798727 100644 --- a/lib/HashedSet.v +++ b/lib/HashedSet.v @@ -3,6 +3,8 @@ Require Import Bool. Require Import List. Require Coq.Logic.Eqdep_dec. +Require Extraction. + Module Type POSITIVE_SET. Parameter t : Type. Parameter empty : t. @@ -116,7 +118,7 @@ Axiom gfilter: End POSITIVE_SET. -Module PSet <: POSITIVE_SET. +Module PSet : POSITIVE_SET. (* begin from Maps *) Fixpoint prev_append (i j: positive) {struct i} : positive := match i with @@ -1382,10 +1384,8 @@ Proof. intros. apply WR.gfilter. Qed. -End PSet. -Require Extraction. - -Extract Inductive PSet.WR.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". +Extract Inductive WR.pset => "HashedSetaux.pset" [ "HashedSetaux.empty" "HashedSetaux.node" ] "HashedSetaux.pset_match". -Extract Inlined Constant PSet.WR.pset_eq => "HashedSetaux.eq". +Extract Inlined Constant WR.pset_eq => "HashedSetaux.eq". +End PSet. diff --git a/lib/Lattice.v b/lib/Lattice.v index 2b81f7af..8ea736ad 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -30,7 +30,8 @@ Local Unset Case Analysis Schemes. [bot], and an upper bound operation [lub]. Note that we do not demand that [lub] computes the least upper bound. *) -Module Type SEMILATTICE. + +Module Type SEMILATTICE_WITHOUT_BOTTOM. Parameter t: Type. Parameter eq: t -> t -> Prop. @@ -42,45 +43,29 @@ Module Type SEMILATTICE. Parameter ge: t -> t -> Prop. Axiom ge_refl: forall x y, eq x y -> ge x y. Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Parameter bot: t. - Axiom ge_bot: forall x, ge x bot. Parameter lub: t -> t -> t. Axiom ge_lub_left: forall x y, ge (lub x y) x. Axiom ge_lub_right: forall x y, ge (lub x y) y. +End SEMILATTICE_WITHOUT_BOTTOM. + +Module Type SEMILATTICE. + Include SEMILATTICE_WITHOUT_BOTTOM. + Parameter bot: t. + Axiom ge_bot: forall x, ge x bot. End SEMILATTICE. (** A semi-lattice ``with top'' is similar, but also has a greatest element [top]. *) Module Type SEMILATTICE_WITH_TOP. - Include SEMILATTICE. Parameter top: t. Axiom ge_top: forall x, ge top x. - End SEMILATTICE_WITH_TOP. -Module Type SEMILATTICE_WITHOUT_BOTTOM. - - Parameter t: Type. - Parameter eq: t -> t -> Prop. - Axiom eq_refl: forall x, eq x x. - Axiom eq_sym: forall x y, eq x y -> eq y x. - Axiom eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Parameter beq: t -> t -> bool. - Axiom beq_correct: forall x y, beq x y = true -> eq x y. - Parameter ge: t -> t -> Prop. - Axiom ge_refl: forall x y, eq x y -> ge x y. - Axiom ge_trans: forall x y z, ge x y -> ge y z -> ge x z. - Parameter lub: t -> t -> t. - Axiom ge_lub_left: forall x y, ge (lub x y) x. - Axiom ge_lub_right: forall x y, ge (lub x y) y. - -End SEMILATTICE_WITHOUT_BOTTOM. - -Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). +Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM) <: SEMILATTICE. Definition t := option L.t. Definition eq (a b : t) := match a, b with |