{-# LANGUAGE TypeApplications #-}

{- | The type @RDualBool@ is like 'Bool', but allows recursive definitions:

>>> :{
  let x = RDB.true
      y = x RDB.&& z
      z = y RDB.|| RDB.false
  in RDB.get x
:}
True


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

>>> :{
  let x = x RDB.&& y
      y = y RDB.&& x
  in (RDB.get x, RDB.get y)
:}
(True,True)

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

-}
module Data.Recursive.DualBool (RDualBool, module Data.Recursive.DualBool) where

import Data.Recursive.Internal
import qualified Data.Propagator.Purify as Purify
import Data.Propagator.P2

-- $setup
-- >>> :load Data.Recursive.Bool Data.Recursive.DualBool
-- >>> :module - Data.Recursive.Bool Data.Recursive.DualBool
--
-- >>> :set -XFlexibleInstances
-- >>> import Test.QuickCheck
-- >>> import qualified Data.Recursive.Bool as RB
-- >>> instance Arbitrary RB.RBool where arbitrary = RB.mk <$> arbitrary
-- >>> instance Show RB.RBool where show = show . RB.get
--
-- >>> import qualified Data.Recursive.DualBool as RDB
-- >>> instance Arbitrary RDB.RDualBool where arbitrary = RDB.mk <$> arbitrary
-- >>> instance Show RDB.RDualBool where show = show . RDB.get

-- | Extracts the value of a 'RDualBool'
get :: RDualBool -> Bool
get :: RDualBool -> Bool
get (RDualBool Purify P2
p) = Bool -> Bool
Prelude.not (Purify P2 -> Bool
forall pa a. Propagator pa a => Purify pa -> a
Purify.get Purify P2
p)

-- | prop> RDB.get (RDB.mk b) === b
mk :: Bool -> RDualBool
mk :: Bool -> RDualBool
mk Bool
b = OpenR RDualBool -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR RDualBool -> RDualBool) -> OpenR RDualBool -> RDualBool
forall a b. (a -> b) -> a -> b
$ Bool -> Purify P2
forall p a. Propagator p a => a -> Purify p
Purify.mk (Bool -> Bool
Prelude.not Bool
b)

-- | prop> RDB.get RDB.true == True
true :: RDualBool
true :: RDualBool
true = OpenR RDualBool -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR RDualBool -> RDualBool) -> OpenR RDualBool -> RDualBool
forall a b. (a -> b) -> a -> b
$ Bool -> Purify P2
forall p a. Propagator p a => a -> Purify p
Purify.mk Bool
False

-- | prop> RDB.get RDB.false == False
false :: RDualBool
false :: RDualBool
false = OpenR RDualBool -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR RDualBool -> RDualBool) -> OpenR RDualBool -> RDualBool
forall a b. (a -> b) -> a -> b
$ Bool -> Purify P2
forall p a. Propagator p a => a -> Purify p
Purify.mk Bool
True

-- | prop> RDB.get (r1 RDB.&& r2) === (RDB.get r1 && RDB.get r2)
(&&) :: RDualBool -> RDualBool -> RDualBool
&& :: RDualBool -> RDualBool -> RDualBool
(&&) = OpenR (RDualBool -> RDualBool -> RDualBool)
-> RDualBool -> RDualBool -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RDualBool -> RDualBool -> RDualBool)
 -> RDualBool -> RDualBool -> RDualBool)
-> OpenR (RDualBool -> RDualBool -> RDualBool)
-> RDualBool
-> RDualBool
-> RDualBool
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)

-- | prop> RDB.get (r1 RDB.|| r2) === (RDB.get r1 || RDB.get r2)
(||) :: RDualBool -> RDualBool -> RDualBool
|| :: RDualBool -> RDualBool -> RDualBool
(||) = OpenR (RDualBool -> RDualBool -> RDualBool)
-> RDualBool -> RDualBool -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RDualBool -> RDualBool -> RDualBool)
 -> RDualBool -> RDualBool -> RDualBool)
-> OpenR (RDualBool -> RDualBool -> RDualBool)
-> RDualBool
-> RDualBool
-> RDualBool
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))

-- | prop> RDB.get (RDB.and rs) === and (map RDB.get rs)
and :: [RDualBool] -> RDualBool
and :: [RDualBool] -> RDualBool
and = OpenR ([RDualBool] -> RDualBool) -> [RDualBool] -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR ([RDualBool] -> RDualBool) -> [RDualBool] -> RDualBool)
-> OpenR ([RDualBool] -> RDualBool) -> [RDualBool] -> RDualBool
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

-- | prop> RDB.get (RDB.or rs) === or (map RDB.get rs)
or :: [RDualBool] -> RDualBool
or :: [RDualBool] -> RDualBool
or = OpenR ([RDualBool] -> RDualBool) -> [RDualBool] -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR ([RDualBool] -> RDualBool) -> [RDualBool] -> RDualBool)
-> OpenR ([RDualBool] -> RDualBool) -> [RDualBool] -> RDualBool
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 ()
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> RDB.get (RDB.not r1) === not (RB.get r1)
not :: RBool -> RDualBool
not :: RBool -> RDualBool
not = OpenR (RBool -> RDualBool) -> RBool -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RBool -> RDualBool) -> RBool -> RDualBool)
-> OpenR (RBool -> RDualBool) -> RBool -> RDualBool
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

-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:
--
-- > let x = x in RDB.get x
--
-- will not work, but
--
-- >>> let x = RDB.id x in RDB.get x
-- True
--
-- does.
--
-- | prop> RDB.get (RDB.id r) === RDB.get r
id :: RDualBool -> RDualBool
id :: RDualBool -> RDualBool
id = OpenR (RDualBool -> RDualBool) -> RDualBool -> RDualBool
forall a. Coercible a (OpenR a) => OpenR a -> a
openR (OpenR (RDualBool -> RDualBool) -> RDualBool -> RDualBool)
-> OpenR (RDualBool -> RDualBool) -> RDualBool -> RDualBool
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