diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -6,7 +6,43 @@ and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). -## Unreleased +## v0.9.2 — 2026-07-13 + +Added: + +- **Language server: cross-file references, hover, symbols, and better highlighting** (see [#282](https://github.com/rzk-lang/rzk/pull/282)). Go-to-definition and find-references work across the files of a project. Hover shows a definition's elaborated type (falling back to the written annotation), rendered as an rzk code block; long signatures are split across lines, pair binders are split through weak head normalisation, and shaped binders are shown with their tope. Document symbols populate the outline view. Semantic tokens are computed from the lexer token stream, and a per-file parse cache keeps the last good parse across syntax errors, so highlighting, hover, and references keep working while a file is temporarily broken. No grammar changes are involved. A matching `vscode-rzk` release should be pinned to this version, so editor users actually receive the new UX. + +- **Language server: typecheck progress reporting and a responsive server** (see [#283](https://github.com/rzk-lang/rzk/pull/283)). Typechecking now reports its progress to the editor (via `$/progress`), showing the file being checked and the fraction of modules done. The project re-check runs on a worker thread, so requests such as formatting on save are answered while the re-check is still running; a newer change cancels and restarts the re-check, keeping the modules it has finished. Checking stops at the first module with errors; the modules a run never reaches are now marked with a warning naming the blocker (e.g. `Not checked: blocked by an error in …`) instead of keeping stale diagnostics. + +- **Language server: workspace symbol search** (see [#285](https://github.com/rzk-lang/rzk/pull/285)). Every definition of the project is searchable by name. In VS Code, press `Ctrl+T` (`⌘T` on macOS, "Go to Symbol in Workspace…"), or type `#` followed by the name in Quick Open, e.g. `#yoneda`; Enter jumps to the definition. Matching is case-insensitive and by infix, and the results span all files of the project, not just the open one (that remains the job of document symbols, `Ctrl+Shift+O`). Definitions are served from the typecheck cache, so a module becomes searchable once it has been checked. + +- **Language server: holes are highlighted** (see [#284](https://github.com/rzk-lang/rzk/pull/284)). A hole (`?` or `?name`) now gets its own semantic token. It is computed from the lexer token stream, so holes stay highlighted while the file temporarily fails to parse. + +Changed: + +- Function types no longer show unused anonymous binders (see [#286](https://github.com/rzk-lang/rzk/pull/286)). A goal `#!rzk U → U` used to print as `#!rzk (x₁ : U) → U`, with a machine-generated name; the domain is now rendered as a plain parameter everywhere a type is shown (hover, hole goals, error messages). A user-written name is kept even when unused. + +Fixed: + +- Subtype checks now respect variance. Three asymmetric checks (tope-family domains, the domain topes of Π-types, and restriction faces) ran in a fixed direction regardless of the ambient variance, so in negative positions they ran backwards. For example, `#!rzk k : (f : (t : 2 | ⊤) → A) → A` was accepted where `#!rzk (f : (t : 2 | t ≡ 0₂) → A) → A` is expected, letting `#!rzk k` apply a partial `#!rzk f` outside its domain. Each check now consults the variance flag; six regression fixtures are added, and the sHoTT corpus is unaffected (see [#269](https://github.com/rzk-lang/rzk/pull/269)). + +- Unification no longer equates identity types over different types. Identity types were equated whenever their endpoints unified, accepting e.g. a free homotopy (a path in `#!rzk Δ¹ → A`) where an endpoint-fixing one (a path in `#!rzk hom A x y`) is expected. The underlying types are now compared, invariantly, so subtyping does not leak into equality of identity types (see [#270](https://github.com/rzk-lang/rzk/pull/270)). + +Performance: + +- A performance pass over the typechecker roughly halves the wall-clock time of a full sHoTT check (26–28 s down to ~13.5 s) and cuts its maximum residency fourfold (8 GB down to 2.1 GB): + + - the tope solver short-circuits its Boolean search, maintains the flat-cube discreteness axioms incrementally, and builds its debug traces only at `Debug` verbosity (see [#273](https://github.com/rzk-lang/rzk/pull/273)); + - variable lookups no longer project the whole context (see [#276](https://github.com/rzk-lang/rzk/pull/276)); + - top-level entries are kept unshifted and embedded on lookup (see [#277](https://github.com/rzk-lang/rzk/pull/277)); + - the name-shadowing check no longer embeds global payloads (see [#279](https://github.com/rzk-lang/rzk/pull/279)); + - the saturated tope context is cached lazily, recomputed only when the context changes (see [#280](https://github.com/rzk-lang/rzk/pull/280)). + + A corpus benchmark harness under `bench/` records the measurements (see [#274](https://github.com/rzk-lang/rzk/pull/274)). + +CI / infrastructure: + +- The parser-drift workflow now also fails on LR conflicts and unused rules in the grammar (`make -C rzk check-parser-conflicts`), so a grammar change cannot silently introduce ambiguity (see [#281](https://github.com/rzk-lang/rzk/pull/281)). ## v0.9.1 — 2026-06-26 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.9.1 +version: 0.9.2 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types @@ -39,6 +39,9 @@ test/typecheck/cases/happy-refl-path.rzk test/typecheck/cases/happy-restrict-face-not-contained.rzk test/typecheck/cases/happy-shott-simplicial-subcomplexes.rzk + test/typecheck/cases/happy-subtype-variance-pi-shape-domain.rzk + test/typecheck/cases/happy-subtype-variance-restriction-faces.rzk + test/typecheck/cases/happy-subtype-variance-tope-family.rzk test/typecheck/cases/happy-tope-high-dim-cubes.rzk test/typecheck/cases/happy-tope-nested-rec-or-d4.rzk test/typecheck/cases/happy-tope-nested-rec-or-d5.rzk @@ -92,6 +95,9 @@ test/typecheck/cases/ill-set-option-render.rzk test/typecheck/cases/ill-set-option-unknown.rzk test/typecheck/cases/ill-set-option-verbosity.rzk + test/typecheck/cases/ill-subtype-variance-pi-shape-domain.rzk + test/typecheck/cases/ill-subtype-variance-restriction-faces.rzk + test/typecheck/cases/ill-subtype-variance-tope-family.rzk test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d4.rzk test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d5.rzk test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d6.rzk @@ -113,6 +119,7 @@ test/typecheck/cases/ill-unexpected-lambda.rzk test/typecheck/cases/ill-unexpected-pair.rzk test/typecheck/cases/ill-unexpected-refl.rzk + test/typecheck/cases/ill-unify-id-free-path.rzk test/typecheck/cases/ill-unify-terms-path.rzk test/typecheck/cases/ill-unify.rzk test/typecheck/cases/ill-unset-option-unknown.rzk @@ -142,6 +149,9 @@ test/typecheck/cases/happy-refl-path.expect.yaml test/typecheck/cases/happy-restrict-face-not-contained.expect.yaml test/typecheck/cases/happy-shott-simplicial-subcomplexes.expect.yaml + test/typecheck/cases/happy-subtype-variance-pi-shape-domain.expect.yaml + test/typecheck/cases/happy-subtype-variance-restriction-faces.expect.yaml + test/typecheck/cases/happy-subtype-variance-tope-family.expect.yaml test/typecheck/cases/happy-tope-high-dim-cubes.expect.yaml test/typecheck/cases/happy-tope-nested-rec-or-d4.expect.yaml test/typecheck/cases/happy-tope-nested-rec-or-d5.expect.yaml @@ -195,6 +205,9 @@ test/typecheck/cases/ill-set-option-render.expect.yaml test/typecheck/cases/ill-set-option-unknown.expect.yaml test/typecheck/cases/ill-set-option-verbosity.expect.yaml + test/typecheck/cases/ill-subtype-variance-pi-shape-domain.expect.yaml + test/typecheck/cases/ill-subtype-variance-restriction-faces.expect.yaml + test/typecheck/cases/ill-subtype-variance-tope-family.expect.yaml test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d4.expect.yaml test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d5.expect.yaml test/typecheck/cases/ill-tope-nested-rec-or-inner-singleton-d6.expect.yaml @@ -216,6 +229,7 @@ test/typecheck/cases/ill-unexpected-lambda.expect.yaml test/typecheck/cases/ill-unexpected-pair.expect.yaml test/typecheck/cases/ill-unexpected-refl.expect.yaml + test/typecheck/cases/ill-unify-id-free-path.expect.yaml test/typecheck/cases/ill-unify-terms-path.expect.yaml test/typecheck/cases/ill-unify.expect.yaml test/typecheck/cases/ill-unset-option-unknown.expect.yaml @@ -288,9 +302,12 @@ Language.Rzk.VSCode.Logging Language.Rzk.VSCode.Lsp Language.Rzk.VSCode.Tokenize + Language.Rzk.VSCode.ReferenceIndex build-depends: aeson >=2.0.0.0 && <3 + , async >=2.2 && <3 , co-log-core >=0.3.2.0 && <1 + , containers >=0.6 && <1 , data-default-class >=0.1.2.0 && <1 , filepath >=1.4.100.0 && <2 , lens >=5.0.1 && <6 @@ -362,9 +379,12 @@ type: exitcode-stdio-1.0 main-is: Spec.hs other-modules: + Rzk.BinderTypesSpec Rzk.DiagnosticSpec Rzk.FormatSpec Rzk.HolesSpec + Rzk.RefIndexSpec + Rzk.SemanticTokensSpec Rzk.TypeCheckSpec Paths_rzk autogen-modules: @@ -395,3 +415,6 @@ default-language: Haskell2010 if flag(lsp) && !impl(ghcjs) cpp-options: -DLSP_ENABLED + if flag(lsp) && !impl(ghcjs) + build-depends: + lsp-types >=2.1.1.0 && <3 diff --git a/src/Language/Rzk/Free/Syntax.hs b/src/Language/Rzk/Free/Syntax.hs --- a/src/Language/Rzk/Free/Syntax.hs +++ b/src/Language/Rzk/Free/Syntax.hs @@ -667,6 +667,13 @@ f Z = Pure x f (S z) = Pure z +-- | Drop the binder of a scope that does not use it. The error is +-- unreachable when 'Z' is not among the scope's free variables. +unusedScope :: Scope Term var -> Term var +unusedScope scope = scope >>= \case + Z -> error "unusedScope: the bound variable is used" + S z -> Pure z + -- | Like 'fromScope'', but additionally restores pattern-binder component names -- inside the scope: projections of the bound variable @x@ are folded back to -- the names recorded in @binder@ (e.g. @π₁ x@ becomes @t@). For a binder that @@ -755,6 +762,12 @@ Hole mname -> Rzk.Hole loc (Rzk.HoleIdent loc (Rzk.HoleIdentToken (holeIdentToken mname))) + -- An anonymous binder that the return type does not use is not shown: + -- @(x₁ : A) → B@ reads better as @A → B@. A user-written name is kept + -- even when unused. + TypeFun (BinderVar Nothing) Id arg Nothing ret + | Z `notElem` freeVars ret -> + Rzk.TypeFun loc (Rzk.ParamType loc (go arg)) (go (unusedScope ret)) TypeFun z Id arg Nothing ret -> withFreshBinder z $ \(x, z', xs) -> Rzk.TypeFun loc (Rzk.ParamTermType loc (patternToTerm (binderToPattern z')) (go arg)) (fromScopeBinder' z' x used xs ret) TypeFun z Id arg (Just tope) ret -> withFreshBinder z $ \(x, z', xs) -> diff --git a/src/Language/Rzk/VSCode/Env.hs b/src/Language/Rzk/VSCode/Env.hs --- a/src/Language/Rzk/VSCode/Env.hs +++ b/src/Language/Rzk/VSCode/Env.hs @@ -1,10 +1,18 @@ +{-# LANGUAGE ScopedTypeVariables #-} module Language.Rzk.VSCode.Env where +import Control.Concurrent.Async (Async, async, cancel) import Control.Concurrent.STM +import Control.Exception (catch) import Control.Monad.Reader +import qualified Data.Map.Strict as Map +import qualified Data.Text as T import Language.LSP.Server import Language.Rzk.Free.Syntax (VarIdent) +import Language.Rzk.Syntax (Module) import qualified Language.Rzk.VSCode.Config as RzkConfig +import Language.Rzk.VSCode.Logging +import qualified Language.Rzk.VSCode.ReferenceIndex as RefInd import Rzk.TypeCheck (Decl', TypeErrorInScopedContext) data RzkCachedModule = RzkCachedModule @@ -14,38 +22,117 @@ type RzkTypecheckCache = [(FilePath, RzkCachedModule)] -newtype RzkEnv = RzkEnv - { rzkEnvTypecheckCache :: TVar RzkTypecheckCache +-- | Where a parse came from, deciding whether it may be reused. +data ParseSource + = ParsedFromBuffer T.Text + -- ^ Parsed from the editor buffer with this text; reusable for the + -- current file while the buffer text is unchanged. + | ParsedFromDisk + -- ^ Parsed from the file on disk; trusted until invalidated by a + -- file-change notification. + | ParseInvalidated + -- ^ The file changed; must be re-parsed. The module is kept as the last + -- good parse, which hover falls back to while the file fails to parse. + +-- | A parse result for the reference index. A failed parse is a 'Nothing' +-- module and is not retried until the source changes. +data ParsedModule = ParsedModule + { parsedSource :: ParseSource + , parsedModule :: Maybe Module } +data ReferenceIndexCache = ReferenceIndexCache + { indexCacheModules :: Map.Map FilePath ParsedModule + -- ^ Per-file parse cache. Entries parsed from disk are trusted until a + -- file-change notification evicts them ('resetCacheForFiles'); the entry + -- for the file being edited is revalidated against the editor buffer. + , indexCacheResult :: Maybe ([FilePath], RefInd.ReferenceIndex) + -- ^ The index last built, with the file set it was built from. + } + +emptyReferenceIndexCache :: ReferenceIndexCache +emptyReferenceIndexCache = ReferenceIndexCache Map.empty Nothing + +data RzkEnv = RzkEnv + { rzkEnvTypecheckCache :: TVar RzkTypecheckCache + , rzkEnvReferenceIndexCache :: TVar ReferenceIndexCache + , rzkEnvTypecheckWorker :: TVar (Maybe (Async ())) + -- ^ The thread running the current project typecheck, if any. + } + defaultRzkEnv :: IO RzkEnv defaultRzkEnv = do typecheckCache <- newTVarIO [] + referenceIndexCache <- newTVarIO emptyReferenceIndexCache + typecheckWorker <- newTVarIO Nothing return RzkEnv - { rzkEnvTypecheckCache = typecheckCache } + { rzkEnvTypecheckCache = typecheckCache + , rzkEnvReferenceIndexCache = referenceIndexCache + , rzkEnvTypecheckWorker = typecheckWorker + } type LSP = LspT RzkConfig.ServerConfig (ReaderT RzkEnv IO) --- | Override the cache with given typechecked modules. +-- | Run the given action (a project typecheck) on a fresh worker thread, +-- cancelling the previous worker first. Cancellation waits for the old +-- worker to stop, so it can no longer write to the caches once the new +-- one starts. Typechecking runs on a worker so that the handler dispatch +-- thread stays responsive: 'lsp' dispatches messages sequentially, so a +-- multi-second re-check run directly in a notification handler would +-- block every later request (e.g. formatting on save). +spawnTypecheckWorker :: LSP () -> LSP () +spawnTypecheckWorker action = do + lspEnv <- getLspEnv + rzkEnv <- lift ask + let run act = runReaderT (runLspT lspEnv act) rzkEnv + liftIO $ do + oldWorker <- atomically $ swapTVar (rzkEnvTypecheckWorker rzkEnv) Nothing + mapM_ cancel oldWorker + worker <- async $ + run action `catch` \(_ :: ProgressCancelledException) -> + run (logInfo (T.pack "Typechecking was cancelled by the client")) + atomically $ writeTVar (rzkEnvTypecheckWorker rzkEnv) (Just worker) + cacheTypecheckedModules :: RzkTypecheckCache -> LSP () cacheTypecheckedModules cache = lift $ do typecheckCache <- asks rzkEnvTypecheckCache + referenceIndexCache <- asks rzkEnvReferenceIndexCache liftIO $ atomically $ do writeTVar typecheckCache cache + -- Drop the built index (the declaration set may have changed), but keep + -- the parse entries: files changed on disk are already evicted per path + -- by 'resetCacheForFiles' on file-change notifications, and a kept entry + -- may hold the last good parse of a file that currently has a syntax + -- error, which hover falls back to. + modifyTVar referenceIndexCache $ \c -> c { indexCacheResult = Nothing } --- | Completely invalidate the cache of typechecked files. resetCacheForAllFiles :: LSP () resetCacheForAllFiles = cacheTypecheckedModules [] --- | Invalidate the cache for a list of file paths. resetCacheForFiles :: [FilePath] -> LSP () resetCacheForFiles paths = lift $ do typecheckCache <- asks rzkEnvTypecheckCache + referenceIndexCache <- asks rzkEnvReferenceIndexCache liftIO $ atomically $ do modifyTVar typecheckCache (takeWhile ((`notElem` paths) . fst)) + modifyTVar referenceIndexCache $ \c -> ReferenceIndexCache + { indexCacheModules = + foldr (Map.adjust (\pm -> pm { parsedSource = ParseInvalidated })) + (indexCacheModules c) paths + , indexCacheResult = Nothing + } --- | Get the current state of the cache. getCachedTypecheckedModules :: LSP RzkTypecheckCache getCachedTypecheckedModules = lift $ do typecheckCache <- asks rzkEnvTypecheckCache liftIO $ readTVarIO typecheckCache + +cacheReferenceIndex :: ReferenceIndexCache -> LSP () +cacheReferenceIndex cache = lift $ do + referenceIndexCache <- asks rzkEnvReferenceIndexCache + liftIO $ atomically $ writeTVar referenceIndexCache cache + +getCachedReferenceIndex :: LSP ReferenceIndexCache +getCachedReferenceIndex = lift $ do + referenceIndexCache <- asks rzkEnvReferenceIndexCache + liftIO $ readTVarIO referenceIndexCache 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 @@ -11,34 +11,48 @@ module Language.Rzk.VSCode.Handlers ( typecheckFromConfigFile, provideCompletions, + provideSymbols, + provideWorkspaceSymbols, + findDefinition, + findReferences, + provideHover, + formatSignature, formatDocument, provideSemanticTokens, handleFilesChanged, ) where -import Control.Exception (SomeException, evaluate, try) +import Control.Applicative ((<|>)) +import Control.Exception (SomeAsyncException (..), + SomeException, evaluate, + fromException, throwIO, try) import Control.Lens -import Control.Monad (forM_, when) +import Control.Monad (forM, forM_, unless, when) import Control.Monad.Except (ExceptT (ExceptT), MonadError (throwError), runExceptT) import Control.Monad.Error.Class (modifyError) import Control.Monad.IO.Class (MonadIO (..)) import Data.Default.Class -import Data.List (isSuffixOf, sort, (\\)) -import qualified Data.List.NonEmpty as NE +import Data.List (find, intercalate, isSuffixOf, + nub, sort, (\\)) +import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe, isNothing) import qualified Data.Text as T import qualified Data.Yaml as Yaml import Language.LSP.Diagnostics (partitionBySource) -import Language.LSP.Protocol.Lens (HasDetail (detail), +import Language.LSP.Protocol.Lens (HasContext (context), + HasDetail (detail), HasDocumentation (documentation), HasLabel (label), HasParams (params), + HasPosition (position), + HasQuery (query), HasTextDocument (textDocument), HasUri (uri), changes, uri) import Language.LSP.Protocol.Message import Language.LSP.Protocol.Types +import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Server import Language.LSP.VFS (virtualFileText) import System.FilePath (makeRelative, ()) @@ -46,20 +60,38 @@ import Data.Char (isDigit) import Language.Rzk.Free.Syntax (RzkPosition (RzkPosition), - VarIdent (getVarIdent)) -import Language.Rzk.Syntax (Module, VarIdent' (VarIdent), + VarIdent (getVarIdent), + fromTerm') +import Language.Rzk.Syntax (Module, Term, + Term' (ASCII_TypeFun, TypeFun), + VarIdent' (VarIdent), parseModuleFile, parseModuleSafe, printTree) import qualified Language.Rzk.VSCode.Config as RzkConfig import Language.Rzk.VSCode.Env +import qualified Language.Rzk.VSCode.ReferenceIndex as RefInd import Language.Rzk.VSCode.Logging -import Language.Rzk.VSCode.Tokenize (tokenizeModule) +import Language.Rzk.VSCode.Tokenize (mergeTokens, tokenizeModule, + tokenizeSyntaxSymbols) +import Free.Scoped (untyped) import qualified Rzk.Diagnostic as Diag import Rzk.Format (format) import Rzk.Project.Config (ProjectConfig (include)) import Rzk.TypeCheck import Text.Read (readMaybe) +-- | Like 'try', but re-throws asynchronous exceptions (a worker restart) and +-- 'ProgressCancelledException' (a client-side progress cancel; delivered by +-- 'Control.Concurrent.Async.cancelWith', so 'fromException' does not classify +-- it as asynchronous). Cancellation must abort the whole run instead of being +-- reported as a typechecker failure of the current module. +tryTypecheck :: IO a -> IO (Either SomeException a) +tryTypecheck action = try action >>= \case + Left e + | Just (SomeAsyncException _) <- fromException e -> throwIO e + | Just cancelled <- fromException @ProgressCancelledException e -> throwIO cancelled + result -> return result + -- | Given a list of file paths, reads them and parses them as Rzk modules, -- returning the same list of file paths but with the parsed module (or parse error) parseFiles :: [FilePath] -> IO [(FilePath, Either T.Text Module)] @@ -91,6 +123,27 @@ tshow :: Show a => a -> T.Text tshow = T.pack . show +fromLspUri :: LSP.Uri -> RefInd.Uri +fromLspUri u = RefInd.Uri { uriPath = fromMaybe "" (uriToFilePath u) } + +toLspUri :: RefInd.Uri -> LSP.Uri +toLspUri (RefInd.Uri { uriPath = p }) = filePathToUri p + +fromLspPosition :: LSP.Position -> RefInd.Position +fromLspPosition (LSP.Position l c) = + RefInd.Position (fromIntegral l) (fromIntegral c) + +toLspPosition :: RefInd.Position -> LSP.Position +toLspPosition (RefInd.Position l c) = + LSP.Position (fromIntegral l) (fromIntegral c) + +toLspRange :: RefInd.Range -> Range +toLspRange (RefInd.Range s e) = Range (toLspPosition s) (toLspPosition e) + +toLspLocation :: RefInd.Location -> LSP.Location +toLspLocation (RefInd.Location u r) = + LSP.Location (toLspUri u) (toLspRange r) + typecheckFromConfigFile :: LSP () typecheckFromConfigFile = do logInfo "Looking for rzk.yaml" @@ -111,8 +164,7 @@ rawPaths <- liftIO $ globDir (map compile (include config)) rootPath let paths = concatMap sort rawPaths - typecheckedCachedModules <- getCachedTypecheckedModules - let cachedModules = map (\(path, RzkCachedModule{..}) -> (path, cachedModuleDecls)) typecheckedCachedModules + cachedModules <- getCachedTypecheckedModules let cachedPaths = map fst cachedModules modifiedFiles = paths \\ cachedPaths @@ -120,56 +172,125 @@ logDebug (tshow (length modifiedFiles) <> " files have been modified") (parseErrors, parsedModules) <- liftIO $ collectErrors <$> parseFiles modifiedFiles + + -- Report parse errors to the client + forM_ parseErrors $ \(path, err) -> do + publishDiagnostics maxDiagnosticCount (filePathToNormalizedUri path) Nothing (partitionBySource [diagnosticOfParseError err]) + + -- Files after the first parse error are not typechecked at all + -- ('collectErrors' stops collecting modules there); mark the ones + -- without a parse error of their own as blocked. + case parseErrors of + [] -> return () + (blockingPath, _) : _ -> do + let reported = map fst parsedModules <> map fst parseErrors + publishBlockedDiagnostics rootPath blockingPath + (filter (`notElem` reported) modifiedFiles) + + -- Typecheck the modified modules one at a time on top of the cached + -- prefix, reporting progress to the client. Each module is cached + -- and its diagnostics are published as soon as it is checked, so a + -- cancelled run keeps the modules it has finished and the next run + -- continues from there. + unless (null parsedModules) $ + withProgress "rzk typechecking" Nothing Cancellable $ \reportProgress -> + checkModules reportProgress rootPath cachedModules parsedModules + where + checkModules + :: (ProgressAmount -> LSP ()) + -> FilePath -- ^ Workspace root (for progress messages). + -> RzkTypecheckCache -- ^ Cached results for the unchanged prefix. + -> [(FilePath, Module)] -- ^ Modified modules, in project order. + -> LSP () + checkModules reportProgress rootPath cache modules = go (0 :: Int) cache modules + where + total = length modules + + go _ _ [] = return () + go i checked ((path, module_) : rest) = do + reportProgress (ProgressAmount + (Just (fromIntegral (100 * i `div` total))) + (Just (T.pack (makeRelative rootPath path)))) -- Run in lenient hole mode so holes are collected (and surfaced as -- hints) rather than reported as errors while editing. - tcResults <- liftIO $ try $ evaluate $ - defaultTypeCheckWithHoles (typecheckModulesWithLocationIncremental cachedModules parsedModules) - - (typeErrors, holeInfos) <- case tcResults of + tcResult <- liftIO $ tryTypecheck $ evaluate $ + defaultTypeCheckWithHoles $ typecheckModulesWithLocationIncremental + (map (fmap cachedModuleDecls) checked) [(path, module_)] + case tcResult of Left (ex :: SomeException) -> do -- Just a warning to be logged in the "Output" panel and not shown to the user as an error message -- because exceptions are expected when the file has invalid syntax logWarning ("Encountered an exception while typechecking:\n" <> tshow ex) - return ([], []) + publishBlockedDiagnostics rootPath path (map fst rest) Right (Left err) -> do logError ("An impossible error happened! Please report a bug:\n" <> T.pack (ppTypeErrorInScopedContext' BottomUp err)) - return ([err], []) -- sort of impossible - Right (Right ((checkedModules, errors), foundHoles)) -> do - -- cache well-typed modules - logInfo (tshow (length checkedModules) <> " modules successfully typechecked") - logInfo (tshow (length errors) <> " errors found") - logInfo (tshow (length foundHoles) <> " holes found") - let checkedModules' = map (\(path, decls) -> (path, RzkCachedModule decls (filter ((== path) . filepathOfTypeError) errors))) checkedModules - cacheTypecheckedModules checkedModules' - return (errors, foundHoles) + publishModuleDiagnostics path [err] [] -- sort of impossible + publishBlockedDiagnostics rootPath path (map fst rest) + Right (Right ((checkedModules, errors), holeInfos)) -> do + logDebug (T.pack path <> ": " <> tshow (length errors) <> " errors, " + <> tshow (length holeInfos) <> " holes") + let decls = fromMaybe [] (lookup path checkedModules) + checked' = checked ++ + [(path, RzkCachedModule decls (filter ((== path) . filepathOfTypeError) errors))] + cacheTypecheckedModules checked' + publishModuleDiagnostics path errors holeInfos + -- Stop at the first module with errors, like the batch checker + -- ('typecheckModulesWithLocation'') does: later modules depend + -- on this one and would report cascading errors. Mark the + -- modules this run will not reach. + if null errors + then go (i + 1) checked' rest + else publishBlockedDiagnostics rootPath path (map fst rest) - -- Reset all published diags - -- TODO: remove this after properly grouping by path below, after which there can be an empty list of errors - -- TODO: handle clearing diagnostics for files that got removed from the project (rzk.yaml) - forM_ modifiedFiles $ \path -> do - publishDiagnostics 0 (filePathToNormalizedUri path) Nothing (partitionBySource []) + -- Publish the diagnostics of one checked module, grouped by file so all + -- diagnostics for a file are published in a single call + -- (publishDiagnostics replaces a source's diagnostics per URI, so + -- publishing them one at a time would clobber all but the last). The + -- module's own file is always published, possibly with an empty list, + -- replacing stale diagnostics from the previous run. + -- + -- An empty list needs care: the lsp diagnostic store unions the new + -- per-source map over the old one, and @partitionBySource []@ has no + -- "rzk" key, so the old diagnostics would survive and be re-sent. A + -- max count of 0 forces an empty publish to the client, clearing it. + publishModuleDiagnostics :: FilePath -> [TypeErrorInScopedContext VarIdent] -> [HoleInfo] -> LSP () + publishModuleDiagnostics path typeErrors holeInfos = do + let errDiagnostics = [ (filepathOfTypeError err, [diagnosticOfTypeError err]) + | err <- typeErrors ] + holeDiagnostics = [ (path', [diagnosticOfHole hole]) + | hole <- holeInfos + , Just path' <- [holeLocation hole >>= locationFilePath] ] + diagnosticsByFile = Map.insertWith (flip (<>)) path [] $ + Map.fromListWith (flip (<>)) (errDiagnostics <> holeDiagnostics) + forM_ (Map.toList diagnosticsByFile) $ \(path', diags) -> + publishDiagnostics (if null diags then 0 else maxDiagnosticCount) + (filePathToNormalizedUri path') Nothing (partitionBySource diags) - -- Report parse errors to the client - forM_ parseErrors $ \(path, err) -> do - publishDiagnostics maxDiagnosticCount (filePathToNormalizedUri path) Nothing (partitionBySource [diagnosticOfParseError err]) + -- Modules that a run never reaches (they come after a module with an + -- error, and every rzk module depends on all earlier ones) get a single + -- warning diagnostic naming the blocker, instead of keeping whatever + -- diagnostics a previous run left behind. Warning severity keeps the + -- file visible in the explorer (yellow badge) while staying distinct + -- from a real error in the file itself. It is replaced by real + -- diagnostics once the blocker is fixed and the module is reached + -- again. + publishBlockedDiagnostics :: FilePath -> FilePath -> [FilePath] -> LSP () + publishBlockedDiagnostics rootPath blockingPath notReached = + forM_ notReached $ \path -> + publishDiagnostics maxDiagnosticCount (filePathToNormalizedUri path) Nothing + (partitionBySource [blockedDiagnostic]) + where + blockedDiagnostic = Diagnostic + (Range (Position 0 0) (Position 0 99)) + (Just DiagnosticSeverity_Warning) + (Just (InR "not-checked")) + Nothing -- diagnostic description + (Just "rzk") -- A human-readable string describing the source of this diagnostic + ("Not checked: blocked by an error in " <> T.pack (makeRelative rootPath blockingPath)) + Nothing -- tags + (Just []) -- related information + Nothing -- data that is preserved between different calls - -- Report typechecking errors and holes to the client, grouped by file - -- so all diagnostics for a file are published in a single call - -- (publishDiagnostics replaces a source's diagnostics per URI, so - -- publishing them one at a time would clobber all but the last). - let errDiagnostics = [ (filepathOfTypeError err, diagnosticOfTypeError err) - | err <- typeErrors ] - holeDiagnostics = [ (path, diagnosticOfHole hole) - | hole <- holeInfos - , Just path <- [holeLocation hole >>= locationFilePath] ] - -- group by file path (NE.groupAllWith sorts then groups, and - -- yields NonEmpty groups so taking the key is total) - diagnosticsByFile = - map (\grp -> (fst (NE.head grp), map snd (NE.toList grp))) $ - NE.groupAllWith fst (errDiagnostics <> holeDiagnostics) - forM_ diagnosticsByFile $ \(path, diags) -> - publishDiagnostics maxDiagnosticCount (filePathToNormalizedUri path) Nothing (partitionBySource diags) - where filepathOfTypeError :: TypeErrorInScopedContext var -> FilePath filepathOfTypeError (PlainTypeError err) = case location (typeErrorContext err) >>= locationFilePath of @@ -349,8 +470,17 @@ mdoc <- getVirtualFile doc possibleTokens <- case virtualFileText <$> mdoc of Nothing -> return (Left "Failed to get file content") - Just sourceCode -> fmap (fmap tokenizeModule) $ liftIO $ - parseModuleSafe (T.filter (/= '\r') sourceCode) + Just sourceCode -> do + let src = T.filter (/= '\r') sourceCode + -- Fixed symbols (commands, keywords, operators) are highlighted from + -- the lexer token stream, so they survive parse failures; identifiers + -- need the parsed module. + astTokens <- liftIO (parseModuleSafe src) >>= \case + Left err -> do + logWarning ("Failed to parse file for semantic tokens: " <> err) + return [] + Right rzkModule -> return (tokenizeModule rzkModule) + return (Right (mergeTokens astTokens (tokenizeSyntaxSymbols src))) case possibleTokens of Left err -> do -- Exception occurred when parsing the module @@ -364,7 +494,210 @@ Right list -> responder (Right (InL (SemanticTokens Nothing list))) +findDefinition :: Handler LSP 'Method_TextDocumentDefinition +findDefinition req res = do + let uri' = req ^. params . textDocument . uri + currentFile = fromMaybe "" (uriToFilePath uri') + referenceIndex <- indexProject currentFile + case RefInd.lookupAt referenceIndex (fromLspUri uri') (fromLspPosition (req ^. params . position)) of + Just binding -> res $ Right $ InL $ Definition $ InL (toLspLocation (RefInd.bindingDef binding)) + Nothing -> res $ Right $ InR $ InR Null +findReferences :: Handler LSP 'Method_TextDocumentReferences +findReferences req res = do + let uri' = req ^. params . textDocument . uri + currentFile = fromMaybe "" (uriToFilePath uri') + includeDeclaration = req ^. params . context . to (\(ReferenceContext incl) -> incl) + referenceIndex <- indexProject currentFile + case RefInd.lookupAt referenceIndex (fromLspUri uri') (fromLspPosition (req ^. params . position)) of + Just binding -> + let sites + | includeDeclaration = RefInd.bindingSites binding + | otherwise = RefInd.bindingRefs binding + in res $ Right $ InL (map toLspLocation sites) + Nothing -> res $ Right $ InL [] + +indexProject :: FilePath -> LSP RefInd.ReferenceIndex +indexProject currentFile = do + cached <- getCachedTypecheckedModules + let paths = nub (currentFile : map fst cached) + mdoc <- getVirtualFile (filePathToNormalizedUri currentFile) + let msrc = T.filter (/= '\r') <$> (virtualFileText <$> mdoc) + ReferenceIndexCache oldModules oldResult <- getCachedReferenceIndex + -- Re-parse only what changed: the current file is revalidated against the + -- editor buffer, while other files keep their cached parse until a + -- file-change notification invalidates it (see resetCacheForFiles). + let reusable p pm = case parsedSource pm of + ParseInvalidated -> False + ParsedFromBuffer t -> p /= currentFile || msrc == Just t + ParsedFromDisk -> p /= currentFile || isNothing msrc + entries <- forM paths $ \p -> + case Map.lookup p oldModules of + Just pm | reusable p pm -> return (p, pm, False) + mold -> do + parsed <- parseProjectFile currentFile msrc p + let source = if p == currentFile + then maybe ParsedFromDisk ParsedFromBuffer msrc + else ParsedFromDisk + -- A failed parse (a syntax error mid-edit) keeps the last good + -- module, so hover and navigation stay available; the source is + -- still updated, so the parse is retried once per edit, not once + -- per request. + module_ = parsed <|> (parsedModule =<< mold) + return (p, ParsedModule source module_, True) + let reparsed = or [ r | (_, _, r) <- entries ] + case oldResult of + Just (ps, cachedIndex) | ps == paths, not reparsed -> return cachedIndex + _ -> do + let referenceIndex = RefInd.indexModules + [ (p, m) | (p, ParsedModule _ (Just m), _) <- entries ] + cacheReferenceIndex $ ReferenceIndexCache + (Map.fromList [ (p, pm) | (p, pm, _) <- entries ]) + (Just (paths, referenceIndex)) + return referenceIndex + +parseProjectFile :: FilePath -> Maybe T.Text -> FilePath -> LSP (Maybe Module) +parseProjectFile currentFile msrc p + | p == currentFile = case msrc of + Just src -> parseOr (parseModuleSafe src) + Nothing -> parseOr (parseModuleFile p) + | otherwise = parseOr (parseModuleFile p) + where + parseOr act = either (const Nothing) Just <$> liftIO act + +-- | A signature for the hover code block. A long function type is split +-- with one parameter per line, in the style rzk definitions are written: +-- +-- > is-equiv +-- > : ( A : U) +-- > → ( B : U) +-- > → ( f : A → B) +-- > → U +formatSignature :: String -> Term -> String +formatSignature name ty + | length inline <= 60 = name ++ " : " ++ inline + | (piParams@(_ : _), ret) <- peelPi ty = + intercalate "\n" (name : zipWith (++) (" : " : repeat " → ") (piParams ++ [printTree ret])) + | otherwise = name ++ " : " ++ inline + where + inline = printTree ty + peelPi (TypeFun _ param ret) = let (ps, r) = peelPi ret in (printTree param : ps, r) + peelPi (ASCII_TypeFun _ param ret) = let (ps, r) = peelPi ret in (printTree param : ps, r) + peelPi r = ([], r) + +provideHover :: Handler LSP 'Method_TextDocumentHover +provideHover req res = do + let uri' = req ^. params . textDocument . uri + pos = fromLspPosition (req ^. params . position) + currentFile = fromMaybe "" $ uriToFilePath uri' + referenceIndex <- indexProject currentFile + case RefInd.lookupAt referenceIndex (fromLspUri uri') pos of + Nothing -> res $ Right $ InR Null + Just binding -> do + cached <- getCachedTypecheckedModules + let body = hoverContent binding cached + res $ Right $ InL $ Hover + (InL (MarkupContent MarkupKind_Markdown body)) + (Just (toLspRange (RefInd.locationRange (RefInd.bindingDef binding)))) + where + hoverContent binding cached = + T.pack (file ++ "\n\n```rzk\n" ++ signature ++ "\n```") + where + file = RefInd.locationPath (RefInd.bindingDef binding) + name = RefInd.bindingName binding + defLine = RefInd.positionLine (RefInd.rangeStart (RefInd.locationRange (RefInd.bindingDef binding))) + decls = maybe [] cachedModuleDecls (lookup file cached) + -- The elaborated type is the default: for a local binder, from the + -- binder-type walk over the cached declarations; for a top-level + -- name, from the declaration itself (preferring the one on the same + -- line, so that a local that shadows a global does not show the + -- global's type). The surface annotation from the reference index is + -- the fallback, e.g. for mid-edit or ill-typed code with no cache. + defCol = RefInd.positionCharacter (RefInd.rangeStart (RefInd.locationRange (RefInd.bindingDef binding))) + -- All cached declarations go in scope, so that splitting a pair + -- binder can unfold defined Σ-types from any file of the project. + allDecls = concatMap (cachedModuleDecls . snd) cached + elaboratedLocal = lookup (defLine, defCol) + [ ((l - 1, c - 1), t) + | (v, t) <- binderTypesInScopeOf allDecls decls + , let VarIdent (RzkPosition _path mpos) _ = getVarIdent v + , Just (l, c) <- [mpos] + ] + signature = case elaboratedLocal of + Just (TypeView t) -> formatSignature (T.unpack name) (fromTerm' t) + Just (ShapeView c tope) -> T.unpack name ++ " : " ++ show c ++ " | " ++ show tope + Nothing -> case find declOnSameLine decls of + Just (Decl _ ty _ _ _ _) -> formatSignature (T.unpack name) (fromTerm' (untyped ty)) + Nothing -> case RefInd.bindingType binding of + Just ann -> T.unpack name ++ " : " ++ T.unpack ann + Nothing -> case find declWithName decls of + Just (Decl _ ty _ _ _ _) -> formatSignature (T.unpack name) (fromTerm' (untyped ty)) + Nothing -> T.unpack name ++ " : ?" + declWithName (Decl v _ _ _ _ _) = + T.pack (printTree (getVarIdent v)) == name + declOnSameLine d@(Decl _ _ _ _ _ mloc) = + declWithName d && (locationLine =<< mloc) == Just (defLine + 1) + +-- | The printed name of a declaration and the range of its defining +-- occurrence, shared by the document and workspace symbol providers. +declNameRange :: Decl' -> (T.Text, Range) +declNameRange (Decl name _ _ _ _ _) = (T.pack (printTree ident), range) + where + ident = getVarIdent name + VarIdent pos _ = ident + RzkPosition _path pos' = pos + (line, col) = fromMaybe (0, 0) pos' + len = length (printTree ident) + pos0 = Position (fromIntegral (max 0 (line - 1))) (fromIntegral (max 0 (col - 1))) + end = Position (fromIntegral (max 0 (line - 1))) (fromIntegral (max 0 (col - 1) + len)) + range = Range pos0 end + +provideSymbols :: Handler LSP 'Method_TextDocumentDocumentSymbol +provideSymbols req res = do + let currentFile = fromMaybe "" $ uriToFilePath $ req ^. params . textDocument . uri + cachedModules <- getCachedTypecheckedModules + let decls = maybe [] cachedModuleDecls (lookup currentFile cachedModules) + res $ Right $ InR $ InL $ map declToSymbol decls + where + declToSymbol :: Decl' -> DocumentSymbol + declToSymbol decl@(Decl _ type' _ _ _ _loc) = DocumentSymbol + { _name = symbolName + , _detail = Just (T.pack (show (untyped type'))) + , _kind = SymbolKind_Function + , _tags = Nothing + , _deprecated = Nothing + , _range = range + , _selectionRange = range + , _children = Nothing + } + where + (symbolName, range) = declNameRange decl + +-- | Workspace-wide symbol search over every typechecked module in the cache. +-- The query is matched case-insensitively as an infix of the definition name; +-- an empty query lists all definitions (clients filter further as the user +-- types). +provideWorkspaceSymbols :: Handler LSP 'Method_WorkspaceSymbol +provideWorkspaceSymbols req res = do + let symbolQuery = T.toLower (req ^. params . query) + cachedModules <- getCachedTypecheckedModules + let symbols = + [ WorkspaceSymbol + { _name = symbolName + , _kind = SymbolKind_Function + , _tags = Nothing + , _containerName = Nothing + , _location = InL (Location (filePathToUri path) range) + , _data_ = Nothing + } + | (path, cachedModule) <- cachedModules + , decl <- cachedModuleDecls cachedModule + , let (symbolName, range) = declNameRange decl + , symbolQuery `T.isInfixOf` T.toLower symbolName + ] + res $ Right $ InR $ InL symbols + + data IsChanged = HasChanged | NotChanged @@ -407,15 +740,21 @@ then dropWhileM p xs else return (x:xs) +-- | The cache eviction and the re-typecheck run on the typecheck worker +-- thread, so this handler returns immediately and later requests (e.g. a +-- formatting request from format-on-save) are answered while the project +-- re-check is still running. Spawning the worker cancels the previous one, +-- so a newer change restarts the re-check. handleFilesChanged :: Handler LSP 'Method_WorkspaceDidChangeWatchedFiles handleFilesChanged msg = do let modifiedPaths = msg ^.. params . changes . traverse . uri . to uriToFilePath . _Just - if any ("rzk.yaml" `isSuffixOf`) modifiedPaths - then do - logDebug "rzk.yaml modified. Clearing module cache" - resetCacheForAllFiles - else do - cache <- getCachedTypecheckedModules - actualModified <- dropWhileM (hasNotChanged cache) modifiedPaths - resetCacheForFiles actualModified - typecheckFromConfigFile + spawnTypecheckWorker $ do + if any ("rzk.yaml" `isSuffixOf`) modifiedPaths + then do + logDebug "rzk.yaml modified. Clearing module cache" + resetCacheForAllFiles + else do + cache <- getCachedTypecheckedModules + actualModified <- dropWhileM (hasNotChanged cache) modifiedPaths + resetCacheForFiles actualModified + typecheckFromConfigFile 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 @@ -24,7 +24,8 @@ handlers :: Handlers LSP handlers = mconcat - [ notificationHandler SMethod_Initialized $ const typecheckFromConfigFile + [ notificationHandler SMethod_Initialized $ const $ + spawnTypecheckWorker typecheckFromConfigFile -- TODO: add logging -- Empty handlers to silence the errors , notificationHandler SMethod_TextDocumentDidOpen $ \_msg -> pure () @@ -37,14 +38,15 @@ return () -- FIXME: typecheck standalone files (if they are not a part of the project) -- An empty hadler is needed to silence the error since it is already handled by the LSP package , notificationHandler SMethod_WorkspaceDidChangeConfiguration $ const $ pure () - -- , requestHandler SMethod_TextDocumentHover $ \req responder -> do - -- TODO: Read from the list of symbols that is supposed to be cached by the typechecker - -- let TRequestMessage _ _ _ (HoverParams _doc pos _workDone) = req - -- Position _l _c' = pos - -- rsp = Hover (InL ms) (Just range') - -- ms = mkMarkdown "Hello world" - -- range' = Range pos pos - -- responder (Right $ InL rsp) + -- Progress cancellation is handled by the lsp library's bookkeeping (it + -- cancels the corresponding withProgress action); the empty handler only + -- silences the missing-handler warning. + , notificationHandler SMethod_WindowWorkDoneProgressCancel $ const $ pure () + , requestHandler SMethod_TextDocumentHover provideHover + , requestHandler SMethod_TextDocumentDocumentSymbol provideSymbols + , requestHandler SMethod_WorkspaceSymbol provideWorkspaceSymbols + , requestHandler SMethod_TextDocumentDefinition findDefinition + , requestHandler SMethod_TextDocumentReferences findReferences , requestHandler SMethod_TextDocumentCompletion provideCompletions , requestHandler SMethod_TextDocumentSemanticTokensFull provideSemanticTokens , requestHandler SMethod_TextDocumentFormatting formatDocument diff --git a/src/Language/Rzk/VSCode/ReferenceIndex.hs b/src/Language/Rzk/VSCode/ReferenceIndex.hs new file mode 100644 --- /dev/null +++ b/src/Language/Rzk/VSCode/ReferenceIndex.hs @@ -0,0 +1,453 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + +module Language.Rzk.VSCode.ReferenceIndex ( + Uri (..), + Position (..), + Range (..), + Location (..), + Binding (..), + ReferenceIndex (..), + indexModules, + lookupAt, + bindingSites, + locationPath, +) where + +import Control.Applicative ((<|>)) +import Data.Bifunctor (bimap) +import qualified Data.Map.Strict as Map +import Data.Maybe (listToMaybe) +import qualified Data.Text as T + +import qualified Free.Scoped as Scoped +import qualified Language.Rzk.Free.Syntax as Free +import qualified Language.Rzk.Syntax as Rzk + +data Uri = Uri + { uriPath :: FilePath + } + deriving (Eq, Ord, Show) + +data Position = Position + { positionLine :: Int + , positionCharacter :: Int + } + deriving (Eq, Ord, Show) + +data Range = Range + { rangeStart :: Position + , rangeEnd :: Position + } + deriving (Eq, Ord, Show) + +data Location = Location + { locationUri :: Uri + , locationRange :: Range + } + deriving (Eq, Ord, Show) + +data Binding = Binding + { bindingName :: T.Text + , bindingDef :: Location + , bindingType :: Maybe T.Text + -- ^ The printed surface annotation of the binder, when it has one + -- (e.g. @A@ for @(x : A)@, @I | φ t@ for @(t : I | φ t)@). Top-level + -- names carry 'Nothing'; their elaborated type comes from the + -- typecheck cache instead. + , bindingRefs :: [Location] + } + deriving (Eq, Show) + +newtype ReferenceIndex = ReferenceIndex + { occurrences :: Map.Map (FilePath, Int) [(Int, Int, Binding)] + -- ^ Every occurrence (definition or reference), keyed by file and line, + -- as column spans; identifiers never span lines. This is what makes + -- 'lookupAt' a map lookup rather than a scan over all bindings. + } + deriving (Show) + +-- | One resolved occurrence: name, definition site, occurrence site, and +-- (for the self-link of a binder) its printed type annotation. +data Link = Link T.Text Location Location (Maybe T.Text) + +-- | Names in scope. Locals shadow globals by insertion. +type Env = Map.Map T.Text Location + +varText :: Rzk.VarIdent' a -> T.Text +varText (Rzk.VarIdent _ (Rzk.VarIdentToken t)) = t + +identLoc :: FilePath -> Rzk.VarIdent -> Maybe Location +identLoc file (Rzk.VarIdent pos (Rzk.VarIdentToken name)) = case pos of + Just (l, c) -> + let l0 = max 0 (l - 1) + c0 = max 0 (c - 1) + c1 = c0 + T.length name + in Just (Location (Uri { uriPath = file }) (Range (Position l0 c0) (Position l0 c1))) + Nothing -> Nothing + +locationPath :: Location -> FilePath +locationPath (Location u _) = uriPath u + +bindingSites :: Binding -> [Location] +bindingSites b = bindingDef b : bindingRefs b + +lookupAt :: ReferenceIndex -> Uri -> Position -> Maybe Binding +lookupAt index (Uri path) (Position l c) = + case Map.lookup (path, l) (occurrences index) of + Nothing -> Nothing + Just spans -> listToMaybe [ b | (s, e, b) <- spans, s <= c, c < e ] + +indexModules :: [(FilePath, Rzk.Module)] -> ReferenceIndex +indexModules modules = group $ + concat [ goCommand file env0 c | (file, m) <- modules, c <- moduleCommands m ] + where + -- On duplicate names, the first definition wins (as scope lookup would). + env0 = Map.fromListWith (\_new old -> old) + [ (varText v, loc) + | (file, m) <- modules, v <- globalNames m, Just loc <- [identLoc file v] ] + group links = ReferenceIndex + { occurrences = Map.fromListWith (++) + [ ((path, l), [(s, e, b)]) + | b <- bs + , Location (Uri path) (Range (Position l s) (Position _ e)) <- bindingSites b + ] + } + where + -- Binders produce a self-link (definition site linked to itself) so + -- that every binding has a key; keep it out of the reference list, + -- which 'bindingSites' prepends the definition to. + -- Accumulate by prepending (constant time per link) and restore the + -- encounter order with one reverse at the end; appending would be + -- quadratic in the number of references of a binding. + bs = [ Binding n d ann (reverse rs) + | ((n, d), (rs, ann)) <- Map.toList $ Map.fromListWith merge + [ ((n, d), (if r == d then [] else [r], a)) | Link n d r a <- links ] + ] + -- fromListWith combines as f new old: prepend the new references, + -- prefer the earliest annotation (the binder's self-link). + merge (rsNew, aNew) (rsOld, aOld) = (rsNew ++ rsOld, aOld <|> aNew) + +moduleCommands :: Rzk.Module -> [Rzk.Command] +moduleCommands (Rzk.Module _ _ cmds) = cmds + +globalNames :: Rzk.Module -> [Rzk.VarIdent] +globalNames = concatMap cmd . moduleCommands + where + cmd = \case + Rzk.CommandDefine _ name _ _ _ _ -> [name] + Rzk.CommandPostulate _ name _ _ _ -> [name] + Rzk.CommandAssume _ vars _ -> vars + _ -> [] + +use :: FilePath -> Env -> Rzk.VarIdent -> [Link] +use file env v = case (Map.lookup (varText v) env, identLoc file v) of + (Just defLoc, Just occLoc) -> [Link (varText v) defLoc occLoc Nothing] + _ -> [] + +-- | A binder annotation, kept structured so that a pair pattern can be +-- matched against the shape of its type. +data BinderAnn + = AnnType Rzk.Term -- ^ @(x : A)@ + | AnnShape Rzk.Term Rzk.Term -- ^ @(t : I | φ)@ + +typeAnn :: Rzk.Term -> Maybe BinderAnn +typeAnn = Just . AnnType + +shapeAnn :: Rzk.Term -> Rzk.Term -> Maybe BinderAnn +shapeAnn cube tope = Just (AnnShape cube tope) + +printAnn :: BinderAnn -> T.Text +printAnn (AnnType ty) = T.pack (Rzk.printTree ty) +printAnn (AnnShape cube tope) = + T.pack (Rzk.printTree cube ++ " | " ++ Rzk.printTree tope) + +-- | Decompose the annotation of a pair pattern into annotations of the two +-- components, through the scoped core: a cube product splits into its two +-- sides, and for a Σ-type the first component gets the base while the second +-- gets the family instantiated at the first component (@q : B p@, not +-- @q : B x@). Substitution in the core is capture-avoiding. For a shape +-- annotation, the tope constrains the components jointly, so the components +-- only inherit their cube. +splitPairAnn :: Rzk.Term -> BinderAnn -> Maybe (BinderAnn, BinderAnn) +splitPairAnn firstComp (AnnShape cube _tope) = splitPairAnn firstComp (AnnType cube) +splitPairAnn firstComp (AnnType ty) = case Free.toTerm' ty of + Free.CubeProduct a b -> Just (fromCore a, fromCore b) + Free.TypeSigma _ _ a scope -> + Just ( fromCore a + , fromCore (reduceProjections (Scoped.substitute (Free.toTerm' firstComp) scope)) + ) + _ -> Nothing + where + fromCore = AnnType . Free.fromTerm' + +-- | Reduce projections of literal pairs (π₁ (a, b) → a). A pattern binder +-- refers to its components through projections, so substituting a pair for +-- it leaves these redexes behind. +reduceProjections :: Scoped.FS Free.TermF a -> Scoped.FS Free.TermF a +reduceProjections = \case + Scoped.Pure x -> Scoped.Pure x + Scoped.Free f -> case Scoped.Free (bimap reduceProjections reduceProjections f) of + Free.First (Free.Pair a _) -> a + Free.Second (Free.Pair _ b) -> b + t -> t + +-- | A pattern as the term it matches. +patternTerm :: Rzk.Pattern -> Rzk.Term +patternTerm = \case + Rzk.PatternUnit loc -> Rzk.Unit loc + Rzk.PatternVar loc v -> Rzk.Var loc v + Rzk.PatternPair loc a b -> Rzk.Pair loc (patternTerm a) (patternTerm b) + Rzk.PatternTuple loc a b cs -> Rzk.Tuple loc (patternTerm a) (patternTerm b) (map patternTerm cs) + +bindVars :: FilePath -> Env -> [(Rzk.VarIdent, Maybe T.Text)] -> (Env, [Link]) +bindVars file env vs = + ( Map.union (Map.fromListWith (\_new old -> old) [ (n, loc) | (n, loc, _) <- binds ]) env + , [ Link n loc loc ann | (n, loc, ann) <- binds ] + ) + where + binds = [ (varText v, loc, ann) | (v, ann) <- vs, Just loc <- [identLoc file v] ] + +bindPat :: FilePath -> Env -> Maybe BinderAnn -> Rzk.Pattern -> (Env, [Link]) +bindPat file env ann = bindVars file env . annotatedPatternVars ann + +-- | Distribute an annotation over a pattern: a plain variable inherits it, +-- a pair pattern splits it along the type when the type's shape allows. +-- Tuples desugar to left-nested pairs, matching both 'Free.toTerm'''s +-- treatment of tuple patterns and its translation of Σ-tuples. +annotatedPatternVars :: Maybe BinderAnn -> Rzk.Pattern -> [(Rzk.VarIdent, Maybe T.Text)] +annotatedPatternVars ann = \case + Rzk.PatternUnit _ -> [] + Rzk.PatternVar _ v -> [(v, printAnn <$> ann)] + Rzk.PatternPair _ a b -> case ann >>= splitPairAnn (patternTerm a) of + Just (annA, annB) -> + annotatedPatternVars (Just annA) a ++ annotatedPatternVars (Just annB) b + Nothing -> + annotatedPatternVars Nothing a ++ annotatedPatternVars Nothing b + Rzk.PatternTuple loc a b cs -> + -- Reuse the core's own tuple desugaring (left-nested pairs), so this + -- split cannot drift from how toTerm' scopes tuple patterns. + annotatedPatternVars ann (Free.desugarTuple loc (reverse cs) b a) + +annotatedTermPatVars :: Maybe BinderAnn -> Rzk.Term -> [(Rzk.VarIdent, Maybe T.Text)] +annotatedTermPatVars ann = \case + Rzk.Var _ v -> [(v, printAnn <$> ann)] + Rzk.Pair _ a b -> case ann >>= splitPairAnn a of + Just (annA, annB) -> + annotatedTermPatVars (Just annA) a ++ annotatedTermPatVars (Just annB) b + Nothing -> + annotatedTermPatVars Nothing a ++ annotatedTermPatVars Nothing b + Rzk.Tuple loc a b cs -> + annotatedTermPatVars ann (tuplePairs loc a b cs) + t -> [ (v, Nothing) | v <- termPatVars t ] + +-- | A tuple term as left-nested pairs, following the treatment of tuples in +-- 'Free.toTerm''. +tuplePairs :: a -> Rzk.Term' a -> Rzk.Term' a -> [Rzk.Term' a] -> Rzk.Term' a +tuplePairs loc t1 t2 [] = Rzk.Pair loc t1 t2 +tuplePairs loc t1 t2 (t : ts) = tuplePairs loc (Rzk.Pair loc t1 t2) t ts + +termPatVars :: Rzk.Term -> [Rzk.VarIdent] +termPatVars = \case + Rzk.Var _ v -> [v] + Rzk.Pair _ a b -> termPatVars a ++ termPatVars b + Rzk.Tuple _ a b cs -> concatMap termPatVars (a : b : cs) + _ -> [] + +goCommand :: FilePath -> Env -> Rzk.Command -> [Link] +goCommand file env = \case + Rzk.CommandDefine _ name _ ps ty body -> + let (env', occs) = goParams file env ps + in def name ++ occs ++ goTerm file env' ty ++ goTerm file env' body + Rzk.CommandPostulate _ name _ ps ty -> + let (env', occs) = goParams file env ps + in def name ++ occs ++ goTerm file env' ty + -- Assumptions (#assume, #variable, #variables) carry their declared type + -- as the annotation; unlike #define, nothing is elaborated away. + Rzk.CommandAssume _ vars ty -> + [ Link (varText v) loc loc (Just (printAnn (AnnType ty))) + | v <- vars, Just loc <- [identLoc file v] ] + ++ goTerm file env ty + Rzk.CommandCheck _ a b -> goTerm file env a ++ goTerm file env b + Rzk.CommandCompute _ a -> goTerm file env a + Rzk.CommandComputeWHNF _ a -> goTerm file env a + Rzk.CommandComputeNF _ a -> goTerm file env a + Rzk.CommandSetOption{} -> [] + Rzk.CommandUnsetOption{} -> [] + Rzk.CommandSection{} -> [] + Rzk.CommandSectionEnd{} -> [] + where + def v = [ Link (varText v) loc loc Nothing | Just loc <- [identLoc file v] ] + +goTerm :: FilePath -> Env -> Rzk.Term -> [Link] +goTerm file env = \case + Rzk.Var _ v -> use file env v + Rzk.Hole _ _ -> [] + + Rzk.Lambda _ ps body -> paramScope file env ps body + Rzk.ASCII_Lambda _ ps body -> paramScope file env ps body + Rzk.Let _ bind val body -> letScope file env bind val body + Rzk.LetMod _ _ bind val body -> letScope file env bind val body + Rzk.TypeSigma _ pat ty ret -> sigmaScope file env pat ty ret + Rzk.ASCII_TypeSigma _ pat ty ret -> sigmaScope file env pat ty ret + Rzk.TypeSigmaModal _ pat _ ty ret -> sigmaScope file env pat ty ret + Rzk.TypeSigmaTuple _ sp sps ret -> sigmaTupleScope file env (sp : sps) ret + Rzk.ASCII_TypeSigmaTuple _ sp sps ret -> sigmaTupleScope file env (sp : sps) ret + Rzk.TypeFun _ pd ret -> paramDeclScope file env pd ret + Rzk.ASCII_TypeFun _ pd ret -> paramDeclScope file env pd ret + Rzk.TypeExtensionDeprecated _ pd ty -> paramDeclScope file env pd ty + Rzk.ASCII_TypeExtensionDeprecated _ pd ty -> paramDeclScope file env pd ty + + Rzk.CubeProduct _ a b -> goTerm file env a ++ goTerm file env b + Rzk.TopeEQ _ a b -> goTerm file env a ++ goTerm file env b + Rzk.TopeLEQ _ a b -> goTerm file env a ++ goTerm file env b + Rzk.TopeAnd _ a b -> goTerm file env a ++ goTerm file env b + Rzk.TopeOr _ a b -> goTerm file env a ++ goTerm file env b + Rzk.ASCII_TopeEQ _ a b -> goTerm file env a ++ goTerm file env b + Rzk.ASCII_TopeLEQ _ a b -> goTerm file env a ++ goTerm file env b + Rzk.ASCII_TopeAnd _ a b -> goTerm file env a ++ goTerm file env b + Rzk.ASCII_TopeOr _ a b -> goTerm file env a ++ goTerm file env b + Rzk.TopeInv _ a -> goTerm file env a + Rzk.TopeUninv _ a -> goTerm file env a + Rzk.CubeFlip _ a -> goTerm file env a + Rzk.CubeUnflip _ a -> goTerm file env a + Rzk.RecOr _ rs -> concatMap (restriction file env) rs + Rzk.RecOrDeprecated _ a b c d -> concatMap (goTerm file env) [a, b, c, d] + Rzk.TypeId _ a b c -> concatMap (goTerm file env) [a, b, c] + Rzk.TypeIdSimple _ a b -> goTerm file env a ++ goTerm file env b + Rzk.TypeRestricted _ a rs -> goTerm file env a ++ concatMap (restriction file env) rs + Rzk.App _ a b -> goTerm file env a ++ goTerm file env b + Rzk.Pair _ a b -> goTerm file env a ++ goTerm file env b + Rzk.Tuple _ a b cs -> concatMap (goTerm file env) (a : b : cs) + Rzk.ModApp _ _ a -> goTerm file env a + Rzk.ModType _ _ a -> goTerm file env a + Rzk.ModExtract _ _ a -> goTerm file env a + Rzk.First _ a -> goTerm file env a + Rzk.Second _ a -> goTerm file env a + Rzk.ASCII_First _ a -> goTerm file env a + Rzk.ASCII_Second _ a -> goTerm file env a + Rzk.ReflTerm _ a -> goTerm file env a + Rzk.ReflTermType _ a b -> goTerm file env a ++ goTerm file env b + Rzk.IdJ _ a b c d e f -> concatMap (goTerm file env) [a, b, c, d, e, f] + Rzk.TypeAsc _ a b -> goTerm file env a ++ goTerm file env b + + Rzk.Universe{} -> [] + Rzk.UniverseCube{} -> [] + Rzk.UniverseTope{} -> [] + Rzk.CubeUnit{} -> [] + Rzk.CubeUnitStar{} -> [] + Rzk.Cube2{} -> [] + Rzk.Cube2_0{} -> [] + Rzk.Cube2_1{} -> [] + Rzk.CubeI{} -> [] + Rzk.CubeI_0{} -> [] + Rzk.CubeI_1{} -> [] + Rzk.TopeTop{} -> [] + Rzk.TopeBottom{} -> [] + Rzk.RecBottom{} -> [] + Rzk.TypeUnit{} -> [] + Rzk.Unit{} -> [] + Rzk.Refl{} -> [] + Rzk.ASCII_CubeUnitStar{} -> [] + Rzk.ASCII_Cube2_0{} -> [] + Rzk.ASCII_Cube2_1{} -> [] + Rzk.ASCII_CubeI{} -> [] + Rzk.ASCII_CubeI_0{} -> [] + Rzk.ASCII_CubeI_1{} -> [] + Rzk.ASCII_TopeTop{} -> [] + Rzk.ASCII_TopeBottom{} -> [] + +paramScope :: FilePath -> Env -> [Rzk.Param] -> Rzk.Term -> [Link] +paramScope file env ps body = + let (env', occs) = goParams file env ps in occs ++ goTerm file env' body + +letScope :: FilePath -> Env -> Rzk.Bind -> Rzk.Term -> Rzk.Term -> [Link] +letScope file env bind val body = + let (env', occs) = goBind file env bind + in goTerm file env val ++ occs ++ goTerm file env' body + +sigmaScope :: FilePath -> Env -> Rzk.Pattern -> Rzk.Term -> Rzk.Term -> [Link] +sigmaScope file env pat ty ret = + let (env', occs) = bindPat file env (typeAnn ty) pat + in goTerm file env ty ++ occs ++ goTerm file env' ret + +sigmaTupleScope :: FilePath -> Env -> [Rzk.SigmaParam] -> Rzk.Term -> [Link] +sigmaTupleScope file env sps ret = + let (env', occs) = goSigmaParams file env sps in occs ++ goTerm file env' ret + +paramDeclScope :: FilePath -> Env -> Rzk.ParamDecl -> Rzk.Term -> [Link] +paramDeclScope file env pd ret = + let (env', occs) = goParamDecl file env pd in occs ++ goTerm file env' ret + +restriction :: FilePath -> Env -> Rzk.Restriction -> [Link] +restriction file env = \case + Rzk.Restriction _ a b -> goTerm file env a ++ goTerm file env b + Rzk.ASCII_Restriction _ a b -> goTerm file env a ++ goTerm file env b + +goBind :: FilePath -> Env -> Rzk.Bind -> (Env, [Link]) +goBind file env = \case + Rzk.BindPattern _ pat -> bindPat file env Nothing pat + Rzk.BindPatternType _ pat ty -> + let (env', occs) = bindPat file env (typeAnn ty) pat in (env', goTerm file env ty ++ occs) + +goParams :: FilePath -> Env -> [Rzk.Param] -> (Env, [Link]) +goParams _ env [] = (env, []) +goParams file env (p : ps) = + let (env1, o1) = goParam file env p + (env2, o2) = goParams file env1 ps + in (env2, o1 ++ o2) + +goParam :: FilePath -> Env -> Rzk.Param -> (Env, [Link]) +goParam file env = \case + Rzk.ParamPattern _ pat -> bindPat file env Nothing pat + Rzk.ParamPatternType _ pats ty -> + let (env', occs) = bindVars file env (concatMap (annotatedPatternVars (typeAnn ty)) pats) + in (env', goTerm file env ty ++ occs) + Rzk.ParamPatternShape _ pats cube tope -> + let (env', occs) = bindVars file env (concatMap (annotatedPatternVars (shapeAnn cube tope)) pats) + in (env', goTerm file env cube ++ occs ++ goTerm file env' tope) + Rzk.ParamPatternShapeDeprecated _ pat cube tope -> + let (env', occs) = bindPat file env (shapeAnn cube tope) pat + in (env', goTerm file env cube ++ occs ++ goTerm file env' tope) + Rzk.ParamPatternModalType _ pats _ ty -> + let (env', occs) = bindVars file env (concatMap (annotatedPatternVars (typeAnn ty)) pats) + in (env', goTerm file env ty ++ occs) + Rzk.ParamPatternModalShape _ pats _ cube tope -> + let (env', occs) = bindVars file env (concatMap (annotatedPatternVars (shapeAnn cube tope)) pats) + in (env', goTerm file env cube ++ occs ++ goTerm file env' tope) + +goParamDecl :: FilePath -> Env -> Rzk.ParamDecl -> (Env, [Link]) +goParamDecl file env = \case + Rzk.ParamType _ ty -> (env, goTerm file env ty) + Rzk.ParamTermType _ patTerm ty -> + let (env', occs) = bindVars file env (annotatedTermPatVars (typeAnn ty) patTerm) + in (env', goTerm file env ty ++ occs) + Rzk.ParamTermShape _ patTerm cube tope -> + let (env', occs) = bindVars file env (annotatedTermPatVars (shapeAnn cube tope) patTerm) + in (env', goTerm file env cube ++ occs ++ goTerm file env' tope) + Rzk.ParamTermTypeDeprecated _ pat ty -> + let (env', occs) = bindPat file env (typeAnn ty) pat + in (env', goTerm file env ty ++ occs) + Rzk.ParamVarShapeDeprecated _ pat cube tope -> + let (env', occs) = bindPat file env (shapeAnn cube tope) pat + in (env', goTerm file env cube ++ occs ++ goTerm file env' tope) + Rzk.ParamTermModalType _ patTerm _ ty -> + let (env', occs) = bindVars file env (annotatedTermPatVars (typeAnn ty) patTerm) + in (env', goTerm file env ty ++ occs) + Rzk.ParamTermModalShape _ patTerm _ cube tope -> + let (env', occs) = bindVars file env (annotatedTermPatVars (shapeAnn cube tope) patTerm) + in (env', goTerm file env cube ++ occs ++ goTerm file env' tope) + +goSigmaParams :: FilePath -> Env -> [Rzk.SigmaParam] -> (Env, [Link]) +goSigmaParams _ env [] = (env, []) +goSigmaParams file env (p : ps) = + let (env1, o1) = goSigmaParam file env p + (env2, o2) = goSigmaParams file env1 ps + in (env2, o1 ++ o2) + +goSigmaParam :: FilePath -> Env -> Rzk.SigmaParam -> (Env, [Link]) +goSigmaParam file env = \case + Rzk.SigmaParam _ pat ty -> + let (env', occs) = bindPat file env (typeAnn ty) pat in (env', goTerm file env ty ++ occs) + Rzk.SigmaParamModal _ pat _ ty -> + let (env', occs) = bindPat file env (typeAnn ty) pat in (env', goTerm file env ty ++ occs) diff --git a/src/Language/Rzk/VSCode/Tokenize.hs b/src/Language/Rzk/VSCode/Tokenize.hs --- a/src/Language/Rzk/VSCode/Tokenize.hs +++ b/src/Language/Rzk/VSCode/Tokenize.hs @@ -2,10 +2,18 @@ {-# LANGUAGE OverloadedStrings #-} module Language.Rzk.VSCode.Tokenize where +import Data.Char (isAlphaNum) +import Data.List (sortOn) +import qualified Data.Text as T import Language.LSP.Protocol.Types (SemanticTokenAbsolute (..), SemanticTokenModifiers (..), SemanticTokenTypes (..)) import Language.Rzk.Syntax +import Language.Rzk.Syntax.Lex (Posn (Pn), + Tok (T_HoleIdentToken, TK), + TokSymbol (TokSymbol), + Token (PT)) +import qualified Language.Rzk.Syntax.Lex as Lex tokenizeModule :: Module -> [SemanticTokenAbsolute] tokenizeModule (Module _loc langDecl commands) = concat @@ -25,13 +33,15 @@ CommandComputeNF _loc term -> tokenizeTerm term CommandComputeWHNF _loc term -> tokenizeTerm term - CommandPostulate _loc name _declUsedVars params type_ -> concat + CommandPostulate _loc name declUsedVars params type_ -> concat [ mkToken name SemanticTokenTypes_Function [SemanticTokenModifiers_Declaration] + , tokenizeDeclUsedVars declUsedVars , foldMap tokenizeParam params , tokenizeTerm type_ ] - CommandDefine _loc name _declUsedVars params type_ term -> concat + CommandDefine _loc name declUsedVars params type_ term -> concat [ mkToken name SemanticTokenTypes_Function [SemanticTokenModifiers_Declaration] + , tokenizeDeclUsedVars declUsedVars , foldMap tokenizeParam params , foldMap tokenizeTerm [type_, term] ] @@ -40,9 +50,18 @@ [ foldMap (\var -> mkToken var SemanticTokenTypes_Parameter [SemanticTokenModifiers_Declaration]) vars , tokenizeTerm type_ ] - CommandSection _loc _nameStart -> [] - CommandSectionEnd _loc _nameEnd -> [] + CommandSection _loc name -> tokenizeSectionName name + CommandSectionEnd _loc name -> tokenizeSectionName name +tokenizeDeclUsedVars :: DeclUsedVars -> [SemanticTokenAbsolute] +tokenizeDeclUsedVars (DeclUsedVars _loc vars) = + foldMap (\var -> mkToken var SemanticTokenTypes_Parameter []) vars + +tokenizeSectionName :: SectionName -> [SemanticTokenAbsolute] +tokenizeSectionName = \case + NoSectionName{} -> [] + SomeSectionName _ name -> mkToken name SemanticTokenTypes_Property [] + tokenizeBind :: Bind -> [SemanticTokenAbsolute] tokenizeBind = \case BindPattern _loc pat -> tokenizePattern pat @@ -89,7 +108,7 @@ tokenizeTerm' varTokenType = go where go term = case term of - Hole{} -> [] -- FIXME + Hole{} -> [] -- highlighted from the token stream ('tokenizeSyntaxSymbols') Var{} -> case varTokenType of Nothing -> [] Just token_type -> mkToken term token_type [] @@ -285,3 +304,68 @@ , _length = fromIntegral $ Prelude.length (printTree x) } ] + +-- * Syntax highlighting from the token stream + +-- | Highlight the fixed syntax of the language (command names, reserved +-- words, operators) and holes directly from the lexer token stream. +-- +-- This complements 'tokenizeModule', which highlights identifiers and +-- special term formers from the parsed module. Fixed symbols do not need +-- parsing at all: a @:=@ is a @:=@ wherever it occurs, and a hole @?@ (or +-- @?name@) is its own lexer token. Working on the token stream means that +-- the grammar (and the abstract syntax) does not have to track positions of +-- keywords, and that highlighting keeps working for files that +-- (temporarily) fail to parse. +tokenizeSyntaxSymbols :: T.Text -> [SemanticTokenAbsolute] +tokenizeSyntaxSymbols input = + [ SemanticTokenAbsolute + { _tokenType = tokenType + , _tokenModifiers = [] + , _line = fromIntegral line - 1 -- NOTE: 0-indexed output for LSP + , _startChar = fromIntegral col - 1 -- NOTE: 0-indexed output for LSP + , _length = fromIntegral (T.length sym) + } + | PT (Pn _ line col) tok <- Lex.tokens (tryExtractMarkdownCodeBlocks "rzk" input) + , Just (sym, tokenType) <- [classifyToken tok] + ] + +-- | How to highlight a lexer token, if at all: fixed symbols by +-- 'classifySymbol', holes as a distinct token. Identifiers are left to the +-- AST pass ('tokenizeModule'), which knows their role. +classifyToken :: Tok -> Maybe (T.Text, SemanticTokenTypes) +classifyToken = \case + TK (TokSymbol sym _) -> (,) sym <$> classifySymbol sym + -- Holes are goals to come back to, so they should stand out; among the + -- standard token types, regexp is rendered most distinctly by the default + -- themes (themes and clients may restyle it). + T_HoleIdentToken sym -> Just (sym, SemanticTokenTypes_Regexp) + _ -> Nothing + +-- | How to highlight a fixed symbol of the grammar, if at all. +classifySymbol :: T.Text -> Maybe SemanticTokenTypes +classifySymbol s + | s `elem` ignored = Nothing + | "#" `T.isPrefixOf` s = Just SemanticTokenTypes_Macro + | s == "rzk-1" = Just SemanticTokenTypes_Macro + | T.any isAlphaNum s = Just SemanticTokenTypes_Keyword + | otherwise = Just SemanticTokenTypes_Operator + where + -- Plain brackets are left to the editor (e.g. bracket pair colorization). + ignored = ["(", ")", "[", "]", "{", "}", ";", "<", ">"] + +-- | Combine tokens from the parsed module with tokens from the raw symbol +-- stream. On overlap (same start position) the AST-based token wins, since +-- it carries more precise semantics (e.g. @unit@ as an enum member rather +-- than a keyword). The result is sorted by position, as required for the +-- LSP delta encoding. +mergeTokens :: [SemanticTokenAbsolute] -> [SemanticTokenAbsolute] -> [SemanticTokenAbsolute] +mergeTokens astTokens symbolTokens = go (sortOn key astTokens) (sortOn key symbolTokens) + where + key t = (_line t, _startChar t) + go [] ss = ss + go as [] = as + go (a:as) (s:ss) = case compare (key a) (key s) of + LT -> a : go as (s:ss) + EQ -> a : go as ss + GT -> s : go (a:as) ss diff --git a/src/Rzk/TypeCheck.hs b/src/Rzk/TypeCheck.hs --- a/src/Rzk/TypeCheck.hs +++ b/src/Rzk/TypeCheck.hs @@ -40,15 +40,15 @@ fromString = unsafeInferStandalone' . fromString defaultTypeCheck - :: TypeCheck var a - -> Either (TypeErrorInScopedContext var) a + :: TypeCheck VarIdent a + -> Either (TypeErrorInScopedContext VarIdent) a defaultTypeCheck = fmap fst . defaultTypeCheckWithHoles' emptyContext -- | Like 'defaultTypeCheck', but runs in lenient hole mode ('allowHoles') and -- also returns the holes recorded during checking (with their goal and context). defaultTypeCheckWithHoles - :: TypeCheck var a - -> Either (TypeErrorInScopedContext var) (a, [HoleInfo]) + :: TypeCheck VarIdent a + -> Either (TypeErrorInScopedContext VarIdent) (a, [HoleInfo]) defaultTypeCheckWithHoles = defaultTypeCheckWithHoles' (allowHoles emptyContext) defaultTypeCheckWithHoles' @@ -951,7 +951,7 @@ contextEntailsBottom :: Eq var => TypeCheck var Bool contextEntailsBottom = asks localTopesEntailBottom >>= \case Just b -> return b - Nothing -> asks localTopesNF >>= (`entailM` topeBottomT) + Nothing -> entailContextM topeBottomT -- | Ex falso: in a contradictory tope context @recBOT@ inhabits any type, so it -- is a candidate for every goal there (and only there — elsewhere it would not @@ -966,9 +966,8 @@ -- yes\/no query rather than a check that issues an error. coverageHolds :: Eq var => [TermT var] -> TypeCheck var Bool coverageHolds topes = do - contextTopes <- asks localTopesNF - topesNF <- mapM nfTope topes - contextTopes `entailM` foldr topeOrT topeBottomT topesNF + topesNF <- mapM nfTope topes + entailContextM (foldr topeOrT topeBottomT topesNF) -- | Tope case-split moves: ways to build a value of the goal by @recOR@, -- splitting the proof over a cover of the local tope context. Three sources, @@ -1256,6 +1255,17 @@ , scopeVars :: [(var, VarInfo var)] } deriving (Functor, Foldable) +-- | A scope of top-level entries (definitions, postulates, section +-- assumptions). The payload is pinned at 'VarIdent': shifting the context +-- under a binder ('enterScopeContext') maps only the keys and never +-- traverses the elaborated terms, which is what made @S <$>@ on the whole +-- context account for most of the checker's allocation and residency. +-- A payload is embedded into the current scope on lookup via 'globalEmbed'. +data GlobalScopeInfo var = GlobalScopeInfo + { gscopeName :: Maybe Rzk.SectionName + , gscopeVars :: [(var, VarInfo VarIdent)] + } deriving (Functor, Foldable) + addVarToScope :: var -> VarInfo var -> ScopeInfo var -> ScopeInfo var addVarToScope var info ScopeInfo{..} = ScopeInfo { scopeVars = (var, info) : scopeVars, .. } @@ -1316,12 +1326,54 @@ , tTope :: TermT var } deriving (Functor, Foldable, Eq) +-- | The state of the tope-saturation cache in a 'Context' +-- (see 'localTopesSaturated' and 'withRefreshedTopes'). +data CachedSaturation var + = SaturationUncached + -- ^ No cache was installed for this tope context ('entailContextM' + -- falls back to the per-query pipeline). + | SaturationCached (Maybe [[ModalTope var]]) + -- ^ A deferred pipeline run: forced by the first query under this + -- context. 'Nothing' records that the pipeline errored; queries then + -- fall back, so the error surfaces exactly where it would have. + deriving (Functor) + +-- Deliberately empty: the cache's variables duplicate those of +-- 'localTopesNF', and folding a 'Context' (e.g. collecting names when +-- printing a scoped error) must not force the deferred pipeline. +instance Foldable CachedSaturation where + foldMap _ _ = mempty + data Context var = Context { localScopes :: [ScopeInfo var] + -- ^ Binder scopes: variables bound while checking the current + -- declaration. Top-level entries live in 'globalScopes'. + , globalScopes :: [GlobalScopeInfo var] + -- ^ Top-level definitions, postulates and section assumptions, with + -- their payloads pinned at 'VarIdent' (see 'GlobalScopeInfo'). + , globalEmbed :: VarIdent -> var + -- ^ The composed injection of top-level names into the current scope + -- (extended by @S .@ at each binder entry; the derived 'Functor' + -- composes it on 'fmap'). Embeds a global payload on lookup. + , localDiscreteTopes :: [ModalTope var] + -- ^ Discreteness axioms for the flat cube variables in scope (a flat + -- point of @2@ or @I@ is an endpoint). Maintained incrementally at + -- binder entry (see 'enterScopeMaybe'), so 'entailM' does not rescan + -- the whole context on every entailment query. A variable's modality + -- is fixed at binding time ('addModalityToScope' only touches + -- 'modAccum'), so entries never need to be revised. , localTopes :: [ModalTope var] , localTopesNF :: [ModalTope var] , localTopesNFUnion :: [[ModalTope var]] , localTopesEntailBottom :: Maybe Bool + , localTopesSaturated :: CachedSaturation var + -- ^ The saturated alternatives for the context's own tope context + -- ('localTopesNF' plus the discreteness axioms): exactly the + -- preprocessing 'entailM' runs per query, cached at the points where + -- the tope context changes ('localTope', 'enterModality', + -- 'inAllSubContexts', a flat cube binder) via 'withRefreshedTopes'. + -- Ordinary binder entries shift the cached value with the rest of the + -- context, which is sound because saturation commutes with renaming. , actionStack :: [Action var] , currentCommand :: Maybe Rzk.Command , location :: Maybe LocationInfo @@ -1351,8 +1403,23 @@ -- the local hypotheses (see 'withHintLemmas'). A caller (the game) supplies -- a small curated allow-list per level; each listed lemma whose type fits -- the goal is then offered, applied to holes (e.g. @concat ? ? ?@). - } deriving (Functor, Foldable) + } deriving (Functor) +-- Hand-written because the 'globalEmbed' function field cannot be folded; +-- its image is exactly the keys of 'globalScopes', which are folded. +instance Foldable Context where + foldMap f Context{..} = mconcat + [ foldMap (foldMap f) localScopes + , foldMap (foldMap f) globalScopes + , foldMap (foldMap f) localDiscreteTopes + , foldMap (foldMap f) localTopes + , foldMap (foldMap f) localTopesNF + , foldMap (foldMap (foldMap f)) localTopesNFUnion + -- localTopesSaturated is skipped: its Foldable is deliberately empty + -- (folding must not force the deferred saturation pipeline). + , foldMap (foldMap f) actionStack + ] + addVarInCurrentScope :: var -> VarInfo var -> Context var -> Context var addVarInCurrentScope var info Context{..} = Context { localScopes = @@ -1361,18 +1428,35 @@ scope : scopes -> addVarToScope var info scope : scopes , .. } +-- | Add a top-level entry (definition, postulate, section assumption) to the +-- current global scope. Only ever happens at the top level, where variables +-- are plain 'VarIdent's. +addVarInCurrentGlobalScope :: VarIdent -> VarInfo VarIdent -> Context VarIdent -> Context VarIdent +addVarInCurrentGlobalScope var info Context{..} = Context + { globalScopes = + case globalScopes of + [] -> [GlobalScopeInfo Nothing [(var, info)]] + scope : scopes -> scope { gscopeVars = (var, info) : gscopeVars scope } : scopes + , .. } + applyModalityToScopes :: TModality -> [ScopeInfo var] -> [ScopeInfo var] applyModalityToScopes md scopes = map (addModalityToScope md) scopes +applyModalityToGlobalScopes :: TModality -> [GlobalScopeInfo var] -> [GlobalScopeInfo var] +applyModalityToGlobalScopes md = map $ \scope -> scope + { gscopeVars = map (fmap (\VarInfo{..} -> VarInfo{ modAccum = comp modAccum md, .. })) (gscopeVars scope) } + applyModalityToTopes :: TModality -> [ModalTope var] -> [ModalTope var] applyModalityToTopes md topes = map (\ModalTope{..} -> ModalTope{tModAccum = comp tModAccum md, ..}) topes applyModality :: TModality -> Context var -> Context var applyModality md Context{..} = Context { localScopes = applyModalityToScopes md localScopes + , globalScopes = applyModalityToGlobalScopes md globalScopes , localTopes = applyModalityToTopes md localTopes , localTopesNF = applyModalityToTopes md localTopesNF , localTopesNFUnion = map (applyModalityToTopes md) localTopesNFUnion + , localTopesSaturated = SaturationUncached -- accessibility changed; 'enterModality' refreshes , .. } emptyTopeContext :: [ModalTope var] @@ -1383,13 +1467,28 @@ , ModalTope Id Sharp topeTopT ] -emptyContext :: Context var -emptyContext = Context +emptyContext :: Context VarIdent +emptyContext = unseeded { localTopesSaturated = SaturationCached sat } + where + -- Seed the saturation cache for the empty tope context, so top-level + -- entailment queries hit the cached path from the start. Deferred, like + -- every other installation (see 'withRefreshedTopes'). + sat = case runExcept (runWriterT (runReaderT (saturateForEntailment emptyTopeContext) unseeded)) of + Left _ -> Nothing + Right (s, _) -> Just s + unseeded = emptyContextUnseeded + +emptyContextUnseeded :: Context VarIdent +emptyContextUnseeded = Context { localScopes = [ScopeInfo Nothing []] + , globalScopes = [GlobalScopeInfo Nothing []] + , globalEmbed = id + , localDiscreteTopes = [] , localTopes = emptyTopeContext , localTopesNF = emptyTopeContext , localTopesNFUnion = [emptyTopeContext] , localTopesEntailBottom = Just False + , localTopesSaturated = SaturationUncached , actionStack = [] , currentCommand = Nothing , location = Nothing @@ -1451,9 +1550,34 @@ availableTopesNF :: Context var -> [TermT var] availableTopesNF ctx = map tTope $ filterAccessible (localTopesNF ctx) +-- | All in-scope variables: binder-bound locals first, then the top-level +-- entries with their payloads embedded into the current scope. Locals are +-- always more recent than the globals, so this matches the pre-split order. varInfos :: Context var -> [(var, VarInfo var)] varInfos Context{..} = concatMap scopeVars localScopes + <> [ (v, globalEmbed <$> info) + | (v, info) <- concatMap gscopeVars globalScopes ] +-- | Look up one variable's 'VarInfo' by walking the scopes directly. The +-- per-variable lookups ('typeOfVar', 'valueOfVar', …) run on every 'typeOf' +-- of a variable, so going through a projected association list (as the +-- whole-context views below do) allocates a pair per scanned entry on the +-- hottest path of the checker. A hit in the global scopes is embedded into +-- the current scope ('globalEmbed'); the payload itself is never shifted. +lookupVarInfo :: Eq var => var -> Context var -> Maybe (VarInfo var) +lookupVarInfo x Context{..} = go localScopes + where + go [] = goGlobal globalScopes + go (scope : scopes) = + case lookup x (scopeVars scope) of + Just info -> Just info + Nothing -> go scopes + goGlobal [] = Nothing + goGlobal (scope : scopes) = + case lookup x (gscopeVars scope) of + Just info -> Just (globalEmbed <$> info) + Nothing -> goGlobal scopes + varTypes :: Context var -> [(var, TermT var)] varTypes = map (fmap varType) . varInfos @@ -1469,15 +1593,6 @@ varBinders :: Context var -> [(var, Binder)] varBinders = map (fmap varOrig) . varInfos -varModalities :: Context var -> [(var, TModality)] -varModalities = map (fmap varModality) . varInfos - -varLocks :: Context var -> [(var, TModality)] -varLocks = map (fmap modAccum) . varInfos - -varTopLevels :: Context var -> [(var, Bool)] -varTopLevels = map (fmap varIsTopLevel) . varInfos - withPartialDecls :: TypeCheck VarIdent ([Decl'], [err]) -> TypeCheck VarIdent ([Decl'], [err]) @@ -1507,11 +1622,18 @@ startSection :: Maybe Rzk.SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a startSection name = local $ \Context{..} -> Context - { localScopes = ScopeInfo { scopeName = name, scopeVars = [] } : localScopes + { globalScopes = GlobalScopeInfo { gscopeName = name, gscopeVars = [] } : globalScopes , .. } +-- | The current global scope, as a plain 'ScopeInfo' (at the top level the +-- keys and payloads coincide at 'VarIdent'). +askCurrentGlobalScope :: TypeCheck VarIdent (ScopeInfo VarIdent) +askCurrentGlobalScope = asks globalScopes >>= \case + [] -> panicImpossible "no current global scope available" + scope : _scopes -> pure ScopeInfo { scopeName = gscopeName scope, scopeVars = gscopeVars scope } + endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) -endSection errs = askCurrentScope >>= scopeToDecls errs +endSection errs = askCurrentGlobalScope >>= scopeToDecls errs scopeToDecls :: Eq var => [TypeErrorInScopedContext var] -> ScopeInfo var -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var]) scopeToDecls errs ScopeInfo{..} = do @@ -1713,9 +1835,20 @@ -- a pattern binder is shown as its pattern, e.g. (t , s); others by name dispName x = maybe (show (Pure x :: Term')) (show . binderDisplayName) (lookup x fbs) +-- | All display names in scope, read off the raw entries: a binder +-- ('varOrig') never mentions the scope's variables, so no global payload +-- needs embedding. Going through 'varOrigs' here instead embedded every +-- global 'VarInfo' once per new top-level name ('checkTopLevelDuplicate'), +-- quadratically over a project. +scopeNames :: Context var -> [VarIdent] +scopeNames Context{..} = mapMaybe entryName (concatMap scopeVars localScopes) + <> mapMaybe entryName (concatMap gscopeVars globalScopes) + where + entryName :: (v, VarInfo w) -> Maybe VarIdent + entryName = binderName . varOrig . snd + doesShadowName :: VarIdent -> TypeCheck var [VarIdent] -doesShadowName name = asks $ \ctx -> - filter (name ==) (mapMaybe snd (varOrigs ctx)) +doesShadowName name = asks (filter (name ==) . scopeNames) checkTopLevelDuplicate :: VarIdent -> TypeCheck var () checkTopLevelDuplicate name = do @@ -1771,7 +1904,7 @@ checkTopLevelDuplicate x local update tc where - update = addVarInCurrentScope x VarInfo + update = addVarInCurrentGlobalScope x VarInfo { varType = ty , varValue = term , varOrig = BinderVar (Just x) @@ -1831,47 +1964,91 @@ freeVarsT_ :: Eq var => TermT var -> TypeCheck var [var] freeVarsT_ term = do - types <- asks varTypes + ctx <- ask let typeOfVar' x = - case lookup x types of - Nothing -> panicImpossible "undefined variable" - Just ty -> ty + case lookupVarInfo x ctx of + Nothing -> panicImpossible "undefined variable" + Just info -> varType info return (freeVarsT typeOfVar' term) traceStartAndFinish :: Show a => String -> a -> a traceStartAndFinish tag = trace ("start [" <> tag <> "]") . (\x -> trace ("finish [" <> tag <> "] with " <> show x) x) +-- | Monadic 'all' that stops at the first failing element. +allM :: Monad m => (a -> m Bool) -> [a] -> m Bool +allM p = go + where + go [] = return True + go (x:xs) = p x >>= \case + False -> return False + True -> go xs + entailM :: Eq var => [ModalTope var] -> TermT var -> TypeCheck var Bool entailM modalTopes goal = do -- genTopes <- generateTopesForPointsM (allTopePoints goal) + topes''' <- saturateForEntailment modalTopes + entailSaturatedM topes''' goal + +-- | The preprocessing 'entailM' performs before searching: dedup, split off +-- context disjunctions, and saturate each alternative. Depends only on the +-- given topes (plus the discreteness axioms of the context), not on the goal +-- (the points argument of 'saturateTopes' is ignored). +saturateForEntailment :: Eq var => [ModalTope var] -> TypeCheck var [[ModalTope var]] +saturateForEntailment modalTopes = do discreteAxioms <- generateTopesForModalCubeVarsM - let topes' = nubTermT (modalTopes <> discreteAxioms) - topes'' = simplifyLHSwithDisjunctions topes' - topes''' <- mapM (fmap (saturateTopes (allTopePoints goal) . saturateBottom) . saturateInv) topes'' - prettyTopes <- mapM ppTermInContext (map tTope (saturateTopes (allTopePoints goal) (simplifyLHS topes'))) - prettyTope <- ppTermInContext goal - traceTypeCheck Debug - ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $ - and <$> mapM (`solveRHSM` goal) topes''' + let topes' = nubTermT (modalTopes <> discreteAxioms) + topes'' = simplifyLHSwithDisjunctions topes' + mapM (fmap (saturateTopes [] . saturateBottom) . saturateInv) topes'' +-- | Search each saturated alternative for the goal; the shared tail of +-- 'entailM' and the cached 'entailContextM'. +entailSaturatedM :: Eq var => [[ModalTope var]] -> TermT var -> TypeCheck var Bool +entailSaturatedM topes''' goal = asks verbosity >>= \case + Debug -> do + prettyTopes <- mapM ppTermInContext (map tTope (concat topes''')) + prettyTope <- ppTermInContext goal + traceTypeCheck Debug + ("entail " <> intercalate ", " prettyTopes <> " |- " <> prettyTope) $ + allM (`solveRHSM` goal) topes''' + _ -> allM (`solveRHSM` goal) topes''' -generateTopesForModalCubeVarsM :: Eq var => TypeCheck var [ModalTope var] -generateTopesForModalCubeVarsM = do - infos <- asks varInfos - fmap (nubTermT . concat) $ forM infos $ \(var, info) -> - case varModality info of - Flat -> do - whnfT (varType info) >>= \case - Cube2T{} -> do - let pt = Pure var - return [plainTope (topeOrT (topeEQT pt cube2_0T) (topeEQT pt cube2_1T))] - CubeIT{} -> do - let pt = Pure var - return [plainTope (topeOrT (topeEQT pt cubeI_0T) (topeEQT pt cubeI_1T))] - _ -> return [] - _ -> return [] +-- | Entailment against the context's own tope context, using the +-- 'localTopesSaturated' cache when one was installed (it is maintained at +-- the points where the tope context changes); otherwise fall back to the +-- per-query pipeline over 'localTopesNF'. Matching on the payload of +-- 'SaturationCached' is what forces the deferred pipeline, so the cost is +-- paid at the first query under a context, and never for contexts that are +-- never queried. +entailContextM :: Eq var => TermT var -> TypeCheck var Bool +entailContextM goal = asks localTopesSaturated >>= \case + SaturationCached (Just topes''') -> entailSaturatedM topes''' goal + SaturationCached Nothing -> fallback + SaturationUncached -> fallback + where + fallback = asks localTopesNF >>= (`entailM` goal) +-- | Install a deferred 'localTopesSaturated' cache for the transformed +-- context, and run the action with it. The pipeline's effects (Reader, +-- Writer, Except) are discharged purely into a thunk: installation costs +-- nothing, holes recorded by the speculative run are discarded, and a +-- pipeline error (e.g. a tope guard with a hole in lenient mode, which the +-- per-query path would never have evaluated) becomes 'Nothing', so errors +-- surface exactly where they did before. Used at every point where the tope +-- context changes; ordinary binder entries instead shift the cached value +-- with the rest of the context (saturation commutes with renaming). +withRefreshedTopes :: Eq var => (Context var -> Context var) -> TypeCheck var a -> TypeCheck var a +withRefreshedTopes f action = do + ctx' <- asks f + let sat = case runExcept (runWriterT (runReaderT (saturateForEntailment (localTopesNF ctx')) ctx')) of + Left _ -> Nothing + Right (s, _) -> Just s + local (const ctx' { localTopesSaturated = SaturationCached sat }) action + + +generateTopesForModalCubeVarsM :: TypeCheck var [ModalTope var] +generateTopesForModalCubeVarsM = asks localDiscreteTopes + entailTraceM :: Eq var => [ModalTope var] -> TermT var -> TypeCheck var Bool entailTraceM modalTopes goal = do topes' <- mapM ppTermInContext (accessibleTopes modalTopes) @@ -2157,9 +2334,9 @@ | 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 modalTopes l - <*> solveRHSM modalTopes r + TopeAndT _ l r -> solveRHSM modalTopes l >>= \case + False -> return False + True -> solveRHSM modalTopes r _ | goal `elem` topes -> return True TopeInvT{} -> do goal' <- nfTope goal @@ -2172,9 +2349,10 @@ TopeUninvT{} -> return False _ -> solveRHSM modalTopes goal' TopeOrT _ l r -> do - l' <- solveRHSM modalTopes l - r' <- solveRHSM modalTopes r - if (l' || r') + found <- solveRHSM modalTopes l >>= \case + True -> return True + False -> solveRHSM modalTopes r + if found then return True else do lems <- generateTopesForPointsM (allTopePoints goal) @@ -2183,10 +2361,10 @@ withTope t = hidden ++ saturateTopes [] (plainTope t : accessible) case lems' of - TopeOrT _ t1 t2 : _ -> do - l'' <- solveRHSM (withTope t1) goal - r'' <- solveRHSM (withTope t2) goal - return (l'' && r'') + TopeOrT _ t1 t2 : _ -> + solveRHSM (withTope t1) goal >>= \case + False -> return False + True -> solveRHSM (withTope t2) goal _ -> return False _ -> return False @@ -2220,9 +2398,8 @@ checkTope tope = do ctxTopes <- asks availableTopes performing (ActionContextEntails ctxTopes tope) $ do - topes' <- asks localTopesNF tope' <- nfTope tope - topes' `entailM` tope' + entailContextM tope' checkTopeEntails :: Eq var => TermT var -> TypeCheck var Bool checkTopeEntails tope = do @@ -2273,7 +2450,7 @@ contextTopes <- asks localTopesNF topesNF <- mapM nfTope topes let unionRHS = foldr topeOrT topeBottomT topesNF - contextTopes `entailM` unionRHS >>= \case + entailContextM unionRHS >>= \case -- a guard mentioning an (unfilled) hole can't be decided; defer coverage False | not (any containsHole topesNF) -> issueTypeError $ TypeErrorTopeNotSatisfied (accessibleTopes contextTopes) unionRHS @@ -2342,15 +2519,28 @@ } (S <$> context) -enterScopeMaybe :: Binder -> TModality -> TermT var -> Maybe (TermT var) -> TypeCheck (Inc var) b -> TypeCheck var b +enterScopeMaybe :: Eq var => Binder -> TModality -> TermT var -> Maybe (TermT var) -> TypeCheck (Inc var) b -> TypeCheck var b enterScopeMaybe orig md ty mval action = do + mDiscrete <- case md of + Flat -> whnfT ty >>= \case + Cube2T{} -> pure (Just (topeOrT (topeEQT z cube2_0T) (topeEQT z cube2_1T))) + CubeIT{} -> pure (Just (topeOrT (topeEQT z cubeI_0T) (topeEQT z cubeI_1T))) + _ -> pure Nothing + _ -> pure Nothing newContext <- asks (enterScopeContext orig md ty mval) - closeScope orig (runReaderT action newContext) + let newContext' = newContext + { localDiscreteTopes = maybe id ((:) . plainTope) mDiscrete (localDiscreteTopes newContext) } + -- A new discreteness axiom changes the saturation input; ordinary + -- binders keep the shifted cache (saturation commutes with renaming). + refresh = maybe id (const (withRefreshedTopes id)) mDiscrete + closeScope orig (runReaderT (refresh action) newContext') + where + z = Pure Z -enterScope :: Binder -> TModality -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b +enterScope :: Eq var => Binder -> TModality -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b enterScope orig md ty = enterScopeMaybe orig md ty Nothing -enterScopeWithBind :: Binder -> TModality -> TermT var -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b +enterScopeWithBind :: Eq var => Binder -> TModality -> TermT var -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b enterScopeWithBind orig md ty val = enterScopeMaybe orig md ty (Just val) -- | Run a sub-scope computation and lift it back to the enclosing scope: close @@ -2368,12 +2558,14 @@ lift (tell holes) return b -enterModality :: TModality -> TypeCheck var b -> TypeCheck var b +enterModality :: Eq var => TModality -> TypeCheck var b -> TypeCheck var b enterModality Id action = action enterModality md action = do newContext <- asks (applyModality md) let newContext' = newContext { localTopesEntailBottom = Nothing } - lift $ runReaderT action newContext' + -- 'applyModality' invalidated the saturation cache (accessibility + -- changed); refresh it under the shifted context. + lift $ runReaderT (withRefreshedTopes id action) newContext' performing :: Eq var => Action var -> TypeCheck var a -> TypeCheck var a performing action tc = do @@ -3069,35 +3261,30 @@ [] -> nfT type_ rs'' -> TypeRestrictedT ty <$> nfT type_ <*> pure rs'' +-- | Look up a variable and project one field of its 'VarInfo'; the shared +-- shape of the per-variable accessors below. +infoOfVar :: Eq var => (VarInfo var -> a) -> var -> TypeCheck var a +infoOfVar f x = asks (lookupVarInfo x) >>= \case + Nothing -> issueTypeError $ TypeErrorUndefined x + Just info -> return (f info) + checkDefinedVar :: VarIdent -> TypeCheck VarIdent () -checkDefinedVar x = asks (lookup x . varInfos) >>= \case - Nothing -> issueTypeError $ TypeErrorUndefined x - Just _ty -> return () +checkDefinedVar = infoOfVar (const ()) valueOfVar :: Eq var => var -> TypeCheck var (Maybe (TermT var)) -valueOfVar x = asks (lookup x . varValues) >>= \case - Nothing -> issueTypeError $ TypeErrorUndefined x - Just ty -> return ty +valueOfVar = infoOfVar varValue typeOfVar :: Eq var => var -> TypeCheck var (TermT var) -typeOfVar x = asks (lookup x . varTypes) >>= \case - Nothing -> issueTypeError $ TypeErrorUndefined x - Just ty -> return ty +typeOfVar = infoOfVar varType modalityOfVar :: Eq var => var -> TypeCheck var (TModality) -modalityOfVar x = asks (lookup x . varModalities) >>= \case - Nothing -> issueTypeError $ TypeErrorUndefined x - Just m -> return m +modalityOfVar = infoOfVar varModality locksOfVar :: Eq var => var -> TypeCheck var (TModality) -locksOfVar x = asks (lookup x . varLocks) >>= \case - Nothing -> issueTypeError $ TypeErrorUndefined x - Just m -> return m +locksOfVar = infoOfVar modAccum isTopLevelVar :: Eq var => var -> TypeCheck var Bool -isTopLevelVar x = asks (lookup x . varTopLevels) >>= \case - Nothing -> issueTypeError $ TypeErrorUndefined x - Just b -> return b +isTopLevelVar = infoOfVar varIsTopLevel typeOfUncomputed :: Eq var => TermT var -> TypeCheck var (TermT var) typeOfUncomputed = \case @@ -3115,7 +3302,7 @@ unless equiv $ issueTypeError (TypeErrorTopesNotEquivalent l r) -inAllSubContexts :: TypeCheck var () -> TypeCheck var () -> TypeCheck var () +inAllSubContexts :: Eq var => TypeCheck var () -> TypeCheck var () -> TypeCheck var () inAllSubContexts handleSingle tc = do topeSubContexts <- asks localTopesNFUnion case topeSubContexts of @@ -3123,7 +3310,7 @@ [_] -> handleSingle _:_:_ -> do forM_ topeSubContexts $ \topes' -> do - local (\Context{..} -> Context + withRefreshedTopes (\Context{..} -> Context { localTopes = topes' , localTopesNF = topes' , localTopesNFUnion = [topes'] @@ -3289,6 +3476,15 @@ switchVariance $ -- unifying in the negative position! unifyTerms cube cube' -- FIXME: unifyCubes enterScope orig' md cube' $ do + -- The tope checks below are subtyping checks with a fixed + -- direction relative to (subtype, supertype). Which side is + -- the subtype depends on the ambient variance: under + -- Covariant the actual type must be a subtype of the + -- expected one; under Contravariant (inside a domain) the + -- roles are reversed. Invariant is normally handled + -- upstream by running both directions; it is handled here + -- as well for safety. + variance <- asks covariance case ret' of UniverseTopeT{} -> do -- This is the case for tope families (shapes) @@ -3300,9 +3496,16 @@ -- we DO NOT take tope context Φ into account! expectedTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope actualTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope' - actualEntailsExpected <- [plainTope actualTopeNF] `entailM` expectedTopeNF - unless (actualEntailsExpected || containsHole expectedTopeNF || containsHole actualTopeNF) $ - issueTypeError (TypeErrorTopeNotSatisfied [actualTopeNF] expectedTopeNF) + let subEntailsSuper subNF superNF = do + entails <- [plainTope subNF] `entailM` superNF + unless (entails || containsHole subNF || containsHole superNF) $ + issueTypeError (TypeErrorTopeNotSatisfied [subNF] superNF) + case variance of + Covariant -> subEntailsSuper actualTopeNF expectedTopeNF + Contravariant -> subEntailsSuper expectedTopeNF actualTopeNF + Invariant -> do + subEntailsSuper actualTopeNF expectedTopeNF + subEntailsSuper expectedTopeNF actualTopeNF _ -> do -- this is the case for Π-types and extension types -- @@ -3311,8 +3514,15 @@ -- Ξ | Φ, ψ ⊢ φ expectedTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope actualTopeNF <- fromMaybe topeTopT <$> traverse nfT mtope' - localTope expectedTopeNF $ - contextEntails actualTopeNF + let superEntailsSub superNF subNF = + localTope superNF $ + contextEntails subNF + case variance of + Covariant -> superEntailsSub expectedTopeNF actualTopeNF + Contravariant -> superEntailsSub actualTopeNF expectedTopeNF + Invariant -> do + superEntailsSub expectedTopeNF actualTopeNF + superEntailsSub actualTopeNF expectedTopeNF case mterm of Nothing -> unifyTerms ret ret' Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret' @@ -3327,10 +3537,19 @@ enterScope orig' md a' $ unify Nothing b b' _ -> err - TypeIdT _ty x _tA y -> + TypeIdT _ty x tA y -> case actual' of - TypeIdT _ty' x' _tA' y' -> do - -- unify Nothing tA tA' -- TODO: do we need this check? + TypeIdT _ty' x' tA' y' -> do + -- The underlying types must be compared: without this + -- check the routine equates identity types over + -- different types whenever the endpoints unify, + -- accepting e.g. a free homotopy (a path in the type + -- of functions) where an endpoint-fixing one (a path + -- in a hom-type) is expected. Compared invariantly: + -- subtyping between the underlying types must not + -- leak into equality of identity types over them. + mapM_ (\(t1, t2) -> setVariance Invariant (unify Nothing t1 t2)) + ((,) <$> tA <*> tA') unify Nothing x x' unify Nothing y y' _ -> err @@ -3404,15 +3623,26 @@ case actual' of TypeRestrictedT _ty' ty' rs' -> do unify mterm ty ty' - sequence_ - [ localTope tope $ do - -- FIXME: can do less entails checks? - contextEntails (foldr topeOrT topeBottomT (map fst rs')) -- expected is less specified than actual - forM_ rs' $ \(tope', term') -> do - localTope tope' $ - unify Nothing term term' - | (tope, term) <- rs - ] + -- The faces of the supertype must be covered by the faces + -- of the subtype (the subtype is at least as specified), + -- with the boundary terms agreeing on overlaps. Which side + -- is the subtype depends on the ambient variance. + variance <- asks covariance + let subCoversSuper subRs superRs = sequence_ + [ localTope tope $ do + -- FIXME: can do less entails checks? + contextEntails (foldr topeOrT topeBottomT (map fst subRs)) + forM_ subRs $ \(tope', term') -> do + localTope tope' $ + unify Nothing term term' + | (tope, term) <- superRs + ] + case variance of + Covariant -> subCoversSuper rs' rs + Contravariant -> subCoversSuper rs rs' + Invariant -> do + subCoversSuper rs' rs + subCoversSuper rs rs' _ -> err -- FIXME: need better unification for restrictions TypeModalT _ty m ty -> case actual' of @@ -3438,7 +3668,6 @@ _ | holePresent -> return () _ -> panicImpossible "unexpected term in UNIFY" - where action = case mterm of Nothing -> ActionUnifyTerms expected actual @@ -3462,7 +3691,7 @@ | otherwise -> id refine $ do entailsBottom <- (modalTope' : localTopesNF) `entailM` topeBottomT - local (f modalTope' entailsBottom) tc + withRefreshedTopes (f modalTope' entailsBottom) tc where f tope' entailsBottom Context{..} = Context { localTopes = plainTope tope : localTopes @@ -4487,7 +4716,7 @@ unifyTerms ltype rtype unifyTerms lterm rterm -inferStandalone :: Eq var => Term var -> Either (TypeErrorInScopedContext var) (TermT var) +inferStandalone :: Term VarIdent -> Either (TypeErrorInScopedContext VarIdent) (TermT VarIdent) inferStandalone term = defaultTypeCheck (infer term) unsafeInferStandalone' :: Term' -> TermT' @@ -5095,3 +5324,184 @@ , cameraFoV = pi/15 , cameraAspectRatio = 1 } + +-- * Elaborated types of local binders (for LSP hover) + +-- | Naming environment for rendering types found under binders: how to +-- display each variable, plus the pattern binders passed on the way down, +-- for projection restoration (as in 'recordHoleShape'). +data BinderNames var = BinderNames + { binderNameOf :: var -> VarIdent + , binderNameProjs :: [(VarIdent, [([Proj], VarIdent)])] + , binderNamePats :: [(VarIdent, Binder)] + } + +topLevelBinderNames :: BinderNames VarIdent +topLevelBinderNames = BinderNames id [] [] + +renderBinderType :: BinderNames var -> TermT var -> Term' +renderBinderType names t = + restorePatternVars (binderNamePats names) + (foldBinderProjections (binderNameProjs names) (untyped (binderNameOf names <$> t))) + +underBinder :: Binder -> BinderNames var -> BinderNames (Inc var) +underBinder binder names = BinderNames + { binderNameOf = \case + Z -> zName + S v -> binderNameOf names v + , binderNameProjs = case binder of + BinderVar{} -> binderNameProjs names + _ -> (zName, binderPaths binder) : binderNameProjs names + , binderNamePats = case binder of + BinderVar{} -> binderNamePats names + _ -> (zName, binder) : binderNamePats names + } + where + zName = binderDisplayName binder + +-- | The memoised weak head normal form of a typed term, if present. +memoWHNF :: TermT var -> TermT var +memoWHNF t@(Free (AnnF info _)) = fromMaybe t (infoWHNF info) +memoWHNF t = t + + +-- | The variables a binder introduces, with rendered types. A pair binder +-- splits its type along Σ-types and cube products; when the shape is not +-- syntactic (e.g. the type is a defined name applied to arguments, as in +-- @((η , (ϵ , (α , β))) : has-quasi-diagrammatic-adj A B f u)@), the type is +-- put in weak head normal form first, which needs the global declarations in +-- scope (see 'binderTypesInScopeOf'). The dependent part is rendered under +-- the earlier component's display name, giving @q : B p@. +-- | A binder's displayed type: a plain type, or a cube together with a tope +-- for shaped binders like @(t : I | φ t)@. +data BinderTypeView + = TypeView Term' + | ShapeView Term' Term' + +binderTypeEntriesM :: Eq var => BinderNames var -> Binder -> TermT var -> TypeCheck var [(VarIdent, BinderTypeView)] +binderTypeEntriesM names binder ty = case binder of + BinderUnit -> pure [] + BinderVar Nothing -> pure [] + BinderVar (Just x) -> pure [(x, TypeView (renderBinderType names ty))] + BinderPair l r -> splitViewM ty >>= \case + Just (TypeSigmaT _ _ md a bscope) -> do + ls <- binderTypeEntriesM names l a + rs <- enterScope l md a (binderTypeEntriesM (underBinder l names) r bscope) + pure (ls ++ rs) + Just (CubeProductT _ a b) -> + (++) <$> binderTypeEntriesM names l a <*> binderTypeEntriesM names r b + _ -> pure [] -- unrecognised shape; the surface annotation is the fallback + +-- | View a type as a Σ-type or cube product: syntactically or through the +-- memoised WHNF if possible, computing the WHNF otherwise. Never throws. +splitViewM :: Eq var => TermT var -> TypeCheck var (Maybe (TermT var)) +splitViewM ty = case splitView (memoWHNF ty) of + Just t -> pure (Just t) + Nothing -> (splitView <$> whnfT ty) `catchError` \_ -> pure Nothing + where + splitView t = case stripTypeRestrictions t of + t'@TypeSigmaT{} -> Just t' + t'@CubeProductT{} -> Just t' + _ -> Nothing + +-- | Elaborated types of the local binders of a typed term, keyed by the +-- binder's original identifier (whose position points at its defining +-- occurrence). Every node of a typed term carries its type, so even a bare +-- lambda's binder is typed, by the domain of the lambda's own Π-type. +binderTypesOfTermM :: Eq var => BinderNames var -> TermT var -> TypeCheck var [(VarIdent, BinderTypeView)] +binderTypesOfTermM names = go + where + go t = case t of + Pure _ -> pure [] + LambdaT info binder mparam body -> do + (paramType, paramTope) <- case mparam of + Just (_, ty, mtope) -> pure (Just ty, mtope) + -- A bare lambda: the domain (and shape) of its own Π-type. + Nothing -> case funView (memoWHNF (infoType info)) of + Just (p, mtope) -> pure (Just p, mtope) + Nothing -> + (maybe (Nothing, Nothing) (\(p, mtope) -> (Just p, mtope)) . funView + <$> whnfT (infoType info)) + `catchError` \_ -> pure (Nothing, Nothing) + entries <- shapedBinderEntries names binder paramType paramTope + annEntries <- case mparam of + Nothing -> pure [] + Just (md, ty, mtope) -> do + tyEntries <- go ty + topeEntries <- maybe (pure []) (enterScope binder md ty . under binder) mtope + pure (tyEntries ++ topeEntries) + let md = maybe Id (\(m, _, _) -> m) mparam + bodyEntries <- enterScope binder md (fromMaybe universeT paramType) (under binder body) + pure (entries ++ annEntries ++ bodyEntries) + TypeFunT _ binder md param mtope ret -> do + entries <- shapedBinderEntries names binder (Just param) mtope + paramEntries <- go param + topeEntries <- maybe (pure []) (enterScope binder md param . under binder) mtope + retEntries <- enterScope binder md param (under binder ret) + pure (entries ++ paramEntries ++ topeEntries ++ retEntries) + TypeSigmaT _ binder md a bscope -> do + entries <- binderTypeEntriesM names binder a + aEntries <- go a + bEntries <- enterScope binder md a (under binder bscope) + pure (entries ++ aEntries ++ bEntries) + LetT _ binder manno value body -> do + let valueType = case value of + Free (AnnF valueInfo _) -> Just (infoType valueInfo) + Pure _ -> manno + entries <- maybe (pure []) (binderTypeEntriesM names binder) valueType + annEntries <- maybe (pure []) go manno + valueEntries <- go value + bodyEntries <- enterScopeWithBind binder Id (fromMaybe universeT valueType) value + (under binder body) + pure (entries ++ annEntries ++ valueEntries ++ bodyEntries) + LetModT _ binder _nu mu manno value body -> do + unwrapped <- case value of + Pure _ -> pure Nothing + Free (AnnF valueInfo _) -> do + let vt = infoType valueInfo + case modalView (memoWHNF vt) of + Just a -> pure (Just a) + Nothing -> (modalView <$> whnfT vt) `catchError` \_ -> pure Nothing + entries <- maybe (pure []) (binderTypeEntriesM names binder) unwrapped + annEntries <- maybe (pure []) go manno + valueEntries <- go value + bodyEntries <- enterScope binder mu (fromMaybe universeT unwrapped) (under binder body) + pure (entries ++ annEntries ++ valueEntries ++ bodyEntries) + Free (AnnF _ f) -> concat <$> mapM go (bifoldr (\_ acc -> acc) (:) [] f) + under binder = binderTypesOfTermM (underBinder binder names) + funView t = case stripTypeRestrictions t of + TypeFunT _ _ _ param mtope _ -> Just (param, mtope) + _ -> Nothing + modalView t = case stripTypeRestrictions t of + TypeModalT _ _ a -> Just a + _ -> Nothing + -- A shaped plain binder shows its cube together with the tope, as it is + -- written: (t : I | φ t). A shaped pair binder splits along the cube, + -- the tope constraining the components jointly (as in the surface tier). + shapedBinderEntries names' binder mty mtope = case (binder, mty, mtope) of + (BinderVar (Just x), Just cube, Just tope) -> + pure [(x, ShapeView (renderBinderType names' cube) + (renderBinderType (underBinder binder names') tope))] + (_, Just ty, _) -> binderTypeEntriesM names' binder ty + _ -> pure [] + +-- | All local binder types of a declaration: Π and Σ binders from the type, +-- lambda and let binders from the value. +declBinderTypes :: Decl' -> TypeCheck VarIdent [(VarIdent, BinderTypeView)] +declBinderTypes decl = + (++) <$> binderTypesOfTermM topLevelBinderNames (declType decl) + <*> maybe (pure []) (binderTypesOfTermM topLevelBinderNames) (declValue decl) + +-- | Elaborated types of the local binders of @fileDecls@, with @globalDecls@ +-- in scope so that 'whnfT' can unfold definitions when splitting pair +-- binders. Pure at the interface: runs the checker silently and returns no +-- entries where it fails. +binderTypesInScopeOf :: [Decl'] -> [Decl'] -> [(VarIdent, BinderTypeView)] +binderTypesInScopeOf globalDecls fileDecls = + case defaultTypeCheck action of + Left _ -> [] + Right entries -> entries + where + action = localVerbosity Silent $ + localDeclsPrepared globalDecls $ + concat <$> mapM declBinderTypes fileDecls diff --git a/test/Rzk/BinderTypesSpec.hs b/test/Rzk/BinderTypesSpec.hs new file mode 100644 --- /dev/null +++ b/test/Rzk/BinderTypesSpec.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE OverloadedStrings #-} +-- | Tests for 'declBinderTypes', the elaborated types of local binders that +-- the LSP hover consumes. The interesting cases are the ones the surface +-- annotations cannot provide: bare lambda binders (typed by the domain of +-- the lambda's own Π-type) and pair patterns, whose dependent components are +-- instantiated at the earlier components. +module Rzk.BinderTypesSpec (spec) where + +import qualified Data.Text as T + +import Language.Rzk.Free.Syntax (RzkPosition (RzkPosition), + getVarIdent) +import qualified Language.Rzk.Syntax as Rzk +import Language.Rzk.Syntax (VarIdent' (VarIdent)) +import Rzk.TypeCheck + +import Test.Hspec + +-- | Parse and typecheck a module, returning rendered binder types keyed by +-- the binder's (1-based) source position. Errors out loudly so a broken +-- fixture is obvious. +binderTypesOf :: T.Text -> [((Int, Int), String)] +binderTypesOf src = + case Rzk.parseModule src of + Left err -> error ("parse error: " <> T.unpack err) + Right m -> case defaultTypeCheck (localVerbosity Silent (typecheckModulesWithLocation [("", m)])) of + Left err -> error ("typecheck threw: " <> ppTypeErrorInScopedContext' BottomUp err) + Right decls -> + let ds = concatMap snd decls + in [ (pos, view t) + | (v, t) <- binderTypesInScopeOf ds ds + , let VarIdent (RzkPosition _ mpos) _ = getVarIdent v + , Just pos <- [mpos] + ] + where + view (TypeView t) = show t + view (ShapeView c tope) = show c <> " | " <> show tope + +exampleModule :: T.Text +exampleModule = T.unlines + [ "#lang rzk-1" -- line 1 + , "#define comp (A : U) (f : A -> A) : A -> A" -- line 2 + , " := \\ z -> let w := f z in f w" -- line 3 + , "#define dep" -- line 4 + , " ( A : U)" -- line 5 + , " ( B : A -> U)" -- line 6 + , " ( C : (x : A) -> B x -> U)" -- line 7 + , " ( (p , q , r) : Sigma (x : A , y : B x) , C x y)" -- line 8 + , " : U" -- line 9 + , " := A" -- line 10 + , "#define uncur (A : U) (B : A -> U)" -- line 11 + , " : (Sigma (x : A) , B x) -> U" -- line 12 + , " := \\ (a , b) -> A" -- line 13 + , "#define quasi-pair (A : U) (B : A -> U) : U" -- line 14 + , " := Sigma (x : A) , B x" -- line 15 + , "#define use-quasi (A : U) (B : A -> U)" -- line 16 + , " ( (s , t) : quasi-pair A B)" -- line 17 + , " : U := A" -- line 18 + , "#define shaped (A : U) (a : A)" -- line 19 + , " ( p : (t : 2 | t === t) -> A)" -- line 20 + , " : (s : 2 | TOP) -> A" -- line 21 + , " := \\ r -> a" -- line 22 + ] + +spec :: Spec +spec = describe "declBinderTypes" $ do + let entries = binderTypesOf exampleModule + at pos = lookup pos entries + + it "types an annotated parameter" $ + at (2, 15) `shouldBe` Just "U" -- (A : U) + + it "types a bare lambda binder from the enclosing Π-type" $ + at (3, 8) `shouldBe` Just "A" -- \ z -> + + it "types an unannotated let binder from its value" $ + at (3, 17) `shouldBe` Just "A" -- let w := f z + + it "types a Π binder inside a parameter's type" $ + at (7, 10) `shouldBe` Just "A" -- C : (x : A) -> ... + + it "instantiates dependent tuple components at earlier components" $ do + at (8, 6) `shouldBe` Just "A" -- p + at (8, 10) `shouldBe` Just "B p" -- q + at (8, 14) `shouldBe` Just "C p q" -- r + + it "types a bare pair lambda against its Σ domain" $ do + at (13, 9) `shouldBe` Just "A" -- \ (a , b) -> + at (13, 13) `shouldBe` Just "B a" + + it "splits a pair against a defined Σ-type by computing its WHNF" $ do + at (17, 6) `shouldBe` Just "A" -- ( (s , t) : quasi-pair A B) + at (17, 10) `shouldBe` Just "B s" + + it "shows a shaped binder with its tope" $ + at (20, 10) `shouldBe` Just "2 | t ≡ t" -- (t : 2 | t === t) + + it "shows a bare lambda binder against a shaped Π with its tope" $ + at (22, 8) `shouldBe` Just "2 | ⊤" -- \ r -> against (s : 2 | TOP) -> A diff --git a/test/Rzk/HolesSpec.hs b/test/Rzk/HolesSpec.hs --- a/test/Rzk/HolesSpec.hs +++ b/test/Rzk/HolesSpec.hs @@ -89,6 +89,17 @@ names (holeTermVars h) `shouldNotContain` ["t"] hs -> expectationFailure ("expected exactly one hole, got " <> show (length hs)) + -- Rendering: an anonymous binder that the return type does not use is + -- not shown ("U → U" rather than "(x₁ : U) → U"), while a user-written + -- name is kept even when unused. + it "hides unused anonymous binders in rendered types" $ do + case holesOf "#lang rzk-1\n#define mp : (A : U) -> (B : U) -> A -> (A -> B) -> B := ?\n" of + [h] -> show (holeGoal h) `shouldBe` "(A : U) → (B : U) → A → (A → B) → B" + hs -> expectationFailure ("expected exactly one hole, got " <> show (length hs)) + case holesOf "#lang rzk-1\n#define keep : (x : U) -> U -> U := ?\n" of + [h] -> show (holeGoal h) `shouldBe` "(x : U) → U → U" + hs -> expectationFailure ("expected exactly one hole, got " <> show (length hs)) + it "records every hole in a module" $ do let holes = holesOf "#lang rzk-1\n#define p : (A : U) -> (B : U) -> A -> B -> A\n := \\ A B a b -> ?\n" length holes `shouldBe` 1 diff --git a/test/Rzk/RefIndexSpec.hs b/test/Rzk/RefIndexSpec.hs new file mode 100644 --- /dev/null +++ b/test/Rzk/RefIndexSpec.hs @@ -0,0 +1,128 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE OverloadedStrings #-} +-- | Tests for the reference index behind go-to-definition, find-references, +-- and the surface-annotation tier of hover. Everything here is pure: modules +-- are parsed, never typechecked, which is exactly the situation the index is +-- for (mid-edit and ill-typed code). +module Rzk.RefIndexSpec (spec) where + +import Test.Hspec + +#ifdef LSP_ENABLED +import qualified Data.Text as T +import Language.Rzk.Syntax (parseModule) +import qualified Language.Rzk.VSCode.ReferenceIndex as RI + +indexOf :: [(FilePath, T.Text)] -> RI.ReferenceIndex +indexOf sources = RI.indexModules + [ (path, m) + | (path, src) <- sources + , Right m <- [parseModule src] + ] + +-- All positions are 0-based, as in the LSP protocol. +lookupAt' :: RI.ReferenceIndex -> FilePath -> (Int, Int) -> Maybe RI.Binding +lookupAt' ri path (l, c) = RI.lookupAt ri (RI.Uri path) (RI.Position l c) + +-- | Like 'lookupAt'', erroring out loudly when nothing is there, so a +-- misplaced test position is obvious. +bindingAt :: RI.ReferenceIndex -> FilePath -> (Int, Int) -> RI.Binding +bindingAt ri path pos = case lookupAt' ri path pos of + Just b -> b + Nothing -> error ("no binding at " <> path <> ":" <> show pos) + +defPos :: RI.Binding -> (FilePath, Int, Int) +defPos b = + let RI.Location (RI.Uri p) (RI.Range (RI.Position l c) _) = RI.bindingDef b + in (p, l, c) + +libSrc :: T.Text +libSrc = T.unlines + [ "#lang rzk-1" -- 0 + , "#define id (A : U) (x : A) : A := x" -- 1 + ] + +mainSrc :: T.Text +mainSrc = T.unlines + [ "#lang rzk-1" -- 0 + , "#variable C : U" -- 1 + , "#variables D E : C -> U" -- 2 + , "#define twice (A : U) (f : A -> A) (x : A) : A := f (f x)" -- 3 + , "#define use-id (A : U) (x : A) : A := id A (twice A (id A) x)" -- 4 + , "#define shadow (id : C) : C := id" -- 5 + , "#define pairs" -- 6 + , " ( A : U)" -- 7 + , " ( B : A -> U)" -- 8 + , " ( (p , q) : Sigma (x : A) , B x)" -- 9 + , " ( (t , s) : 2 * 2)" -- 10 + , " ( ((a , b) , c) : (2 * 2) * 2)" -- 11 + , " ( (u , v) : 2 * 2 | t <= u /\\ s <= v)" -- 12 + , " ( (h , k , l) : Sigma (x : A , y : B x) , C)" -- 13 + , " : U" -- 14 + , " := A" -- 15 + ] + +spec :: Spec +spec = describe "reference index" $ do + let ri = indexOf [("lib.rzk", libSrc), ("main.rzk", mainSrc)] + annAt path pos = lookupAt' ri path pos >>= RI.bindingType + + describe "definitions and references" $ do + it "resolves a cross-file use to its definition" $ + (defPos <$> lookupAt' ri "main.rzk" (4, 38)) `shouldBe` Just ("lib.rzk", 1, 8) + + it "lists references without duplicating the definition site" $ do + let b = bindingAt ri "lib.rzk" (1, 8) + length (RI.bindingRefs b) `shouldBe` 2 -- two uses in use-id + RI.bindingDef b `notElem` RI.bindingRefs b `shouldBe` True + length (RI.bindingSites b) `shouldBe` 3 -- def : refs + + it "resolves a local binder and its use" $ do + let b = bindingAt ri "main.rzk" (3, 55) -- x in f (f x) + defPos b `shouldBe` ("main.rzk", 3, 36) + length (RI.bindingSites b) `shouldBe` 2 + + it "resolves a local that shadows a global to the local" $ + (defPos <$> lookupAt' ri "main.rzk" (5, 31)) -- id in := id + `shouldBe` Just ("main.rzk", 5, 16) + + it "misses positions outside identifiers" $ + lookupAt' ri "main.rzk" (3, 13) `shouldBe` Nothing -- whitespace + + describe "surface type annotations" $ do + it "annotates parameters" $ do + annAt "main.rzk" (3, 15) `shouldBe` Just "U" -- (A : U) + annAt "main.rzk" (3, 23) `shouldBe` Just "A -> A" -- (f : A -> A) + + it "annotates assumptions (#variable, #variables)" $ do + annAt "main.rzk" (1, 10) `shouldBe` Just "U" + annAt "main.rzk" (2, 11) `shouldBe` Just "C -> U" + annAt "main.rzk" (2, 13) `shouldBe` Just "C -> U" + + it "leaves top-level names to the elaborated tier" $ do + let b = bindingAt ri "main.rzk" (3, 8) -- twice + RI.bindingType b `shouldBe` Nothing + + it "splits a pair against a Σ-type, instantiating the dependency" $ do + annAt "main.rzk" (9, 5) `shouldBe` Just "A" -- p + annAt "main.rzk" (9, 9) `shouldBe` Just "B p" -- q + + it "splits pairs against cube products, nested too" $ do + annAt "main.rzk" (10, 5) `shouldBe` Just "2" -- t + annAt "main.rzk" (10, 9) `shouldBe` Just "2" -- s + annAt "main.rzk" (11, 6) `shouldBe` Just "2" -- a + annAt "main.rzk" (11, 10) `shouldBe` Just "2" -- b + annAt "main.rzk" (11, 15) `shouldBe` Just "2" -- c + + it "gives shaped pair components their cube" $ do + annAt "main.rzk" (12, 5) `shouldBe` Just "2" -- u + annAt "main.rzk" (12, 9) `shouldBe` Just "2" -- v + + it "splits a tuple against a Σ-tuple" $ do + annAt "main.rzk" (13, 5) `shouldBe` Just "A" -- h + annAt "main.rzk" (13, 9) `shouldBe` Just "B h" -- k + annAt "main.rzk" (13, 13) `shouldBe` Just "C" -- l +#else +spec :: Spec +spec = describe "reference index" (pure ()) +#endif diff --git a/test/Rzk/SemanticTokensSpec.hs b/test/Rzk/SemanticTokensSpec.hs new file mode 100644 --- /dev/null +++ b/test/Rzk/SemanticTokensSpec.hs @@ -0,0 +1,109 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE OverloadedStrings #-} +-- | Tests for the LSP presentation layer: the merged semantic tokens +-- (AST-based plus lexer-based) and the hover signature formatting. +module Rzk.SemanticTokensSpec (spec) where + +import Test.Hspec + +#ifdef LSP_ENABLED +import qualified Data.Text as T +import Language.LSP.Protocol.Types (SemanticTokenAbsolute (..), + SemanticTokenTypes (..)) +import Language.Rzk.Syntax (parseModule, parseTerm) +import Language.Rzk.VSCode.Handlers (formatSignature) +import Language.Rzk.VSCode.Tokenize (mergeTokens, tokenizeModule, + tokenizeSyntaxSymbols) + +-- | Merged tokens of a module, as 'provideSemanticTokens' produces them. +tokensOf :: T.Text -> [SemanticTokenAbsolute] +tokensOf src = case parseModule src of + Left err -> error ("parse error: " <> T.unpack err) + Right m -> mergeTokens (tokenizeModule m) (tokenizeSyntaxSymbols src) + +-- | The token type starting at a (0-based) position, if any. +tokenAt :: [SemanticTokenAbsolute] -> (Int, Int) -> Maybe SemanticTokenTypes +tokenAt toks (l, c) = case + [ _tokenType t + | t <- toks + , _line t == fromIntegral l, _startChar t == fromIntegral c + ] of + (tt : _) -> Just tt + [] -> Nothing + +exampleModule :: T.Text +exampleModule = T.unlines + [ "#lang rzk-1" -- 0 + , "#define weird uses (A) (x : A) : A := x" -- 1 + , "#check TOP : TOPE" -- 2 + ] + +spec :: Spec +spec = do + describe "semantic tokens" $ do + let toks = tokensOf exampleModule + positions = [ (_line t, _startChar t) | t <- toks ] + + it "are sorted by position, as the LSP delta encoding requires" $ + -- Regression: tokens of a uses-clause used to be emitted before the + -- declaration name. + and (zipWith (<) positions (drop 1 positions)) `shouldBe` True + + it "classify commands, keywords, and operators from the lexer" $ do + tokenAt toks (1, 0) `shouldBe` Just SemanticTokenTypes_Macro -- #define + tokenAt toks (1, 14) `shouldBe` Just SemanticTokenTypes_Keyword -- uses + tokenAt toks (1, 26) `shouldBe` Just SemanticTokenTypes_Operator -- : + tokenAt toks (1, 35) `shouldBe` Just SemanticTokenTypes_Operator -- := + + it "let AST-based tokens win over lexer tokens on overlap" $ do + tokenAt toks (1, 8) `shouldBe` Just SemanticTokenTypes_Function -- weird (declaration) + tokenAt toks (2, 7) `shouldBe` Just SemanticTokenTypes_String -- TOP (tope literal, not keyword) + + it "skip plain brackets" $ + tokenAt toks (1, 23) `shouldBe` Nothing -- ( + + it "survive files that do not parse" $ + tokenizeSyntaxSymbols "#lang rzk-1\n#define broken (x : A) :=\n" + `shouldNotBe` [] + + it "mark holes, including named ones" $ do + let toks' = tokensOf $ T.unlines + [ "#lang rzk-1" -- 0 + , "#define gap (A : U) : A := ?" -- 1 + , "#define named (A : U) : A := ?goal" -- 2 + ] + tokenAt toks' (1, 27) `shouldBe` Just SemanticTokenTypes_Regexp -- ? + tokenAt toks' (2, 29) `shouldBe` Just SemanticTokenTypes_Regexp -- ?goal + + it "mark holes even in files that do not parse" $ + tokenizeSyntaxSymbols "#lang rzk-1\n#define broken (x : A) := ?\n" + `shouldSatisfy` any ((== SemanticTokenTypes_Regexp) . _tokenType) + + describe "formatSignature" $ do + let fmt name src = case parseTerm (T.pack src) of + Left err -> error ("parse error: " <> T.unpack err) + Right t -> formatSignature name t + + it "keeps short types on one line" $ + fmt "x" "A -> B" `shouldBe` "x : A -> B" + + it "splits long function types one parameter per line" $ + fmt "long" "(A : U) -> (B : A -> U) -> (C : (x : A) -> B x -> U) -> ((x : A) -> B x) -> U" + `shouldBe` unlines' + [ "long" + , " : (A : U)" + , " → (B : A -> U)" + , " → (C : (x : A) -> B x -> U)" + , " → ((x : A) -> B x)" + , " → U" + ] + + it "keeps long non-function types on one line" $ do + let sigma = "Sigma (f : (x : A) -> (y : A) -> hom A x y -> hom A x y), (x : A) -> U" + fmt "s" sigma `shouldBe` ("s : " <> sigma) + where + unlines' = foldr1 (\l r -> l <> "\n" <> r) +#else +spec :: Spec +spec = describe "semantic tokens" (pure ()) +#endif diff --git a/test/typecheck/cases/happy-subtype-variance-pi-shape-domain.expect.yaml b/test/typecheck/cases/happy-subtype-variance-pi-shape-domain.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-subtype-variance-pi-shape-domain.expect.yaml @@ -0,0 +1,3 @@ +status: ok +regression_for: + - subtype-variance-direction diff --git a/test/typecheck/cases/happy-subtype-variance-pi-shape-domain.rzk b/test/typecheck/cases/happy-subtype-variance-pi-shape-domain.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-subtype-variance-pi-shape-domain.rzk @@ -0,0 +1,22 @@ +#lang rzk-1 + +-- PROBE: should be ACCEPTED (paper rules / dRzk). +-- +-- Requirement for `g k`: +-- (f : (t : 2 | t === 0_2) → A) → A <: (f : (t : 2 | TOP) → A) → A +-- By contravariance of Π domains this needs +-- (t : 2 | TOP) → A <: (t : 2 | t === 0_2) → A +-- which by S-Pi-Shape needs t === 0_2 ⊢ TOP — TRUE. +-- +-- Semantically: g calls its parameter with total functions, and k is +-- happy to receive them (it only ever applies f on t === 0_2). +-- +-- A checker whose Π-domain tope check ignores the variance flag checks +-- TOP ⊢ t === 0_2 (false) and REJECTS. + +#def pi-shape-wrong-reject + ( A : U) + ( g : ((f : (t : 2 | TOP) → A) → A) → A) + ( k : (f : (t : 2 | t === 0_2) → A) → A) + : A + := g k diff --git a/test/typecheck/cases/happy-subtype-variance-restriction-faces.expect.yaml b/test/typecheck/cases/happy-subtype-variance-restriction-faces.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-subtype-variance-restriction-faces.expect.yaml @@ -0,0 +1,3 @@ +status: ok +regression_for: + - subtype-variance-direction diff --git a/test/typecheck/cases/happy-subtype-variance-restriction-faces.rzk b/test/typecheck/cases/happy-subtype-variance-restriction-faces.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-subtype-variance-restriction-faces.rzk @@ -0,0 +1,27 @@ +#lang rzk-1 + +-- PROBE: should be ACCEPTED (paper rules / dRzk). +-- +-- Requirement for `g k`: +-- (x : A [t === 0_2 |-> a]) → A +-- <: (x : A [t === 0_2 |-> a, t === 1_2 |-> b]) → A +-- By contravariance of Π domains this needs +-- A [t === 0_2 |-> a, t === 1_2 |-> b] <: A [t === 0_2 |-> a] +-- which holds by S-Restr: the single face of the supertype is among the +-- subtype's faces. +-- +-- Semantically: g feeds k elements with both boundary promises; k only +-- relies on the promise at t === 0_2. +-- +-- A checker whose restriction-face coverage check ignores the variance +-- flag demands the converse inclusion (false) and REJECTS. + +#def restr-wrong-reject + ( A : U) + ( a : A) + ( b : A) + ( t : 2) + ( g : ((x : A [t === 0_2 |-> a, t === 1_2 |-> b]) → A) → A) + ( k : (x : A [t === 0_2 |-> a]) → A) + : A + := g k diff --git a/test/typecheck/cases/happy-subtype-variance-tope-family.expect.yaml b/test/typecheck/cases/happy-subtype-variance-tope-family.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-subtype-variance-tope-family.expect.yaml @@ -0,0 +1,3 @@ +status: ok +regression_for: + - subtype-variance-direction diff --git a/test/typecheck/cases/happy-subtype-variance-tope-family.rzk b/test/typecheck/cases/happy-subtype-variance-tope-family.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/happy-subtype-variance-tope-family.rzk @@ -0,0 +1,22 @@ +#lang rzk-1 + +-- PROBE: should be ACCEPTED (paper rules / dRzk). +-- +-- Requirement for `g h`: +-- (φ : (t : 2 | TOP) → TOPE) → A <: (φ : (t : 2 | t === 0_2) → TOPE) → A +-- By contravariance of Π domains this needs +-- (t : 2 | t === 0_2) → TOPE <: (t : 2 | TOP) → TOPE +-- which by S-TopeFam (covariant domains) needs t === 0_2 ⊢ TOP — TRUE. +-- +-- Semantically: g passes h tope families bounded by t === 0_2; h accepts +-- any tope family whatsoever (bound TOP), so this is safe. +-- +-- A checker whose S-TopeFam check ignores the variance flag checks +-- TOP ⊢ t === 0_2 (false) and REJECTS. + +#def tope-fam-wrong-reject + ( A : U) + ( g : ((φ : (t : 2 | t === 0_2) → TOPE) → A) → A) + ( h : (φ : (t : 2 | TOP) → TOPE) → A) + : A + := g h diff --git a/test/typecheck/cases/ill-subtype-variance-pi-shape-domain.expect.yaml b/test/typecheck/cases/ill-subtype-variance-pi-shape-domain.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-subtype-variance-pi-shape-domain.expect.yaml @@ -0,0 +1,4 @@ +status: error +error_tag: TypeErrorTopeNotSatisfied +regression_for: + - subtype-variance-direction diff --git a/test/typecheck/cases/ill-subtype-variance-pi-shape-domain.rzk b/test/typecheck/cases/ill-subtype-variance-pi-shape-domain.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-subtype-variance-pi-shape-domain.rzk @@ -0,0 +1,22 @@ +#lang rzk-1 + +-- PROBE: should be REJECTED (paper rules / dRzk). +-- +-- Requirement for `g k`: typeof(k) <: dom(typeof(g)), i.e. +-- (f : (t : 2 | TOP) → A) → A <: (f : (t : 2 | t === 0_2) → A) → A +-- By contravariance of Π domains this needs +-- (t : 2 | t === 0_2) → A <: (t : 2 | TOP) → A +-- which by S-Pi-Shape needs TOP ⊢ t === 0_2 — FALSE. +-- +-- Semantically: g may call its parameter with an f defined only on +-- t === 0_2; k demands a total f and applies it anywhere. +-- +-- A checker whose Π-domain tope check ignores the variance flag checks +-- the converse entailment t === 0_2 ⊢ TOP (true) and ACCEPTS. + +#def pi-shape-wrong-accept + ( A : U) + ( g : ((f : (t : 2 | t === 0_2) → A) → A) → A) + ( k : (f : (t : 2 | TOP) → A) → A) + : A + := g k diff --git a/test/typecheck/cases/ill-subtype-variance-restriction-faces.expect.yaml b/test/typecheck/cases/ill-subtype-variance-restriction-faces.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-subtype-variance-restriction-faces.expect.yaml @@ -0,0 +1,4 @@ +status: error +error_tag: TypeErrorTopeNotSatisfied +regression_for: + - subtype-variance-direction diff --git a/test/typecheck/cases/ill-subtype-variance-restriction-faces.rzk b/test/typecheck/cases/ill-subtype-variance-restriction-faces.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-subtype-variance-restriction-faces.rzk @@ -0,0 +1,27 @@ +#lang rzk-1 + +-- PROBE: should be REJECTED (paper rules / dRzk). +-- +-- Requirement for `g k`: +-- (x : A [t === 0_2 |-> a, t === 1_2 |-> b]) → A +-- <: (x : A [t === 0_2 |-> a]) → A +-- By contravariance of Π domains this needs +-- A [t === 0_2 |-> a] <: A [t === 0_2 |-> a, t === 1_2 |-> b] +-- which by S-Restr fails: the face t === 1_2 |-> b of the supertype is +-- not covered by the subtype's faces. +-- +-- Semantically: g feeds k elements that promise nothing at t === 1_2; +-- k's type entitles it to compute x ≡ b there. +-- +-- A checker whose restriction-face coverage check ignores the variance +-- flag checks the converse inclusion (true) and ACCEPTS. + +#def restr-wrong-accept + ( A : U) + ( a : A) + ( b : A) + ( t : 2) + ( g : ((x : A [t === 0_2 |-> a]) → A) → A) + ( k : (x : A [t === 0_2 |-> a, t === 1_2 |-> b]) → A) + : A + := g k diff --git a/test/typecheck/cases/ill-subtype-variance-tope-family.expect.yaml b/test/typecheck/cases/ill-subtype-variance-tope-family.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-subtype-variance-tope-family.expect.yaml @@ -0,0 +1,4 @@ +status: error +error_tag: TypeErrorTopeNotSatisfied +regression_for: + - subtype-variance-direction diff --git a/test/typecheck/cases/ill-subtype-variance-tope-family.rzk b/test/typecheck/cases/ill-subtype-variance-tope-family.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-subtype-variance-tope-family.rzk @@ -0,0 +1,22 @@ +#lang rzk-1 + +-- PROBE: should be REJECTED (paper rules / dRzk). +-- +-- Requirement for `g h`: +-- (φ : (t : 2 | t === 0_2) → TOPE) → A <: (φ : (t : 2 | TOP) → TOPE) → A +-- By contravariance of Π domains this needs +-- (t : 2 | TOP) → TOPE <: (t : 2 | t === 0_2) → TOPE +-- which by S-TopeFam (covariant domains) needs TOP ⊢ t === 0_2 — FALSE. +-- +-- Semantically: g passes h tope families with no bound at all; h's type +-- promises its φ is bounded by t === 0_2. +-- +-- A checker whose S-TopeFam check ignores the variance flag checks +-- t === 0_2 ⊢ TOP (true) and ACCEPTS. + +#def tope-fam-wrong-accept + ( A : U) + ( g : ((φ : (t : 2 | TOP) → TOPE) → A) → A) + ( h : (φ : (t : 2 | t === 0_2) → TOPE) → A) + : A + := g h diff --git a/test/typecheck/cases/ill-unify-id-free-path.expect.yaml b/test/typecheck/cases/ill-unify-id-free-path.expect.yaml new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-unify-id-free-path.expect.yaml @@ -0,0 +1,6 @@ +status: error +error_tag: TypeErrorUnifyTerms +message_contains: + - cannot unify +regression_for: + - unify-id-compares-underlying-types diff --git a/test/typecheck/cases/ill-unify-id-free-path.rzk b/test/typecheck/cases/ill-unify-id-free-path.rzk new file mode 100644 --- /dev/null +++ b/test/typecheck/cases/ill-unify-id-free-path.rzk @@ -0,0 +1,20 @@ +#lang rzk-1 + +-- Identity types over different types must not be unified even when their +-- endpoints agree. Here `hom A x y` is a subtype of `Δ¹ → A` (its elements are +-- exactly the functions with the given boundary), so `f` and `g` inhabit both; +-- but a path in `(t : Δ¹) → A` is a free homotopy, while a path in +-- `hom A x y` fixes the endpoints. Accepting `q` below transports a free +-- homotopy into the endpoint-fixing path type, which is unsound. rzk used to +-- accept this (the type components of the identity types were not compared). +#define Δ¹ : (2 → TOPE) + := \ t → TOP + +#define hom (A : U) (x y : A) + : U + := (t : Δ¹) → A [t ≡ 0₂ ↦ x, t ≡ 1₂ ↦ y] + +#define narrow (A : U) (x y : A) (f g : hom A x y) + (q : f =_{(t : Δ¹) → A} g) + : f =_{hom A x y} g + := q