{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}

{-|
Module      : Data.Input.Config
Description : My horror at his crimes was lost in my admiration at his skill.
Copyright   : (c) Tom Harding, 2020
License     : MIT

'MoriarT' is a monad transformer implementing the 'MonadCell' class with
provenance and backtracking search. In other words, it can search large
parameter spaces using different parameter configurations, looking for
contradicting sets of parameters to prune out parts of the search tree. It does
this by keeping track of which cells influence which results, and considering
any influencers on a failure to be contradictory.

In other words: if a write to cell @A@ fails, and the write was based on values
from cells @B@ and @C@, any search branch in which @B@ and @C@ have these
current values will be /pruned/ from the search, and we won't try them.

(In practice, this isn't strictly true: we just abort any branch that ever
produces any cell with any provenance that contains those values for @B@ and
@C@. This is a "lazier" strategy, and doesn't involve evaluating the search
space up front).
-}
module Control.Monad.MoriarT
  ( MoriarT (..)

  , runAll
  , runOne
  , solve
  , unsafeRead
  ) where

import Control.Applicative (Alternative (..))
import Control.Monad (MonadPlus, guard)
import Control.Monad.Cell.Class (MonadCell (..))
import qualified Control.Monad.Cell.Class as Cell
import Control.Monad.IO.Class (MonadIO (..))
import Control.Monad.Logic (MonadLogic, LogicT (..))
import qualified Control.Monad.Logic as LogicT
import Control.Monad.Primitive (PrimMonad (..))
import Control.Monad.Reader.Class (MonadReader (..))
import qualified Control.Monad.Reader.Class as Reader
import Control.Monad.State.Class (MonadState (..))
import qualified Control.Monad.State.Class as State
import Control.Monad.Trans.Class (MonadTrans (..))
import Control.Monad.Trans.Reader (ReaderT (..))
import Control.Monad.Trans.State (StateT (..))
import qualified Control.Monad.Trans.State as StateT
import qualified Data.CDCL as CDCL
import Data.Foldable (asum)
import Data.Function ((&))
import Data.Functor ((<&>))
import Data.Input.Config (Config (..))
import Data.JoinSemilattice.Class.Boolean (BooleanR (..))
import Data.JoinSemilattice.Class.Eq (EqR (..))
import Data.JoinSemilattice.Class.Merge (Merge (..), Result (..))
import Data.Kind (Type)
import Data.Maybe (listToMaybe)
import Data.Monoid (Ap (..))
import Data.Primitive.MutVar (MutVar)
import qualified Data.Primitive.MutVar as MutVar
import Data.Propagator (Prop)
import qualified Data.Propagator as Prop
import Type.Reflection (Typeable)

