diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 16:57:54 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 16:57:54 +0100 |
commit | 78c4974c0a362cd0ab3bbd80203c0277d267afbb (patch) | |
tree | 225700cd45255386d154044976827c0af0ecc408 /lib/Lattice.v | |
parent | 660c1ec3bb6e52720660d6fbb054884b12dca9ca (diff) | |
download | compcert-kvx-78c4974c0a362cd0ab3bbd80203c0277d267afbb.tar.gz compcert-kvx-78c4974c0a362cd0ab3bbd80203c0277d267afbb.zip |
streamlined lattice code
Diffstat (limited to 'lib/Lattice.v')
-rw-r--r-- | lib/Lattice.v | 33 |
1 files changed, 9 insertions, 24 deletions
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 |