{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- The Swarm interpreter uses a technique known as a
-- <https://matt.might.net/articles/cesk-machines/ CESK machine> (if
-- you want to read up on them, you may want to start by reading about
-- <https://matt.might.net/articles/cek-machines/ CEK machines>
-- first).  Execution happens simply by iterating a step function,
-- sending one state of the CESK machine to the next. In addition to
-- being relatively efficient, this means we can easily run a bunch of
-- robots synchronously, in parallel, without resorting to any threads
-- (by stepping their machines in a round-robin fashion); pause and
-- single-step the game; save and resume, and so on.
--
-- Essentially, a CESK machine state has four components:
--
-- - The __C__ontrol is the thing we are currently focused on:
--   either a 'Term' to evaluate, or a 'Value' that we have
--   just finished evaluating.
-- - The __E__nvironment ('Env') is a mapping from variables that might
--   occur free in the Control to their values.
-- - The __S__tore ('Store') is a mapping from abstract integer
--   /locations/ to values.  We use it to store delayed (lazy) values,
--   so they will be computed at most once.
-- - The __K__ontinuation ('Cont') is a stack of 'Frame's,
--   representing the evaluation context, /i.e./ what we are supposed
--   to do after we finish with the currently focused thing.  When we
--   reduce the currently focused term to a value, the top frame on
--   the stack tells us how to proceed.
--
-- You can think of a CESK machine as a defunctionalization of a
-- recursive big-step interpreter, where we explicitly keep track of
-- the call stack and the environments that would be in effect at
-- various places in the recursion.  One could probably even derive
-- this mechanically, by writing a recursive big-step interpreter,
-- then converting it to CPS, then defunctionalizing the
-- continuations.
--
-- The slightly confusing thing about CESK machines is how we
-- have to pass around environments everywhere.  Basically,
-- anywhere there can be unevaluated terms containing free
-- variables (in values, in continuation stack frames, ...), we
-- have to store the proper environment alongside so that when
-- we eventually get around to evaluating it, we will be able to
-- pull out the environment to use.
module Swarm.Game.CESK (
  -- * Frames and continuations
  Frame (..),
  Cont,

  -- ** Wrappers for creating delayed change of state
  WorldUpdate (..),
  RobotUpdate (..),

  -- * Store
  Store,
  Addr,
  emptyStore,
  MemCell (..),
  allocate,
  lookupStore,
  setStore,

  -- * CESK machine states
  CESK (..),

  -- ** Construction
  initMachine,
  initMachine',
  cancel,
  resetBlackholes,

  -- ** Extracting information
  finalValue,
  TickNumber (..),
  addTicks,
) where

import Control.Lens ((^.))
import Control.Lens.Combinators (pattern Empty)
import Data.Aeson (FromJSON, ToJSON)
import Data.Int (Int64)
import Data.IntMap.Strict (IntMap)
import Data.IntMap.Strict qualified as IM
import GHC.Generics (Generic)
import Prettyprinter (Doc, Pretty (..), encloseSep, hsep, (<+>))
import Swarm.Game.Entity (Count, Entity)
import Swarm.Game.Exception
import Swarm.Game.World (WorldUpdate (..))
import Swarm.Language.Context
import Swarm.Language.Module
import Swarm.Language.Pipeline
import Swarm.Language.Pretty
import Swarm.Language.Requirement (ReqCtx)
import Swarm.Language.Syntax
import Swarm.Language.Types
import Swarm.Language.Value as V
import Swarm.Util.WindowedCounter (Offsettable (..))

