add TTydef syntax node and related infrastructure

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 -> 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

@@ -26,7 +26,8 @@ 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.
+--   as a context, which maps term variable names to their types, and
+--   type synonym names to their definitions.
 data Module s t = Module {moduleAST :: Syntax' s, moduleCtx :: Ctx t}
   deriving (Show, Eq, Functor, Data, Generic, FromJSON, ToJSON)
 

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

@@ -576,6 +576,9 @@ inferModule s@(CSyntax l t cs) = addLocToTypeErr l $ case t of
     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)
 
+  -- Simply record a type synonym definition in the context.
+  TTydef x pty ->
+    return $ Module (Syntax' l (TTydef x pty) cs (UTyCmd UTyUnit)) (singleton (lvVar x) (toU 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.
@@ -1104,6 +1107,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.