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