{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE CPP #-}

{-|
Module      : Control.Monad.Watson
Description : A much purer soul than Holmes.
Copyright   : (c) Tom Harding, 2020
License     : MIT

Watson works in a near-identical way to Holmes, but with one distinction: its
base type is 'ST' rather than 'IO', so the API calculates the results with
"observably pure" functions. There are downsides: for example, 'Watson' can't
perform random restart with operations like 'Control.Monad.Holmes.shuffle'.
However, this is often an acceptable compromise to avoid 'IO' entirely!
-}
module Control.Monad.Watson
  ( Watson
  , MonadCell (..)

  , backward
  , forward
  , runAll
  , runOne
  , satisfying
  , unsafeRead
  , whenever
  ) where

#if __GLASGOW_HASKELL__ == 806
import Control.Monad.Fail (MonadFail, fail)
#endif
import Control.Monad.ST (ST, runST)
import Control.Monad.Cell.Class (MonadCell (..))
import qualified Control.Monad.Cell.Class as Cell
import Control.Monad.MoriarT (MoriarT (..))
import qualified Control.Monad.MoriarT as MoriarT
import Data.Coerce (coerce)
import Data.Input.Config (Config (..))
import Data.JoinSemilattice.Class.Eq (EqR (..))
import Data.JoinSemilattice.Class.Merge (Merge)
import Data.Kind (Type)
import Data.Propagator (Prop)
import qualified Data.Propagator as Prop
import Type.Reflection (Typeable)

-- | A monad capable of solving constraint problems using 'ST' as the
-- evaluation type. Cells are represented using 'Data.STRef.STRef' references,
-- and __provenance__ is tracked to optimise backtracking search across
-- multiple branches.
newtype Watson (h :: Type) (x :: Type)
  = Watson { Watson h x -> MoriarT (ST h) x
runWatson :: MoriarT (ST h) x }
  deriving (a -> Watson h b -> Watson h a
(a -> b) -> Watson h a -> Watson h b
(forall a b. (a -> b) -> Watson h a -> Watson h b)
-> (forall a b. a -> Watson h b -> Watson h a)
-> Functor (Watson h)
forall a b. a -> Watson h b -> Watson h a
forall a b. (a -> b) -> Watson h a -> Watson h b
forall h a b. a -> Watson h b -> Watson h a
forall h a b. (a -> b) -> Watson h a -> Watson h b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Watson h b -> Watson h a
$c<$ :: forall h a b. a -> Watson h b -> Watson h a
fmap :: (a -> b) -> Watson h a -> Watson h b
$cfmap :: forall h a b. (a -> b) -> Watson h a -> Watson h b
Functor, Functor (Watson h)
a -> Watson h a
Functor (Watson h)
-> (forall a. a -> Watson h a)
-> (forall a b. Watson h (a -> b) -> Watson h a -> Watson h b)
-> (forall a b c.
    (a -> b -> c) -> Watson h a -> Watson h b -> Watson h c)
-> (forall a b. Watson h a -> Watson h b -> Watson h b)
-> (forall a b. Watson h a -> Watson h b -> Watson h a)
-> Applicative (Watson h)
Watson h a -> Watson h b -> Watson h b
Watson h a -> Watson h b -> Watson h a
Watson h (a -> b) -> Watson h a -> Watson h b
(a -> b -> c) -> Watson h a -> Watson h b -> Watson h c
forall h. Functor (Watson h)
forall a. a -> Watson h a
forall h a. a -> Watson h a
forall a b. Watson h a -> Watson h b -> Watson h a
forall a b. Watson h a -> Watson h b -> Watson h b
forall a b. Watson h (a -> b) -> Watson h a -> Watson h b
forall h a b. Watson h a -> Watson h b -> Watson h a
forall h a b. Watson h a -> Watson h b -> Watson h b
forall h a b. Watson h (a -> b) -> Watson h a -> Watson h b
forall a b c.
(a -> b -> c) -> Watson h a -> Watson h b -> Watson h c
forall h a b c.
(a -> b -> c) -> Watson h a -> Watson h b -> Watson h c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Watson h a -> Watson h b -> Watson h a
$c<* :: forall h a b. Watson h a -> Watson h b -> Watson h a
*> :: Watson h a -> Watson h b -> Watson h b
$c*> :: forall h a b. Watson h a -> Watson h b -> Watson h b
liftA2 :: (a -> b -> c) -> Watson h a -> Watson h b -> Watson h c
$cliftA2 :: forall h a b c.
(a -> b -> c) -> Watson h a -> Watson h b -> Watson h c
<*> :: Watson h (a -> b) -> Watson h a -> Watson h b
$c<*> :: forall h a b. Watson h (a -> b) -> Watson h a -> Watson h b
pure :: a -> Watson h a
$cpure :: forall h a. a -> Watson h a
$cp1Applicative :: forall h. Functor (Watson h)
Applicative, Applicative (Watson h)
a -> Watson h a
Applicative (Watson h)
-> (forall a b. Watson h a -> (a -> Watson h b) -> Watson h b)
-> (forall a b. Watson h a -> Watson h b -> Watson h b)
-> (forall a. a -> Watson h a)
-> Monad (Watson h)
Watson h a -> (a -> Watson h b) -> Watson h b
Watson h a -> Watson h b -> Watson h b
forall h. Applicative (Watson h)
forall a. a -> Watson h a
forall h a. a -> Watson h a
forall a b. Watson h a -> Watson h b -> Watson h b
forall a b. Watson h a -> (a -> Watson h b) -> Watson h b
forall h a b. Watson h a -> Watson h b -> Watson h b
forall h a b. Watson h a -> (a -> Watson h b) -> Watson h b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Watson h a
$creturn :: forall h a. a -> Watson h a
>> :: Watson h a -> Watson h b -> Watson h b
$c>> :: forall h a b. Watson h a -> Watson h b -> Watson h b
>>= :: Watson h a -> (a -> Watson h b) -> Watson h b
$c>>= :: forall h a b. Watson h a -> (a -> Watson h b) -> Watson h b
$cp1Monad :: forall h. Applicative (Watson h)
Monad)

instance MonadFail (Watson h) where
  fail :: String -> Watson h a
fail String
_ = Watson h a
forall (m :: * -> *) x. MonadCell m => m x
discard

instance MonadCell (Watson h) where
  newtype Cell (Watson h) x = Cell { Cell (Watson h) x -> Cell (MoriarT (ST h)) x
unwrap :: Cell (MoriarT (ST h)) x }

  discard :: Watson h x
discard = MoriarT (ST h) x -> Watson h x
coerce (forall x. MonadCell (MoriarT (ST h)) => MoriarT (ST h) x
forall (m :: * -> *) x. MonadCell m => m x
discard @(MoriarT (ST h)))
  fill :: x -> Watson h (Cell (Watson h) x)
fill = (Cell (MoriarT (ST h)) x -> Cell (Watson h) x)
-> Watson h (Cell (MoriarT (ST h)) x)
-> Watson h (Cell (Watson h) x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cell (MoriarT (ST h)) x -> Cell (Watson h) x
forall h x. Cell (MoriarT (ST h)) x -> Cell (Watson h) x
Cell (Watson h (Cell (MoriarT (ST h)) x)
 -> Watson h (Cell (Watson h) x))
-> (x -> Watson h (Cell (MoriarT (ST h)) x))
-> x
-> Watson h (Cell (Watson h) x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (x -> MoriarT (ST h) (Cell (MoriarT (ST h)) x))
-> x -> Watson h (Cell (MoriarT (ST h)) x)
coerce (forall x.
MonadCell (MoriarT (ST h)) =>
x -> MoriarT (ST h) (Cell (MoriarT (ST h)) x)
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
fill @(MoriarT (ST h)))

  watch :: Cell (Watson h) x -> (x -> Watson h ()) -> Watson h ()
watch (Cell cell) = ((x -> MoriarT (ST h) ()) -> MoriarT (ST h) ())
-> (x -> Watson h ()) -> Watson h ()
coerce (Cell (MoriarT (ST h)) x
-> (x -> MoriarT (ST h) ()) -> MoriarT (ST h) ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
watch @(MoriarT (ST h)) Cell (MoriarT (ST h)) x
cell)
  with :: Cell (Watson h) x -> (x -> Watson h ()) -> Watson h ()
with  (Cell cell) = ((x -> MoriarT (ST h) ()) -> MoriarT (ST h) ())
-> (x -> Watson h ()) -> Watson h ()
coerce (Cell (MoriarT (ST h)) x
-> (x -> MoriarT (ST h) ()) -> MoriarT (ST h) ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
with  @(MoriarT (ST h)) Cell (MoriarT (ST h)) x
cell)
  write :: Cell (Watson h) x -> x -> Watson h ()
write (Cell cell) = (x -> MoriarT (ST h) ()) -> x -> Watson h ()
coerce (Cell (MoriarT (ST h)) x -> x -> MoriarT (ST h) ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
write @(MoriarT (ST h)) Cell (MoriarT (ST h)) x
cell)

-- | Unsafely read from a cell. This operation is unsafe because it doesn't
-- factor this cell into the provenance of any subsequent writes. If this value
-- ends up causing a contradiction, we may end up removing branches of the
-- search tree that are totally valid! This operation is safe as long as it is
-- the __very last thing__ you do in a computation, and its value is __never__
-- used to influence any writes in any way.
unsafeRead :: Cell (Watson h) x -> Watson h x
unsafeRead :: Cell (Watson h) x -> Watson h x
unsafeRead = MoriarT (ST h) x -> Watson h x
coerce (MoriarT (ST h) x -> Watson h x)
-> (Cell (Watson h) x -> MoriarT (ST h) x)
-> Cell (Watson h) x
-> Watson h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cell (MoriarT (ST h)) x -> MoriarT (ST h) x
forall (m :: * -> *) x.
PrimMonad m =>
Cell (MoriarT m) x -> MoriarT m x
MoriarT.unsafeRead (Cell (MoriarT (ST h)) x -> MoriarT (ST h) x)
-> (Cell (Watson h) x -> Cell (MoriarT (ST h)) x)
-> Cell (Watson h) x
-> MoriarT (ST h) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cell (Watson h) x -> Cell (MoriarT (ST h)) x
forall h x. Cell (Watson h) x -> Cell (MoriarT (ST h)) x
unwrap

-- | Run a function between propagators "backwards", writing the given value as
-- the output and then trying to push information backwards to the input cell.
backward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> y -> Maybe x
backward :: (forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y)
-> y -> Maybe x
backward forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f y
y = (forall s. ST s (Maybe x)) -> Maybe x
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Maybe x)) -> Maybe x)
-> (forall s. ST s (Maybe x)) -> Maybe x
forall a b. (a -> b) -> a -> b
$ MoriarT (ST s) x -> ST s (Maybe x)
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne (MoriarT (ST s) x -> ST s (Maybe x))
-> MoriarT (ST s) x -> ST s (Maybe x)
forall a b. (a -> b) -> a -> b
$ Watson s x -> MoriarT (ST s) x
forall h x. Watson h x -> MoriarT (ST h) x
runWatson do
  Cell (Watson s) x
