From 3e8c332e2b0dbeaac7aeeff54e2d35fe1db6a07a Mon Sep 17 00:00:00 2001
From: Sean Gillespie <sean@mistersg.net>
Date: Fri, 30 Dec 2016 22:25:07 -0500
Subject: [PATCH] Update System F parser
* Add type abstraction `\X. body`
* enforce case for variable names
* Types begin with a capital
* Variables begin with a lower
---
src/Language/SystemF/Expression.hs | 6 +++---
src/Language/SystemF/Parser.hs | 26 +++++++++++++++++++-------
test/Language/SystemF/ParserSpec.hs | 3 +++
3 files changed, 25 insertions(+), 10 deletions(-)
diff --git a/src/Language/SystemF/Expression.hs b/src/Language/SystemF/Expression.hs
index 437f0e2..ece7e15 100644
--- a/src/Language/SystemF/Expression.hs
+++ b/src/Language/SystemF/Expression.hs
@@ -9,7 +9,7 @@ data SystemFExpr name ty
= Var name -- Variable
| App (SystemFExpr name ty) (SystemFExpr name ty) -- Application
| Abs name (Ty ty) (SystemFExpr name ty) -- Abstraction
- | TyAbs (Ty ty) (SystemFExpr name ty) -- Type Abstraction
+ | TyAbs ty (SystemFExpr name ty) -- Type Abstraction
-- \X. body
| TyApp (SystemFExpr name ty) (Ty ty) -- Type Application
@@ -117,7 +117,7 @@ pprTyArrow' space a b = a <> arrow <> b
-- Pretty print a type abstraction
pprTAbs :: (PrettyPrint n, PrettyPrint t)
=> PDoc String
- -> Ty t
+ -> t
-> SystemFExpr n t
-> PDoc String
pprTAbs pdoc ty body = between vars' lambda' ". " (pprExpr pdoc body')
@@ -130,7 +130,7 @@ uncurryAbs name ty = uncurry' [(name, ty)]
where uncurry' ns (Abs n' t' body') = uncurry' ((n', t'):ns) body'
uncurry' ns body' = (reverse ns, body')
-uncurryTAbs :: Ty t -> SystemFExpr n t -> ([Ty t], SystemFExpr n t)
+uncurryTAbs :: t -> SystemFExpr n t -> ([t], SystemFExpr n t)
uncurryTAbs ty = uncurry' [ty]
where uncurry' ts (TyAbs t' body') = uncurry' (t':ts) body'
uncurry' ts body' = (reverse ts, body')
diff --git a/src/Language/SystemF/Parser.hs b/src/Language/SystemF/Parser.hs
index fbcb40a..8a1709f 100644
--- a/src/Language/SystemF/Parser.hs
+++ b/src/Language/SystemF/Parser.hs
@@ -25,18 +25,26 @@ app :: Parser (SystemFExpr String String)
app = chainl1 term (return App)
term :: Parser (SystemFExpr String String)
-term = abs <|> var <|> parens expr
+term = try abs
+ <|> tyabs
+ <|> var
+ <|> parens expr
var :: Parser (SystemFExpr String String)
-var = Var <$> identifier
+var = Var <$> exprId
abs :: Parser (SystemFExpr String String)
abs = curry
<$> (symbol '\\' *> many1 args <* symbol '.')
<*> expr
- where args = (,) <$> (identifier <* symbol ':') <*> ty
+ where args = (,) <$> (exprId <* symbol ':') <*> ty
curry = flip . foldr . uncurry $ Abs
+tyabs :: Parser (SystemFExpr String String)
+tyabs = curry <$> args <*> expr
+ where args = symbol '\\' *> many1 typeId <* symbol '.'
+ curry = flip (foldr TyAbs)
+
-- Parse type expressions
ty :: Parser (Ty String)
ty = try arrow
@@ -48,16 +56,20 @@ tyterm :: Parser (Ty String)
tyterm = tyvar <|> parens ty
tyvar :: Parser (Ty String)
-tyvar = TyVar <$> identifier
+tyvar = TyVar <$> typeId
parens :: Parser a -> Parser a
parens p = symbol '(' *> p <* symbol ')'
-identifier :: Parser String
-identifier = lexeme ((:) <$> first <*> many rest)
- where first = letter <|> char '_'
+identifier :: Parser Char -> Parser String
+identifier firstChar = lexeme ((:) <$> first <*> many rest)
+ where first = firstChar <|> char '_'
rest = first <|> digit
+typeId, exprId :: Parser String
+typeId = identifier upper
+exprId = identifier lower
+
whitespace :: Parser ()
whitespace = void . many . oneOf $ " \t"
diff --git a/test/Language/SystemF/ParserSpec.hs b/test/Language/SystemF/ParserSpec.hs
index 57160fd..1bcfb04 100644
--- a/test/Language/SystemF/ParserSpec.hs
+++ b/test/Language/SystemF/ParserSpec.hs
@@ -19,6 +19,9 @@ spec = do
it "parses simple abstractions" $
parseExpr "\\x:T. x" `shouldBe` Right (Abs "x" (TyVar "T") (Var "x"))
+ it "parses simple type abstractions" $
+ parseExpr "\\X. x" `shouldBe` Right (TyAbs "X" (Var "x"))
+
it "parses nested abstractions" $
parseExpr "\\a:A b:B. b"
`shouldBe` Right (Abs "a" (TyVar "A") (Abs "b" (TyVar "B") (Var "b")))
--
GitLab