-- | A newtype representing a count of ticks (typically since the
--   start of a game).
newtype TickNumber = TickNumber {TickNumber -> Int64
getTickNumber :: Int64}
  deriving (TickNumber -> TickNumber -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TickNumber -> TickNumber -> Bool
$c/= :: TickNumber -> TickNumber -> Bool
== :: TickNumber -> TickNumber -> Bool
$c== :: TickNumber -> TickNumber -> Bool
Eq, Eq TickNumber
TickNumber -> TickNumber -> Bool
TickNumber -> TickNumber -> Ordering
TickNumber -> TickNumber -> TickNumber
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TickNumber -> TickNumber -> TickNumber
$cmin :: TickNumber -> TickNumber -> TickNumber
max :: TickNumber -> TickNumber -> TickNumber
$cmax :: TickNumber -> TickNumber -> TickNumber
>= :: TickNumber -> TickNumber -> Bool
$c>= :: TickNumber -> TickNumber -> Bool
> :: TickNumber -> TickNumber -> Bool
$c> :: TickNumber -> TickNumber -> Bool
<= :: TickNumber -> TickNumber -> Bool
$c<= :: TickNumber -> TickNumber -> Bool
< :: TickNumber -> TickNumber -> Bool
$c< :: TickNumber -> TickNumber -> Bool
compare :: TickNumber -> TickNumber -> Ordering
$ccompare :: TickNumber -> TickNumber -> Ordering
Ord, Addr -> TickNumber -> ShowS
[TickNumber] -> ShowS
TickNumber -> String
forall a.
(Addr -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TickNumber] -> ShowS
$cshowList :: [TickNumber] -> ShowS
show :: TickNumber -> String
$cshow :: TickNumber -> String
showsPrec :: Addr -> TickNumber -> ShowS
$cshowsPrec :: Addr -> TickNumber -> ShowS
Show, ReadPrec [TickNumber]
ReadPrec TickNumber
Addr -> ReadS TickNumber
ReadS [TickNumber]
forall a.
(Addr -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [TickNumber]
$creadListPrec :: ReadPrec [TickNumber]
readPrec :: ReadPrec TickNumber
$creadPrec :: ReadPrec TickNumber
readList :: ReadS [TickNumber]
$creadList :: ReadS [TickNumber]
readsPrec :: Addr -> ReadS TickNumber
$creadsPrec :: Addr -> ReadS TickNumber
Read, forall x. Rep TickNumber x -> TickNumber
forall x. TickNumber -> Rep TickNumber x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TickNumber x -> TickNumber
$cfrom :: forall x. TickNumber -> Rep TickNumber x
Generic, Value -> Parser [TickNumber]
Value -> Parser TickNumber
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [TickNumber]
$cparseJSONList :: Value -> Parser [TickNumber]
parseJSON :: Value -> Parser TickNumber
$cparseJSON :: Value -> Parser TickNumber
FromJSON, [TickNumber] -> Encoding
[TickNumber] -> Value
TickNumber -> Encoding
TickNumber -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [TickNumber] -> Encoding
$ctoEncodingList :: [TickNumber] -> Encoding
toJSONList :: [TickNumber] -> Value
$ctoJSONList :: [TickNumber] -> Value
toEncoding :: TickNumber -> Encoding
$ctoEncoding :: TickNumber -> Encoding
toJSON :: TickNumber -> Value
$ctoJSON :: TickNumber -> Value
ToJSON)

-- | Add an offset to a 'TickNumber'.
addTicks :: Int -> TickNumber -> TickNumber
addTicks :: Addr -> TickNumber -> TickNumber
addTicks Addr
i (TickNumber Int64
n) = Int64 -> TickNumber
TickNumber forall a b. (a -> b) -> a -> b
$ Int64
n forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Addr
i

instance Offsettable TickNumber where
  offsetBy :: Addr -> TickNumber -> TickNumber
offsetBy = Addr -> TickNumber -> TickNumber
addTicks

instance Pretty TickNumber where
  pretty :: forall ann. TickNumber -> Doc ann
pretty (TickNumber Int64
i) = forall a ann. Pretty a => a -> Doc ann
pretty Int64
i

------------------------------------------------------------
-- Frames and continuations
------------------------------------------------------------

-- | A frame is a single component of a continuation stack, explaining
--   what to do next after we finish evaluating the currently focused
--   term.
data Frame
  = -- | We were evaluating the first component of a pair; next, we
    --   should evaluate the second component which was saved in this
    --   frame (and push a 'FFst' frame on the stack to save the first component).
    FSnd Term Env
  | -- | We were evaluating the second component of a pair; when done,
    --   we should combine it with the value of the first component saved
    --   in this frame to construct a fully evaluated pair.
    FFst Value
  | -- | @FArg t e@ says that we were evaluating the left-hand side of
    -- an application, so the next thing we should do is evaluate the
    -- term @t@ (the right-hand side, /i.e./ argument of the
    -- application) in environment @e@.  We will also push an 'FApp'
    -- frame on the stack.
    FArg Term Env
  | -- | @FApp v@ says that we were evaluating the right-hand side of
    -- an application; once we are done, we should pass the resulting
    -- value as an argument to @v@.
    FApp Value
  | -- | @FLet x t2 e@ says that we were evaluating a term @t1@ in an
    -- expression of the form @let x = t1 in t2@, that is, we were
    -- evaluating the definition of @x@; the next thing we should do
    -- is evaluate @t2@ in the environment @e@ extended with a binding
    -- for @x@.
    FLet Var Term Env
  | -- | We are executing inside a 'Try' block.  If an exception is
    --   raised, we will execute the stored term (the "catch" block).
    FTry Value
  | -- | We were executing a command; next we should take any
    --   environment it returned and union it with this one to produce
    --   the result of a bind expression.
    FUnionEnv Env
  | -- | We were executing a command that might have definitions; next
    --   we should take the resulting 'Env' and add it to the robot's
    --   'Swarm.Game.Robot.robotEnv', along with adding this accompanying 'Ctx' and
    --   'ReqCtx' to the robot's 'Swarm.Game.Robot.robotCtx'.
    FLoadEnv TCtx ReqCtx
  | -- | We were executing a definition; next we should take the resulting value
    --   and return a context binding the variable to the value.
    FDef Var
  | -- | An @FExec@ frame means the focused value is a command, which
    -- we should now execute.
    FExec
  | -- | We are in the process of executing the first component of a
    --   bind; once done, we should also execute the second component
    --   in the given environment (extended by binding the variable,
    --   if there is one, to the output of the first command).
    FBind (Maybe Var) Term Env
  | -- | Discard any environment generated as the result of executing
    --   a command.
    FDiscardEnv
  | -- | Apply specific updates to the world and current robot.
    --
    -- The 'Const' is used to track the original command for error messages.
    FImmediate Const [WorldUpdate Entity] [RobotUpdate]
  | -- | Update the memory cell at a certain location with the computed value.
    FUpdate Addr
  | -- | Signal that we are done with an atomic computation.
    FFinishAtomic
  | -- | We are in the middle of running a computation for all the
    --   nearby robots.  We have the function to run, and the list of
    --   robot IDs to run it on.
    FMeetAll Value [Int]
  | -- | We are in the middle of evaluating a record: some fields have
    --   already been evaluated; we are focusing on evaluating one
    --   field; and some fields have yet to be evaluated.
    FRcd Env [(Var, Value)] Var [(Var, Maybe Term)]
  | -- | We are in the middle of evaluating a record field projection.
    FProj Var
  deriving (Frame -> Frame -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Frame -> Frame -> Bool
$c/= :: Frame -> Frame -> Bool
== :: Frame -> Frame -> Bool
$c== :: Frame -> Frame -> Bool
Eq, Addr -> Frame -> ShowS
Cont -> ShowS
Frame -> String
forall a.
(Addr -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: Cont -> ShowS
$cshowList :: Cont -> ShowS
show :: Frame -> String
$cshow :: Frame -> String
showsPrec :: Addr -> Frame -> ShowS
$cshowsPrec :: Addr -> Frame -> ShowS
Show, forall x. Rep Frame x -> Frame
forall x. Frame -> Rep Frame x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Frame x -> Frame
$cfrom :: forall x. Frame -> Rep Frame x
Generic, Value -> Parser Cont
Value -> Parser Frame
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser Cont
$cparseJSONList :: Value -> Parser Cont
parseJSON :: Value -> Parser Frame
$cparseJSON :: Value -> Parser Frame
FromJSON, Cont -> Encoding
Cont -> Value
Frame -> Encoding
Frame -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: Cont -> Encoding
$ctoEncodingList :: Cont -> Encoding
toJSONList :: Cont -> Value
$ctoJSONList :: Cont -> Value
toEncoding :: Frame -> Encoding
$ctoEncoding :: Frame -> Encoding
toJSON :: Frame -> Value
$ctoJSON :: Frame -> Value
ToJSON)

-- | A continuation is just a stack of frames.
type Cont = [Frame]

------------------------------------------------------------
-- Store
------------------------------------------------------------

type Addr = Int

-- | 'Store' represents a store, /i.e./ memory, indexing integer
--   locations to 'MemCell's.
data Store = Store {Store -> Addr
next :: Addr, Store -> IntMap MemCell
mu :: IntMap MemCell}
  deriving (Addr -> Store -> ShowS
[Store] -> ShowS
Store -> String
forall a.
(Addr -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Store] -> ShowS
$cshowList :: [Store] -> ShowS
show :: Store -> String
$cshow :: Store -> String
showsPrec :: Addr -> Store -> ShowS
$cshowsPrec :: Addr -> Store -> ShowS
Show, Store -> Store -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Store -> Store -> Bool
$c/= :: Store -> Store -> Bool
== :: Store -> Store -> Bool
$c== :: Store -> Store -> Bool
Eq, forall x. Rep Store x -> Store
forall x. Store -> Rep Store x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Store x -> Store
$cfrom :: forall x. Store -> Rep Store x
Generic, Value -> Parser [Store]
Value -> Parser Store
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Store]
$cparseJSONList :: Value -> Parser [Store]
parseJSON :: Value -> Parser Store
$cparseJSON :: Value -> Parser Store
FromJSON, [Store] -> Encoding
[Store] -> Value
Store -> Encoding
Store -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Store] -> Encoding
$ctoEncodingList :: [Store] -> Encoding
toJSONList :: [Store] -> Value
$ctoJSONList :: [Store] -> Value
toEncoding :: Store -> Encoding
$ctoEncoding :: Store -> Encoding
toJSON :: Store -> Value
$ctoJSON :: Store -> Value
ToJSON)

