1------------------------------------------------------------------------
2-- | Functions which map between module names and file names.
3--
4-- Note that file name lookups are cached in the 'TCState'. The code
5-- assumes that no Agda source files are added or removed from the
6-- include directories while the code is being type checked.
7------------------------------------------------------------------------
8
9module Agda.Interaction.FindFile
10  ( SourceFile(..), InterfaceFile(intFilePath)
11  , toIFile, mkInterfaceFile
12  , FindError(..), findErrorToTypeError
13  , findFile, findFile', findFile''
14  , findInterfaceFile', findInterfaceFile
15  , checkModuleName
16  , moduleName
17  , rootNameModule
18  , replaceModuleExtension
19  ) where
20
21import Prelude hiding (null)
22
23import Control.Monad
24import Control.Monad.Except
25import Control.Monad.Trans
26import Data.Maybe (catMaybes)
27import qualified Data.Map as Map
28import System.FilePath
29
30import Agda.Interaction.Library ( findProjectRoot )
31
32import Agda.Syntax.Concrete
33import Agda.Syntax.Parser
34import Agda.Syntax.Parser.Literate (literateExtsShortList)
35import Agda.Syntax.Position
36
37import Agda.Interaction.Options ( optLocalInterfaces )
38
39import Agda.TypeChecking.Monad.Base
40import Agda.TypeChecking.Monad.Benchmark (billTo)
41import qualified Agda.TypeChecking.Monad.Benchmark as Bench
42import Agda.TypeChecking.Monad.Options (getIncludeDirs, libToTCM)
43import Agda.TypeChecking.Warnings (runPM)
44
45import Agda.Version ( version )
46
47import Agda.Utils.Applicative ( (?$>) )
48import Agda.Utils.FileName
49import Agda.Utils.List  ( stripSuffix, nubOn )
50import Agda.Utils.List1 ( List1, pattern (:|) )
51import qualified Agda.Utils.List1 as List1
52import Agda.Utils.Monad ( ifM, unlessM )
53import Agda.Utils.Pretty ( prettyShow )
54import Agda.Utils.Singleton
55
56import Agda.Utils.Impossible
57
58-- | Type aliases for source files and interface files.
59--   We may only produce one of these if we know for sure that the file
60--   does exist. We can always output an @AbsolutePath@ if we are not sure.
61
62-- TODO: do not export @SourceFile@ and force users to check the
63-- @AbsolutePath@ does exist.
64newtype SourceFile    = SourceFile    { srcFilePath :: AbsolutePath } deriving (Eq, Ord)
65newtype InterfaceFile = InterfaceFile { intFilePath :: AbsolutePath }
66
67-- | Makes an interface file from an AbsolutePath candidate.
68--   If the file does not exist, then fail by returning @Nothing@.
69
70mkInterfaceFile
71  :: AbsolutePath             -- ^ Path to the candidate interface file
72  -> IO (Maybe InterfaceFile) -- ^ Interface file iff it exists
73mkInterfaceFile fp = do
74  ex <- doesFileExistCaseSensitive $ filePath fp
75  pure (ex ?$> InterfaceFile fp)
76
77-- | Converts an Agda file name to the corresponding interface file
78--   name. Note that we do not guarantee that the file exists.
79
80toIFile :: SourceFile -> TCM AbsolutePath
81toIFile (SourceFile src) = do
82  let fp = filePath src
83  mroot <- ifM (optLocalInterfaces <$> commandLineOptions)
84               {- then -} (pure Nothing)
85               {- else -} (libToTCM $ findProjectRoot (takeDirectory fp))
86  pure $ replaceModuleExtension ".agdai" $ case mroot of
87    Nothing   -> src
88    Just root ->
89      let buildDir = root </> "_build" </> version </> "agda"
90          fileName = makeRelative root fp
91      in mkAbsolute $ buildDir </> fileName
92
93replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
94replaceModuleExtension ext@('.':_) = mkAbsolute . (++ ext) .  dropAgdaExtension . filePath
95replaceModuleExtension ext = replaceModuleExtension ('.':ext)
96
97-- | Errors which can arise when trying to find a source file.
98--
99-- Invariant: All paths are absolute.
100
101data FindError
102  = NotFound [SourceFile]
103    -- ^ The file was not found. It should have had one of the given
104    -- file names.
105  | Ambiguous [SourceFile]
106    -- ^ Several matching files were found.
107    --
108    -- Invariant: The list of matching files has at least two
109    -- elements.
110
111-- | Given the module name which the error applies to this function
112-- converts a 'FindError' to a 'TypeError'.
113
114findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
115findErrorToTypeError m (NotFound  files) = FileNotFound m (map srcFilePath files)
116findErrorToTypeError m (Ambiguous files) =
117  AmbiguousTopLevelModuleName m (map srcFilePath files)
118
119-- | Finds the source file corresponding to a given top-level module
120-- name. The returned paths are absolute.
121--
122-- Raises an error if the file cannot be found.
123
124findFile :: TopLevelModuleName -> TCM SourceFile
125findFile m = do
126  mf <- findFile' m
127  case mf of
128    Left err -> typeError $ findErrorToTypeError m err
129    Right f  -> return f
130
131-- | Tries to find the source file corresponding to a given top-level
132--   module name. The returned paths are absolute.
133--
134--   SIDE EFFECT:  Updates 'stModuleToSource'.
135findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
136findFile' m = do
137    dirs         <- getIncludeDirs
138    modFile      <- useTC stModuleToSource
139    (r, modFile) <- liftIO $ findFile'' dirs m modFile
140    stModuleToSource `setTCLens` modFile
141    return r
142
143-- | A variant of 'findFile'' which does not require 'TCM'.
144
145findFile''
146  :: [AbsolutePath]
147  -- ^ Include paths.
148  -> TopLevelModuleName
149  -> ModuleToSource
150  -- ^ Cached invocations of 'findFile'''. An updated copy is returned.
151  -> IO (Either FindError SourceFile, ModuleToSource)
152findFile'' dirs m modFile =
153  case Map.lookup m modFile of
154    Just f  -> return (Right (SourceFile f), modFile)
155    Nothing -> do
156      files          <- fileList acceptableFileExts
157      filesShortList <- fileList parseFileExtsShortList
158      existingFiles  <-
159        liftIO $ filterM (doesFileExistCaseSensitive . filePath . srcFilePath) files
160      return $ case nubOn id existingFiles of
161        []     -> (Left (NotFound filesShortList), modFile)
162        [file] -> (Right file, Map.insert m (srcFilePath file) modFile)
163        files  -> (Left (Ambiguous existingFiles), modFile)
164  where
165    fileList exts = mapM (fmap SourceFile . absolute)
166                    [ filePath dir </> file
167                    | dir  <- dirs
168                    , file <- map (moduleNameToFileName m) exts
169                    ]
170
171-- | Finds the interface file corresponding to a given top-level
172-- module file. The returned paths are absolute.
173--
174-- Raises 'Nothing' if the the interface file cannot be found.
175
176findInterfaceFile'
177  :: SourceFile                 -- ^ Path to the source file
178  -> TCM (Maybe InterfaceFile)  -- ^ Maybe path to the interface file
179findInterfaceFile' fp = liftIO . mkInterfaceFile =<< toIFile fp
180
181-- | Finds the interface file corresponding to a given top-level
182-- module file. The returned paths are absolute.
183--
184-- Raises an error if the source file cannot be found, and returns
185-- 'Nothing' if the source file can be found but not the interface
186-- file.
187
188findInterfaceFile :: TopLevelModuleName -> TCM (Maybe InterfaceFile)
189findInterfaceFile m = findInterfaceFile' =<< findFile m
190
191-- | Ensures that the module name matches the file name. The file
192-- corresponding to the module name (according to the include path)
193-- has to be the same as the given file name.
194
195checkModuleName
196  :: TopLevelModuleName
197     -- ^ The name of the module.
198  -> SourceFile
199     -- ^ The file from which it was loaded.
200  -> Maybe TopLevelModuleName
201     -- ^ The expected name, coming from an import statement.
202  -> TCM ()
203checkModuleName name (SourceFile file) mexpected = do
204  findFile' name >>= \case
205
206    Left (NotFound files)  -> typeError $
207      case mexpected of
208        Nothing -> ModuleNameDoesntMatchFileName name (map srcFilePath files)
209        Just expected -> ModuleNameUnexpected name expected
210
211    Left (Ambiguous files) -> typeError $
212      AmbiguousTopLevelModuleName name (map srcFilePath files)
213
214    Right src -> do
215      let file' = srcFilePath src
216      file <- liftIO $ absolute (filePath file)
217      unlessM (liftIO $ sameFile file file') $
218        typeError $ ModuleDefinedInOtherFile name file file'
219
220  -- Andreas, 2020-09-28, issue #4671:  In any case, make sure
221  -- that we do not end up with a mismatch between expected
222  -- and actual module name.
223
224  forM_ mexpected $ \ expected ->
225    unless (name == expected) $
226      typeError $ OverlappingProjects file name expected
227      -- OverlappingProjects is the correct error for
228      -- test/Fail/customized/NestedProjectRoots
229      -- -- typeError $ ModuleNameUnexpected name expected
230
231
232-- | Computes the module name of the top-level module in the given
233-- file.
234--
235-- If no top-level module name is given, then an attempt is made to
236-- use the file name as a module name.
237
238-- TODO: Perhaps it makes sense to move this procedure to some other
239-- module.
240
241moduleName
242  :: AbsolutePath
243     -- ^ The path to the file.
244  -> Module
245     -- ^ The parsed module.
246  -> TCM TopLevelModuleName
247moduleName file parsedModule = billTo [Bench.ModuleName] $
248  case moduleNameParts name of
249    "_" :| [] -> do
250      m <- runPM (parse moduleNameParser defaultName)
251             `catchError` \_ ->
252           typeError $ GenericError $
253             "The file name " ++ prettyShow file ++
254             " is invalid because it does not correspond to a valid module name."
255      case m of
256        Qual {} ->
257          typeError $ GenericError $
258            "The file name " ++ prettyShow file ++ " is invalid because " ++
259            defaultName ++ " is not an unqualified module name."
260        QName {} ->
261          return $ TopLevelModuleName (getRange m) $ singleton defaultName
262    _ -> return name
263  where
264  name        = topLevelModuleName parsedModule
265  defaultName = rootNameModule file
266
267parseFileExtsShortList :: [String]
268parseFileExtsShortList = ".agda" : literateExtsShortList
269
270dropAgdaExtension :: String -> String
271dropAgdaExtension s = case catMaybes [ stripSuffix ext s
272                                     | ext <- acceptableFileExts ] of
273    [name] -> name
274    _      -> __IMPOSSIBLE__
275
276rootNameModule :: AbsolutePath -> String
277rootNameModule = dropAgdaExtension . snd . splitFileName . filePath
278