-- | Boolean algebra re-read as a ring of characteristic 2.
--
-- > (+)  = XOR   (symmetric difference)
-- > (*)  = AND
-- > zero = false
-- > one  = true
-- > negate = id
--
-- Keeps Boolean and ring APIs separate while documenting the bridge —
-- relevant if numhask ever wants an explicit Boolean↔Ring story.
module Circuit.Logics.Boolean2Ring
  ( Boolean2Ring (..),
    xorBool,
  )
where

import Circuit.Logics.Boolean (Complemented (..))
import Circuit.Logics.Lattice (LowerBounded (..), MeetSemiLattice (..), UpperBounded (..), (/\))

-- | Carrier wrapper: same Boolean values, ring operations.
newtype Boolean2Ring b = Boolean2Ring {forall b. Boolean2Ring b -> b
getBoolean2Ring :: b}
  deriving (Boolean2Ring b -> Boolean2Ring b -> Bool
(Boolean2Ring b -> Boolean2Ring b -> Bool)
-> (Boolean2Ring b -> Boolean2Ring b -> Bool)
-> Eq (Boolean2Ring b)
forall b. Eq b => Boolean2Ring b -> Boolean2Ring b -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall b. Eq b => Boolean2Ring b -> Boolean2Ring b -> Bool
== :: Boolean2Ring b -> Boolean2Ring b -> Bool
$c/= :: forall b. Eq b => Boolean2Ring b -> Boolean2Ring b -> Bool
/= :: Boolean2Ring b -> Boolean2Ring b -> Bool
Eq, Eq (Boolean2Ring b)
Eq (Boolean2Ring b) =>
(Boolean2Ring b -> Boolean2Ring b -> Ordering)
-> (Boolean2Ring b -> Boolean2Ring b -> Bool)
-> (Boolean2Ring b -> Boolean2Ring b -> Bool)
-> (Boolean2Ring b -> Boolean2Ring b -> Bool)
-> (Boolean2Ring b -> Boolean2Ring b -> Bool)
-> (Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b)
-> (Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b)
-> Ord (Boolean2Ring b)
Boolean2Ring b -> Boolean2Ring b -> Bool
Boolean2Ring b -> Boolean2Ring b -> Ordering
Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
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
forall b. Ord b => Eq (Boolean2Ring b)
forall b. Ord b => Boolean2Ring b -> Boolean2Ring b -> Bool
forall b. Ord b => Boolean2Ring b -> Boolean2Ring b -> Ordering
forall b.
Ord b =>
Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
$ccompare :: forall b. Ord b => Boolean2Ring b -> Boolean2Ring b -> Ordering
compare :: Boolean2Ring b -> Boolean2Ring b -> Ordering
$c< :: forall b. Ord b => Boolean2Ring b -> Boolean2Ring b -> Bool
< :: Boolean2Ring b -> Boolean2Ring b -> Bool
$c<= :: forall b. Ord b => Boolean2Ring b -> Boolean2Ring b -> Bool
<= :: Boolean2Ring b -> Boolean2Ring b -> Bool
$c> :: forall b. Ord b => Boolean2Ring b -> Boolean2Ring b -> Bool
> :: Boolean2Ring b -> Boolean2Ring b -> Bool
$c>= :: forall b. Ord b => Boolean2Ring b -> Boolean2Ring b -> Bool
>= :: Boolean2Ring b -> Boolean2Ring b -> Bool
$cmax :: forall b.
Ord b =>
Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
max :: Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
$cmin :: forall b.
Ord b =>
Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
min :: Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
Ord, Int -> Boolean2Ring b -> ShowS
[Boolean2Ring b] -> ShowS
Boolean2Ring b -> String
(Int -> Boolean2Ring b -> ShowS)
-> (Boolean2Ring b -> String)
-> ([Boolean2Ring b] -> ShowS)
-> Show (Boolean2Ring b)
forall b. Show b => Int -> Boolean2Ring b -> ShowS
forall b. Show b => [Boolean2Ring b] -> ShowS
forall b. Show b => Boolean2Ring b -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall b. Show b => Int -> Boolean2Ring b -> ShowS
showsPrec :: Int -> Boolean2Ring b -> ShowS
$cshow :: forall b. Show b => Boolean2Ring b -> String
show :: Boolean2Ring b -> String
$cshowList :: forall b. Show b => [Boolean2Ring b] -> ShowS
showList :: [Boolean2Ring b] -> ShowS
Show, ReadPrec [Boolean2Ring b]
ReadPrec (Boolean2Ring b)
Int -> ReadS (Boolean2Ring b)
ReadS [Boolean2Ring b]
(Int -> ReadS (Boolean2Ring b))
-> ReadS [Boolean2Ring b]
-> ReadPrec (Boolean2Ring b)
-> ReadPrec [Boolean2Ring b]
-> Read (Boolean2Ring b)
forall b. Read b => ReadPrec [Boolean2Ring b]
forall b. Read b => ReadPrec (Boolean2Ring b)
forall b. Read b => Int -> ReadS (Boolean2Ring b)
forall b. Read b => ReadS [Boolean2Ring b]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall b. Read b => Int -> ReadS (Boolean2Ring b)
readsPrec :: Int -> ReadS (Boolean2Ring b)
$creadList :: forall b. Read b => ReadS [Boolean2Ring b]
readList :: ReadS [Boolean2Ring b]
$creadPrec :: forall b. Read b => ReadPrec (Boolean2Ring b)
readPrec :: ReadPrec (Boolean2Ring b)
$creadListPrec :: forall b. Read b => ReadPrec [Boolean2Ring b]
readListPrec :: ReadPrec [Boolean2Ring b]
Read)

