    ------------------------------------------------------------------------
    -- | 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''
      , findInterfaceFile', findInterfaceFile
      , checkModuleName
      , moduleName
      , rootNameModule
      , replaceModuleExtension
      ) where

    import Prelude hiding (null)

    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.Trans
    import Data.Maybe (catMaybes)
    import qualified Data.Map as Map
    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.Interaction.Options ( optLocalInterfaces )

    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.Warnings (runPM)

    import Agda.Version ( version )

    import Agda.Utils.Applicative ( (?$>) )
    import Agda.Utils.FileName
    import Agda.Utils.List  ( stripSuffix, nubOn )
    import Agda.Utils.List1 ( List1, pattern (:|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Monad ( ifM, unlessM )
    import Agda.Utils.Pretty ( Pretty(..), prettyShow )
    import Agda.Utils.Singleton

    import Agda.Utils.Impossible

    -- | Type aliases for source files and interface files.
    --   We may only produce one of these if we know for sure that the file
    --   does exist. We can always output an @AbsolutePath@ if we are not sure.

    -- TODO: do not export @SourceFile@ and force users to check the
    -- @AbsolutePath@ does exist.
    newtype SourceFile    = SourceFile    { SourceFile -> AbsolutePath
    srcFilePath :: AbsolutePath } deriving (SourceFile -> SourceFile -> Bool
    (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool) -> Eq SourceFile
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: SourceFile -> SourceFile -> Bool
    $c/= :: SourceFile -> SourceFile -> Bool
    == :: SourceFile -> SourceFile -> Bool
    $c== :: SourceFile -> SourceFile -> Bool
    Eq, Eq SourceFile
    Eq SourceFile
    -> (SourceFile -> SourceFile -> Ordering)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> Bool)
    -> (SourceFile -> SourceFile -> SourceFile)
    -> (SourceFile -> SourceFile -> SourceFile)
    -> Ord SourceFile
    SourceFile -> SourceFile -> Bool
    SourceFile -> SourceFile -> Ordering
    SourceFile -> SourceFile -> SourceFile
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: SourceFile -> SourceFile -> SourceFile
    $cmin :: SourceFile -> SourceFile -> SourceFile
    max :: SourceFile -> SourceFile -> SourceFile
    $cmax :: SourceFile -> SourceFile -> SourceFile
    >= :: SourceFile -> SourceFile -> Bool
    $c>= :: SourceFile -> SourceFile -> Bool
    > :: SourceFile -> SourceFile -> Bool
    $c> :: SourceFile -> SourceFile -> Bool
    <= :: SourceFile -> SourceFile -> Bool
    $c<= :: SourceFile -> SourceFile -> Bool
    < :: SourceFile -> SourceFile -> Bool
    $c< :: SourceFile -> SourceFile -> Bool
    compare :: SourceFile -> SourceFile -> Ordering
    $ccompare :: SourceFile -> SourceFile -> Ordering
    Ord)
    newtype InterfaceFile = InterfaceFile { InterfaceFile -> AbsolutePath
    intFilePath :: AbsolutePath }

    instance Pretty SourceFile    where pretty :: SourceFile -> Doc
    pretty = AbsolutePath -> Doc
    forall a. Pretty a => a -> Doc
    pretty (AbsolutePath -> Doc)
    -> (SourceFile -> AbsolutePath) -> SourceFile -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SourceFile -> AbsolutePath
    srcFilePath
    instance Pretty InterfaceFile where pretty :: InterfaceFile -> Doc
    pretty = AbsolutePath -> Doc
    forall a. Pretty a => a -> Doc
    pretty (AbsolutePath -> Doc)
    -> (InterfaceFile -> AbsolutePath) -> InterfaceFile -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . InterfaceFile -> AbsolutePath
    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 :: AbsolutePath -> IO (Maybe InterfaceFile)
    mkInterfaceFile AbsolutePath
    fp = do
      Bool
    ex <- String -> IO Bool
    doesFileExistCaseSensitive (String -> IO Bool) -> String -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> String
    filePath AbsolutePath
    fp
      Maybe InterfaceFile -> IO (Maybe InterfaceFile)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Bool
    ex Bool -> InterfaceFile -> Maybe InterfaceFile
    forall (f :: * -> *) a. Alternative f => Bool -> a -> f a
    ?$> AbsolutePath -> InterfaceFile
    InterfaceFile AbsolutePath
    fp)

    -- | Converts an Agda file name to the corresponding interface file
    --   name. Note that we do not guarantee that the file exists.

    toIFile :: SourceFile -> TCM AbsolutePath
    toIFile :: SourceFile -> TCM AbsolutePath
    toIFile (SourceFile AbsolutePath
    src) = do
      let fp :: String
    fp = AbsolutePath -> String
    filePath AbsolutePath
    src
      Maybe String
    mroot <- TCMT IO Bool
    -> TCMT IO (Maybe String)
    -> TCMT IO (Maybe String)
    -> TCMT IO (Maybe String)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (CommandLineOptions -> Bool
    optLocalInterfaces (CommandLineOptions -> Bool)
    -> TCMT IO CommandLineOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO CommandLineOptions
    forall (m :: * -> *). HasOptions m => m CommandLineOptions
    commandLineOptions)
                   {- then -} (Maybe String -> TCMT IO (Maybe String)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe String
    forall a. Maybe a
    Nothing)
                   {- else -} (LibM (Maybe String) -> TCMT IO (Maybe String)
    forall a. LibM a -> TCM a
    libToTCM (LibM (Maybe String) -> TCMT IO (Maybe String))
    -> LibM (Maybe String) -> TCMT IO (Maybe String)
    forall a b. (a -> b) -> a -> b
    $ String -> LibM (Maybe String)
    findProjectRoot (String -> String
    takeDirectory String
    fp))
      AbsolutePath -> TCM AbsolutePath
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (AbsolutePath -> TCM AbsolutePath)
    -> AbsolutePath -> TCM AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension String
    ".agdai" (AbsolutePath -> AbsolutePath) -> AbsolutePath -> AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ case Maybe String
    mroot of
        Maybe String
    Nothing   -> AbsolutePath
    src
        Just String
    root ->
          let buildDir :: String
    buildDir = String
    root String -> String -> String
    </> String
    "_build" String -> String -> String
    </> String
    version String -> String -> String
    </> String
    "agda"
              fileName :: String
    fileName = String -> String -> String
    makeRelative String
    root String
    fp
          in String -> AbsolutePath
    mkAbsolute (String -> AbsolutePath) -> String -> AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ String
    buildDir String -> String -> String
    </> String
    fileName

    replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension ext :: String
    ext@(Char
    '.':String
    _) = String -> AbsolutePath
    mkAbsolute (String -> AbsolutePath)
    -> (AbsolutePath -> String) -> AbsolutePath -> AbsolutePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ext) (String -> String)
    -> (AbsolutePath -> String) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .  String -> String
    dropAgdaExtension (String -> String)
    -> (AbsolutePath -> String) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> String
    filePath
    replaceModuleExtension String
    ext = String -> AbsolutePath -> AbsolutePath
    replaceModuleExtension (Char
    '.'Char -> String -> String
    forall a. a -> [a] -> [a]
    :String
    ext)

    -- | Errors which can arise when trying to find a source file.
    --
    -- Invariant: All paths are absolute.

    data FindError
      = NotFound [SourceFile]
        -- ^ The file was not found. It should have had one of the given
        -- file names.
      | Ambiguous [SourceFile]
        -- ^ Several matching files were found.
        --
        -- Invariant: The list of matching files has at least two
        -- elements.

    -- | Given the module name which the error applies to this function
    -- converts a 'FindError' to a 'TypeError'.

    findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
    findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
    findErrorToTypeError TopLevelModuleName
    m (NotFound  [SourceFile]
    files) = TopLevelModuleName -> [AbsolutePath] -> TypeError
    FileNotFound TopLevelModuleName
    m ((SourceFile -> AbsolutePath) -> [SourceFile] -> [AbsolutePath]
    forall a b. (a -> b) -> [a] -> [b]
    map SourceFile -> AbsolutePath
    srcFilePath [SourceFile]
    files)
    findErrorToTypeError TopLevelModuleName
    m (Ambiguous [SourceFile]
    files) =
      TopLevelModuleName -> [AbsolutePath] -> TypeError
    AmbiguousTopLevelModuleName TopLevelModuleName
    m ((SourceFile -> AbsolutePath) -> [SourceFile] -> [AbsolutePath]
    forall a b. (a -> b) -> [a] -> [b]
    map SourceFile -> AbsolutePath
    srcFilePath [SourceFile]
    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 :: TopLevelModuleName -> TCM SourceFile
    findFile TopLevelModuleName
    m = do
      Either FindError SourceFile
    mf <- TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' TopLevelModuleName
    m
      case Either FindError SourceFile
    mf of
        Left FindError
    err -> TypeError -> TCM SourceFile
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM SourceFile) -> TypeError -> TCM SourceFile
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> FindError -> TypeError
    findErrorToTypeError TopLevelModuleName
    m FindError
    err
        Right SourceFile
    f  -> SourceFile -> TCM SourceFile
    forall (m :: * -> *) a. Monad m => a -> m a
    return SourceFile
    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' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' TopLevelModuleName
    m = do
        [AbsolutePath]
    dirs         <- TCMT IO [AbsolutePath]
    forall (m :: * -> *). HasOptions m => m [AbsolutePath]
    getIncludeDirs
        ModuleToSource
    modFile      <- Lens' ModuleToSource TCState -> TCMT IO ModuleToSource
    forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
    useTC Lens' ModuleToSource TCState
    stModuleToSource
        (Either FindError SourceFile
    r, ModuleToSource
    modFile) <- IO (Either FindError SourceFile, ModuleToSource)
    -> TCMT IO (Either FindError SourceFile, ModuleToSource)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Either FindError SourceFile, ModuleToSource)
     -> TCMT IO (Either FindError SourceFile, ModuleToSource))
    -> IO (Either FindError SourceFile, ModuleToSource)
    -> TCMT IO (Either FindError SourceFile, ModuleToSource)
    forall a b. (a -> b) -> a -> b
    $ [AbsolutePath]
    -> TopLevelModuleName
    -> ModuleToSource
    -> IO (Either FindError SourceFile, ModuleToSource)
    findFile'' [AbsolutePath]
    dirs TopLevelModuleName
    m ModuleToSource
    modFile
        Lens' ModuleToSource TCState
    stModuleToSource Lens' ModuleToSource TCState -> ModuleToSource -> TCMT IO ()
    forall (m :: * -> *) a.
    MonadTCState m =>
    Lens' a TCState -> a -> m ()
    `setTCLens` ModuleToSource
    modFile
        Either FindError SourceFile -> TCM (Either FindError SourceFile)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Either FindError SourceFile
    r

    -- | A variant of 'findFile'' which does not require 'TCM'.

    findFile''
      :: [AbsolutePath]
      -- ^ Include paths.
      -> TopLevelModuleName
      -> ModuleToSource
      -- ^ Cached invocations of 'findFile'''. An updated copy is returned.
      -> IO (Either FindError SourceFile, ModuleToSource)
    findFile'' :: [AbsolutePath]
    -> TopLevelModuleName
    -> ModuleToSource
    -> IO (Either FindError SourceFile, ModuleToSource)
    findFile'' [AbsolutePath]
    dirs TopLevelModuleName
    m ModuleToSource
    modFile =
      case TopLevelModuleName -> ModuleToSource -> Maybe AbsolutePath
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TopLevelModuleName
    m ModuleToSource
    modFile of
        Just AbsolutePath
    f  -> (Either FindError SourceFile, ModuleToSource)
    -> IO (Either FindError SourceFile, ModuleToSource)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SourceFile -> Either FindError SourceFile
    forall a b. b -> Either a b
    Right (AbsolutePath -> SourceFile
    SourceFile AbsolutePath
    f), ModuleToSource
    modFile)
        Maybe AbsolutePath
    Nothing -> do
          [SourceFile]
    files          <- [String] -> IO [SourceFile]
    fileList [String]
    acceptableFileExts
          [SourceFile]
    filesShortList <- [String] -> IO [SourceFile]
    fileList [String]
    parseFileExtsShortList
          [SourceFile]
    existingFiles  <-
            IO [SourceFile] -> IO [SourceFile]
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO [SourceFile] -> IO [SourceFile])
    -> IO [SourceFile] -> IO [SourceFile]
    forall a b. (a -> b) -> a -> b
    $ (SourceFile -> IO Bool) -> [SourceFile] -> IO [SourceFile]
    forall (m :: * -> *) a.
    Applicative m =>
    (a -> m Bool) -> [a] -> m [a]
    filterM (String -> IO Bool
    doesFileExistCaseSensitive (String -> IO Bool)
    -> (SourceFile -> String) -> SourceFile -> IO Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> String
    filePath (AbsolutePath -> String)
    -> (SourceFile -> AbsolutePath) -> SourceFile -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SourceFile -> AbsolutePath
    srcFilePath) [SourceFile]
    files
          (Either FindError SourceFile, ModuleToSource)
    -> IO (Either FindError SourceFile, ModuleToSource)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Either FindError SourceFile, ModuleToSource)
     -> IO (Either FindError SourceFile, ModuleToSource))
    -> (Either FindError SourceFile, ModuleToSource)
    -> IO (Either FindError SourceFile, ModuleToSource)
    forall a b. (a -> b) -> a -> b
    $ case (SourceFile -> SourceFile) -> [SourceFile] -> [SourceFile]
    forall b a. Ord b => (a -> b) -> [a] -> [a]
    nubOn SourceFile -> SourceFile
    forall a. a -> a
    id [SourceFile]
    existingFiles of
            []     -> (FindError -> Either FindError SourceFile
    forall a b. a -> Either a b
    Left ([SourceFile] -> FindError
    NotFound [SourceFile]
    filesShortList), ModuleToSource
    modFile)
            [SourceFile
    file] -> (SourceFile -> Either FindError SourceFile
    forall a b. b -> Either a b
    Right SourceFile
    file, TopLevelModuleName
    -> AbsolutePath -> ModuleToSource -> ModuleToSource
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    Map.insert TopLevelModuleName
    m (SourceFile -> AbsolutePath
    srcFilePath SourceFile
    file) ModuleToSource
    modFile)
            [SourceFile]
    files  -> (FindError -> Either FindError SourceFile
    forall a b. a -> Either a b
    Left ([SourceFile] -> FindError
    Ambiguous [SourceFile]
    existingFiles), ModuleToSource
    modFile)
      where
        fileList :: [String] -> IO [SourceFile]
    fileList [String]
    exts = (String -> IO SourceFile) -> [String] -> IO [SourceFile]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((AbsolutePath -> SourceFile) -> IO AbsolutePath -> IO SourceFile
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap AbsolutePath -> SourceFile
    SourceFile (IO AbsolutePath -> IO SourceFile)
    -> (String -> IO AbsolutePath) -> String -> IO SourceFile
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> IO AbsolutePath
    absolute)
                        [ AbsolutePath -> String
    filePath AbsolutePath
    dir String -> String -> String
    </> String
    file
                        | AbsolutePath
    dir  <- [AbsolutePath]
    dirs
                        , String
    file <- (String -> String) -> [String] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map (TopLevelModuleName -> String -> String
    moduleNameToFileName TopLevelModuleName
    m) [String]
    exts
                        ]

    -- | Finds the interface file corresponding to a given top-level
    -- module file. The returned paths are absolute.
    --
    -- Raises 'Nothing' if the the interface file cannot be found.

    findInterfaceFile'
      :: SourceFile                 -- ^ Path to the source file
      -> TCM (Maybe InterfaceFile)  -- ^ Maybe path to the interface file
    findInterfaceFile' :: SourceFile -> TCM (Maybe InterfaceFile)
    findInterfaceFile' SourceFile
    fp = IO (Maybe InterfaceFile) -> TCM (Maybe InterfaceFile)
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO (Maybe InterfaceFile) -> TCM (Maybe InterfaceFile))
    -> (AbsolutePath -> IO (Maybe InterfaceFile))
    -> AbsolutePath
    -> TCM (Maybe InterfaceFile)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> IO (Maybe InterfaceFile)
    mkInterfaceFile (AbsolutePath -> TCM (Maybe InterfaceFile))
    -> TCM AbsolutePath -> TCM (Maybe InterfaceFile)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SourceFile -> TCM AbsolutePath
    toIFile SourceFile
    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 :: TopLevelModuleName -> TCM (Maybe InterfaceFile)
    findInterfaceFile :: TopLevelModuleName -> TCM (Maybe InterfaceFile)
    findInterfaceFile TopLevelModuleName
    m = SourceFile -> TCM (Maybe InterfaceFile)
    findInterfaceFile' (SourceFile -> TCM (Maybe InterfaceFile))
    -> TCM SourceFile -> TCM (Maybe InterfaceFile)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TopLevelModuleName -> TCM SourceFile
    findFile TopLevelModuleName
    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 :: TopLevelModuleName
    -> SourceFile -> Maybe TopLevelModuleName -> TCMT IO ()
    checkModuleName TopLevelModuleName
    name (SourceFile AbsolutePath
    file) Maybe TopLevelModuleName
    mexpected = do
      TopLevelModuleName -> TCM (Either FindError SourceFile)
    findFile' TopLevelModuleName
    name TCM (Either FindError SourceFile)
    -> (Either FindError SourceFile -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case

        Left (NotFound [SourceFile]
    files)  -> TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          case Maybe TopLevelModuleName
    mexpected of
            Maybe TopLevelModuleName
    Nothing -> TopLevelModuleName -> [AbsolutePath] -> TypeError
    ModuleNameDoesntMatchFileName TopLevelModuleName
    name ((SourceFile -> AbsolutePath) -> [SourceFile] -> [AbsolutePath]
    forall a b. (a -> b) -> [a] -> [b]
    map SourceFile -> AbsolutePath
    srcFilePath [SourceFile]
    files)
            Just TopLevelModuleName
    expected -> TopLevelModuleName -> TopLevelModuleName -> TypeError
    ModuleNameUnexpected TopLevelModuleName
    name TopLevelModuleName
    expected

        Left (Ambiguous [SourceFile]
    files) -> TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          TopLevelModuleName -> [AbsolutePath] -> TypeError
    AmbiguousTopLevelModuleName TopLevelModuleName
    name ((SourceFile -> AbsolutePath) -> [SourceFile] -> [AbsolutePath]
    forall a b. (a -> b) -> [a] -> [b]
    map SourceFile -> AbsolutePath
    srcFilePath [SourceFile]
    files)

        Right SourceFile
    src -> do
          let file' :: AbsolutePath
    file' = SourceFile -> AbsolutePath
    srcFilePath SourceFile
    src
          AbsolutePath
    file <- IO AbsolutePath -> TCM AbsolutePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO AbsolutePath -> TCM AbsolutePath)
    -> IO AbsolutePath -> TCM AbsolutePath
    forall a b. (a -> b) -> a -> b
    $ String -> IO AbsolutePath
    absolute (AbsolutePath -> String
    filePath AbsolutePath
    file)
          TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (IO Bool -> TCMT IO Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> TCMT IO Bool) -> IO Bool -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath -> AbsolutePath -> IO Bool
    sameFile AbsolutePath
    file AbsolutePath
    file') (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
            TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> AbsolutePath -> AbsolutePath -> TypeError
    ModuleDefinedInOtherFile TopLevelModuleName
    name AbsolutePath
    file AbsolutePath
    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.

      Maybe TopLevelModuleName
    -> (TopLevelModuleName -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ Maybe TopLevelModuleName
    mexpected ((TopLevelModuleName -> TCMT IO ()) -> TCMT IO ())
    -> (TopLevelModuleName -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ TopLevelModuleName
    expected ->
        Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (TopLevelModuleName
    name TopLevelModuleName -> TopLevelModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == TopLevelModuleName
    expected) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $
          TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ AbsolutePath
    -> TopLevelModuleName -> TopLevelModuleName -> TypeError
    OverlappingProjects AbsolutePath
    file TopLevelModuleName
    name TopLevelModuleName
    expected
          -- OverlappingProjects is the correct error for
          -- test/Fail/customized/NestedProjectRoots
          -- -- typeError $ ModuleNameUnexpected name expected

    -- | 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.

    -- TODO: Perhaps it makes sense to move this procedure to some other
    -- module.

    moduleName
      :: AbsolutePath
         -- ^ The path to the file.
      -> Module
         -- ^ The parsed module.
      -> TCM TopLevelModuleName
    moduleName :: AbsolutePath -> Module -> TCM TopLevelModuleName
    moduleName AbsolutePath
    file Module
    parsedModule = Account (BenchPhase (TCMT IO))
    -> TCM TopLevelModuleName -> TCM TopLevelModuleName
    forall (m :: * -> *) c.
    MonadBench m =>
    Account (BenchPhase m) -> m c -> m c
    billTo [BenchPhase (TCMT IO)
    Phase
    Bench.ModuleName] (TCM TopLevelModuleName -> TCM TopLevelModuleName)
    -> TCM TopLevelModuleName -> TCM TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $
      case TopLevelModuleName -> List1 String
    moduleNameParts TopLevelModuleName
    name of
        String
    "_" :| [] -> do
          QName
    m <- PM QName -> TCM QName
    forall a. PM a -> TCM a
    runPM (Parser QName -> String -> PM QName
    forall a. Parser a -> String -> PM a
    parse Parser QName
    moduleNameParser String
    defaultName)
                 TCM QName -> (TCErr -> TCM QName) -> TCM QName
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \TCErr
    _ ->
               TypeError -> TCM QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM QName) -> TypeError -> TCM QName
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                 String
    "The file name " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ AbsolutePath -> String
    forall a. Pretty a => a -> String
    prettyShow AbsolutePath
    file String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                 String
    " is invalid because it does not correspond to a valid module name."
          case QName
    m of
            Qual {} ->
              TypeError -> TCM TopLevelModuleName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCM TopLevelModuleName)
    -> TypeError -> TCM TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
                String
    "The file name " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ AbsolutePath -> String
    forall a. Pretty a => a -> String
    prettyShow AbsolutePath
    file String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is invalid because " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                String
    defaultName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not an unqualified module name."
            QName {} ->
              TopLevelModuleName -> TCM TopLevelModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TopLevelModuleName -> TCM TopLevelModuleName)
    -> TopLevelModuleName -> TCM TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ Range -> List1 String -> TopLevelModuleName
    TopLevelModuleName (QName -> Range
    forall a. HasRange a => a -> Range
    getRange QName
    m) (List1 String -> TopLevelModuleName)
    -> List1 String -> TopLevelModuleName
    forall a b. (a -> b) -> a -> b
    $ String -> List1 String
    forall el coll. Singleton el coll => el -> coll
    singleton String
    defaultName
        List1 String
    _ -> TopLevelModuleName -> TCM TopLevelModuleName
    forall (m :: * -> *) a. Monad m => a -> m a
    return TopLevelModuleName
    name
      where
      name :: TopLevelModuleName
    name        = Module -> TopLevelModuleName
    topLevelModuleName Module
    parsedModule
      defaultName :: String
    defaultName = AbsolutePath -> String
    rootNameModule AbsolutePath
    file

    parseFileExtsShortList :: [String]
    parseFileExtsShortList :: [String]
    parseFileExtsShortList = String
    ".agda" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    literateExtsShortList

    dropAgdaExtension :: String -> String
    dropAgdaExtension :: String -> String
    dropAgdaExtension String
    s = case [Maybe String] -> [String]
    forall a. [Maybe a] -> [a]
    catMaybes [ String -> String -> Maybe String
    forall a. Eq a => Suffix a -> Suffix a -> Maybe (Suffix a)
    stripSuffix String
    ext String
    s
                                         | String
    ext <- [String]
    acceptableFileExts ] of
        [String
    name] -> String
    name
        [String]
    _      -> String
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    rootNameModule :: AbsolutePath -> String
    rootNameModule :: AbsolutePath -> String
    rootNameModule = String -> String
    dropAgdaExtension (String -> String)
    -> (AbsolutePath -> String) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String, String) -> String
    forall a b. (a, b) -> b
    snd ((String, String) -> String)
    -> (AbsolutePath -> (String, String)) -> AbsolutePath -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> (String, String)
    splitFileName (String -> (String, String))
    -> (AbsolutePath -> String) -> AbsolutePath -> (String, String)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> String
    filePath