module Agda.Interaction.FindFile
( SourceFile(..), InterfaceFile(intFilePath)
, toIFile, mkInterfaceFile
, FindError(..), findErrorToTypeError
, findFile, findFile', findFile''
, findInterfaceFile', findInterfaceFile
, checkModuleName
, moduleName
, rootNameModule
, replaceModuleExtension
) where
import Prelude hiding (null)
import Control.Monad
import Control.Monad.Trans
import qualified Data.List as List
import Data.Maybe (catMaybes)
import qualified Data.Map as Map
import System.FilePath
import Agda.Interaction.Library ( findProjectRoot )
import Agda.Syntax.Concrete
import Agda.Syntax.Parser
import Agda.Syntax.Parser.Literate (literateExtsShortList)
import Agda.Syntax.Position
import Agda.Interaction.Options ( optLocalInterfaces )
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Benchmark (billTo)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import {-# SOURCE #-} Agda.TypeChecking.Monad.Options (getIncludeDirs)
import Agda.TypeChecking.Warnings (runPM)
import Agda.Utils.Applicative ( (?$>) )
import Agda.Utils.Except
import Agda.Utils.FileName
import Agda.Utils.List ( stripSuffix, nubOn )
import Agda.Utils.Monad ( ifM )
import Agda.Utils.Impossible
import Agda.Version ( version )
newtype SourceFile = SourceFile { srcFilePath :: AbsolutePath } deriving (Eq, Ord)
newtype InterfaceFile = InterfaceFile { intFilePath :: AbsolutePath }
mkInterfaceFile
:: AbsolutePath
-> IO (Maybe InterfaceFile)
mkInterfaceFile fp = do
ex <- doesFileExistCaseSensitive $ filePath fp
pure (ex ?$> InterfaceFile fp)
toIFile :: SourceFile -> TCM AbsolutePath
toIFile (SourceFile src) = do
let fp = filePath src
mroot <- ifM (optLocalInterfaces <$> commandLineOptions)
(pure Nothing)
(liftIO $ findProjectRoot $ takeDirectory fp)
pure $ replaceModuleExtension ".agdai" $ case mroot of
Nothing -> src
Just root ->
let buildDir = root </> "_build" </> version </> "agda"
fileName = makeRelative root fp
in mkAbsolute $ buildDir </> fileName
replaceModuleExtension :: String -> AbsolutePath -> AbsolutePath
replaceModuleExtension ext@('.':_) = mkAbsolute . (++ ext) . dropAgdaExtension . filePath
replaceModuleExtension ext = replaceModuleExtension ('.':ext)
data FindError
= NotFound [SourceFile]
| Ambiguous [SourceFile]
findErrorToTypeError :: TopLevelModuleName -> FindError -> TypeError
findErrorToTypeError m (NotFound files) = FileNotFound m (map srcFilePath files)
findErrorToTypeError m (Ambiguous files) =
AmbiguousTopLevelModuleName m (map srcFilePath files)
findFile :: TopLevelModuleName -> TCM SourceFile
findFile m = do
mf <- findFile' m
case mf of
Left err -> typeError $ findErrorToTypeError m err
Right f -> return f
findFile' :: TopLevelModuleName -> TCM (Either FindError SourceFile)
findFile' m = do
dirs <- getIncludeDirs
modFile <- useTC stModuleToSource
(r, modFile) <- liftIO $ findFile'' dirs m modFile
stModuleToSource `setTCLens` modFile
return r
findFile''
:: [AbsolutePath]
-> TopLevelModuleName
-> ModuleToSource
-> IO (Either FindError SourceFile, ModuleToSource)
findFile'' dirs m modFile =
case Map.lookup m modFile of
Just f -> return (Right (SourceFile f), modFile)
Nothing -> do
files <- fileList acceptableFileExts
filesShortList <- fileList parseFileExtsShortList
existingFiles <-
liftIO $ filterM (doesFileExistCaseSensitive . filePath . srcFilePath) files
return $ case nubOn id existingFiles of
[] -> (Left (NotFound filesShortList), modFile)
[file] -> (Right file, Map.insert m (srcFilePath file) modFile)
files -> (Left (Ambiguous existingFiles), modFile)
where
fileList exts = mapM (fmap SourceFile . absolute)
[ filePath dir </> file
| dir <- dirs
, file <- map (moduleNameToFileName m) exts
]
findInterfaceFile'
:: SourceFile
-> TCM (Maybe InterfaceFile)
findInterfaceFile' fp = liftIO . mkInterfaceFile =<< toIFile fp
findInterfaceFile :: TopLevelModuleName -> TCM (Maybe InterfaceFile)
findInterfaceFile m = findInterfaceFile' =<< findFile m
checkModuleName
:: TopLevelModuleName
-> SourceFile
-> Maybe TopLevelModuleName
-> TCM ()
checkModuleName name (SourceFile file) mexpected =
findFile' name >>= \case
Left (NotFound files) -> typeError $
case mexpected of
Nothing -> ModuleNameDoesntMatchFileName name (map srcFilePath files)
Just expected -> ModuleNameUnexpected name expected
Left (Ambiguous files) -> typeError $
AmbiguousTopLevelModuleName name (map srcFilePath files)
Right src -> do
let file' = srcFilePath src
file <- liftIO $ absolute (filePath file)
if file === file' then
return ()
else
typeError $ ModuleDefinedInOtherFile name file file'
moduleName
:: AbsolutePath
-> Module
-> TCM TopLevelModuleName
moduleName file parsedModule = billTo [Bench.ModuleName] $
case moduleNameParts name of
["_"] -> do
m <- runPM (parse moduleNameParser defaultName)
`catchError` \_ ->
typeError $ GenericError $
"The file name " ++ show file ++
" is invalid because it does not correspond to a valid module name."
case m of
Qual {} ->
typeError $ GenericError $
"The file name " ++ show file ++ " is invalid because " ++
defaultName ++ " is not an unqualified module name."
QName {} ->
return $ TopLevelModuleName (getRange m) [defaultName]
_ -> return name
where
name = topLevelModuleName parsedModule
defaultName = rootNameModule file
parseFileExtsShortList :: [String]
parseFileExtsShortList = [".agda"] ++ literateExtsShortList
dropAgdaExtension :: String -> String
dropAgdaExtension s = case catMaybes [ stripSuffix ext s
| ext <- acceptableFileExts ] of
[name] -> name
_ -> __IMPOSSIBLE__
rootNameModule :: AbsolutePath -> String
rootNameModule = dropAgdaExtension . snd . splitFileName . filePath