From d4c3e96fa2c41b0ab2e241ebc204f83a2aade167 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Sun, 26 May 2024 16:26:32 -0500
Subject: [PATCH] parsing for type definitions

---
 src/swarm-lang/Swarm/Language/Parser/Lex.hs  | 18 +++++++++++++---
 src/swarm-lang/Swarm/Language/Parser/Term.hs | 22 +++++++++++++++++++-
 2 files changed, 36 insertions(+), 4 deletions(-)

diff --git a/src/swarm-lang/Swarm/Language/Parser/Lex.hs b/src/swarm-lang/Swarm/Language/Parser/Lex.hs
index a407ea432a..d06b5204e9 100644
--- a/src/swarm-lang/Swarm/Language/Parser/Lex.hs
+++ b/src/swarm-lang/Swarm/Language/Parser/Lex.hs
@@ -31,6 +31,7 @@ module Swarm.Language.Parser.Lex (
   IdentifierType (..),
   locIdentifier,
   locTmVar,
+  locTyName,
   identifier,
   tyVar,
   tmVar,
@@ -45,7 +46,7 @@ module Swarm.Language.Parser.Lex (
 
 import Control.Lens (use, view, (%=), (.=))
 import Control.Monad (void)
-import Data.Char (isUpper)
+import Data.Char (isLower, isUpper)
 import Data.Containers.ListUtils (nubOrd)
 import Data.Sequence qualified as Seq
 import Data.Set (Set)
@@ -161,7 +162,7 @@ primitiveTypeNames = "Cmd" : baseTypeNames
 
 -- | List of keywords built into the language.
 keywords :: [Text]
-keywords = T.words "let in def end true false forall require requirements"
+keywords = T.words "let in def tydef end true false forall require requirements"
 
 -- | List of reserved words that cannot be used as variable names.
 reservedWords :: Set Text
@@ -194,7 +195,7 @@ reserved :: Text -> Parser ()
 reserved = reservedGen string'
 
 -- | What kind of identifier are we parsing?
-data IdentifierType = IDTyVar | IDTmVar
+data IdentifierType = IDTyVar | IDTyName | IDTmVar
   deriving (Eq, Ord, Show)
 
 -- | Parse an identifier together with its source location info.
@@ -215,6 +216,12 @@ locIdentifier idTy = do
       | IDTyVar <- idTy
       , T.toTitle t `S.member` reservedWords ->
           failT ["Reserved type name", squote t, "cannot be used as a type variable name; perhaps you meant", squote (T.toTitle t) <> "?"]
+      | IDTyName <- idTy
+      , T.toTitle t `S.member` reservedWords ->
+          failT ["Reserved type name", squote t, "cannot be redefined."]
+      | IDTyName <- idTy
+      , isLower (T.head t) ->
+          failT ["Type synonym names must start with an uppercase letter"]
       | IDTyVar <- idTy
       , isUpper (T.head t) ->
           failT ["Type variable names must start with a lowercase letter"]
@@ -224,6 +231,11 @@ locIdentifier idTy = do
 locTmVar :: Parser LocVar
 locTmVar = locIdentifier IDTmVar
 
+-- | Parse a user-defined type name together with its source location
+--   info.
+locTyName :: Parser LocVar
+locTyName = locIdentifier IDTyName
+
 -- | Parse an identifier, i.e. any non-reserved string containing
 --   alphanumeric characters and underscores, not starting with a
 --   digit. The Bool indicates whether we are parsing a type variable.
diff --git a/src/swarm-lang/Swarm/Language/Parser/Term.hs b/src/swarm-lang/Swarm/Language/Parser/Term.hs
index d345da8e76..867ef140f9 100644
--- a/src/swarm-lang/Swarm/Language/Parser/Term.hs
+++ b/src/swarm-lang/Swarm/Language/Parser/Term.hs
@@ -7,7 +7,7 @@
 module Swarm.Language.Parser.Term where
 
 import Control.Lens (view, (^.))
-import Control.Monad (guard)
+import Control.Monad (guard, join)
 import Control.Monad.Combinators.Expr
 import Data.Foldable (asum)
 import Data.List (foldl')
@@ -22,8 +22,10 @@ import Swarm.Language.Parser.Record (parseRecord)
 import Swarm.Language.Parser.Type
 import Swarm.Language.Syntax
 import Swarm.Language.Types
+import Swarm.Util (findDup)
 import Text.Megaparsec hiding (runParser)
 import Text.Megaparsec.Char
+import Witch (into)
 
 -- Imports for doctests (cabal-docspec needs this)
 
@@ -86,6 +88,9 @@ parseTermAtom2 =
           <$> (reserved "def" *> locTmVar)
           <*> optional (symbol ":" *> parsePolytype)
           <*> (symbol "=" *> parseTerm <* reserved "end")
+        <|> TTydef
+          <$> (reserved "tydef" *> locTyName)
+          <*> join (bindTydef <$> many tyVar <*> (symbol "=" *> parseType <* reserved "end"))
         <|> SRcd <$> brackets (parseRecord (optional (symbol "=" *> parseTerm)))
         <|> parens (view sTerm . mkTuple <$> (parseTerm `sepBy` symbol ","))
     )
@@ -109,6 +114,21 @@ sLet x ty t1 = SLet (lvVar x `S.member` setOf freeVarsV t1) x ty t1
 sDef :: LocVar -> Maybe Polytype -> Syntax -> Term
 sDef x ty t = SDef (lvVar x `S.member` setOf freeVarsV t) x ty t
 
+-- | Create a polytype from a list of variable binders and a type.
+--   Ensure that no binder is repeated, and all type variables in the
+--   type are present in the list of binders (/i.e./ the type contains
+--   no free type variables).
+bindTydef :: [Var] -> Type -> Parser Polytype
+bindTydef xs ty
+  | Just repeated <- findDup xs = fail $ "Duplicate variable on left-hand side of tydef: " ++ into @String repeated
+  | not (S.null free) =
+      fail $
+        "Undefined type variable(s) on right-hand side of tydef: "
+          ++ unwords (map (into @String) (S.toList free))
+  | otherwise = return $ Forall xs ty
+ where
+  free = tyVars ty `S.difference` S.fromList xs
+
 parseAntiquotation :: Parser Term
 parseAntiquotation =
   TAntiText <$> (lexeme . try) (symbol "$str:" *> tmVar)