------------------------------------------------------------------------
-- | 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.Trans
import qualified Data.List as List
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 Agda.TypeChecking.Warnings (runPM)

import Agda.Utils.Applicative ( (?$>) )
import Agda.Utils.Except
import Agda.Utils.FileName
import Agda.Utils.List ( stripSuffix, nubOn )
import Agda.Utils.Monad ( ifM )
import Agda.Utils.Impossible
import Agda.Version ( version )

-- | 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
$cp1Ord :: Eq SourceFile
Ord)
newtype InterfaceFile = InterfaceFile { InterfaceFile -> AbsolutePath
intFilePath :: AbsolutePath }

-- | 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 <- FilePath -> IO Bool
doesFileExistCaseSensitive (FilePath -> IO Bool) -> FilePath -> IO Bool
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> FilePath
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 :: FilePath
fp = AbsolutePath -> FilePath
filePath AbsolutePath
src
  Maybe FilePath
mroot <- TCMT IO Bool
-> TCMT IO (Maybe FilePath)
-> TCMT IO (Maybe FilePath)
-> TCMT IO (Maybe FilePath)
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 FilePath -> TCMT IO (Maybe FilePath)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe FilePath
forall a. Maybe a
Nothing)
               {- else -} (IO (Maybe FilePath) -> TCMT IO (Maybe FilePath)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe FilePath) -> TCMT IO (Maybe FilePath))
-> IO (Maybe FilePath) -> TCMT IO (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> IO (Maybe FilePath)
findProjectRoot (FilePath -> IO (Maybe FilePath))
-> FilePath -> IO (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
takeDirectory FilePath
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
$ FilePath -> AbsolutePath -> AbsolutePath
replaceModuleExtension FilePath
".agdai" (AbsolutePath -> AbsolutePath) -> AbsolutePath -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ case Maybe FilePath
mroot of
    Maybe FilePath
Nothing   -> AbsolutePath
src
    Just FilePath
root ->
      let buildDir :: FilePath
buildDir = FilePath
root FilePath -> FilePath -> FilePath
</> FilePath
"_build" FilePath -> FilePath -> FilePath
</> FilePath
version FilePath -> FilePath -> FilePath
</> FilePath
"agda"
          fileName :: FilePath
fileName = FilePath -> FilePath -> FilePath
makeRelative FilePath
root FilePath
fp
      in FilePath -> AbsolutePath
mkAbsolute (FilePath -> AbsolutePath) -> FilePath -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ FilePath
buildDir FilePath -> FilePath -> FilePath
</> FilePath
fileName

replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
replaceModuleExtension :: FilePath -> AbsolutePath -> AbsolutePath
replaceModuleExtension ext :: FilePath
ext@(Char
'.':FilePath
_) = FilePath -> AbsolutePath
mkAbsolute (FilePath -> AbsolutePath)
-> (AbsolutePath -> FilePath) -> AbsolutePath -> AbsolutePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
ext) (FilePath -> FilePath)
-> (AbsolutePath -> FilePath) -> AbsolutePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  FilePath -> FilePath
dropAgdaExtension (FilePath -> FilePath)
-> (AbsolutePath -> FilePath) -> AbsolutePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> FilePath
filePath
replaceModuleExtension FilePath
ext = FilePath -> AbsolutePath -> AbsolutePath
replaceModuleExtension (Char
'.'Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:FilePath
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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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          <- [FilePath] -> IO [SourceFile]
fileList [FilePath]
acceptableFileExts
      [SourceFile]
filesShortList <- [FilePath] -> IO [SourceFile]
fileList [FilePath]
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 (FilePath -> IO Bool
doesFileExistCaseSensitive (FilePath -> IO Bool)
-> (SourceFile -> FilePath) -> SourceFile -> IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> FilePath
filePath (AbsolutePath -> FilePath)
-> (SourceFile -> AbsolutePath) -> SourceFile -> FilePath
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 :: [FilePath] -> IO [SourceFile]
fileList [FilePath]
exts = (FilePath -> IO SourceFile) -> [FilePath] -> 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)
-> (FilePath -> IO AbsolutePath) -> FilePath -> IO SourceFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO AbsolutePath
absolute)
                    [ AbsolutePath -> FilePath
filePath AbsolutePath
dir FilePath -> FilePath -> FilePath
</> FilePath
file
                    | AbsolutePath
dir  <- [AbsolutePath]
dirs
                    , FilePath
file <- (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (TopLevelModuleName -> FilePath -> FilePath
moduleNameToFileName TopLevelModuleName
m) [FilePath]
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 =
  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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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
$ FilePath -> IO AbsolutePath
absolute (AbsolutePath -> FilePath
filePath AbsolutePath
file)
      if AbsolutePath
file AbsolutePath -> AbsolutePath -> Bool
=== AbsolutePath
file' then
        () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       else
        TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr 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'

-- | 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 Phase -> TCM TopLevelModuleName -> TCM TopLevelModuleName
forall a (m :: * -> *) c. MonadBench a m => Account a -> m c -> m c
billTo [Phase
Bench.ModuleName] (TCM TopLevelModuleName -> TCM TopLevelModuleName)
-> TCM TopLevelModuleName -> TCM TopLevelModuleName
forall a b. (a -> b) -> a -> b
$
  case TopLevelModuleName -> [FilePath]
moduleNameParts TopLevelModuleName
name of
    [FilePath
"_"] -> do
      QName
m <- PM QName -> TCM QName
forall a. PM a -> TCM a
runPM (Parser QName -> FilePath -> PM QName
forall a. Parser a -> FilePath -> PM a
parse Parser QName
moduleNameParser FilePath
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.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM QName) -> TypeError -> TCM QName
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError
GenericError (FilePath -> TypeError) -> FilePath -> TypeError
forall a b. (a -> b) -> a -> b
$
             FilePath
"The file name " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> FilePath
forall a. Show a => a -> FilePath
show AbsolutePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
             FilePath
" is invalid because it does not correspond to a valid module name."
      case QName
m of
        Qual {} ->
          TypeError -> TCM TopLevelModuleName
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM TopLevelModuleName)
-> TypeError -> TCM TopLevelModuleName
forall a b. (a -> b) -> a -> b
$ FilePath -> TypeError
GenericError (FilePath -> TypeError) -> FilePath -> TypeError
forall a b. (a -> b) -> a -> b
$
            FilePath
"The file name " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ AbsolutePath -> FilePath
forall a. Show a => a -> FilePath
show AbsolutePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" is invalid because " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
            FilePath
defaultName FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" 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 -> [FilePath] -> TopLevelModuleName
TopLevelModuleName (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
m) [FilePath
defaultName]
    [FilePath]
_ -> TopLevelModuleName -> TCM TopLevelModuleName
forall (m :: * -> *) a. Monad m => a -> m a
return TopLevelModuleName
name
  where
  name :: TopLevelModuleName
name        = Module -> TopLevelModuleName
topLevelModuleName Module
parsedModule
  defaultName :: FilePath
defaultName = AbsolutePath -> FilePath
rootNameModule AbsolutePath
file

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

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

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