module Agda.Interaction.FindFile
( toIFile
, FindError(..), findErrorToTypeError
, findFile, findFile', findFile''
, findInterfaceFile
, checkModuleName
, ModuleToSource
, SourceToModule, sourceToModule
, tests
) where
import Control.Applicative
import Control.Monad
import Control.Monad.State.Class
import Control.Monad.Trans
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import System.FilePath
import System.Directory
import Agda.Syntax.Concrete.Name
import Agda.TypeChecking.Monad
import Agda.Utils.FileName
import Agda.Utils.Monad
toIFile :: AbsolutePath -> AbsolutePath
toIFile f = mkAbsolute (replaceExtension (filePath f) ".agdai")
data FindError
= NotFound [AbsolutePath]
| Ambiguous [AbsolutePath]
findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError m (NotFound files) = FileNotFound m files
findErrorToTypeError m (Ambiguous files) =
AmbiguousTopLevelModuleName m files
findFile :: TopLevelModuleName -> TCM AbsolutePath
findFile m = do
mf <- findFile' m
case mf of
Left err -> typeError $ findErrorToTypeError m err
Right f -> return f
findFile' :: TopLevelModuleName -> TCM (Either FindError AbsolutePath)
findFile' m = do
dirs <- getIncludeDirs
modFile <- stModuleToSource <$> get
(r, modFile) <- liftIO $ findFile'' dirs m modFile
modify $ \s -> s { stModuleToSource = modFile }
return r
findFile''
:: [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError AbsolutePath, ModuleToSource)
findFile'' dirs m modFile =
case Map.lookup m modFile of
Just f -> return (Right f, modFile)
Nothing -> do
existingFiles <-
liftIO $ filterM (doesFileExist . filePath) files
return $ case nub existingFiles of
[] -> (Left (NotFound files), modFile)
[file] -> (Right file, Map.insert m file modFile)
files -> (Left (Ambiguous files), modFile)
where
files = [ mkAbsolute (filePath dir </> file)
| dir <- dirs
, file <- map (moduleNameToFileName m) [".agda", ".lagda"]
]
findInterfaceFile :: TopLevelModuleName -> TCM (Maybe AbsolutePath)
findInterfaceFile m = do
f <- toIFile <$> findFile m
ex <- liftIO $ doesFileExist $ filePath f
return $ if ex then Just f else Nothing
checkModuleName :: TopLevelModuleName
-> AbsolutePath
-> TCM ()
checkModuleName name file = do
moduleShouldBeIn <- findFile' name
case moduleShouldBeIn of
Left (NotFound files) -> typeError $
ModuleNameDoesntMatchFileName name files
Left (Ambiguous files) -> typeError $
AmbiguousTopLevelModuleName name files
Right file' ->
ifM (liftIO $ filePath file === filePath file')
(return ())
(typeError $ ModuleDefinedInOtherFile name file file')
type ModuleToSource = Map TopLevelModuleName AbsolutePath
type SourceToModule = Map AbsolutePath TopLevelModuleName
sourceToModule :: TCM SourceToModule
sourceToModule =
Map.fromList
. map (\(m, f) -> (f, m))
. Map.toList
. stModuleToSource
<$> get