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

-- |
-- SPDX-License-Identifier: BSD-3-Clause
-- Description: State machine of Swarm's interpreter
--
-- 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,
  allocate,
  resolveValue,
  lookupStore,
  setStore,

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

  -- ** Construction
  initMachine,
  continue,
  cancel,
  prepareTerm,

  -- ** Extracting information
  finalValue,
  suspendedEnv,
  store,
  cont,
) where

import Control.Lens (Lens', Traversal', lens, traversal, (^.))
import Data.Aeson (FromJSON (..), ToJSON (..), genericParseJSON, genericToJSON)
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 (Entity)
import Swarm.Game.Exception
import Swarm.Game.Ingredients (Count)
import Swarm.Game.Tick
import Swarm.Game.World (WorldUpdate (..))
import Swarm.Language.Elaborate (insertSuspend)
import Swarm.Language.Requirements.Type (Requirements)
import Swarm.Language.Syntax
import Swarm.Language.Types
import Swarm.Language.Value as V
import Swarm.Pretty (PrettyPrec (..), pparens, ppr)
import Swarm.Util.JSON (optionsMinimize)

------------------------------------------------------------
-- 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
  | -- | @FVArg v@ says that we were evaluating the left-hand side of
    --   an application, and the next thing we should do is apply it
    --   to the given value.  This does not normally occur as part of
    --   the usual evaluation process for applications, which instead
    --   uses FArg.  However, it is sometimes useful when reducing
    --   other constructs---for example, the pair eliminator 'match'.
    FVArg Value
  | -- | @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 ty t2 e@ says that we were evaluating a term @t1@ of
    -- type @ty@ 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 (Maybe (Polytype, Requirements)) 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
  | -- | 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) (Maybe (Polytype, Requirements)) Term Env
  | -- | 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 cell at a certain location in the store with the computed value.
    FUpdate Addr
  | -- | Signal that we are done with an atomic computation.
    FFinishAtomic
  | -- | 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
  | -- | We should suspend with the given environment once we finish
    --   the current evaluation.
    FSuspend Env
  | -- | If an exception bubbles all the way up to this frame, then
    --   switch to Suspended mode with this saved top-level context.
    FRestoreEnv Env
  deriving ((forall x. Frame -> Rep Frame x)
-> (forall x. Rep Frame x -> Frame) -> Generic Frame
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
$cfrom :: forall x. Frame -> Rep Frame x
from :: forall x. Frame -> Rep Frame x
$cto :: forall x. Rep Frame x -> Frame
to :: forall x. Rep Frame x -> Frame
Generic)

instance ToJSON Frame where
  toJSON :: Frame -> Value
toJSON = Options -> Frame -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
optionsMinimize

-- | 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 'Value's.
data Store = Store {Store -> Addr
next :: Addr, Store -> IntMap Value
mu :: IntMap Value}
  deriving ((forall x. Store -> Rep Store x)
-> (forall x. Rep Store x -> Store) -> Generic Store
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
$cfrom :: forall x. Store -> Rep Store x
from :: forall x. Store -> Rep Store x
$cto :: forall x. Rep Store x -> Store
to :: forall x. Rep Store x -> Store
Generic, [Store] -> Value
[Store] -> Encoding
Store -> Bool
Store -> Value
Store -> Encoding
(Store -> Value)
-> (Store -> Encoding)
-> ([Store] -> Value)
-> ([Store] -> Encoding)
-> (Store -> Bool)
-> ToJSON Store
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> (a -> Bool)
-> ToJSON a
$ctoJSON :: Store -> Value
toJSON :: Store -> Value
$ctoEncoding :: Store -> Encoding
toEncoding :: Store -> Encoding
$ctoJSONList :: [Store] -> Value
toJSONList :: [Store] -> Value
$ctoEncodingList :: [Store] -> Encoding
toEncodingList :: [Store] -> Encoding
$comitField :: Store -> Bool
omitField :: Store -> Bool
ToJSON)

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