-- | A memory cell can be in one of three states.
data MemCell
  = -- | A cell starts out life as an unevaluated term together with
    --   its environment.
    E Term Env
  | -- | When the cell is 'Force'd, it is set to a 'Blackhole' while
    --   being evaluated.  If it is ever referenced again while still
    --   a 'Blackhole', that means it depends on itself in a way that
    --   would trigger an infinite loop, and we can signal an error.
    --   (Of course, we
    --   <http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html cannot
    --   detect /all/ infinite loops this way>.)
    --
    --   A 'Blackhole' saves the original 'Term' and 'Env' that are
    --   being evaluated; if Ctrl-C is used to cancel a computation
    --   while we are in the middle of evaluating a cell, the
    --   'Blackhole' can be reset to 'E'.
    Blackhole Term Env
  | -- | Once evaluation is complete, we cache the final 'Value' in
    --   the 'MemCell', so that subsequent lookups can just use it
    --   without recomputing anything.
    V Value
  deriving (Addr -> MemCell -> ShowS
[MemCell] -> ShowS
MemCell -> String
forall a.
(Addr -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MemCell] -> ShowS
$cshowList :: [MemCell] -> ShowS
show :: MemCell -> String
$cshow :: MemCell -> String
showsPrec :: Addr -> MemCell -> ShowS
$cshowsPrec :: Addr -> MemCell -> ShowS
Show, MemCell -> MemCell -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MemCell -> MemCell -> Bool
$c/= :: MemCell -> MemCell -> Bool
== :: MemCell -> MemCell -> Bool
$c== :: MemCell -> MemCell -> Bool
Eq, forall x. Rep MemCell x -> MemCell
forall x. MemCell -> Rep MemCell x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep MemCell x -> MemCell
$cfrom :: forall x. MemCell -> Rep MemCell x
Generic, Value -> Parser [MemCell]
Value -> Parser MemCell
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [MemCell]
$cparseJSONList :: Value -> Parser [MemCell]
parseJSON :: Value -> Parser MemCell
$cparseJSON :: Value -> Parser MemCell
FromJSON, [MemCell] -> Encoding
[MemCell] -> Value
MemCell -> Encoding
MemCell -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [MemCell] -> Encoding
$ctoEncodingList :: [MemCell] -> Encoding
toJSONList :: [MemCell] -> Value
$ctoJSONList :: [MemCell] -> Value
toEncoding :: MemCell -> Encoding
$ctoEncoding :: MemCell -> Encoding
toJSON :: MemCell -> Value
$ctoJSON :: MemCell -> Value
ToJSON)

