Skip to content

Commit

Permalink
small parsing adjustments
Browse files Browse the repository at this point in the history
  • Loading branch information
VictorTaelin committed Oct 19, 2024
1 parent 90405be commit e9b0ccc
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 10 deletions.
2 changes: 1 addition & 1 deletion src/Kind/API.hs
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ apiLoad basePath book name = do

-- Normalizes a term
apiNormal :: Book -> String -> IO (Either String ())
apiNormal book name = case M.lookup name book of
apiNormal book name = case M.lookup (name ++ "/main") book of
Just term -> do
result <- infoShow book IM.empty (Print (normal book IM.empty 2 term 0) 0)
putStrLn result
Expand Down
24 changes: 15 additions & 9 deletions src/Kind/Parse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -218,7 +218,7 @@ parseIns = withSrc $ do
return $ Ins val

parseDat = withSrc $ do
P.try $ string "#["
P.try $ P.choice [string "#[", string "data["]
scp <- P.many parseTerm
char ']'
char '{'
Expand All @@ -232,13 +232,15 @@ parseDat = withSrc $ do

parseTele :: Parser Tele
parseTele = do
char '{'
fields <- P.many $ P.try $ do
nam <- parseName
char ':'
typ <- parseTerm
return (nam, typ)
char '}'
fields <- P.option [] $ do
char '{'
fields <- P.many $ P.try $ do
nam <- parseName
char ':'
typ <- parseTerm
return (nam, typ)
char '}'
return fields
char ':'
ret <- parseTerm
return $ foldr (\(nam, typ) acc -> TExt nam typ (\x -> acc)) (TRet ret) fields
Expand All @@ -261,7 +263,11 @@ parseCon = withSrc $ do
return $ Con nam args

parseSwi = withSrc $ do
P.try $ string "λ{0:"
P.try $ do
string "λ"
string "{"
string "0"
string ":"
zero <- parseTerm
string "_:"
succ <- parseTerm
Expand Down

0 comments on commit e9b0ccc

Please sign in to comment.