add TTydef syntax node and related infrastructure

feedback.yaml

@@ -1,3 +1,4 @@
 loops:
+  build: cabal build -j -O0 all
   test: cabal test -j -O0 --test-show-details=direct swarm:swarm-integration swarm:swarm-unit
   unit: cabal test -j -O0 --test-show-details=direct swarm:swarm-unit

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

@@ -290,14 +290,15 @@ initMachine t e s = initMachine' t e s []
 
 -- | Like 'initMachine', but also take an explicit starting continuation.
 initMachine' :: ProcessedTerm -> Env -> Store -> Cont -> CESK
-initMachine' (ProcessedTerm (Module t' ctx) _ reqCtx) e s k =
+initMachine' (ProcessedTerm (Module t' ctx _tydefs) _ reqCtx) e s k =
   case t' ^. sType of
     -- If the starting term has a command type...
     Forall _ (TyCmd _) ->
       case ctx of
         -- ...but doesn't contain any definitions, just create a machine
         -- that will evaluate it and then execute it.
         Empty -> In t e s (FExec : k)
+        -- XXX do we also need to load tydefs?
         -- Or, if it does contain definitions, then load the resulting
         -- context after executing it.
         _ -> In t e s (FExec : FLoadEnv ctx reqCtx : k)

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

@@ -133,9 +133,8 @@ import Swarm.Game.World qualified as W
 import Swarm.Game.World.Gen (Seed)
 import Swarm.Language.Capability (constCaps)
 import Swarm.Language.Context qualified as Ctx
