diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -6,6 +6,15 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.6.2 — 2023-09-26 + +This version contains some improvements in efficiency and also to the language server: + +- Improve efficiency of the tope solver, applying LEM for directed interval only as a fallback option (see [#102](https://github.com/rzk-lang/rzk/pull/102)) +- Support autocompleting definitions from previous modules (see [#102](https://github.com/rzk-lang/rzk/pull/103)) + - Well-typed definitions from the same module also work if the module is only partially well-typed! +- Improve information order in the error messages given in LSP diagnostics (see [#104](https://github.com/rzk-lang/rzk/pull/104)) + ## v0.6.1 — 2023-09-24 This version contains a minor fix: diff --git a/rzk.cabal b/rzk.cabal --- a/rzk.cabal +++ b/rzk.cabal @@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: rzk -version: 0.6.1 +version: 0.6.2 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types @@ -54,6 +54,7 @@ , base >=4.7 && <5 , bifunctors , bytestring + , data-default-class , filepath , lens , mtl @@ -91,6 +92,7 @@ , base >=4.7 && <5 , bifunctors , bytestring + , data-default-class , filepath , lens , mtl @@ -122,6 +124,7 @@ , base , bifunctors , bytestring + , data-default-class , doctest , filepath , lens @@ -151,6 +154,7 @@ , base >=4.7 && <5 , bifunctors , bytestring + , data-default-class , filepath , lens , mtl diff --git a/src/Language/Rzk/Syntax/Print.hs b/src/Language/Rzk/Syntax/Print.hs --- a/src/Language/Rzk/Syntax/Print.hs +++ b/src/Language/Rzk/Syntax/Print.hs @@ -1,8 +1,8 @@ -- File generated by the BNF Converter (bnfc 2.9.4.1). -{-# LANGUAGE CPP #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE LambdaCase #-} #if __GLASGOW_HASKELL__ <= 708 {-# LANGUAGE OverlappingInstances #-} #endif @@ -11,16 +11,13 @@ module Language.Rzk.Syntax.Print where -import Prelude - ( ($), (.) - , Bool(..), (==), (<) - , Int, Integer, Double, (+), (-), (*) - , String, (++) - , ShowS, showChar, showString - , all, elem, foldr, id, map, null, replicate, shows, span - ) -import Data.Char ( Char, isSpace ) +import Data.Char (Char, isSpace) import qualified Language.Rzk.Syntax.Abs +import Prelude (Bool (..), Double, Int, Integer, + ShowS, String, all, elem, foldr, id, + map, null, replicate, showChar, + showString, shows, span, ($), (*), + (++), (.), (<), (==)) -- | The top-level printing method. @@ -43,9 +40,9 @@ rend i p = \case "[" :ts -> char '[' . rend i False ts "(" :ts -> char '(' . rend i False ts - "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts - "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts - "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts + -- "{" :ts -> onNewLine i p . showChar '{' . new (i+1) ts + -- "}" : ";":ts -> onNewLine (i-1) p . showString "};" . new (i-1) ts + -- "}" :ts -> onNewLine (i-1) p . showChar '}' . new (i-1) ts [";"] -> char ';' ";" :ts -> char ';' . new i ts t : ts@(s:_) | closingOrPunctuation s @@ -70,8 +67,8 @@ new j ts = showChar '\n' . rend j True ts -- Make sure we are on a fresh line. - onNewLine :: Int -> Bool -> ShowS - onNewLine i p = (if p then id else showChar '\n') . indent i + -- onNewLine :: Int -> Bool -> ShowS + -- onNewLine i p = (if p then id else showChar '\n') . indent i -- Separate given string from following text by a space (if needed). space :: String -> ShowS @@ -124,10 +121,10 @@ mkEsc :: Char -> Char -> ShowS mkEsc q = \case s | s == q -> showChar '\\' . showChar s - '\\' -> showString "\\\\" - '\n' -> showString "\\n" - '\t' -> showString "\\t" - s -> showChar s + '\\' -> showString "\\\\" + '\n' -> showString "\\n" + '\t' -> showString "\\t" + s -> showChar s prPrec :: Int -> Int -> Doc -> Doc prPrec i j = if j < i then parenth else id @@ -155,8 +152,8 @@ Language.Rzk.Syntax.Abs.VarIdent _ varidenttoken -> prPrec i 0 (concatD [prt 0 varidenttoken]) instance Print [Language.Rzk.Syntax.Abs.VarIdent' a] where - prt _ [] = concatD [] - prt _ [x] = concatD [prt 0 x] + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.LanguageDecl' a) where @@ -182,7 +179,7 @@ Language.Rzk.Syntax.Abs.CommandDefine _ varident declusedvars params term1 term2 -> prPrec i 0 (concatD [doc (showString "#define"), prt 0 varident, prt 0 declusedvars, prt 0 params, doc (showString ":"), prt 0 term1, doc (showString ":="), prt 0 term2]) instance Print [Language.Rzk.Syntax.Abs.Command' a] where - prt _ [] = concatD [] + prt _ [] = concatD [] prt _ (x:xs) = concatD [prt 0 x, doc (showString ";"), prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.DeclUsedVars' a) where @@ -201,8 +198,8 @@ Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")]) instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where - prt _ [] = concatD [] - prt _ [x] = concatD [prt 0 x] + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.Param' a) where @@ -213,8 +210,8 @@ Language.Rzk.Syntax.Abs.ParamPatternShapeDeprecated _ pattern_ term1 term2 -> prPrec i 0 (concatD [doc (showString "{"), prt 0 pattern_, doc (showString ":"), prt 0 term1, doc (showString "|"), prt 0 term2, doc (showString "}")]) instance Print [Language.Rzk.Syntax.Abs.Param' a] where - prt _ [] = concatD [] - prt _ [x] = concatD [prt 0 x] + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.ParamDecl' a) where @@ -231,8 +228,8 @@ Language.Rzk.Syntax.Abs.ASCII_Restriction _ term1 term2 -> prPrec i 0 (concatD [prt 0 term1, doc (showString "|->"), prt 0 term2]) instance Print [Language.Rzk.Syntax.Abs.Restriction' a] where - prt _ [] = concatD [] - prt _ [x] = concatD [prt 0 x] + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] instance Print (Language.Rzk.Syntax.Abs.Term' a) where @@ -292,6 +289,6 @@ Language.Rzk.Syntax.Abs.ASCII_Second _ term -> prPrec i 6 (concatD [doc (showString "second"), prt 7 term]) instance Print [Language.Rzk.Syntax.Abs.Term' a] where - prt _ [] = concatD [] - prt _ [x] = concatD [prt 0 x] + prt _ [] = concatD [] + prt _ [x] = concatD [prt 0 x] prt _ (x:xs) = concatD [prt 0 x, doc (showString ","), prt 0 xs] diff --git a/src/Language/Rzk/VSCode/Handlers.hs b/src/Language/Rzk/VSCode/Handlers.hs --- a/src/Language/Rzk/VSCode/Handlers.hs +++ b/src/Language/Rzk/VSCode/Handlers.hs @@ -1,24 +1,36 @@ +{-# LANGUAGE DataKinds #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Language.Rzk.VSCode.Handlers where import Control.Exception (SomeException, evaluate, try) +import Control.Lens import Control.Monad.Cont (MonadIO (liftIO), forM_) +import Data.Default.Class import Data.List (sort, (\\)) +import Data.Maybe (fromMaybe) import qualified Data.Text as T import qualified Data.Yaml as Yaml import Language.LSP.Diagnostics (partitionBySource) +import Language.LSP.Protocol.Lens (HasDetail (detail), + HasDocumentation (documentation), + HasLabel (label), + HasParams (params), + HasTextDocument (textDocument), + HasUri (uri)) import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types import Language.LSP.Server -import System.FilePath (()) +import System.FilePath (makeRelative, ()) import System.FilePath.Glob (compile, globDir) -import Data.Maybe (fromMaybe) -import Language.Rzk.Free.Syntax (VarIdent) -import Language.Rzk.Syntax (Module, parseModuleFile) +import Language.Rzk.Free.Syntax (RzkPosition (RzkPosition), + VarIdent (getVarIdent)) +import Language.Rzk.Syntax (Module, VarIdent' (VarIdent), + parseModuleFile, printTree) import Language.Rzk.VSCode.Env import Language.Rzk.VSCode.State (ProjectConfig (include)) import Rzk.TypeCheck @@ -121,7 +133,7 @@ (Just []) -- related information Nothing -- data that is preserved between different calls where - msg = ppTypeErrorInScopedContext' err + msg = ppTypeErrorInScopedContext' TopDown err extractLineNumber :: TypeErrorInScopedContext var -> Maybe Int extractLineNumber (PlainTypeError e) = do @@ -142,3 +154,40 @@ Nothing (Just []) Nothing + +instance Default T.Text where def = "" +instance Default CompletionItem +instance Default CompletionItemLabelDetails + +provideCompletions :: Handler LSP 'Method_TextDocumentCompletion +provideCompletions req res = do + root <- getRootPath + let rootDir = fromMaybe "/" root + cachedModules <- getCachedTypecheckedModules + let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri + -- Take all the modules up to and including the currently open one + let modules = takeWhileInc ((/= currentFile) . fst) cachedModules + where + takeWhileInc _ [] = [] + takeWhileInc p (x:xs) + | p x = x : takeWhileInc p xs + | otherwise = [x] + + let items = concatMap (declsToItems rootDir) modules + res $ Right $ InL items + where + declsToItems :: FilePath -> (FilePath, [Decl']) -> [CompletionItem] + declsToItems root (path, decls) = map (declToItem root path) decls + declToItem :: FilePath -> FilePath -> Decl' -> CompletionItem + declToItem rootDir path (Decl name type' _ _ _) = def + & label .~ T.pack (printTree $ getVarIdent name) + & detail ?~ T.pack (show type') + & documentation ?~ InR (MarkupContent MarkupKind_Markdown $ T.pack $ + "---\nDefined" ++ + (if line > 0 then " at line " ++ show line else "") + ++ " in *" ++ makeRelative rootDir path ++ "*") + where + (VarIdent pos _) = getVarIdent name + (RzkPosition _path pos') = pos + line = maybe 0 fst pos' + _col = maybe 0 snd pos' diff --git a/src/Language/Rzk/VSCode/Lsp.hs b/src/Language/Rzk/VSCode/Lsp.hs --- a/src/Language/Rzk/VSCode/Lsp.hs +++ b/src/Language/Rzk/VSCode/Lsp.hs @@ -58,6 +58,7 @@ -- ms = mkMarkdown "Hello world" -- range' = Range pos pos -- responder (Right $ InL rsp) + , requestHandler SMethod_TextDocumentCompletion provideCompletions , requestHandler SMethod_TextDocumentSemanticTokensFull $ \req responder -> do let doc = req ^. params . textDocument . uri . to toNormalizedUri mdoc <- getVirtualFile doc diff --git a/src/Rzk/Main.hs b/src/Rzk/Main.hs --- a/src/Rzk/Main.hs +++ b/src/Rzk/Main.hs @@ -35,7 +35,7 @@ putStrLn "An error occurred when typechecking!" putStrLn $ unlines [ "Type Error:" - , ppTypeErrorInScopedContext' err + , ppTypeErrorInScopedContext' BottomUp err ] exitFailure Right _declsByPath -> putStrLn "Everything is ok!" @@ -93,7 +93,7 @@ , "Rendering type error... (this may take a few seconds)" , unlines [ "Type Error:" - , ppTypeErrorInScopedContext' err + , ppTypeErrorInScopedContext' BottomUp err ] ] Right _ -> pure "Everything is ok!" diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs --- a/src/Rzk/TypeCheck.hs +++ b/src/Rzk/TypeCheck.hs @@ -12,6 +12,7 @@ import Control.Applicative ((<|>)) import Control.Monad.Except import Control.Monad.Reader +import Data.Bifunctor (first) import Data.List (intercalate, intersect, nub, tails, (\\)) import Data.Maybe (catMaybes, fromMaybe, isNothing, @@ -63,10 +64,10 @@ typecheckModulesWithLocation' = \case [] -> return ([], []) m@(path, _) : ms -> do - declsE <- (Right <$> typecheckModuleWithLocation m) `catchError` (return . Left) - case declsE of - Left err -> return ([], [err]) - Right decls -> do + (decls, errs) <- typecheckModuleWithLocation m + case errs of + _:_ -> return ([(path, decls)], errs) + _ -> do localDeclsPrepared decls $ do (decls', errors) <- typecheckModulesWithLocation' ms return ((path, decls) : decls', errors) @@ -75,19 +76,27 @@ typecheckModulesWithLocation = \case [] -> return [] m@(path, _) : ms -> do - decls <- typecheckModuleWithLocation m - localDeclsPrepared decls $ - ((path, decls) :) <$> typecheckModulesWithLocation ms + (decls, errs) <- typecheckModuleWithLocation m + if null errs + then + localDeclsPrepared decls $ + ((path, decls) :) <$> typecheckModulesWithLocation ms + else + return [(path, decls)] typecheckModules :: [Rzk.Module] -> TypeCheck VarIdent [Decl'] typecheckModules = \case [] -> return [] m : ms -> do - decls <- typecheckModule Nothing m - localDeclsPrepared decls $ - (decls <>) <$> typecheckModules ms + (decls, errs) <- typecheckModule Nothing m + if null errs + then + localDeclsPrepared decls $ + (decls <>) <$> typecheckModules ms + else + return decls -typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent [Decl'] +typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) typecheckModuleWithLocation (path, module_) = do traceTypeCheck Normal ("Checking module from " <> path) $ do withLocation (LocationInfo { locationFilePath = Just path, locationLine = Nothing }) $ @@ -96,15 +105,15 @@ countCommands :: Integral a => [Rzk.Command] -> a countCommands = fromIntegral . length -typecheckModule :: Maybe FilePath -> Rzk.Module -> TypeCheck VarIdent [Decl'] +typecheckModule :: Maybe FilePath -> Rzk.Module -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) typecheckModule path (Rzk.Module _moduleLoc _lang commands) = withSection Nothing (go 1 commands) $ -- FIXME: use module name? or anonymous section? - return [] + return ([], []) where totalCommands = countCommands commands - go :: Integer -> [Rzk.Command] -> TypeCheck VarIdent [Decl'] - go _i [] = return [] + go :: Integer -> [Rzk.Command] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) + go _i [] = return ([], []) go i (command@(Rzk.CommandUnsetOption _loc optionName) : moreCommands) = do traceTypeCheck Normal ("[ " <> show i <> " out of " <> show totalCommands <> " ]" @@ -129,7 +138,7 @@ ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT let decl = Decl (varIdentAt path name) ty' (Just term') False (varIdentAt path <$> vars) - fmap (decl :) $ + fmap (first (decl :)) $ localDeclPrepared decl $ do Context{..} <- ask termSVG <- @@ -148,7 +157,7 @@ paramDecls <- concat <$> mapM paramToParamDecl params ty' <- typecheck (toTerm' (addParamDecls paramDecls ty)) universeT >>= whnfT let decl = Decl (varIdentAt path name) ty' Nothing False (varIdentAt path <$> vars) - fmap (decl :) $ + fmap (first (decl :)) $ localDeclPrepared decl $ go (i + 1) moreCommands @@ -185,7 +194,7 @@ withCommand command $ do ty' <- typecheck (toTerm' ty) universeT let decls = [ Decl (varIdentAt path name) ty' Nothing True [] | name <- names ] - fmap (decls <>) $ + fmap (first (decls <>)) $ localDeclsPrepared decls $ go (i + 1) moreCommands @@ -404,21 +413,22 @@ , " " <> Rzk.printTree (getVarIdent name) ] -ppTypeErrorInContext :: TypeErrorInContext VarIdent -> String -ppTypeErrorInContext TypeErrorInContext{..} = intercalate "\n" - [ ppContext' typeErrorContext - , ppTypeError' typeErrorError +ppTypeErrorInContext :: OutputDirection -> TypeErrorInContext VarIdent -> String +ppTypeErrorInContext dir TypeErrorInContext{..} = block dir + [ ppTypeError' typeErrorError + , ppContext' dir typeErrorContext ] ppTypeErrorInScopedContextWith' - :: [VarIdent] + :: OutputDirection -> [VarIdent] + -> [VarIdent] -> TypeErrorInScopedContext VarIdent -> String -ppTypeErrorInScopedContextWith' used vars = \case - PlainTypeError err -> ppTypeErrorInContext err +ppTypeErrorInScopedContextWith' dir used vars = \case + PlainTypeError err -> ppTypeErrorInContext dir err ScopedTypeError orig err -> withFresh orig $ \(x, xs) -> - ppTypeErrorInScopedContextWith' (x:used) xs $ fmap (g x) err + ppTypeErrorInScopedContextWith' dir (x:used) xs $ fmap (g x) err where g x Z = x g _ (S y) = y @@ -431,8 +441,9 @@ where z' = refreshVar used z -- FIXME: inefficient -ppTypeErrorInScopedContext' :: TypeErrorInScopedContext VarIdent -> String -ppTypeErrorInScopedContext' err = ppTypeErrorInScopedContextWith' vars (defaultVarIdents \\ vars) err +ppTypeErrorInScopedContext' :: OutputDirection -> TypeErrorInScopedContext VarIdent -> String +ppTypeErrorInScopedContext' dir err = + ppTypeErrorInScopedContextWith' dir vars (defaultVarIdents \\ vars) err where vars = nub (foldMap pure err) @@ -669,36 +680,46 @@ varOrigs :: Context var -> [(var, Maybe VarIdent)] varOrigs = map (fmap varOrig) . varInfos +withPartialDecls + :: TypeCheck VarIdent ([Decl'], [err]) + -> TypeCheck VarIdent ([Decl'], [err]) + -> TypeCheck VarIdent ([Decl'], [err]) +withPartialDecls tc next = do + (decls, errs) <- tc + if null errs + then first (decls <>) + <$> localDeclsPrepared decls next + else return (decls, errs) + withSection :: Maybe Rzk.SectionName - -> TypeCheck VarIdent [Decl VarIdent] - -> TypeCheck VarIdent [Decl VarIdent] - -> TypeCheck VarIdent [Decl VarIdent] -withSection name sectionBody next = do - sectionDecls <- startSection name $ do - decls <- sectionBody + -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) + -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) + -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) +withSection name sectionBody = + withPartialDecls $ startSection name $ do + (decls, errs) <- sectionBody localDeclsPrepared decls $ performing (ActionCloseSection name) $ do - endSection - fmap (sectionDecls <>) $ - localDeclsPrepared sectionDecls $ - next + (\ decls' -> (decls', errs)) <$> endSection errs startSection :: Maybe Rzk.SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a startSection name = local $ \Context{..} -> Context { localScopes = ScopeInfo { scopeName = name, scopeVars = [] } : localScopes , .. } -endSection :: TypeCheck VarIdent [Decl VarIdent] -endSection = askCurrentScope >>= scopeToDecls +endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent [Decl'] +endSection errs = askCurrentScope >>= scopeToDecls errs -scopeToDecls :: Eq var => ScopeInfo var -> TypeCheck var [Decl var] -scopeToDecls ScopeInfo{..} = do - decls <- collectScopeDecls [] scopeVars - forM_ decls $ \Decl{..} -> do - let unusedUsedVars = declUsedVars `intersect` map fst scopeVars - when (not (null unusedUsedVars)) $ - issueTypeError $ TypeErrorUnusedUsedVariables unusedUsedVars declName +scopeToDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> ScopeInfo var -> TypeCheck var [Decl var] +scopeToDecls errs ScopeInfo{..} = do + decls <- collectScopeDecls errs [] scopeVars + -- only issue unused variable errors if there were no errors prior in the section + when (null errs) $ do + forM_ decls $ \Decl{..} -> do + let unusedUsedVars = declUsedVars `intersect` map fst scopeVars + when (not (null unusedUsedVars)) $ + issueTypeError $ TypeErrorUnusedUsedVariables unusedUsedVars declName return decls insertExplicitAssumptionFor @@ -759,16 +780,18 @@ } xs' = map (fmap (insertExplicitAssumptionFor' a (x, xInfo))) xs -collectScopeDecls :: Eq var => [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var [Decl var] -collectScopeDecls recentVars (decl@(var, VarInfo{..}) : vars) +collectScopeDecls :: Eq var => [TypeErrorInScopedContext VarIdent] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var [Decl var] +collectScopeDecls errs recentVars (decl@(var, VarInfo{..}) : vars) | varIsAssumption = do (used, recentVars') <- makeAssumptionExplicit decl recentVars - when (not used) $ do - issueTypeError $ TypeErrorUnusedVariable var varType - collectScopeDecls recentVars' vars + -- only issue unused vars error if there were no other errors previously + when (null errs) $ do + when (not used) $ do + issueTypeError $ TypeErrorUnusedVariable var varType + collectScopeDecls errs recentVars' vars | otherwise = do - collectScopeDecls (decl : recentVars) vars -collectScopeDecls recentVars [] = return (toDecl <$> recentVars) + collectScopeDecls errs (decl : recentVars) vars +collectScopeDecls _ recentVars [] = return (toDecl <$> recentVars) where toDecl (var, VarInfo{..}) = Decl { declName = var @@ -789,21 +812,27 @@ where newDeclType = typeFunT varOrig varType Nothing (abstract var declType) -ppContext' :: Context VarIdent -> String -ppContext' ctx@Context{..} = unlines - [ "Definitions in context:" - , unlines - [ show (Pure x :: Term') <> " : " <> show (untyped ty) - | (x, ty) <- reverse (varTypes ctx) ] --- , unlines --- [ show (Pure x :: Term') <> " = " <> show (untyped term) --- | (x, Just term) <- reverse varValues ] - , intercalate "\n" (map (("when " <>) . ppAction 0) (reverse actionStack)) - , "Local tope context:" - , intercalate "\n" (map ((" " <>) . show . untyped) localTopes) - , case location of - Just (LocationInfo (Just path) _) -> "\n" <> path <> ":" - _ -> "" +data OutputDirection = TopDown | BottomUp + +block :: OutputDirection -> [String] -> String +block TopDown = intercalate "\n" +block BottomUp = intercalate "\n" . reverse + +namedBlock :: OutputDirection -> String -> [String] -> String +namedBlock dir name lines_ = block dir $ + name : map indent lines_ + where + indent = intercalate "\n" . (map (" " ++)) . lines + + +ppContext' :: OutputDirection -> Context VarIdent -> String +ppContext' dir ctx@Context{..} = block dir + [ case location of + Just (LocationInfo (Just path) (Just lineNo)) -> + path <> " (line " <> show lineNo <> "):" + Just (LocationInfo (Just path) _) -> + path <> ":" + _ -> "" , case currentCommand of Just (Rzk.CommandDefine _loc name _vars _params _ty _term) -> " Error occurred when checking\n #define " <> Rzk.printTree name @@ -827,9 +856,21 @@ " Error occurred when checking\n #section " <> Rzk.printTree name Just (Rzk.CommandSectionEnd _loc name) -> " Error occurred when checking\n #end " <> Rzk.printTree name - Nothing -> " Error occurred" --- , "Local tope context (expanded):" --- , intercalate "\n" (map ((" " <>) . show . untyped) (intercalate [TopeAndT topeT topeBottomT topeBottomT] (saturateTopes [] <$> simplifyLHS localTopes))) + Nothing -> " Error occurred outside of any command!" + , "" + , case filter (/= topeTopT) localTopes of + [] -> "Local tope context is unrestricted (⊤)." + localTopes' -> namedBlock TopDown "Local tope context:" + [ " " <> show (untyped tope) + | tope <- localTopes' ] + , "" + , block dir + [ "when " <> ppAction 0 action + | action <- actionStack ] + , namedBlock TopDown "Definitions in context:" + [ block dir + [ show (Pure x :: Term') <> " : " <> show (untyped ty) + | (x, ty) <- reverse (varTypes ctx) ] ] ] doesShadowName :: VarIdent -> TypeCheck var [VarIdent] @@ -858,12 +899,17 @@ withLocation :: LocationInfo -> TypeCheck var a -> TypeCheck var a withLocation loc = local $ \Context{..} -> Context { location = Just loc, .. } -withCommand :: Rzk.Command -> TypeCheck var a -> TypeCheck var a -withCommand command = local $ \Context{..} -> Context - { currentCommand = Just command - , location = updatePosition (Rzk.hasPosition command) <$> location - , .. } +withCommand :: Rzk.Command -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) +withCommand command tc = local f $ do + result <- (Right <$> tc) `catchError` (return . Left) + case result of + Left err -> return ([], [err]) + Right (decls, errs) -> return (decls, errs) where + f Context{..} = Context + { currentCommand = Just command + , location = updatePosition (Rzk.hasPosition command) <$> location + , .. } updatePosition pos loc = loc { locationLine = fst <$> pos } localDecls :: [Decl VarIdent] -> TypeCheck VarIdent a -> TypeCheck VarIdent a @@ -917,15 +963,15 @@ entailM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool entailM topes tope = do - genTopes <- generateTopesForPointsM (allTopePoints tope) - let topes' = nubTermT (topes <> genTopes) + -- genTopes <- generateTopesForPointsM (allTopePoints tope) + let topes' = nubTermT topes -- (topes <> genTopes) topes'' = simplifyLHSwithDisjunctions topes' topes''' = saturateTopes (allTopePoints tope) <$> topes'' - -- prettyTopes <- mapM ppTermInContext (saturateTopes (allTopePoints tope) (simplifyLHS topes')) - -- prettyTope <- ppTermInContext =<< nfTope tope - return $ - -- trace ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $ - all (`solveRHS` tope) topes''' + prettyTopes <- mapM ppTermInContext (saturateTopes (allTopePoints tope) (simplifyLHS topes')) + prettyTope <- ppTermInContext tope + traceTypeCheck Debug + ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $ + and <$> mapM (`solveRHSM` tope) topes''' entailTraceM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool entailTraceM topes tope = do @@ -1106,6 +1152,54 @@ simplifyLHS (topeEQT x x' : topeEQT y y' : topes') t : topes' -> t : simplifyLHS topes' +solveRHSM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool +solveRHSM topes tope = + case tope of + _ | topeBottomT `elem` topes -> return True + TopeTopT{} -> return True + TopeEQT _ty (PairT _ty1 x y) (PairT _ty2 x' y') -> + solveRHSM topes $ topeAndT + (topeEQT x x') + (topeEQT y y') + TopeEQT _ty (PairT TypeInfo{ infoType = CubeProductT _ cubeI cubeJ } x y) r -> + solveRHSM topes $ topeAndT + (topeEQT x (firstT cubeI r)) + (topeEQT y (secondT cubeJ r)) + TopeEQT _ty l (PairT TypeInfo{ infoType = CubeProductT _ cubeI cubeJ } x y) -> + solveRHSM topes $ topeAndT + (topeEQT (firstT cubeI l) x) + (topeEQT (secondT cubeJ l) y) + TopeEQT _ty l r + | or + [ l == r + , tope `elem` topes + , topeEQT r l `elem` topes + ] -> return True + TopeLEQT _ty l r + | l == r -> return True + | solveRHS topes (topeEQT l r) -> return True + | solveRHS topes (topeEQT l cube2_0T) -> return True + | solveRHS topes (topeEQT r cube2_1T) -> return True + TopeAndT _ l r -> (&&) + <$> solveRHSM topes l + <*> solveRHSM topes r + _ | tope `elem` topes -> return True + TopeOrT _ l r -> do + l' <- solveRHSM topes l + r' <- solveRHSM topes r + if (l' || r') + then return True + else do + lems <- generateTopesForPointsM (allTopePoints tope) + let lems' = [ lem | lem@(TopeOrT _ t1 t2) <- lems, all (`notElem` topes) [t1, t2] ] + case lems' of + TopeOrT _ t1 t2 : _ -> do + l'' <- solveRHSM (saturateTopes [] (t1 : topes)) tope + r'' <- solveRHSM (saturateTopes [] (t2 : topes)) tope + return (l'' && r'') + _ -> return False + _ -> return False + solveRHS :: Eq var => [TermT var] -> TermT var -> Bool solveRHS topes tope = case tope of @@ -2634,10 +2728,7 @@ unsafeTypeCheck' :: TypeCheck VarIdent a -> a unsafeTypeCheck' tc = case defaultTypeCheck tc of - Left err -> error $ intercalate "\n" - [ "Type Error:" - , ppTypeErrorInScopedContext' err - ] + Left err -> error $ ppTypeErrorInScopedContext' BottomUp err Right result -> result type PointId = String