agda-language-server (empty) → 0.0.3.0
raw patch · 31 files changed
+3479/−0 lines, 31 filesdep +Agdadep +aesondep +agda-language-serversetup-changed
Dependencies added: Agda, aeson, agda-language-server, base, bytestring, containers, lsp, mtl, network, network-simple, process, stm, strict, text
Files
- CHANGELOG.md +0/−0
- LICENSE +21/−0
- README.md +55/−0
- Setup.hs +2/−0
- agda-language-server.cabal +123/−0
- app/Main.hs +50/−0
- src/Agda.hs +109/−0
- src/Agda/Convert.hs +628/−0
- src/Agda/IR.hs +101/−0
- src/Agda/Misc.hs +89/−0
- src/Agda/Parser.hs +56/−0
- src/Agda/Position.hs +87/−0
- src/Control/Concurrent/SizedChan.hs +99/−0
- src/Monad.hs +81/−0
- src/Render.hs +16/−0
- src/Render/Class.hs +70/−0
- src/Render/Common.hs +90/−0
- src/Render/Concrete.hs +678/−0
- src/Render/Interaction.hs +124/−0
- src/Render/Internal.hs +187/−0
- src/Render/Literal.hs +21/−0
- src/Render/Name.hs +38/−0
- src/Render/Position.hs +48/−0
- src/Render/RichText.hs +333/−0
- src/Render/TypeChecking.hs +40/−0
- src/Render/Utils.hs +9/−0
- src/Server.hs +136/−0
- src/Server/CommandController.hs +44/−0
- src/Server/ResponseController.hs +75/−0
- src/Switchboard.hs +67/−0
- test/Spec.hs +2/−0
+ CHANGELOG.md view
+ LICENSE view
@@ -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.
+ README.md view
@@ -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 (<kbd>C-c</kbd> <kbd>C-l</kbd>)+++++## 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
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ agda-language-server.cabal view
@@ -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 <https://github.com/banacorn/agda-language-server#readme>+category: Development+homepage: https://github.com/banacorn/agda-language-server#readme+bug-reports: https://github.com/banacorn/agda-language-server/issues+author: Ting-gan LUA+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
+ app/Main.hs view
@@ -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
+ src/Agda.hs view
@@ -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
+ src/Agda/Convert.hs view
@@ -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
+ src/Agda/IR.hs view
@@ -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
+ src/Agda/Misc.hs view
@@ -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)
+ src/Agda/Parser.hs view
@@ -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))
+ src/Agda/Position.hs view
@@ -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)
+ src/Control/Concurrent/SizedChan.hs view
@@ -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
+ src/Monad.hs view
@@ -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
+ src/Render.hs view
@@ -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 ()
+ src/Render/Class.hs view
@@ -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)) <> "]"
+ src/Render/Common.hs view
@@ -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
+ src/Render/Concrete.hs view
@@ -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
+ src/Render/Interaction.hs view
@@ -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
+ src/Render/Internal.hs view
@@ -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
+ src/Render/Literal.hs view
@@ -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
+ src/Render/Name.hs view
@@ -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
+ src/Render/Position.hs view
@@ -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)
+ src/Render/RichText.hs view
@@ -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 = "(|)"+ }
+ src/Render/TypeChecking.hs view
@@ -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 -> "_"
+ src/Render/Utils.hs view
@@ -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
+ src/Server.hs view
@@ -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
+ src/Server/CommandController.hs view
@@ -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
+ src/Server/ResponseController.hs view
@@ -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
+ src/Switchboard.hs view
@@ -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 ()
+ test/Spec.hs view
@@ -0,0 +1,2 @@+main :: IO ()+main = putStrLn "Test suite not yet implemented"