Skip to content

Commit

Permalink
TCO WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
VictorTaelin committed Oct 25, 2024
1 parent 144f2dd commit 427d638
Show file tree
Hide file tree
Showing 5 changed files with 472 additions and 189 deletions.
3 changes: 3 additions & 0 deletions src/Kind/API.hs
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,9 @@ import Debug.Trace
type FileCtx = (Book, M.Map FilePath [String], M.Map FilePath [String])
type Command = String -> FileCtx -> String -> String -> IO (Either String ())

-- main :: IO ()
-- main = ctest

main :: IO ()
main = do
args <- getArgs
Expand Down
2 changes: 1 addition & 1 deletion src/Kind/Check.hs
Original file line number Diff line number Diff line change
Expand Up @@ -384,7 +384,7 @@ checkUnreachable src cNam term dep = go src cNam term dep where
go src cNam (Use nam val bod) dep = go src cNam (bod (Con "void" [])) (dep+1)
go _ cNam (Src src val) dep = go (Just src) cNam val dep
go src cNam (Hol nam ctx) dep = envLog (Found nam (Hol "unreachable" []) ctx dep) >> go src cNam Set dep
go src cNam term dep = return (cNam, Ann False (Num 0) U64)
go src cNam term dep = return (cNam, Ann False Set U64)

checkLater :: Bool -> Maybe Cod -> Term -> Term -> Int -> Env Term
checkLater False src term typx dep = check False src term typx dep
Expand Down
Loading

0 comments on commit 427d638

Please sign in to comment.