-- | Encodes a security lattice.
module SME.Lattice where


-- | Type class to encode security lattices.
class Eq a => Lattice  a where
    -- | The greatest lower bound between two security levels.
    meet :: a -> a -> Maybe a
    -- | The lowest upper bound between two security levels.
    join :: a -> a -> Maybe a

-- | Type class to encode finite security lattices.
class Lattice a => FiniteLattice a where
    -- | All the elements in the lattice. 
    universe :: [a]
    -- | It returns all the elements in the lattice that are strictly above the security level given as argument. 
    upset :: a -> [a]   -- upper set



-- | Implementation of the order relationship between elements of the lattice.
less :: Lattice a => a -> a -> Bool 
less l  h  = case h `meet` l of 
                  Nothing -> False 
                  Just r  -> h == r  

-- | Implementation of the strict order relationship between security levels of the lattice.
sless :: Lattice a => a -> a -> Bool 
sless p q  = p `less` q && p /= q