{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternSynonyms #-}

-- |
-- Module      :  Swarm.Game.CESK
-- Copyright   :  Brent Yorgey
-- Maintainer  :  byorgey@gmail.com
--
-- 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

  --    See 'FImmediate'.
  WorldUpdate (..),
  RobotUpdate (..),

  -- * Store
  Store,
  Loc,
  emptyStore,
  Cell (..),
  allocate,
  lookupCell,
  setCell,

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

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

  -- ** Extracting information
  finalValue,

  -- ** Pretty-printing
  prettyFrame,
  prettyCont,
  prettyCESK,
) where

import Control.Lens.Combinators (pattern Empty)
import Data.Aeson (FromJSON, ToJSON)
import Data.Aeson qualified
import Data.IntMap.Strict (IntMap)
import Data.IntMap.Strict qualified as IM
import Data.List (intercalate)
import GHC.Generics (Generic)
import Swarm.Game.Entity (Entity, Inventory)
import Swarm.Game.Exception
import Swarm.Game.Value as V
import Swarm.Game.World (World)
import Swarm.Language.Context
import Swarm.Language.Pipeline
import Swarm.Language.Pretty
import Swarm.Language.Requirement (ReqCtx)
import Swarm.Language.Syntax
import Swarm.Language.Types
import Witch (from)

------------------------------------------------------------
-- 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
  | -- | Apply specific updates to the world and current robot.
    FImmediate WorldUpdate RobotUpdate
  | -- | Update the memory cell at a certain location with the computed value.
    FUpdate Loc
  | -- | Signal that we are done with an atomic computation.
    FFinishAtomic
  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, Loc -> Frame -> ShowS
Cont -> ShowS
Frame -> [Char]
forall a.
(Loc -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: Cont -> ShowS
$cshowList :: Cont -> ShowS
show :: Frame -> [Char]
$cshow :: Frame -> [Char]
showsPrec :: Loc -> Frame -> ShowS
$cshowsPrec :: Loc -> 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 Loc = Int

-- | 'Store' represents a store, indexing integer locations to 'Cell's.
data Store = Store {Store -> Loc
next :: Loc, Store -> IntMap Cell
mu :: IntMap Cell} deriving (Loc -> Store -> ShowS
[Store] -> ShowS
Store -> [Char]
forall a.
(Loc -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Store] -> ShowS
$cshowList :: [Store] -> ShowS
show :: Store -> [Char]
$cshow :: Store -> [Char]
showsPrec :: Loc -> Store -> ShowS
$cshowsPrec :: Loc -> 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 Cell
  = -- | 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 'Cell', so that subsequent lookups can just use it
    --   without recomputing anything.
    V Value
  deriving (Loc -> Cell -> ShowS
[Cell] -> ShowS
Cell -> [Char]
forall a.
(Loc -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Cell] -> ShowS
$cshowList :: [Cell] -> ShowS
show :: Cell -> [Char]
$cshow :: Cell -> [Char]
showsPrec :: Loc -> Cell -> ShowS
$cshowsPrec :: Loc -> Cell -> ShowS
Show, Cell -> Cell -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Cell -> Cell -> Bool
$c/= :: Cell -> Cell -> Bool
== :: Cell -> Cell -> Bool
$c== :: Cell -> Cell -> Bool
Eq, forall x. Rep Cell x -> Cell
forall x. Cell -> Rep Cell x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Cell x -> Cell
$cfrom :: forall x. Cell -> Rep Cell x
Generic, Value -> Parser [Cell]
Value -> Parser Cell
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
parseJSONList :: Value -> Parser [Cell]
$cparseJSONList :: Value -> Parser [Cell]
parseJSON :: Value -> Parser Cell
$cparseJSON :: Value -> Parser Cell
FromJSON, [Cell] -> Encoding
[Cell] -> Value
Cell -> Encoding
Cell -> Value
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
toEncodingList :: [Cell] -> Encoding
$ctoEncodingList :: [Cell] -> Encoding
toJSONList :: [Cell] -> Value
$ctoJSONList :: [Cell] -> Value
toEncoding :: Cell -> Encoding
$ctoEncoding :: Cell -> Encoding
toJSON :: Cell -> Value
$ctoJSON :: Cell -> Value
ToJSON)

emptyStore :: Store
emptyStore :: Store
emptyStore = Loc -> IntMap Cell -> Store
Store Loc
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 -> (Loc, Store)
allocate :: Env -> Term -> Store -> (Loc, Store)
allocate Env
e Term
t (Store Loc
n IntMap Cell
m) = (Loc
n, Loc -> IntMap Cell -> Store
Store (Loc
n forall a. Num a => a -> a -> a
+ Loc
1) (forall a. Loc -> a -> IntMap a -> IntMap a
IM.insert Loc
n (Term -> Env -> Cell
E Term
t Env
e) IntMap Cell
m))

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

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

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

-- | The overall state of a CESK machine, which can actually be one of
--   three 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 Integer 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, Loc -> CESK -> ShowS
[CESK] -> ShowS
CESK -> [Char]
forall a.
(Loc -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [CESK] -> ShowS
$cshowList :: [CESK] -> ShowS
show :: CESK -> [Char]
$cshow :: CESK -> [Char]
showsPrec :: Loc -> CESK -> ShowS
$cshowsPrec :: Loc -> 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 Term
t (Module (Forall [Var]
_ (TyCmd Type
_)) TCtx
ctx) Requirements
_ ReqCtx
reqCtx) Env
e Store
s Cont
k =
  case TCtx
ctx of
    TCtx
Empty -> Term -> Env -> Store -> Cont -> CESK
In Term
t Env
e Store
s (Frame
FExec forall a. a -> [a] -> [a]
: Cont
k)
    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)
initMachine' (ProcessedTerm Term
t Module (Poly Type) (Poly Type)
_ Requirements
_ ReqCtx
_) Env
e Store
s Cont
k = Term -> Env -> Store -> Cont -> CESK
In Term
t Env
e Store
s Cont
k

