agda-language-server 0.0.3.0 → 0.2.0
raw patch · 32 files changed
+1429/−803 lines, 32 filesdep +tastydep +tasty-goldendep +tasty-hunitdep ~Agdadep ~lsp
Dependencies added: tasty, tasty-golden, tasty-hunit, tasty-quickcheck
Dependency ranges changed: Agda, lsp
Files
- CHANGELOG.md +27/−0
- README.md +9/−38
- agda-language-server.cabal +56/−18
- app/Main.hs +10/−44
- package.yaml +120/−0
- src/Agda.hs +206/−74
- src/Agda/Convert.hs +30/−31
- src/Agda/IR.hs +1/−1
- src/Agda/Misc.hs +0/−89
- src/Agda/Parser.hs +2/−1
- src/Agda/Position.hs +110/−59
- src/Monad.hs +43/−26
- src/Options.hs +113/−0
- src/Render/Class.hs +21/−12
- src/Render/Common.hs +26/−9
- src/Render/Concrete.hs +132/−99
- src/Render/Interaction.hs +61/−76
- src/Render/Internal.hs +36/−21
- src/Render/Literal.hs +8/−10
- src/Render/Name.hs +5/−6
- src/Render/Position.hs +0/−1
- src/Render/RichText.hs +28/−43
- src/Render/TypeChecking.hs +0/−3
- src/Render/Utils.hs +4/−2
- src/Server.hs +92/−117
- src/Server/Handler.hs +155/−0
- src/Server/ResponseController.hs +20/−15
- src/Switchboard.hs +5/−6
- stack.yaml +42/−0
- test/Spec.hs +0/−2
- test/Test.hs +11/−0
- test/Test/SrcLoc.hs +56/−0
CHANGELOG.md view
@@ -0,0 +1,27 @@+# Changelog++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).++## v0.2.0 - TBA++### 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++### Fixed +- #5: Connection Error+
README.md view
@@ -1,52 +1,23 @@-# agda-language-server--Language Server Protocol for Agda--To be developed alongside [agda-mode-vscode](https://github.com/banacorn/agda-mode-vscode)--## Can I try it now?--Yes.--However, this project is not available on Hackage for the moment.-You will have to pull it from GitHub--```-git clone git@github.com:banacorn/agda-language-server.git-```+# Agda Language Server -Checkout to a version that is compatible with your agda-mode on VS Code+## Installation -```-git checkout v0.0.1.0-```+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).+Follow the instructions and the language server should be installed within seconds. -Here are the versions that work (on my machine)+### Prebuilt binaries -| Language Server | [agda-mode](https://marketplace.visualstudio.com/items?itemName=banacorn.agda-mode) |-| --------------- | ------------- |-| [v0.0.1.0](https://github.com/banacorn/agda-language-server/releases/tag/v0.0.1.0) | v0.2.8 |-| [v0.0.2.0](https://github.com/banacorn/agda-language-server/releases/tag/v0.0.2.0) | v0.2.10 |+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. +Supported platforms: **Windows**, **Mac**, and **Ubuntu**. -Build it with the package manager you hate the least. +### Build from source -I use Stack. But honestly, I couldn't care less.+You will need [Haskell Stack](https://docs.haskellstack.org/en/stable/README/) to build the project: ``` stack install ```--Once you have `als` installed on your machine. Open VS Code and go to agda-mode's settings. Enable "Agda Mode: Agda Language Server".----## Current features--More stuff are clickable in the panel after loading (<kbd>C-c</kbd> <kbd>C-l</kbd>)--- ## Why make it standalone?
agda-language-server.cabal view
@@ -1,27 +1,27 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack------ hash: 0f24217c91b5f8c3f3d6da5c70694d98b0ef55971a5324a2c460ca48c06c4bb1 name: agda-language-server-version: 0.0.3.0-synopsis: LSP server for Agda+version: 0.2.0+synopsis: An implementation of language server protocal (LSP) for Agda 2. description: Please see the README on GitHub at <https://github.com/banacorn/agda-language-server#readme> category: Development homepage: https://github.com/banacorn/agda-language-server#readme bug-reports: https://github.com/banacorn/agda-language-server/issues-author: Ting-gan LUA+author: Ting-Gian LUA maintainer: banacorn@gmail.com-copyright: 2020 Ting-gan LUA+copyright: 2020 Author name here :) license: MIT license-file: LICENSE build-type: Simple extra-source-files: README.md CHANGELOG.md+ stack.yaml+ package.yaml source-repository head type: git@@ -32,11 +32,11 @@ Agda Agda.Convert Agda.IR- Agda.Misc Agda.Parser Agda.Position Control.Concurrent.SizedChan Monad+ Options Render Render.Class Render.Common@@ -51,19 +51,24 @@ Render.Utils Server Server.CommandController+ Server.Handler Server.ResponseController Switchboard other-modules: Paths_agda_language_server hs-source-dirs: src+ default-extensions:+ LambdaCase+ OverloadedStrings+ 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:- Agda+ Agda ==2.6.2 , aeson , base >=4.7 && <5 , bytestring , containers- , lsp+ , lsp <2 , mtl , network , network-simple@@ -79,15 +84,15 @@ Paths_agda_language_server hs-source-dirs: app- ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N -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 -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans build-depends:- Agda+ Agda ==2.6.2 , aeson , agda-language-server , base >=4.7 && <5 , bytestring , containers- , lsp+ , lsp <2 , mtl , network , network-simple@@ -99,25 +104,58 @@ test-suite als-test type: exitcode-stdio-1.0- main-is: Spec.hs+ main-is: Test.hs other-modules:+ Test.SrcLoc+ Agda+ Agda.Convert+ Agda.IR+ Agda.Parser+ Agda.Position+ Control.Concurrent.SizedChan+ Monad+ Options+ Render+ Render.Class+ Render.Common+ Render.Concrete+ Render.Interaction+ Render.Internal+ Render.Literal+ Render.Name+ Render.Position+ Render.RichText+ Render.TypeChecking+ Render.Utils+ Server+ Server.CommandController+ Server.Handler+ Server.ResponseController+ Switchboard Paths_agda_language_server hs-source-dirs: test- ghc-options: -threaded -rtsopts -with-rtsopts=-N+ src+ default-extensions:+ LambdaCase+ OverloadedStrings+ 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 build-depends:- Agda+ Agda ==2.6.2 , aeson- , agda-language-server , base >=4.7 && <5 , bytestring , containers- , lsp+ , lsp <2 , mtl , network , network-simple , process , stm , strict+ , tasty+ , tasty-golden+ , tasty-hunit+ , tasty-quickcheck , text default-language: Haskell2010
app/Main.hs view
@@ -1,50 +1,16 @@ module Main where -import Server (run)-import System.Console.GetOpt-import System.Environment (getArgs)-import Text.Read (readMaybe)+import Options+import Server ( run )+import System.Console.GetOpt+import System.Environment ( getArgs )+import Text.Read ( readMaybe ) main :: IO () main = do- (opts, _) <- getArgs >>= parseOpts- if optHelp opts - then putStrLn $ usageInfo usage options- else do - _ <- run (optViaTCP opts)+ options <- getOptionsFromArgv+ if optHelp options+ then putStrLn usageMessage+ else do+ _ <- run options return ()-------------------------------------------------------------------------------------- | Command-line arguments-data Options = Options- { optViaTCP :: Maybe Int,- optHelp :: Bool- }--defaultOptions :: Options-defaultOptions = Options {optViaTCP = Nothing, optHelp = 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}) "PORT")- "talk with the editor via TCP port (4096 as default)"- ]--usage :: String-usage = "Agda Language Server v0.0.3.0 \nUsage: als [Options...]\n"--parseOpts :: [String] -> IO (Options, [String])-parseOpts argv = case getOpt Permute options argv of- (o, n, []) -> return (foldl (flip id) defaultOptions o, n)- (_, _, errs) -> ioError $ userError $ concat errs ++ usageInfo usage options
+ package.yaml view
@@ -0,0 +1,120 @@+name: agda-language-server+version: 0.2.0+github: "banacorn/agda-language-server"+license: MIT+author: "Ting-Gian LUA"+maintainer: "banacorn@gmail.com"+copyright: "2020 Author name here :)"++extra-source-files:+- README.md+- CHANGELOG.md+- stack.yaml+- package.yaml++# Metadata used when publishing your package+synopsis: An implementation of language server protocal (LSP) for Agda 2. +category: Development++# To avoid duplicated efforts in documentation and dealing with the+# complications of embedding Haddock markup inside cabal files, it is+# common to point users to the README.md file.+description: Please see the README on GitHub at <https://github.com/banacorn/agda-language-server#readme>++dependencies:+ - base >= 4.7 && < 5+ - Agda == 2.6.2+ - aeson+ - bytestring+ - containers+ - lsp < 2+ - mtl+ - network+ - network-simple+ - strict+ - stm+ - text+ - process++library:+ source-dirs: src+ 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+ default-extensions:+ - LambdaCase+ - OverloadedStrings++executables:+ als:+ main: Main.hs+ source-dirs: app+ 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+ dependencies:+ - agda-language-server++tests:+ als-test:+ main: Test.hs+ source-dirs:+ - test+ - src+ dependencies:+ - tasty+ - tasty-hunit+ - tasty-golden+ - tasty-quickcheck++ 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++ default-extensions:+ - LambdaCase+ - OverloadedStrings++# tests:+# als-test:+# main: Spec.hs+# source-dirs: test+# ghc-options:+# - -threaded+# - -rtsopts+# - -with-rtsopts=-N+# dependencies:+# - agda-language-server
src/Agda.hs view
@@ -1,109 +1,241 @@-{-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -Wno-missing-methods #-}+{-# LANGUAGE DeriveGeneric #-} -module Agda where+module Agda+ ( start+ , runAgda+ , sendCommand+ , getCommandLineOptions+ ) where -import Agda.Convert (fromResponse)-import Agda.Interaction.Base (Command, Command' (Command, Done, Error), CommandM, CommandState (optionsOnReload), IOTCM, initCommandState)-import qualified Agda.Interaction.Imports as Imp-import Agda.Interaction.InteractionTop (initialiseCommandQueue, maybeAbort, runInteraction)-import Agda.Interaction.Options (CommandLineOptions (optAbsoluteIncludePaths))-import Agda.TypeChecking.Errors (prettyError, prettyTCWarnings')-import Agda.TypeChecking.Monad- ( TCErr,- commandLineOptions,- runTCMTop',- )-import Agda.TypeChecking.Monad.Base (TCM)-import qualified Agda.TypeChecking.Monad.Benchmark as Bench-import Agda.TypeChecking.Monad.State (setInteractionOutputCallback)-import Agda.Utils.Impossible (CatchImpossible (catchImpossible), Impossible)-import Agda.VersionCommit (versionWithCommitInfo)-import Monad-import Control.Exception-import Control.Monad.Except (catchError)-import Control.Monad.Reader-import Control.Monad.State-import Data.Maybe (listToMaybe)-import Data.Text (pack)+import Agda.Compiler.Backend ( parseBackendOptions )+import Agda.Compiler.Builtin ( builtinBackends )+import Agda.Convert ( fromResponse )+import Agda.Interaction.Base ( Command+ , Command'(Command, Done, Error)+ , CommandM+ , CommandState(optionsOnReload)+ , IOTCM+ , initCommandState+ )+import Agda.Interaction.InteractionTop+ ( initialiseCommandQueue+ , maybeAbort+ , runInteraction+ )+import Agda.Interaction.Options ( CommandLineOptions+ ( optAbsoluteIncludePaths+ )+ , defaultOptions+ , runOptM+ )+import Agda.TypeChecking.Errors ( getAllWarningsOfTCErr+ , prettyError+ , prettyTCWarnings'+ )+import Agda.TypeChecking.Monad ( HasOptions+ , TCErr+ , commandLineOptions+ , runTCMTop'+ )+import Agda.TypeChecking.Monad.Base ( TCM )+import qualified Agda.TypeChecking.Monad.Benchmark+ as Bench+import Agda.TypeChecking.Monad.State ( setInteractionOutputCallback )+import Agda.Utils.FileName ( absolute )+import Agda.Utils.Impossible ( CatchImpossible+ ( catchImpossible+ )+ , Impossible+ )+import Agda.VersionCommit ( versionWithCommitInfo )+import Control.Exception ( SomeException+ , catch+ )+import Control.Monad.Except+import Control.Monad.Reader+import Control.Monad.State+import Data.Aeson ( FromJSON+ , ToJSON(toJSON)+ , Value+ , fromJSON+ )+import qualified Data.Aeson as JSON+import Data.Maybe ( listToMaybe )+import Data.Text ( pack )+import GHC.Generics ( Generic )+import Language.LSP.Server ( getConfig )+import Monad+import Options ( Config(configRawAgdaOptions)+ , Options(optRawAgdaOptions)+ ) getAgdaVersion :: String getAgdaVersion = versionWithCommitInfo -interact :: ServerM IO ()-interact = do+start :: ServerM IO ()+start = do env <- ask writeLog "[Agda] interaction start" - result <- mapReaderT runTCMPrettyErrors $ do+ result <- runAgda $ do -- decides how to output Response- lift $- setInteractionOutputCallback $ \response -> do- reaction <- fromResponse response- sendResponse env reaction+ lift $ setInteractionOutputCallback $ \response -> do+ reaction <- fromResponse response+ sendResponse env reaction -- keep reading command commands <- liftIO $ initialiseCommandQueue (readCommand env) + -- get command line options + options <- getCommandLineOptions+ -- start the loop- opts <- commandLineOptions- let commandState = (initCommandState commands) {optionsOnReload = opts {optAbsoluteIncludePaths = []}}+ let commandState = (initCommandState commands)+ { optionsOnReload = options { optAbsoluteIncludePaths = [] }+ } _ <- mapReaderT (`runStateT` commandState) (loop env) return () -- TODO: we should examine the result case result of- Left _err -> return ()+ Left _err -> return () Right _val -> return ()- where- loop :: Env -> ServerM CommandM ()- loop env = do- Bench.reset- done <- Bench.billTo [] $ do- r <- lift $ maybeAbort runInteraction- case r of- Done -> return True -- Done.- Error s -> do- writeLog ("Error " <> pack s)- return False- Command _ -> do- writeLog "[Response] Finished sending, waiting for them to complete"- waitUntilResponsesSent- signalCommandFinish- return False+ where+ loop :: Env -> ServerM CommandM ()+ loop env = do+ Bench.reset+ done <- Bench.billTo [] $ do+ r <- lift $ maybeAbort runInteraction+ case r of+ Done -> return True -- Done.+ Error s -> do+ writeLog ("Error " <> pack s)+ return False+ Command _ -> do+ writeLog "[Response] Finished sending, waiting for them to complete"+ waitUntilResponsesSent+ signalCommandFinish+ return False - lift Bench.print- unless done (loop env)+ lift Bench.print+ unless done (loop env) - -- Reads the next command from the Channel- readCommand :: Env -> IO Command- readCommand env = Command <$> consumeCommand env+ -- Reads the next command from the Channel+ readCommand :: Env -> IO Command+ readCommand env = Command <$> consumeCommand env +--------------------------------------------------------------------------------++-- | Convert "CommandReq" to "CommandRes"++sendCommand :: MonadIO m => Value -> ServerM m Value+sendCommand value = do+ -- JSON Value => Request => Response+ case fromJSON value of+ JSON.Error msg ->+ return+ $ toJSON+ $ CmdRes+ $ Just+ $ CmdErrCannotDecodeJSON+ $ show msg+ ++ "\n"+ ++ show value+ JSON.Success request -> toJSON <$> handleCommandReq request+++handleCommandReq :: MonadIO m => CommandReq -> ServerM m CommandRes+handleCommandReq CmdReqSYN = return $ CmdResACK Agda.getAgdaVersion+handleCommandReq (CmdReq cmd) = do+ case parseIOTCM cmd of+ Left err -> do+ writeLog $ "[Error] CmdErrCannotParseCommand:\n" <> pack err+ return $ CmdRes (Just (CmdErrCannotParseCommand err))+ Right iotcm -> do+ writeLog $ "[Request] " <> pack (show cmd)+ provideCommand iotcm+ return $ CmdRes Nothing+ parseIOTCM :: String -> Either String IOTCM parseIOTCM raw = case listToMaybe $ reads raw of- Just (x, "") -> Right x+ Just (x, "" ) -> Right x Just (_, remnent) -> Left $ "not consumed: " ++ remnent- _ -> Left $ "cannot read: " ++ raw+ _ -> Left $ "cannot read: " ++ raw --- TODO: handle the caught errors+-------------------------------------------------------------------------------- +getCommandLineOptions+ :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions+getCommandLineOptions = do+ -- command line options from ARGV + argv <- asks (optRawAgdaOptions . envOptions)+ -- command line options from agda-mode+ config <- asks (configRawAgdaOptions . envConfig)+ -- concatenate both + let merged = argv <> config++ result <- runExceptT $ do+ (bs, opts) <- ExceptT $ runOptM $ parseBackendOptions builtinBackends+ merged+ defaultOptions+ return opts+ case result of+ -- something bad happened, use the default options instead + Left _ -> commandLineOptions+ Right opts -> return opts+ -- | Run a TCM action in IO and throw away all of the errors-runTCMPrettyErrors :: TCM a -> IO (Either String a)-runTCMPrettyErrors p =- runTCMTop' ((Right <$> p) `catchError` handleTCErr `catchImpossible` handleImpossible) `catch` catchException- where- handleTCErr :: TCErr -> TCM (Either String a)- handleTCErr err = do- s2s <- prettyTCWarnings' =<< Imp.getAllWarningsOfTCErr err- s1 <- prettyError err- let ss = filter (not . null) $ s2s ++ [s1]- let errorMsg = unlines ss- return (Left errorMsg)+-- TODO: handle the caught errors+runAgda :: MonadIO m => ServerM TCM a -> ServerM m (Either String a)+runAgda p = do+ env <- ask+ let p' = runServerM env p+ liftIO+ $ runTCMTop'+ ( (Right <$> p')+ `catchError` handleTCErr+ `catchImpossible` handleImpossible+ )+ `catch` catchException+ where+ handleTCErr :: TCErr -> TCM (Either String a)+ handleTCErr err = do+ s2s <- prettyTCWarnings' =<< getAllWarningsOfTCErr err+ s1 <- prettyError err+ let ss = filter (not . null) $ s2s ++ [s1]+ let errorMsg = unlines ss+ return (Left errorMsg) - handleImpossible :: Impossible -> TCM (Either String a)- handleImpossible = return . Left . show+ handleImpossible :: Impossible -> TCM (Either String a)+ handleImpossible = return . Left . show - catchException :: SomeException -> IO (Either String a)- catchException e = return $ Left $ show e+ catchException :: SomeException -> IO (Either String a)+ catchException e = return $ Left $ show e++--------------------------------------------------------------------------------++data CommandReq+ = CmdReqSYN -- ^ For client to initiate a 2-way handshake+ | CmdReq String+ deriving (Generic)++instance FromJSON CommandReq++data CommandRes+ = CmdResACK -- ^ For server to complete a 2-way handshake+ String -- ^ Version number of Agda+ | CmdRes -- ^ Response for 'CmdReq'+ (Maybe CommandErr) -- ^ 'Nothing' to indicate success+ deriving (Generic)++instance ToJSON CommandRes++data CommandErr+ = CmdErrCannotDecodeJSON String+ | CmdErrCannotParseCommand String+ deriving (Generic)++instance ToJSON CommandErr
src/Agda/Convert.hs view
@@ -1,6 +1,3 @@-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}- module Agda.Convert where import Render ( Block(..), Inlines, renderATop, Render(..) )@@ -11,18 +8,18 @@ import Agda.Interaction.BasicOps as B import Agda.Interaction.EmacsCommand (Lisp) import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)-import Agda.Interaction.Highlighting.Precise (Aspects (..), CompressedFile (ranges), DefinitionSite (..), HighlightingInfo, TokenBased (..))+import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..)) import qualified Agda.Interaction.Highlighting.Range as Highlighting-import Agda.Interaction.Imports (getAllWarningsOfTCErr) import Agda.Interaction.InteractionTop (localStateCommandM) import Agda.Interaction.Response as R import Agda.Syntax.Abstract as A import Agda.Syntax.Abstract.Pretty (prettyATop) import Agda.Syntax.Common import Agda.Syntax.Concrete as C+import Agda.Syntax.Internal (alwaysUnblock) import Agda.Syntax.Position (HasRange (getRange), Range, noRange) import Agda.Syntax.Scope.Base-import Agda.TypeChecking.Errors (prettyError)+import Agda.TypeChecking.Errors (getAllWarningsOfTCErr, prettyError) import Agda.TypeChecking.Monad hiding (Function) import Agda.TypeChecking.Pretty (prettyTCM) import qualified Agda.TypeChecking.Pretty as TCP@@ -35,6 +32,7 @@ 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.String (delimiter) import Agda.Utils.Time (CPUTime) import Agda.VersionCommit (versionWithCommitInfo)@@ -80,12 +78,12 @@ fromResponse (Resp_Status s) = return $ IR.ResponseStatus (sChecked s) (sShowImplicitArguments s) fromResponse (Resp_JumpToError f p) = return $ IR.ResponseJumpToError f (fromIntegral p) fromResponse (Resp_InteractionPoints is) =- return $ IR.ResponseInteractionPoints (map interactionId is)+ return $ IR.ResponseInteractionPoints (fmap interactionId is) fromResponse (Resp_GiveAction (InteractionId i) giveAction) = return $ IR.ResponseGiveAction i (fromAgda giveAction) fromResponse (Resp_MakeCase _ Function pcs) = return $ IR.ResponseMakeCaseFunction pcs fromResponse (Resp_MakeCase _ ExtendedLambda pcs) = return $ IR.ResponseMakeCaseExtendedLambda pcs-fromResponse (Resp_SolveAll ps) = return $ IR.ResponseSolveAll (map prn ps)+fromResponse (Resp_SolveAll ps) = return $ IR.ResponseSolveAll (fmap prn ps) where prn (InteractionId i, e) = (i, prettyShow e) @@ -116,7 +114,7 @@ (filePath (Map.findWithDefault __IMPOSSIBLE__ moduleName modFile), offset) infos :: [IR.HighlightingInfo]- infos = map fromAspects (ranges h)+ infos = fmap fromAspects (toList h) keepHighlighting :: Bool keepHighlighting =@@ -139,14 +137,14 @@ -- serializes warnings <- mapM prettyTCM filteredWarnings errors <- mapM prettyTCM filteredErrors- return $ IR.DisplayInfoCompilationOk (map show warnings) (map show errors)+ return $ IR.DisplayInfoCompilationOk (fmap show warnings) (fmap show errors) Info_Constraints s -> do -- constraints <- forM s $ \e -> do -- rendered <- renderTCM e -- let raw = show (pretty e) -- return $ Unlabeled rendered (Just raw) -- return $ IR.DisplayInfoGeneric "Constraints" constraints- return $ IR.DisplayInfoGeneric "Constraints" [Unlabeled (Render.text $ show $ vcat $ map pretty s) Nothing Nothing]+ return $ IR.DisplayInfoGeneric "Constraints" [Unlabeled (Render.text $ show $ vcat $ fmap pretty s) Nothing Nothing] Info_AllGoalsWarnings (ims, hms) ws -> do -- visible metas (goals) goals <- mapM convertGoal ims@@ -173,7 +171,7 @@ " Done" <$ guard (not (isG || isW || isE)) ] - return $ IR.DisplayInfoAllGoalsWarnings ("*All" ++ title ++ "*") goals metas (map show warnings) (map show errors)+ return $ IR.DisplayInfoAllGoalsWarnings ("*All" ++ title ++ "*") goals metas (fmap show warnings) (fmap show errors) where convertHiddenMeta :: OutputConstraint A.Expr NamedMeta -> TCM Block convertHiddenMeta m = do@@ -190,11 +188,11 @@ convertGoal i = do -- output constrain goal <-- withInteractionId (outputFormId $ OutputForm noRange [] i) $+ withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock i) $ renderATop i serialized <-- withInteractionId (outputFormId $ OutputForm noRange [] i) $+ withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock i) $ prettyATop i return $ Unlabeled goal (Just $ show serialized) Nothing Info_Auto s -> return $ IR.DisplayInfoAuto s@@ -243,7 +241,7 @@ return $ vcat [ "Modules",- nest 2 $ vcat $ map pretty modules,+ nest 2 $ vcat $ fmap pretty modules, "Names", nest 2 $ align 10 typeDocs ]@@ -308,14 +306,14 @@ then [] else Header "Boundary" :- map (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries+ 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" :- map (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints+ fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints return $ IR.DisplayInfoGeneric "Goal type etc" $ goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect@@ -403,24 +401,25 @@ shadowing :: LocalVar -> TCM Doc shadowing (LocalVar _ _ []) = "shadowing" shadowing _ = "in conflict with"- names = TCP.vcat . map pName- modules = TCP.vcat . map pMod+ names = TCP.vcat . fmap pName+ modules = TCP.vcat . fmap pMod pKind = \case- ConName -> "constructor"- FldName -> "record field"- PatternSynName -> "pattern synonym"- GeneralizeName -> "generalizable variable"+ AxiomName -> "postulate"+ ConName -> "constructor"+ CoConName -> "coinductive constructor"+ DataName -> "data type" DisallowedGeneralizeName -> "generalizable variable from let open"- MacroName -> "macro name"- QuotableName -> "quotable name"+ FldName -> "record field"+ FunName -> "defined name"+ GeneralizeName -> "generalizable variable"+ MacroName -> "macro name"+ PatternSynName -> "pattern synonym"+ PrimName -> "primitive function"+ QuotableName -> "quotable name" -- previously DefName:- DataName -> "data type"- RecName -> "record type"- AxiomName -> "postulate"- PrimName -> "primitive function"- FunName -> "defined name"- OtherDefName -> "defined name"+ RecName -> "record type"+ OtherDefName -> "defined name" pName :: AbstractName -> TCM Doc pName a =
src/Agda/IR.hs view
@@ -89,7 +89,7 @@ Int -- ending offset [String] -- list of names of aspects Bool -- is token based?- (Maybe String) -- note+ String -- note (Maybe (FilePath, Int)) -- the defining module of the token and its position in that module deriving (Generic, Show)
− src/Agda/Misc.hs
@@ -1,89 +0,0 @@-{-# LANGUAGE OverloadedStrings #-}--module Agda.Misc where--import Agda (runTCMPrettyErrors)-import Agda.Interaction.Base (CommandM, CommandQueue (..), CommandState (optionsOnReload), Rewrite (AsIs), initCommandState)-import Agda.Interaction.BasicOps (atTopLevel, typeInCurrent)-import qualified Agda.Interaction.Imports as Imp-import Agda.Interaction.InteractionTop (cmd_load', localStateCommandM)-import Agda.Interaction.Options (CommandLineOptions (optAbsoluteIncludePaths))-import qualified Agda.Parser as Parser-import Agda.Position (makeOffsetTable, toPositionWithoutFile)-import Agda.Syntax.Abstract.Pretty (prettyATop)-import Agda.Syntax.Parser (exprParser, parse)-import Agda.Syntax.Translation.ConcreteToAbstract (concreteToAbstract_)-import Agda.TypeChecking.Monad (HasOptions (commandLineOptions), setInteractionOutputCallback)-import Agda.TypeChecking.Warnings (runPM)-import Agda.Utils.Pretty (render)-import Control.Concurrent.STM-import Control.Monad.Reader-import Control.Monad.State-import Data.Text (Text, pack, unpack)-import Language.LSP.Server (LspM)-import qualified Language.LSP.Server as LSP-import qualified Language.LSP.Types as LSP-import qualified Language.LSP.VFS as VFS-import Monad (ServerM)--initialiseCommandQueue :: IO CommandQueue-initialiseCommandQueue = CommandQueue <$> newTChanIO <*> newTVarIO Nothing--runCommandM :: CommandM a -> IO (Either String a)-runCommandM program = runTCMPrettyErrors $ do- -- we need to set InteractionOutputCallback else it would panic- setInteractionOutputCallback $ \response -> return ()-- -- setup the command state- commandQueue <- liftIO initialiseCommandQueue- opts <- commandLineOptions- let commandState = (initCommandState commandQueue) {optionsOnReload = opts {optAbsoluteIncludePaths = []}}-- evalStateT program commandState--inferTypeOfText :: FilePath -> Text -> ServerM (LspM ()) (Either String String)-inferTypeOfText filepath text = liftIO $- runCommandM $ do- -- load first- cmd_load' filepath [] True Imp.TypeCheck $ \_ -> return ()- -- infer later- let norm = AsIs- -- localStateCommandM: restore TC state afterwards, do we need this here?- typ <- localStateCommandM $ do- e <- lift $ runPM $ parse exprParser (unpack text)- lift $- atTopLevel $ do- concreteToAbstract_ e >>= typeInCurrent norm-- render <$> prettyATop typ--onHover :: LSP.Uri -> LSP.Position -> ServerM (LspM ()) (Maybe LSP.Hover)-onHover uri pos = do- result <- LSP.getVirtualFile (LSP.toNormalizedUri uri)- case result of- Nothing -> return Nothing- Just file -> do- let source = VFS.virtualFileText file- let offsetTable = makeOffsetTable source- let agdaPos = toPositionWithoutFile offsetTable pos- lookupResult <-- Parser.tokenAt- uri- source- agdaPos- case lookupResult of- Nothing -> return Nothing- Just (token, text) -> do- case LSP.uriToFilePath uri of- Nothing -> return Nothing- Just filepath -> do- let range = LSP.Range pos pos-- inferResult <- inferTypeOfText filepath text- case inferResult of- Left error -> do- let content = LSP.HoverContents $ LSP.markedUpContent "agda-language-server" ("Error: " <> pack error)- return $ Just $ 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)
src/Agda/Parser.hs view
@@ -14,10 +14,11 @@ import qualified Data.Text as Text import Language.LSP.Server (LspM) import qualified Language.LSP.Types as LSP+import Options (Config) -------------------------------------------------------------------------------- -tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM ()) (Maybe (Token, Text))+tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM Config) (Maybe (Token, Text)) tokenAt uri source position = case LSP.uriToFilePath uri of Nothing -> return Nothing Just filepath -> do
src/Agda/Position.hs view
@@ -1,85 +1,136 @@--- {-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}- module Agda.Position- ( OffsetTable,- makeOffsetTable,- lookupOffsetTable,- toPositionWithoutFile,- toRange,- prettyPositionWithoutFile,- )-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.Sequence (Seq)-import qualified Data.Sequence as Seq-import qualified Data.Strict.Maybe as Strict-import Data.Text (Text, foldl')-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.Types as LSP -- Note: LSP srclocs are 0-base -- Agda srclocs are 1-base ------------------------------------------------------------------------------------ | LSP locations -> Agda locations+-- | LSP source locations => Agda source locations -- | LSP Range -> Agda Range-toRange :: OffsetTable -> Text -> LSP.Range -> Range-toRange table path (LSP.Range start end) =- Range (Strict.Just (AbsolutePath path)) (Seq.singleton interval)- where- interval :: IntervalWithoutFile- interval = Interval (toPositionWithoutFile table start) (toPositionWithoutFile table end)+toAgdaRange :: ToOffset -> Text -> LSP.Range -> Range+toAgdaRange table path (LSP.Range start end) = Range+ (Strict.Just (AbsolutePath path))+ (Seq.singleton interval)+ where+ interval :: IntervalWithoutFile+ interval = Interval (toAgdaPositionWithoutFile table start)+ (toAgdaPositionWithoutFile table end) -- | LSP Position -> Agda PositionWithoutFile-toPositionWithoutFile :: OffsetTable -> LSP.Position -> PositionWithoutFile-toPositionWithoutFile table (LSP.Position line col) =- Pn- ()- (fromIntegral (lookupOffsetTable table line col) + 1)- (fromIntegral line + 1)- (fromIntegral col + 1)+toAgdaPositionWithoutFile :: ToOffset -> LSP.Position -> PositionWithoutFile+toAgdaPositionWithoutFile table (LSP.Position line col) = Pn+ ()+ (fromIntegral (toOffset table (line, col)) + 1)+ (fromIntegral line + 1)+ (fromIntegral col + 1) prettyPositionWithoutFile :: PositionWithoutFile -> String-prettyPositionWithoutFile pos@(Pn () offset line col) = "[" <> show pos <> "-" <> show offset <> "]"+prettyPositionWithoutFile pos@(Pn () offset _line _col) =+ "[" <> show pos <> "-" <> show offset <> "]" ------------------------------------------------------------------------------------ | Positon -> Offset convertion+-- | Positon => Offset convertion --- | A list of offsets of linebreaks ("\n", "\r" or "\r\n")-newtype OffsetTable = OffsetTable [Int]+-- Keeps record of offsets of every line break ("\n", "\r" and "\r\n")+--+-- Example text corresponding entry of IntMap +-- >abc\n (1, 4)+-- >def123\r\n (2, 11)+-- >ghi\r (3, 15)+--+newtype ToOffset = ToOffset { unToOffset :: IntMap Int } data Accum = Accum- { accumPreviousChar :: Maybe Char,- accumCurrentOffset :: Int,- accumOffsetTable :: [Int]+ { accumPreviousChar :: Maybe Char+ , accumCurrentOffset :: Int+ , accumCurrentLine :: Int+ , accumResult :: IntMap Int } -initAccum :: Accum-initAccum = Accum Nothing 0 [0]- -- | Return a list of offsets of linebreaks ("\n", "\r" or "\r\n")-makeOffsetTable :: Text -> OffsetTable-makeOffsetTable = OffsetTable . reverse . accumOffsetTable . Text.foldl' go initAccum- where- go :: Accum -> Char -> Accum- go (Accum (Just '\r') n []) '\n' = Accum (Just '\n') (1 + n) [1] -- impossible case- go (Accum (Just '\r') n (m : acc)) '\n' = Accum (Just '\n') (1 + n) (1 + m : acc)- go (Accum previous n acc) '\n' = Accum (Just '\n') (1 + n) (1 + n : acc)- go (Accum previous n acc) '\r' = Accum (Just '\r') (1 + n) (1 + n : acc)- go (Accum previous n acc) char = Accum (Just char) (1 + n) acc+makeToOffset :: Text -> ToOffset+makeToOffset = ToOffset . accumResult . Text.foldl' go initAccum+ where+ initAccum :: Accum+ initAccum = Accum Nothing 0 0 IntMap.empty --- | Zero-based-lookupOffsetTable :: OffsetTable -> Int -> Int -> Int-lookupOffsetTable (OffsetTable offsets) line col = offsets !! line + col+ 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 --- toLSPRange :: Range -> LSP.Range--- toLSPRange range = case rangeToIntervalWithFile range of+-- | (line, col) => offset (zero-based)+toOffset :: ToOffset -> (Int, Int) -> Int+toOffset (ToOffset table) (line, col) = case IntMap.lookup line table of+ Nothing -> col+ Just offset -> offset + col++--------------------------------------------------------------------------------+-- | Offset => Position convertion++-- An IntMap for speeding up Offset => Position convertion+-- Keeps record of offsets of every line break ("\n", "\r" and "\r\n")+--+-- Example text corresponding entry of IntMap +-- >abc\n (4, 1)+-- >def123\r\n (11, 2)+-- >ghi\r (15, 3)+--+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+ 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++-- --------------------------------------------------------------------------------+-- -- | Agda Highlighting Range -> Agda Range++-- fromAgdaHighlightingRangeToLSPRange :: Range -> LSP.Range+-- fromAgdaHighlightingRangeToLSPRange range = case rangeToIntervalWithFile range of -- Nothing -> LSP.Range (LSP.Position (-1) (-1)) (LSP.Position (-1) (-1)) -- Just (Interval start end) -> LSP.Range (toLSPPosition start) (toLSPPosition end)
src/Monad.hs view
@@ -1,36 +1,53 @@-{-# LANGUAGE OverloadedStrings #-}-+{-# LANGUAGE FlexibleContexts #-} module Monad where -import Agda.IR+import Agda.IR -import Agda.Interaction.Base (IOTCM)-import Agda.TypeChecking.Monad (TCMT)-import Control.Concurrent-import Server.ResponseController (ResponseController)-import qualified Server.ResponseController as ResponseController-import Server.CommandController (CommandController)-import qualified Server.CommandController as CommandController-import Control.Monad.Reader-import Data.Text (Text, pack)+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 +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+ -------------------------------------------------------------------------------- data Env = Env- { envLogChan :: Chan Text,- envCommandController :: CommandController,- envResponseChan :: Chan Response,- envResponseController :: ResponseController,- envDevMode :: Bool+ { envOptions :: Options+ , envDevMode :: Bool+ , envConfig :: Config+ , envLogChan :: Chan Text+ , envCommandController :: CommandController+ , envResponseChan :: Chan Response+ , envResponseController :: ResponseController } -createInitEnv :: Bool -> IO Env-createInitEnv devMode =- Env <$> newChan- <*> CommandController.new- <*> newChan- <*> ResponseController.new- <*> pure devMode+createInitEnv :: (MonadIO m, MonadLsp Config m) => Options -> m Env+createInitEnv options =+ Env options (isJust (optViaTCP options))+ <$> getConfig+ <*> liftIO newChan+ <*> liftIO CommandController.new+ <*> liftIO newChan+ <*> liftIO ResponseController.new -------------------------------------------------------------------------------- @@ -76,6 +93,6 @@ -- allow the next Command to be consumed liftIO $ CommandController.release (envCommandController env) +-- | Sends a Response to the client via "envResponseChan" sendResponse :: (Monad m, MonadIO m) => Env -> Response -> TCMT m ()-sendResponse env reaction = do- liftIO $ writeChan (envResponseChan env) reaction+sendResponse env response = liftIO $ writeChan (envResponseChan env) response
+ src/Options.hs view
@@ -0,0 +1,113 @@+{-# 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 )++getOptionsFromArgv :: IO Options+getOptionsFromArgv = do+ -- extract options for Agda from ARGV + (argvForALS, argvForAgda) <- extractAgdaOpts <$> getArgs+ -- parse options for ALS + (opts , _ ) <- parseOpts argvForALS+ -- save options for Agda back+ return $ opts { optRawAgdaOptions = argvForAgda }++usageMessage :: String+usageMessage = usageInfo usage options ++ usageAboutAgdaOptions++--------------------------------------------------------------------------------++-- | Command-line arguments+data Options = Options+ { optViaTCP :: Maybe Int+ , optRawAgdaOptions :: [String]+ , optHelp :: Bool+ }++defaultOptions :: Options+defaultOptions =+ Options { optViaTCP = Nothing, optRawAgdaOptions = [], optHelp = 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 }+ )+ "PORT"+ )+ "talk with the editor via TCP port (4096 as default)"+ ]++usage :: String+usage = "Agda Language Server v0.0.3.0 \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\+ \"++parseOpts :: [String] -> IO (Options, [String])+parseOpts argv = case getOpt Permute options argv of+ (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 ("--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)++-- | Extract Agda options (+AGDA ... -AGDA) from a list of options+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')++--------------------------------------------------------------------------------++newtype Config = Config { configRawAgdaOptions :: [String] }+ deriving (Eq, Show, Generic)++instance FromJSON Config where+ parseJSON (Object v) = Config <$> v .: "commandLineOptions"+ -- We do not expect a non-Object value here.+ -- We could use empty to fail, but typeMismatch+ -- gives a much more informative error message.+ parseJSON invalid =+ prependFailure "parsing Config failed, " (typeMismatch "Object" invalid)++initConfig :: Config+initConfig = Config []
src/Render/Class.hs view
@@ -1,5 +1,5 @@-{-# LANGUAGE OverloadedStrings #-}-+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeSynonymInstances #-} module Render.Class ( Render (..), -- RenderTCM (..),@@ -10,12 +10,16 @@ ) where -import Agda.Syntax.Fixity (Precedence (TopCtx))-import qualified Agda.Syntax.Translation.AbstractToConcrete as Agda-import qualified Agda.TypeChecking.Monad.Base as Agda-import Agda.Utils.Pretty (Doc)+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 Data.Int (Int32)++import Data.Int (Int32)+import GHC.Exts ( IsList(toList) ) import Render.RichText --------------------------------------------------------------------------------@@ -41,12 +45,12 @@ renderP = pure . text . Doc.render . Doc.pretty -- | like 'prettyA'-renderA :: (Render c, Agda.ToConcrete a c) => a -> Agda.TCM Inlines-renderA x = render <$> Agda.abstractToConcrete_ x +renderA :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines+renderA x = render <$> A.abstractToConcrete_ x -- | like 'prettyATop'-renderATop :: (Render c, Agda.ToConcrete a c) => a -> Agda.TCM Inlines-renderATop x = render <$> Agda.abstractToConcreteCtx TopCtx x+renderATop :: (Render c, A.ToConcrete a, A.ConOfAbs a ~ c) => a -> A.TCM Inlines+renderATop x = render <$> A.abstractToConcreteCtx TopCtx x -------------------------------------------------------------------------------- @@ -67,4 +71,9 @@ render = text . Doc.render instance Render a => Render [a] where- render xs = "[" <> fsep (punctuate "," (map render xs)) <> "]"+ render xs = "[" <> fsep (punctuate "," (fmap render xs)) <> "]"+instance Render a => Render (List1 a) where+ render = render . toList++instance Render a => Render (List2 a) where+ render = render . toList
src/Render/Common.hs view
@@ -1,13 +1,26 @@-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}- 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 ((<&>))+ import Render.Class import Render.RichText-import Agda.Utils.Functor ((<&>)) -------------------------------------------------------------------------------- @@ -33,7 +46,7 @@ in if Agda.null o then "@0" else text s- Quantity1 o -> + Quantity1 o -> let s = show o in if Agda.null o then "@1"@@ -79,12 +92,16 @@ -------------------------------------------------------------------------------- -instance (Render p, Render e) => Render (RewriteEqn' qn p e) where+instance (Render p, Render e) => Render (RewriteEqn' qn nm p e) where render = \case- Rewrite es -> prefixedThings (text "rewrite") (render . snd <$> es)- Invert _ pes -> prefixedThings (text "invert") (pes <&> \ (p, e) -> render p <+> "<-" <+> render e)+ Rewrite es -> prefixedThings (text "rewrite") (render . snd <$> toList es)+ Invert _ pes -> prefixedThings (text "invert") (toList pes <&> (\ (p, e) -> render p <+> "<-" <+> render e) . namedThing) prefixedThings :: Inlines -> [Inlines] -> Inlines prefixedThings kw = \case [] -> mempty- (doc : docs) -> fsep $ (kw <+> doc) : map ("|" <+>) docs+ (doc : docs) -> fsep $ (kw <+> doc) : fmap ("|" <+>) docs++instance Render Induction where+ render Inductive = "inductive"+ render CoInductive = "coinductive"
src/Render/Concrete.hs view
@@ -1,21 +1,25 @@ {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiWayIf #-}-{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} 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.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.Utils.Float (toStringWithoutDotZero) import Agda.Utils.Function (applyWhen) import Agda.Utils.Functor (dget, (<&>)) import Agda.Utils.Impossible (__IMPOSSIBLE__)-import Data.Maybe (isNothing, maybeToList)-import qualified Data.Strict.Maybe as Strict+ import Render.Class import Render.Common import Render.Literal ()@@ -28,6 +32,13 @@ 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)+ ]+ -- | OpApp instance Render (OpApp Expr) where render (Ordinary e) = render e@@ -50,7 +61,7 @@ instance Render Expr where render expr = case expr of Ident qname -> render qname- Lit lit -> render lit+ Lit range lit -> render lit -- no hole index, use LinkRange instead QuestionMark range Nothing -> linkRange range "?" QuestionMark _range (Just n) -> linkHole n@@ -58,16 +69,16 @@ -- '_range' is almost always 'NoRange' :( App _range _ _ -> case appView expr of- AppView e1 args -> fsep $ render e1 : map render args- RawApp _ es -> fsep $ map render es+ AppView e1 args -> fsep $ render e1 : fmap render args+ RawApp _ es -> fsep $ fmap render (List2.toList es) OpApp _ q _ es -> fsep $ renderOpApp q es- WithApp _ e es -> fsep $ render e : map ((text' ["delimiter"] "|" <+>) . render) es+ WithApp _ e es -> fsep $ render e : fmap ((text' ["delimiter"] "|" <+>) . render) es HiddenArg _ e -> braces' $ render e InstanceArg _ e -> dbraces $ render e- Lam _ bs (AbsurdLam _ h) -> lambda <+> fsep (map render bs) <+> absurd h- Lam _ bs e -> sep [lambda <+> fsep (map render bs) <+> arrow, render e]+ Lam _ bs (AbsurdLam _ h) -> lambda <+> fsep (fmap render (toList bs)) <+> absurd h+ Lam _ bs e -> sep [lambda <+> fsep (fmap render (toList bs)) <+> arrow, render e] AbsurdLam _ h -> lambda <+> absurd h- ExtendedLam _ pes -> lambda <+> bracesAndSemicolons (map render pes)+ ExtendedLam range _ pes -> lambda <+> bracesAndSemicolons (fmap render (toList pes)) Fun _ e1 e2 -> sep [ renderCohesion e1 (renderQuantity e1 (render e1)) <+> arrow,@@ -75,16 +86,12 @@ ] Pi tel e -> sep- [ render (Tel $ smashTel tel) <+> arrow,+ [ render (Tel $ smashTel (toList tel)) <+> arrow, render e ]- Set range -> linkRange range "Set"- Prop range -> linkRange range "Prop"- SetN range n -> linkRange range $ "Set" <> text (showIndex n)- PropN range n -> linkRange range $ "Prop" <> text (showIndex n) Let _ ds me -> sep- [ "let" <+> vcat (map render ds),+ [ "let" <+> vcat (fmap render (toList ds)), maybe mempty (\e -> "in" <+> render e) me ] Paren _ e -> parens $ render e@@ -92,17 +99,17 @@ case exprs of [] -> emptyIdiomBrkt [e] -> leftIdiomBrkt <+> render e <+> rightIdiomBrkt- e : es -> leftIdiomBrkt <+> render e <+> fsep (map (("|" <+>) . render) es) <+> rightIdiomBrkt- DoBlock _ ss -> "do" <+> vcat (map render ss)+ e : es -> leftIdiomBrkt <+> render e <+> fsep (fmap (("|" <+>) . render) es) <+> rightIdiomBrkt+ DoBlock _ ss -> "do" <+> vcat (fmap render (toList ss)) As _ x e -> render x <> "@" <> render e Dot _ e -> "." <> render e DoubleDot _ e -> ".." <> render e Absurd _ -> "()"- Rec _ xs -> sep ["record", bracesAndSemicolons (map render xs)]+ Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)] RecUpdate _ e xs ->- sep ["record" <+> render e, bracesAndSemicolons (map render xs)]+ sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)] ETel [] -> "()"- ETel tel -> fsep $ map render tel+ ETel tel -> fsep $ fmap render tel Quote _ -> "quote" QuoteTerm _ -> "quoteTerm" Unquote _ -> "unquote"@@ -129,14 +136,13 @@ render (FieldAssignment x e) = sep [render x <+> "=", render e] instance Render ModuleAssignment where- render (ModuleAssignment m es i) = fsep (render m : map render es) <+> render i+ render (ModuleAssignment m es i) = fsep (render m : fmap render es) <+> render i instance Render LamClause where- render (LamClause lhs rhs wh _) =+ render (LamClause lhs rhs _) = sep [ render lhs,- render' rhs,- render wh+ render' rhs ] where render' (RHS e) = arrow <+> render e@@ -193,9 +199,9 @@ -- | TypedBinding instance Render TypedBinding where- render (TLet _ ds) = parens $ "let" <+> vcat (map render ds)+ render (TLet _ ds) = parens $ "let" <+> vcat (fmap render (toList ds)) render (TBind _ xs (Underscore _ Nothing)) =- fsep (map (render . NamedBinding True) xs)+ fsep (fmap (render . NamedBinding True) (toList xs)) render (TBind _ binders e) = fsep [ renderRelevance y $@@ -204,10 +210,10 @@ renderQuantity y $ renderTactic (binderName $ namedArg y) $ sep- [ fsep (map (render . NamedBinding False) ys),+ [ fsep (fmap (render . NamedBinding False) ys), ":" <+> render e ]- | ys@(y : _) <- groupBinds binders+ | ys@(y : _) <- groupBinds (toList binders) ] where groupBinds [] = []@@ -220,8 +226,8 @@ instance Render Tel where render (Tel tel)- | any isMeta tel = forallQ <+> fsep (map render tel)- | otherwise = fsep (map render tel)+ | any isMeta tel = forallQ <+> fsep (fmap render tel)+ | otherwise = fsep (fmap render tel) where isMeta (TBind _ _ (Underscore _ Nothing)) = True isMeta _ = False@@ -232,7 +238,7 @@ : TBind _ ys e' : tel )- | show e == show e' = smashTel (TBind r (xs ++ ys) e : tel)+ | show e == show e' = smashTel (TBind r (fromList (toList xs ++ toList ys)) e : tel) smashTel (b : tel) = b : smashTel tel smashTel [] = [] @@ -242,45 +248,53 @@ instance Render WhereClause where render NoWhere = mempty- render (AnyWhere [Module _ x [] ds])+ render (AnyWhere _range [Module _ x [] ds]) | isNoName (unqualify x) =- vcat ["where", vcat $ map render ds]- render (AnyWhere ds) = vcat ["where", vcat $ map render ds]- render (SomeWhere m a ds) =+ vcat ["where", vcat $ fmap render ds]+ render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds]+ render (SomeWhere _range m a ds) = vcat [ hsep $ applyWhen (a == PrivateAccess UserWritten) ("private" :) ["module", render m, "where"],- vcat $ map render ds+ vcat $ fmap render ds ] instance Render LHS where- render (LHS p eqs es _) =+ render (LHS p eqs es) = sep [ render p,- if null eqs then mempty else fsep $ map render eqs,- prefixedThings "with" (map render es)+ if null eqs then mempty else fsep $ fmap render eqs,+ prefixedThings "with" (fmap renderWithd es) ]+ where+ renderWithd :: WithExpr -> Inlines+ renderWithd (Named nm wh) =+ 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 : map (parens . render) ps+ render (LHSHead f ps) = sep $ render f : fmap (parens . render) ps render (LHSProj d ps lhscore ps') = sep $ render d :- map (parens . render) ps+ fmap (parens . render) ps ++ parens (render lhscore) :- map (parens . render) ps'+ fmap (parens . render) ps' render (LHSWith h wps ps) = if null ps then doc- else sep $ parens doc : map (parens . render) ps+ else sep $ parens doc : fmap (parens . render) ps where- doc = sep $ render h : map (("|" <+>) . render) wps+ doc = sep $ render h : fmap (("|" <+>) . render) wps+ render (LHSEllipsis r p) = "..." instance Render ModuleApplication where- render (SectionApp _ bs e) = fsep (map render bs) <+> "=" <+> render e+ render (SectionApp _ bs e) = fsep (fmap render bs) <+> "=" <+> render e render (RecordModuleInstance _ rec) = "=" <+> render rec <+> "{{...}}" instance Render DoStmt where@@ -288,9 +302,9 @@ fsep [render p <+> "←", render e, prCs cs] where prCs [] = mempty- prCs cs' = fsep ["where", vcat (map render cs')]+ prCs cs' = fsep ["where", vcat (fmap render cs')] render (DoThen e) = render e- render (DoLet _ ds) = "let" <+> vcat (map render ds)+ render (DoLet _ ds) = "let" <+> vcat (fmap render $ toList ds) instance Render Declaration where render d =@@ -318,7 +332,7 @@ Field _ fs -> sep [ "field",- vcat (map render fs)+ vcat (fmap render fs) ] FunClause lhs rhs wh _ -> sep@@ -331,7 +345,7 @@ [ hsep [ "data", render x,- fcat (map render tel)+ fcat (fmap render tel) ], hsep [ ":",@@ -343,48 +357,51 @@ [ hsep [ "data", render x,- fcat (map render tel)+ fcat (fmap render tel) ], hsep [ ":", render e, "where" ],- vcat $ map render cs+ vcat $ fmap render cs ] DataDef _ x tel cs -> sep [ hsep [ "data", render x,- fcat (map render tel)+ fcat (fmap render tel) ], "where",- vcat $ map render cs+ vcat $ fmap render cs ] RecordSig _ x tel e -> sep [ hsep [ "record", render x,- fcat (map render tel)+ fcat (fmap render tel) ], hsep [ ":", render e ] ]- Record _ x ind eta con tel e cs ->- pRecord x ind eta con tel (Just e) cs- RecordDef _ x ind eta con tel cs ->- pRecord x ind eta con tel Nothing cs- Infix f xs -> render f <+> fsep (punctuate "," $ map render xs)+ Record _ x dir tel e cs ->+ pRecord x dir tel (Just e) cs+ RecordDef _ x dir tel cs ->+ pRecord x dir tel Nothing cs+ RecordDirective r -> pRecordDirective r+ Infix f xs -> render f <+> fsep (punctuate "," $ fmap render (toList xs)) Syntax n _ -> "syntax" <+> render n <+> "..." PatternSyn _ n as p ->- "pattern" <+> render n <+> fsep (map render as)+ "pattern" <+> render n <+> fsep (fmap render as) <+> "=" <+> render p Mutual _ ds -> namedBlock "mutual" ds+ InterleavedMutual _ ds -> namedBlock "interleaved mutual" ds+ LoneConstructor _ ds -> namedBlock "constructor" ds Abstract _ ds -> namedBlock "abstract" ds Private _ _ ds -> namedBlock "private" ds InstanceB _ ds -> namedBlock "instance" ds@@ -397,10 +414,10 @@ [ hsep [ "module", render x,- fcat (map render tel),+ fcat (fmap render tel), "where" ],- vcat $ map render ds+ vcat $ fmap render ds ] ModuleMacro _ x (SectionApp _ [] e) DoOpen i | isNoName x ->@@ -411,7 +428,7 @@ ] ModuleMacro _ x (SectionApp _ tel e) open i -> fsep- [ render open <+> "module" <+> render x <+> fcat (map render tel),+ [ render open <+> "module" <+> render x <+> fcat (fmap render tel), "=" <+> render e <+> render i ] ModuleMacro _ x (RecordModuleInstance _ rec) open _ ->@@ -426,39 +443,55 @@ as Nothing = mempty as (Just y) = "as" <+> render (asName y) UnquoteDecl _ xs t ->- fsep ["unquoteDecl" <+> fsep (map render xs) <+> "=", render t]+ fsep ["unquoteDecl" <+> fsep (fmap render xs) <+> "=", render t] UnquoteDef _ xs t ->- fsep ["unquoteDef" <+> fsep (map render xs) <+> "=", render t]+ fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t] Pragma pr -> sep ["{-#" <+> render pr, "#-}"] where namedBlock s ds = fsep [ text s,- vcat $ map render ds+ vcat $ fmap render ds ] +pHasEta0 :: HasEta0 -> Inlines+pHasEta0 = \case+ YesEta -> "eta-equality"+ NoEta () -> "no-eta-equality"++pRecordDirective :: + RecordDirective ->+ Inlines+pRecordDirective = \case+ Induction ind -> render (rangedThing ind)+ Constructor n inst -> hsep [ pInst, "constructor", render n ] where+ pInst = case inst of+ InstanceDef{} -> "instance"+ NotInstanceDef{} -> mempty+ Eta eta -> pHasEta0 (rangedThing eta)+ PatternOrCopattern{} -> "pattern"++ pRecord :: Name ->- Maybe (Ranged Induction) ->- Maybe HasEta ->- Maybe (Name, IsInstance) ->+ RecordDirectives -> [LamBinding] -> Maybe Expr -> [Declaration] -> Inlines-pRecord x ind eta con tel me cs =+pRecord x (RecordDirectives ind eta pat con) tel me cs = sep [ hsep [ "record", render x,- fcat (map render tel)+ fcat (fmap render tel) ], pType me, vcat $ pInd ++ pEta ++ pCon- ++ map render cs+ ++ fmap render cs ] where pType (Just e) =@@ -474,7 +507,7 @@ maybeToList $ eta <&> \case YesEta -> "eta-equality"- NoEta -> "no-eta-equality"+ NoEta _ -> "no-eta-equality" pCon = maybeToList $ (("constructor" <+>) . render) . fst <$> con instance Render OpenShortHand where@@ -482,14 +515,14 @@ render DontOpen = mempty instance Render Pragma where- render (OptionsPragma _ opts) = fsep $ map text $ "OPTIONS" : opts+ render (OptionsPragma _ opts) = fsep $ fmap text $ "OPTIONS" : opts render (BuiltinPragma _ b x) = hsep ["BUILTIN", text (rangedThing b), render x] render (RewritePragma _ _ xs) =- hsep ["REWRITE", hsep $ map render xs]+ hsep ["REWRITE", hsep $ fmap render xs] render (CompilePragma _ b x e) = hsep ["COMPILE", text (rangedThing b), render x, text e] render (ForeignPragma _ b s) =- vcat $ text ("FOREIGN " ++ rangedThing b) : map text (lines s)+ vcat $ text ("FOREIGN " ++ rangedThing b) : fmap text (lines s) render (StaticPragma _ i) = hsep ["STATIC", render i] render (InjectivePragma _ i) =@@ -498,8 +531,8 @@ hsep ["INLINE", render i] render (InlinePragma _ False i) = hsep ["NOINLINE", render i]- render (ImpossiblePragma _) =- hsep ["IMPOSSIBLE"]+ render (ImpossiblePragma _ strs) =+ hsep $ "IMPOSSIBLE" : fmap text strs render (EtaPragma _ x) = hsep ["ETA", render x] render (TerminationCheckPragma _ tc) =@@ -510,13 +543,13 @@ Terminating -> "TERMINATING" TerminationMeasure _ x -> hsep ["MEASURE", render x] render (NoCoverageCheckPragma _) = "NON_COVERING"- render (WarningOnUsage _ nm str) = hsep ["WARNING_ON_USAGE", render nm, text str]- render (WarningOnImport _ str) = hsep ["WARNING_ON_IMPORT", text str]+ render (WarningOnUsage _ nm str) = hsep ["WARNING_ON_USAGE", render nm, text $ T.unpack str]+ render (WarningOnImport _ str) = hsep ["WARNING_ON_IMPORT", text $ T.unpack str] render (CatchallPragma _) = "CATCHALL" render (DisplayPragma _ lhs rhs) = "DISPLAY" <+> fsep [render lhs <+> "=", render rhs] render (NoPositivityCheckPragma _) = "NO_POSITIVITY_CHECK" render (PolarityPragma _ q occs) =- hsep ("POLARITY" : render q : map render occs)+ hsep ("POLARITY" : render q : fmap render occs) render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK" instance Render Fixity where@@ -560,7 +593,7 @@ render = \case IdentP x -> render x AppP p1 p2 -> fsep [render p1, render p2]- RawAppP _ ps -> fsep $ map render ps+ RawAppP _ ps -> fsep $ fmap render (List2.toList ps) OpAppP _ q _ ps -> fsep $ renderOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps) HiddenP _ p -> braces' $ render p InstanceP _ p -> dbraces $ render p@@ -569,16 +602,16 @@ AsP _ x p -> render x <> "@" <> render p DotP _ p -> "." <> render p AbsurdP _ -> "()"- LitP l -> render l+ LitP _ l -> render l QuoteP _ -> "quote"- RecP _ fs -> sep ["record", bracesAndSemicolons (map render fs)]+ RecP _ fs -> sep ["record", bracesAndSemicolons (fmap render fs)] EqualP _ es -> sep $ [parens (sep [render e1, "=", render e2]) | (e1, e2) <- es]- EllipsisP _ -> "..."+ EllipsisP _ mp -> "..." WithP _ p -> "|" <+> render p bracesAndSemicolons :: [Inlines] -> Inlines bracesAndSemicolons [] = "{}"-bracesAndSemicolons (d : ds) = sep (["{" <+> d] ++ map (";" <+>) ds ++ ["}"])+bracesAndSemicolons (d : ds) = sep (["{" <+> d] ++ fmap (";" <+>) ds ++ ["}"]) renderOpApp :: forall a.@@ -589,10 +622,10 @@ renderOpApp q args = merge [] $ prOp moduleNames concreteNames args where -- ms: the module part of the name.- moduleNames = init (qnameParts q)+ moduleNames = List1.init (qnameParts q) -- xs: the concrete name (alternation of @Id@ and @Hole@) concreteNames = case unqualify q of- Name _ _ xs -> xs+ Name _ _ xs -> List1.toList xs NoName {} -> __IMPOSSIBLE__ prOp :: Render a => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]@@ -603,16 +636,16 @@ -- Module qualifier needs to go on section holes (#3072) prOp _ (Hole : _) [] = __IMPOSSIBLE__ prOp ms (Id x : xs) es =- ( qual ms $ render $ Name noRange InScope [Id x],+ ( 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+ prOp _ [] es = fmap (\e -> (render e, Nothing)) es - qual ms' doc = hcat $ punctuate "." $ map render ms' ++ [doc]+ qual ms' doc = hcat $ punctuate "." $ fmap render ms' ++ [doc] -- Section underscores should be printed without surrounding -- whitespace. This function takes care of that.@@ -648,19 +681,19 @@ public Nothing = mempty renderHiding' [] = mempty- renderHiding' xs = "hiding" <+> parens (fsep $ punctuate ";" $ map render xs)+ renderHiding' xs = "hiding" <+> parens (fsep $ punctuate ";" $ fmap render xs) rename [] = mempty rename xs = hsep [ "renaming",- parens $ fsep $ punctuate ";" $ map render xs+ parens $ fsep $ punctuate ";" $ fmap render xs ] instance (Render a, Render b) => Render (Using' a b) where render UseEverything = mempty render (Using xs) =- "using" <+> parens (fsep $ punctuate ";" $ map render xs)+ "using" <+> parens (fsep $ punctuate ";" $ fmap render xs) instance (Render a, Render b) => Render (Renaming' a b) where render (Renaming from to mfx _r) =
src/Render/Interaction.hs view
@@ -1,38 +1,47 @@-{-# LANGUAGE OverloadedStrings #-}- module Render.Interaction where -import Agda.Interaction.Base-import Agda.TypeChecking.Monad-import Render.Class-import Render.Name ()-import Render.Position ()-import Render.RichText-import Render.TypeChecking ()+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 ( )+ -------------------------------------------------------------------------------- -- | OutputForm+ instance (Render a, Render b) => Render (OutputForm a b) where- render (OutputForm r pids c) = fsep [render c, prange r, prPids pids]- where- prPids [] = mempty- prPids [pid] = parens $ "problem" <+> render pid- prPids pids' = parens $ "problems" <+> fsep (punctuate "," $ map render pids')- prange rr- | null s = mempty- | otherwise = text $ " [ at " ++ s ++ " ]"- where- s = show $ render rr+ 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 = ","++ 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+ -- | 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 (OfType name expr) = render name <> " : " <> render expr+ render (JustType name ) = "Type " <> render name+ render (JustSort name ) = "Sort " <> render name render (CmpInType cmp expr name1 name2) = render name1 <> " "@@ -50,75 +59,51 @@ <> " : " <> render expr render (CmpTypes cmp name1 name2) =- render name1- <> " "- <> render cmp- <> " "- <> render name2+ render name1 <> " " <> render cmp <> " " <> render name2 render (CmpLevels cmp name1 name2) =- render name1- <> " "- <> render cmp- <> " "- <> render name2+ render name1 <> " " <> render cmp <> " " <> render name2 render (CmpTeles cmp name1 name2) =- render name1- <> " "- <> render cmp- <> " "- <> render name2+ render name1 <> " " <> render cmp <> " " <> render name2 render (CmpSorts cmp name1 name2) =- render name1- <> " "- <> render cmp- <> " "- <> render name2- render (Guard x (ProblemId pid)) =- fsep- [ render x- <> parens ("blocked by problem " <> render pid)- ]- render (Assign name expr) =- render name <> " := " <> render expr+ render name1 <> " " <> render cmp <> " " <> render name2+ render (Assign name expr) = render name <> " := " <> render expr render (TypedAssign name expr1 expr2) = render name <> " := " <> render expr1 <> " :? " <> render expr2 render (PostponedCheckArgs name exprs expr1 expr2) =- let exprs' = map (parens . render) exprs- in render name <> " := "+ let exprs' = fmap (parens . render) exprs+ in render name+ <> " := " <> parens ("_ : " <> render expr1) <> " " <> fsep exprs' <> " : " <> render expr2- render (IsEmptyType expr) =- "Is empty: " <> render expr- render (SizeLtSat expr) =- "Not empty type of sizes: " <> render expr+ render (IsEmptyType expr) = "Is empty: " <> render expr+ render (SizeLtSat expr) = "Not empty type of sizes: " <> render expr render (FindInstanceOF name expr exprs) =- let exprs' = map (\(e, t) -> render e <> " : " <> render t) exprs- in fsep- [ "Resolve instance argument ",- render name <> " : " <> render expr,- "Candidate:",- vcat 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' ] render (PTSInstance name1 name2) =- "PTS instance for ("- <> render name1- <> ", "- <> render name2- <> ")"- render (PostponedCheckFunDef name expr) =- "Check definition of "- <> render name- <> " : "- <> render expr+ "PTS instance for (" <> render name1 <> ", " <> render name2 <> ")"+ render (PostponedCheckFunDef name expr _err) =+ "Check definition of " <> render name <> " : " <> render expr+ render (CheckLock t lk) =+ "Check lock" <+> render lk <+> "allows" <+> render t+ render (UsableAtMod modality t) =+ "Is usable at" <+> render modality <+> render t -- | IPBoundary' instance Render c => Render (IPBoundary' c) where render (IPBoundary eqs val meta over) = do- let xs = map (\(l, r) -> render l <+> "=" <+> render r) eqs+ let xs = fmap (\(l, r) -> render l <+> "=" <+> render r) eqs rhs = case over of- Overapplied -> "=" <+> render meta+ Overapplied -> "=" <+> render meta NotOverapplied -> mempty fsep (punctuate "," xs) <+> "⊢" <+> render val <+> rhs
src/Render/Internal.hs view
@@ -1,5 +1,4 @@ {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE OverloadedStrings #-} module Render.Internal where @@ -10,6 +9,7 @@ import Render.Common (renderHiding) import Render.Concrete () import Render.RichText+import qualified Data.Set as Set -------------------------------------------------------------------------------- @@ -58,7 +58,7 @@ where pApp d els = mparens (not (null els) && p > 9) $- fsep [d, fsep (map (renderPrec 10) els)]+ fsep [d, fsep (fmap (renderPrec 10) els)] instance (Render t, Render e) => Render (Dom' t e) where render dom = pTac <+> renderDom dom (render $ unDom dom)@@ -79,7 +79,7 @@ sep [ render tel <+> "|-", fsep- [ fsep (map (renderPrec 10) ps) <+> "=",+ [ fsep (fmap (renderPrec 10) ps) <+> "=", pBody body ty ] ]@@ -106,20 +106,21 @@ _ -> mparens (p > 9) $ List.foldr1 (\a b -> "lub" <+> a <+> b) $- [renderN | n > 0] ++ map (renderPrec 10) as+ [renderN | n > 0] ++ fmap (renderPrec 10) as where renderN = renderPrecLevelSucs p n (const "lzero") instance Render PlusLevel where renderPrec p (Plus n a) = renderPrecLevelSucs p n $ \p' -> renderPrec p' a -instance Render LevelAtom where- renderPrec p a =- case a of- MetaLevel x els -> renderPrec p (MetaV x els)- BlockedLevel _ v -> renderPrec p v- NeutralLevel _ v -> renderPrec p v- UnreducedLevel v -> renderPrec p v+--instance Render LevelAtom where+-- LevelAtom is just Term+-- renderPrec p a =+-- case a of+-- MetaLevel x els -> renderPrec p (MetaV x els)+-- BlockedLevel _ v -> renderPrec p v+-- NeutralLevel _ v -> renderPrec p v+-- UnreducedLevel v -> renderPrec p v instance Render Sort where renderPrec p srt =@@ -130,15 +131,20 @@ Prop (ClosedLevel 0) -> "Prop" Prop (ClosedLevel n) -> text $ "Prop" ++ show n Prop l -> mparens (p > 9) $ "Prop" <+> renderPrec 10 l- Inf -> "Setω"+ 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"- PiSort a b ->+ LockUniv -> "LockUniv"+ PiSort a _s1 s2 -> mparens (p > 9) $- "piSort" <+> renderDom (domInfo a) (text (absName b) <+> ":" <+> render (unDom a))+ "piSort" <+> renderDom (domInfo a) (text (absName s2) <+> ":" <+> render (unDom a)) <+> parens ( fsep- [ text ("λ " ++ absName b ++ " ->"),- render (unAbs b)+ [ text ("λ " ++ absName s2 ++ " ->"),+ render (unAbs s2) ] ) FunSort a b ->@@ -165,23 +171,32 @@ renderPrec _ (DotP _o t) = "." <> renderPrec 10 t renderPrec n (ConP c i nps) = mparens (n > 0 && not (null nps)) $- (lazy <> render (conName c)) <+> fsep (map (renderPrec 10) ps)+ (lazy <> render (conName c)) <+> fsep (fmap (renderPrec 10) ps) where- ps = map (fmap namedThing) nps+ ps = fmap (fmap namedThing) nps lazy | conPLazy i = "~" | otherwise = mempty renderPrec n (DefP _ q nps) = mparens (n > 0 && not (null nps)) $- render q <+> fsep (map (renderPrec 10) ps)+ render q <+> fsep (fmap (renderPrec 10) ps) where- ps = map (fmap namedThing) nps+ ps = fmap (fmap namedThing) nps -- -- Version with printing record type: -- renderPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $- -- text (show $ conName c) <+> fsep (map (render . namedArg) ps)+ -- text (show $ conName c) <+> fsep (fmap (render . namedArg) ps) -- where -- b = maybe False (== ConOSystem) $ conPRecord i -- prTy d = caseMaybe (conPType i) d $ \ t -> d <+> ":" <+> render t renderPrec _ (LitP _ l) = render l renderPrec _ (ProjP _o q) = "." <> render q renderPrec n (IApplyP _o _ _ x) = renderPrec n x++--------------------------------------------------------------------------------+-- 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 (UnblockOnProblem pid) = "problem" <+> render pid
src/Render/Literal.hs view
@@ -1,8 +1,6 @@-{-# LANGUAGE OverloadedStrings #-}- module Render.Literal where -import Agda.Syntax.Literal+import Agda.Syntax.Literal ( Literal(..), showChar', showText ) import Render.Class import Render.RichText import Render.Name ()@@ -12,10 +10,10 @@ -- | Literal instance Render Literal where- render (LitNat _ n) = text $ show n- render (LitWord64 _ n) = text $ show n- render (LitFloat _ d) = text $ show d- render (LitString _ s) = text $ showString' s ""- render (LitChar _ c) = text $ "'" ++ showChar' c "'"- render (LitQName _ x) = render x- render (LitMeta _ _ x) = render x+ render (LitNat n) = text $ show n+ render (LitWord64 n) = text $ show n+ render (LitFloat d) = text $ show d+ render (LitString s) = text $ showText s ""+ render (LitChar c) = text $ "'" ++ showChar' c "'"+ render (LitQName x) = render x+ render (LitMeta _ x) = render x
src/Render/Name.hs view
@@ -1,14 +1,13 @@-{-# LANGUAGE OverloadedStrings #-}- module Render.Name where import qualified Agda.Syntax.Abstract as A import qualified Agda.Syntax.Concrete as C+import qualified Agda.Syntax.Common as C+import qualified Agda.Utils.List1 as Agda+ import Render.Class import Render.RichText-import qualified Agda.Syntax.Common as C - -------------------------------------------------------------------------------- -- | Concrete @@ -18,7 +17,7 @@ -- glueing name parts together instance Render C.Name where- render (C.Name range _inScope xs) = linkRange range $ mconcat (map render xs)+ render (C.Name range _inScope xs) = linkRange range $ mconcat (fmap render $ Agda.toList xs) render (C.NoName _ _) = "_" instance Render C.QName where@@ -35,4 +34,4 @@ render = render . A.nameConcrete instance Render A.QName where- render = hcat . punctuate "." . map render . A.qnameToList+ render = hcat . punctuate "." . fmap render . Agda.toList . A.qnameToList
src/Render/Position.hs view
@@ -1,5 +1,4 @@ {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE OverloadedStrings #-} module Render.Position where
src/Render/RichText.hs view
@@ -1,6 +1,5 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE OverloadedStrings #-} module Render.RichText ( Block(..),@@ -38,21 +37,22 @@ ) where -import qualified Agda.Interaction.Options.IORefs 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 (subscriptAllowed, toSubscriptDigit)-import Data.Aeson (ToJSON (toJSON), Value (Null))-import Data.Foldable (toList)-import Data.IORef (readIORef)-import Data.Sequence (Seq (..))-import qualified Data.Sequence as Seq+-- 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 Data.Strict.Maybe as Strict-import Data.String (IsString (..))-import GHC.Generics (Generic)-import qualified GHC.IO.Unsafe as UNSAFE +import GHC.Generics (Generic)+ -------------------------------------------------------------------------------- -- | Block elements @@ -186,8 +186,8 @@ -------------------------------------------------------------------------------- --- | ToJSON instances for Agda types-instance ToJSON Agda.Range+-- | ToJSON instances for A.types+instance {-# OVERLAPS #-} ToJSON Agda.Range instance ToJSON (Agda.Interval' ()) where toJSON (Agda.Interval start end) = toJSON (start, end)@@ -195,7 +195,7 @@ instance ToJSON (Agda.Position' ()) where toJSON (Agda.Pn () pos line col) = toJSON [line, col, pos] -instance ToJSON Agda.SrcFile where+instance {-# OVERLAPS #-} ToJSON Agda.SrcFile where toJSON Strict.Nothing = Null toJSON (Strict.Just path) = toJSON path @@ -287,12 +287,10 @@ -- | Shows a non-negative integer using the characters ₀-₉ instead of -- 0-9 unless the user explicitly asked us to not use any unicode characters. showIndex :: (Show i, Integral i) => i -> String-showIndex = case subscriptAllowed of- Agda.UnicodeOk -> map toSubscriptDigit . show- Agda.AsciiOnly -> show+showIndex = map toSubscriptDigit . show ---------------------------------------------------------------------------------+-- -- | Picking the appropriate set of special characters depending on -- whether we are allowed to use unicode or have to limit ourselves -- to ascii.@@ -309,25 +307,12 @@ {-# NOINLINE specialCharacters #-} specialCharacters :: SpecialCharacters specialCharacters =- let opt = UNSAFE.unsafePerformIO (readIORef Agda.unicodeOrAscii)- in case opt of- Agda.UnicodeOk ->- SpecialCharacters- { _dbraces = ("\x2983 " <>) . (<> " \x2984"),- _lambda = "\x03bb",- _arrow = "\x2192",- _forallQ = "\x2200",- _leftIdiomBrkt = "\x2987",- _rightIdiomBrkt = "\x2988",- _emptyIdiomBrkt = "\x2987\x2988"- }- Agda.AsciiOnly ->- SpecialCharacters- { _dbraces = braces . braces',- _lambda = "\\",- _arrow = "->",- _forallQ = "forall",- _leftIdiomBrkt = "(|",- _rightIdiomBrkt = "|)",- _emptyIdiomBrkt = "(|)"- }+ SpecialCharacters+ { _dbraces = ("\x2983 " <>) . (<> " \x2984"),+ _lambda = "\x03bb",+ _arrow = "\x2192",+ _forallQ = "\x2200",+ _leftIdiomBrkt = "\x2987",+ _rightIdiomBrkt = "\x2988",+ _emptyIdiomBrkt = "\x2987\x2988"+ }
src/Render/TypeChecking.hs view
@@ -1,6 +1,3 @@-{-# LANGUAGE LambdaCase #-}-{-# LANGUAGE OverloadedStrings #-}- module Render.TypeChecking where import Agda.Syntax.Common
src/Render/Utils.hs view
@@ -1,9 +1,11 @@ module Render.Utils where +import Agda.Utils.Time ( CPUTime )+import Agda.Utils.Pretty (pretty)+ import Render.Class import Render.RichText-import Agda.Utils.Time-import Agda.Utils.Pretty (pretty)+ instance Render CPUTime where render = text . show . pretty
src/Server.hs view
@@ -1,136 +1,111 @@ {-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE OverloadedStrings #-} -module Server (run) where- -- entry point of the LSP server -import Monad-import Control.Monad.Reader+module Server+ ( run+ ) where+ import qualified Agda-import Data.Aeson (FromJSON, ToJSON)-import qualified Data.Aeson as JSON-import Data.Text (pack)-import GHC.Generics (Generic)-import GHC.IO.IOMode (IOMode (ReadWriteMode))-import Language.LSP.Server-import Language.LSP.Types hiding (TextDocumentSyncClientCapabilities (..))-import qualified Network.Simple.TCP as TCP-import Network.Socket (socketToHandle)+import Control.Concurrent ( writeChan )+import Control.Monad.Reader ( MonadIO(liftIO)+ , void+ )+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 qualified Switchboard-import Switchboard (Switchboard)-import Control.Concurrent+import Switchboard ( Switchboard ) -import Agda.Misc (onHover)-import Data.Maybe (isJust)+import qualified Server.Handler as Handler +import qualified Language.LSP.Server as LSP+import Options++ -------------------------------------------------------------------------------- -run :: Maybe Int -> IO Int-run viaTCP = do- env <- createInitEnv (isJust viaTCP)- switchboard <- Switchboard.new env- case viaTCP of - Just port -> do - 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 handle handle (serverDefn env switchboard)- return ()- Switchboard.destroy switchboard+run :: Options -> IO Int+run options = do+ case optViaTCP options of+ Just port -> do+ 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 handle handle (serverDefn options)+ return ()+ -- Switchboard.destroy switchboard return 0- Nothing -> do - runServer (serverDefn env switchboard)- where- serverDefn :: Env -> Switchboard -> ServerDefinition ()- serverDefn env switchboard =- ServerDefinition- { onConfigurationChange = const $ pure $ Right (),- doInitialize = \ctxEnv _req -> do- Switchboard.setupLanguageContextEnv switchboard ctxEnv- pure $ Right ctxEnv,- staticHandlers = handlers,- interpretHandler = \ctxEnv -> Iso (runLspT ctxEnv . runServerM env) liftIO,- options = lspOptions- }- lspOptions :: Options- lspOptions =- defaultOptions- { textDocumentSync = Just syncOptions- }+ Nothing -> do+ 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+ } - -- 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- }+ lspOptions :: LSP.Options+ lspOptions = defaultOptions { textDocumentSync = Just syncOptions } - changeOptions :: TextDocumentSyncKind- changeOptions = TdSyncIncremental+ -- 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+ } - -- includes the document content on save, so that we don't have to read it from the disk- saveOptions :: SaveOptions- saveOptions = SaveOptions (Just True)+ changeOptions :: TextDocumentSyncKind+ changeOptions = TdSyncIncremental + -- includes the document content on save, so that we don't have to read it from the disk+ saveOptions :: SaveOptions+ saveOptions = SaveOptions (Just True)+ -- handlers of the LSP server-handlers :: Handlers (ServerM (LspM ()))+handlers :: Handlers (ServerM (LspM Config)) handlers = mconcat- [ -- custom methods, not part of LSP- requestHandler (SCustomMethod "agda") $ \req responder -> do- let RequestMessage _ _i _ params = req- -- JSON Value => Request => Response- response <- case JSON.fromJSON params of- JSON.Error msg -> return $ CmdRes $ Just $ CmdErrCannotDecodeJSON $ show msg ++ "\n" ++ show params- JSON.Success request -> handleCommandReq request- -- respond with the Response- responder $ Right $ JSON.toJSON response,+ [ -- 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 <- onHover uri pos- responder $ Right result- ]------------------------------------------------------------------------------------handleCommandReq :: CommandReq -> ServerM (LspM ()) CommandRes-handleCommandReq CmdReqSYN = return $ CmdResACK Agda.getAgdaVersion-handleCommandReq (CmdReq cmd) = do- case Agda.parseIOTCM cmd of- Left err -> do- writeLog $ "[Error] CmdErrCannotParseCommand:\n" <> pack err- return $ CmdRes (Just (CmdErrCannotParseCommand err))- Right iotcm -> do- writeLog $ "[Request] " <> pack (show cmd)- provideCommand iotcm- return $ CmdRes Nothing------------------------------------------------------------------------------------data CommandReq- = CmdReqSYN -- ^ Client initiates a 2-way handshake- | CmdReq String- deriving (Generic)--instance FromJSON CommandReq--data CommandRes- = CmdResACK -- ^ Server complets the 2-way handshake- String -- ^ Version number of Agda- | CmdRes -- ^ The response for 'CmdReq'- (Maybe CommandErr) -- ^ 'Nothing' to indicate success- deriving (Generic)--instance ToJSON CommandRes--data CommandErr- = CmdErrCannotDecodeJSON String- | CmdErrCannotParseCommand String- deriving (Generic)+ 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+ ] -instance ToJSON CommandErr
+ src/Server/Handler.hs view
@@ -0,0 +1,155 @@+module Server.Handler where++import Agda ( getCommandLineOptions+ , runAgda+ )+import qualified Agda.IR as IR+import Agda.Interaction.Base ( CommandM+ , CommandQueue(..)+ , CommandState(optionsOnReload)+ , Rewrite(AsIs)+ , initCommandState+ )+import Agda.Interaction.BasicOps ( atTopLevel+ , typeInCurrent+ )+import Agda.Interaction.Highlighting.Precise+ ( HighlightingInfo )+import qualified Agda.Interaction.Imports as Imp+import Agda.Interaction.InteractionTop+ ( cmd_load'+ , localStateCommandM+ )+import Agda.Interaction.Options ( CommandLineOptions+ ( optAbsoluteIncludePaths+ )+ )+import qualified Agda.Parser as Parser+import Agda.Position ( makeToOffset+ , toAgdaPositionWithoutFile+ )+import Agda.Syntax.Abstract.Pretty ( prettyATop )+import Agda.Syntax.Parser ( exprParser+ , parse+ )+import Agda.Syntax.Translation.ConcreteToAbstract+ ( concreteToAbstract_ )+import Agda.TypeChecking.Monad ( HasOptions(commandLineOptions)+ , setInteractionOutputCallback+ )+import Agda.TypeChecking.Warnings ( runPM )+import Agda.Utils.Pretty ( render )+import Control.Concurrent.STM+import Control.Monad.Reader+import Control.Monad.State+import Data.Text ( Text+ , pack+ , unpack+ )+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.VFS as VFS+import Monad+import Options ( Config+ , Options(optRawAgdaOptions)+ )++initialiseCommandQueue :: IO CommandQueue+initialiseCommandQueue = CommandQueue <$> newTChanIO <*> newTVarIO Nothing++runCommandM :: CommandM a -> ServerM (LspM Config) (Either String a)+runCommandM program = do+ env <- ask+ runAgda $ do+ -- get command line options + options <- getCommandLineOptions++ -- we need to set InteractionOutputCallback else it would panic+ lift $ setInteractionOutputCallback $ \_response -> return ()++ -- setup the command state+ commandQueue <- liftIO initialiseCommandQueue+ let commandState = (initCommandState commandQueue)+ { optionsOnReload = options { optAbsoluteIncludePaths = [] }+ }++ lift $ evalStateT program commandState++inferTypeOfText+ :: FilePath -> Text -> ServerM (LspM Config) (Either String String)+inferTypeOfText filepath text = runCommandM $ do+ -- load first+ cmd_load' filepath [] True Imp.TypeCheck $ \_ -> return ()+ -- infer later+ let norm = AsIs+ -- localStateCommandM: restore TC state afterwards, do we need this here?+ typ <- localStateCommandM $ do+ e <- 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 uri pos = do+ result <- LSP.getVirtualFile (LSP.toNormalizedUri uri)+ case result of+ Nothing -> return Nothing+ 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+ Just (_token, text) -> do+ case LSP.uriToFilePath uri of+ Nothing -> return Nothing+ 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)+ Right typeString -> do+ let content = LSP.HoverContents $ LSP.markedUpContent+ "agda-language-server"+ (pack typeString)+ return $ Just $ LSP.Hover content (Just range)++--------------------------------------------------------------------------------+-- 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 []++-- HighlightingInfo+-- Int -- starting offset+-- Int -- ending offset+-- [String] -- list of names of aspects+-- Bool -- is token based?+-- String -- note+-- (Maybe (FilePath, Int)) -- the defining module of the token and its position in that module++-- toToken+-- :: Ranged a+-- => J.SemanticTokenTypes+-- -> [J.SemanticTokenModifiers]+-- -> a+-- -> [J.SemanticTokenAbsolute]+-- toToken types modifiers x =+-- let range = rangeOf x+-- in [ J.SemanticTokenAbsolute (posLine (rangeStart range) - 1)+-- (posCol (rangeStart range) - 1)+-- (rangeSpan range)+-- types+-- modifiers+-- ]
src/Server/ResponseController.hs view
@@ -1,20 +1,29 @@ -- | -- Makes sure that all dispatched works are done. -- Notify when all dispatched works are done.-module Server.ResponseController where+module Server.ResponseController+ ( 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"@@ -22,11 +31,7 @@ -- | Constructs a new ResponseController new :: IO ResponseController-new =- ResponseController- <$> newIORef 0- <*> newIORef 0- <*> newSizedChan+new = ResponseController <$> newIORef 0 <*> newIORef 0 <*> newSizedChan -- | Returns a callback, invoked the callback to signal completion. -- This function and the returned callback are both non-blocking.@@ -42,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)@@ -57,7 +62,7 @@ setCheckpoint :: ResponseController -> (() -> IO ()) -> IO () setCheckpoint controller callback = do dispatched <- readIORef (dispatchedCount controller)- completed <- readIORef (completedCount controller)+ completed <- readIORef (completedCount controller) -- see if the previously dispatched works have been completed if dispatched == completed then callback ()
src/Switchboard.hs view
@@ -1,5 +1,3 @@-{-# LANGUAGE OverloadedStrings #-}- module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy) where import Monad@@ -12,12 +10,13 @@ import Language.LSP.Server import Language.LSP.Types hiding (TextDocumentSyncClientCapabilities (..)) import Data.IORef+import Options (Config) data Switchboard = Switchboard { sbPrintLog :: ThreadId , sbSendResponse :: ThreadId , sbRunAgda :: ThreadId- , sbLanguageContextEnv :: IORef (Maybe (LanguageContextEnv ()))+ , sbLanguageContextEnv :: IORef (Maybe (LanguageContextEnv Config)) } -- | All channels go in and out from here@@ -27,11 +26,11 @@ Switchboard <$> forkIO (keepPrintingLog env) <*> forkIO (keepSendindResponse env ctxEnvIORef)- <*> forkIO (runReaderT Agda.interact env)+ <*> forkIO (runReaderT Agda.start env) <*> pure ctxEnvIORef -- | For sending reactions to the client -setupLanguageContextEnv :: Switchboard -> LanguageContextEnv () -> IO ()+setupLanguageContextEnv :: Switchboard -> LanguageContextEnv Config -> IO () setupLanguageContextEnv switchboard ctxEnv = do writeIORef (sbLanguageContextEnv switchboard) (Just ctxEnv) @@ -52,7 +51,7 @@ -- | Keep sending reactions -- Consumer of `envResponseChan`-keepSendindResponse :: Env -> IORef (Maybe (LanguageContextEnv ())) -> IO ()+keepSendindResponse :: Env -> IORef (Maybe (LanguageContextEnv Config)) -> IO () keepSendindResponse env ctxEnvIORef = forever $ do response <- readChan (envResponseChan env)
+ stack.yaml view
@@ -0,0 +1,42 @@+resolver: lts-18.5+# Allow a newer minor version of GHC than the snapshot specifies+compiler-check: match-exact++# User packages to be built.+# Various formats can be used as shown in the example below.+#+# packages:+# - some-directory+# - https://example.com/foo/bar/baz-0.0.2.tar.gz+# subdirs:+# - auto-update+# - wai+packages:+- .++extra-deps:+ # LSP+ - lexer-applicative-2.1.0.2+ - github: haskell/lsp+ commit: dce30c9d345f63921cf9cf5045e1dcd753e4fe34+ subdirs: + - lsp+ - github: haskell/lsp+ commit: dce30c9d345f63921cf9cf5045e1dcd753e4fe34+ subdirs: + - lsp-types+ # - some-1.0.1@sha256:26e5bab7276f48b25ea8660d3fd1166c0f20fd497dac879a40f408e23211f93e,2055+ - dependent-map-0.4.0.0@sha256:ca2b131046f4340a1c35d138c5a003fe4a5be96b14efc26291ed35fd08c62221,1657+ - dependent-sum-0.7.1.0@sha256:0e419237f5b86da3659772afff9cab355c0f8d5b3fdb15a5b30e673d8dc83941,2147+ - dependent-sum-template-0.1.0.3@sha256:0bbbacdfbd3abf2a15aaf0cf2c27e5bdd159b519441fec39e1e6f2f54424adde,1682+ - unliftio-core-0.2.0.1@sha256:9b3e44ea9aacacbfc35b3b54015af450091916ac3618a41868ebf6546977659a,1082+ - constraints-extras-0.3.1.0@sha256:12016ebb91ad5ed2c82bf7e48c6bd6947d164d33c9dca5ac3965de1bb6c780c0,1777+ - constraints-0.12@sha256:71c7999d7fa01d8941f08d37d4c107c6b1bcbd0306e234157557b9b096b7f1be,2217+++++flags:+ Agda:+ # optimise-heavily: true+ enable-cluster-counting: true
− test/Spec.hs
@@ -1,2 +0,0 @@-main :: IO ()-main = putStrLn "Test suite not yet implemented"
+ test/Test.hs view
@@ -0,0 +1,11 @@+import qualified Test.SrcLoc as SrcLoc+import Test.Tasty ( TestTree+ , defaultMain+ , testGroup+ )++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests = testGroup "Tests" [SrcLoc.tests]
+ test/Test/SrcLoc.hs view
@@ -0,0 +1,56 @@+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++tests :: TestTree+tests = testGroup "Source Location" [positionToOffsetTests, offsetToPositionTests]++--------------------------------------------------------------------------------++positionToOffsetTests :: TestTree+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]+ ]+ where+ text :: Text + text = "012\n456\r\n90\r23"++ table :: ToOffset+ table = makeToOffset text++ 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)]+ ]+ where+ text :: Text + text = "012\n456\r\n90\r23"++ table :: FromOffset+ table = makeFromOffset text++ run :: [Int] -> [(Int, Int)]+ run = map (fromOffset table)+