{-# LANGUAGE TypeApplications #-}
module Data.Recursive.Bool (RBool, module Data.Recursive.Bool) where
import Data.Recursive.Internal
import qualified Data.Propagator.Purify as Purify
import Data.Propagator.P2
get :: RBool -> Bool
get :: RBool -> Bool
get (RBool Purify P2
p) = Purify P2 -> Bool
forall pa a. Propagator pa a => Purify pa -> a
Purify.get Purify P2
p
mk :: Bool -> RBool
mk :: Bool -> RBool
mk Bool
b = OpenR RBool -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR RBool -> RBool) -> OpenR RBool -> RBool
forall a b. (a -> b) -> a -> b
$ Bool -> Purify P2
forall p a. Propagator p a => a -> Purify p
Purify.mk Bool
b
true :: RBool
true :: RBool
true = OpenR RBool -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR RBool -> RBool) -> OpenR RBool -> RBool
forall a b. (a -> b) -> a -> b
$ Bool -> Purify P2
forall p a. Propagator p a => a -> Purify p
Purify.mk Bool
True
false :: RBool
false :: RBool
false = OpenR RBool -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR RBool -> RBool) -> OpenR RBool -> RBool
forall a b. (a -> b) -> a -> b
$ Bool -> Purify P2
forall p a. Propagator p a => a -> Purify p
Purify.mk Bool
False
(&&) :: RBool -> RBool -> RBool
&& :: RBool -> RBool -> RBool
(&&) = OpenR (RBool -> RBool -> RBool) -> RBool -> RBool -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RBool -> RBool -> RBool) -> RBool -> RBool -> RBool)
-> OpenR (RBool -> RBool -> RBool) -> RBool -> RBool -> RBool
forall a b. (a -> b) -> a -> b
$ (P2 -> P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2 -> Purify P2
forall pa a pb b pc c.
(Propagator pa a, Propagator pb b, Propagator pc c) =>
(pa -> pb -> pc -> IO ()) -> Purify pa -> Purify pb -> Purify pc
Purify.def2 ((P2 -> P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2 -> Purify P2)
-> (P2 -> P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2 -> Purify P2
forall a b. (a -> b) -> a -> b
$ \P2
p1 P2
p2 P2
p ->
P2 -> IO () -> IO ()
whenTop P2
p1 (P2 -> IO () -> IO ()
whenTop P2
p2 (P2 -> IO ()
setTop P2
p))
(||) :: RBool -> RBool -> RBool
|| :: RBool -> RBool -> RBool
(||) = OpenR (RBool -> RBool -> RBool) -> RBool -> RBool -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RBool -> RBool -> RBool) -> RBool -> RBool -> RBool)
-> OpenR (RBool -> RBool -> RBool) -> RBool -> RBool -> RBool
forall a b. (a -> b) -> a -> b
$ (P2 -> P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2 -> Purify P2
forall pa a pb b pc c.
(Propagator pa a, Propagator pb b, Propagator pc c) =>
(pa -> pb -> pc -> IO ()) -> Purify pa -> Purify pb -> Purify pc
Purify.def2 ((P2 -> P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2 -> Purify P2)
-> (P2 -> P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2 -> Purify P2
forall a b. (a -> b) -> a -> b
$ \P2
p1 P2
p2 P2
p -> do
P2 -> IO () -> IO ()
whenTop P2
p1 (P2 -> IO ()
setTop P2
p)
P2 -> IO () -> IO ()
whenTop P2
p2 (P2 -> IO ()
setTop P2
p)
and :: [RBool] -> RBool
and :: [RBool] -> RBool
and = OpenR ([RBool] -> RBool) -> [RBool] -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR ([RBool] -> RBool) -> [RBool] -> RBool)
-> OpenR ([RBool] -> RBool) -> [RBool] -> RBool
forall a b. (a -> b) -> a -> b
$ ([P2] -> P2 -> IO ()) -> [Purify P2] -> Purify P2
forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
([pa] -> pb -> IO ()) -> [Purify pa] -> Purify pb
Purify.defList (([P2] -> P2 -> IO ()) -> [Purify P2] -> Purify P2)
-> ([P2] -> P2 -> IO ()) -> [Purify P2] -> Purify P2
forall a b. (a -> b) -> a -> b
$ [P2] -> P2 -> IO ()
go
where
go :: [P2] -> P2 -> IO ()
go [] P2
p = P2 -> IO ()
setTop P2
p
go (P2
p':[P2]
ps) P2
p = P2 -> IO () -> IO ()
whenTop P2
p' ([P2] -> P2 -> IO ()
go [P2]
ps P2
p)
or :: [RBool] -> RBool
or :: [RBool] -> RBool
or = OpenR ([RBool] -> RBool) -> [RBool] -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR ([RBool] -> RBool) -> [RBool] -> RBool)
-> OpenR ([RBool] -> RBool) -> [RBool] -> RBool
forall a b. (a -> b) -> a -> b
$ ([P2] -> P2 -> IO ()) -> [Purify P2] -> Purify P2
forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
([pa] -> pb -> IO ()) -> [Purify pa] -> Purify pb
Purify.defList (([P2] -> P2 -> IO ()) -> [Purify P2] -> Purify P2)
-> ([P2] -> P2 -> IO ()) -> [Purify P2] -> Purify P2
forall a b. (a -> b) -> a -> b
$ \[P2]
ps P2
p ->
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ @[] (P2 -> P2 -> IO ()
`implies` P2
p) [P2]
ps
not :: RDualBool -> RBool
not :: RDualBool -> RBool
not = OpenR (RDualBool -> RBool) -> RDualBool -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RDualBool -> RBool) -> RDualBool -> RBool)
-> OpenR (RDualBool -> RBool) -> RDualBool -> RBool
forall a b. (a -> b) -> a -> b
$ (P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2
forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 ((P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2)
-> (P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2
forall a b. (a -> b) -> a -> b
$ \P2
p1 P2
p -> do
P2 -> P2 -> IO ()
implies P2
p1 P2
p
id :: RBool -> RBool
id :: RBool -> RBool
id = OpenR (RBool -> RBool) -> RBool -> RBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RBool -> RBool) -> RBool -> RBool)
-> OpenR (RBool -> RBool) -> RBool -> RBool
forall a b. (a -> b) -> a -> b
$ (P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2
forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 ((P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2)
-> (P2 -> P2 -> IO ()) -> Purify P2 -> Purify P2
forall a b. (a -> b) -> a -> b
$ \P2
p1 P2
p ->
P2 -> P2 -> IO ()
implies P2
p1 P2
p