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"