-- | H3 — smallest Heyting algebra that is not Boolean.
--
-- Values: true / false / unknown. Implication is defined so Heyting laws
-- hold; excluded middle fails at @HUnknown@.
--
-- Epistemic reading: \"do we know enough to assert?\" — a natural output
-- alphabet for @Process obs H3@.
module Circuit.Logics.H3
  ( H3 (..),
  )
where

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

-- | Three-valued Heyting algebra (intuitionistic toy model).
data H3
  = -- | Known false / bottom.
    HFalse
  | -- | Open / undecided.
    HUnknown
  | -- | Known true / top.
    HTrue
  deriving (H3 -> H3 -> Bool
(H3 -> H3 -> Bool) -> (H3 -> H3 -> Bool) -> Eq H3
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: H3 -> H3 -> Bool
== :: H3 -> H3 -> Bool
$c/= :: H3 -> H3 -> Bool
/= :: H3 -> H3 -> Bool
Eq, Eq H3
Eq H3 =>
(H3 -> H3 -> Ordering)
-> (H3 -> H3 -> Bool)
-> (H3 -> H3 -> Bool)
-> (H3 -> H3 -> Bool)
-> (H3 -> H3 -> Bool)
-> (H3 -> H3 -> H3)
-> (H3 -> H3 -> H3)
-> Ord H3
H3 -> H3 -> Bool
H3 -> H3 -> Ordering
H3 -> H3 -> H3
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 :: H3 -> H3 -> Ordering
compare :: H3 -> H3 -> Ordering
$c< :: H3 -> H3 -> Bool
< :: H3 -> H3 -> Bool
$c<= :: H3 -> H3 -> Bool
<= :: H3 -> H3 -> Bool
$c> :: H3 -> H3 -> Bool
> :: H3 -> H3 -> Bool
$c>= :: H3 -> H3 -> Bool
>= :: H3 -> H3 -> Bool
$cmax :: H3 -> H3 -> H3
max :: H3 -> H3 -> H3
$cmin :: H3 -> H3 -> H3
min :: H3 -> H3 -> H3
Ord, Int -> H3 -> ShowS
[H3] -> ShowS
H3 -> String
(Int -> H3 -> ShowS)
-> (H3 -> String) -> ([H3] -> ShowS) -> Show H3
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> H3 -> ShowS
showsPrec :: Int -> H3 -> ShowS
$cshow :: H3 -> String
show :: H3 -> String
$cshowList :: [H3] -> ShowS
showList :: [H3] -> ShowS
Show, ReadPrec [H3]
ReadPrec H3
Int -> ReadS H3
ReadS [H3]
(Int -> ReadS H3)
-> ReadS [H3] -> ReadPrec H3 -> ReadPrec [H3] -> Read H3
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS H3
readsPrec :: Int -> ReadS H3
$creadList :: ReadS [H3]
readList :: ReadS [H3]
$creadPrec :: ReadPrec H3
readPrec :: ReadPrec H3
$creadListPrec :: ReadPrec [H3]
readListPrec :: ReadPrec [H3]
Read, H3
H3 -> H3 -> Bounded H3
forall a. a -> a -> Bounded a
$cminBound :: H3
minBound :: H3
$cmaxBound :: H3
maxBound :: H3
Bounded, Int -> H3
H3 -> Int
H3 -> [H3]
H3 -> H3
H3 -> H3 -> [H3]
H3 -> H3 -> H3 -> [H3]
(H3 -> H3)
-> (H3 -> H3)
-> (Int -> H3)
-> (H3 -> Int)
-> (H3 -> [H3])
-> (H3 -> H3 -> [H3])
-> (H3 -> H3 -> [H3])
-> (H3 -> H3 -> H3 -> [H3])
-> Enum H3
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 :: H3 -> H3
succ :: H3 -> H3
$cpred :: H3 -> H3
pred :: H3 -> H3
$ctoEnum :: Int -> H3
toEnum :: Int -> H3
$cfromEnum :: H3 -> Int
fromEnum :: H3 -> Int
$cenumFrom :: H3 -> [H3]
enumFrom :: H3 -> [H3]
$cenumFromThen :: H3 -> H3 -> [H3]
enumFromThen :: H3 -> H3 -> [H3]
$cenumFromTo :: H3 -> H3 -> [H3]
enumFromTo :: H3 -> H3 -> [H3]
$cenumFromThenTo :: H3 -> H3 -> H3 -> [H3]
enumFromThenTo :: H3 -> H3 -> H3 -> [H3]
Enum)

instance JoinSemiLattice H3 where
  H3
HFalse \/ :: H3 -> H3 -> H3
\/ H3
x = H3
x
  H3
x \/ H3
HFalse = H3
x
  H3
HUnknown \/ H3
HUnknown = H3
HUnknown
  H3
_ \/ H3
_ = H3
HTrue

instance MeetSemiLattice H3 where
  H3
HTrue /\ :: H3 -> H3 -> H3
/\ H3
x = H3
x
  H3
x /\ H3
HTrue = H3
x
  H3
HUnknown /\ H3
HUnknown = H3
HUnknown
  H3
_ /\ H3
_ = H3
HFalse

instance LowerBounded H3 where
  bottom :: H3
bottom = H3
HFalse

instance UpperBounded H3 where
  top :: H3
top = H3
HTrue

instance Heyting H3 where
  H3
_ ==> :: H3 -> H3 -> H3
==> H3
HTrue = H3
HTrue
  H3
HFalse ==> H3
_ = H3
HTrue
  H3
HTrue ==> H3
HFalse = H3
HFalse
  H3
HUnknown ==> H3
HUnknown = H3
HTrue
  H3
HUnknown ==> H3
HFalse = H3
HFalse
  H3
_ ==> H3
_ = H3
HUnknown

-- | Pseudo-complement @a ==> HFalse@. Not a Boolean complement:
-- @HUnknown \\/ complement HUnknown /= HTrue@.
instance Complemented H3 where
  complement :: H3 -> H3
complement H3
a = H3
a H3 -> H3 -> H3
forall a. Heyting a => a -> a -> a
==> H3
HFalse