streamlined lattice code

2 files changed, 15 insertions, 30 deletions

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