diff --git a/.gitignore b/.gitignore index 14ce36d..c978c7c 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,7 @@ cabal-dev dist dist-* +test/data/AST/ node_modules/ *.o *.hi diff --git a/agda-language-server.cabal b/agda-language-server.cabal index 378b857..eefadc2 100644 --- a/agda-language-server.cabal +++ b/agda-language-server.cabal @@ -1,6 +1,6 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.37.0. +-- This file has been generated from package.yaml by hpack version 0.38.1. -- -- see: https://github.com/sol/hpack @@ -49,10 +49,22 @@ library exposed-modules: Agda Agda.Convert + Agda.Interaction.Imports.More + Agda.Interaction.Imports.Virtual + Agda.Interaction.Library.More + Agda.Interaction.Library.Parse.More Agda.IR Agda.Parser Agda.Position + Agda.Syntax.Abstract.More + Agda.TypeChecking.Monad.Options.More Control.Concurrent.SizedChan + Indexer + Indexer.Indexer + Indexer.Monad + Indexer.Postprocess + Language.LSP.Protocol.Types.More + Language.LSP.Protocol.Types.Uri.More Monad Options Render @@ -68,9 +80,20 @@ library Render.TypeChecking Render.Utils Server + Server.AgdaLibResolver Server.CommandController + Server.Filesystem Server.Handler + Server.Handler.TextDocument.DocumentSymbol + Server.Handler.TextDocument.FileManagement + Server.Model + Server.Model.AgdaFile + Server.Model.AgdaLib + Server.Model.Handler + Server.Model.Monad + Server.Model.Symbol Server.ResponseController + Server.VfsIndex Switchboard other-modules: Paths_agda_language_server @@ -92,6 +115,7 @@ library , filepath , lsp >=2 , lsp-types >=2 + , modern-uri , mtl , network , network-simple ==0.4.2 @@ -139,6 +163,7 @@ executable als , filepath , lsp >=2 , lsp-types >=2 + , modern-uri , mtl , network , network-simple ==0.4.2 @@ -160,23 +185,46 @@ executable als if arch(wasm32) build-depends: unix >=2.8.0.0 && <2.9 - ghc-options: -with-rtsopts=-V1 - else + if !arch(wasm32) ghc-options: -threaded -with-rtsopts=-N test-suite als-test type: exitcode-stdio-1.0 main-is: Test.hs other-modules: + Test.AgdaLibResolution + Test.Indexer + Test.Indexer.Invariants + Test.Indexer.Invariants.NoDuplicateDecl + Test.Indexer.Invariants.NoMissing + Test.Indexer.Invariants.NoOverlap + Test.Indexer.NoAnonFunSymbol + Test.Indexer.Reload Test.LSP + Test.Model + Test.ModelMonad Test.SrcLoc + Test.Uri Test.WASM + TestData Agda Agda.Convert + Agda.Interaction.Imports.More + Agda.Interaction.Imports.Virtual + Agda.Interaction.Library.More + Agda.Interaction.Library.Parse.More Agda.IR Agda.Parser Agda.Position + Agda.Syntax.Abstract.More + Agda.TypeChecking.Monad.Options.More Control.Concurrent.SizedChan + Indexer + Indexer.Indexer + Indexer.Monad + Indexer.Postprocess + Language.LSP.Protocol.Types.More + Language.LSP.Protocol.Types.Uri.More Monad Options Render @@ -192,9 +240,20 @@ test-suite als-test Render.TypeChecking Render.Utils Server + Server.AgdaLibResolver Server.CommandController + Server.Filesystem Server.Handler + Server.Handler.TextDocument.DocumentSymbol + Server.Handler.TextDocument.FileManagement + Server.Model + Server.Model.AgdaFile + Server.Model.AgdaLib + Server.Model.Handler + Server.Model.Monad + Server.Model.Symbol Server.ResponseController + Server.VfsIndex Switchboard Paths_agda_language_server hs-source-dirs: @@ -217,6 +276,7 @@ test-suite als-test , lsp >=2 , lsp-test , lsp-types >=2 + , modern-uri , mtl , network , network-simple ==0.4.2 @@ -242,6 +302,5 @@ test-suite als-test if arch(wasm32) build-depends: unix >=2.8.0.0 && <2.9 - ghc-options: -with-rtsopts=-V1 - else + if !arch(wasm32) ghc-options: -threaded -with-rtsopts=-N diff --git a/package.yaml b/package.yaml index b0fe8d9..2db68d3 100644 --- a/package.yaml +++ b/package.yaml @@ -62,6 +62,7 @@ dependencies: - filepath - lsp-types >= 2 - lsp >= 2 + - modern-uri - mtl - network - network-simple == 0.4.2 diff --git a/src/Agda.hs b/src/Agda.hs index 53f7330..ff053b1 100644 --- a/src/Agda.hs +++ b/src/Agda.hs @@ -99,7 +99,7 @@ import Agda.Interaction.JSONTop () getAgdaVersion :: String getAgdaVersion = versionWithCommitInfo -start :: ServerM IO () +start :: ServerT IO () start = do env <- ask @@ -136,7 +136,7 @@ start = do Left _err -> return () Right _val -> return () where - loop :: Env -> ServerM CommandM () + loop :: Env -> ServerT CommandM () loop env = do Bench.reset done <- Bench.billTo [] $ do @@ -163,7 +163,7 @@ start = do -- | Convert "CommandReq" to "CommandRes" -sendCommand :: MonadIO m => Value -> ServerM m Value +sendCommand :: MonadIO m => Value -> ServerT m Value sendCommand value = do -- JSON Value => Request => Response case fromJSON value of @@ -179,7 +179,7 @@ sendCommand value = do JSON.Success request -> toJSON <$> handleCommandReq request -handleCommandReq :: MonadIO m => CommandReq -> ServerM m CommandRes +handleCommandReq :: MonadIO m => CommandReq -> ServerT m CommandRes handleCommandReq CmdReqSYN = return $ CmdResACK Agda.getAgdaVersion versionNumber handleCommandReq (CmdReq cmd) = do case parseIOTCM cmd of @@ -194,7 +194,7 @@ handleCommandReq (CmdReq cmd) = do -------------------------------------------------------------------------------- getCommandLineOptions - :: (HasOptions m, MonadIO m) => ServerM m CommandLineOptions + :: (HasOptions m, MonadIO m) => ServerT m CommandLineOptions getCommandLineOptions = do -- command line options from ARGV argv <- asks (optRawAgdaOptions . envOptions) @@ -215,10 +215,10 @@ getCommandLineOptions = do -- | Run a TCM action in IO and throw away all of the errors -- TODO: handle the caught errors -runAgda :: MonadIO m => ServerM TCM a -> ServerM m (Either String a) +runAgda :: MonadIO m => ServerT TCM a -> ServerT m (Either String a) runAgda p = do env <- ask - let p' = runServerM env p + let p' = runServerT env p liftIO $ runTCMTop' ( (Right <$> p') diff --git a/src/Agda/Interaction/Imports/More.hs b/src/Agda/Interaction/Imports/More.hs new file mode 100644 index 0000000..1c2b374 --- /dev/null +++ b/src/Agda/Interaction/Imports/More.hs @@ -0,0 +1,209 @@ +{-# LANGUAGE CPP #-} + +module Agda.Interaction.Imports.More + ( setOptionsFromSourcePragmas, + checkModuleName', + runPMDropWarnings, + moduleName, + runPM, + beginningOfFile, + ) +where + +import Agda.Interaction.FindFile ( + SourceFile (SourceFile), + checkModuleName, +#if MIN_VERSION_Agda(2,8,0) + rootNameModule, +#else + moduleName, +#endif + ) +import Agda.Interaction.Imports (Source (..)) +import qualified Agda.Interaction.Imports as Imp +import Agda.Interaction.Library (OptionsPragma (..), _libPragmas) +import Agda.Interaction.Library.More () +import Agda.Syntax.Common (TopLevelModuleName') +import qualified Agda.Syntax.Concrete as C +import Agda.Syntax.Parser ( + moduleParser, + parseFile, +#if MIN_VERSION_Agda(2,8,0) + parse, + moduleNameParser, +#else + PM, + runPMIO, +#endif + ) +import Agda.Syntax.Position + ( Range, + Range' (Range), + RangeFile, + getRange, + intervalToRange, + mkRangeFile, + posToRange, + posToRange', + startPos, +#if MIN_VERSION_Agda(2,8,0) + beginningOfFile, + rangeFromAbsolutePath, +#endif + ) +import Agda.Syntax.TopLevelModuleName ( + TopLevelModuleName, + RawTopLevelModuleName (..), +#if MIN_VERSION_Agda(2,8,0) + rawTopLevelModuleNameForModule, +#endif + ) +import Agda.Syntax.Common.Pretty (Pretty, pretty, text, prettyAssign, (<+>)) +import Agda.TypeChecking.Monad + ( Interface, + TCM, + setCurrentRange, + setOptionsFromPragma, + setTCLens, + stPragmaOptions, + useTC, +#if MIN_VERSION_Agda(2,7,0) + checkAndSetOptionsFromPragma, +#endif +#if MIN_VERSION_Agda(2,8,0) + runPM, + runPMDropWarnings, +#endif + ) +import qualified Agda.TypeChecking.Monad as TCM +import qualified Agda.TypeChecking.Monad.Benchmark as Bench +#if MIN_VERSION_Agda(2,8,0) +#else +import Agda.TypeChecking.Warnings (runPM) +#endif +import Agda.Utils.FileName (AbsolutePath) +import Agda.Utils.Monad (bracket_) +#if MIN_VERSION_Agda(2,8,0) +import qualified Data.Text as T +#endif +import qualified Data.Text.Lazy as TL +import Control.Monad.Error.Class ( +#if MIN_VERSION_Agda(2,8,0) + catchError, +#else + throwError, +#endif + ) +#if MIN_VERSION_Agda(2,8,0) +import Agda.Utils.Singleton (singleton) +#endif + +srcFilePath :: SourceFile -> TCM AbsolutePath +#if MIN_VERSION_Agda(2,8,0) +srcFilePath = TCM.srcFilePath +#else +srcFilePath (SourceFile f) = return f +#endif + +#if MIN_VERSION_Agda(2,8,0) +-- beginningOfFile was generalized in Agda 2.8.0 to support the features we +-- need, so we just import it +#else +beginningOfFile :: RangeFile -> Range +beginningOfFile rf = posToRange (startPos $ Just rf) (startPos $ Just rf) +#endif + +#if MIN_VERSION_Agda(2,8,0) +-- runPMDropWarnings was introduced in Agda 2.8.0, so we just import it +#else +runPMDropWarnings :: PM a -> TCM a +runPMDropWarnings m = do + (res, _ws) <- runPMIO m + case res of + Left e -> throwError $ TCM.Exception (getRange e) (pretty e) + Right a -> return a +#endif + +-- Unexported Agda functions + +srcDefaultPragmas :: Imp.Source -> [OptionsPragma] +srcDefaultPragmas src = map _libPragmas (Imp.srcProjectLibs src) + +srcFilePragmas :: Imp.Source -> [OptionsPragma] +srcFilePragmas src = pragmas + where + cpragmas = C.modPragmas (Imp.srcModule src) + pragmas = + [ OptionsPragma + { pragmaStrings = opts, + pragmaRange = r + } + | C.OptionsPragma r opts <- cpragmas + ] + +-- | Set options from a 'Source' pragma, using the source +-- ranges of the pragmas for error reporting. Flag to check consistency. +setOptionsFromSourcePragmas :: Bool -> Imp.Source -> TCM () +setOptionsFromSourcePragmas checkOpts src = do + mapM_ setOpts (srcDefaultPragmas src) + mapM_ setOpts (srcFilePragmas src) + where +#if MIN_VERSION_Agda(2,7,0) + setOpts + | checkOpts = checkAndSetOptionsFromPragma + | otherwise = setOptionsFromPragma +#else + setOpts = setOptionsFromPragma +#endif + +-- Andreas, 2016-07-11, issue 2092 +-- The error range should be set to the file with the wrong module name +-- not the importing one (which would be the default). +checkModuleName' :: TopLevelModuleName' Range -> SourceFile -> TCM () +checkModuleName' m f = + setCurrentRange m $ checkModuleName m f Nothing + +#if MIN_VERSION_Agda(2,8,0) +-- moduleName was exported until 2.8.0 + +-- | Computes the module name of the top-level module in the given file. +-- +-- If no top-level module name is given, then an attempt is made to +-- use the file name as a module name. + +moduleName :: + AbsolutePath + -- ^ The path to the file. + -> C.Module + -- ^ The parsed module. + -> TCM TopLevelModuleName +moduleName file parsedModule = Bench.billTo [Bench.ModuleName] $ do + let defaultName = rootNameModule file + raw = rawTopLevelModuleNameForModule parsedModule + TCM.topLevelModuleName =<< if C.isNoName raw + then setCurrentRange (rangeFromAbsolutePath file) $ do + m <- runPM (fst <$> parse moduleNameParser defaultName) + `catchError` \_ -> + TCM.typeError $ TCM.InvalidFileName file TCM.DoesNotCorrespondToValidModuleName + case m of + C.Qual{} -> + TCM.typeError $ TCM.InvalidFileName file $ + TCM.RootNameModuleNotAQualifiedModuleName $ T.pack defaultName + C.QName{} -> + return $ RawTopLevelModuleName + { rawModuleNameRange = getRange m + , rawModuleNameParts = singleton (T.pack defaultName) + , rawModuleNameInferred = True + -- Andreas, 2025-06-21, issue #7953: + -- Remember we made up this module name to improve errors. + } + else return raw +#endif + +-- Orphan instances + +instance Pretty Imp.Source where + pretty src = + text "Source" + <+> pretty (Imp.srcModuleName src) + <+> pretty (Imp.srcProjectLibs src) diff --git a/src/Agda/Interaction/Imports/Virtual.hs b/src/Agda/Interaction/Imports/Virtual.hs new file mode 100644 index 0000000..02d7e07 --- /dev/null +++ b/src/Agda/Interaction/Imports/Virtual.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} + +module Agda.Interaction.Imports.Virtual + ( VSourceFile (..), + vSrcFromUri, + parseSourceFromContents, + parseVSource, + ) +where + +#if MIN_VERSION_Agda(2,8,0) +import Agda.TypeChecking.Monad (SourceFile (SourceFile)) +#else +import Agda.Interaction.FindFile (SourceFile (SourceFile)) +#endif +import qualified Agda.Interaction.Imports as Imp +import qualified Agda.Interaction.Imports.More as Imp +import Agda.Syntax.Parser (moduleParser, parseFile) +import Agda.Syntax.Position (mkRangeFile) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.FileName (AbsolutePath) +import Agda.Utils.Maybe (maybeToList) +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Trans (lift) +import qualified Data.Strict as Strict +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Types as LSP +import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidAbsolutePath) +import qualified Language.LSP.Server as LSP +import qualified Language.LSP.VFS as VFS +import Server.Model.AgdaLib (agdaLibToFile) +import Server.Model.Monad (MonadAgdaLib (askAgdaLib)) + +data VSourceFile = VSourceFile + { vSrcFileSrcFile :: SourceFile, + vSrcUri :: LSP.NormalizedUri, + vSrcVFile :: VFS.VirtualFile + } + +#if MIN_VERSION_Agda(2,8,0) +srcFilePath :: (TCM.MonadFileId m) => SourceFile -> m AbsolutePath +srcFilePath = TCM.srcFilePath +#else +srcFilePath :: (Monad m) => SourceFile -> m AbsolutePath +srcFilePath (SourceFile path) = return path +#endif + +#if MIN_VERSION_Agda(2,8,0) +vSrcFilePath :: (TCM.MonadFileId m) => VSourceFile -> m AbsolutePath +#else +vSrcFilePath :: (Monad m) => VSourceFile -> m AbsolutePath +#endif +vSrcFilePath = srcFilePath . vSrcFileSrcFile + +#if MIN_VERSION_Agda(2,8,0) +vSrcFromUri :: + (TCM.MonadFileId m, MonadIO m) => + LSP.NormalizedUri -> + VFS.VirtualFile -> + m VSourceFile +vSrcFromUri normUri file = do + absPath <- uriToPossiblyInvalidAbsolutePath normUri + src <- TCM.srcFromPath absPath + return $ VSourceFile src normUri file +#else +vSrcFromUri :: + (MonadIO m) => + LSP.NormalizedUri -> + VFS.VirtualFile -> + m VSourceFile +vSrcFromUri normUri file = do + absPath <- uriToPossiblyInvalidAbsolutePath normUri + let src = SourceFile absPath + return $ VSourceFile src normUri file +#endif + +parseSourceFromContents :: + (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) => + LSP.NormalizedUri -> + SourceFile -> + Text.Text -> + m Imp.Source +parseSourceFromContents srcUri srcFile contentsStrict = do + f <- TCM.liftTCM $ srcFilePath srcFile + + let rf0 = mkRangeFile f Nothing + TCM.setCurrentRange (Imp.beginningOfFile rf0) $ do + let contents = Strict.toLazy contentsStrict + let contentsString = Text.unpack contentsStrict + + parsedModName0 <- + TCM.liftTCM $ + Imp.moduleName f . fst . fst =<< do + Imp.runPMDropWarnings $ parseFile moduleParser rf0 contentsString + + let rf = mkRangeFile f $ Just parsedModName0 + ((parsedMod, attrs), fileType) <- TCM.liftTCM $ Imp.runPM $ parseFile moduleParser rf contentsString + parsedModName <- TCM.liftTCM $ Imp.moduleName f parsedMod + + agdaLib <- askAgdaLib + let libs = maybeToList $ agdaLibToFile srcUri agdaLib + + return + Imp.Source + { Imp.srcText = contents, + Imp.srcFileType = fileType, + Imp.srcOrigin = srcFile, + Imp.srcModule = parsedMod, + Imp.srcModuleName = parsedModName, + Imp.srcProjectLibs = libs, + Imp.srcAttributes = attrs + } + +-- | Based on @parseSource@ +parseVSource :: (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) => VSourceFile -> m Imp.Source +parseVSource (VSourceFile srcFile uri vFile) = + parseSourceFromContents uri srcFile (VFS.virtualFileText vFile) diff --git a/src/Agda/Interaction/Library/More.hs b/src/Agda/Interaction/Library/More.hs new file mode 100644 index 0000000..da5e264 --- /dev/null +++ b/src/Agda/Interaction/Library/More.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE CPP #-} + +module Agda.Interaction.Library.More + ( tryRunLibM, +#if MIN_VERSION_Agda(2,8,0) +#else + runLibErrorIO, +#endif + ) +where + +import Agda.Interaction.Library (LibM, AgdaLibFile) +import Agda.Interaction.Library.Base (LibErrorIO, libName, libFile, libIncludes) +import Agda.Utils.Either (maybeRight) +import Agda.Utils.Null (Null (empty)) +import Control.Category ((>>>)) +import Control.Monad.Except (runExceptT) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.State.Lazy (evalStateT) +import Control.Monad.Writer.Lazy (runWriterT) +import Agda.Syntax.Common.Pretty (Pretty, pretty, text, (<+>)) +import Agda.Utils.Lens ((^.)) + +#if MIN_VERSION_Agda(2,8,0) +-- Unneeded in 2.8.0 due to API changes +#else +runLibErrorIO :: (MonadIO m) => LibErrorIO a -> m a +runLibErrorIO = + runWriterT + >>> flip evalStateT empty + >>> fmap fst + >>> liftIO +#endif + +tryRunLibM :: (MonadIO m) => LibM a -> m (Maybe a) +tryRunLibM = + runExceptT + >>> runWriterT + >>> flip evalStateT empty + >>> fmap (fst >>> maybeRight) + >>> liftIO + +instance Pretty AgdaLibFile where + pretty agdaLibFile = + text "AgdaLibFile" + <+> (pretty $ agdaLibFile ^. libName) + <+> (pretty $ agdaLibFile ^. libFile) + <+> (pretty $ agdaLibFile ^. libIncludes) diff --git a/src/Agda/Interaction/Library/Parse/More.hs b/src/Agda/Interaction/Library/Parse/More.hs new file mode 100644 index 0000000..b8227f8 --- /dev/null +++ b/src/Agda/Interaction/Library/Parse/More.hs @@ -0,0 +1,297 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} + +-- | Adaptation of Agda.Interaction.Library.Parse +-- +-- Agda only exports functions which read from the filesystem, so we reproduce +-- and modify them here to interact with LSP filesystem abstractions. +module Agda.Interaction.Library.Parse.More + ( parseLibFile, + runP, + ) +where + +import Agda.Interaction.Library.Base +import Agda.Syntax.Position +import Agda.Utils.Applicative +import Agda.Utils.FileName +import Agda.Utils.IO (catchIO) +import qualified Agda.Utils.IO.UTF8 as UTF8 +import Agda.Utils.Lens +import Agda.Utils.List (duplicates) +import Agda.Utils.List1 (List1, toList) +import qualified Agda.Utils.List1 as List1 +import qualified Agda.Utils.Maybe.Strict as Strict +import Agda.Utils.Singleton +import Agda.Utils.String (ltrim) +import Control.Monad +import Control.Monad.Except +import Control.Monad.Writer +import Data.Char +import qualified Data.List as List +import Data.Text (Text) +import qualified Data.Text as T +import qualified Data.Text as Text +import Monad (ServerM) +import qualified Server.Filesystem as FS +import System.FilePath + +-- | Parser monad: Can throw @LibParseError@s, and collects +-- @LibWarning'@s library warnings. +type P = ExceptT LibParseError (Writer [LibWarning']) + +runP :: P a -> (Either LibParseError a, [LibWarning']) +runP = runWriter . runExceptT + +warningP :: LibWarning' -> P () +warningP = tell . pure + +-- | The config files we parse have the generic structure of a sequence +-- of @field : content@ entries. +type GenericFile = [GenericEntry] + +data GenericEntry = GenericEntry + { -- | E.g. field name. @trim@med. + geHeader :: String, + -- | E.g. field content. @trim@med. + _geContent :: [String] + } + +-- | Library file field format format [sic!]. +data Field = forall a. Field + { -- | Name of the field. + fName :: String, + -- | Is it optional? + fOptional :: Bool, + -- | Content parser for this field. + -- + -- The range points to the start of the file. + fParse :: Range -> [String] -> P a, + -- | Sets parsed content in 'AgdaLibFile' structure. + fSet :: LensSet AgdaLibFile a + } + +optionalField :: + String -> (Range -> [String] -> P a) -> Lens' AgdaLibFile a -> Field +optionalField str p l = Field str True p (set l) + +-- | @.agda-lib@ file format with parsers and setters. +agdaLibFields :: [Field] +agdaLibFields = + -- Andreas, 2017-08-23, issue #2708, field "name" is optional. + [ optionalField "name" (\_ -> parseName) libName, + optionalField "include" (\_ -> pure . concatMap parsePaths) libIncludes, +#if MIN_VERSION_Agda(2,8,0) + optionalField "depend" (\_ -> pure . map parseLibName . concatMap splitCommas) libDepends, +#else + optionalField "depend" (\_ -> pure . concatMap splitCommas) libDepends, +#endif + optionalField "flags" (\r -> pure . foldMap (parseFlags r)) libPragmas + ] + where + parseName :: [String] -> P LibName +#if MIN_VERSION_Agda(2,8,0) + parseName [s] | [name] <- words s = pure $ parseLibName name +#else + parseName [s] | [name] <- words s = pure name +#endif + parseName ls = throwError $ BadLibraryName $ unwords ls + + parsePaths :: String -> [FilePath] + parsePaths = go id + where + fixup acc = let fp = acc [] in not (null fp) ?$> fp + go acc [] = fixup acc + go acc ('\\' : ' ' : cs) = go (acc . (' ' :)) cs + go acc ('\\' : '\\' : cs) = go (acc . ('\\' :)) cs + go acc (' ' : cs) = fixup acc ++ go id cs + go acc (c : cs) = go (acc . (c :)) cs + + parseFlags :: Range -> String -> OptionsPragma + parseFlags r s = + OptionsPragma + { pragmaStrings = words s, + pragmaRange = r + } + +-- | Parse @.agda-lib@ file. +-- +-- In the Agda implementation, this is where the path is set in AgdaLibFile. We +-- don't, since we don't really want to work with paths in the first place. +parseLibFile :: (FS.Provider p, FS.IsFileId f) => p -> f -> ServerM (Maybe (P AgdaLibFile)) +parseLibFile provider fileId = do + abs <- FS.fileIdToPossiblyInvalidAbsolutePath $ FS.toFileId fileId + contents <- FS.getFileContents provider fileId + case contents of + Nothing -> return Nothing + Just contents -> + return $ Just $ parseLib abs (Text.unpack contents) + +-- | Parse file contents. +parseLib :: + -- | The parsed file. + AbsolutePath -> + String -> + P AgdaLibFile +parseLib file s = fromGeneric file =<< parseGeneric s + +-- | Parse 'GenericFile' with 'agdaLibFields' descriptors. +fromGeneric :: + -- | The parsed file. + AbsolutePath -> + GenericFile -> + P AgdaLibFile +fromGeneric file = fromGeneric' file agdaLibFields + +-- | Given a list of 'Field' descriptors (with their custom parsers), +-- parse a 'GenericFile' into the 'AgdaLibFile' structure. +-- +-- Checks mandatory fields are present; +-- no duplicate fields, no unknown fields. +fromGeneric' :: + -- | The parsed file. + AbsolutePath -> + [Field] -> + GenericFile -> + P AgdaLibFile +fromGeneric' file fields fs = do + checkFields fields (map geHeader fs) + foldM upd emptyLibFile fs + where + -- The range points to the start of the file. + r = + Range + (Strict.Just $ mkRangeFile file Nothing) + (singleton (posToInterval () p p)) + where + p = + Pn + { srcFile = (), + posPos = 1, + posLine = 1, + posCol = 1 + } + + upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile + upd l (GenericEntry h cs) = do + mf <- findField h fields + case mf of + Just Field {..} -> do + x <- fParse r cs + return $ fSet x l + Nothing -> return l + +-- | Ensure that there are no duplicate fields and no mandatory fields are missing. +checkFields :: [Field] -> [String] -> P () +checkFields fields fs = do + -- Report missing mandatory fields. + () <- List1.unlessNull missing $ throwError . MissingFields + -- Report duplicate fields. + List1.unlessNull (duplicates fs) $ throwError . DuplicateFields + where + mandatory :: [String] + mandatory = [fName f | f <- fields, not $ fOptional f] + missing :: [String] + missing = mandatory List.\\ fs + +-- | Find 'Field' with given 'fName', throw error if unknown. +findField :: String -> [Field] -> P (Maybe Field) +findField s fs = maybe err (return . Just) $ List.find ((s ==) . fName) fs + where + err = warningP (UnknownField s) >> return Nothing + +-- Generic file parser ---------------------------------------------------- + +-- | Example: +-- +-- @ +-- parseGeneric "name:Main--BLA\ndepend:--BLA\n standard-library--BLA\ninclude : . --BLA\n src more-src \n" +-- == Right [("name",["Main"]),("depend",["standard-library"]),("include",[".","src more-src"])] +-- @ +parseGeneric :: String -> P GenericFile +parseGeneric s = + groupLines =<< concat <$> zipWithM parseLine [1 ..] (map stripComments $ lines s) + +-- | Lines with line numbers. +data GenericLine + = -- | Header line, like a field name, e.g. "include :". Cannot be indented. + -- @String@ is 'trim'med. + Header LineNumber String + | -- | Other line. Must be indented. + -- @String@ is 'trim'med. + Content LineNumber String + deriving (Show) + +-- | Parse line into 'Header' and 'Content' components. +-- +-- Precondition: line comments and trailing whitespace have been stripped away. +-- +-- Example file: +-- +-- @ +-- name: Main +-- depend: +-- standard-library +-- include: . +-- src more-src +-- @ +-- +-- This should give +-- +-- @ +-- [ Header 1 "name" +-- , Content 1 "Main" +-- , Header 2 "depend" +-- , Content 3 "standard-library" +-- , Header 4 "include" +-- , Content 4 "." +-- , Content 5 "src more-src" +-- ] +-- @ +parseLine :: LineNumber -> String -> P [GenericLine] +parseLine _ "" = pure [] +parseLine l s@(c : _) + -- Indented lines are 'Content'. + | isSpace c = pure [Content l $ ltrim s] + -- Non-indented lines are 'Header'. + | otherwise = + case break (== ':') s of + -- Headers are single words followed by a colon. + -- Anything after the colon that is not whitespace is 'Content'. + (h, ':' : r) -> + case words h of + [h] -> pure $ Header l h : [Content l r' | let r' = ltrim r, not (null r')] + [] -> throwError $ MissingFieldName l + hs -> throwError $ BadFieldName l h + _ -> throwError $ MissingColonForField l (ltrim s) + +-- | Collect 'Header' and subsequent 'Content's into 'GenericEntry'. +-- +-- Leading 'Content's? That's an error. +groupLines :: [GenericLine] -> P GenericFile +groupLines [] = pure [] +groupLines (Content l c : _) = throwError $ ContentWithoutField l +groupLines (Header _ h : ls) = (GenericEntry h [c | Content _ c <- cs] :) <$> groupLines ls1 + where + (cs, ls1) = span isContent ls + isContent Content {} = True + isContent Header {} = False + +-- | Remove leading whitespace and line comment. +trimLineComment :: String -> String +trimLineComment = stripComments . ltrim + +-- | Break a comma-separated string. Result strings are @trim@med. +splitCommas :: String -> [String] +splitCommas = words . map (\c -> if c == ',' then ' ' else c) + +-- | ...and trailing, but not leading, whitespace. +stripComments :: String -> String +stripComments "" = "" +stripComments ('-' : '-' : c : _) | isSpace c = "" +stripComments (c : s) = cons c (stripComments s) + where + cons c "" | isSpace c = "" + cons c s = c : s \ No newline at end of file diff --git a/src/Agda/Parser.hs b/src/Agda/Parser.hs index 6e52b91..10cfc07 100644 --- a/src/Agda/Parser.hs +++ b/src/Agda/Parser.hs @@ -15,12 +15,12 @@ import Data.Text (Text, unpack) import qualified Data.Text as Text import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Server (LspM) -import Monad (ServerM) +import Monad (ServerM, ServerT) import Options (Config) -------------------------------------------------------------------------------- -tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (LspM Config) (Maybe (Token, Text)) +tokenAt :: LSP.Uri -> Text -> PositionWithoutFile -> ServerM (Maybe (Token, Text)) tokenAt uri source position = case LSP.uriToFilePath uri of Nothing -> return Nothing Just filepath -> do diff --git a/src/Agda/Position.hs b/src/Agda/Position.hs index 3e65b88..d90e96d 100644 --- a/src/Agda/Position.hs +++ b/src/Agda/Position.hs @@ -10,8 +10,8 @@ module Agda.Position toAgdaPositionWithoutFile, toAgdaRange, prettyPositionWithoutFile, - -- , toLSPRange - -- , toLSPPosition + toLspRange, + toLspPosition, ) where @@ -24,6 +24,7 @@ import qualified Data.Strict.Maybe as Strict import Data.Text (Text) import qualified Data.Text as Text import qualified Language.LSP.Protocol.Types as LSP +import Data.Functor (void) -- Note: LSP srclocs are 0-base -- Agda srclocs are 1-base @@ -64,6 +65,31 @@ prettyPositionWithoutFile pos@(Pn () offset _line _col) = -------------------------------------------------------------------------------- +-- | Agda source locations => LSP source locations + +intervalStart :: Interval -> PositionWithoutFile +intervalEnd :: Interval -> PositionWithoutFile + +#if MIN_VERSION_Agda(2,8,0) +intervalStart (Interval _ start _end) = start +intervalEnd (Interval _ _start end) = end +#else +intervalStart (Interval start _end) = void start +intervalEnd (Interval _start end) = void end +#endif + +-- | Agda Range -> LSP Range +toLspRange :: Range -> LSP.Range +toLspRange range = case rangeToIntervalWithFile range of + Nothing -> LSP.Range (LSP.Position (-1) (-1)) (LSP.Position (-1) (-1)) + Just interval -> LSP.Range (toLspPosition $ intervalStart interval) (toLspPosition $ intervalEnd interval) + +-- | Agda Position -> LSP Position +toLspPosition :: Position' a -> LSP.Position +toLspPosition (Pn _ offset line col) = LSP.Position (fromIntegral line - 1) (fromIntegral col - 1) + +-------------------------------------------------------------------------------- + -- | Positon => Offset convertion -- Keeps record of offsets of every line break ("\n", "\r" and "\r\n") @@ -142,14 +168,3 @@ makeFromOffset = go (Accum previous n l table) '\r' = Accum (Just '\r') (1 + n) (1 + l) (IntMap.insert (1 + n) (1 + l) table) go (Accum previous n l table) char = Accum (Just char) (1 + n) l table - --- -------------------------------------------------------------------------------- --- -- | Agda Highlighting Range -> Agda Range - --- fromAgdaHighlightingRangeToLSPRange :: Range -> LSP.Range --- fromAgdaHighlightingRangeToLSPRange range = case rangeToIntervalWithFile range of --- Nothing -> LSP.Range (LSP.Position (-1) (-1)) (LSP.Position (-1) (-1)) --- Just (Interval start end) -> LSP.Range (toLSPPosition start) (toLSPPosition end) - --- toLSPPosition :: Position -> LSP.Position --- toLSPPosition (Pn _ offset line col) = LSP.Position (fromIntegral line - 1) (fromIntegral col - 1) diff --git a/src/Agda/Syntax/Abstract/More.hs b/src/Agda/Syntax/Abstract/More.hs new file mode 100644 index 0000000..cf36516 --- /dev/null +++ b/src/Agda/Syntax/Abstract/More.hs @@ -0,0 +1,213 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Agda.Syntax.Abstract.More () where + +import Agda.Syntax.Abstract +import Agda.Syntax.Common +import Agda.Syntax.Common (ArgInfo (argInfoOrigin)) +import Agda.Syntax.Common.Pretty +import Agda.Syntax.Info +import Agda.Utils.Functor ((<&>)) +import Data.Foldable (Foldable (toList)) +import qualified Data.Map as Map + +instance Pretty Declaration where + pretty decl = prettyAssign $ case decl of + Axiom kindOfName _defInfo _argInfo _polarities name type' -> + ( text "Axiom", + prettyMap + [ (text "kindOfName", pshow kindOfName), + (text "name", pretty name), + (text "type", pretty type') + ] + ) + Generalize _namesInType _defInfo _argInfo name type' -> + ( text "Generalize", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + Field _defInfo name type' -> + ( text "Field", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + Primitive _defInfo name type' -> + ( text "Primitive", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + Mutual _mutualInfo decls -> (text "Mutual", pretty decls) + Section _range _erased moduleName genTel decls -> + ( text "Section", + prettyMap + [ (text "moduleName", pretty moduleName), + (text "genTel", pretty genTel), + (text "decls", pretty decls) + ] + ) + Apply _moduleInfo _erased moduleName _moduleApp _scopeCopyInfo _importDirective -> + (text "Apply", pretty moduleName) + Import _moduleInfo moduleName _importDirective -> (text "Import", pretty moduleName) + Pragma _range _pragma -> (text "Pragma", mempty) + Open _moduleInfo moduleName _importDirective -> + (text "Open", pretty moduleName) + FunDef _defInfo name clauses -> + ( text "FunDef", + prettyMap + [ (text "name", pretty name), + (text "clauses", pretty clauses) + ] + ) + DataSig _defInfo _erased name _genTel type' -> + ( text "DataSig", + prettyMap + [ (text "name", pretty name), + (text "type", pretty type') + ] + ) + DataDef _defIngo name _univCheck dataDefParams _ctors -> + ( text "DataDef", + prettyMap + [ (text "name", pretty name), + (text "dataDefParams", pretty dataDefParams) + ] + ) + RecSig _defInfo _erased name genTel type' -> + ( text "RecSig", + prettyMap + [ (text "name", pretty name), + (text "genTel", pretty genTel), + (text "type", pretty type') + ] + ) + RecDef _defInfo name _univCheck _recDirs dataDefParams _type' decls -> + ( text "RecDef", + prettyMap + [ (text "name", pretty name), + (text "dataDefParams", pretty dataDefParams), + (text "decls", pretty decls) + ] + ) + PatternSynDef name _args _body -> (text "PatternSynDef", pretty name) + -- ... + ScopedDecl scopeInfo decls -> (text "ScopedDecl", pretty decls) + -- ... + _ -> ("Decl", mempty) + +instance Pretty Expr where + pretty expr = prettyAssign $ case expr of + Var name -> (text "Var", pretty name) + Def' name _suffix -> (text "Def'", pretty name) + Proj _origin name -> (text "Proj", pretty name) + Con name -> (text "Con", pretty name) + PatternSyn name -> (text "PatternSyn", pretty name) + Macro name -> (text "Macro", pretty name) + -- ... + App _appInfo f arg -> + ( text "App", + prettyMap + [ (text "f", pretty f), + (text "arg", pretty arg) + ] + ) + -- ... + Pi _exprInfo dom codom -> + ( text "Pi", + prettyMap + [ (text "dom", pretty dom), + (text "codom", pretty codom) + ] + ) + Generalized dom codom -> + ( text "Generalized", + prettyMap + [ (text "dom", pretty $ toList dom), + (text "codom", pretty codom) + ] + ) + Fun _exprInfo dom codom -> + ( text "Fun", + prettyMap + [ (text "dom", pretty dom), + (text "codom", pretty codom) + ] + ) + Let _exprInfo bindings body -> + ( text "Let", + prettyMap + [ (text "bindings", pretty bindings), + (text "body", pretty body) + ] + ) + -- ... + ScopedExpr _scopeInfo expr -> (text "ScopedExpr", pretty expr) + -- ... + _ -> ("Expr", mempty) + +instance (Pretty a) => Pretty (Pattern' a) where + pretty _pat = text "pat" + +debugNamedBinder :: NamedArg Binder -> Doc +debugNamedBinder (Arg argInfo binder) = pshow (argInfoOrigin argInfo) <+> pretty binder + +instance Pretty TypedBinding where + pretty = \case + TBind _range _typedBindingInfo binders type' -> + parens (prettyList (debugNamedBinder <$> toList binders) <+> colon <+> pretty type') + TLet _range _letBindings -> text "TLet" + +instance Pretty LetBinding where + pretty = \case + LetBind _letInfo _argInfo name type' expr -> + text "let" <+> pretty (unBind name) <+> text "=" <+> pretty expr + LetPatBind _letInfo pat expr -> + text "letPat" <+> pretty pat <+> text "=" <+> pretty expr + _ -> text "LetBinding" + +instance Pretty Binder where + pretty binder = pretty $ unBind $ binderName binder + +instance Pretty LamBinding where + pretty = \case + DomainFree _tacticAttr namedArgBinder -> debugNamedBinder namedArgBinder + DomainFull binding -> pretty binding + +instance (Pretty t) => Pretty (DefInfo' t) where + pretty defInfo = + align + 20 + [("DefInfo", prettyMap [(text "defTactic", defTactic defInfo)])] + +instance Pretty GeneralizeTelescope where + pretty genTel = + align + 20 + [ ( "GeneralizeTelescope", + prettyMap + [ (text "generalizeTelVars", prettyMap $ Map.toList $ generalizeTelVars genTel), + (text "generalizeTel", pretty $ generalizeTel genTel) + ] + ) + ] + +instance (Pretty lhs) => Pretty (Clause' lhs) where + pretty (Clause lhs _strippedPats rhs whereDecls _catchall) = + pretty lhs <+> text "=" <+> pretty rhs + +instance Pretty LHS where + pretty _lhs = text "lhs" + +instance Pretty RHS where + pretty = \case + RHS expr _concrete -> pretty expr + _ -> text "rhs" + +instance Pretty DataDefParams where + pretty (DataDefParams _generalized params) = pretty params diff --git a/src/Agda/TypeChecking/Monad/Options/More.hs b/src/Agda/TypeChecking/Monad/Options/More.hs new file mode 100644 index 0000000..daf8b2d --- /dev/null +++ b/src/Agda/TypeChecking/Monad/Options/More.hs @@ -0,0 +1,59 @@ +module Agda.TypeChecking.Monad.Options.More (setCommandLineOptionsByLib) where + +import Agda.Interaction.Options (CommandLineOptions (..)) +import qualified Agda.Interaction.Options.Lenses as Lens +import Agda.TypeChecking.Monad (MonadTCM) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.TypeChecking.Monad.Benchmark (updateBenchmarkingStatus) +import Agda.Utils.FileName (AbsolutePath, absolute) +import Agda.Utils.Lens ((^.)) +import qualified Agda.Utils.List1 as List1 +import Control.Monad.IO.Class (liftIO) +import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidFilePath) +import qualified Server.Filesystem as FS +import Server.Model.AgdaLib (AgdaLib, agdaLibDependencies, agdaLibIncludes) +import Server.Model.Monad (MonadAgdaLib (askAgdaLib)) +import System.Directory (getCurrentDirectory) + +setCommandLineOptionsByLib :: + (MonadTCM m, MonadAgdaLib m) => + CommandLineOptions -> + m () +setCommandLineOptionsByLib opts = do + root <- liftIO (absolute =<< getCurrentDirectory) + setCommandLineOptionsByLib' root opts + +setCommandLineOptionsByLib' :: + (MonadTCM m, MonadAgdaLib m) => + AbsolutePath -> + CommandLineOptions -> + m () +setCommandLineOptionsByLib' root opts = do + incs <- case optAbsoluteIncludePaths opts of + [] -> do + opts' <- setLibraryPathsByLib opts + let incs = optIncludePaths opts' + TCM.liftTCM $ TCM.setIncludeDirs incs root + List1.toList <$> TCM.getIncludeDirs + incs -> return incs + TCM.modifyTC $ Lens.setCommandLineOptions opts {optAbsoluteIncludePaths = incs} + TCM.liftTCM $ TCM.setPragmaOptions (optPragmaOptions opts) + TCM.liftTCM updateBenchmarkingStatus + +setLibraryPathsByLib :: + (MonadTCM m, MonadAgdaLib m) => + CommandLineOptions -> + m CommandLineOptions +setLibraryPathsByLib o = do + agdaLib <- askAgdaLib + return $ addDefaultLibrariesByLib agdaLib o + +-- TODO: resolve dependency libs; see setLibraryIncludes in Agda + +addDefaultLibrariesByLib :: AgdaLib -> CommandLineOptions -> CommandLineOptions +addDefaultLibrariesByLib agdaLib o + | not (null $ optLibraries o) || not (optUseLibs o) = o + | otherwise = do + let libs = agdaLib ^. agdaLibDependencies + let incs = uriToPossiblyInvalidFilePath . FS.fileIdToUri <$> agdaLib ^. agdaLibIncludes + o {optIncludePaths = incs ++ optIncludePaths o, optLibraries = libs} diff --git a/src/Indexer.hs b/src/Indexer.hs new file mode 100644 index 0000000..ae24085 --- /dev/null +++ b/src/Indexer.hs @@ -0,0 +1,66 @@ +{-# LANGUAGE CPP #-} + +module Indexer + ( withAstFor, + usingSrcAsCurrent, + indexFile, + ) +where + +#if MIN_VERSION_Agda(2,8,0) +#else +import Agda.Interaction.FindFile (srcFilePath) +#endif +import qualified Agda.Interaction.Imports as Imp +import qualified Agda.Interaction.Imports.More as Imp +import Agda.Syntax.Common.Pretty (prettyShow) +import qualified Agda.Syntax.Concrete as C +import Agda.Syntax.Translation.ConcreteToAbstract (ToAbstract (toAbstract), TopLevel (TopLevel), TopLevelInfo) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.TypeChecking.Monad.Options.More (setCommandLineOptionsByLib) +import qualified Data.Map as Map +import Indexer.Indexer (indexAst) +import Indexer.Monad (execIndexerM) +import Indexer.Postprocess (postprocess) +import Server.Model.AgdaFile (AgdaFile) +import Server.Model.Monad (WithAgdaLibM) + +usingSrcAsCurrent :: Imp.Source -> WithAgdaLibM a -> WithAgdaLibM a +usingSrcAsCurrent src x = do + TCM.liftTCM TCM.resetState + + TCM.liftTCM $ Imp.setOptionsFromSourcePragmas True src + + TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $ + -- Now reset the options + setCommandLineOptionsByLib . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC + +#if MIN_VERSION_Agda(2,8,0) + TCM.modifyTCLens TCM.stModuleToSourceId $ Map.insert (Imp.srcModuleName src) (Imp.srcOrigin src) + TCM.localTC (\e -> e {TCM.envCurrentPath = Just (TCM.srcFileId $ Imp.srcOrigin src)}) x +#else + TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src) + TCM.localTC (\e -> e {TCM.envCurrentPath = Just (srcFilePath $ Imp.srcOrigin src)}) x +#endif + +withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaLibM a) -> WithAgdaLibM a +withAstFor src f = usingSrcAsCurrent src $ do +#if MIN_VERSION_Agda(2,8,0) + let srcFile = Imp.srcOrigin src +#else + let srcFile = srcFilePath $ Imp.srcOrigin src +#endif + let topLevel = + TopLevel + srcFile + (Imp.srcModuleName src) + (C.modDecls $ Imp.srcModule src) + ast <- TCM.liftTCM $ toAbstract topLevel + f ast + +indexFile :: + Imp.Source -> + WithAgdaLibM AgdaFile +indexFile src = withAstFor src $ \ast -> execIndexerM $ do + indexAst ast + postprocess diff --git a/src/Indexer/Indexer.hs b/src/Indexer/Indexer.hs new file mode 100644 index 0000000..40030ca --- /dev/null +++ b/src/Indexer/Indexer.hs @@ -0,0 +1,705 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Indexer.Indexer (indexAst) where + +import qualified Agda.Syntax.Abstract as A +import qualified Agda.Syntax.Common as C +import Agda.Syntax.Common.Pretty (render) +import qualified Agda.Syntax.Concrete as C +import qualified Agda.Syntax.Info as Info +import qualified Agda.Syntax.Internal as I +import qualified Agda.Syntax.Literal as Lit +import qualified Agda.Syntax.Scope.Base as Scope +import Agda.Syntax.Translation.ConcreteToAbstract (TopLevelInfo (TopLevelInfo)) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.TypeChecking.Pretty (prettyTCM) +import Agda.Utils.Functor ((<&>)) +import Agda.Utils.List1 (List1) +import qualified Agda.Utils.List1 as List1 +import Agda.Utils.Maybe (whenJust) +import Agda.Utils.Monad (when) +import Data.Foldable (forM_, traverse_, toList) +import Data.Functor.Compose (Compose (Compose, getCompose)) +import qualified Data.Set as Set +import Data.Void (absurd) +import Indexer.Monad + ( AmbiguousNameLike (..), + BindingKind (..), + HasParamNames (..), + IndexerM, + NameLike (..), + NoType (NoType), + SymbolKindLike (..), + TypeLike (..), + UnknownType (UnknownType), + tellBinding, + tellDecl, + tellDef, + tellDefParams, + tellGenTel, + tellImport, + tellNamedArgUsage, + tellParamNames, + tellUsage, + withBindingKind, + withParent, + ) +import Server.Model.Symbol (SymbolKind (..)) + +indexAst :: TopLevelInfo -> IndexerM () +indexAst (TopLevelInfo decls _scope) = index decls + +class Indexable a where + index :: a -> IndexerM () + default index :: (Foldable f, Indexable b, a ~ f b) => a -> IndexerM () + index = traverse_ index + +instance Indexable A.Declaration where + index = \case + A.Axiom kindOfName defInfo _argInfo _polarities name type' -> do + -- TODO: what does the `ArgInfo` mean? + -- Includes postulates, function declarations + tellDecl name kindOfName type' + index defInfo + index type' + A.Generalize _generalizeVars defInfo _argInfo name type' -> do + -- TODO: what does the `ArgInfo` mean? + tellDecl name GeneralizeVar type' + index defInfo + index type' + A.Field defInfo name type' -> do + tellDecl name Field type' + index defInfo + index type' + A.Primitive defInfo name type' -> do + tellDecl name Prim type' + index defInfo + index type' + A.Mutual _mutualInfo decls -> + index decls + A.Section _range _erased moduleName genTel decls -> do + tellDecl moduleName Module NoType + tellParamNames moduleName genTel + withParent moduleName $ do + index genTel + index decls + A.Apply _moduleInfo _erased moduleName moduleApp _scopeCopyInfo importDirective -> do + tellUsage moduleName + index moduleApp + index importDirective + A.Import _moduleInfo moduleName importDirective -> do + tellUsage moduleName + index importDirective + A.Pragma _range pragma -> + index pragma + A.Open _moduleInfo moduleName importDirective -> do + tellUsage moduleName + index importDirective + A.FunDef _defInfo name clauses -> withBindingKind DefBinding $ do + -- function declarations are captured by the `Axiom` case + withParent name $ do + index $ WithLHSNaming LHSNamed <$> clauses + A.DataSig defInfo _erased name genTel type' -> + withBindingKind DeclBinding $ do + tellDecl name Data type' + index defInfo + index genTel + tellGenTel name genTel + index type' + A.DataDef _defInfo name _univCheck dataDefParams constructors -> + withBindingKind DefBinding $ do + tellDef name Data UnknownType + index dataDefParams + tellDefParams name dataDefParams + index constructors + A.RecSig defInfo _erased name genTel type' -> + withBindingKind DeclBinding $ do + tellDecl name Record type' + index defInfo + index genTel + tellGenTel name genTel + index type' + A.RecDef _defInfo name _univCheck recDirectives dataDefParams _type' decls -> + withBindingKind DefBinding $ do + -- The type associated with a `RecDef` is a Pi type including the record's + -- fields, which is not what we want. The `RecSig` does have the type we + -- want, so we use that instead. + tellDef name Record UnknownType + index dataDefParams + tellDefParams name dataDefParams + withParent name $ do + index recDirectives + index decls + A.PatternSynDef name bindings pat -> do + tellDecl name PatternSyn UnknownType +#if MIN_VERSION_Agda(2,7,0) + forM_ bindings $ \(C.WithHiding _hiding binding) -> +#else + forM_ bindings $ \(C.Arg _argInfo binding) -> +#endif + tellDef binding Param UnknownType + let pat' :: A.Pattern = fmap absurd pat + index pat' + A.UnquoteDecl _mutualInfo defInfos names expr -> do + forM_ names $ \name -> + tellDef name Unknown UnknownType + index defInfos + index expr + A.UnquoteDef defInfos names expr -> do + forM_ names $ \name -> + tellDef name Unknown UnknownType + index defInfos + index expr + A.UnquoteData defInfos name _univCheck conDefInfos conNames expr -> do + tellDef name Data UnknownType + forM_ conNames $ \conName -> + tellDef conName Con UnknownType + index defInfos + index conDefInfos + index expr + A.ScopedDecl _scope decls -> + index decls + A.UnfoldingDecl _range names -> + forM_ names $ \name -> + tellUsage name + +instance Indexable A.Expr where + index = \case + A.Var name -> + tellUsage name + A.Def' name _suffix -> + tellUsage name + A.Proj _origin ambiguousName -> + tellUsage ambiguousName + A.Con ambiguousName -> + tellUsage ambiguousName + A.PatternSyn ambiguousName -> + tellUsage ambiguousName + A.Macro name -> + tellUsage name + A.Lit _exprInfo lit -> + index lit + A.QuestionMark _metaInfo _interactionId -> + return () + A.Underscore _metaInfo -> + return () + A.Dot _exprInfo expr' -> + index expr' + A.App _appInfo exprF exprArg -> do + index exprF + case funNameFromExpr exprF of + Just name -> indexNamedArgs name [exprArg] + Nothing -> + when (C.argInfoOrigin (C.argInfo exprArg) == C.UserWritten) $ do + index $ C.namedThing $ C.unArg exprArg + A.WithApp _appInfo exprF exprArgs -> do + index exprF + index exprArgs + A.Lam _exprInfo binding body -> do + index binding + index body + A.AbsurdLam _exprInfo _hiding -> + return () + A.ExtendedLam _exprInfo defInfo _erased _generatedFn clauses -> do + index defInfo + index $ WithLHSNaming LHSAnonymous <$> clauses + A.Pi _exprInfo tel type' -> do + index tel + index type' + A.Generalized _generalizeVars type' -> do + index type' + A.Fun _exprInfo dom codom -> do + index dom + index codom + A.Let _exprInfo bindings body -> do + index bindings + index body +#if MIN_VERSION_Agda(2,8,0) + A.Rec _kwRange _exprInfo recAssigns -> +#else + A.Rec _exprInfo recAssigns -> +#endif + index recAssigns +#if MIN_VERSION_Agda(2,8,0) + A.RecUpdate _kwRange _exprInfo exprRec assigns -> do +#else + A.RecUpdate _exprInfo exprRec assigns -> do +#endif + index exprRec + index assigns + A.ScopedExpr _scope expr' -> + index expr' + A.Quote _exprInfo -> return () + A.QuoteTerm _exprInfo -> return () + A.Unquote _exprInfo -> return () + A.DontCare expr' -> index expr' + +funNameFromExpr :: A.Expr -> Maybe A.AmbiguousQName +funNameFromExpr = \case + A.Var name -> Just $ A.unambiguous $ A.qualify_ name + A.Def' name _suffix -> Just $ A.unambiguous name + A.Proj _origin name -> Just name + A.Con name -> Just name + A.PatternSyn name -> Just name + A.Dot _exprInfo expr -> funNameFromExpr expr + A.App _appInfo exprF _exprArgs -> funNameFromExpr exprF + A.WithApp _appInfo exprF _exprArgs -> funNameFromExpr exprF + A.ScopedExpr _scopeInfo expr -> funNameFromExpr expr + A.DontCare expr -> funNameFromExpr expr + _noFunName -> Nothing + +instance (Indexable a) => Indexable (A.Pattern' a) where + index = \case + A.VarP binding -> do + tellDef binding Local UnknownType + A.ConP _conPatInfo ambiguousName naps -> do + tellUsage ambiguousName + indexNamedArgs ambiguousName naps + A.ProjP _patInfo _projOrigin ambiguousName -> + tellUsage ambiguousName + A.DefP _patInfo ambiguousName naps -> do + tellUsage ambiguousName + indexNamedArgs ambiguousName naps + A.WildP _patInfo -> return () + A.AsP _patInfo binding pat' -> do + tellDef binding Local UnknownType + index pat' + A.DotP _patInfo expr -> + index expr + A.AbsurdP _patInfo -> return () + A.LitP _patInfo lit -> + index lit + A.PatternSynP _patInfo ambiguousName naps -> do + tellUsage ambiguousName + indexNamedArgs ambiguousName naps + A.EqualP _patInfo exprPairs -> + forM_ exprPairs $ \(lhs, rhs) -> do + index lhs + index rhs + A.WithP _patInfo pat' -> + index pat' +#if MIN_VERSION_Agda(2,8,0) + A.RecP _kwRange _conPatInfo fieldAssignments -> +#else + A.RecP _conPatInfo fieldAssignments -> +#endif + index fieldAssignments +#if MIN_VERSION_Agda(2,8,0) +#else + A.AnnP _patInfo type' pat' -> do + index type' + index pat' +#endif + +instance (Indexable a) => Indexable (Maybe a) + +instance (Indexable a) => Indexable [a] + +instance (Indexable a) => Indexable (List1 a) + +instance (Indexable a) => Indexable (C.Arg a) where + index (C.Arg argInfo x) = + when (C.argInfoOrigin argInfo == C.UserWritten) $ + index x + +#if MIN_VERSION_Agda(2,7,0) +instance Indexable A.TacticAttribute +#else +instance (Indexable a) => Indexable (C.Ranged a) +#endif + +instance Indexable A.DefInfo where + index = index . Info.defTactic + +indexNamedArgs :: (AmbiguousNameLike n, Indexable a) => n -> [C.NamedArg a] -> IndexerM () +indexNamedArgs headNameLike args = do + let headName = toAmbiguousQName headNameLike + forM_ args $ \(C.Arg argInfo (C.Named maybeName x)) -> + when (C.argInfoOrigin argInfo == C.UserWritten) $ do + whenJust maybeName $ tellNamedArgUsage headName + index x + +indexWithExpr :: A.WithExpr -> IndexerM () +indexWithExpr (C.Named maybeName (C.Arg argInfo expr)) = + when (C.argInfoOrigin argInfo == C.UserWritten) $ do + whenJust maybeName $ \(A.BindName name) -> + tellDef name Param UnknownType + index expr + +instance Indexable Lit.Literal where + index = \case + Lit.LitQName name -> tellUsage name + _otherLit -> return () + +instance (Indexable a) => Indexable (C.FieldAssignment' a) where + index (C.FieldAssignment fieldCName expr) = do + scope <- TCM.getScope + let fieldNames = Scope.anameName <$> Scope.scopeLookup (C.QName fieldCName) scope + List1.ifNull fieldNames (return ()) $ \fieldNames1 -> do + let fieldName = A.AmbQ fieldNames1 + tellUsage fieldName + index expr + +instance Indexable A.RecordAssign where + index = \case + Left assign -> + index assign + Right moduleName -> + tellUsage moduleName + +instance Indexable A.WhereDeclarations where + index whereDecls = case whereDecls of + A.WhereDecls (Just moduleName) _ decl -> do + tellDecl moduleName Module NoType + withParent moduleName $ + index decl + A.WhereDecls Nothing _ decl -> + index decl + +data LHSNaming = LHSNamed | LHSAnonymous deriving (Eq) + +data WithLHSNaming a = WithLHSNaming LHSNaming a + +instance (Indexable a) => Indexable (WithLHSNaming (A.LHSCore' a)) where + index (WithLHSNaming lhsNaming core) = case core of + A.LHSHead name pats -> do + when (lhsNaming == LHSNamed) $ + tellDef name Param UnknownType + indexNamedArgs name pats + A.LHSProj destructor focus pats -> do + tellUsage destructor + -- TODO: what does the named arg in `focus` mean? + indexNamedArgs destructor [getCompose $ WithLHSNaming lhsNaming <$> Compose focus] + indexNamedArgs destructor pats + A.LHSWith lhsHead withPatterns pats -> do + index $ WithLHSNaming lhsNaming lhsHead + index withPatterns + -- TODO: what do the named args mean? + forM_ pats $ \(C.Arg argInfo (C.Named _name pat)) -> + when (C.argInfoOrigin argInfo == C.UserWritten) $ + index pat + +instance Indexable (WithLHSNaming A.LHS) where + index (WithLHSNaming lhsNaming (A.LHS lhsInfo core)) = case Info.lhsEllipsis lhsInfo of + C.ExpandedEllipsis _range _withArgs -> return () + C.NoEllipsis -> index $ WithLHSNaming lhsNaming core + +instance Indexable A.RewriteEqn where + index eqn = case eqn of + C.Rewrite exprs -> + forM_ exprs $ \(_name, expr) -> + index expr + C.Invert _generatedFn bindings -> + forM_ bindings $ \(C.Named maybeName (pat, expr)) -> do + whenJust maybeName $ \bindName -> + tellDef bindName Param UnknownType + index pat + index expr +#if MIN_VERSION_Agda(2,7,0) + C.LeftLet bindings -> + forM_ bindings $ \(pat, expr) -> do + index pat + index expr +#endif + +instance Indexable A.RHS where + index rhs = case rhs of + A.RHS expr _concrete -> + index expr + A.AbsurdRHS -> + return () + A.WithRHS _generatedFn withExprs clauses -> do + forM_ withExprs indexWithExpr + index $ WithLHSNaming LHSAnonymous <$> clauses + A.RewriteRHS rewriteExprs _strippedPats rewriteRhs whereDecls -> do + index rewriteExprs + index rewriteRhs + index whereDecls + +instance Indexable (WithLHSNaming A.Clause) where + index (WithLHSNaming lhsNaming (A.Clause lhs _strippedPats rhs whereDecls _catchall)) = do + index $ WithLHSNaming lhsNaming lhs + index rhs + index whereDecls + +instance Indexable A.ModuleApplication where + index = \case + A.SectionApp tele moduleName args -> do + withBindingKind DeclBinding $ index tele + tellUsage moduleName + indexNamedArgs moduleName args + A.RecordModuleInstance moduleName -> + tellUsage moduleName + +-- Since `HidingDirective' a b` is just `[ImportedName' a b]`, it's much more +-- explicit to give it a special function than try to use instance resolution. +indexHidingDirective :: C.HidingDirective' A.QName A.ModuleName -> IndexerM () +indexHidingDirective = traverse_ tellUsage + +instance Indexable A.Renaming where + index (C.Renaming fromName toName _toFixity _toRange) = do + tellUsage fromName + let toNameKind = case toName of + C.ImportedModule _moduleName -> Module + C.ImportedName _name -> Unknown + tellImport fromName + -- TODO: better handling of renamed imports + tellDef toName toNameKind UnknownType + +instance Indexable (C.Using' A.QName A.ModuleName) where + index using = case using of + C.UseEverything -> return () + C.Using importedNames -> traverse_ tellImport importedNames + +instance Indexable A.ImportDirective where + index (C.ImportDirective _range using hiding renaming _publicRange) = do + index using + indexHidingDirective hiding + index renaming + +instance Indexable A.LetBinding where + index = \case + A.LetBind _letInfo _argInfo boundName type' expr -> do + -- TODO: what does the `ArgInfo` mean? + tellBinding boundName Local type' + index type' + index expr + A.LetPatBind _letInfo pat expr -> do + index pat + index expr + A.LetApply _moduleInfo _erased moduleName moduleApp _scopeCopyInfo importDirective -> do + tellUsage moduleName + index moduleApp + index importDirective + A.LetOpen _moduleInfo moduleName importDirective -> do + tellUsage moduleName + index importDirective +#if MIN_VERSION_Agda(2,8,0) + A.LetAxiom _letInfo _argInfo boundName type' -> do + -- TODO: what does the `ArgInfo` mean? + tellBinding boundName Axiom type' + index type' +#else + A.LetDeclaredVariable boundName -> + -- This is always a declaration + tellDecl boundName Local UnknownType +#endif + +indexNamedArgBinder :: + (TypeLike t, HasParamNames t) => + C.NamedArg A.Binder -> t -> IndexerM () +#if MIN_VERSION_Agda(2,8,0) +indexNamedArgBinder + (C.Arg argInfo (C.Named _maybeArgName (A.Binder pat nameOrigin name))) + typeLike = + when (C.argInfoOrigin argInfo == C.UserWritten && nameOrigin == C.UserBinderName) $ do + tellBinding name Param typeLike + index pat +#else +indexNamedArgBinder + (C.Arg argInfo (C.Named _maybeArgName (A.Binder pat name))) + typeLike = + when (C.argInfoOrigin argInfo == C.UserWritten) $ do + tellBinding name Param typeLike + index pat +#endif + +instance Indexable A.TypedBinding where + index = \case + A.TBind _range typedBindInfo binders type' -> do + index $ A.tbTacticAttr typedBindInfo + forM_ binders $ \binder -> + indexNamedArgBinder binder type' + index type' + A.TLet _range letBindings -> index letBindings + +instance Indexable A.LamBinding where + index lamBinding = case lamBinding of + A.DomainFree tacticAttr binder -> do + index tacticAttr + indexNamedArgBinder binder UnknownType + A.DomainFull binding -> + index binding + +instance Indexable A.GeneralizeTelescope where + index (A.GeneralizeTel _generalizeVars tel) = index tel + +instance Indexable A.DataDefParams where + index (A.DataDefParams _generalizeParams params) = + withBindingKind DefBinding $ index params + +instance Indexable A.RecordDirectives where + index = \case +#if MIN_VERSION_Agda(2,8,0) + (C.RecordDirectives inductive _hasEta _patRange (A.NamedRecCon conName)) -> +#else + (C.RecordDirectives inductive _hasEta _patRange (Just conName)) -> +#endif + tellDef conName (constructorSymbolKind inductive) UnknownType + _noUserConstructor -> return () + where + constructorSymbolKind :: Maybe (C.Ranged C.Induction) -> SymbolKind + constructorSymbolKind (Just (C.Ranged _range C.CoInductive)) = CoCon + constructorSymbolKind _inductive = Con + +instance Indexable A.Pragma where + index = \case + A.OptionsPragma _options -> + return () + A.BuiltinPragma _rstring resolvedName -> + whenJust (resolvedNameToAmbiguousQName resolvedName) $ \name -> + tellUsage name + A.BuiltinNoDefPragma _rstring kindOfName name -> do + tellDef name kindOfName UnknownType + A.RewritePragma _range ruleNames -> + forM_ ruleNames $ \ruleName -> + tellUsage ruleName + A.CompilePragma _backendName name _compileAs -> + tellUsage name + A.StaticPragma name -> + tellUsage name + A.EtaPragma name -> + tellUsage name + A.InjectivePragma name -> + tellUsage name + A.InlinePragma _shouldInline name -> + tellUsage name + A.NotProjectionLikePragma name -> + tellUsage name + A.DisplayPragma name args displayExpr -> do + tellUsage name + indexNamedArgs name args + index displayExpr +#if MIN_VERSION_Agda(2,7,0) + A.InjectiveForInferencePragma name -> + tellUsage name + A.OverlapPragma name _overlapMode -> + tellUsage name +#endif + +-------------------------------------------------------------------------------- + +instance NameLike A.QName where + toQName = id + +instance NameLike A.ModuleName where + toQName = A.mnameToQName + +instance NameLike A.Name where + toQName = A.qualify_ + +instance NameLike A.BindName where + toQName = toQName . A.unBind + +instance (NameLike n, NameLike m) => NameLike (C.ImportedName' n m) where + toQName (C.ImportedModule moduleName) = toQName moduleName + toQName (C.ImportedName name) = toQName name + +instance AmbiguousNameLike A.AmbiguousQName where + toAmbiguousQName = id + +instance AmbiguousNameLike A.QName where + toAmbiguousQName = A.unambiguous + +instance AmbiguousNameLike A.ModuleName where + toAmbiguousQName = toAmbiguousQName . A.mnameToQName + +instance AmbiguousNameLike A.Name where + toAmbiguousQName = toAmbiguousQName . A.qualify_ + +instance AmbiguousNameLike A.BindName where + toAmbiguousQName = toAmbiguousQName . A.unBind + +instance AmbiguousNameLike Scope.AbstractName where + toAmbiguousQName = toAmbiguousQName . Scope.anameName + +instance (AmbiguousNameLike n, AmbiguousNameLike m) => AmbiguousNameLike (C.ImportedName' n m) where + toAmbiguousQName (C.ImportedModule moduleName) = toAmbiguousQName moduleName + toAmbiguousQName (C.ImportedName name) = toAmbiguousQName name + +resolvedNameToAmbiguousQName :: Scope.ResolvedName -> Maybe A.AmbiguousQName +resolvedNameToAmbiguousQName = \case + Scope.VarName name _bindingSource -> Just $ toAmbiguousQName name + Scope.DefinedName _access name _suffix -> Just $ toAmbiguousQName name + Scope.FieldName name -> Just $ toAmbiguousQName name + Scope.ConstructorName _inductive name -> Just $ toAmbiguousQName name + Scope.PatternSynResName name -> Just $ toAmbiguousQName name + Scope.UnknownName -> Nothing + +instance SymbolKindLike SymbolKind where + toSymbolKind = id + +instance SymbolKindLike Scope.KindOfName where + toSymbolKind = \case + Scope.ConName -> Con + Scope.CoConName -> CoCon + Scope.FldName -> Field + Scope.PatternSynName -> PatternSyn + Scope.GeneralizeName -> GeneralizeVar + Scope.DisallowedGeneralizeName -> GeneralizeVar + Scope.MacroName -> Macro + Scope.QuotableName -> Unknown + Scope.DataName -> Data + Scope.RecName -> Record + Scope.FunName -> Fun + Scope.AxiomName -> Axiom + Scope.PrimName -> Prim + Scope.OtherDefName -> Unknown + +instance SymbolKindLike TCM.Defn where + toSymbolKind = \case + TCM.AxiomDefn _axiomData -> Axiom + TCM.DataOrRecSigDefn _dataOrRecSigData -> Unknown +#if MIN_VERSION_Agda(2,8,0) + TCM.GeneralizableVar _numGeneralizableArgs -> GeneralizeVar +#else + TCM.GeneralizableVar -> GeneralizeVar +#endif + TCM.AbstractDefn defn -> toSymbolKind defn + TCM.FunctionDefn _functionData -> Fun + TCM.DatatypeDefn _datatypeData -> Data + TCM.RecordDefn _recordData -> Record + TCM.ConstructorDefn _constructorData -> Con + TCM.PrimitiveDefn _primitiveData -> Prim + TCM.PrimitiveSortDefn _primitiveSortData -> Prim + +instance (TypeLike t) => TypeLike (C.Arg t) where + toTypeString = toTypeString . C.unArg + +instance TypeLike A.Type where + toTypeString = fmap (Just . render) . TCM.liftTCM . prettyTCM + +instance TypeLike I.Type where + toTypeString = fmap (Just . render) . TCM.liftTCM . prettyTCM + +instance (HasParamNames p) => HasParamNames (C.Arg p) where + getParamNames = getParamNames . C.unArg + +instance (HasParamNames p) => HasParamNames [p] + +instance (HasParamNames p) => HasParamNames (List1 p) + +instance HasParamNames A.Type where + getParamNames = \case + A.Pi _exprInfo tel codom -> + getParamNames tel <> getParamNames codom + A.Fun _exprInfo _dom codom -> getParamNames codom + A.Generalized varNames codom -> + toList varNames <> getParamNames codom + A.ScopedExpr _scopeInfo expr -> getParamNames expr + _noMoreParams -> [] + +instance HasParamNames A.TypedBinding where + getParamNames = \case + A.TBind _range _typedBindingInfo binders' _type -> + List1.toList binders' + <&> C.namedThing . C.unArg + <&> (A.qualify_ . A.unBind . A.binderName) + A.TLet _range _letBindings -> [] + +instance HasParamNames A.GeneralizeTelescope where + getParamNames (A.GeneralizeTel _vars tel) = getParamNames tel diff --git a/src/Indexer/Monad.hs b/src/Indexer/Monad.hs new file mode 100644 index 0000000..543c6d0 --- /dev/null +++ b/src/Indexer/Monad.hs @@ -0,0 +1,269 @@ +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Indexer.Monad + ( IndexerM, + execIndexerM, + modifyAgdaFile', + tellParamNames, + DataRecordParams (..), + tellDefParams, + tellGenTel, + getDataRecordParams, + tellDef, + tellDecl, + tellBinding, + tellUsage, + tellImport, + tellNamedArgUsage, + withParent, + BindingKind (..), + withBindingKind, + NameLike (..), + AmbiguousNameLike (..), + SymbolKindLike (..), + TypeLike (..), + HasParamNames (..), + UnknownType (UnknownType), + NoType (NoType), + ) +where + +import Agda.Position (toLspRange) +import qualified Agda.Syntax.Abstract as A +import qualified Agda.Syntax.Common as C +import Agda.Syntax.Position (getRange) +import Agda.Utils.IORef (IORef, modifyIORef', newIORef, readIORef) +import Agda.Utils.List1 (List1, concatMap1) +import Control.Applicative ((<|>)) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) +import Control.Monad.Trans (lift) +import Data.Map (Map) +import qualified Data.Map as Map +import Server.Model.AgdaFile (AgdaFile, emptyAgdaFile, insertRef, insertSymbolInfo) +import Server.Model.Monad (WithAgdaLibM) +import Server.Model.Symbol (Ref (Ref), RefKind (..), SymbolInfo (..), SymbolKind (..)) + +data NamedArgUsage = NamedArgUsage + { nauHead :: !A.AmbiguousQName, + nauArg :: !C.NamedName + } + +data DataRecordParams = DataRecordParams + { drpGenTel :: !(Maybe A.GeneralizeTelescope), + drpParams :: !(Maybe A.DataDefParams) + } + +instance Semigroup DataRecordParams where + DataRecordParams x y <> DataRecordParams x' y' = DataRecordParams (x <|> x') (y <|> y') + +instance Monoid DataRecordParams where + mempty = DataRecordParams Nothing Nothing + +data BindingKind = DeclBinding | DefBinding + +bindingKindToRefKind :: BindingKind -> RefKind +bindingKindToRefKind DeclBinding = Decl +bindingKindToRefKind DefBinding = Def + +data Env = Env + { envAgdaFile :: !(IORef AgdaFile), + envParent :: !(Maybe A.QName), + envBindingKind :: !BindingKind, + -- | Parameter names in implicit arguments, such as x in `f {x = y} = y` and + -- `g y = f {x = y}`, are represented by strings in abstract syntax. This is + -- because we need type checking information to resolve these names, not + -- just scope checking information. + -- + -- Agda doesn't seem to expose its internal type checker resolution of these + -- names. We hack around it by storing the implicit parameter names for each + -- function ourselves, then looking up the strings at the end and emitting + -- them as references. Ideally, this solution is eventually replaced by + -- changing the type checker so it emits this information for us. + -- + -- These are the stored parameter names, indexed by the name of the function + -- (or other defined symbol). + envParamNames :: !(IORef (Map A.QName [A.QName])), + envNamedArgUsages :: !(IORef [NamedArgUsage]), + envDataRecordParams :: !(IORef (Map A.QName DataRecordParams)) + } + +initEnv :: (MonadIO m) => m Env +initEnv = do + agdaFile <- liftIO $ newIORef emptyAgdaFile + let parent = Nothing + paramNames <- liftIO $ newIORef Map.empty + namedArgUsages <- liftIO $ newIORef [] + dataRecordParams <- liftIO $ newIORef mempty + return $ Env agdaFile parent DeclBinding paramNames namedArgUsages dataRecordParams + +type IndexerM = ReaderT Env WithAgdaLibM + +execIndexerM :: IndexerM a -> WithAgdaLibM AgdaFile +execIndexerM x = do + env <- initEnv + _ <- runReaderT x env + liftIO $ readIORef $ envAgdaFile env + +-------------------------------------------------------------------------------- + +modifyAgdaFile' :: (AgdaFile -> AgdaFile) -> IndexerM () +modifyAgdaFile' f = do + agdaFileRef <- asks envAgdaFile + liftIO $ modifyIORef' agdaFileRef f + +tellSymbolInfo' :: A.QName -> SymbolInfo -> IndexerM () +tellSymbolInfo' name symbolInfo = do + agdaFileRef <- asks envAgdaFile + liftIO $ modifyIORef' agdaFileRef $ insertSymbolInfo name symbolInfo + +tellSymbolInfo :: + (NameLike n, SymbolKindLike s, TypeLike t) => + n -> s -> t -> IndexerM () +tellSymbolInfo nameLike symbolKindLike typeLike = do + let name = toQName nameLike + symbolKind = toSymbolKind symbolKindLike + type' <- lift $ toTypeString typeLike + parent <- asks envParent + let symbolInfo = SymbolInfo name symbolKind type' parent + tellSymbolInfo' name symbolInfo + +tellRef' :: A.AmbiguousQName -> Ref -> IndexerM () +tellRef' ambiguousName ref = do + agdaFileRef <- asks envAgdaFile + liftIO $ modifyIORef' agdaFileRef $ insertRef ambiguousName ref + +tellRef :: + (AmbiguousNameLike n) => + n -> RefKind -> IndexerM () +tellRef nameLike refKind = do + let name = toAmbiguousQName nameLike + range = toLspRange $ getRange name + ref = Ref refKind range (A.isAmbiguous name) + tellRef' name ref + +tellParamNames :: (NameLike n, HasParamNames p) => n -> p -> IndexerM () +tellParamNames nameLike hasParamNames = do + let name = toQName nameLike + let paramNames = getParamNames hasParamNames + paramNamesRef <- asks envParamNames + liftIO $ modifyIORef' paramNamesRef $ Map.insert name paramNames + +tellDefParams :: (NameLike n) => n -> A.DataDefParams -> IndexerM () +tellDefParams nameLike defParams = do + let name = toQName nameLike + dataRecordParamsRef <- asks envDataRecordParams + liftIO $ + modifyIORef' dataRecordParamsRef $ + Map.insertWith (<>) name (DataRecordParams Nothing (Just defParams)) + +tellGenTel :: (NameLike n) => n -> A.GeneralizeTelescope -> IndexerM () +tellGenTel nameLike genTel = do + let name = toQName nameLike + dataRecordParamsRef <- asks envDataRecordParams + liftIO $ + modifyIORef' dataRecordParamsRef $ + Map.insertWith (<>) name (DataRecordParams (Just genTel) Nothing) + +getDataRecordParams :: IndexerM (Map A.QName DataRecordParams) +getDataRecordParams = do + dataRecordParamsRef <- asks envDataRecordParams + liftIO $ readIORef dataRecordParamsRef + +tellBinding' :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + BindingKind -> n -> s -> t -> IndexerM () +tellBinding' b n s t = do + tellSymbolInfo n s t + tellRef n (bindingKindToRefKind b) + tellParamNames n t + +tellDef :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + n -> s -> t -> IndexerM () +tellDef = tellBinding' DefBinding + +tellDecl :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + n -> s -> t -> IndexerM () +tellDecl = tellBinding' DeclBinding + +tellBinding :: + (NameLike n, SymbolKindLike s, TypeLike t, HasParamNames t) => + n -> s -> t -> IndexerM () +tellBinding n s t = do + b <- asks envBindingKind + tellBinding' b n s t + +tellUsage :: (AmbiguousNameLike n) => n -> IndexerM () +tellUsage n = tellRef n Usage + +tellImport :: (AmbiguousNameLike n) => n -> IndexerM () +tellImport n = tellRef n Import + +tellNamedArgUsage :: (AmbiguousNameLike n) => n -> C.NamedName -> IndexerM () +tellNamedArgUsage headNameLike argName = do + let headName = toAmbiguousQName headNameLike + namedArgUsage = NamedArgUsage headName argName + namedArgUsagesRef <- asks envNamedArgUsages + liftIO $ modifyIORef' namedArgUsagesRef $ (namedArgUsage :) + +withParent :: (NameLike n) => n -> IndexerM a -> IndexerM a +withParent nameLike = local $ \e -> e {envParent = Just $ toQName nameLike} + +withBindingKind :: BindingKind -> IndexerM a -> IndexerM a +withBindingKind bindingKind = local $ \e -> e {envBindingKind = bindingKind} + +-------------------------------------------------------------------------------- + +class (AmbiguousNameLike n) => NameLike n where + toQName :: n -> A.QName + +class AmbiguousNameLike n where + toAmbiguousQName :: n -> A.AmbiguousQName + +instance (AmbiguousNameLike n) => AmbiguousNameLike (List1 n) where + toAmbiguousQName = A.AmbQ . concatMap1 (A.unAmbQ . toAmbiguousQName) + +class SymbolKindLike a where + toSymbolKind :: a -> SymbolKind + +class HasParamNames p where + getParamNames :: p -> [A.QName] + default getParamNames :: (Foldable f, HasParamNames b, p ~ f b) => p -> [A.QName] + getParamNames = foldMap getParamNames + +instance (HasParamNames p) => HasParamNames (Maybe p) where + getParamNames = maybe [] getParamNames + +class TypeLike t where + -- | Try to render a type to a @String@. Strings were chosen because: + -- - they are easily obtained from abstract and internal terms + -- - they do not depend on the scope, context, or other TC state + -- - they have a low memory footprint compared to unrendered @Doc@s + -- + -- However, strings do lose semantic information otherwise available to us, + -- so this representation may be switched in the future if that information is + -- needed. + toTypeString :: t -> WithAgdaLibM (Maybe String) + +instance (TypeLike t) => TypeLike (Maybe t) where + toTypeString = maybe (return Nothing) toTypeString + +data UnknownType = UnknownType + +instance HasParamNames UnknownType where + getParamNames UnknownType = [] + +instance TypeLike UnknownType where + toTypeString UnknownType = return Nothing + +data NoType = NoType + +instance HasParamNames NoType where + getParamNames NoType = [] + +instance TypeLike NoType where + toTypeString NoType = return Nothing diff --git a/src/Indexer/Postprocess.hs b/src/Indexer/Postprocess.hs new file mode 100644 index 0000000..2ad2879 --- /dev/null +++ b/src/Indexer/Postprocess.hs @@ -0,0 +1,57 @@ +module Indexer.Postprocess (postprocess) where + +import qualified Agda.Syntax.Abstract as A +import qualified Agda.Syntax.Common as C +import Agda.Utils.Lens (over) +import Control.Arrow ((>>>)) +import Data.Foldable (Foldable (toList), find) +import qualified Data.Map as Map +import Indexer.Monad (DataRecordParams (DataRecordParams), IndexerM, getDataRecordParams, modifyAgdaFile') +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs, mergeSymbols) +import Server.Model.Symbol (Ref, RefKind (..), refKind, refRange) + +postprocess :: IndexerM () +postprocess = do + dataRecordParams <- Map.elems <$> getDataRecordParams + modifyAgdaFile' $ + dedupDataRecordParams dataRecordParams + >>> dedupSimultaneousDeclDef + +-- | We sometimes emit a `Decl` and `Def` for the same source range. For +-- example, we must emit a distinct `Decl` and `Def` when a `data` is declared +-- and defined separately, but not when it is declared and defined all at once. +-- It is harder distinguish these in abstract syntax than to idenfify and +-- correct them at the end. +dedupSimultaneousDeclDef :: AgdaFile -> AgdaFile +dedupSimultaneousDeclDef = over agdaFileRefs $ Map.map worker + where + worker :: [Ref] -> [Ref] + worker refs = + case find (\ref -> refKind ref == Decl) refs of + Nothing -> refs + Just decl -> + let pred ref = not (refKind ref == Def && refRange ref == refRange decl) + in filter pred refs + +dedupDataRecordParams :: [DataRecordParams] -> AgdaFile -> AgdaFile +dedupDataRecordParams dataRecordParams file = foldl' (flip worker) file dataRecordParams + where + namedArgBinderName :: C.NamedArg A.Binder -> A.QName + namedArgBinderName namedArgBinder = + A.qualify_ $ A.unBind $ A.binderName $ C.namedThing $ C.unArg namedArgBinder + typedBindingNames :: A.TypedBinding -> [A.QName] + typedBindingNames = \case + A.TBind _range _typedBindingInfo nabs _type' -> + namedArgBinderName <$> toList nabs + A.TLet _range _letBindings -> [] + lamBindingNames :: A.LamBinding -> [A.QName] + lamBindingNames = \case + A.DomainFree _tacticAttr nab -> [namedArgBinderName nab] + A.DomainFull typedBindings -> typedBindingNames typedBindings + worker :: DataRecordParams -> AgdaFile -> AgdaFile + worker (DataRecordParams (Just genTel) (Just params)) file = + let paramsNames = concatMap lamBindingNames $ A.dataDefParams params + genTelNames = concatMap typedBindingNames $ A.generalizeTel genTel + names = zip paramsNames genTelNames + in foldl' (\file (old, new) -> mergeSymbols old new file) file names + worker _missingParams file = file diff --git a/src/Language/LSP/Protocol/Types/More.hs b/src/Language/LSP/Protocol/Types/More.hs new file mode 100644 index 0000000..c64f51f --- /dev/null +++ b/src/Language/LSP/Protocol/Types/More.hs @@ -0,0 +1,24 @@ +module Language.LSP.Protocol.Types.More () where + +import Agda.Syntax.Common.Pretty +import Agda.Utils.Lens ((^.)) +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Types as LSP + +instance Pretty LSP.Uri where + pretty = text . Text.unpack . LSP.getUri + +instance Pretty LSP.Position where + pretty pos = pshow (pos ^. LSP.line + 1) <> text ":" <> pshow (pos ^. LSP.character + 1) + +instance Pretty LSP.Range where + pretty range = + if range ^. LSP.start . LSP.line == range ^. LSP.end . LSP.line + then + pshow (range ^. LSP.start . LSP.line + 1) + <> text ":" + <> pshow (range ^. LSP.start . LSP.character + 1) + <> text "-" + <> pshow (range ^. LSP.end . LSP.character + 1) + else pretty (range ^. LSP.start) <> text "-" <> pretty (range ^. LSP.end) diff --git a/src/Language/LSP/Protocol/Types/Uri/More.hs b/src/Language/LSP/Protocol/Types/Uri/More.hs new file mode 100644 index 0000000..f5823d0 --- /dev/null +++ b/src/Language/LSP/Protocol/Types/Uri/More.hs @@ -0,0 +1,102 @@ +module Language.LSP.Protocol.Types.Uri.More + ( getNormalizedUri, + isUriAncestorOf, + uriHeightAbove, + uriParent, + uriExtension, + uriToPossiblyInvalidAbsolutePath, + uriToPossiblyInvalidFilePath, + ) +where + +import Agda.Utils.FileName (AbsolutePath (AbsolutePath), absolute) +import Agda.Utils.Lens (set, (^.)) +import Agda.Utils.List (initMaybe, lastMaybe) +import Agda.Utils.Maybe (fromMaybe) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Data.Function ((&)) +import Data.Text (Text) +import qualified Data.Text as Text +import Language.LSP.Protocol.Types (uriToFilePath) +import qualified Language.LSP.Protocol.Types as LSP +import qualified Text.URI as ParsedUri +import qualified Text.URI.Lens as ParsedUriLens + +getNormalizedUri :: LSP.NormalizedUri -> Text +getNormalizedUri = LSP.getUri . LSP.fromNormalizedUri + +-- | Determine if the first URI is an ancestor of the second. +-- +-- This is a heuristic implementation and may need replacement if the heuristic +-- leads to bugs. +isUriAncestorOf :: LSP.NormalizedUri -> LSP.NormalizedUri -> Bool +isUriAncestorOf ancestor descendant = + getNormalizedUri ancestor `Text.isPrefixOf` getNormalizedUri descendant + +-- | If @ancestor@ is an ancestor of @descendant@, then +-- @uriHeightAbove ancestor descendant@ is the height of @ancestor@ above +-- @descendant@. +-- +-- For example, the height of @https://example.com/a/@ over +-- @https://example.com/a/b/c/@ is 2. +-- +-- This is a heuristic implementation and may need replacement if the heuristic +-- leads to bugs. +uriHeightAbove :: LSP.NormalizedUri -> LSP.NormalizedUri -> Int +uriHeightAbove ancestor descendant = + let suffix = pathBetween (getNormalizedUri ancestor) (getNormalizedUri descendant) + path = stripSlash $ stripScheme suffix + in countPathComponents path + where + pathBetween :: Text -> Text -> Text + pathBetween a b = case Text.commonPrefixes a b of + Just (_prefix, _suffixA, suffixB) -> suffixB + Nothing -> "" + + stripScheme :: Text -> Text + stripScheme uri = + let (prefix, suffix) = Text.breakOn "//" uri + in if Text.null suffix then prefix else suffix + + stripSlash :: Text -> Text + stripSlash = Text.dropAround (== '/') + + countPathComponents :: Text -> Int + countPathComponents path = + if Text.null path + then 0 + else Text.count "/" path + 1 + +uriParent :: LSP.NormalizedUri -> Maybe LSP.NormalizedUri +uriParent uri = do + parsedUri <- ParsedUri.mkURI $ getNormalizedUri uri + pathInit <- initMaybe $ parsedUri ^. ParsedUriLens.uriPath + let newParsedUri = set ParsedUriLens.uriPath pathInit parsedUri + return $ LSP.toNormalizedUri $ LSP.Uri $ ParsedUri.render newParsedUri + +uriExtension :: LSP.NormalizedUri -> Text +uriExtension uri = fromMaybe "" $ do + parsedUri <- ParsedUri.mkURI $ getNormalizedUri uri + pathEndRefined <- lastMaybe $ parsedUri ^. ParsedUriLens.uriPath + let pathEnd = ParsedUri.unRText pathEndRefined + let (prefix, suffix) = Text.breakOnEnd "." pathEnd + if Text.null prefix -- The prefix will contain the final ".", if one is found + then Nothing + else return $ "." <> suffix + +uriToPossiblyInvalidAbsolutePath :: (MonadIO m) => LSP.NormalizedUri -> m AbsolutePath +uriToPossiblyInvalidAbsolutePath uri = do + case LSP.uriToFilePath $ LSP.fromNormalizedUri uri of + Just path -> liftIO $ absolute path + Nothing -> return $ uriToInvalidAbsolutePath uri + +uriToInvalidAbsolutePath :: LSP.NormalizedUri -> AbsolutePath +uriToInvalidAbsolutePath = AbsolutePath . getNormalizedUri + +uriToPossiblyInvalidFilePath :: LSP.NormalizedUri -> FilePath +uriToPossiblyInvalidFilePath uri = case LSP.uriToFilePath $ LSP.fromNormalizedUri uri of + Just path -> path + Nothing -> uriToInvalidFilePath uri + +uriToInvalidFilePath :: LSP.NormalizedUri -> FilePath +uriToInvalidFilePath = Text.unpack . getNormalizedUri diff --git a/src/Monad.hs b/src/Monad.hs index 3726b86..d3efe02 100644 --- a/src/Monad.hs +++ b/src/Monad.hs @@ -1,12 +1,20 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} module Monad where import Agda.IR import Agda.Interaction.Base (IOTCM) +import Agda.Interaction.Library (findProjectRoot) +import Agda.Interaction.Library.More (tryRunLibM) import Agda.TypeChecking.Monad (TCMT) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.Lens (Lens', (^.)) import Control.Concurrent +import Control.Exception (Exception) +import qualified Control.Exception as E import Control.Monad.Reader import Data.IORef ( IORef, @@ -15,21 +23,31 @@ import Data.IORef readIORef, writeIORef, ) -import Data.Maybe (isJust) +import Data.Maybe (fromMaybe, isJust) import Data.Text ( Text, pack, ) import qualified Language.LSP.Protocol.Types as LSP import Language.LSP.Server - ( MonadLsp, + ( LspM, + MonadLsp, getConfig, ) +import qualified Language.LSP.Server as LSP import Options import Server.CommandController (CommandController) import qualified Server.CommandController as CommandController +import Server.Filesystem (MonadFilesystem) +import qualified Server.Filesystem as FS +import Server.Model (Model) +import qualified Server.Model as Model +import Server.Model.AgdaLib (AgdaLib, initAgdaLib) import Server.ResponseController (ResponseController) import qualified Server.ResponseController as ResponseController +import Server.VfsIndex (VfsIndex) +import qualified Server.VfsIndex as VfsIndex +import System.FilePath (takeDirectory) -------------------------------------------------------------------------------- @@ -40,7 +58,10 @@ data Env = Env envLogChan :: Chan Text, envCommandController :: CommandController, envResponseChan :: Chan Response, - envResponseController :: ResponseController + envResponseController :: ResponseController, + envFilesystemProvider :: !FS.Layered, + envVfsIndex :: !(IORef VfsIndex), + envModel :: !(IORef Model) } createInitEnv :: (MonadIO m, MonadLsp Config m) => Options -> m Env @@ -51,43 +72,80 @@ createInitEnv options = <*> liftIO CommandController.new <*> liftIO newChan <*> liftIO ResponseController.new + <*> (pure $ FS.Layered [FS.Wrap FS.LspVirtualFilesystem, FS.Wrap FS.OsFilesystem]) + <*> liftIO (newIORef VfsIndex.empty) + <*> liftIO (newIORef Model.empty) -------------------------------------------------------------------------------- -- | OUR monad -type ServerM m = ReaderT Env m +type ServerT m = ReaderT Env m -runServerM :: Env -> ServerM m a -> m a -runServerM = flip runReaderT +type ServerM = ServerT (LspM Config) + +runServerT :: Env -> ServerT m a -> m a +runServerT = flip runReaderT + +instance MonadFilesystem ServerM where + askVfsIndex = askVfsIndex -------------------------------------------------------------------------------- -writeLog :: (Monad m, MonadIO m) => Text -> ServerM m () +writeLog :: (Monad m, MonadIO m) => Text -> ServerT m () writeLog msg = do chan <- asks envLogChan liftIO $ writeChan chan msg -writeLog' :: (Monad m, MonadIO m, Show a) => a -> ServerM m () +writeLog' :: (Monad m, MonadIO m, Show a) => a -> ServerT m () writeLog' x = do chan <- asks envLogChan liftIO $ writeChan chan $ pack $ show x +askFilesystemProvider :: (MonadIO m) => ServerT m FS.Layered +askFilesystemProvider = asks envFilesystemProvider + +askModel :: (MonadIO m) => ServerT m Model +askModel = do + modelVar <- asks envModel + liftIO $ readIORef modelVar + +modifyModel :: (MonadIO m) => (Model -> Model) -> ServerT m () +modifyModel f = do + modelVar <- asks envModel + liftIO $ modifyIORef' modelVar f + +askVfsIndex :: (MonadIO m) => ServerT m VfsIndex +askVfsIndex = do + vfsIndexVar <- asks envVfsIndex + liftIO $ readIORef vfsIndexVar + +modifyVfsIndex :: (MonadIO m) => (VfsIndex -> VfsIndex) -> ServerT m () +modifyVfsIndex f = do + vfsIndexVar <- asks envVfsIndex + liftIO $ modifyIORef' vfsIndexVar f + +catchTCError :: ServerM a -> (TCM.TCErr -> ServerM a) -> ServerM a +catchTCError m h = + ReaderT $ \env -> LSP.LspT $ ReaderT $ \lspEnv -> + LSP.runLspT lspEnv (runServerT env m) + `E.catch` \err -> LSP.runLspT lspEnv (runServerT env (h err)) + -- | Provider -provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerM m () +provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerT m () provideCommand iotcm = do controller <- asks envCommandController liftIO $ CommandController.put controller iotcm --- | Consumter +-- | Consumer consumeCommand :: (Monad m, MonadIO m) => Env -> m IOTCM consumeCommand env = liftIO $ CommandController.take (envCommandController env) -waitUntilResponsesSent :: (Monad m, MonadIO m) => ServerM m () +waitUntilResponsesSent :: (Monad m, MonadIO m) => ServerT m () waitUntilResponsesSent = do controller <- asks envResponseController liftIO $ ResponseController.setCheckpointAndWait controller -signalCommandFinish :: (Monad m, MonadIO m) => ServerM m () +signalCommandFinish :: (Monad m, MonadIO m) => ServerT m () signalCommandFinish = do writeLog "[Command] Finished" -- send `ResponseEnd` diff --git a/src/Options.hs b/src/Options.hs index 27742d5..d79be07 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -3,6 +3,7 @@ module Options ( Options (..), + defaultOptions, getOptionsFromArgv, versionNumber, versionString, @@ -42,12 +43,13 @@ data Options = Options optRawResponses :: Bool, optSetup :: Bool, optHelp :: Bool, - optVersion :: Bool + optVersion :: Bool, + optStdin :: Bool } defaultOptions :: Options defaultOptions = - Options {optViaTCP = Nothing, optRawAgdaOptions = [], optRawResponses = False, optSetup = False, optHelp = False, optVersion = False} + Options {optViaTCP = Nothing, optRawAgdaOptions = [], optRawResponses = False, optSetup = False, optHelp = False, optVersion = False, optStdin = False} options :: [OptDescr (Options -> Options)] options = @@ -83,7 +85,12 @@ options = ['V'] ["version"] (NoArg (\opts -> opts {optVersion = True})) - "print version information and exit" + "print version information and exit", + Option + [] + ["stdio"] + (NoArg (\opts -> opts {optStdin = True})) + "connect via stdio" ] versionNumber :: Int diff --git a/src/Server.hs b/src/Server.hs index df833f4..41fd5a6 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -28,6 +28,8 @@ import Options import qualified Server.Handler as Handler import Switchboard (Switchboard, agdaCustomMethod) import qualified Switchboard +import Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) +import Server.Handler.TextDocument.FileManagement (didOpenHandler, didCloseHandler, didSaveHandler) #if defined(wasm32_HOST_ARCH) import Agda.Utils.IO (catchIO) @@ -74,14 +76,14 @@ run options = do staticHandlers = const handlers, interpretHandler = \(ctxEnv, env) -> Iso - { forward = runLspT ctxEnv . runServerM env, + { forward = runLspT ctxEnv . runServerT env, backward = liftIO }, options = lspOptions } lspOptions :: LSP.Options -lspOptions = defaultOptions {optTextDocumentSync = Just syncOptions} +lspOptions = LSP.defaultOptions {optTextDocumentSync = Just syncOptions} -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client -- syncOptions :: TextDocumentSyncOptions @@ -100,11 +102,11 @@ syncOptions = _change = Just TextDocumentSyncKind_Incremental, -- receive change notifications from the client _willSave = Just False, -- receive willSave notifications from the client _willSaveWaitUntil = Just False, -- receive willSave notifications from the client - _save = Just $ InR $ SaveOptions (Just True) -- includes the document content on save, so that we don't have to read it from the disk (not sure if this is still true in lsp 2) + _save = Just $ InR $ SaveOptions (Just False) } -- handlers of the LSP server -handlers :: Handlers (ServerM (LspM Config)) +handlers :: Handlers ServerM handlers = mconcat [ -- custom methods, not part of LSP @@ -117,6 +119,7 @@ handlers = let TRequestMessage _ _ _ (HoverParams (TextDocumentIdentifier uri) pos _workDone) = req result <- Handler.onHover uri pos responder $ Right result, + documentSymbolHandler, -- -- syntax highlighting -- , requestHandler STextDocumentSemanticTokensFull $ \req responder -> do -- result <- Handler.onHighlight (req ^. (params . textDocument . uri)) @@ -127,11 +130,11 @@ handlers = -- `workspace/didChangeConfiguration` notificationHandler SMethod_WorkspaceDidChangeConfiguration $ \_notification -> return (), -- `textDocument/didOpen` - notificationHandler SMethod_TextDocumentDidOpen $ \_notification -> return (), + didOpenHandler, -- `textDocument/didClose` - notificationHandler SMethod_TextDocumentDidClose $ \_notification -> return (), + didCloseHandler, -- `textDocument/didChange` notificationHandler SMethod_TextDocumentDidChange $ \_notification -> return (), -- `textDocument/didSave` - notificationHandler SMethod_TextDocumentDidSave $ \_notification -> return () - ] \ No newline at end of file + didSaveHandler + ] diff --git a/src/Server/AgdaLibResolver.hs b/src/Server/AgdaLibResolver.hs new file mode 100644 index 0000000..187e06b --- /dev/null +++ b/src/Server/AgdaLibResolver.hs @@ -0,0 +1,62 @@ +module Server.AgdaLibResolver (findAgdaLib) where + +import Agda.Interaction.Library (AgdaLibFile) +import Agda.Interaction.Library.Parse.More (parseLibFile, runP) +import Agda.Utils.Either (maybeRight) +import Agda.Utils.Maybe (caseMaybe, ifJust, listToMaybe) +import qualified Language.LSP.Protocol.Types as LSP +import Monad (ServerM, askFilesystemProvider, askModel, modifyModel) +import qualified Server.Filesystem as FS +import qualified Server.Model as Model +import Server.Model.AgdaLib (AgdaLib, agdaLibFromFile, initAgdaLib) + +-- | Find cached 'AgdaLib', or else make one from @.agda-lib@ files on the file +-- system, or else provide a default +findAgdaLib :: (FS.IsFileId f) => f -> ServerM AgdaLib +findAgdaLib isFileId = do + let fileId = FS.toFileId isFileId + let uri = FS.fileIdToUri fileId + model <- askModel + case Model.getKnownAgdaLib uri model of + Just lib -> return lib + Nothing -> do + provider <- askFilesystemProvider + result <- searchFilesystemForAgdaLib provider fileId + lib <- case result of + Just lib -> return lib + Nothing -> initAgdaLib + modifyModel $ Model.withAgdaLib lib + return lib + +searchFilesystemForAgdaLib :: (FS.Provider p, FS.IsFileId f) => p -> f -> ServerM (Maybe AgdaLib) +searchFilesystemForAgdaLib provider agdaIsFileId = do + let agdaFileId = FS.toFileId agdaIsFileId + libFileId <- searchForAgdaLibFile provider agdaFileId + case libFileId of + Nothing -> return Nothing + Just fileId -> do + agdaLibFile <- fileIdToAgdaLibFile provider fileId + case agdaLibFile of + Nothing -> return Nothing + Just agdaLibFile -> do + agdaLib <- agdaLibFromFile agdaLibFile fileId + return $ Just agdaLib + where + searchForAgdaLibFile :: (FS.Provider p) => p -> FS.FileId -> ServerM (Maybe FS.FileId) + searchForAgdaLibFile provider childFileId = do + parentFileId <- FS.fileIdParent childFileId + caseMaybe parentFileId (return Nothing) $ \parentFileId -> do + children <- FS.getChildren provider parentFileId + let candidates = filter (\child -> FS.fileIdExtension child == ".agda-lib") children + case listToMaybe candidates of + Nothing -> searchForAgdaLibFile provider parentFileId + Just candidate -> return $ Just candidate + + fileIdToAgdaLibFile :: (FS.Provider p) => p -> FS.FileId -> ServerM (Maybe AgdaLibFile) + fileIdToAgdaLibFile provider fileId = do + agdaLibFile <- parseLibFile provider fileId + case agdaLibFile of + Nothing -> return Nothing + Just agdaLibFile -> do + let (result, _warnings) = runP agdaLibFile + return $ maybeRight result diff --git a/src/Server/Filesystem.hs b/src/Server/Filesystem.hs new file mode 100644 index 0000000..6b55725 --- /dev/null +++ b/src/Server/Filesystem.hs @@ -0,0 +1,243 @@ +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} + +module Server.Filesystem + ( FileId (..), + fileIdToUri, + fileIdToPossiblyInvalidAbsolutePath, + fileIdRelativeTo, + fileIdParent, + fileIdExtension, + IsFileId (..), + MonadFilesystem (..), + Provider, + getFileContents, + getChildren, + LspVirtualFilesystem (..), + OsFilesystem (..), + ProviderWrapper (..), + Layered (..), + ) +where + +import Agda.Syntax.Common.Pretty (Pretty, pretty, prettyShow) +import Agda.Utils.Either (maybeRight) +import Agda.Utils.FileName (AbsolutePath, absolute, sameFile) +import Agda.Utils.IO (catchIO) +import Agda.Utils.IO.UTF8 (ReadException, readTextFile) +import Agda.Utils.List (nubM) +import Agda.Utils.Maybe (fromMaybe, maybe) +import Control.Exception (try, tryJust) +import qualified Control.Exception as E +import Control.Monad (foldM, forM) +import Control.Monad.IO.Class (MonadIO (liftIO)) +import qualified Data.Strict as Strict +import Data.Text (Text) +import qualified Data.Text as Text +import Language.LSP.Protocol.Types (NormalizedUri) +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Types.Uri.More as LSP +import Language.LSP.Server (MonadLsp) +import qualified Language.LSP.Server as LSP +import qualified Language.LSP.VFS as VFS +import Options (Config) +import Server.VfsIndex (VfsIndex, getEntry, getEntryChildren) +import System.Directory (canonicalizePath, doesDirectoryExist, getDirectoryContents) +import System.FilePath (isAbsolute, takeDirectory, takeExtension, ()) +import System.IO.Error (isPermissionError) +import qualified Text.URI as ParsedUri + +data FileId + = Uri !LSP.NormalizedUri + | LocalFilePath !FilePath + deriving (Eq) + +instance Pretty FileId where + pretty (Uri uri) = pretty $ LSP.getNormalizedUri uri + pretty (LocalFilePath path) = pretty path + +instance Show FileId where + show = prettyShow + +referToSameFile :: FileId -> FileId -> IO Bool +referToSameFile a b = + case (tryFileIdToFilePath a, tryFileIdToFilePath b) of + (Just a, Just b) -> do + absA <- absolute a + absB <- absolute b + sameFile absA absB + (Just _, Nothing) -> return False + (Nothing, Just _) -> return False + (Nothing, Nothing) -> do + let uriA = fileIdToUri a + let uriB = fileIdToUri b + return $ uriA == uriB + +fileIdToUri :: FileId -> LSP.NormalizedUri +fileIdToUri = \case + Uri uri -> uri + LocalFilePath filePath -> LSP.toNormalizedUri $ LSP.filePathToUri filePath + +fileIdToParsedUri :: FileId -> Maybe ParsedUri.URI +fileIdToParsedUri = ParsedUri.mkURI . LSP.getNormalizedUri . fileIdToUri + +tryFileIdToFilePath :: FileId -> Maybe FilePath +tryFileIdToFilePath = \case + Uri uri -> LSP.uriToFilePath $ LSP.fromNormalizedUri uri + LocalFilePath filePath -> Just filePath + +fileIdToPossiblyInvalidAbsolutePath :: (MonadIO m) => FileId -> m AbsolutePath +fileIdToPossiblyInvalidAbsolutePath (Uri uri) = LSP.uriToPossiblyInvalidAbsolutePath uri +fileIdToPossiblyInvalidAbsolutePath (LocalFilePath path) = liftIO $ absolute path + +fileIdIsAbsolute :: FileId -> Bool +fileIdIsAbsolute (Uri uri) = + maybe + True + ParsedUri.isPathAbsolute + (ParsedUri.mkURI (LSP.getNormalizedUri uri)) +fileIdIsAbsolute (LocalFilePath path) = isAbsolute path + +-- | Makes the first 'FileId' absolute, treating the second 'FileId' as the base +fileIdRelativeTo :: (MonadIO m) => FileId -> FileId -> m FileId +fileIdRelativeTo fileId _baseFileId | fileIdIsAbsolute fileId = return fileId +fileIdRelativeTo (LocalFilePath path) (LocalFilePath basePath) = fmap LocalFilePath . liftIO $ canonicalizePath $ basePath path +fileIdRelativeTo fileId baseFileId = fromMaybe (pure fileId) $ do + uri <- fileIdToParsedUri fileId + baseUri <- fileIdToParsedUri baseFileId + absUri <- uri `ParsedUri.relativeTo` baseUri + return $ return $ Uri $ LSP.toNormalizedUri $ LSP.Uri $ ParsedUri.render absUri + +fileIdParent :: (MonadIO m) => FileId -> m (Maybe FileId) +fileIdParent (Uri uri) = return $ Uri <$> LSP.uriParent uri +fileIdParent (LocalFilePath path) = do + isDir <- liftIO $ doesDirectoryExist path + if isDir + then liftIO $ dirParent path + else return $ fileParent path + where + -- Taken from Agda's findProjectConfig + dirParent :: FilePath -> IO (Maybe FileId) + dirParent dirPath = do + up <- canonicalizePath $ path ".." + if up == path then return Nothing else return $ Just $ LocalFilePath up + + fileParent :: FilePath -> Maybe FileId + fileParent filePath = Just $ LocalFilePath $ takeDirectory filePath + +fileIdExtension :: FileId -> Text +fileIdExtension (Uri uri) = LSP.uriExtension uri +fileIdExtension (LocalFilePath path) = Text.pack $ takeExtension path + +class IsFileId a where + toFileId :: a -> FileId + +instance IsFileId FileId where + toFileId = id + +instance IsFileId LSP.Uri where + toFileId = Uri . LSP.toNormalizedUri + +instance IsFileId LSP.NormalizedUri where + toFileId = Uri + +instance IsFileId FilePath where + toFileId = LocalFilePath + +data File = File {fileContents :: !Text} + +-- | A monad where a filesystem provider can run. This is a bit of a hack. Its +-- capabilities are really just chosen to support the providers we need. We may +-- as well use 'ServerM', except that we would get circular dependencies when we +-- include a provider in its environment. +class (MonadLsp Config m) => MonadFilesystem m where + askVfsIndex :: m VfsIndex + +class Provider a where + getFileImpl :: (MonadFilesystem m) => a -> FileId -> m (Maybe File) + getChildrenImpl :: (MonadFilesystem m) => a -> FileId -> m [FileId] + +getFile :: (MonadFilesystem m, Provider a, IsFileId f) => a -> f -> m (Maybe File) +getFile provider fileId = getFileImpl provider (toFileId fileId) + +getFileContents :: (MonadFilesystem m, Provider a, IsFileId f) => a -> f -> m (Maybe Text) +getFileContents provider fileId = do + file <- getFile provider fileId + return $ fileContents <$> file + +getChildren :: (MonadFilesystem m, Provider a, IsFileId f) => a -> f -> m [FileId] +getChildren provider fileId = getChildrenImpl provider (toFileId fileId) + +data LspVirtualFilesystem = LspVirtualFilesystem + +instance Provider LspVirtualFilesystem where + getFileImpl _provider fileId = do + let uri = fileIdToUri fileId + vfile <- LSP.getVirtualFile uri + case vfile of + Nothing -> return Nothing + Just vfile -> do + let contents = VFS.virtualFileText vfile + return $ Just $ File contents + + getChildrenImpl _provider parent = do + let uri = fileIdToUri parent + vfsIndex <- askVfsIndex + let children = concat $ getEntryChildren <$> getEntry uri vfsIndex + return $ Uri <$> children + +data OsFilesystem = OsFilesystem + +instance Provider OsFilesystem where + getFileImpl _provider fileId = + case tryFileIdToFilePath fileId of + Nothing -> return Nothing + Just filePath -> do + let result :: IO (Either E.IOException File) + result = try $ do + contents <- Strict.toStrict <$> readTextFile filePath + return $ File contents + liftIO $ maybeRight <$> result + + getChildrenImpl _provider parent = + case tryFileIdToFilePath parent of + Nothing -> return [] + Just parent -> + liftIO + $ (flip catchIO) + (\e -> if isPermissionError e then return [] else E.throwIO e) + $ do + relativeChildren <- liftIO $ getDirectoryContents parent + let absoluteChildren = fmap (\child -> parent child) relativeChildren + return $ LocalFilePath <$> absoluteChildren + +-- TODO: Proper WASM support probably means custom extensions of LSP for +-- filesystem access. When/if these are implemented, they should get a provider +-- here. Include the provider in the default provider instance when running WASM +-- with whatever client the custom extension is for, and hopefully it should all +-- Just Work. + +data ProviderWrapper = forall a. (Provider a) => Wrap a + +instance Provider ProviderWrapper where + getFileImpl (Wrap provider) = getFileImpl provider + + getChildrenImpl (Wrap provider) = getChildrenImpl provider + +data Layered = Layered {layeredProviders :: ![ProviderWrapper]} + +instance Provider Layered where + getFileImpl (Layered providers) fileId = do + let results = flip getFileImpl fileId <$> providers + foldM + ( \file candidate -> case file of + Just _ -> return file + Nothing -> candidate + ) + Nothing + results + + getChildrenImpl (Layered providers) fileId = do + allChildren <- forM providers $ \provider -> getChildrenImpl provider fileId + liftIO $ nubM referToSameFile (concat allChildren) diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs index 05f33d0..1f3b64a 100644 --- a/src/Server/Handler.hs +++ b/src/Server/Handler.hs @@ -81,7 +81,7 @@ import Options ( Config initialiseCommandQueue :: IO CommandQueue initialiseCommandQueue = CommandQueue <$> newTChanIO <*> newTVarIO Nothing -runCommandM :: CommandM a -> ServerM (LspM Config) (Either String a) +runCommandM :: CommandM a -> ServerM (Either String a) runCommandM program = do env <- ask runAgda $ do @@ -100,7 +100,7 @@ runCommandM program = do lift $ evalStateT program commandState inferTypeOfText - :: FilePath -> Text -> ServerM (LspM Config) (Either String String) + :: FilePath -> Text -> ServerM (Either String String) inferTypeOfText filepath text = runCommandM $ do -- load first cmd_load' filepath [] True Imp.TypeCheck $ \_ -> return () @@ -114,7 +114,7 @@ inferTypeOfText filepath text = runCommandM $ do render <$> prettyATop typ -onHover :: LSP.Uri -> LSP.Position -> ServerM (LspM Config) (LSP.Hover LSP.|? LSP.Null) +onHover :: LSP.Uri -> LSP.Position -> ServerM (LSP.Hover LSP.|? LSP.Null) onHover uri pos = do result <- LSP.getVirtualFile (LSP.toNormalizedUri uri) case result of diff --git a/src/Server/Handler/TextDocument/DocumentSymbol.hs b/src/Server/Handler/TextDocument/DocumentSymbol.hs new file mode 100644 index 0000000..d82f581 --- /dev/null +++ b/src/Server/Handler/TextDocument/DocumentSymbol.hs @@ -0,0 +1,77 @@ +module Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler) where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Utils.Maybe (fromMaybe, mapMaybe) +import Agda.Utils.Monad (forMaybeM) +import Control.Monad (forM) +import Control.Monad.Trans (lift) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (ServerM) +import Server.Model.AgdaFile (AgdaFile, agdaFileSymbols, defNameRange, symbolByName, symbolsByParent) +import Server.Model.Handler (requestHandlerWithAgdaFile) +import Server.Model.Monad (MonadAgdaFile (askAgdaFile), useAgdaFile) +import Server.Model.Symbol (SymbolInfo (symbolName), SymbolKind (..), lspSymbolKind, symbolKind, symbolShortName, symbolType) + +documentSymbolHandler :: LSP.Handlers ServerM +documentSymbolHandler = requestHandlerWithAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do + file <- askAgdaFile + let symbols = symbolsByParent file + let topLevelNames = fromMaybe [] $ Map.lookup Nothing symbols + let topLevelSymbols = mapMaybe (symbolByName file) topLevelNames + topLevelDocumentSymbols <- lift $ forMaybeM topLevelSymbols $ symbolToDocumentSymbol file symbols + responder $ Right $ LSP.InR $ LSP.InL topLevelDocumentSymbols + +symbolToDocumentSymbol :: + AgdaFile -> + Map (Maybe A.QName) [A.QName] -> + SymbolInfo -> + ServerM (Maybe LSP.DocumentSymbol) +symbolToDocumentSymbol file symbolsByParent symbol = + if symbolIsDocumentSymbol symbol + then do + let name = symbolName symbol + let range = defNameRange file name + let childrenNames = fromMaybe [] $ Map.lookup (Just name) symbolsByParent + let childrenSymbols = mapMaybe (symbolByName file) childrenNames + childrenDocumentSymbols <- + forMaybeM childrenSymbols $ + symbolToDocumentSymbol file symbolsByParent + return $ + Just $ + LSP.DocumentSymbol + (symbolShortName symbol) + (Text.pack <$> symbolType symbol) + (lspSymbolKind symbol) + Nothing + Nothing + range + range + (Just childrenDocumentSymbols) + else return Nothing + +-- | We only want to report "important" symbols as document symbols. For +-- example, top level module definitions should be document symbols, but local +-- variables should not. +symbolIsDocumentSymbol :: SymbolInfo -> Bool +symbolIsDocumentSymbol symbol = case symbolKind symbol of + Con -> True + CoCon -> True + Field -> True + PatternSyn -> True + GeneralizeVar -> True + Macro -> True + Data -> True + Record -> True + Fun -> True + Axiom -> True + Prim -> True + Module -> True + Param -> False + Local -> False + Unknown -> False diff --git a/src/Server/Handler/TextDocument/FileManagement.hs b/src/Server/Handler/TextDocument/FileManagement.hs new file mode 100644 index 0000000..a060328 --- /dev/null +++ b/src/Server/Handler/TextDocument/FileManagement.hs @@ -0,0 +1,61 @@ +module Server.Handler.TextDocument.FileManagement + ( didOpenHandler, + didCloseHandler, + didSaveHandler, + ) +where + +import Agda.Interaction.FindFile (SourceFile (SourceFile)) +import qualified Agda.Interaction.Imports.More as Imp +import Agda.Interaction.Imports.Virtual (parseVSource, vSrcFromUri) +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.TypeChecking.Monad (MonadTCM (liftTCM)) +import Agda.Utils.Lens ((^.)) +import Control.Monad.Trans (lift) +import Data.Strict (Strict (toLazy)) +import qualified Data.Text as Text +import Indexer (indexFile) +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidAbsolutePath) +import qualified Language.LSP.Server as LSP +import qualified Language.LSP.VFS as VFS +import Monad (ServerM, modifyModel, modifyVfsIndex) +import qualified Server.Model as Model +import Server.Model.Handler (notificationHandlerWithAgdaLib, takeOverNotificationHandlerWithAgdaLib) +import qualified Server.VfsIndex as VFSIndex +import qualified Server.VfsIndex as VfsIndex + +didOpenHandler :: LSP.Handlers ServerM +didOpenHandler = LSP.notificationHandler LSP.SMethod_TextDocumentDidOpen $ \notification -> do + let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri + modifyVfsIndex $ VfsIndex.onOpen uri + takeOverNotificationHandlerWithAgdaLib notification $ \uri notification -> do + vfile <- lift $ LSP.getVirtualFile uri + case vfile of + Nothing -> return () + Just vfile -> do + vSourceFile <- vSrcFromUri uri vfile + src <- parseVSource vSourceFile + lift $ LSP.sendNotification LSP.SMethod_WindowLogMessage $ LSP.LogMessageParams LSP.MessageType_Info $ Text.pack $ prettyShow src + agdaFile <- indexFile src + lift $ modifyModel $ Model.setAgdaFile uri agdaFile + +didCloseHandler :: LSP.Handlers ServerM +didCloseHandler = LSP.notificationHandler LSP.SMethod_TextDocumentDidClose $ \notification -> do + let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri + modifyVfsIndex $ VFSIndex.onClose uri + modifyModel $ Model.deleteAgdaFile $ LSP.toNormalizedUri uri + +didSaveHandler :: LSP.Handlers ServerM +didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \uri notification -> do + vfile <- lift $ LSP.getVirtualFile uri + case vfile of + Nothing -> return () + Just vfile -> do + vSourceFile <- vSrcFromUri uri vfile + src <- parseVSource vSourceFile + lift $ LSP.sendNotification LSP.SMethod_WindowLogMessage $ LSP.LogMessageParams LSP.MessageType_Info $ Text.pack $ prettyShow src + agdaFile <- indexFile src + lift $ modifyModel $ Model.setAgdaFile uri agdaFile diff --git a/src/Server/Model.hs b/src/Server/Model.hs new file mode 100644 index 0000000..bf8fab6 --- /dev/null +++ b/src/Server/Model.hs @@ -0,0 +1,50 @@ +module Server.Model + ( Model (Model), + empty, + getKnownAgdaLib, + withAgdaLib, + getAgdaFile, + setAgdaFile, + deleteAgdaFile, + ) +where + +import Agda.Utils.Lens (Lens', over) +import Control.Monad.IO.Class (MonadIO) +import Data.Foldable (find) +import Data.Functor ((<&>)) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.AgdaFile (AgdaFile) +import Server.Model.AgdaLib (AgdaLib, initAgdaLib, isAgdaLibForUri) + +data Model = Model + { _modelAgdaLibs :: !([AgdaLib]), + _modelAgdaFiles :: !(Map LSP.NormalizedUri AgdaFile) + } + +empty :: Model +empty = Model [] Map.empty + +agdaLibs :: Lens' Model [AgdaLib] +agdaLibs f a = f (_modelAgdaLibs a) <&> \x -> a {_modelAgdaLibs = x} + +agdaFiles :: Lens' Model (Map LSP.NormalizedUri AgdaFile) +agdaFiles f a = f (_modelAgdaFiles a) <&> \x -> a {_modelAgdaFiles = x} + +getKnownAgdaLib :: LSP.NormalizedUri -> Model -> Maybe AgdaLib +getKnownAgdaLib uri = find (`isAgdaLibForUri` uri) . _modelAgdaLibs + +-- | Add an 'AgdaLib' to the model +withAgdaLib :: AgdaLib -> Model -> Model +withAgdaLib lib model = model {_modelAgdaLibs = lib : _modelAgdaLibs model} + +getAgdaFile :: LSP.NormalizedUri -> Model -> Maybe AgdaFile +getAgdaFile uri = Map.lookup uri . _modelAgdaFiles + +setAgdaFile :: LSP.NormalizedUri -> AgdaFile -> Model -> Model +setAgdaFile uri agdaFile = over agdaFiles $ Map.insert uri agdaFile + +deleteAgdaFile :: LSP.NormalizedUri -> Model -> Model +deleteAgdaFile uri = over agdaFiles $ Map.delete uri diff --git a/src/Server/Model/AgdaFile.hs b/src/Server/Model/AgdaFile.hs new file mode 100644 index 0000000..2056c8a --- /dev/null +++ b/src/Server/Model/AgdaFile.hs @@ -0,0 +1,99 @@ +module Server.Model.AgdaFile + ( AgdaFile, + emptyAgdaFile, + agdaFileSymbols, + agdaFileRefs, + insertSymbolInfo, + insertRef, + mergeSymbols, + symbolByName, + symbolsByParent, + defNameRange, + ) +where + +import Agda.Position (toLspRange) +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (Pretty, pretty, prettyAssign, prettyMap, prettyShow, text, vcat) +import Agda.Syntax.Position (getRange) +import Agda.Utils.Lens (Lens', over, (<&>), (^.)) +import Data.Foldable (find) +import Data.Function ((&)) +import Data.Map (Map) +import qualified Data.Map as Map +import Data.Monoid (Endo (Endo, appEndo)) +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.Symbol (Ref, SymbolInfo, refIsDef, refRange, symbolParent) + +data AgdaFile = AgdaFile + { _agdaFileSymbols :: !(Map A.QName SymbolInfo), + _agdaFileRefs :: !(Map A.QName [Ref]) + } + deriving (Eq) + +instance Pretty AgdaFile where + pretty agdaFile = + vcat + [ prettyAssign (text "symbols", prettyMap $ Map.toList $ agdaFile ^. agdaFileSymbols), + prettyAssign (text "refs", prettyMap $ Map.toList $ agdaFile ^. agdaFileRefs) + ] + +instance Show AgdaFile where + show = prettyShow + +emptyAgdaFile :: AgdaFile +emptyAgdaFile = AgdaFile Map.empty Map.empty + +agdaFileSymbols :: Lens' AgdaFile (Map A.QName SymbolInfo) +agdaFileSymbols f a = f (_agdaFileSymbols a) <&> \x -> a {_agdaFileSymbols = x} + +agdaFileRefs :: Lens' AgdaFile (Map A.QName [Ref]) +agdaFileRefs f a = f (_agdaFileRefs a) <&> \x -> a {_agdaFileRefs = x} + +insertSymbolInfo :: + A.QName -> + SymbolInfo -> + AgdaFile -> + AgdaFile +insertSymbolInfo name symbolInfo = + over agdaFileSymbols $ Map.insertWith (<>) name symbolInfo + +insertRef :: A.AmbiguousQName -> Ref -> AgdaFile -> AgdaFile +insertRef ambiguousName ref = + over agdaFileRefs $ + appEndo $ + foldMap (\name -> Endo $ Map.insertWith (<>) name [ref]) (A.unAmbQ ambiguousName) + +mergeSymbols :: A.QName -> A.QName -> AgdaFile -> AgdaFile +mergeSymbols old new file = + file + & over + agdaFileSymbols + ( \symbols -> + let (oldSymbolInfo, symbols') = + Map.updateLookupWithKey (\_ _ -> Nothing) old symbols + in Map.alter (<> oldSymbolInfo) new symbols' + ) + & over + agdaFileRefs + ( \refs -> + let (oldRefs, refs') = + Map.updateLookupWithKey (\_ _ -> Nothing) old refs + in Map.alter (<> oldRefs) new refs' + ) + +symbolByName :: AgdaFile -> A.QName -> Maybe SymbolInfo +symbolByName agdaFile symbolName = Map.lookup symbolName $ agdaFile ^. agdaFileSymbols + +symbolsByParent :: AgdaFile -> Map (Maybe A.QName) [A.QName] +symbolsByParent agdaFile = + let symbols = Map.toList $ agdaFile ^. agdaFileSymbols + in Map.fromListWith (++) $ (\(symbolName, symbol) -> (symbolParent symbol, [symbolName])) <$> symbols + +refsByName :: AgdaFile -> A.QName -> [Ref] +refsByName agdaFile name = Map.findWithDefault [] name $ agdaFile ^. agdaFileRefs + +defNameRange :: AgdaFile -> A.QName -> LSP.Range +defNameRange agdaFile name = + let defs = find refIsDef $ refsByName agdaFile name + in maybe (toLspRange $ getRange name) refRange defs diff --git a/src/Server/Model/AgdaLib.hs b/src/Server/Model/AgdaLib.hs new file mode 100644 index 0000000..28d9a9c --- /dev/null +++ b/src/Server/Model/AgdaLib.hs @@ -0,0 +1,134 @@ +{-# LANGUAGE CPP #-} + +module Server.Model.AgdaLib + ( AgdaLibOrigin (..), + AgdaLib (AgdaLib), + initAgdaLib, + agdaLibName, + agdaLibIncludes, + agdaLibDependencies, + agdaLibTcStateRef, + agdaLibTcEnv, + agdaLibOrigin, + isAgdaLibForUri, + agdaLibFromFile, + agdaLibToFile, + ) +where + +import Agda.Interaction.Library ( + AgdaLibFile (_libIncludes, AgdaLibFile), + findProjectRoot, + LibName, + OptionsPragma (OptionsPragma), + ) +import Agda.Interaction.Library.More (tryRunLibM) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.IORef (IORef, newIORef) +import Agda.Utils.Lens (Lens', (<&>), (^.), set) +import Agda.Utils.Maybe (listToMaybe, catMaybes) +import Control.Monad.IO.Class (MonadIO (liftIO)) +import Data.Map (Map) +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Types.Uri.More as LSP +import Server.Model.AgdaFile (AgdaFile) +import Agda.Interaction.Library.Base (libFile, LibName (..), libName, libIncludes, libPragmas) +import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidFilePath) +import Agda.Utils.Null (empty) +import Agda.Syntax.Common.Pretty (Pretty, pretty, vcat, prettyAssign, text, pshow, doubleQuotes, (<+>)) +import qualified Text.URI as ParsedUri +import qualified Data.Text as Text +import qualified Server.Filesystem as FS +import Control.Monad (forM) + +data AgdaLibOrigin = FromFile !FS.FileId | Defaulted + deriving (Show, Eq) + +data AgdaLib = AgdaLib + { _agdaLibName :: !LibName, + _agdaLibIncludes :: ![FS.FileId], + _agdaLibOptionsPragma :: !OptionsPragma, + _agdaLibDependencies :: ![LibName], + _agdaLibTcStateRef :: !(IORef TCM.TCState), + _agdaLibTcEnv :: !TCM.TCEnv, + _agdaLibOrigin :: !AgdaLibOrigin + } + +instance Pretty AgdaLib where + pretty agdaLib = + text "AgdaLib" + <+> doubleQuotes (pretty $ agdaLib ^. agdaLibName) + <+> pshow (agdaLib ^. agdaLibOrigin) + <+> text "includes:" + <+> pretty (agdaLib ^. agdaLibIncludes) + +initAgdaLibWithOrigin :: (MonadIO m) => AgdaLibOrigin -> m AgdaLib +initAgdaLibWithOrigin origin = do +#if MIN_VERSION_Agda(2,8,0) + let libName = LibName "" [] + tcState <- liftIO TCM.initStateIO +#else + let libName = "" + let tcState = TCM.initState +#endif + let persistentState = TCM.stPersistentState tcState + let tcState' = tcState { TCM.stPersistentState = persistentState { TCM.stInteractionOutputCallback = \_ -> return () } } + tcStateRef <- liftIO $ newIORef tcState' + let tcEnv = TCM.initEnv + let optionsPragma = OptionsPragma [] empty + return $ AgdaLib libName [] optionsPragma [] tcStateRef tcEnv origin + +initAgdaLib :: (MonadIO m) => m AgdaLib +initAgdaLib = initAgdaLibWithOrigin Defaulted + +agdaLibName :: Lens' AgdaLib LibName +agdaLibName f a = f (_agdaLibName a) <&> \x -> a {_agdaLibName = x} + +agdaLibIncludes :: Lens' AgdaLib [FS.FileId] +agdaLibIncludes f a = f (_agdaLibIncludes a) <&> \x -> a {_agdaLibIncludes = x} + +agdaLibOptionsPragma :: Lens' AgdaLib OptionsPragma +agdaLibOptionsPragma f a = f (_agdaLibOptionsPragma a) <&> \x -> a {_agdaLibOptionsPragma = x} + +agdaLibDependencies :: Lens' AgdaLib [LibName] +agdaLibDependencies f a = f (_agdaLibDependencies a) <&> \x -> a {_agdaLibDependencies = x} + +agdaLibTcStateRef :: Lens' AgdaLib (IORef TCM.TCState) +agdaLibTcStateRef f a = f (_agdaLibTcStateRef a) <&> \x -> a {_agdaLibTcStateRef = x} + +agdaLibTcEnv :: Lens' AgdaLib TCM.TCEnv +agdaLibTcEnv f a = f (_agdaLibTcEnv a) <&> \x -> a {_agdaLibTcEnv = x} + +agdaLibOrigin :: Lens' AgdaLib AgdaLibOrigin +agdaLibOrigin f a = f (_agdaLibOrigin a) <&> \x -> a {_agdaLibOrigin = x} + +isAgdaLibForUri :: AgdaLib -> LSP.NormalizedUri -> Bool +isAgdaLibForUri agdaLib uri = any (\include -> FS.fileIdToUri include `LSP.isUriAncestorOf` uri) (agdaLib ^. agdaLibIncludes) + +-- | Given an 'AgdaLibFile' and the URI of that file, create the +-- corresponding 'AgdaLib' +agdaLibFromFile :: (MonadIO m, FS.IsFileId f) => AgdaLibFile -> f -> m AgdaLib +agdaLibFromFile agdaLibFile agdaLibIsFileId = do + let agdaLibFileId = FS.toFileId agdaLibIsFileId + agdaLibParent <- FS.fileIdParent agdaLibFileId + let includeToAbsolute = case agdaLibParent of + Nothing -> return . FS.LocalFilePath + Just parent -> \include -> FS.LocalFilePath include `FS.fileIdRelativeTo` parent + includes <- forM (agdaLibFile ^. libIncludes) includeToAbsolute + initAgdaLibWithOrigin (FromFile agdaLibFileId) + <&> set agdaLibName (agdaLibFile ^. libName) + <&> set agdaLibIncludes includes + <&> set agdaLibOptionsPragma (agdaLibFile ^. libPragmas) + +-- | If the given `AgdaLib` came from a file, turn it back into one. Since +-- `AgdaLibFile`s are relative to an Agda file on the filesystem, the first +-- parameter is for the URI for the Agda file +agdaLibToFile :: LSP.NormalizedUri -> AgdaLib -> Maybe AgdaLibFile +agdaLibToFile relativeToUri agdaLib = case agdaLib ^. agdaLibOrigin of + Defaulted -> Nothing + FromFile fileId -> + let includePaths = uriToPossiblyInvalidFilePath . FS.fileIdToUri <$> agdaLib ^. agdaLibIncludes + uri = FS.fileIdToUri fileId + above = LSP.uriHeightAbove uri relativeToUri + filePath = LSP.uriToPossiblyInvalidFilePath uri + in Just $ AgdaLibFile (agdaLib ^. agdaLibName) filePath above includePaths [] (agdaLib ^. agdaLibOptionsPragma) diff --git a/src/Server/Model/Handler.hs b/src/Server/Model/Handler.hs new file mode 100644 index 0000000..3b687e4 --- /dev/null +++ b/src/Server/Model/Handler.hs @@ -0,0 +1,111 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} + +module Server.Model.Handler + ( notificationHandlerWithAgdaLib, + takeOverNotificationHandlerWithAgdaLib, + requestHandlerWithAgdaFile, + ) +where + +import Agda.Syntax.Common (WithHiding (whHiding)) +import Agda.Syntax.Common.Pretty (prettyShow) +import qualified Agda.TypeChecking.Monad as TCM +import qualified Agda.TypeChecking.Pretty as TCM +import Agda.Utils.Either (fromRightM) +import Agda.Utils.Lens ((^.)) +import Control.Monad.Trans (MonadTrans, lift) +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Message as Lsp +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (ServerM, askModel, catchTCError) +import Server.AgdaLibResolver (findAgdaLib) +import qualified Server.Model as Model +import Server.Model.Monad (WithAgdaFileM, WithAgdaLibM, runWithAgdaFileT, runWithAgdaLibT) +import qualified Server.Model.Monad as LSP +#if MIN_VERSION_Agda(2,7,0) +#else +import Agda.TypeChecking.Errors () +#endif + +tryTC :: ServerM a -> ServerM (Either TCM.TCErr a) +tryTC handler = (Right <$> handler) `catchTCError` (return . Left) + +-------------------------------------------------------------------------------- + +type NotificationHandlerWithAgdaLib + (m :: LSP.Method LSP.ClientToServer LSP.Notification) = + LSP.NormalizedUri -> LSP.TNotificationMessage m -> WithAgdaLibM () + +notificationHandlerWithAgdaLib :: + (LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) => + LSP.SMethod m -> + NotificationHandlerWithAgdaLib m -> + LSP.Handlers ServerM +notificationHandlerWithAgdaLib m handlerWithAgdaLib = + LSP.notificationHandler m $ flip takeOverNotificationHandlerWithAgdaLib handlerWithAgdaLib + +takeOverNotificationHandlerWithAgdaLib :: + (LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) => + LSP.TNotificationMessage m -> + NotificationHandlerWithAgdaLib m -> + ServerM () +takeOverNotificationHandlerWithAgdaLib notification handlerWithAgdaLib = do + let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri + normUri = LSP.toNormalizedUri uri + agdaLib <- findAgdaLib normUri + lift $ LSP.sendNotification LSP.SMethod_WindowLogMessage $ LSP.LogMessageParams LSP.MessageType_Info $ Text.pack $ prettyShow agdaLib + + let notificationHandler = runWithAgdaLibT agdaLib . handlerWithAgdaLib normUri + let handler = tryTC $ notificationHandler notification + + let onErr = \err -> runWithAgdaLibT agdaLib $ do + message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err) + lift $ LSP.sendNotification LSP.SMethod_WindowShowMessage $ LSP.ShowMessageParams LSP.MessageType_Error message + lift $ LSP.sendNotification LSP.SMethod_WindowLogMessage $ LSP.LogMessageParams LSP.MessageType_Error message + + fromRightM onErr handler + +-------------------------------------------------------------------------------- + +type RequestCallbackWithAgdaFile + (m :: LSP.Method LSP.ClientToServer LSP.Request) = + Either (LSP.TResponseError m) (LSP.MessageResult m) -> WithAgdaFileM () + +type RequestHandlerWithAgdaFile + (m :: LSP.Method LSP.ClientToServer LSP.Request) = + LSP.TRequestMessage m -> + RequestCallbackWithAgdaFile m -> + WithAgdaFileM () + +requestHandlerWithAgdaFile :: + (LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) => + LSP.SMethod m -> + RequestHandlerWithAgdaFile m -> + LSP.Handlers ServerM +requestHandlerWithAgdaFile m handlerWithAgdaFile = LSP.requestHandler m $ \req responder -> do + let uri = req ^. LSP.params . LSP.textDocument . LSP.uri + normUri = LSP.toNormalizedUri uri + + model <- askModel + case Model.getAgdaFile normUri model of + Nothing -> do + let message = "Request for unknown Agda file at URI: " <> LSP.getUri uri + responder $ Left $ LSP.TResponseError (LSP.InR LSP.ErrorCodes_InvalidParams) message Nothing + Just agdaFile -> do + agdaLib <- findAgdaLib normUri + let responderWithAgdaFile = lift . responder + let handler = tryTC $ runWithAgdaFileT agdaLib agdaFile $ handlerWithAgdaFile req responderWithAgdaFile + + let onErr = \err -> runWithAgdaFileT agdaLib agdaFile $ do + message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err) + lift $ responder $ Left $ LSP.TResponseError (LSP.InL LSP.LSPErrorCodes_RequestFailed) message Nothing + + fromRightM onErr handler diff --git a/src/Server/Model/Monad.hs b/src/Server/Model/Monad.hs new file mode 100644 index 0000000..e5459c8 --- /dev/null +++ b/src/Server/Model/Monad.hs @@ -0,0 +1,325 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeSynonymInstances #-} + +module Server.Model.Monad + ( MonadAgdaLib (..), + useAgdaLib, + MonadAgdaFile (..), + useAgdaFile, + WithAgdaLibT, + runWithAgdaLibT, + WithAgdaLibM, + runWithAgdaLib, + WithAgdaFileT, + runWithAgdaFileT, + WithAgdaFileM, + ) +where + +import Agda.Interaction.Options (CommandLineOptions (optPragmaOptions), PragmaOptions) +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Syntax.Position (getRange) +import Agda.TypeChecking.Monad (HasOptions (..), MonadTCEnv (..), MonadTCM (..), MonadTCState (..), MonadTrace, PersistentTCState (stPersistentOptions), ReadTCState (..), TCEnv (..), TCM, TCMT (..), TCState (stPersistentState), catchError_, modifyTCLens, setTCLens, stPragmaOptions, useTC, viewTC) +import qualified Agda.TypeChecking.Monad as TCM +import qualified Agda.TypeChecking.Pretty as TCM +import Agda.Utils.IORef (modifyIORef', readIORef, writeIORef) +import Agda.Utils.Lens (Lens', locally, over, use, view, (<&>), (^.)) +import Agda.Utils.Monad (and2M, bracket_, ifNotM, unless) +import Agda.Utils.Null (null) +import Control.Monad.IO.Class (MonadIO (liftIO)) +import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), ask, asks) +import Control.Monad.Trans (MonadTrans, lift) +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Types.Uri.More as LSP +import Language.LSP.Server (LspM) +import qualified Language.LSP.Server as LSP +import Monad (ServerM, ServerT, askModel, catchTCError) +import Options (Config) +import qualified Server.Model as Model +import Server.Model.AgdaFile (AgdaFile) +import Server.Model.AgdaLib (AgdaLib, agdaLibTcEnv, agdaLibTcStateRef) +import Prelude hiding (null) +#if MIN_VERSION_Agda(2,8,0) +import Agda.Utils.FileId (File, getIdFile) +#endif +#if MIN_VERSION_Agda(2,7,0) +import Agda.Interaction.Response (Response_boot(Resp_HighlightingInfo)) +import Server.AgdaLibResolver (findAgdaLib) +#else +import Agda.Interaction.Response (Response(Resp_HighlightingInfo)) +#endif + +-------------------------------------------------------------------------------- + +class (MonadTCM m, ReadTCState m) => MonadAgdaLib m where + askAgdaLib :: m AgdaLib + localAgdaLib :: (AgdaLib -> AgdaLib) -> m a -> m a + +useAgdaLib :: (MonadAgdaLib m) => Lens' AgdaLib a -> m a +useAgdaLib lens = do + agdaLib <- askAgdaLib + return $ agdaLib ^. lens + +class (MonadAgdaLib m) => MonadAgdaFile m where + askAgdaFile :: m AgdaFile + localAgdaFile :: (AgdaFile -> AgdaFile) -> m a -> m a + +useAgdaFile :: (MonadAgdaFile m) => Lens' AgdaFile a -> m a +useAgdaFile lens = do + agdaFile <- askAgdaFile + return $ agdaFile ^. lens + +-------------------------------------------------------------------------------- + +defaultAskTC :: (MonadAgdaLib m) => m TCEnv +defaultAskTC = useAgdaLib agdaLibTcEnv + +defaultLocalTC :: (MonadAgdaLib m) => (TCEnv -> TCEnv) -> m a -> m a +defaultLocalTC f = localAgdaLib (over agdaLibTcEnv f) + +defaultGetTC :: (MonadAgdaLib m) => m TCState +defaultGetTC = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + liftIO $ readIORef tcStateRef + +defaultPutTC :: (MonadAgdaLib m) => TCState -> m () +defaultPutTC tcState = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + liftIO $ writeIORef tcStateRef tcState + +defaultModifyTC :: (MonadAgdaLib m) => (TCState -> TCState) -> m () +defaultModifyTC f = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + liftIO $ modifyIORef' tcStateRef f + +-- Taken from TCMT implementation +defaultLocallyTCState :: (MonadAgdaLib m) => Lens' TCState a -> (a -> a) -> m b -> m b +defaultLocallyTCState lens f = bracket_ (useTC lens <* modifyTCLens lens f) (setTCLens lens) + +-- Taken from TCMT implementation +defaultPragmaOptionsImpl :: (MonadAgdaLib m) => m PragmaOptions +defaultPragmaOptionsImpl = useTC stPragmaOptions + +-- Taken from TCMT implementation +defaultCommandLineOptionsImpl :: (MonadAgdaLib m) => m CommandLineOptions +defaultCommandLineOptionsImpl = do + p <- useTC stPragmaOptions + cl <- stPersistentOptions . stPersistentState <$> getTC + return $ cl {optPragmaOptions = p} + +defaultLiftTCM :: (MonadAgdaLib m) => TCM a -> m a +defaultLiftTCM (TCM f) = do + tcStateRef <- useAgdaLib agdaLibTcStateRef + tcEnv <- useAgdaLib agdaLibTcEnv + liftIO $ f tcStateRef tcEnv + +-- Taken from TCM implementation +defaultTraceClosureCall :: (MonadAgdaLib m, MonadTrace m) => TCM.Closure TCM.Call -> m a -> m a +defaultTraceClosureCall cl m = do + -- Compute update to 'Range' and 'Call' components of 'TCEnv'. + let withCall = + localTC $ + foldr (.) id $ + concat $ + [ [\e -> e {envCall = Just cl} | TCM.interestingCall call], + [ \e -> e {envHighlightingRange = callRange} + | callHasRange && highlightCall + || isNoHighlighting + ], + [\e -> e {envRange = callRange} | callHasRange] + ] + + -- For interactive highlighting, also wrap computation @m@ in 'highlightAsTypeChecked': + ifNotM + (pure highlightCall `and2M` do (TCM.Interactive ==) . envHighlightingLevel <$> askTC) + {-then-} (withCall m) + {-else-} $ do + oldRange <- envHighlightingRange <$> askTC + TCM.highlightAsTypeChecked oldRange callRange $ + withCall m + where + call = TCM.clValue cl + callRange = getRange call + callHasRange = not $ null callRange + + -- Should the given call trigger interactive highlighting? + highlightCall = case call of + TCM.CheckClause {} -> True + TCM.CheckLHS {} -> True + TCM.CheckPattern {} -> True + TCM.CheckPatternLinearityType {} -> False + TCM.CheckPatternLinearityValue {} -> False + TCM.CheckLetBinding {} -> True + TCM.InferExpr {} -> True + TCM.CheckExprCall {} -> True + TCM.CheckDotPattern {} -> True + TCM.IsTypeCall {} -> True + TCM.IsType_ {} -> True + TCM.InferVar {} -> True + TCM.InferDef {} -> True + TCM.CheckArguments {} -> True + TCM.CheckMetaSolution {} -> False + TCM.CheckTargetType {} -> False + TCM.CheckDataDef {} -> True + TCM.CheckRecDef {} -> True + TCM.CheckConstructor {} -> True + TCM.CheckConArgFitsIn {} -> False + TCM.CheckFunDefCall _ _ _ h -> h + TCM.CheckPragma {} -> True + TCM.CheckPrimitive {} -> True + TCM.CheckIsEmpty {} -> True + TCM.CheckConfluence {} -> False + TCM.CheckIApplyConfluence {} -> False + TCM.CheckModuleParameters {} -> False + TCM.CheckWithFunctionType {} -> True + TCM.CheckSectionApplication {} -> True + TCM.CheckNamedWhere {} -> False + TCM.ScopeCheckExpr {} -> False + TCM.ScopeCheckDeclaration {} -> False + TCM.ScopeCheckLHS {} -> False + TCM.NoHighlighting {} -> True + TCM.CheckProjection {} -> False + TCM.SetRange {} -> False + TCM.ModuleContents {} -> False + + isNoHighlighting = case call of + TCM.NoHighlighting {} -> True + _ -> False + + printHighlightingInfo remove info = do + modToSrc <- useTC TCM.stModuleToSource + method <- viewTC TCM.eHighlightingMethod + -- reportSDoc "highlighting" 50 $ + -- pure $ + -- vcat + -- [ "Printing highlighting info:", + -- nest 2 $ (text . show) info, + -- "File modules:", + -- nest 2 $ pretty modToSrc + -- ] + unless (null info) $ do + TCM.appInteractionOutputCallback $ + Resp_HighlightingInfo info remove method modToSrc + +#if MIN_VERSION_Agda(2,8,0) +-- Taken from TCMT implementation +defaultFileFromId :: (MonadAgdaLib m) => TCM.FileId -> m File +defaultFileFromId fi = useTC TCM.stFileDict <&> (`getIdFile` fi) + +-- Taken from TCMT implementation +defaultIdFromFile :: (MonadAgdaLib m) => File -> m TCM.FileId +defaultIdFromFile = TCM.stateTCLens TCM.stFileDict . TCM.registerFileIdWithBuiltin +#endif + +-------------------------------------------------------------------------------- + +newtype WithAgdaLibT m a = WithAgdaLibT {unWithAgdaLibT :: ReaderT AgdaLib m a} + deriving (Functor, Applicative, Monad, MonadIO, MonadTrans) + +runWithAgdaLibT :: AgdaLib -> WithAgdaLibT m a -> m a +runWithAgdaLibT agdaLib = flip runReaderT agdaLib . unWithAgdaLibT + +type WithAgdaLibM = WithAgdaLibT ServerM + +runWithAgdaLib :: LSP.Uri -> WithAgdaLibM a -> ServerM a +runWithAgdaLib uri x = do + agdaLib <- findAgdaLib uri + runWithAgdaLibT agdaLib x + +instance (MonadIO m) => MonadAgdaLib (WithAgdaLibT m) where + askAgdaLib = WithAgdaLibT ask + localAgdaLib f = WithAgdaLibT . local f . unWithAgdaLibT + +instance (MonadIO m) => MonadTCEnv (WithAgdaLibT m) where + askTC = defaultAskTC + localTC = defaultLocalTC + +instance (MonadIO m) => MonadTCState (WithAgdaLibT m) where + getTC = defaultGetTC + putTC = defaultPutTC + modifyTC = defaultModifyTC + +instance (MonadIO m) => ReadTCState (WithAgdaLibT m) where + getTCState = defaultGetTC + locallyTCState = defaultLocallyTCState + +instance (MonadIO m) => HasOptions (WithAgdaLibT m) where + pragmaOptions = defaultPragmaOptionsImpl + commandLineOptions = defaultCommandLineOptionsImpl + +-- TODO: how should this really be implemented? +instance (MonadIO m) => MonadTrace (WithAgdaLibT m) where + traceClosureCall = defaultTraceClosureCall + printHighlightingInfo _ _ = return () + +instance (MonadIO m) => MonadTCM (WithAgdaLibT m) where + liftTCM = defaultLiftTCM + +#if MIN_VERSION_Agda(2,8,0) +instance (MonadIO m) => TCM.MonadFileId (WithAgdaLibT m) where + fileFromId = defaultFileFromId + idFromFile = defaultIdFromFile +#endif + +-------------------------------------------------------------------------------- + +data WithAgdaFileEnv = WithAgdaFileEnv + { _withAgdaFileEnvAgdaLib :: !AgdaLib, + _withAgdaFileEnvAgdaFile :: !AgdaFile + } + +withAgdaFileEnvAgdaLib :: Lens' WithAgdaFileEnv AgdaLib +withAgdaFileEnvAgdaLib f a = f (_withAgdaFileEnvAgdaLib a) <&> \x -> a {_withAgdaFileEnvAgdaLib = x} + +withAgdaFileEnvAgdaFile :: Lens' WithAgdaFileEnv AgdaFile +withAgdaFileEnvAgdaFile f a = f (_withAgdaFileEnvAgdaFile a) <&> \x -> a {_withAgdaFileEnvAgdaFile = x} + +newtype WithAgdaFileT m a = WithAgdaFileT + {unWithAgdaFileT :: ReaderT WithAgdaFileEnv m a} + deriving (Functor, Applicative, Monad, MonadIO, MonadTrans) + +runWithAgdaFileT :: AgdaLib -> AgdaFile -> WithAgdaFileT m a -> m a +runWithAgdaFileT agdaLib agdaFile = + let env = WithAgdaFileEnv agdaLib agdaFile + in flip runReaderT env . unWithAgdaFileT + +type WithAgdaFileM = WithAgdaFileT ServerM + +instance (MonadIO m) => MonadAgdaLib (WithAgdaFileT m) where + askAgdaLib = WithAgdaFileT $ view withAgdaFileEnvAgdaLib + localAgdaLib f = WithAgdaFileT . locally withAgdaFileEnvAgdaLib f . unWithAgdaFileT + +instance (MonadIO m) => MonadAgdaFile (WithAgdaFileT m) where + askAgdaFile = WithAgdaFileT $ view withAgdaFileEnvAgdaFile + localAgdaFile f = WithAgdaFileT . locally withAgdaFileEnvAgdaFile f . unWithAgdaFileT + +instance (MonadIO m) => MonadTCEnv (WithAgdaFileT m) where + askTC = defaultAskTC + localTC = defaultLocalTC + +instance (MonadIO m) => MonadTCState (WithAgdaFileT m) where + getTC = defaultGetTC + putTC = defaultPutTC + modifyTC = defaultModifyTC + +instance (MonadIO m) => ReadTCState (WithAgdaFileT m) where + getTCState = defaultGetTC + locallyTCState = defaultLocallyTCState + +instance (MonadIO m) => HasOptions (WithAgdaFileT m) where + pragmaOptions = defaultPragmaOptionsImpl + commandLineOptions = defaultCommandLineOptionsImpl + +instance (MonadIO m) => MonadTCM (WithAgdaFileT m) where + liftTCM = defaultLiftTCM diff --git a/src/Server/Model/Symbol.hs b/src/Server/Model/Symbol.hs new file mode 100644 index 0000000..696674a --- /dev/null +++ b/src/Server/Model/Symbol.hs @@ -0,0 +1,133 @@ +module Server.Model.Symbol + ( SymbolKind (..), + SymbolInfo (..), + symbolShortName, + lspSymbolKind, + RefKind (..), + Ref (..), + refIsDef, + ) +where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (Doc, Pretty, comma, parensNonEmpty, pretty, prettyShow, pshow, text, (<+>)) +import Control.Applicative ((<|>)) +import Data.Text (Text) +import qualified Data.Text as Text +import qualified Language.LSP.Protocol.Types as LSP +import Language.LSP.Protocol.Types.More () + +data SymbolKind + = Con + | CoCon + | Field + | PatternSyn + | GeneralizeVar + | Macro + | Data + | Record + | Fun + | Axiom + | Prim + | Module + | Param + | Local + | Unknown + deriving (Show, Eq) + +instance Pretty SymbolKind where + pretty = pshow + +instance Semigroup SymbolKind where + Unknown <> k = k + k <> _k = k + +toLspSymbolKind :: SymbolKind -> LSP.SymbolKind +toLspSymbolKind = \case + Con -> LSP.SymbolKind_Constructor + CoCon -> LSP.SymbolKind_Constructor + Field -> LSP.SymbolKind_Field + PatternSyn -> LSP.SymbolKind_Function + GeneralizeVar -> LSP.SymbolKind_Variable + Macro -> LSP.SymbolKind_Function + Data -> LSP.SymbolKind_Enum + Record -> LSP.SymbolKind_Struct + Fun -> LSP.SymbolKind_Function + Axiom -> LSP.SymbolKind_Constant + Prim -> LSP.SymbolKind_Constant + Module -> LSP.SymbolKind_Module + Param -> LSP.SymbolKind_Variable + Local -> LSP.SymbolKind_Variable + Unknown -> LSP.SymbolKind_Variable + +data SymbolInfo = SymbolInfo + { symbolName :: !A.QName, + symbolKind :: !SymbolKind, + symbolType :: !(Maybe String), + symbolParent :: !(Maybe A.QName) + } + deriving (Eq) + +instance Pretty SymbolInfo where + pretty symbolInfo = + pretty (symbolKind symbolInfo) + <+> parensNonEmpty (pretty $ symbolType symbolInfo) + +instance Semigroup SymbolInfo where + new <> old = + SymbolInfo + (symbolName new) + (symbolKind old <> symbolKind new) + (symbolType old <|> symbolType new) + (symbolParent old <|> symbolParent new) + +symbolShortName :: SymbolInfo -> Text +symbolShortName = Text.pack . prettyShow . A.qnameName . symbolName + +lspSymbolKind :: SymbolInfo -> LSP.SymbolKind +lspSymbolKind = toLspSymbolKind . symbolKind + +data RefKind + = -- | The symbol is being declared. There should be at most one declaration + -- for any given symbol (in correct Agda code). Roughly speaking, this is + -- the "single most important defining reference" + -- + -- For example, a function's name in its signature + Decl + | -- | The symbol is being defined, but is not being declared in the sense + -- that @Decl@ would apply. Typically, this means the definition may be + -- split into several parts, and this is one of the "less important" parts + -- + -- For example, a function's name in the LHS of a clause in its definition + Def + | -- | The symbol is (expected to be) already defined and is being used + -- + -- For example, a function's name in function application + Usage + | -- | The symbol is being imported here + Import + deriving (Show, Eq) + +instance Pretty RefKind where + pretty = pshow + +data Ref = Ref + { refKind :: !RefKind, + refRange :: !LSP.Range, + refIsAmbiguous :: !Bool + } + deriving (Eq) + +prettyAmbiguity :: Ref -> Doc +prettyAmbiguity ref = + if refIsAmbiguous ref + then text "ambiguous" + else text "unambiguous" + +instance Pretty Ref where + pretty ref = + ((prettyAmbiguity ref <+> pretty (refKind ref)) <> comma) + <+> pretty (refRange ref) + +refIsDef :: Ref -> Bool +refIsDef ref = refKind ref == Def diff --git a/src/Server/VfsIndex.hs b/src/Server/VfsIndex.hs new file mode 100644 index 0000000..e5a4de3 --- /dev/null +++ b/src/Server/VfsIndex.hs @@ -0,0 +1,123 @@ +{-# LANGUAGE DataKinds #-} + +module Server.VfsIndex + ( Entry, + getEntryChildren, + VfsIndex, + empty, + onOpen, + onClose, + getEntry, + ) +where + +import Agda.Utils.Functor ((<&>)) +import Agda.Utils.List1 (NonEmpty ((:|))) +import Agda.Utils.Maybe (maybeToList) +import Data.List (delete, union) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Types.Uri.More as LSP +import qualified Text.URI as ParsedUri + +data Entry = Entry + { _children :: ![ParsedUri.URI], + _isInVfs :: !Bool + } + +instance Semigroup Entry where + (Entry childrenA isInVfsA) <> (Entry childrenB isInVfsB) = Entry (union childrenA childrenB) (isInVfsA || isInVfsB) + +getEntryChildren :: Entry -> [LSP.NormalizedUri] +getEntryChildren = fmap (LSP.toNormalizedUri . LSP.Uri . ParsedUri.render) . _children + +-- | The index allows users to traverse the VFS like a tree. We infer an entry +-- for each "directory" which ultimately contains actual VFS entries. +-- For example, say the VFS contains files with the following URIs: +-- - @file:\/\/\/a\/b\/c.agda@ +-- - @file:\/\/\/a\/.agda-lib@ +-- +-- The index would store entries for the following URIs: +-- - @file:\/\/@ +-- - @file:\/\/\/a@ +-- - @file:\/\/\/a\/b@ +-- - @file:\/\/\/a\/b\/c.agda@ +-- - @file:\/\/\/a\/.agda-lib@ +data VfsIndex = VfsIndex (Map ParsedUri.URI Entry) + +empty :: VfsIndex +empty = VfsIndex Map.empty + +onOpen :: LSP.Uri -> VfsIndex -> VfsIndex +onOpen uri vfsIndex = + case ParsedUri.mkURI $ LSP.getNormalizedUri $ LSP.toNormalizedUri uri of + Nothing -> vfsIndex -- TODO: log this as an error + Just uri -> + let entryUris = dice uri + entries = + zip entryUris (True : repeat False) + <&> \(uri, isInVfs) -> (uri, Entry (maybeToList $ chop uri) isInVfs) + in foldl' (\vfsIndex (uri, entry) -> insertEntry uri entry vfsIndex) vfsIndex entries + +onClose :: LSP.Uri -> VfsIndex -> VfsIndex +onClose uri vfsIndex = + case ParsedUri.mkURI $ LSP.getNormalizedUri $ LSP.toNormalizedUri uri of + Nothing -> vfsIndex -- TODO: log this as an error + Just uri -> removeEntryFromVfs uri vfsIndex + +getEntry :: LSP.NormalizedUri -> VfsIndex -> Maybe Entry +getEntry uri (VfsIndex map) = + case ParsedUri.mkURI $ LSP.getNormalizedUri uri of + Nothing -> Nothing + Just uri -> Map.lookup uri map + +insertEntry :: ParsedUri.URI -> Entry -> VfsIndex -> VfsIndex +insertEntry uri entry (VfsIndex map) = VfsIndex $ Map.insertWith (<>) uri entry map + +removeEntryFromVfs :: ParsedUri.URI -> VfsIndex -> VfsIndex +removeEntryFromVfs uri (VfsIndex map) = deleteIfInvalidLeaf uri $ VfsIndex $ Map.adjust (\entry -> entry {_isInVfs = False}) uri map + +updateParentAfterDelete :: ParsedUri.URI -> VfsIndex -> VfsIndex +updateParentAfterDelete childUri vfsIndex@(VfsIndex map) = + case chop childUri of + Nothing -> vfsIndex + Just parentUri -> + deleteIfInvalidLeaf parentUri $ + VfsIndex $ + Map.adjust (\entry -> entry {_children = delete childUri $ _children entry}) parentUri map + +isValidLeaf :: Entry -> Bool +isValidLeaf entry = _isInVfs entry || not (null (_children entry)) + +deleteIfInvalidLeaf :: ParsedUri.URI -> VfsIndex -> VfsIndex +deleteIfInvalidLeaf uri vfsIndex@(VfsIndex map) = + case Map.lookup uri map of + Just entry + | not (isValidLeaf entry) -> + updateParentAfterDelete uri $ VfsIndex $ Map.delete uri map + _ -> vfsIndex + +dice :: ParsedUri.URI -> [ParsedUri.URI] +dice uri = uri : concat (dice <$> chop uri) + +chop :: ParsedUri.URI -> Maybe ParsedUri.URI +chop (ParsedUri.URI scheme authority path query (Just _fragment)) = + Just $ ParsedUri.URI scheme authority path query Nothing +chop (ParsedUri.URI scheme authority path query@(_ : _) Nothing) = + Just $ ParsedUri.URI scheme authority path (init query) Nothing +chop (ParsedUri.URI scheme authority path@(Just _) [] Nothing) = + Just $ ParsedUri.URI scheme authority (chopPath path) [] Nothing +chop (ParsedUri.URI scheme authority@(Right _) Nothing [] Nothing) = + Just $ ParsedUri.URI scheme (Left True) Nothing [] Nothing +chop (ParsedUri.URI scheme@(Just _) authority@(Left _) Nothing [] Nothing) = + Just $ ParsedUri.URI Nothing authority Nothing [] Nothing +chop (ParsedUri.URI Nothing authority@(Left _) Nothing [] Nothing) = Nothing + +type Path = Maybe (Bool, NonEmpty (ParsedUri.RText 'ParsedUri.PathPiece)) + +chopPath :: Path -> Path +chopPath (Just (True, parts)) = Just (False, parts) +chopPath (Just (False, part :| parts@(_ : _))) = Just (False, part :| init parts) +chopPath (Just (False, part :| [])) = Nothing +chopPath Nothing = Nothing diff --git a/stack.yaml.lock b/stack.yaml.lock index d9c754b..82be79c 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -5,9 +5,9 @@ packages: - completed: - hackage: Agda-2.8.0@sha256:f85f3b10eb034687b07d073686ab97c947082eecc5ad268cbe20a4c774abcaae,34434 + hackage: Agda-2.8.0@sha256:b73b1b6685650d4429074f10440952cecb7aef190a994f75d168c354d20b01a8,34453 pantry-tree: - sha256: 01cbe34629f37fa56a411390d4d9fa281bb92b8a66a6757232240f58380678a7 + sha256: 7dace5cc1fe5a4f09212dda58392ae29f34bb1382c6eb04cb86514b5f5e2da32 size: 43914 original: hackage: Agda-2.8.0 diff --git a/test/Test.hs b/test/Test.hs index cb14b2a..f964065 100644 --- a/test/Test.hs +++ b/test/Test.hs @@ -9,6 +9,13 @@ import qualified Test.WASM as WASM #endif import Test.Tasty import Test.Tasty.Options +import qualified Test.Model as Model +import qualified Test.ModelMonad as ModelMonad +import qualified Test.Indexer.Invariants as IndexerInvariants +import qualified Test.Indexer.NoAnonFunSymbol as NoAnonFunSymbol +import qualified Test.Uri as URI +import qualified Test.Indexer as Indexer +import qualified Test.AgdaLibResolution as AgdaLibResolution -- Define the custom option newtype AlsPathOption = AlsPathOption FilePath @@ -24,15 +31,22 @@ main :: IO () main = do let opts = [Option (Proxy :: Proxy AlsPathOption)] ingredients = includingOptions opts : defaultIngredients - defaultMainWithIngredients ingredients tests + defaultMainWithIngredients ingredients =<< tests -tests :: TestTree -tests = askOption $ \(AlsPathOption alsPath) -> - testGroup - "Tests" - [ SrcLoc.tests, - LSP.tests alsPath +tests :: IO TestTree +tests = do + indexerTests <- Indexer.tests + return $ askOption $ \(AlsPathOption alsPath) -> + testGroup + "Tests" + [ SrcLoc.tests, + LSP.tests alsPath, + URI.tests, + Model.tests, + ModelMonad.tests, + AgdaLibResolution.tests, + indexerTests #if defined(wasm32_HOST_ARCH) - , WASM.tests alsPath + , WASM.tests alsPath #endif - ] \ No newline at end of file + ] \ No newline at end of file diff --git a/test/Test/AgdaLibResolution.hs b/test/Test/AgdaLibResolution.hs new file mode 100644 index 0000000..457db09 --- /dev/null +++ b/test/Test/AgdaLibResolution.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE CPP #-} + +module Test.AgdaLibResolution (tests) where + +#if MIN_VERSION_Agda(2,8,0) +import Agda.Interaction.Library (parseLibName) +#endif +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Utils.Lens ((^.)) +import Control.Monad.IO.Class (liftIO) +import Indexer (indexFile, usingSrcAsCurrent) +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (runServerT) +import Server.AgdaLibResolver (findAgdaLib) +import qualified Server.Filesystem as FS +import Server.Model.AgdaLib (AgdaLibOrigin (FromFile), agdaLibIncludes, agdaLibName, agdaLibOrigin) +import Server.Model.Monad (MonadAgdaLib, askAgdaLib, runWithAgdaLib, runWithAgdaLibT) +import System.Directory (makeAbsolute) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?=)) +import qualified TestData + +natPath, constPath, agdaLibPath, srcPath :: FilePath +natPath = "test/data/libs/no-deps/src/Data/Nat.agda" +constPath = "test/data/libs/no-deps/src/Constants.agda" +agdaLibPath = "test/data/libs/no-deps/no-deps.agda-lib" +srcPath = "test/data/libs/no-deps/src" + +tests :: TestTree +tests = + testGroup + "Agda lib resolution" + [ testCase "Explicit" $ do + model <- TestData.getModel + + absConstPath <- makeAbsolute constPath + absAgdaLibPath <- makeAbsolute agdaLibPath + absSrcPath <- makeAbsolute srcPath + + LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ do + lib <- findAgdaLib absConstPath + +#if MIN_VERSION_Agda(2,8,0) + liftIO $ lib ^. agdaLibName @?= parseLibName "no-deps" +#else + liftIO $ lib ^. agdaLibName @?= "no-deps" +#endif + liftIO $ lib ^. agdaLibOrigin @?= FromFile (FS.LocalFilePath absAgdaLibPath) + liftIO $ lib ^. agdaLibIncludes @?= [FS.LocalFilePath absSrcPath], + testCase "Module without imports in lib without dependencies" $ do + model <- TestData.getModel + + LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ do + runWithAgdaLib (LSP.filePathToUri natPath) $ do + natSrc <- TestData.parseSourceFromPath natPath + _ <- indexFile natSrc + return (), + testCase "Module with imports in lib without lib dependencies" $ do + model <- TestData.getModel + + LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ do + runWithAgdaLib (LSP.filePathToUri constPath) $ do + constSrc <- TestData.parseSourceFromPath constPath + _ <- indexFile constSrc + return () + ] diff --git a/test/Test/Indexer.hs b/test/Test/Indexer.hs new file mode 100644 index 0000000..dcf3b9f --- /dev/null +++ b/test/Test/Indexer.hs @@ -0,0 +1,16 @@ +module Test.Indexer (tests) where + +import qualified Test.Indexer.Invariants as Invariants +import qualified Test.Indexer.NoAnonFunSymbol as NoAnonFunSymbol +import qualified Test.Indexer.Reload as Reload +import Test.Tasty (TestTree, testGroup) + +tests :: IO TestTree +tests = do + invariantsTests <- Invariants.tests + return $ + testGroup "Indexer" $ + [ invariantsTests, + NoAnonFunSymbol.tests, + Reload.tests + ] diff --git a/test/Test/Indexer/Invariants.hs b/test/Test/Indexer/Invariants.hs new file mode 100644 index 0000000..663a8a8 --- /dev/null +++ b/test/Test/Indexer/Invariants.hs @@ -0,0 +1,24 @@ +module Test.Indexer.Invariants (tests) where + +import Control.Monad (forM) +import Test.Indexer.Invariants.NoDuplicateDecl (testNoDuplicateDecl) +import Test.Indexer.Invariants.NoMissing (testNoMissing) +import Test.Indexer.Invariants.NoOverlap (testNoOverlap) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Golden (findByExtension) +import qualified TestData + +tests :: IO TestTree +tests = do + inPaths <- findByExtension [".agda"] "test/data/Indexer" + files <- forM inPaths $ \inPath -> do + TestData.AgdaFileDetails testName file interface <- TestData.agdaFileDetails inPath + return (testName, file, interface) + + return $ + testGroup + "Invariants" + [ testGroup "No reference overlap" ((\(name, file, _interface) -> testNoOverlap name file) <$> files), + testGroup "No missing references" ((\(name, file, interface) -> testNoMissing name file interface) <$> files), + testGroup "No duplicate declarations" ((\(name, file, _interface) -> testNoDuplicateDecl name file) <$> files) + ] diff --git a/test/Test/Indexer/Invariants/NoDuplicateDecl.hs b/test/Test/Indexer/Invariants/NoDuplicateDecl.hs new file mode 100644 index 0000000..415c698 --- /dev/null +++ b/test/Test/Indexer/Invariants/NoDuplicateDecl.hs @@ -0,0 +1,46 @@ +module Test.Indexer.Invariants.NoDuplicateDecl (testNoDuplicateDecl) where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (Pretty, align, pretty, prettyList, prettyShow, text, vcat, (<+>)) +import Agda.Utils.Lens ((^.)) +import Control.Monad (forM_) +import Control.Monad.Writer.CPS (Writer, execWriter, tell) +import qualified Data.Map as Map +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) +import Server.Model.Symbol (Ref, RefKind (..), refKind) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) + +data DuplicateDecl = DuplicateDecl + { ddName :: A.QName, + ddDecls :: [Ref] + } + +instance Pretty DuplicateDecl where + pretty dupDecl = + vcat $ + [text "Duplicate declarations for" <+> pretty (ddName dupDecl)] + <> fmap pretty (ddDecls dupDecl) + + prettyList = \case + [] -> text "No duplicate declarations" + [err] -> pretty err + errs -> align 5 $ (\err -> ("-", vcat [pretty err, text ""])) <$> errs + +checkDupDecls :: A.QName -> [Ref] -> Writer [DuplicateDecl] () +checkDupDecls name refs = do + let decls = filter (\ref -> refKind ref == Decl) refs + if length decls > 1 + then tell [DuplicateDecl name decls] + else return () + +testNoDuplicateDecl :: String -> AgdaFile -> TestTree +testNoDuplicateDecl name agdaFile = + testCase name $ do + let symbolRefs = (Map.toList $ agdaFile ^. agdaFileRefs) + let dupDecls = execWriter $ forM_ symbolRefs $ \(name, refs) -> + checkDupDecls name refs + + case dupDecls of + [] -> return () + _ -> assertFailure $ prettyShow dupDecls diff --git a/test/Test/Indexer/Invariants/NoMissing.hs b/test/Test/Indexer/Invariants/NoMissing.hs new file mode 100644 index 0000000..33cc208 --- /dev/null +++ b/test/Test/Indexer/Invariants/NoMissing.hs @@ -0,0 +1,82 @@ +-- | Check that highlighting data doesn't show more references than we have +-- `Ref`s. We expect to sometimes pick up references that highlighting does not, +-- so it's okay if we have more. +module Test.Indexer.Invariants.NoMissing (testNoMissing) where + +import Agda.Interaction.Highlighting.Precise (Aspects, HighlightingInfo) +import qualified Agda.Interaction.Highlighting.Precise as HL +import Agda.Position (FromOffset, fromOffset, makeFromOffset) +import Agda.Syntax.Common.Pretty (Pretty, align, pretty, prettyList, prettyShow, pshow, text, vcat, (<+>)) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.Lens ((^.)) +import Agda.Utils.Maybe (isJust, isNothing) +import Agda.Utils.RangeMap (PairInt (PairInt), RangeMap (rangeMap)) +import Control.Monad (forM_, guard) +import Control.Monad.Writer.CPS (Writer, execWriter, tell) +import qualified Data.Map as Map +import Data.Strict (Pair ((:!:))) +import qualified Data.Strict as Strict +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) +import Server.Model.Symbol (Ref (refRange)) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) + +data MissingRefError = MissingRefError + { mreAspects :: !Aspects, + mreRange :: !LSP.Range + } + +instance Pretty MissingRefError where + pretty err = + text "Missing ref error at" + <+> pretty (mreRange err) + <+> text "with aspects" + <+> pshow (mreAspects err) + + prettyList = \case + [] -> text "No missing ref errors" + [err] -> pretty err + errs -> align 5 $ (\err -> ("-", vcat [pretty err, text ""])) <$> errs + +areAspectsRef :: Aspects -> Bool +areAspectsRef aspects = case HL.aspect aspects of + Just HL.PrimitiveType -> True + Just (HL.Name _ _) -> True + _ -> False + +highlightingRefRanges :: FromOffset -> HighlightingInfo -> [(Aspects, LSP.Range)] +highlightingRefRanges table highlightingInfo = do + (startOffset, PairInt (endOffset :!: aspects)) <- Map.toList $ rangeMap highlightingInfo + guard $ areAspectsRef aspects + let (startLine, startChar) = fromOffset table startOffset + startPos = LSP.Position (fromIntegral startLine) (fromIntegral startChar - 1) + (endLine, endChar) = fromOffset table (endOffset - 1) + endPos = LSP.Position (fromIntegral endLine) (fromIntegral endChar) + range = LSP.Range startPos endPos + return (aspects, range) + +hasCorrespondingRef :: AgdaFile -> Aspects -> LSP.Range -> Bool +hasCorrespondingRef agdaFile aspects range = + let refs = concat $ Map.elems $ agdaFile ^. agdaFileRefs + in isNothing (HL.definitionSite aspects) + || any (\ref -> refRange ref == range) refs + +checkCorrespondingRef :: AgdaFile -> Aspects -> LSP.Range -> Writer [MissingRefError] () +checkCorrespondingRef agdaFile aspects range = + if hasCorrespondingRef agdaFile aspects range + then return () + else tell $ [MissingRefError aspects range] + +testNoMissing :: String -> AgdaFile -> TCM.Interface -> TestTree +testNoMissing name agdaFile interface = testCase name $ do + let highlighting = TCM.iHighlighting interface + let table = makeFromOffset $ Strict.toStrict $ TCM.iSource interface + let highlightingRanges = highlightingRefRanges table highlighting + + let errors = execWriter $ forM_ highlightingRanges $ \(aspects, range) -> + checkCorrespondingRef agdaFile aspects range + + case errors of + [] -> return () + _ -> assertFailure $ prettyShow errors diff --git a/test/Test/Indexer/Invariants/NoOverlap.hs b/test/Test/Indexer/Invariants/NoOverlap.hs new file mode 100644 index 0000000..7bdb0ec --- /dev/null +++ b/test/Test/Indexer/Invariants/NoOverlap.hs @@ -0,0 +1,154 @@ +-- | Check that `Ref`s don't overlap, so that there is only one `Ref` instance +-- per actual reference. +module Test.Indexer.Invariants.NoOverlap (testNoOverlap) where + +import qualified Agda.Syntax.Abstract as A +import Agda.Syntax.Common.Pretty (Doc, Pretty (prettyList), align, parens, pretty, prettyShow, text, vcat, (<+>)) +import Agda.Utils.Lens ((^.)) +import Control.Monad (forM, forM_) +import Control.Monad.Writer.CPS (Writer, execWriter, tell) +import Data.Foldable (foldrM) +import Data.IntMap (IntMap) +import qualified Data.IntMap as IntMap +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Lens as LSP +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model.AgdaFile (AgdaFile, agdaFileRefs) +import Server.Model.Symbol (Ref (refRange), refIsAmbiguous) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) + +data OverlapError = OverlapError + { oeLineNum :: !Int, + oePart1 :: !LinePart, + oePart2 :: !LinePart + } + +instance Pretty OverlapError where + pretty err = + vcat + [ text "Overlap error at line number" + <+> pretty (oeLineNum err + 1) + <+> linePartPrettyRange (oePart1 err) + <+> text "and" + <+> linePartPrettyRange (oePart2 err), + pretty (linePartName (oePart1 err)) + <+> pretty (linePartRef (oePart1 err)), + pretty (linePartName (oePart2 err)) + <+> pretty (linePartRef (oePart2 err)) + ] + + prettyList = \case + [] -> text "No overlap errors" + [err] -> pretty err + errs -> align 5 $ (\err -> ("-", vcat [pretty err, text ""])) <$> errs + +type OverlapResult = Writer [OverlapError] + +data LinePart + = RangePart !A.QName !Ref !Int !Int + | ToEndPart !A.QName !Ref !Int + +linePartPrettyRange :: LinePart -> Doc +linePartPrettyRange (RangePart _ _ start end) = text "from" <+> pretty start <+> text "to" <+> pretty end +linePartPrettyRange (ToEndPart _ _ start) = text "from" <+> pretty start <+> text "to the end of the line" + +linePartName :: LinePart -> A.QName +linePartName (RangePart name _ _ _) = name +linePartName (ToEndPart name _ _) = name + +linePartRef :: LinePart -> Ref +linePartRef (RangePart _ ref _ _) = ref +linePartRef (ToEndPart _ ref _) = ref + +assertPartsNonoverlapping :: Int -> LinePart -> LinePart -> OverlapResult () +assertPartsNonoverlapping lineNum part1 part2 = case (part1, part2) of + -- Allow refs known to be ambiguous + (_, _) + | refIsAmbiguous (linePartRef part1) + && refIsAmbiguous (linePartRef part2) -> + return () + (ToEndPart _ _ _, ToEndPart _ _ _) -> err + (RangePart _ _ _ rangeEnd, ToEndPart _ _ toEndStart) + | rangeEnd > toEndStart -> err + (ToEndPart _ _ toEndStart, RangePart _ _ _ rangeEnd) + | rangeEnd > toEndStart -> err + (RangePart _ _ start1 end1, RangePart _ _ start2 end2) + | (start1 <= start2 && end1 > start2) + || (start2 <= start1 && end2 > start1) -> + err + _ -> return () + where + err = tell $ [OverlapError lineNum part1 part2] + +newtype Line = Line [LinePart] + +rangePart :: (Integral n) => A.QName -> Ref -> n -> n -> Line +rangePart name ref start end = Line [RangePart name ref (fromIntegral start) (fromIntegral end)] + +toEndPart :: (Integral n) => A.QName -> Ref -> n -> Line +toEndPart name ref start = Line [ToEndPart name ref (fromIntegral start)] + +tryInsertPart :: Int -> LinePart -> Line -> OverlapResult (Line) +tryInsertPart lineNum part (Line parts) = do + forM_ parts $ \part2 -> + assertPartsNonoverlapping lineNum part part2 + return $ Line $ part : parts + +tryMerge :: Int -> Line -> Line -> OverlapResult (Line) +tryMerge lineNum (Line newParts) line = foldrM (tryInsertPart lineNum) line newParts + +rangeToLines :: A.QName -> Ref -> LSP.Range -> [(Int, Line)] +rangeToLines name ref range = + if startLine == endLine + then + [ ( startLine, + rangePart + name + ref + (range ^. LSP.start . LSP.character) + (range ^. LSP.end . LSP.character) + ) + ] + else + let start = (startLine, toEndPart name ref $ range ^. LSP.start . LSP.character) + end = (endLine, rangePart name ref 0 $ range ^. LSP.end . LSP.character) + middle = do + lineNum <- [startLine + 1 .. endLine - 1] + return (lineNum, toEndPart name ref 0) + in [start] <> middle <> [end] + where + startLine = fromIntegral $ range ^. LSP.start . LSP.line + endLine = fromIntegral $ range ^. LSP.end . LSP.line + +newtype FileRanges = FileRanges (IntMap (Line)) + +emptyFileRanges :: FileRanges +emptyFileRanges = FileRanges IntMap.empty + +tryInsertLine :: Int -> Line -> FileRanges -> OverlapResult (FileRanges) +tryInsertLine lineNum line (FileRanges ranges) = + FileRanges <$> IntMap.alterF helper lineNum ranges + where + helper Nothing = return $ Just line + helper (Just oldLine) = Just <$> tryMerge lineNum line oldLine + +tryInsertRange :: A.QName -> Ref -> LSP.Range -> FileRanges -> OverlapResult (FileRanges) +tryInsertRange name ref range fileRanges = do + let lines = rangeToLines name ref range + foldrM (uncurry tryInsertLine) fileRanges lines + +testNoOverlap :: String -> AgdaFile -> TestTree +testNoOverlap name file = testCase name $ do + let refs = + concatMap (\(name, refs) -> (\ref -> (name, ref)) <$> refs) $ + Map.toList $ + file ^. agdaFileRefs + let fileRanges = emptyFileRanges + let errors = + execWriter $ + foldrM (\(name, ref) -> tryInsertRange name ref (refRange ref)) fileRanges refs + + case errors of + [] -> return () + _ -> assertFailure $ prettyShow errors diff --git a/test/Test/Indexer/NoAnonFunSymbol.hs b/test/Test/Indexer/NoAnonFunSymbol.hs new file mode 100644 index 0000000..4a6f997 --- /dev/null +++ b/test/Test/Indexer/NoAnonFunSymbol.hs @@ -0,0 +1,25 @@ +module Test.Indexer.NoAnonFunSymbol (tests) where + +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Utils.Lens ((^.)) +import Agda.Utils.Maybe (ifJustM, whenJust, whenJustM) +import Control.Monad (forM) +import Data.Foldable (find) +import Data.List (isInfixOf) +import qualified Data.Map as Map +import Server.Model.AgdaFile (agdaFileSymbols) +import Test.Tasty (TestTree) +import Test.Tasty.HUnit (assertFailure, testCase) +import qualified TestData + +tests :: TestTree +tests = + testCase "No symbols for internal anonymous function names" $ do + TestData.AgdaFileDetails name agdaFile interface <- TestData.agdaFileDetails "test/data/AnonFun.agda" + + let symbolNames = prettyShow <$> Map.keys (agdaFile ^. agdaFileSymbols) + whenJust (find isAnonFunName symbolNames) $ \name -> + assertFailure $ "Found symbol for internal anonymous function: " ++ name + +isAnonFunName :: String -> Bool +isAnonFunName name = ".extendedlambda" `isInfixOf` name diff --git a/test/Test/Indexer/Reload.hs b/test/Test/Indexer/Reload.hs new file mode 100644 index 0000000..a3b4ef5 --- /dev/null +++ b/test/Test/Indexer/Reload.hs @@ -0,0 +1,74 @@ +module Test.Indexer.Reload (tests) where + +import Agda.Interaction.Imports.Virtual (parseSourceFromContents) +import Agda.Syntax.Common.Pretty (prettyShow) +import Control.Monad.IO.Class (liftIO) +import qualified Data.Text as Text +import Indexer (indexFile) +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (runServerT) +import Server.Model.Monad (runWithAgdaLib) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (assertFailure, testCase, (@?=)) +import qualified TestData + +tests :: TestTree +tests = + testGroup "Reload" $ + [ testCase "Reload single file" $ testReloadFile "test/data/A.agda", + testCase "Reload after changes" testReloadChanges + ] + +testReloadFile :: FilePath -> IO () +testReloadFile path = do + let uri = LSP.filePathToUri path + model <- TestData.getModel + + LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ do + runWithAgdaLib uri $ do + src <- TestData.parseSourceFromPath path + _ <- indexFile src + _ <- indexFile src + return () + +testReloadChanges :: IO () +testReloadChanges = do + let path = "test/data/A.agda" + let contentsA = + Text.unlines + [ "module A where", + "", + "data T : Set where", + " tt : T" + ] + let contentsB = + Text.unlines + [ "module A where", + "", + "data T : Set where", + " tt : T", + "", + "f : T -> T", + "f x = x" + ] + + let uri = LSP.filePathToUri path + model <- TestData.getModel + + LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ do + runWithAgdaLib uri $ do + src0 <- TestData.parseSourceFromPathAndContents path contentsA + agdaFile0 <- indexFile src0 + + src1 <- TestData.parseSourceFromPathAndContents path contentsB + agdaFile1 <- indexFile src1 + + src2 <- TestData.parseSourceFromPathAndContents path contentsA + agdaFile2 <- indexFile src2 + + liftIO $ agdaFile0 @?= agdaFile2 diff --git a/test/Test/Model.hs b/test/Test/Model.hs new file mode 100644 index 0000000..e4f5432 --- /dev/null +++ b/test/Test/Model.hs @@ -0,0 +1,59 @@ +module Test.Model (tests) where + +import Agda.Utils.Lens (set, (<&>), (^.)) +import Agda.Utils.Maybe (isJust, isNothing) +import qualified Data.Map as Map +import qualified Language.LSP.Protocol.Types as LSP +import Server.Model (Model (Model)) +import qualified Server.Model as Model +import Server.Model.AgdaFile (emptyAgdaFile) +import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?), (@?=)) +import qualified TestData + +tests :: TestTree +tests = + testGroup + "Model" + [ testCase "getKnownAgdaLib gets known Agda lib" $ do + model <- TestData.getModel + + let Just agdaLib = Model.getKnownAgdaLib TestData.fileUri1 model + length (agdaLib ^. agdaLibIncludes) @?= 3 + + let Just agdaLib = Model.getKnownAgdaLib TestData.fileUri2 model + length (agdaLib ^. agdaLibIncludes) @?= 1 + + let Just agdaLib = Model.getKnownAgdaLib TestData.fileUri3 model + length (agdaLib ^. agdaLibIncludes) @?= 3 + + return (), + testCase "getKnownAgdaLib fails on unknown Agda lib" $ do + model <- TestData.getModel + + let result = Model.getKnownAgdaLib TestData.fakeUri model + isNothing result @? "got Agda lib, but should be unknown" + + return (), + testCase "getAgdaFile gets known Agda file" $ do + model <- TestData.getModel + + let result = Model.getAgdaFile TestData.fileUri1 model + isJust result @? "didn't get known Agda file" + + let result = Model.getAgdaFile TestData.fileUri2 model + isJust result @? "didn't get known Agda file" + + let result = Model.getAgdaFile TestData.fileUri3 model + isJust result @? "didn't get known Agda file" + + return (), + testCase "getAgdaFile fails on unknown Agda file" $ do + model <- TestData.getModel + + let result = Model.getAgdaFile TestData.fakeUri model + isNothing result @? "got Agda file, but should be unknown" + + return () + ] diff --git a/test/Test/ModelMonad.hs b/test/Test/ModelMonad.hs new file mode 100644 index 0000000..13bc440 --- /dev/null +++ b/test/Test/ModelMonad.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE RankNTypes #-} + +module Test.ModelMonad (tests) where + +import qualified Agda.Compiler.Backend as TestData +import Agda.Utils.Either (isLeft, isRight) +import Agda.Utils.IORef (newIORef, readIORef, writeIORef) +import Agda.Utils.Lens ((^.)) +import Control.Concurrent (newChan) +import Control.Monad.IO.Class (MonadIO (liftIO)) +import Control.Monad.Reader (ReaderT (ReaderT, runReaderT)) +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Protocol.Utils.SMethodMap as SMethodMap +import qualified Language.LSP.Server as LSP +import Monad (Env (Env, envModel), ServerT, createInitEnv, runServerT) +import Options (Config, defaultOptions, initConfig) +import qualified Server.CommandController as CommandController +import Server.Model (Model) +import Server.Model.AgdaLib (agdaLibIncludes) +import Server.Model.Handler (requestHandlerWithAgdaFile) +import Server.Model.Monad (MonadAgdaLib (askAgdaLib)) +import qualified Server.ResponseController as ResponseController +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?), (@?=)) +import qualified TestData + +tests :: TestTree +tests = + testGroup + "Model monads" + [ testGroup + "WithAgdaFileM" + [ testCase "gets known Agda file" $ do + let method = LSP.SMethod_TextDocumentDocumentSymbol + message = TestData.documentSymbolMessage TestData.fileUri1 + + let handlers = requestHandlerWithAgdaFile method $ \req responder -> do + agdaLib <- askAgdaLib + liftIO $ length (agdaLib ^. agdaLibIncludes) @?= 3 + responder $ Right $ LSP.InL [] + + model <- TestData.getModel + result <- runHandler method message model handlers + + isRight result @? "didn't get known Agda file: " <> show result + + return (), + testCase "fails on unknown Agda file" $ do + let method = LSP.SMethod_TextDocumentDocumentSymbol + message = TestData.documentSymbolMessage TestData.fakeUri + + let handlers = requestHandlerWithAgdaFile method $ \req responder -> do + responder $ Right $ LSP.InL [] + + model <- TestData.getModel + result <- runHandler method message model handlers + + isLeft result @? "got Agda file, but should be unknown" + + return () + ] + ] + +runHandler :: + forall (m :: LSP.Method LSP.ClientToServer LSP.Request). + (Show (LSP.ErrorData m)) => + LSP.SMethod m -> + LSP.TRequestMessage m -> + Model -> + LSP.Handlers (ServerT (LSP.LspM Config)) -> + IO (Either (LSP.TResponseError m) (LSP.MessageResult m)) +runHandler m request model handlers = do + resultRef <- newIORef Nothing + let callback = \response -> liftIO $ writeIORef resultRef (Just response) + + let Just (LSP.ClientMessageHandler handler) = SMethodMap.lookup m $ LSP.reqHandlers handlers + + LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ handler request callback + + Just result <- readIORef resultRef + return result diff --git a/test/Test/Uri.hs b/test/Test/Uri.hs new file mode 100644 index 0000000..e35947f --- /dev/null +++ b/test/Test/Uri.hs @@ -0,0 +1,23 @@ +module Test.Uri (tests) where + +import qualified Language.LSP.Protocol.Types as LSP +import Language.LSP.Protocol.Types.Uri.More (uriHeightAbove) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit (testCase, (@?=)) + +tests :: TestTree +tests = + testGroup "URI" $ + [ testGroup "uriHeightAbove" $ + [ testCase "calculates positive height" $ do + let ancestor = LSP.toNormalizedUri $ LSP.Uri "https://example.com/a/b/c/d/" + let descendant = LSP.toNormalizedUri $ LSP.Uri "https://example.com/a/b/c/d/e/f" + let height = uriHeightAbove ancestor descendant + height @?= 2, + testCase "calculates 0 height" $ do + let ancestor = LSP.toNormalizedUri $ LSP.Uri "file://home/user/username/a/" + let descendant = LSP.toNormalizedUri $ LSP.Uri "file://home/user/username/a" + let height = uriHeightAbove ancestor descendant + height @?= 0 + ] + ] diff --git a/test/TestData.hs b/test/TestData.hs new file mode 100644 index 0000000..4766974 --- /dev/null +++ b/test/TestData.hs @@ -0,0 +1,190 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} + +module TestData + ( documentSymbolMessage, + getModel, + fileUri1, + fileUri2, + fileUri3, + fakeUri, + getServerEnv, + AgdaFileDetails (..), + agdaFileDetails, + parseSourceFromPath, + parseSourceFromPathAndContents, + ) +where + +import Agda.Interaction.FindFile + ( SourceFile (SourceFile), +#if MIN_VERSION_Agda(2,8,0) +#else + srcFilePath, +#endif + ) +import qualified Agda.Interaction.Imports as Imp +import qualified Agda.Interaction.Options +import Agda.Syntax.Abstract.More () +import Agda.Syntax.Common.Pretty (prettyShow) +import Agda.Syntax.Translation.ConcreteToAbstract (topLevelDecls) +import qualified Agda.TypeChecking.Monad as TCM +import Agda.Utils.FileName (absolute) +import Agda.Utils.IORef (newIORef) +import Agda.Utils.Lens (set, (<&>)) +import Control.Concurrent (newChan) +import Control.Monad.IO.Class (MonadIO, liftIO) +import qualified Data.Map as Map +import Indexer (indexFile, withAstFor, usingSrcAsCurrent) +import qualified Language.LSP.Protocol.Message as LSP +import qualified Language.LSP.Protocol.Types as LSP +import qualified Language.LSP.Server as LSP +import Monad (Env (Env), runServerT, catchTCError) +import Options (defaultOptions, initConfig) +import qualified Server.CommandController as CommandController +import Server.Model (Model (Model)) +import Server.Model.AgdaFile (AgdaFile, emptyAgdaFile) +import Server.Model.AgdaLib (agdaLibIncludes, initAgdaLib) +import Server.Model.Monad (runWithAgdaLib, MonadAgdaLib) +import qualified Server.ResponseController as ResponseController +import System.FilePath (takeBaseName, ()) +import Agda.TypeChecking.Pretty (prettyTCM) +import Data.Text (Text) +import Agda.Interaction.Imports.Virtual (parseSourceFromContents) +import qualified Server.Filesystem as FS +import qualified Server.VfsIndex as VfsIndex + +data AgdaFileDetails = AgdaFileDetails + { fileName :: String, + agdaFile :: AgdaFile, + interface :: TCM.Interface + } + +agdaFileDetails :: FilePath -> IO AgdaFileDetails +agdaFileDetails inPath = do + let testName = takeBaseName inPath + uri = LSP.filePathToUri inPath + model <- TestData.getModel + + (file, interface) <- LSP.runLspT undefined $ do + env <- TestData.getServerEnv model + runServerT env $ do + let withSrc f = runWithAgdaLib uri $ do + TCM.liftTCM $ TCM.setCommandLineOptions Agda.Interaction.Options.defaultOptions + src <- parseSourceFromPath inPath + + f src + + let onErr = \err -> runWithAgdaLib uri $ do + t <- TCM.liftTCM $ prettyTCM err + error $ prettyShow t + + interface <- (withSrc $ \src -> usingSrcAsCurrent src $ do + checkResult <- TCM.liftTCM $ Imp.typeCheckMain Imp.TypeCheck src + return $ Imp.crInterface checkResult) `catchTCError` onErr + + file <- withSrc indexFile `catchTCError` onErr + + return (file, interface) + + return $ AgdaFileDetails testName file interface + +sourceFileFromPath :: (TCM.MonadTCM m) => FilePath -> m SourceFile +sourceFileFromPath path = do + absPath <- liftIO $ absolute path +#if MIN_VERSION_Agda(2,8,0) + TCM.liftTCM $ TCM.srcFromPath absPath +#else + return $ SourceFile absPath +#endif + +parseSourceFromPath :: (TCM.MonadTCM m) => FilePath -> m Imp.Source +parseSourceFromPath path = do + srcFile <- sourceFileFromPath path + TCM.liftTCM $ Imp.parseSource srcFile + +parseSourceFromPathAndContents :: + (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) => + FilePath -> + Text -> + m Imp.Source +parseSourceFromPathAndContents path contents = do + srcFile <- sourceFileFromPath path + let uri = LSP.toNormalizedUri $ LSP.filePathToUri path + parseSourceFromContents uri srcFile contents + +-------------------------------------------------------------------------------- + +documentSymbolMessage :: LSP.NormalizedUri -> LSP.TRequestMessage LSP.Method_TextDocumentDocumentSymbol +documentSymbolMessage uri = + let params = + LSP.DocumentSymbolParams + Nothing + Nothing + (LSP.TextDocumentIdentifier $ LSP.fromNormalizedUri uri) + in LSP.TRequestMessage + "2.0" + (LSP.IdInt 0) + LSP.SMethod_TextDocumentDocumentSymbol + params + +-------------------------------------------------------------------------------- + +fileUri1 :: LSP.NormalizedUri +fileUri1 = LSP.toNormalizedUri $ LSP.Uri "file:///home/user2/project2/A/B/C.agda" + +fileUri2 :: LSP.NormalizedUri +fileUri2 = LSP.toNormalizedUri $ LSP.Uri "file:///home/user/project2/X.agda" + +fileUri3 :: LSP.NormalizedUri +fileUri3 = LSP.toNormalizedUri $ LSP.Uri "https://example.com/agda/Main.agda" + +fakeUri :: LSP.NormalizedUri +fakeUri = LSP.toNormalizedUri $ LSP.Uri "file:///home/user2/project/Test.agda" + +getModel :: IO Model +getModel = do + let includes1 = + FS.Uri . LSP.toNormalizedUri . LSP.Uri + <$> [ "file:///home/user/project1/", + "file:///home/user2/project2/", + "https://example.com/agda/" + ] + testLib1 <- + initAgdaLib + <&> set agdaLibIncludes includes1 + + let includes2 = + FS.Uri . LSP.toNormalizedUri . LSP.Uri + <$> ["file:///home/user/project2/"] + testLib2 <- + initAgdaLib + <&> set agdaLibIncludes includes2 + + let libs = [testLib1, testLib2] + + let testFile1 = emptyAgdaFile + let testFile2 = emptyAgdaFile + let testFile3 = emptyAgdaFile + + let files = + Map.fromList + [ (fileUri1, testFile1), + (fileUri2, testFile2), + (fileUri3, testFile3) + ] + + return $ Model libs files + +-------------------------------------------------------------------------------- + +getServerEnv :: (MonadIO m) => Model -> m Env +getServerEnv model = + Env defaultOptions True initConfig + <$> liftIO newChan + <*> liftIO CommandController.new + <*> liftIO newChan + <*> liftIO ResponseController.new + <*> (pure $ FS.Layered [FS.Wrap FS.OsFilesystem]) + <*> liftIO (newIORef VfsIndex.empty) + <*> liftIO (newIORef model) diff --git a/test/data/AST/Basic b/test/data/AST/Basic new file mode 100644 index 0000000..49fe7d5 --- /dev/null +++ b/test/data/AST/Basic @@ -0,0 +1,237 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Basic, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.one, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Nat}], + ScopedDecl -> + [FunDef -> + {name -> Basic.one, + clauses -> + [lhs = ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Con -> Basic.Nat.suc, + arg -> ScopedExpr -> Con -> Basic.Nat.zero}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.two, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Nat}], + ScopedDecl -> + [FunDef -> + {name -> Basic.two, + clauses -> + [lhs = ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Con -> Basic.Nat.suc, + arg -> ScopedExpr -> Def' -> Basic.one}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Test, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Test, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Test', + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Test', dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.hello, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Test}], + ScopedDecl -> + [FunDef -> + {name -> Basic.hello, + clauses -> + [lhs = ScopedExpr -> + Con -> Basic.Test.test | Basic.Test'.test]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Basic.Empty, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Basic.Empty, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.Not, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Agda.Primitive.Set, + codom -> ScopedExpr -> Def' -> Agda.Primitive.Set}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.Not, + clauses -> + [lhs = ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Def' -> Basic.Empty}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.Goodbye, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [FunDef -> + {name -> Basic.Goodbye, + clauses -> + [lhs = ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Def' -> Basic.Not, + arg -> ScopedExpr -> Def' -> Basic.Test}]}]]], + ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> Basic.A, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Basic.Test, + codom -> ScopedExpr -> Def' -> Agda.Primitive.Set}}], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.testId, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Basic.Test, + codom -> ScopedExpr -> Def' -> Basic.Test}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.testId, + clauses -> + [lhs = ScopedExpr -> + Con -> Basic.Test.test | Basic.Test'.test]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.id, + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Var -> A}}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.id, clauses -> [lhs = ScopedExpr -> Expr ->]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.id', + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Var -> A}}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.id', clauses -> [lhs = ScopedExpr -> Expr ->]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.id'', + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Var -> A, + codom -> ScopedExpr -> Var -> A}}}], + ScopedDecl -> + [FunDef -> + {name -> Basic.id'', + clauses -> + [lhs = ScopedExpr -> + Let -> + {bindings -> + [letDeclared x, let x = ScopedExpr -> Var -> x, letDeclared A, + let A = ScopedExpr -> Var -> A], + body -> ScopedExpr -> Var -> x}]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [RecSig -> + {name -> Basic.World, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + type -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [RecDef -> + {name -> Basic.World, dataDefParams -> [], + decls -> + [ScopedDecl -> + [Field -> + {name -> Basic.World.north, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Test}], + ScopedDecl -> + [Field -> + {name -> Basic.World.south, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.Test'}]]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Basic.earth, + type -> ScopedExpr -> ScopedExpr -> Def' -> Basic.World}], + ScopedDecl -> + [FunDef -> + {name -> Basic.earth, + clauses -> + [lhs = ScopedExpr -> Con -> Basic.Test.test | Basic.Test'.test, + lhs = ScopedExpr -> + Con -> Basic.Test.test | Basic.Test'.test]}]]]]}] \ No newline at end of file diff --git a/test/data/AST/FunWithoutDeclOrDef b/test/data/AST/FunWithoutDeclOrDef new file mode 100644 index 0000000..b731557 --- /dev/null +++ b/test/data/AST/FunWithoutDeclOrDef @@ -0,0 +1,34 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> FunWithoutDeclOrDef, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> FunWithoutDeclOrDef.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> + {name -> FunWithoutDeclOrDef.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> FunWithoutDeclOrDef.sucsuc, + type -> ScopedExpr -> Expr ->}], + ScopedDecl -> + [FunDef -> + {name -> FunWithoutDeclOrDef.sucsuc, + clauses -> [lhs = ScopedExpr -> Expr ->]}]]], + ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> FunWithoutDeclOrDef.sucsucsuc, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> FunWithoutDeclOrDef.Nat, + codom -> ScopedExpr -> Def' -> FunWithoutDeclOrDef.Nat}}]]}] \ No newline at end of file diff --git a/test/data/AST/Module b/test/data/AST/Module new file mode 100644 index 0000000..69683cc --- /dev/null +++ b/test/data/AST/Module @@ -0,0 +1,42 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Module, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Module.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Module.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Section -> + {moduleName -> Module.M, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Module.M.f, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Module.Nat, + codom -> ScopedExpr -> Def' -> Module.Nat}}], + ScopedDecl -> + [FunDef -> + {name -> Module.M.f, clauses -> [lhs = ScopedExpr -> Var -> n]}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Module.M.N, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Module.M.N, dataDefParams -> []}]]]]}]]}] \ No newline at end of file diff --git a/test/data/AST/Mutual b/test/data/AST/Mutual new file mode 100644 index 0000000..3afcbad --- /dev/null +++ b/test/data/AST/Mutual @@ -0,0 +1,133 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Mutual, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Mutual.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Mutual.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Section -> + {moduleName -> Mutual.Forward, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [RecSig -> + {name -> Mutual.Forward.MutualRecord, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, + generalizeTel -> + [([UserWritten A] : ScopedExpr -> + Def' -> + Agda.Primitive.Set), + ([UserWritten n] : ScopedExpr -> + Def' -> Mutual.Nat)]}, + type -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataSig -> + {name -> Mutual.Forward.MutualData, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataSig -> + {name -> Mutual.Forward.MutualData', + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Mutual.Nat, + codom -> ScopedExpr -> Def' -> Agda.Primitive.Set}}], + ScopedDecl -> + [Axiom -> + {kindOfName -> FunName, name -> Mutual.Forward.mutualFun, + type -> + ScopedExpr -> + ScopedExpr -> + Fun -> + {dom -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualRecord, + arg -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualData}, + arg -> ScopedExpr -> Con -> Mutual.Nat.zero}, + codom -> + ScopedExpr -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + App -> + {f -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualRecord, + arg -> + ScopedExpr -> + Def' -> Mutual.Forward.MutualData}, + arg -> ScopedExpr -> Con -> Mutual.Nat.zero}}}], + ScopedDecl -> + [RecDef -> + {name -> Mutual.Forward.MutualRecord, + dataDefParams -> [UserWritten A, UserWritten m], + decls -> + [ScopedDecl -> + [Field -> + {name -> Mutual.Forward.MutualRecord.mutFieldX, + type -> ScopedExpr -> ScopedExpr -> Var -> A}], + ScopedDecl -> + [Field -> + {name -> Mutual.Forward.MutualRecord.mutFieldY, + type -> ScopedExpr -> ScopedExpr -> Def' -> Mutual.Nat}]]}], + ScopedDecl -> + [DataDef -> + {name -> Mutual.Forward.MutualData, dataDefParams -> []}], + ScopedDecl -> + [DataDef -> + {name -> Mutual.Forward.MutualData', + dataDefParams -> [UserWritten A]}], + ScopedDecl -> + [FunDef -> + {name -> Mutual.Forward.mutualFun, + clauses -> [lhs = ScopedExpr -> Var -> x]}]]]]}], + ScopedDecl -> + [Section -> + {moduleName -> Mutual.Backward, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> Mutual.Backward.MutualData, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [Axiom -> + {kindOfName -> AxiomName, name -> Mutual.Backward.MutualData', + type -> + ScopedExpr -> + ScopedExpr -> + Pi -> + {dom -> + [([UserWritten A] : ScopedExpr -> + Def' -> Agda.Primitive.Set)], + codom -> + ScopedExpr -> + Fun -> + {dom -> ScopedExpr -> Def' -> Mutual.Nat, + codom -> + ScopedExpr -> Def' -> Agda.Primitive.Set}}}]]]]}]]}] \ No newline at end of file diff --git a/test/data/AST/Record b/test/data/AST/Record new file mode 100644 index 0000000..85f93a6 --- /dev/null +++ b/test/data/AST/Record @@ -0,0 +1,68 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Record, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> + [ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [DataSig -> + {name -> Record.Nat, + type -> ScopedExpr -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [DataDef -> {name -> Record.Nat, dataDefParams -> []}]]], + ScopedDecl -> + [Mutual -> + [ScopedDecl -> + [RecSig -> + {name -> Record.R, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, + generalizeTel -> + [([UserWritten n] : ScopedExpr -> Def' -> Record.Nat), + ([UserWritten A] : ScopedExpr -> + Fun -> + {dom -> + ScopedExpr -> + Def' -> Record.Nat, + codom -> + ScopedExpr -> + Def' -> + Agda.Primitive.Set}), + ([UserWritten x] : ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Var -> A, + arg -> + ScopedExpr -> Var -> n})]}, + type -> ScopedExpr -> Def' -> Agda.Primitive.Set}], + ScopedDecl -> + [RecDef -> + {name -> Record.R, + dataDefParams -> [UserWritten n, UserWritten A, UserWritten x], + decls -> + [ScopedDecl -> + [Field -> + {name -> Record.R.fieldX, + type -> ScopedExpr -> ScopedExpr -> Def' -> Record.Nat}], + ScopedDecl -> + [Field -> + {name -> Record.R.fieldY, + type -> + ScopedExpr -> + ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Var -> A, + arg -> ScopedExpr -> Var -> n}}], + ScopedDecl -> + [Field -> + {name -> Record.R.fieldZ, + type -> + ScopedExpr -> + ScopedExpr -> + ScopedExpr -> + App -> + {f -> ScopedExpr -> Var -> A, + arg -> ScopedExpr -> Proj -> Record.R.fieldX}}]]}]]]]}] \ No newline at end of file diff --git a/test/data/AST/Small b/test/data/AST/Small new file mode 100644 index 0000000..5651642 --- /dev/null +++ b/test/data/AST/Small @@ -0,0 +1,6 @@ +[ScopedDecl -> [Import -> Agda.Primitive], + Section -> + {moduleName -> Small, + genTel -> + GeneralizeTelescope {generalizeTelVars -> {}, generalizeTel -> []}, + decls -> []}] \ No newline at end of file diff --git a/test/data/AnonFun.agda b/test/data/AnonFun.agda new file mode 100644 index 0000000..c62b8a6 --- /dev/null +++ b/test/data/AnonFun.agda @@ -0,0 +1,4 @@ +module AnonFun where + +f : {A : Set} -> A -> A +f = \where x -> x diff --git a/test/data/Indexer/Basic.agda b/test/data/Indexer/Basic.agda new file mode 100644 index 0000000..3ddbb80 --- /dev/null +++ b/test/data/Indexer/Basic.agda @@ -0,0 +1,54 @@ +module Basic where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +one : Nat +one = suc zero + +two : Nat +two = suc one + +data Test : Set where + test : Test + +data Test' : Set where + test : Test' + +hello : Test +hello = test + +data Empty : Set where + +Not : Set -> Set +Not A = A -> Empty + +Goodbye : Set +Goodbye = Not Test + +postulate A : Test -> Set + +testId : Test -> Test +testId test = test + +id : {A : Set} -> A -> A +id = \where x -> x + +id' : {A : Set} -> A -> A +id' = \x -> let x = x in x + +id'' : {A : Set} -> A -> A +id'' {A = A} x = + let x = x + A = A + in x + +record World : Set where + field + north : Test + south : Test' + +earth : World +earth .World.north = test +earth .World.south = test diff --git a/test/data/Indexer/FunWithoutDeclOrDef.agda b/test/data/Indexer/FunWithoutDeclOrDef.agda new file mode 100644 index 0000000..86f00bd --- /dev/null +++ b/test/data/Indexer/FunWithoutDeclOrDef.agda @@ -0,0 +1,11 @@ +module FunWithoutDeclOrDef where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +-- No declaration +sucsuc = \n -> suc (suc n) + +-- No definition +sucsucsuc : Nat -> Nat diff --git a/test/data/Indexer/Module.agda b/test/data/Indexer/Module.agda new file mode 100644 index 0000000..817d050 --- /dev/null +++ b/test/data/Indexer/Module.agda @@ -0,0 +1,12 @@ +module Indexer.Module where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +module M where + f : Nat -> Nat + f n = n + + data N : Set where + n : N diff --git a/test/data/Indexer/Mutual.agda b/test/data/Indexer/Mutual.agda new file mode 100644 index 0000000..68f4f07 --- /dev/null +++ b/test/data/Indexer/Mutual.agda @@ -0,0 +1,41 @@ +module Mutual where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +module Forward where + interleaved mutual + record MutualRecord (A : Set) (n : Nat) : Set + data MutualData : Set + data MutualData' (A : Set) : Nat -> Set + mutualFun : MutualRecord MutualData zero -> MutualRecord MutualData zero + + record MutualRecord A m where + constructor makeMutualRecord + field + mutFieldX : A + field mutFieldY : Nat + + data MutualData where + mutCtorX : MutualData + + data _ where + mutCtorX' : MutualData' A zero + mutCtorY : MutualData + + mutualFun x = x + +module Backward where + interleaved mutual + data MutualData where + mutCtorX : MutualData + + data MutualData' where + mutCtorX' : MutualData' A zero + + data MutualData where + mutCtorY : MutualData + + data MutualData : Set + data MutualData' (A : Set) : Nat -> Set diff --git a/test/data/Indexer/Record.agda b/test/data/Indexer/Record.agda new file mode 100644 index 0000000..3330b2c --- /dev/null +++ b/test/data/Indexer/Record.agda @@ -0,0 +1,12 @@ +module Record where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat + +record R (n : Nat) (A : Nat -> Set) (x : A n) : Set where + constructor makeR + field + fieldX : Nat + fieldY : A n + fieldZ : A fieldX diff --git a/test/data/Indexer/Small.agda b/test/data/Indexer/Small.agda new file mode 100644 index 0000000..56db13e --- /dev/null +++ b/test/data/Indexer/Small.agda @@ -0,0 +1 @@ +module Small where \ No newline at end of file diff --git a/test/data/libs/no-deps/no-deps.agda-lib b/test/data/libs/no-deps/no-deps.agda-lib new file mode 100644 index 0000000..9970791 --- /dev/null +++ b/test/data/libs/no-deps/no-deps.agda-lib @@ -0,0 +1,2 @@ +name: no-deps +include: src diff --git a/test/data/libs/no-deps/src/Constants.agda b/test/data/libs/no-deps/src/Constants.agda new file mode 100644 index 0000000..699e243 --- /dev/null +++ b/test/data/libs/no-deps/src/Constants.agda @@ -0,0 +1,9 @@ +module Constants where + +open import Data.Nat + +one : Nat +one = suc zero + +two : Nat +two = suc one diff --git a/test/data/libs/no-deps/src/Data/Nat.agda b/test/data/libs/no-deps/src/Data/Nat.agda new file mode 100644 index 0000000..9ee2cba --- /dev/null +++ b/test/data/libs/no-deps/src/Data/Nat.agda @@ -0,0 +1,5 @@ +module Data.Nat where + +data Nat : Set where + zero : Nat + suc : Nat -> Nat diff --git a/test/data/test.agda-lib b/test/data/test.agda-lib new file mode 100644 index 0000000..33f7e30 --- /dev/null +++ b/test/data/test.agda-lib @@ -0,0 +1,2 @@ +name: test +include: . \ No newline at end of file