```{-# LANGUAGE TypeApplications #-}

{- | The type @R Bool@ is ike 'Bool', but allows recursive definitions:

>>> :{
let x = rTrue
y = x &&& z
z = y ||| rFalse
in getR x
:}
True

This finds the least solution, i.e. prefers 'False' over 'True':

>>> :{
let x = x &&& y
y = y &&& x
in (getR x, getR y)
:}
(False,False)

Use @R (Dual Bool)@ from "Data.Recursive.DualBool" if you want the greatest solution.

-}
module Data.Recursive.Bool
( R
, getR
, module Data.Recursive.Bool
) where

import Data.Coerce
import Data.Monoid

import Data.Recursive.R.Internal
import Data.Recursive.R
import Data.Recursive.Propagator.P2

-- \$setup
-- >>> :set -XFlexibleInstances
-- >>> import Test.QuickCheck
-- >>> instance Arbitrary (R Bool) where arbitrary = mkR <\$> arbitrary
-- >>> instance Show (R Bool) where show = show . getR
-- >>> instance Arbitrary (R (Dual Bool)) where arbitrary = mkR <\$> arbitrary
-- >>> instance Show (R (Dual Bool)) where show = show . getR

-- | prop> getR rTrue == True
rTrue :: R Bool
rTrue :: R Bool
rTrue = forall a. HasPropagator a => a -> R a
mkR Bool
True

-- | prop> getR rFalse == False
rFalse :: R Bool
rFalse :: R Bool
rFalse = forall a. HasPropagator a => a -> R a
mkR Bool
False

{- Using the naive propagator:

(&&&) :: R Bool -> R Bool -> R Bool
(&&&) = defR2 \$ lift2 (&&)

(|||) :: R Bool -> R Bool -> R Bool
(|||) = defR2 \$ lift2 (||)

rand :: [R Bool] -> R Bool
rand = defRList \$ liftList and

ror :: [R Bool] -> R Bool
ror = defRList \$ liftList or

rnot :: R (Dual Bool) -> R Bool
rnot = defR1 \$ lift1 \$ coerce not

-}

-- | prop> getR (r1 &&& r2) === (getR r1 && getR r2)
(&&&) :: R Bool -> R Bool -> R Bool
&&& :: R Bool -> R Bool -> R Bool
(&&&) = forall a b c.
(HasPropagator a, HasPropagator b, HasPropagator c) =>
(Prop a -> Prop b -> Prop c -> IO ()) -> R a -> R b -> R c
defR2 forall a b. (a -> b) -> a -> b
\$ coerce :: forall a b. Coercible a b => a -> b
coerce 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))

-- | prop> getR (r1 ||| r2) === (getR r1 || getR r2)
(|||) :: R Bool -> R Bool -> R Bool
||| :: R Bool -> R Bool -> R Bool
(|||) = forall a b c.
(HasPropagator a, HasPropagator b, HasPropagator c) =>
(Prop a -> Prop b -> Prop c -> IO ()) -> R a -> R b -> R c
defR2 forall a b. (a -> b) -> a -> b
\$ coerce :: forall a b. Coercible a b => a -> b
coerce 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)

-- | prop> getR (rand rs) === and (map getR rs)
rand :: [R Bool] -> R Bool
rand :: [R Bool] -> R Bool
rand = forall a b.
(HasPropagator a, HasPropagator b) =>
([Prop a] -> Prop b -> IO ()) -> [R a] -> R b
defRList forall a b. (a -> b) -> a -> b
\$ coerce :: forall a b. Coercible a b => a -> b
coerce [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)

-- | prop> getR (ror rs) === or (map getR rs)
ror :: [R Bool] -> R Bool
ror :: [R Bool] -> R Bool
ror = forall a b.
(HasPropagator a, HasPropagator b) =>
([Prop a] -> Prop b -> IO ()) -> [R a] -> R b
defRList forall a b. (a -> b) -> a -> b
\$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
\$ \[P2]
ps P2
p ->
forall (t :: * -> *) (m :: * -> *) a b.
(a -> m b) -> t a -> m ()
mapM_ @[] (P2 -> P2 -> IO ()
`implies` P2
p) [P2]
ps

-- | prop> getR (rnot r1) === not (getRDual r1)
rnot :: R (Dual Bool) -> R Bool
rnot :: R (Dual Bool) -> R Bool
rnot = forall a b.
(HasPropagator a, HasPropagator b) =>
(Prop a -> Prop b -> IO ()) -> R a -> R b
defR1 forall a b. (a -> b) -> a -> b
\$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
\$ \P2
p1 P2
p -> do
P2 -> P2 -> IO ()
implies P2
p1 P2
p
```