Skip to content

Commit 7ee1627

Browse files
nvarnernvarner
committed
Split AgdaLib into AgdaProject and AgdaLib
1 parent 5bfd102 commit 7ee1627

File tree

15 files changed

+214
-111
lines changed

15 files changed

+214
-111
lines changed

‎agda-language-server.cabal‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,7 @@ library
8181
Render.Utils
8282
Server
8383
Server.AgdaLibResolver
84+
Server.AgdaProjectResolver
8485
Server.CommandController
8586
Server.Filesystem
8687
Server.Handler
@@ -89,6 +90,7 @@ library
8990
Server.Model
9091
Server.Model.AgdaFile
9192
Server.Model.AgdaLib
93+
Server.Model.AgdaProject
9294
Server.Model.Handler
9395
Server.Model.Monad
9496
Server.Model.Symbol
@@ -241,6 +243,7 @@ test-suite als-test
241243
Render.Utils
242244
Server
243245
Server.AgdaLibResolver
246+
Server.AgdaProjectResolver
244247
Server.CommandController
245248
Server.Filesystem
246249
Server.Handler
@@ -249,6 +252,7 @@ test-suite als-test
249252
Server.Model
250253
Server.Model.AgdaFile
251254
Server.Model.AgdaLib
255+
Server.Model.AgdaProject
252256
Server.Model.Handler
253257
Server.Model.Monad
254258
Server.Model.Symbol

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidAbsolutePath)
3030
import qualified Language.LSP.Server as LSP
3131
import qualified Language.LSP.VFS as VFS
3232
import Server.Model.AgdaLib (agdaLibToFile)
33-
import Server.Model.Monad (MonadAgdaLib (askAgdaLib))
33+
import Server.Model.Monad (MonadAgdaProject, askAgdaLib)
3434

3535
data VSourceFile = VSourceFile
3636
{ vSrcFileSrcFile :: SourceFile,
@@ -76,7 +76,7 @@ vSrcFromUri normUri file = do
7676
#endif
7777

7878
parseSourceFromContents ::
79-
(TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) =>
79+
(TCM.MonadTrace m, MonadAgdaProject m) =>
8080
LSP.NormalizedUri ->
8181
SourceFile ->
8282
Text.Text ->
@@ -113,6 +113,6 @@ parseSourceFromContents srcUri srcFile contentsStrict = do
113113
}
114114

115115
-- | Based on @parseSource@
116-
parseVSource :: (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) => VSourceFile -> m Imp.Source
116+
parseVSource :: (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaProject m) => VSourceFile -> m Imp.Source
117117
parseVSource (VSourceFile srcFile uri vFile) =
118118
parseSourceFromContents uri srcFile (VFS.virtualFileText vFile)

‎src/Agda/TypeChecking/Monad/Options/More.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -12,19 +12,19 @@ import Control.Monad.IO.Class (liftIO)
1212
import Language.LSP.Protocol.Types.Uri.More (uriToPossiblyInvalidFilePath)
1313
import qualified Server.Filesystem as FS
1414
import Server.Model.AgdaLib (AgdaLib, agdaLibDependencies, agdaLibIncludes)
15-
import Server.Model.Monad (MonadAgdaLib (askAgdaLib))
15+
import Server.Model.Monad (MonadAgdaProject, askAgdaLib)
1616
import System.Directory (getCurrentDirectory)
1717

1818
setCommandLineOptionsByLib ::
19-
(MonadTCM m, MonadAgdaLib m) =>
19+
(MonadTCM m, MonadAgdaProject m) =>
2020
CommandLineOptions ->
2121
m ()
2222
setCommandLineOptionsByLib opts = do
2323
root <- liftIO (absolute =<< getCurrentDirectory)
2424
setCommandLineOptionsByLib' root opts
2525

2626
setCommandLineOptionsByLib' ::
27-
(MonadTCM m, MonadAgdaLib m) =>
27+
(MonadTCM m, MonadAgdaProject m) =>
2828
AbsolutePath ->
2929
CommandLineOptions ->
3030
m ()
@@ -41,7 +41,7 @@ setCommandLineOptionsByLib' root opts = do
4141
TCM.liftTCM updateBenchmarkingStatus
4242

4343
setLibraryPathsByLib ::
44-
(MonadTCM m, MonadAgdaLib m) =>
44+
(MonadTCM m, MonadAgdaProject m) =>
4545
CommandLineOptions ->
4646
m CommandLineOptions
4747
setLibraryPathsByLib o = do