emptyStore :: Store
emptyStore :: Store
emptyStore = Addr -> IntMap MemCell -> Store
Store Addr
0 forall a. IntMap a
IM.empty

-- | Allocate a new memory cell containing an unevaluated expression
--   with the current environment.  Return the index of the allocated
--   cell.
allocate :: Env -> Term -> Store -> (Addr, Store)
allocate :: Env -> Term -> Store -> (Addr, Store)
allocate Env
e Term
t (Store Addr
n IntMap MemCell
m) = (Addr
n, Addr -> IntMap MemCell -> Store
Store (Addr
n forall a. Num a => a -> a -> a
+ Addr
1) (forall a. Addr -> a -> IntMap a -> IntMap a
IM.insert Addr
n (Term -> Env -> MemCell
E Term
t Env
e) IntMap MemCell
m))

-- | Look up the cell at a given index.
lookupStore :: Addr -> Store -> Maybe MemCell
lookupStore :: Addr -> Store -> Maybe MemCell
lookupStore Addr
n = forall a. Addr -> IntMap a -> Maybe a
IM.lookup Addr
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. Store -> IntMap MemCell
mu

-- | Set the cell at a given index.
setStore :: Addr -> MemCell -> Store -> Store
setStore :: Addr -> MemCell -> Store -> Store
setStore Addr
n MemCell
c (Store Addr
nxt IntMap MemCell
m) = Addr -> IntMap MemCell -> Store
Store Addr
nxt (forall a. Addr -> a -> IntMap a -> IntMap a
IM.insert Addr
n MemCell
c IntMap MemCell
m)

------------------------------------------------------------
-- CESK machine
------------------------------------------------------------

