{-# 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.
(Foldable t, Monad m) =>
(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