{-# LANGUAGE TypeFamilies #-}
{- | The type @RS.RSet a@ is like 'S.Set' @a@, but allows recursive definitions:

>>> :{
  let s1 = RS.insert 23 s2
      s2 = RS.insert 42 s1
  in RS.get s1
 :}
fromList [23,42]

-}
module Data.Recursive.Set (RSet, module Data.Recursive.Set) where

import qualified Data.Set as S
import Control.Monad hiding (when)

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

-- $setup
-- >>> :load Data.Recursive.Set Data.Recursive.Bool Data.Recursive.DualBool
-- >>> :module - Data.Recursive.Set Data.Recursive.Bool Data.Recursive.DualBool
-- >>> import qualified Data.Recursive.Set as RS
-- >>> import qualified Data.Recursive.Bool as RB
-- >>> import qualified Data.Recursive.DualBool as RDB
-- >>> import qualified Data.Set as S
-- >>> :set -XFlexibleInstances
-- >>> :set -XScopedTypeVariables
-- >>> import Test.QuickCheck
-- >>> instance (Ord a, Arbitrary a) => Arbitrary (RS.RSet a) where arbitrary = RS.mk <$> arbitrary
-- >>> instance (Ord a, Show a) => Show (RS.RSet a) where show = show . RS.get
-- >>> instance Arbitrary RB.RBool where arbitrary = RB.mk <$> arbitrary
-- >>> instance Show RB.RBool where show = show . RB.get

-- | Extracts the value of a 'RSet a'
get :: RSet a -> S.Set a
get :: forall a. RSet a -> Set a
get (RSet Purify (Prop (Set a))
p) = forall pa a. Propagator pa a => Purify pa -> a
Purify.get Purify (Prop (Set a))
p

-- | prop> RB.get (RB.mk s) === s
mk :: S.Set a -> RSet a
mk :: forall a. Set a -> RSet a
mk Set a
s = forall a. Purify (Prop (Set a)) -> RSet a
RSet forall a b. (a -> b) -> a -> b
$ forall p a. Propagator p a => a -> Purify p
Purify.mk Set a
s

-- | prop> RS.get RS.empty === S.empty
empty :: RSet a
empty :: forall a. RSet a
empty = forall a. Purify (Prop (Set a)) -> RSet a
RSet forall a b. (a -> b) -> a -> b
$ forall p a. Propagator p a => a -> Purify p
Purify.mk forall a. Set a
S.empty

-- | prop> RS.get (RS.singleton x) === S.singleton x
singleton :: a -> RSet a
singleton :: forall a. a -> RSet a
singleton a
x = forall a. Purify (Prop (Set a)) -> RSet a
RSet forall a b. (a -> b) -> a -> b
$ forall p a. Propagator p a => a -> Purify p
Purify.mk forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
S.singleton a
x

-- | prop> RS.get (RS.insert n r1) === S.insert n (RS.get r1)
insert :: Ord a => a -> RSet a -> RSet a
insert :: forall a. Ord a => a -> RSet a -> RSet a
insert a
x = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 forall a b. (a -> b) -> a -> b
$ forall b a. POrder b => (a -> b) -> Prop a -> Prop b -> IO ()
lift1 forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
S.insert a
x

-- | prop> RS.get (RS.delete n r1) === S.delete n (RS.get r1)
delete :: Ord a => a -> RSet a -> RSet a
delete :: forall a. Ord a => a -> RSet a -> RSet a
delete a
x = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 forall a b. (a -> b) -> a -> b
$ forall b a. POrder b => (a -> b) -> Prop a -> Prop b -> IO ()
lift1 forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
S.delete a
x

-- | prop> \(Fun _ p) -> RS.get (RS.filter p r1) === S.filter p (RS.get r1)
filter :: Ord a => (a -> Bool) -> RSet a -> RSet a
filter :: forall a. Ord a => (a -> Bool) -> RSet a -> RSet a
filter a -> Bool
f = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 forall a b. (a -> b) -> a -> b
$ forall b a. POrder b => (a -> b) -> Prop a -> Prop b -> IO ()
lift1 forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> Set a -> Set a
S.filter a -> Bool
f

-- | prop> RS.get (RS.union r1 r2) === S.union (RS.get r1) (RS.get r2)
union :: Ord a => RSet a -> RSet a -> RSet a
union :: forall a. Ord a => RSet a -> RSet a -> RSet a
union = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall c a b.
POrder c =>
(a -> b -> c) -> Prop a -> Prop b -> Prop c -> IO ()
lift2 forall a. Ord a => Set a -> Set a -> Set a
S.union

-- | prop> RS.get (RS.unions rs) === S.unions (map RS.get rs)
unions :: Ord a => [RSet a] -> RSet a
unions :: forall a. Ord a => [RSet a] -> RSet a
unions = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
([pa] -> pb -> IO ()) -> [Purify pa] -> Purify pb
Purify.defList forall a b. (a -> b) -> a -> b
$ forall b a. POrder b => ([a] -> b) -> [Prop a] -> Prop b -> IO ()
liftList forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions

-- | prop> RS.get (RS.intersection r1 r2) === S.intersection (RS.get r1) (RS.get r2)
intersection :: Ord a => RSet a -> RSet a -> RSet a
intersection :: forall a. Ord a => RSet a -> RSet a -> RSet a
intersection = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ forall c a b.
POrder c =>
(a -> b -> c) -> Prop a -> Prop b -> Prop c -> IO ()
lift2 forall a. Ord a => Set a -> Set a -> Set a
S.intersection

-- | prop> RB.get (RS.member n r1) === S.member n (RS.get r1)
member :: Ord a => a -> RSet a -> RBool
member :: forall a. Ord a => a -> RSet a -> RBool
member a
x = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 forall a b. (a -> b) -> a -> b
$ \Prop (Set a)
ps P2
pb -> do
    let update :: IO ()
update = do
            Set a
s <- forall a. Prop a -> IO a
readProp Prop (Set a)
ps
            if forall a. Ord a => a -> Set a -> Bool
S.member a
x Set a
s then P2 -> IO ()
setTop P2
pb else forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    forall a. Prop a -> IO () -> IO ()
watchProp Prop (Set a)
ps IO ()
update
    IO ()
update

-- | prop> RDB.get (RS.notMember n r1) === S.notMember n (RS.get r1)
notMember :: Ord a => a -> RSet a -> RDualBool
notMember :: forall a. Ord a => a -> RSet a -> RDualBool
notMember a
x = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 forall a b. (a -> b) -> a -> b
$ \Prop (Set a)
ps P2
pb -> do
    let update :: IO ()
update = do
            Set a
s <- forall a. Prop a -> IO a
readProp Prop (Set a)
ps
            if forall a. Ord a => a -> Set a -> Bool
S.member a
x Set a
s then P2 -> IO ()
setTop P2
pb else forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    forall a. Prop a -> IO () -> IO ()
watchProp Prop (Set a)
ps IO ()
update
    IO ()
update

-- | prop> RDB.get (RS.null s) === S.null (RS.get s)
null :: RSet a -> RDualBool
null :: forall a. RSet a -> RDualBool
null = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 forall a b. (a -> b) -> a -> b
$ \Prop (Set a)
ps P2
pb -> do
    let update :: IO ()
update = do
            Set a
s <- forall a. Prop a -> IO a
readProp Prop (Set a)
ps
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Set a -> Bool
S.null Set a
s) forall a b. (a -> b) -> a -> b
$ P2 -> IO ()
setTop P2
pb
    forall a. Prop a -> IO () -> IO ()