-- | The overall state of a CESK machine, which can actually be one of
--   four kinds of states. The CESK machine is named after the first
--   kind of state, and it would probably be possible to inline a
--   bunch of things and get rid of the second state, but I find it
--   much more natural and elegant this way.  Most tutorial
--   presentations of CEK/CESK machines only have one kind of state, but
--   then again, most tutorial presentations only deal with the bare
--   lambda calculus, so one can tell whether a term is a value just
--   by seeing whether it is syntactically a lambda.  I learned this
--   approach from Harper's Practical Foundations of Programming
--   Languages.
data CESK
  = -- | When we are on our way "in/down" into a term, we have a
    --   currently focused term to evaluate in the environment, a store,
    --   and a continuation.  In this mode we generally pattern-match on the
    --   'Term' to decide what to do next.
    In Term Env Store Cont
  | -- | Once we finish evaluating a term, we end up with a 'Value'
    --   and we switch into "out" mode, bringing the value back up
    --   out of the depths to the context that was expecting it.  In
    --   this mode we generally pattern-match on the 'Cont' to decide
    --   what to do next.
    --
    --   Note that there is no 'Env', because we don't have anything
    --   with variables to evaluate at the moment, and we maintain the
    --   invariant that any unevaluated terms buried inside a 'Value'
    --   or 'Cont' must carry along their environment with them.
    Out Value Store Cont
  | -- | An exception has been raised.  Keep unwinding the
    --   continuation stack (until finding an enclosing 'Try' in the
    --   case of a command failure or a user-generated exception, or
    --   until the stack is empty in the case of a fatal exception).
    Up Exn Store Cont
  | -- | The machine is waiting for the game to reach a certain time
    --   to resume its execution.
    Waiting TickNumber CESK
  deriving (CESK -> CESK -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CESK -> CESK -> Bool
$c/= :: CESK -> CESK -> Bool
== :: CESK -> CESK -> Bool
$c== :: CESK -> CESK -> Bool
Eq, Addr -> CESK -> ShowS
[CESK] -> ShowS
CESK -> String
forall a.
(Addr -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CESK] -> ShowS
$cshowList :: [CESK] -> ShowS
show :: CESK -> String
$cshow :: CESK -> String
showsPrec :: Addr -> CESK -> ShowS
$cshowsPrec :: Addr -> CESK -> ShowS
Show, forall x. Rep CESK x -> CESK
forall x. CESK -> Rep CESK x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CESK x -> CESK
$cfrom :: forall x. CESK -> Rep CESK x
Generic, Value -> Parser [CESK]
Value -> Parser CESK
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [CESK]
$cparseJSONList :: Value -> Parser [CESK]
parseJSON :: Value -> Parser CESK
$cparseJSON :: Value -> Parser CESK
FromJSON, [CESK] -> Encoding
[CESK] -> Value
CESK -> Encoding
CESK -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [CESK] -> Encoding
$ctoEncodingList :: [CESK] -> Encoding
toJSONList :: [CESK] -> Value
$ctoJSONList :: [CESK] -> Value
toEncoding :: CESK -> Encoding
$ctoEncoding :: CESK -> Encoding
toJSON :: CESK -> Value
$ctoJSON :: CESK -> Value
ToJSON)

-- | Is the CESK machine in a final (finished) state?  If so, extract
--   the final value and store.
finalValue :: CESK -> Maybe (Value, Store)
{-# INLINE finalValue #-}
finalValue :: CESK -> Maybe (Value, Store)
finalValue (Out Value
v Store
s []) = forall a. a -> Maybe a
Just (Value
v, Store
s)
finalValue CESK
_ = forall a. Maybe a
Nothing

-- | Initialize a machine state with a starting term along with its
--   type; the term will be executed or just evaluated depending on
--   whether it has a command type or not.
initMachine :: ProcessedTerm -> Env -> Store -> CESK
initMachine :: ProcessedTerm -> Env -> Store -> CESK
initMachine ProcessedTerm
t Env
e Store
s = ProcessedTerm -> Env -> Store -> Cont -> CESK
initMachine' ProcessedTerm
t Env
e Store
s []

-- | Like 'initMachine', but also take an explicit starting continuation.
initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK
initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK
initMachine' (ProcessedTerm (Module Syntax' (Poly Type)
t' TCtx
ctx) Requirements
_ ReqCtx
reqCtx) Env
e Store
s Cont
k =
  case Syntax' (Poly Type)
t' forall s a. s -> Getting a s a -> a
^. forall ty. Lens' (Syntax' ty) ty
sType of
    -- If the starting term has a command type...
    Forall [Var]
_ (TyCmd Type
_) ->
      case TCtx
ctx of
        -- ...but doesn't contain any definitions, just create a machine
        -- that will evaluate it and then execute it.
        TCtx
Empty -> Term -> Env -> Store -> Cont -> CESK
In Term
t Env
e Store
s (Frame
FExec forall a. a -> [a] -> [a]
: Cont
k)
        -- Or, if it does contain definitions, then load the resulting
        -- context after executing it.
        TCtx
_ -> Term -> Env -> Store -> Cont -> CESK
In Term
t Env
e Store
s (Frame
FExec forall a. a -> [a] -> [a]
: TCtx -> ReqCtx -> Frame
FLoadEnv TCtx
ctx ReqCtx
reqCtx forall a. a -> [a] -> [a]
: Cont
k)
    -- Otherwise, for a term with a non-command type, just
    -- create a machine to evaluate it.
    Poly Type
_ -> Term -> Env -> Store -> Cont -> CESK
In Term
t Env
e Store
s Cont
k
 where
  -- Erase all type and SrcLoc annotations from the term before
  -- putting it in the machine state, since those are irrelevant at
  -- runtime.
  t :: Term
t = forall ty. Syntax' ty -> Term
eraseS Syntax' (Poly Type)
t'

-- | Cancel the currently running computation.
cancel :: CESK -> CESK
cancel :: CESK -> CESK
cancel CESK
cesk = Value -> Store -> Cont -> CESK
Out Value
VUnit Store
s' []
 where
  s' :: Store