-- | Allocate a new memory cell containing a given value.  Return the
--   index of the allocated cell.
allocate :: Value -> Store -> (Addr, Store)
allocate :: Value -> Store -> (Addr, Store)
allocate Value
v (Store Addr
n IntMap Value
m) = (Addr
n, Addr -> IntMap Value -> Store
Store (Addr
n Addr -> Addr -> Addr
forall a. Num a => a -> a -> a
+ Addr
1) (Addr -> Value -> IntMap Value -> IntMap Value
forall a. Addr -> a -> IntMap a -> IntMap a
IM.insert Addr
n Value
v IntMap Value
m))

-- | Resolve a value, recursively looking up any indirections in the
--   store.
resolveValue :: Store -> Value -> Either Addr Value
resolveValue :: Store -> Value -> Either Addr Value
resolveValue Store
s = \case
  VIndir Addr
loc -> Store -> Addr -> Either Addr Value
lookupStore Store
s Addr
loc
  Value
v -> Value -> Either Addr Value
forall a b. b -> Either a b
Right Value
v

-- | Look up the value at a given index, but keep following
--   indirections until encountering a value that is not a 'VIndir'.
lookupStore :: Store -> Addr -> Either Addr Value
lookupStore :: Store -> Addr -> Either Addr Value
lookupStore Store
s = Addr -> Either Addr Value
go
 where
  go :: Addr -> Either Addr Value
go Addr
loc = case Addr -> IntMap Value -> Maybe Value
forall a. Addr -> IntMap a -> Maybe a
IM.lookup Addr
loc (Store -> IntMap Value
mu Store
s) of
    Maybe Value
Nothing -> Addr -> Either Addr Value
forall a b. a -> Either a b
Left Addr
loc
    Just Value
v -> case Value
v of
      VIndir Addr
loc' -> Addr -> Either Addr Value
go Addr
loc'
      Value
_ -> Value -> Either Addr Value
forall a b. b -> Either a b
Right Value
v

-- | Set the value at a given index.
setStore :: Addr -> Value -> Store -> Store
setStore :: Addr -> Value -> Store -> Store
setStore Addr
n Value
c (Store Addr
nxt IntMap Value
m) = Addr -> IntMap Value -> Store
Store Addr
nxt (Addr -> Value -> IntMap Value -> IntMap Value
forall a. Addr -> a -> IntMap a -> IntMap a
IM.insert Addr
n Value
c IntMap Value
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
  | -- | The machine is suspended, i.e. waiting for another term to
    --   evaluate.  This happens after we have evaluated whatever the
    --   user entered at the REPL and we are waiting for them to type
    --   something else.  Conceptually, this is like a combination of
    --   'Out' and 'In': we store a 'Value' that was just yielded by
    --   evaluation, and otherwise it is just like 'In' with a hole
    --   for the 'Term' we are going to evaluate.
    Suspended Value Env Store Cont
  deriving ((forall x. CESK -> Rep CESK x)
-> (forall x. Rep CESK x -> CESK) -> Generic CESK
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
$cfrom :: forall x. CESK -> Rep CESK x
from :: forall x. CESK -> Rep CESK x
$cto :: forall x. Rep CESK x -> CESK
to :: forall x. Rep CESK x -> CESK
Generic)

instance ToJSON CESK where
  toJSON :: CESK -> Value
toJSON = Options -> CESK -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
optionsMinimize

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

-- | Extract the environment from a suspended CESK machine (/e.g./ to
--   use for typechecking).
suspendedEnv :: Traversal' CESK Env
suspendedEnv :: Traversal' CESK Env
suspendedEnv = ((Env -> f Env) -> CESK -> f CESK)
-> (Env -> f Env) -> CESK -> f CESK
forall a (f :: * -> *) b s t.
((a -> f b) -> s -> f t) -> (a -> f b) -> s -> f t
traversal (Env -> f Env) -> CESK -> f CESK
Traversal' CESK Env
go
 where
  go :: Applicative f => (Env -> f Env) -> CESK -> f CESK
  go :: Traversal' CESK Env
go Env -> f Env
f (Suspended Value
v Env
e Store
s [Frame]
k) = Value -> Env -> Store -> [Frame] -> CESK
Suspended Value
v (Env -> Store -> [Frame] -> CESK)
-> f Env -> f (Store -> [Frame] -> CESK)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> f Env
f Env
e f (Store -> [Frame] -> CESK) -> f Store -> f ([Frame] -> CESK)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Store -> f Store
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Store
s f ([Frame] -> CESK) -> f [Frame] -> f CESK
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Frame] -> f [Frame]
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Frame]
k
  go Env -> f Env
