From eb156a688fba5f60d7a8b55c2f4505fa022f6a17 Mon Sep 17 00:00:00 2001 From: Brent Yorgey Date: Wed, 19 Jun 2024 15:17:22 -0500 Subject: [PATCH] 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! :partying_face: 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 | 91 +++++++------------ src/swarm-engine/Swarm/Game/Step.hs | 49 +++++----- .../Swarm/Game/Step/Arithmetic.hs | 2 + src/swarm-engine/Swarm/Game/Step/Const.hs | 27 ------ src/swarm-lang/Swarm/Language/Elaborate.hs | 33 +------ src/swarm-lang/Swarm/Language/LSP/Hover.hs | 2 +- src/swarm-lang/Swarm/Language/LSP/VarUsage.hs | 2 +- src/swarm-lang/Swarm/Language/Parser/Term.hs | 10 +- src/swarm-lang/Swarm/Language/Pretty.hs | 4 +- .../Swarm/Language/Requirements/Analysis.hs | 2 +- src/swarm-lang/Swarm/Language/Syntax/AST.hs | 2 +- .../Swarm/Language/Syntax/Pattern.hs | 4 +- src/swarm-lang/Swarm/Language/Syntax/Util.hs | 2 +- src/swarm-lang/Swarm/Language/Typecheck.hs | 16 +--- src/swarm-lang/Swarm/Language/Value.hs | 37 ++++++-- test/unit/TestScoring.hs | 4 +- 16 files changed, 104 insertions(+), 183 deletions(-) diff --git a/src/swarm-engine/Swarm/Game/CESK.hs b/src/swarm-engine/Swarm/Game/CESK.hs index f8f80a920..750d07217 100644 --- a/src/swarm-engine/Swarm/Game/CESK.hs +++ b/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 - -- .) - -- - -- 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)) diff --git a/src/swarm-engine/Swarm/Game/Step.hs b/src/swarm-engine/Swarm/Game/Step.hs index 4713c8fc7..e633e901b 100644 --- a/src/swarm-engine/Swarm/Game/Step.hs +++ b/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 diff --git a/src/swarm-engine/Swarm/Game/Step/Arithmetic.hs b/src/swarm-engine/Swarm/Game/Step/Arithmetic.hs index 193a279d9..08ced6c3a 100644 --- a/src/swarm-engine/Swarm/Game/Step/Arithmetic.hs +++ b/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. diff --git a/src/swarm-engine/Swarm/Game/Step/Const.hs b/src/swarm-engine/Swarm/Game/Step/Const.hs index 8bdbd57bc..0c72c300d 100644 --- a/src/swarm-engine/Swarm/Game/Step/Const.hs +++ b/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. diff --git a/src/swarm-lang/Swarm/Language/Elaborate.hs b/src/swarm-lang/Swarm/Language/Elaborate.hs index 9bde0bf15..4b368798d 100644 --- a/src/swarm-lang/Swarm/Language/Elaborate.hs +++ b/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 diff --git a/src/swarm-lang/Swarm/Language/LSP/Hover.hs b/src/swarm-lang/Swarm/Language/LSP/Hover.hs index a2a5128d4..c1432b627 100644 --- a/src/swarm-lang/Swarm/Language/LSP/Hover.hs +++ b/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 diff --git a/src/swarm-lang/Swarm/Language/LSP/VarUsage.hs b/src/swarm-lang/Swarm/Language/LSP/VarUsage.hs index a94098e8d..5b2fdd3cc 100644 --- a/src/swarm-lang/Swarm/Language/LSP/VarUsage.hs +++ b/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 diff --git a/src/swarm-lang/Swarm/Language/Parser/Term.hs b/src/swarm-lang/Swarm/Language/Parser/Term.hs index 26f95a2f7..b1eb4a87c 100644 --- a/src/swarm-lang/Swarm/Language/Parser/Term.hs +++ b/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 diff --git a/src/swarm-lang/Swarm/Language/Pretty.hs b/src/swarm-lang/Swarm/Language/Pretty.hs index 7318cabdf..04cfa0cf1 100644 --- a/src/swarm-lang/Swarm/Language/Pretty.hs +++ b/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) $ diff --git a/src/swarm-lang/Swarm/Language/Requirements/Analysis.hs b/src/swarm-lang/Swarm/Language/Requirements/Analysis.hs index e0d62a730..89a03c455 100644 --- a/src/swarm-lang/Swarm/Language/Requirements/Analysis.hs +++ b/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 diff --git a/src/swarm-lang/Swarm/Language/Syntax/AST.hs b/src/swarm-lang/Swarm/Language/Syntax/AST.hs index e065f4b27..35508aaf7 100644 --- a/src/swarm-lang/Swarm/Language/Syntax/AST.hs +++ b/src/swarm-lang/Swarm/Language/Syntax/AST.hs @@ -125,7 +125,7 @@ data Term' ty -- Note that 'Force' is just a constant, whereas 'SDelay' has to -- be a special syntactic form so its argument can get special -- treatment during evaluation. - SDelay DelayType (Syntax' ty) + SDelay (Syntax' ty) | -- | Record literals @[x1 = e1, x2 = e2, x3, ...]@ Names @x@ -- without an accompanying definition are sugar for writing -- @x=x@. diff --git a/src/swarm-lang/Swarm/Language/Syntax/Pattern.hs b/src/swarm-lang/Swarm/Language/Syntax/Pattern.hs index 850130ef7..5f564d729 100644 --- a/src/swarm-lang/Swarm/Language/Syntax/Pattern.hs +++ b/src/swarm-lang/Swarm/Language/Syntax/Pattern.hs @@ -122,8 +122,8 @@ pattern TBind mv mty mreq t1 t2 <- SBind (fmap lvVar -> mv) _ mty mreq (STerm t1 TBind mv mty mreq t1 t2 = SBind (LV NoLoc <$> mv) Nothing mty mreq (STerm t1) (STerm t2) -- | Match a TDelay without annotations. -pattern TDelay :: DelayType -> Term -> Term -pattern TDelay m t = SDelay m (STerm t) +pattern TDelay :: Term -> Term +pattern TDelay t = SDelay (STerm t) -- | Match a TRcd without annotations. pattern TRcd :: Map Var (Maybe Term) -> Term diff --git a/src/swarm-lang/Swarm/Language/Syntax/Util.hs b/src/swarm-lang/Swarm/Language/Syntax/Util.hs index 16c303481..f3ed8d1a1 100644 --- a/src/swarm-lang/Swarm/Language/Syntax/Util.hs +++ b/src/swarm-lang/Swarm/Language/Syntax/Util.hs @@ -140,7 +140,7 @@ freeVarsS f = go S.empty STydef x xdef tdInfo t1 -> rewrap $ STydef x xdef tdInfo <$> go bound t1 SPair s1 s2 -> rewrap $ SPair <$> go bound s1 <*> go bound s2 SBind mx mty mpty mreq s1 s2 -> rewrap $ SBind mx mty mpty mreq <$> go bound s1 <*> go (maybe id (S.insert . lvVar) mx bound) s2 - SDelay m s1 -> rewrap $ SDelay m <$> go bound s1 + SDelay s1 -> rewrap $ SDelay <$> go bound s1 SRcd m -> rewrap $ SRcd <$> (traverse . traverse) (go bound) m SProj s1 x -> rewrap $ SProj <$> go bound s1 <*> pure x SAnnotate s1 pty -> rewrap $ SAnnotate <$> go bound s1 <*> pure pty diff --git a/src/swarm-lang/Swarm/Language/Typecheck.hs b/src/swarm-lang/Swarm/Language/Typecheck.hs index 6473d5474..260bccb58 100644 --- a/src/swarm-lang/Swarm/Language/Typecheck.hs +++ b/src/swarm-lang/Swarm/Language/Typecheck.hs @@ -886,19 +886,11 @@ check :: UType -> m (Syntax' UType) check s@(CSyntax l t cs) expected = addLocToTypeErr l $ case t of - -- if t : ty, then {t} : {ty}. - -- Note that in theory, if the @Maybe Var@ component of the @SDelay@ - -- is @Just@, we should typecheck the body under a context extended - -- with a type binding for the variable, and ensure that the type of - -- the variable is the same as the type inferred for the overall - -- @SDelay@. However, we rely on the invariant that such recursive - -- @SDelay@ nodes are never generated from the surface syntax, only - -- dynamically at runtime when evaluating recursive let or def expressions, - -- so we don't have to worry about typechecking them here. - SDelay d s1 -> do + -- If t : ty, then {t} : {ty}. + SDelay s1 -> do ty1 <- decomposeDelayTy s (Expected, expected) s1' <- check s1 ty1 - return $ Syntax' l (SDelay d s1') cs (UTyDelay ty1) + return $ Syntax' l (SDelay s1') cs (UTyDelay ty1) -- To check the type of a pair, make sure the expected type is a -- product type, and push the two types down into the left and right. @@ -1164,7 +1156,7 @@ analyzeAtomic locals (Syntax l t) = case t of -- Pairs, application, and delay are simple: just recurse and sum the results. SPair s1 s2 -> (+) <$> analyzeAtomic locals s1 <*> analyzeAtomic locals s2 SApp s1 s2 -> (+) <$> analyzeAtomic locals s1 <*> analyzeAtomic locals s2 - SDelay _ s1 -> analyzeAtomic locals s1 + SDelay s1 -> analyzeAtomic locals s1 -- Bind is similarly simple except that we have to keep track of a local variable -- bound in the RHS. SBind mx _ _ _ s1 s2 -> (+) <$> analyzeAtomic locals s1 <*> analyzeAtomic (maybe id (S.insert . lvVar) mx locals) s2 diff --git a/src/swarm-lang/Swarm/Language/Value.hs b/src/swarm-lang/Swarm/Language/Value.hs index b2cbd72d1..885673b6f 100644 --- a/src/swarm-lang/Swarm/Language/Value.hs +++ b/src/swarm-lang/Swarm/Language/Value.hs @@ -91,6 +91,13 @@ data Value where VDelay :: Term -> Env -> Value -- | A reference to a memory cell in the store. VRef :: Int -> Value + -- | An indirection to a value stored in a memory cell. The + -- difference between VRef and VIndir is that VRef is a "real" + -- value (of Ref type), whereas VIndir is just a placeholder. If + -- a VRef is encountered during evaluation, it is the final + -- result; if VIndir is encountered during evaluation, the value + -- it points to should be looked up. + VIndir :: Int -> Value -- | A record value. VRcd :: Map Var Value -> Value -- | A keyboard input. @@ -102,6 +109,15 @@ data Value where -- | A special value representing a program that terminated with -- an exception. VExc :: Value + -- | A special value used temporarily as the value for a variable + -- bound by a recursive let, while its definition is being + -- evaluated. If the variable is ever referenced again while its + -- value is still 'VBlackhole', that means it depends on itself in + -- a way that would trigger an infinite loop, and we can signal an + -- error. (Of course, we + -- .) + VBlackhole :: Value deriving (Eq, Show, Generic) -- | A value context is a mapping from variable names to their runtime @@ -113,17 +129,15 @@ type VCtx = Ctx Value -------------------------------------------------- -- | An environment is a record that stores relevant information for --- all the names currently in scope. +-- all the variables currently in scope. data Env = Env { _envTypes :: TCtx - -- ^ Map definition names to their types. + -- ^ Map variables to their types. , _envReqs :: ReqCtx - -- ^ Map definition names to the capabilities - -- required to evaluate/execute them. + -- ^ Map variables to the capabilities required to evaluate/execute + -- them. , _envVals :: VCtx - -- ^ Map definition names to their values. Note that since - -- definitions are delayed, the values will just consist of - -- 'VRef's pointing into the store. + -- ^ Map variables to their values. , _envTydefs :: TDCtx -- ^ Type synonym definitions. } @@ -209,15 +223,20 @@ valueToTerm = \case VPair v1 v2 -> TPair (valueToTerm v1) (valueToTerm v2) VClo x t e -> M.foldrWithKey - (\y v -> TLet LSLet False y Nothing Nothing (valueToTerm v)) + ( \y v -> case v of + VIndir {} -> id + _ -> TLet LSLet False y Nothing Nothing (valueToTerm v) + ) (TLam x Nothing t) (M.restrictKeys (Ctx.unCtx (e ^. envVals)) (S.delete x (setOf freeVarsV (Syntax' NoLoc t Empty ())))) VCApp c vs -> foldl' TApp (TConst c) (reverse (map valueToTerm vs)) VBind mx mty mreq c1 c2 _ -> TBind mx mty mreq c1 c2 - VDelay t _ -> TDelay SimpleDelay t + VDelay t _ -> TDelay t VRef n -> TRef n + VIndir n -> TRef n VRcd m -> TRcd (Just . valueToTerm <$> m) VKey kc -> TApp (TConst Key) (TText (prettyKeyCombo kc)) VRequirements x t _ -> TRequirements x t VSuspend t _ -> TSuspend t VExc -> TConst Undefined + VBlackhole -> TConst Undefined diff --git a/test/unit/TestScoring.hs b/test/unit/TestScoring.hs index 408c619bd..147abe6af 100644 --- a/test/unit/TestScoring.hs +++ b/test/unit/TestScoring.hs @@ -33,8 +33,8 @@ testHighScores = , compareAstSize 5 "double-move-let-with-invocation.sw" , compareAstSize 3 "single-move-def-with-invocation.sw" , compareAstSize 5 "double-move-def-with-invocation.sw" - , compareAstSize 27 "single-def-two-args-recursive.sw" - , compareAstSize 34 "single-def-two-args-recursive-with-invocation.sw" + , compareAstSize 25 "single-def-two-args-recursive.sw" + , compareAstSize 30 "single-def-two-args-recursive-with-invocation.sw" ] , testGroup "Precedence"