s' = Store -> Store
resetBlackholes forall a b. (a -> b) -> a -> b
$ CESK -> Store
getStore CESK
cesk
  getStore :: CESK -> Store
getStore (In Term
_ Env
_ Store
s Cont
_) = Store
s
  getStore (Out Value
_ Store
s Cont
_) = Store
s
  getStore (Up Exn
_ Store
s Cont
_) = Store
s
  getStore (Waiting TickNumber
_ CESK
c) = CESK -> Store
getStore CESK
c

-- | Reset any 'Blackhole's in the 'Store'.  We need to use this any
--   time a running computation is interrupted, either by an exception
--   or by a Ctrl+C.
resetBlackholes :: Store -> Store
resetBlackholes :: Store -> Store
resetBlackholes (Store Addr
n IntMap MemCell
m) = Addr -> IntMap MemCell -> Store
Store Addr
n (forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map MemCell -> MemCell
resetBlackhole IntMap MemCell
m)
 where
  resetBlackhole :: MemCell -> MemCell
resetBlackhole (Blackhole Term
t Env
e) = Term -> Env -> MemCell
E Term
t Env
e
  resetBlackhole MemCell
c = MemCell
c

------------------------------------------------------------
-- Pretty printing CESK machine states
------------------------------------------------------------

instance PrettyPrec CESK where
  prettyPrec :: forall ann. Addr -> CESK -> Doc ann
prettyPrec Addr
_ (In Term
c Env
_ Store
_ Cont
k) = forall ann. Cont -> (Addr, Doc ann) -> Doc ann
prettyCont Cont
k (Addr
11, Doc ann
"▶" forall a. Semigroup a => a -> a -> a
<> forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
c forall a. Semigroup a => a -> a -> a
<> Doc ann
"◀")
  prettyPrec Addr
_ (Out Value
v Store
_ Cont
k) = forall ann. Cont -> (Addr, Doc ann) -> Doc ann
prettyCont Cont
k (Addr
11, Doc ann
"◀" forall a. Semigroup a => a -> a -> a
<> forall a ann. PrettyPrec a => a -> Doc ann
ppr (Value -> Term
valueToTerm Value
v) forall a. Semigroup a => a -> a -> a
<> Doc ann
"▶")
  prettyPrec Addr
_ (Up Exn
e Store
_ Cont
k) = forall ann. Cont -> (Addr, Doc ann) -> Doc ann
prettyCont Cont
k (Addr
11, Doc ann
"!" forall a. Semigroup a => a -> a -> a
<> (forall a ann. Pretty a => a -> Doc ann
pretty (EntityMap -> Exn -> Var
formatExn forall a. Monoid a => a
mempty Exn
e) forall a. Semigroup a => a -> a -> a
<> Doc ann
"!"))
  prettyPrec Addr
_ (Waiting TickNumber
t CESK
cesk) = Doc ann
"🕑" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty TickNumber
t forall a. Semigroup a => a -> a -> a
<> Doc ann
"(" forall a. Semigroup a => a -> a -> a
<> forall a ann. PrettyPrec a => a -> Doc ann
ppr CESK
cesk forall a. Semigroup a => a -> a -> a
<> Doc ann
")"

-- | Take a continuation, and the pretty-printed expression which is
--   the focus of the continuation (i.e. the expression whose value
--   will be given to the continuation) along with its top-level
--   precedence, and pretty-print the whole thing.
--
--   As much as possible, we try to print to look like an *expression*
--   with a currently focused part, that is, we print the continuation
--   from the inside out instead of as a list of frames.  This makes
--   it much more intuitive to read.
prettyCont :: Cont -> (Int, Doc ann) -> Doc ann
prettyCont :: forall ann. Cont -> (Addr, Doc ann) -> Doc ann
prettyCont [] (Addr
_, Doc ann
inner) = Doc ann
inner
prettyCont (Frame
f : Cont
k) (Addr, Doc ann)
inner = forall ann. Cont -> (Addr, Doc ann) -> Doc ann
prettyCont Cont
k (forall ann. Frame -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyFrame Frame
f (Addr, Doc ann)
inner)

