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

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

import Data.Propagator.Class

-- 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 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 MVar_  MVar
#define M      IO

import Control.Exception
import Control.Concurrent.MVar

#endif

data MaybeTop_
        = StillBottom (M ()) -- ^ Just act: Still bottom, run act (once!) when triggered
        | SurelyBottom       -- ^ Definitely bottom 
        | 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 (MVar MaybeTop -> P2) -> IO (MVar MaybeTop) -> IO P2
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeTop -> IO (MVar MaybeTop)
forall a. a -> IO (MVar a)
newMVar (IO () -> MaybeTop
StillBottom (() -> IO ()
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 (MVar MaybeTop -> P2) -> IO (MVar MaybeTop) -> IO P2
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeTop -> IO (MVar MaybeTop)
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 = MVar MaybeTop -> IO MaybeTop
forall a. MVar a -> IO a
takeMVar MVar MaybeTop
p1 IO MaybeTop -> (MaybeTop -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MaybeTop
SurelyTop        -> MVar MaybeTop -> MaybeTop -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p1 MaybeTop
SurelyTop IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
act
    MaybeTop
SurelyBottom     -> MVar MaybeTop -> MaybeTop -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p1 MaybeTop
SurelyBottom
    StillBottom IO ()
act' -> MVar MaybeTop -> MaybeTop -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p1 (IO () -> MaybeTop
StillBottom (IO ()
act IO () -> IO () -> IO ()
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) = MVar MaybeTop -> IO MaybeTop
forall a. MVar a -> IO a
takeMVar MVar MaybeTop
p IO MaybeTop -> (MaybeTop -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MaybeTop
SurelyTop -> MVar MaybeTop -> MaybeTop -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p MaybeTop
SurelyTop
    MaybeTop
SurelyBottom -> WriteToFrozenPropagatorException -> IO ()
forall a e. Exception e => e -> a
throw WriteToFrozenPropagatorException
WriteToFrozenPropagatorException
    StillBottom IO ()
act -> do
        -- Do this first, this breaks cycles
        MVar MaybeTop -> MaybeTop -> IO ()
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) = MVar MaybeTop -> IO MaybeTop
forall a. MVar a -> IO a
readMVar MVar MaybeTop
p IO MaybeTop -> (MaybeTop -> IO Bool) -> IO Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MaybeTop
SurelyTop -> Bool -> IO Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
    MaybeTop
SurelyBottom -> Bool -> IO Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
    StillBottom IO ()
_ -> Bool -> IO Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False

#ifndef DEJAFU

-- | Freezes the value. Drops references to watchers.
freeze :: Ctxt P2_ -> M ()
freeze :: P2 -> IO ()
freeze (P2 MVar MaybeTop
p) = MVar MaybeTop -> IO MaybeTop
forall a. MVar a -> IO a
takeMVar MVar MaybeTop
p IO MaybeTop -> (MaybeTop -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    MaybeTop
SurelyTop -> MVar MaybeTop -> MaybeTop -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p MaybeTop
SurelyTop
    MaybeTop
_  -> MVar MaybeTop -> MaybeTop -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar MaybeTop
p MaybeTop
SurelyBottom

instance Propagator P2_ Bool where
    newProp :: IO P2
newProp = IO P2
newP2
    newConstProp :: Bool -> IO P2
newConstProp Bool
False = IO P2
newP2
    newConstProp Bool
True = IO P2
newTopP2
    freezeProp :: P2 -> IO ()
freezeProp = P2 -> IO ()
freeze
    readProp :: P2 -> IO Bool
readProp = P2 -> IO Bool
isTop
#endif