better support for include paths

Author: nvarner

agda-language-server.cabal

@@ -56,6 +56,7 @@ library
       Agda.Parser
       Agda.Position
       Agda.Syntax.Abstract.More
+      Agda.TypeChecking.Monad.Options.More
       Control.Concurrent.SizedChan
       Indexer
       Indexer.Indexer
@@ -194,6 +195,7 @@ test-suite als-test
       Test.Model
       Test.ModelMonad
       Test.SrcLoc
+      Test.Uri
       Test.WASM
       TestData
       Agda
@@ -205,6 +207,7 @@ test-suite als-test
       Agda.Parser
       Agda.Position
       Agda.Syntax.Abstract.More
+      Agda.TypeChecking.Monad.Options.More
       Control.Concurrent.SizedChan
       Indexer
       Indexer.Indexer

src/Agda/Interaction/Imports/More.hs

@@ -22,6 +22,7 @@ import Agda.Interaction.FindFile (
 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 (
@@ -57,6 +58,7 @@ import Agda.Syntax.TopLevelModuleName (
     rawTopLevelModuleNameForModule,
 #endif
   )
+import Agda.Syntax.Common.Pretty (Pretty, pretty, text, prettyAssign, (<+>))
 import Agda.TypeChecking.Monad
   ( Interface,
     TCM,
@@ -92,8 +94,6 @@ import Control.Monad.Error.Class (
   )
 #if MIN_VERSION_Agda(2,8,0)
 import Agda.Utils.Singleton (singleton)
-#else
-import Agda.Syntax.Common.Pretty (pretty)
 #endif
 
 srcFilePath :: SourceFile -> TCM AbsolutePath
@@ -193,3 +193,11 @@ moduleName file parsedModule = Bench.billTo [Bench.ModuleName] $ do
             }
     else return raw
 #endif
+
+-- Orphan instances
+
+instance Pretty Imp.Source where
+  pretty src =
+    text "Source"
+      <+> pretty (Imp.srcModuleName src)
+      <+> pretty (Imp.srcProjectLibs src)

src/Agda/Interaction/Imports/Virtual.hs

@@ -19,6 +19,7 @@ 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
@@ -27,6 +28,8 @@ 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,
@@ -67,10 +70,10 @@ vSrcFromUri normUri file = do
 #endif
 
 -- | Based on @parseSource@
-parseVSource :: (TCM.MonadTCM m) => VSourceFile -> m Imp.Source
-parseVSource vSrcFile = TCM.liftTCM $ do
+parseVSource :: (TCM.MonadTCM m, TCM.MonadTrace m, MonadAgdaLib m) => VSourceFile -> m Imp.Source
+parseVSource vSrcFile = do
   let sourceFile = vSrcFileSrcFile vSrcFile
-  f <- vSrcFilePath vSrcFile
+  f <- TCM.liftTCM $ vSrcFilePath vSrcFile
 
   let rf0 = mkRangeFile f Nothing
   TCM.setCurrentRange (Imp.beginningOfFile rf0) $ do
@@ -79,15 +82,16 @@ parseVSource vSrcFile = TCM.liftTCM $ do
     let txt = Text.unpack sourceStrict
 
     parsedModName0 <-
-      Imp.moduleName f . fst . fst =<< do
-        Imp.runPMDropWarnings $ parseFile moduleParser rf0 txt
+      TCM.liftTCM $
+        Imp.moduleName f . fst . fst =<< do
+          Imp.runPMDropWarnings $ parseFile moduleParser rf0 txt
 
     let rf = mkRangeFile f $ Just parsedModName0
-    ((parsedMod, attrs), fileType) <- Imp.runPM $ parseFile moduleParser rf txt
-    parsedModName <- Imp.moduleName f parsedMod
+    ((parsedMod, attrs), fileType) <- TCM.liftTCM $ Imp.runPM $ parseFile moduleParser rf txt
+    parsedModName <- TCM.liftTCM $ Imp.moduleName f parsedMod
 
-    -- TODO: handle libs properly
-    let libs = []
+    agdaLib <- askAgdaLib
+    let libs = maybeToList $ agdaLibToFile (vSrcUri vSrcFile) agdaLib
 
     return
       Imp.Source

src/Agda/Interaction/Library/More.hs

@@ -9,15 +9,17 @@ module Agda.Interaction.Library.More
   )
 where
 
-import Agda.Interaction.Library (LibM)
-import Agda.Interaction.Library.Base (LibErrorIO)
+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
@@ -37,3 +39,10 @@ tryRunLibM =
     >>> flip evalStateT empty
     >>> fmap (fst >>> maybeRight)
     >>> liftIO
+
+instance Pretty AgdaLibFile where
+  pretty agdaLibFile =
+    text "AgdaLibFile"
+      <+> (pretty $ agdaLibFile ^. libName)
+      <+> (pretty $ agdaLibFile ^. libFile)
+      <+> (pretty $ agdaLibFile ^. libIncludes)

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

@@ -0,0 +1,58 @@
+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 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 <$> agdaLib ^. agdaLibIncludes
+      o {optIncludePaths = incs ++ optIncludePaths o, optLibraries = libs}

src/Indexer.hs

@@ -12,9 +12,12 @@ where
 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)