_ CESK
cesk = CESK -> f CESK
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CESK
cesk

-- | Lens focusing on the store of a CESK machine.
store :: Lens' CESK Store
store :: Lens' CESK Store
store = (CESK -> Store) -> (CESK -> Store -> CESK) -> Lens' CESK Store
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CESK -> Store
get CESK -> Store -> CESK
set
 where
  get :: CESK -> Store
get = \case
    In Term
_ Env
_ Store
s [Frame]
_ -> Store
s
    Out Value
_ Store
s [Frame]
_ -> Store
s
    Up Exn
_ Store
s [Frame]
_ -> Store
s
    Waiting TickNumber
_ CESK
c -> CESK -> Store
get CESK
c
    Suspended Value
_ Env
_ Store
s [Frame]
_ -> Store
s
  set :: CESK -> Store -> CESK
set CESK
cesk Store
s = case CESK
cesk of
    In Term
t Env
e Store
_ [Frame]
k -> Term -> Env -> Store -> [Frame] -> CESK
In Term
t Env
e Store
s [Frame]
k
    Out Value
v Store
_ [Frame]
k -> Value -> Store -> [Frame] -> CESK
Out Value
v Store
s [Frame]
k
    Up Exn
x Store
_ [Frame]
k -> Exn -> Store -> [Frame] -> CESK
Up Exn
x Store
s [Frame]
k
    Waiting TickNumber
t CESK
c -> TickNumber -> CESK -> CESK
Waiting TickNumber
t (CESK -> Store -> CESK
set CESK
c Store
s)
    Suspended Value
v Env
e Store
_ [Frame]
k -> Value -> Env -> Store -> [Frame] -> CESK
Suspended Value
v Env
e Store
s [Frame]
k

-- | Lens focusing on the continuation of a CESK machine.
cont :: Lens' CESK Cont
cont :: Lens' CESK [Frame]
cont = (CESK -> [Frame])
-> (CESK -> [Frame] -> CESK) -> Lens' CESK [Frame]
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CESK -> [Frame]
get CESK -> [Frame] -> CESK
set
 where
  get :: CESK -> [Frame]
get = \case
    In Term
_ Env
_ Store
_ [Frame]
k -> [Frame]
k
    Out Value
_ Store
_ [Frame]
k -> [Frame]
k
    Up Exn
_ Store
_ [Frame]
k -> [Frame]
k
    Waiting TickNumber
_ CESK
c -> CESK -> [Frame]
get CESK
c
    Suspended Value
_ Env
_ Store
_ [Frame]
k -> [Frame]
k
  set :: CESK -> [Frame] -> CESK
set CESK
cesk [Frame]
k = case CESK
cesk of
    In Term
t Env
e Store
s [Frame]
_ -> Term -> Env -> Store -> [Frame] -> CESK
In Term
t Env
e Store
s [Frame]
k
    Out Value
v Store
s [Frame]
_ -> Value -> Store -> [Frame] -> CESK
Out Value
v Store
s [Frame]
k
    Up Exn
