------------------------------------------------------------------------
-- | 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 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.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.Monad.State (topLevelModuleName)
import Agda.TypeChecking.Monad.Trace (runPM, setCurrentRange)
import Agda.TypeChecking.Warnings    (warning)

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

-- | 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
$c== :: SourceFile -> SourceFile -> Bool
== :: SourceFile -> SourceFile -> Bool
$c/= :: SourceFile -> SourceFile -> Bool
/= :: 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
$ccompare :: SourceFile -> SourceFile -> Ordering
compare :: SourceFile -> SourceFile -> Ordering
$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
>= :: SourceFile -> SourceFile -> Bool
$cmax :: SourceFile -> SourceFile -> SourceFile
max :: SourceFile -> SourceFile -> SourceFile
$cmin :: SourceFile -> SourceFile -> SourceFile
min :: SourceFile -> SourceFile -> SourceFile
Ord, Int -> SourceFile -> ShowS
[SourceFile] -> ShowS
SourceFile -> String
(Int -> SourceFile -> ShowS)
-> (SourceFile -> String)
-> ([SourceFile] -> ShowS)
-> Show SourceFile
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SourceFile -> ShowS
showsPrec :: Int -> SourceFile -> ShowS
$cshow :: SourceFile -> String
show :: SourceFile -> String
$cshowList :: [SourceFile] -> ShowS
showList :: [SourceFile] -> ShowS
Show)
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
  ex <- String -> IO Bool
doesFileExistCaseSensitive (String -> IO Bool) -> String -> IO Bool
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> String
filePath AbsolutePath
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 :: SourceFile -> TCM AbsolutePath
toIFile :: SourceFile -> TCM AbsolutePath
toIFile (SourceFile AbsolutePath
src) = do
  let fp :: String
fp = AbsolutePath -> String
filePath AbsolutePath
src
  let localIFile :: AbsolutePath
localIFile = String -> AbsolutePath -> AbsolutePath
replaceModuleExtension String
".agdai" AbsolutePath
src
  mroot <- LibM (Maybe String) -> TCM (Maybe String)
forall a. LibM a -> TCM a
libToTCM (LibM (Maybe String) -> TCM (Maybe String))
-> LibM (Maybe String) -> TCM (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> LibM (Maybe String)
findProjectRoot (ShowS
takeDirectory String
fp)
  case mroot of
    Maybe String
Nothing   -> AbsolutePath -> TCM AbsolutePath
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AbsolutePath
localIFile
    Just String
root -> do
      let buildDir :: String
buildDir = String
root String -> ShowS
</> String
"_build" String -> ShowS
</> String
version String -> ShowS
</> String
"agda"
      fileName <- IO String -> TCMT IO String
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO String -> TCMT IO String) -> IO String -> TCMT IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> IO String
makeRelativeCanonical String
root (AbsolutePath -> String
filePath AbsolutePath
localIFile)
      let separatedIFile = String -> AbsolutePath
mkAbsolute (String -> AbsolutePath) -> String -> AbsolutePath
forall a b. (a -> b) -> a -> b
$ String
buildDir String -> ShowS
</> String
fileName
          ifilePreference = TCMT IO Bool
-> TCMT IO (AbsolutePath, AbsolutePath)
-> TCMT IO (AbsolutePath, AbsolutePath)
-> TCMT IO (AbsolutePath, AbsolutePath)
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)
            ((AbsolutePath, AbsolutePath)
-> TCMT IO (AbsolutePath, AbsolutePath)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AbsolutePath
localIFile, AbsolutePath
separatedIFile))
            ((AbsolutePath, AbsolutePath)
-> TCMT IO (AbsolutePath, AbsolutePath)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AbsolutePath
separatedIFile, AbsolutePath
localIFile))
      separatedIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath separatedIFile
      localIFileExists <- liftIO $ doesFileExistCaseSensitive $ filePath localIFile
      case (separatedIFileExists, localIFileExists) of
        (Bool
False, Bool
False) -> (AbsolutePath, AbsolutePath) -> AbsolutePath
forall a b. (a, b) -> a
fst ((AbsolutePath, AbsolutePath) -> AbsolutePath)
-> TCMT IO (AbsolutePath, AbsolutePath) -> TCM AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (AbsolutePath, AbsolutePath)
ifilePreference
        (Bool
False, Bool
True) -> AbsolutePath -> TCM AbsolutePath
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AbsolutePath
localIFile
        (Bool
True, Bool
False) -> AbsolutePath -> TCM AbsolutePath
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure AbsolutePath
separatedIFile
        (Bool
True, Bool
True) -> do
          ifiles <- TCMT IO (AbsolutePath, AbsolutePath)
