james
/
ivo
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

WIP new syntax, revision 2

new-syntax-wip-2
James T. Martin 2021-04-05 09:47:10 -07:00
parent e49be205f2
commit 4988bd9118
Signed by: james
GPG Key ID: 4B7F3DA9351E577C
7 changed files with 482 additions and 585 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

45
examples/examples.ivo
View File

@ -1,47 +1,52 @@
#!/usr/bin/env -S ivo -c #!/usr/bin/env -S ivo -c
// Create a list by iterating `f` `n` times: ;; Create a list by iterating `f` `n` times:
let iterate = \f x. iterate = \f x.
{ Z -> [] { Z -> []
; S n -> (x :: iterate f (f x) n) ; S n -> (x :: iterate f (f x) n)
}; };
// Use the iterate function to count to 10: ;; Use the iterate function to count to 10:
let countToTen : [Nat] = countToTen : [Nat];
countToTen =
let countTo = iterate S 1 let countTo = iterate S 1
in countTo 10; in countTo 10;
// Append two lists together: ;; Append two lists together:
let append = \xs ys. append = \xs ys.
{ [] -> ys { [] -> ys
; (x :: xs) -> (x :: append xs ys) ; (x :: xs) -> (x :: append xs ys)
} xs; } xs;
// Reverse a list: ;; Reverse a list:
let reverse = reverse =
{ [] -> [] { [] -> []
; (x :: xs) -> append (reverse xs) [x] ; (x :: xs) -> append (reverse xs) [x]
}; };
// Now we can reverse `"reverse"`: ;; Now we can reverse `"reverse"`:
let reverseReverse : [Char] = reverse "reverse"; reverseReverse : [Char];
reverseReverse = reverse "reverse";
// Calculating `3 + 2` with the help of Church-encoded numerals: ;; Calculating `3 + 2` with the help of Church-encoded numerals:
let threePlusTwo : Nat = threePlusTwo : Nat;
threePlusTwo =
let Sf = \n f x. f (n f x) let Sf = \n f x. f (n f x)
; plus = \x. x Sf ; plus = \x. x Sf
in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z; 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! ;; This expression would loop forever, but `callcc` saves the day!
let callccSaves : Nat = S (callcc \k. undefined (k Z)); callccSaves : Nat;
callccSaves = S (callcc \k. undefined (k Z));
// And if it wasn't clear, this is what the `Char` constructor does: ;; And if it wasn't clear, this is what the `Char` constructor does:
let charB : Char = { Char c -> Char (S c) } 'a; charB : Char;
// (it outputs `'b`) charB = { Char c -> Char (S c) } 'a;
;; (it outputs `'b`)
// pack all of the examples into tuples so the main function can print them ;; pack all of the examples into tuples so the main function can print them
let main = main =
( countToTen ( countToTen
, ( reverseReverse , ( reverseReverse
, ( callccSaves , ( callccSaves

21
src/Ivo/Expression.hs
View File

@ -16,7 +16,7 @@ module Ivo.Expression
) where ) where
import Ivo.Evaluator.Base import Ivo.Evaluator.Base
import Ivo.Syntax.Base import Ivo.Syntax.Base qualified as S
import Ivo.Types.Base import Ivo.Types.Base
import Data.Functor.Foldable (cata, hoist) import Data.Functor.Foldable (cata, hoist)
@ -30,12 +30,12 @@ builtins :: HashMap Text CheckExpr
builtins = HM.fromList [("callcc", CallCCC)] builtins = HM.fromList [("callcc", CallCCC)]
-- | Convert from an abstract syntax tree to a typechecker expression. -- | Convert from an abstract syntax tree to a typechecker expression.
ast2check :: AST -> CheckExpr ast2check :: S.Expr Text -> Either Text CheckExpr
ast2check = substitute builtins . cata \case ast2check = fmap (substitute builtins) . cata \case
VarF name -> Var name VarF name -> Var name
AppF ef exs -> foldl' App ef $ toList exs AppF ef exs -> fmap (foldl' App ef) $ sequenceA $ toList exs
AbsF ns e -> foldr Abs e $ toList ns AbsF ns e -> fmap (foldr Abs e) $ sequenceA $ toList ns
LetF ds e -> LetF scope e ->
let let
letExpr, letPlainExpr, letRecExpr letExpr, letPlainExpr, letRecExpr
:: Text -> CheckExpr -> CheckExpr -> CheckExpr :: Text -> CheckExpr -> CheckExpr -> CheckExpr
@ -47,7 +47,7 @@ ast2check = substitute builtins . cata \case
letExpr name val body' letExpr name val body'
| name `freeIn` val = letRecExpr name val body' | name `freeIn` val = letRecExpr name val body'
| otherwise = letPlainExpr 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 CtrF ctr es -> foldl' App (CtrC ctr) es
CaseF ps -> Case ps CaseF ps -> Case ps
AnnF () e t -> Ann () e t AnnF () e t -> Ann () e t
@ -64,6 +64,9 @@ ast2check = substitute builtins . cata \case
mkList :: [CheckExpr] -> CheckExpr mkList :: [CheckExpr] -> CheckExpr
mkList = foldr (App . App (CtrC CCons)) (CtrC CNil) 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. -- | Convert from declaration abstract syntax to a typechecker expression.
decl2check :: Text -> AST -> CheckExpr decl2check :: Text -> AST -> CheckExpr
decl2check name ast decl2check name ast
@ -111,6 +114,10 @@ check2ast = hoist go . rename (HM.keysSet builtins)
FixFC -> VarF "fix" FixFC -> VarF "fix"
HoleFC -> HoleFP 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. -- | Convert from an evaluator expression to an abstract syntax tree.
eval2ast :: EvalExpr -> AST eval2ast :: EvalExpr -> AST
-- Because all `ast2eval` replaces all free instances of `callcc`, -- Because all `ast2eval` replaces all free instances of `callcc`,

189
src/Ivo/Syntax/Base.hs
View File

@ -1,160 +1,49 @@
module Ivo.Syntax.Base module Ivo.Syntax.Base
( Expr (..), ExprF (..), Ctr (..), Pat, Def, DefF (..), PatF (..), VoidF, Text, NonEmpty (..) ( Scope (..), Def (..)
, Type (..), TypeF (..), Scheme (..), tapp , Expr (..), Type
, substitute, substitute1, rename, rename1, free, freeIn, bound, used , CaseBranches (..), Pattern (..)
, Parse, AST, ASTF, ASTX, ASTXF (..), NonEmptyDefFs (..) , Literal (..)
, pattern LetFP
, pattern PNat, pattern PNatF, pattern PList, pattern PListF, pattern PChar, pattern PCharF
, pattern PStr, pattern PStrF, pattern HoleP, pattern HoleFP
, simplify
) where ) where
import Ivo.Expression.Base import Data.List.NonEmpty (NonEmpty)
import Data.Text (Text)
import Data.Foldable (fold) data Scope name = Scope { getScope :: ![Def name] }
import Data.Functor.Foldable (embed, project, cata) deriving (Eq, Show)
import Data.List.NonEmpty (NonEmpty (..), toList)
import Data.Text qualified as T
data Parse data Def name
-- | The abstract syntax tree reflects the structure of the externally-visible syntax. = BasicDef !name !(Expr name)
-- | BasicDecl !(NonEmpty name) !(Type name)
-- It includes syntactic sugar, which allows multiple ways to express many constructions, deriving (Eq, Show)
-- 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
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 Type name = Expr name
type instance AppArgsF Parse = NonEmpty
type instance LetArgsF Parse = NonEmptyDefFs
type instance CtrArgsF Parse = []
type instance XExprF Parse = ASTXF
data ASTXF r data CaseBranches name = CaseBranches ![(Pattern name, Expr name)]
-- | A natural number literal, e.g. `10`. deriving (Eq, Show)
= 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)
instance RecursivePhase Parse where data Pattern name
projectLetArgs = NonEmptyDefFs = PatVar !name
embedLetArgs = getNonEmptyDefFs | PatLit !(Literal (Pattern name))
| Irrelevant
| PatApp !name [Pattern name]
deriving (Eq, Show)
newtype NonEmptyDefFs r = NonEmptyDefFs { getNonEmptyDefFs :: NonEmpty (Text, r) } data Literal r
deriving (Eq, Functor, Foldable, Traversable, Show) = LitInt Int
| LitChar Char
pattern LetFP :: NonEmpty (Text, r) -> r -> ASTF r | LitStr Text
pattern LetFP ds e = LetF (NonEmptyDefFs ds) e | LitList [r]
deriving (Eq, Show)
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

542
src/Ivo/Syntax/Parser.hs
View File

@ -1,297 +1,279 @@
module Ivo.Syntax.Parser module Ivo.Syntax.Parser
( ParseError, parse ( ParseError, parse
, Declaration, TopLevelAST, ProgramAST , fileParser, scopeParser, defParser, exprParser
, parseAST, parseTopLevel, parseProgram
, typeParser, schemeParser, astParser, topLevelParser, programParser
) where ) where
import Ivo.Syntax.Base import Ivo.Syntax.Base
import Data.Functor.Identity (Identity) import Data.Char (isSeparator)
import Data.List.NonEmpty (fromList) import Data.Functor (void)
import Data.List.NonEmpty (NonEmpty (..), fromList)
import Data.Text (Text)
import Data.Text qualified as T import Data.Text qualified as T
import Prelude hiding (succ, either) import Text.Parsec hiding (spaces, label, sepBy, sepBy1, sepEndBy, sepEndBy1)
import Text.Parsec hiding (label, token, spaces) import Text.Parsec qualified as P
import Text.Parsec qualified import Text.Parsec.Char ()
import Text.Parsec.Expr
import Text.Parsec.Text (Parser) import Text.Parsec.Text (Parser)
spaces :: Parser () fileParser :: Parser (Scope Text)
spaces = Text.Parsec.spaces >> optional (try (comment >> spaces)) fileParser = do
where shebang
comment, lineComment, blockComment :: Parser () scope
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
shebang :: Parser () shebang :: Parser ()
shebang = do shebang = do
try $ keyword "#!" _ <- try $ string "#!"
skipMany (noneOf "\n") skipMany (noneOf "\n")
spaces spaces
programParser :: Parser ProgramAST scopeParser, scope :: Parser (Scope Text)
programParser = shebang *> sepEndBy declaration (token ';') <* eof scopeParser = scope
parseTopLevel :: Text -> Either ParseError TopLevelAST scope = Scope <$> flexBraces def
parseTopLevel = parse topLevelParser "input"
parseProgram :: Text -> Either ParseError ProgramAST defParser, def, basicDef, basicDecl :: Parser (Def Text)
parseProgram = parse programParser "input" 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

208
src/Ivo/Syntax/Printer.hs
View File

@ -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 Ivo.Syntax.Base
import Data.Functor.Base (NonEmptyF (NonEmptyF)) import Data.Foldable (foldl', toList)
import Data.Functor.Foldable (cata) import Data.Text (Text)
import Data.List.NonEmpty (toList)
import Data.Text qualified as T import Data.Text qualified as T
import Data.Text.Lazy (fromStrict, toStrict, intercalate, unwords, singleton) import Data.Text.Lazy (toStrict)
import Data.Text.Lazy.Builder (Builder, fromText, fromLazyText, toLazyText, fromString) import Data.Text.Lazy.Builder (Builder, fromText, toLazyText, fromString)
import Prelude hiding (unwords) import Prelude hiding (unwords)
-- I'm surprised this isn't in base somewhere. unparseScope :: Scope Text -> Text
unsnoc :: NonEmpty a -> ([a], a) unparseScope = unparse scope
unsnoc = cata \case
NonEmptyF x' Nothing -> ([], x')
NonEmptyF x (Just (xs, x')) -> (x : xs, x')
data SyntaxType unparseDef :: Def Text -> Text
-- | Ambiguous syntax is not necessarily finite and not guaranteed to consume any input. unparseDef = unparse def
= 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)
tag :: SyntaxType -> a -> Tagged a unparseExpr :: Expr Text -> Text
tag = (,) unparseExpr = unparse expr
group :: Builder -> Builder scope :: Unparser (Scope Text)
group x = "(" <> x <> ")" scope (Scope defs) = Block $ flexSepEndBy "; " $ map (ambiguous . def) defs
-- | An unambiguous context has a marked beginning and end. def :: Unparser (Def Text)
unambiguous :: Tagged Builder -> Builder def (BasicDef name body) =
unambiguous (_, t) = t 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, expr :: Unparser (Expr Text)
-- so we provide a grouper when a beginning marker is necessary. expr (Var name) = Finite $ fromText name
final :: Tagged Builder -> Builder expr (Lit lit) = Block $ literal expr lit
final (Ambiguous, t) = group t expr (App ef exs) = Ambiguous $ sepBy " " $ map (finite . expr) $ ef : toList exs
final (_, t) = t 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 :: Tagged Builder -> Builder
ambiguous (Finite, t) = t ambiguous = untag
ambiguous (_, t) = group t
-- | Turn an abstract syntax tree into the corresponding concrete syntax. block :: Tagged Builder -> Builder
-- block (Ambiguous x) = parens x
-- This is *not* a pretty-printer; it uses minimal whitespace. block x = untag x
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)
unparseDef (name, val) = fromText name <> " = " <> unambiguous val finite :: Tagged Builder -> Builder
unparseDefs defs = fromLazyText (intercalate "; " $ map (toLazyText . unparseDef) $ toList defs) finite (Finite x) = x
finite x = parens $ untag x
unparseCtr :: Ctr -> [Tagged Builder] -> Tagged Builder parens :: Builder -> Builder
-- Fully-applied special syntax forms parens = between "(" ")"
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)
unparsePat (Pat ctr ns e) unparse :: Unparser a -> a -> Text
= unambiguous (unparseCtr ctr (map (tag Finite . fromText) ns)) <> " -> " <> unambiguous e unparse up = toStrict . toLazyText . untag . up
-- 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

