Refactor CESK machine to track environments through new Suspended s…

…tate (#1928)

The big idea of this PR is to add a new type of CESK machine state, `Suspended`, which is a state the base robot automatically goes into after completing execution of a program entered at the REPL.  It is as if the base robot is still within the local context of any definitions etc. entered previously, just printed out an "intermediate result", and is now waiting to find out what the next term to be executed will be.  This allows us to treat `def` as syntax sugar for `let` and results in a much cleaner way to manage the context of definitions, which in turn allows us to remove a whole lot of special cases and fixes several annoying bugs.  See #1087 for more explanation and discussion.

Things that are **deleted** (!) by this PR:
- `TDef` (`def` is now just syntax sugar for `let`) (#997)
- `VResult` (we no longer need to return anything other than plain values)
- `FUnionEnv`, `FDiscardEnv`, `FLoadEnv` (we no longer need machinery to collect up definitions while evaluating terms)
- `ProcessedTerm` (just a plain `TSyntax` (i.e. `Syntax' Polytype`) is now enough)
- `Module` (it only existed to package up some contexts with typechecked terms, but we don't need them anymore)
- `RobotContext` and `topContext` (we don't need to store those things separately any more, they are just stored in the `CESK` machine where they belong)

Additions/changes:
- The `Requirement` module is split into `Requirements.Type` and `Requirements.Analysis` to avoid circular module imports
- New `Suspended` state for the CESK machine
- `def` and `tydef` are now allowed anywhere (even nested inside other definitions etc.) since `def x = y end; z` is just syntax sugar for `let x = y in z` (see #349)
- Code size decreased slightly for many programs using `def`, since `def` is now a synonym for `let`, and consecutive `def`s therefore do not require a `bind`.

Closes #1087.  Fixes #681 (hence also #736, #1796). Fixes #1032. Closes #1047. Closes #997. Fixes #1900. Fixes #1466. Fixes #1424.

See also #636.

src/swarm-doc/Swarm/Doc/Pedagogy.hs

@@ -54,7 +54,6 @@ import Swarm.Game.ScenarioInfo (
   scenarioPath,
  )
 import Swarm.Game.World.Load (loadWorlds)
-import Swarm.Language.Pipeline (ProcessedTerm, processedSyntax)
 import Swarm.Language.Syntax
 import Swarm.Language.Text.Markdown (docToText, findCode)
 import Swarm.Language.Types (Polytype)
@@ -128,13 +127,13 @@ isConsidered c = isUserFunc c && c `S.notMember` ignoredCommands
 -- the player did not write it explicitly in their code.
 --
 -- Also, the code from `run` is not parsed transitively yet.
-getCommands :: Maybe ProcessedTerm -> Map Const [SrcLoc]
+getCommands :: Maybe TSyntax -> Map Const [SrcLoc]
 getCommands Nothing = mempty
-getCommands (Just pt) =
+getCommands (Just tsyn) =
   M.fromListWith (<>) $ mapMaybe isCommand nodelist
  where
   nodelist :: [Syntax' Polytype]
-  nodelist = universe (pt ^. processedSyntax)
+  nodelist = universe tsyn
   isCommand (Syntax' sloc t _ _) = case t of
     TConst c -> guard (isConsidered c) >> Just (c, [sloc])
     _ -> Nothing

src/swarm-engine/Swarm/Game/CESK.hs

@@ -1,6 +1,5 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE PatternSynonyms #-}
 
 -- |
 -- SPDX-License-Identifier: BSD-3-Clause
@@ -71,16 +70,19 @@ module Swarm.Game.CESK (
 
   -- ** Construction
   initMachine,
-  initMachine',
+  continue,
   cancel,
   resetBlackholes,
+  prepareTerm,
 
   -- ** Extracting information
   finalValue,
+  suspendedEnv,
+  store,
+  cont,
 ) where
 
-import Control.Lens ((^.))
-import Control.Lens.Combinators (pattern Empty)
+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
@@ -92,9 +94,9 @@ import Swarm.Game.Ingredients (Count)
 import Swarm.Game.Tick
 import Swarm.Game.World (WorldUpdate (..))
 import Swarm.Language.Context
-import Swarm.Language.Module
-import Swarm.Language.Pipeline
+import Swarm.Language.Elaborate (insertSuspend)
 import Swarm.Language.Pretty
+import Swarm.Language.Requirements.Type (Requirements)
 import Swarm.Language.Syntax
 import Swarm.Language.Types
 import Swarm.Language.Value as V
@@ -126,38 +128,23 @@ data Frame
     -- 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
+  | -- | @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
-  | -- | 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 Contexts
-  | -- | 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
+    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.
@@ -176,6 +163,12 @@ data Frame
     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 (Eq, Show, Generic)
 
 instance ToJSON Frame where
@@ -285,6 +278,14 @@ data CESK
   | -- | 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 (Eq, Show, Generic)
 
 instance ToJSON CESK where
@@ -295,48 +296,107 @@ instance FromJSON CESK where
 
 -- | Is the CESK machine in a final (finished) state?  If so, extract
 --   the final value and store.
-finalValue :: CESK -> Maybe (Value, Store)
+finalValue :: CESK -> Maybe Value
 {-# INLINE finalValue #-}
-finalValue (Out v s []) = Just (v, s)
+finalValue (Out v _ []) = Just v
+finalValue (Suspended v _ _ []) = Just v
 finalValue _ = 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 t e s = initMachine' t e s []
-
--- | Like 'initMachine', but also take an explicit starting continuation.
-initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK
-initMachine' (ProcessedTerm (Module t' ctx tydefs) _ reqCtx) e s k =
-  case t' ^. sType of
-    -- If the starting term has a command type...
-    Forall _ (TyCmd _) ->
-      case (ctx, tydefs) of
-        -- ...but doesn't contain any definitions, just create a machine
-        -- that will evaluate it and then execute it.
-        (Empty, Empty) -> In t e s (FExec : k)
-        -- Or, if it does contain definitions, then load the resulting
-        -- context after executing it.
-        _ -> In t e s (FExec : FLoadEnv (Contexts ctx reqCtx tydefs) : k)
-    -- Otherwise, for a term with a non-command type, just
-    -- create a machine to evaluate it.
-    _ -> In t e s k
+-- | Extract the environment from a suspended CESK machine (/e.g./ to
+--   use for typechecking).
+suspendedEnv :: Traversal' CESK Env
+suspendedEnv = traversal go
  where
-  -- Erase all type and SrcLoc annotations from the term before
-  -- putting it in the machine state, since those are irrelevant at
-  -- runtime.
-  t = eraseS t'
+  go :: Applicative f => (Env -> f Env) -> CESK -> f CESK
+  go f (Suspended v e s k) = Suspended v <$> f e <*> pure s <*> pure k
+  go _ cesk = pure cesk
+
+-- | Lens focusing on the store of a CESK machine.
+store :: Lens' CESK Store
+store = lens get set
+ where
+  get = \case
+    In _ _ s _ -> s
+    Out _ s _ -> s
+    Up _ s _ -> s
+    Waiting _ c -> get c
+    Suspended _ _ s _ -> s
+  set cesk s = case cesk of
+    In t e _ k -> In t e s k
+    Out v _ k -> Out v s k
+    Up x _ k -> Up x s k
+    Waiting t c -> Waiting t (set c s)
+    Suspended v e _ k -> Suspended v e s k
+
+-- | Lens focusing on the continuation of a CESK machine.
+cont :: Lens' CESK Cont
+cont = lens get set
+ where
+  get = \case
+    In _ _ _ k -> k
+    Out _ _ k -> k
+    Up _ _ k -> k
+    Waiting _ c -> get c
+    Suspended _ _ _ k -> k
+  set cesk k = case cesk of
+    In t e s _ -> In t e s k
+    Out v s _ -> Out v s k
+    Up x s _ -> Up x s k
+    Waiting t c -> Waiting t (set c k)
+    Suspended v e s _ -> Suspended v e s 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 @return@.
+initMachine :: TSyntax -> CESK
+initMachine t = In (prepareTerm mempty t) mempty emptyStore [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 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 _ e s k -> In (insertSuspend $ prepareTerm e t) e s (FExec : FRestoreEnv e : 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 -> In (insertSuspend $ prepareTerm mempty t) mempty (cesk ^. store) (FExec : (cesk ^. cont))
+
+-- | Prepare a term for evaluation by a CESK machine in the given
+--   environment: erase all type annotations, and optionally wrap it
+--   in @return@ 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 e t = case whnfType (e ^. envTydefs) (ptBody (t ^. sType)) of
+  TyCmd _ -> t'
+  _ -> TApp (TConst Return) t'
+ where
+  t' = eraseS t
 
 -- | Cancel the currently running computation.
 cancel :: CESK -> CESK
-cancel cesk = Out VUnit s' []
+cancel cesk = Up Cancel s' (cesk ^. cont)
  where
-  s' = resetBlackholes $ getStore cesk
-  getStore (In _ _ s _) = s
-  getStore (Out _ s _) = s
-  getStore (Up _ s _) = s
-  getStore (Waiting _ c) = getStore c
+  s' = resetBlackholes $ cesk ^. store
 
 -- | Reset any 'Blackhole's in the 'Store'.  We need to use this any
 --   time a running computation is interrupted, either by an exception
@@ -352,10 +412,12 @@ resetBlackholes (Store n m) = Store n (IM.map resetBlackhole m)
 ------------------------------------------------------------
 
 instance PrettyPrec CESK where
-  prettyPrec _ (In c _ _ k) = prettyCont k (11, "▶" <> ppr c <> "◀")
-  prettyPrec _ (Out v _ k) = prettyCont k (11, "◀" <> ppr (valueToTerm v) <> "▶")
-  prettyPrec _ (Up e _ k) = prettyCont k (11, "!" <> (pretty (formatExn mempty e) <> "!"))
-  prettyPrec _ (Waiting t cesk) = "🕑" <> pretty t <> "(" <> ppr cesk <> ")"
+  prettyPrec _ = \case
+    In c _ _ k -> prettyCont k (11, "▶" <> ppr c <> "◀")
+    Out v _ k -> prettyCont k (11, "◀" <> ppr (valueToTerm v) <> "▶")
+    Up e _ k -> prettyCont k (11, "!" <> (pretty (formatExn mempty e) <> "!"))
+    Waiting t cesk -> "🕑" <> pretty t <> "(" <> ppr cesk <> ")"
+    Suspended v _ _ k -> prettyCont k (11, "◀" <> ppr (valueToTerm v) <> "...▶")
 
 -- | Take a continuation, and the pretty-printed expression which is
 --   the focus of the continuation (i.e. the expression whose value
@@ -383,15 +445,11 @@ prettyFrame f (p, inner) = case f of
   FFst v -> (11, "(" <> ppr (valueToTerm v) <> "," <+> inner <> ")")
   FArg t _ -> (10, pparens (p < 10) inner <+> prettyPrec 11 t)
   FApp v -> (10, prettyPrec 10 (valueToTerm v) <+> pparens (p < 11) inner)
-  FLet x t _ -> (11, hsep ["let", pretty x, "=", inner, "in", ppr t])
+  FLet x _ t _ -> (11, hsep ["let", pretty x, "=", inner, "in", ppr t])
   FTry v -> (10, "try" <+> pparens (p < 11) inner <+> prettyPrec 11 (valueToTerm v))
-  FUnionEnv _ -> prettyPrefix "∪·" (p, inner)
-  FLoadEnv {} -> prettyPrefix "L·" (p, inner)
-  FDef x -> (11, "def" <+> pretty x <+> "=" <+> inner <+> "end")
   FExec -> prettyPrefix "E·" (p, inner)
-  FBind Nothing t _ -> (0, pparens (p < 1) inner <+> ";" <+> ppr t)
-  FBind (Just x) t _ -> (0, hsep [pretty x, "<-", pparens (p < 1) inner, ";", ppr t])
-  FDiscardEnv -> prettyPrefix "D·" (p, inner)
+  FBind Nothing _ t _ -> (0, pparens (p < 1) inner <+> ";" <+> ppr t)
+  FBind (Just x) _ t _ -> (0, hsep [pretty x, "<-", pparens (p < 1) inner, ";", ppr t])
   FImmediate c _worldUpds _robotUpds -> prettyPrefix ("I[" <> ppr c <> "]·") (p, inner)
   FUpdate addr -> prettyPrefix ("S@" <> pretty addr) (p, inner)
   FFinishAtomic -> prettyPrefix "A·" (p, inner)
@@ -404,6 +462,8 @@ prettyFrame f (p, inner) = case f of
     pprEq (x, Nothing) = pretty x
     pprEq (x, Just t) = pretty x <+> "=" <+> ppr t
   FProj x -> (11, pparens (p < 11) inner <> "." <> pretty x)
+  FSuspend _ -> (10, "suspend" <+> pparens (p < 11) inner)
+  FRestoreEnv _ -> (10, "restore" <+> pparens (p < 11) inner)
 
 -- | Pretty-print a special "prefix application" frame, i.e. a frame
 --   formatted like @X· inner@.  Unlike typical applications, these

src/swarm-engine/Swarm/Game/Exception.hs

@@ -9,6 +9,7 @@ module Swarm.Game.Exception (
   Exn (..),
   IncapableFix (..),
   formatExn,
+  exnSeverity,
   IncapableFixWords (..),
 
   -- * Helper functions
@@ -28,9 +29,11 @@ import Swarm.Constant
 import Swarm.Game.Achievement.Definitions
 import Swarm.Game.Entity (EntityMap, devicesForCap, entityName)
 import Swarm.Language.Capability (Capability (CGod), capabilityName)
+import Swarm.Language.JSON ()
 import Swarm.Language.Pretty (prettyText)
-import Swarm.Language.Requirement (Requirements (..))
+import Swarm.Language.Requirements.Type (Requirements (..))
 import Swarm.Language.Syntax (Const, Term)
+import Swarm.Log (Severity (..))
 import Swarm.Util
 import Witch (from)
 
@@ -45,7 +48,7 @@ import Witch (from)
 -- >>> import Swarm.Language.Capability
 -- >>> import Swarm.Game.Entity
 -- >>> import Swarm.Game.Display
--- >>> import qualified Swarm.Language.Requirement as R
+-- >>> import qualified Swarm.Language.Requirements.Type as R
 
 -- ------------------------------------------------------------------
 
@@ -66,6 +69,11 @@ data Exn
     --   be caught by a @try@ block (but at least it will not crash
     --   the entire UI).
     Fatal Text
+  | -- | The user manually cancelled the computation (e.g. by hitting
+    --   Ctrl-C). This cannot be caught by a @try@ block, and results
+    --   in the CESK machine unwinding the stack all the way back to
+    --   the top level.
+    Cancel
   | -- | An infinite loop was detected via a blackhole.  This cannot
     --   be caught by a @try@ block.
     InfiniteLoop
@@ -93,11 +101,21 @@ formatExn em = \case
       , "Please report this as a bug at"
       , "<" <> swarmRepoUrl <> "issues/new>."
       ]
+  Cancel -> "Computation cancelled."
   InfiniteLoop -> "Infinite loop detected!"
   (CmdFailed c t _) -> T.concat [prettyText c, ": ", t]
   (User t) -> "Player exception: " <> t
   (Incapable f caps tm) -> formatIncapable em f caps tm
 
+exnSeverity :: Exn -> Severity
+exnSeverity = \case
+  Fatal {} -> Critical
+  Cancel {} -> Info
+  InfiniteLoop {} -> Error
+  Incapable {} -> Error
+  CmdFailed {} -> Error
+  User {} -> Error
+
 -- ------------------------------------------------------------------
 -- INCAPABLE HELPERS
 -- ------------------------------------------------------------------