-- | The constraint-solving monad transformer. We implement the current
-- computation context with 'MonadReader', and the current "no goods" list with
-- 'MonadState'.
--
-- This transformer exposes its internals through the 'MonadReader',
-- 'MonadState', 'MonadLogic', and 'MonadIO' interfaces, and should therefore
-- /not/ be used directly. The reason is simply that misuse of any of these
-- will break the computation, so the library provides "Control.Monad.Holmes"
-- and "Control.Monad.Watson", who do their best to thwart 'MoriarT'.
newtype MoriarT (m :: Type -> Type) (x :: Type)
  = MoriarT
      { MoriarT m x -> ReaderT Rule (LogicT (StateT Group m)) x
unMoriarT :: ReaderT CDCL.Rule (LogicT (StateT CDCL.Group m)) x
      }
   deriving newtype
    ( a -> MoriarT m b -> MoriarT m a
(a -> b) -> MoriarT m a -> MoriarT m b
(forall a b. (a -> b) -> MoriarT m a -> MoriarT m b)
-> (forall a b. a -> MoriarT m b -> MoriarT m a)
-> Functor (MoriarT m)
forall a b. a -> MoriarT m b -> MoriarT m a
forall a b. (a -> b) -> MoriarT m a -> MoriarT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
forall (m :: * -> *) a b. a -> MoriarT m b -> MoriarT m a
forall (m :: * -> *) a b. (a -> b) -> MoriarT m a -> MoriarT m b
<$ :: a -> MoriarT m b -> MoriarT m a
$c<$ :: forall (m :: * -> *) a b. a -> MoriarT m b -> MoriarT m a
fmap :: (a -> b) -> MoriarT m a -> MoriarT m b
$cfmap :: forall (m :: * -> *) a b. (a -> b) -> MoriarT m a -> MoriarT m b
Functor
    , Functor (MoriarT m)
a -> MoriarT m a
Functor (MoriarT m)
-> (forall a. a -> MoriarT m a)
-> (forall a b. MoriarT m (a -> b) -> MoriarT m a -> MoriarT m b)
-> (forall a b c.
    (a -> b -> c) -> MoriarT m a -> MoriarT m b -> MoriarT m c)
-> (forall a b. MoriarT m a -> MoriarT m b -> MoriarT m b)
-> (forall a b. MoriarT m a -> MoriarT m b -> MoriarT m a)
-> Applicative (MoriarT m)
MoriarT m a -> MoriarT m b -> MoriarT m b
MoriarT m a -> MoriarT m b -> MoriarT m a
MoriarT m (a -> b) -> MoriarT m a -> MoriarT m b
(a -> b -> c) -> MoriarT m a -> MoriarT m b -> MoriarT m c
forall a. a -> MoriarT m a
forall a b. MoriarT m a -> MoriarT m b -> MoriarT m a
forall a b. MoriarT m a -> MoriarT m b -> MoriarT m b
forall a b. MoriarT m (a -> b) -> MoriarT m a -> MoriarT m b
forall a b c.
(a -> b -> c) -> MoriarT m a -> MoriarT m b -> MoriarT m c
forall (m :: * -> *). Functor (MoriarT m)
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
forall (m :: * -> *) a. a -> MoriarT m a
forall (m :: * -> *) a b. MoriarT m a -> MoriarT m b -> MoriarT m a
forall (m :: * -> *) a b. MoriarT m a -> MoriarT m b -> MoriarT m b
forall (m :: * -> *) a b.
MoriarT m (a -> b) -> MoriarT m a -> MoriarT m b
forall (m :: * -> *) a b c.
(a -> b -> c) -> MoriarT m a -> MoriarT m b -> MoriarT m c
<* :: MoriarT m a -> MoriarT m b -> MoriarT m a
$c<* :: forall (m :: * -> *) a b. MoriarT m a -> MoriarT m b -> MoriarT m a
*> :: MoriarT m a -> MoriarT m b -> MoriarT m b
$c*> :: forall (m :: * -> *) a b. MoriarT m a -> MoriarT m b -> MoriarT m b
liftA2 :: (a -> b -> c) -> MoriarT m a -> MoriarT m b -> MoriarT m c
$cliftA2 :: forall (m :: * -> *) a b c.
(a -> b -> c) -> MoriarT m a -> MoriarT m b -> MoriarT m c
<*> :: MoriarT m (a -> b) -> MoriarT m a -> MoriarT m b
$c<*> :: forall (m :: * -> *) a b.
MoriarT m (a -> b) -> MoriarT m a -> MoriarT m b
pure :: a -> MoriarT m a
$cpure :: forall (m :: * -> *) a. a -> MoriarT m a
$cp1Applicative :: forall (m :: * -> *). Functor (MoriarT m)
Applicative
    , Applicative (MoriarT m)
MoriarT m a
Applicative (MoriarT m)
-> (forall a. MoriarT m a)
-> (forall a. MoriarT m a -> MoriarT m a -> MoriarT m a)
-> (forall a. MoriarT m a -> MoriarT m [a])
-> (forall a. MoriarT m a -> MoriarT m [a])
-> Alternative (MoriarT m)
MoriarT m a -> MoriarT m a -> MoriarT m a
MoriarT m a -> MoriarT m [a]
MoriarT m a -> MoriarT m [a]
forall a. MoriarT m a
forall a. MoriarT m a -> MoriarT m [a]
forall a. MoriarT m a -> MoriarT m a -> MoriarT m a
forall (m :: * -> *). Applicative (MoriarT m)
forall (f :: * -> *).
Applicative f
-> (forall a. f a)
-> (forall a. f a -> f a -> f a)
-> (forall a. f a -> f [a])
-> (forall a. f a -> f [a])
-> Alternative f
forall (m :: * -> *) a. MoriarT m a
forall (m :: * -> *) a. MoriarT m a -> MoriarT m [a]
forall (m :: * -> *) a. MoriarT m a -> MoriarT m a -> MoriarT m a
many :: MoriarT m a -> MoriarT m [a]
$cmany :: forall (m :: * -> *) a. MoriarT m a -> MoriarT m [a]
some :: MoriarT m a -> MoriarT m [a]
$csome :: forall (m :: * -> *) a. MoriarT m a -> MoriarT m [a]
<|> :: MoriarT m a -> MoriarT m a -> MoriarT m a
$c<|> :: forall (m :: * -> *) a. MoriarT m a -> MoriarT m a -> MoriarT m a
empty :: MoriarT m a
$cempty :: forall (m :: * -> *) a. MoriarT m a
$cp1Alternative :: forall (m :: * -> *). Applicative (MoriarT m)
Alternative
    , Applicative (MoriarT m)
a -> MoriarT m a
Applicative (MoriarT m)
-> (forall a b. MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b)
-> (forall a b. MoriarT m a -> MoriarT m b -> MoriarT m b)
-> (forall a. a -> MoriarT m a)
-> Monad (MoriarT m)
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
MoriarT m a -> MoriarT m b -> MoriarT m b
forall a. a -> MoriarT m a
forall a b. MoriarT m a -> MoriarT m b -> MoriarT m b
forall a b. MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
forall (m :: * -> *). Applicative (MoriarT m)
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
forall (m :: * -> *) a. a -> MoriarT m a
forall (m :: * -> *) a b. MoriarT m a -> MoriarT m b -> MoriarT m b
forall (m :: * -> *) a b.
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
return :: a -> MoriarT m a
$creturn :: forall (m :: * -> *) a. a -> MoriarT m a
>> :: MoriarT m a -> MoriarT m b -> MoriarT m b
$c>> :: forall (m :: * -> *) a b. MoriarT m a -> MoriarT m b -> MoriarT m b
>>= :: MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
$c>>= :: forall (m :: * -> *) a b.
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
$cp1Monad :: forall (m :: * -> *). Applicative (MoriarT m)
Monad
    , Monad (MoriarT m)
Monad (MoriarT m)
-> (forall a. IO a -> MoriarT m a) -> MonadIO (MoriarT m)
IO a -> MoriarT m a
forall a. IO a -> MoriarT m a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
forall (m :: * -> *). MonadIO m => Monad (MoriarT m)
forall (m :: * -> *) a. MonadIO m => IO a -> MoriarT m a
liftIO :: IO a -> MoriarT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> MoriarT m a
$cp1MonadIO :: forall (m :: * -> *). MonadIO m => Monad (MoriarT m)
MonadIO
    , MonadPlus (MoriarT m)
MonadPlus (MoriarT m)
-> (forall a. MoriarT m a -> MoriarT m (Maybe (a, MoriarT m a)))
-> (forall a. MoriarT m a -> MoriarT m a -> MoriarT m a)
-> (forall a b. MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b)
-> (forall a b.
    MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b -> MoriarT m b)
-> (forall a. MoriarT m a -> MoriarT m a)
-> (forall a. MoriarT m a -> MoriarT m ())
-> MonadLogic (MoriarT m)
MoriarT m a -> MoriarT m (Maybe (a, MoriarT m a))
MoriarT m a -> MoriarT m a -> MoriarT m a
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b -> MoriarT m b
MoriarT m a -> MoriarT m a
MoriarT m a -> MoriarT m ()
forall a. MoriarT m a -> MoriarT m a
forall a. MoriarT m a -> MoriarT m (Maybe (a, MoriarT m a))
forall a. MoriarT m a -> MoriarT m ()
forall a. MoriarT m a -> MoriarT m a -> MoriarT m a
forall a b. MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
forall a b.
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b -> MoriarT m b
forall (m :: * -> *). Monad m => MonadPlus (MoriarT m)
forall (m :: * -> *) a. Monad m => MoriarT m a -> MoriarT m a
forall (m :: * -> *) a.
Monad m =>
MoriarT m a -> MoriarT m (Maybe (a, MoriarT m a))
forall (m :: * -> *) a. Monad m => MoriarT m a -> MoriarT m ()
forall (m :: * -> *) a.
Monad m =>
MoriarT m a -> MoriarT m a -> MoriarT m a
forall (m :: * -> *) a b.
Monad m =>
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
forall (m :: * -> *) a b.
Monad m =>
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b -> MoriarT m b
forall (m :: * -> *).
MonadPlus m
-> (forall a. m a -> m (Maybe (a, m a)))
-> (forall a. m a -> m a -> m a)
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> (a -> m b) -> m b -> m b)
-> (forall a. m a -> m a)
-> (forall a. m a -> m ())
-> MonadLogic m
lnot :: MoriarT m a -> MoriarT m ()
$clnot :: forall (m :: * -> *) a. Monad m => MoriarT m a -> MoriarT m ()
once :: MoriarT m a -> MoriarT m a
$conce :: forall (m :: * -> *) a. Monad m => MoriarT m a -> MoriarT m a
ifte :: MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b -> MoriarT m b
$cifte :: forall (m :: * -> *) a b.
Monad m =>
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b -> MoriarT m b
>>- :: MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
$c>>- :: forall (m :: * -> *) a b.
Monad m =>
MoriarT m a -> (a -> MoriarT m b) -> MoriarT m b
interleave :: MoriarT m a -> MoriarT m a -> MoriarT m a
$cinterleave :: forall (m :: * -> *) a.
Monad m =>
MoriarT m a -> MoriarT m a -> MoriarT m a
msplit :: MoriarT m a -> MoriarT m (Maybe (a, MoriarT m a))
$cmsplit :: forall (m :: * -> *) a.
Monad m =>
MoriarT m a -> MoriarT m (Maybe (a, MoriarT m a))
$cp1MonadLogic :: forall (m :: * -> *). Monad m => MonadPlus (MoriarT m)
MonadLogic
    , Monad (MoriarT m)
