{-# 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
    { forall a. Var a -> VariableIndex
variableIndex :: {-# UNPACK #-} !FastDownward.SAS.VariableIndex
      -- ^ The SAS variable index of this variable.
    , forall a. 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.
    , forall a. Var a -> IORef (a -> DomainIndex -> IO ())
subscribed :: {-# UNPACK #-} !( IORef ( a -> FastDownward.SAS.DomainIndex -> IO () ) )
    , forall a. 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 { forall a. Problem a -> StateT ProblemState IO a
unProblem :: StateT ProblemState IO a }
  deriving
    ( 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
<$ :: forall a b. a -> Problem b -> Problem a
$c<$ :: forall a b. a -> Problem b -> Problem a
fmap :: forall a b. (a -> b) -> Problem a -> Problem b
$cfmap :: forall a b. (a -> b) -> Problem a -> Problem b
Functor, Functor Problem
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
<* :: forall a b. Problem a -> Problem b -> Problem a
$c<* :: forall a b. Problem a -> Problem b -> Problem a
*> :: forall a b. Problem a -> Problem b -> Problem b
$c*> :: forall a b. Problem a -> Problem b -> Problem b
liftA2 :: forall a b c. (a -> b -> c) -> Problem a -> Problem b -> Problem c
$cliftA2 :: forall a b c. (a -> b -> c) -> Problem a -> Problem b -> Problem c
<*> :: forall a b. Problem (a -> b) -> Problem a -> Problem b
$c<*> :: forall a b. Problem (a -> b) -> Problem a -> Problem b
pure :: forall a. a -> Problem a
$cpure :: forall a. a -> Problem a
Applicative, Applicative Problem
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 :: forall a. a -> Problem a
$creturn :: forall a. a -> Problem a
>> :: forall a b. Problem a -> Problem b -> Problem b
$c>> :: forall a b. Problem a -> Problem b -> Problem b
>>= :: forall a b. Problem a -> (a -> Problem b) -> Problem b
$c>>= :: forall a b. Problem a -> (a -> Problem b) -> Problem b
Monad, Monad Problem
forall a. IO a -> Problem a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> Problem a
$cliftIO :: forall a. IO a -> Problem a
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 :: forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var a
var a
a = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
  Map a (Committed, DomainIndex)
vs <-
    forall a. IORef a -> IO a
readIORef ( forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var )

  case 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 ) ->
      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 ( forall a b. (Integral a, Num b) => a -> b
fromIntegral ( forall k a. Map k a -> Int
Map.size Map a (Committed, DomainIndex)
vs ) )

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

      DomainIndex
i forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef ( forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var ) ( 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 :: forall a (m :: * -> *). (Ord a, MonadIO m) => Var a -> a -> m ()
commit Var a
var a
a = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
  forall a. IORef a -> (a -> a) -> IO ()
modifyIORef ( forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var ) ( 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 :: forall a. Ord a => a -> Problem (Var a)
newVar =
  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 :: forall a. Ord a => Int -> a -> Problem (Var a)
newVarAt Int
axiomLayer a
initialValue = do
  -- Allocate the domain IORef
  IORef (Map a (Committed, DomainIndex))
values <-
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( forall a. a -> IO (IORef a)
newIORef forall a. Monoid a => a
mempty )

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

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

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

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

    var :: Var a
var =
      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 <-
    forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var a
var a
initialValue

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

  -- ... and record it in the ProblemState.
  forall a. StateT ProblemState IO a -> Problem a
Problem
    ( forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify
        ( \ProblemState
ps ->
            ProblemState
ps
              { initialState :: Map VariableIndex VariableDeclaration
initialState =
                  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 )
              }
        )
    )

  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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. StateT ProblemState IO a -> Problem a
Problem ( forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ( forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> Int
Map.size 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 :: forall a. Ord a => Var a -> a -> Effect ()
writeVar Var a
var a
a = forall a. ContT () (ReaderT EffectState IO) a -> Effect a
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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do
    Map a (Committed, DomainIndex)
currentValues <-
      forall a. IORef a -> IO a
readIORef ( forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var )

    case 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 ) ->
        forall (m :: * -> *) a. Monad m => a -> m a
return ( forall a b. b -> Either a b
Right DomainIndex
domainIndex )

      Just ( Committed
Uncommitted, DomainIndex
domainIndex ) ->
        forall (m :: * -> *) a. Monad m => a -> m a
return ( 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.
        forall a b. a -> Either a b
Left forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(Ord a, MonadIO m) =>
Var a -> a -> m DomainIndex
observeValue Var a
var a
a

  forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT forall a b. (a -> b) -> a -> b
$ \() -> ReaderT EffectState IO ()
k -> forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT 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 <-
            forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ do
              Map a (Committed, DomainIndex)
currentValues <-
                forall a. IORef a -> IO a
readIORef ( forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var )

              case 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
_ ) ->
                  forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

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

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

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

                  forall a. IORef a -> a -> IO ()
writeIORef IORef (IO ())
laterRef ( forall (m :: * -> *) a. Monad m => a -> m a
return () )
                    forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> IO ()
action
                    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.
          forall (m :: * -> *) a. Monad m => a -> m a
return
            EffectState
es
              { writes :: IntMap DomainIndex
writes =
                  forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert ( coerce :: forall a b. Coercible a b => a -> b
coerce ( forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) DomainIndex
domainIndex ( EffectState -> IntMap DomainIndex
writes EffectState
es )
              }

    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 :: forall a. Ord a => Var a -> Effect a
readVar Var a
var = forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect forall a b. (a -> b) -> a -> b
$ forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT forall a b. (a -> b) -> a -> b
$ \a -> ReaderT EffectState IO ()
k -> forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT 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 =
      forall a. Int -> IntMap a -> Maybe a
IntMap.lookup ( coerce :: forall a b. Coercible a b => a -> b
coerce ( forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) ( EffectState -> IntMap DomainIndex
reads EffectState
es )

    mPrevWrite :: Maybe DomainIndex
mPrevWrite =
      forall a. Int -> IntMap a -> Maybe a
IntMap.lookup ( coerce :: forall a b. Coercible a b => a -> b
coerce ( 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 <-
        ( forall k a. Ord k => Map k a -> k -> a
Map.! DomainIndex
prevWriteIndex ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef ( forall a. Var a -> IORef (Map DomainIndex a)
fromDomainIndex Var a
var )

      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 <-
        ( forall k a. Ord k => Map k a -> k -> a
Map.! DomainIndex
prevReadIndex ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef ( forall a. Var a -> IORef (Map DomainIndex a)
fromDomainIndex Var a
var )

      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 =
                    forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert ( coerce :: forall a b. Coercible a b => a -> b
coerce ( forall a. Var a -> VariableIndex
variableIndex Var a
var ) ) DomainIndex
domainIndex ( EffectState -> IntMap DomainIndex
reads EffectState
es )
                }

          in 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 <-
        forall a. IORef a -> IO a
readIORef ( 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).
      forall a. IORef a -> (a -> a) -> IO ()
modifyIORef
        ( 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 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.
      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
_ ->
                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 :: forall a. Ord a => Var a -> (a -> a) -> Effect ()
modifyVar Var a
v a -> a
f =
  forall a. Ord a => Var a -> Effect a
readVar Var a
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. Ord a => Var a -> a -> Effect ()
writeVar Var a
v 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 { forall a. Effect a -> ContT () (ReaderT EffectState IO) a
runEffect :: ContT () ( ReaderT EffectState IO ) a }
  deriving
    ( 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
<$ :: forall a b. a -> Effect b -> Effect a
$c<$ :: forall a b. a -> Effect b -> Effect a
fmap :: forall a b. (a -> b) -> Effect a -> Effect b
$cfmap :: forall a b. (a -> b) -> Effect a -> Effect b
Functor, Functor Effect
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
<* :: forall a b. Effect a -> Effect b -> Effect a
$c<* :: forall a b. Effect a -> Effect b -> Effect a
*> :: forall a b. Effect a -> Effect b -> Effect b
$c*> :: forall a b. Effect a -> Effect b -> Effect b
liftA2 :: forall a b c. (a -> b -> c) -> Effect a -> Effect b -> Effect c
$cliftA2 :: forall a b c. (a -> b -> c) -> Effect a -> Effect b -> Effect c
<*> :: forall a b. Effect (a -> b) -> Effect a -> Effect b
$c<*> :: forall a b. Effect (a -> b) -> Effect a -> Effect b
pure :: forall a. a -> Effect a
$cpure :: forall a. a -> Effect a
Applicative )


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

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


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


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

  Effect ContT () (ReaderT EffectState IO) a
a <|> :: forall a. Effect a -> Effect a -> Effect a
<|> Effect ContT () (ReaderT EffectState IO) a
b =
    forall a. ContT () (ReaderT EffectState IO) a -> Effect a
Effect forall a b. (a -> b) -> a -> b
$ forall {k} (r :: k) (m :: k -> *) a.
((a -> m r) -> m r) -> ContT r m a
ContT forall a b. (a -> b) -> a -> b
$ \a -> ReaderT EffectState IO ()
k ->
      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 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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
    ( 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
<$ :: forall a b. a -> SolveResult b -> SolveResult a
$c<$ :: forall a b. a -> SolveResult b -> SolveResult a
fmap :: forall a b. (a -> b) -> SolveResult a -> SolveResult b
$cfmap :: forall a b. (a -> b) -> SolveResult a -> SolveResult b
Functor, Int -> SolveResult a -> ShowS
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
    { forall a. Solution a -> Plan
sas :: FastDownward.SAS.Plan
    , forall a. Solution a -> IntMap a
operators :: IntMap.IntMap a
    , forall a. Solution a -> [Int]
stepIndices :: [ IntMap.Key ]
    }
  deriving
    ( 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
<$ :: forall a b. a -> Solution b -> Solution a
$c<$ :: forall a b. a -> Solution b -> Solution a
fmap :: forall a b. (a -> b) -> Solution a -> Solution b
$cfmap :: forall a b. (a -> b) -> Solution a -> Solution b
Functor, Int -> Solution a -> ShowS
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 :: forall a. 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
..} =
  forall a b. (a -> b) -> [a] -> [b]
map ( IntMap a
operators 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 :: forall a.
Show a =>
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 <-
    forall a. StateT ProblemState IO a -> Problem a
Problem forall s (m :: * -> *). MonadState s m => m s
get

  forall a. StateT ProblemState IO a -> Problem a
Problem forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ProblemState
s0 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 <-
      forall a. Problem a -> StateT ProblemState IO a
unProblem ( 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 <-
      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( forall (t :: * -> *) a.
Traversable t =>
t (Effect a) -> IO [(a, EffectState)]
exhaustEffects [Effect a]
ops )

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

    Seq Axiom
axioms <-
      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 <-
      forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for
        ( 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 <-
              forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [DomainIndex]
enumerate

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

    let
      plan :: Plan
plan =
        FastDownward.SAS.Plan
          { version :: Version
version =
              Version
FastDownward.SAS.SAS3
          , useCosts :: UseCosts
useCosts =
              UseCosts
FastDownward.SAS.NoCosts
          , variables :: Seq Variable
variables =
              forall a. [a] -> Seq a
Seq.fromList [Variable]
variables
          , mutexGroups :: Seq MutexGroup
mutexGroups =
              forall a. Monoid a => a
mempty
          , initialState :: State
initialState =
              Seq DomainIndex -> State
FastDownward.SAS.State
                ( forall a. [a] -> Seq a
Seq.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ( VariableDeclaration -> DomainIndex
initial forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd ) ( forall k a. Map k a -> [(k, a)]
Map.toAscList Map VariableIndex VariableDeclaration
initialState ) )
          , goal :: Goal
goal =
              Seq VariableAssignment -> Goal
FastDownward.SAS.Goal ( forall a. [a] -> Seq a
Seq.fromList [VariableAssignment]
goal )
          , operators :: Seq Operator
operators =
              forall a. [a] -> Seq a
Seq.fromList forall a b. (a -> b) -> a -> b
$ 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 =
                        forall a b. (a -> Maybe b) -> IntMap a -> IntMap b
IntMap.mapMaybe
                          ( \( DomainIndex
a, DomainIndex
b ) -> if DomainIndex
a forall a. Eq a => a -> a -> Bool
== DomainIndex
b then forall a. a -> Maybe a
Just DomainIndex
a else forall a. Maybe a
Nothing )
                          ( 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 forall a b. IntMap a -> IntMap b -> IntMap a
`IntMap.difference` IntMap DomainIndex
unchangedWrites

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

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

    ( ExitCode
exitCode, String
stdout, String
stderr ) <-
      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
        ( forall (m :: * -> *).
MonadIO m =>
Options -> m (ExitCode, String, String)
Exec.callFastDownward
            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 ->
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. SolveResult a
Unsolvable

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

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

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

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

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

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

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

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

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

        forall (m :: * -> *) a. Monad m => a -> m a
return
          ( forall a. Solution a -> SolveResult a
Solved
              Solution
                { sas :: Plan
sas = Plan
plan
                , operators :: IntMap a
operators = forall a. [(Int, a)] -> IntMap a
IntMap.fromList ( forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ( forall a b. (a -> b) -> [a] -> [b]
map 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 :: forall (t :: * -> *) a.
Traversable t =>
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.
    forall a. a -> IO (IORef a)
newIORef []

  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 ) ) ->
        forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT
          ( (a -> ReaderT EffectState IO ()) -> ReaderT EffectState IO ()
k
              ( \a
a ->
                  forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \EffectState
es -> do
                    EffectState -> IO ()
onCommit EffectState
es

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

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

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

  where

    s0 :: EffectState
s0 =
      IntMap DomainIndex -> IntMap DomainIndex -> IO () -> EffectState
EffectState forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty ( 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 :: forall (m :: * -> *) a. MonadIO m => Problem a -> m a
runProblem Problem a
p = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT
    ( forall a. Problem a -> StateT ProblemState IO a
unProblem Problem a
p )
    ProblemState { initialState :: Map VariableIndex VariableDeclaration
initialState = forall a. Monoid a => a
mempty , axioms :: Seq Axiom
axioms = forall a. Monoid a => a
mempty }


-- | Test that a 'Var' is set to a particular value.
(?=) :: Ord a => Var a -> a -> Test
?= :: forall a. Ord a => 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 :: forall a. Ord a => Var a -> a -> Problem ()
resetInitial Var a
var a
a = do
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO ( forall a. IORef a -> a -> IO ()
writeIORef ( forall a. Var a -> IORef (Map a (Committed, DomainIndex))
values Var a
var ) forall a. Monoid a => a
mempty )

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

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

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

  forall a. StateT ProblemState IO a -> Problem a
Problem forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \ProblemState
ps ->
    ProblemState
ps
      { initialState :: Map VariableIndex VariableDeclaration
initialState =
          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 } )
            ( 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 ( forall a. Var a -> VariableIndex
variableIndex Var a
var )
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <-
    forall a. Ord a => Int -> a -> Problem (Var a)
newVarAt Int
0 Bool
False

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

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

  [VariableAssignment]
assigns <-
    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

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

      }

  forall (m :: * -> *) a. Monad m => a -> m a
return ( VariableIndex -> DomainIndex -> VariableAssignment
FastDownward.SAS.VariableAssignment ( 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 :: forall a.
Ord a =>
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 =
      forall a. [(Int, a)] -> IntMap a
IntMap.fromList ( forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ( 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 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 <-
        forall a b. (a -> b) -> [a] -> [b]
map
          forall a. [a] -> [a]
reverse
          ( forall a. [a] -> [a]
tail ( forall a. [a] -> [[a]]
inits ( forall a b. (a -> b) -> [a] -> [b]
map ( \Int
i -> ( Int
i, Int -> Operator
operation Int
i ) ) [Int]
stepIndices ) ) )

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

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

    ( Graph
gr, Int -> (a, Int, [Int])
fromVertex, Int -> Maybe Int
toVertex ) =
      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 <- 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 forall a. Semigroup a => a -> a -> a
<> 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 =
  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 )
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Effect -> Maybe DomainIndex
FastDownward.SAS.Effect.pre Effect
e
    )
    ( 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 ( forall (t :: * -> *) a. Foldable t => t a -> Bool
null ( forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList ( Operator -> Seq VariableAssignment
requirements Operator
o ) forall a. Eq a => [a] -> [a] -> [a]
`intersect` Operator -> [VariableAssignment]
assignments Operator
x ) ) Bool -> Bool -> Bool
||
    Bool -> Bool
not ( forall (t :: * -> *) a. Foldable t => t a -> Bool
null ( forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList ( Operator -> Seq VariableAssignment
requirements Operator
x ) forall a. Eq a => [a] -> [a] -> [a]
`intersect` Operator -> [VariableAssignment]
original Operator
o ) )