diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2017 - 2020 Luā Tîng-Giān
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,55 @@
+# 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
+```
+
+Checkout to a version that is compatible with your agda-mode on VS Code
+
+```
+git checkout v0.0.1.0
+```
+
+Here are the versions that work (on my machine)
+
+| 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 |
+
+
+Build it with the package manager you hate the least.
+
+I use Stack. But honestly, I couldn't care less.
+
+```
+stack install
+```
+
+Once you have `als` installed on your machine. Open VS Code and go to agda-mode's settings. Enable "Agda Mode: Agda Language Server".
+
+
+
+## Current features
+
+More stuff are clickable in the panel after loading (C-c C-l)
+
+
+
+
+## Why make it standalone?
+
+* for less impact on the Agda codebase
+* to help [decouple the Agda codebase](https://github.com/agda/agda/projects/5)
+* we can always merge it back to Agda later anyway
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/agda-language-server.cabal b/agda-language-server.cabal
new file mode 100644
--- /dev/null
+++ b/agda-language-server.cabal
@@ -0,0 +1,123 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.33.0.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 0f24217c91b5f8c3f3d6da5c70694d98b0ef55971a5324a2c460ca48c06c4bb1
+
+name: agda-language-server
+version: 0.0.3.0
+synopsis: LSP server for Agda
+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
+maintainer: banacorn@gmail.com
+copyright: 2020 Ting-gan LUA
+license: MIT
+license-file: LICENSE
+build-type: Simple
+extra-source-files:
+ README.md
+ CHANGELOG.md
+
+source-repository head
+ type: git
+ location: https://github.com/banacorn/agda-language-server
+
+library
+ exposed-modules:
+ Agda
+ Agda.Convert
+ Agda.IR
+ Agda.Misc
+ Agda.Parser
+ Agda.Position
+ Control.Concurrent.SizedChan
+ Monad
+ 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.ResponseController
+ Switchboard
+ other-modules:
+ Paths_agda_language_server
+ hs-source-dirs:
+ src
+ build-depends:
+ Agda
+ , aeson
+ , base >=4.7 && <5
+ , bytestring
+ , containers
+ , lsp
+ , mtl
+ , network
+ , network-simple
+ , process
+ , stm
+ , strict
+ , text
+ default-language: Haskell2010
+
+executable als
+ main-is: Main.hs
+ other-modules:
+ Paths_agda_language_server
+ hs-source-dirs:
+ app
+ ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N -fno-warn-orphans
+ build-depends:
+ Agda
+ , aeson
+ , agda-language-server
+ , base >=4.7 && <5
+ , bytestring
+ , containers
+ , lsp
+ , mtl
+ , network
+ , network-simple
+ , process
+ , stm
+ , strict
+ , text
+ default-language: Haskell2010
+
+test-suite als-test
+ type: exitcode-stdio-1.0
+ main-is: Spec.hs
+ other-modules:
+ Paths_agda_language_server
+ hs-source-dirs:
+ test
+ ghc-options: -threaded -rtsopts -with-rtsopts=-N
+ build-depends:
+ Agda
+ , aeson
+ , agda-language-server
+ , base >=4.7 && <5
+ , bytestring
+ , containers
+ , lsp
+ , mtl
+ , network
+ , network-simple
+ , process
+ , stm
+ , strict
+ , text
+ default-language: Haskell2010
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,50 @@
+module Main where
+
+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)
+ 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/src/Agda.hs b/src/Agda.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda.hs
@@ -0,0 +1,109 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-missing-methods #-}
+
+module Agda 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)
+
+getAgdaVersion :: String
+getAgdaVersion = versionWithCommitInfo
+
+interact :: ServerM IO ()
+interact = do
+ env <- ask
+
+ writeLog "[Agda] interaction start"
+
+ result <- mapReaderT runTCMPrettyErrors $ do
+ -- decides how to output Response
+ lift $
+ setInteractionOutputCallback $ \response -> do
+ reaction <- fromResponse response
+ sendResponse env reaction
+
+ -- keep reading command
+ commands <- liftIO $ initialiseCommandQueue (readCommand env)
+
+ -- start the loop
+ opts <- commandLineOptions
+ let commandState = (initCommandState commands) {optionsOnReload = opts {optAbsoluteIncludePaths = []}}
+
+ _ <- mapReaderT (`runStateT` commandState) (loop env)
+
+ return ()
+ -- TODO: we should examine the result
+ case result of
+ 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
+
+ lift Bench.print
+ unless done (loop env)
+
+ -- Reads the next command from the Channel
+ readCommand :: Env -> IO Command
+ readCommand env = Command <$> consumeCommand env
+
+parseIOTCM :: String -> Either String IOTCM
+parseIOTCM raw = case listToMaybe $ reads raw of
+ Just (x, "") -> Right x
+ Just (_, remnent) -> Left $ "not consumed: " ++ remnent
+ _ -> Left $ "cannot read: " ++ raw
+
+-- TODO: handle the caught errors
+
+-- | 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)
+
+ handleImpossible :: Impossible -> TCM (Either String a)
+ handleImpossible = return . Left . show
+
+ catchException :: SomeException -> IO (Either String a)
+ catchException e = return $ Left $ show e
diff --git a/src/Agda/Convert.hs b/src/Agda/Convert.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Convert.hs
@@ -0,0 +1,628 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Agda.Convert where
+
+import Render ( Block(..), Inlines, renderATop, Render(..) )
+
+import Agda.IR (FromAgda (..))
+import qualified Agda.IR as IR
+import Agda.Interaction.Base
+import Agda.Interaction.BasicOps as B
+import Agda.Interaction.EmacsCommand (Lisp)
+import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)
+import Agda.Interaction.Highlighting.Precise (Aspects (..), CompressedFile (ranges), 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.Position (HasRange (getRange), Range, noRange)
+import Agda.Syntax.Scope.Base
+import Agda.TypeChecking.Errors (prettyError)
+import Agda.TypeChecking.Monad hiding (Function)
+import Agda.TypeChecking.Pretty (prettyTCM)
+import qualified Agda.TypeChecking.Pretty as TCP
+import Agda.TypeChecking.Pretty.Warning (filterTCWarnings, prettyTCWarnings, prettyTCWarnings')
+import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors (..))
+import Agda.Utils.FileName (filePath)
+import Agda.Utils.Function (applyWhen)
+import Agda.Utils.IO.TempFile (writeToTempFile)
+import Agda.Utils.Impossible (__IMPOSSIBLE__)
+import Agda.Utils.Maybe (catMaybes)
+import Agda.Utils.Null (empty)
+import Agda.Utils.Pretty hiding (render)
+import Agda.Utils.String (delimiter)
+import Agda.Utils.Time (CPUTime)
+import Agda.VersionCommit (versionWithCommitInfo)
+import Control.Monad.State hiding (state)
+import qualified Data.Aeson as JSON
+import qualified Data.ByteString.Lazy.Char8 as BS8
+import qualified Data.List as List
+import qualified Data.Map as Map
+import Data.String (IsString)
+import qualified Render
+
+responseAbbr :: IsString a => Response -> a
+responseAbbr res = case res of
+ Resp_HighlightingInfo {} -> "Resp_HighlightingInfo"
+ Resp_Status {} -> "Resp_Status"
+ Resp_JumpToError {} -> "Resp_JumpToError"
+ Resp_InteractionPoints {} -> "Resp_InteractionPoints"
+ Resp_GiveAction {} -> "Resp_GiveAction"
+ Resp_MakeCase {} -> "Resp_MakeCase"
+ Resp_SolveAll {} -> "Resp_SolveAll"
+ Resp_DisplayInfo {} -> "Resp_DisplayInfo"
+ Resp_RunningInfo {} -> "Resp_RunningInfo"
+ Resp_ClearRunningInfo {} -> "Resp_ClearRunningInfo"
+ Resp_ClearHighlighting {} -> "Resp_ClearHighlighting"
+ Resp_DoneAborting {} -> "Resp_DoneAborting"
+ Resp_DoneExiting {} -> "Resp_DoneExiting"
+
+----------------------------------
+
+serialize :: Lisp String -> String
+serialize = show . pretty
+
+fromResponse :: Response -> TCM IR.Response
+fromResponse (Resp_HighlightingInfo info remove method modFile) =
+ fromHighlightingInfo info remove method modFile
+fromResponse (Resp_DisplayInfo info) = IR.ResponseDisplayInfo <$> fromDisplayInfo info
+fromResponse (Resp_ClearHighlighting TokenBased) = return IR.ResponseClearHighlightingTokenBased
+fromResponse (Resp_ClearHighlighting NotOnlyTokenBased) = return IR.ResponseClearHighlightingNotOnlyTokenBased
+fromResponse Resp_DoneAborting = return IR.ResponseDoneAborting
+fromResponse Resp_DoneExiting = return IR.ResponseDoneExiting
+fromResponse Resp_ClearRunningInfo = return IR.ResponseClearRunningInfo
+fromResponse (Resp_RunningInfo n s) = return $ IR.ResponseRunningInfo n s
+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)
+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)
+ where
+ prn (InteractionId i, e) = (i, prettyShow e)
+
+fromHighlightingInfo ::
+ HighlightingInfo ->
+ RemoveTokenBasedHighlighting ->
+ HighlightingMethod ->
+ ModuleToSource ->
+ TCM IR.Response
+fromHighlightingInfo h remove method modFile =
+ case chooseHighlightingMethod h method of
+ Direct -> return $ IR.ResponseHighlightingInfoDirect info
+ Indirect -> IR.ResponseHighlightingInfoIndirect <$> indirect
+ where
+ fromAspects ::
+ (Highlighting.Range, Aspects) ->
+ IR.HighlightingInfo
+ fromAspects (range, aspects) =
+ IR.HighlightingInfo
+ (Highlighting.from range)
+ (Highlighting.to range)
+ (toAtoms aspects)
+ (tokenBased aspects == TokenBased)
+ (note aspects)
+ (defSite <$> definitionSite aspects)
+ where
+ defSite (DefinitionSite moduleName offset _ _) =
+ (filePath (Map.findWithDefault __IMPOSSIBLE__ moduleName modFile), offset)
+
+ infos :: [IR.HighlightingInfo]
+ infos = map fromAspects (ranges h)
+
+ keepHighlighting :: Bool
+ keepHighlighting =
+ case remove of
+ RemoveHighlighting -> False
+ KeepHighlighting -> True
+
+ info :: IR.HighlightingInfos
+ info = IR.HighlightingInfos keepHighlighting infos
+
+ indirect :: TCM FilePath
+ indirect = liftIO $ writeToTempFile (BS8.unpack (JSON.encode info))
+
+fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo
+fromDisplayInfo info = case info of
+ Info_CompilationOk ws -> do
+ -- filter
+ let filteredWarnings = filterTCWarnings (tcWarnings ws)
+ let filteredErrors = filterTCWarnings (nonFatalErrors ws)
+ -- serializes
+ warnings <- mapM prettyTCM filteredWarnings
+ errors <- mapM prettyTCM filteredErrors
+ return $ IR.DisplayInfoCompilationOk (map show warnings) (map 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]
+ Info_AllGoalsWarnings (ims, hms) ws -> do
+ -- visible metas (goals)
+ goals <- mapM convertGoal ims
+ -- hidden (unsolved) metas
+ metas <- mapM convertHiddenMeta hms
+
+ -- errors / warnings
+ -- filter
+ let filteredWarnings = filterTCWarnings (tcWarnings ws)
+ let filteredErrors = filterTCWarnings (nonFatalErrors ws)
+ -- serializes
+ warnings <- mapM prettyTCM filteredWarnings
+ errors <- mapM prettyTCM filteredErrors
+
+ let isG = not (null goals && null metas)
+ let isW = not $ null warnings
+ let isE = not $ null errors
+ let title =
+ List.intercalate "," $
+ catMaybes
+ [ " Goals" <$ guard isG,
+ " Errors" <$ guard isE,
+ " Warnings" <$ guard isW,
+ " Done" <$ guard (not (isG || isW || isE))
+ ]
+
+ return $ IR.DisplayInfoAllGoalsWarnings ("*All" ++ title ++ "*") goals metas (map show warnings) (map show errors)
+ where
+ convertHiddenMeta :: OutputConstraint A.Expr NamedMeta -> TCM Block
+ convertHiddenMeta m = do
+ let i = nmid $ namedMetaOf m
+ -- output constrain
+ meta <- withMetaId i $ renderATop m
+ serialized <- show <$> withMetaId i (prettyATop m)
+ -- range
+ range <- getMetaRange i
+
+ return $ Unlabeled meta (Just serialized) (Just range)
+
+ convertGoal :: OutputConstraint A.Expr InteractionId -> TCM Block
+ convertGoal i = do
+ -- output constrain
+ goal <-
+ withInteractionId (outputFormId $ OutputForm noRange [] i) $
+ renderATop i
+
+ serialized <-
+ withInteractionId (outputFormId $ OutputForm noRange [] i) $
+ prettyATop i
+ return $ Unlabeled goal (Just $ show serialized) Nothing
+ Info_Auto s -> return $ IR.DisplayInfoAuto s
+ Info_Error err -> do
+ s <- showInfoError err
+ return $ IR.DisplayInfoError s
+ Info_Time s ->
+ return $ IR.DisplayInfoTime (show (prettyTimed s))
+ Info_NormalForm state cmode time expr -> do
+ exprDoc <- evalStateT prettyExpr state
+ let doc = maybe empty prettyTimed time $$ exprDoc
+ return $ IR.DisplayInfoNormalForm (show doc)
+ where
+ prettyExpr =
+ localStateCommandM $
+ lift $
+ B.atTopLevel $
+ allowNonTerminatingReductions $
+ (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode) $
+ B.showComputed cmode expr
+ Info_InferredType state time expr -> do
+ renderedExpr <-
+ flip evalStateT state $
+ localStateCommandM $
+ lift $
+ B.atTopLevel $
+ Render.renderA expr
+ let rendered = case time of
+ Nothing -> renderedExpr
+ -- TODO: handle this newline
+ Just t -> "Time:" Render.<+> Render.render t Render.<+> "\n" Render.<+> renderedExpr
+ exprDoc <-
+ flip evalStateT state $
+ localStateCommandM $
+ lift $
+ B.atTopLevel $
+ TCP.prettyA expr
+ let raw = show $ maybe empty prettyTimed time $$ exprDoc
+ return $ IR.DisplayInfoGeneric "Inferred Type" [Unlabeled rendered (Just raw) Nothing]
+ Info_ModuleContents modules tel types -> do
+ doc <- localTCState $ do
+ typeDocs <- addContext tel $
+ forM types $ \(x, t) -> do
+ doc <- prettyTCM t
+ return (prettyShow x, ":" <+> doc)
+ return $
+ vcat
+ [ "Modules",
+ nest 2 $ vcat $ map pretty modules,
+ "Names",
+ nest 2 $ align 10 typeDocs
+ ]
+ return $ IR.DisplayInfoGeneric "Module contents" [Unlabeled (Render.text $ show doc) Nothing Nothing]
+ Info_SearchAbout hits names -> do
+ hitDocs <- forM hits $ \(x, t) -> do
+ doc <- prettyTCM t
+ return (prettyShow x, ":" <+> doc)
+ let doc =
+ "Definitions about"
+ <+> text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs)
+ return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
+ Info_WhyInScope s cwd v xs ms -> do
+ doc <- explainWhyInScope s cwd v xs ms
+ return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing]
+ Info_Context ii ctx -> do
+ doc <- localTCState (prettyResponseContexts ii False ctx)
+ return $ IR.DisplayInfoGeneric "Context" [Unlabeled (Render.text $ show doc) Nothing Nothing]
+ Info_Intro_NotFound ->
+ return $ IR.DisplayInfoGeneric "Intro" [Unlabeled (Render.text "No introduction forms found.") Nothing Nothing]
+ Info_Intro_ConstructorUnknown ss -> do
+ let doc =
+ sep
+ [ "Don't know which constructor to introduce of",
+ let mkOr [] = []
+ mkOr [x, y] = [text x <+> "or" <+> text y]
+ mkOr (x : xs) = text x : mkOr xs
+ in nest 2 $ fsep $ punctuate comma (mkOr ss)
+ ]
+ return $ IR.DisplayInfoGeneric "Intro" [Unlabeled (Render.text $ show doc) Nothing Nothing]
+ Info_Version ->
+ return $ IR.DisplayInfoGeneric "Agda Version" [Unlabeled (Render.text $ "Agda version " ++ versionWithCommitInfo) Nothing Nothing]
+ Info_GoalSpecific ii kind -> lispifyGoalSpecificDisplayInfo ii kind
+
+lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM IR.DisplayInfo
+lispifyGoalSpecificDisplayInfo ii kind = localTCState $
+ B.withInteractionId ii $
+ case kind of
+ Goal_HelperFunction helperType -> do
+ doc <- inTopContext $ prettyATop helperType
+ return $ IR.DisplayInfoGeneric "Helper function" [Unlabeled (Render.text $ show doc ++ "\n") Nothing Nothing]
+ Goal_NormalForm cmode expr -> do
+ doc <- showComputed cmode expr
+ return $ IR.DisplayInfoGeneric "Normal Form" [Unlabeled (Render.text $ show doc) Nothing Nothing]
+ Goal_GoalType norm aux resCtxs boundaries constraints -> do
+ goalSect <- do
+ (rendered, raw) <- prettyTypeOfMeta norm ii
+ return [Labeled rendered (Just raw) Nothing "Goal" "special"]
+
+ auxSect <- case aux of
+ GoalOnly -> return []
+ GoalAndHave expr -> do
+ rendered <- renderATop expr
+ raw <- show <$> prettyATop expr
+ return [Labeled rendered (Just raw) Nothing "Have" "special"]
+ GoalAndElaboration term -> do
+ let rendered = render term
+ raw <- show <$> TCP.prettyTCM term
+ return [Labeled rendered (Just raw) Nothing "Elaborates to" "special"]
+ let boundarySect =
+ if null boundaries
+ then []
+ else
+ Header "Boundary" :
+ map (\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
+
+ return $
+ IR.DisplayInfoGeneric "Goal type etc" $ goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect
+ Goal_CurrentGoal norm -> do
+ (rendered, raw) <- prettyTypeOfMeta norm ii
+ return $ IR.DisplayInfoCurrentGoal (Unlabeled rendered (Just raw) Nothing)
+ Goal_InferredType expr -> do
+ rendered <- renderATop expr
+ raw <- show <$> prettyATop expr
+ return $ IR.DisplayInfoInferredType (Unlabeled rendered (Just raw) Nothing)
+
+-- -- | Format responses of DisplayInfo
+-- formatPrim :: Bool -> [Block] -> String -> TCM IR.DisplayInfo
+-- formatPrim _copy items header = return $ IR.DisplayInfoGeneric header items
+
+-- -- | Format responses of DisplayInfo ("agda2-info-action")
+-- format :: [Block] -> String -> TCM IR.DisplayInfo
+-- format = formatPrim False
+
+-- -- | Format responses of DisplayInfo ("agda2-info-action-copy")
+-- formatAndCopy :: [Block] -> String -> TCM IR.DisplayInfo
+-- formatAndCopy = formatPrim True
+
+--------------------------------------------------------------------------------
+
+-- | Serializing Info_Error
+showInfoError :: Info_Error -> TCM String
+showInfoError (Info_GenericError err) = do
+ e <- prettyError err
+ w <- prettyTCWarnings' =<< getAllWarningsOfTCErr err
+
+ let errorMsg =
+ if null w
+ then e
+ else delimiter "Error" ++ "\n" ++ e
+ let warningMsg =
+ List.intercalate "\n" $
+ delimiter "Warning(s)" :
+ filter (not . null) w
+ return $
+ if null w
+ then errorMsg
+ else errorMsg ++ "\n\n" ++ warningMsg
+showInfoError (Info_CompilationError warnings) = do
+ s <- prettyTCWarnings warnings
+ return $
+ unlines
+ [ "You need to fix the following errors before you can compile",
+ "the module:",
+ "",
+ s
+ ]
+showInfoError (Info_HighlightingParseError ii) =
+ return $ "Highlighting failed to parse expression in " ++ show ii
+showInfoError (Info_HighlightingScopeCheckError ii) =
+ return $ "Highlighting failed to scope check expression in " ++ show ii
+
+explainWhyInScope ::
+ FilePath ->
+ String ->
+ Maybe LocalVar ->
+ [AbstractName] ->
+ [AbstractModule] ->
+ TCM Doc
+explainWhyInScope s _ Nothing [] [] = TCP.text (s ++ " is not in scope.")
+explainWhyInScope s _ v xs ms =
+ TCP.vcat
+ [ TCP.text (s ++ " is in scope as"),
+ TCP.nest 2 $ TCP.vcat [variable v xs, modules ms]
+ ]
+ where
+ -- variable :: Maybe _ -> [_] -> TCM Doc
+ variable Nothing vs = names vs
+ variable (Just x) vs
+ | null vs = asVar
+ | otherwise =
+ TCP.vcat
+ [ TCP.sep [asVar, TCP.nest 2 $ shadowing x],
+ TCP.nest 2 $ names vs
+ ]
+ where
+ asVar :: TCM Doc
+ asVar =
+ "* a variable bound at" TCP.<+> TCP.prettyTCM (nameBindingSite $ localVar x)
+ shadowing :: LocalVar -> TCM Doc
+ shadowing (LocalVar _ _ []) = "shadowing"
+ shadowing _ = "in conflict with"
+ names = TCP.vcat . map pName
+ modules = TCP.vcat . map pMod
+
+ pKind = \case
+ ConName -> "constructor"
+ FldName -> "record field"
+ PatternSynName -> "pattern synonym"
+ GeneralizeName -> "generalizable variable"
+ DisallowedGeneralizeName -> "generalizable variable from let open"
+ MacroName -> "macro name"
+ QuotableName -> "quotable name"
+ -- previously DefName:
+ DataName -> "data type"
+ RecName -> "record type"
+ AxiomName -> "postulate"
+ PrimName -> "primitive function"
+ FunName -> "defined name"
+ OtherDefName -> "defined name"
+
+ pName :: AbstractName -> TCM Doc
+ pName a =
+ TCP.sep
+ [ "* a"
+ TCP.<+> pKind (anameKind a)
+ TCP.<+> TCP.text (prettyShow $ anameName a),
+ TCP.nest 2 "brought into scope by"
+ ]
+ TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a))
+ pMod :: AbstractModule -> TCM Doc
+ pMod a =
+ TCP.sep
+ [ "* a module" TCP.<+> TCP.text (prettyShow $ amodName a),
+ TCP.nest 2 "brought into scope by"
+ ]
+ TCP.$$ TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ mnameToQName $ amodName a) (amodLineage a))
+
+ pWhy :: Range -> WhyInScope -> TCM Doc
+ pWhy r Defined = "- its definition at" TCP.<+> TCP.prettyTCM r
+ pWhy r (Opened (C.QName x) w) | isNoName x = pWhy r w
+ pWhy r (Opened m w) =
+ "- the opening of"
+ TCP.<+> TCP.prettyTCM m
+ TCP.<+> "at"
+ TCP.<+> TCP.prettyTCM (getRange m)
+ TCP.$$ pWhy r w
+ pWhy r (Applied m w) =
+ "- the application of"
+ TCP.<+> TCP.prettyTCM m
+ TCP.<+> "at"
+ TCP.<+> TCP.prettyTCM (getRange m)
+ TCP.$$ pWhy r w
+
+-- | Pretty-prints the context of the given meta-variable.
+prettyResponseContexts ::
+ -- | Context of this meta-variable.
+ InteractionId ->
+ -- | Print the elements in reverse order?
+ Bool ->
+ [ResponseContextEntry] ->
+ TCM Doc
+prettyResponseContexts ii rev ctxs = do
+ rows <- mapM (prettyResponseContext ii) ctxs
+ return $ align 10 $ concat $ applyWhen rev reverse rows
+
+-- | Pretty-prints the context of the given meta-variable.
+prettyResponseContext ::
+ -- | Context of this meta-variable.
+ InteractionId ->
+ ResponseContextEntry ->
+ TCM [(String, Doc)]
+prettyResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
+ modality <- asksTC getModality
+ do
+ let prettyCtxName :: String
+ prettyCtxName
+ | n == x = prettyShow x
+ | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
+ | otherwise = prettyShow x
+
+ -- Some attributes are useful to report whenever they are not
+ -- in the default state.
+ attribute :: String
+ attribute = c ++ if null c then "" else " "
+ where
+ c = prettyShow (getCohesion ai)
+
+ extras :: [Doc]
+ extras =
+ concat
+ [ ["not in scope" | isInScope nis == C.NotInScope],
+ -- Print erased if hypothesis is erased by goal is non-erased.
+ ["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
+ -- Print irrelevant if hypothesis is strictly less relevant than goal.
+ ["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
+ -- Print instance if variable is considered by instance search
+ ["instance" | isInstance ai]
+ ]
+ ty <- prettyATop expr
+
+ letv' <- case letv of
+ Nothing -> return []
+ Just val -> do
+ val' <- prettyATop val
+ return [(prettyShow x, "=" <+> val')]
+
+ return $
+ (attribute ++ prettyCtxName, ":" <+> ty <+> parenSep extras) : letv'
+ where
+ parenSep :: [Doc] -> Doc
+ parenSep docs
+ | null docs = empty
+ | otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs
+
+-- | Render the context of the given meta-variable.
+renderResponseContext ::
+ -- | Context of this meta-variable.
+ InteractionId ->
+ ResponseContextEntry ->
+ TCM [Block]
+renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
+ modality <- asksTC getModality
+ do
+ let
+ rawCtxName :: String
+ rawCtxName
+ | n == x = prettyShow x
+ | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
+ | otherwise = prettyShow x
+
+ renderedCtxName :: Inlines
+ renderedCtxName
+ | n == x = render x
+ | isInScope n == InScope = render n Render.<+> "=" Render.<+> render x
+ | otherwise = render x
+
+ -- Some attributes are useful to report whenever they are not
+ -- in the default state.
+ rawAttribute :: String
+ rawAttribute = c ++ if null c then "" else " "
+ where
+ c = prettyShow (getCohesion ai)
+
+ renderedAttribute :: Inlines
+ renderedAttribute = c <> if null (show c) then "" else " "
+ where
+ c = render (getCohesion ai)
+
+ extras :: IsString a => [a]
+ extras =
+ concat
+ [ ["not in scope" | isInScope nis == C.NotInScope],
+ -- Print erased if hypothesis is erased by goal is non-erased.
+ ["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
+ -- Print irrelevant if hypothesis is strictly less relevant than goal.
+ ["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
+ -- Print instance if variable is considered by instance search
+ ["instance" | isInstance ai]
+ ]
+
+ extras2 :: [Inlines]
+ extras2 =
+ concat
+ [ ["not in scope" | isInScope nis == C.NotInScope],
+ -- Print erased if hypothesis is erased by goal is non-erased.
+ ["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
+ -- Print irrelevant if hypothesis is strictly less relevant than goal.
+ ["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
+ -- Print instance if variable is considered by instance search
+ ["instance" | isInstance ai]
+ ]
+
+ -- raw
+ rawExpr <- prettyATop expr
+ let rawType = show $ align 10 [(rawAttribute ++ rawCtxName, ":" <+> rawExpr <+> parenSep extras)]
+ -- rendered
+ renderedExpr <- renderATop expr
+ let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2
+ -- (Render.fsep $ Render.punctuate "," extras)
+
+ -- result
+ let typeItem = Unlabeled renderedType (Just rawType) Nothing
+
+ valueItem <- case letv of
+ Nothing -> return []
+ Just val -> do
+ valText <- renderATop val
+ valString <- prettyATop val
+ let renderedValue = Render.render x Render.<+> "=" Render.<+> valText
+ let rawValue = show $ align 10 [(prettyShow x, "=" <+> valString)]
+ return
+ [ Unlabeled renderedValue (Just rawValue) Nothing
+ ]
+
+ return $ typeItem : valueItem
+ where
+ parenSep :: [Doc] -> Doc
+ parenSep docs
+ | null docs = empty
+ | otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs
+
+ parenSep2 :: [Inlines] -> Inlines
+ parenSep2 docs
+ | null docs = mempty
+ | otherwise = (" " Render.<+>) $ Render.parens $ Render.fsep $ Render.punctuate "," docs
+
+
+-- | Pretty-prints the type of the meta-variable.
+prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
+prettyTypeOfMeta norm ii = do
+ form <- B.typeOfMeta norm ii
+ case form of
+ OfType _ e -> do
+ rendered <- renderATop e
+ raw <- show <$> prettyATop e
+ return (rendered, raw)
+ _ -> do
+ rendered <- renderATop form
+ raw <- show <$> prettyATop form
+ return (rendered, raw)
+
+-- | Prefix prettified CPUTime with "Time:"
+prettyTimed :: CPUTime -> Doc
+prettyTimed time = "Time:" <+> pretty time
diff --git a/src/Agda/IR.hs b/src/Agda/IR.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/IR.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FunctionalDependencies #-}
+
+-- | Intermediate Representation for Agda's types
+module Agda.IR where
+
+import qualified Agda.Interaction.Response as Agda
+import Agda.TypeChecking.Monad (TCM)
+import Data.Aeson
+import GHC.Generics (Generic)
+import Render
+
+--------------------------------------------------------------------------------
+
+-- | Typeclass for converting Agda values into IR
+class FromAgda a b | a -> b where
+ fromAgda :: a -> b
+
+class FromAgdaTCM a b | a -> b where
+ fromAgdaTCM :: a -> TCM b
+
+--------------------------------------------------------------------------------
+-- | IR for IOCTM
+data Response
+ = -- non-last responses
+ ResponseHighlightingInfoDirect HighlightingInfos
+ | ResponseHighlightingInfoIndirect FilePath
+ | ResponseDisplayInfo DisplayInfo
+ | ResponseStatus Bool Bool
+ | ResponseClearHighlightingTokenBased
+ | ResponseClearHighlightingNotOnlyTokenBased
+ | ResponseRunningInfo Int String
+ | ResponseClearRunningInfo
+ | ResponseDoneAborting
+ | ResponseDoneExiting
+ | ResponseGiveAction Int GiveResult
+ | -- priority: 1
+ ResponseInteractionPoints [Int]
+ | -- priority: 2
+ ResponseMakeCaseFunction [String]
+ | ResponseMakeCaseExtendedLambda [String]
+ | ResponseSolveAll [(Int, String)]
+ | -- priority: 3
+ ResponseJumpToError FilePath Int
+ | ResponseEnd
+ deriving (Generic)
+
+instance ToJSON Response
+
+--------------------------------------------------------------------------------
+
+-- | IR for DisplayInfo
+data DisplayInfo
+ = DisplayInfoGeneric String [Block]
+ | DisplayInfoAllGoalsWarnings String [Block] [Block] [String] [String]
+ | DisplayInfoCurrentGoal Block
+ | DisplayInfoInferredType Block
+ | DisplayInfoCompilationOk [String] [String]
+ | DisplayInfoAuto String
+ | DisplayInfoError String
+ | DisplayInfoTime String
+ | DisplayInfoNormalForm String
+ deriving (Generic)
+
+instance ToJSON DisplayInfo
+
+--------------------------------------------------------------------------------
+
+-- | GiveResult
+data GiveResult
+ = GiveString String
+ | GiveParen
+ | GiveNoParen
+ deriving (Generic)
+
+instance FromAgda Agda.GiveResult GiveResult where
+ fromAgda (Agda.Give_String s) = GiveString s
+ fromAgda Agda.Give_Paren = GiveParen
+ fromAgda Agda.Give_NoParen = GiveNoParen
+
+instance ToJSON GiveResult
+
+--------------------------------------------------------------------------------
+
+-- | IR for HighlightingInfo
+data HighlightingInfo
+ = HighlightingInfo
+ Int -- starting offset
+ Int -- ending offset
+ [String] -- list of names of aspects
+ Bool -- is token based?
+ (Maybe String) -- note
+ (Maybe (FilePath, Int)) -- the defining module of the token and its position in that module
+ deriving (Generic, Show)
+
+instance ToJSON HighlightingInfo
+
+data HighlightingInfos = HighlightingInfos Bool [HighlightingInfo]
+ deriving (Generic, Show)
+
+instance ToJSON HighlightingInfos
diff --git a/src/Agda/Misc.hs b/src/Agda/Misc.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Misc.hs
@@ -0,0 +1,89 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/src/Agda/Parser.hs
@@ -0,0 +1,56 @@
+module Agda.Parser where
+
+--------------------------------------------------------------------------------
+
+import Agda.Syntax.Parser (parseFile, runPMIO, tokensParser)
+import Agda.Syntax.Parser.Tokens (Token)
+import Agda.Syntax.Position (Position' (posPos), PositionWithoutFile, Range, getRange, rEnd', rStart')
+import Agda.Utils.FileName (mkAbsolute)
+import Monad ( ServerM )
+import Control.Monad.State
+import Data.List (find)
+import Data.Maybe (fromMaybe)
+import Data.Text (Text, unpack)
+import qualified Data.Text as Text
+import Language.LSP.Server (LspM)
+import qualified Language.LSP.Types as LSP
+
+--------------------------------------------------------------------------------
+
+tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM ()) (Maybe (Token, Text))
+tokenAt uri source position = case LSP.uriToFilePath uri of
+ Nothing -> return Nothing
+ Just filepath -> do
+ (result, _warnings) <- liftIO $
+ runPMIO $ do
+ -- parse the file and get all tokens
+ (tokens, _fileType) <- parseFile tokensParser (mkAbsolute filepath) (unpack source)
+ -- find the token at the position
+ return $ find (pointedBy position) tokens
+ case result of
+ Left _err -> return Nothing
+ Right Nothing -> return Nothing
+ Right (Just token) -> do
+ -- get the range of the token
+ case tokenOffsets token of
+ Nothing -> return Nothing
+ Just (start, end) -> do
+ -- get the text from the range of the token
+ let text = Text.drop (start - 1) (Text.take (end - 1) source)
+ return $ Just (token, text)
+ where
+ startAndEnd :: Range -> Maybe (PositionWithoutFile, PositionWithoutFile)
+ startAndEnd range = do
+ start <- rStart' range
+ end <- rEnd' range
+ return (start, end)
+
+ pointedBy :: PositionWithoutFile -> Token -> Bool
+ pointedBy pos token = fromMaybe False $ do
+ (start, end) <- startAndEnd (getRange token)
+ return $ start <= pos && pos < end
+
+ tokenOffsets :: Token -> Maybe (Int, Int)
+ tokenOffsets token = do
+ (start, end) <- startAndEnd (getRange token)
+ return (fromIntegral (posPos start), fromIntegral (posPos end))
diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs
new file mode 100644
--- /dev/null
+++ b/src/Agda/Position.hs
@@ -0,0 +1,87 @@
+-- {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Agda.Position
+ ( OffsetTable,
+ makeOffsetTable,
+ lookupOffsetTable,
+ toPositionWithoutFile,
+ toRange,
+ prettyPositionWithoutFile,
+ )
+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
+
+-- Note: LSP srclocs are 0-base
+-- Agda srclocs are 1-base
+
+--------------------------------------------------------------------------------
+
+-- | LSP locations -> Agda 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)
+
+-- | 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)
+
+prettyPositionWithoutFile :: PositionWithoutFile -> String
+prettyPositionWithoutFile pos@(Pn () offset line col) = "[" <> show pos <> "-" <> show offset <> "]"
+
+--------------------------------------------------------------------------------
+
+-- | Positon -> Offset convertion
+
+-- | A list of offsets of linebreaks ("\n", "\r" or "\r\n")
+newtype OffsetTable = OffsetTable [Int]
+
+data Accum = Accum
+ { accumPreviousChar :: Maybe Char,
+ accumCurrentOffset :: Int,
+ accumOffsetTable :: [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
+
+-- | Zero-based
+lookupOffsetTable :: OffsetTable -> Int -> Int -> Int
+lookupOffsetTable (OffsetTable offsets) line col = offsets !! line + col
+
+-- toLSPRange :: Range -> LSP.Range
+-- toLSPRange 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)
+
+-- toLSPPosition :: Position -> LSP.Position
+-- toLSPPosition (Pn _ offset line col) = LSP.Position (fromIntegral line - 1) (fromIntegral col - 1)
diff --git a/src/Control/Concurrent/SizedChan.hs b/src/Control/Concurrent/SizedChan.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Concurrent/SizedChan.hs
@@ -0,0 +1,99 @@
+-- | Chan with size
+module Control.Concurrent.SizedChan (SizedChan, newSizedChan, writeSizedChan, readSizedChan, tryReadSizedChan, peekSizedChan, tryPeekSizedChan, isEmptySizedChan) where
+
+import Control.Concurrent.Chan
+import Data.IORef
+
+data SizedChan a =
+ SizedChan
+ (Chan a) -- ^ The channel
+ (IORef Int) -- ^ Its size
+ (IORef (Maybe a)) -- ^ Peeked payload
+
+-- | Build and returns a new instance of 'SizedChan'.
+newSizedChan :: IO (SizedChan a)
+newSizedChan =
+ SizedChan
+ <$> newChan
+ <*> newIORef 0
+ <*> newIORef Nothing
+
+-- | Write a value to a 'SizedChan'.
+writeSizedChan :: SizedChan a -> a -> IO ()
+writeSizedChan (SizedChan chan sizeIORef _) val = do
+ writeChan chan val
+ modifyIORef' sizeIORef succ
+
+-- | Read the next value from the 'SizedChan'. Blocks when the channel is empty.
+readSizedChan :: SizedChan a -> IO a
+readSizedChan (SizedChan chan sizeIORef peekedIORef) = do
+ peeked <- readIORef peekedIORef
+ case peeked of
+ -- return and remove the peeked value
+ Just val -> do
+ writeIORef peekedIORef Nothing
+ modifyIORef' sizeIORef pred
+ return val
+ -- else read from the channel
+ Nothing -> do
+ val <- readChan chan
+ modifyIORef' sizeIORef pred
+ return val
+
+-- | A version of `readSizedChan` which does not block. Instead it returns Nothing if no value is available.
+tryReadSizedChan :: SizedChan a -> IO (Maybe a)
+tryReadSizedChan (SizedChan chan sizeIORef peekedIORef) = do
+ peeked <- readIORef peekedIORef
+ case peeked of
+ -- return and remove the peeked value
+ Just val -> do
+ writeIORef peekedIORef Nothing
+ modifyIORef' sizeIORef pred
+ return $ Just val
+ -- check the size before reading from the channel, to prevent blocking
+ Nothing -> do
+ size <- readIORef sizeIORef
+ if size == 0
+ then return Nothing
+ else do
+ val <- readChan chan
+ modifyIORef' sizeIORef pred
+ return $ Just val
+
+-- | Peek the next value from the 'SizedChan' without removing it. Blocks when the channel is empty.
+peekSizedChan :: SizedChan a -> IO a
+peekSizedChan (SizedChan chan _ peekedIORef) = do
+ peeked <- readIORef peekedIORef
+ case peeked of
+ -- return the peeked value
+ Just val -> return val
+ -- read from the channel instead
+ Nothing -> do
+ val <- readChan chan
+ writeIORef peekedIORef (Just val)
+ return val
+
+-- | A version of `peekSizedChan` which does not block. Instead it returns Nothing if no value is available.
+tryPeekSizedChan :: SizedChan a -> IO (Maybe a)
+tryPeekSizedChan (SizedChan chan sizeIORef peekedIORef) = do
+ peeked <- readIORef peekedIORef
+ case peeked of
+ -- return the peeked value
+ Just val -> return $ Just val
+ -- check the size before reading from the channel, to prevent blocking
+ Nothing -> do
+ size <- readIORef sizeIORef
+ if size == 0
+ then return Nothing
+ else do
+ val <- readChan chan
+ writeIORef peekedIORef (Just val)
+ return $ Just val
+
+measureSizedChan :: SizedChan a -> IO Int
+measureSizedChan (SizedChan _ sizeIORef _) = readIORef sizeIORef
+
+isEmptySizedChan :: SizedChan a -> IO Bool
+isEmptySizedChan chan = do
+ size <- measureSizedChan chan
+ return $ size == 0
diff --git a/src/Monad.hs b/src/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Monad.hs
@@ -0,0 +1,81 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Monad where
+
+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)
+
+--------------------------------------------------------------------------------
+
+data Env = Env
+ { envLogChan :: Chan Text,
+ envCommandController :: CommandController,
+ envResponseChan :: Chan Response,
+ envResponseController :: ResponseController,
+ envDevMode :: Bool
+ }
+
+createInitEnv :: Bool -> IO Env
+createInitEnv devMode =
+ Env <$> newChan
+ <*> CommandController.new
+ <*> newChan
+ <*> ResponseController.new
+ <*> pure devMode
+
+--------------------------------------------------------------------------------
+
+-- | OUR monad
+type ServerM m = ReaderT Env m
+
+runServerM :: Env -> ServerM m a -> m a
+runServerM = flip runReaderT
+
+--------------------------------------------------------------------------------
+
+writeLog :: (Monad m, MonadIO m) => Text -> ServerM m ()
+writeLog msg = do
+ chan <- asks envLogChan
+ liftIO $ writeChan chan msg
+
+writeLog' :: (Monad m, MonadIO m, Show a) => a -> ServerM m ()
+writeLog' x = do
+ chan <- asks envLogChan
+ liftIO $ writeChan chan $ pack $ show x
+
+-- | Provider
+provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerM m ()
+provideCommand iotcm = do
+ controller <- asks envCommandController
+ liftIO $ CommandController.put controller iotcm
+
+-- | Consumter
+consumeCommand :: (Monad m, MonadIO m) => Env -> m IOTCM
+consumeCommand env = liftIO $ CommandController.take (envCommandController env)
+
+waitUntilResponsesSent :: (Monad m, MonadIO m) => ServerM m ()
+waitUntilResponsesSent = do
+ controller <- asks envResponseController
+ liftIO $ ResponseController.setCheckpointAndWait controller
+
+signalCommandFinish :: (Monad m, MonadIO m) => ServerM m ()
+signalCommandFinish = do
+ writeLog "[Command] Finished"
+ -- send `ResponseEnd`
+ env <- ask
+ liftIO $ writeChan (envResponseChan env) ResponseEnd
+ -- allow the next Command to be consumed
+ liftIO $ CommandController.release (envCommandController env)
+
+sendResponse :: (Monad m, MonadIO m) => Env -> Response -> TCMT m ()
+sendResponse env reaction = do
+ liftIO $ writeChan (envResponseChan env) reaction
diff --git a/src/Render.hs b/src/Render.hs
new file mode 100644
--- /dev/null
+++ b/src/Render.hs
@@ -0,0 +1,16 @@
+module Render
+ ( module Render.RichText,
+ module Render.Class,
+ module Render.Concrete,
+ )
+where
+
+import Render.Class
+import Render.Concrete
+import Render.Interaction ()
+import Render.Internal ()
+import Render.Name ()
+import Render.RichText
+import Render.TypeChecking ()
+import Render.Position ()
+import Render.Utils ()
diff --git a/src/Render/Class.hs b/src/Render/Class.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Class.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.Class
+ ( Render (..),
+ -- RenderTCM (..),
+ renderM,
+ renderP,
+ renderA,
+ renderATop,
+ )
+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 qualified Agda.Utils.Pretty as Doc
+import Data.Int (Int32)
+import Render.RichText
+
+--------------------------------------------------------------------------------
+
+-- | Typeclass for rendering Inlines
+class Render a where
+ render :: a -> Inlines
+ renderPrec :: Int -> a -> Inlines
+
+ render = renderPrec 0
+ renderPrec = const render
+
+-- | Rendering undersome context
+-- class RenderTCM a where
+-- renderTCM :: a -> Agda.TCM Inlines
+
+-- | Simply "pure . render"
+renderM :: (Applicative m, Render a) => a -> m Inlines
+renderM = pure . render
+
+-- | Render instances of Pretty
+renderP :: (Applicative m, Doc.Pretty a) => a -> m Inlines
+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
+
+-- | like 'prettyATop'
+renderATop :: (Render c, Agda.ToConcrete a c) => a -> Agda.TCM Inlines
+renderATop x = render <$> Agda.abstractToConcreteCtx TopCtx x
+
+--------------------------------------------------------------------------------
+
+-- | Other instances of Render
+instance Render Int where
+ render = text . show
+
+instance Render Int32 where
+ render = text . show
+
+instance Render Integer where
+ render = text . show
+
+instance Render Bool where
+ render = text . show
+
+instance Render Doc where
+ render = text . Doc.render
+
+instance Render a => Render [a] where
+ render xs = "[" <> fsep (punctuate "," (map render xs)) <> "]"
diff --git a/src/Render/Common.hs b/src/Render/Common.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Common.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.Common where
+
+import Agda.Syntax.Common
+import qualified Agda.Utils.Null as Agda
+import Render.Class
+import Render.RichText
+import Agda.Utils.Functor ((<&>))
+
+--------------------------------------------------------------------------------
+
+-- | NameId
+instance Render NameId where
+ render (NameId n m) = text $ show n ++ "@" ++ show m
+
+-- | MetaId
+instance Render MetaId where
+ render (MetaId n) = text $ "_" ++ show n
+
+-- | Relevance
+instance Render Relevance where
+ render Relevant = mempty
+ render Irrelevant = "."
+ render NonStrict = ".."
+
+-- | Quantity
+instance Render Quantity where
+ render = \case
+ Quantity0 o ->
+ let s = show o
+ in if Agda.null o
+ then "@0"
+ else text s
+ Quantity1 o ->
+ let s = show o
+ in if Agda.null o
+ then "@1"
+ else text s
+ Quantityω o -> render o
+
+instance Render QωOrigin where
+ render = \case
+ QωInferred -> mempty
+ Qω{} -> "@ω"
+ QωPlenty{} -> "@plenty"
+
+instance Render Cohesion where
+ render Flat = "@♭"
+ render Continuous = mempty
+ render Squash = "@⊤"
+
+--------------------------------------------------------------------------------
+
+-- | From 'prettyHiding'
+-- @renderHiding info visible text@ puts the correct braces
+-- around @text@ according to info @info@ and returns
+-- @visible text@ if the we deal with a visible thing.
+renderHiding :: LensHiding a => a -> (Inlines -> Inlines) -> Inlines -> Inlines
+renderHiding a parensF =
+ case getHiding a of
+ Hidden -> braces'
+ Instance {} -> dbraces
+ NotHidden -> parensF
+
+renderRelevance :: LensRelevance a => a -> Inlines -> Inlines
+renderRelevance a d =
+ if show d == "_" then d else render (getRelevance a) <> d
+
+renderQuantity :: LensQuantity a => a -> Inlines -> Inlines
+renderQuantity a d =
+ if show d == "_" then d else render (getQuantity a) <+> d
+
+renderCohesion :: LensCohesion a => a -> Inlines -> Inlines
+renderCohesion a d =
+ if show d == "_" then d else render (getCohesion a) <+> d
+
+--------------------------------------------------------------------------------
+
+
+instance (Render p, Render e) => Render (RewriteEqn' qn 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)
+
+prefixedThings :: Inlines -> [Inlines] -> Inlines
+prefixedThings kw = \case
+ [] -> mempty
+ (doc : docs) -> fsep $ (kw <+> doc) : map ("|" <+>) docs
diff --git a/src/Render/Concrete.hs b/src/Render/Concrete.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Concrete.hs
@@ -0,0 +1,678 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiWayIf #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RankNTypes #-}
+
+module Render.Concrete where
+
+import Agda.Syntax.Common
+import Agda.Syntax.Concrete
+import Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)
+import Agda.Syntax.Position (noRange)
+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 ()
+import Render.Name ()
+import Render.RichText
+import Render.TypeChecking ()
+
+--------------------------------------------------------------------------------
+
+instance Render a => Render (WithHiding a) where
+ render w = renderHiding w id $ render $ dget w
+
+-- | OpApp
+instance Render (OpApp Expr) where
+ render (Ordinary e) = render e
+ render (SyntaxBindingLambda r bs e) = render (Lam r bs e)
+
+-- | MaybePlaceholder
+instance Render a => Render (MaybePlaceholder a) where
+ render Placeholder {} = "_"
+ render (NoPlaceholder _ e) = render e
+
+--------------------------------------------------------------------------------
+
+-- | InteractionId
+instance Render InteractionId where
+ render (InteractionId i) = linkHole i
+
+--------------------------------------------------------------------------------
+
+-- | Expression
+instance Render Expr where
+ render expr = case expr of
+ Ident qname -> render qname
+ Lit lit -> render lit
+ -- no hole index, use LinkRange instead
+ QuestionMark range Nothing -> linkRange range "?"
+ QuestionMark _range (Just n) -> linkHole n
+ Underscore range n -> linkRange range $ maybe "_" text n
+ -- '_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
+ OpApp _ q _ es -> fsep $ renderOpApp q es
+ WithApp _ e es -> fsep $ render e : map ((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]
+ AbsurdLam _ h -> lambda <+> absurd h
+ ExtendedLam _ pes -> lambda <+> bracesAndSemicolons (map render pes)
+ Fun _ e1 e2 ->
+ sep
+ [ renderCohesion e1 (renderQuantity e1 (render e1)) <+> arrow,
+ render e2
+ ]
+ Pi tel e ->
+ sep
+ [ render (Tel $ smashTel 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),
+ maybe mempty (\e -> "in" <+> render e) me
+ ]
+ Paren _ e -> parens $ render e
+ IdiomBrackets _ exprs ->
+ 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)
+ As _ x e -> render x <> "@" <> render e
+ Dot _ e -> "." <> render e
+ DoubleDot _ e -> ".." <> render e
+ Absurd _ -> "()"
+ Rec _ xs -> sep ["record", bracesAndSemicolons (map render xs)]
+ RecUpdate _ e xs ->
+ sep ["record" <+> render e, bracesAndSemicolons (map render xs)]
+ ETel [] -> "()"
+ ETel tel -> fsep $ map render tel
+ Quote _ -> "quote"
+ QuoteTerm _ -> "quoteTerm"
+ Unquote _ -> "unquote"
+ Tactic _ t -> "tactic" <+> render t
+ -- Andreas, 2011-10-03 print irrelevant things as .(e)
+ DontCare e -> "." <> parens (render e)
+ Equal _ a b -> render a <+> "=" <+> render b
+ Ellipsis _ -> "..."
+ Generalized e -> render e
+ where
+ absurd NotHidden = "()"
+ absurd Instance {} = "{{}}"
+ absurd Hidden = "{}"
+
+-- instance RenderTCM Expr where
+-- renderTCM = render
+
+--------------------------------------------------------------------------------
+
+instance (Render a, Render b) => Render (Either a b) where
+ render = either render render
+
+instance Render a => Render (FieldAssignment' a) where
+ 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
+
+instance Render LamClause where
+ render (LamClause lhs rhs wh _) =
+ sep
+ [ render lhs,
+ render' rhs,
+ render wh
+ ]
+ where
+ render' (RHS e) = arrow <+> render e
+ render' AbsurdRHS = mempty
+
+instance Render BoundName where
+ render BName {boundName = x} = render x
+
+instance Render a => Render (Binder' a) where
+ render (Binder mpat n) =
+ let d = render n
+ in case mpat of
+ Nothing -> d
+ Just pat -> d <+> "@" <+> parens (render pat)
+
+--------------------------------------------------------------------------------
+
+-- | NamedBinding
+instance Render NamedBinding where
+ render (NamedBinding withH x) =
+ prH $
+ if
+ | Just l <- isLabeled x -> text l <> " = " <> render xb
+ | otherwise -> render xb
+ where
+ xb = namedArg x
+ bn = binderName xb
+ prH
+ | withH =
+ renderRelevance x
+ . renderHiding x mparens'
+ . renderCohesion x
+ . renderQuantity x
+ . renderTactic bn
+ | otherwise = id
+ -- Parentheses are needed when an attribute @... is present
+ mparens'
+ | noUserQuantity x, Nothing <- bnameTactic bn = id
+ | otherwise = parens
+
+renderTactic :: BoundName -> Inlines -> Inlines
+renderTactic = renderTactic' . bnameTactic
+
+renderTactic' :: TacticAttribute -> Inlines -> Inlines
+renderTactic' Nothing d = d
+renderTactic' (Just t) d = "@" <> (parens ("tactic " <> render t) <+> d)
+
+--------------------------------------------------------------------------------
+
+-- | LamBinding
+instance Render LamBinding where
+ render (DomainFree x) = render (NamedBinding True x)
+ render (DomainFull b) = render b
+
+-- | TypedBinding
+instance Render TypedBinding where
+ render (TLet _ ds) = parens $ "let" <+> vcat (map render ds)
+ render (TBind _ xs (Underscore _ Nothing)) =
+ fsep (map (render . NamedBinding True) xs)
+ render (TBind _ binders e) =
+ fsep
+ [ renderRelevance y $
+ renderHiding y parens $
+ renderCohesion y $
+ renderQuantity y $
+ renderTactic (binderName $ namedArg y) $
+ sep
+ [ fsep (map (render . NamedBinding False) ys),
+ ":" <+> render e
+ ]
+ | ys@(y : _) <- groupBinds binders
+ ]
+ where
+ groupBinds [] = []
+ groupBinds (x : xs)
+ | Just {} <- isLabeled x = [x] : groupBinds xs
+ | otherwise = (x : ys) : groupBinds zs
+ where
+ (ys, zs) = span (same x) xs
+ same a b = getArgInfo a == getArgInfo b && isNothing (isLabeled b)
+
+instance Render Tel where
+ render (Tel tel)
+ | any isMeta tel = forallQ <+> fsep (map render tel)
+ | otherwise = fsep (map render tel)
+ where
+ isMeta (TBind _ _ (Underscore _ Nothing)) = True
+ isMeta _ = False
+
+smashTel :: Telescope -> Telescope
+smashTel
+ ( TBind r xs e
+ : TBind _ ys e'
+ : tel
+ )
+ | show e == show e' = smashTel (TBind r (xs ++ ys) e : tel)
+smashTel (b : tel) = b : smashTel tel
+smashTel [] = []
+
+instance Render RHS where
+ render (RHS e) = "=" <+> render e
+ render AbsurdRHS = mempty
+
+instance Render WhereClause where
+ render NoWhere = mempty
+ render (AnyWhere [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
+ [ hsep $
+ applyWhen
+ (a == PrivateAccess UserWritten)
+ ("private" :)
+ ["module", render m, "where"],
+ vcat $ map render ds
+ ]
+
+instance Render LHS where
+ render (LHS p eqs es _) =
+ sep
+ [ render p,
+ if null eqs then mempty else fsep $ map render eqs,
+ prefixedThings "with" (map render es)
+ ]
+
+instance Render LHSCore where
+ render (LHSHead f ps) = sep $ render f : map (parens . render) ps
+ render (LHSProj d ps lhscore ps') =
+ sep $
+ render d :
+ map (parens . render) ps
+ ++ parens (render lhscore) :
+ map (parens . render) ps'
+ render (LHSWith h wps ps) =
+ if null ps
+ then doc
+ else sep $ parens doc : map (parens . render) ps
+ where
+ doc = sep $ render h : map (("|" <+>) . render) wps
+
+instance Render ModuleApplication where
+ render (SectionApp _ bs e) = fsep (map render bs) <+> "=" <+> render e
+ render (RecordModuleInstance _ rec) = "=" <+> render rec <+> "{{...}}"
+
+instance Render DoStmt where
+ render (DoBind _ p e cs) =
+ fsep [render p <+> "←", render e, prCs cs]
+ where
+ prCs [] = mempty
+ prCs cs' = fsep ["where", vcat (map render cs')]
+ render (DoThen e) = render e
+ render (DoLet _ ds) = "let" <+> vcat (map render ds)
+
+instance Render Declaration where
+ render d =
+ case d of
+ TypeSig i tac x e ->
+ sep
+ [ renderTactic' tac $ renderRelevance i $ renderCohesion i $ renderQuantity i $ render x <+> ":",
+ render e
+ ]
+ FieldSig inst tac x (Arg i e) ->
+ mkInst inst $
+ mkOverlap i $
+ renderRelevance i $
+ renderHiding i id $
+ renderCohesion i $
+ renderQuantity i $
+ render $ TypeSig (setRelevance Relevant i) tac x e
+ where
+ mkInst (InstanceDef _) f = sep ["instance", f]
+ mkInst NotInstanceDef f = f
+
+ mkOverlap j f
+ | isOverlappable j = "overlap" <+> f
+ | otherwise = f
+ Field _ fs ->
+ sep
+ [ "field",
+ vcat (map render fs)
+ ]
+ FunClause lhs rhs wh _ ->
+ sep
+ [ render lhs,
+ render rhs,
+ render wh
+ ]
+ DataSig _ x tel e ->
+ fsep
+ [ hsep
+ [ "data",
+ render x,
+ fcat (map render tel)
+ ],
+ hsep
+ [ ":",
+ render e
+ ]
+ ]
+ Data _ x tel e cs ->
+ fsep
+ [ hsep
+ [ "data",
+ render x,
+ fcat (map render tel)
+ ],
+ hsep
+ [ ":",
+ render e,
+ "where"
+ ],
+ vcat $ map render cs
+ ]
+ DataDef _ x tel cs ->
+ sep
+ [ hsep
+ [ "data",
+ render x,
+ fcat (map render tel)
+ ],
+ "where",
+ vcat $ map render cs
+ ]
+ RecordSig _ x tel e ->
+ sep
+ [ hsep
+ [ "record",
+ render x,
+ fcat (map 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)
+ Syntax n _ -> "syntax" <+> render n <+> "..."
+ PatternSyn _ n as p ->
+ "pattern" <+> render n <+> fsep (map render as)
+ <+> "="
+ <+> render p
+ Mutual _ ds -> namedBlock "mutual" ds
+ Abstract _ ds -> namedBlock "abstract" ds
+ Private _ _ ds -> namedBlock "private" ds
+ InstanceB _ ds -> namedBlock "instance" ds
+ Macro _ ds -> namedBlock "macro" ds
+ Postulate _ ds -> namedBlock "postulate" ds
+ Primitive _ ds -> namedBlock "primitive" ds
+ Generalize _ ds -> namedBlock "variable" ds
+ Module _ x tel ds ->
+ fsep
+ [ hsep
+ [ "module",
+ render x,
+ fcat (map render tel),
+ "where"
+ ],
+ vcat $ map render ds
+ ]
+ ModuleMacro _ x (SectionApp _ [] e) DoOpen i
+ | isNoName x ->
+ fsep
+ [ render DoOpen,
+ render e,
+ render i
+ ]
+ ModuleMacro _ x (SectionApp _ tel e) open i ->
+ fsep
+ [ render open <+> "module" <+> render x <+> fcat (map render tel),
+ "=" <+> render e <+> render i
+ ]
+ ModuleMacro _ x (RecordModuleInstance _ rec) open _ ->
+ fsep
+ [ render open <+> "module" <+> render x,
+ "=" <+> render rec <+> "{{...}}"
+ ]
+ Open _ x i -> hsep ["open", render x, render i]
+ Import _ x rn open i ->
+ hsep [render open, "import", render x, as rn, render i]
+ where
+ as Nothing = mempty
+ as (Just y) = "as" <+> render (asName y)
+ UnquoteDecl _ xs t ->
+ fsep ["unquoteDecl" <+> fsep (map render xs) <+> "=", render t]
+ UnquoteDef _ xs t ->
+ fsep ["unquoteDef" <+> fsep (map render xs) <+> "=", render t]
+ Pragma pr -> sep ["{-#" <+> render pr, "#-}"]
+ where
+ namedBlock s ds =
+ fsep
+ [ text s,
+ vcat $ map render ds
+ ]
+
+pRecord ::
+ Name ->
+ Maybe (Ranged Induction) ->
+ Maybe HasEta ->
+ Maybe (Name, IsInstance) ->
+ [LamBinding] ->
+ Maybe Expr ->
+ [Declaration] ->
+ Inlines
+pRecord x ind eta con tel me cs =
+ sep
+ [ hsep
+ [ "record",
+ render x,
+ fcat (map render tel)
+ ],
+ pType me,
+ vcat $
+ pInd
+ ++ pEta
+ ++ pCon
+ ++ map render cs
+ ]
+ where
+ pType (Just e) =
+ hsep
+ [ ":",
+ render e,
+ "where"
+ ]
+ pType Nothing =
+ "where"
+ pInd = maybeToList $ text . show . rangedThing <$> ind
+ pEta =
+ maybeToList $
+ eta <&> \case
+ YesEta -> "eta-equality"
+ NoEta -> "no-eta-equality"
+ pCon = maybeToList $ (("constructor" <+>) . render) . fst <$> con
+
+instance Render OpenShortHand where
+ render DoOpen = "open"
+ render DontOpen = mempty
+
+instance Render Pragma where
+ render (OptionsPragma _ opts) = fsep $ map text $ "OPTIONS" : opts
+ render (BuiltinPragma _ b x) = hsep ["BUILTIN", text (rangedThing b), render x]
+ render (RewritePragma _ _ xs) =
+ hsep ["REWRITE", hsep $ map 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)
+ render (StaticPragma _ i) =
+ hsep ["STATIC", render i]
+ render (InjectivePragma _ i) =
+ hsep ["INJECTIVE", render i]
+ render (InlinePragma _ True i) =
+ hsep ["INLINE", render i]
+ render (InlinePragma _ False i) =
+ hsep ["NOINLINE", render i]
+ render (ImpossiblePragma _) =
+ hsep ["IMPOSSIBLE"]
+ render (EtaPragma _ x) =
+ hsep ["ETA", render x]
+ render (TerminationCheckPragma _ tc) =
+ case tc of
+ TerminationCheck -> __IMPOSSIBLE__
+ NoTerminationCheck -> "NO_TERMINATION_CHECK"
+ NonTerminating -> "NON_TERMINATING"
+ 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 (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)
+ render (NoUniverseCheckPragma _) = "NO_UNIVERSE_CHECK"
+
+instance Render Fixity where
+ render (Fixity _ Unrelated _) = __IMPOSSIBLE__
+ render (Fixity _ (Related d) ass) = s <+> text (toStringWithoutDotZero d)
+ where
+ s = case ass of
+ LeftAssoc -> "infixl"
+ RightAssoc -> "infixr"
+ NonAssoc -> "infix"
+
+instance Render GenPart where
+ render (IdPart x) = text $ rangedThing x
+ render BindHole {} = "_"
+ render NormalHole {} = "_"
+ render WildHole {} = "_"
+
+instance Render Fixity' where
+ render (Fixity' fix nota _)
+ | nota == noNotation = render fix
+ | otherwise = "syntax" <+> render nota
+
+-- | Arg
+instance Render a => Render (Arg a) where
+ renderPrec p (Arg ai e) = renderHiding ai localParens $ renderPrec p' e
+ where
+ p'
+ | visible ai = p
+ | otherwise = 0
+ localParens
+ | getOrigin ai == Substitution = parens
+ | otherwise = id
+
+-- | Named NamedName (Named_)
+instance Render e => Render (Named NamedName e) where
+ renderPrec p (Named nm e)
+ | Just s <- bareNameOf nm = mparens (p > 0) $ sep [text s <> " =", render e]
+ | otherwise = renderPrec p e
+
+instance Render Pattern where
+ render = \case
+ IdentP x -> render x
+ AppP p1 p2 -> fsep [render p1, render p2]
+ RawAppP _ ps -> fsep $ map render ps
+ OpAppP _ q _ ps -> fsep $ renderOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps)
+ HiddenP _ p -> braces' $ render p
+ InstanceP _ p -> dbraces $ render p
+ ParenP _ p -> parens $ render p
+ WildP _ -> "_"
+ AsP _ x p -> render x <> "@" <> render p
+ DotP _ p -> "." <> render p
+ AbsurdP _ -> "()"
+ LitP l -> render l
+ QuoteP _ -> "quote"
+ RecP _ fs -> sep ["record", bracesAndSemicolons (map render fs)]
+ EqualP _ es -> sep $ [parens (sep [render e1, "=", render e2]) | (e1, e2) <- es]
+ EllipsisP _ -> "..."
+ WithP _ p -> "|" <+> render p
+
+bracesAndSemicolons :: [Inlines] -> Inlines
+bracesAndSemicolons [] = "{}"
+bracesAndSemicolons (d : ds) = sep (["{" <+> d] ++ map (";" <+>) ds ++ ["}"])
+
+renderOpApp ::
+ forall a.
+ Render a =>
+ QName ->
+ [NamedArg (MaybePlaceholder a)] ->
+ [Inlines]
+renderOpApp q args = merge [] $ prOp moduleNames concreteNames args
+ where
+ -- ms: the module part of the name.
+ moduleNames = init (qnameParts q)
+ -- xs: the concrete name (alternation of @Id@ and @Hole@)
+ concreteNames = case unqualify q of
+ Name _ _ xs -> xs
+ NoName {} -> __IMPOSSIBLE__
+
+ prOp :: Render a => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]
+ prOp ms (Hole : xs) (e : es) =
+ case namedArg e of
+ Placeholder p -> (qual ms $ render e, Just p) : prOp [] xs es
+ NoPlaceholder {} -> (render e, Nothing) : prOp ms xs es
+ -- Module qualifier needs to go on section holes (#3072)
+ prOp _ (Hole : _) [] = __IMPOSSIBLE__
+ prOp ms (Id x : xs) es =
+ ( qual ms $ render $ Name noRange InScope [Id x],
+ Nothing
+ ) :
+ prOp [] xs es
+ -- Qualify the name part with the module.
+ -- We then clear @ms@ such that the following name parts will not be qualified.
+
+ prOp _ [] es = map (\e -> (render e, Nothing)) es
+
+ qual ms' doc = hcat $ punctuate "." $ map render ms' ++ [doc]
+
+ -- Section underscores should be printed without surrounding
+ -- whitespace. This function takes care of that.
+ merge :: [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
+ merge before [] = reverse before
+ merge before ((d, Nothing) : after) = merge (d : before) after
+ merge before ((d, Just Beginning) : after) = mergeRight before d after
+ merge before ((d, Just End) : after) = case mergeLeft d before of
+ (d', bs) -> merge (d' : bs) after
+ merge before ((d, Just Middle) : after) = case mergeLeft d before of
+ (d', bs) -> mergeRight bs d' after
+
+ mergeRight before d after =
+ reverse before
+ ++ case merge [] after of
+ [] -> [d]
+ a : as -> (d <> a) : as
+
+ mergeLeft d before = case before of
+ [] -> (d, [])
+ b : bs -> (b <> d, bs)
+
+instance (Render a, Render b) => Render (ImportDirective' a b) where
+ render i =
+ sep
+ [ public (publicOpen i),
+ render $ using i,
+ renderHiding' $ hiding i,
+ rename $ impRenaming i
+ ]
+ where
+ public Just {} = "public"
+ public Nothing = mempty
+
+ renderHiding' [] = mempty
+ renderHiding' xs = "hiding" <+> parens (fsep $ punctuate ";" $ map render xs)
+
+ rename [] = mempty
+ rename xs =
+ hsep
+ [ "renaming",
+ parens $ fsep $ punctuate ";" $ map 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)
+
+instance (Render a, Render b) => Render (Renaming' a b) where
+ render (Renaming from to mfx _r) =
+ hsep
+ [ render from,
+ "to",
+ maybe mempty render mfx,
+ case to of
+ ImportedName a -> render a
+ ImportedModule b -> render b -- don't print "module" here
+ ]
+
+instance (Render a, Render b) => Render (ImportedName' a b) where
+ render (ImportedName a) = render a
+ render (ImportedModule b) = "module" <+> render b
diff --git a/src/Render/Interaction.hs b/src/Render/Interaction.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Interaction.hs
@@ -0,0 +1,124 @@
+{-# 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 ()
+
+--------------------------------------------------------------------------------
+
+-- | 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
+
+-- | 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 (CmpInType cmp expr name1 name2) =
+ render name1
+ <> " "
+ <> render cmp
+ <> " "
+ <> render name2
+ <> " : "
+ <> render expr
+ render (CmpElim pols expr names1 names2) =
+ render names1
+ <> " "
+ <> render pols
+ <> " "
+ <> render names2
+ <> " : "
+ <> render expr
+ render (CmpTypes cmp name1 name2) =
+ render name1
+ <> " "
+ <> render cmp
+ <> " "
+ <> render name2
+ render (CmpLevels cmp name1 name2) =
+ render name1
+ <> " "
+ <> render cmp
+ <> " "
+ <> render name2
+ render (CmpTeles cmp name1 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 (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 <> " := "
+ <> 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 (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'
+ ]
+ render (PTSInstance name1 name2) =
+ "PTS instance for ("
+ <> render name1
+ <> ", "
+ <> render name2
+ <> ")"
+ render (PostponedCheckFunDef name expr) =
+ "Check definition of "
+ <> render name
+ <> " : "
+ <> render expr
+
+-- | 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
+ rhs = case over of
+ Overapplied -> "=" <+> render meta
+ NotOverapplied -> mempty
+ fsep (punctuate "," xs) <+> "⊢" <+> render val <+> rhs
diff --git a/src/Render/Internal.hs b/src/Render/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Internal.hs
@@ -0,0 +1,187 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.Internal where
+
+import Agda.Syntax.Common (Hiding (..), LensHiding (getHiding), Named (namedThing))
+import Agda.Syntax.Internal hiding (telToList)
+import qualified Data.List as List
+import Render.Class
+import Render.Common (renderHiding)
+import Render.Concrete ()
+import Render.RichText
+
+--------------------------------------------------------------------------------
+
+instance Render a => Render (Substitution' a) where
+ renderPrec = pr
+ where
+ pr p input = case input of
+ IdS -> "idS"
+ EmptyS _ -> "emptyS"
+ t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t]
+ Strengthen _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho
+ Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho
+ Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho
+
+-- | Term
+instance Render Term where
+ renderPrec p val =
+ case val of
+ Var x els -> text ("@" ++ show x) `pApp` els
+ Lam ai b ->
+ mparens (p > 0) $
+ fsep
+ [ "λ" <+> renderHiding ai id (text . absName $ b) <+> "->",
+ render (unAbs b)
+ ]
+ Lit l -> render l
+ Def q els -> render q `pApp` els
+ Con c _ vs -> render (conName c) `pApp` vs
+ Pi a (NoAbs _ b) ->
+ mparens (p > 0) $
+ fsep
+ [ renderPrec 1 (unDom a) <+> "->",
+ render b
+ ]
+ Pi a b ->
+ mparens (p > 0) $
+ fsep
+ [ renderDom (domInfo a) (text (absName b) <+> ":" <+> render (unDom a)) <+> "->",
+ render (unAbs b)
+ ]
+ Sort s -> renderPrec p s
+ Level l -> renderPrec p l
+ MetaV x els -> render x `pApp` els
+ DontCare v -> renderPrec p v
+ Dummy s es -> parens (text s) `pApp` es
+ where
+ pApp d els =
+ mparens (not (null els) && p > 9) $
+ fsep [d, fsep (map (renderPrec 10) els)]
+
+instance (Render t, Render e) => Render (Dom' t e) where
+ render dom = pTac <+> renderDom dom (render $ unDom dom)
+ where
+ pTac
+ | Just t <- domTactic dom = "@" <> parens ("tactic" <+> render t)
+ | otherwise = mempty
+
+renderDom :: LensHiding a => a -> Inlines -> Inlines
+renderDom i =
+ case getHiding i of
+ NotHidden -> parens
+ Hidden -> braces
+ Instance {} -> braces . braces
+
+instance Render Clause where
+ render Clause {clauseTel = tel, namedClausePats = ps, clauseBody = body, clauseType = ty} =
+ sep
+ [ render tel <+> "|-",
+ fsep
+ [ fsep (map (renderPrec 10) ps) <+> "=",
+ pBody body ty
+ ]
+ ]
+ where
+ pBody Nothing _ = "(absurd)"
+ pBody (Just b) Nothing = render b
+ pBody (Just b) (Just t) = fsep [render b <+> ":", render t]
+
+instance Render a => Render (Tele (Dom a)) where
+ render tel = fsep [renderDom a (text x <+> ":" <+> render (unDom a)) | (x, a) <- telToList tel]
+ where
+ telToList EmptyTel = []
+ telToList (ExtendTel a tel') = (absName tel', a) : telToList (unAbs tel')
+
+renderPrecLevelSucs :: Int -> Integer -> (Int -> Inlines) -> Inlines
+renderPrecLevelSucs p 0 d = d p
+renderPrecLevelSucs p n d = mparens (p > 9) $ "lsuc" <+> renderPrecLevelSucs 10 (n - 1) d
+
+instance Render Level where
+ renderPrec p (Max n as) =
+ case as of
+ [] -> renderN
+ [a] | n == 0 -> renderPrec p a
+ _ ->
+ mparens (p > 9) $
+ List.foldr1 (\a b -> "lub" <+> a <+> b) $
+ [renderN | n > 0] ++ map (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 Sort where
+ renderPrec p srt =
+ case srt of
+ Type (ClosedLevel 0) -> "Set"
+ Type (ClosedLevel n) -> text $ "Set" ++ show n
+ Type l -> mparens (p > 9) $ "Set" <+> renderPrec 10 l
+ Prop (ClosedLevel 0) -> "Prop"
+ Prop (ClosedLevel n) -> text $ "Prop" ++ show n
+ Prop l -> mparens (p > 9) $ "Prop" <+> renderPrec 10 l
+ Inf -> "Setω"
+ SizeUniv -> "SizeUniv"
+ PiSort a b ->
+ mparens (p > 9) $
+ "piSort" <+> renderDom (domInfo a) (text (absName b) <+> ":" <+> render (unDom a))
+ <+> parens
+ ( fsep
+ [ text ("λ " ++ absName b ++ " ->"),
+ render (unAbs b)
+ ]
+ )
+ FunSort a b ->
+ mparens (p > 9) $
+ "funSort" <+> renderPrec 10 a <+> renderPrec 10 b
+ UnivSort s -> mparens (p > 9) $ "univSort" <+> renderPrec 10 s
+ MetaS x es -> renderPrec p $ MetaV x es
+ DefS d es -> renderPrec p $ Def d es
+ DummyS s -> parens $ text s
+
+instance Render Type where
+ renderPrec p (El _ a) = renderPrec p a
+
+instance Render tm => Render (Elim' tm) where
+ renderPrec p (Apply v) = renderPrec p v
+ renderPrec _ (Proj _o x) = "." <> render x
+ renderPrec p (IApply _ _ r) = renderPrec p r
+
+instance Render DBPatVar where
+ renderPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex x)
+
+instance Render a => Render (Pattern' a) where
+ renderPrec n (VarP _o x) = renderPrec n x
+ renderPrec _ (DotP _o t) = "." <> renderPrec 10 t
+ renderPrec n (ConP c i nps) =
+ mparens (n > 0 && not (null nps)) $
+ (lazy <> render (conName c)) <+> fsep (map (renderPrec 10) ps)
+ where
+ ps = map (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)
+ where
+ ps = map (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)
+ -- 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
diff --git a/src/Render/Literal.hs b/src/Render/Literal.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Literal.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.Literal where
+
+import Agda.Syntax.Literal
+import Render.Class
+import Render.RichText
+import Render.Name ()
+import Render.Common ()
+
+--------------------------------------------------------------------------------
+
+-- | 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
diff --git a/src/Render/Name.hs b/src/Render/Name.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Name.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.Name where
+
+import qualified Agda.Syntax.Abstract as A
+import qualified Agda.Syntax.Concrete as C
+import Render.Class
+import Render.RichText
+import qualified Agda.Syntax.Common as C
+
+
+--------------------------------------------------------------------------------
+
+-- | Concrete
+instance Render C.NamePart where
+ render C.Hole = "_"
+ render (C.Id s) = text $ C.rawNameToString s
+
+-- glueing name parts together
+instance Render C.Name where
+ render (C.Name range _inScope xs) = linkRange range $ mconcat (map render xs)
+ render (C.NoName _ _) = "_"
+
+instance Render C.QName where
+ render (C.Qual m x)
+ | C.isUnderscore m = render x -- don't print anonymous modules
+ | otherwise = render m <> "." <> render x
+ render (C.QName x) = render x
+
+
+--------------------------------------------------------------------------------
+
+-- | Abstract
+instance Render A.Name where
+ render = render . A.nameConcrete
+
+instance Render A.QName where
+ render = hcat . punctuate "." . map render . A.qnameToList
diff --git a/src/Render/Position.hs b/src/Render/Position.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Position.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.Position where
+
+import Agda.Syntax.Position
+import Agda.Utils.FileName
+import qualified Data.Strict.Maybe as Strict
+import Render.Class
+import Render.RichText
+
+instance Render AbsolutePath where
+ render = text . filePath
+
+--------------------------------------------------------------------------------
+
+instance Render a => Render (Position' (Strict.Maybe a)) where
+ render (Pn Strict.Nothing _ l c) = render l <> "," <> render c
+ render (Pn (Strict.Just f) _ l c) =
+ render f <> ":" <> render l <> "," <> render c
+
+instance Render PositionWithoutFile where
+ render p = render (p {srcFile = Strict.Nothing} :: Position)
+
+instance Render IntervalWithoutFile where
+ render (Interval s e) = start <> "-" <> end
+ where
+ sl = posLine s
+ el = posLine e
+ sc = posCol s
+ ec = posCol e
+
+ start = render sl <> "," <> render sc
+
+ end
+ | sl == el = render ec
+ | otherwise = render el <> "," <> render ec
+
+instance Render a => Render (Interval' (Strict.Maybe a)) where
+ render i@(Interval s _) = file <> render (setIntervalFile () i)
+ where
+ file :: Inlines
+ file = case srcFile s of
+ Strict.Nothing -> mempty
+ Strict.Just f -> render f <> ":"
+
+instance Render a => Render (Range' (Strict.Maybe a)) where
+ render r = maybe mempty render (rangeToIntervalWithFile r)
diff --git a/src/Render/RichText.hs b/src/Render/RichText.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/RichText.hs
@@ -0,0 +1,333 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.RichText
+ ( Block(..),
+ Inlines (..),
+ -- LinkTarget (..),
+ space,
+ text,
+ text',
+ parens,
+ -- link,
+ linkRange,
+ linkHole,
+ icon,
+ -- combinators
+ (<+>),
+ punctuate,
+ braces,
+ braces',
+ dbraces,
+ mparens,
+ hcat,
+ hsep,
+ sep,
+ fsep,
+ vcat,
+ fcat,
+ -- symbols
+ arrow,
+ lambda,
+ forallQ,
+ showIndex,
+ leftIdiomBrkt,
+ rightIdiomBrkt,
+ emptyIdiomBrkt,
+ )
+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 Data.Strict.Maybe as Strict
+import Data.String (IsString (..))
+import GHC.Generics (Generic)
+import qualified GHC.IO.Unsafe as UNSAFE
+
+--------------------------------------------------------------------------------
+-- | Block elements
+
+data Block
+ -- for blocks like "Goal" & "Have"
+ = Labeled Inlines (Maybe String) (Maybe Agda.Range) String String
+ -- for ordinary goals & context
+ | Unlabeled Inlines (Maybe String) (Maybe Agda.Range)
+ -- headers
+ | Header String
+ deriving (Generic)
+
+instance ToJSON Block
+
+--------------------------------------------------------------------------------
+
+newtype Inlines = Inlines {unInlines :: Seq Inline}
+
+-- Represent Inlines with String literals
+instance IsString Inlines where
+ fromString s = Inlines (Seq.singleton (Text s mempty))
+
+instance Semigroup Inlines where
+ Inlines as <> Inlines bs = Inlines (merge as bs)
+ where
+ merge :: Seq Inline -> Seq Inline -> Seq Inline
+ merge Empty ys = ys
+ merge (xs :|> x) ys = merge xs (cons x ys)
+
+ cons :: Inline -> Seq Inline -> Seq Inline
+ cons (Text s c) (Text t d :<| xs)
+ -- merge 2 adjacent Text if they have the same classnames
+ | c == d = Text (s <> t) c :<| xs
+ | otherwise = Text s c :<| Text t d :<| xs
+ cons (Text s c) (Horz [] :<| xs) = cons (Text s c) xs
+ cons (Text s c) (Horz (Inlines t:ts) :<| xs)
+ -- merge Text with Horz when possible
+ = Horz (Inlines (cons (Text s c) t) :ts) :<| xs
+ cons x xs = x :<| xs
+
+
+instance Monoid Inlines where
+ mempty = Inlines mempty
+
+instance ToJSON Inlines where
+ toJSON (Inlines xs) = toJSON xs
+
+instance Show Inlines where
+ show (Inlines xs) = unwords $ map show $ toList xs
+
+-- | see if the rendered text is "empty"
+isEmpty :: Inlines -> Bool
+isEmpty (Inlines elems) = all elemIsEmpty (Seq.viewl elems)
+ where
+ elemIsEmpty :: Inline -> Bool
+ elemIsEmpty (Icon _ _) = False
+ elemIsEmpty (Text "" _) = True
+ elemIsEmpty (Text _ _) = False
+ elemIsEmpty (Link _ xs _) = all elemIsEmpty $ unInlines xs
+ elemIsEmpty (Hole _) = False
+ elemIsEmpty (Horz xs) = all isEmpty xs
+ elemIsEmpty (Vert xs) = all isEmpty xs
+ elemIsEmpty (Parn _) = False
+ elemIsEmpty (PrHz _) = False
+
+infixr 6 <+>
+
+(<+>) :: Inlines -> Inlines -> Inlines
+x <+> y
+ | isEmpty x = y
+ | isEmpty y = x
+ | otherwise = x <> " " <> y
+
+-- | Whitespace
+space :: Inlines
+space = " "
+
+text :: String -> Inlines
+text s = Inlines $ Seq.singleton $ Text s mempty
+
+text' :: ClassNames -> String -> Inlines
+text' cs s = Inlines $ Seq.singleton $ Text s cs
+
+-- When there's only 1 Horz inside a Parn, convert it to PrHz
+parens :: Inlines -> Inlines
+parens (Inlines (Horz xs :<| Empty)) = Inlines $ Seq.singleton $ PrHz xs
+parens others = Inlines $ Seq.singleton $ Parn others
+
+icon :: String -> Inlines
+icon s = Inlines $ Seq.singleton $ Icon s []
+
+linkRange :: Agda.Range -> Inlines -> Inlines
+linkRange range xs = Inlines $ Seq.singleton $ Link range xs mempty
+
+linkHole :: Int -> Inlines
+linkHole i = Inlines $ Seq.singleton $ Hole i
+
+--------------------------------------------------------------------------------
+
+type ClassNames = [String]
+
+--------------------------------------------------------------------------------
+
+-- | Internal type, to be converted to JSON values
+data Inline
+ = Icon String ClassNames
+ | Text String ClassNames
+ | Link Agda.Range Inlines ClassNames
+ | Hole Int
+ | -- | Horizontal grouping, wrap when there's no space
+ Horz [Inlines]
+ | -- | Vertical grouping, each children would end with a newline
+ Vert [Inlines]
+ | -- | Parenthese
+ Parn Inlines
+ | -- | Parenthese around a Horizontal, special case
+ PrHz [Inlines]
+ deriving (Generic)
+
+instance ToJSON Inline
+
+instance Show Inline where
+ show (Icon s _) = s
+ show (Text s _) = s
+ show (Link _ xs _) = mconcat (map show $ toList $ unInlines xs)
+ show (Hole i) = "?" ++ show i
+ show (Horz xs) = unwords (map show $ toList xs)
+ show (Vert xs) = unlines (map show $ toList xs)
+ show (Parn x) = "(" <> show x <> ")"
+ show (PrHz xs) = "(" <> unwords (map show $ toList xs) <> ")"
+
+--------------------------------------------------------------------------------
+
+-- | ToJSON instances for Agda types
+instance ToJSON Agda.Range
+
+instance ToJSON (Agda.Interval' ()) where
+ toJSON (Agda.Interval start end) = toJSON (start, end)
+
+instance ToJSON (Agda.Position' ()) where
+ toJSON (Agda.Pn () pos line col) = toJSON [line, col, pos]
+
+instance ToJSON Agda.SrcFile where
+ toJSON Strict.Nothing = Null
+ toJSON (Strict.Just path) = toJSON path
+
+instance ToJSON Agda.AbsolutePath where
+ toJSON (Agda.AbsolutePath path) = toJSON path
+
+--------------------------------------------------------------------------------
+
+-- | Utilities / Combinators
+
+-- -- TODO: implement this
+-- indent :: Inlines -> Inlines
+-- indent x = " " <> x
+
+punctuate :: Inlines -> [Inlines] -> [Inlines]
+punctuate _ [] = []
+punctuate delim xs = zipWith (<>) xs (replicate (length xs - 1) delim ++ [mempty])
+
+--------------------------------------------------------------------------------
+
+-- | Just pure concatenation, no grouping or whatsoever
+hcat :: [Inlines] -> Inlines
+hcat = mconcat
+
+hsep :: [Inlines] -> Inlines
+hsep [] = mempty
+hsep [x] = x
+hsep (x : xs) = x <+> hsep xs
+
+--------------------------------------------------------------------------------
+
+-- | Vertical listing
+vcat :: [Inlines] -> Inlines
+vcat = Inlines . pure . Vert
+
+-- | Horizontal listing
+sep :: [Inlines] -> Inlines
+sep = Inlines . pure . Horz
+
+fsep :: [Inlines] -> Inlines
+fsep = sep
+
+fcat :: [Inlines] -> Inlines
+fcat = sep
+
+--------------------------------------------------------------------------------
+
+-- | Single braces
+braces :: Inlines -> Inlines
+braces x = "{" <> x <> "}"
+
+-- | Double braces
+dbraces :: Inlines -> Inlines
+dbraces = _dbraces specialCharacters
+
+arrow :: Inlines
+arrow = _arrow specialCharacters
+
+lambda :: Inlines
+lambda = _lambda specialCharacters
+
+forallQ :: Inlines
+forallQ = _forallQ specialCharacters
+
+-- left, right, and empty idiom bracket
+leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Inlines
+leftIdiomBrkt = _leftIdiomBrkt specialCharacters
+rightIdiomBrkt = _rightIdiomBrkt specialCharacters
+emptyIdiomBrkt = _emptyIdiomBrkt specialCharacters
+
+-- | Apply 'parens' to 'Doc' if boolean is true.
+mparens :: Bool -> Inlines -> Inlines
+mparens True = parens
+mparens False = id
+
+-- | From braces'
+braces' :: Inlines -> Inlines
+braces' d =
+ let s = show d
+ in if Agda.null s
+ then braces d
+ else braces (spaceIfDash (head s) <> d <> spaceIfDash (last s))
+ where
+ -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269)
+ -- Andreas, 2018-07-21, #3161: Also avoid ending a comment
+ spaceIfDash '-' = " "
+ spaceIfDash _ = mempty
+
+-- | 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
+
+--------------------------------------------------------------------------------
+
+-- | Picking the appropriate set of special characters depending on
+-- whether we are allowed to use unicode or have to limit ourselves
+-- to ascii.
+data SpecialCharacters = SpecialCharacters
+ { _dbraces :: Inlines -> Inlines,
+ _lambda :: Inlines,
+ _arrow :: Inlines,
+ _forallQ :: Inlines,
+ _leftIdiomBrkt :: Inlines,
+ _rightIdiomBrkt :: Inlines,
+ _emptyIdiomBrkt :: Inlines
+ }
+
+{-# 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 = "(|)"
+ }
diff --git a/src/Render/TypeChecking.hs b/src/Render/TypeChecking.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/TypeChecking.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Render.TypeChecking where
+
+import Agda.Syntax.Common
+import Agda.TypeChecking.Monad.Base
+import Agda.TypeChecking.Positivity.Occurrence
+import Render.Class
+import Render.RichText
+
+instance Render NamedMeta where
+ render (NamedMeta "" (MetaId x)) = render x
+ render (NamedMeta "_" (MetaId x)) = render x
+ render (NamedMeta s (MetaId x)) = "_" <> text s <> render x
+
+instance Render Occurrence where
+ render =
+ text . \case
+ Unused -> "_"
+ Mixed -> "*"
+ JustNeg -> "-"
+ JustPos -> "+"
+ StrictPos -> "++"
+ GuardPos -> "g+"
+
+instance Render ProblemId where
+ render (ProblemId n) = render n
+
+instance Render Comparison where
+ render CmpEq = "="
+ render CmpLeq = "=<"
+
+instance Render Polarity where
+ render =
+ text . \case
+ Covariant -> "+"
+ Contravariant -> "-"
+ Invariant -> "*"
+ Nonvariant -> "_"
diff --git a/src/Render/Utils.hs b/src/Render/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Render/Utils.hs
@@ -0,0 +1,9 @@
+module Render.Utils where
+
+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
new file mode 100644
--- /dev/null
+++ b/src/Server.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module Server (run) where
+
+-- entry point of the LSP server
+
+import Monad
+import Control.Monad.Reader
+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 qualified Switchboard
+import Switchboard (Switchboard)
+import Control.Concurrent
+
+import Agda.Misc (onHover)
+import Data.Maybe (isJust)
+
+--------------------------------------------------------------------------------
+
+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
+ 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
+ }
+
+ -- 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
+ }
+
+ 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 = 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,
+ -- 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)
+
+instance ToJSON CommandErr
diff --git a/src/Server/CommandController.hs b/src/Server/CommandController.hs
new file mode 100644
--- /dev/null
+++ b/src/Server/CommandController.hs
@@ -0,0 +1,44 @@
+module Server.CommandController
+ ( CommandController,
+ new,
+ take,
+ release,
+ put,
+ )
+where
+
+import Agda.Interaction.Base (IOTCM)
+import Control.Concurrent
+import Control.Concurrent.SizedChan
+import Control.Monad (forM_)
+import Prelude hiding (take)
+
+data CommandController
+ = CommandController
+ (SizedChan IOTCM)
+ -- ^ Unbounded Command queue
+ (MVar IOTCM)
+ -- ^ MVar for the Command consumer
+
+new :: IO CommandController
+new = CommandController <$> newSizedChan <*> newEmptyMVar
+
+-- | Blocks if the front is empty
+take :: CommandController -> IO IOTCM
+take (CommandController _ front) = takeMVar front
+
+-- | Move the payload from the queue to the front
+-- Does not block if the front or the queue is empty
+release :: CommandController -> IO ()
+release (CommandController queue front) = do
+ result <- tryReadSizedChan queue
+ forM_ result (tryPutMVar front)
+
+-- | Does not block
+-- Move the payload to the front if the front is empty
+put :: CommandController -> IOTCM -> IO ()
+put (CommandController queue front) command = do
+ isEmpty <- isEmptyMVar front
+ if isEmpty
+ then putMVar front command
+ else writeSizedChan queue command
diff --git a/src/Server/ResponseController.hs b/src/Server/ResponseController.hs
new file mode 100644
--- /dev/null
+++ b/src/Server/ResponseController.hs
@@ -0,0 +1,75 @@
+-- |
+-- Makes sure that all dispatched works are done.
+-- Notify when all dispatched works are done.
+module Server.ResponseController where
+
+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,
+ -- | The number of work completed
+ completedCount :: IORef Int,
+ -- | A channel of "Checkpoints" to be met
+ checkpointChan :: SizedChan Checkpoint
+ }
+
+-- | An "Checkpoint" is just a number with a callback, the callback will be invoked once the number is "met"
+type Checkpoint = (Int, () -> IO ())
+
+-- | Constructs a new ResponseController
+new :: IO ResponseController
+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.
+dispatch :: ResponseController -> IO (() -> IO ())
+dispatch controller = do
+ -- bump `dispatchedCount`
+ modifyIORef' (dispatchedCount controller) succ
+ return $ \() -> do
+ -- work completed, bump `completedCount`
+ modifyIORef' (completedCount controller) succ
+
+ -- see if there's any Checkpoint
+ result <- tryPeekSizedChan (checkpointChan controller)
+ case result of
+ -- no checkpoints, do nothing
+ Nothing -> return ()
+ -- a checkpoint is set!
+ Just (dispatched, callback) -> do
+ completed <- readIORef (completedCount controller)
+ -- see if the checkpoint is met
+ when (dispatched == completed) $ do
+ -- invoke the callback and remove the checkpoint
+ callback ()
+ void $ readSizedChan (checkpointChan controller)
+
+-- | Expects a callback, which will be invoked once all works dispatched BEFORE have been completed
+-- This function is non-blocking
+setCheckpoint :: ResponseController -> (() -> IO ()) -> IO ()
+setCheckpoint controller callback = do
+ dispatched <- readIORef (dispatchedCount controller)
+ completed <- readIORef (completedCount controller)
+ -- see if the previously dispatched works have been completed
+ if dispatched == completed
+ then callback ()
+ else do
+ -- constructs a Checkpoint from `dispatchedCount`
+ let checkpoint = (dispatched, callback)
+ -- write it to the channel
+ writeSizedChan (checkpointChan controller) checkpoint
+
+-- | The blocking version of `setCheckpoint`
+setCheckpointAndWait :: ResponseController -> IO ()
+setCheckpointAndWait controller = do
+ mvar <- newEmptyMVar
+ setCheckpoint controller (putMVar mvar)
+ takeMVar mvar
diff --git a/src/Switchboard.hs b/src/Switchboard.hs
new file mode 100644
--- /dev/null
+++ b/src/Switchboard.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE OverloadedStrings #-}
+
+module Switchboard (Switchboard, new, setupLanguageContextEnv, destroy) where
+
+import Monad
+import Control.Concurrent
+import qualified Server.ResponseController as ResponseController
+import Control.Monad.Reader
+import qualified Agda
+import qualified Data.Aeson as JSON
+import qualified Data.Text.IO as Text
+import Language.LSP.Server
+import Language.LSP.Types hiding (TextDocumentSyncClientCapabilities (..))
+import Data.IORef
+
+data Switchboard = Switchboard
+ { sbPrintLog :: ThreadId
+ , sbSendResponse :: ThreadId
+ , sbRunAgda :: ThreadId
+ , sbLanguageContextEnv :: IORef (Maybe (LanguageContextEnv ()))
+ }
+
+-- | All channels go in and out from here
+new :: Env -> IO Switchboard
+new env = do
+ ctxEnvIORef <- newIORef Nothing
+ Switchboard
+ <$> forkIO (keepPrintingLog env)
+ <*> forkIO (keepSendindResponse env ctxEnvIORef)
+ <*> forkIO (runReaderT Agda.interact env)
+ <*> pure ctxEnvIORef
+
+-- | For sending reactions to the client
+setupLanguageContextEnv :: Switchboard -> LanguageContextEnv () -> IO ()
+setupLanguageContextEnv switchboard ctxEnv = do
+ writeIORef (sbLanguageContextEnv switchboard) (Just ctxEnv)
+
+destroy :: Switchboard -> IO ()
+destroy switchboard = do
+ killThread (sbPrintLog switchboard)
+ killThread (sbSendResponse switchboard)
+ killThread (sbRunAgda switchboard)
+ writeIORef (sbLanguageContextEnv switchboard) Nothing
+
+-- | Keep printing log
+-- Consumer of `envLogChan`
+keepPrintingLog :: Env -> IO ()
+keepPrintingLog env = forever $ do
+ result <- readChan (envLogChan env)
+ when (envDevMode env) $ do
+ Text.putStrLn result
+
+-- | Keep sending reactions
+-- Consumer of `envResponseChan`
+keepSendindResponse :: Env -> IORef (Maybe (LanguageContextEnv ())) -> IO ()
+keepSendindResponse env ctxEnvIORef = forever $ do
+ response <- readChan (envResponseChan env)
+
+ result <- readIORef ctxEnvIORef
+ forM_ result $ \ctxEnv -> do
+ runLspT ctxEnv $ do
+ callback <- liftIO $ ResponseController.dispatch (envResponseController env)
+
+ let value = JSON.toJSON response
+ sendRequest (SCustomMethod "agda") value $ \_result -> liftIO $ do
+ -- writeChan (envLogChan env) $ "[Response] >>>> " <> pack (show value)
+ callback ()
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,2 @@
+main :: IO ()
+main = putStrLn "Test suite not yet implemented"