3
src/Ivo/Types.hs
View File

@ -79,8 +79,9 @@ j (Abs n_arg e_ret) = do
t_arg <- fresh t_arg <- fresh
t_ret <- bindVar n_arg t_arg $ j e_ret t_ret <- bindVar n_arg t_arg $ j e_ret
pure $ tapp [TAbs, t_arg, t_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 (t_x_mono, c) <- listen $ j e_x
mapM_ (unify t_x_mono) t_ann_x
s <- solve' c s <- solve' c
t_x_poly <- generalize $ substitute s t_x_mono t_x_poly <- generalize $ substitute s t_x_mono
local (HM.insert n_x t_x_poly) $ j e_ret local (HM.insert n_x t_x_poly) $ j e_ret

59
src/Ivo/Types/Base.hs
View File

@ -3,8 +3,9 @@ module Ivo.Types.Base
, Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text , Expr (..), Ctr (..), Pat, ExprF (..), PatF (..), VoidF, UnitF (..), Text
, Type (..), TypeF (..), Scheme (..), tapp , Type (..), TypeF (..), Scheme (..), tapp
, substitute, substitute1, rename, rename1, free, bound, used , substitute, substitute1, rename, rename1, free, bound, used
, Check, CheckExpr, CheckExprF, CheckX, CheckXF (..) , Check, CheckExpr, CheckExprF, CheckLet, CheckLetF (..), CheckX, CheckXF (..)
, pattern AppFC, pattern CtrC, pattern CtrFC, pattern CallCCC, pattern CallCCFC , pattern AppFC, pattern LetC, pattern LetFC
, pattern CtrC, pattern CtrFC, pattern CallCCC, pattern CallCCFC
, pattern FixC, pattern FixFC, pattern HoleC, pattern HoleFC , pattern FixC, pattern FixFC, pattern HoleC, pattern HoleFC
, Substitution, Context, Constraint , Substitution, Context, Constraint
, MonoSubstitutable, substituteMono, substituteMono1 , MonoSubstitutable, substituteMono, substituteMono1
@ -26,19 +27,23 @@ data Check
type CheckExpr = Expr Check type CheckExpr = Expr Check
type instance AppArgs Check = CheckExpr type instance AppArgs Check = CheckExpr
type instance AbsArgs Check = Text type instance AbsArgs Check = Text
type instance LetArgs Check = (Text, CheckExpr) type instance LetArgs Check = CheckLet
type instance CtrArgs Check = UnitF CheckExpr type instance CtrArgs Check = UnitF CheckExpr
type instance AnnX Check = () type instance AnnX Check = ()
type instance XExpr Check = CheckX type instance XExpr Check = CheckX
type CheckLet = CheckLetF CheckExpr
type CheckX = CheckXF CheckExpr type CheckX = CheckXF CheckExpr
type CheckExprF = ExprF Check type CheckExprF = ExprF Check
type instance AppArgsF Check = Identity type instance AppArgsF Check = Identity
type instance LetArgsF Check = DefF type instance LetArgsF Check = CheckLetF
type instance CtrArgsF Check = UnitF type instance CtrArgsF Check = UnitF
type instance XExprF Check = CheckXF type instance XExprF Check = CheckXF
data CheckLetF r = CheckLet Text (Maybe Type) r
deriving (Eq, Functor, Foldable, Traversable, Show)
data CheckXF r data CheckXF r
-- | Call-with-current-continuation. -- | Call-with-current-continuation.
= CallCCC_ = CallCCC_
@ -49,6 +54,12 @@ data CheckXF r
| HoleC_ | HoleC_
deriving (Eq, Functor, Foldable, Traversable, Show) 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 :: Ctr -> CheckExpr
pattern CtrC c = Ctr c Unit pattern CtrC c = Ctr c Unit
@ -76,38 +87,44 @@ pattern HoleC = ExprX HoleC_
pattern HoleFC :: CheckExprF r pattern HoleFC :: CheckExprF r
pattern HoleFC = ExprXF HoleC_ pattern HoleFC = ExprXF HoleC_
{-# COMPLETE Var, App, Abs, Let, CtrC, Case, Ann, ExprX #-} {-# COMPLETE Var, App, Abs, Let, CtrC, Case, Ann, ExprX #-}
{-# COMPLETE VarF, AppF, AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF #-} {-# COMPLETE VarF, AppF, AbsF, LetF, CtrFC, CaseF, AnnF, ExprXF #-}
{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF, CaseF, AnnF, ExprXF #-} {-# COMPLETE VarF, AppFC, AbsF, LetF, CtrF, CaseF, AnnF, ExprXF #-}
{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, 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, Ctr, Case, Ann, CallCCC, FixC, HoleC #-}
{-# COMPLETE Var, App, Abs, Let, CtrC, 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, 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, CtrF, CaseF, AnnF, CallCCFC, FixFC, HoleFC #-}
{-# COMPLETE VarF, AppFC, AbsF, LetF, CtrFC, 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 instance RecursivePhase Check where
projectAppArgs = Identity projectAppArgs = Identity
projectLetArgs = projectDef
embedAppArgs = runIdentity embedAppArgs = runIdentity
embedLetArgs = embedDef
instance Substitutable CheckExpr where instance Substitutable CheckExpr where
collectVars withVar withBinder = cata \case collectVars withVar withBinder = cata \case
VarF n -> withVar n VarF n -> withVar n
AbsF n e -> withBinder n e 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 CaseF pats -> foldMap (\(Pat _ ns e) -> foldr withBinder e ns) pats
e -> fold e e -> fold e
rename = runRenamer $ \badNames -> cata \case rename = runRenamer $ \badNames -> cata \case
VarF n -> asks $ Var . HM.findWithDefault n n VarF n -> asks $ Var . HM.findWithDefault n n
AbsF n e -> uncurry Abs . first runIdentity <$> replaceNames badNames (Identity n) e 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 x' <- x
(Identity n', e') <- replaceNames badNames (Identity n) e (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) -> CaseF ps -> Case <$> forM ps \(Pat ctr ns e) ->
uncurry (Pat ctr) <$> replaceNames badNames ns e uncurry (Pat ctr) <$> replaceNames badNames ns e
e -> embed <$> sequenceA e e -> embed <$> sequenceA e
@ -115,10 +132,10 @@ instance Substitutable CheckExpr where
unsafeSubstitute = runSubstituter $ para \case unsafeSubstitute = runSubstituter $ para \case
VarF name -> asks $ HM.findWithDefault (Var name) name VarF name -> asks $ HM.findWithDefault (Var name) name
AbsF name e -> Abs name <$> maySubstitute (Identity name) e AbsF name e -> Abs name <$> maySubstitute (Identity name) e
LetF (Def name (_, x)) e -> do LetFC name ty (_, x) e -> do
x' <- x x' <- x
e' <- maySubstitute (Identity name) e 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 CaseF pats -> Case <$> for pats \(Pat ctr ns e) -> Pat ctr ns <$> maySubstitute ns e
e -> embed <$> traverse snd e e -> embed <$> traverse snd e