Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix typecheckString behaviour #115

Merged
merged 1 commit into from Oct 1, 2023
Merged

Fix typecheckString behaviour #115

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
2 changes: 1 addition & 1 deletion rzk/src/Rzk/Main.hs
View file
Open in desktop
Expand Up @@ -89,7 +89,7 @@ parseRzkFilesOrStdin = \case
typecheckString :: String -> Either String String
typecheckString moduleString = do
rzkModule <- Rzk.parseModule moduleString
case defaultTypeCheck (typecheckModule Nothing rzkModule) of
case defaultTypeCheck (typecheckModules [rzkModule]) of
Left err -> Left $ unlines
[ "An error occurred when typechecking!"
, "Rendering type error... (this may take a few seconds)"
Expand Down
33 changes: 21 additions & 12 deletions rzk/src/Rzk/TypeCheck.hs
View file
Open in desktop
Expand Up @@ -88,12 +88,12 @@ typecheckModules = \case
[] -> return []
m : ms -> do
(decls, errs) <- typecheckModule Nothing m
if null errs
then
case errs of
err : _ -> do
throwError err
_ -> do
localDeclsPrepared decls $
(decls <>) <$> typecheckModules ms
else
return decls

typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
typecheckModuleWithLocation (path, module_) = do
Expand Down Expand Up @@ -1938,14 +1938,23 @@ unifyInCurrentContext mterm expected actual = performing action $
switchVariance $ -- unifying in the negative position!
unifyTerms cube cube' -- FIXME: unifyCubes
enterScope orig' cube $ do
case (mtope, mtope') of
(Just tope, Just tope') -> do
topeNF <- nfT tope
topeNF' <- nfT tope'
unifyTopes topeNF topeNF'
(Nothing, Nothing) -> return ()
(Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)
(Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT
case ret' of
-- UniverseTopeT{} ->
-- (Just tope, Just tope') -> do
-- topeNF <- nfT tope
-- topeNF' <- nfT tope'
-- unifyTopes topeNF topeNF'
-- (Nothing, Nothing) -> return ()
-- (Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)
-- (Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT
_ -> case (mtope, mtope') of
(Just tope, Just tope') -> do
topeNF <- nfT tope
topeNF' <- nfT tope'
unifyTopes topeNF topeNF'
(Nothing, Nothing) -> return ()
(Just tope, Nothing) -> nfT tope >>= (`unifyTopes` topeTopT)
(Nothing, Just tope) -> nfT tope >>= unifyTopes topeTopT
case mterm of
Nothing -> unifyTerms ret ret'
Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'
Expand Down