ifilePreference
          warning $ uncurry DuplicateInterfaceFiles ifiles
          pure $ fst ifiles

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 -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ext) ShowS -> (AbsolutePath -> String) -> AbsolutePath -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  ShowS
dropAgdaExtension ShowS -> (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 -> ShowS
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 (List2 SourceFile)
    -- ^ Several matching files were found.
  deriving Int -> FindError -> ShowS
[FindError] -> ShowS
FindError -> String
(Int -> FindError -> ShowS)
-> (FindError -> String)
-> ([FindError] -> ShowS)
-> Show FindError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FindError -> ShowS
showsPrec :: Int -> FindError -> ShowS
$cshow :: FindError -> String
show :: FindError -> String
$cshowList :: [FindError] -> ShowS
showList :: [FindError] -> ShowS
Show

-- | 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 = \case
  NotFound  [SourceFile]
files -> TopLevelModuleName -> [AbsolutePath] -> TypeError
FileNotFound TopLevelModuleName
m ([AbsolutePath] -> TypeError) -> [AbsolutePath] -> TypeError
forall a b. (a -> b) -> a -> b
$ (SourceFile -> AbsolutePath) -> [SourceFile] -> [AbsolutePath]
forall a b. (a -> b) -> [a] -> [b]
map SourceFile -> AbsolutePath
srcFilePath [SourceFile]
files
  Ambiguous List2 SourceFile
files -> TopLevelModuleName -> List2 AbsolutePath -> TypeError
AmbiguousTopLevelModuleName TopLevelModuleName
m (List2 AbsolutePath -> TypeError)
-> List2 AbsolutePath -> TypeError
forall a b. (a -> b) -> a -> b
$ (SourceFile -> AbsolutePath)
-> List2 SourceFile -> List2 AbsolutePath
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SourceFile -> AbsolutePath
srcFilePath List2 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
  mf <- TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' TopLevelModuleName
m
  case 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 a. a -> TCMT IO a
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
    dirs         <- TCMT IO (List1 AbsolutePath)
forall (m :: * -> *). HasOptions m => m (List1 AbsolutePath)
getIncludeDirs
    modFile      <- useTC stModuleToSource
    (r, modFile) <- liftIO $ findFile'' dirs m modFile
    stModuleToSource `setTCLens` modFile
    return r

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

findFile'' ::
     List1 AbsolutePath
  -- ^ Include paths.
  -> TopLevelModuleName
  -> ModuleToSource
  -- ^ Cached invocations of 'findFile'''. An updated copy is returned.
  -> IO (Either FindError SourceFile, ModuleToSource)
findFile'' :: List1 AbsolutePath
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' List1 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 a. a -> IO a
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
      files          <- [String] -> IO [SourceFile]
fileList [String]
acceptableFileExts
      filesShortList <- fileList $ List2.toList parseFileExtsShortList
      existingFiles  <-
        liftIO $ filterM (doesFileExistCaseSensitive . filePath . srcFilePath) files
      return $ case nubOn id 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
f0:SourceFile
f1:[SourceFile]
fs -> (FindError -> Either FindError SourceFile
forall a b. a -> Either a b
Left (List2 SourceFile -> FindError
Ambiguous (List2 SourceFile -> FindError) -> List2 SourceFile -> FindError
forall a b. (a -> b) -> a -> b
$ SourceFile -> SourceFile -> [SourceFile] -> List2 SourceFile
forall a. a -> a -> [a] -> List2 a
List2 SourceFile
f0 SourceFile
f1 [SourceFile]
fs), 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((AbsolutePath -> SourceFile) -> IO AbsolutePath -> IO SourceFile
forall a b. (a -> b) -> IO a -> IO b
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 -> ShowS
</> String
file
                    | AbsolutePath
dir  <- List1 AbsolutePath -> [Item (List1 AbsolutePath)]
forall l. IsList l => l -> [Item l]
List1.toList List1 AbsolutePath
dirs
                    , String
file <- ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (TopLevelModuleName -> ShowS
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 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 a. IO a -> TCMT IO a
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 a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
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 List2 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 -> List2 AbsolutePath -> TypeError
AmbiguousTopLevelModuleName TopLevelModuleName
name (List2 AbsolutePath -> TypeError)
-> List2 AbsolutePath -> TypeError
forall a b. (a -> b) -> a -> b
$ (SourceFile -> AbsolutePath)
-> List2 SourceFile -> List2 AbsolutePath
forall a b. (a -> b) -> List2 a -> List2 b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SourceFile -> AbsolutePath
srcFilePath List2 SourceFile
files

    Right SourceFile
src -> do
      let file' :: AbsolutePath
file' = SourceFile -> AbsolutePath
srcFilePath SourceFile
src
      file <- IO AbsolutePath -> TCM AbsolutePath
forall a. IO a -> TCMT IO a
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)
      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.

  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
$ do
  let defaultName :: String
defaultName = AbsolutePath -> String
rootNameModule AbsolutePath
file
      raw :: RawTopLevelModuleName
raw         = Module -> RawTopLevelModuleName
rawTopLevelModuleNameForModule Module
parsedModule
  RawTopLevelModuleName -> TCM TopLevelModuleName
topLevelModuleName (RawTopLevelModuleName -> TCM TopLevelModuleName)
-> TCMT IO RawTopLevelModuleName -> TCM TopLevelModuleName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< if RawTopLevelModuleName -> Bool
forall a. IsNoName a => a -> Bool
isNoName RawTopLevelModuleName
raw
    then Range
-> TCMT IO RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange (AbsolutePath -> Range
rangeFromAbsolutePath AbsolutePath
file) do
      m <- PM QName -> TCM QName
forall a. PM a -> TCM a
runPM ((QName, Attributes) -> QName
forall a b. (a, b) -> a
fst ((QName, Attributes) -> QName)
-> PM (QName, Attributes) -> PM QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser QName -> String -> PM (QName, Attributes)
forall a. Parser a -> String -> PM (a, Attributes)
parse Parser QName
moduleNameParser String
defaultName)
             TCM QName -> (TCErr -> TCM QName) -> TCM QName
forall a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
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
$ AbsolutePath -> InvalidFileNameReason -> TypeError
InvalidFileName AbsolutePath
file InvalidFileNameReason
DoesNotCorrespondToValidModuleName
      case m of
        Qual {} ->
          TypeError -> TCMT IO RawTopLevelModuleName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO RawTopLevelModuleName)
-> TypeError -> TCMT IO RawTopLevelModuleName
forall a b. (a -> b) -> a -> b
$ AbsolutePath -> InvalidFileNameReason -> TypeError
InvalidFileName AbsolutePath
file (InvalidFileNameReason -> TypeError)
-> InvalidFileNameReason -> TypeError
forall a b. (a -> b) -> a -> b
$
            Text -> InvalidFileNameReason
RootNameModuleNotAQualifiedModuleName (Text -> InvalidFileNameReason) -> Text -> InvalidFileNameReason
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack String
defaultName
        QName {} ->
          RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName)
-> RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall a b. (a -> b) -> a -> b
$ RawTopLevelModuleName
            { rawModuleNameRange :: Range
rawModuleNameRange = QName -> Range
forall a. HasRange a => a -> Range
getRange QName
m
            , rawModuleNameParts :: TopLevelModuleNameParts
rawModuleNameParts = Text -> TopLevelModuleNameParts
forall el coll. Singleton el coll => el -> coll
singleton (String -> Text
T.pack String
defaultName)
            }
    else RawTopLevelModuleName -> TCMT IO RawTopLevelModuleName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return RawTopLevelModuleName
raw

parseFileExtsShortList :: List2 String
parseFileExtsShortList :: List2 String
parseFileExtsShortList = String -> List1 String -> List2 String
forall a. a -> List1 a -> List2 a
List2.cons String
".agda" List1 String
literateExtsShortList

dropAgdaExtension :: String -> String
dropAgdaExtension :: ShowS
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 = ShowS
dropAgdaExtension ShowS -> (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