P2.hs

{-# 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 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.Exception
import Control.Concurrent.MVar
import Data.IORef

#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 = P2 <$> newMVar (StillBottom (pure()))

-- | A new propagator, already set to top
newTopP2 :: Ctxt M P2_
newTopP2 = P2 <$> newMVar SurelyTop

-- | @whenTop p act@ runs @act@ if @p@ is already top, or after @setTop p@ is run
whenTop :: Ctxt P2_ -> M () -> M ()
whenTop (P2 p1) act = takeMVar p1 >>= \case
    SurelyTop        -> putMVar p1 SurelyTop >> act
    SurelyBottom     -> putMVar p1 SurelyBottom
    StillBottom act' -> putMVar p1 (StillBottom (act >> 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 p) = takeMVar p >>= \case
    SurelyTop -> putMVar p SurelyTop
    SurelyBottom -> throw WriteToFrozenPropagatorException
    StillBottom act -> do
        -- Do this first, this breaks cycles
        putMVar p SurelyTop
        -- Now notify the dependencies
        act

-- | @p1 `implies` p2@ chains propagators: If @p1@ becomes top, then so does @p2@.
implies :: Ctxt P2_ -> P2_ -> M ()
implies p1 p2 = whenTop p1 (setTop 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 p) = readMVar p >>= \case
    SurelyTop -> pure True
    SurelyBottom -> pure False
    StillBottom _ -> pure False

-- | Freezes the value. Drops references to watchers.
freeze :: Ctxt P2_ -> M ()
freeze (P2 p) = takeMVar p >>= \case
    SurelyTop -> putMVar p SurelyTop
    _  -> putMVar p SurelyBottom

#ifndef DEJAFU
instance Propagator P2_ Bool where
    newProp = newP2
    newConstProp False = newP2
    newConstProp True = newTopP2
    freezeProp = freeze
    readProp = isTop
#endif