x Store
s [Frame]
_ -> Exn -> Store -> [Frame] -> CESK
Up Exn
x Store
s [Frame]
k
    Waiting TickNumber
t CESK
c -> TickNumber -> CESK -> CESK
Waiting TickNumber
t (CESK -> [Frame] -> CESK
set CESK
c [Frame]
k)
    Suspended Value
v Env
e Store
s [Frame]
_ -> Value -> Env -> Store -> [Frame] -> CESK
Suspended Value
v Env
e Store
s [Frame]
k

-- | Create a brand new CESK machine, with empty environment and
--   store, to evaluate a given term.  We always initialize the
--   machine with a single FExec frame as the continuation; if the
--   given term does not have a command type, we wrap it in @pure@.
initMachine :: TSyntax -> CESK
initMachine :: TSyntax -> CESK
initMachine TSyntax
t = Term -> Env -> Store -> [Frame] -> CESK
In (Env -> TSyntax -> Term
prepareTerm Env
V.emptyEnv TSyntax
t) Env
V.emptyEnv Store
emptyStore [Frame
FExec]

-- | Load a program into an existing robot CESK machine: either
--   continue from a suspended state, or, as a fallback, start from
--   scratch with an empty environment but the same store.
--
--   Also insert a @suspend@ primitive at the end, so the resulting
--   term is suitable for execution by the base (REPL) robot.
continue :: TSyntax -> CESK -> CESK
continue :: TSyntax -> CESK -> CESK
continue TSyntax
t = \case
  -- The normal case is when we are continuing from a suspended state. We:
  --
  --   (1) insert a suspend call at the end of the term, so that in
  --   the normal case after executing the entire term we will suspend
  --   in the innermost scope, to continue executing another term
  --   within that scope later.
  --
  --   (2) insert a failsafe FRestoreEnv frame into the continuation
  --   stack, in case execution of the term throws an exception.  In
  --   that case we will fall back to suspending with the original
  --   environment e (any names brought into scope by executing the
  --   term will be discarded).  If the term succeeds, the extra
  --   FRestoreEnv frame will be discarded.
  Suspended Value
