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

{-|
Module      : Control.Monad.Holmes
Description : A monad for constructing constraint-solving computations, and executing them inside 'IO'.
Copyright   : (c) Tom Harding, 2020
License     : MIT

'Holmes' is a type for solving constraint problems. These computations are
executed with 'IO', which allows for extra features such as the ability to
'shuffle' the input configuration.

If this isn't a feature you require, you may prefer to use the
"Control.Monad.Watson" interface, which offers a pure version of the API thanks
to its use of 'Control.Monad.ST'. The internal code is shared between the two,
so results between the two are consistent.
-}
module Control.Monad.Holmes
  ( Holmes
  , MonadCell

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

#if __GLASGOW_HASKELL__ == 806
import Control.Monad.Fail (MonadFail, fail)
#endif
import Control.Monad.Cell.Class (MonadCell (..))
import Control.Monad.IO.Class (MonadIO (..))
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 qualified Hedgehog.Gen as Gen
import Type.Reflection (Typeable)

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

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

instance MonadCell Holmes where
  newtype Cell Holmes x = Cell { Cell Holmes x -> Cell (MoriarT IO) x
unwrap :: Cell (MoriarT IO) x }

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

  watch :: Cell Holmes x -> (x -> Holmes ()) -> Holmes ()
watch (Cell cell) = ((x -> MoriarT IO ()) -> MoriarT IO ())
-> (x -> Holmes ()) -> Holmes ()
coerce (Cell (MoriarT IO) x -> (x -> MoriarT IO ()) -> MoriarT IO ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
watch @(MoriarT IO) Cell (MoriarT IO) x
cell)
  with :: Cell Holmes x -> (x -> Holmes ()) -> Holmes ()
with  (Cell cell) = ((x -> MoriarT IO ()) -> MoriarT IO ())
-> (x -> Holmes ()) -> Holmes ()
coerce (Cell (MoriarT IO) x -> (x -> MoriarT IO ()) -> MoriarT IO ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
with  @(MoriarT IO) Cell (MoriarT IO) x
cell)
  write :: Cell Holmes x -> x -> Holmes ()
write (Cell cell) = (x -> MoriarT IO ()) -> x -> Holmes ()
coerce (Cell (MoriarT IO) x -> x -> MoriarT IO ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
write @(MoriarT IO) Cell (MoriarT IO) 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 Holmes x -> Holmes x
unsafeRead :: Cell Holmes x -> Holmes x
unsafeRead = MoriarT IO x -> Holmes x
coerce (MoriarT IO x -> Holmes x)
-> (Cell Holmes x -> MoriarT IO x) -> Cell Holmes x -> Holmes x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cell (MoriarT IO) x -> MoriarT IO x
forall (m :: * -> *) x.
PrimMonad m =>
Cell (MoriarT m) x -> MoriarT m x
MoriarT.unsafeRead (Cell (MoriarT IO) x -> MoriarT IO x)
-> (Cell Holmes x -> Cell (MoriarT IO) x)
-> Cell Holmes x
-> MoriarT IO x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cell Holmes x -> Cell (MoriarT IO) x
forall x. Cell Holmes x -> Cell (MoriarT IO) 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 -> IO (Maybe x)
backward :: (forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y)
-> y -> IO (Maybe x)
backward forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f y
y = MoriarT IO x -> IO (Maybe x)
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne (MoriarT IO x -> IO (Maybe x)) -> MoriarT IO x -> IO (Maybe x)
forall a b. (a -> b) -> a -> b
$ Holmes x -> MoriarT IO x
forall x. Holmes x -> MoriarT IO x
runHolmes do
  Cell Holmes x
input  <- Holmes (Cell Holmes x)
forall (m :: * -> *) x. (MonadCell m, Monoid x) => m (Cell m x)
Cell.make
  Cell Holmes y
output <- Prop Holmes y -> Holmes (Cell Holmes y)
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
Prop.down (Prop Holmes x -> Prop Holmes y
forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f (Cell Holmes x -> Prop Holmes x
forall (m :: * -> *) x. Applicative m => Cell m x -> Prop m x
Prop.up Cell Holmes x
input))

  Cell Holmes y -> y -> Holmes ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
Cell.write Cell Holmes y
output y
y
  Cell Holmes x -> Holmes x
forall x. Cell Holmes x -> Holmes x
unsafeRead Cell Holmes 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 -> IO (Maybe y)
forward :: (forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y)
-> x -> IO (Maybe y)
forward forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f x
x = MoriarT IO y -> IO (Maybe y)
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne (MoriarT IO y -> IO (Maybe y)) -> MoriarT IO y -> IO (Maybe y)
forall a b. (a -> b) -> a -> b
$ Holmes y -> MoriarT IO y
forall x. Holmes x -> MoriarT IO x
runHolmes do
  Cell Holmes x
input  <- Holmes (Cell Holmes x)
forall (m :: * -> *) x. (MonadCell m, Monoid x) => m (Cell m x)
Cell.make
  Cell Holmes y
output <- Prop Holmes y -> Holmes (Cell Holmes y)
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
Prop.down (Prop Holmes x -> Prop Holmes y
forall (m :: * -> *). MonadCell m => Prop m x -> Prop m y
f (Cell Holmes x -> Prop Holmes x
forall (m :: * -> *) x. Applicative m => Cell m x -> Prop m x
Prop.up Cell Holmes x
input))

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

-- | Interpret a 'Holmes' program into 'IO', 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 :: Holmes x -> IO [ x ]
runAll :: Holmes x -> IO [x]
runAll = (MoriarT IO x -> IO [x]) -> Holmes x -> IO [x]
coerce (forall x. Monad IO => MoriarT IO x -> IO [x]
forall (m :: * -> *) x. Monad m => MoriarT m x -> m [x]
MoriarT.runAll @IO)

-- | Interpret a 'Holmes' program into 'IO', 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 :: Holmes x -> IO (Maybe x)
runOne :: Holmes x -> IO (Maybe x)
runOne = (MoriarT IO x -> IO (Maybe x)) -> Holmes x -> IO (Maybe x)
coerce (forall x. Monad IO => MoriarT IO x -> IO (Maybe x)
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne @IO)

-- | 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
     )
  => Config Holmes (f x)
  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
  -> IO (Maybe [ f x ])
satisfying :: Config Holmes (f x)
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> IO (Maybe [f x])
satisfying (Config Holmes (f x) -> Config (MoriarT IO) (f x)
coerce -> Config (MoriarT IO) (f x)
config :: Config (MoriarT IO) (f x)) forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f
  = MoriarT IO [f x] -> IO (Maybe [f x])
forall (m :: * -> *) x. Monad m => MoriarT m x -> m (Maybe x)
MoriarT.runOne (Config (MoriarT IO) (f x)
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> MoriarT IO [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 (MoriarT IO) (f x)
config forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f)

-- | Shuffle the refinements in a configuration. If we make a configuration
-- like @100 `from` [1 .. 10]@, the first configuration will be one hundred @1@
-- values. Sometimes, we might find we get to a first solution /faster/ by
-- randomising the order in which refinements are given. This is similar to the
-- "random restart" strategy in hill-climbing problems.
--
-- Another nice use for this function is procedural generation: often, your
-- results will look more "natural" if you introduce an element of randomness.
shuffle :: Config Holmes x -> Config Holmes x
shuffle :: Config Holmes x -> Config Holmes x
shuffle Config{[x]
x -> Holmes [x]
refine :: forall (m :: * -> *) x. Config m x -> x -> m [x]
initial :: forall (m :: * -> *) x. Config m x -> [x]
refine :: x -> Holmes [x]
initial :: [x]
..} = [x] -> (x -> Holmes [x]) -> Config Holmes x
forall (m :: * -> *) x. [x] -> (x -> m [x]) -> Config m x
Config [x]
initial \x
x -> do
  let shuffle' :: [a] -> MoriarT IO [a]
shuffle' = IO [a] -> MoriarT IO [a]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [a] -> MoriarT IO [a])
-> ([a] -> IO [a]) -> [a] -> MoriarT IO [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Gen [a] -> IO [a]
forall (m :: * -> *) a. MonadIO m => Gen a -> m a
Gen.sample (Gen [a] -> IO [a]) -> ([a] -> Gen [a]) -> [a] -> IO [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Gen [a]
forall (m :: * -> *) a. MonadGen m => [a] -> m [a]
Gen.shuffle
  MoriarT IO [x] -> Holmes [x]
forall x. MoriarT IO x -> Holmes x
Holmes (Holmes [x] -> MoriarT IO [x]
forall x. Holmes x -> MoriarT IO x
runHolmes (x -> Holmes [x]
refine x
x) MoriarT IO [x] -> ([x] -> MoriarT IO [x]) -> MoriarT IO [x]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [x] -> MoriarT IO [x]
forall a. [a] -> MoriarT IO [a]
shuffle')

-- | 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
     )
  => Config Holmes (f x)
  -> (forall m. MonadCell m => [ Prop m (f x) ] -> Prop m (f Bool))
  -> IO [[ f x ]]
whenever :: Config Holmes (f x)
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> IO [[f x]]
whenever (Config Holmes (f x) -> Config (MoriarT IO) (f x)
coerce -> Config (MoriarT IO) (f x)
config :: Config (MoriarT IO) (f x)) forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f
  = MoriarT IO [f x] -> IO [[f x]]
forall (m :: * -> *) x. Monad m => MoriarT m x -> m [x]
MoriarT.runAll (Config (MoriarT IO) (f x)
-> (forall (m :: * -> *).
    MonadCell m =>
    [Prop m (f x)] -> Prop m (f Bool))
-> MoriarT IO [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 (MoriarT IO) (f x)
config forall (m :: * -> *).
MonadCell m =>
[Prop m (f x)] -> Prop m (f Bool)
f)