diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -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
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -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 C-x C-s 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.
diff --git a/agda-language-server.cabal b/agda-language-server.cabal
--- a/agda-language-server.cabal
+++ b/agda-language-server.cabal
@@ -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
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
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -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 ()
diff --git a/app/Reactor.hs b/app/Reactor.hs
new file mode 100644
--- /dev/null
+++ b/app/Reactor.hs
@@ -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
diff --git a/package.yaml b/package.yaml
--- a/package.yaml
+++ b/package.yaml
@@ -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
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:
diff --git a/src/Agda.hs b/src/Agda.hs
--- a/src/Agda.hs
+++ b/src/Agda.hs
@@ -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)
diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs
--- a/src/Agda/Convert.hs
+++ b/src/Agda/Convert.hs
@@ -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)
diff --git a/src/Agda/IR.hs b/src/Agda/IR.hs
--- a/src/Agda/IR.hs
+++ b/src/Agda/IR.hs
@@ -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)
diff --git a/src/Agda/Parser.hs b/src/Agda/Parser.hs
--- a/src/Agda/Parser.hs
+++ b/src/Agda/Parser.hs
@@ -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
diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs
--- a/src/Agda/Position.hs
+++ b/src/Agda/Position.hs
@@ -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
diff --git a/src/Monad.hs b/src/Monad.hs
--- a/src/Monad.hs
+++ b/src/Monad.hs
@@ -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
diff --git a/src/Options.hs b/src/Options.hs
--- a/src/Options.hs
+++ b/src/Options.hs
@@ -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
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -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 ()
diff --git a/src/Render/Class.hs b/src/Render/Class.hs
--- a/src/Render/Class.hs
+++ b/src/Render/Class.hs
@@ -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
diff --git a/src/Render/Common.hs b/src/Render/Common.hs
--- a/src/Render/Common.hs
+++ b/src/Render/Common.hs
@@ -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"
diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs
--- a/src/Render/Concrete.hs
+++ b/src/Render/Concrete.hs
@@ -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.
diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs
--- a/src/Render/Interaction.hs
+++ b/src/Render/Interaction.hs
@@ -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
diff --git a/src/Render/Internal.hs b/src/Render/Internal.hs
--- a/src/Render/Internal.hs
+++ b/src/Render/Internal.hs
@@ -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
diff --git a/src/Render/Literal.hs b/src/Render/Literal.hs
--- a/src/Render/Literal.hs
+++ b/src/Render/Literal.hs
@@ -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
diff --git a/src/Render/Name.hs b/src/Render/Name.hs
--- a/src/Render/Name.hs
+++ b/src/Render/Name.hs
@@ -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
diff --git a/src/Render/Position.hs b/src/Render/Position.hs
--- a/src/Render/Position.hs
+++ b/src/Render/Position.hs
@@ -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)
diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs
--- a/src/Render/RichText.hs
+++ b/src/Render/RichText.hs
@@ -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.
diff --git a/src/Render/TypeChecking.hs b/src/Render/TypeChecking.hs
--- a/src/Render/TypeChecking.hs
+++ b/src/Render/TypeChecking.hs
@@ -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 =
diff --git a/src/Render/Utils.hs b/src/Render/Utils.hs
--- a/src/Render/Utils.hs
+++ b/src/Render/Utils.hs
@@ -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
diff --git a/src/Server.hs b/src/Server.hs
--- a/src/Server.hs
+++ b/src/Server.hs
@@ -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 ()
+ ]
diff --git a/src/Server/CommandController.hs b/src/Server/CommandController.hs
--- a/src/Server/CommandController.hs
+++ b/src/Server/CommandController.hs
@@ -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
diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs
--- a/src/Server/Handler.hs
+++ b/src/Server/Handler.hs
@@ -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
diff --git a/src/Server/ResponseController.hs b/src/Server/ResponseController.hs
--- a/src/Server/ResponseController.hs
+++ b/src/Server/ResponseController.hs
@@ -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 ()
diff --git a/src/Switchboard.hs b/src/Switchboard.hs
--- a/src/Switchboard.hs
+++ b/src/Switchboard.hs
@@ -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")
diff --git a/stack-8.10-Agda-2.6.2.2.yaml b/stack-8.10-Agda-2.6.2.2.yaml
deleted file mode 100644
--- a/stack-8.10-Agda-2.6.2.2.yaml
+++ /dev/null
@@ -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
diff --git a/stack-9.0-Agda-2.6.2.2.yaml b/stack-9.0-Agda-2.6.2.2.yaml
deleted file mode 100644
--- a/stack-9.0-Agda-2.6.2.2.yaml
+++ /dev/null
@@ -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
diff --git a/stack-9.10.2-Agda-2.6.4.3.yaml b/stack-9.10.2-Agda-2.6.4.3.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.10.2-Agda-2.6.4.3.yaml
@@ -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
diff --git a/stack-9.10.2-Agda-2.7.0.1.yaml b/stack-9.10.2-Agda-2.7.0.1.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.10.2-Agda-2.7.0.1.yaml
@@ -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
diff --git a/stack-9.10.2-Agda-2.8.0.yaml b/stack-9.10.2-Agda-2.8.0.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.10.2-Agda-2.8.0.yaml
@@ -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
diff --git a/stack-9.2-Agda-2.6.2.2.yaml b/stack-9.2-Agda-2.6.2.2.yaml
deleted file mode 100644
--- a/stack-9.2-Agda-2.6.2.2.yaml
+++ /dev/null
@@ -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
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -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
diff --git a/test/Test.hs b/test/Test.hs
--- a/test/Test.hs
+++ b/test/Test.hs
@@ -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
+ ]
diff --git a/test/Test/LSP.hs b/test/Test/LSP.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/LSP.hs
@@ -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))
diff --git a/test/Test/SrcLoc.hs b/test/Test/SrcLoc.hs
--- a/test/Test/SrcLoc.hs
+++ b/test/Test/SrcLoc.hs
@@ -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)
-
diff --git a/test/Test/WASM.hs b/test/Test/WASM.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/WASM.hs
@@ -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