content: ------------------------------------------------------------------------
  -- | Functions which map between module names and file names.
  --
  -- Note that file name lookups are cached in the 'TCState'. The code
  -- assumes that no Agda source files are added or removed from the
  -- include directories while the code is being type checked.
  ------------------------------------------------------------------------
  
  module Agda.Interaction.FindFile
    ( SourceFile(..), InterfaceFile(intFilePath)
    , toIFile, mkInterfaceFile
    , FindError(..), findErrorToTypeError
    , findFile, findFile', findFile'_, findFile''
    , findInterfaceFile', findInterfaceFile
    , checkModuleName
    , rootNameModule
    , replaceModuleExtension
    , dropAgdaExtension, hasAgdaExtension, stripAgdaExtension
    ) where
  
  import Prelude hiding (null)
  
  import Control.Monad
  import Control.Monad.Except
  import Control.Monad.State
  import Control.Monad.Trans
  import Data.Maybe (catMaybes, fromMaybe, isJust)
  import qualified Data.Map as Map
  import qualified Data.Text as T
  import System.FilePath
  
  import Agda.Interaction.Library ( findProjectRoot )
  
  import Agda.Syntax.Concrete
  import Agda.Syntax.Parser
  import Agda.Syntax.Parser.Literate (literateExtsShortList)
  import Agda.Syntax.Position
  import Agda.Syntax.TopLevelModuleName
  
  import Agda.TypeChecking.Monad.Base
  import Agda.TypeChecking.Monad.Benchmark (billTo)
  import qualified Agda.TypeChecking.Monad.Benchmark as Bench
  import {-# SOURCE #-} Agda.TypeChecking.Monad.Options
    (getIncludeDirs, libToTCM)
  import Agda.TypeChecking.Monad.State ( registerFileIdWithBuiltin, topLevelModuleName )
  import Agda.TypeChecking.Monad.Trace (runPM, setCurrentRange)
  
  import Agda.Version ( version )
  
  import Agda.Utils.Applicative ( (?$>) )
  import Agda.Utils.CallStack   ( HasCallStack )
  import Agda.Utils.FileId
  import Agda.Utils.FileName
  import Agda.Utils.List  ( stripSuffix, nubOn )
  import Agda.Utils.List1 ( List1, pattern (:|) )
  import Agda.Utils.List2 ( List2, pattern List2 )
  import qualified Agda.Utils.List1 as List1
  import qualified Agda.Utils.List2 as List2
  import Agda.Utils.Monad ( ifM, unlessM )
  import Agda.Syntax.Common.Pretty ( Pretty(..), prettyShow )
  import qualified Agda.Syntax.Common.Pretty as P
  import Agda.Utils.Singleton
  
  import Agda.Utils.Impossible
  
  -- This instance isn't producing something pretty.
  -- instance Pretty SourceFile where
  --   pretty = pretty . srcFileId
  
  -- | File must exist.
  newtype InterfaceFile = InterfaceFile { intFilePath :: AbsolutePath }
  
  instance Pretty InterfaceFile where
    pretty = pretty . intFilePath
  
  -- | Makes an interface file from an AbsolutePath candidate.
  --   If the file does not exist, then fail by returning @Nothing@.
  
  mkInterfaceFile
    :: AbsolutePath             -- ^ Path to the candidate interface file
    -> IO (Maybe InterfaceFile) -- ^ Interface file iff it exists
  mkInterfaceFile fp = do
    ex <- doesFileExistCaseSensitive $ filePath fp
    pure (ex ?$> InterfaceFile fp)
  
  -- | Converts an Agda file name to the corresponding interface file
  --   name. Note that we do not guarantee that the file exists.
  
  toIFile :: HasCallStack => SourceFile -> TCM AbsolutePath
  toIFile (SourceFile fi) = do
    src <- fileFromId fi -- partial function, thus HasCallStack
    let fp = filePath src
    let localIFile = replaceModuleExtension ".agdai" src
    mroot <- libToTCM $ findProjectRoot (takeDirectory fp)
    case mroot of
      Nothing   -> pure localIFile
      Just root -> do
        let buildDir = root </> "_build" </> version </> "agda"
        fileName <- liftIO $ makeRelativeCanonical root (filePath localIFile)
        let separatedIFile = mkAbsolute $ buildDir </> fileName
        pure separatedIFile
  
  replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
  replaceModuleExtension ext@('.':_) = mkAbsolute . (++ ext) .  dropAgdaExtension . filePath
  replaceModuleExtension ext = replaceModuleExtension ('.':ext)
  
  -- | Errors which can arise when trying to find a source file.
  --
  -- Invariant: All paths are absolute.
  
  data FindError
    = NotFound [AbsolutePath]
        -- ^ The file was not found.
        --   It should have had one of the given file names.
    | Ambiguous (List2 AbsolutePath)
        -- ^ Several matching files were found.
    deriving Show
  
  -- | Given the module name which the error applies to this function
  -- converts a 'FindError' to a 'TypeError'.
  
  findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
  findErrorToTypeError m = \case
    NotFound  files -> FileNotFound m files
    Ambiguous files -> AmbiguousTopLevelModuleName m files
  
  -- findErrorToTypeError :: MonadFileId m => TopLevelModuleName -> FindError -> m TypeError
  -- findErrorToTypeError m = \case
  --   NotFound  files -> FileNotFound m <$> mapM srcFilePath files
  --   Ambiguous files -> AmbiguousTopLevelModuleName m <$> mapM srcFilePath files
  
  -- | Finds the source file corresponding to a given top-level module
  -- name. The returned paths are absolute.
  --
  -- Raises an error if the file cannot be found.
  
  findFile :: TopLevelModuleName -> TCM SourceFile
  findFile m = do
    mf <- findFile' m
    case mf of
      Left err -> typeError $ findErrorToTypeError m err
      Right f  -> return f
  
  -- | Tries to find the source file corresponding to a given top-level
  --   module name. The returned paths are absolute.
  --
  --   SIDE EFFECT:  Updates 'stModuleToSource'.
  findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
  findFile' m = do
      dirs     <- getIncludeDirs
      modToSrc <- useTC stModuleToSource
      (r, modToSrc) <- liftIO $ runStateT (findFile'' dirs m) modToSrc
      stModuleToSource `setTCLens` modToSrc
      return r
  
  -- | A variant of 'findFile'' which manipulates an extra 'ModuleToSourceId'
  
  findFile'_ ::
       List1 AbsolutePath
         -- ^ Include paths.
    -> TopLevelModuleName
    -> StateT ModuleToSourceId TCM (Either FindError SourceFile)
  findFile'_ incs m = do
    dict <- useTC stFileDict
    m2s  <- get
    (r, ModuleToSource dict' m2s') <- liftIO $
      runStateT (findFile'' incs m) $ ModuleToSource dict m2s
    setTCLens stFileDict dict'
    put m2s'
    return r
  
  -- | A variant of 'findFile'' which does not require 'TCM'.
  
  findFile'' ::
       List1 AbsolutePath
         -- ^ Include paths.
    -> TopLevelModuleName
    -> StateT ModuleToSource IO (Either FindError SourceFile)
  findFile'' dirs m = do
    ModuleToSource dict modToSrc <- get
    case Map.lookup m modToSrc of
      Just sf -> return $ Right sf
      Nothing -> do
        files          <- liftIO $ fileList agdaFileExtensions
        existingFiles  <- liftIO $ filterM (doesFileExistCaseSensitive . filePath) files
        case nubOn id existingFiles of
          [file]   -> do
            let (i, dict') = registerFileIdWithBuiltin file dict
            let src = SourceFile i
            put $ ModuleToSource dict' $ Map.insert m src modToSrc
            return (Right src)
          []       -> do
            filesShortList <- liftIO $ fileList $ List2.toList parseFileExtsShortList
            return (Left (NotFound filesShortList))
          f0:f1:fs -> return (Left (Ambiguous $ List2 f0 f1 fs))
    where
      fileList exts = mapM absolute
                      [ filePath dir </> file
                      | dir  <- List1.toList dirs
                      , file <- map (moduleNameToFileName m) exts
                      ]
  
  -- | Finds the interface file corresponding to a given top-level
  -- module file. The returned paths are absolute.
  --
  -- Raises 'Nothing' if the interface file cannot be found.
  
  findInterfaceFile' :: HasCallStack  -- We are calling partial function toIFile, thus want a call stack.
    => SourceFile                 -- ^ Path to the source file
    -> TCM (Maybe InterfaceFile)  -- ^ Maybe path to the interface file
  findInterfaceFile' fp = liftIO . mkInterfaceFile =<< toIFile fp
  
  
  -- | Finds the interface file corresponding to a given top-level
  -- module file. The returned paths are absolute.
  --
  -- Raises an error if the source file cannot be found, and returns
  -- 'Nothing' if the source file can be found but not the interface
  -- file.
  
  findInterfaceFile :: HasCallStack  -- because of calling a partial function
    => TopLevelModuleName -> TCM (Maybe InterfaceFile)
  findInterfaceFile m = findInterfaceFile' =<< findFile m
  
  -- | Ensures that the module name matches the file name. The file
  -- corresponding to the module name (according to the include path)
  -- has to be the same as the given file name.
  
  checkModuleName ::
       TopLevelModuleName
         -- ^ The name of the module.
    -> SourceFile
         -- ^ The file from which it was loaded.
    -> Maybe TopLevelModuleName
         -- ^ The expected name, coming from an import statement.
    -> TCM ()
  checkModuleName name src0 mexpected = do
    file <- srcFilePath src0
    findFile' name >>= \case
  
      Left (NotFound files)  -> typeError $
        case mexpected of
          Nothing -> ModuleNameDoesntMatchFileName name files
          Just expected -> ModuleNameUnexpected name expected
  
      Left (Ambiguous files) -> typeError $
        AmbiguousTopLevelModuleName name files
  
      Right src -> do
        file' <- srcFilePath src
        file  <- liftIO $ absolute $ filePath file
        unlessM (liftIO $ sameFile file file') $
          typeError $ ModuleDefinedInOtherFile name file file'
  
    -- Andreas, 2020-09-28, issue #4671:  In any case, make sure
    -- that we do not end up with a mismatch between expected
    -- and actual module name.
  
    forM_ mexpected \ expected ->
      unless (name == expected) $
        typeError $ OverlappingProjects file name expected
        -- OverlappingProjects is the correct error for
        -- test/Fail/customized/NestedProjectRoots
        -- -- typeError $ ModuleNameUnexpected name expected
  
  
  parseFileExtsShortList :: List2 String
  parseFileExtsShortList = List2.cons ".agda" literateExtsShortList
  
  -- | Remove an Agda file extension from a filepath, if possible.
  stripAgdaExtension :: FilePath -> Maybe FilePath
  stripAgdaExtension = stripAnyOfExtensions agdaFileExtensions
  
  -- | Check if a file path has an Agda extension.
  hasAgdaExtension :: FilePath -> Bool
  hasAgdaExtension = isJust . stripAgdaExtension
  
  -- | Remove an existing Agda file extension from a file path.
  dropAgdaExtension :: FilePath -> FilePath
  dropAgdaExtension = fromMaybe __IMPOSSIBLE__ . stripAgdaExtension
  
  
  rootNameModule :: AbsolutePath -> String
  rootNameModule = dropAgdaExtension . snd . splitFileName . filePath
  