{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE CPP #-}

-- | A propagator for the two-point lattice
--
module Data.Recursive.Propagator.P2
    ( P2
    , newP2
    , newTopP2
    , setTop
    , whenTop
    , implies
    , isTop
    , PBool(..)
    , PDualBool(..)
    )
    where

-- I want to test this code with dejafu, without carrying it as a dependency
-- of the main library. So here is a bit of CPP to care for that.

#ifdef DEJAFU

#define Ctxt   MonadConc m =>
#define MaybeTop_  (MaybeTop m)
#define P2_  (P2 m)
#define PBool_  PBool m
#define PDualBool_  PDualBool m
#define IORef_ IORef m
#define MVar_  MVar m
#define M      m

import Control.Concurrent.Classy

#else

#define Ctxt
#define MaybeTop_  MaybeTop
#define P2_  P2
#define PBool_  PBool
#define PDualBool_  PDualBool
#define IORef_ IORef
#define MVar_  MVar
#define M      IO

import Control.Concurrent.MVar
import Data.IORef

#endif

data MaybeTop_
        = StillBottom (M ()) -- ^ Just act: Still bottom, run act (once!) when triggered
        | SurelyTop           -- ^ Definitely top

-- | A type for propagators for the two-point lattice, consisting of bottom and top
newtype P2_ = P2 (MVar_ MaybeTop_)

-- | A new propagator, initialized at bottom
newP2 :: Ctxt M P2_
newP2 :: IO P2
newP2 = MVar MaybeTop -> P2
P2 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> IO (MVar a)
newMVar (IO () -> MaybeTop
StillBottom (forall (f :: * -> *) a. Applicative f => a -> f a
pure()))

-- | A new propagator, already set to top
newTopP2 :: Ctxt M P2_
newTopP2 :: IO P2
newTopP2 = MVar MaybeTop -> P2
P2 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> IO (MVar a)
newMVar MaybeTop
SurelyTop

-- | @whenTop p act@ runs @act@ if @p@ is already top, or after @setTop p@ is run
whenTop :: Ctxt P2_ -> M () -> M ()
whenTop :: P2 -> IO () -> IO ()
whenTop (P2 MVar MaybeTop
p1) IO ()
act = forall a. MVar a -> IO a
takeMVar MVar MaybeTop
p1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MaybeTop
SurelyTop        -> forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p1 MaybeTop
SurelyTop forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
act
    StillBottom IO ()
act' -> forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p1 (IO () -> MaybeTop
StillBottom (IO ()
act forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
act'))


-- | Set a propagator to top.
--
-- If it was bottom before, runs the actions queued with 'whenTop'. It does so
-- _after_ setting the propagator to top, so that cycles are broken.
setTop :: Ctxt P2_ -> M ()
setTop :: P2 -> IO ()
setTop (P2 MVar MaybeTop
p) = forall a. MVar a -> IO a
takeMVar MVar MaybeTop
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MaybeTop
SurelyTop -> forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p MaybeTop
SurelyTop
    StillBottom IO ()
act -> do
        -- Do this first, this breaks cycles
        forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p MaybeTop
SurelyTop
        -- Now notify the dependencies
        IO ()
act

-- | @p1 `implies` p2@ chains propagators: If @p1@ becomes top, then so does @p2@.
implies :: Ctxt P2_ -> P2_ -> M ()
implies :: P2 -> P2 -> IO ()
implies P2
p1 P2
p2 = P2 -> IO () -> IO ()
whenTop P2
p1 (P2 -> IO ()
setTop P2
p2)

-- | Queries the current state of the propagator. All related calls to @setTop@
-- that have executed so far are taken into account.
isTop :: Ctxt P2_ -> M Bool
isTop :: P2 -> IO Bool
isTop (P2 MVar MaybeTop
p) = forall a. MVar a -> IO a
readMVar MVar MaybeTop
p forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MaybeTop
SurelyTop -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    StillBottom IO ()
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

-- | A newtype around 'P2' to denote that bottom is 'False' and top is 'True'
newtype PBool_ = PBool P2_

-- | A newtype around 'P2' to denote that bottom is 'True' and top is 'False'
newtype PDualBool_ = PDualBool P2_