_ Env
e Store
s [Frame]
k -> Term -> Env -> Store -> [Frame] -> CESK
In (Term -> Term
insertSuspend (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Env -> TSyntax -> Term
prepareTerm Env
e TSyntax
t) Env
e Store
s (Frame
FExec Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: Env -> Frame
FRestoreEnv Env
e Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: [Frame]
k)
  -- In any other state, just start with an empty environment.  This
  -- happens e.g. when running a program on the base robot for the
  -- very first time.
  CESK
cesk -> Term -> Env -> Store -> [Frame] -> CESK
In (Term -> Term
insertSuspend (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Env -> TSyntax -> Term
prepareTerm Env
V.emptyEnv TSyntax
t) Env
V.emptyEnv (CESK
cesk CESK -> Getting Store CESK Store -> Store
forall s a. s -> Getting a s a -> a
^. Getting Store CESK Store
Lens' CESK Store
store) (Frame
FExec Frame -> [Frame] -> [Frame]
forall a. a -> [a] -> [a]
: (CESK
cesk CESK -> Getting [Frame] CESK [Frame] -> [Frame]
forall s a. s -> Getting a s a -> a
^. Getting [Frame] CESK [Frame]
Lens' CESK [Frame]
cont))

-- | Prepare a term for evaluation by a CESK machine in the given
--   environment: erase all type annotations, and optionally wrap it
--   in @pure@ if it does not have a command type.  Note that since
--   the environment might contain type aliases, we have to be careful
--   to expand them before concluding whether the term has a command
--   type or not.
prepareTerm :: Env -> TSyntax -> Term
prepareTerm :: Env -> TSyntax -> Term
prepareTerm Env
e TSyntax
t = case TDCtx -> Type -> Type
whnfType (Env
e Env -> Getting TDCtx Env TDCtx -> TDCtx
forall s a. s -> Getting a s a -> a
^. Getting TDCtx Env TDCtx
Lens' Env TDCtx
envTydefs) (Poly 'Quantified Type -> Type
forall (q :: ImplicitQuantification) t. Poly q t -> t
ptBody (TSyntax
t TSyntax
-> Getting (Poly 'Quantified Type) TSyntax (Poly 'Quantified Type)
-> Poly 'Quantified Type
forall s a. s -> Getting a s a -> a
^. Getting (Poly 'Quantified Type) TSyntax (Poly 'Quantified Type)
forall ty (f :: * -> *).
Functor f =>
(ty -> f ty) -> Syntax' ty -> f (Syntax' ty)
sType)) of
  TyCmd Type
_ -> Term
t'
  Type
_ -> Term -> Term -> Term
TApp (Const -> Term
forall ty. Const -> Term' ty
TConst Const
Pure) Term
t'
 where
  t' :: Term
t' = TSyntax -> Term
forall ty. Syntax' ty -> Term
eraseS TSyntax
t

-- | Cancel the currently running computation.
cancel :: CESK -> CESK
cancel :: CESK -> CESK
cancel CESK
cesk = Exn -> Store -> [Frame] -> CESK
Up Exn
Cancel (CESK
cesk CESK -> Getting Store CESK Store -> Store
forall s a. s -> Getting a s a -> a
^. Getting Store CESK Store
Lens' CESK Store
store) (CESK
cesk CESK -> Getting [Frame] CESK [Frame] -> [Frame]
forall s a. s -> Getting a s a -> a
^. Getting [Frame] CESK [Frame]
Lens' CESK [Frame]
cont)

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

instance PrettyPrec CESK where
  prettyPrec :: forall ann. Addr -> CESK -> Doc ann
prettyPrec Addr
_ = \case
    In Term
c Env
_ Store
_ [Frame]
k -> [Frame] -> (Addr, Doc ann) -> Doc ann
forall ann. [Frame] -> (Addr, Doc ann) -> Doc ann
prettyCont [Frame]
k (Addr
11, Doc ann
"▶" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
c Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"◀")
    Out Value
v Store
_ [Frame]
k -> [Frame] -> (Addr, Doc ann) -> Doc ann
forall ann. [Frame] -> (Addr, Doc ann) -> Doc ann
prettyCont [Frame]
k (Addr
11, Doc ann
"◀" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr (Value -> Term
valueToTerm Value
v) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"▶")
    Up Exn
e Store
_ [Frame]
k -> [Frame] -> (Addr, Doc ann) -> Doc ann
forall ann. [Frame] -> (Addr, Doc ann) -> Doc ann
prettyCont [Frame]
k (Addr
11, Doc ann
"!" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> (Var -> Doc ann
forall ann. Var -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (EntityMap -> Exn -> Var
formatExn EntityMap
forall a. Monoid a => a
mempty Exn
e) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"!"))
    Waiting TickNumber
t CESK
cesk -> Doc ann
"🕑" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> TickNumber -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. TickNumber -> Doc ann
pretty TickNumber
t Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> CESK -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr CESK
cesk Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")"
    Suspended Value
v Env
_ Store
_ [Frame]
k -> [Frame] -> (Addr, Doc ann) -> Doc ann
forall ann. [Frame] -> (Addr, Doc ann) -> Doc ann
prettyCont [Frame]
k (Addr
11, Doc ann
"◀" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr (Value -> Term
valueToTerm Value
v) Doc ann -> Doc ann -> Doc ann
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. [Frame] -> (Addr, Doc ann) -> Doc ann
prettyCont [] (Addr
_, Doc ann
inner) = Doc ann
inner
prettyCont (Frame
f : [Frame]
k) (Addr, Doc ann)
inner = [Frame] -> (Addr, Doc ann) -> Doc ann
forall ann. [Frame] -> (Addr, Doc ann) -> Doc ann
prettyCont [Frame]
k (Frame -> (Addr, Doc ann) -> (Addr, Doc ann)
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 Frame
f (Addr
p, Doc ann
inner) = case Frame
f of
  FSnd Term
t Env
_ -> (Addr
11, Doc ann
"(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
inner Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"," Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")")
  FFst Value
v -> (Addr
11, Doc ann
"(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr (Value -> Term
valueToTerm Value
v) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"," Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
inner Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")")
  FArg Term
t Env
_ -> (Addr
10, Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
10) Doc ann
inner Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Addr -> Term -> Doc ann
forall ann. Addr -> Term -> Doc ann
forall a ann. PrettyPrec a => Addr -> a -> Doc ann
prettyPrec Addr
11 Term
t)
  FVArg Value
v -> (Addr
10, Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
10) Doc ann
inner Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Addr -> Term -> Doc ann
forall ann. Addr -> Term -> Doc ann
forall a ann. PrettyPrec a => Addr -> a -> Doc ann
prettyPrec Addr
11 (Value -> Term
valueToTerm Value
v))
  FApp Value