‎src/Indexer.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,9 @@ import Indexer.Indexer (indexAst)
2323
import Indexer.Monad (execIndexerM)
2424
import Indexer.Postprocess (postprocess)
2525
import Server.Model.AgdaFile (AgdaFile)
26-
import Server.Model.Monad (WithAgdaLibM)
26+
import Server.Model.Monad (WithAgdaProjectM)
2727

28-
usingSrcAsCurrent :: Imp.Source -> WithAgdaLibM a -> WithAgdaLibM a
28+
usingSrcAsCurrent :: Imp.Source -> WithAgdaProjectM a -> WithAgdaProjectM a
2929
usingSrcAsCurrent src x = do
3030
TCM.liftTCM TCM.resetState
3131

@@ -43,7 +43,7 @@ usingSrcAsCurrent src x = do
4343
TCM.localTC (\e -> e {TCM.envCurrentPath = Just (srcFilePath $ Imp.srcOrigin src)}) x
4444
#endif
4545

46-
withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaLibM a) -> WithAgdaLibM a
46+
withAstFor :: Imp.Source -> (TopLevelInfo -> WithAgdaProjectM a) -> WithAgdaProjectM a
4747
withAstFor src f = usingSrcAsCurrent src $ do
4848
#if MIN_VERSION_Agda(2,8,0)
4949
let srcFile = Imp.srcOrigin src
@@ -60,7 +60,7 @@ withAstFor src f = usingSrcAsCurrent src $ do
6060

6161
indexFile ::
6262
Imp.Source ->
63-
WithAgdaLibM AgdaFile
63+
WithAgdaProjectM AgdaFile
6464
indexFile src = withAstFor src $ \ast -> execIndexerM $ do
6565
indexAst ast
6666
postprocess

‎src/Indexer/Monad.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ import Control.Monad.Trans (lift)
4343
import Data.Map (Map)
4444
import qualified Data.Map as Map
4545
import Server.Model.AgdaFile (AgdaFile, emptyAgdaFile, insertRef, insertSymbolInfo)
46-
import Server.Model.Monad (WithAgdaLibM)
46+
import Server.Model.Monad (WithAgdaProjectM)
4747
import Server.Model.Symbol (Ref (Ref), RefKind (..), SymbolInfo (..), SymbolKind (..))
4848

4949
data NamedArgUsage = NamedArgUsage
@@ -99,9 +99,9 @@ initEnv = do
9999
dataRecordParams <- liftIO $ newIORef mempty
100100
return $ Env agdaFile parent DeclBinding paramNames namedArgUsages dataRecordParams
101101

102-
type IndexerM = ReaderT Env WithAgdaLibM
102+
type IndexerM = ReaderT Env WithAgdaProjectM
103103

104-
execIndexerM :: IndexerM a -> WithAgdaLibM AgdaFile
104+
execIndexerM :: IndexerM a -> WithAgdaProjectM AgdaFile
105105
execIndexerM x = do
106106
env <- initEnv
107107
_ <- runReaderT x env
@@ -247,7 +247,7 @@ class TypeLike t where
247247
-- However, strings do lose semantic information otherwise available to us,
248248
-- so this representation may be switched in the future if that information is
249249
-- needed.
250-
toTypeString :: t -> WithAgdaLibM (Maybe String)
250+
toTypeString :: t -> WithAgdaProjectM (Maybe String)
251251

252252
instance (TypeLike t) => TypeLike (Maybe t) where
253253
toTypeString = maybe (return Nothing) toTypeString

‎src/Server/AgdaProjectResolver.hs‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
module Server.AgdaProjectResolver (findAgdaProject) where
2+
3+
import Monad (ServerM, askFilesystemProvider, askModel, modifyModel)
4+
import Server.AgdaLibResolver (findAgdaLib)
5+
import qualified Server.Filesystem as FS
6+
import qualified Server.Model as Model
7+
import Server.Model.AgdaProject (AgdaProject)
8+
import qualified Server.Model.AgdaProject as AgdaProject
9+
10+
-- | Find cached 'AgdaProject', or else make one from @.agda-lib@ files on the
11+
-- file system, or else provide a default
12+
findAgdaProject :: (FS.IsFileId f) => f -> ServerM AgdaProject
13+
findAgdaProject isFileId = do
14+
let fileId = FS.toFileId isFileId
15+
let uri = FS.fileIdToUri fileId
16+
model <- askModel
17+
case Model.getKnownAgdaProject uri model of
18+
Just project -> return project
19+
Nothing -> do
20+
lib <- findAgdaLib fileId
21+
project <- AgdaProject.new lib
22+
modifyModel $ Model.withAgdaProject project
23+
return project

