module Agda.Interaction.FindFile
( toIFile
, FindError(..), findErrorToTypeError
, findFile, findFile', findFile''
, findInterfaceFile
, checkModuleName
, moduleName', moduleName
, rootNameModule
, replaceModuleExtension
) where
import Prelude hiding (null)
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.Trans
import Data.List hiding (null)
import Data.Maybe (catMaybes)
import qualified Data.Map as Map
import System.FilePath
import Agda.Syntax.Common
import Agda.Syntax.Concrete
import Agda.Syntax.Parser
import Agda.Syntax.Parser.Literate (literateExts, literateExtsShortList)
import Agda.Syntax.Position
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Trace
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
import Agda.Utils.Null
#include "undefined.h"
import Agda.Utils.Impossible
toIFile :: AbsolutePath -> AbsolutePath
toIFile = replaceModuleExtension ".agdai"
replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
replaceModuleExtension ext@('.':_) = mkAbsolute . (++ ext) . dropAgdaExtension . filePath
replaceModuleExtension ext = replaceModuleExtension ('.':ext)
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 <- fileList sourceFileExts
filesShortList <- fileList sourceFileExtsShortList
existingFiles <-
liftIO $ filterM (doesFileExistCaseSensitive . filePath) files
return $ case nub existingFiles of
[] -> (Left (NotFound filesShortList), modFile)
[file] -> (Right file, Map.insert m file modFile)
files -> (Left (Ambiguous existingFiles), modFile)
where
fileList exts = mapM absolute
[ filePath dir </> file
| dir <- dirs
, file <- map (moduleNameToFileName m) exts
]
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
-> Maybe TopLevelModuleName
-> TCM ()
checkModuleName name file mexpected = do
findFile' name >>= \case
Left (NotFound files) -> typeError $
case mexpected of
Nothing -> ModuleNameDoesntMatchFileName name files
Just expected -> ModuleNameUnexpected name expected
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 (Ranged TopLevelModuleName)
moduleName' file = billTo [Bench.ModuleName] $ do
q <- runPM (parseFile' moduleParser file)
let name = topLevelModuleName q
case name of
TopLevelModuleName ["_"] -> do
q <- runPM (parse moduleNameParser defaultName)
`catchError` \_ ->
typeError $
GenericError $ "File name " ++ show file ++
" is invalid as it does not correspond to a valid module name."
return $ Ranged (getRange q) $ TopLevelModuleName [defaultName]
_ -> return $ Ranged (getRange q) name
where
defaultName = rootNameModule file
sourceFileExts :: [String]
sourceFileExts = [".agda"] ++ literateExts
sourceFileExtsShortList :: [String]
sourceFileExtsShortList = [".agda"] ++ literateExtsShortList
dropAgdaExtension :: String -> String
dropAgdaExtension s = case catMaybes [ stripExtension ext s
| ext <- sourceFileExts ] of
[name] -> name
_ -> __IMPOSSIBLE__
where
stripExtension :: String -> String -> Maybe String
stripExtension e = fmap reverse . stripPrefix (reverse e) . reverse
rootNameModule :: AbsolutePath -> String
rootNameModule = dropAgdaExtension . snd . splitFileName . filePath
moduleName :: AbsolutePath -> TCM TopLevelModuleName
moduleName file = do
Ranged r m <- moduleName' file
(if null r then id else traceCall (SetRange r)) $
checkModuleName m file Nothing
return m