Commit d91e3bbb authored by Tim Steenvoorden's avatar Tim Steenvoorden
Browse files

implement Lattice for Bool

parent d2c48eb9
......@@ -2,20 +2,6 @@ definition module Algebra.Lattice
/// Based on the Haskell Library Algebra.Lattice by Maximilian Bolingbroke and Oleg Grenrus
/// Sets equipped with a binary operation that is commutative, associative and
/// idempotent. Must satisfy the following laws:
///
/// - Associativity of join:
/// forall a b c, join a (join b c) == join (join a b) c
/// - Commutativity of join:
/// forall a b, join a b == join b a
/// - Idempotency of join:
/// forall a, join a a == a
///
/// Join semilattices capture the notion of sets with a "least upper bound".
class JoinSemilattice a where
(\/) infixr 2 :: !a !a -> a
/// Sets equipped with a binary operation that is commutative, associative and
/// idempotent. Must satisfy the following laws:
///
......@@ -30,6 +16,20 @@ class JoinSemilattice a where
class MeetSemilattice a where
(/\) infixr 3 :: !a !a -> a
/// Sets equipped with a binary operation that is commutative, associative and
/// idempotent. Must satisfy the following laws:
///
/// - Associativity of join:
/// forall a b c, join a (join b c) == join (join a b) c
/// - Commutativity of join:
/// forall a b, join a b == join b a
/// - Idempotency of join:
/// forall a, join a a == a
///
/// Join semilattices capture the notion of sets with a "least upper bound".
class JoinSemilattice a where
(\/) infixr 2 :: !a !a -> a
/// Sets equipped with two binary operations that are both commutative,
/// associative and idempotent, along with absorbtion laws for relating the two
/// binary operations. Must satisfy the following:
......@@ -48,25 +48,6 @@ class MeetSemilattice a where
/// forall a b, join a (meet a b) == a
class Lattice a | JoinSemilattice a & MeetSemilattice a
/// Sets equipped with a binary operation that is commutative, associative and
/// idempotent and supplied with a unitary element. Must satisfy the following
/// laws:
///
/// - Associativity of join:
/// forall a b c, join a (join b c) == join (join a b) c
/// - Commutativity of join:
/// forall a b, join a b == join b a
/// - Idempotency of join:
/// forall a, join a a == a
/// - Bottom (Unitary Element):
/// forall a, join a bottom == a
///
/// Join semilattices capture the notion of sets with a "least upper bound"
/// equipped with a "bottom" element.
//TODO BottomSemilattice? BoundedJoinSemilattice?
class LowerBounded a | JoinSemilattice a where
bottom :: a
/// Sets equipped with a binary operation that is commutative, associative and
/// idempotent and supplied with a unitary element. Must satisfy the following
/// laws:
......@@ -86,6 +67,25 @@ class LowerBounded a | JoinSemilattice a where
class UpperBounded a | MeetSemilattice a where
top :: a
/// Sets equipped with a binary operation that is commutative, associative and
/// idempotent and supplied with a unitary element. Must satisfy the following
/// laws:
///
/// - Associativity of join:
/// forall a b c, join a (join b c) == join (join a b) c
/// - Commutativity of join:
/// forall a b, join a b == join b a
/// - Idempotency of join:
/// forall a, join a a == a
/// - Bottom (Unitary Element):
/// forall a, join a bottom == a
///
/// Join semilattices capture the notion of sets with a "least upper bound"
/// equipped with a "bottom" element.
//TODO BottomSemilattice? BoundedJoinSemilattice?
class LowerBounded a | JoinSemilattice a where
bottom :: a
/// Sets equipped with two binary operations that are both commutative,
/// associative and idempotent and supplied with neutral elements, along with
/// absorbtion laws for relating the two binary operations. Must satisfy the
......
......@@ -14,6 +14,9 @@ prim_noop :: .a
prim_eqBool :: !Bool !Bool -> Bool
prim_trueBool :: Bool
prim_falseBool :: Bool
prim_andBool :: !Bool Bool -> Bool
prim_orBool :: !Bool Bool -> Bool
prim_notBool :: !Bool -> Bool
......
......@@ -26,6 +26,18 @@ prim_eqBool a b = code inline {
eqB
}
/// ## Literals
prim_trueBool :: Bool
prim_trueBool = code inline {
pushB TRUE
}
prim_falseBool :: Bool
prim_falseBool = code inline {
pushB FALSE
}
/// ## Logic
prim_andBool :: !Bool Bool -> Bool
......
......@@ -4,6 +4,7 @@ definition module Data.Bool
// - test inlining of primitives when used as functions or macros
from Algebra.Order import class Eq, class Ord
from Algebra.Lattice import class MeetSemilattice, class JoinSemilattice, class UpperBounded, class LowerBounded
/// # Definition
......@@ -14,6 +15,12 @@ from Algebra.Order import class Eq, class Ord
instance Eq Bool
instance Ord Bool
// instance Enum Bool
instance MeetSemilattice Bool
instance JoinSemilattice Bool
instance UpperBounded Bool
instance LowerBounded Bool
/// # Operations
......
implementation module Data.Bool
import Algebra.Order
import Algebra.Lattice
import Clean.Prim
......@@ -9,7 +10,7 @@ import Clean.Prim
// :: Bool = True | False
// BUILTIN
/// # Instances
/// # Order
instance Eq Bool where
(==) x y = prim_eqBool x y
......@@ -18,6 +19,20 @@ instance Ord Bool where
(<) False True = True
(<) _ _ = False
/// # Algebra
instance MeetSemilattice Bool where
(/\) x y = prim_andBool x y
instance JoinSemilattice Bool where
(\/) x y = prim_orBool x y
instance UpperBounded Bool where
top = prim_trueBool
instance LowerBounded Bool where
bottom = prim_falseBool
/// # Operations
not :: !Bool -> Bool
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment