{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternSynonyms #-}
module Swarm.Game.CESK (
Frame (..),
Cont,
WorldUpdate (..),
RobotUpdate (..),
Store,
Loc,
emptyStore,
Cell (..),
allocate,
lookupCell,
setCell,
CESK (..),
initMachine,
initMachine',
cancel,
resetBlackholes,
finalValue,
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)
data Frame
=
FSnd Term Env
|
FFst Value
|
FArg Term Env
|
FApp Value
|
FLet Var Term Env
|
FTry Value
|
FUnionEnv Env
|
FLoadEnv TCtx ReqCtx
|
FDef Var
|
FExec
|
FBind (Maybe Var) Term Env
|
FImmediate WorldUpdate RobotUpdate
|
FUpdate Loc
|
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)
type Cont = [Frame]
type Loc = Int
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)
data Cell
=
E Term Env
|
Blackhole Term Env
|
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 :: 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))
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
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)
data CESK
=
In Term Env Store Cont
|
Out Value Store Cont
|
Up Exn Store Cont
|
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)
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
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 []
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 :: 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
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
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
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
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"
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
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