Fakultas Ilmu Komputer UI

Commit 3e8c332e authored by Sean Gillespie's avatar Sean Gillespie
Browse files

Update System F parser

 * Add type abstraction `\X. body`
 * enforce case for variable names
   * Types begin with a capital
   * Variables begin with a lower
parent 3aca5ff7
......@@ -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')
......@@ -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"
......
......@@ -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")))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment