agda-language-server 0.2.6.3.0 → 7
raw patch · 41 files changed
+1985/−973 lines, 41 filesdep +attoparsecdep +directorydep +filepathdep ~Agdadep ~lspdep ~network-simplePVP ok
version bump matches the API change (PVP)
Dependencies added: attoparsec, directory, filepath, ghc-experimental, lsp-test, lsp-types, prettyprinter, unix
Dependency ranges changed: Agda, lsp, network-simple
API changes (from Hackage documentation)
- Agda.Convert: explainWhyInScope :: String -> FilePath -> Maybe LocalVar -> [AbstractName] -> [AbstractModule] -> TCM Doc
- Agda.Convert: showInfoError :: Info_Error -> TCM String
- Agda.IR: instance Agda.IR.FromAgda Agda.Interaction.Response.GiveResult Agda.IR.GiveResult
- Render.Class: instance Render.Class.Render Text.PrettyPrint.HughesPJ.Doc
- Render.Common: instance Render.Class.Render Agda.Syntax.Common.Induction
- Render.Interaction: instance (Render.Class.Render a, Render.Class.Render b) => Render.Class.Render (Agda.Interaction.Base.OutputConstraint a b)
- Render.Interaction: instance (Render.Class.Render a, Render.Class.Render b) => Render.Class.Render (Agda.Interaction.Base.OutputForm a b)
- Render.TypeChecking: instance Render.Class.Render Agda.TypeChecking.Monad.Base.Comparison
- Render.TypeChecking: instance Render.Class.Render Agda.TypeChecking.Monad.Base.NamedMeta
- Render.TypeChecking: instance Render.Class.Render Agda.TypeChecking.Monad.Base.Polarity
+ Agda: CmdReq :: String -> CommandReq
+ Agda: CmdReqSYN :: CommandReq
+ Agda: CmdRes :: Maybe CommandErr -> CommandRes
+ Agda: CmdResACK :: String -> Int -> CommandRes
+ Agda: data CommandReq
+ Agda: data CommandRes
+ Agda: instance Data.Aeson.Types.ToJSON.ToJSON Agda.CommandReq
+ Agda.IR: ResponseJSONRaw :: Value -> Response
+ Agda.IR: ResponseMimer :: Int -> Maybe String -> Response
+ Agda.IR: instance Agda.IR.FromAgda Agda.Interaction.Response.Base.GiveResult Agda.IR.GiveResult
+ Options: [optRawResponses] :: Options -> Bool
+ Options: [optSetup] :: Options -> Bool
+ Options: [optVersion] :: Options -> Bool
+ Options: versionNumber :: Int
+ Options: versionString :: String
+ Render.Class: instance Render.Class.Render Agda.Syntax.Common.Pretty.Doc
+ Render.Class: instance Render.Class.Render Data.Text.Internal.Text
+ Render.Class: instance Render.Class.Render GHC.Word.Word32
+ Render.Class: instance Render.Class.Render a => Render.Class.Render (GHC.Maybe.Maybe a)
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.Aspect.Induction
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.Lock
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.ModalPolarity
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.OriginIrrelevant
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.OriginRelevant
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.OriginShapeIrrelevant
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.OverlapMode
+ Render.Common: instance Render.Class.Render Agda.Syntax.Common.PolarityModality
+ Render.Common: renderErased :: Erased -> Inlines -> Inlines
+ Render.Concrete: instance Render.Class.Render Agda.Syntax.Concrete.RecordDirective
+ Render.Concrete: instance Render.Class.Render a => Render.Class.Render (Agda.Syntax.Concrete.TacticAttribute' a)
+ Render.Concrete: renderOpApp280 :: Render a => Aspect -> QName -> List1 (NamedArg (MaybePlaceholder a)) -> [Inlines]
+ Render.Interaction: instance (Render.Class.Render a, Render.Class.Render b) => Render.Class.Render (Agda.Interaction.Output.OutputConstraint a b)
+ Render.Interaction: instance (Render.Class.Render a, Render.Class.Render b) => Render.Class.Render (Agda.Interaction.Output.OutputForm a b)
+ Render.Interaction: instance Render.Class.Render c => Render.Class.Render (Agda.TypeChecking.Monad.Base.Types.IPFace' c)
+ Render.RichText: (<?>) :: Inlines -> Inlines -> Inlines
+ Render.RichText: infixl 6 <?>
+ Render.RichText: instance Agda.Utils.Null.Null Render.RichText.Inlines
+ Render.RichText: textNonEmpty :: String -> Inlines
+ Render.TypeChecking: instance Render.Class.Render Agda.TypeChecking.Monad.Base.Types.Comparison
+ Render.TypeChecking: instance Render.Class.Render Agda.TypeChecking.Monad.Base.Types.NamedMeta
+ Render.TypeChecking: instance Render.Class.Render Agda.TypeChecking.Monad.Base.Types.Polarity
+ Server: serverDefn :: Options -> ServerDefinition Config
+ Switchboard: agdaCustomMethod :: forall {f :: MessageDirection} {t :: MessageKind}. SMethod ('Method_CustomMethod "agda" :: Method f t)
- Agda: getCommandLineOptions :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions
+ Agda: getCommandLineOptions :: forall (m :: Type -> Type). (HasOptions m, MonadIO m) => ServerM m CommandLineOptions
- Agda: runAgda :: MonadIO m => ServerM TCM a -> ServerM m (Either String a)
+ Agda: runAgda :: forall (m :: Type -> Type) a. MonadIO m => ServerM TCM a -> ServerM m (Either String a)
- Agda: sendCommand :: MonadIO m => Value -> ServerM m Value
+ Agda: sendCommand :: forall (m :: Type -> Type). MonadIO m => Value -> ServerM m Value
- Monad: provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerM m ()
+ Monad: provideCommand :: forall (m :: Type -> Type). (Monad m, MonadIO m) => IOTCM -> ServerM m ()
- Monad: sendResponse :: (Monad m, MonadIO m) => Env -> Response -> TCMT m ()
+ Monad: sendResponse :: forall (m :: Type -> Type). (Monad m, MonadIO m) => Env -> Response -> TCMT m ()
- Monad: signalCommandFinish :: (Monad m, MonadIO m) => ServerM m ()
+ Monad: signalCommandFinish :: forall (m :: Type -> Type). (Monad m, MonadIO m) => ServerM m ()
- Monad: type ServerM m = ReaderT Env m
+ Monad: type ServerM (m :: Type -> Type) = ReaderT Env m
- Monad: waitUntilResponsesSent :: (Monad m, MonadIO m) => ServerM m ()
+ Monad: waitUntilResponsesSent :: forall (m :: Type -> Type). (Monad m, MonadIO m) => ServerM m ()
- Monad: writeLog :: (Monad m, MonadIO m) => Text -> ServerM m ()
+ Monad: writeLog :: forall (m :: Type -> Type). (Monad m, MonadIO m) => Text -> ServerM m ()
- Monad: writeLog' :: (Monad m, MonadIO m, Show a) => a -> ServerM m ()
+ Monad: writeLog' :: forall (m :: Type -> Type) a. (Monad m, MonadIO m, Show a) => a -> ServerM m ()
- Options: Options :: Maybe Int -> [String] -> Bool -> Options
+ Options: Options :: Maybe Int -> [String] -> Bool -> Bool -> Bool -> Bool -> Options
- Render.Concrete: pRecord :: Name -> RecordDirectives -> [LamBinding] -> Maybe Expr -> [Declaration] -> Inlines
+ Render.Concrete: pRecord :: Erased -> Name -> [RecordDirective] -> [LamBinding] -> Maybe Expr -> [Declaration] -> Inlines
- Render.Concrete: renderOpApp :: forall a. Render a => QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]
+ Render.Concrete: renderOpApp :: Render a => QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]
- Server.Handler: onHover :: Uri -> Position -> ServerM (LspM Config) (Maybe Hover)
+ Server.Handler: onHover :: Uri -> Position -> ServerM (LspM Config) (Hover |? Null)
Files
- CHANGELOG.md +116/−0
- README.md +43/−3
- agda-language-server.cabal +103/−29
- app/Main.hs +46/−10
- app/Reactor.hs +117/−0
- package.yaml +68/−19
- src/Agda.hs +35/−19
- src/Agda/Convert.hs +63/−148
- src/Agda/IR.hs +4/−0
- src/Agda/Parser.hs +5/−18
- src/Agda/Position.hs +81/−71
- src/Monad.hs +36/−33
- src/Options.hs +105/−57
- src/Render.hs +1/−1
- src/Render/Class.hs +29/−14
- src/Render/Common.hs +117/−32
- src/Render/Concrete.hs +359/−108
- src/Render/Interaction.hs +65/−47
- src/Render/Internal.hs +41/−53
- src/Render/Literal.hs +7/−7
- src/Render/Name.hs +8/−10
- src/Render/Position.hs +17/−6
- src/Render/RichText.hs +78/−53
- src/Render/TypeChecking.hs +2/−2
- src/Render/Utils.hs +4/−4
- src/Server.hs +114/−86
- src/Server/CommandController.hs +2/−2
- src/Server/Handler.hs +39/−25
- src/Server/ResponseController.hs +18/−18
- src/Switchboard.hs +26/−13
- stack-8.10-Agda-2.6.2.2.yaml +0/−21
- stack-9.0-Agda-2.6.2.2.yaml +0/−19
- stack-9.10.2-Agda-2.6.4.3.yaml +26/−0
- stack-9.10.2-Agda-2.7.0.1.yaml +25/−0
- stack-9.10.2-Agda-2.8.0.yaml +25/−0
- stack-9.2-Agda-2.6.2.2.yaml +0/−17
- stack.yaml +6/−3
- test/Test.hs +34/−7
- test/Test/LSP.hs +49/−0
- test/Test/SrcLoc.hs +17/−18
- test/Test/WASM.hs +54/−0
CHANGELOG.md view
@@ -4,6 +4,115 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). +## v7 - 2026-09-16++### Added+- #48: Support for building a WASI reactor module via a flag by [@andy0130tw](https://github.com/andy0130tw).+- CI workflow to publish releases to Hackage.++### Changed+- Redesign native Stack caching: single-writer, exact-match cache keys for the toolchain and compiled-dependency caches.+- Require exact cache hits for the WASM toolchain and native-utilities (alex/happy) caches.+- Hash the workflow file itself into the compiled-dependency cache key, so changes to the build commands invalidate stale caches.+- Pin `haskell-actions/setup` to a full commit SHA instead of a mutable tag.++### Fixed+- #47: Fix a broken link to the release page by [@xnuk](https://github.com/xnuk).+- Install clang64 ICU and pkgconf on Windows CI builds.+- Fix the WASM `dist-newstyle` cache key to catch gitlink-only submodule bumps.+- Fix alex/happy datadir loss across native-utilities cache restores.+- Restore the ghcup cache before Haskell setup on macOS.+- Pin the `yq` version on Windows to avoid GitHub API rate-limit failures.+- Reuse the ghcup-installed GHC instead of Stack's own copy.+- Stop treating a version print as WASM toolchain validation.+- Drop the invalid `-with-rtsopts` `ghc-options` entry from the library stanza, which caused Hackage to reject package uploads.++## v6 - 2026-04-11++### Added+- Support for Agda-2.8.0.+- WASM build and release artefacts by [@andy0130tw](https://github.com/andy0130tw).+- Development and stable release artefacts for all supported Agda versions: Agda-2.6.4.3, Agda-2.7.0.1, and Agda-2.8.0.+- Separate release artefacts for macOS Apple Silicon and Intel Macs.+- #39: Agda setup support for Agda-2.8.0 by [@andy0130tw](https://github.com/andy0130tw).+- #40: JSON interaction mode response option by [@andy0130tw](https://github.com/andy0130tw).+- #45: Support multiple `+AGDA ... -AGDA` blocks in CLI arguments by [@juliapath](https://github.com/juliapath).+- WASM-specific test target.++### Changed+- Use single-digit language server release tags such as `v6`.+- Drop Agda-2.6.3 support from the release matrix.+- Target Agda-2.6.4.3, Agda-2.7.0.1, and Agda-2.8.0.+- Build supported Agda targets with the GHC 9.10.2 Stack configuration.+- Publish the rolling `dev` prerelease from `master`.+- Replace the retired `macos-13` GitHub Actions runner with `macos-15-intel`.++### Fixed+- #44: Keep WASM RTS options in `package.yaml` so generated Cabal metadata does not drift by [@juliapath](https://github.com/juliapath).+- Fix native and WASM compatibility issues by [@andy0130tw](https://github.com/andy0130tw).+- Fix WASM CI for Agda-2.8.0 by checking out the matching Agda WASM submodule revision.+- Fix WASM dependency resolution by pinning the WASM Cabal package set.+- Fix dev release publishing so native and WASM artefacts are uploaded by the final release job.+- Fix WASM `dist-newstyle` cache restore/save key mismatch.+- Fix unsafe use of `Data.List.head` in rich-text rendering.++## v0.2.7.0.1.5 - 2024-12-18++### Added+- New command line option `--version` and `-V` for printing version information.++## v0.2.7.0.1.4 - 2024-12-6++### Changed+- Target only 3 versions of Agda at a time: Agda-2.7.0.1, Agda-2.6.4.3, and Agda-2.6.3.++## v0.2.7.0.1.3 - 2024-12-5++### Fixed+- Add dummy LSP handlers for `initialized`, `workspace/didChangeConfiguration`, `textDocument/didOpen`, `textDocument/didClose`, `textDocument/didChange`, and `textDocument/didSave` to avoid errors in the client.++## v0.2.7.0.1.2 - 2024-12-4++### Fixed+- Release of artefacts on macOS++## v0.2.7.0.1.1 - 2024-12-4++### Added+- #29: Integration testing for the language server+- Prebuilt binaries for Intel x64 macOS +- Support for Agda-2.7.0.1++### Changed+- Unfied workflow for building and testing the language server across all platforms++## v0.2.7.0.1.0 - 2024-12-2++### Added+- #22: agda 2.6.4 by [@andreasabel](https://github.com/andreasabel)+- #23: lsp 2 by [@andreasabel](https://github.com/andreasabel)++### Fixed+- Version information of the language server++## v0.2.6.4.0.3 - 2023-12-14++### Fixed+- #15: Add missing handlers for `lsp` methods.+- #24: Fix the encoding of binaries built on GitHub Actions.+- Patch path to the "data" directory when the executable is built on GitHub Actions.++## v0.2.6.4.0.0 - 2023-12-12++### Changed+- Embed Agda-2.6.4.+- Builds with `lsp` < 1.7 on GHC 9.2 (LTS 20.26),+ and with Cabal also on 9.4 and 9.6.++### Added+- Build flag `Agda-2-6-3` to embed Agda-2.6.3 rather than 2.6.4.++ ## v0.2.6.3.0 - 2023-11-23 ### Changed@@ -14,6 +123,7 @@ ### Added - Build flag `Agda-2-6-2-2` to embed Agda-2.6.2.2 rather than 2.6.3. + ## v0.2.6.2.2.1 - 2023-11-21 ### Added@@ -21,6 +131,7 @@ - Building with `lsp-1.6`. Builds with `lsp` < 1.7 on GHC 8.10 (LTS 18.28), 9.0 (LTS 19.33), and 9.2 (LTS 20.26). + ## v0.2.6.2.2 - 2023-11-21 ### Changed@@ -29,24 +140,29 @@ - Versioning scheme: _x.a.b.c.d.y_ where _a.b.c.d_ is the 4-digit Agda version (2.6.2.2), _x_ is 0 but may be bumped for revolutionary changes to the agda-language-server, and _y_ is for patch releases. - Builds with `lsp` < 1.5 on GHC 8.10 (LTS 18.28) and 9.0 (LTS 19.33). + ## v0.2.1 - 2021-10-25 No changes. + ## v0.2.0 - 2021-10-22 ### Fixed - #2: Allow user to supply command-line options via agda-mode + ## v0.1.4 - 2021-10-04 ### Fixed - Resume sending HighlightingInfos to agda-mode + ## v0.1.3 - 2021-10-04 ### Fixed - Include DLLs in the bundle+ ## v0.1.2 - 2021-10-03
README.md view
@@ -1,5 +1,16 @@ # Agda Language Server +## Supported versions of Agda++These are the currently supported versions of Agda:+* Agda-2.8.0+* Agda-2.7.0.1+* Agda-2.6.4.3++All releases will come with binaries built with these versions of Agda.++We plan to make the codebase compatible with **at most 3 versions of Agda** at a single time. Because otherwise we'd be drowned by CPP macros for conditional compilation.+ ## Installation The simplest way of acquiring Agda Language Server is through [agda-mode on VS Code](https://github.com/banacorn/agda-mode-vscode#agda-language-server).@@ -7,10 +18,18 @@ ### Prebuilt binaries -You can also download prebuilt binaries [from the release page](https://github.com/banacorn/agda-language-server/releases) if you are using other LSP-compatible text editors.+You can also download prebuilt binaries [from the release page](https://github.com/agda/agda-language-server/releases) if you are using other LSP-compatible text editors. Supported platforms: **Windows**, **Mac**, and **Ubuntu**. +#### Development releases++For testing the latest features and bug fixes, you can download development pre-releases:+- **Stable releases**: Tagged as `v6`, `v7`, etc. - recommended for general use+- **Development releases**: Tagged as `dev` - latest features, may be unstable++Development releases are updated as needed and contain the latest changes from the main branch.+ ### Build from source You will need [Haskell Stack](https://docs.haskellstack.org/en/stable/README/) to build the project:@@ -21,11 +40,32 @@ ## Versioning -The version is _x.y.z.w.a.b.c.d_ where _x.y.z.w_ is the version of the Agda Language Server and _a.b.c.d_ the version of Agda it embeds.-It follows the Haskell PVP (package versioning policy).+Single-digit versioning for the language server itself - people mostly just care about the Agda version it supports anyway. ## Why make it standalone? * for less impact on the Agda codebase * to help [decouple the Agda codebase](https://github.com/agda/agda/projects/5) * we can always merge it back to Agda later anyway++## Hacking++This language server is co-developed alongside [agda-mode on VS Code](https://github.com/banacorn/agda-mode-vscode).++### TCP server for development++To make development easier, you can host the language server locally at `localhost:4096` by running `:main -p` in the REPL (`stack repl`).++Add `lsp://localhost:4096` to `agdaMode.connection.paths` in VS Code's settings, then hit <kbd>C-x</kbd> <kbd>C-s</kbd> to select it as the endpoint.++This allows you to reload the language server in the REPL without recompiling and reinstalling the whole project every time you make changes.++### Creating development releases++To create a development pre-release, push to the `master` branch:++```bash+git push origin master+```++This creates/updates the `dev` pre-release with artifacts from the latest `master` commit on all supported targets.
agda-language-server.cabal view
@@ -1,19 +1,19 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.36.0.+-- This file has been generated from package.yaml by hpack version 0.38.3. -- -- see: https://github.com/sol/hpack name: agda-language-server-version: 0.2.6.3.0+version: 7 synopsis: An implementation of language server protocal (LSP) for Agda 2. description: Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme> category: Development homepage: https://github.com/banacorn/agda-language-server#readme bug-reports: https://github.com/banacorn/agda-language-server/issues author: Ting-Gian LUA-maintainer: banacorn@gmail.com-copyright: 2020 Author name here :)+maintainer: banacorn@gmail.com, Andreas Abel+copyright: 2020-23 Ting-Gian LUA, Andreas ABEL license: MIT license-file: LICENSE build-type: Simple@@ -22,19 +22,34 @@ CHANGELOG.md package.yaml stack.yaml- stack-8.10-Agda-2.6.2.2.yaml- stack-9.0-Agda-2.6.2.2.yaml- stack-9.2-Agda-2.6.2.2.yaml+ stack-9.10.2-Agda-2.6.4.3.yaml+ stack-9.10.2-Agda-2.7.0.1.yaml+ stack-9.10.2-Agda-2.8.0.yaml source-repository head type: git location: https://github.com/banacorn/agda-language-server -flag Agda-2-6-2-2- description: Embed Agda-2.6.2.2 (rather than 2.6.3)+flag Agda-2-6-4+ description: Embed Agda-2.6.4.3 manual: True default: False +flag Agda-2-7-0+ description: Embed Agda-2.7.0.1+ manual: True+ default: False++flag Agda-2-8-0+ description: Embed Agda-2.8.0+ manual: True+ default: False++flag reactor+ description: Build as a WASI reactor module+ manual: True+ default: False+ library exposed-modules: Agda@@ -69,6 +84,7 @@ default-extensions: LambdaCase OverloadedStrings+ PatternSynonyms TypeOperators ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -Werror=incomplete-patterns -fno-warn-orphans build-depends:@@ -77,21 +93,35 @@ , base >=4.7 && <5 , bytestring , containers- , lsp <1.7+ , directory+ , filepath+ , lsp >=2+ , lsp-types >=2 , mtl- , network- , network-simple+ , prettyprinter , process , stm , strict , text default-language: Haskell2010- if flag(Agda-2-6-2-2)+ if flag(Agda-2-6-4) build-depends:- Agda ==2.6.2.2+ Agda ==2.6.4.3+ if flag(Agda-2-7-0)+ build-depends:+ Agda ==2.7.0.1+ if flag(Agda-2-8-0)+ build-depends:+ Agda ==2.8.0+ if arch(wasm32)+ build-depends:+ unix >=2.8.0.0 && <2.9 else build-depends:- Agda ==2.6.3+ network+ , network-simple ==0.4.2+ if !arch(wasm32)+ ghc-options: -threaded executable als main-is: Main.hs@@ -102,8 +132,9 @@ default-extensions: LambdaCase OverloadedStrings+ PatternSynonyms TypeOperators- ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans+ ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans build-depends: Agda , aeson@@ -111,27 +142,52 @@ , base >=4.7 && <5 , bytestring , containers- , lsp <1.7+ , directory+ , filepath+ , lsp >=2+ , lsp-types >=2 , mtl- , network- , network-simple+ , prettyprinter , process , stm , strict , text default-language: Haskell2010- if flag(Agda-2-6-2-2)+ if flag(Agda-2-6-4) build-depends:- Agda ==2.6.2.2+ Agda ==2.6.4.3+ if flag(Agda-2-7-0)+ build-depends:+ Agda ==2.7.0.1+ if flag(Agda-2-8-0)+ build-depends:+ Agda ==2.8.0+ if arch(wasm32)+ build-depends:+ unix >=2.8.0.0 && <2.9 else build-depends:- Agda ==2.6.3+ network+ , network-simple ==0.4.2+ if arch(wasm32)+ ghc-options: -with-rtsopts=-V1+ if flag(reactor)+ other-modules:+ Reactor+ ghc-options: -no-hs-main -optl-mexec-model=reactor -optl-Wl,--export=hs_init,--export=run_setup,--export=new_language_server,--export=free_language_server,--export=run_language_server,--export=send_message,--export=recv_message+ build-depends:+ attoparsec+ , ghc-experimental+ if !arch(wasm32)+ ghc-options: -threaded -with-rtsopts=-N test-suite als-test type: exitcode-stdio-1.0 main-is: Test.hs other-modules:+ Test.LSP Test.SrcLoc+ Test.WASM Agda Agda.Convert Agda.IR@@ -164,18 +220,22 @@ default-extensions: LambdaCase OverloadedStrings+ PatternSynonyms TypeOperators- ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans+ ghc-options: -Wincomplete-patterns -Wunused-do-bind -Wunused-foralls -Wwarnings-deprecations -Wwrong-do-bind -Wmissing-fields -Wmissing-methods -Wmissing-pattern-synonym-signatures -Wmissing-signatures -rtsopts -Werror=incomplete-patterns -fno-warn-orphans build-depends: Agda , aeson , base >=4.7 && <5 , bytestring , containers- , lsp <1.7+ , directory+ , filepath+ , lsp >=2+ , lsp-test+ , lsp-types >=2 , mtl- , network- , network-simple+ , prettyprinter , process , stm , strict@@ -185,9 +245,23 @@ , tasty-quickcheck , text default-language: Haskell2010- if flag(Agda-2-6-2-2)+ if flag(Agda-2-6-4) build-depends:- Agda ==2.6.2.2+ Agda ==2.6.4.3+ if flag(Agda-2-7-0)+ build-depends:+ Agda ==2.7.0.1+ if flag(Agda-2-8-0)+ build-depends:+ Agda ==2.8.0+ if arch(wasm32)+ build-depends:+ unix >=2.8.0.0 && <2.9 else build-depends:- Agda ==2.6.3+ network+ , network-simple ==0.4.2+ if arch(wasm32)+ ghc-options: -with-rtsopts=-V1+ if !arch(wasm32)+ ghc-options: -threaded -with-rtsopts=-N
app/Main.hs view
@@ -1,16 +1,52 @@+{-# LANGUAGE CPP #-} module Main where -import Options-import Server ( run )-import System.Console.GetOpt-import System.Environment ( getArgs )-import Text.Read ( readMaybe )+import Control.Monad (when)+import Options+import Server (run)+-- import Simple (run)+import System.Console.GetOpt+import System.Directory (doesDirectoryExist)+import System.Environment+import System.FilePath ((</>))+import System.IO+import Text.Read (readMaybe) +#if MIN_VERSION_Agda(2,8,0)+import Agda.Setup (setup)+#endif+ main :: IO () main = do+ -- set locale to UTF-8+ -- https://github.com/agda/agda-language-server/issues/24+ hSetEncoding stdout utf8+ hSetEncoding stdin utf8+ hSetEncoding stderr utf8++-- getExecutablePath returns argv[0] in WASM, which is useless+#ifndef wasm32_HOST_ARCH+ -- The GitHub CI-built executable lacks the correct data directory path.+ -- If there's directory named "data" in the executable's directory,+ -- then we assume that the executable is built by GitHub CI+ -- and we should set the $Agda_datadir environment variable to the correct directory.+ executablePath <- getExecutablePath+ let dataDir = executablePath </> "data"+ isBuiltByCI <- doesDirectoryExist dataDir+ when isBuiltByCI $ do+ setEnv "Agda_datadir" dataDir+#endif+ options <- getOptionsFromArgv- if optHelp options- then putStrLn usageMessage- else do- _ <- run options- return ()+ case () of+ _ | optHelp options -> putStrLn usageMessage+ | optVersion options -> putStrLn versionString+#if MIN_VERSION_Agda(2,8,0)+ | optSetup options -> do+ setup True+ return ()+#endif+ | otherwise -> do+ _ <- run options+ -- _ <- run+ return ()
+ app/Reactor.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE CPP #-}+module Reactor where++import GHC.Wasm.Prim+import Options+import Server (serverDefn)+import qualified Data.Text as T+import qualified Data.ByteString as B+import qualified Data.ByteString.Lazy as BL+import qualified Data.Text.Lazy as TL+import Data.Text.Encoding (encodeUtf8)+import Data.Text.Lazy.Encoding (decodeUtf8)+import Control.Concurrent (MVar, newEmptyMVar, takeMVar, putMVar)+import Foreign.StablePtr (StablePtr, newStablePtr, freeStablePtr, deRefStablePtr)++import Data.ByteString.Lazy (LazyByteString)+import Language.LSP.Server (ServerConfig(..), runServerWithConfig)+import qualified Data.Attoparsec.ByteString as Attoparsec++data ReactorEnv = ReactorEnv+ { options :: Options+ , incomingMessage :: MVar B.StrictByteString+ , outgoingMessage :: MVar String+ }++initialEnv :: IO ReactorEnv+initialEnv = ReactorEnv <$> getOptionsFromArgv <*> newEmptyMVar <*> newEmptyMVar++type ServerHandle = StablePtr ReactorEnv++foreign export javascript "run_setup"+ runSetup :: IO ()++foreign export javascript "new_language_server"+ newLanguageServer :: IO ServerHandle++foreign export javascript "run_language_server"+ runLanguageServer :: ServerHandle -> IO Int++foreign export javascript "free_language_server"+ freeLanguageServer :: ServerHandle -> IO ()++foreign export javascript "send_message"+ sendMessage :: ServerHandle -> JSString -> IO ()++foreign export javascript "recv_message"+ recvMessage :: ServerHandle -> IO JSString++runSetup :: IO ()+#if MIN_VERSION_Agda(2,8,0)+runSetup = setup True+#else+runSetup = error "This Agda version does not have setup functionality."+#endif++newLanguageServer :: IO ServerHandle+newLanguageServer = initialEnv >>= newStablePtr++freeLanguageServer :: ServerHandle -> IO ()+freeLanguageServer = freeStablePtr++runLanguageServer :: ServerHandle -> IO Int+runLanguageServer hdl = do+ env <- deRefStablePtr hdl++ let+ serverInwards :: IO B.StrictByteString+ serverInwards = takeMVar (incomingMessage env)++ serverOutwards :: BL.LazyByteString -> IO ()+ serverOutwards s = (return . TL.unpack . decodeUtf8) s >>= putMVar (outgoingMessage env)++ runFromReactor serverInwards serverOutwards (options env)++runFromReactor :: IO B.StrictByteString -> (LazyByteString -> IO ()) -> Options -> IO Int+runFromReactor serverInwards serverOutwards options = do+ runServerWithConfig serverConfig (serverDefn options)+ where+ serverConfig :: ServerConfig Config+ serverConfig = ServerConfig+ { ioLogger = mempty+ , lspLogger = mempty+ , inwards = serverInwards+ , outwards = serverOutwards+ , prepareOutwards = id+ , parseInwards = do+ -- using takeByteString here will make it return partial result,+ -- requiring another empty string to signal its end+ chunk <- Attoparsec.getChunk+ case chunk of+ Nothing -> pure B.empty+ Just xs -> Attoparsec.take $ B.length xs+ }++sendMessage :: ServerHandle -> JSString -> IO ()+sendMessage hdl s = do+ env <- deRefStablePtr hdl+ let input = fromJSString s+ putMVar (incomingMessage env) $ (encodeUtf8 . T.pack) input+ return ()++recvMessage :: ServerHandle -> IO JSString+recvMessage hdl = do+ env <- deRefStablePtr hdl+ str <- takeMVar (outgoingMessage env)+ return $ toJSString str++-- for shimming types when GHC.Wasm.Prim is not available, e.g., when using HLS+#if 0+data JSVal = JSVal {}+newtype JSString = JSString JSVal++fromJSString :: JSString -> String+fromJSString = undefined+toJSString :: String -> JSString+toJSString = undefined+#endif
package.yaml view
@@ -1,19 +1,19 @@ name: agda-language-server-version: 0.2.6.3.0+version: 7 github: "banacorn/agda-language-server" license: MIT author: "Ting-Gian LUA"-maintainer: "banacorn@gmail.com"-copyright: "2020 Author name here :)"+maintainer: "banacorn@gmail.com, Andreas Abel"+copyright: "2020-23 Ting-Gian LUA, Andreas ABEL" extra-source-files: - README.md - CHANGELOG.md - package.yaml - stack.yaml-- stack-8.10-Agda-2.6.2.2.yaml-- stack-9.0-Agda-2.6.2.2.yaml-- stack-9.2-Agda-2.6.2.2.yaml+- stack-9.10.2-Agda-2.6.4.3.yaml+- stack-9.10.2-Agda-2.7.0.1.yaml+- stack-9.10.2-Agda-2.8.0.yaml # Metadata used when publishing your package synopsis: An implementation of language server protocal (LSP) for Agda 2.@@ -25,19 +25,40 @@ description: Please see the README on GitHub at <https://github.com/agda/agda-language-server#readme> flags:- Agda-2-6-2-2:- description: Embed Agda-2.6.2.2 (rather than 2.6.3)+ Agda-2-6-4:+ description: Embed Agda-2.6.4.3 manual: true default: false-+ Agda-2-7-0:+ description: Embed Agda-2.7.0.1+ manual: true+ default: false+ Agda-2-8-0:+ description: Embed Agda-2.8.0+ manual: true+ default: false+ reactor:+ description: Build as a WASI reactor module+ manual: true+ default: false when:-- condition: flag(Agda-2-6-2-2)+- condition: "flag(Agda-2-6-4)"+ dependencies:+ - Agda == 2.6.4.3+- condition: "flag(Agda-2-7-0)"+ dependencies:+ - Agda == 2.7.0.1+- condition: "flag(Agda-2-8-0)"+ dependencies:+ - Agda == 2.8.0+- condition: "arch(wasm32)" then: dependencies:- - Agda == 2.6.2.2+ - unix >= 2.8.0.0 && < 2.9 else: dependencies:- - Agda == 2.6.3+ - network+ - network-simple == 0.4.2 dependencies: - base >= 4.7 && < 5@@ -45,18 +66,21 @@ - aeson - bytestring - containers- - lsp < 1.7+ - directory+ - filepath+ - lsp-types >= 2+ - lsp >= 2 - mtl- - network- - network-simple - strict - stm - text - process+ - prettyprinter default-extensions: - LambdaCase - OverloadedStrings+- PatternSynonyms - TypeOperators library:@@ -73,6 +97,10 @@ - -Wmissing-signatures - -Werror=incomplete-patterns - -fno-warn-orphans+ when:+ - condition: "!arch(wasm32)"+ ghc-options:+ - -threaded executables: als:@@ -88,11 +116,26 @@ - -Wmissing-methods - -Wmissing-pattern-synonym-signatures - -Wmissing-signatures- - -threaded - -rtsopts- - -with-rtsopts=-N - -Werror=incomplete-patterns - -fno-warn-orphans+ when:+ - condition: "arch(wasm32)"+ ghc-options: -with-rtsopts=-V1+ - condition: "flag(reactor)"+ other-modules:+ - Reactor+ dependencies:+ - ghc-experimental+ - attoparsec+ ghc-options:+ - -no-hs-main+ - -optl-mexec-model=reactor+ - -optl-Wl,--export=hs_init,--export=run_setup,--export=new_language_server,--export=free_language_server,--export=run_language_server,--export=send_message,--export=recv_message+ - condition: "!arch(wasm32)"+ ghc-options:+ - -threaded+ - -with-rtsopts=-N dependencies: - agda-language-server @@ -103,6 +146,7 @@ - test - src dependencies:+ - lsp-test - tasty - tasty-hunit - tasty-golden@@ -118,11 +162,16 @@ - -Wmissing-methods - -Wmissing-pattern-synonym-signatures - -Wmissing-signatures- - -threaded - -rtsopts- - -with-rtsopts=-N - -Werror=incomplete-patterns - -fno-warn-orphans+ when:+ - condition: "arch(wasm32)"+ ghc-options: -with-rtsopts=-V1+ - condition: "!arch(wasm32)"+ ghc-options:+ - -threaded+ - -with-rtsopts=-N # tests: # als-test:
src/Agda.hs view
@@ -8,25 +8,39 @@ , runAgda , sendCommand , getCommandLineOptions+ , CommandReq(..)+ , CommandRes(..) ) where +import Prelude hiding ( null )+ import Agda.Compiler.Backend ( parseBackendOptions ) import Agda.Compiler.Builtin ( builtinBackends ) import Agda.Convert ( fromResponse ) import Agda.Interaction.Base ( Command , Command'(Command, Done, Error)+#if MIN_VERSION_Agda(2,7,0)+#else , CommandM+#endif , CommandState(optionsOnReload) , IOTCM , initCommandState-#if MIN_VERSION_Agda(2,6,3) , parseIOTCM-#endif )++#if MIN_VERSION_Agda(2,8,0)+import Agda.Interaction.Command ( CommandM )+#endif+import Agda.Syntax.Common.Pretty ( render, vcat ) import Agda.Interaction.InteractionTop ( initialiseCommandQueue , maybeAbort , runInteraction+#if MIN_VERSION_Agda(2,8,0)+#elif MIN_VERSION_Agda(2,7,0)+ , CommandM+#endif ) import Agda.Interaction.Options ( CommandLineOptions ( optAbsoluteIncludePaths@@ -53,6 +67,7 @@ ) , Impossible )+import Agda.Utils.Null ( null ) import Agda.VersionCommit ( versionWithCommitInfo ) import Control.Exception ( SomeException , catch@@ -73,9 +88,14 @@ import Language.LSP.Server ( getConfig ) import Monad import Options ( Config(configRawAgdaOptions)- , Options(optRawAgdaOptions)+ , Options(optRawAgdaOptions, optRawResponses)+ , versionNumber ) +import qualified Agda.IR as IR+import Agda.Interaction.JSON ( encode, encodeTCM )+import Agda.Interaction.JSONTop ()+ getAgdaVersion :: String getAgdaVersion = versionWithCommitInfo @@ -88,9 +108,15 @@ result <- runAgda $ do -- decides how to output Response lift $ setInteractionOutputCallback $ \response -> do- reaction <- fromResponse response- sendResponse env reaction+ resp <- if optRawResponses (envOptions env)+ then do+ value <- (pure . encodeTCM) response+ resp' <- fmap IR.ResponseJSONRaw value+ return resp'+ else fromResponse response + sendResponse env resp+ -- keep reading command commands <- liftIO $ initialiseCommandQueue (readCommand env) @@ -154,7 +180,7 @@ handleCommandReq :: MonadIO m => CommandReq -> ServerM m CommandRes-handleCommandReq CmdReqSYN = return $ CmdResACK Agda.getAgdaVersion+handleCommandReq CmdReqSYN = return $ CmdResACK Agda.getAgdaVersion versionNumber handleCommandReq (CmdReq cmd) = do case parseIOTCM cmd of Left err -> do@@ -165,14 +191,6 @@ provideCommand iotcm return $ CmdRes Nothing -#if !MIN_VERSION_Agda(2,6,3)-parseIOTCM :: String -> Either String IOTCM-parseIOTCM raw = case listToMaybe $ reads raw of- Just (x, "" ) -> Right x- Just (_, remnent) -> Left $ "not consumed: " ++ remnent- _ -> Left $ "cannot read: " ++ raw-#endif- -------------------------------------------------------------------------------- getCommandLineOptions@@ -187,12 +205,8 @@ result <- runExceptT $ do let p = parseBackendOptions builtinBackends merged defaultOptions-#if MIN_VERSION_Agda(2,6,3) let (r, _warns) = runOptM p (bs, opts) <- ExceptT $ pure r-#else- (bs, opts) <- ExceptT $ runOptM p-#endif return opts case result of -- something bad happened, use the default options instead@@ -218,7 +232,7 @@ s2s <- prettyTCWarnings' =<< getAllWarningsOfTCErr err s1 <- prettyError err let ss = filter (not . null) $ s2s ++ [s1]- let errorMsg = unlines ss+ let errorMsg = render $ vcat ss return (Left errorMsg) handleImpossible :: Impossible -> TCM (Either String a)@@ -234,11 +248,13 @@ | CmdReq String deriving (Generic) +instance ToJSON CommandReq instance FromJSON CommandReq data CommandRes = CmdResACK -- ^ For server to complete a 2-way handshake String -- ^ Version number of Agda+ Int -- ^ Version number of the language server | CmdRes -- ^ Response for 'CmdReq' (Maybe CommandErr) -- ^ 'Nothing' to indicate success deriving (Generic)
src/Agda/Convert.hs view
@@ -2,17 +2,24 @@ module Agda.Convert where -import Render ( Block(..), Inlines, renderATop, Render(..) )- import Agda.IR (FromAgda (..)) import qualified Agda.IR as IR import Agda.Interaction.Base import Agda.Interaction.BasicOps as B import Agda.Interaction.EmacsCommand (Lisp)+import Agda.Interaction.EmacsTop (showInfoError) import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms) import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..)) import qualified Agda.Interaction.Highlighting.Range as Highlighting+#if MIN_VERSION_Agda(2,8,0)+import Agda.Interaction.Command (localStateCommandM)+import Agda.TypeChecking.Monad.Base (topLevelModuleFilePath)+#else import Agda.Interaction.InteractionTop (localStateCommandM)+#endif+#if MIN_VERSION_Agda(2,7,0)+import Agda.Interaction.Output ( OutputConstraint )+#endif import Agda.Interaction.Response as R import Agda.Syntax.Abstract as A import Agda.Syntax.Abstract.Pretty (prettyATop)@@ -21,7 +28,7 @@ import Agda.Syntax.Internal (alwaysUnblock) import Agda.Syntax.Position (HasRange (getRange), Range, noRange) import Agda.Syntax.Scope.Base-import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError)+import Agda.TypeChecking.Errors (explainWhyInScope, getAllWarningsOfTCErr, prettyError) import Agda.TypeChecking.Monad hiding (Function) import Agda.TypeChecking.Monad.MetaVars (withInteractionId) import Agda.TypeChecking.Pretty (prettyTCM)@@ -34,8 +41,7 @@ import Agda.Utils.Impossible (__IMPOSSIBLE__) import Agda.Utils.Maybe (catMaybes) import Agda.Utils.Null (empty)-import Agda.Utils.Pretty hiding (render)-import Agda.Utils.RangeMap ( IsBasicRangeMap(toList) )+import Agda.Utils.RangeMap (IsBasicRangeMap (toList)) import Agda.Utils.String (delimiter) import Agda.Utils.Time (CPUTime) import Agda.VersionCommit (versionWithCommitInfo)@@ -46,9 +52,13 @@ import qualified Data.List as List import qualified Data.Map as Map import Data.String (IsString)+import Render (Block (..), Inlines, Render (..), renderATop) import qualified Render -responseAbbr :: IsString a => Response -> a+import Agda.Syntax.Common.Pretty hiding (render)+import qualified Prettyprinter++responseAbbr :: (IsString a) => Response -> a responseAbbr res = case res of Resp_HighlightingInfo {} -> "Resp_HighlightingInfo" Resp_Status {} -> "Resp_Status"@@ -57,6 +67,9 @@ Resp_GiveAction {} -> "Resp_GiveAction" Resp_MakeCase {} -> "Resp_MakeCase" Resp_SolveAll {} -> "Resp_SolveAll"+#if MIN_VERSION_Agda(2,7,0)+ Resp_Mimer {} -> "Resp_Mimer"+#endif Resp_DisplayInfo {} -> "Resp_DisplayInfo" Resp_RunningInfo {} -> "Resp_RunningInfo" Resp_ClearRunningInfo {} -> "Resp_ClearRunningInfo"@@ -87,6 +100,9 @@ return $ IR.ResponseGiveAction i (fromAgda giveAction) fromResponse (Resp_MakeCase _ Function pcs) = return $ IR.ResponseMakeCaseFunction pcs fromResponse (Resp_MakeCase _ ExtendedLambda pcs) = return $ IR.ResponseMakeCaseExtendedLambda pcs+#if MIN_VERSION_Agda(2,7,0)+fromResponse (Resp_Mimer (InteractionId i) s) = return $ IR.ResponseMimer i s+#endif fromResponse (Resp_SolveAll ps) = return $ IR.ResponseSolveAll (fmap prn ps) where prn (InteractionId i, e) = (i, prettyShow e)@@ -115,7 +131,11 @@ (defSite <$> definitionSite aspects) where defSite (DefinitionSite moduleName offset _ _) =+#if MIN_VERSION_Agda(2,8,0)+ (filePath (topLevelModuleFilePath modFile moduleName), offset)+#else (filePath (Map.findWithDefault __IMPOSSIBLE__ moduleName modFile), offset)+#endif infos :: [IR.HighlightingInfo] infos = fmap fromAspects (toList h)@@ -136,8 +156,13 @@ fromDisplayInfo = \case Info_CompilationOk _ ws -> do -- filter+#if MIN_VERSION_Agda(2,8,0)+ filteredWarnings <- filterTCWarnings (tcWarnings ws)+ filteredErrors <- filterTCWarnings (nonFatalErrors ws)+#else let filteredWarnings = filterTCWarnings (tcWarnings ws) let filteredErrors = filterTCWarnings (nonFatalErrors ws)+#endif -- serializes warnings <- mapM prettyTCM filteredWarnings errors <- mapM prettyTCM filteredErrors@@ -157,8 +182,13 @@ -- errors / warnings -- filter+#if MIN_VERSION_Agda(2,8,0)+ filteredWarnings <- filterTCWarnings (tcWarnings ws)+ filteredErrors <- filterTCWarnings (nonFatalErrors ws)+#else let filteredWarnings = filterTCWarnings (tcWarnings ws) let filteredErrors = filterTCWarnings (nonFatalErrors ws)+#endif -- serializes warnings <- mapM prettyTCM filteredWarnings errors <- mapM prettyTCM filteredErrors@@ -256,15 +286,11 @@ return (prettyShow x, ":" <+> doc) let doc = "Definitions about"- <+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)+ <+> text (List.intercalate ", " $ words names)+ $$ nest 2 (align 10 hitDocs) return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]-#if MIN_VERSION_Agda(2,6,3)- Info_WhyInScope (WhyInScopeData q cwd v xs ms) -> do- doc <- explainWhyInScope (prettyShow q) cwd v xs ms-#else- Info_WhyInScope s cwd v xs ms -> do- doc <- explainWhyInScope s cwd v xs ms-#endif+ Info_WhyInScope why -> do+ doc <- explainWhyInScope why return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing] Info_Context ii ctx -> do doc <- localTCState (prettyResponseContexts ii False ctx)@@ -302,30 +328,36 @@ auxSect <- case aux of GoalOnly -> return []- GoalAndHave expr -> do+ GoalAndHave expr bndry -> do+ -- TODO: render bndry rendered <- renderATop expr raw <- show <$> prettyATop expr return [Labeled rendered (Just raw) Nothing "Have" "special"]- GoalAndElaboration term -> do- let rendered = render term- raw <- show <$> TCP.prettyTCM term+ GoalAndElaboration expr -> do+#if MIN_VERSION_Agda(2,8,0)+ rendered <- renderATop expr+#else+ let rendered = render expr+#endif+ raw <- show <$> TCP.prettyTCM expr return [Labeled rendered (Just raw) Nothing "Elaborates to" "special"] let boundarySect = if null boundaries then [] else- Header "Boundary" :- fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries+ Header "Boundary"+ : fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries contextSect <- reverse . concat <$> mapM (renderResponseContext ii) resCtxs let constraintSect =- if null constraints- then []- else- Header "Constraints" :- fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints+ if null constraints+ then []+ else+ Header "Constraints"+ : fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints return $- IR.DisplayInfoGeneric "Goal type etc" $ goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect+ IR.DisplayInfoGeneric "Goal type etc" $+ goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect Goal_CurrentGoal norm -> do (rendered, raw) <- prettyTypeOfMeta norm ii return $ IR.DisplayInfoCurrentGoal (Unlabeled rendered (Just raw) Nothing)@@ -348,121 +380,6 @@ -------------------------------------------------------------------------------- --- | Serializing Info_Error-showInfoError :: Info_Error -> TCM String-showInfoError (Info_GenericError err) = do- e <- prettyError err- w <- prettyTCWarnings' =<< getAllWarningsOfTCErr err-- let errorMsg =- if null w- then e- else delimiter "Error" ++ "\n" ++ e- let warningMsg =- List.intercalate "\n" $- delimiter "Warning(s)" :- filter (not . null) w- return $- if null w- then errorMsg- else errorMsg ++ "\n\n" ++ warningMsg-showInfoError (Info_CompilationError warnings) = do- s <- prettyTCWarnings warnings- return $- unlines- [ "You need to fix the following errors before you can compile",- "the module:",- "",- s- ]-showInfoError (Info_HighlightingParseError ii) =- return $ "Highlighting failed to parse expression in " ++ show ii-showInfoError (Info_HighlightingScopeCheckError ii) =- return $ "Highlighting failed to scope check expression in " ++ show ii--explainWhyInScope ::- String ->- FilePath ->- Maybe LocalVar ->- [AbstractName] ->- [AbstractModule] ->- TCM Doc-explainWhyInScope s _ Nothing [] [] = TCP.text (s ++ " is not in scope.")-explainWhyInScope s _ v xs ms =- TCP.vcat- [ TCP.text (s ++ " is in scope as"),- TCP.nest 2 $ TCP.vcat [variable v xs, modules ms]- ]- where- -- variable :: Maybe _ -> [_] -> TCM Doc- variable Nothing vs = names vs- variable (Just x) vs- | null vs = asVar- | otherwise =- TCP.vcat- [ TCP.sep [asVar, TCP.nest 2 $ shadowing x],- TCP.nest 2 $ names vs- ]- where- asVar :: TCM Doc- asVar =- "* a variable bound at" TCP.<+> TCP.prettyTCM (nameBindingSite $ localVar x)- shadowing :: LocalVar -> TCM Doc- shadowing (LocalVar _ _ []) = "shadowing"- shadowing _ = "in conflict with"- names = TCP.vcat . fmap pName- modules = TCP.vcat . fmap pMod-- pKind = \case- AxiomName -> "postulate"- ConName -> "constructor"- CoConName -> "coinductive constructor"- DataName -> "data type"- DisallowedGeneralizeName -> "generalizable variable from let open"- FldName -> "record field"- FunName -> "defined name"- GeneralizeName -> "generalizable variable"- MacroName -> "macro name"- PatternSynName -> "pattern synonym"- PrimName -> "primitive function"- QuotableName -> "quotable name"- -- previously DefName:- RecName -> "record type"- OtherDefName -> "defined name"-- pName :: AbstractName -> TCM Doc- pName a =- TCP.sep- [ "* a"- TCP.<+> pKind (anameKind a)- TCP.<+> TCP.text (prettyShow $ anameName a),- TCP.nest 2 "brought into scope by"- ]- TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a))- pMod :: AbstractModule -> TCM Doc- pMod a =- TCP.sep- [ "* a module" TCP.<+> TCP.text (prettyShow $ amodName a),- TCP.nest 2 "brought into scope by"- ]- TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ mnameToQName $ amodName a) (amodLineage a))-- pWhy :: Range -> WhyInScope -> TCM Doc- pWhy r Defined = "- its definition at" TCP.<+> TCP.prettyTCM r- pWhy r (Opened (C.QName x) w) | isNoName x = pWhy r w- pWhy r (Opened m w) =- "- the opening of"- TCP.<+> TCP.prettyTCM m- TCP.<+> "at"- TCP.<+> TCP.prettyTCM (getRange m)- TCP.$$ pWhy r w- pWhy r (Applied m w) =- "- the application of"- TCP.<+> TCP.prettyTCM m- TCP.<+> "at"- TCP.<+> TCP.prettyTCM (getRange m)- TCP.$$ pWhy r w- -- | Pretty-prints the context of the given meta-variable. prettyResponseContexts :: -- | Context of this meta-variable.@@ -482,7 +399,7 @@ ResponseContextEntry -> TCM [(String, Doc)] prettyResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do- modality <- asksTC getModality+ modality <- currentModality do let prettyCtxName :: String prettyCtxName@@ -531,10 +448,9 @@ ResponseContextEntry -> TCM [Block] renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do- modality <- asksTC getModality+ modality <- currentModality do- let- rawCtxName :: String+ let rawCtxName :: String rawCtxName | n == x = prettyShow x | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x@@ -558,7 +474,7 @@ where c = render (getCohesion ai) - extras :: IsString a => [a]+ extras :: (IsString a) => [a] extras = concat [ ["not in scope" | isInScope nis == C.NotInScope],@@ -588,7 +504,7 @@ -- rendered renderedExpr <- renderATop expr let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2- -- (Render.fsep $ Render.punctuate "," extras)+ -- (Render.fsep $ Render.punctuate "," extras) -- result let typeItem = Unlabeled renderedType (Just rawType) Nothing@@ -615,7 +531,6 @@ parenSep2 docs | null docs = mempty | otherwise = (" " Render.<+>) $ Render.parens $ Render.fsep $ Render.punctuate "," docs- -- | Pretty-prints the type of the meta-variable. prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
src/Agda/IR.hs view
@@ -20,6 +20,7 @@ fromAgdaTCM :: a -> TCM b --------------------------------------------------------------------------------+ -- | IR for IOCTM data Response = -- non-last responses@@ -40,8 +41,11 @@ ResponseMakeCaseFunction [String] | ResponseMakeCaseExtendedLambda [String] | ResponseSolveAll [(Int, String)]+ | ResponseMimer Int (Maybe String) | -- priority: 3 ResponseJumpToError FilePath Int+ | -- raw form+ ResponseJSONRaw Value | ResponseEnd deriving (Generic)
src/Agda/Parser.hs view
@@ -6,19 +6,16 @@ import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser) import Agda.Syntax.Parser.Tokens (Token)-import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')-#if MIN_VERSION_Agda(2,6,3)-import Agda.Syntax.Position (RangeFile(RangeFile))-#endif+import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, RangeFile (RangeFile), getRange, rEnd', rStart') import Agda.Utils.FileName (mkAbsolute)-import Monad ( ServerM ) import Control.Monad.State import Data.List (find) import Data.Maybe (fromMaybe) import Data.Text (Text, unpack) import qualified Data.Text as Text+import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Server (LspM)-import qualified Language.LSP.Types as LSP+import Monad (ServerM) import Options (Config) --------------------------------------------------------------------------------@@ -27,22 +24,12 @@ tokenAt uri source position = case LSP.uriToFilePath uri of Nothing -> return Nothing Just filepath -> do- let file =-#if MIN_VERSION_Agda(2,6,3)- RangeFile (mkAbsolute filepath) Nothing-#else- mkAbsolute filepath-#endif+ let file = RangeFile (mkAbsolute filepath) Nothing (result, _warnings) <- liftIO $ runPMIO $ do -- parse the file and get all tokens (r, _fileType) <- parseFile tokensParser file (unpack source)- let tokens =-#if MIN_VERSION_Agda(2,6,3)- fst r-#else- r-#endif+ let tokens = fst r -- find the token at the position return $ find (pointedBy position) tokens case result of
src/Agda/Position.hs view
@@ -1,63 +1,69 @@ {-# LANGUAGE CPP #-} module Agda.Position- ( ToOffset(..)- , makeToOffset- , toOffset- , FromOffset(..)- , makeFromOffset- , fromOffset- , toAgdaPositionWithoutFile- , toAgdaRange- , prettyPositionWithoutFile- -- , toLSPRange- -- , toLSPPosition- ) where+ ( ToOffset (..),+ makeToOffset,+ toOffset,+ FromOffset (..),+ makeFromOffset,+ fromOffset,+ toAgdaPositionWithoutFile,+ toAgdaRange,+ prettyPositionWithoutFile,+ -- , toLSPRange+ -- , toLSPPosition+ )+where -import Agda.Syntax.Position-import Agda.Utils.FileName ( AbsolutePath(AbsolutePath) )-import Data.IntMap ( IntMap )-import qualified Data.IntMap as IntMap-import qualified Data.Sequence as Seq-import qualified Data.Strict.Maybe as Strict-import Data.Text ( Text )-import qualified Data.Text as Text-import qualified Language.LSP.Types as LSP+import Agda.Syntax.Position+import Agda.Utils.FileName (AbsolutePath (AbsolutePath))+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import qualified Data.Sequence as Seq+import qualified Data.Strict.Maybe as Strict+import Data.Text (Text)+import qualified Data.Text as Text+import qualified Language.LSP.Protocol.Types as LSP -- Note: LSP srclocs are 0-base -- Agda srclocs are 1-base --------------------------------------------------------------------------------+ -- | LSP source locations => Agda source locations -- | LSP Range -> Agda Range toAgdaRange :: ToOffset -> Text -> LSP.Range -> Range-toAgdaRange table path (LSP.Range start end) = Range- (Strict.Just $ mkRangeFile $ AbsolutePath path)- (Seq.singleton interval)- where- interval :: IntervalWithoutFile- interval = Interval (toAgdaPositionWithoutFile table start)- (toAgdaPositionWithoutFile table end)-#if MIN_VERSION_Agda(2,6,3)- mkRangeFile path = RangeFile path Nothing-#else- mkRangeFile = id+toAgdaRange table path (LSP.Range start end) =+ Range+ (Strict.Just $ mkRangeFile $ AbsolutePath path)+ (Seq.singleton interval)+ where+ interval :: IntervalWithoutFile+ interval =+ Interval+#if MIN_VERSION_Agda(2,8,0)+ () #endif+ (toAgdaPositionWithoutFile table start)+ (toAgdaPositionWithoutFile table end)+ mkRangeFile path = RangeFile path Nothing -- | LSP Position -> Agda PositionWithoutFile toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile-toAgdaPositionWithoutFile table (LSP.Position line col) = Pn- ()- (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)- (fromIntegral line + 1)- (fromIntegral col + 1)+toAgdaPositionWithoutFile table (LSP.Position line col) =+ Pn+ ()+ (fromIntegral (toOffset table (fromIntegral line, fromIntegral col)) + 1)+ (fromIntegral line + 1)+ (fromIntegral col + 1) prettyPositionWithoutFile :: PositionWithoutFile -> String prettyPositionWithoutFile pos@(Pn () offset _line _col) = "[" <> show pos <> "-" <> show offset <> "]" --------------------------------------------------------------------------------+ -- | Positon => Offset convertion -- Keeps record of offsets of every line break ("\n", "\r" and "\r\n")@@ -67,38 +73,39 @@ -- >def123\r\n (2, 11) -- >ghi\r (3, 15) ---newtype ToOffset = ToOffset { unToOffset :: IntMap Int }+newtype ToOffset = ToOffset {unToOffset :: IntMap Int} data Accum = Accum- { accumPreviousChar :: Maybe Char- , accumCurrentOffset :: Int- , accumCurrentLine :: Int- , accumResult :: IntMap Int+ { accumPreviousChar :: Maybe Char,+ accumCurrentOffset :: Int,+ accumCurrentLine :: Int,+ accumResult :: IntMap Int } -- | Return a list of offsets of linebreaks ("\n", "\r" or "\r\n") makeToOffset :: Text -> ToOffset makeToOffset = ToOffset . accumResult . Text.foldl' go initAccum- where- initAccum :: Accum- initAccum = Accum Nothing 0 0 IntMap.empty+ where+ initAccum :: Accum+ initAccum = Accum Nothing 0 0 IntMap.empty - go :: Accum -> Char -> Accum- go (Accum (Just '\r') n l table) '\n' =- Accum (Just '\n') (1 + n) l (IntMap.updateMax (Just . succ) table)- go (Accum previous n l table) '\n' =- Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)- go (Accum previous n l table) '\r' =- Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)- go (Accum previous n l table) char = Accum (Just char) (1 + n) l table+ go :: Accum -> Char -> Accum+ go (Accum (Just '\r') n l table) '\n' =+ Accum (Just '\n') (1 + n) l (IntMap.updateMax (Just . succ) table)+ go (Accum previous n l table) '\n' =+ Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)+ go (Accum previous n l table) '\r' =+ Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + l) (1 + n) table)+ go (Accum previous n l table) char = Accum (Just char) (1 + n) l table -- | (line, col) => offset (zero-based) toOffset :: ToOffset -> (Int, Int) -> Int toOffset (ToOffset table) (line, col) = case IntMap.lookup line table of- Nothing -> col+ Nothing -> col Just offset -> offset + col --------------------------------------------------------------------------------+ -- | Offset => Position convertion -- An IntMap for speeding up Offset => Position convertion@@ -109,29 +116,32 @@ -- >def123\r\n (11, 2) -- >ghi\r (15, 3) ---newtype FromOffset = FromOffset { unFromOffset :: IntMap Int }+newtype FromOffset = FromOffset {unFromOffset :: IntMap Int} fromOffset :: FromOffset -> Int -> (Int, Int) fromOffset (FromOffset table) offset = case IntMap.lookupLE offset table of- Nothing -> (0, offset) -- no previous lines+ Nothing -> (0, offset) -- no previous lines Just (offsetOfFirstChar, lineNo) -> (lineNo, offset - offsetOfFirstChar) makeFromOffset :: Text -> FromOffset-makeFromOffset = FromOffset . accumResult . Text.foldl'- go- (Accum Nothing 0 0 IntMap.empty)- where- go :: Accum -> Char -> Accum- -- encountered a "\r\n", update the latest entry- go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of- ((offset, lineNo), table') ->- Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table')- -- encountered a line break, add a new entry- go (Accum previous n l table) '\n' =- Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)- go (Accum previous n l table) '\r' =- Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)- go (Accum previous n l table) char = Accum (Just char) (1 + n) l table+makeFromOffset =+ FromOffset+ . accumResult+ . Text.foldl'+ go+ (Accum Nothing 0 0 IntMap.empty)+ where+ go :: Accum -> Char -> Accum+ -- encountered a "\r\n", update the latest entry+ go (Accum (Just '\r') n l table) '\n' = case IntMap.deleteFindMax table of+ ((offset, lineNo), table') ->+ Accum (Just '\n') (1 + n) l (IntMap.insert (1 + offset) lineNo table')+ -- encountered a line break, add a new entry+ go (Accum previous n l table) '\n' =+ Accum (Just '\n') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)+ go (Accum previous n l table) '\r' =+ Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table)+ go (Accum previous n l table) char = Accum (Just char) (1 + n) l table -- -------------------------------------------------------------------------------- -- -- | Agda Highlighting Range -> Agda Range
src/Monad.hs view
@@ -1,43 +1,46 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-}-module Monad where -import Agda.IR--import Agda.Interaction.Base ( IOTCM )-import Agda.TypeChecking.Monad ( TCMT )-import Control.Concurrent-import Control.Monad.Reader-import Data.Text ( Text- , pack- )-import Server.CommandController ( CommandController )-import qualified Server.CommandController as CommandController-import Server.ResponseController ( ResponseController )-import qualified Server.ResponseController as ResponseController+module Monad where -import Data.IORef ( IORef- , modifyIORef'- , newIORef- , readIORef- , writeIORef- )-import Data.Maybe ( isJust )-import Language.LSP.Server ( MonadLsp- , getConfig- )-import qualified Language.LSP.Types as LSP-import Options+import Agda.IR+import Agda.Interaction.Base (IOTCM)+import Agda.TypeChecking.Monad (TCMT)+import Control.Concurrent+import Control.Monad.Reader+import Data.IORef+ ( IORef,+ modifyIORef',+ newIORef,+ readIORef,+ writeIORef,+ )+import Data.Maybe (isJust)+import Data.Text+ ( Text,+ pack,+ )+import qualified Language.LSP.Protocol.Types as LSP+import Language.LSP.Server+ ( MonadLsp,+ getConfig,+ )+import Options+import Server.CommandController (CommandController)+import qualified Server.CommandController as CommandController+import Server.ResponseController (ResponseController)+import qualified Server.ResponseController as ResponseController -------------------------------------------------------------------------------- data Env = Env- { envOptions :: Options- , envDevMode :: Bool- , envConfig :: Config- , envLogChan :: Chan Text- , envCommandController :: CommandController- , envResponseChan :: Chan Response- , envResponseController :: ResponseController+ { envOptions :: Options,+ envDevMode :: Bool,+ envConfig :: Config,+ envLogChan :: Chan Text,+ envCommandController :: CommandController,+ envResponseChan :: Chan Response,+ envResponseController :: ResponseController } createInitEnv :: (MonadIO m, MonadLsp Config m) => Options -> m Env
src/Options.hs view
@@ -1,27 +1,34 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-}+ module Options- ( Options(..)- , getOptionsFromArgv- , usageMessage- , Config(..)- , initConfig- ) where-import Data.Aeson.Types hiding ( Options- , defaultOptions- )-import GHC.Generics ( Generic )-import System.Console.GetOpt-import System.Environment ( getArgs )-import Text.Read ( readMaybe )+ ( Options (..),+ getOptionsFromArgv,+ versionNumber,+ versionString,+ usageMessage,+ Config (..),+ initConfig,+ )+where +import Data.Aeson.Types hiding+ ( Options,+ defaultOptions,+ )+import GHC.Generics (Generic)+import System.Console.GetOpt+import System.Environment (getArgs)+import Text.Read (readMaybe)+ getOptionsFromArgv :: IO Options getOptionsFromArgv = do- -- extract options for Agda from ARGV + -- extract options for Agda from ARGV (argvForALS, argvForAgda) <- extractAgdaOpts <$> getArgs- -- parse options for ALS - (opts , _ ) <- parseOpts argvForALS+ -- parse options for ALS+ (opts, _) <- parseOpts argvForALS -- save options for Agda back- return $ opts { optRawAgdaOptions = argvForAgda }+ return $ opts {optRawAgdaOptions = argvForAgda} usageMessage :: String usageMessage = usageInfo usage options ++ usageAboutAgdaOptions@@ -30,75 +37,116 @@ -- | Command-line arguments data Options = Options- { optViaTCP :: Maybe Int- , optRawAgdaOptions :: [String]- , optHelp :: Bool+ { optViaTCP :: Maybe Int,+ optRawAgdaOptions :: [String],+ optRawResponses :: Bool,+ optSetup :: Bool,+ optHelp :: Bool,+ optVersion :: Bool } defaultOptions :: Options defaultOptions =- Options { optViaTCP = Nothing, optRawAgdaOptions = [], optHelp = False }+ Options {optViaTCP = Nothing, optRawAgdaOptions = [], optRawResponses = False, optSetup = False, optHelp = False, optVersion = False} options :: [OptDescr (Options -> Options)] options =- [ Option ['h']- ["help"]- (NoArg (\opts -> opts { optHelp = True }))- "print this help message"- , Option- ['p']- ["port"]- (OptArg- (\port opts -> case port of- Just n -> opts { optViaTCP = readMaybe n }- Nothing -> opts { optViaTCP = Just 4096 }+ [ Option+ ['h']+ ["help"]+ (NoArg (\opts -> opts {optHelp = True}))+ "print this help message",+ Option+ ['p']+ ["port"]+ ( OptArg+ ( \port opts -> case port of+ Just n -> opts {optViaTCP = readMaybe n}+ Nothing -> opts {optViaTCP = Just 4096}+ )+ "PORT" )- "PORT"- )- "talk with the editor via TCP port (4096 as default)"+ "talk with the editor via TCP port (4096 as default)",+ Option+ []+ ["raw"]+ (NoArg (\opts -> opts {optRawResponses = True}))+ "return all responses in raw JSON format",+#if MIN_VERSION_Agda(2,8,0)+ Option+ []+ ["setup"]+ (NoArg (\opts -> opts {optSetup = True}))+ "run Agda setup and exit",+#endif+ Option+ ['V']+ ["version"]+ (NoArg (\opts -> opts {optVersion = True}))+ "print version information and exit" ] +versionNumber :: Int+versionNumber = 6++versionString :: String+versionString =+#if MIN_VERSION_Agda(2,8,0)+ "Agda v2.8.0 Language Server v" <> show versionNumber <> suffix+#elif MIN_VERSION_Agda(2,7,0)+ "Agda v2.7.0.1 Language Server v" <> show versionNumber <> suffix+#elif MIN_VERSION_Agda(2,6,4)+ "Agda v2.6.4.3 Language Server v" <> show versionNumber <> suffix+#else+ error "Unsupported Agda version"+#endif+ where+#ifdef wasm32_HOST_ARCH+ suffix = " (WebAssembly build)"+#else+ suffix = ""+#endif+ usage :: String-usage = "Agda Language Server v0.0.3.0 \nUsage: als [Options...]\n"+usage = versionString <> "\nUsage: als [Options...]\n" usageAboutAgdaOptions :: String-usageAboutAgdaOptions =- "\n\- \ +AGDA [Options for Agda ...] -AGDA\n\- \ To pass command line options to Agda, put them in between '+AGDA' and '-AGDA'\n\- \ For example:\n\- \ als -p=3000 +AGDA --cubical -AGDA\n\- \ If you are using agda-mode on VS Code, put them in the Settings at:\n\- \ agdaMode.connection.commandLineOptions\n\- \"+usageAboutAgdaOptions = "\n +AGDA [Options for Agda ...] -AGDA\n To pass command line options to Agda, put them in between '+AGDA' and '-AGDA'\n For example:\n als -p=3000 +AGDA --cubical -AGDA\n If you are using agda-mode on VS Code, put them in the Settings at:\n agdaMode.connection.commandLineOptions\n" parseOpts :: [String] -> IO (Options, [String]) parseOpts argv = case getOpt Permute options argv of- (o, n, [] ) -> return (foldl (flip id) defaultOptions o, n)+ (o, n, []) -> return (foldl (flip id) defaultOptions o, n) (_, _, errs) -> ioError $ userError $ concat errs ++ usageInfo usage options - -- | Removes RTS options from a list of options (stolen from Agda) stripRTS :: [String] -> [String]-stripRTS [] = []+stripRTS [] = [] stripRTS ("--RTS" : argv) = argv stripRTS (arg : argv) | is "+RTS" arg = stripRTS $ drop 1 $ dropWhile (not . is "-RTS") argv- | otherwise = arg : stripRTS argv- where is x arg = [x] == take 1 (words arg)+ | otherwise = arg : stripRTS argv+ where+ is x arg = [x] == take 1 (words arg) -- | Extract Agda options (+AGDA ... -AGDA) from a list of options+--+-- >>> extractAgdaOpts [ "als1", "+AGDA", "agda1", "-AGDA", "als2", "+AGDA", "agda2" ]+-- (["als1","als2"],["agda1","agda2"]) extractAgdaOpts :: [String] -> ([String], [String])-extractAgdaOpts argv =- let (before , argv') = break (== "+AGDA") argv- (forAgda, after) = break (== "-AGDA") argv'- forALS = before ++ dropWhile (== "-AGDA") after- forAgda' = dropWhile (== "+AGDA") forAgda- in (forALS, forAgda')+extractAgdaOpts argv = go False argv+ where+ go False ("+AGDA":xs) = go True xs+ go True ("-AGDA":xs) = go False xs+ go inagda (arg:xs) =+ let (forALS, forAgda) = go inagda xs in+ if inagda+ then (forALS, arg:forAgda)+ else (arg:forALS, forAgda)+ go _ [] = ([], []) -------------------------------------------------------------------------------- -newtype Config = Config { configRawAgdaOptions :: [String] }+newtype Config = Config {configRawAgdaOptions :: [String]} deriving (Eq, Show, Generic) instance FromJSON Config where
src/Render.hs view
@@ -10,7 +10,7 @@ import Render.Interaction () import Render.Internal () import Render.Name ()+import Render.Position () import Render.RichText import Render.TypeChecking ()-import Render.Position () import Render.Utils ()
src/Render/Class.hs view
@@ -1,5 +1,7 @@-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies #-}+ module Render.Class ( Render (..), -- RenderTCM (..),@@ -10,16 +12,18 @@ ) where -import Agda.Syntax.Fixity (Precedence (TopCtx))+import Agda.Syntax.Fixity (Precedence (TopCtx)) import qualified Agda.Syntax.Translation.AbstractToConcrete as A-import qualified Agda.TypeChecking.Monad.Base as A-import Agda.Utils.List1 (List1)-import Agda.Utils.List2 (List2)-import Agda.Utils.Pretty (Doc)-import qualified Agda.Utils.Pretty as Doc+import qualified Agda.TypeChecking.Monad.Base as A+import Agda.Utils.List1 (List1)+import Agda.Utils.List2 (List2)+import Agda.Syntax.Common.Pretty (Doc)+import qualified Agda.Syntax.Common.Pretty as Doc -import Data.Int (Int32)-import GHC.Exts ( IsList(toList) )+import Data.Int (Int32)+import Data.Text (Text)+import Data.Word (Word32)+import GHC.Exts (IsList (toList)) import Render.RichText --------------------------------------------------------------------------------@@ -46,7 +50,7 @@ -- | like 'prettyA' renderA :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines-renderA x = render <$> A.abstractToConcrete_ x +renderA x = render <$> A.abstractToConcrete_ x -- | like 'prettyATop' renderATop :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines@@ -61,19 +65,30 @@ instance Render Int32 where render = text . show +instance Render Word32 where+ render = text . show+ instance Render Integer where render = text . show instance Render Bool where render = text . show +instance Render Text where+ render = text . show+ instance Render Doc where render = text . Doc.render -instance Render a => Render [a] where+instance (Render a) => Render (Maybe a) where+ renderPrec p Nothing = mempty+ renderPrec p (Just x) = renderPrec p x++instance (Render a) => Render [a] where render xs = "[" <> fsep (punctuate "," (fmap render xs)) <> "]"-instance Render a => Render (List1 a) where++instance (Render a) => Render (List1 a) where render = render . toList -instance Render a => Render (List2 a) where+instance (Render a) => Render (List2 a) where render = render . toList
src/Render/Common.hs view
@@ -3,26 +3,45 @@ module Render.Common where import Agda.Syntax.Common- ( Named(namedThing),- Hiding(NotHidden, Hidden, Instance),- LensHiding(getHiding),- RewriteEqn'(..),- MetaId(MetaId),- LensQuantity(getQuantity),- Quantity(..),- LensRelevance(getRelevance),- Relevance(..),- Induction(..),- Cohesion(..),- QωOrigin(..),- LensCohesion(getCohesion),- NameId(..) )-import qualified Agda.Utils.Null as Agda-import Agda.Utils.List1 (toList)-import Agda.Utils.Functor ((<&>))+ ( Cohesion (..),+ Erased (..),+ Hiding (Hidden, Instance, NotHidden),+ Induction (..),+ LensCohesion (getCohesion),+ LensHiding (getHiding),+ LensQuantity (getQuantity),+ LensRelevance (getRelevance),+ Lock (..), + LockOrigin (..),++ MetaId (MetaId),+ NameId (..),+ Named (namedThing),+#if MIN_VERSION_Agda(2,7,0)+ OverlapMode (..),+#endif++ Quantity (..),+ QωOrigin (..),+ Relevance (..),+ RewriteEqn' (..),+ asQuantity,+#if MIN_VERSION_Agda(2,8,0)+ OriginRelevant (..), + OriginIrrelevant (..), + OriginShapeIrrelevant (..), + PolarityModality (..),+ ModalPolarity (..),+#endif+ )+import Agda.Utils.Functor ((<&>))+import Agda.Utils.List1 (toList)+import qualified Agda.Utils.List1 as List1+import qualified Agda.Utils.Null as Agda import Render.Class import Render.RichText+import Data.Text (Text) -------------------------------------------------------------------------------- @@ -32,17 +51,42 @@ -- | MetaId instance Render MetaId where-#if MIN_VERSION_Agda(2,6,3) render (MetaId n m) = text $ "_" ++ show n ++ "@" ++ show m-#else- render (MetaId n) = text $ "_" ++ show n++#if MIN_VERSION_Agda(2,8,0)+-- | OriginRelevant+instance Render OriginRelevant where+ render = \case+ ORelInferred {} -> mempty+ ORelRelevant {} -> "@relevant"++instance Render OriginIrrelevant where+ render = \case+ OIrrInferred {} -> mempty+ OIrrDot {} -> "."+ OIrrIrr {} -> "@irr"+ OIrrIrrelevant {} -> "@irrelevant"++instance Render OriginShapeIrrelevant where+ render = \case+ OShIrrInferred {} -> mempty+ OShIrrDotDot {} -> ".."+ OShIrrShIrr {} -> "@shirr"+ OShIrrShapeIrrelevant {} -> "@shape-irrelevant" #endif -- | Relevance+#if MIN_VERSION_Agda(2,8,0) instance Render Relevance where+ render (Relevant o) = render o+ render (Irrelevant o) = Agda.ifNull (render o) "." id+ render (ShapeIrrelevant o) = Agda.ifNull (render o) ".." id+#else+instance Render Relevance where render Relevant = mempty render Irrelevant = "." render NonStrict = ".."+#endif -- | Quantity instance Render Quantity where@@ -62,46 +106,87 @@ instance Render QωOrigin where render = \case QωInferred -> mempty- Qω{} -> "@ω"- QωPlenty{} -> "@plenty"+ Qω {} -> "@ω"+ QωPlenty {} -> "@plenty" instance Render Cohesion where- render Flat = "@♭"+ render Flat = "@♭" render Continuous = mempty- render Squash = "@⊤"+ render Squash = "@⊤" +-- | Polarity++#if MIN_VERSION_Agda(2,8,0)+instance Render ModalPolarity where+ render p = case p of+ UnusedPolarity -> "@unused"+ StrictlyPositive -> "@++"+ Positive -> "@+"+ Negative -> "@-"+ MixedPolarity -> mempty++instance Render PolarityModality where+ render (PolarityModality p _ _) = render p+#endif+ -------------------------------------------------------------------------------- +#if MIN_VERSION_Agda(2,7,0)+instance Render OverlapMode where+ render = \case+ Overlappable -> "OVERLAPPABLE"+ Overlapping -> "OVERLAPPING"+ Incoherent -> "INCOHERENT"+ Overlaps -> "OVERLAPS"+ FieldOverlap -> "overlap"+ DefaultOverlap -> mempty+#endif++--------------------------------------------------------------------------------+ -- | From 'prettyHiding' -- @renderHiding info visible text@ puts the correct braces -- around @text@ according to info @info@ and returns -- @visible text@ if the we deal with a visible thing.-renderHiding :: LensHiding a => a -> (Inlines -> Inlines) -> Inlines -> Inlines+renderHiding :: (LensHiding a) => a -> (Inlines -> Inlines) -> Inlines -> Inlines renderHiding a parensF = case getHiding a of Hidden -> braces' Instance {} -> dbraces NotHidden -> parensF -renderRelevance :: LensRelevance a => a -> Inlines -> Inlines+renderRelevance :: (LensRelevance a) => a -> Inlines -> Inlines renderRelevance a d = if show d == "_" then d else render (getRelevance a) <> d -renderQuantity :: LensQuantity a => a -> Inlines -> Inlines+renderQuantity :: (LensQuantity a) => a -> Inlines -> Inlines renderQuantity a d = if show d == "_" then d else render (getQuantity a) <+> d -renderCohesion :: LensCohesion a => a -> Inlines -> Inlines+instance Render Lock where+ render = \case+ IsLock LockOLock -> "@lock"+ IsLock LockOTick -> "@tick"+ IsNotLock -> mempty++#if MIN_VERSION_Agda(2,7,0)+renderErased :: Erased -> Inlines -> Inlines+renderErased = renderQuantity . asQuantity+#endif++renderCohesion :: (LensCohesion a) => a -> Inlines -> Inlines renderCohesion a d = if show d == "_" then d else render (getCohesion a) <+> d -------------------------------------------------------------------------------- - instance (Render p, Render e) => Render (RewriteEqn' qn nm p e) where render = \case- Rewrite es -> prefixedThings (text "rewrite") (render . snd <$> toList es)- Invert _ pes -> prefixedThings (text "invert") (toList pes <&> (\ (p, e) -> render p <+> "<-" <+> render e) . namedThing)+ Rewrite es -> prefixedThings (text "rewrite") (render . snd <$> toList es)+ Invert _ pes -> prefixedThings (text "invert") (toList pes <&> (\(p, e) -> render p <+> "<-" <+> render e) . namedThing)+#if MIN_VERSION_Agda(2,7,0)+ LeftLet pes -> prefixedThings (text "using") [render p <+> "<-" <+> render e | (p, e) <- List1.toList pes]+#endif prefixedThings :: Inlines -> [Inlines] -> Inlines prefixedThings kw = \case@@ -109,5 +194,5 @@ (doc : docs) -> fsep $ (kw <+> doc) : fmap ("|" <+>) docs instance Render Induction where- render Inductive = "inductive"+ render Inductive = "inductive" render CoInductive = "coinductive"
src/Render/Concrete.hs view
@@ -5,43 +5,50 @@ module Render.Concrete where -import qualified Data.Text as T-import Data.Maybe (isNothing, maybeToList)-import qualified Data.Strict.Maybe as Strict- import Agda.Syntax.Common-import Agda.Syntax.Concrete-import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)---import Agda.Syntax.Position (noRange)-import Agda.Utils.List1 as List1 (toList, fromList)-import qualified Agda.Utils.List1 as List1-import qualified Agda.Utils.List2 as List2+import Agda.Syntax.Concrete+import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled) import Agda.Utils.Float (toStringWithoutDotZero)-import Agda.Utils.Function (applyWhen)-import Agda.Utils.Functor (dget, (<&>))+import Agda.Utils.Function+import Agda.Utils.Functor (dget, (<&>), for) import Agda.Utils.Impossible (__IMPOSSIBLE__)-+import Agda.Utils.List1 as List1 (fromList, toList, List1)+import qualified Agda.Utils.List1 as List1+import qualified Agda.Utils.List2 as List2+import Agda.Utils.Null+import Data.Maybe (isNothing, maybeToList)+import qualified Data.Strict.Maybe as Strict+import qualified Data.Text as T import Render.Class import Render.Common import Render.Literal () import Render.Name () import Render.RichText import Render.TypeChecking ()+import Prelude hiding (null)+import qualified Agda.Syntax.Common.Aspect as Asp -------------------------------------------------------------------------------- -instance Render a => Render (Ranged a) where+#if MIN_VERSION_Agda(2,7,0)+instance (Render a) => Render (TacticAttribute' a) where+ render (TacticAttribute t) =+ ifNull (render t) empty $ \d -> "@" <> parens ("tactic" <+> d)+#endif++instance (Render a) => Render (Ranged a) where render = render . rangedThing -instance Render a => Render (WithHiding a) where+instance (Render a) => Render (WithHiding a) where render w = renderHiding w id $ render $ dget w instance Render Modality where- render mod = hsep- [ render (getRelevance mod)- , render (getQuantity mod)- , render (getCohesion mod)- ]+ render mod =+ hsep+ [ render (getRelevance mod),+ render (getQuantity mod),+ render (getCohesion mod)+ ] -- | OpApp instance Render (OpApp Expr) where@@ -49,7 +56,7 @@ render (SyntaxBindingLambda r bs e) = render (Lam r bs e) -- | MaybePlaceholder-instance Render a => Render (MaybePlaceholder a) where+instance (Render a) => Render (MaybePlaceholder a) where render Placeholder {} = "_" render (NoPlaceholder _ e) = render e @@ -75,8 +82,15 @@ case appView expr of AppView e1 args -> fsep $ render e1 : fmap render args RawApp _ es -> fsep $ fmap render (List2.toList es)+#if MIN_VERSION_Agda(2,8,0)+ OpApp _ q _ es -> fsep $ renderOpApp280 (Asp.Name Nothing True) q es+ WithApp _ e es -> fsep $ render e : fmap (("|" <+>) . render) (toList es)+ KnownOpApp nk _ q _ es -> fsep $ renderOpApp280 (Asp.Name (Just nk) True) q es+#else OpApp _ q _ es -> fsep $ renderOpApp q es WithApp _ e es -> fsep $ render e : fmap ((text' ["delimiter"] "|" <+>) . render) es+ KnownOpApp _ _ q _ es -> fsep $ renderOpApp q es+#endif HiddenArg _ e -> braces' $ render e InstanceArg _ e -> dbraces $ render e Lam _ bs (AbsurdLam _ h) -> lambda <+> fsep (fmap render (toList bs)) <+> absurd h@@ -109,12 +123,14 @@ Dot _ e -> "." <> render e DoubleDot _ e -> ".." <> render e Absurd _ -> "()"+#if MIN_VERSION_Agda(2,8,0)+ Rec _ _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)]+ RecUpdate _ _ e xs ->+ sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]+#else Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)] RecUpdate _ e xs -> sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]-#if !MIN_VERSION_Agda(2,6,3)- ETel [] -> "()"- ETel tel -> fsep $ fmap render tel #endif Quote _ -> "quote" QuoteTerm _ -> "quoteTerm"@@ -125,20 +141,18 @@ Equal _ a b -> render a <+> "=" <+> render b Ellipsis _ -> "..." Generalized e -> render e+ KnownIdent _ q -> render q where absurd NotHidden = "()" absurd Instance {} = "{{}}" absurd Hidden = "{}" --- instance RenderTCM Expr where--- renderTCM = render- -------------------------------------------------------------------------------- instance (Render a, Render b) => Render (Either a b) where render = either render render -instance Render a => Render (FieldAssignment' a) where+instance (Render a) => Render (FieldAssignment' a) where render (FieldAssignment x e) = sep [render x <+> "=", render e] instance Render ModuleAssignment where@@ -157,44 +171,105 @@ instance Render BoundName where render BName {boundName = x} = render x -instance Render a => Render (Binder' a) where+instance (Render a) => Render (Binder' a) where+#if MIN_VERSION_Agda(2,8,0)+ render (Binder mpat UserBinderName n) =+ applyWhenJust mpat (\ pat -> (<+> ("@" <+> parens (render pat)))) $ render n+ render (Binder pat InsertedBinderName n) = case pat of+ Just pat -> parens (render pat)+ Nothing -> render n+#else render (Binder mpat n) = let d = render n in case mpat of Nothing -> d Just pat -> d <+> "@" <+> parens (render pat)+#endif -------------------------------------------------------------------------------- -- | NamedBinding instance Render NamedBinding where+#if MIN_VERSION_Agda(2,8,0)+ render (NamedBinding withH+ x@(Arg (ArgInfo h (Modality r q c p) _o _fv (Annotation lock))+ (Named _mn xb@(Binder _mp _ (BName _y _fix t _fin))))) =+ applyWhen withH prH $+ applyWhenJust (isLabeled x) (\ l -> (text l <+>) . ("=" <+>)) (render xb)+ where+ prH = renderRelevance r+ . renderHiding h mparens+ . (coh <+>)+ . (qnt <+>)+ . (pol <+>)+ . (lck <+>)+ . (tac <+>)+ coh = render c+ qnt = render q+ pol = render p+ tac = render t+ lck = render lock+ -- Parentheses are needed when an attribute @... is printed+ mparens = applyUnless (null coh && null qnt && null lck && null tac && null pol) parens+#elif MIN_VERSION_Agda(2,7,0)+ render+ ( NamedBinding+ withH+ x@( Arg+ (ArgInfo h (Modality r q c) _o _fv (Annotation lock))+ (Named _mn xb@(Binder _mp (BName _y _fix t _fin)))+ )+ ) =+ applyWhen withH prH $+ applyWhenJust (isLabeled x) (\l -> (text l <+>) . ("=" <+>)) (render xb)+ where+ prH =+ (render r <>)+ . renderHiding h mparens+ . (coh <+>)+ . (qnt <+>)+ . (lck <+>)+ . (tac <+>)+ coh = render c+ qnt = render q+ tac = render t+ lck = render lock+ -- Parentheses are needed when an attribute @... is printed+ mparens = applyUnless (null coh && null qnt && null lck && null tac) parens++#else render (NamedBinding withH x) = prH $ if- | Just l <- isLabeled x -> text l <> " = " <> render xb- | otherwise -> render xb+ | Just l <- isLabeled x -> text l <> " = " <> render xb+ | otherwise -> render xb where xb = namedArg x bn = binderName xb prH | withH =- renderRelevance x- . renderHiding x mparens'- . renderCohesion x- . renderQuantity x- . renderTactic bn+ renderRelevance x+ . renderHiding x mparens'+ . renderCohesion x+ . renderQuantity x+ . renderTactic bn | otherwise = id -- Parentheses are needed when an attribute @... is present mparens' | noUserQuantity x, Nothing <- bnameTactic bn = id | otherwise = parens+#endif renderTactic :: BoundName -> Inlines -> Inlines renderTactic = renderTactic' . bnameTactic renderTactic' :: TacticAttribute -> Inlines -> Inlines+#if MIN_VERSION_Agda(2,7,0)+renderTactic' t = (render t <+>)+#else renderTactic' Nothing d = d renderTactic' (Just t) d = "@" <> (parens ("tactic " <> render t) <+> d)+#endif -------------------------------------------------------------------------------- @@ -254,19 +329,35 @@ instance Render WhereClause where render NoWhere = mempty- render (AnyWhere _range [Module _ x [] ds])+ render (AnyWhere _range [Module _ _ x [] ds]) | isNoName (unqualify x) =- vcat ["where", vcat $ fmap render ds]+ vcat ["where", vcat $ fmap render ds] render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds]- render (SomeWhere _range m a ds) =+#if MIN_VERSION_Agda(2,7,0)+ render (SomeWhere _ erased m a ds) = vcat [ hsep $+ privateWhenUserWritten+ a+ ["module", renderErased erased (render m), "where"],+ vcat $ map render ds+ ]+ where+ privateWhenUserWritten = \case+ PrivateAccess _ UserWritten -> ("private" :)+ _ -> id++#else+ render (SomeWhere _range _er m a ds) =+ vcat+ [ hsep $ applyWhen (a == PrivateAccess UserWritten) ("private" :) ["module", render m, "where"], vcat $ fmap render ds ]+#endif instance Render LHS where render (LHS p eqs es) =@@ -278,29 +369,37 @@ where renderWithd :: WithExpr -> Inlines renderWithd (Named nm wh) =- let e = render wh in- case nm of- Nothing -> e- Just n -> render n <+> ":" <+> e+ let e = render wh+ in case nm of+ Nothing -> e+ Just n -> render n <+> ":" <+> e instance Render LHSCore where render (LHSHead f ps) = sep $ render f : fmap (parens . render) ps render (LHSProj d ps lhscore ps') = sep $- render d :- fmap (parens . render) ps- ++ parens (render lhscore) :- fmap (parens . render) ps'+ render d+ : fmap (parens . render) ps+ ++ parens (render lhscore)+ : fmap (parens . render) ps' render (LHSWith h wps ps) = if null ps then doc else sep $ parens doc : fmap (parens . render) ps where- doc = sep $ render h : fmap (("|" <+>) . render) wps+ doc = sep $ render h : fmap (("|" <+>) . render) (toList wps) render (LHSEllipsis r p) = "..." instance Render ModuleApplication where+#if MIN_VERSION_Agda(2,8,0)+ render (SectionApp _ bs x es) = fsep $ concat+ [ map render bs+ , [ "=", render x ]+ , map render es+ ]+#else render (SectionApp _ bs e) = fsep (fmap render bs) <+> "=" <+> render e+#endif render (RecordModuleInstance _ rec) = "=" <+> render rec <+> "{{...}}" instance Render DoStmt where@@ -310,7 +409,7 @@ prCs [] = mempty prCs cs' = fsep ["where", vcat (fmap render cs')] render (DoThen e) = render e- render (DoLet _ ds) = "let" <+> vcat (fmap render $ toList ds)+ render (DoLet _ ds) = "let" <+> vcat (render <$> toList ds) instance Render Declaration where render d =@@ -320,21 +419,33 @@ [ renderTactic' tac $ renderRelevance i $ renderCohesion i $ renderQuantity i $ render x <+> ":", render e ]+#if MIN_VERSION_Agda(2,8,0) FieldSig inst tac x (Arg i e) ->+ mkInst inst $ mkOverlap i $+ -- We print relevance before hiding, need to clear it before printing the rest of the attributes with TypeSig.+ renderRelevance i $ renderHiding i id $+ render $ TypeSig (setRelevance relevant i) tac x e+#else+ FieldSig inst tac x (Arg i e) -> mkInst inst $ mkOverlap i $ renderRelevance i $ renderHiding i id $ renderCohesion i $ renderQuantity i $- render $ TypeSig (setRelevance Relevant i) tac x e+ render $+ TypeSig (setRelevance Relevant i) tac x e+#endif where mkInst (InstanceDef _) f = sep ["instance", f] mkInst NotInstanceDef f = f-- mkOverlap j f- | isOverlappable j = "overlap" <+> f- | otherwise = f+#if MIN_VERSION_Agda(2,7,0)+ mkOverlap i d+ | isYesOverlap i = "overlap" <+> d+#else+ mkOverlap i d | isOverlappable i = "overlap" <+> d+#endif+ | otherwise = d Field _ fs -> sep [ "field",@@ -346,7 +457,7 @@ render rhs, render wh ]- DataSig _ x tel e ->+ DataSig _ _er x tel e -> fsep [ hsep [ "data",@@ -358,7 +469,7 @@ render e ] ]- Data _ x tel e cs ->+ Data _ _er x tel e cs -> fsep [ hsep [ "data",@@ -382,7 +493,7 @@ "where", vcat $ fmap render cs ]- RecordSig _ x tel e ->+ RecordSig _ _er x tel e -> sep [ hsep [ "record",@@ -394,19 +505,29 @@ render e ] ]- Record _ x dir tel e cs ->- pRecord x dir tel (Just e) cs- RecordDef _ x dir tel cs ->- pRecord x dir tel Nothing cs+#if MIN_VERSION_Agda(2,7,0)+ Record _ erased x dir tel e cs -> pRecord erased x dir tel (Just e) cs+#else+ Record _ _er x dir tel e cs -> pRecord x dir tel (Just e) cs+#endif+#if MIN_VERSION_Agda(2,7,0)+ RecordDef _ x dir tel cs -> pRecord defaultErased x dir tel Nothing cs+#else+ RecordDef _ x dir tel cs -> pRecord x dir tel Nothing cs+#endif+#if !MIN_VERSION_Agda(2,7,0) RecordDirective r -> pRecordDirective r+#endif Infix f xs -> render f <+> fsep (punctuate "," $ fmap render (toList xs)) Syntax n _ -> "syntax" <+> render n <+> "..." PatternSyn _ n as p ->- "pattern" <+> render n <+> fsep (fmap render as)+ "pattern"+ <+> render n+ <+> fsep (fmap render as) <+> "=" <+> render p Mutual _ ds -> namedBlock "mutual" ds- InterleavedMutual _ ds -> namedBlock "interleaved mutual" ds+ InterleavedMutual _ ds -> namedBlock "interleaved mutual" ds LoneConstructor _ ds -> namedBlock "constructor" ds Abstract _ ds -> namedBlock "abstract" ds Private _ _ ds -> namedBlock "private" ds@@ -415,7 +536,7 @@ Postulate _ ds -> namedBlock "postulate" ds Primitive _ ds -> namedBlock "primitive" ds Generalize _ ds -> namedBlock "variable" ds- Module _ x tel ds ->+ Module _ _er x tel ds -> fsep [ hsep [ "module",@@ -425,23 +546,43 @@ ], vcat $ fmap render ds ]- ModuleMacro _ x (SectionApp _ [] e) DoOpen i+#if MIN_VERSION_Agda(2,8,0)+ ModuleMacro _ NotErased{} x (SectionApp _ [] y es) DoOpen i | isNoName x ->+ sep [ render DoOpen+ , fsep $ render y : map render es+ , render i+ ]+ ModuleMacro _ erased x (SectionApp _ tel y es) open i ->+ sep [ render open <+> "module" <+>+ renderErased erased (render x) <+> fsep (map render tel)+ , fsep $ concat [ [ "=", render y ], map render es, [ render i ] ]+ ]+ ModuleMacro _ erased x (RecordModuleInstance _ rec) open _i ->+ sep [ render open <+> "module" <+> renderErased erased (render x)+ , "=" <+> render rec <+> "{{...}}"+ ]+#else+ ModuleMacro _ _er x m open i -> case m of+ (SectionApp _ [] e)+ | open == DoOpen,+ isNoName x ->+ fsep+ [ render open,+ render e,+ render i+ ]+ (SectionApp _ tel e) -> fsep- [ render DoOpen,- render e,- render i+ [ render open <+> "module" <+> render x <+> fcat (fmap render tel),+ "=" <+> render e <+> render i ]- ModuleMacro _ x (SectionApp _ tel e) open i ->- fsep- [ render open <+> "module" <+> render x <+> fcat (fmap render tel),- "=" <+> render e <+> render i- ]- ModuleMacro _ x (RecordModuleInstance _ rec) open _ ->- fsep- [ render open <+> "module" <+> render x,- "=" <+> render rec <+> "{{...}}"- ]+ (RecordModuleInstance _ rec) ->+ fsep+ [ render open <+> "module" <+> render x,+ "=" <+> render rec <+> "{{...}}"+ ]+#endif Open _ x i -> hsep ["open", render x, render i] Import _ x rn open i -> hsep [render open, "import", render x, as rn, render i]@@ -453,11 +594,14 @@ UnquoteDef _ xs t -> fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t] Pragma pr -> sep ["{-#" <+> render pr, "#-}"]-#if MIN_VERSION_Agda(2,6,3) UnquoteData _ x xs e ->- fsep [ hsep [ "unquoteData", render x, fsep (fmap render xs), "=" ], render e ]-#endif+ fsep [hsep ["unquoteData", render x, fsep (fmap render xs), "="], render e]+ Opaque _ ds ->+ namedBlock "opaque" ds+ Unfolding _ xs ->+ fsep ("unfolding" : fmap render xs) where+ namedBlock s ds = fsep [ text s,@@ -466,22 +610,61 @@ pHasEta0 :: HasEta0 -> Inlines pHasEta0 = \case- YesEta -> "eta-equality"+ YesEta -> "eta-equality" NoEta () -> "no-eta-equality" +instance Render RecordDirective where+ render = pRecordDirective+ pRecordDirective :: RecordDirective -> Inlines pRecordDirective = \case Induction ind -> render ind- Constructor n inst -> hsep [ pInst, "constructor", render n ] where- pInst = case inst of- InstanceDef{} -> "instance"- NotInstanceDef{} -> mempty+ Constructor n inst -> hsep [pInst, "constructor", render n]+ where+ pInst = case inst of+ InstanceDef {} -> "instance"+ NotInstanceDef {} -> mempty Eta eta -> pHasEta0 (rangedThing eta)- PatternOrCopattern{} -> "pattern"+ PatternOrCopattern {} -> "pattern" +#if MIN_VERSION_Agda(2,7,0)+pRecord ::+ Erased ->+ Name ->+ [RecordDirective] ->+ [LamBinding] ->+ Maybe Expr ->+ [Declaration] ->+ Inlines+pRecord erased x directives tel me ds =+ vcat+ [ sep+ [ hsep+ [ "record",+ renderErased erased (render x),+ fsep (map render tel)+ ],+ pType me+ ],+ vcat $+ concat+ [ map render directives,+ map render ds+ ]+ ]+ where+ pType (Just e) =+ hsep+ [ ":",+ render e,+ "where"+ ]+ pType Nothing =+ "where" +#else pRecord :: Name -> RecordDirectives ->@@ -519,6 +702,7 @@ YesEta -> "eta-equality" NoEta _ -> "no-eta-equality" pCon = maybeToList $ (("constructor" <+>) . render) . fst <$> con+#endif instance Render OpenShortHand where render DoOpen = "open"@@ -529,10 +713,17 @@ render (BuiltinPragma _ b x) = hsep ["BUILTIN", text (rangedThing b), render x] render (RewritePragma _ _ xs) = hsep ["REWRITE", hsep $ fmap render xs]+#if MIN_VERSION_Agda(2,8,0) render (CompilePragma _ b x e) =+ hsep [ "COMPILE", render (rangedThing b), render x, textNonEmpty e ]+ render (ForeignPragma _ b s) =+ vcat $ hsep [ "FOREIGN", render (rangedThing b) ] : map text (lines s)+#else+ render (CompilePragma _ b x e) = hsep ["COMPILE", text (rangedThing b), render x, text e] render (ForeignPragma _ b s) = vcat $ text ("FOREIGN " ++ rangedThing b) : fmap text (lines s)+#endif render (StaticPragma _ i) = hsep ["STATIC", render i] render (InjectivePragma _ i) =@@ -561,9 +752,12 @@ render (PolarityPragma _ q occs) = hsep ("POLARITY" : render q : fmap render occs) render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"-#if MIN_VERSION_Agda(2,6,3) render (NotProjectionLikePragma _ q) =- hsep [ "NOT_PROJECTION_LIKE", render q ]+ hsep ["NOT_PROJECTION_LIKE", render q]+#if MIN_VERSION_Agda(2,7,0)+ render (InjectiveForInferencePragma _ i) =+ hsep ["INJECTIVE_FOR_INFERENCE", render i]+ render (OverlapPragma _ x m) = hsep [render m, render x] #endif instance Render Fixity where@@ -575,20 +769,12 @@ RightAssoc -> "infixr" NonAssoc -> "infix" -#if MIN_VERSION_Agda(2,6,3) instance Render NotationPart where render = \case- IdPart x -> text $ rangedThing x- HolePart{} -> "_"+ IdPart x -> text $ rangedThing x+ HolePart {} -> "_" VarPart {} -> "_"- WildPart{} -> "_"-#else-instance Render GenPart where- render (IdPart x) = text $ rangedThing x- render BindHole {} = "_"- render NormalHole {} = "_"- render WildHole {} = "_"-#endif+ WildPart {} -> "_" instance Render Fixity' where render (Fixity' fix nota _)@@ -596,7 +782,7 @@ | otherwise = "syntax" <+> render nota -- | Arg-instance Render a => Render (Arg a) where+instance (Render a) => Render (Arg a) where renderPrec p (Arg ai e) = renderHiding ai localParens $ renderPrec p' e where p'@@ -607,28 +793,37 @@ | otherwise = id -- | Named NamedName (Named_)-instance Render e => Render (Named NamedName e) where+instance (Render e) => Render (Named NamedName e) where renderPrec p (Named nm e) | Just s <- bareNameOf nm = mparens (p > 0) $ sep [text s <> " =", render e] | otherwise = renderPrec p e instance Render Pattern where render = \case- IdentP x -> render x+ IdentP _ x -> render x AppP p1 p2 -> fsep [render p1, render p2] RawAppP _ ps -> fsep $ fmap render (List2.toList ps)- OpAppP _ q _ ps -> fsep $ renderOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps)+ OpAppP _ q _ ps -> fsep $ renderOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) (toList ps)) HiddenP _ p -> braces' $ render p InstanceP _ p -> dbraces $ render p ParenP _ p -> parens $ render p WildP _ -> "_" AsP _ x p -> render x <> "@" <> render p+#if MIN_VERSION_Agda(2,8,0)+ DotP _ _ p -> "." <> render p+#else DotP _ p -> "." <> render p+#endif AbsurdP _ -> "()" LitP _ l -> render l QuoteP _ -> "quote"+#if MIN_VERSION_Agda(2,8,0)+ RecP _ _ fs -> sep [ "record", bracesAndSemicolons (map render fs) ]+ EqualP _ es -> sep $ for (toList es) (\ (e1, e2) -> parens $ sep [render e1, "=", render e2])+#else RecP _ fs -> sep ["record", bracesAndSemicolons (fmap render fs)] EqualP _ es -> sep $ [parens (sep [render e1, "=", render e2]) | (e1, e2) <- es]+#endif EllipsisP _ mp -> "..." WithP _ p -> "|" <+> render p @@ -636,9 +831,10 @@ bracesAndSemicolons [] = "{}" bracesAndSemicolons (d : ds) = sep (["{" <+> d] ++ fmap (";" <+>) ds ++ ["}"]) +-- `prettyOpApp` for Agda 2.7.0.1 and below renderOpApp :: forall a.- Render a =>+ (Render a) => QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]@@ -651,7 +847,7 @@ Name _ _ xs -> List1.toList xs NoName {} -> __IMPOSSIBLE__ - prOp :: Render a => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]+ prOp :: (Render a) => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)] prOp ms (Hole : xs) (e : es) = case namedArg e of Placeholder p -> (qual ms $ render e, Just p) : prOp [] xs es@@ -661,14 +857,69 @@ prOp ms (Id x : xs) es = ( qual ms $ render $ simpleName x, Nothing- ) :- prOp [] xs es+ )+ : prOp [] xs es -- Qualify the name part with the module. -- We then clear @ms@ such that the following name parts will not be qualified. prOp _ [] es = fmap (\e -> (render e, Nothing)) es qual ms' doc = hcat $ punctuate "." $ fmap render ms' ++ [doc]++ -- Section underscores should be printed without surrounding+ -- whitespace. This function takes care of that.+ merge :: [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]+ merge before [] = reverse before+ merge before ((d, Nothing) : after) = merge (d : before) after+ merge before ((d, Just Beginning) : after) = mergeRight before d after+ merge before ((d, Just End) : after) = case mergeLeft d before of+ (d', bs) -> merge (d' : bs) after+ merge before ((d, Just Middle) : after) = case mergeLeft d before of+ (d', bs) -> mergeRight bs d' after++ mergeRight before d after =+ reverse before+ ++ case merge [] after of+ [] -> [d]+ a : as -> (d <> a) : as++ mergeLeft d before = case before of+ [] -> (d, [])+ b : bs -> (b <> d, bs)++-- `prettyOpApp` for Agda 2.8.0 and above+renderOpApp280 :: + forall a.+ (Render a) =>+ Asp.Aspect ->+ QName ->+ List1 (NamedArg (MaybePlaceholder a)) ->+ [Inlines]+renderOpApp280 asp q es = merge [] $ prOp ms xs $ List1.toList es+ where+ -- ms: the module part of the name.+ ms = List1.init (qnameParts q)+ -- xs: the concrete name (alternation of @Id@ and @Hole@)+ xs = case unqualify q of+ Name _ _ xs -> List1.toList xs+ NoName{} -> __IMPOSSIBLE__++ prOp :: (Render a) => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]+ prOp ms (Hole : xs) (e : es) =+ case namedArg e of+ Placeholder p -> (qual ms $ render e, Just p) : prOp [] xs es+ NoPlaceholder {} -> (render e, Nothing) : prOp ms xs es+ -- Module qualifier needs to go on section holes (#3072)+ prOp _ (Hole : _) [] = __IMPOSSIBLE__+ prOp ms (Id x : xs) es = ( qual ms $ render $ simpleName x+ , Nothing+ ) : prOp [] xs es+ -- Qualify the name part with the module.+ -- We then clear @ms@ such that the following name parts will not be qualified.++ prOp _ [] es = map (\e -> (render e, Nothing)) es++ qual ms doc = hcat $ punctuate "." $ map render ms ++ [doc] -- Section underscores should be printed without surrounding -- whitespace. This function takes care of that.
src/Render/Interaction.hs view
@@ -1,49 +1,60 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-} module Render.Interaction where -import qualified Data.Set as Set--import Agda.Interaction.Base-import Agda.Syntax.Internal ( Blocker(..) )-import Agda.TypeChecking.Monad-import Render.Class-import Render.Concrete ( )-import Render.Internal ( )-import Render.Name ( )-import Render.Position ( )-import Render.RichText-import Render.TypeChecking ( )+import Agda.Interaction.Base+#if MIN_VERSION_Agda(2,7,0)+import Agda.Interaction.Output (OutputConstraint, OutputForm)+#endif+import Agda.Syntax.Internal (Blocker (..))+import Agda.TypeChecking.Monad+import qualified Data.IntMap as IntMap+import qualified Data.Map as Map+import qualified Data.Set as Set+import Render.Class+import Render.Concrete ()+import Render.Internal ()+import Render.Name ()+import Render.Position ()+import Render.RichText+import Render.TypeChecking () -------------------------------------------------------------------------------- -- | OutputForm- instance (Render a, Render b) => Render (OutputForm a b) where- render (OutputForm r pids unblock c) = fsep- [render c, prange r, parens (sep [blockedOn unblock, prPids pids])]- where- prPids [] = mempty- prPids [pid] = parens $ "belongs to problem" <+> render pid- prPids pids' = parens $ "belongs to problems" <+> fsep- (punctuate "," $ fmap render pids')+ render (OutputForm r pids unblock c) =+ fsep+ [render c, prange r, parens (sep [blockedOn unblock, prPids pids])]+ where+ prPids [] = mempty+ prPids [pid] = parens $ "belongs to problem" <+> render pid+ prPids pids' =+ parens $+ "belongs to problems"+ <+> fsep+ (punctuate "," $ fmap render pids') - comma | null pids = mempty- | otherwise = ","+ comma+ | null pids = mempty+ | otherwise = "," - blockedOn (UnblockOnAll bs) | Set.null bs = mempty- blockedOn (UnblockOnAny bs) | Set.null bs = "stuck" <> comma- blockedOn u = "blocked on" <+> (render u <> comma)+ blockedOn (UnblockOnAll bs) | Set.null bs = mempty+ blockedOn (UnblockOnAny bs) | Set.null bs = "stuck" <> comma+ blockedOn u = "blocked on" <+> (render u <> comma) - prange rr | null s = mempty- | otherwise = text $ " [ at " ++ s ++ " ]"- where s = show $ render rr+ prange rr+ | null s = mempty+ | otherwise = text $ " [ at " ++ s ++ " ]"+ where+ s = show $ render rr -- | OutputConstraint instance (Render a, Render b) => Render (OutputConstraint a b) where render (OfType name expr) = render name <> " : " <> render expr- render (JustType name ) = "Type " <> render name- render (JustSort name ) = "Sort " <> render name+ render (JustType name) = "Type " <> render name+ render (JustSort name) = "Sort " <> render name render (CmpInType cmp expr name1 name2) = render name1 <> " "@@ -73,7 +84,7 @@ render name <> " := " <> render expr1 <> " :? " <> render expr2 render (PostponedCheckArgs name exprs expr1 expr2) = let exprs' = fmap (parens . render) exprs- in render name+ in render name <> " := " <> parens ("_ : " <> render expr1) <> " "@@ -81,17 +92,20 @@ <> " : " <> render expr2 render (IsEmptyType expr) = "Is empty: " <> render expr- render (SizeLtSat expr) = "Not empty type of sizes: " <> render expr+ render (SizeLtSat expr) = "Not empty type of sizes: " <> render expr render (FindInstanceOF name expr exprs) = let exprs' = (\(q, e, t) -> render q <> "=" <> render e <> " : " <> render t) <$> exprs- in fsep- [ "Resolve instance argument "- , render name <> " : " <> render expr- , "Candidate:"- , vcat exprs'+ in fsep+ [ "Resolve instance argument ",+ render name <> " : " <> render expr,+ "Candidate:",+ vcat exprs' ]+#if MIN_VERSION_Agda(2,7,0)+ render (ResolveInstanceOF q) = "Resolve output type of instance" <?> render q+#endif render (PTSInstance name1 name2) = "PTS instance for (" <> render name1 <> ", " <> render name2 <> ")" render (PostponedCheckFunDef name expr _err) =@@ -100,16 +114,20 @@ "Check lock" <+> render lk <+> "allows" <+> render t render (UsableAtMod modality t) = "Is usable at" <+> render modality <+> render t-#if MIN_VERSION_Agda(2,6,3) render (DataSort _name expr) =- fsep [ "Sort", render expr, "allows data/record definitions" ]-#endif+ fsep ["Sort", render expr, "allows data/record definitions"] -- | IPBoundary'-instance Render c => Render (IPBoundary' c) where- render (IPBoundary eqs val meta over) = do- let xs = fmap (\(l, r) -> render l <+> "=" <+> render r) eqs- rhs = case over of- Overapplied -> "=" <+> render meta- NotOverapplied -> mempty- fsep (punctuate "," xs) <+> "⊢" <+> render val <+> rhs+instance (Render c) => Render (IPBoundary' c) where+ render (IPBoundary m) = vcat $ flip fmap (Map.toList m) $ \case+ (boundary, rhs) ->+ fsep (punctuate "," xs) <+> "⊢" <+> render rhs+ where+ xs = flip fmap (IntMap.toList boundary) $ \(l, r) ->+ text $ concat ["@", show l, " = ", if r then "i1" else "i0"]++instance Render c => Render (IPFace' c) where+ render (IPFace' eqs val) = do+ let+ xs = map (\ (l,r) -> render l <+> "=" <+> render r) eqs+ fsep (punctuate "," xs) <+> "⊢" <+> render val
src/Render/Internal.hs view
@@ -5,28 +5,25 @@ import Agda.Syntax.Common (Hiding (..), LensHiding (getHiding), Named (namedThing)) import Agda.Syntax.Internal hiding (telToList)+import Agda.Utils.Function (applyWhen)+import Control.Monad import qualified Data.List as List+import qualified Data.Set as Set import Render.Class import Render.Common (renderHiding) import Render.Concrete () import Render.RichText-import qualified Data.Set as Set -------------------------------------------------------------------------------- -instance Render a => Render (Substitution' a) where+instance (Render a) => Render (Substitution' a) where renderPrec = pr where pr p input = case input of IdS -> "idS" EmptyS _ -> "emptyS" t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t]-#if MIN_VERSION_Agda(2,6,3)- Strengthen _ _ rho ->-#else- Strengthen _ rho ->-#endif- mparens (p > 9) $ "strS" <+> pr 10 rho+ Strengthen _ _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho @@ -73,7 +70,7 @@ | Just t <- domTactic dom = "@" <> parens ("tactic" <+> render t) | otherwise = mempty -renderDom :: LensHiding a => a -> Inlines -> Inlines+renderDom :: (LensHiding a) => a -> Inlines -> Inlines renderDom i = case getHiding i of NotHidden -> parens@@ -94,7 +91,7 @@ pBody (Just b) Nothing = render b pBody (Just b) (Just t) = fsep [render b <+> ":", render t] -instance Render a => Render (Tele (Dom a)) where+instance (Render a) => Render (Tele (Dom a)) where render tel = fsep [renderDom a (text x <+> ":" <+> render (unDom a)) | (x, a) <- telToList tel] where telToList EmptyTel = []@@ -119,7 +116,7 @@ instance Render PlusLevel where renderPrec p (Plus n a) = renderPrecLevelSucs p n $ \p' -> renderPrec p' a ---instance Render LevelAtom where+-- instance Render LevelAtom where -- LevelAtom is just Term -- renderPrec p a = -- case a of@@ -129,45 +126,38 @@ -- UnreducedLevel v -> renderPrec p v instance Render Sort where- renderPrec p srt =- case srt of- Type (ClosedLevel 0) -> "Set"- Type (ClosedLevel n) -> text $ "Set" ++ show n- Type l -> mparens (p > 9) $ "Set" <+> renderPrec 10 l- Prop (ClosedLevel 0) -> "Prop"- Prop (ClosedLevel n) -> text $ "Prop" ++ show n- Prop l -> mparens (p > 9) $ "Prop" <+> renderPrec 10 l- Inf IsFibrant 0 -> "Setω"- Inf IsStrict 0 -> "SSetω"- Inf IsFibrant n -> text $ "Setω" ++ show n- Inf IsStrict n -> text $ "SSetω" ++ show n- SSet l -> mparens (p > 9) $ "SSet" <+> renderPrec 10 l- SizeUniv -> "SizeUniv"- LockUniv -> "LockUniv"- PiSort a _s1 s2 ->- mparens (p > 9) $- "piSort" <+> renderDom (domInfo a) (text (absName s2) <+> ":" <+> render (unDom a))- <+> parens- ( fsep- [ text ("λ " ++ absName s2 ++ " ->"),- render (unAbs s2)- ]- )- FunSort a b ->- mparens (p > 9) $- "funSort" <+> renderPrec 10 a <+> renderPrec 10 b- UnivSort s -> mparens (p > 9) $ "univSort" <+> renderPrec 10 s- MetaS x es -> renderPrec p $ MetaV x es- DefS d es -> renderPrec p $ Def d es- DummyS s -> parens $ text s-#if MIN_VERSION_Agda(2,6,3)- IntervalUniv -> "IntervalUniv"-#endif+ renderPrec p = \case+ Univ u (ClosedLevel n) -> text $ suffix n $ showUniv u+ Univ u l -> mparens (p > 9) $ text (showUniv u) <+> renderPrec 10 l+ Inf u n -> text $ suffix n $ showUniv u ++ "ω"+ LevelUniv -> "LevelUniv"+ SizeUniv -> "SizeUniv"+ LockUniv -> "LockUniv"+ PiSort a _s1 s2 ->+ mparens (p > 9) $+ "piSort"+ <+> renderDom (domInfo a) (text (absName s2) <+> ":" <+> render (unDom a))+ <+> parens+ ( fsep+ [ text ("λ " ++ absName s2 ++ " ->"),+ render (unAbs s2)+ ]+ )+ FunSort a b ->+ mparens (p > 9) $+ "funSort" <+> renderPrec 10 a <+> renderPrec 10 b+ UnivSort s -> mparens (p > 9) $ "univSort" <+> renderPrec 10 s+ MetaS x es -> renderPrec p $ MetaV x es+ DefS d es -> renderPrec p $ Def d es+ DummyS s -> parens $ text s+ IntervalUniv -> "IntervalUniv"+ where+ suffix n = applyWhen (n /= 0) (++ show n) instance Render Type where renderPrec p (El _ a) = renderPrec p a -instance Render tm => Render (Elim' tm) where+instance (Render tm) => Render (Elim' tm) where renderPrec p (Apply v) = renderPrec p v renderPrec _ (Proj _o x) = "." <> render x renderPrec p (IApply _ _ r) = renderPrec p r@@ -175,7 +165,7 @@ instance Render DBPatVar where renderPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex x) -instance Render a => Render (Pattern' a) where+instance (Render a) => Render (Pattern' a) where renderPrec n (VarP _o x) = renderPrec n x renderPrec _ (DotP _o t) = "." <> renderPrec 10 t renderPrec n (ConP c i nps) =@@ -205,10 +195,8 @@ -- Agda.Syntax.Internal.Blockers instance Render Blocker where- render (UnblockOnAll us) = "all" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)- render (UnblockOnAny us) = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)- render (UnblockOnMeta m) = render m+ render (UnblockOnAll us) = "all" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)+ render (UnblockOnAny us) = "any" <> parens (fsep $ punctuate "," $ map render $ Set.toList us)+ render (UnblockOnMeta m) = render m render (UnblockOnProblem pid) = "problem" <+> render pid-#if MIN_VERSION_Agda(2,6,3)- render (UnblockOnDef q) = "definition" <+> render q-#endif+ render (UnblockOnDef q) = "definition" <+> render q
src/Render/Literal.hs view
@@ -1,19 +1,19 @@ module Render.Literal where -import Agda.Syntax.Literal ( Literal(..), showChar', showText )+import Agda.Syntax.Literal (Literal (..), showChar', showText) import Render.Class-import Render.RichText-import Render.Name () import Render.Common ()+import Render.Name ()+import Render.RichText -------------------------------------------------------------------------------- -- | Literal instance Render Literal where- render (LitNat n) = text $ show n+ render (LitNat n) = text $ show n render (LitWord64 n) = text $ show n- render (LitFloat d) = text $ show d+ render (LitFloat d) = text $ show d render (LitString s) = text $ showText s ""- render (LitChar c) = text $ "'" ++ showChar' c "'"- render (LitQName x) = render x+ render (LitChar c) = text $ "'" ++ showChar' c "'"+ render (LitQName x) = render x render (LitMeta _ x) = render x
src/Render/Name.hs view
@@ -1,35 +1,33 @@ module Render.Name where import qualified Agda.Syntax.Abstract as A+import qualified Agda.Syntax.Common as C import qualified Agda.Syntax.Concrete as C-import qualified Agda.Syntax.Common as C-import qualified Agda.Utils.List1 as Agda-+import qualified Agda.Utils.List1 as Agda import Render.Class import Render.RichText -------------------------------------------------------------------------------- --- | Concrete +-- | Concrete instance Render C.NamePart where render C.Hole = "_" render (C.Id s) = text $ C.rawNameToString s --- glueing name parts together +-- glueing name parts together instance Render C.Name where- render (C.Name range _inScope xs) = linkRange range $ mconcat (fmap render $ Agda.toList xs)+ render (C.Name range _inScope xs) = linkRange range $ mconcat (render <$> Agda.toList xs) render (C.NoName _ _) = "_" instance Render C.QName where render (C.Qual m x) | C.isUnderscore m = render x -- don't print anonymous modules- | otherwise = render m <> "." <> render x- render (C.QName x) = render x-+ | otherwise = render m <> "." <> render x+ render (C.QName x) = render x -------------------------------------------------------------------------------- --- | Abstract +-- | Abstract instance Render A.Name where render = render . A.nameConcrete
src/Render/Position.hs view
@@ -12,14 +12,12 @@ instance Render AbsolutePath where render = text . filePath -#if MIN_VERSION_Agda(2,6,3) instance Render RangeFile where- render = render . rangeFilePath -- TODO rangeFileName ?-#endif+ render = render . rangeFilePath -- TODO rangeFileName ? -------------------------------------------------------------------------------- -instance Render a => Render (Position' (Strict.Maybe a)) where+instance (Render a) => Render (Position' (Strict.Maybe a)) where render (Pn Strict.Nothing _ l c) = render l <> "," <> render c render (Pn (Strict.Just f) _ l c) = render f <> ":" <> render l <> "," <> render c@@ -28,7 +26,11 @@ render (Pn () _ l c) = render l <> "," <> render c instance Render IntervalWithoutFile where+#if MIN_VERSION_Agda(2,8,0)+ render (Interval () s e) = start <> "-" <> end+#else render (Interval s e) = start <> "-" <> end+#endif where sl = posLine s el = posLine e@@ -41,13 +43,22 @@ | sl == el = render ec | otherwise = render el <> "," <> render ec -instance Render a => Render (Interval' (Strict.Maybe a)) where+instance (Render a) => Render (Interval' (Strict.Maybe a)) where+#if MIN_VERSION_Agda(2,8,0)+ render i@(Interval f s e) = file <> render (Interval () s e)+ where+ file :: Inlines+ file = case f of+ Strict.Nothing -> mempty+ Strict.Just f -> render f <> ":"+#else render i@(Interval s _) = file <> render (setIntervalFile () i) where file :: Inlines file = case srcFile s of Strict.Nothing -> mempty Strict.Just f -> render f <> ":"+#endif -instance Render a => Render (Range' (Strict.Maybe a)) where+instance (Render a) => Render (Range' (Strict.Maybe a)) where render r = maybe mempty render (rangeToIntervalWithFile r)
src/Render/RichText.hs view
@@ -3,7 +3,7 @@ {-# LANGUAGE FlexibleInstances #-} module Render.RichText- ( Block(..),+ ( Block (..), Inlines (..), -- LinkTarget (..), space,@@ -16,11 +16,13 @@ icon, -- combinators (<+>),+ (<?>), punctuate, braces, braces', dbraces, mparens,+ textNonEmpty, hcat, hsep, sep,@@ -40,30 +42,31 @@ -- import qualified Agda.Interaction.Options as Agda -- import qualified Agda.Syntax.Concrete.Glyph as Agda-import qualified Agda.Syntax.Position as Agda-import qualified Agda.Utils.FileName as Agda-import qualified Agda.Utils.Null as Agda-import Agda.Utils.Suffix (toSubscriptDigit)--import Data.Aeson (ToJSON (toJSON), Value (Null))-import Data.Foldable (toList)-import Data.Sequence (Seq (..))-import qualified Data.Sequence as Seq-import Data.String (IsString (..))+import qualified Agda.Syntax.Position as Agda+import qualified Agda.Utils.FileName as Agda+import Agda.Utils.List (caseList, last1)+import Agda.Utils.Null+import qualified Agda.Utils.Null as Agda+import Agda.Utils.Suffix (toSubscriptDigit)+import Data.Aeson (ToJSON (toJSON), Value (Null))+import Data.Foldable (toList)+import Data.Sequence (Seq (..))+import qualified Data.Sequence as Seq import qualified Data.Strict.Maybe as Strict--import GHC.Generics (Generic)+import Data.String (IsString (..))+import GHC.Generics (Generic)+import Prelude hiding (null) ----------------------------------------------------------------------------------- | Block elements +-- | Block elements data Block- -- for blocks like "Goal" & "Have"- = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String- -- for ordinary goals & context- | Unlabeled Inlines (Maybe String) (Maybe Agda.Range)- -- headers- | Header String+ = -- for blocks like "Goal" & "Have"+ Labeled Inlines (Maybe String) (Maybe Agda.Range) String String+ | -- for ordinary goals & context+ Unlabeled Inlines (Maybe String) (Maybe Agda.Range)+ | -- headers+ Header String deriving (Generic) instance ToJSON Block@@ -80,21 +83,20 @@ Inlines as <> Inlines bs = Inlines (merge as bs) where merge :: Seq Inline -> Seq Inline -> Seq Inline- merge Empty ys = ys+ merge Empty ys = ys merge (xs :|> x) ys = merge xs (cons x ys) cons :: Inline -> Seq Inline -> Seq Inline cons (Text s c) (Text t d :<| xs) -- merge 2 adjacent Text if they have the same classnames- | c == d = Text (s <> t) c :<| xs+ | c == d = Text (s <> t) c :<| xs | otherwise = Text s c :<| Text t d :<| xs cons (Text s c) (Horz [] :<| xs) = cons (Text s c) xs- cons (Text s c) (Horz (Inlines t:ts) :<| xs)+ cons (Text s c) (Horz (Inlines t : ts) :<| xs) = -- merge Text with Horz when possible- = Horz (Inlines (cons (Text s c) t) :ts) :<| xs+ Horz (Inlines (cons (Text s c) t) : ts) :<| xs cons x xs = x :<| xs - instance Monoid Inlines where mempty = Inlines mempty @@ -104,29 +106,37 @@ instance Show Inlines where show (Inlines xs) = unwords $ map show $ toList xs --- | see if the rendered text is "empty"-isEmpty :: Inlines -> Bool-isEmpty (Inlines elems) = all elemIsEmpty (Seq.viewl elems)- where- elemIsEmpty :: Inline -> Bool- elemIsEmpty (Icon _ _) = False- elemIsEmpty (Text "" _) = True- elemIsEmpty (Text _ _) = False- elemIsEmpty (Link _ xs _) = all elemIsEmpty $ unInlines xs- elemIsEmpty (Hole _) = False- elemIsEmpty (Horz xs) = all isEmpty xs- elemIsEmpty (Vert xs) = all isEmpty xs- elemIsEmpty (Parn _) = False- elemIsEmpty (PrHz _) = False+instance Null Inlines where+ empty = mempty+ null (Inlines elems) = all elemIsNull (Seq.viewl elems)+ where+ elemIsNull :: Inline -> Bool+ elemIsNull (Icon _ _) = False+ elemIsNull (Text "" _) = True+ elemIsNull (Text _ _) = False+ elemIsNull (Link _ xs _) = all elemIsNull $ unInlines xs+ elemIsNull (Hole _) = False+ elemIsNull (Horz xs) = all null xs+ elemIsNull (Vert xs) = all null xs+ elemIsNull (Parn _) = False+ elemIsNull (PrHz _) = False +-- -- | see if the rendered text is "empty"+ infixr 6 <+> (<+>) :: Inlines -> Inlines -> Inlines x <+> y- | isEmpty x = y- | isEmpty y = x+ | null x = y+ | null y = x | otherwise = x <> " " <> y +infixl 6 <?>++-- | A synonym for '<+>' at the moment+(<?>) :: Inlines -> Inlines -> Inlines+(<?>) = (<+>)+ -- | Whitespace space :: Inlines space = " "@@ -191,7 +201,11 @@ instance {-# OVERLAPS #-} ToJSON Agda.Range instance ToJSON (Agda.Interval' ()) where+#if MIN_VERSION_Agda(2,8,0)+ toJSON (Agda.Interval () start end) = toJSON (start, end)+#else toJSON (Agda.Interval start end) = toJSON (start, end)+#endif instance ToJSON (Agda.Position' ()) where toJSON (Agda.Pn () pos line col) = toJSON [line, col, pos]@@ -203,18 +217,26 @@ instance ToJSON Agda.AbsolutePath where toJSON (Agda.AbsolutePath path) = toJSON path -#if MIN_VERSION_Agda(2,6,3) instance ToJSON Agda.RangeFile where toJSON (Agda.RangeFile path _maybeTopLevelModuleName) = toJSON path-#endif -------------------------------------------------------------------------------- -- | Utilities / Combinators --- -- TODO: implement this--- indent :: Inlines -> Inlines--- indent x = " " <> x+-- TODO: implement this+-- Modeled after `nest` defined in ‘Text.PrettyPrint.Annotated.HughesPJ’ (pretty-1.1.3.6)+--+-- Indent a Inline by a given number of positions (which may also be negative). `indent` satisfies the laws:+--+-- `indent` 0 x = x+-- `indent` k ( `indent` k' x) = `indent` (k+k') x+-- `indent` k (x `<>` y) = `indent` k z `<>` `indent` k y+-- `indent` k (x `$$` y) = `indent` k x `$$` `indent` k y+-- `indent` k `empty` = `empty`+-- `x <> indent k y = x <> y` , if x non-empty+-- indent :: Int -> Inlines -> Inlines+-- indent 0 x = x punctuate :: Inlines -> [Inlines] -> [Inlines] punctuate _ [] = []@@ -272,18 +294,20 @@ rightIdiomBrkt = _rightIdiomBrkt specialCharacters emptyIdiomBrkt = _emptyIdiomBrkt specialCharacters --- | Apply 'parens' to 'Doc' if boolean is true.+-- | Apply 'parens' to 'Inlines' if boolean is true. mparens :: Bool -> Inlines -> Inlines mparens True = parens mparens False = id --- | From braces'+-- | Return 'empty' for empty strings.+textNonEmpty :: String -> Inlines+textNonEmpty = \case+ "" -> empty+ s -> text s++-- | From braces'. v2.7.0.1 braces' :: Inlines -> Inlines-braces' d =- let s = show d- in if Agda.null s- then braces d- else braces (spaceIfDash (head s) <> d <> spaceIfDash (last s))+braces' d = caseList (show d) (braces d {-else-}) $ \c cs -> braces (spaceIfDash c <> d <> spaceIfDash (last1 c cs)) where -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269) -- Andreas, 2018-07-21, #3161: Also avoid ending a comment@@ -297,6 +321,7 @@ -------------------------------------------------------------------------------- --+ -- | Picking the appropriate set of special characters depending on -- whether we are allowed to use unicode or have to limit ourselves -- to ascii.
src/Render/TypeChecking.hs view
@@ -8,9 +8,9 @@ import Render.RichText instance Render NamedMeta where- render (NamedMeta "" x) = render x+ render (NamedMeta "" x) = render x render (NamedMeta "_" x) = render x- render (NamedMeta s x) = "_" <> text s <> render x+ render (NamedMeta s x) = "_" <> text s <> render x instance Render Occurrence where render =
src/Render/Utils.hs view
@@ -1,11 +1,11 @@-module Render.Utils where+{-# LANGUAGE CPP #-} -import Agda.Utils.Time ( CPUTime )-import Agda.Utils.Pretty (pretty)+module Render.Utils where +import Agda.Utils.Time (CPUTime)+import Agda.Syntax.Common.Pretty (pretty) import Render.Class import Render.RichText- instance Render CPUTime where render = text . show . pretty
src/Server.hs view
@@ -1,37 +1,40 @@ {-# LANGUAGE CPP #-}-{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ScopedTypeVariables #-} -- entry point of the LSP server -module Server- ( run- ) where+module Server (run, serverDefn) where import qualified Agda-import Control.Concurrent ( writeChan )-import Control.Monad ( void )-import Control.Monad.Reader ( MonadIO(liftIO) )-import Data.Aeson ( FromJSON- , ToJSON- )-import qualified Data.Aeson as JSON-import Data.Text ( pack )-import GHC.IO.IOMode ( IOMode(ReadWriteMode) )-import Language.LSP.Server hiding ( Options )-import Language.LSP.Types hiding ( Options(..)- , TextDocumentSyncClientCapabilities(..)- )-import Monad-import qualified Network.Simple.TCP as TCP-import Network.Socket ( socketToHandle )+import Control.Concurrent (writeChan)+import Control.Monad (void)+import Control.Monad.Reader (MonadIO (liftIO))+import Data.Aeson+ ( FromJSON,+ ToJSON,+ )+import qualified Data.Aeson as JSON+import Data.Text (pack)+import GHC.IO.IOMode (IOMode (ReadWriteMode))+import Language.LSP.Protocol.Message+import Language.LSP.Protocol.Types (HoverParams (..), SaveOptions (..), TextDocumentIdentifier (..), TextDocumentSyncKind (..), TextDocumentSyncOptions (..), type (|?) (..))+import Language.LSP.Server hiding (Options)+import qualified Language.LSP.Server hiding (Options)+import qualified Language.LSP.Server as LSP+import Monad+import Options+import qualified Server.Handler as Handler+import Switchboard (Switchboard, agdaCustomMethod) import qualified Switchboard-import Switchboard ( Switchboard ) -import qualified Server.Handler as Handler--import qualified Language.LSP.Server as LSP-import Options-+#if defined(wasm32_HOST_ARCH)+import Agda.Utils.IO (catchIO)+import System.IO (hPutStrLn, stderr)+import System.Posix.IO (stdInput, setFdOption, FdOption (..))+#else+import qualified Network.Simple.TCP as TCP+import Network.Socket (socketToHandle)+#endif -------------------------------------------------------------------------------- @@ -39,76 +42,101 @@ run options = do case optViaTCP options of Just port -> do- void- $ TCP.serve (TCP.Host "127.0.0.1") (show port)- $ \(sock, _remoteAddr) -> do+#if defined(wasm32_HOST_ARCH)+ error "WASM does not support listening to a port."+#else+ void $+ TCP.serve (TCP.Host "127.0.0.1") (show port) $+ \(sock, _remoteAddr) -> do -- writeChan (envLogChan env) "[Server] connection established" handle <- socketToHandle sock ReadWriteMode- _ <- runServerWithHandles-#if MIN_VERSION_lsp(1,5,0)- mempty mempty-#endif- handle handle (serverDefn options)+ _ <- runServerWithHandles mempty mempty handle handle (serverDefn options) return () -- Switchboard.destroy switchboard return 0+#endif Nothing -> do+#if defined(wasm32_HOST_ARCH)+ liftIO $ setFdOption stdInput NonBlockingRead True+ `catchIO` (\ (e :: IOError) -> hPutStrLn stderr $ "Failed to enable nonblocking on stdin: " ++ (show e) ++ "\nThe WASM module might not behave correctly.")+#endif runServer (serverDefn options)- where- serverDefn :: Options -> ServerDefinition Config- serverDefn options = ServerDefinition- { defaultConfig = initConfig- , onConfigurationChange = \old newRaw -> case JSON.fromJSON newRaw of- JSON.Error s -> Left $ pack $ "Cannot parse server configuration: " <> s- JSON.Success new -> Right new- , doInitialize = \ctxEnv _req -> do- env <- runLspT ctxEnv (createInitEnv options)- switchboard <- Switchboard.new env- Switchboard.setupLanguageContextEnv switchboard ctxEnv- pure $ Right (ctxEnv, env)- , staticHandlers = handlers- , interpretHandler = \(ctxEnv, env) ->- Iso (runLspT ctxEnv . runServerM env) liftIO- , options = lspOptions- } - lspOptions :: LSP.Options- lspOptions = defaultOptions { textDocumentSync = Just syncOptions }-- -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client- syncOptions :: TextDocumentSyncOptions- syncOptions = TextDocumentSyncOptions { _openClose = Just True -- receive open and close notifications from the client- , _change = Just changeOptions -- receive change notifications from the client- , _willSave = Just False -- receive willSave notifications from the client- , _willSaveWaitUntil = Just False -- receive willSave notifications from the client- , _save = Just $ InR saveOptions- }+serverDefn :: Options -> ServerDefinition Config+serverDefn options =+ ServerDefinition+ { defaultConfig = initConfig,+ onConfigChange = const $ pure (),+ parseConfig = \old newRaw -> case JSON.fromJSON newRaw of+ JSON.Error s -> Left $ pack $ "Cannot parse server configuration: " <> s+ JSON.Success new -> Right new,+ doInitialize = \ctxEnv _req -> do+ env <- runLspT ctxEnv (createInitEnv options)+ switchboard <- Switchboard.new env+ Switchboard.setupLanguageContextEnv switchboard ctxEnv+ pure $ Right (ctxEnv, env),+ configSection = "dummy",+ staticHandlers = const handlers,+ interpretHandler = \(ctxEnv, env) ->+ Iso+ { forward = runLspT ctxEnv . runServerM env,+ backward = liftIO+ },+ options = lspOptions+ } - changeOptions :: TextDocumentSyncKind- changeOptions = TdSyncIncremental+lspOptions :: LSP.Options+lspOptions = defaultOptions {optTextDocumentSync = Just syncOptions} - -- includes the document content on save, so that we don't have to read it from the disk- saveOptions :: SaveOptions- saveOptions = SaveOptions (Just True)+-- these `TextDocumentSyncOptions` are essential for receiving notifications from the client+-- syncOptions :: TextDocumentSyncOptions+-- syncOptions =+-- TextDocumentSyncOptions+-- { _openClose = Just True, -- receive open and close notifications from the client+-- _change = Just changeOptions, -- receive change notifications from the client+-- _willSave = Just False, -- receive willSave notifications from the client+-- _willSaveWaitUntil = Just False, -- receive willSave notifications from the client+-- _save = Just $ InR saveOptions+-- }+syncOptions :: TextDocumentSyncOptions+syncOptions =+ TextDocumentSyncOptions+ { _openClose = Just True, -- receive open and close notifications from the client+ _change = Just TextDocumentSyncKind_Incremental, -- receive change notifications from the client+ _willSave = Just False, -- receive willSave notifications from the client+ _willSaveWaitUntil = Just False, -- receive willSave notifications from the client+ _save = Just $ InR $ SaveOptions (Just True) -- includes the document content on save, so that we don't have to read it from the disk (not sure if this is still true in lsp 2)+ } -- handlers of the LSP server handlers :: Handlers (ServerM (LspM Config))-handlers = mconcat- [ -- custom methods, not part of LSP- requestHandler (SCustomMethod "agda") $ \req responder -> do- let RequestMessage _ _i _ params = req- response <- Agda.sendCommand params- responder $ Right response- ,- -- hover provider- requestHandler STextDocumentHover $ \req responder -> do- let- RequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone)- = req- result <- Handler.onHover uri pos- responder $ Right result- -- -- syntax highlighting- -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do- -- result <- Handler.onHighlight (req ^. (params . textDocument . uri))- -- responder result- ]+handlers =+ mconcat+ [ -- custom methods, not part of LSP+ requestHandler agdaCustomMethod $ \req responder -> do+ let TRequestMessage _ _i _ params = req+ response <- Agda.sendCommand params+ responder $ Right response,+ -- `textDocument/hover`+ requestHandler SMethod_TextDocumentHover $ \req responder -> do+ let TRequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) = req+ result <- Handler.onHover uri pos+ responder $ Right result,+ -- -- syntax highlighting+ -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do+ -- result <- Handler.onHighlight (req ^. (params . textDocument . uri))+ -- responder result++ -- `initialized`+ notificationHandler SMethod_Initialized $ \_notification -> return (),+ -- `workspace/didChangeConfiguration`+ notificationHandler SMethod_WorkspaceDidChangeConfiguration $ \_notification -> return (),+ -- `textDocument/didOpen`+ notificationHandler SMethod_TextDocumentDidOpen $ \_notification -> return (),+ -- `textDocument/didClose`+ notificationHandler SMethod_TextDocumentDidClose $ \_notification -> return (),+ -- `textDocument/didChange`+ notificationHandler SMethod_TextDocumentDidChange $ \_notification -> return (),+ -- `textDocument/didSave`+ notificationHandler SMethod_TextDocumentDidSave $ \_notification -> return ()+ ]
src/Server/CommandController.hs view
@@ -15,10 +15,10 @@ data CommandController = CommandController+ -- | Unbounded Command queue (SizedChan IOTCM)- -- ^ Unbounded Command queue+ -- | MVar for the Command consumer (MVar IOTCM)- -- ^ MVar for the Command consumer new :: IO CommandController new = CommandController <$> newSizedChan <*> newEmptyMVar
src/Server/Handler.hs view
@@ -6,8 +6,12 @@ , runAgda ) import qualified Agda.IR as IR-import Agda.Interaction.Base ( CommandM- , CommandQueue(..)++import Agda.Interaction.Base ( CommandQueue(..)+#if MIN_VERSION_Agda(2,7,0)+#else+ , CommandM+#endif , CommandState(optionsOnReload) , Rewrite(AsIs) , initCommandState@@ -20,7 +24,16 @@ import qualified Agda.Interaction.Imports as Imp import Agda.Interaction.InteractionTop ( cmd_load'+#if MIN_VERSION_Agda(2,8,0)+#else , localStateCommandM+#endif++#if MIN_VERSION_Agda(2,8,0)+#elif MIN_VERSION_Agda(2,7,0)+ , CommandM+#else+#endif ) import Agda.Interaction.Options ( CommandLineOptions ( optAbsoluteIncludePaths@@ -39,8 +52,15 @@ import Agda.TypeChecking.Monad ( HasOptions(commandLineOptions) , setInteractionOutputCallback )+#if MIN_VERSION_Agda(2,8,0)+import Agda.Interaction.Command ( CommandM, localStateCommandM )+import Agda.TypeChecking.Monad.Trace ( runPM )+#endif+#if MIN_VERSION_Agda(2,8,0)+#else import Agda.TypeChecking.Warnings ( runPM )-import Agda.Utils.Pretty ( render )+#endif+import Agda.Syntax.Common.Pretty ( render ) import Control.Concurrent.STM import Control.Monad.Reader import Control.Monad.State@@ -51,7 +71,7 @@ import qualified Data.Text as Text import Language.LSP.Server ( LspM ) import qualified Language.LSP.Server as LSP-import qualified Language.LSP.Types as LSP+import qualified Language.LSP.Protocol.Types as LSP import qualified Language.LSP.VFS as VFS import Monad import Options ( Config@@ -88,55 +108,49 @@ let norm = AsIs -- localStateCommandM: restore TC state afterwards, do we need this here? typ <- localStateCommandM $ do-#if MIN_VERSION_Agda(2,6,3)- (e, _attrs)-#else- e-#endif- <- lift $ runPM $ parse exprParser (unpack text)+ (e, _attrs) <- lift $ runPM $ parse exprParser (unpack text) lift $ atTopLevel $ do concreteToAbstract_ e >>= typeInCurrent norm render <$> prettyATop typ -onHover :: LSP.Uri -> LSP.Position -> ServerM (LspM Config) (Maybe LSP.Hover)+onHover :: LSP.Uri -> LSP.Position -> ServerM (LspM Config) (LSP.Hover LSP.|? LSP.Null) onHover uri pos = do result <- LSP.getVirtualFile (LSP.toNormalizedUri uri) case result of- Nothing -> return Nothing+ Nothing -> return $ LSP.InR LSP.Null Just file -> do let source = VFS.virtualFileText file let offsetTable = makeToOffset source let agdaPos = toAgdaPositionWithoutFile offsetTable pos lookupResult <- Parser.tokenAt uri source agdaPos case lookupResult of- Nothing -> return Nothing+ Nothing -> return $ LSP.InR LSP.Null Just (_token, text) -> do case LSP.uriToFilePath uri of- Nothing -> return Nothing+ Nothing -> return $ LSP.InR LSP.Null Just filepath -> do let range = LSP.Range pos pos- inferResult <- inferTypeOfText filepath text case inferResult of Left err -> do- let content = LSP.HoverContents $ LSP.markedUpContent- "agda-language-server"- ("Error: " <> pack err)- return $ Just $ LSP.Hover content (Just range)+ let content = hoverContent $ "Error: " <> pack err+ return $ LSP.InL $ LSP.Hover content (Just range) Right typeString -> do- let content = LSP.HoverContents $ LSP.markedUpContent- "agda-language-server"- (pack typeString)- return $ Just $ LSP.Hover content (Just range)-+ let content = hoverContent $ pack typeString+ return $ LSP.InL $ LSP.Hover content (Just range)+ where+ hoverContent =+ LSP.InL . LSP.mkMarkdownCodeBlock "agda-language-server" -------------------------------------------------------------------------------- -- Helper functions for converting stuff to SemanticTokenAbsolute fromHighlightingInfo :: IR.HighlightingInfo -> LSP.SemanticTokenAbsolute fromHighlightingInfo (IR.HighlightingInfo start end aspects isTokenBased note defSrc)- = LSP.SemanticTokenAbsolute 1 1 3 LSP.SttKeyword []+ = LSP.SemanticTokenAbsolute 1 1 3 kw []+ where+ kw = LSP.SemanticTokenTypes_Keyword -- HighlightingInfo -- Int -- starting offset
src/Server/ResponseController.hs view
@@ -2,28 +2,28 @@ -- Makes sure that all dispatched works are done. -- Notify when all dispatched works are done. module Server.ResponseController- ( ResponseController- , new- , dispatch- , setCheckpointAndWait- ) where+ ( ResponseController,+ new,+ dispatch,+ setCheckpointAndWait,+ )+where -import Control.Concurrent-import Control.Concurrent.SizedChan-import Control.Monad ( void- , when- )-import Data.IORef+import Control.Concurrent+import Control.Concurrent.SizedChan+import Control.Monad+ ( void,+ when,+ )+import Data.IORef data ResponseController = ResponseController { -- | The number of work dispatched- dispatchedCount :: IORef Int- ,+ dispatchedCount :: IORef Int, -- | The number of work completed- completedCount :: IORef Int- ,+ completedCount :: IORef Int, -- | A channel of "Checkpoints" to be met- checkpointChan :: SizedChan Checkpoint+ checkpointChan :: SizedChan Checkpoint } -- | An "Checkpoint" is just a number with a callback, the callback will be invoked once the number is "met"@@ -47,7 +47,7 @@ result <- tryPeekSizedChan (checkpointChan controller) case result of -- no checkpoints, do nothing- Nothing -> return ()+ Nothing -> return () -- a checkpoint is set! Just (dispatched, callback) -> do completed <- readIORef (completedCount controller)@@ -62,7 +62,7 @@ setCheckpoint :: ResponseController -> (() -> IO ()) -> IO () setCheckpoint controller callback = do dispatched <- readIORef (dispatchedCount controller)- completed <- readIORef (completedCount controller)+ completed <- readIORef (completedCount controller) -- see if the previously dispatched works have been completed if dispatched == completed then callback ()
src/Switchboard.hs view
@@ -1,23 +1,33 @@-module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy) where+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeApplications #-} -import Monad+module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy, agdaCustomMethod) where++import qualified Agda import Control.Concurrent-import qualified Server.ResponseController as ResponseController import Control.Monad import Control.Monad.Reader-import qualified Agda import qualified Data.Aeson as JSON+import Data.IORef+import Data.Proxy (Proxy (Proxy)) import qualified Data.Text.IO as Text+import Language.LSP.Protocol.Message+import Language.LSP.Protocol.Types hiding+ ( TextDocumentSyncClientCapabilities (..),+ ) import Language.LSP.Server-import Language.LSP.Types hiding (TextDocumentSyncClientCapabilities (..))-import Data.IORef+import Monad import Options (Config)+import qualified Server.ResponseController as ResponseController+import System.IO (stderr) data Switchboard = Switchboard- { sbPrintLog :: ThreadId- , sbSendResponse :: ThreadId- , sbRunAgda :: ThreadId- , sbLanguageContextEnv :: IORef (Maybe (LanguageContextEnv Config))+ { sbPrintLog :: ThreadId,+ sbSendResponse :: ThreadId,+ sbRunAgda :: ThreadId,+ sbLanguageContextEnv :: IORef (Maybe (LanguageContextEnv Config)) } -- | All channels go in and out from here@@ -42,13 +52,13 @@ killThread (sbRunAgda switchboard) writeIORef (sbLanguageContextEnv switchboard) Nothing --- | Keep printing log+-- | Keep printing log to stderr -- Consumer of `envLogChan` keepPrintingLog :: Env -> IO () keepPrintingLog env = forever $ do result <- readChan (envLogChan env) when (envDevMode env) $ do- Text.putStrLn result+ Text.hPutStrLn stderr result -- | Keep sending reactions -- Consumer of `envResponseChan`@@ -62,6 +72,9 @@ callback <- liftIO $ ResponseController.dispatch (envResponseController env) let value = JSON.toJSON response- sendRequest (SCustomMethod "agda") value $ \_result -> liftIO $ do+ sendRequest agdaCustomMethod value $ \_result -> liftIO $ do -- writeChan (envLogChan env) $ "[Response] >>>> " <> pack (show value) callback ()++agdaCustomMethod :: SMethod ('Method_CustomMethod "agda")+agdaCustomMethod = SMethod_CustomMethod (Proxy @"agda")
− stack-8.10-Agda-2.6.2.2.yaml
@@ -1,21 +0,0 @@-resolver: lts-18.28-compiler: ghc-8.10.7-# Allow a newer minor version of GHC than the snapshot specifies-compiler-check: newer-minor--packages:-- .--# Use some newer versions than in the lts-18.28 snapshot-extra-deps:-- Agda-2.6.2.2-- text-icu-0.8.0.1-- lsp-1.2.0.1-- lsp-types-1.3.0.1--flags:- agda-language-server:- Agda-2-6-2-2: true- Agda:- # optimise-heavily: true- enable-cluster-counting: true
− stack-9.0-Agda-2.6.2.2.yaml
@@ -1,19 +0,0 @@-resolver: lts-19.33-compiler: ghc-9.0.2-# Allow a newer minor version of GHC than the snapshot specifies-compiler-check: newer-minor--packages:-- .--# Use some newer versions than in the lts-19.33 snapshot-extra-deps:-- text-icu-0.8.0.1-# - Agda-2.6.2.2 # This is the lts-19.33 version of Agda--flags:- agda-language-server:- Agda-2-6-2-2: true- Agda:- # optimise-heavily: true- enable-cluster-counting: true
+ stack-9.10.2-Agda-2.6.4.3.yaml view
@@ -0,0 +1,26 @@+resolver: lts-24.1+compiler: ghc-9.10.2+# Allow a newer minor version of GHC than the snapshot specifies+compiler-check: newer-minor+# CI pins and installs GHC itself (haskell-actions/setup, via ghcup); use+# that GHC directly instead of Stack downloading its own separate copy+# into ~/.stack/programs. Without this, every job -- cold or warm alike+# -- pays a redundant full GHC download+configure, since ~/.stack/programs+# is untracked by the cache and Stack is otherwise unaware the+# ghcup-installed GHC exists.+system-ghc: true++packages:+- .++extra-deps:+- Agda-2.6.4.3 +- hashable-1.4.7.0@sha256:573f3ab242f75465a0d67ce9d84202650a1606575e6dbd6d31ffcf4767a9a379,6629+- network-simple-0.4.2@sha256:3614a0b7e51bcafb5643c3dc3a3a89d20a99671998c8814eb6fc55fa99e38444,1375++flags:+ agda-language-server:+ Agda-2-6-4: true+ Agda:+ # optimise-heavily: true+ enable-cluster-counting: true
+ stack-9.10.2-Agda-2.7.0.1.yaml view
@@ -0,0 +1,25 @@+resolver: lts-24.1+compiler: ghc-9.10.2+# Allow a newer minor version of GHC than the snapshot specifies+compiler-check: newer-minor+# CI pins and installs GHC itself (haskell-actions/setup, via ghcup); use+# that GHC directly instead of Stack downloading its own separate copy+# into ~/.stack/programs. Without this, every job -- cold or warm alike+# -- pays a redundant full GHC download+configure, since ~/.stack/programs+# is untracked by the cache and Stack is otherwise unaware the+# ghcup-installed GHC exists.+system-ghc: true++packages:+- .++extra-deps:+- Agda-2.7.0.1+- network-simple-0.4.2@sha256:3614a0b7e51bcafb5643c3dc3a3a89d20a99671998c8814eb6fc55fa99e38444,1375++flags:+ agda-language-server:+ Agda-2-7-0: true+ Agda:+ # optimise-heavily: true+ enable-cluster-counting: true
+ stack-9.10.2-Agda-2.8.0.yaml view
@@ -0,0 +1,25 @@+resolver: lts-24.1+compiler: ghc-9.10.2+# Allow a newer minor version of GHC than the snapshot specifies+compiler-check: newer-minor+# CI pins and installs GHC itself (haskell-actions/setup, via ghcup); use+# that GHC directly instead of Stack downloading its own separate copy+# into ~/.stack/programs. Without this, every job -- cold or warm alike+# -- pays a redundant full GHC download+configure, since ~/.stack/programs+# is untracked by the cache and Stack is otherwise unaware the+# ghcup-installed GHC exists.+system-ghc: true++packages:+- .++extra-deps:+- Agda-2.8.0+- network-simple-0.4.2@sha256:3614a0b7e51bcafb5643c3dc3a3a89d20a99671998c8814eb6fc55fa99e38444,1375++flags:+ agda-language-server:+ Agda-2-8-0: true+ Agda:+ # optimise-heavily: true+ enable-cluster-counting: true
− stack-9.2-Agda-2.6.2.2.yaml
@@ -1,17 +0,0 @@-resolver: lts-20.26-compiler: ghc-9.2.8-# Allow a newer minor version of GHC than the snapshot specifies-compiler-check: newer-minor--packages:-- .--extra-deps:-- Agda-2.6.2.2--flags:- agda-language-server:- Agda-2-6-2-2: true- Agda:- # optimise-heavily: true- enable-cluster-counting: true
stack.yaml view
@@ -1,5 +1,5 @@-resolver: lts-20.26-compiler: ghc-9.2.8+resolver: lts-24.1+compiler: ghc-9.10.2 # Allow a newer minor version of GHC than the snapshot specifies compiler-check: newer-minor @@ -7,9 +7,12 @@ - . extra-deps:-- Agda-2.6.3+- Agda-2.8.0+- network-simple-0.4.2@sha256:3614a0b7e51bcafb5643c3dc3a3a89d20a99671998c8814eb6fc55fa99e38444,1375 flags:+ agda-language-server:+ Agda-2-8-0: true Agda: # optimise-heavily: true enable-cluster-counting: true
test/Test.hs view
@@ -1,11 +1,38 @@-import qualified Test.SrcLoc as SrcLoc-import Test.Tasty ( TestTree- , defaultMain- , testGroup- )+{-# LANGUAGE CPP #-} +import Data.Proxy (Proxy (..))+import Data.Typeable (Typeable)+import qualified Test.LSP as LSP+import qualified Test.SrcLoc as SrcLoc+#if defined(wasm32_HOST_ARCH)+import qualified Test.WASM as WASM+#endif+import Test.Tasty+import Test.Tasty.Options++-- Define the custom option+newtype AlsPathOption = AlsPathOption FilePath+ deriving (Show, Typeable)++instance IsOption AlsPathOption where+ defaultValue = AlsPathOption "als"+ parseValue = Just . AlsPathOption+ optionName = return "als-path"+ optionHelp = return "Path to the als executable"+ main :: IO ()-main = defaultMain tests+main = do+ let opts = [Option (Proxy :: Proxy AlsPathOption)]+ ingredients = includingOptions opts : defaultIngredients+ defaultMainWithIngredients ingredients tests tests :: TestTree-tests = testGroup "Tests" [SrcLoc.tests]+tests = askOption $ \(AlsPathOption alsPath) ->+ testGroup+ "Tests"+ [ SrcLoc.tests,+ LSP.tests alsPath+#if defined(wasm32_HOST_ARCH)+ , WASM.tests alsPath+#endif+ ]
+ test/Test/LSP.hs view
@@ -0,0 +1,49 @@+{-# LANGUAGE OverloadedStrings #-}++module Test.LSP (tests) where++import Agda+import Control.Monad.IO.Class+import qualified Data.Aeson as JSON+import Language.LSP.Protocol.Message+import Language.LSP.Protocol.Types+import Language.LSP.Test+import Switchboard (agdaCustomMethod)+import Test.Tasty+import Test.Tasty.HUnit++tests :: FilePath -> TestTree+tests alsPath =+ testGroup+ "LSP"+ [ testCase "load" (demo alsPath)+ ]++demo :: FilePath -> IO ()+demo alsPath = do+ putStrLn $ "Running LSP tests on the server with the following path to the als executable: " ++ alsPath+ runSession alsPath fullLatestClientCaps "test/data/" $ do+ doc <- openDoc "A.agda" "agda"++ -- hover+ TResponseMessage _ _ rsp <- request SMethod_TextDocumentHover (HoverParams doc (Position 3 9) Nothing)+ case rsp of+ Right (InL (Hover (InL (MarkupContent _ content)) (Just (Range start end)))) -> liftIO $ do+ -- disregard the content of the hover message for now+ -- because it varies depending on the version of Agda+ -- content @?= "\n```agda-language-server\nAgda.Primitive.Set\n```\n"+ start @?= Position 3 9+ end @?= Position 3 9+ _ -> liftIO $ assertFailure "Unexpected response"++ -- agda-mode:load+ testCustomMethod "IOTCM \"test/data/A.agdaa\" NonInteractive Direct( Cmd_load \"test/data/A.agda\" [] )"++-- | Sends a custom method request to the server and expects a response of `CmdRes Nothing`+testCustomMethod :: String -> Session ()+testCustomMethod cmd = do+ TResponseMessage _ _ rsp <-+ request agdaCustomMethod $+ JSON.toJSON $+ CmdReq cmd+ liftIO $ rsp @?= Right (JSON.toJSON (CmdRes Nothing))
test/Test/SrcLoc.hs view
@@ -1,11 +1,11 @@ module Test.SrcLoc where -import Test.Tasty-import Test.Tasty.HUnit-import Data.List (sort) import Agda.Position-import Data.Text (Text) import qualified Data.IntMap as IntMap+import Data.List (sort)+import Data.Text (Text)+import Test.Tasty+import Test.Tasty.HUnit tests :: TestTree tests = testGroup "Source Location" [positionToOffsetTests, offsetToPositionTests]@@ -16,14 +16,14 @@ positionToOffsetTests = testGroup "Position => Offset"- [ testCase "cached table" $ IntMap.toList (unToOffset table) @?= [(1, 4), (2, 9), (3, 12)]- , testCase "line 0" $ run [(0, 0), (0, 1), (0, 2), (0, 3)] @?= [0, 1, 2, 3]- , testCase "line 1" $ run [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)] @?= [4, 5, 6, 7, 8]- , testCase "line 2" $ run [(2, 0), (2, 1)] @?= [9, 10]- , testCase "line 3" $ run [(3, 0), (3, 1)] @?= [12, 13]+ [ testCase "cached table" $ IntMap.toList (unToOffset table) @?= [(1, 4), (2, 9), (3, 12)],+ testCase "line 0" $ run [(0, 0), (0, 1), (0, 2), (0, 3)] @?= [0, 1, 2, 3],+ testCase "line 1" $ run [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)] @?= [4, 5, 6, 7, 8],+ testCase "line 2" $ run [(2, 0), (2, 1)] @?= [9, 10],+ testCase "line 3" $ run [(3, 0), (3, 1)] @?= [12, 13] ] where- text :: Text + text :: Text text = "012\n456\r\n90\r23" table :: ToOffset@@ -31,21 +31,21 @@ run :: [(Int, Int)] -> [Int] run = map (toOffset table)- + -------------------------------------------------------------------------------- offsetToPositionTests :: TestTree offsetToPositionTests = testGroup "Offset => Position"- [ testCase "cached table" $ IntMap.toList (unFromOffset table) @?= [(4, 1), (9, 2), (12, 3)]- , testCase "line 0" $ run [0, 1, 2, 3] @?= [(0, 0), (0, 1), (0, 2), (0, 3)]- , testCase "line 1" $ run [4, 5, 6, 7, 8] @?= [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)]- , testCase "line 2" $ run [9, 10] @?= [(2, 0), (2, 1)]- , testCase "line 3" $ run [12, 13] @?= [(3, 0), (3, 1)]+ [ testCase "cached table" $ IntMap.toList (unFromOffset table) @?= [(4, 1), (9, 2), (12, 3)],+ testCase "line 0" $ run [0, 1, 2, 3] @?= [(0, 0), (0, 1), (0, 2), (0, 3)],+ testCase "line 1" $ run [4, 5, 6, 7, 8] @?= [(1, 0), (1, 1), (1, 2), (1, 3), (1, 4)],+ testCase "line 2" $ run [9, 10] @?= [(2, 0), (2, 1)],+ testCase "line 3" $ run [12, 13] @?= [(3, 0), (3, 1)] ] where- text :: Text + text :: Text text = "012\n456\r\n90\r23" table :: FromOffset@@ -53,4 +53,3 @@ run :: [Int] -> [(Int, Int)] run = map (fromOffset table)-
+ test/Test/WASM.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}++module Test.WASM (tests) where++import Test.Tasty+import Test.Tasty.HUnit++#if defined(wasm32_HOST_ARCH)++tests :: FilePath -> TestTree+tests alsPath = testGroup "WASM Tests"+ [ testCase "WASM generation" wasmGenerationTest+ , testCase "WASM compilation" wasmCompilationTest+ , testCase "WASM execution dummy" wasmExecutionTest+ ]++wasmGenerationTest :: IO ()+wasmGenerationTest = do+ putStrLn "Testing WASM generation..."+ -- Dummy test for WASM generation+ -- In a real implementation, this would:+ -- 1. Compile Agda code to WASM+ -- 2. Verify the WASM file is generated+ -- 3. Check WASM file structure/validity+ assertBool "WASM generation succeeds" True++wasmCompilationTest :: IO ()+wasmCompilationTest = do+ putStrLn "Testing WASM compilation..."+ -- Dummy test for WASM compilation+ -- In a real implementation, this would:+ -- 1. Take sample Agda code+ -- 2. Compile it with WASM backend+ -- 3. Verify compilation succeeds+ assertBool "WASM compilation succeeds" True++wasmExecutionTest :: IO ()+wasmExecutionTest = do+ putStrLn "Testing WASM execution..."+ -- Dummy test for WASM execution+ -- In a real implementation, this would:+ -- 1. Load compiled WASM module+ -- 2. Execute WASM functions+ -- 3. Verify expected results+ assertBool "WASM execution works" True++#else++-- When not building for WASM, provide empty tests +tests :: FilePath -> TestTree+tests _ = testGroup "WASM Tests (disabled - only available when building for wasm32 architecture)" []++#endif