diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 + diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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". - -![截圖 2021-03-03 下午6 53 11](https://user-images.githubusercontent.com/797844/109795292-b709cc80-7c51-11eb-909d-982f647bd282.png) - -## Current features - -More stuff are clickable in the panel after loading (C-c C-l) - -![截圖 2021-03-03 下午6 59 43](https://user-images.githubusercontent.com/797844/109796026-a017aa00-7c52-11eb-9e03-d21bca12e603.png) - ## Why make it standalone? diff --git a/agda-language-server.cabal b/agda-language-server.cabal --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -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 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 diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -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 diff --git a/package.yaml b/package.yaml new file mode 100644 --- /dev/null +++ b/package.yaml @@ -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 + +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 diff --git a/src/Agda.hs b/src/Agda.hs --- a/src/Agda.hs +++ b/src/Agda.hs @@ -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 diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs --- a/src/Agda/Convert.hs +++ b/src/Agda/Convert.hs @@ -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 = diff --git a/src/Agda/IR.hs b/src/Agda/IR.hs --- a/src/Agda/IR.hs +++ b/src/Agda/IR.hs @@ -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) diff --git a/src/Agda/Misc.hs b/src/Agda/Misc.hs deleted file mode 100644 --- a/src/Agda/Misc.hs +++ /dev/null @@ -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) diff --git a/src/Agda/Parser.hs b/src/Agda/Parser.hs --- a/src/Agda/Parser.hs +++ b/src/Agda/Parser.hs @@ -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 diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs --- a/src/Agda/Position.hs +++ b/src/Agda/Position.hs @@ -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) diff --git a/src/Monad.hs b/src/Monad.hs --- a/src/Monad.hs +++ b/src/Monad.hs @@ -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 diff --git a/src/Options.hs b/src/Options.hs new file mode 100644 --- /dev/null +++ b/src/Options.hs @@ -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 [] diff --git a/src/Render/Class.hs b/src/Render/Class.hs --- a/src/Render/Class.hs +++ b/src/Render/Class.hs @@ -1,5 +1,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 diff --git a/src/Render/Common.hs b/src/Render/Common.hs --- a/src/Render/Common.hs +++ b/src/Render/Common.hs @@ -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" diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs --- a/src/Render/Concrete.hs +++ b/src/Render/Concrete.hs @@ -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) = diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs --- a/src/Render/Interaction.hs +++ b/src/Render/Interaction.hs @@ -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 diff --git a/src/Render/Internal.hs b/src/Render/Internal.hs --- a/src/Render/Internal.hs +++ b/src/Render/Internal.hs @@ -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 diff --git a/src/Render/Literal.hs b/src/Render/Literal.hs --- a/src/Render/Literal.hs +++ b/src/Render/Literal.hs @@ -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 diff --git a/src/Render/Name.hs b/src/Render/Name.hs --- a/src/Render/Name.hs +++ b/src/Render/Name.hs @@ -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 diff --git a/src/Render/Position.hs b/src/Render/Position.hs --- a/src/Render/Position.hs +++ b/src/Render/Position.hs @@ -1,5 +1,4 @@ {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE OverloadedStrings #-} module Render.Position where diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs --- a/src/Render/RichText.hs +++ b/src/Render/RichText.hs @@ -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" + } diff --git a/src/Render/TypeChecking.hs b/src/Render/TypeChecking.hs --- a/src/Render/TypeChecking.hs +++ b/src/Render/TypeChecking.hs @@ -1,6 +1,3 @@ -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE OverloadedStrings #-} - module Render.TypeChecking where import Agda.Syntax.Common diff --git a/src/Render/Utils.hs b/src/Render/Utils.hs --- a/src/Render/Utils.hs +++ b/src/Render/Utils.hs @@ -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 diff --git a/src/Server.hs b/src/Server.hs --- a/src/Server.hs +++ b/src/Server.hs @@ -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 diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs new file mode 100644 --- /dev/null +++ b/src/Server/Handler.hs @@ -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 +-- ] diff --git a/src/Server/ResponseController.hs b/src/Server/ResponseController.hs --- a/src/Server/ResponseController.hs +++ b/src/Server/ResponseController.hs @@ -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 () diff --git a/src/Switchboard.hs b/src/Switchboard.hs --- a/src/Switchboard.hs +++ b/src/Switchboard.hs @@ -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) diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -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 diff --git a/test/Spec.hs b/test/Spec.hs deleted file mode 100644 --- a/test/Spec.hs +++ /dev/null @@ -1,2 +0,0 @@ -main :: IO () -main = putStrLn "Test suite not yet implemented" diff --git a/test/Test.hs b/test/Test.hs new file mode 100644 --- /dev/null +++ b/test/Test.hs @@ -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] diff --git a/test/Test/SrcLoc.hs b/test/Test/SrcLoc.hs new file mode 100644 --- /dev/null +++ b/test/Test/SrcLoc.hs @@ -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) +