1
------------------------------------------------------------------------
2
-- | Functions which map between module names and file names.
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
------------------------------------------------------------------------
9
module Agda.Interaction.FindFile
11
, FindError(..), findErrorToTypeError
12
, findFile, findFile', findFile''
16
, SourceToModule, sourceToModule
20
import Control.Applicative
22
import Control.Monad.State.Class
23
import Control.Monad.Trans
26
import qualified Data.Map as Map
27
import System.FilePath
28
import System.Directory
30
import Agda.Syntax.Concrete.Name
31
import Agda.TypeChecking.Monad
32
import Agda.Utils.FileName
33
import Agda.Utils.Monad
35
-- | Converts an Agda file name to the corresponding interface file
38
toIFile :: AbsolutePath -> AbsolutePath
39
toIFile f = mkAbsolute (replaceExtension (filePath f) ".agdai")
41
-- | Errors which can arise when trying to find a source file.
43
-- Invariant: All paths are absolute.
46
= NotFound [AbsolutePath]
47
-- ^ The file was not found. It should have had one of the given
49
| Ambiguous [AbsolutePath]
50
-- ^ Several matching files were found.
52
-- Invariant: The list of matching files has at least two
55
-- | Given the module name which the error applies to this function
56
-- converts a 'FindError' to a 'TypeError'.
58
findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
59
findErrorToTypeError m (NotFound files) = FileNotFound m files
60
findErrorToTypeError m (Ambiguous files) =
61
AmbiguousTopLevelModuleName m files
63
-- | Finds the source file corresponding to a given top-level module
64
-- name. The returned paths are absolute.
66
-- Raises an error if the file cannot be found.
68
findFile :: TopLevelModuleName -> TCM AbsolutePath
72
Left err -> typeError $ findErrorToTypeError m err
75
-- | Tries to find the source file corresponding to a given top-level
76
-- module name. The returned paths are absolute.
78
findFile' :: TopLevelModuleName -> TCM (Either FindError AbsolutePath)
80
dirs <- getIncludeDirs
81
modFile <- stModuleToSource <$> get
82
(r, modFile) <- liftIO $ findFile'' dirs m modFile
83
modify $ \s -> s { stModuleToSource = modFile }
86
-- | A variant of 'findFile'' which does not require 'TCM'.
93
-- ^ Cached invocations of 'findFile'''. An updated copy is returned.
94
-> IO (Either FindError AbsolutePath, ModuleToSource)
95
findFile'' dirs m modFile =
96
case Map.lookup m modFile of
97
Just f -> return (Right f, modFile)
100
liftIO $ filterM (doesFileExist . filePath) files
101
return $ case nub existingFiles of
102
[] -> (Left (NotFound files), modFile)
103
[file] -> (Right file, Map.insert m file modFile)
104
files -> (Left (Ambiguous files), modFile)
106
files = [ mkAbsolute (filePath dir </> file)
108
, file <- map (moduleNameToFileName m) [".agda", ".lagda"]
111
-- | Finds the interface file corresponding to a given top-level
112
-- module name. The returned paths are absolute.
114
-- Raises an error if the source file cannot be found, and returns
115
-- 'Nothing' if the source file can be found but not the interface
118
findInterfaceFile :: TopLevelModuleName -> TCM (Maybe AbsolutePath)
119
findInterfaceFile m = do
120
f <- toIFile <$> findFile m
121
ex <- liftIO $ doesFileExist $ filePath f
122
return $ if ex then Just f else Nothing
124
-- | Ensures that the module name matches the file name. The file
125
-- corresponding to the module name (according to the include path)
126
-- has to be the same as the given file name.
128
checkModuleName :: TopLevelModuleName
129
-- ^ The name of the module.
131
-- ^ The file from which it was loaded.
133
checkModuleName name file = do
134
moduleShouldBeIn <- findFile' name
135
case moduleShouldBeIn of
136
Left (NotFound files) -> typeError $
137
ModuleNameDoesntMatchFileName name files
138
Left (Ambiguous files) -> typeError $
139
AmbiguousTopLevelModuleName name files
141
ifM (liftIO $ filePath file === filePath file')
143
(typeError $ ModuleDefinedInOtherFile name file file')
145
-- | Maps top-level module names to the corresponding source file
148
type ModuleToSource = Map TopLevelModuleName AbsolutePath
150
-- | Maps source file names to the corresponding top-level module
153
type SourceToModule = Map AbsolutePath TopLevelModuleName
155
-- | Creates a 'SourceToModule' map based on 'stModuleToSource'.
157
sourceToModule :: TCM SourceToModule
160
. map (\(m, f) -> (f, m))
added
removed
src/full/Agda/Interaction/FindFile.hs
