{-# language DeriveFunctor #-}
{-# language FlexibleContexts #-}
{-# language GADTs #-}
{-# language GeneralizedNewtypeDeriving #-}
{-# language LambdaCase #-}
{-# language NamedFieldPuns #-}
{-# language OverloadedStrings #-}
{-# language RecordWildCards #-}

{-| This module exposes a small DSL for building and solving planning problems
using <http://www.fast-downward.org Fast Downward> - an open source solver for
<https://en.wikipedia.org/wiki/Automated_planning_and_scheduling classical planning problems>.

Using this module, you model problems with a finite-domain representation
through state variables (see, 'Var', 'newVar'), and model their changes through
'Effect's (see 'readVar', and 'writeVar'). If you're familiar with software
transactional memory, an effect is like a transaction, except the process of
solving will choose the appropriate sequence for you.
-}

module FastDownward
  ( -- * Defining Problems
    Problem

    -- ** @Var@iables
  , Var
  , newVar
  , readVar
  , writeVar
  , modifyVar
  , resetInitial

    -- ** @Effect@s
  , Effect

    -- ** @Test@s
  , Test
  , (?=)
  , FastDownward.any
  , requiresAxioms

    -- * Solving Problems
  , solve
  , SolveResult(..)
  , Solution
  , runProblem

    -- ** Extracting Plans
  , totallyOrderedPlan
  , partiallyOrderedPlan
  )
  where

import Control.Applicative ( Alternative(..) )
import qualified Control.Monad.Fail
import Control.Monad.IO.Class ( MonadIO, liftIO )
import Control.Monad.State.Class ( get, gets, modify )
import Control.Monad.Trans.Cont
import Control.Monad.Trans.Reader ( ReaderT(..), runReaderT )
import Control.Monad.Trans.State.Lazy ( StateT, evalStateT )
import Data.Coerce ( coerce )
import qualified Data.Foldable
import qualified Data.Graph
import Data.IORef
import Data.IntMap.Lazy ( IntMap )
import qualified Data.IntMap.Lazy as IntMap
import Data.List ( inits, intersect )
import Data.Map.Lazy ( Map )
import qualified Data.Map.Lazy as Map
import Data.Maybe ( mapMaybe )
import Data.Sequence ( Seq )
import qualified Data.Sequence as Seq
import Data.String ( fromString )
import qualified Data.Text.Lazy
import qualified Data.Text.Lazy.IO
import Data.Traversable ( for )
import qualified FastDownward.Exec as Exec
import qualified FastDownward.SAS
import qualified FastDownward.SAS.Axiom
import qualified FastDownward.SAS.Effect
import qualified FastDownward.SAS.Operator
import qualified FastDownward.SAS.Plan
import qualified FastDownward.SAS.Variable
import Prelude hiding ( reads )
import System.Exit
import System.IO.Temp


-- | A @Var@ is a state variable - a variable who's contents may change over
-- the execution of a plan. 'Effect's can read and write from variables in
-- order to change their state.
data Var a =
  Var
    { Var a -> VariableIndex
variableIndex :: {-# UNPACK #-} !FastDownward.SAS.VariableIndex
      -- ^ The SAS variable index of this variable.
    , Var a -> IORef (Map a (Committed, DomainIndex))
values :: {-# UNPACK #-} !( IORef ( Map a ( Committed, FastDownward.SAS.DomainIndex ) ) )
      -- ^ Map Haskell values to the index in the domain in the SAS
      -- representation.
    , Var a -> IORef (a -> DomainIndex -> IO ())
subscribed :: {-# UNPACK #-} !( IORef ( a -> FastDownward.SAS.DomainIndex -> IO () ) )
    , Var a -> IORef (Map DomainIndex a)
fromDomainIndex :: {-# UNPACK #-} !( IORef ( Map FastDownward.SAS.DomainIndex a ) )
      -- ^ Map back from a domain index to the Haskell value.
    }


data Committed =
  Committed | Uncommitted


-- | The @Problem@ monad is used to build a computation that describes a
-- particular planning problem. In this monad you can declare state variables
-- - 'Var's - using 'newVar', and you can solve planning problems using 'solve'.
newtype Problem a =
  Problem { Problem a -> StateT ProblemState IO a
unProblem :: StateT ProblemState IO a }
  deriving
    ( a -> Problem b -> Problem a
(a -> b) -> Problem a -> Problem b
(forall a b. (a -> b) -> Problem a -> Problem b)
-> (forall a b. a -> Problem b -> Problem a) -> Functor Problem
forall a b. a -> Problem b -> Problem a
forall a b. (a -> b) -> Problem a -> Problem b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Problem b -> Problem a
$c<$ :: forall a b. a -> Problem b -> Problem a
fmap :: (a -> b) -> Problem a -> Problem b
$cfmap :: forall a b. (a -> b) -> Problem a -> Problem b
Functor, Functor Problem
a -> Problem a
Functor Problem
-> (forall a. a -> Problem a)
-> (forall a b. Problem (a -> b) -> Problem a -> Problem b)
-> (forall a b c.
    (a -> b -> c) -> Problem a -> Problem b -> Problem c)
-> (forall a b. Problem a -> Problem b -> Problem b)
-> (forall a b. Problem a -> Problem b -> Problem a)
-> Applicative Problem
Problem a -> Problem b -> Problem b
Problem a -> Problem b -> Problem a
Problem (a -> b) -> Problem a -> Problem b
(a -> b -> c) -> Problem a -> Problem b -> Problem c
forall a. a -> Problem a
forall a b. Problem a -> Problem b -> Problem a
forall a b. Problem a -> Problem b -> Problem b
forall a b. Problem (a -> b) -> Problem a -> Problem b
forall a b c. (a -> b -> c) -> Problem a -> Problem b -> Problem 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
<* :: Problem a -> Problem b -> Problem a
$c<* :: forall a b. Problem a -> Problem b -> Problem a
*> :: Problem a -> Problem b -> Problem b
$c*> :: forall a b. Problem a -> Problem b -> Problem b
liftA2 :: (a -> b -> c) -> Problem a -> Problem b -> Problem c
$cliftA2 :: forall a b c. (a -> b -> c) -> Problem a -> Problem b -> Problem c
<*> :: Problem (a -> b) -> Problem a -> Problem b
$c<*> :: forall a b. Problem (a -> b) -> Problem a -> Problem b
pure :: a -> Problem a
$cpure :: forall a. a -> Problem a
$cp1Applicative :: Functor Problem
Applicative, Applicative Problem
a -> Problem a
Applicative Problem
-> (forall a b. Problem a -> (a -> Problem b) -> Problem b)
-> (forall a b. Problem a -> Problem b -> Problem b)
-> (forall a. a -> Problem a)
-> Monad Problem
Problem a -> (a -> Problem b) -> Problem b
Problem a -> Problem b -> Problem b
forall a. a -> Problem a
forall a b. Problem a -> Problem b -> Problem b
forall a b. Problem a -> (a -> Problem b) -> Problem 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 -> Problem a
$creturn :: forall a. a -> Problem a
>> :: Problem a -> Problem b -> Problem b
$c>> :: forall a b. Problem a -> Problem b -> Problem b
>>= :: Problem a -> (a -> Problem b) -> Problem b
$c>>= :: forall a b. Problem a -> (a -> Problem b) -> Problem b
$cp1Monad :: Applicative Problem
Monad, Monad Problem
Monad Problem -> (forall a. IO a -> Problem a) -> MonadIO Problem
IO a -> Problem a
forall a. IO a -> Problem a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: IO a -> Problem a
$cliftIO :: forall a. IO a -> Problem a
$cp1MonadIO :: Monad Problem
MonadIO )


-- | Information needed to translate a 'Var' into its SAS equivalance.
data VariableDeclaration =
  VariableDeclaration
    { VariableDeclaration -> DomainIndex
initial :: {-# UNPACK #-} !FastDownward.SAS.DomainIndex
      -- ^ The index of the initial (starting) value.
    , VariableDeclaration -> IO [DomainIndex]
_enumerateDomain :: IO [ FastDownward.SAS.DomainIndex ]
      -- ^ List all values this variable can take.
    , VariableDeclaration -> Int
_axiomLayer :: {-# UNPACK #-} !Int
      -- ^ The axiom layer of this variable. Most variables live at -1, derived
      -- variables at higher layers.
    }


-- | The state used to translate a 'Problem' its SAS equivalance.
data ProblemState =
  ProblemState
    { ProblemState -> Map VariableIndex VariableDeclaration
initialState :: !( Map FastDownward.SAS.VariableIndex VariableDeclaration )
      -- ^ A table of variables, indexed by their apperance in the SAS variable
      -- list.
    , ProblemState -> Seq Axiom
axioms :: !( Seq FastDownward.SAS.Axiom )
      -- ^ A list of derived axioms.
    }


-- | Observe that a 'Var' can take a particular value.
observeValue :: ( Ord a, MonadIO m ) => Var a -> a -> m FastDownward.SAS.DomainIndex
observeValue :: Var a -> a -> m DomainIndex
observeValue Var a
var a
a = IO DomainIndex -> m DomainIndex
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO DomainIndex -> m DomainIndex)
-> IO DomainIndex -> m DomainIndex
forall a b. (a -> b) -> a -> b
$ do
  Map a (Committed, DomainIndex)
vs <-
    IORef (Map a (Committed, DomainIndex))
-> IO (Map a (Committed, DomainIndex))
forall a. IORef a -> IO a
readIORef ( Var a -> IORef (Map a (Committed, DomainIndex))
forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var )

  case a
-> Map a (Committed, DomainIndex) -> Maybe (Committed, DomainIndex)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a (Committed, DomainIndex)
vs of
    Just ( Committed
_, DomainIndex
i ) ->
      DomainIndex -> IO DomainIndex
forall (m :: * -> *) a. Monad m => a -> m a
return DomainIndex
i

    Maybe (Committed, DomainIndex)
Nothing -> do
      let
        i :: DomainIndex
i =
          Int -> DomainIndex
FastDownward.SAS.DomainIndex ( Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral ( Map a (Committed, DomainIndex) -> Int
forall k a. Map k a -> Int
Map.size Map a (Committed, DomainIndex)
vs ) )

      IORef (Map DomainIndex a)
-> (Map DomainIndex a -> Map DomainIndex a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef ( Var a -> IORef (Map DomainIndex a)
forall a. Var a -> IORef (Map DomainIndex a)
fromDomainIndex Var a
var ) ( DomainIndex -> a -> Map DomainIndex a -> Map DomainIndex a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert DomainIndex
i a
a )

      DomainIndex
i DomainIndex -> IO () -> IO DomainIndex
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IORef (Map a (Committed, DomainIndex))
-> (Map a (Committed, DomainIndex)
    -> Map a (Committed, DomainIndex))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef ( Var a -> IORef (Map a (Committed, DomainIndex))
forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var ) ( a
-> (Committed, DomainIndex)
-> Map a (Committed, DomainIndex)
-> Map a (Committed, DomainIndex)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert a
a ( Committed
Uncommitted, DomainIndex
i ) )


commit :: ( Ord a, MonadIO m ) => Var a -> a -> m ()
commit :: Var a -> a -> m ()
commit Var a
var a
a = IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
  IORef (Map a (Committed, DomainIndex))
-> (Map a (Committed, DomainIndex)
    -> Map a (Committed, DomainIndex))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef ( Var a -> IORef (Map a (Committed, DomainIndex))
forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var ) ( ((Committed, DomainIndex) -> (Committed, DomainIndex))
-> a
-> Map a (Committed, DomainIndex)
-> Map a (Committed, DomainIndex)
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust ( \( Committed
_, DomainIndex
x ) -> ( Committed
Committed, DomainIndex
x ) ) a
a )


-- | Introduce a new state variable into a problem, and set it to an initial
-- starting value.
newVar :: Ord a => a -> Problem ( Var a )
newVar :: a -> Problem (Var a)
newVar =
  Int -> a -> Problem (Var a)
forall a. Ord a => Int -> a -> Problem (Var a)
newVarAt (-Int
1)


-- | Introduce a new state variable into a problem at a particular axiom layer.
newVarAt :: Ord a => Int -> a -> Problem ( Var a )
newVarAt :: Int -> a -> Problem (Var a)
newVarAt Int
axiomLayer a
initialValue = do
  -- Allocate the domain IORef
  IORef (Map a (Committed, DomainIndex))
values <-
    IO (IORef (Map a (Committed, DomainIndex)))
-> Problem (IORef (Map a (Committed, DomainIndex)))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( Map a (Committed, DomainIndex)
-> IO (IORef (Map a (Committed, DomainIndex)))
forall a. a -> IO (IORef a)
newIORef Map a (Committed, DomainIndex)
forall a. Monoid a => a
mempty )

  -- Lookup an unused index for this variable.
  VariableIndex
variableIndex <-
    Problem VariableIndex
freshIndex

  IORef (a -> DomainIndex -> IO ())
subscribed <-
    IO (IORef (a -> DomainIndex -> IO ()))
-> Problem (IORef (a -> DomainIndex -> IO ()))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( (a -> DomainIndex -> IO ())
-> IO (IORef (a -> DomainIndex -> IO ()))
forall a. a -> IO (IORef a)
newIORef ( \a
_ DomainIndex
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () ) )

  IORef (Map DomainIndex a)
fromDomainIndex <-
    IO (IORef (Map DomainIndex a))
-> Problem (IORef (Map DomainIndex a))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( Map DomainIndex a -> IO (IORef (Map DomainIndex a))
forall a. a -> IO (IORef a)
newIORef Map DomainIndex a
forall a. Monoid a => a
mempty )

  let
    enumerate :: IO [DomainIndex]
enumerate =
      ((Committed, DomainIndex) -> DomainIndex)
-> [(Committed, DomainIndex)] -> [DomainIndex]
forall a b. (a -> b) -> [a] -> [b]
map (Committed, DomainIndex) -> DomainIndex
forall a b. (a, b) -> b
snd ([(Committed, DomainIndex)] -> [DomainIndex])
-> (Map a (Committed, DomainIndex) -> [(Committed, DomainIndex)])
-> Map a (Committed, DomainIndex)
-> [DomainIndex]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (Committed, DomainIndex) -> [(Committed, DomainIndex)]
forall k a. Map k a -> [a]
Map.elems (Map a (Committed, DomainIndex) -> [DomainIndex])
-> IO (Map a (Committed, DomainIndex)) -> IO [DomainIndex]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Map a (Committed, DomainIndex))
-> IO (Map a (Committed, DomainIndex))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( IORef (Map a (Committed, DomainIndex))
-> IO (Map a (Committed, DomainIndex))
forall a. IORef a -> IO a
readIORef IORef (Map a (Committed, DomainIndex))
values )

    var :: Var a
var =
      Var :: forall a.
VariableIndex
-> IORef (Map a (Committed, DomainIndex))
-> IORef (a -> DomainIndex -> IO ())
-> IORef (Map DomainIndex a)
-> Var a
Var{IORef (Map a (Committed, DomainIndex))
IORef (Map DomainIndex a)
IORef (a -> DomainIndex -> IO ())
VariableIndex
fromDomainIndex :: IORef (Map DomainIndex a)
subscribed :: IORef (a -> DomainIndex -> IO ())
variableIndex :: VariableIndex
values :: IORef (Map a (Committed, DomainIndex))
fromDomainIndex :: IORef (Map DomainIndex a)
subscribed :: IORef (a -> DomainIndex -> IO ())
values :: IORef (Map a (Committed, DomainIndex))
variableIndex :: VariableIndex
..}

  -- Observe the initial value...
  DomainIndex
initialI <-
    Var a -> a -> Problem DomainIndex
forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var a
var a
initialValue

  Var a -> a -> Problem ()
forall a (m :: * -> *). (Ord a, MonadIO m) => Var a -> a -> m ()
commit Var a
var a
initialValue

  -- ... and record it in the ProblemState.
  StateT ProblemState IO () -> Problem ()
forall a. StateT ProblemState IO a -> Problem a
Problem
    ( (ProblemState -> ProblemState) -> StateT ProblemState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify
        ( \ProblemState
ps ->
            ProblemState
ps
              { initialState :: Map VariableIndex VariableDeclaration
initialState =
                  VariableIndex
-> VariableDeclaration
-> Map VariableIndex VariableDeclaration
-> Map VariableIndex VariableDeclaration
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
                    VariableIndex
variableIndex
                    ( DomainIndex -> IO [DomainIndex] -> Int -> VariableDeclaration
VariableDeclaration DomainIndex
initialI IO [DomainIndex]
enumerate Int
axiomLayer )
                    ( ProblemState -> Map VariableIndex VariableDeclaration
initialState ProblemState
ps )
              }
        )
    )

  Var a -> Problem (Var a)
forall (m :: * -> *) a. Monad m => a -> m a
return Var a
var


-- | Lookup the next unused variable index.
freshIndex :: Problem FastDownward.SAS.VariableIndex
freshIndex :: Problem VariableIndex
freshIndex =
  Int -> VariableIndex
FastDownward.SAS.VariableIndex (Int -> VariableIndex) -> Problem Int -> Problem VariableIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ProblemState IO Int -> Problem Int
forall a. StateT ProblemState IO a -> Problem a
Problem ( (ProblemState -> Int) -> StateT ProblemState IO Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ( Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (ProblemState -> Int) -> ProblemState -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map VariableIndex VariableDeclaration -> Int
forall k a. Map k a -> Int
Map.size (Map VariableIndex VariableDeclaration -> Int)
-> (ProblemState -> Map VariableIndex VariableDeclaration)
-> ProblemState
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProblemState -> Map VariableIndex VariableDeclaration
initialState ) )


-- | Write a value into 'Var'. If the solver choses to use this particular
-- 'Effect', then the @Var@ will begin take this new value.
writeVar :: Ord a => Var a -> a -> Effect ()
writeVar :: Var a -> a -> Effect ()
writeVar Var a
var a
a = ContT () (ReaderT EffectState IO) () -> Effect ()
forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect (ContT () (ReaderT EffectState IO) () -> Effect ())
-> ContT () (ReaderT EffectState IO) () -> Effect ()
forall a b. (a -> b) -> a -> b
$ do
  -- Writing a variable is fairly simple. First, we check what values the
  -- variable has already taken. If the value we're writing is in that set, then
  -- there's not much to do - we've already considered this assignment.
  --
  -- If the value is new, we record that this write invalidated a Var, which
  -- will cause exhaustEffects to run again.
  Either DomainIndex DomainIndex
edomainIndex <- IO (Either DomainIndex DomainIndex)
-> ContT
     () (ReaderT EffectState IO) (Either DomainIndex DomainIndex)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either DomainIndex DomainIndex)
 -> ContT
      () (ReaderT EffectState IO) (Either DomainIndex DomainIndex))
-> IO (Either DomainIndex DomainIndex)
-> ContT
     () (ReaderT EffectState IO) (Either DomainIndex DomainIndex)
forall a b. (a -> b) -> a -> b
$ do
    Map a (Committed, DomainIndex)
currentValues <-
      IORef (Map a (Committed, DomainIndex))
-> IO (Map a (Committed, DomainIndex))
forall a. IORef a -> IO a
readIORef ( Var a -> IORef (Map a (Committed, DomainIndex))
forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var )

    case a
-> Map a (Committed, DomainIndex) -> Maybe (Committed, DomainIndex)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a (Committed, DomainIndex)
currentValues of
      Just ( Committed
Committed, DomainIndex
domainIndex ) ->
        Either DomainIndex DomainIndex
-> IO (Either DomainIndex DomainIndex)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DomainIndex -> Either DomainIndex DomainIndex
forall a b. b -> Either a b
Right DomainIndex
domainIndex )

      Just ( Committed
Uncommitted, DomainIndex
domainIndex ) ->
        Either DomainIndex DomainIndex
-> IO (Either DomainIndex DomainIndex)
forall (m :: * -> *) a. Monad m => a -> m a
return ( DomainIndex -> Either DomainIndex DomainIndex
forall a b. a -> Either a b
Left DomainIndex
domainIndex )

      Maybe (Committed, DomainIndex)
Nothing -> do
        -- We've never seen this value before, first observe it to obtain
        -- its domain index.
        DomainIndex -> Either DomainIndex DomainIndex
forall a b. a -> Either a b
Left (DomainIndex -> Either DomainIndex DomainIndex)
-> IO DomainIndex -> IO (Either DomainIndex DomainIndex)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var a -> a -> IO DomainIndex
forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var a
var a
a

  ((() -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
-> ContT () (ReaderT EffectState IO) ()
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((() -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
 -> ContT () (ReaderT EffectState IO) ())
-> ((() -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
-> ContT () (ReaderT EffectState IO) ()
forall a b. (a -> b) -> a -> b
$ \() -> ReaderT EffectState IO ()
k -> (EffectState -> IO ()) -> ReaderT EffectState IO ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((EffectState -> IO ()) -> ReaderT EffectState IO ())
-> (EffectState -> IO ()) -> ReaderT EffectState IO ()
forall a b. (a -> b) -> a -> b
$ \EffectState
es -> do
    EffectState
es' <-
      case Either DomainIndex DomainIndex
edomainIndex of
        Left DomainIndex
domainIndex -> do
          -- We just discovered a new value, so we'll broadcast this.
          IORef (IO ())
laterRef <-
            IO () -> IO (IORef (IO ()))
forall a. a -> IO (IORef a)
newIORef (IO () -> IO (IORef (IO ()))) -> IO () -> IO (IORef (IO ()))
forall a b. (a -> b) -> a -> b
$ do
              Map a (Committed, DomainIndex)
currentValues <-
                IORef (Map a (Committed, DomainIndex))
-> IO (Map a (Committed, DomainIndex))
forall a. IORef a -> IO a
readIORef ( Var a -> IORef (Map a (Committed, DomainIndex))
forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var )

              case a
-> Map a (Committed, DomainIndex) -> Maybe (Committed, DomainIndex)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
a Map a (Committed, DomainIndex)
currentValues of
                Just ( Committed
Committed, DomainIndex
_ ) ->
                  () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

                Maybe (Committed, DomainIndex)
_ -> do
                  Var a -> a -> IO ()
forall a (m :: * -> *). (Ord a, MonadIO m) => Var a -> a -> m ()
commit Var a
var a
a

                  a -> DomainIndex -> IO ()
notify <-
                    IORef (a -> DomainIndex -> IO ()) -> IO (a -> DomainIndex -> IO ())
forall a. IORef a -> IO a
readIORef ( Var a -> IORef (a -> DomainIndex -> IO ())
forall a. Var a -> IORef (a -> DomainIndex -> IO ())
subscribed Var a
var )

                  a -> DomainIndex -> IO ()
notify a
a DomainIndex
domainIndex

          EffectState -> IO EffectState
forall (m :: * -> *) a. Monad m => a -> m a
return
            EffectState
es
              { writes :: IntMap DomainIndex
writes =
                  Int -> DomainIndex -> IntMap DomainIndex -> IntMap DomainIndex
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert ( VariableIndex -> Int
coerce ( Var a -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) DomainIndex
domainIndex ( EffectState -> IntMap DomainIndex
writes EffectState
es )
              , onCommit :: IO ()
onCommit = do
                  IO ()
action <-
                    IORef (IO ()) -> IO (IO ())
forall a. IORef a -> IO a
readIORef IORef (IO ())
laterRef

                  IORef (IO ()) -> IO () -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (IO ())
laterRef ( () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () )
                    IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
action
                    IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> EffectState -> IO ()
onCommit EffectState
es
              }

        Right DomainIndex
domainIndex ->
          -- This is not a new value, so just record it and continue.
          EffectState -> IO EffectState
forall (m :: * -> *) a. Monad m => a -> m a
return
            EffectState
es
              { writes :: IntMap DomainIndex
writes =
                  Int -> DomainIndex -> IntMap DomainIndex -> IntMap DomainIndex
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert ( VariableIndex -> Int
coerce ( Var a -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) DomainIndex
domainIndex ( EffectState -> IntMap DomainIndex
writes EffectState
es )
              }

    ReaderT EffectState IO () -> EffectState -> IO ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ( () -> ReaderT EffectState IO ()
k () ) EffectState
es'


-- | Read the value of a 'Var' at the point the 'Effect' is invoked by the
-- solver.
readVar :: Ord a => Var a -> Effect a
readVar :: Var a -> Effect a
readVar Var a
var = ContT () (ReaderT EffectState IO) a -> Effect a
forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect (ContT () (ReaderT EffectState IO) a -> Effect a)
-> ContT () (ReaderT EffectState IO) a -> Effect a
forall a b. (a -> b) -> a -> b
$ ((a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
-> ContT () (ReaderT EffectState IO) a
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
 -> ContT () (ReaderT EffectState IO) a)
-> ((a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
-> ContT () (ReaderT EffectState IO) a
forall a b. (a -> b) -> a -> b
$ \a -> ReaderT EffectState IO ()
k -> (EffectState -> IO ()) -> ReaderT EffectState IO ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((EffectState -> IO ()) -> ReaderT EffectState IO ())
-> (EffectState -> IO ()) -> ReaderT EffectState IO ()
forall a b. (a -> b) -> a -> b
$ \EffectState
es -> do
  -- To "read" a variable is actually to read *all* of its values
  -- non-deterministically. The first time the Var v1 is read, we enumerate it
  -- and run the continuation with all values. However, in this continuation a
  -- subsquent read from v1 should be stable - that is, deterministic. This
  -- is done by consulting the 'reads' map of prior reads first.
  -- Furthermore, if this variable has been written too, we re-read the last
  -- write.
  let
    mPrevRead :: Maybe DomainIndex
mPrevRead =
      Int -> IntMap DomainIndex -> Maybe DomainIndex
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup ( VariableIndex -> Int
coerce ( Var a -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) ( EffectState -> IntMap DomainIndex
reads EffectState
es )

    mPrevWrite :: Maybe DomainIndex
mPrevWrite =
      Int -> IntMap DomainIndex -> Maybe DomainIndex
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup ( VariableIndex -> Int
coerce ( Var a -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) ( EffectState -> IntMap DomainIndex
writes EffectState
es )

  case ( Maybe DomainIndex
mPrevWrite, Maybe DomainIndex
mPrevRead ) of
    ( Just DomainIndex
prevWriteIndex, Maybe DomainIndex
_ ) -> do
      -- We've written this variable, so continue with what we last wrote.
      a
prevWrite <-
        ( Map DomainIndex a -> DomainIndex -> a
forall k a. Ord k => Map k a -> k -> a
Map.! DomainIndex
prevWriteIndex ) (Map DomainIndex a -> a) -> IO (Map DomainIndex a) -> IO a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map DomainIndex a) -> IO (Map DomainIndex a)
forall a. IORef a -> IO a
readIORef ( Var a -> IORef (Map DomainIndex a)
forall a. Var a -> IORef (Map DomainIndex a)
fromDomainIndex Var a
var )

      ReaderT EffectState IO () -> EffectState -> IO ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ( a -> ReaderT EffectState IO ()
k a
prevWrite ) EffectState
es

    ( Maybe DomainIndex
Nothing, Just DomainIndex
prevReadIndex ) -> do
      -- We've seen this variable before, so just continue with it.
      a
prevRead <-
        ( Map DomainIndex a -> DomainIndex -> a
forall k a. Ord k => Map k a -> k -> a
Map.! DomainIndex
prevReadIndex ) (Map DomainIndex a -> a) -> IO (Map DomainIndex a) -> IO a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map DomainIndex a) -> IO (Map DomainIndex a)
forall a. IORef a -> IO a
readIORef ( Var a -> IORef (Map DomainIndex a)
forall a. Var a -> IORef (Map DomainIndex a)
fromDomainIndex Var a
var )

      ReaderT EffectState IO () -> EffectState -> IO ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ( a -> ReaderT EffectState IO ()
k a
prevRead ) EffectState
es

    ( Maybe DomainIndex
Nothing, Maybe DomainIndex
Nothing ) -> do
      -- We have never seen this variable before.
      let
        runRecordingRead :: a -> DomainIndex -> IO ()
runRecordingRead a
a DomainIndex
domainIndex =
          let
            es' :: EffectState
es' =
              EffectState
es
                { reads :: IntMap DomainIndex
reads =
                    Int -> DomainIndex -> IntMap DomainIndex -> IntMap DomainIndex
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert ( VariableIndex -> Int
coerce ( Var a -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) DomainIndex
domainIndex ( EffectState -> IntMap DomainIndex
reads EffectState
es )
                }

          in ReaderT EffectState IO () -> EffectState -> IO ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ( a -> ReaderT EffectState IO ()
k a
a ) EffectState
es'

      Map a (Committed, DomainIndex)
currentValues <-
        IORef (Map a (Committed, DomainIndex))
-> IO (Map a (Committed, DomainIndex))
forall a. IORef a -> IO a
readIORef ( Var a -> IORef (Map a (Committed, DomainIndex))
forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var )

      -- First, subscribe to any new writes. This has to be done first because
      -- yielding known values could immediately cause a write to happen
      -- (e.g., in the case of using modifyVar = readVar v >>= writeVar . f).
      IORef (a -> DomainIndex -> IO ())
-> ((a -> DomainIndex -> IO ()) -> a -> DomainIndex -> IO ())
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef
        ( Var a -> IORef (a -> DomainIndex -> IO ())
forall a. Var a -> IORef (a -> DomainIndex -> IO ())
subscribed Var a
var )
        ( \a -> DomainIndex -> IO ()
io a
x DomainIndex
y -> a -> DomainIndex -> IO ()
runRecordingRead a
x DomainIndex
y IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> a -> DomainIndex -> IO ()
io a
x DomainIndex
y )

      -- Now enumerate all known reads.
      (a -> (Committed, DomainIndex) -> IO ())
-> Map a (Committed, DomainIndex) -> IO ()
forall m k a. Monoid m => (k -> a -> m) -> Map k a -> m
Map.foldMapWithKey
        ( \a
a ( Committed
committed, DomainIndex
domainIndex ) ->
            case Committed
committed of
              Committed
Committed ->
                a -> DomainIndex -> IO ()
runRecordingRead a
a DomainIndex
domainIndex

              Committed
_ ->
                () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        )
        Map a (Committed, DomainIndex)
currentValues


-- | Modify the contents of a 'Var' by using a function.
--
-- @modifyVar v f = readVar v >>= writeVar v . f@
modifyVar :: Ord a => Var a -> ( a -> a ) -> Effect ()
modifyVar :: Var a -> (a -> a) -> Effect ()
modifyVar Var a
v a -> a
f =
  Var a -> Effect a
forall a. Ord a => Var a -> Effect a
readVar Var a
v Effect a -> (a -> Effect ()) -> Effect ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Var a -> a -> Effect ()
forall a. Ord a => Var a -> a -> Effect ()
writeVar Var a
v (a -> Effect ()) -> (a -> a) -> a -> Effect ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
f


-- | An 'Effect' is a transition in a planning problem - a point where variables
-- can be inspected for their current values, and where they can take on new
-- values. For example, there might be an @Effect@ to instruct the robot to
-- move to a particular target location, if its current location is adjacent.
--
-- The @Effect@ monad supports failure, so you can 'guard' an @Effect@ to only
-- be applicable under particular circumstances. Continuing the above example,
-- we loosely mentioned the constraint that the robot must be adjacent to a
-- target location - something that could be modelled by using 'readVar' to
-- read the current location, and 'guard' to guard that this location is
-- adjacent to our goal.
newtype Effect a =
  Effect { Effect a -> ContT () (ReaderT EffectState IO) a
runEffect :: ContT () ( ReaderT EffectState IO ) a }
  deriving
    ( a -> Effect b -> Effect a
(a -> b) -> Effect a -> Effect b
(forall a b. (a -> b) -> Effect a -> Effect b)
-> (forall a b. a -> Effect b -> Effect a) -> Functor Effect
forall a b. a -> Effect b -> Effect a
forall a b. (a -> b) -> Effect a -> Effect b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Effect b -> Effect a
$c<$ :: forall a b. a -> Effect b -> Effect a
fmap :: (a -> b) -> Effect a -> Effect b
$cfmap :: forall a b. (a -> b) -> Effect a -> Effect b
Functor, Functor Effect
a -> Effect a
Functor Effect
-> (forall a. a -> Effect a)
-> (forall a b. Effect (a -> b) -> Effect a -> Effect b)
-> (forall a b c.
    (a -> b -> c) -> Effect a -> Effect b -> Effect c)
-> (forall a b. Effect a -> Effect b -> Effect b)
-> (forall a b. Effect a -> Effect b -> Effect a)
-> Applicative Effect
Effect a -> Effect b -> Effect b
Effect a -> Effect b -> Effect a
Effect (a -> b) -> Effect a -> Effect b
(a -> b -> c) -> Effect a -> Effect b -> Effect c
forall a. a -> Effect a
forall a b. Effect a -> Effect b -> Effect a
forall a b. Effect a -> Effect b -> Effect b
forall a b. Effect (a -> b) -> Effect a -> Effect b
forall a b c. (a -> b -> c) -> Effect a -> Effect b -> Effect 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
<* :: Effect a -> Effect b -> Effect a
$c<* :: forall a b. Effect a -> Effect b -> Effect a
*> :: Effect a -> Effect b -> Effect b
$c*> :: forall a b. Effect a -> Effect b -> Effect b
liftA2 :: (a -> b -> c) -> Effect a -> Effect b -> Effect c
$cliftA2 :: forall a b c. (a -> b -> c) -> Effect a -> Effect b -> Effect c
<*> :: Effect (a -> b) -> Effect a -> Effect b
$c<*> :: forall a b. Effect (a -> b) -> Effect a -> Effect b
pure :: a -> Effect a
$cpure :: forall a. a -> Effect a
$cp1Applicative :: Functor Effect
Applicative )


instance Monad Effect where
  return :: a -> Effect a
return a
a =
    ContT () (ReaderT EffectState IO) a -> Effect a
forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect ( a -> ContT () (ReaderT EffectState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a )
  {-# INLINE return #-}

  Effect ContT () (ReaderT EffectState IO) a
a >>= :: Effect a -> (a -> Effect b) -> Effect b
>>= a -> Effect b
f = ContT () (ReaderT EffectState IO) b -> Effect b
forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect (ContT () (ReaderT EffectState IO) b -> Effect b)
-> ContT () (ReaderT EffectState IO) b -> Effect b
forall a b. (a -> b) -> a -> b
$
    ContT () (ReaderT EffectState IO) a
a ContT () (ReaderT EffectState IO) a
-> (a -> ContT () (ReaderT EffectState IO) b)
-> ContT () (ReaderT EffectState IO) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Effect b -> ContT () (ReaderT EffectState IO) b
forall a. Effect a -> ContT () (ReaderT EffectState IO) a
runEffect (Effect b -> ContT () (ReaderT EffectState IO) b)
-> (a -> Effect b) -> a -> ContT () (ReaderT EffectState IO) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Effect b
f
  {-# INLINE (>>=) #-}


instance Control.Monad.Fail.MonadFail Effect where
  fail :: String -> Effect a
fail String
_ =
    Effect a
forall (f :: * -> *) a. Alternative f => f a
empty
  {-# INLINE fail #-}


instance Alternative Effect where
  empty :: Effect a
empty =
    ContT () (ReaderT EffectState IO) a -> Effect a
forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect ( ((a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
-> ContT () (ReaderT EffectState IO) a
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT ( \a -> ReaderT EffectState IO ()
_k -> () -> ReaderT EffectState IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () ) )
  {-# INLINE empty #-}

  Effect ContT () (ReaderT EffectState IO) a
a <|> :: Effect a -> Effect a -> Effect a
<|> Effect ContT () (ReaderT EffectState IO) a
b =
    ContT () (ReaderT EffectState IO) a -> Effect a
forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect (ContT () (ReaderT EffectState IO) a -> Effect a)
-> ContT () (ReaderT EffectState IO) a -> Effect a
forall a b. (a -> b) -> a -> b
$ ((a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
-> ContT () (ReaderT EffectState IO) a
forall k (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT (((a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
 -> ContT () (ReaderT EffectState IO) a)
-> ((a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ())
-> ContT () (ReaderT EffectState IO) a
forall a b. (a -> b) -> a -> b
$ \a -> ReaderT EffectState IO ()
k ->
      ContT () (ReaderT EffectState IO) a
-> (a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ()
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT ContT () (ReaderT EffectState IO) a
a a -> ReaderT EffectState IO ()
k ReaderT EffectState IO ()
-> ReaderT EffectState IO () -> ReaderT EffectState IO ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ContT () (ReaderT EffectState IO) a
-> (a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ()
forall k (r :: k) (m :: k -> *) a. ContT r m a -> (a -> m r) -> m r
runContT ContT () (ReaderT EffectState IO) a
b a -> ReaderT EffectState IO ()
k
  {-# INLINE (<|>) #-}


-- | Used to track the evaluation of an 'Effect' as we enumerate all possible
-- outcomes.
data EffectState =
  EffectState
    { EffectState -> IntMap DomainIndex
reads :: IntMap FastDownward.SAS.DomainIndex
      -- ^ The variables and their exact values read to reach a certain outcome.
    , EffectState -> IntMap DomainIndex
writes :: IntMap FastDownward.SAS.DomainIndex
      -- ^ The changes made by this instance.
    , EffectState -> IO ()
onCommit :: IO ()
    }


-- | The result from the solver on a call to 'solve'.
data SolveResult a
  = Unsolvable
    -- ^ The problem was proven to be unsolvable.
  | UnsolvableIncomplete
    -- ^ The problem was determined to be unsolvable, but the entire search
    -- space was not explored.
  | OutOfMemory
    -- ^ The @downward@ executable ran out of memory.
  | OutOfTime
    -- ^ The @downward@ executable ran out of time.
  | CriticalError
    -- ^ The @downward@ executable encountered a critical error.
  | InputError
    -- ^ The @downward@ executable encountered an error parsing input.
  | Unsupported
    -- ^ The @downward@ executable was called with a search engine that is
    -- incompatible with the problem definition.
  | Crashed String String ExitCode
    -- ^ Fast Downward crashed (or otherwise rejected) the given problem.
  | Solved ( Solution a )
    -- ^ A solution was found.
  deriving
    ( a -> SolveResult b -> SolveResult a
(a -> b) -> SolveResult a -> SolveResult b
(forall a b. (a -> b) -> SolveResult a -> SolveResult b)
-> (forall a b. a -> SolveResult b -> SolveResult a)
-> Functor SolveResult
forall a b. a -> SolveResult b -> SolveResult a
forall a b. (a -> b) -> SolveResult a -> SolveResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SolveResult b -> SolveResult a
$c<$ :: forall a b. a -> SolveResult b -> SolveResult a
fmap :: (a -> b) -> SolveResult a -> SolveResult b
$cfmap :: forall a b. (a -> b) -> SolveResult a -> SolveResult b
Functor, Int -> SolveResult a -> ShowS
[SolveResult a] -> ShowS
SolveResult a -> String
(Int -> SolveResult a -> ShowS)
-> (SolveResult a -> String)
-> ([SolveResult a] -> ShowS)
-> Show (SolveResult a)
forall a. Show a => Int -> SolveResult a -> ShowS
forall a. Show a => [SolveResult a] -> ShowS
forall a. Show a => SolveResult a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolveResult a] -> ShowS
$cshowList :: forall a. Show a => [SolveResult a] -> ShowS
show :: SolveResult a -> String
$cshow :: forall a. Show a => SolveResult a -> String
showsPrec :: Int -> SolveResult a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> SolveResult a -> ShowS
Show )


-- | A successful solution to a planning problem. You can unpack a @Solution@
-- into a plan by using 'totallyOrderedPlan' and 'partiallyOrderedPlan'.
data Solution a =
  Solution
    { Solution a -> Plan
sas :: FastDownward.SAS.Plan
    , Solution a -> IntMap a
operators :: IntMap.IntMap a
    , Solution a -> [Int]
stepIndices :: [ IntMap.Key ]
    }
  deriving
    ( a -> Solution b -> Solution a
(a -> b) -> Solution a -> Solution b
(forall a b. (a -> b) -> Solution a -> Solution b)
-> (forall a b. a -> Solution b -> Solution a) -> Functor Solution
forall a b. a -> Solution b -> Solution a
forall a b. (a -> b) -> Solution a -> Solution b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Solution b -> Solution a
$c<$ :: forall a b. a -> Solution b -> Solution a
fmap :: (a -> b) -> Solution a -> Solution b
$cfmap :: forall a b. (a -> b) -> Solution a -> Solution b
Functor, Int -> Solution a -> ShowS
[Solution a] -> ShowS
Solution a -> String
(Int -> Solution a -> ShowS)
-> (Solution a -> String)
-> ([Solution a] -> ShowS)
-> Show (Solution a)
forall a. Show a => Int -> Solution a -> ShowS
forall a. Show a => [Solution a] -> ShowS
forall a. Show a => Solution a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Solution a] -> ShowS
$cshowList :: forall a. Show a => [Solution a] -> ShowS
show :: Solution a -> String
$cshow :: forall a. Show a => Solution a -> String
showsPrec :: Int -> Solution a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Solution a -> ShowS
Show )


-- | Extract a totally ordered plan from a solution.
totallyOrderedPlan :: Solution a -> [ a ]
totallyOrderedPlan :: Solution a -> [a]
totallyOrderedPlan Solution{[Int]
IntMap a
Plan
stepIndices :: [Int]
operators :: IntMap a
sas :: Plan
stepIndices :: forall a. Solution a -> [Int]
operators :: forall a. Solution a -> IntMap a
sas :: forall a. Solution a -> Plan
..} =
  (Int -> a) -> [Int] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ( IntMap a
operators IntMap a -> Int -> a
forall a. IntMap a -> Int -> a
IntMap.! ) [Int]
stepIndices


-- | Given a particular 'Exec.SearchEngine', attempt to solve a planning
-- problem.
solve
  :: Show a
  => Exec.SearchConfiguration
  -> [ Effect a ]
     -- ^ The set of effects available to the planner. Each effect can return
     -- some domain-specific information of type @a@ which you can use to
     -- interpret the plan. This will usually be some kind of @Action@ type.
  -> [ Test ]
     -- ^ A conjunction of tests that must true for a solution to be considered
     -- acceptable.
  -> Problem ( SolveResult a )
     -- ^ The list of steps that will converge the initial state to a state that
     -- satisfies the given goal predicates.
solve :: SearchConfiguration
-> [Effect a] -> [Test] -> Problem (SolveResult a)
solve SearchConfiguration
cfg [Effect a]
ops [Test]
tests = do
  -- It's convenient to work in the 'Problem' monad, but we don't want to dirty
  -- the state. (E.g., maybe the user will want to call @solve@ again with
  -- something that doesn't require axioms derived to satisfy the first calls
  -- 'Test').
  ProblemState
s0 <-
    StateT ProblemState IO ProblemState -> Problem ProblemState
forall a. StateT ProblemState IO a -> Problem a
Problem StateT ProblemState IO ProblemState
forall s (m :: * -> *). MonadState s m => m s
get

  StateT ProblemState IO (SolveResult a) -> Problem (SolveResult a)
forall a. StateT ProblemState IO a -> Problem a
Problem (StateT ProblemState IO (SolveResult a) -> Problem (SolveResult a))
-> StateT ProblemState IO (SolveResult a)
-> Problem (SolveResult a)
forall a b. (a -> b) -> a -> b
$ IO (SolveResult a) -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SolveResult a) -> StateT ProblemState IO (SolveResult a))
-> IO (SolveResult a) -> StateT ProblemState IO (SolveResult a)
forall a b. (a -> b) -> a -> b
$ (StateT ProblemState IO (SolveResult a)
 -> ProblemState -> IO (SolveResult a))
-> ProblemState
-> StateT ProblemState IO (SolveResult a)
-> IO (SolveResult a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip StateT ProblemState IO (SolveResult a)
-> ProblemState -> IO (SolveResult a)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ProblemState
s0 (StateT ProblemState IO (SolveResult a) -> IO (SolveResult a))
-> StateT ProblemState IO (SolveResult a) -> IO (SolveResult a)
forall a b. (a -> b) -> a -> b
$ do
    -- First, convert the given goal into a list of variable assignments. This
    -- will also introduce axioms for conjunctions, and will observe all test
    -- variable values.
    [VariableAssignment]
goal <-
      Problem [VariableAssignment]
-> StateT ProblemState IO [VariableAssignment]
forall a. Problem a -> StateT ProblemState IO a
unProblem ( (Test -> Problem VariableAssignment)
-> [Test] -> Problem [VariableAssignment]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
Prelude.traverse Test -> Problem VariableAssignment
testToVariableAssignment [Test]
tests )

    -- Now that we've observed every value we know up-front, find the fixed point
    -- of the set of operators.
    [(a, EffectState)]
operators <-
      IO [(a, EffectState)] -> StateT ProblemState IO [(a, EffectState)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( [Effect a] -> IO [(a, EffectState)]
forall (t :: * -> *) a.
Traversable t =>
t (Effect a) -> IO [(a, EffectState)]
exhaustEffects [Effect a]
ops )

    Map VariableIndex VariableDeclaration
initialState <-
      (ProblemState -> Map VariableIndex VariableDeclaration)
-> StateT ProblemState IO (Map VariableIndex VariableDeclaration)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ProblemState -> Map VariableIndex VariableDeclaration
initialState

    Seq Axiom
axioms <-
      (ProblemState -> Seq Axiom) -> StateT ProblemState IO (Seq Axiom)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ProblemState -> Seq Axiom
axioms

    -- For all variables, convert them into a SAS-compatible list.
    [Variable]
variables <-
      [(VariableIndex, VariableDeclaration)]
-> ((VariableIndex, VariableDeclaration)
    -> StateT ProblemState IO Variable)
-> StateT ProblemState IO [Variable]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for
        ( Map VariableIndex VariableDeclaration
-> [(VariableIndex, VariableDeclaration)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map VariableIndex VariableDeclaration
initialState )
        ( \( FastDownward.SAS.VariableIndex Int
i
           , VariableDeclaration DomainIndex
_ IO [DomainIndex]
enumerate Int
axiomLayer
           ) -> do
            [DomainIndex]
domain <-
              IO [DomainIndex] -> StateT ProblemState IO [DomainIndex]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [DomainIndex]
enumerate

            Variable -> StateT ProblemState IO Variable
forall (m :: * -> *) a. Monad m => a -> m a
return
              Variable :: Text -> Seq Text -> Int -> Variable
FastDownward.SAS.Variable
                { name :: Text
name =
                    String -> Text
forall a. IsString a => String -> a
fromString ( String
"var-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i )
                , domain :: Seq Text
domain =
                    [Text] -> Seq Text
forall a. [a] -> Seq a
Seq.fromList ([Text] -> Seq Text) -> [Text] -> Seq Text
forall a b. (a -> b) -> a -> b
$
                    (DomainIndex -> Text) -> [DomainIndex] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map
                      ( \( FastDownward.SAS.DomainIndex Int
d ) ->
                          String -> Text
forall a. IsString a => String -> a
fromString
                            ( String
"Atom var-" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
d String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")" )
                      )
                      [DomainIndex]
domain
                      [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [ Text
"Atom dummy(dummy)" ]
                , axiomLayer :: Int
axiomLayer = Int
axiomLayer
                }
        )

    let
      plan :: Plan
plan =
        Plan :: Version
-> UseCosts
-> Seq Variable
-> Seq MutexGroup
-> State
-> Goal
-> Seq Operator
-> Seq Axiom
-> Plan
FastDownward.SAS.Plan
          { version :: Version
version =
              Version
FastDownward.SAS.SAS3
          , useCosts :: UseCosts
useCosts =
              UseCosts
FastDownward.SAS.NoCosts
          , variables :: Seq Variable
variables =
              [Variable] -> Seq Variable
forall a. [a] -> Seq a
Seq.fromList [Variable]
variables
          , mutexGroups :: Seq MutexGroup
mutexGroups =
              Seq MutexGroup
forall a. Monoid a => a
mempty
          , initialState :: State
initialState =
              Seq DomainIndex -> State
FastDownward.SAS.State
                ( [DomainIndex] -> Seq DomainIndex
forall a. [a] -> Seq a
Seq.fromList ([DomainIndex] -> Seq DomainIndex)
-> [DomainIndex] -> Seq DomainIndex
forall a b. (a -> b) -> a -> b
$ ((VariableIndex, VariableDeclaration) -> DomainIndex)
-> [(VariableIndex, VariableDeclaration)] -> [DomainIndex]
forall a b. (a -> b) -> [a] -> [b]
map ( VariableDeclaration -> DomainIndex
initial (VariableDeclaration -> DomainIndex)
-> ((VariableIndex, VariableDeclaration) -> VariableDeclaration)
-> (VariableIndex, VariableDeclaration)
-> DomainIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (VariableIndex, VariableDeclaration) -> VariableDeclaration
forall a b. (a, b) -> b
snd ) ( Map VariableIndex VariableDeclaration
-> [(VariableIndex, VariableDeclaration)]
forall k a. Map k a -> [(k, a)]
Map.toAscList Map VariableIndex VariableDeclaration
initialState ) )
          , goal :: Goal
goal =
              Seq VariableAssignment -> Goal
FastDownward.SAS.Goal ( [VariableAssignment] -> Seq VariableAssignment
forall a. [a] -> Seq a
Seq.fromList [VariableAssignment]
goal )
          , operators :: Seq Operator
operators =
              [Operator] -> Seq Operator
forall a. [a] -> Seq a
Seq.fromList ([Operator] -> Seq Operator) -> [Operator] -> Seq Operator
forall a b. (a -> b) -> a -> b
$ (Int -> (a, EffectState) -> Operator)
-> [Int] -> [(a, EffectState)] -> [Operator]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
                ( \Int
i ( a
_, EffectState{ IntMap DomainIndex
reads :: IntMap DomainIndex
reads :: EffectState -> IntMap DomainIndex
reads, IntMap DomainIndex
writes :: IntMap DomainIndex
writes :: EffectState -> IntMap DomainIndex
writes } ) ->
                    let
                      unchangedWrites :: IntMap DomainIndex
unchangedWrites =
                        ((DomainIndex, DomainIndex) -> Maybe DomainIndex)
-> IntMap (DomainIndex, DomainIndex) -> IntMap DomainIndex
forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe
                          ( \( DomainIndex
a, DomainIndex
b ) -> if DomainIndex
a DomainIndex -> DomainIndex -> Bool
forall a. Eq a => a -> a -> Bool
== DomainIndex
b then DomainIndex -> Maybe DomainIndex
forall a. a -> Maybe a
Just DomainIndex
a else Maybe DomainIndex
forall a. Maybe a
Nothing )
                          ( (DomainIndex -> DomainIndex -> (DomainIndex, DomainIndex))
-> IntMap DomainIndex
-> IntMap DomainIndex
-> IntMap (DomainIndex, DomainIndex)
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWith (,) IntMap DomainIndex
writes IntMap DomainIndex
reads )

                      actualWrites :: IntMap DomainIndex
actualWrites =
                        IntMap DomainIndex
writes IntMap DomainIndex -> IntMap DomainIndex -> IntMap DomainIndex
forall a b. IntMap a -> IntMap b -> IntMap a
`IntMap.difference` IntMap DomainIndex
unchangedWrites

                    in
                    Operator :: Text -> Seq VariableAssignment -> Seq Effect -> Operator
FastDownward.SAS.Operator
                      { name :: Text
name = String -> Text
forall a. IsString a => String -> a
fromString ( String
"op" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i )
                      , prevail :: Seq VariableAssignment
prevail =
                          [VariableAssignment] -> Seq VariableAssignment
forall a. [a] -> Seq a
Seq.fromList ([VariableAssignment] -> Seq VariableAssignment)
-> [VariableAssignment] -> Seq VariableAssignment
forall a b. (a -> b) -> a -> b
$ ((Int, DomainIndex) -> VariableAssignment)
-> [(Int, DomainIndex)] -> [VariableAssignment]
forall a b. (a -> b) -> [a] -> [b]
map
                            ( \( Int
x, DomainIndex
y ) -> VariableIndex -> DomainIndex -> VariableAssignment
FastDownward.SAS.VariableAssignment ( Int -> VariableIndex
coerce Int
x ) DomainIndex
y )
                            ( IntMap DomainIndex -> [(Int, DomainIndex)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList
                                ( IntMap DomainIndex -> IntMap DomainIndex -> IntMap DomainIndex
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference IntMap DomainIndex
reads IntMap DomainIndex
writes IntMap DomainIndex -> IntMap DomainIndex -> IntMap DomainIndex
forall a. Semigroup a => a -> a -> a
<> IntMap DomainIndex
unchangedWrites
                                )
                            )
                      , effects :: Seq Effect
effects =
                          [Effect] -> Seq Effect
forall a. [a] -> Seq a
Seq.fromList ([Effect] -> Seq Effect) -> [Effect] -> Seq Effect
forall a b. (a -> b) -> a -> b
$ ((Int, DomainIndex) -> Effect) -> [(Int, DomainIndex)] -> [Effect]
forall a b. (a -> b) -> [a] -> [b]
map
                            ( \( Int
v, DomainIndex
post ) -> VariableIndex -> Maybe DomainIndex -> DomainIndex -> Effect
FastDownward.SAS.Effect ( Int -> VariableIndex
coerce Int
v ) Maybe DomainIndex
forall a. Maybe a
Nothing DomainIndex
post )
                            ( IntMap DomainIndex -> [(Int, DomainIndex)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList ( IntMap DomainIndex -> IntMap DomainIndex -> IntMap DomainIndex
forall a b. IntMap a -> IntMap b -> IntMap a
IntMap.difference IntMap DomainIndex
writes IntMap DomainIndex
reads ) )
                            [Effect] -> [Effect] -> [Effect]
forall a. [a] -> [a] -> [a]
++
                              IntMap Effect -> [Effect]
forall a. IntMap a -> [a]
IntMap.elems
                                ( (Int -> DomainIndex -> DomainIndex -> Effect)
-> IntMap DomainIndex -> IntMap DomainIndex -> IntMap Effect
forall a b c.
(Int -> a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWithKey
                                    ( \Int
v DomainIndex
pre DomainIndex
post ->
                                        VariableIndex -> Maybe DomainIndex -> DomainIndex -> Effect
FastDownward.SAS.Effect ( Int -> VariableIndex
coerce Int
v ) ( DomainIndex -> Maybe DomainIndex
forall a. a -> Maybe a
Just DomainIndex
pre ) DomainIndex
post
                                    )
                                    IntMap DomainIndex
reads
                                    IntMap DomainIndex
actualWrites
                                )
                      }
                )
                [ Int
0 :: Int .. ]
                [(a, EffectState)]
operators
          , axioms :: Seq Axiom
axioms =
              [Axiom] -> Seq Axiom
forall a. [a] -> Seq a
Seq.fromList ([Axiom] -> Seq Axiom) -> [Axiom] -> Seq Axiom
forall a b. (a -> b) -> a -> b
$ Seq Axiom -> [Axiom]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList Seq Axiom
axioms
          }

    String
planFilePath <-
      IO String -> StateT ProblemState IO String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( String -> IO String
emptySystemTempFile String
"sas_plan" )

    ( ExitCode
exitCode, String
stdout, String
stderr ) <-
      IO (ExitCode, String, String)
-> StateT ProblemState IO (ExitCode, String, String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
        ( Options -> IO (ExitCode, String, String)
forall (m :: * -> *).
MonadIO m =>
Options -> m (ExitCode, String, String)
Exec.callFastDownward
            Options :: String -> Plan -> String -> SearchConfiguration -> Options
Exec.Options
              { $sel:fastDownward:Options :: String
fastDownward = String
"downward"
              , $sel:problem:Options :: Plan
problem = Plan
plan
              , $sel:planFilePath:Options :: String
planFilePath = String
planFilePath
              , $sel:searchConfiguration:Options :: SearchConfiguration
searchConfiguration = SearchConfiguration
cfg
              }
        )

    case ExitCode
exitCode of
      ExitFailure Int
11 ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return SolveResult a
forall a. SolveResult a
Unsolvable

      ExitFailure Int
12 ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return SolveResult a
forall a. SolveResult a
UnsolvableIncomplete

      ExitFailure Int
22 ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return SolveResult a
forall a. SolveResult a
OutOfMemory

      ExitFailure Int
23 ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return SolveResult a
forall a. SolveResult a
OutOfTime

      ExitFailure Int
32 ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return SolveResult a
forall a. SolveResult a
CriticalError

      ExitFailure Int
33 ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return SolveResult a
forall a. SolveResult a
InputError

      ExitFailure Int
34 ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return SolveResult a
forall a. SolveResult a
Unsupported

      ExitFailure Int
other ->
        SolveResult a -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return ( String -> String -> ExitCode -> SolveResult a
forall a. String -> String -> ExitCode -> SolveResult a
Crashed String
stdout String
stderr ( Int -> ExitCode
ExitFailure Int
other ) )

      ExitCode
ExitSuccess -> IO (SolveResult a) -> StateT ProblemState IO (SolveResult a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SolveResult a) -> StateT ProblemState IO (SolveResult a))
-> IO (SolveResult a) -> StateT ProblemState IO (SolveResult a)
forall a b. (a -> b) -> a -> b
$ do
        Text
planText <-
          String -> IO Text
Data.Text.Lazy.IO.readFile String
planFilePath

        let
          stepIndices :: [Int]
stepIndices =
            (Text -> Int) -> [Text] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map                           -- Read "(op42)" as 42
              ( String -> Int
forall a. Read a => String -> a
read
                  (String -> Int) -> (Text -> String) -> Text -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Data.Text.Lazy.unpack
                  (Text -> String) -> (Text -> Text) -> Text -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
Data.Text.Lazy.init   -- keep everything up to ")"
                  (Text -> Text) -> (Text -> Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int64 -> Text -> Text
Data.Text.Lazy.drop Int64
3 -- drop "(op"
              )
              ( (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile
                  ( Text
"(" Text -> Text -> Bool
`Data.Text.Lazy.isPrefixOf` )
                  ( Text -> [Text]
Data.Text.Lazy.lines Text
planText )
              )

        SolveResult a -> IO (SolveResult a)
forall (m :: * -> *) a. Monad m => a -> m a
return
          ( Solution a -> SolveResult a
forall a. Solution a -> SolveResult a
Solved
              Solution :: forall a. Plan -> IntMap a -> [Int] -> Solution a
Solution
                { sas :: Plan
sas = Plan
plan
                , operators :: IntMap a
operators = [(Int, a)] -> IntMap a
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ( [Int] -> [a] -> [(Int, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ( ((a, EffectState) -> a) -> [(a, EffectState)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, EffectState) -> a
forall a b. (a, b) -> a
fst [(a, EffectState)]
operators ) )
                , [Int]
stepIndices :: [Int]
stepIndices :: [Int]
..
                }
          )


exhaustEffects
  :: Traversable t
  => t ( Effect a )
  -> IO [ ( a, EffectState ) ]
exhaustEffects :: t (Effect a) -> IO [(a, EffectState)]
exhaustEffects t (Effect a)
ops = do
  IORef [(a, EffectState)]
out <-
    -- Every 'Effect' branch will eventually write it's output here.
    [(a, EffectState)] -> IO (IORef [(a, EffectState)])
forall a. a -> IO (IORef a)
newIORef []

  t (Effect a) -> (Effect a -> IO ()) -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
Data.Foldable.for_
    t (Effect a)
ops
    ( \( Effect ( ContT (a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ()
k ) ) ->
        ReaderT EffectState IO () -> EffectState -> IO ()
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT
          ( (a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ()
k
              ( \a
a ->
                  (EffectState -> IO ()) -> ReaderT EffectState IO ()
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((EffectState -> IO ()) -> ReaderT EffectState IO ())
-> (EffectState -> IO ()) -> ReaderT EffectState IO ()
forall a b. (a -> b) -> a -> b
$ \EffectState
es -> do
                    EffectState -> IO ()
onCommit EffectState
es

                    let
                      es' :: EffectState
es' = EffectState
es { onCommit :: IO ()
onCommit = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }

                    IORef [(a, EffectState)]
-> ([(a, EffectState)] -> [(a, EffectState)]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [(a, EffectState)]
out ( ( a
a, EffectState
es' ) (a, EffectState) -> [(a, EffectState)] -> [(a, EffectState)]
forall a. a -> [a] -> [a]
: )
              )
          )
          EffectState
s0
    )

  IORef [(a, EffectState)] -> IO [(a, EffectState)]
forall a. IORef a -> IO a
readIORef IORef [(a, EffectState)]
out

  where

    s0 :: EffectState
s0 =
      IntMap DomainIndex -> IntMap DomainIndex -> IO () -> EffectState
EffectState IntMap DomainIndex
forall a. Monoid a => a
mempty IntMap DomainIndex
forall a. Monoid a => a
mempty ( () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () )


-- | Leave the 'Problem' monad by running the given computation to 'IO'.
runProblem :: MonadIO m => Problem a -> m a
runProblem :: Problem a -> m a
runProblem Problem a
p = IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$
  StateT ProblemState IO a -> ProblemState -> IO a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT
    ( Problem a -> StateT ProblemState IO a
forall a. Problem a -> StateT ProblemState IO a
unProblem Problem a
p )
    ProblemState :: Map VariableIndex VariableDeclaration -> Seq Axiom -> ProblemState
ProblemState { initialState :: Map VariableIndex VariableDeclaration
initialState = Map VariableIndex VariableDeclaration
forall a. Monoid a => a
mempty , axioms :: Seq Axiom
axioms = Seq Axiom
forall a. Monoid a => a
mempty }


-- | Test that a 'Var' is set to a particular value.
(?=) :: Ord a => Var a -> a -> Test
?= :: Var a -> a -> Test
(?=) =
  Var a -> a -> Test
forall a. Ord a => Var a -> a -> Test
TestEq


-- | @Test@s are use to drive the solver in order to find a plan to the goal.
data Test where
  TestEq :: Ord a => {-# UNPACK #-} !( Var a ) -> !a -> Test
  Any :: ![ Test ] -> Test


requiresAxioms :: Test -> Bool
requiresAxioms :: Test -> Bool
requiresAxioms =
  \case
    TestEq{} ->
      Bool
False

    Any{} ->
      Bool
True


-- | Reset the initial state of a variable (the value that the solver will begin
-- with).
resetInitial :: Ord a => Var a -> a -> Problem ()
resetInitial :: Var a -> a -> Problem ()
resetInitial Var a
var a
a = do
  IO () -> Problem ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( IORef (Map a (Committed, DomainIndex))
-> Map a (Committed, DomainIndex) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef ( Var a -> IORef (Map a (Committed, DomainIndex))
forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var ) Map a (Committed, DomainIndex)
forall a. Monoid a => a
mempty )

  IO () -> Problem ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( IORef (Map DomainIndex a) -> Map DomainIndex a -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef ( Var a -> IORef (Map DomainIndex a)
forall a. Var a -> IORef (Map DomainIndex a)
fromDomainIndex Var a
var ) Map DomainIndex a
forall a. Monoid a => a
mempty )

  DomainIndex
i <-
    Var a -> a -> Problem DomainIndex
forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var a
var a
a

  Var a -> a -> Problem ()
forall a (m :: * -> *). (Ord a, MonadIO m) => Var a -> a -> m ()
commit Var a
var a
a

  StateT ProblemState IO () -> Problem ()
forall a. StateT ProblemState IO a -> Problem a
Problem (StateT ProblemState IO () -> Problem ())
-> StateT ProblemState IO () -> Problem ()
forall a b. (a -> b) -> a -> b
$ (ProblemState -> ProblemState) -> StateT ProblemState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ProblemState -> ProblemState) -> StateT ProblemState IO ())
-> (ProblemState -> ProblemState) -> StateT ProblemState IO ()
forall a b. (a -> b) -> a -> b
$ \ProblemState
ps ->
    ProblemState
ps
      { initialState :: Map VariableIndex VariableDeclaration
initialState =
          (VariableDeclaration -> VariableDeclaration)
-> VariableIndex
-> Map VariableIndex VariableDeclaration
-> Map VariableIndex VariableDeclaration
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust
            ( \VariableDeclaration
decl -> VariableDeclaration
decl { initial :: DomainIndex
initial = DomainIndex
i } )
            ( Var a -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var a
var )
            ( ProblemState -> Map VariableIndex VariableDeclaration
initialState ProblemState
ps )
      }


-- | Take the disjunction (or) of a list of 'Test's to a form new a @Test@ that
-- succeeds when at least one of the given tests is true.
--
-- __Caution!__ The use of @any@ introduces /axioms/ into the problem definition,
-- which is not compatible with many search engines.
any :: [ Test ] -> Test
any :: [Test] -> Test
any =
  [Test] -> Test
Any


testToVariableAssignment :: Test -> Problem FastDownward.SAS.VariableAssignment
testToVariableAssignment :: Test -> Problem VariableAssignment
testToVariableAssignment ( TestEq Var a
var a
a ) =
  VariableIndex -> DomainIndex -> VariableAssignment
FastDownward.SAS.VariableAssignment ( Var a -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var a
var )
    (DomainIndex -> VariableAssignment)
-> Problem DomainIndex -> Problem VariableAssignment
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var a -> a -> Problem DomainIndex
forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var a
var a
a

testToVariableAssignment ( Any [Test]
tests ) = do
  Var Bool
axiom <-
    Int -> Bool -> Problem (Var Bool)
forall a. Ord a => Int -> a -> Problem (Var a)
newVarAt Int
0 Bool
False

  DomainIndex
falseI <-
    Var Bool -> Bool -> Problem DomainIndex
forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var Bool
axiom Bool
False

  DomainIndex
trueI <-
    Var Bool -> Bool -> Problem DomainIndex
forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var Bool
axiom Bool
True

  [VariableAssignment]
assigns <-
    (Test -> Problem VariableAssignment)
-> [Test] -> Problem [VariableAssignment]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
Prelude.traverse Test -> Problem VariableAssignment
testToVariableAssignment [Test]
tests

  StateT ProblemState IO () -> Problem ()
forall a. StateT ProblemState IO a -> Problem a
Problem (StateT ProblemState IO () -> Problem ())
-> StateT ProblemState IO () -> Problem ()
forall a b. (a -> b) -> a -> b
$ (ProblemState -> ProblemState) -> StateT ProblemState IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ProblemState -> ProblemState) -> StateT ProblemState IO ())
-> (ProblemState -> ProblemState) -> StateT ProblemState IO ()
forall a b. (a -> b) -> a -> b
$ \ProblemState
ps ->
    ProblemState
ps
      { axioms :: Seq Axiom
axioms =
          [Axiom] -> Seq Axiom
forall a. [a] -> Seq a
Seq.fromList
            [ Axiom :: VariableIndex
-> Seq VariableAssignment -> DomainIndex -> DomainIndex -> Axiom
FastDownward.SAS.Axiom
                { variable :: VariableIndex
variable = Var Bool -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var Bool
axiom
                , conditions :: Seq VariableAssignment
conditions = VariableAssignment -> Seq VariableAssignment
forall a. a -> Seq a
Seq.singleton VariableAssignment
va
                , pre :: DomainIndex
pre = DomainIndex
falseI
                , post :: DomainIndex
post = DomainIndex
trueI
                }
            | VariableAssignment
va <- [VariableAssignment]
assigns
            ]
            Seq Axiom -> Seq Axiom -> Seq Axiom
forall a. Semigroup a => a -> a -> a
<> ProblemState -> Seq Axiom
axioms ProblemState
ps

      }

  VariableAssignment -> Problem VariableAssignment
forall (m :: * -> *) a. Monad m => a -> m a
return ( VariableIndex -> DomainIndex -> VariableAssignment
FastDownward.SAS.VariableAssignment ( Var Bool -> VariableIndex
forall a. Var a -> VariableIndex
variableIndex Var Bool
axiom ) DomainIndex
trueI )


-- | Deorder a plan into a partially ordered plan. This attempts to recover some
-- concurrency when adjacent plan steps do not need to be totally ordered. The
-- result of this function is the same as the result of
-- 'Data.Graph.graphFromEdges'.
partiallyOrderedPlan
  :: Ord a
  => Solution a
  -> ( Data.Graph.Graph
     , Data.Graph.Vertex -> ( a, IntMap.Key, [ IntMap.Key ] )
     , IntMap.Key -> Maybe Data.Graph.Vertex
     )
partiallyOrderedPlan :: Solution a -> (Graph, Int -> (a, Int, [Int]), Int -> Maybe Int)
partiallyOrderedPlan Solution{[Int]
IntMap a
Plan
stepIndices :: [Int]
operators :: IntMap a
sas :: Plan
stepIndices :: forall a. Solution a -> [Int]
operators :: forall a. Solution a -> IntMap a
sas :: forall a. Solution a -> Plan
..} =
  let
    ops :: IntMap Operator
ops =
      [(Int, Operator)] -> IntMap Operator
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ( [Int] -> [Operator] -> [(Int, Operator)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ( Seq Operator -> [Operator]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList ( Plan -> Seq Operator
FastDownward.SAS.Plan.operators Plan
sas ) ) )

    operation :: Int -> Operator
operation Int
i =
      IntMap Operator
ops IntMap Operator -> Int -> Operator
forall a. IntMap a -> Int -> a
IntMap.! Int
i

    g :: [(a, Int, [Int])]
g = do
      -- Here we consider every step in the list of steps. Using a combination
      -- of inits and reverse, given x1, x2, ..., xn, we end up with the
      -- following iterations:
      --
      -- 1. ( x1, [] )
      -- 2. ( x2, [ x1 ] )
      -- 3. ( xn, [ x1, x2, .., x(n-1) ] )
      --
      ( Int
i, Operator
o ) : [(Int, Operator)]
priorReversed <-
        ([(Int, Operator)] -> [(Int, Operator)])
-> [[(Int, Operator)]] -> [[(Int, Operator)]]
forall a b. (a -> b) -> [a] -> [b]
map
          [(Int, Operator)] -> [(Int, Operator)]
forall a. [a] -> [a]
reverse
          ( [[(Int, Operator)]] -> [[(Int, Operator)]]
forall a. [a] -> [a]
tail ( [(Int, Operator)] -> [[(Int, Operator)]]
forall a. [a] -> [[a]]
inits ( (Int -> (Int, Operator)) -> [Int] -> [(Int, Operator)]
forall a b. (a -> b) -> [a] -> [b]
map ( \Int
i -> ( Int
i, Int -> Operator
operation Int
i ) ) [Int]
stepIndices ) ) )

      let
        priors :: [(Int, Operator)]
priors =
          [(Int, Operator)] -> [(Int, Operator)]
forall a. [a] -> [a]
reverse [(Int, Operator)]
priorReversed

      -- For each step return it, and a list of any supporting operators.
      (a, Int, [Int]) -> [(a, Int, [Int])]
forall (m :: * -> *) a. Monad m => a -> m a
return
        ( IntMap a
operators IntMap a -> Int -> a
forall a. IntMap a -> Int -> a
IntMap.! Int
i
        , Int
i
        , ((Int, Operator) -> Maybe Int) -> [(Int, Operator)] -> [Int]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
            ( \( Int
j, Operator
x ) -> if Operator
o Operator -> Operator -> Bool
`after` Operator
x then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
j else Maybe Int
forall a. Maybe a
Nothing )
            [(Int, Operator)]
priors
        )

    ( Graph
gr, Int -> (a, Int, [Int])
fromVertex, Int -> Maybe Int
toVertex ) =
      [(a, Int, [Int])]
-> (Graph, Int -> (a, Int, [Int]), Int -> Maybe Int)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Int -> (node, key, [key]), key -> Maybe Int)
Data.Graph.graphFromEdges [(a, Int, [Int])]
g

  in
  ( Graph -> Graph
Data.Graph.transposeG Graph
gr, Int -> (a, Int, [Int])
fromVertex, Int -> Maybe Int
toVertex )


-- | Given an 'Problem.Operator', return its effects as a list of variable
-- assignments.
assignments :: FastDownward.SAS.Operator -> [ FastDownward.SAS.VariableAssignment ]
assignments :: Operator -> [VariableAssignment]
assignments Operator
o =
  [ VariableIndex -> DomainIndex -> VariableAssignment
FastDownward.SAS.VariableAssignment
      ( Effect -> VariableIndex
FastDownward.SAS.Effect.variable Effect
e )
      ( Effect -> DomainIndex
FastDownward.SAS.Effect.post Effect
e )
  | Effect
e <- Seq Effect -> [Effect]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList ( Operator -> Seq Effect
FastDownward.SAS.Operator.effects Operator
o )
  ]



-- | Given an 'Problem.Operator', return a list of variable assignments that
-- must be such in order for this operator to be applicable. This is the
-- combination of the prevailing conditions for the operator, and the original
-- state for all variables updated by effects.
requirements :: FastDownward.SAS.Operator -> Seq FastDownward.SAS.VariableAssignment
requirements :: Operator -> Seq VariableAssignment
requirements Operator
o =
  Operator -> Seq VariableAssignment
FastDownward.SAS.Operator.prevail Operator
o Seq VariableAssignment
-> Seq VariableAssignment -> Seq VariableAssignment
forall a. Semigroup a => a -> a -> a
<> [VariableAssignment] -> Seq VariableAssignment
forall a. [a] -> Seq a
Seq.fromList ( Operator -> [VariableAssignment]
original Operator
o )


-- | Return all the original 'FastDownward.VariableAssignment's for an
-- 'Problem.Operator'. This is the set of original assignments before the
-- operator is applied.
original :: FastDownward.SAS.Operator -> [ FastDownward.SAS.VariableAssignment ]
original :: Operator -> [VariableAssignment]
original Operator
o =
  (Effect -> Maybe VariableAssignment)
-> [Effect] -> [VariableAssignment]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
    ( \Effect
e ->
        VariableIndex -> DomainIndex -> VariableAssignment
FastDownward.SAS.VariableAssignment ( Effect -> VariableIndex
FastDownward.SAS.Effect.variable Effect
e )
          (DomainIndex -> VariableAssignment)
-> Maybe DomainIndex -> Maybe VariableAssignment
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Effect -> Maybe DomainIndex
FastDownward.SAS.Effect.pre Effect
e
    )
    ( Seq Effect -> [Effect]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList ( Operator -> Seq Effect
FastDownward.SAS.Operator.effects Operator
o ) )


-- | @o `after` x@ is true if:
--
-- 1. o requires an initial variable state produced by x.
-- 2. x requires an initial variable state that it is also required by
--    o. This is because x will be changing the state of a variable o
--    required by o.
after
  :: FastDownward.SAS.Operator.Operator
  -> FastDownward.SAS.Operator.Operator
  -> Bool
Operator
o after :: Operator -> Operator -> Bool
`after` Operator
x =
  Bool -> Bool
not ( [VariableAssignment] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ( Seq VariableAssignment -> [VariableAssignment]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList ( Operator -> Seq VariableAssignment
requirements Operator
o ) [VariableAssignment]
-> [VariableAssignment] -> [VariableAssignment]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` Operator -> [VariableAssignment]
assignments Operator
x ) ) Bool -> Bool -> Bool
||
    Bool -> Bool
not ( [VariableAssignment] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ( Seq VariableAssignment -> [VariableAssignment]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList ( Operator -> Seq VariableAssignment
requirements Operator
x ) [VariableAssignment]
-> [VariableAssignment] -> [VariableAssignment]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` Operator -> [VariableAssignment]
original Operator
o ) )