module Agda.Interaction.FindFile
( toIFile
, FindError(..), findErrorToTypeError
, findFile, findFile', findFile''
, findInterfaceFile
, checkModuleName
, moduleName', moduleName
, 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 Agda.Syntax.Concrete
import Agda.Syntax.Parser
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Options (getIncludeDirs)
import Agda.Utils.FileName
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
files <- mapM absolute
[ filePath dir </> file
| dir <- dirs
, file <- map (moduleNameToFileName m)
[".agda", ".lagda"]
]
existingFiles <-
liftIO $ filterM (doesFileExistCaseSensitive . filePath) files
return $ case nub existingFiles of
[] -> (Left (NotFound files), modFile)
[file] -> (Right file, Map.insert m file modFile)
files -> (Left (Ambiguous files), modFile)
findInterfaceFile :: TopLevelModuleName -> TCM (Maybe AbsolutePath)
findInterfaceFile m = do
f <- toIFile <$> findFile m
ex <- liftIO $ doesFileExistCaseSensitive $ 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' ->
if file === file' then
return ()
else
typeError $ ModuleDefinedInOtherFile name file file'
moduleName' :: AbsolutePath -> TCM TopLevelModuleName
moduleName' file = liftIO $ do
topLevelModuleName <$> parseFile' moduleParser file
moduleName :: AbsolutePath -> TCM TopLevelModuleName
moduleName file = do
m <- moduleName' file
checkModuleName m file
return m
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