v -> (Addr
10, Addr -> Term -> Doc ann
forall ann. Addr -> Term -> Doc ann
forall a ann. PrettyPrec a => Addr -> a -> Doc ann
prettyPrec Addr
10 (Value -> Term
valueToTerm Value
v) Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner)
  FLet Var
x Maybe (Poly 'Quantified Type, Requirements)
_ Term
t Env
_ -> (Addr
11, [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Doc ann
"let", Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x, Doc ann
"=", Doc ann
inner, Doc ann
"in", Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t])
  FTry Value
v -> (Addr
10, Doc ann
"try" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Addr -> Term -> Doc ann
forall ann. Addr -> Term -> Doc ann
forall a ann. PrettyPrec a => Addr -> a -> Doc ann
prettyPrec Addr
11 (Value -> Term
valueToTerm Value
v))
  Frame
FExec -> Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"E·" (Addr
p, Doc ann
inner)
  FBind Maybe Var
Nothing Maybe (Poly 'Quantified Type, Requirements)
_ Term
t Env
_ -> (Addr
0, Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
1) Doc ann
inner Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
";" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t)
  FBind (Just Var
x) Maybe (Poly 'Quantified Type, Requirements)
_ Term
t Env
_ -> (Addr
0, [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
hsep [Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x, Doc ann
"<-", Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
1) Doc ann
inner, Doc ann
";", Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Term
t])
  FImmediate Const
c [WorldUpdate Entity]
_worldUpds [RobotUpdate]
_robotUpds -> Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix (Doc ann
"I[" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Const -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Const
c Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"]·") (Addr
p, Doc ann
inner)
  FUpdate {} -> (Addr
p, Doc ann
inner)
  Frame
FFinishAtomic -> Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
forall ann. Doc ann -> (Addr, Doc ann) -> (Addr, Doc ann)
prettyPrefix Doc ann
"A·" (Addr
p, Doc ann
inner)
  FRcd Env
_ [(Var, Value)]
done Var
foc [(Var, Maybe Term)]
rest -> (Addr
11, Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ann
"[" Doc ann
"]" Doc ann
", " ([Doc ann]
forall {ann}. [Doc ann]
pDone [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Doc ann
pFoc] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Doc ann]
forall {ann}. [Doc ann]
pRest))
   where
    pDone :: [Doc ann]
pDone = ((Var, Value) -> Doc ann) -> [(Var, Value)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
x, Value
v) -> Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Term -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr (Value -> Term
valueToTerm Value
v)) ([(Var, Value)] -> [(Var, Value)]
forall a. [a] -> [a]
reverse [(Var, Value)]
done)
    pFoc :: Doc ann
pFoc = Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
foc Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
inner
    pRest :: [Doc ann]
