diff options
Diffstat (limited to 'lib/Lattice.v')
| -rw-r--r-- | lib/Lattice.v | 27 |
1 files changed, 6 insertions, 21 deletions
diff --git a/lib/Lattice.v b/lib/Lattice.v index 3c39006..1d58ee5 100644 --- a/lib/Lattice.v +++ b/lib/Lattice.v @@ -25,7 +25,7 @@ Require Import FSets. Module Type SEMILATTICE. - Variable t: Set. + Variable t: Type. Variable eq: t -> t -> Prop. Hypothesis eq_refl: forall x, eq x x. Hypothesis eq_sym: forall x y, eq x y -> eq y x. @@ -49,24 +49,9 @@ End SEMILATTICE. Module Type SEMILATTICE_WITH_TOP. - Variable t: Set. - Variable eq: t -> t -> Prop. - Hypothesis eq_refl: forall x, eq x x. - Hypothesis eq_sym: forall x y, eq x y -> eq y x. - Hypothesis eq_trans: forall x y z, eq x y -> eq y z -> eq x z. - Variable beq: t -> t -> bool. - Hypothesis beq_correct: forall x y, beq x y = true -> eq x y. - 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. + Include Type SEMILATTICE. Variable top: t. Hypothesis ge_top: forall x, ge top x. - 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. End SEMILATTICE_WITH_TOP. @@ -78,11 +63,11 @@ End SEMILATTICE_WITH_TOP. Module LPMap(L: SEMILATTICE_WITH_TOP) <: SEMILATTICE_WITH_TOP. -Inductive t_ : Set := +Inductive t_ : Type := | Bot_except: PTree.t L.t -> t_ | Top_except: PTree.t L.t -> t_. -Definition t: Set := t_. +Definition t: Type := t_. Definition get (p: positive) (x: t) : L.t := match x with @@ -333,12 +318,12 @@ End LFSet. Module LFlat(X: EQUALITY_TYPE) <: SEMILATTICE_WITH_TOP. -Inductive t_ : Set := +Inductive t_ : Type := | Bot: t_ | Inj: X.t -> t_ | Top: t_. -Definition t : Set := t_. +Definition t : Type := t_. Definition eq (x y: t) := (x = y). Definition eq_refl: forall x, eq x x := (@refl_equal t). |