-- | K3 — Kleene three-valued logic.
--
-- Same three labels as 'Circuit.Logics.H3.H3' (true / false / unknown) and
-- the same lattice tables, but __not__ Heyting: there is no coherent
-- implication instance here. Partial-computation / undefinedness reading.
module Circuit.Logics.K3
  ( K3 (..),
  )
where

import Circuit.Logics.Lattice
  ( JoinSemiLattice (..),
    LowerBounded (..),
    MeetSemiLattice (..),
    UpperBounded (..),
  )

-- | Kleene three-valued logic (lattice only).
data K3
  = KFalse
  | KUnknown
  | KTrue
  deriving (K3 -> K3 -> Bool
(K3 -> K3 -> Bool) -> (K3 -> K3 -> Bool) -> Eq K3
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: K3 -> K3 -> Bool
== :: K3 -> K3 -> Bool
$c/= :: K3 -> K3 -> Bool
/= :: K3 -> K3 -> Bool
Eq, Eq K3
Eq K3 =>
(K3 -> K3 -> Ordering)
-> (K3 -> K3 -> Bool)
-> (K3 -> K3 -> Bool)
-> (K3 -> K3 -> Bool)
-> (K3 -> K3 -> Bool)
-> (K3 -> K3 -> K3)
-> (K3 -> K3 -> K3)
-> Ord K3
K3 -> K3 -> Bool
K3 -> K3 -> Ordering
K3 -> K3 -> K3
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: K3 -> K3 -> Ordering
compare :: K3 -> K3 -> Ordering
$c< :: K3 -> K3 -> Bool
< :: K3 -> K3 -> Bool
$c<= :: K3 -> K3 -> Bool
<= :: K3 -> K3 -> Bool
$c> :: K3 -> K3 -> Bool
> :: K3 -> K3 -> Bool
$c>= :: K3 -> K3 -> Bool
>= :: K3 -> K3 -> Bool
$cmax :: K3 -> K3 -> K3
max :: K3 -> K3 -> K3
$cmin :: K3 -> K3 -> K3
min :: K3 -> K3 -> K3
Ord, Int -> K3 -> ShowS
[K3] -> ShowS
K3 -> String
(Int -> K3 -> ShowS)
-> (K3 -> String) -> ([K3] -> ShowS) -> Show K3
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> K3 -> ShowS
showsPrec :: Int -> K3 -> ShowS
$cshow :: K3 -> String
show :: K3 -> String
$cshowList :: [K3] -> ShowS
showList :: [K3] -> ShowS
Show, ReadPrec [K3]
ReadPrec K3
Int -> ReadS K3
ReadS [K3]
(Int -> ReadS K3)
-> ReadS [K3] -> ReadPrec K3 -> ReadPrec [K3] -> Read K3
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS K3
readsPrec :: Int -> ReadS K3
$creadList :: ReadS [K3]
readList :: ReadS [K3]
$creadPrec :: ReadPrec K3
readPrec :: ReadPrec K3
$creadListPrec :: ReadPrec [K3]
readListPrec :: ReadPrec [K3]
Read, K3
K3 -> K3 -> Bounded K3
forall a. a -> a -> Bounded a
$cminBound :: K3
minBound :: K3
$cmaxBound :: K3
maxBound :: K3
Bounded, Int -> K3
K3 -> Int
K3 -> [K3]
K3 -> K3
K3 -> K3 -> [K3]
K3 -> K3 -> K3 -> [K3]
(K3 -> K3)
-> (K3 -> K3)
-> (Int -> K3)
-> (K3 -> Int)
-> (K3 -> [K3])
-> (K3 -> K3 -> [K3])
-> (K3 -> K3 -> [K3])
-> (K3 -> K3 -> K3 -> [K3])
-> Enum K3
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: K3 -> K3
succ :: K3 -> K3
$cpred :: K3 -> K3
pred :: K3 -> K3
$ctoEnum :: Int -> K3
toEnum :: Int -> K3
$cfromEnum :: K3 -> Int
fromEnum :: K3 -> Int
$cenumFrom :: K3 -> [K3]
enumFrom :: K3 -> [K3]
$cenumFromThen :: K3 -> K3 -> [K3]
enumFromThen :: K3 -> K3 -> [K3]
$cenumFromTo :: K3 -> K3 -> [K3]
enumFromTo :: K3 -> K3 -> [K3]
$cenumFromThenTo :: K3 -> K3 -> K3 -> [K3]
enumFromThenTo :: K3 -> K3 -> K3 -> [K3]
Enum)

instance JoinSemiLattice K3 where
  K3
KFalse \/ :: K3 -> K3 -> K3
\/ K3
x = K3
x
  K3
x \/ K3
KFalse = K3
x
  K3
KUnknown \/ K3
KUnknown = K3
KUnknown
  K3
_ \/ K3
_ = K3
KTrue

instance MeetSemiLattice K3 where
  K3
KTrue /\ :: K3 -> K3 -> K3
/\ K3
x = K3
x
  K3
x /\ K3
KTrue = K3
x
  K3
KUnknown /\ K3
KUnknown = K3
KUnknown
  K3
_ /\ K3
_ = K3
KFalse

instance LowerBounded K3 where
  bottom :: K3
bottom = K3
KFalse

instance UpperBounded K3 where
  top :: K3
top = K3
KTrue