module UVMHS.Core.Classes.Lattice where

import UVMHS.Core.Init
import UVMHS.Core.Classes.Order

infix  4 ∇,⊑,⊒,⪤
infixl 5 ⊔,⊟
infixl 6 ⊓

class POrd a where (⊑) ∷ a → a → 𝔹

class Bot a where bot ∷ a
class Join a where (⊔) ∷ a → a → a
class (Bot a,Join a) ⇒ JoinLattice a
class Top a where top ∷ a
class Meet a where (⊓) ∷ a → a → a
class (Top a,Meet a) ⇒ MeetLattice a
class (JoinLattice a,MeetLattice a) ⇒ Lattice a

class Dual a where dual ∷ a → a
class Difference a where (⊟) ∷ a → a → a   

data PartialOrdering = PLT | PEQ | PGT | PUN

(∇) ∷ (POrd a) ⇒ a → a → PartialOrdering
a
x ∇ :: forall a. POrd a => a -> a -> PartialOrdering
∇ a
y = case (a
x a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
y,a
y a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
x) of
  (𝔹
True,𝔹
True) → PartialOrdering
PEQ
  (𝔹
True,𝔹
False) → PartialOrdering
PLT
  (𝔹
False,𝔹
True) → PartialOrdering
PGT
  (𝔹
False,𝔹
False) → PartialOrdering
PUN

(⊒) ∷ (POrd a) ⇒ a → a → 𝔹
⊒ :: forall a. POrd a => a -> a -> 𝔹
(⊒) = (a -> a -> 𝔹) -> a -> a -> 𝔹
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
(⊑)

(⪤) ∷ (POrd a) ⇒ a → a → 𝔹
a
x ⪤ :: forall a. POrd a => a -> a -> 𝔹
⪤ a
y = ((a
x a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
y) 𝔹 -> 𝔹 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ 𝔹
True) 𝔹 -> 𝔹 -> 𝔹
⩓ ((a
y a -> a -> 𝔹
forall a. POrd a => a -> a -> 𝔹
⊑ a
x) 𝔹 -> 𝔹 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ 𝔹
False)