Alternative (MoriarT m)
MoriarT m a
Alternative (MoriarT m)
-> Monad (MoriarT m)
-> (forall a. MoriarT m a)
-> (forall a. MoriarT m a -> MoriarT m a -> MoriarT m a)
-> MonadPlus (MoriarT m)
MoriarT m a -> MoriarT m a -> MoriarT m a
forall a. MoriarT m a
forall a. MoriarT m a -> MoriarT m a -> MoriarT m a
forall (m :: * -> *). Monad (MoriarT m)
forall (m :: * -> *). Alternative (MoriarT m)
forall (m :: * -> *).
Alternative m
-> Monad m
-> (forall a. m a)
-> (forall a. m a -> m a -> m a)
-> MonadPlus m
forall (m :: * -> *) a. MoriarT m a
forall (m :: * -> *) a. MoriarT m a -> MoriarT m a -> MoriarT m a
mplus :: MoriarT m a -> MoriarT m a -> MoriarT m a
$cmplus :: forall (m :: * -> *) a. MoriarT m a -> MoriarT m a -> MoriarT m a
mzero :: MoriarT m a
$cmzero :: forall (m :: * -> *) a. MoriarT m a
$cp2MonadPlus :: forall (m :: * -> *). Monad (MoriarT m)
$cp1MonadPlus :: forall (m :: * -> *). Alternative (MoriarT m)
MonadPlus
    , MonadReader CDCL.Rule
    , MonadState CDCL.Group
    )
  deriving (b -> MoriarT m x -> MoriarT m x
NonEmpty (MoriarT m x) -> MoriarT m x
MoriarT m x -> MoriarT m x -> MoriarT m x
(MoriarT m x -> MoriarT m x -> MoriarT m x)
-> (NonEmpty (MoriarT m x) -> MoriarT m x)
-> (forall b. Integral b => b -> MoriarT m x -> MoriarT m x)
-> Semigroup (MoriarT m x)
forall b. Integral b => b -> MoriarT m x -> MoriarT m x
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall (m :: * -> *) x.
Semigroup x =>
NonEmpty (MoriarT m x) -> MoriarT m x
forall (m :: * -> *) x.
Semigroup x =>
MoriarT m x -> MoriarT m x -> MoriarT m x
forall (m :: * -> *) x b.
(Semigroup x, Integral b) =>
b -> MoriarT m x -> MoriarT m x
stimes :: b -> MoriarT m x -> MoriarT m x
$cstimes :: forall (m :: * -> *) x b.
(Semigroup x, Integral b) =>
b -> MoriarT m x -> MoriarT m x
sconcat :: NonEmpty (MoriarT m x) -> MoriarT m x
$csconcat :: forall (m :: * -> *) x.
Semigroup x =>
NonEmpty (MoriarT m x) -> MoriarT m x
<> :: MoriarT m x -> MoriarT m x -> MoriarT m x
$c<> :: forall (m :: * -> *) x.
Semigroup x =>
MoriarT m x -> MoriarT m x -> MoriarT m x
Semigroup, Semigroup (MoriarT m x)
MoriarT m x
Semigroup (MoriarT m x)
-> MoriarT m x
-> (MoriarT m x -> MoriarT m x -> MoriarT m x)
-> ([MoriarT m x] -> MoriarT m x)
-> Monoid (MoriarT m x)
[MoriarT m x] -> MoriarT m x
MoriarT m x -> MoriarT m x -> MoriarT m x
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall (m :: * -> *) x. Monoid x => Semigroup (MoriarT m x)
forall (m :: * -> *) x. Monoid x => MoriarT m x
forall (m :: * -> *) x. Monoid x => [MoriarT m x] -> MoriarT m x
forall (m :: * -> *) x.
Monoid x =>
MoriarT m x -> MoriarT m x -> MoriarT m x
mconcat :: [MoriarT m x] -> MoriarT m x
$cmconcat :: forall (m :: * -> *) x. Monoid x => [MoriarT m x] -> MoriarT m x
mappend :: MoriarT m x -> MoriarT m x -> MoriarT m x
$cmappend :: forall (m :: * -> *) x.
Monoid x =>
MoriarT m x -> MoriarT m x -> MoriarT m x
mempty :: MoriarT m x
$cmempty :: forall (m :: * -> *) x. Monoid x => MoriarT m x
$cp1Monoid :: forall (m :: * -> *) x. Monoid x => Semigroup (MoriarT m x)
Monoid)
    via (Ap (MoriarT m) x)