@@ -25,20 +28,24 @@ import Server.Model.Monad (WithAgdaLibM)
 usingSrcAsCurrent :: Imp.Source -> WithAgdaLibM a -> WithAgdaLibM a
 #if MIN_VERSION_Agda(2,8,0)
 usingSrcAsCurrent src x = do
-  TCM.liftTCM $
-    TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $
-      -- Now reset the options
-      TCM.setCommandLineOptions . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC
+  TCM.liftTCM $ Imp.setOptionsFromSourcePragmas True src
+
+  TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $
+    -- Now reset the options
+    setCommandLineOptionsByLib . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC
 
   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
+  TCM.localTC (\e -> e {TCM.envCurrentPath = Just (TCM.srcFileId $ Imp.srcOrigin src)}) $ do
+    TCM.liftTCM $ Imp.setOptionsFromSourcePragmas False src
+    -- includeDirs <- TCM.getIncludeDirs
+    -- _ <- TCM.liftTCM $ TCM.typeError $ TCM.InternalError $ prettyShow includeDirs
+    x
 #else
 usingSrcAsCurrent src x = do
-  TCM.liftTCM $
-    TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $
-      -- Now reset the options
-      TCM.setCommandLineOptions . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC
+  TCM.setCurrentRange (C.modPragmas . Imp.srcModule $ src) $
+    -- Now reset the options
+    setCommandLineOptionsByLib . TCM.stPersistentOptions . TCM.stPersistentState =<< TCM.getTC
 
   TCM.modifyTCLens TCM.stModuleToSource $ Map.insert (Imp.srcModuleName src) (srcFilePath $ Imp.srcOrigin src)
 

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

@@ -1,7 +1,9 @@
 module Language.LSP.Protocol.Types.Uri.More
   ( getNormalizedUri,
     isUriAncestorOf,
+    uriHeightAbove,
     uriToPossiblyInvalidAbsolutePath,
+    uriToPossiblyInvalidFilePath,
   )
 where
 
@@ -24,6 +26,40 @@ 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
+
 uriToPossiblyInvalidAbsolutePath :: (MonadIO m) => LSP.NormalizedUri -> m AbsolutePath
 uriToPossiblyInvalidAbsolutePath uri = do
   case LSP.uriToFilePath $ LSP.fromNormalizedUri uri of
@@ -32,3 +68,11 @@ uriToPossiblyInvalidAbsolutePath uri = do
 
 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

src/Server/Handler/TextDocument/FileManagement.hs

@@ -8,10 +8,12 @@ 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
@@ -30,7 +32,8 @@ didOpenHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidOpen
     Nothing -> return ()
     Just vfile -> do
       vSourceFile <- vSrcFromUri uri vfile
-      src <- liftTCM $ parseVSource vSourceFile
+      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
 
@@ -45,6 +48,7 @@ didSaveHandler = notificationHandlerWithAgdaLib LSP.SMethod_TextDocumentDidSave
     Nothing -> return ()
     Just vfile -> do
       vSourceFile <- vSrcFromUri uri vfile
-      src <- liftTCM $ parseVSource vSourceFile
+      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