input  <- Watson s (Cell (Watson s) x)
forall (m :: * -> *) x. (MonadCell m, Monoid x) => m (Cell m x)
Cell.make
  Cell (Watson s) y
output <- Prop (Watson s) y -> Watson s (Cell (Watson s) y)
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
Prop.down (Prop (Watson s) x -> Prop (Watson s) y
forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f (Cell (Watson s) x -> Prop (Watson s) x
forall (m :: * -> *) x. Applicative m => Cell m x -> Prop m x
Prop.up Cell (Watson s) x
input))

  Cell (Watson s) y -> y -> Watson s ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
Cell.write Cell (Watson s) y
output y
y
  Cell (Watson s) x -> Watson s x
forall h x. Cell (Watson h) x -> Watson h x
unsafeRead Cell (Watson s) x
input

-- | Run a function between propagators with a raw value, writing the given
-- value to the "input" cell and reading the result from the "output" cell.
forward :: (Typeable x, Merge x, Merge y) => (forall m. MonadCell m => Prop m x -> Prop m y) -> x -> Maybe y
forward :: (forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y)
-> x -> Maybe y
forward forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f x
x = (forall s. ST s (Maybe y)) -> Maybe y
forall a. (forall s. ST s a) -> a
runST ((forall s. ST s (Maybe y)) -> Maybe y)
-> (forall s. ST s (Maybe y)) -> Maybe y
forall a b. (a -> b) -> a -> b
$ MoriarT (ST s) y -> ST s (Maybe y)
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne (MoriarT (ST s) y -> ST s (Maybe y))
-> MoriarT (ST s) y -> ST s (Maybe y)
forall a b. (a -> b) -> a -> b
$ Watson s y -> MoriarT (ST s) y
forall h x. Watson h x -> MoriarT (ST h) x
runWatson do
  Cell (Watson s) x