-- | 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 Integer
_ 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 Loc
n IntMap Cell
m) = Loc -> IntMap Cell -> Store
Store Loc
n (forall a b. (a -> b) -> IntMap a -> IntMap b
IM.map Cell -> Cell
resetBlackhole IntMap Cell
m)
 where
  resetBlackhole :: Cell -> Cell
resetBlackhole (Blackhole Term
t Env
e) = Term -> Env -> Cell
E Term
t Env
e
  resetBlackhole Cell
c = Cell
c

------------------------------------------------------------
-- Very crude pretty-printing of CESK states.  Should really make a
-- nicer version of this code...
------------------------------------------------------------

-- | Very poor pretty-printing of CESK machine states, really just for
--   debugging. At some point we should make a nicer version.
prettyCESK :: CESK -> String
prettyCESK :: CESK -> [Char]
prettyCESK (In Term
c Env
_ Store
_ Cont
k) =
  [[Char]] -> [Char]
unlines
    [ [Char]
"▶ " forall a. [a] -> [a] -> [a]
++ forall a. PrettyPrec a => a -> [Char]
prettyString Term
c
    , [Char]
"  " forall a. [a] -> [a] -> [a]
++ Cont -> [Char]
prettyCont Cont
k
    ]
prettyCESK (Out Value
v Store
_ Cont
k) =
  [[Char]] -> [Char]
unlines
    [ [Char]
"◀ " forall a. [a] -> [a] -> [a]
++ forall source target. From source target => source -> target
from (Value -> Var
prettyValue Value
v)
    , [Char]
"  " forall a. [a] -> [a] -> [a]
++ Cont -> [Char]
prettyCont Cont
k
    ]
prettyCESK (Up Exn
e Store
_ Cont
k) =
  [[Char]] -> [Char]
unlines
    [ [Char]
"! " forall a. [a] -> [a] -> [a]
++ forall source target. From source target => source -> target
from (EntityMap -> Exn -> Var
formatExn forall a. Monoid a => a
mempty Exn
e)
    , [Char]
"  " forall a. [a] -> [a] -> [a]
++ Cont -> [Char]
prettyCont Cont
k
    ]
prettyCESK (Waiting Integer
t CESK
cek) =
  [Char]
"🕑" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show Integer
t forall a. Semigroup a => a -> a -> a
<> [Char]
" " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show CESK
cek

-- | Poor pretty-printing of continuations.
prettyCont :: Cont -> String
prettyCont :: Cont -> [Char]
prettyCont = ([Char]
"[" forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ [Char]
"]") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" | " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Frame -> [Char]
prettyFrame

