aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/CSE2.v115
-rw-r--r--driver/Compiler.v1
-rw-r--r--lib/HashedSet.v12
-rw-r--r--lib/Lattice.v33
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
generated by cgit (git 2.34.1) at 2024-07-02 00:09:30 +0000