From 4988bd9118b922c6af85563a79b1e606fc81b46c Mon Sep 17 00:00:00 2001 From: James Martin Date: Mon, 5 Apr 2021 09:47:10 -0700 Subject: [PATCH] WIP new syntax, revision 2 --- examples/examples.ivo | 45 ++-- src/Ivo/Expression.hs | 21 +- src/Ivo/Syntax/Base.hs | 189 +++---------- src/Ivo/Syntax/Parser.hs | 542 ++++++++++++++++++-------------------- src/Ivo/Syntax/Printer.hs | 208 +++++++-------- src/Ivo/Types.hs | 3 +- src/Ivo/Types/Base.hs | 59 +++-- 7 files changed, 482 insertions(+), 585 deletions(-) diff --git a/examples/examples.ivo b/examples/examples.ivo index 72994ab..7ca6c10 100755 --- a/examples/examples.ivo +++ b/examples/examples.ivo @@ -1,47 +1,52 @@ #!/usr/bin/env -S ivo -c -// Create a list by iterating `f` `n` times: -let iterate = \f x. +;; Create a list by iterating `f` `n` times: +iterate = \f x. { Z -> [] ; S n -> (x :: iterate f (f x) n) }; -// Use the iterate function to count to 10: -let countToTen : [Nat] = +;; Use the iterate function to count to 10: +countToTen : [Nat]; +countToTen = let countTo = iterate S 1 in countTo 10; -// Append two lists together: -let append = \xs ys. +;; Append two lists together: +append = \xs ys. { [] -> ys ; (x :: xs) -> (x :: append xs ys) } xs; -// Reverse a list: -let reverse = +;; Reverse a list: +reverse = { [] -> [] ; (x :: xs) -> append (reverse xs) [x] }; -// Now we can reverse `"reverse"`: -let reverseReverse : [Char] = reverse "reverse"; +;; Now we can reverse `"reverse"`: +reverseReverse : [Char]; +reverseReverse = reverse "reverse"; -// Calculating `3 + 2` with the help of Church-encoded numerals: -let threePlusTwo : Nat = +;; Calculating `3 + 2` with the help of Church-encoded numerals: +threePlusTwo : Nat; +threePlusTwo = let Sf = \n f x. f (n f x) ; plus = \x. x Sf in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z; -let undefined = undefined; +undefined = undefined; -// This expression would loop forever, but `callcc` saves the day! -let callccSaves : Nat = S (callcc \k. undefined (k Z)); +;; This expression would loop forever, but `callcc` saves the day! +callccSaves : Nat; +callccSaves = S (callcc \k. undefined (k Z)); -// And if it wasn't clear, this is what the `Char` constructor does: -let charB : Char = { Char c -> Char (S c) } 'a; -// (it outputs `'b`) +;; And if it wasn't clear, this is what the `Char` constructor does: +charB : Char; +charB = { Char c -> Char (S c) } 'a; +;; (it outputs `'b`) -// pack all of the examples into tuples so the main function can print them -let main = +;; pack all of the examples into tuples so the main function can print them +main = ( countToTen , ( reverseReverse , ( callccSaves diff --git a/src/Ivo/Expression.hs b/src/Ivo/Expression.hs index a768da4..74b09b9 100644 --- a/src/Ivo/Expression.hs +++ b/src/Ivo/Expression.hs @@ -16,7 +16,7 @@ module Ivo.Expression ) where import Ivo.Evaluator.Base -import Ivo.Syntax.Base +import Ivo.Syntax.Base qualified as S import Ivo.Types.Base import Data.Functor.Foldable (cata, hoist) @@ -30,12 +30,12 @@ builtins :: HashMap Text CheckExpr builtins = HM.fromList [("callcc", CallCCC)] -- | Convert from an abstract syntax tree to a typechecker expression. -ast2check :: AST -> CheckExpr -ast2check = substitute builtins . cata \case +ast2check :: S.Expr Text -> Either Text CheckExpr +ast2check = fmap (substitute builtins) . cata \case VarF name -> Var name - AppF ef exs -> foldl' App ef $ toList exs - AbsF ns e -> foldr Abs e $ toList ns - LetF ds e -> + AppF ef exs -> fmap (foldl' App ef) $ sequenceA $ toList exs + AbsF ns e -> fmap (foldr Abs e) $ sequenceA $ toList ns + LetF scope e -> let letExpr, letPlainExpr, letRecExpr :: Text -> CheckExpr -> CheckExpr -> CheckExpr @@ -47,7 +47,7 @@ ast2check = substitute builtins . cata \case letExpr name val body' | name `freeIn` val = letRecExpr name val body' | otherwise = letPlainExpr name val body' - in foldr (uncurry letExpr) e $ getNonEmptyDefFs ds + in fmap (foldr letExpr e) $ solveScope scope CtrF ctr es -> foldl' App (CtrC ctr) es CaseF ps -> Case ps AnnF () e t -> Ann () e t @@ -64,6 +64,9 @@ ast2check = substitute builtins . cata \case mkList :: [CheckExpr] -> CheckExpr mkList = foldr (App . App (CtrC CCons)) (CtrC CNil) +solveScope :: ScopeF CheckExpr -> Either Text [(Text, Maybe Type, CheckExpr)] +solveScope (ScopeF items) = _ + -- | Convert from declaration abstract syntax to a typechecker expression. decl2check :: Text -> AST -> CheckExpr decl2check name ast @@ -111,6 +114,10 @@ check2ast = hoist go . rename (HM.keysSet builtins) FixFC -> VarF "fix" HoleFC -> HoleFP +-- | Convert from a type to an abstract syntax tree. +type2ast :: Type -> S.Expr Text +type2ast = _ + -- | Convert from an evaluator expression to an abstract syntax tree. eval2ast :: EvalExpr -> AST -- Because all `ast2eval` replaces all free instances of `callcc`, diff --git a/src/Ivo/Syntax/Base.hs b/src/Ivo/Syntax/Base.hs index 4444088..66d346a 100644 --- a/src/Ivo/Syntax/Base.hs +++ b/src/Ivo/Syntax/Base.hs @@ -1,160 +1,49 @@ module Ivo.Syntax.Base - ( Expr (..), ExprF (..), Ctr (..), Pat, Def, DefF (..), PatF (..), VoidF, Text, NonEmpty (..) - , Type (..), TypeF (..), Scheme (..), tapp - , substitute, substitute1, rename, rename1, free, freeIn, bound, used - , Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..) - , pattern LetFP - , pattern PNat, pattern PNatF, pattern PList, pattern PListF, pattern PChar, pattern PCharF - , pattern PStr, pattern PStrF, pattern HoleP, pattern HoleFP - , simplify + ( Scope (..), Def (..) + , Expr (..), Type + , CaseBranches (..), Pattern (..) + , Literal (..) ) where -import Ivo.Expression.Base +import Data.List.NonEmpty (NonEmpty) +import Data.Text (Text) -import Data.Foldable (fold) -import Data.Functor.Foldable (embed, project, cata) -import Data.List.NonEmpty (NonEmpty (..), toList) -import Data.Text qualified as T +data Scope name = Scope { getScope :: ![Def name] } + deriving (Eq, Show) -data Parse --- | The abstract syntax tree reflects the structure of the externally-visible syntax. --- --- It includes syntactic sugar, which allows multiple ways to express many constructions, --- e.g. multiple definitions in a single let expression or multiple names bound by one abstraction. -type AST = Expr Parse --- There is no technical reason that the AST can't allow nullary applications and so forth, --- nor is there any technical reason that the parser couldn't parse them, --- but the parser *does* reject them to avoid confusing edge cases like `let x=in`, --- so they're forbidden here too so that the syntax tree can't contain data --- --- that the parser would refuse to accept. --- As a matter of curiosity, here's why `let x=in` was syntactically valid: --- 1. Parentheses in `let` statements are optional, infer them: `let x=()in()`. --- 2. Insert optional whitespace: `let x = () in ()`. --- 3. Nullary application expands to the identity function because --- the identity function is the left identity of function application: --- `let x=(\x.x) in \x.x`. -type instance AppArgs Parse = NonEmpty AST -type instance AbsArgs Parse = NonEmpty Text -type instance LetArgs Parse = NonEmpty (Def Parse) -type instance CtrArgs Parse = [AST] -type instance AnnX Parse = () -type instance XExpr Parse = ASTX +data Def name + = BasicDef !name !(Expr name) + | BasicDecl !(NonEmpty name) !(Type name) + deriving (Eq, Show) -type ASTX = ASTXF AST +data Expr name + = Var !name + | Lit !(Literal (Expr name)) + | App !(Expr name) !(NonEmpty (Expr name)) + | Let !(NonEmpty (Def name)) !(Expr name) + | Lam !(NonEmpty name) !(Expr name) + | Case !(Expr name) !(CaseBranches name) + | Forall !(NonEmpty name) !(Type name) + | Arrow !(Type name) !(Type name) + | Ann !(Expr name) !(Type name) + | Hole + deriving (Eq, Show) -type ASTF = ExprF Parse -type instance AppArgsF Parse = NonEmpty -type instance LetArgsF Parse = NonEmptyDefFs -type instance CtrArgsF Parse = [] -type instance XExprF Parse = ASTXF +type Type name = Expr name -data ASTXF r - -- | A natural number literal, e.g. `10`. - = PNat_ Int - -- | A list literal, e.g. `[x, y, z]`. - | PList_ [r] - -- | A character literal, e.g. `'a`. - | PChar_ Char - -- | A string literal, e.g. `"abcd"`. - | PStr_ Text - -- | A type hole. - | HoleP_ - deriving (Eq, Functor, Foldable, Traversable, Show) +data CaseBranches name = CaseBranches ![(Pattern name, Expr name)] + deriving (Eq, Show) -instance RecursivePhase Parse where - projectLetArgs = NonEmptyDefFs - embedLetArgs = getNonEmptyDefFs +data Pattern name + = PatVar !name + | PatLit !(Literal (Pattern name)) + | Irrelevant + | PatApp !name [Pattern name] + deriving (Eq, Show) -newtype NonEmptyDefFs r = NonEmptyDefFs { getNonEmptyDefFs :: NonEmpty (Text, r) } - deriving (Eq, Functor, Foldable, Traversable, Show) - -pattern LetFP :: NonEmpty (Text, r) -> r -> ASTF r -pattern LetFP ds e = LetF (NonEmptyDefFs ds) e - -pattern PNat :: Int -> AST -pattern PNat n = ExprX (PNat_ n) - -pattern PNatF :: Int -> ASTF r -pattern PNatF n = ExprXF (PNat_ n) - -pattern PList :: [AST] -> AST -pattern PList es = ExprX (PList_ es) - -pattern PListF :: [r] -> ASTF r -pattern PListF es = ExprXF (PList_ es) - -pattern PChar :: Char -> AST -pattern PChar c = ExprX (PChar_ c) - -pattern PCharF :: Char -> ASTF r -pattern PCharF c = ExprXF (PChar_ c) - -pattern PStrF :: Text -> ASTF r -pattern PStrF s = ExprXF (PStr_ s) - -pattern PStr :: Text -> AST -pattern PStr s = ExprX (PStr_ s) - -pattern HoleP :: AST -pattern HoleP = ExprX HoleP_ - -pattern HoleFP :: ASTF r -pattern HoleFP = ExprXF HoleP_ - -{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, AnnF, ExprXF #-} -{-# COMPLETE Var, App, Abs, Let, Ctr, Case, Ann, PNat, PList, PChar, PStr, HoleP #-} -{-# COMPLETE VarF, AppF, AbsF, LetF , CtrF, CaseF, AnnF, PNatF, PListF, PCharF, PStrF, HoleFP #-} -{-# COMPLETE VarF, AppF, AbsF, LetFP, CtrF, CaseF, AnnF, PNatF, PListF, PCharF, PStrF, HoleFP #-} - -instance Substitutable AST where - collectVars withVar withBinder = cata \case - VarF name -> withVar name - AbsF names body -> compose (fmap withBinder names) body - LetFP defs body -> - composeMap (\(name, def) body' -> - withBinder name def <> withBinder name body' - ) defs body - CaseF pats -> foldMap (\(Pat _ ns e) -> foldr withBinder e ns) pats - e -> fold e - - -- TODO - rename = error "rename not yet implemented for AST" - - -- TODO - unsafeSubstitute = error "unsafeSubstitute not yet implemented for AST" - --- | Combine nested expressions into compound expressions or literals when possible. -simplify :: AST -> AST -simplify = simplify' . embed . fmap simplify . project - where - -- Combine sequences of nat constructors into literals. - simplify' (Ctr CZero []) = PNat 0 - simplify' (Ctr CSucc [PNat n]) = PNat (n + 1) - -- Combine sequences of string constructors into string literals. - simplify' (Ctr CChar [PNat n]) = PChar (toEnum n) - simplify' o@(Ctr CCons [PChar c, PList []]) - | c /= '"' = PStr (T.singleton c) - | otherwise = o - simplify' o@(Ctr CCons [PChar c, PStr cs]) - | c /= '"' = PStr (T.cons c cs) - | otherwise = o - -- Combine sequences of list contructors into list literals. - simplify' (Ctr CNil []) = PList [] - simplify' (Ctr CCons [x, PList xs]) = PList (x : xs) - -- Move applications into constructors. - simplify' (App (Ctr ctr es1) es2) = simplify' $ Ctr ctr (es1 <> toList es2) - -- Combine reducible applications into let expressions. - simplify' (App (Abs (nx :| ns) eb) (ex :| es)) = simplify' $ app' es $ Let ((nx, ex) :| []) $ abs' ns eb - where app' [] e = e - app' (ex2:es2) e = App e (ex2 :| es2) - - abs' [] e = e - abs' (nx2:ns2) e = Abs (nx2 :| ns2) e - -- Combine sequences of nested applications into n-ary applications. - simplify' (App (App f es1) es2) = simplify' $ App f (es1 <> es2) - -- Combine sequences of nested abstractions into n-argument abstractions. - simplify' (Abs ns1 (Abs ns2 e)) = simplify' $ Abs (ns1 <> ns2) e - -- Combine sequences of nested let expressions into n-definition let expressions. - simplify' (Let ds1 (Let ds2 e)) = simplify' $ Let (ds1 <> ds2) e - simplify' e = e +data Literal r + = LitInt Int + | LitChar Char + | LitStr Text + | LitList [r] + deriving (Eq, Show) diff --git a/src/Ivo/Syntax/Parser.hs b/src/Ivo/Syntax/Parser.hs index 9591131..001251c 100644 --- a/src/Ivo/Syntax/Parser.hs +++ b/src/Ivo/Syntax/Parser.hs @@ -1,297 +1,279 @@ module Ivo.Syntax.Parser ( ParseError, parse - , Declaration, TopLevelAST, ProgramAST - , parseAST, parseTopLevel, parseProgram - , typeParser, schemeParser, astParser, topLevelParser, programParser + , fileParser, scopeParser, defParser, exprParser ) where import Ivo.Syntax.Base -import Data.Functor.Identity (Identity) -import Data.List.NonEmpty (fromList) +import Data.Char (isSeparator) +import Data.Functor (void) +import Data.List.NonEmpty (NonEmpty (..), fromList) +import Data.Text (Text) import Data.Text qualified as T -import Prelude hiding (succ, either) -import Text.Parsec hiding (label, token, spaces) -import Text.Parsec qualified -import Text.Parsec.Expr +import Text.Parsec hiding (spaces, label, sepBy, sepBy1, sepEndBy, sepEndBy1) +import Text.Parsec qualified as P +import Text.Parsec.Char () import Text.Parsec.Text (Parser) -spaces :: Parser () -spaces = Text.Parsec.spaces >> optional (try (comment >> spaces)) - where - comment, lineComment, blockComment :: Parser () - comment = blockComment <|> lineComment - lineComment = label "line comment" $ do - _ <- try (string "//") - _ <- many1 (noneOf "\n") - pure () - blockComment = label "block comment" $ do - _ <- try (string "/*") - _ <- many1 $ notFollowedBy (string "*/") >> anyChar - _ <- string "*/" - pure () - -label :: String -> Parser a -> Parser a -label = flip Text.Parsec.label - -token :: Char -> Parser () -token ch = label [ch] $ char ch *> spaces - -keywords :: [Text] -keywords = ["let", "in", "Left", "Right", "S", "Z", "forall", "Char", "Void", "Unit", "Nat", "Char"] - --- | A keyword is an exact string which is not part of an identifier. -keyword :: Text -> Parser () -keyword kwd = label (T.unpack kwd) $ do - try do - _ <- string $ T.unpack kwd - notFollowedBy letter - spaces - --- | An identifier is a sequence of letters which is not a keyword. -identifier :: Parser Text -identifier = label "identifier" $ do - notFollowedBy anyKeyword - T.pack <$> (many1 letter <* spaces) - where anyKeyword = choice $ map keyword keywords - -variable :: Parser AST -variable = label "variable" $ Var <$> identifier - -tvariable :: Parser Type -tvariable = label "variable" $ TVar <$> identifier - -many1' :: Parser a -> Parser (NonEmpty a) -many1' p = fromList <$> many1 p - -many2 :: Parser a -> Parser (a, NonEmpty a) -many2 p = (,) <$> p <*> many1' p - -grouping :: Parser AST -grouping = label "grouping" $ between (token '(') (token ')') ambiguous - -tgrouping :: Parser Type -tgrouping = label "grouping" $ between (token '(') (token ')') tambiguous - -application :: Parser AST -application = label "application" $ uncurry App <$> many2 block - -tapplication :: Parser Type -tapplication = label "application" $ uncurry tapp' <$> many2 tblock - where tapp' t1 (t2 :| ts) = tapp (t1 : t2 : ts) - -abstraction :: Parser AST -abstraction = label "lambda abstraction" $ Abs <$> between lambda (token '.') (many1' identifier) <*> ambiguous - where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces - -definition :: Parser (Def Parse) -definition = label "definition" $ do - name <- identifier - token '=' - value <- ambiguous - pure (name, value) - -let_ :: Parser AST -let_ = label "let expression" $ - Let <$> between (keyword "let") (keyword "in") definitions <*> ambiguous - where - definitions :: Parser (NonEmpty (Def Parse)) - definitions = fromList <$> sepBy1 definition (token ';') - -ctr :: Parser AST -ctr = label "data constructor" $ pair <|> unit <|> either <|> nat <|> list <|> str - where - unit, pairCtr, tuple, either, left, right, - zero, succ, natLit, consCtr, cons, charCtr, charLit, strLit :: Parser AST - unit = Ctr CUnit [] <$ keyword "()" - pair = pairCtr <|> tuple - pairCtr = Ctr CPair [] <$ keyword "(,)" - tuple = try $ between (token '(') (token ')') do - e1 <- ambiguous - token ',' - e2 <- ambiguous - pure $ Ctr CPair [e1, e2] - either = left <|> right - left = Ctr CLeft [] <$ keyword "Left" - right = Ctr CRight [] <$ keyword "Right" - nat = zero <|> succ <|> natLit - zero = Ctr CZero [] <$ keyword "Z" - succ = Ctr CSucc [] <$ keyword "S" - natLit = (PNat . read <$> many1 digit) <* spaces - list = cons <|> consCtr <|> listLit - consCtr = Ctr CCons [] <$ keyword "(::)" - cons = try $ between (token '(') (token ')') do - e1 <- ambiguous - keyword "::" - e2 <- ambiguous - pure $ Ctr CCons [e1, e2] - listLit = fmap PList $ between (token '[') (token ']') $ sepEndBy ambiguous (token ',') - str = charCtr <|> charLit <|> strLit - charCtr = Ctr CChar [] <$ keyword "Char" - charLit = fmap PChar $ char '\'' *> anyChar <* spaces - strLit = fmap (PStr . T.pack) $ between (token '"') (token '"') $ many (noneOf "\"") - -pat :: Parser (Pat Parse) -pat = label "case alternate" $ do - (c, ns) <- label "pattern" $ - pair <|> unit <|> left <|> right <|> zero <|> succ <|> nil <|> cons <|> char' - keyword "->" - e <- ambiguous - pure $ Pat c ns e - where - pair = try $ between (token '(') (token ')') do - e1 <- identifier - token ',' - e2 <- identifier - pure (CPair, [e1, e2]) - unit = (CUnit, []) <$ keyword "()" - left = do - keyword "Left" - e <- identifier - pure (CLeft, [e]) - right = do - keyword "Right" - e <- identifier - pure (CRight, [e]) - zero = (CZero, []) <$ keyword "Z" - succ = do - keyword "S" - e <- identifier - pure (CSucc, [e]) - nil = (CNil, []) <$ keyword "[]" - cons = try $ between (token '(') (token ')') do - e1 <- identifier - keyword "::" - e2 <- identifier - pure (CCons, [e1, e2]) - char' = do - keyword "Char" - e <- identifier - pure (CChar, [e]) - -case_ :: Parser AST -case_ = label "case patterns" $ do - token '{' - pats <- sepEndBy pat (token ';') - token '}' - pure $ Case pats - -ann :: Parser AST -ann = label "type annotation" $ do - e <- block - token ':' - t <- tambiguous - pure (Ann () e t) - -hole :: Parser AST -hole = label "hole" $ HoleP <$ token '_' - -tlist :: Parser Type -tlist = between (token '[') (token ']') $ ((TApp TList <$> tambiguous) <|> pure TList) - -tinfix :: Parser Type -tinfix = buildExpressionParser ttable tblock - where - ttable :: [[Operator Text () Identity Type]] - ttable = [ [Infix (binop TAbs <$ arrSym) AssocRight] - , [Infix (binop TProd <$ token '*') AssocRight] - , [Infix (binop TSum <$ token '+') AssocRight] - ] - - arrSym :: Parser () - arrSym = token '→' <|> keyword "->" - - binop :: Type -> Type -> Type -> Type - binop c t1 t2 = TApp (TApp c t1) t2 - -tctr :: Parser Type -tctr = tlist <|> tunit <|> tvoid <|> tnat <|> tchar - where - tunit = TUnit <$ (keyword "Unit" <|> keyword "⊤") - tvoid = TVoid <$ (keyword "Void" <|> keyword "⊥") - tnat = TNat <$ (keyword "Nat" <|> keyword "ℕ") - tchar = TChar <$ keyword "Char" - -tfinite :: Parser Type -tfinite = tvariable <|> tlist <|> tctr <|> tgrouping - -tblock :: Parser Type -tblock = tfinite - -tambiguous :: Parser Type -tambiguous = try tinfix <|> try tapplication <|> tblock - -tforall :: Parser Scheme -tforall = do - keyword "forall" <|> token '∀' - names <- many1 (identifier <* spaces) - token '.' - ty <- tambiguous - pure $ TForall names ty - -scheme :: Parser Scheme -scheme = tforall <|> (TForall [] <$> tambiguous) - --- | Guaranteed to consume a finite amount of input -finite :: Parser AST -finite = label "finite expression" $ variable <|> hole <|> ctr <|> case_ <|> grouping - --- | Guaranteed to consume input, but may continue until it reaches a terminator -block :: Parser AST -block = label "block expression" $ abstraction <|> let_ <|> finite - --- | Not guaranteed to consume input at all, may continue until it reaches a terminator -ambiguous :: Parser AST -ambiguous = label "any expression" $ try ann <|> try application <|> block - -typeParser :: Parser Type -typeParser = tambiguous - -schemeParser :: Parser Scheme -schemeParser = scheme - -astParser :: Parser AST -astParser = ambiguous - -parseAST :: Text -> Either ParseError AST -parseAST = parse (spaces *> ambiguous <* eof) "input" - -type Declaration = (Text, Maybe Type, AST) - -definitionAnn :: Parser Declaration -definitionAnn = do - name <- identifier - ty <- optionMaybe $ token ':' *> tambiguous - token '=' - e <- ambiguous - pure (name, ty, e) - -declaration :: Parser Declaration -declaration = notFollowedBy (try let_) >> do - keyword "let" - definitionAnn - --- | A program is a series of declarations and expressions to execute. -type ProgramAST = [Declaration] -type TopLevelAST = [Either Declaration AST] - -topLevel :: Parser (Either Declaration AST) -topLevel = try (Left <$> declaration) <|> (Right <$> ambiguous) - -topLevelParser :: Parser TopLevelAST -topLevelParser = spaces *> sepEndBy topLevel (token ';') <* eof +fileParser :: Parser (Scope Text) +fileParser = do + shebang + scope shebang :: Parser () shebang = do - try $ keyword "#!" + _ <- try $ string "#!" skipMany (noneOf "\n") spaces -programParser :: Parser ProgramAST -programParser = shebang *> sepEndBy declaration (token ';') <* eof +scopeParser, scope :: Parser (Scope Text) +scopeParser = scope -parseTopLevel :: Text -> Either ParseError TopLevelAST -parseTopLevel = parse topLevelParser "input" +scope = Scope <$> flexBraces def -parseProgram :: Text -> Either ParseError ProgramAST -parseProgram = parse programParser "input" +defParser, def, basicDef, basicDecl :: Parser (Def Text) +defParser = def + +def = try basicDef <|> basicDecl + +basicDef = do + n <- name + tokEquals + body <- ambiguous + pure $ BasicDef n body + +basicDecl = do + names <- many1' name + tokCol + ty <- ambiguous + pure $ BasicDecl names ty + +exprParser, ambiguous, block, finite :: Parser (Expr Text) +exprParser = ambiguous + +-- | Syntax which may recurse before consuming input. +ambiguous = try app <|> try arrow <|> try ann <|> block + +-- | Syntax which consumes input before recursing. +block = let_ <|> lam <|> case_ <|> forall <|> finite + +-- | Syntax which consumes input both before and after recursing. +finite = hole <|> lit <|> var <|> parens ambiguous + +var, lit, app, let_, lam, case_, forall, arrow, ann, hole :: Parser (Expr Text) + +var = Var <$> name + +lit = Lit <$> literal ambiguous + +app = uncurry App <$> many2' ambiguous + +let_ = do + kwdLet + defs <- flexSepBy1' (tok ";") def + kwdIn + body <- ambiguous + pure $ Let defs body + +lam = do + kwdLam + args <- many1' name + kwdArrow + body <- ambiguous + pure $ Lam args body + +case_ = do + kwdCase + arg <- ambiguous + branches <- caseBranches + pure $ Case arg branches + +forall = do + kwdForall + names <- many1' name + kwdFatArrow + ty <- ambiguous + pure $ Forall names ty + +arrow = do + arg <- block + kwdArrow + ret <- ambiguous + pure $ Arrow arg ret + +ann = do + expr <- block + kwdCol + ty <- ambiguous + pure $ Ann expr ty + +hole = Hole <$ kwdHole + +caseBranches :: Parser (CaseBranches Text) +caseBranches = CaseBranches <$> flexBraces caseBranch + +caseBranch :: Parser (Pattern Text, Expr Text) +caseBranch = do + pat <- pattern_ + kwdArrow + body <- ambiguous + pure (pat, body) + +pattern_, patVar, patLit, patIrrelevant, patApp :: Parser (Pattern Text) + +pattern_ = patVar <|> patLit <|> patIrrelevant <|> patApp + +patVar = PatVar <$> name + +patLit = PatLit <$> literal pattern_ + +patIrrelevant = Irrelevant <$ kwdHole + +patApp = do + ctr <- name + args <- many1 pattern_ + pure $ PatApp ctr args + +literal :: Parser r -> Parser (Literal r) +literal p = litInt <|> litChar <|> litStr <|> litList p + +litInt, litChar, litStr :: Parser (Literal r) + +litInt = do + sign <- ("-" <$ tokNegative) <|> ("" <$ tokPositive) <|> pure "" + digits <- many1 $ optional (char '_') *> digit + pure $ LitInt $ read $ sign ++ digits + +litChar = do + close <- matchingSingleQuote <$> tokOpenSingleQuote + body <- noneOf (close : "\n") + tok $ T.singleton close + pure $ LitChar body + +litStr = do + close <- matchingQuote <$> tokOpenQuote + body <- many1 $ satisfy \c -> c /= close && not (isSeparator c) + tok $ T.singleton close + pure $ LitStr $ T.pack body + +litList :: Parser r -> Parser (Literal r) +litList p = LitList <$> flexBrackets p + +comment :: Parser () +comment = do + tok ";;" + skipMany1 $ noneOf "\n" + spaces + +name :: Parser Text +name = do + notFollowedBy (anyKwd <|> void litInt) + n <- many1 legalChar + spaces + pure $ T.pack n + +legalChar :: Parser Char +legalChar = satisfy isLegalChar + +isLegalChar :: Char -> Bool +isLegalChar c = not (isSeparator c) && c `notElem` forbidden + where + forbidden :: String + forbidden = "\"“”'‘’(){};" + +kwdLet, kwdIn, kwdLam, kwdCase, kwdForall, kwdFatArrow, kwdArrow, + kwdCol, kwdHole :: Parser () +kwdLet = kwd "let" +kwdIn = kwd "in" +kwdLam = kwd "λ" <|> kwd "\\" +kwdCase = kwd "case" +kwdForall = kwd "∀" <|> kwd "forall" +kwdFatArrow = kwd "⇒" <|> kwd "=>" +kwdArrow = kwd "→" <|> kwd "->" +kwdCol = kwd ":" +kwdHole = kwd "_" + +kwd :: Text -> Parser () +kwd txt = try do + _ <- string $ T.unpack txt + notFollowedBy legalChar + +anyKwd :: Parser () +anyKwd = kwdLet <|> kwdIn <|> kwdLam <|> kwdCase <|> kwdForall <|> kwdFatArrow + <|> kwdArrow <|> kwdCol <|> kwdHole + +tokEquals, tokCol, tokNegative, tokPositive :: Parser () + +tokEquals = void $ char '=' -- U+003D EQUALS SIGN + +tokCol = void $ char ':' -- U+003A COLON + +tokNegative = void $ + char '-' -- U+002D HYPHEN-MINUS + <|> char '⁻' -- U+207B SUPERSCRIPT MINUS + +tokPositive = void $ + char '+' -- U+002B PLUS SIGN + <|> char '⁺' -- U+207A SUPERSCRIPT PLUS SIGN + +tokOpenQuote, tokOpenSingleQuote :: Parser Char + +tokOpenQuote = + char '"' -- U+0022 QUOTATION MARK + <|> char '“' -- U+201C LEFT DOUBLE QUOTATION MARK + +tokOpenSingleQuote = + char '\'' -- U+0027 APOSTROPHE + <|> char '‘' -- U+2018 LEFT SINGLE QUOTATION MARK + +matchingQuote, matchingSingleQuote :: Char -> Char + +matchingQuote = \case + '"' -> '"' -- U+0022 QUOTATION MARK (again) + '“' -> '”' -- U+201D RIGHT DOUBLE QUOTATION MARK + _ -> error "no matching double quote" + +matchingSingleQuote = \case + '\'' -> '\'' -- U+0027 APOSTROPHE (again) + '‘' -> '’' -- U+2019 RIGHT SINGLE QUOTATION MARK + _ -> error "no matching single quote" + +tok :: Text -> Parser () +tok txt = do + _ <- string $ T.unpack txt + spaces + +sepEndBy, sepEndBy1 :: Parser delim -> Parser a -> Parser [a] +sepEndBy = flip P.sepEndBy +sepEndBy1 = flip P.sepEndBy1 + +flexSepBy :: Parser delim -> Parser a -> Parser [a] +flexSepBy delim p = do + optional delim + sepEndBy delim p + +flexSepBy1 :: Parser delim -> Parser a -> Parser [a] +flexSepBy1 delim p = do + optional delim + sepEndBy1 delim p + +flexSepBy1' :: Parser delim -> Parser a -> Parser (NonEmpty a) +flexSepBy1' delim p = fromList <$> flexSepBy1 delim p + +parens :: Parser a -> Parser a +parens = between (tok "(") (tok ")") + +flexBrackets :: Parser a -> Parser [a] +flexBrackets = between (kwd "[") (kwd "]") . flexSepBy (tok ";") + +flexBraces :: Parser a -> Parser [a] +flexBraces = between (tok "{") (tok "}") . flexSepBy (tok ";") + +many1' :: Parser a -> Parser (NonEmpty a) +many1' p = (:|) <$> p <*> many p + +many2' :: Parser a -> Parser (a, NonEmpty a) +many2' p = (,) <$> p <*> many1' p + +spaces :: Parser () +spaces = P.spaces >> optional comment diff --git a/src/Ivo/Syntax/Printer.hs b/src/Ivo/Syntax/Printer.hs index 2c47cfe..90e7fd2 100644 --- a/src/Ivo/Syntax/Printer.hs +++ b/src/Ivo/Syntax/Printer.hs @@ -1,123 +1,119 @@ -module Ivo.Syntax.Printer (unparseAST, unparseType, unparseScheme) where +module Ivo.Syntax.Printer + ( unparseScope, unparseDef, unparseExpr + ) where import Ivo.Syntax.Base -import Data.Functor.Base (NonEmptyF (NonEmptyF)) -import Data.Functor.Foldable (cata) -import Data.List.NonEmpty (toList) +import Data.Foldable (foldl', toList) +import Data.Text (Text) import Data.Text qualified as T -import Data.Text.Lazy (fromStrict, toStrict, intercalate, unwords, singleton) -import Data.Text.Lazy.Builder (Builder, fromText, fromLazyText, toLazyText, fromString) +import Data.Text.Lazy (toStrict) +import Data.Text.Lazy.Builder (Builder, fromText, toLazyText, fromString) import Prelude hiding (unwords) --- I'm surprised this isn't in base somewhere. -unsnoc :: NonEmpty a -> ([a], a) -unsnoc = cata \case - NonEmptyF x' Nothing -> ([], x') - NonEmptyF x (Just (xs, x')) -> (x : xs, x') +unparseScope :: Scope Text -> Text +unparseScope = unparse scope -data SyntaxType - -- | Ambiguous syntax is not necessarily finite and not guaranteed to consume any input. - = Ambiguous - -- | Block syntax is not necessarily finite but is guaranteed to consume input. - | Block - -- | Unambiguous syntax is finite and guaranteed to consume input. - | Finite -type Tagged a = (SyntaxType, a) +unparseDef :: Def Text -> Text +unparseDef = unparse def -tag :: SyntaxType -> a -> Tagged a -tag = (,) +unparseExpr :: Expr Text -> Text +unparseExpr = unparse expr -group :: Builder -> Builder -group x = "(" <> x <> ")" +scope :: Unparser (Scope Text) +scope (Scope defs) = Block $ flexSepEndBy "; " $ map (ambiguous . def) defs --- | An unambiguous context has a marked beginning and end. -unambiguous :: Tagged Builder -> Builder -unambiguous (_, t) = t +def :: Unparser (Def Text) +def (BasicDef name body) = + Block $ fromText name <> " = " <> ambiguous (expr body) +def (BasicDecl names ty) = + Block $ unnames names <> " : " <> ambiguous (expr ty) --- | A final context has a marked end but no marked beginning, --- so we provide a grouper when a beginning marker is necessary. -final :: Tagged Builder -> Builder -final (Ambiguous, t) = group t -final (_, t) = t +expr :: Unparser (Expr Text) +expr (Var name) = Finite $ fromText name +expr (Lit lit) = Block $ literal expr lit +expr (App ef exs) = Ambiguous $ sepBy " " $ map (finite . expr) $ ef : toList exs +expr (Let defs body) = Block $ + "let " <> ambiguous (scope $ Scope $ toList defs) <> + " in " <> ambiguous (expr body) +expr (Lam names body) = Block $ + "λ " <> unnames names <> " → " <> ambiguous (expr body) +expr (Case arg branches) = Block $ + "case " <> ambiguous (expr arg) <> " " <> caseBranches branches +expr (Forall names ty) = Block $ + "∀ " <> unnames names <> " ⇒ " <> ambiguous (expr ty) +expr (Arrow arg ty) = Ambiguous $ + block (expr arg) <> " → " <> ambiguous (expr ty) +expr (Ann e ty) = Ambiguous $ + block (expr e) <> " : " <> ambiguous (expr ty) +expr Hole = Finite "_" + +caseBranches :: CaseBranches Text -> Builder +caseBranches (CaseBranches pats) = flexBraces $ map caseBranch pats + +caseBranch :: (Pattern Text, Expr Text) -> Builder +caseBranch (pat, body) = pattern_ pat <> " → " <> ambiguous (expr body) + +pattern_ :: Pattern Text -> Builder +pattern_ (PatVar name) = fromText name +pattern_ (PatLit lit) = literal (Finite . pattern_) lit +pattern_ Irrelevant = "_" +pattern_ (PatApp ctr args) = + fromText ctr <> " " <> sepBy " " (map pattern_ args) + +literal :: Unparser a -> Literal a -> Builder +literal up = \case + LitInt n + | n > 0 -> fromString $ "⁻" <> show (abs n) + | otherwise -> fromString $ show n + LitChar c -> "‘" <> fromText (T.singleton c) <> "’" + LitStr s -> "“" <> fromText s <> "”" + LitList xs -> flexBrackets $ map (ambiguous . up) xs + +unnames :: Foldable t => t Text -> Builder +unnames = fromText . T.unwords . toList + +between :: Builder -> Builder -> Builder -> Builder +between l r x = l <> x <> r + +sepBy, flexSepEndBy :: Foldable t => Builder -> t Builder -> Builder + +sepBy delim = foldl' (\x xs -> x <> delim <> xs) "" + +flexSepEndBy delim = foldMap (<> delim) + +flexBrackets, flexBraces :: Foldable t => t Builder -> Builder + +flexBrackets = between "[ " " ]" . sepBy "; " + +flexBraces = between "{ " " }" . sepBy "; " + +type Unparser a = a -> Tagged Builder + +data Tagged a + = Ambiguous !a + | Block !a + | Finite !a + +untag :: Tagged a -> a +untag = \case + Ambiguous x -> x + Block x -> x + Finite x -> x --- | An ambiguous context has neither a marked end nor marked beginning, --- so we provide a grouper when an ending marker is necessary. ambiguous :: Tagged Builder -> Builder -ambiguous (Finite, t) = t -ambiguous (_, t) = group t +ambiguous = untag --- | Turn an abstract syntax tree into the corresponding concrete syntax. --- --- This is *not* a pretty-printer; it uses minimal whitespace. -unparseAST :: AST -> Text -unparseAST = toStrict . toLazyText . snd . cata \case - VarF name -> tag Finite $ fromText name - AppF ef exs -> unparseApp ef exs - AbsF names body -> tag Block $ - let names' = fromLazyText (unwords $ map fromStrict $ toList names) - in "λ" <> names' <> ". " <> unambiguous body - LetFP defs body -> tag Block $ "let " <> unparseDefs defs <> " in " <> unambiguous body - CtrF ctr e -> unparseCtr ctr e - CaseF pats -> - let pats' = fromLazyText $ intercalate "; " $ map (toLazyText . unparsePat) pats - in tag Finite $ "{ " <> pats' <> " }" - AnnF () e t -> tag Ambiguous $ final e <> " : " <> fromText (unparseType t) - PNatF n -> tag Finite $ fromString $ show n - PListF es -> - let es' = fromLazyText $ intercalate ", " $ map (toLazyText . unambiguous) es - in tag Finite $ "[" <> es' <> "]" - PStrF s -> tag Finite $ "\"" <> fromText s <> "\"" - PCharF c -> tag Finite $ "'" <> fromLazyText (singleton c) - HoleFP -> tag Finite "_" - where - unparseApp :: Tagged Builder -> NonEmpty (Tagged Builder) -> Tagged Builder - unparseApp ef (unsnoc -> (exs, efinal)) - = tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) (ef : exs) +block :: Tagged Builder -> Builder +block (Ambiguous x) = parens x +block x = untag x - unparseDef (name, val) = fromText name <> " = " <> unambiguous val - unparseDefs defs = fromLazyText (intercalate "; " $ map (toLazyText . unparseDef) $ toList defs) +finite :: Tagged Builder -> Builder +finite (Finite x) = x +finite x = parens $ untag x - unparseCtr :: Ctr -> [Tagged Builder] -> Tagged Builder - -- Fully-applied special syntax forms - unparseCtr CPair [x, y] = tag Finite $ "(" <> unambiguous x <> ", " <> unambiguous y <> ")" - unparseCtr CCons [x, y] = tag Finite $ "(" <> unambiguous x <> " :: " <> unambiguous y <> ")" - -- Partially-applied syntax forms - unparseCtr CUnit [] = tag Finite "()" - unparseCtr CPair [] = tag Finite "(,)" - unparseCtr CLeft [] = tag Finite "Left" - unparseCtr CRight [] = tag Finite "Right" - unparseCtr CZero [] = tag Finite "Z" - unparseCtr CSucc [] = tag Finite "S" - unparseCtr CNil [] = tag Finite "[]" - unparseCtr CCons [] = tag Finite "(::)" - unparseCtr CChar [] = tag Finite "Char" - unparseCtr ctr (x:xs) = unparseApp (unparseCtr ctr []) (x :| xs) +parens :: Builder -> Builder +parens = between "(" ")" - unparsePat (Pat ctr ns e) - = unambiguous (unparseCtr ctr (map (tag Finite . fromText) ns)) <> " -> " <> unambiguous e - --- HACK -pattern TApp2 :: Type -> Type -> Type -> Type -pattern TApp2 tf tx ty = TApp (TApp tf tx) ty - --- TODO: Improve these printers. -unparseType :: Type -> Text -unparseType (TVar name) = name -unparseType (TApp2 TAbs a b) = "(" <> unparseType a <> " -> " <> unparseType b <> ")" -unparseType (TApp2 TProd a b) = "(" <> unparseType a <> " * " <> unparseType b <> ")" -unparseType (TApp2 TSum a b) = "(" <> unparseType a <> " + " <> unparseType b <> ")" -unparseType (TApp TList a) = "[" <> unparseType a <> "]" -unparseType (TApp a b) = "(" <> unparseType a <> " " <> unparseType b <> ")" -unparseType TAbs = "(->)" -unparseType TProd = "(*)" -unparseType TSum = "(+)" -unparseType TUnit = "★" -unparseType TVoid = "⊥" -unparseType TNat = "Nat" -unparseType TList = "[]" -unparseType TChar = "Char" - -unparseScheme :: Scheme -> Text -unparseScheme (TForall [] t) = unparseType t -unparseScheme (TForall names t) = "∀" <> T.unwords names <> ". " <> unparseType t +unparse :: Unparser a -> a -> Text +unparse up = toStrict . toLazyText . untag . up diff --git a/src/Ivo/Types.hs b/src/Ivo/Types.hs index e08b9b8..6d51b89 100644 --- a/src/Ivo/Types.hs +++ b/src/Ivo/Types.hs @@ -79,8 +79,9 @@ j (Abs n_arg e_ret) = do t_arg <- fresh t_ret <- bindVar n_arg t_arg $ j e_ret pure $ tapp [TAbs, t_arg, t_ret] -j (Let (n_x, e_x) e_ret) = do +j (LetC n_x t_ann_x e_x e_ret) = do (t_x_mono, c) <- listen $ j e_x + mapM_ (unify t_x_mono) t_ann_x s <- solve' c t_x_poly <- generalize $ substitute s t_x_mono local (HM.insert n_x t_x_poly) $ j e_ret diff --git a/src/Ivo/Types/Base.hs b/src/Ivo/Types/Base.hs index 145a14a..40abb3d 100644 --- a/src/Ivo/Types/Base.hs +++ b/src/Ivo/Types/Base.hs @@ -3,8 +3,9 @@ module Ivo.Types.Base , Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text , Type (..), TypeF (..), Scheme (..), tapp , substitute, substitute1, rename, rename1, free, bound, used - , Check, CheckExpr, CheckExprF, CheckX, CheckXF (..) - , pattern AppFC, pattern CtrC, pattern CtrFC, pattern CallCCC, pattern CallCCFC + , Check, CheckExpr, CheckExprF, CheckLet, CheckLetF (..), CheckX, CheckXF (..) + , pattern AppFC, pattern LetC, pattern LetFC + , pattern CtrC, pattern CtrFC, pattern CallCCC, pattern CallCCFC , pattern FixC, pattern FixFC, pattern HoleC, pattern HoleFC , Substitution, Context, Constraint , MonoSubstitutable, substituteMono, substituteMono1 @@ -26,19 +27,23 @@ data Check type CheckExpr = Expr Check type instance AppArgs Check = CheckExpr type instance AbsArgs Check = Text -type instance LetArgs Check = (Text, CheckExpr) +type instance LetArgs Check = CheckLet type instance CtrArgs Check = UnitF CheckExpr type instance AnnX Check = () type instance XExpr Check = CheckX +type CheckLet = CheckLetF CheckExpr type CheckX = CheckXF CheckExpr type CheckExprF = ExprF Check type instance AppArgsF Check = Identity -type instance LetArgsF Check = DefF +type instance LetArgsF Check = CheckLetF type instance CtrArgsF Check = UnitF type instance XExprF Check = CheckXF +data CheckLetF r = CheckLet Text (Maybe Type) r + deriving (Eq, Functor, Foldable, Traversable, Show) + data CheckXF r -- | Call-with-current-continuation. = CallCCC_ @@ -49,6 +54,12 @@ data CheckXF r | HoleC_ deriving (Eq, Functor, Foldable, Traversable, Show) +pattern LetC :: Text -> Maybe Type -> CheckExpr -> CheckExpr -> CheckExpr +pattern LetC name ty expr body = Let (CheckLet name ty expr) body + +pattern LetFC :: Text -> Maybe Type -> r -> r -> CheckExprF r +pattern LetFC name ty expr body = LetF (CheckLet name ty expr) body + pattern CtrC :: Ctr -> CheckExpr pattern CtrC c = Ctr c Unit @@ -76,38 +87,44 @@ pattern HoleC = ExprX HoleC_ pattern HoleFC :: CheckExprF r pattern HoleFC = ExprXF HoleC_ -{-# COMPLETE Var, App, Abs, Let, CtrC, Case, Ann, ExprX #-} -{-# COMPLETE VarF, AppF, AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF #-} -{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF, CaseF, AnnF, ExprXF #-} -{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF #-} -{-# COMPLETE Var, App, Abs, Let, Ctr, Case, Ann, CallCCC, FixC, HoleC #-} -{-# COMPLETE Var, App, Abs, Let, CtrC, Case, Ann, CallCCC, FixC, HoleC #-} -{-# COMPLETE VarF, AppF, AbsF, LetF, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} -{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} -{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} +{-# COMPLETE Var, App, Abs, Let, CtrC, Case, Ann, ExprX #-} +{-# COMPLETE VarF, AppF, AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF #-} +{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF, CaseF, AnnF, ExprXF #-} +{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF #-} +{-# COMPLETE Var, App, Abs, Let, Ctr, Case, Ann, CallCCC, FixC, HoleC #-} +{-# COMPLETE Var, App, Abs, Let, CtrC, Case, Ann, CallCCC, FixC, HoleC #-} +{-# COMPLETE VarF, AppF, AbsF, LetF, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} +{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} +{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} +{-# COMPLETE Var, App, Abs, LetC, CtrC, Case, Ann, ExprX #-} +{-# COMPLETE VarF, AppF, AbsF, LetFC, CtrFC, CaseF, AnnF, ExprXF #-} +{-# COMPLETE VarF, AppFC, AbsF, LetFC, CtrF, CaseF, AnnF, ExprXF #-} +{-# COMPLETE VarF, AppFC, AbsF, LetFC, CtrFC, CaseF, AnnF, ExprXF #-} +{-# COMPLETE Var, App, Abs, LetC, Ctr, Case, Ann, CallCCC, FixC, HoleC #-} +{-# COMPLETE Var, App, Abs, LetC, CtrC, Case, Ann, CallCCC, FixC, HoleC #-} +{-# COMPLETE VarF, AppF, AbsF, LetFC, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} +{-# COMPLETE VarF, AppFC, AbsF, LetFC, CtrF, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} +{-# COMPLETE VarF, AppFC, AbsF, LetFC, CtrFC, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-} instance RecursivePhase Check where projectAppArgs = Identity - projectLetArgs = projectDef - embedAppArgs = runIdentity - embedLetArgs = embedDef instance Substitutable CheckExpr where collectVars withVar withBinder = cata \case VarF n -> withVar n AbsF n e -> withBinder n e - LetF (Def n x) e -> x <> withBinder n e + LetF (CheckLet n _ x) e -> x <> withBinder n e CaseF pats -> foldMap (\(Pat _ ns e) -> foldr withBinder e ns) pats e -> fold e rename = runRenamer $ \badNames -> cata \case VarF n -> asks $ Var . HM.findWithDefault n n AbsF n e -> uncurry Abs . first runIdentity <$> replaceNames badNames (Identity n) e - LetF (Def n x) e -> do + LetFC n ty x e -> do x' <- x (Identity n', e') <- replaceNames badNames (Identity n) e - pure $ Let (n', x') e' + pure $ LetC n' ty x' e' CaseF ps -> Case <$> forM ps \(Pat ctr ns e) -> uncurry (Pat ctr) <$> replaceNames badNames ns e e -> embed <$> sequenceA e @@ -115,10 +132,10 @@ instance Substitutable CheckExpr where unsafeSubstitute = runSubstituter $ para \case VarF name -> asks $ HM.findWithDefault (Var name) name AbsF name e -> Abs name <$> maySubstitute (Identity name) e - LetF (Def name (_, x)) e -> do + LetFC name ty (_, x) e -> do x' <- x e' <- maySubstitute (Identity name) e - pure $ Let (name, x') e' + pure $ LetC name ty x' e' CaseF pats -> Case <$> for pats \(Pat ctr ns e) -> Pat ctr ns <$> maySubstitute ns e e -> embed <$> traverse snd e