module Agda.Interaction.FindFile
( toIFile
, FindError(..), findErrorToTypeError
, findFile, findFile', findFile''
, findInterfaceFile
, checkModuleName
, moduleName', moduleName
, tests
) where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans
import Data.List
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.Benchmark (billTo)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.Options (getIncludeDirs)
import Agda.Utils.Except
import Agda.Utils.FileName
import Agda.Utils.Lens
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 <- use stModuleToSource
(r, modFile) <- liftIO $ findFile'' dirs m modFile
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' -> do
file <- liftIO $ absolute (filePath file)
if file === file' then
return ()
else
typeError $ ModuleDefinedInOtherFile name file file'
moduleName' :: AbsolutePath -> TCM TopLevelModuleName
moduleName' file = billTo [Bench.ModuleName] $ do
name <- topLevelModuleName <$> liftIO (parseFile' moduleParser file)
case name of
TopLevelModuleName ["_"] -> do
_ <- liftIO (parse moduleNameParser defaultName)
`catchError` \_ ->
typeError $
GenericError $ "Invalid file name: " ++ show file ++ "."
return $ TopLevelModuleName [defaultName]
_ -> return name
where
defaultName = rootName file
moduleName :: AbsolutePath -> TCM TopLevelModuleName
moduleName file = do
m <- moduleName' file
checkModuleName m file
return m