watchProp Prop (Set a)
ps IO ()
update
    IO ()
update

-- | prop> RDB.get (RS.disjoint r1 r2) === S.disjoint (RS.get r1) (RS.get r2)
disjoint :: Ord a => RSet a -> RSet a -> RDualBool
disjoint :: forall a. Ord a => RSet a -> RSet a -> RDualBool
disjoint = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \Prop (Set a)
ps1 Prop (Set a)
ps2 P2
pb -> do
    let update :: IO ()
update = do
            Set a
s1 <- forall a. Prop a -> IO a
readProp Prop (Set a)
ps1
            Set a
s2 <- forall a. Prop a -> IO a
readProp Prop (Set a)
ps2
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => Set a -> Set a -> Bool
S.disjoint Set a
s1 Set a
s2) forall a b. (a -> b) -> a -> b
$ P2 -> IO ()
setTop P2
pb
    forall a. Prop a -> IO () -> IO ()
watchProp Prop (Set a)
ps1 IO ()
update
    forall a. Prop a -> IO () -> IO ()
watchProp Prop (Set a)
ps2 IO ()
update
    IO ()
update

-- | An kind of if-then-else statement. Because of monotonicity requirements,
-- this should be sufficient.
--
-- prop> RS.get (RS.when b r) === (if RB.get b then RS.get r else S.empty)
when :: RBool -> RSet a -> RSet a
when :: forall a. RBool -> RSet a -> RSet a
when = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ \P2
pb Prop (Set a)
ps1 Prop (Set a)
ps2 -> do
    P2 -> IO () -> IO ()
whenTop P2
pb forall a b. (a -> b) -> a -> b
$ forall b a. POrder b => (a -> b) -> Prop a -> Prop b -> IO ()
lift1 forall a. a -> a
Prelude.id Prop (Set a)
ps1 Prop (Set a)
ps2

-- | The identity function. This is useful when tying the knot, to avoid a loop that bottoms out:
--
-- > let x = x in RS.get x
--
-- will not work, but
--
-- >>> let x = RS.id x in RS.get x
-- fromList []
--
-- does.
--
-- | prop> RS.get (RS.id s) === RS.get s
id :: RSet a -> RSet a
id :: forall a. RSet a -> RSet a
id = forall a. Coercible a (OpenR a) => OpenR a -> a
openR forall a b. (a -> b) -> a -> b
$ forall pa a pb b.
(Propagator pa a, Propagator pb b) =>
(pa -> pb -> IO ()) -> Purify pa -> Purify pb
Purify.def1 forall a b. (a -> b) -> a -> b
$ forall b a. POrder b => (a -> b) -> Prop a -> Prop b -> IO ()
lift1 forall a. a -> a
Prelude.id