pRest = ((Var, Maybe Term) -> Doc ann) -> [(Var, Maybe Term)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Maybe Term) -> Doc ann
forall {a} {a} {ann}.
(PrettyPrec 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) = a -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr a
x
    pprEq (a
x, Just a
t) = a -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr a
x Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"=" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr a
t
  FProj Var
x -> (Addr
11, Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
"." Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Var -> Doc ann
forall a ann. PrettyPrec a => a -> Doc ann
ppr Var
x)
  FSuspend Env
_ -> (Addr
10, Doc ann
"suspend" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner)
  FRestoreEnv Env
_ -> (Addr
10, Doc ann
"restore" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
forall a. Ord a => a -> a -> Bool
< Addr
11) Doc ann
inner)

-- | 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 Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann -> Doc ann
forall ann. Bool -> Doc ann -> Doc ann
pparens (Addr
p Addr -> Addr -> Bool
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
(RobotUpdate -> RobotUpdate -> Bool)
-> (RobotUpdate -> RobotUpdate -> Bool) -> Eq RobotUpdate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RobotUpdate -> RobotUpdate -> Bool
== :: RobotUpdate -> RobotUpdate -> Bool
$c/= :: RobotUpdate -> RobotUpdate -> Bool
/= :: RobotUpdate -> RobotUpdate -> Bool
Eq, Eq RobotUpdate
Eq RobotUpdate =>
(RobotUpdate -> RobotUpdate -> Ordering)
-> (RobotUpdate -> RobotUpdate -> Bool)
-> (RobotUpdate -> RobotUpdate -> Bool)
-> (RobotUpdate -> RobotUpdate -> Bool)
-> (RobotUpdate -> RobotUpdate -> Bool)
-> (RobotUpdate -> RobotUpdate -> RobotUpdate)
-> (RobotUpdate -> RobotUpdate -> RobotUpdate)
-> Ord 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
$ccompare :: RobotUpdate -> RobotUpdate -> Ordering
compare :: RobotUpdate -> RobotUpdate -> Ordering
$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
>= :: RobotUpdate -> RobotUpdate -> Bool
$cmax :: RobotUpdate -> RobotUpdate -> RobotUpdate
max :: RobotUpdate -> RobotUpdate -> RobotUpdate
$cmin :: RobotUpdate -> RobotUpdate -> RobotUpdate
min :: RobotUpdate -> RobotUpdate -> RobotUpdate
Ord, Addr -> RobotUpdate -> ShowS
[RobotUpdate] -> ShowS
RobotUpdate -> String
(Addr -> RobotUpdate -> ShowS)
-> (RobotUpdate -> String)
-> ([RobotUpdate] -> ShowS)
-> Show RobotUpdate
forall a.
(Addr -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Addr -> RobotUpdate -> ShowS
showsPrec :: Addr -> RobotUpdate -> ShowS
$cshow :: RobotUpdate -> String
show :: RobotUpdate -> String
$cshowList :: [RobotUpdate] -> ShowS
showList :: [RobotUpdate] -> ShowS
Show, (forall x. RobotUpdate -> Rep RobotUpdate x)
-> (forall x. Rep RobotUpdate x -> RobotUpdate)
-> Generic RobotUpdate
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
$cfrom :: forall x. RobotUpdate -> Rep RobotUpdate x
from :: forall x. RobotUpdate -> Rep RobotUpdate x
$cto :: forall x. Rep RobotUpdate x -> RobotUpdate
to :: forall x. Rep RobotUpdate x -> RobotUpdate
Generic)

instance ToJSON RobotUpdate where
  toJSON :: RobotUpdate -> Value
toJSON = Options -> RobotUpdate -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
optionsMinimize

instance FromJSON RobotUpdate where
  parseJSON :: Value -> Parser RobotUpdate
parseJSON = Options -> Value -> Parser RobotUpdate
forall a.
(Generic a, GFromJSON Zero (Rep a)) =>
Options -> Value -> Parser a
genericParseJSON Options
optionsMinimize