From 9074aff1f9b5c717a14b2aeee764942918d2c5bb Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 25 Sep 2023 11:56:45 +0200 Subject: [PATCH 01/11] Output entailment problems in debug mode --- rzk/src/Rzk/TypeCheck.hs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index 66435e261..f1a323ad8 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -921,11 +921,11 @@ entailM topes tope = do let topes' = nubTermT (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 =<< nfTope tope + traceTypeCheck Debug + ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $ + return (all (`solveRHS` tope) topes''') entailTraceM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool entailTraceM topes tope = do From e93a35882d88e3232ef96eb99c736b3a6205693c Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 25 Sep 2023 18:20:07 +0200 Subject: [PATCH 02/11] Fix handling LEM (speedup tope layer solver) --- rzk/src/Rzk/TypeCheck.hs | 56 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 52 insertions(+), 4 deletions(-) diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index f1a323ad8..9fc34c2f5 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -917,15 +917,15 @@ entail topes tope = all (`solveRHS` tope) $ 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 + prettyTope <- ppTermInContext tope traceTypeCheck Debug ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $ - return (all (`solveRHS` tope) topes''') + and <$> mapM (`solveRHSM` tope) topes''' entailTraceM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool entailTraceM topes tope = do @@ -1106,6 +1106,54 @@ simplifyLHS topes = nubTermT $ 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 From 5398f2cb9d0744c50a93c7d1a8ff73934b66cd56 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Mon, 25 Sep 2023 22:22:49 +0200 Subject: [PATCH 03/11] Improve order of error message information for LSP --- rzk/src/Language/Rzk/VSCode/Handlers.hs | 2 +- rzk/src/Rzk/Main.hs | 4 +- rzk/src/Rzk/TypeCheck.hs | 81 +++++++++++++++---------- 3 files changed, 52 insertions(+), 35 deletions(-) diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index 1cdcb9b49..1c27ad0a1 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -121,7 +121,7 @@ typecheckFromConfigFile = do (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 diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs index c92bdc9ba..e637d94e2 100644 --- a/rzk/src/Rzk/Main.hs +++ b/rzk/src/Rzk/Main.hs @@ -35,7 +35,7 @@ main = getRecord "rzk: an experimental proof assistant for synthetic ∞-categor 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 @@ typecheckString moduleString = do , "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/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index 9fc34c2f5..18b1b73a2 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -404,21 +404,22 @@ ppTypeError' = \case , " " <> 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 +432,9 @@ ppTypeErrorInScopedContextWith' used vars = \case 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) @@ -789,21 +791,27 @@ abstractAssumption (var, VarInfo{..}) Decl{..} = Decl 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 +835,21 @@ ppContext' ctx@Context{..} = unlines " 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] @@ -2682,10 +2702,7 @@ unsafeInferStandalone' term = unsafeTypeCheck' (infer term) 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 From cf703bfe4472fce05ff9d2da1533c9e6cf4b1868 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Tue, 26 Sep 2023 00:12:08 +0200 Subject: [PATCH 04/11] Install the data-default-class package --- rzk/package.yaml | 1 + rzk/rzk.cabal | 4 ++++ stack.yaml | 1 + stack.yaml.lock | 7 +++++++ 4 files changed, 13 insertions(+) diff --git a/rzk/package.yaml b/rzk/package.yaml index b8fee82d2..1e70d5256 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -37,6 +37,7 @@ dependencies: - filepath - stm - yaml + - data-default-class ghc-options: - -Wall diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index 34b5285e9..fb8e2462c 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -54,6 +54,7 @@ library , base >=4.7 && <5 , bifunctors , bytestring + , data-default-class , filepath , lens , mtl @@ -91,6 +92,7 @@ executable rzk , base >=4.7 && <5 , bifunctors , bytestring + , data-default-class , filepath , lens , mtl @@ -122,6 +124,7 @@ test-suite doctests , base , bifunctors , bytestring + , data-default-class , doctest , filepath , lens @@ -151,6 +154,7 @@ test-suite rzk-test , base >=4.7 && <5 , bifunctors , bytestring + , data-default-class , filepath , lens , mtl diff --git a/stack.yaml b/stack.yaml index 9c4bbc045..94a17f29f 100644 --- a/stack.yaml +++ b/stack.yaml @@ -48,6 +48,7 @@ extra-deps: - row-types-1.0.1.2 - filepath-1.4.2.2 - yaml-0.11.11.2 + - data-default-class-0.1.2.0 # Override default flag values for local packages and extra-deps # flags: {} diff --git a/stack.yaml.lock b/stack.yaml.lock index 366c7c3ca..34e0aeb5b 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -60,6 +60,13 @@ packages: size: 2044 original: hackage: yaml-0.11.11.2 +- completed: + hackage: data-default-class-0.1.2.0@sha256:63e62120b7efd733a5a17cf59ceb43268e9a929c748127172d7d42f4a336e327,542 + pantry-tree: + sha256: 5017630b11698aefa65fc61cab84a257ce97833c968d425e1b2d53d6c3b5c096 + size: 224 + original: + hackage: data-default-class-0.1.2.0 snapshots: - completed: sha256: cbf721fafa21237e4999d83cfd27137f440ae0e3032ff18fa96e8148d9bf5ce1 From a4e9bcf352d581bb10c966f708c42ab8d5e0ae4e Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Tue, 26 Sep 2023 00:13:04 +0200 Subject: [PATCH 05/11] Define default instances for text completion items --- rzk/src/Language/Rzk/VSCode/Handlers.hs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index 1cdcb9b49..1f2873722 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -1,6 +1,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# OPTIONS_GHC -Wno-orphans #-} module Language.Rzk.VSCode.Handlers where @@ -142,3 +143,8 @@ typecheckFromConfigFile = do Nothing (Just []) Nothing + +instance Default T.Text where def = "" +instance Default CompletionItem +instance Default CompletionItemLabelDetails + From f6ada5a84435e9b6591bf1d22eba56a8106dd070 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Tue, 26 Sep 2023 00:13:54 +0200 Subject: [PATCH 06/11] Define a handler for the completions request --- rzk/src/Language/Rzk/VSCode/Handlers.hs | 51 +++++++++++++++++++++++-- 1 file changed, 47 insertions(+), 4 deletions(-) diff --git a/rzk/src/Language/Rzk/VSCode/Handlers.hs b/rzk/src/Language/Rzk/VSCode/Handlers.hs index 1f2873722..082f209b4 100644 --- a/rzk/src/Language/Rzk/VSCode/Handlers.hs +++ b/rzk/src/Language/Rzk/VSCode/Handlers.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE DataKinds #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -6,20 +7,30 @@ 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 @@ -148,3 +159,35 @@ 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' From e7cdb7e1a7148e85f777c2acc5b718c65469b296 Mon Sep 17 00:00:00 2001 From: Abdelrahman Abounegm Date: Tue, 26 Sep 2023 00:14:41 +0200 Subject: [PATCH 07/11] Register the handler for text completion request --- rzk/src/Language/Rzk/VSCode/Lsp.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/rzk/src/Language/Rzk/VSCode/Lsp.hs b/rzk/src/Language/Rzk/VSCode/Lsp.hs index 2391a67bf..c2a6a069f 100644 --- a/rzk/src/Language/Rzk/VSCode/Lsp.hs +++ b/rzk/src/Language/Rzk/VSCode/Lsp.hs @@ -58,6 +58,7 @@ handlers = -- 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 From 82c40d759025512236ca3b3586c2f30839fe82cd Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Tue, 26 Sep 2023 06:45:16 +0200 Subject: [PATCH 08/11] Update rzk.nix --- rzk/rzk.nix | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/rzk/rzk.nix b/rzk/rzk.nix index 77a556640..c2572664c 100644 --- a/rzk/rzk.nix +++ b/rzk/rzk.nix @@ -1,6 +1,7 @@ { mkDerivation, aeson, alex, array, base, bifunctors, bytestring -, doctest, filepath, Glob, happy, hpack, lens, lib, mtl -, optparse-generic, QuickCheck, stm, template-haskell, text, yaml +, data-default-class, doctest, filepath, Glob, happy, hpack, lens +, lib, mtl, optparse-generic, QuickCheck, stm, template-haskell +, text, yaml }: mkDerivation { pname = "rzk"; @@ -9,18 +10,19 @@ mkDerivation { isLibrary = true; isExecutable = true; libraryHaskellDepends = [ - aeson array base bifunctors bytestring filepath Glob lens mtl - optparse-generic stm template-haskell text yaml + aeson array base bifunctors bytestring data-default-class filepath + Glob lens mtl optparse-generic stm template-haskell text yaml ]; libraryToolDepends = [ alex happy hpack ]; executableHaskellDepends = [ - aeson array base bifunctors bytestring filepath Glob lens mtl - optparse-generic stm template-haskell text yaml + aeson array base bifunctors bytestring data-default-class filepath + Glob lens mtl optparse-generic stm template-haskell text yaml ]; executableToolDepends = [ alex happy ]; testHaskellDepends = [ - aeson array base bifunctors bytestring doctest filepath Glob lens - mtl optparse-generic QuickCheck stm template-haskell text yaml + aeson array base bifunctors bytestring data-default-class doctest + filepath Glob lens mtl optparse-generic QuickCheck stm + template-haskell text yaml ]; testToolDepends = [ alex happy ]; prePatch = "hpack"; From 0e28ed0fdba405f189d4bd1525cb13e06964dfca Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Tue, 26 Sep 2023 10:05:06 +0200 Subject: [PATCH 09/11] Return well-typed declarations from partially well-typed modules --- rzk/src/Rzk/TypeCheck.hs | 128 +++++++++++++++++++++++---------------- 1 file changed, 77 insertions(+), 51 deletions(-) diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index 18b1b73a2..7d1353958 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -12,6 +12,7 @@ module Rzk.TypeCheck where 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' :: [(FilePath, Rzk.Module)] -> TypeCheck VarIdent 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 :: [(FilePath, Rzk.Module)] -> TypeCheck VarIdent [ 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 - -typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent [Decl'] + (decls, errs) <- typecheckModule Nothing m + if null errs + then + localDeclsPrepared decls $ + (decls <>) <$> typecheckModules ms + else + return decls + +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 @@ typecheckModuleWithLocation (path, module_) = do 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 @@ typecheckModule path (Rzk.Module _moduleLoc _lang commands) = 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 @@ typecheckModule path (Rzk.Module _moduleLoc _lang commands) = 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 @@ typecheckModule path (Rzk.Module _moduleLoc _lang commands) = 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 @@ -671,36 +680,46 @@ varValues = map (fmap varValue) . varInfos 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 - -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 +endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent [Decl'] +endSection errs = askCurrentScope >>= scopeToDecls errs + +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 @@ -761,16 +780,18 @@ makeAssumptionExplicit assumption@(a, aInfo) ((x, xInfo) : xs) = do } 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 @@ -878,12 +899,17 @@ checkNameShadowing name = do 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 From 53e0ef6e9bf028ee96eb568b4ae777ded8f6f3b1 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Tue, 26 Sep 2023 10:05:58 +0200 Subject: [PATCH 10/11] Fix pretty-printer's layout --- rzk/src/Language/Rzk/Syntax/Print.hs | 61 +++++++++++++--------------- 1 file changed, 29 insertions(+), 32 deletions(-) diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs index 0908fcd06..d6d84fd3a 100644 --- a/rzk/src/Language/Rzk/Syntax/Print.hs +++ b/rzk/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 @@ render d = rend 0 False (map ($ "") $ d []) "" 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 @@ render d = rend 0 False (map ($ "") $ d []) "" 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 @@ printString s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"') 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 @@ instance Print (Language.Rzk.Syntax.Abs.VarIdent' a) where 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 @@ instance Print (Language.Rzk.Syntax.Abs.Command' a) where 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 @@ instance Print (Language.Rzk.Syntax.Abs.Pattern' a) where 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 @@ instance Print (Language.Rzk.Syntax.Abs.Param' a) where 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 @@ instance Print (Language.Rzk.Syntax.Abs.Restriction' a) where 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 @@ instance Print (Language.Rzk.Syntax.Abs.Term' a) where 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] From 8daeea42886c00a48d2682f85b264bbeae85bee6 Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Tue, 26 Sep 2023 10:08:38 +0200 Subject: [PATCH 11/11] Bump version and update changelogs --- docs/docs/getting-started/changelog.md | 9 +++++++++ rzk/ChangeLog.md | 9 +++++++++ rzk/package.yaml | 2 +- rzk/rzk.cabal | 2 +- rzk/rzk.nix | 2 +- 5 files changed, 21 insertions(+), 3 deletions(-) diff --git a/docs/docs/getting-started/changelog.md b/docs/docs/getting-started/changelog.md index 09ed8fed3..5db688608 100644 --- a/docs/docs/getting-started/changelog.md +++ b/docs/docs/getting-started/changelog.md @@ -6,6 +6,15 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), 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/ChangeLog.md b/rzk/ChangeLog.md index 09ed8fed3..5db688608 100644 --- a/rzk/ChangeLog.md +++ b/rzk/ChangeLog.md @@ -6,6 +6,15 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), 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/package.yaml b/rzk/package.yaml index 1e70d5256..f3d67be70 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -1,5 +1,5 @@ name: rzk -version: 0.6.1 +version: 0.6.2 github: 'rzk-lang/rzk' license: BSD3 author: 'Nikolai Kudasov' diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index fb8e2462c..374cf48d3 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -5,7 +5,7 @@ cabal-version: 1.12 -- 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 diff --git a/rzk/rzk.nix b/rzk/rzk.nix index c2572664c..4d0b32d95 100644 --- a/rzk/rzk.nix +++ b/rzk/rzk.nix @@ -5,7 +5,7 @@ }: mkDerivation { pname = "rzk"; - version = "0.6.1"; + version = "0.6.2"; src = ./.; isLibrary = true; isExecutable = true;