Get rid of memoizing delay + switch to a strict store

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