Skip to content

Commit 3707390

Browse files
nvarnernvarner
committed
respond to files opening, closing, and saving
1 parent 238a1c7 commit 3707390

File tree

13 files changed

+266
-33
lines changed

13 files changed

+266
-33
lines changed

‎agda-language-server.cabal‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ library
5050
Agda
5151
Agda.Convert
5252
Agda.Interaction.Imports.More
53+
Agda.Interaction.Library.More
5354
Agda.IR
5455
Agda.Parser
5556
Agda.Position
@@ -79,6 +80,7 @@ library
7980
Server.CommandController
8081
Server.Handler
8182
Server.Handler.TextDocument.DocumentSymbol
83+
Server.Handler.TextDocument.FileManagement
8284
Server.Model
8385
Server.Model.AgdaFile
8486
Server.Model.AgdaLib
@@ -194,6 +196,7 @@ test-suite als-test
194196
Agda
195197
Agda.Convert
196198
Agda.Interaction.Imports.More
199+
Agda.Interaction.Library.More
197200
Agda.IR
198201
Agda.Parser
199202
Agda.Position
@@ -223,6 +226,7 @@ test-suite als-test
223226
Server.CommandController
224227
Server.Handler
225228
Server.Handler.TextDocument.DocumentSymbol
229+
Server.Handler.TextDocument.FileManagement
226230
Server.Model
227231
Server.Model.AgdaFile
228232
Server.Model.AgdaLib

‎src/Agda/Interaction/Imports/More.hs‎