input  <- Watson s (Cell (Watson s) x)
forall (m :: * -> *) x. (MonadCell m, Monoid x) => m (Cell m x)
Cell.make
  Cell (Watson s) y
output <- Prop (Watson s) y -> Watson s (Cell (Watson s) y)
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
Prop.down (Prop (Watson s) x -> Prop (Watson s) y
forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f (Cell (Watson s) x -> Prop (Watson s) x
forall (m :: * -> *) x. Applicative m => Cell m x -> Prop m x
Prop.up Cell (Watson s) x
input))

  Cell (Watson s) x -> x -> Watson s ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
Cell.write Cell (Watson s) x
input x
x
  Cell (Watson s) y -> Watson s y
forall h x. Cell (Watson h) x -> Watson h x
unsafeRead Cell (Watson s) y
output

-- | Interpret a 'Watson' program, returning a list of all successful branches'
-- outputs. It's unlikely that you want to call this directly, though;
-- typically, 'satisfying' or 'whenever' are more likely the things you want.
runAll :: (forall h. Watson h x) -> [ x ]
runAll :: (forall h. Watson h x) -> [x]
runAll forall h. Watson h x
xs = (forall s. ST s [x]) -> [x]
forall a. (forall s. ST s a) -> a
runST (MoriarT (ST s) x -> ST s [x]
forall (m :: * -> *) x. Monad m => MoriarT m x -> m [x]
MoriarT.runAll (Watson s x -> MoriarT (ST s) x
forall h x. Watson h x -> MoriarT (ST h) x
runWatson Watson s x
forall h. Watson h x
xs))

