{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}

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

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


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

>>> :{
  let x = x &&& y
      y = y &&& x
  in (getRDual x, getRDual y)
:}
(True,True)

Use @R Bool@ from "Data.Recursive.Bool" if you want the least solution.

-}
module Data.Recursive.DualBool
  ( R
  , getRDual
  , module Data.Recursive.DualBool
  ) 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> getRDual rTrue == True
rTrue :: R (Dual Bool)
rTrue :: R (Dual Bool)
rTrue = forall a. HasPropagator a => a -> R a
mkR (forall a. a -> Dual a
Dual Bool
True)

-- | prop> getRDual rFalse == False
rFalse :: R (Dual Bool)
rFalse :: R (Dual Bool)
rFalse = forall a. HasPropagator a => a -> R a
mkR (forall a. a -> Dual a
Dual Bool
False)

-- | prop> getRDual (r1 ||| r2) === (getRDual r1 || getRDual r2)
(|||) :: R (Dual Bool) -> R (Dual Bool) -> R (Dual Bool)
||| :: R (Dual Bool) -> R (Dual Bool) -> R (Dual 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> getRDual (r1 &&& r2) === (getRDual r1 && getRDual r2)
(&&&) :: R (Dual Bool) -> R (Dual Bool) -> R (Dual Bool)
&&& :: R (Dual Bool) -> R (Dual Bool) -> R (Dual 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> getRDual (ror rs) === or (map getRDual rs)
ror :: [R (Dual Bool)] -> R (Dual Bool)
ror :: [R (Dual Bool)] -> R (Dual 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 [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> getRDual (rand rs) === and (map getRDual rs)
rand :: [R (Dual Bool)] -> R (Dual Bool)
rand :: [R (Dual Bool)] -> R (Dual 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 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> getRDual (rnot r1) === not (getR r1)
rnot :: R Bool -> R (Dual Bool)
rnot :: R Bool -> R (Dual 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