wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

minor cleanup

Browse source
This commit is contained in:
William Ball 2024-12-08 21:57:17 -08:00
parent 95a4d822b6
commit d15b53da1e
1 changed files with 3 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
lib/Parser.hs
View file

@ -42,10 +42,8 @@ keywords = ["forall", "let", "in", "end", "fun", "def", "axiom", "section", "var
pIdentifier :: Parser Text
pIdentifier = try $ label "identifier" $ lexeme $ do
firstChar <- letterChar <|> char '_'
rest <- many $ alphaNumChar <|> char '_'
let ident = T.pack (firstChar : rest)
guard (ident `notElem` keywords)
ident <- T.pack <$> ((:) <$> (letterChar <|> char '_') <*> many (alphaNumChar <|> char '_'))
guard $ ident `notElem` keywords
pure ident
pVar :: Parser IRExpr
@ -154,9 +152,7 @@ pAppTerm = lexeme $ choice [pLAbs, pPAbs, pLet, pApp]
pIRExpr :: Parser IRExpr
pIRExpr = lexeme $ do
e <- pAppTerm
option e $ do
_ <- symbol "->" <|> symbol "→"
Pi "" e Nothing <$> pIRExpr
option e $ (symbol "->" <|> symbol "→") >> Pi "" e Nothing <$> pIRExpr
pAscription :: Parser IRExpr
pAscription = lexeme $ try $ symbol ":" >> label "type" pIRExpr