-- | Interpret a 'Watson' program, returning the first successful branch's
-- result /if/ any branch succeeds. It's unlikely that you want to call this
-- directly, though; typically, 'satisfying' or 'whenever' are more likely the
-- things you want.
runOne :: (forall h. Watson h x) -> Maybe x
runOne :: (forall h. Watson h x) -> Maybe x
runOne forall h. Watson h x
xs = (forall s. ST s (Maybe x)) -> Maybe x
forall a. (forall s. ST s a) -> a
runST (MoriarT (ST s) x -> ST s (Maybe x)
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne (Watson s x -> MoriarT (ST s) x
forall h x. Watson h x -> MoriarT (ST h) x
runWatson Watson s x
forall h. Watson h x
xs))

-- | Given an input configuration, and a predicate on those input variables,
-- return the __first__ configuration that satisfies the predicate.
satisfying
  :: ( EqC f x
     , EqR f
     , Typeable x
     )
  => (forall h. Config (Watson h) (f x))
  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
  -> Maybe [ f x ]
satisfying :: (forall h. Config (Watson h) (f x))
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> Maybe [f x]
satisfying forall h. Config (Watson h) (f x)
config forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f
  = (forall s. ST s (Maybe [f x])) -> Maybe [f x]
forall a. (forall s. ST s a) -> a
runST (MoriarT (ST s) [f x] -> ST s (Maybe [f x])
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne (Config (MoriarT (ST s)) (f x)
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> MoriarT (ST s) [f x]
forall (m :: * -> *) (f :: * -> *) x.
(PrimMonad m, EqR f, Merge (f x), Typeable x) =>
Config (MoriarT m) (f x)
-> (forall (m' :: * -> *).
    MonadCell m' =>
    [Prop m' (f x)] -> Prop m' (f Bool))
-> MoriarT m [f x]
MoriarT.solve (Config (Watson s) (f x) -> Config (MoriarT (ST s)) (f x)
coerce Config (Watson s) (f x)
forall h. Config (Watson h) (f x)
config) forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f))

-- | Given an input configuration, and a predicate on those input variables,
-- return __all configurations__ that satisfy the predicate. It should be noted
-- that there's nothing lazy about this; if your problem has a lot of
-- solutions, or your search space is very big, you'll be waiting a long time!
whenever
  :: ( EqC f x
     , EqR f
     , Typeable x
     )
  => (forall h. Config (Watson h) (f x))
  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
  -> [[ f x ]]
whenever :: (forall h. Config (Watson h) (f x))
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> [[f x]]
whenever forall h. Config (Watson h) (f x)
config forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f
  = (forall s. ST s [[f x]]) -> [[f x]]
forall a. (forall s. ST s a) -> a
runST (MoriarT (ST s) [f x] -> ST s [[f x]]
forall (m :: * -> *) x. Monad m => MoriarT m x -> m [x]
MoriarT.runAll (Config (MoriarT (ST s)) (f x)
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> MoriarT (ST s) [f x]
forall (m :: * -> *) (f :: * -> *) x.
(PrimMonad m, EqR f, Merge (f x), Typeable x) =>
Config (MoriarT m) (f x)
-> (forall (m' :: * -> *).
    MonadCell m' =>
    [Prop m' (f x)] -> Prop m' (f Bool))
-> MoriarT m [f x]
MoriarT.solve (Config (Watson s) (f x) -> Config (MoriarT (ST s)) (f x)
coerce Config (Watson s) (f x)
forall h. Config (Watson h) (f x)
config) forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f))