-- | XOR on a complemented meet-semilattice with bounds.
xorBool :: (Complemented b) => b -> b -> b
xorBool :: forall b. Complemented b => b -> b -> b
xorBool b
a b
b =
  let either' :: b
either' = (b
a b -> b -> b
forall a. MeetSemiLattice a => a -> a -> a
/\ b -> b
forall a. Complemented a => a -> a
complement b
b) b -> b -> b
forall b. Complemented b => b -> b -> b
`joinLike` (b -> b
forall a. Complemented a => a -> a
complement b
a b -> b -> b
forall a. MeetSemiLattice a => a -> a -> a
/\ b
b)
   in b
either'
  where
    -- local join via De Morgan when we only have meet+complement+bounds
    joinLike :: a -> a -> a
joinLike a
x a
y = a -> a
forall a. Complemented a => a -> a
complement (a -> a
forall a. Complemented a => a -> a
complement a
x a -> a -> a
forall a. MeetSemiLattice a => a -> a -> a
/\ a -> a
forall a. Complemented a => a -> a
complement a
y)

instance (MeetSemiLattice b, Complemented b, LowerBounded b, UpperBounded b) => Num (Boolean2Ring b) where
  Boolean2Ring b
a + :: Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
+ Boolean2Ring b
b = b -> Boolean2Ring b
forall b. b -> Boolean2Ring b
Boolean2Ring (b -> b -> b
forall b. Complemented b => b -> b -> b
xorBool b
a b
b)
  Boolean2Ring b
a * :: Boolean2Ring b -> Boolean2Ring b -> Boolean2Ring b
* Boolean2Ring b
b = b -> Boolean2Ring b
forall b. b -> Boolean2Ring b
Boolean2Ring (b
a b -> b -> b
forall a. MeetSemiLattice a => a -> a -> a
/\ b
b)
  negate :: Boolean2Ring b -> Boolean2Ring b
negate = Boolean2Ring b -> Boolean2Ring b
forall a. a -> a
id
  abs :: Boolean2Ring b -> Boolean2Ring b
abs = Boolean2Ring b -> Boolean2Ring b
forall a. a -> a
id
  signum :: Boolean2Ring b -> Boolean2Ring b
signum (Boolean2Ring b
b) = b -> Boolean2Ring b
forall b. b -> Boolean2Ring b
Boolean2Ring b
b
  fromInteger :: Integer -> Boolean2Ring b
fromInteger Integer
n
    | Integer
n Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = b -> Boolean2Ring b
forall b. b -> Boolean2Ring b
Boolean2Ring b
forall a. LowerBounded a => a
bottom
    | Bool
otherwise = b -> Boolean2Ring b
forall b. b -> Boolean2Ring b
Boolean2Ring b
forall a. UpperBounded a => a
top