instance MonadTrans MoriarT where
  lift :: m a -> MoriarT m a
lift = ReaderT Rule (LogicT (StateT Group m)) a -> MoriarT m a
forall (m :: * -> *) x.
ReaderT Rule (LogicT (StateT Group m)) x -> MoriarT m x
MoriarT (ReaderT Rule (LogicT (StateT Group m)) a -> MoriarT m a)
-> (m a -> ReaderT Rule (LogicT (StateT Group m)) a)
-> m a
-> MoriarT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicT (StateT Group m) a
-> ReaderT Rule (LogicT (StateT Group m)) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (LogicT (StateT Group m) a
 -> ReaderT Rule (LogicT (StateT Group m)) a)
-> (m a -> LogicT (StateT Group m) a)
-> m a
-> ReaderT Rule (LogicT (StateT Group m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT Group m a -> LogicT (StateT Group m) a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT Group m a -> LogicT (StateT Group m) a)
-> (m a -> StateT Group m a) -> m a -> LogicT (StateT Group m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> StateT Group m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

instance PrimMonad m => PrimMonad (MoriarT m) where
  type PrimState (MoriarT m) = PrimState m

  primitive :: (State# (PrimState (MoriarT m))
 -> (# State# (PrimState (MoriarT m)), a #))
-> MoriarT m a
primitive = m a -> MoriarT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> MoriarT m a)
-> ((State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a)
-> (State# (PrimState m) -> (# State# (PrimState m), a #))
-> MoriarT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a
forall (m :: * -> *) a.
PrimMonad m =>
(State# (PrimState m) -> (# State# (PrimState m), a #)) -> m a
primitive

instance PrimMonad m => MonadCell (MoriarT m) where
  newtype Cell (MoriarT m) (content :: Type)
    = Cell (MutVar (PrimState m) (CDCL.Rule, content, MoriarT m ()))

  discard :: MoriarT m x
discard = do
    Rule
context <- MoriarT m Rule
forall r (m :: * -> *). MonadReader r m => m r
Reader.ask
    (Group -> Group) -> MoriarT m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
State.modify (Rule -> Group -> Group
CDCL.resolve Rule
context) -- Add this context to the "no goods" list.
    
    MoriarT m x
forall (f :: * -> *) a. Alternative f => f a
empty

  fill :: x -> MoriarT m (Cell (MoriarT m) x)
fill x
content = do
    Rule
context <- MoriarT m Rule
forall r (m :: * -> *). MonadReader r m => m r
Reader.ask
    MutVar (PrimState m) (Rule, x, MoriarT m ())
mutVar  <- (Rule, x, MoriarT m ())
-> MoriarT
     m (MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ()))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
MutVar.newMutVar (Rule
context, x
content, MoriarT m ()
forall a. Monoid a => a
mempty)
    Cell (MoriarT m) x -> MoriarT m (Cell (MoriarT m) x)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MutVar (PrimState m) (Rule, x, MoriarT m ()) -> Cell (MoriarT m) x
forall (m :: * -> *) content.
MutVar (PrimState m) (Rule, content, MoriarT m ())
-> Cell (MoriarT m) content
Cell MutVar (PrimState m) (Rule, x, MoriarT m ())
mutVar)

  watch :: Cell (MoriarT m) x -> (x -> MoriarT m ()) -> MoriarT m ()
watch cell :: Cell (MoriarT m) x
cell@(Cell mutVar) x -> MoriarT m ()
propagator = do
    let next :: MoriarT m ()
next = Cell (MoriarT m) x -> (x -> MoriarT m ()) -> MoriarT m ()
forall (m :: * -> *) x.
MonadCell m =>
Cell m x -> (x -> m ()) -> m ()
with Cell (MoriarT m) x
cell x -> MoriarT m ()
propagator

    before :: (Rule, x, MoriarT m ())
before@(Rule
provenance, x
content, MoriarT m ()
callbacks)
      <- MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> MoriarT m (Rule, x, MoriarT m ())
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
MutVar.readMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar

    MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> (Rule, x, MoriarT m ()) -> MoriarT m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
MutVar.writeMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar (Rule
provenance, x
content, MoriarT m ()
callbacks MoriarT m () -> MoriarT m () -> MoriarT m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> MoriarT m ()
next) MoriarT m () -> MoriarT m () -> MoriarT m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> MoriarT m ()
next
      MoriarT m () -> MoriarT m () -> MoriarT m ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> (Rule, x, MoriarT m ()) -> MoriarT m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
MutVar.writeMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar (Rule, x, MoriarT m ())
before MoriarT m () -> MoriarT m () -> MoriarT m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> MoriarT m ()
forall (f :: * -> *) a. Alternative f => f a
empty -- Undo the action for the next branch.

  with :: Cell (MoriarT m) x -> (x -> MoriarT m ()) -> MoriarT m ()
with (Cell mutVar) x -> MoriarT m ()
callback = do
    (Rule
provenance, x
content, MoriarT m ()
_) <- MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> MoriarT m (Rule, x, MoriarT m ())
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
MutVar.readMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar
    (Rule -> Rule) -> MoriarT m () -> MoriarT m ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
Reader.local (Rule -> Rule -> Rule
forall a. Semigroup a => a -> a -> a
<> Rule
provenance) (x -> MoriarT m ()
callback x
content)

  write :: Cell (MoriarT m) x -> x -> MoriarT m ()
write (Cell mutVar) x
news = do
    Rule
context <- MoriarT m Rule
forall r (m :: * -> *). MonadReader r m => m r
Reader.ask
    Group
nogoods <- MoriarT m Group
forall s (m :: * -> *). MonadState s m => m s
State.get

    before :: (Rule, x, MoriarT m ())
before@(Rule
provenance, x
content, MoriarT m ()
callbacks)
      <- MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> MoriarT m (Rule, x, MoriarT m ())
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
MutVar.readMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar

    let provenance' :: Rule
provenance' = Rule
context Rule -> Rule -> Rule
forall a. Semigroup a => a -> a -> a
<> Rule
provenance
        content' :: Result x
content'    = x
content x -> x -> Result x
forall x. Merge x => x -> x -> Result x
<<- x
news

    -- Skip this branch if the provenance is no good.
    Bool -> MoriarT m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Group
nogoods Group -> Rule -> Bool
`CDCL.implies` Rule
provenance'))

    case Result x
content' of
      Changed x
update -> do
        MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> (Rule, x, MoriarT m ()) -> MoriarT m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
MutVar.writeMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar (Rule
provenance', x
update, MoriarT m ()
callbacks) MoriarT m () -> MoriarT m () -> MoriarT m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> MoriarT m ()
callbacks
          MoriarT m () -> MoriarT m () -> MoriarT m ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> (Rule, x, MoriarT m ()) -> MoriarT m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
MutVar.writeMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar (Rule, x, MoriarT m ())
before MoriarT m () -> MoriarT m () -> MoriarT m ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> MoriarT m ()
forall (f :: * -> *) a. Alternative f => f a
empty

      Result x
Failure   -> (Rule -> Rule) -> MoriarT m () -> MoriarT m ()
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
Reader.local (Rule -> Rule -> Rule
forall a. Semigroup a => a -> a -> a
<> Rule
context) MoriarT m ()
forall (m :: * -> *) x. MonadCell m => m x
discard
      Result x
Unchanged -> () -> MoriarT m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | 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 :: PrimMonad m => Cell (MoriarT m) x -> MoriarT m x
unsafeRead :: Cell (MoriarT m) x -> MoriarT m x
unsafeRead (Cell mutVar) = do
  (Rule
_, x
content, MoriarT m ()
_) <- MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
-> MoriarT m (Rule, x, MoriarT m ())
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
MutVar.readMutVar MutVar (PrimState m) (Rule, x, MoriarT m ())
MutVar (PrimState (MoriarT m)) (Rule, x, MoriarT m ())
mutVar

  x -> MoriarT m x
forall (f :: * -> *) a. Applicative f => a -> f a
pure x
content

-- | Run a 'MoriarT' computation and return the list of __all__ valid branches'
-- results, in the order in which they were discovered.
runAll :: Monad m => MoriarT m x -> m [ x ]
runAll :: MoriarT m x -> m [x]
runAll
  = (StateT Group m [x] -> Group -> m [x])
-> Group -> StateT Group m [x] -> m [x]
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT Group m [x] -> Group -> m [x]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
StateT.evalStateT Group
forall a. Monoid a => a
mempty
  (StateT Group m [x] -> m [x])
-> (MoriarT m x -> StateT Group m [x]) -> MoriarT m x -> m [x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicT (StateT Group m) x -> StateT Group m [x]
forall (m :: * -> *) a. Monad m => LogicT m a -> m [a]
LogicT.observeAllT
  (LogicT (StateT Group m) x -> StateT Group m [x])
-> (MoriarT m x -> LogicT (StateT Group m) x)
-> MoriarT m x
-> StateT Group m [x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT Rule (LogicT (StateT Group m)) x
 -> Rule -> LogicT (StateT Group m) x)
-> Rule
-> ReaderT Rule (LogicT (StateT Group m)) x
-> LogicT (StateT Group m) x
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Rule (LogicT (StateT Group m)) x
-> Rule -> LogicT (StateT Group m) x
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Rule
forall a. Monoid a => a
mempty
  (ReaderT Rule (LogicT (StateT Group m)) x
 -> LogicT (StateT Group m) x)
-> (MoriarT m x -> ReaderT Rule (LogicT (StateT Group m)) x)
-> MoriarT m x
-> LogicT (StateT Group m) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MoriarT m x -> ReaderT Rule (LogicT (StateT Group m)) x
forall (m :: * -> *) x.
MoriarT m x -> ReaderT Rule (LogicT (StateT Group m)) x
unMoriarT

-- | Run a 'MoriarT' computation and return the /first/ valid branch's result.
runOne :: Monad m => MoriarT m x -> m (Maybe x)
runOne :: MoriarT m x -> m (Maybe x)
runOne
  = ([x] -> Maybe x) -> m [x] -> m (Maybe x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [x] -> Maybe x
forall a. [a] -> Maybe a
listToMaybe
  (m [x] -> m (Maybe x))
-> (MoriarT m x -> m [x]) -> MoriarT m x -> m (Maybe x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateT Group m [x] -> Group -> m [x])
-> Group -> StateT Group m [x] -> m [x]
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT Group m [x] -> Group -> m [x]
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
StateT.evalStateT Group
forall a. Monoid a => a
mempty
  (StateT Group m [x] -> m [x])
-> (MoriarT m x -> StateT Group m [x]) -> MoriarT m x -> m [x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> LogicT (StateT Group m) x -> StateT Group m [x]
forall (m :: * -> *) a. Monad m => Int -> LogicT m a -> m [a]
LogicT.observeManyT Int
1
  (LogicT (StateT Group m) x -> StateT Group m [x])
-> (MoriarT m x -> LogicT (StateT Group m) x)
-> MoriarT m x
-> StateT Group m [x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ReaderT Rule (LogicT (StateT Group m)) x
 -> Rule -> LogicT (StateT Group m) x)
-> Rule
-> ReaderT Rule (LogicT (StateT Group m)) x
-> LogicT (StateT Group m) x
forall a b c. (a -> b -> c) -> b -> a -> c
flip ReaderT Rule (LogicT (StateT Group m)) x
-> Rule -> LogicT (StateT Group m) x
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT Rule
forall a. Monoid a => a
mempty
  (ReaderT Rule (LogicT (StateT Group m)) x
 -> LogicT (StateT Group m) x)
-> (MoriarT m x -> ReaderT Rule (LogicT (StateT Group m)) x)
-> MoriarT m x
-> LogicT (StateT Group m) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MoriarT m x -> ReaderT Rule (LogicT (StateT Group m)) x
forall (m :: * -> *) x.
MoriarT m x -> ReaderT Rule (LogicT (StateT Group m)) x
unMoriarT

-- | Given an input configuration, and a predicate on those input variables,
-- compute the configurations that satisfy the predicate. This result (or these
-- results) can be extracted using 'runOne' or 'runAll'.
solve
  :: ( 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 ]
solve :: Config (MoriarT m) (f x)
-> (forall (m' :: * -> *).
    MonadCell m' =>
    [Prop m' (f x)] -> Prop m' (f Bool))
-> MoriarT m [f x]
solve Config{[f x]
f x -> MoriarT m [f x]
refine :: forall (m :: * -> *) x. Config m x -> x -> m [x]
initial :: forall (m :: * -> *) x. Config m x -> [x]
refine :: f x -> MoriarT m [f x]
initial :: [f x]
..} forall (m' :: * -> *).
MonadCell m' =>
[Prop m' (f x)] -> Prop m' (f Bool)
predicate = do
  [Cell (MoriarT m) (f x)]
inputs <- (f x -> MoriarT m (Cell (MoriarT m) (f x)))
-> [f x] -> MoriarT m [Cell (MoriarT m) (f x)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse f x -> MoriarT m (Cell (MoriarT m) (f x))
forall (m :: * -> *) x. MonadCell m => x -> m (Cell m x)
Cell.fill [f x]
initial
  Cell (MoriarT m) (f Bool)
output <- Prop (MoriarT m) (f Bool) -> MoriarT m (Cell (MoriarT m) (f Bool))
forall (m :: * -> *) x.
(MonadCell m, Monoid x) =>
Prop m x -> m (Cell m x)
Prop.down ([Prop (MoriarT m) (f x)] -> Prop (MoriarT m) (f Bool)
forall (m' :: * -> *).
MonadCell m' =>
[Prop m' (f x)] -> Prop m' (f Bool)
predicate ((Cell (MoriarT m) (f x) -> Prop (MoriarT m) (f x))
-> [Cell (MoriarT m) (f x)] -> [Prop (MoriarT m) (f x)]
forall a b. (a -> b) -> [a] -> [b]
map Cell (MoriarT m) (f x) -> Prop (MoriarT m) (f x)
forall (m :: * -> *) x. Applicative m => Cell m x -> Prop m x
Prop.up [Cell (MoriarT m) (f x)]
inputs))
  Cell (MoriarT m) (f Bool) -> f Bool -> MoriarT m ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> x -> m ()
Cell.write Cell (MoriarT m) (f Bool)
output f Bool
forall (f :: * -> *). BooleanR f => f Bool
trueR

  [()]
_ <- [Int]
-> [Cell (MoriarT m) (f x)] -> [(Int, Cell (MoriarT m) (f x))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Cell (MoriarT m) (f x)]
inputs [(Int, Cell (MoriarT m) (f x))]
-> ([(Int, Cell (MoriarT m) (f x))] -> MoriarT m [()])
-> MoriarT m [()]
forall a b. a -> (a -> b) -> b
& ((Int, Cell (MoriarT m) (f x)) -> MoriarT m ())
-> [(Int, Cell (MoriarT m) (f x))] -> MoriarT m [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse \(Int
major, Cell (MoriarT m) (f x)
cell) -> do
    f x
current     <- Cell (MoriarT m) (f x) -> MoriarT m (f x)
forall (m :: * -> *) x.
PrimMonad m =>
Cell (MoriarT m) x -> MoriarT m x
unsafeRead Cell (MoriarT m) (f x)
cell
    [f x]
refinements <- f x -> MoriarT m [f x]
refine f x
current

    Cell (MoriarT m) (f x)
input <- [MoriarT m (Cell (MoriarT m) (f x))]
-> MoriarT m (Cell (MoriarT m) (f x))
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([MoriarT m (Cell (MoriarT m) (f x))]
 -> MoriarT m (Cell (MoriarT m) (f x)))
-> [MoriarT m (Cell (MoriarT m) (f x))]
-> MoriarT m (Cell (MoriarT m) (f x))
forall a b. (a -> b) -> a -> b
$ Int -> [f x] -> [(Rule, f x)]
forall x. Int -> [x] -> [(Rule, x)]
CDCL.index Int
major [f x]
refinements [(Rule, f x)]
-> ((Rule, f x) -> MoriarT m (Cell (MoriarT m) (f x)))
-> [MoriarT m (Cell (MoriarT m) (f x))]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(Rule
rule, f x
content) ->
      (MutVar (PrimState m) (Rule, f x, MoriarT m ())
 -> Cell (MoriarT m) (f x))
-> MoriarT m (MutVar (PrimState m) (Rule, f x, MoriarT m ()))
-> MoriarT m (Cell (MoriarT m) (f x))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MutVar (PrimState m) (Rule, f x, MoriarT m ())
-> Cell (MoriarT m) (f x)
forall (m :: * -> *) content.
MutVar (PrimState m) (Rule, content, MoriarT m ())
-> Cell (MoriarT m) content
Cell ((Rule, f x, MoriarT m ())
-> MoriarT
     m (MutVar (PrimState (MoriarT m)) (Rule, f x, MoriarT m ()))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
MutVar.newMutVar (Rule
rule, f x
content, MoriarT m ()
forall a. Monoid a => a
mempty))

    Cell (MoriarT m) (f x) -> Cell (MoriarT m) (f x) -> MoriarT m ()
forall (m :: * -> *) x.
(MonadCell m, Merge x) =>
Cell m x -> Cell m x -> m ()
Cell.unify Cell (MoriarT m) (f x)
cell Cell (MoriarT m) (f x)
input

  (Cell (MoriarT m) (f x) -> MoriarT m (f x))
-> [Cell (MoriarT m) (f x)] -> MoriarT m [f x]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Cell (MoriarT m) (f x) -> MoriarT m (f x)
forall (m :: * -> *) x.
PrimMonad m =>
Cell (MoriarT m) x -> MoriarT m x
unsafeRead [Cell (MoriarT m) (f x)]
inputs