-- | Pretty-print a single continuation frame, given its already
--   pretty-printed focus.  In particular, given a frame and its
--   "inside" (i.e. the expression or other frames being focused on,
--   whose value will eventually be passed to this frame), with the
--   precedence of the inside's top-level construct, return a
--   pretty-printed version of the entire frame along with its
--   top-level precedence.
prettyFrame :: Frame -> (Int, Doc ann) -> (Int, Doc ann)
prettyFrame :: forall ann. Frame -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyFrame (FSnd Term
t Env
_) (Addr
_, Doc ann
inner) = (Addr
11, Doc ann
"(" forall a. Semigroup a => a -> a -> a
<> Doc ann
inner forall a. Semigroup a => a -> a -> a
<> Doc ann
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t forall a. Semigroup a => a -> a -> a
<> Doc ann
")")
prettyFrame (FFst Value
v) (Addr
_, Doc ann
inner) = (Addr
11, Doc ann
"(" forall a. Semigroup a => a -> a -> a
<> forall a ann. PrettyPrec a => a -> Doc ann
ppr (Value -> Term
valueToTerm Value
v) forall a. Semigroup a => a -> a -> a
<> Doc ann
"," forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
inner forall a. Semigroup a => a -> a -> a
<> Doc ann
")")
prettyFrame (FArg Term
t Env
_) (Addr
p, Doc ann
inner) = (Addr
10, forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p forall a. Ord a => a -> a -> Bool
< Addr
10) Doc ann
inner forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => Addr -> a -> Doc ann
prettyPrec Addr
11 Term
t)
prettyFrame (FApp Value
v) (Addr
p, Doc ann
inner) = (Addr
10, forall a ann. PrettyPrec a => Addr -> a -> Doc ann
prettyPrec Addr
10 (Value -> Term
valueToTerm Value
v) forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner)
prettyFrame (FLet Var
x Term
t Env
_) (Addr
_, Doc ann
inner) = (Addr
11, forall ann. [Doc ann] -> Doc ann
hsep [Doc ann
"let", forall a ann. Pretty a => a -> Doc ann
pretty Var
x, Doc ann
"=", Doc ann
inner, Doc ann
"in", forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t])
prettyFrame (FTry Value
v) (Addr
p, Doc ann
inner) = (Addr
10, Doc ann
"try" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => Addr -> a -> Doc ann
prettyPrec Addr
11 (Value -> Term
valueToTerm Value
v))
prettyFrame (FUnionEnv Env
_) (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"∪·" (Addr, Doc ann)
inner
prettyFrame (FLoadEnv TCtx
_ ReqCtx
_) (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"L·" (Addr, Doc ann)
inner
prettyFrame (FDef Var
x) (Addr
_, Doc ann
inner) = (Addr
11, Doc ann
"def" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Var
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
inner forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"end")
prettyFrame Frame
FExec (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"E·" (Addr, Doc ann)
inner
prettyFrame (FBind Maybe Var
Nothing Term
t Env
_) (Addr
p, Doc ann
inner) = (Addr
0, forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p forall a. Ord a => a -> a -> Bool
< Addr
1) Doc ann
inner forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
";" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t)
prettyFrame (FBind (Just Var
x) Term
t Env
_) (Addr
p, Doc ann
inner) = (Addr
0, forall ann. [Doc ann] -> Doc ann
hsep [forall a ann. Pretty a => a -> Doc ann
pretty Var
x, Doc ann
"<-", forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p forall a. Ord a => a -> a -> Bool
< Addr
1) Doc ann
inner, Doc ann
";", forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t])
prettyFrame Frame
FDiscardEnv (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"D·" (Addr, Doc ann)
inner
prettyFrame (FImmediate Const
c [WorldUpdate Entity]
_worldUpds [RobotUpdate]
_robotUpds) (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix (Doc ann
"I[" forall a. Semigroup a => a -> a -> a
<> forall a ann. PrettyPrec a => a -> Doc ann
ppr Const
c forall a. Semigroup a => a -> a -> a
<> Doc ann
"]·") (Addr, Doc ann)
inner
prettyFrame (FUpdate Addr
addr) (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix (Doc ann
"S@" forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Addr
addr) (Addr, Doc ann)
inner
prettyFrame Frame
FFinishAtomic (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"A·" (Addr, Doc ann)
inner
prettyFrame (FMeetAll Value
_ [Addr]
_) (Addr, Doc ann)
inner = forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"M·" (Addr, Doc ann)
inner
prettyFrame (FRcd Env
_ [(Var, Value)]
done Var
foc [(Var, Maybe Term)]
rest) (Addr
_, Doc ann
inner) = (Addr
11, forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ann
"[" Doc ann
"]" Doc ann
", " (forall {ann}. [Doc ann]
pDone forall a. [a] -> [a] -> [a]
++ [Doc ann
pFoc] forall a. [a] -> [a] -> [a]
++ forall {ann}. [Doc ann]
pRest))
 where
  pDone :: [Doc ann]
pDone = forall a b. (a -> b) -> [a] -> [b]
map (\(Var
x, Value
v) -> forall a ann. Pretty a => a -> Doc ann
pretty Var
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => a -> Doc ann
ppr (Value -> Term
valueToTerm Value
v)) (forall a. [a] -> [a]
reverse [(Var, Value)]
done)
  pFoc :: Doc ann
pFoc = forall a ann. Pretty a => a -> Doc ann
pretty Var
foc forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
inner
  pRest :: [Doc ann]
pRest = forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a} {ann}.
(Pretty a, PrettyPrec a) =>
(a, Maybe a) -> Doc ann
pprEq [(Var, Maybe Term)]
rest
  pprEq :: (a, Maybe a) -> Doc ann
pprEq (a
x, Maybe a
Nothing) = forall a ann. Pretty a => a -> Doc ann
pretty a
x
  pprEq (a
x, Just a
t) = forall a ann. Pretty a => a -> Doc ann
pretty a
x forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. PrettyPrec a => a -> Doc ann
ppr a
t
prettyFrame (FProj Var
x) (Addr
p, Doc ann
inner) = (Addr
11, forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner forall a. Semigroup a => a -> a -> a
<> Doc ann
"." forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Var
x)

-- | Pretty-print a special "prefix application" frame, i.e. a frame
--   formatted like @X· inner@.  Unlike typical applications, these
--   associate to the *right*, so that we can print something like @X·
--   Y· Z· inner@ with no parens.
prettyPrefix :: Doc ann -> (Int, Doc ann) -> (Int, Doc ann)
prettyPrefix :: forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
pre (Addr
p, Doc ann
inner) = (Addr
11, Doc ann
pre forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner)

--------------------------------------------------------------
-- Runtime robot update
--------------------------------------------------------------

-- | Enumeration of robot updates.  This type is used for changes by
--   /e.g./ the @drill@ command which must be carried out at a later
--   tick. Using a first-order representation (as opposed to /e.g./
--   just a @Robot -> Robot@ function) allows us to serialize and
--   inspect the updates.
--
--   Note that this can not be in 'Swarm.Game.Robot' as it would create
--   a cyclic dependency.
data RobotUpdate
  = -- | Add copies of an entity to the robot's inventory.
    AddEntity Count Entity
  | -- | Make the robot learn about an entity.
    LearnEntity Entity
  deriving (RobotUpdate -> RobotUpdate -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RobotUpdate -> RobotUpdate -> Bool
$c/= :: RobotUpdate -> RobotUpdate -> Bool
== :: RobotUpdate -> RobotUpdate -> Bool
$c== :: RobotUpdate -> RobotUpdate -> Bool
Eq, Eq RobotUpdate
RobotUpdate -> RobotUpdate -> Bool
RobotUpdate -> RobotUpdate -> Ordering
RobotUpdate -> RobotUpdate -> RobotUpdate
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RobotUpdate -> RobotUpdate -> RobotUpdate
$cmin :: RobotUpdate -> RobotUpdate -> RobotUpdate
max :: RobotUpdate -> RobotUpdate -> RobotUpdate
$cmax :: RobotUpdate -> RobotUpdate -> RobotUpdate
>= :: RobotUpdate -> RobotUpdate -> Bool
$c>= :: RobotUpdate -> RobotUpdate -> Bool
> :: RobotUpdate -> RobotUpdate -> Bool
$c> :: RobotUpdate -> RobotUpdate -> Bool
<= :: RobotUpdate -> RobotUpdate -> Bool
$c<= :: RobotUpdate -> RobotUpdate -> Bool
< :: RobotUpdate -> RobotUpdate -> Bool
$c< :: RobotUpdate -> RobotUpdate -> Bool
compare :: RobotUpdate -> RobotUpdate -> Ordering
$ccompare :: RobotUpdate -> RobotUpdate -> Ordering
Ord, Addr -> RobotUpdate -> ShowS
[RobotUpdate] -> ShowS
RobotUpdate -> String
forall a.
(Addr -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RobotUpdate] -> ShowS
$cshowList :: [RobotUpdate] -> ShowS
show :: RobotUpdate -> String
$cshow :: RobotUpdate -> String
showsPrec :: Addr -> RobotUpdate -> ShowS
$cshowsPrec :: Addr -> RobotUpdate -> ShowS
Show, forall x. Rep RobotUpdate x -> RobotUpdate
forall x. RobotUpdate -> Rep RobotUpdate x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RobotUpdate x -> RobotUpdate
$cfrom :: forall x. RobotUpdate -> Rep RobotUpdate x
Generic, Value -> Parser [RobotUpdate]
Value -> Parser RobotUpdate
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [RobotUpdate]
$cparseJSONList :: Value -> Parser [RobotUpdate]
parseJSON :: Value -> Parser RobotUpdate
$cparseJSON :: Value -> Parser RobotUpdate
FromJSON, [RobotUpdate] -> Encoding
[RobotUpdate] -> Value
RobotUpdate -> Encoding
RobotUpdate -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [RobotUpdate] -> Encoding
$ctoEncodingList :: [RobotUpdate] -> Encoding
toJSONList :: [RobotUpdate] -> Value
$ctoJSONList :: [RobotUpdate] -> Value
toEncoding :: RobotUpdate -> Encoding
$ctoEncoding :: RobotUpdate -> Encoding
toJSON :: RobotUpdate -> Value
$ctoJSON :: RobotUpdate -> Value
ToJSON)