‎src/Server/Model.hs‎

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,16 @@ module Server.Model
22
( Model (Model),
33
empty,
44
getKnownAgdaLib,
5+
getKnownAgdaProject,
56
withAgdaLib,
7+
withAgdaProject,
68
getAgdaFile,
79
setAgdaFile,
810
deleteAgdaFile,
911
)
1012
where
1113

12-
import Agda.Utils.Lens (Lens', over)
14+
import Agda.Utils.Lens (Lens', over, (^.))
1315
import Control.Monad.IO.Class (MonadIO)
1416
import Data.Foldable (find)
1517
import Data.Functor ((<&>))
@@ -18,27 +20,41 @@ import qualified Data.Map as Map
1820
import qualified Language.LSP.Protocol.Types as LSP
1921
import Server.Model.AgdaFile (AgdaFile)
2022
import Server.Model.AgdaLib (AgdaLib, initAgdaLib, isAgdaLibForUri)
23+
import Server.Model.AgdaProject (AgdaProject)
24+
import qualified Server.Model.AgdaProject as AgdaProject
2125

2226
data Model = Model
23-
{ _modelAgdaLibs :: !([AgdaLib]),
27+
{ _modelAgdaLibs :: ![AgdaLib],
28+
_modelAgdaProjects :: ![AgdaProject],
2429
_modelAgdaFiles :: !(Map LSP.NormalizedUri AgdaFile)
2530
}
2631

2732
empty :: Model
28-
empty = Model [] Map.empty
33+
empty = Model [] [] Map.empty
2934

3035
agdaLibs :: Lens' Model [AgdaLib]
3136
agdaLibs f a = f (_modelAgdaLibs a) <&> \x -> a {_modelAgdaLibs = x}
3237

38+
agdaProjects :: Lens' Model [AgdaProject]
39+
agdaProjects f a = f (_modelAgdaProjects a) <&> \x -> a {_modelAgdaProjects = x}
40+
3341
agdaFiles :: Lens' Model (Map LSP.NormalizedUri AgdaFile)
3442
agdaFiles f a = f (_modelAgdaFiles a) <&> \x -> a {_modelAgdaFiles = x}
3543

3644
getKnownAgdaLib :: LSP.NormalizedUri -> Model -> Maybe AgdaLib
37-
getKnownAgdaLib uri = find (`isAgdaLibForUri` uri) . _modelAgdaLibs
45+
getKnownAgdaLib uri model = find (`isAgdaLibForUri` uri) $ model ^. agdaLibs
46+
47+
getKnownAgdaProject :: LSP.NormalizedUri -> Model -> Maybe AgdaProject
48+
getKnownAgdaProject uri model =
49+
find ((`isAgdaLibForUri` uri) . (^. AgdaProject.agdaLib)) $ model ^. agdaProjects
3850

3951
-- | Add an 'AgdaLib' to the model
4052
withAgdaLib :: AgdaLib -> Model -> Model
41-
withAgdaLib lib model = model {_modelAgdaLibs = lib : _modelAgdaLibs model}
53+
withAgdaLib lib = over agdaLibs (lib :)
54+
55+
-- | Add an 'AgdaProject' to the model
56+
withAgdaProject :: AgdaProject -> Model -> Model
57+
withAgdaProject project = over agdaProjects (project :)
4258

4359
getAgdaFile :: LSP.NormalizedUri -> Model -> Maybe AgdaFile
4460
getAgdaFile uri = Map.lookup uri . _modelAgdaFiles

‎src/Server/Model/AgdaLib.hs‎

Lines changed: 1 addition & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,6 @@ module Server.Model.AgdaLib
77
agdaLibName,
88
agdaLibIncludes,
99
agdaLibDependencies,
10-
agdaLibTcStateRef,
11-
agdaLibTcEnv,
1210
agdaLibOrigin,
1311
isAgdaLibForUri,
1412
agdaLibFromFile,
@@ -49,8 +47,6 @@ data AgdaLib = AgdaLib
4947
_agdaLibIncludes :: ![FS.FileId],
5048
_agdaLibOptionsPragma :: !OptionsPragma,
5149
_agdaLibDependencies :: ![LibName],
52-
_agdaLibTcStateRef :: !(IORef TCM.TCState),
53-
_agdaLibTcEnv :: !TCM.TCEnv,
5450
_agdaLibOrigin :: !AgdaLibOrigin
5551
}
5652

@@ -76,7 +72,7 @@ initAgdaLibWithOrigin origin = do
7672
tcStateRef <- liftIO $ newIORef tcState'
7773
let tcEnv = TCM.initEnv
7874
let optionsPragma = OptionsPragma [] empty
79-
return $ AgdaLib libName [] optionsPragma [] tcStateRef tcEnv origin
75+
return $ AgdaLib libName [] optionsPragma [] origin
8076

8177
initAgdaLib :: (MonadIO m) => m AgdaLib
8278
initAgdaLib = initAgdaLibWithOrigin Defaulted
@@ -93,12 +89,6 @@ agdaLibOptionsPragma f a = f (_agdaLibOptionsPragma a) <&> \x -> a {_agdaLibOpti
9389
agdaLibDependencies :: Lens' AgdaLib [LibName]
9490
agdaLibDependencies f a = f (_agdaLibDependencies a) <&> \x -> a {_agdaLibDependencies = x}
9591

96-
agdaLibTcStateRef :: Lens' AgdaLib (IORef TCM.TCState)
97-
agdaLibTcStateRef f a = f (_agdaLibTcStateRef a) <&> \x -> a {_agdaLibTcStateRef = x}
98-
99-
agdaLibTcEnv :: Lens' AgdaLib TCM.TCEnv
100-
agdaLibTcEnv f a = f (_agdaLibTcEnv a) <&> \x -> a {_agdaLibTcEnv = x}
101-
10292
agdaLibOrigin :: Lens' AgdaLib AgdaLibOrigin
10393
agdaLibOrigin f a = f (_agdaLibOrigin a) <&> \x -> a {_agdaLibOrigin = x}
10494

‎src/Server/Model/AgdaProject.hs‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
{-# LANGUAGE CPP #-}
2+
3+
module Server.Model.AgdaProject
4+
( AgdaProject,
5+
new,
6+
agdaLib,
7+
tcStateRef,
8+
tcEnv,
9+
)
10+
where
11+
12+
import qualified Agda.TypeChecking.Monad as TCM
13+
import Agda.Utils.IORef (IORef, newIORef)
14+
import Agda.Utils.Lens (Lens', (<&>), (^.))
15+
import Control.Monad.IO.Class (MonadIO, liftIO)
16+
import Server.Model.AgdaLib (AgdaLib, initAgdaLib)
17+
import Agda.Syntax.Common.Pretty (Pretty, pretty, text, (<+>))
18+
19+
data AgdaProject = AgdaProject
20+
{
21+
_agdaLib :: !AgdaLib,
22+
_tcStateRef :: !(IORef TCM.TCState),
23+
_tcEnv :: !TCM.TCEnv
24+
}
25+
26+
instance Pretty AgdaProject where
27+
pretty agdaProject =
28+
text "AgdaProject"
29+
<+> pretty (agdaProject ^. agdaLib)
30+
31+
new :: (MonadIO m) => AgdaLib -> m AgdaProject
32+
new agdaLib = do
33+
#if MIN_VERSION_Agda(2,8,0)
34+
tcState <- liftIO TCM.initStateIO
35+
#else
36+
let tcState = TCM.initState
37+
#endif
38+
let persistentState = TCM.stPersistentState tcState
39+
-- Prevent Agda from writing to standard output by default. LSP likes to use
40+
-- it, so Agda shouldn't try to use it too.
41+
let tcState' = tcState { TCM.stPersistentState = persistentState { TCM.stInteractionOutputCallback = \_ -> return () } }
42+
tcStateRef <- liftIO $ newIORef tcState'
43+
let tcEnv = TCM.initEnv
44+
return $ AgdaProject agdaLib tcStateRef tcEnv
45+
46+
agdaLib :: Lens' AgdaProject AgdaLib
47+
agdaLib f a = f (_agdaLib a) <&> \x -> a {_agdaLib = x}
48+
49+
tcStateRef :: Lens' AgdaProject (IORef TCM.TCState)
50+
tcStateRef f a = f (_tcStateRef a) <&> \x -> a {_tcStateRef = x}
51+
52+
tcEnv :: Lens' AgdaProject TCM.TCEnv
53+
tcEnv f a = f (_tcEnv a) <&> \x -> a {_tcEnv = x}

‎src/Server/Model/Handler.hs‎

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,9 @@ import qualified Language.LSP.Protocol.Types as LSP
2727
import qualified Language.LSP.Server as LSP
2828
import Monad (ServerM, askModel, catchTCError)
2929
import Server.AgdaLibResolver (findAgdaLib)
30+
import Server.AgdaProjectResolver (findAgdaProject)
3031
import qualified Server.Model as Model
31-
import Server.Model.Monad (WithAgdaFileM, WithAgdaLibM, runWithAgdaFileT, runWithAgdaLibT)
32+
import Server.Model.Monad (WithAgdaFileM, WithAgdaProjectM, runWithAgdaFileT, runWithAgdaProjectT)
3233
import qualified Server.Model.Monad as LSP
3334
#if MIN_VERSION_Agda(2,7,0)
3435
#else
@@ -42,7 +43,7 @@ tryTC handler = (Right <$> handler) `catchTCError` (return . Left)
4243

4344
type NotificationHandlerWithAgdaLib
4445
(m :: LSP.Method LSP.ClientToServer LSP.Notification) =
45-
LSP.NormalizedUri -> LSP.TNotificationMessage m -> WithAgdaLibM ()
46+
LSP.NormalizedUri -> LSP.TNotificationMessage m -> WithAgdaProjectM ()
4647

4748
notificationHandlerWithAgdaLib ::
4849
(LSP.HasTextDocument (LSP.MessageParams m) textdoc, LSP.HasUri textdoc LSP.Uri) =>
@@ -60,13 +61,13 @@ takeOverNotificationHandlerWithAgdaLib ::
6061
takeOverNotificationHandlerWithAgdaLib notification handlerWithAgdaLib = do
6162
let uri = notification ^. LSP.params . LSP.textDocument . LSP.uri
6263
normUri = LSP.toNormalizedUri uri
63-
agdaLib <- findAgdaLib normUri
64-
lift $ LSP.sendNotification LSP.SMethod_WindowLogMessage $ LSP.LogMessageParams LSP.MessageType_Info $ Text.pack $ prettyShow agdaLib
64+
agdaProject <- findAgdaProject uri
65+
lift $ LSP.sendNotification LSP.SMethod_WindowLogMessage $ LSP.LogMessageParams LSP.MessageType_Info $ Text.pack $ prettyShow agdaProject
6566

66-
let notificationHandler = runWithAgdaLibT agdaLib . handlerWithAgdaLib normUri
67+
let notificationHandler = runWithAgdaProjectT agdaProject . handlerWithAgdaLib normUri
6768
let handler = tryTC $ notificationHandler notification
6869

69-
let onErr = \err -> runWithAgdaLibT agdaLib $ do
70+
let onErr = \err -> runWithAgdaProjectT agdaProject $ do
7071
message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err)
7172
lift $ LSP.sendNotification LSP.SMethod_WindowShowMessage $ LSP.ShowMessageParams LSP.MessageType_Error message
7273
lift $ LSP.sendNotification LSP.SMethod_WindowLogMessage $ LSP.LogMessageParams LSP.MessageType_Error message
@@ -100,11 +101,11 @@ requestHandlerWithAgdaFile m handlerWithAgdaFile = LSP.requestHandler m $ \req r
100101
let message = "Request for unknown Agda file at URI: " <> LSP.getUri uri
101102
responder $ Left $ LSP.TResponseError (LSP.InR LSP.ErrorCodes_InvalidParams) message Nothing
102103
Just agdaFile -> do
103-
agdaLib <- findAgdaLib normUri
104+
agdaProject <- findAgdaProject uri
104105
let responderWithAgdaFile = lift . responder
105-
let handler = tryTC $ runWithAgdaFileT agdaLib agdaFile $ handlerWithAgdaFile req responderWithAgdaFile
106+
let handler = tryTC $ runWithAgdaFileT agdaProject agdaFile $ handlerWithAgdaFile req responderWithAgdaFile
106107

107-
let onErr = \err -> runWithAgdaFileT agdaLib agdaFile $ do
108+
let onErr = \err -> runWithAgdaFileT agdaProject agdaFile $ do
108109
message <- Text.pack . prettyShow <$> TCM.liftTCM (TCM.prettyTCM err)
109110
lift $ responder $ Left $ LSP.TResponseError (LSP.InL LSP.LSPErrorCodes_RequestFailed) message Nothing
110111

0 commit comments

Comments
 (0)