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