-import Swarm.Language.Module (Module (Module))
-import Swarm.Language.Pipeline (ProcessedTerm (ProcessedTerm), processTermEither)
-import Swarm.Language.Syntax (SrcLoc (..), Syntax' (..), allConst)
+import Swarm.Language.Pipeline (ProcessedTerm, processTermEither, processedSyntax)
+import Swarm.Language.Syntax (SrcLoc (..), allConst, sLoc)
 import Swarm.Language.Typed (Typed (Typed))
 import Swarm.Language.Types
 import Swarm.Log
@@ -167,9 +166,10 @@ parseCodeFile ::
   m CodeToRun
 parseCodeFile filepath = do
   contents <- sendIO $ TIO.readFile filepath
-  pt@(ProcessedTerm (Module (Syntax' srcLoc _ _ _) _) _ _) <-
-    either (throwError . CustomFailure) return (processTermEither contents)
-  let strippedText = stripSrc srcLoc contents
+  pt <- either (throwError . CustomFailure) return (processTermEither contents)
+
+  let srcLoc = pt ^. processedSyntax . sLoc
+      strippedText = stripSrc srcLoc contents
       programBytestring = TL.encodeUtf8 $ TL.fromStrict strippedText
       sha1Hash = showDigest $ sha1 programBytestring
   return $ CodeToRun (PlayerAuthored filepath $ Sha1 sha1Hash) pt

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

@@ -650,7 +650,8 @@ stepCESK cesk = case cesk of
   In tm@(TDef r x _ t) e s k -> withExceptions s k $ do
     hasCapabilityFor CEnv tm
     return $ Out (VDef r x t e) s k
-
+  -- Type definitions just turn into a no-op.
+  In (TTydef {}) e s k -> return $ In (TConst Noop) e s k
   -- Bind expressions don't evaluate: just package it up as a value
   -- until such time as it is to be executed.
   In (TBind mx t1 t2) e s k -> return $ Out (VBind mx t1 t2 e) s k

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

@@ -130,6 +130,7 @@ narrowToPosition s0@(Syntax' _ t _ ty) pos = fromMaybe s0 $ case t of
   TVar {} -> Nothing
   TRequire {} -> Nothing
   TRequireDevice {} -> Nothing
+  TTydef {} -> Nothing
   -- these should not show up in surface language
   TRef {} -> Nothing
   TRobot {} -> Nothing
@@ -188,6 +189,7 @@ explain trm = case trm ^. sTerm of
   TVar v -> pure $ typeSignature v ty ""
   SRcd {} -> literal "A record literal."
   SProj {} -> literal "A record projection."
+  TTydef {} -> literal "A type synonym definition."
   -- type ascription
   SAnnotate lhs typeAnn ->
     Node

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

@@ -10,6 +10,7 @@ module Swarm.Language.Module (
   Module (..),
   moduleSyntax,
   moduleCtx,
+  moduleTydefs,
   TModule,
   UModule,
   trivMod,
@@ -31,8 +32,13 @@ import Swarm.Language.Types (Polytype, UPolytype, UType)
 --   inference on a top-level expression, which in particular can
 --   contain definitions ('Swarm.Language.Syntax.TDef').  A module
 --   contains the type-annotated AST of the expression itself, as well
---   as the context giving the types of any defined variables.
-data Module s t = Module {_moduleSyntax :: Syntax' s, _moduleCtx :: Ctx t}
+--   as a context which maps term variable names to their types, and
+--   another context which maps type synonym names to their definitions.
+data Module s t = Module
+  { _moduleSyntax :: Syntax' s
+  , _moduleCtx :: Ctx t
+  , _moduleTydefs :: Ctx Polytype
+  }
   deriving (Show, Eq, Functor, Data, Generic, FromJSON, ToJSON)
 
 makeLenses ''Module
@@ -51,4 +57,4 @@ type UModule = Module UType UPolytype
 
 -- | The trivial module for a given AST, with the empty context.
 trivMod :: Syntax' s -> Module s t
-trivMod t = Module t empty
+trivMod t = Module t empty empty

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

@@ -110,4 +110,4 @@ processParsedTerm' ctx capCtx t = do
   return $ ProcessedTerm (elaborateModule m) caps capCtx'
 
 elaborateModule :: TModule -> TModule
-elaborateModule (Module ast ctx) = Module (elaborate ast) ctx
+elaborateModule (Module ast ctx tydefs) = Module (elaborate ast) ctx tydefs

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

@@ -267,6 +267,7 @@ instance PrettyPrec (Term' ty) where
       [ prettyDefinition "def" x mty t1
       , "end"
       ]
+  prettyPrec _ (TTydef (LV _ x) pty) = prettyTydef x pty
   -- Special case for printing consecutive defs: don't worry about
   -- precedence, and print a blank line with no semicolon
   prettyPrec _ (SBind Nothing t1@(Syntax' _ (SDef {}) _ _) t2) =
@@ -304,6 +305,9 @@ prettyDefinition defName x mty t1 =
   defEqLambdas = hsep ("=" : map prettyLambda defLambdaList)
   eqAndLambdaLine = if null defLambdaList then "=" else line <> defEqLambdas
 
+prettyTydef :: Var -> Polytype -> Doc ann
+prettyTydef _x _pty = "tydef" -- XXX to do
+
 prettyPrecApp :: Int -> Syntax' ty -> Syntax' ty -> Doc a
 prettyPrecApp p t1 t2 =
   pparens (p > 10) $

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

@@ -144,6 +144,8 @@ requirements ctx tm = first (insert (ReqCap CPower)) $ case tm of
   TDef r x _ t ->
     let bodyReqs = (if r then insert (ReqCap CRecursion) else id) (requirements' ctx t)
      in (singletonCap CEnv, Ctx.singleton x bodyReqs)
+  -- Making a type synonym also requires CEnv.
+  TTydef {} -> (singletonCap CEnv, Ctx.empty)
   TBind _ t1 t2 ->
     -- First, see what the requirements are to execute the
     -- first command.  It may also define some names, so we get a
@@ -237,14 +239,15 @@ requirements' = go
     -- Everything else is straightforward.
     TPair t1 t2 -> insert (ReqCap CProd) $ go ctx t1 <> go ctx t2
     TDelay _ t -> go ctx t
-    -- This case should never happen if the term has been
-    -- typechecked; Def commands are only allowed at the top level,
-    -- so simply returning mempty is safe.
-    TDef {} -> mempty
     TRcd m -> insert (ReqCap CRecord) $ foldMap (go ctx . expandEq) (M.assocs m)
      where
       expandEq (x, Nothing) = TVar x
       expandEq (_, Just t) = t
     TProj t _ -> insert (ReqCap CRecord) $ go ctx t
     -- A type ascription doesn't change requirements
     TAnnotate t _ -> go ctx t
+    -- These cases should never happen if the term has been
+    -- typechecked; Def commands are only allowed at the top level,
+    -- so simply returning mempty is safe.
+    TDef {} -> mempty
+    TTydef {} -> mempty

src/swarm-lang/Swarm/Language/Syntax/AST.hs

@@ -93,6 +93,8 @@ data Term' ty
     --   value in subsequent commands. The @Bool@ indicates whether the
     --   definition is known to be recursive.
     SDef Bool LocVar (Maybe Polytype) (Syntax' ty)
+  | -- | A type synonym definition.
+    TTydef LocVar Polytype
   | -- | A monadic bind for commands, of the form @c1 ; c2@ or @x <- c1; c2@.
     SBind (Maybe LocVar) (Syntax' ty) (Syntax' ty)
   | -- | Delay evaluation of a term, written @{...}@.  Swarm is an

src/swarm-lang/Swarm/Language/Syntax/Pattern.hs

@@ -128,4 +128,4 @@ pattern TAnnotate t pt = SAnnotate (STerm t) pt
 
 -- COMPLETE pragma tells GHC using this set of patterns is complete for Term
 
-{-# COMPLETE TUnit, TConst, TDir, TInt, TAntiInt, TText, TAntiText, TBool, TRequireDevice, TRequire, TRequirements, TVar, TPair, TLam, TApp, TLet, TDef, TBind, TDelay, TRcd, TProj, TAnnotate #-}
+{-# COMPLETE TUnit, TConst, TDir, TInt, TAntiInt, TText, TAntiText, TBool, TRequireDevice, TRequire, TRequirements, TVar, TPair, TLam, TApp, TLet, TDef, TTydef, TBind, TDelay, TRcd, TProj, TAnnotate #-}

src/swarm-lang/Swarm/Language/Syntax/Util.hs

@@ -128,6 +128,7 @@ freeVarsS f = go S.empty
     TRef {} -> pure s
     TRequireDevice {} -> pure s
     TRequire {} -> pure s
+    TTydef {} -> pure s
     SRequirements x s1 -> rewrap $ SRequirements x <$> go bound s1
     TVar x
       | x `S.member` bound -> pure s

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

@@ -154,10 +154,11 @@ fromUModule ::
   ) =>
   UModule ->
   m TModule
-fromUModule (Module u uctx) =
+fromUModule (Module u uctx tydefctx) =
   Module
     <$> mapM (checkPredicative <=< (fmap fromU . generalize)) u
     <*> checkPredicative (fromU uctx)
+    <*> pure tydefctx
 
 finalizeUModule ::
   ( Has Unification sig m
@@ -335,7 +336,7 @@ instance (HasBindings u, Data u) => HasBindings (Syntax' u) where
   applyBindings (Syntax' l t cs u) = Syntax' l <$> applyBindings t <*> pure cs <*> applyBindings u
 
 instance HasBindings UModule where
-  applyBindings (Module u uctx) = Module <$> applyBindings u <*> applyBindings uctx
+  applyBindings (Module u uctx tydefs) = Module <$> applyBindings u <*> applyBindings uctx <*> pure tydefs
 
 -- ------------------------------------------------------------
 -- -- Converting between mono- and polytypes
@@ -566,22 +567,25 @@ inferModule s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
     t1' <- withBinding (lvVar x) (Forall [] xTy) $ infer t1
     _ <- unify (Just t1) (joined xTy (t1' ^. sType))
     pty <- generalize (t1' ^. sType)
-    return $ Module (Syntax' l (SDef r x Nothing t1') cs (UTyCmd UTyUnit)) (singleton (lvVar x) pty)
+    return $ Module (Syntax' l (SDef r x Nothing t1') cs (UTyCmd UTyUnit)) (singleton (lvVar x) pty) empty
 
   -- If a (poly)type signature has been provided, skolemize it and
   -- check the definition.
   SDef r x (Just pty) t1 -> withFrame l (TCDef (lvVar x)) $ do
     let upty = toU pty
     uty <- skolemize upty
     t1' <- withBinding (lvVar x) upty $ check t1 uty
-    return $ Module (Syntax' l (SDef r x (Just pty) t1') cs (UTyCmd UTyUnit)) (singleton (lvVar x) upty)
+    return $ Module (Syntax' l (SDef r x (Just pty) t1') cs (UTyCmd UTyUnit)) (singleton (lvVar x) upty) empty
 
+  -- Simply record a type synonym definition in the context.
+  TTydef x pty ->
+    return $ Module (Syntax' l (TTydef x pty) cs (UTyCmd UTyUnit)) empty (singleton (lvVar x) pty)
   -- To handle a 'TBind', infer the types of both sides, combining the
   -- returned modules appropriately.  Have to be careful to use the
   -- correct context when checking the right-hand side in particular.
   SBind mx c1 c2 -> do
     -- First, infer the left side.
-    Module c1' ctx1 <- withFrame l TCBindL $ inferModule c1
+    Module c1' ctx1 tydefs1 <- withFrame l TCBindL $ inferModule c1
     a <- decomposeCmdTy c1 (Actual, c1' ^. sType)
 
     -- Note we generalize here, similar to how we generalize at let
@@ -607,8 +611,9 @@ inferModule s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
     -- case the bound x should shadow the defined one; hence, we apply
     -- that binding /after/ (i.e. /within/) the application of @ctx1@.
     withBindings ctx1 $
+      -- XXX need to use tydefs1
       maybe id ((`withBinding` genA) . lvVar) mx $ do
-        Module c2' ctx2 <- withFrame l TCBindR $ inferModule c2
+        Module c2' ctx2 tydefs2 <- withFrame l TCBindR $ inferModule c2
 
         -- We don't actually need the result type since we're just
         -- going to return the entire type, but it's important to
@@ -626,6 +631,7 @@ inferModule s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
           Module
             (Syntax' l (SBind mx c1' c2') cs (c2' ^. sType))
             (ctx1 `Ctx.union` ctxX `Ctx.union` ctx2)
+            (tydefs1 `Ctx.union` tydefs2)
 
   -- In all other cases, there can no longer be any definitions in the
   -- term, so delegate to 'infer'.
@@ -1104,6 +1110,7 @@ analyzeAtomic locals (Syntax l t) = case t of
   TRequireDevice {} -> return 0
   TRequire {} -> return 0
   SRequirements {} -> return 0
+  TTydef {} -> return 0
   -- Constants.
   TConst c
     -- Nested 'atomic' is not allowed.

src/swarm-tui/Swarm/TUI/Controller.hs

@@ -95,7 +95,7 @@ import Swarm.Game.Step (finishGameTick, gameTick)
 import Swarm.Language.Capability (Capability (CGod, CMake), constCaps)
 import Swarm.Language.Context
 import Swarm.Language.Key (KeyCombo, mkKeyCombo)
-import Swarm.Language.Module (Module (..))
+import Swarm.Language.Module (moduleSyntax)
 import Swarm.Language.Parser.Lex (reservedWords)
 import Swarm.Language.Pipeline (ProcessedTerm (..), processTerm', processedSyntax)
 import Swarm.Language.Pipeline.QQ (tmQ)
@@ -351,9 +351,9 @@ handleMainEvent ev = do
         then -- ignore repeated keypresses
           continueWithoutRedraw
         else -- hide for two seconds
-        do
-          uiState . uiGameplay . uiHideRobotsUntil .= t + TimeSpec 2 0
-          invalidateCacheEntry WorldCache
+          do
+            uiState . uiGameplay . uiHideRobotsUntil .= t + TimeSpec 2 0
+            invalidateCacheEntry WorldCache
     -- debug focused robot
     MetaChar 'd' | isPaused && hasDebug -> do
       debug <- uiState . uiGameplay . uiShowDebug Lens.<%= not
@@ -1122,9 +1122,9 @@ runBaseTerm topCtx =
   -- The player typed something at the REPL and hit Enter; this
   -- function takes the resulting ProcessedTerm (if the REPL
   -- input is valid) and sets up the base robot to run it.
-  startBaseProgram t@(ProcessedTerm (Module tm _) reqs reqCtx) =
+  startBaseProgram t@(ProcessedTerm m reqs reqCtx) =
     -- Set the REPL status to Working
-    (gameState . gameControls . replStatus .~ REPLWorking (Typed Nothing (tm ^. sType) reqs))
+    (gameState . gameControls . replStatus .~ REPLWorking (Typed Nothing (m ^. moduleSyntax . sType) reqs))
       -- The `reqCtx` maps names of variables defined in the
       -- term (by `def` statements) to their requirements.
       -- E.g. if we had `def m = move end`, the reqCtx would

test/unit/TestLanguagePipeline.hs

@@ -15,7 +15,7 @@ import Data.Maybe
 import Data.Text (Text)
 import Data.Text qualified as T
 import Data.Text.Encoding qualified as T
-import Swarm.Language.Module (Module (..))
+import Swarm.Language.Module (moduleAST)
 import Swarm.Language.Parser (readTerm)
 import Swarm.Language.Parser.QQ (tyQ)
 import Swarm.Language.Pipeline (ProcessedTerm (..), processTerm)
@@ -458,7 +458,7 @@ testLanguagePipeline =
       | otherwise -> error "Unexpected success"
 
   getSyntax :: ProcessedTerm -> Syntax' Polytype
-  getSyntax (ProcessedTerm (Module s _) _ _) = s
+  getSyntax (ProcessedTerm m _ _) = moduleAST m
 
 -- | Check round tripping of term from and to text, then test ToJSON/FromJSON.
 roundTripTerm :: Text -> Assertion

test/unit/TestScoring.hs

@@ -61,10 +61,10 @@ testHighScores =
 compareAstSize :: Int -> FilePath -> TestTree
 compareAstSize expectedSize path = testCase (unwords ["size of", path]) $ do
   contents <- TIO.readFile $ baseTestPath </> path
-  ProcessedTerm (Module stx _) _ _ <- case processTermEither contents of
+  ProcessedTerm m _ _ <- case processTermEither contents of
     Right x -> return x
     Left y -> assertFailure (into @String y)
-  let actualSize = measureAstSize stx
+  let actualSize = measureAstSize (moduleAST m)
   assertEqual "incorrect size" expectedSize actualSize
 
 betterReplTimeAfterCodeSizeRecord :: TestTree