-- | Poor pretty-printing of frames.
prettyFrame :: Frame -> String
prettyFrame :: Frame -> [Char]
prettyFrame (FSnd Term
t Env
_) = [Char]
"(_, " forall a. [a] -> [a] -> [a]
++ forall a. PrettyPrec a => a -> [Char]
prettyString Term
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
prettyFrame (FFst Value
v) = [Char]
"(" forall a. [a] -> [a] -> [a]
++ forall source target. From source target => source -> target
from (Value -> Var
prettyValue Value
v) forall a. [a] -> [a] -> [a]
++ [Char]
", _)"
prettyFrame (FArg Term
t Env
_) = [Char]
"_ " forall a. [a] -> [a] -> [a]
++ forall a. PrettyPrec a => a -> [Char]
prettyString Term
t
prettyFrame (FApp Value
v) = forall a. PrettyPrec a => a -> [Char]
prettyString (Value -> Term
valueToTerm Value
v) forall a. [a] -> [a] -> [a]
++ [Char]
" _"
prettyFrame (FLet Var
x Term
t Env
_) = [Char]
"let " forall a. [a] -> [a] -> [a]
++ forall source target. From source target => source -> target
from Var
x forall a. [a] -> [a] -> [a]
++ [Char]
" = _ in " forall a. [a] -> [a] -> [a]
++ forall a. PrettyPrec a => a -> [Char]
prettyString Term
t
prettyFrame (FTry Value
t) = [Char]
"try _ (" forall a. [a] -> [a] -> [a]
++ forall a. PrettyPrec a => a -> [Char]
prettyString (Value -> Term
valueToTerm Value
t) forall a. [a] -> [a] -> [a]
++ [Char]
")"
prettyFrame FUnionEnv {} = [Char]
"_ ∪ <Env>"
prettyFrame FLoadEnv {} = [Char]
"loadEnv"
prettyFrame (FDef Var
x) = [Char]
"def " forall a. [a] -> [a] -> [a]
++ forall source target. From source target => source -> target
from Var
x forall a. [a] -> [a] -> [a]
++ [Char]
" = _"
prettyFrame Frame
FExec = [Char]
"exec _"
prettyFrame (FBind Maybe Var
Nothing Term
t Env
_) = [Char]
"_ ; " forall a. [a] -> [a] -> [a]
++ forall a. PrettyPrec a => a -> [Char]
prettyString Term
t
prettyFrame (FBind (Just Var
x) Term
t Env
_) = forall source target. From source target => source -> target
from Var
x forall a. [a] -> [a] -> [a]
++ [Char]
" <- _ ; " forall a. [a] -> [a] -> [a]
++ forall a. PrettyPrec a => a -> [Char]
prettyString Term
t
prettyFrame FImmediate {} = [Char]
"(_ : cmd a)"
prettyFrame (FUpdate Loc
loc) = [Char]
"store@" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Loc
loc forall a. [a] -> [a] -> [a]
++ [Char]
"(_)"
prettyFrame Frame
FFinishAtomic = [Char]
"finishAtomic"

--------------------------------------------------------------
-- Wrappers for functions in FImmediate
--
-- NOTE: we can not use GameState and Robot directly, as it
-- would create a cyclic dependency. The alternative is
-- making CESK, Cont and Frame polymorphic which just muddies
-- the picture too much for one little game feature.
--
-- BEWARE: the types do not follow normal laws for Show and Eq
--------------------------------------------------------------

newtype WorldUpdate = WorldUpdate
  { WorldUpdate -> World Loc Entity -> Either Exn (World Loc Entity)
worldUpdate :: World Int Entity -> Either Exn (World Int Entity)
  }

newtype RobotUpdate = RobotUpdate
  { RobotUpdate -> Inventory -> Inventory
robotUpdateInventory :: Inventory -> Inventory
  }

instance Show WorldUpdate where show :: WorldUpdate -> [Char]
show WorldUpdate
_ = [Char]
"WorldUpdate {???}"

instance Show RobotUpdate where show :: RobotUpdate -> [Char]
show RobotUpdate
_ = [Char]
"RobotUpdate {???}"

instance Eq WorldUpdate where WorldUpdate
_ == :: WorldUpdate -> WorldUpdate -> Bool
== WorldUpdate
_ = Bool
True

instance Eq RobotUpdate where RobotUpdate
_ == :: RobotUpdate -> RobotUpdate -> Bool
== RobotUpdate
_ = Bool
True

-- TODO: remove these instances once Update fields are concret
instance FromJSON WorldUpdate where parseJSON :: Value -> Parser WorldUpdate
parseJSON Value
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (World Loc Entity -> Either Exn (World Loc Entity)) -> WorldUpdate
WorldUpdate forall a b. (a -> b) -> a -> b
$ \World Loc Entity
w -> forall a b. b -> Either a b
Right World Loc Entity
w
instance ToJSON WorldUpdate where toJSON :: WorldUpdate -> Value
toJSON WorldUpdate
_ = Value
Data.Aeson.Null
instance FromJSON RobotUpdate where parseJSON :: Value -> Parser RobotUpdate
parseJSON Value
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (Inventory -> Inventory) -> RobotUpdate
RobotUpdate forall a. a -> a
id
instance ToJSON RobotUpdate where toJSON :: RobotUpdate -> Value
toJSON RobotUpdate
_ = Value
Data.Aeson.Null