Get rid of memoizing delay + switch to a strict store (#1949)

Closes #1948; see that issue for a much more in-depth discussion.

Depends on merging #1928 first.

A lot of this PR consists in deleting code that is either (1) ugly or (2) overly clever! 🥳 

The short version is that the `Store` used to incorporate some laziness + memoization: when a cell was first allocated, it was an unevaluated thunk; it then got evaluated the first time it was referenced.  However, this wasn't really needed to handle recursive definitions (which is the only thing we were using it for).  Getting rid of it means we can get rid of a lot of weird ugly code needed to wrap free variables in extra calls to `force` and so on.

The new and improved `Store` just stores `Value`s, period.  A special `VBlackhole` value was added, to be used while evaluating a recursive `let`.

Note that `VRef` is no longer really used, but I left it there for use in implementing #1660 .  Once we have mutable references we can use them + delay/force to implement lazy cells.

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

@@ -60,8 +60,8 @@ module Swarm.Game.CESK (
   Store,
   Addr,
   emptyStore,
-  MemCell (..),
   allocate,
+  resolveValue,
   lookupStore,
   setStore,
 
@@ -72,7 +72,6 @@ module Swarm.Game.CESK (
   initMachine,
   continue,
   cancel,
-  resetBlackholes,
   prepareTerm,
 
   -- ** Extracting information
@@ -149,7 +148,7 @@ data Frame
     --
     -- The 'Const' is used to track the original command for error messages.
     FImmediate Const [WorldUpdate Entity] [RobotUpdate]
-  | -- | Update the memory cell at a certain location with the computed value.
+  | -- | 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
@@ -187,55 +186,38 @@ type Cont = [Frame]
 type Addr = Int
 
 -- | 'Store' represents a store, /i.e./ memory, indexing integer
---   locations to 'MemCell's.
-data Store = Store {next :: Addr, mu :: IntMap MemCell}
+--   locations to 'Value's.
+data Store = Store {next :: Addr, mu :: IntMap Value}
   deriving (Show, Eq, Generic, FromJSON, ToJSON)
 
--- | A memory cell can be in one of three states.
-data MemCell
-  = -- | A cell starts out life as an unevaluated term together with
-    --   its environment.
-    E Term Env
-  | -- | When the cell is 'Force'd, it is set to a 'Blackhole' while
-    --   being evaluated.  If it is ever referenced again while still
-    --   a 'Blackhole', that means it depends on itself in a way that
-    --   would trigger an infinite loop, and we can signal an error.
-    --   (Of course, we
-    --   <http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html cannot
-    --   detect /all/ infinite loops this way>.)
-    --
-    --   A 'Blackhole' saves the original 'Term' and 'Env' that are
-    --   being evaluated; if Ctrl-C is used to cancel a computation
-    --   while we are in the middle of evaluating a cell, the
-    --   'Blackhole' can be reset to 'E'.
-    Blackhole Term Env
-  | -- | Once evaluation is complete, we cache the final 'Value' in
-    --   the 'MemCell', so that subsequent lookups can just use it
-    --   without recomputing anything.
-    V Value
-  deriving (Show, Eq, Generic)
-
-instance ToJSON MemCell where
-  toJSON = genericToJSON optionsMinimize
-
-instance FromJSON MemCell where
-  parseJSON = genericParseJSON optionsMinimize
-
 emptyStore :: Store
 emptyStore = Store 0 IM.empty
 
--- | Allocate a new memory cell containing an unevaluated expression
---   with the current environment.  Return the index of the allocated
---   cell.
-allocate :: Env -> Term -> Store -> (Addr, Store)
-allocate e t (Store n m) = (n, Store (n + 1) (IM.insert n (E t e) m))
-
--- | Look up the cell at a given index.
-lookupStore :: Addr -> Store -> Maybe MemCell
-lookupStore n = IM.lookup n . mu
-
--- | Set the cell at a given index.
-setStore :: Addr -> MemCell -> Store -> Store
+-- | Allocate a new memory cell containing a given value.  Return the
+--   index of the allocated cell.
+allocate :: Value -> Store -> (Addr, Store)
+allocate v (Store n m) = (n, Store (n + 1) (IM.insert n v m))
+
+-- | Resolve a value, recursively looking up any indirections in the
+--   store.
+resolveValue :: Store -> Value -> Either Addr Value
+resolveValue s = \case
+  VIndir loc -> lookupStore s loc
+  v -> Right 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 s = go
+ where
+  go loc = case IM.lookup loc (mu s) of
+    Nothing -> Left loc
+    Just v -> case v of
+      VIndir loc' -> go loc'
+      _ -> Right v
+
+-- | Set the value at a given index.
+setStore :: Addr -> Value -> Store -> Store
 setStore n c (Store nxt m) = Store nxt (IM.insert n c m)
 
 ------------------------------------------------------------
@@ -394,18 +376,7 @@ prepareTerm e t = case whnfType (e ^. envTydefs) (ptBody (t ^. sType)) of
 
 -- | Cancel the currently running computation.
 cancel :: CESK -> CESK
-cancel cesk = Up Cancel s' (cesk ^. cont)
- where
-  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
---   or by a Ctrl+C.
-resetBlackholes :: Store -> Store
-resetBlackholes (Store n m) = Store n (IM.map resetBlackhole m)
- where
-  resetBlackhole (Blackhole t e) = E t e
-  resetBlackhole c = c
+cancel cesk = Up Cancel (cesk ^. store) (cesk ^. cont)
 
 ------------------------------------------------------------
 -- Pretty printing CESK machine states
@@ -451,7 +422,7 @@ prettyFrame f (p, inner) = case f of
   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)
+  FUpdate {} -> (p, inner)
   FFinishAtomic -> prettyPrefix "A·" (p, inner)
   FMeetAll _ _ -> prettyPrefix "M·" (p, inner)
   FRcd _ done foc rest -> (11, encloseSep "[" "]" ", " (pDone ++ [pFoc] ++ pRest))

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

@@ -580,7 +580,12 @@ stepCESK cesk = case cesk of
     v <-
       lookupValue x e
         `isJustOr` Fatal (T.unwords ["Undefined variable", x, "encountered while running the interpreter."])
-    return $ Out v s k
+
+    -- Now look up any indirections and make sure it's not a blackhole.
+    case resolveValue s v of
+      Left loc -> throwError $ Fatal $ T.append "Reference to unknown memory cell " (from (show loc))
+      Right VBlackhole -> throwError InfiniteLoop
+      Right v' -> return $ Out v' s k
 
   -- To evaluate a pair, start evaluating the first component.
   In (TPair t1 t2) e s k -> return $ In t1 e s (FSnd t2 e : k)
@@ -630,12 +635,16 @@ stepCESK cesk = case cesk of
   -- let-bound expression.
   In (TLet _ False x mty mreq t1 t2) e s k ->
     return $ In t1 e s (FLet x ((,) <$> mty <*> mreq) t2 e : k)
-  -- To evaluate recursive let expressions, we evaluate the memoized
-  -- delay of the let-bound expression.  Every free occurrence of x
-  -- in the let-bound expression and the body has already been
-  -- rewritten by elaboration to 'force x'.
-  In (TLet _ True x mty mreq t1 t2) e s k ->
-    return $ In (TDelay (MemoizedDelay $ Just x) t1) e s (FLet x ((,) <$> mty <*> mreq) t2 e : k)
+  -- To evaluate a recursive let binding:
+  In (TLet _ True x mty mreq t1 t2) e s k -> do
+    -- First, allocate a cell for it in the store with the initial
+    -- value of Blackhole.
+    let (loc, s') = allocate VBlackhole s
+    -- Now evaluate the definition with the variable bound to an
+    -- indirection to the new cell, and push an FUpdate stack frame to
+    -- update the cell with the value once we're done evaluating it,
+    -- followed by an FLet frame to evaluate the body of the let.
+    return $ In t1 (addValueBinding x (VIndir loc) e) s' (FUpdate loc : FLet x ((,) <$> mty <*> mreq) t2 e : k)
   -- Once we've finished with the let-binding, we switch to evaluating
   -- the body in a suitably extended environment.
   Out v1 s (FLet x mtr t2 e : k) -> do
@@ -651,22 +660,10 @@ stepCESK cesk = case cesk of
   In (TBind mx mty mreq t1 t2) e s k -> return $ Out (VBind mx mty mreq t1 t2 e) s k
   -- Simple (non-memoized) delay expressions immediately turn into
   -- VDelay values, awaiting application of 'Force'.
-  In (TDelay SimpleDelay t) e s k -> return $ Out (VDelay t e) s k
-  -- For memoized delay expressions, we allocate a new cell in the store and
-  -- return a reference to it.
-  In (TDelay (MemoizedDelay x) t) e s k -> do
-    -- Note that if the delay expression is recursive, we add a
-    -- binding to the environment that wil be used to evaluate the
-    -- body, binding the variable to a reference to the memory cell we
-    -- just allocated for the body expression itself.  As a fun aside,
-    -- notice how Haskell's recursion and laziness play a starring
-    -- role: @loc@ is both an output from @allocate@ and used as part
-    -- of an input! =D
-    let (loc, s') = allocate (maybe id (`addValueBinding` VRef loc) x e) t s
-    return $ Out (VRef loc) s' k
+  In (TDelay t) e s k -> return $ Out (VDelay t e) s k
   -- If we see an update frame, it means we're supposed to set the value
   -- of a particular cell to the value we just finished computing.
-  Out v s (FUpdate loc : k) -> return $ Out v (setStore loc (V v) s) k
+  Out v s (FUpdate loc : k) -> return $ Out v (setStore loc v s) k
   -- If we see a primitive application of suspend, package it up as
   -- a value until it's time to execute.
   In (TSuspend t) e s k -> return $ Out (VSuspend t e) s k
@@ -839,19 +836,15 @@ stepCESK cesk = case cesk of
 
     -- If an exception rises all the way to the top level without being
     -- handled, turn it into an error message.
-
+    --
     -- HOWEVER, we have to make sure to check that the robot has the
     -- 'log' capability which is required to collect and view logs.
-    --
-    -- Notice how we call resetBlackholes on the store, so that any
-    -- cells which were in the middle of being evaluated will be reset.
-    let s' = resetBlackholes s
     h <- hasCapability CLog
     em <- use $ landscape . terrainAndEntities . entityMap
     when h $ void $ traceLog RobotError (exnSeverity exn) (formatExn em exn)
     return $ case menv of
-      Nothing -> Out VExc s' []
-      Just env -> Suspended VExc env s' []
+      Nothing -> Out VExc s []
+      Just env -> Suspended VExc env s []
 
 -- | Execute the given program *hypothetically*: i.e. in a fresh
 -- CESK machine, using *copies* of the current store, robot

src/swarm-engine/Swarm/Game/Step/Arithmetic.hs

@@ -72,9 +72,11 @@ compareValues v1 = case v1 of
   VBind {} -> incomparable v1
   VDelay {} -> incomparable v1
   VRef {} -> incomparable v1
+  VIndir {} -> incomparable v1
   VRequirements {} -> incomparable v1
   VSuspend {} -> incomparable v1
   VExc {} -> incomparable v1
+  VBlackhole {} -> incomparable v1
 
 -- | Values with different types were compared; this should not be
 --   possible since the type system should catch it.

src/swarm-engine/Swarm/Game/Step/Const.hs

@@ -966,33 +966,6 @@ execConst runChildProg c vs s k = do
       _ -> badConst
     Force -> case vs of
       [VDelay t e] -> return $ In t e s k
-      [VRef loc] ->
-        -- To force a VRef, we look up the location in the store.
-        case lookupStore loc s of
-          -- If there's no cell at that location, it's a bug!  It
-          -- shouldn't be possible to get a VRef to a non-existent
-          -- location, since the only way VRefs get created is at the
-          -- time we allocate a new cell.
-          Nothing ->
-            return $
-              Up (Fatal $ T.append "Reference to unknown memory cell " (from (show loc))) s k
-          -- If the location contains an unevaluated expression, it's
-          -- time to evaluate it.  Set the cell to a 'Blackhole', push
-          -- an 'FUpdate' frame so we remember to update the location
-          -- to its value once we finish evaluating it, and focus on
-          -- the expression.
-          Just (E t e') -> return $ In t e' (setStore loc (Blackhole t e') s) (FUpdate loc : k)
-          -- If the location contains a Blackhole, that means we are
-          -- already currently in the middle of evaluating it, i.e. it
-          -- depends on itself, so throw an 'InfiniteLoop' error.
-          Just Blackhole {} -> return $ Up InfiniteLoop s k
-          -- If the location already contains a value, just return it.
-          Just (V v) -> return $ Out v s k
-      -- If a force is applied to any other kind of value, just ignore it.
-      -- This is needed because of the way we wrap all free variables in @force@
-      -- in case they come from a @def@ which are always wrapped in @delay@.
-      -- But binders (i.e. @x <- ...@) are also exported to the global context.
-      [v] -> return $ Out v s k
       _ -> badConst
     If -> case vs of
       -- Use the boolean to pick the correct branch, and apply @force@ to it.

src/swarm-lang/Swarm/Language/Elaborate.hs

@@ -1,5 +1,4 @@
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE PatternSynonyms #-}
 
 -- |
 -- SPDX-License-Identifier: BSD-3-Clause
@@ -8,9 +7,8 @@
 module Swarm.Language.Elaborate where
 
 import Control.Applicative ((<|>))
-import Control.Lens (transform, (%~), (^.), pattern Empty)
+import Control.Lens (transform, (^.))
 import Swarm.Language.Syntax
-import Swarm.Language.Types
 
 -- | Perform some elaboration / rewriting on a fully type-annotated
 --   term.  This currently performs such operations as rewriting @if@
@@ -23,24 +21,14 @@ import Swarm.Language.Types
 --   currently that sort of thing tends to make type inference fall
 --   over.
 elaborate :: TSyntax -> TSyntax
-elaborate =
-  -- Wrap all *free* variables in 'Force'.  Free variables must be
-  -- referring to a previous definition, which are all wrapped in
-  -- 'TDelay'.
-  (freeVarsS %~ \s -> Syntax' (s ^. sLoc) (SApp sForce s) (s ^. sComments) (s ^. sType))
-    -- Now do additional rewriting on all subterms.
-    . transform rewrite
+elaborate = transform rewrite
  where
   rewrite :: TSyntax -> TSyntax
   rewrite (Syntax' l t cs ty) = Syntax' l (rewriteTerm t) cs ty
 
   rewriteTerm :: TTerm -> TTerm
   rewriteTerm = \case
-    -- For recursive let bindings, rewrite any occurrences of x to
-    -- (force x).  When interpreting t1, we will put a binding (x |->
-    -- delay t1) in the context.
-    --
-    -- Here we also take inferred types for variables bound by def or
+    -- Here we take inferred types for variables bound by def or
     -- bind (but NOT let) and stuff them into the term itself, so that
     -- we will still have access to them at runtime, after type
     -- annotations on the AST are erased.  We need them at runtime so
@@ -59,27 +47,16 @@ elaborate =
     -- we'll infer them both at typechecking time then fill them in
     -- during elaboration here.
     SLet ls r x mty mreq t1 t2 ->
-      let wrap
-            | r = wrapForce (lvVar x) -- wrap in 'force' if recursive
-            | otherwise = id
-          mty' = case ls of
+      let mty' = case ls of
             LSDef -> mty <|> Just (t1 ^. sType)
             LSLet -> Nothing
-       in SLet ls r x mty' mreq (wrap t1) (wrap t2)
+       in SLet ls r x mty' mreq t1 t2
     SBind x (Just ty) _ mreq c1 c2 -> SBind x Nothing (Just ty) mreq c1 c2
     -- Rewrite @f $ x@ to @f x@.
     SApp (Syntax' _ (SApp (Syntax' _ (TConst AppF) _ _) l) _ _) r -> SApp l r
     -- Leave any other subterms alone.
     t -> t
 
-wrapForce :: Var -> TSyntax -> TSyntax
-wrapForce x = mapFreeS x (\s@(Syntax' l _ ty cs) -> Syntax' l (SApp sForce s) ty cs)
-
--- Note, TyUnit is not the right type, but I don't want to bother
-
-sForce :: TSyntax
-sForce = Syntax' NoLoc (TConst Force) Empty (Forall ["a"] (TyDelay (TyVar "a") :->: TyVar "a"))
-
 -- | Insert a special 'suspend' primitive at the very end of an erased
 --   term which must have a command type.
 insertSuspend :: Term -> Term

src/swarm-lang/Swarm/Language/LSP/Hover.hs

@@ -114,7 +114,7 @@ narrowToPosition s0@(Syntax' _ t _ ty) pos = fromMaybe s0 $ case t of
   SLet _ _ lv _ _ s1@(Syntax' _ _ _ lty) s2 -> d (locVarToSyntax' lv lty) <|> d s1 <|> d s2
   SBind mlv _ _ _ s1@(Syntax' _ _ _ lty) s2 -> (mlv >>= d . flip locVarToSyntax' (getInnerType lty)) <|> d s1 <|> d s2
   SPair s1 s2 -> d s1 <|> d s2
-  SDelay _ s -> d s
+  SDelay s -> d s
   SRcd m -> asum . map d . catMaybes . M.elems $ m
   SProj s1 _ -> d s1
   SAnnotate s _ -> d s

src/swarm-lang/Swarm/Language/LSP/VarUsage.hs

@@ -109,5 +109,5 @@ getUsage bindings (CSyntax _pos t _comments) = case t of
   SBind maybeVar _ _ _ s1 s2 -> case maybeVar of
     Just v -> checkOccurrences bindings v Bind [s1, s2]
     Nothing -> getUsage bindings s1 <> getUsage bindings s2
-  SDelay _ s -> getUsage bindings s
+  SDelay s -> getUsage bindings s
   _ -> mempty

src/swarm-lang/Swarm/Language/Parser/Term.hs

@@ -98,14 +98,8 @@ parseTermAtom2 =
         <|> SRcd <$> brackets (parseRecord (optional (symbol "=" *> parseTerm)))
         <|> parens (view sTerm . mkTuple <$> (parseTerm `sepBy` symbol ","))
     )
-    -- Potential syntax for explicitly requesting memoized delay.
-    -- Perhaps we will not need this in the end; see the discussion at
-    -- https://github.com/swarm-game/swarm/issues/150 .
-    -- <|> parseLoc (TDelay SimpleDelay (TConst Noop) <$ try (symbol "{{" *> symbol "}}"))
-    -- <|> parseLoc (SDelay MemoizedDelay <$> dbraces parseTerm)
-
-    <|> parseLoc (TDelay SimpleDelay (TConst Noop) <$ try (symbol "{" *> symbol "}"))
-    <|> parseLoc (SDelay SimpleDelay <$> braces parseTerm)
+    <|> parseLoc (TDelay (TConst Noop) <$ try (symbol "{" *> symbol "}"))
+    <|> parseLoc (SDelay <$> braces parseTerm)
     <|> parseLoc (view antiquoting >>= (guard . (== AllowAntiquoting)) >> parseAntiquotation)
 
 -- | Construct an 'SLet', automatically filling in the Boolean field

src/swarm-lang/Swarm/Language/Pretty.hs

@@ -280,8 +280,8 @@ instance PrettyPrec (Term' ty) where
     TRequire n e -> pparens (p > 10) $ "require" <+> pretty n <+> ppr @Term (TText e)
     SRequirements _ e -> pparens (p > 10) $ "requirements" <+> ppr e
     TVar s -> pretty s
-    SDelay _ (Syntax' _ (TConst Noop) _ _) -> "{}"
-    SDelay _ t -> group . encloseWithIndent 2 lbrace rbrace $ ppr t
+    SDelay (Syntax' _ (TConst Noop) _ _) -> "{}"
+    SDelay t -> group . encloseWithIndent 2 lbrace rbrace $ ppr t
     t@SPair {} -> prettyTuple t
     t@SLam {} ->
       pparens (p > 9) $

src/swarm-lang/Swarm/Language/Requirements/Analysis.hs

@@ -148,7 +148,7 @@ requirements tdCtx ctx =
       local @ReqCtx (maybe id Ctx.delete mx) $ go t2
     -- Everything else is straightforward.
     TPair t1 t2 -> add (singletonCap CProd) *> go t1 *> go t2
-    TDelay _ t -> go t
+    TDelay t -> go t
     TRcd m -> add (singletonCap CRecord) *> forM_ (M.assocs m) (go . expandEq)
      where
       expandEq (x, Nothing) = TVar x