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 00f326a
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 14 deletions.
4 changes: 2 additions & 2 deletions src/Kind/API.hs
Original file line number Diff line number Diff line change
Expand Up @@ -74,12 +74,12 @@ 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 "main" book of
Just term -> do
result <- infoShow book IM.empty (Print (normal book IM.empty 2 term 0) 0)
putStrLn result
return $ Right ()
Nothing -> return $ Left $ "Error: Definition '" ++ name ++ "' not found."
Nothing -> return $ Left $ "Error: Definition 'main' not found."

-- Type-checks all terms in a file
apiCheckFile :: Book -> M.Map FilePath [String] -> FilePath -> IO (Either String ())
Expand Down
32 changes: 20 additions & 12 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 Expand Up @@ -508,9 +514,11 @@ parsePattern = do
do
char '#'
name <- parseName
char '{'
args <- P.many parsePattern
char '}'
args <- P.option [] $ P.try $ do
char '{'
args <- P.many parsePattern
char '}'
return args
return (PCtr name args)
]

Expand Down

0 comments on commit 00f326a

Please sign in to comment.