Lines changed: 40 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,55 @@
1-
-- | This module reexports unexported functions
21
module Agda.Interaction.Imports.More
3-
( setOptionsFromSourcePragmas,
2+
( parseVirtualSource,
3+
setOptionsFromSourcePragmas,
44
checkModuleName',
55
)
66
where
77

8-
import Agda.Interaction.FindFile (SourceFile, checkModuleName)
9-
import Agda.Interaction.Imports (Source)
8+
import Agda.Interaction.FindFile (SourceFile (SourceFile), checkModuleName, moduleName)
9+
import Agda.Interaction.Imports (Source (..))
1010
import qualified Agda.Interaction.Imports as Imp
1111
import Agda.Interaction.Library (OptionsPragma (..), _libPragmas)
1212
import Agda.Syntax.Common (TopLevelModuleName')
1313
import qualified Agda.Syntax.Concrete as C
14-
import Agda.Syntax.Position (Range)
14+
import Agda.Syntax.Parser (moduleParser, parseFile)
15+
import Agda.Syntax.Position (Range, mkRangeFile)
1516
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
1617
import Agda.TypeChecking.Monad (Interface, TCM, checkAndSetOptionsFromPragma, setCurrentRange, setOptionsFromPragma, setTCLens, stPragmaOptions, useTC)
18+
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
19+
import Agda.TypeChecking.Warnings (runPM)
1720
import Agda.Utils.Monad (bracket_)
21+
import qualified Data.Text.Lazy as TL
22+
23+
-- | Parse a source file without talking to the filesystem
24+
parseVirtualSource ::
25+
-- | Logical path of the source file. Used in ranges, not filesystem access.
26+
SourceFile ->
27+
-- | Logical contents of the source file
28+
TL.Text ->
29+
TCM Imp.Source
30+
parseVirtualSource sourceFile@(SourceFile f) source = Bench.billTo [Bench.Parsing] $ do
31+
let rf0 = mkRangeFile f Nothing
32+
((parsedMod0, _attrs), _fileType) <- runPM $ parseFile moduleParser rf0 $ TL.unpack source
33+
parsedModName <- moduleName f parsedMod0
34+
35+
let rf = mkRangeFile f (Just parsedModName)
36+
((parsedMod, attrs), fileType) <- runPM $ parseFile moduleParser rf $ TL.unpack source
37+
38+
-- TODO: handle libs properly
39+
let libs = []
40+
41+
return
42+
Source
43+
{ srcText = source,
44+
srcFileType = fileType,
45+
srcOrigin = sourceFile,
46+
srcModule = parsedMod,
47+
srcModuleName = parsedModName,
48+
srcProjectLibs = libs,
49+
srcAttributes = attrs
50+
}
51+
52+
-- Unexported Agda functions
1853

1954
srcDefaultPragmas :: Imp.Source -> [OptionsPragma]
2055
srcDefaultPragmas src = map _libPragmas (Imp.srcProjectLibs src)

‎src/Agda/Interaction/Library/More.hs‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
module Agda.Interaction.Library.More
2+
( runLibErrorIO,
3+
tryRunLibM,
4+
)
5+
where
6+
7+
import Agda.Interaction.Library (LibM)
8+
import Agda.Interaction.Library.Base (LibErrorIO)
9+
import Agda.Utils.Either (maybeRight)
10+
import Control.Category ((>>>))
11+
import Control.Monad.Except (runExceptT)
12+
import Control.Monad.IO.Class (MonadIO, liftIO)
13+
import Control.Monad.State.Lazy (evalStateT)
14+
import Control.Monad.Writer.Lazy (runWriterT)
15+
import qualified Data.Map as Map
16+
17+
runLibErrorIO :: (MonadIO m) => LibErrorIO a -> m a
18+
runLibErrorIO =
19+
runWriterT
20+
>>> flip evalStateT (Map.empty, Map.empty)
21+
>>> fmap fst
22+
>>> liftIO
23+
24+
tryRunLibM :: (MonadIO m) => LibM a -> m (Maybe a)
25+
tryRunLibM =
26+
runExceptT
27+
>>> runWriterT
28+
>>> flip evalStateT (Map.empty, Map.empty)
29+
>>> fmap (fst >>> maybeRight)
30+
>>> liftIO

‎src/Language/LSP/Protocol/Types/Uri/More.hs‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,16 @@
11
module Language.LSP.Protocol.Types.Uri.More
22
( getNormalizedUri,
33
isUriAncestorOf,
4+
uriToPossiblyInvalidAbsolutePath,
45
)
56
where
67

8+
import Agda.Utils.FileName (AbsolutePath (AbsolutePath), absolute)
9+
import Agda.Utils.Maybe (fromMaybe)
10+
import Control.Monad.IO.Class (MonadIO, liftIO)
711
import Data.Text (Text)
812
import qualified Data.Text as Text
13+
import Language.LSP.Protocol.Types (uriToFilePath)
914
import qualified Language.LSP.Protocol.Types as LSP
1015

1116
getNormalizedUri :: LSP.NormalizedUri -> Text
@@ -18,3 +23,12 @@ getNormalizedUri = LSP.getUri . LSP.fromNormalizedUri
1823
isUriAncestorOf :: LSP.NormalizedUri -> LSP.NormalizedUri -> Bool
1924
isUriAncestorOf ancestor descendant =
2025
getNormalizedUri ancestor `Text.isPrefixOf` getNormalizedUri descendant
26+
27+
uriToPossiblyInvalidAbsolutePath :: (MonadIO m) => LSP.NormalizedUri -> m AbsolutePath
28+
uriToPossiblyInvalidAbsolutePath uri = do
29+
case LSP.uriToFilePath $ LSP.fromNormalizedUri uri of
30+
Just path -> liftIO $ absolute path
31+
Nothing -> return $ uriToInvalidAbsolutePath uri
32+
33+
uriToInvalidAbsolutePath :: LSP.NormalizedUri -> AbsolutePath
34+
uriToInvalidAbsolutePath = AbsolutePath . getNormalizedUri

‎src/Monad.hs‎

Lines changed: 28 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ module Monad where
66

77
import Agda.IR
88
import Agda.Interaction.Base (IOTCM)
9+
import Agda.Interaction.Library (findProjectRoot)
10+
import Agda.Interaction.Library.More (tryRunLibM)
911
import Agda.TypeChecking.Monad (TCMT)
1012
import Agda.Utils.Lens (Lens', (^.))
1113
import Control.Concurrent
@@ -17,7 +19,7 @@ import Data.IORef
1719
readIORef,
1820
writeIORef,
1921
)
20-
import Data.Maybe (isJust)
22+
import Data.Maybe (fromMaybe, isJust)
2123
import Data.Text
2224
( Text,
2325
pack,
@@ -33,9 +35,10 @@ import Server.CommandController (CommandController)
3335
import qualified Server.CommandController as CommandController
3436
import Server.Model (Model)
3537
import qualified Server.Model as Model
36-
import Server.Model.AgdaLib (AgdaLib)
38+
import Server.Model.AgdaLib (AgdaLib, agdaLibFromFs, initAgdaLib)
3739
import Server.ResponseController (ResponseController)
3840
import qualified Server.ResponseController as ResponseController
41+
import System.FilePath (takeDirectory)
3942

4043
--------------------------------------------------------------------------------
4144

@@ -87,6 +90,29 @@ askModel = do
8790
modelVar <- asks envModel
8891
liftIO $ readIORef modelVar
8992

93+
modifyModel :: (MonadIO m) => (Model -> Model) -> ServerT m ()
94+
modifyModel f = do
95+
modelVar <- asks envModel
96+
liftIO $ modifyIORef' modelVar f
97+
98+
-- | Find cached 'AgdaLib', or else make one from @.agda-lib@ files on the file
99+
-- system, or else provide a default
100+
findAgdaLib :: (MonadIO m) => LSP.NormalizedUri -> ServerT m AgdaLib
101+
findAgdaLib uri = do
102+
model <- askModel
103+
case Model.getKnownAgdaLib uri model of
104+
Just lib -> return lib
105+
Nothing -> do
106+
lib <- case LSP.uriToFilePath $ LSP.fromNormalizedUri uri of
107+
Just path -> do
108+
lib <- agdaLibFromFs $ takeDirectory path
109+
case lib of
110+
Just lib -> return lib
111+
Nothing -> initAgdaLib
112+
Nothing -> initAgdaLib
113+
modifyModel $ Model.withAgdaLib lib
114+
return lib
115+
90116
-- | Provider
91117
provideCommand :: (Monad m, MonadIO m) => IOTCM -> ServerT m ()
92118
provideCommand iotcm = do

‎src/Server.hs‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ import qualified Server.Handler as Handler
2929
import Switchboard (Switchboard, agdaCustomMethod)
3030
import qualified Switchboard
3131
import Server.Handler.TextDocument.DocumentSymbol (documentSymbolHandler)
32+
import Server.Handler.TextDocument.FileManagement (didOpenHandler, didCloseHandler, didSaveHandler)
3233

3334
#if defined(wasm32_HOST_ARCH)
3435
import Agda.Utils.IO (catchIO)
@@ -129,11 +130,11 @@ handlers =
129130
-- `workspace/didChangeConfiguration`
130131
notificationHandler SMethod_WorkspaceDidChangeConfiguration $ \_notification -> return (),
131132
-- `textDocument/didOpen`
132-
notificationHandler SMethod_TextDocumentDidOpen $ \_notification -> return (),
133+
didOpenHandler,
133134
-- `textDocument/didClose`
134-
notificationHandler SMethod_TextDocumentDidClose $ \_notification -> return (),
135+
didCloseHandler,
135136
-- `textDocument/didChange`
136137
notificationHandler SMethod_TextDocumentDidChange $ \_notification -> return (),
137138
-- `textDocument/didSave`
138-
notificationHandler SMethod_TextDocumentDidSave $ \_notification -> return ()
139-
]
139+
didSaveHandler
140+
]

‎src/Server/Handler/TextDocument/DocumentSymbol.hs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,11 @@ import qualified Language.LSP.Protocol.Types as LSP
1313
import qualified Language.LSP.Server as LSP
1414
import Monad (ServerM)
1515
import Server.Model.AgdaFile (AgdaFile, agdaFileSymbols, defNameRange, symbolByName, symbolsByParent)
16-
import Server.Model.Monad (MonadAgdaFile (askAgdaFile), useAgdaFile, withAgdaFile)
16+
import Server.Model.Monad (MonadAgdaFile (askAgdaFile), requestHandlerWithAgdaFile, useAgdaFile)
1717
import Server.Model.Symbol (SymbolInfo (symbolName), lspSymbolKind, symbolShortName, symbolType)
1818

1919
documentSymbolHandler :: LSP.Handlers ServerM
20-
documentSymbolHandler = withAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do
20+
documentSymbolHandler = requestHandlerWithAgdaFile LSP.SMethod_TextDocumentDocumentSymbol $ \req responder -> do
2121
file <- askAgdaFile
2222
let symbols = symbolsByParent file
2323
let topLevelNames = fromMaybe [] $ Map.lookup Nothing symbols

‎src/Server/Handler/TextDocument/FileManagement.hs‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
module Server.Handler.TextDocument.FileManagement
2+
( didOpenHandler,
3+
didCloseHandler,
4+
didSaveHandler,
5+
)
6+
where
7+
8+
import Agda.Interaction.FindFile (SourceFile (SourceFile))
9+
import qualified Agda.Interaction.Imports.More as Imp
10+
import Agda.TypeChecking.Monad (MonadTCM (liftTCM))
11+
import Agda.Utils.Lens ((^.))
12+
import Control.Monad.Trans (lift)
13+
import Data.Strict (Strict (toLazy))
14+
import Indexer (indexFile)
15+
import qualified Language.LSP.Protocol.Lens as LSP
16+
import qualified Language.LSP.Protocol.Message as LSP
17+
import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidAbsolutePath)
18+
import qualified Language.LSP.Server as LSP
19+
import qualified Language.LSP.Server as VFS
20+
import qualified Language.LSP.VFS as VFS
21+
import Monad (ServerM, modifyModel)
22+
import qualified Server.Model as Model
23+
import Server.Model.Monad (notificationHandlerWithAgdaLib)
24+
25+
didOpenHandler :: LSP.Handlers ServerM
26+
didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen $ \notification uri -> do
27+
sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri
28+
let sourceText = toLazy $ notification ^. LSP.params . LSP.textDocument . LSP.text
29+
src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText
30+
agdaFile <- indexFile src
31+
lift $ modifyModel $ Model.setAgdaFile uri agdaFile
32+
33+
didCloseHandler :: LSP.Handlers ServerM
34+
didCloseHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidClose $ \notification uri -> do
35+
lift $ modifyModel $ Model.deleteAgdaFile uri
36+
37+
didSaveHandler :: LSP.Handlers ServerM
38+
didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave $ \notification uri -> do
39+
sourceFile <- SourceFile <$> uriToPossiblyInvalidAbsolutePath uri
40+
virtualFile <- lift $ VFS.getVirtualFile uri
41+
case virtualFile of
42+
Nothing -> return ()
43+
Just virtualFile -> do
44+
let sourceText = toLazy $ VFS.virtualFileText virtualFile
45+
src <- liftTCM $ Imp.parseVirtualSource sourceFile sourceText
46+
agdaFile <- indexFile src
47+
lift $ modifyModel $ Model.setAgdaFile uri agdaFile

‎src/Server/Model.hs‎

Lines changed: 31 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,19 @@
1-
module Server.Model (Model (Model), empty, getKnownAgdaLib, getAgdaLib, getAgdaFile) where
1+
module Server.Model
2+
( Model (Model),
3+
empty,
4+
getKnownAgdaLib,
5+
getAgdaLib,
6+
withAgdaLib,
7+
getAgdaFile,
8+
setAgdaFile,
9+
deleteAgdaFile,
10+
)
11+
where
212

13+
import Agda.Utils.Lens (Lens', over)
314
import Control.Monad.IO.Class (MonadIO)
415
import Data.Foldable (find)
16+
import Data.Functor ((<&>))
517
import Data.Map (Map)
618
import qualified Data.Map as Map
719
import qualified Language.LSP.Protocol.Types as LSP
@@ -16,11 +28,29 @@ data Model = Model
1628
empty :: Model
1729
empty = Model [] Map.empty
1830

31+
agdaLibs :: Lens' Model [AgdaLib]
32+
agdaLibs f a = f (_modelAgdaLibs a) <&> \x -> a {_modelAgdaLibs = x}
33+
34+
agdaFiles :: Lens' Model (Map LSP.NormalizedUri AgdaFile)
35+
agdaFiles f a = f (_modelAgdaFiles a) <&> \x -> a {_modelAgdaFiles = x}
36+
1937
getKnownAgdaLib :: LSP.NormalizedUri -> Model -> Maybe AgdaLib
2038
getKnownAgdaLib uri = find (`isAgdaLibForUri` uri) . _modelAgdaLibs
2139

40+
-- | Get the Agda library for the given URI if known. Otherwise, get a generic
41+
-- default Agda library.
2242
getAgdaLib :: (MonadIO m) => LSP.NormalizedUri -> Model -> m AgdaLib
2343
getAgdaLib uri = maybe initAgdaLib return . getKnownAgdaLib uri
2444

45+
-- | Add an 'AgdaLib' to the model
46+
withAgdaLib :: AgdaLib -> Model -> Model
47+
withAgdaLib lib model = model {_modelAgdaLibs = lib : _modelAgdaLibs model}
48+
2549
getAgdaFile :: LSP.NormalizedUri -> Model -> Maybe AgdaFile
2650
getAgdaFile uri = Map.lookup uri . _modelAgdaFiles
51+
52+
setAgdaFile :: LSP.NormalizedUri -> AgdaFile -> Model -> Model
53+
setAgdaFile uri agdaFile = over agdaFiles $ Map.insert uri agdaFile
54+
55+
deleteAgdaFile :: LSP.NormalizedUri -> Model -> Model
56+
deleteAgdaFile uri = over agdaFiles $ Map.delete uri

0 commit comments

Comments
 (0)