module Agda.Interaction.Library
( getDefaultLibraries
, getInstalledLibraries
, libraryIncludePaths
, LibName
, LibM
) where
import Control.Arrow (first, second)
import Control.Applicative
import Control.Exception
import Control.Monad.Writer
import Data.Char
import Data.Either
import Data.Function
import Data.List
import Data.Maybe
import System.Directory
import System.FilePath
import System.Environment
import Agda.Interaction.Library.Base
import Agda.Interaction.Library.Parse
import Agda.Utils.Monad
import Agda.Utils.Environment
import Agda.Utils.Except ( ExceptT, runExceptT, MonadError(throwError) )
import Agda.Utils.List
import Agda.Utils.Pretty
import Agda.Version
type LibM = ExceptT Doc IO
catchIO :: IO a -> (IOException -> IO a) -> IO a
catchIO = catch
getAgdaAppDir :: IO FilePath
getAgdaAppDir = do
agdaDir <- lookupEnv "AGDA_DIR"
case agdaDir of
Nothing -> getAppUserDataDirectory "agda"
Just dir ->
ifM (doesDirectoryExist dir) (canonicalizePath dir) $ do
d <- getAppUserDataDirectory "agda"
putStrLn $ "Warning: Environment variable AGDA_DIR points to non-existing directory " ++ show dir ++ ", using " ++ show d ++ " instead."
return d
defaultLibraryFiles :: [FilePath]
defaultLibraryFiles = ["libraries-" ++ version, "libraries"]
defaultsFile :: FilePath
defaultsFile = "defaults"
data LibError = LibNotFound FilePath LibName
| AmbiguousLib LibName [AgdaLibFile]
| OtherError String
deriving (Show)
mkLibM :: [AgdaLibFile] -> IO (a, [LibError]) -> LibM a
mkLibM libs m = do
(x, err) <- lift m
case err of
[] -> return x
_ -> throwError =<< lift (vcat <$> mapM (formatLibError libs) err)
findAgdaLibFiles :: FilePath -> IO [FilePath]
findAgdaLibFiles root = do
libs <- map (root </>) . filter ((== ".agda-lib") . takeExtension) <$> getDirectoryContents root
case libs of
[] -> do
up <- canonicalizePath $ root </> ".."
if up == root then return [] else findAgdaLibFiles up
files -> return files
getDefaultLibraries :: FilePath -> LibM ([LibName], [FilePath])
getDefaultLibraries root = mkLibM [] $ do
libs <- findAgdaLibFiles root
if null libs then first (, []) <$> readDefaultsFile
else first libsAndPaths <$> parseLibFiles Nothing (zip (repeat 0) libs)
where
libsAndPaths ls = (concatMap libDepends ls, concatMap libIncludes ls)
readDefaultsFile :: IO ([LibName], [LibError])
readDefaultsFile = do
agdaDir <- getAgdaAppDir
let file = agdaDir </> defaultsFile
ifM (doesFileExist file) (do
ls <- map snd . stripCommentLines <$> readFile file
return ("." : concatMap splitCommas ls, [])
) (return (["."], []))
`catchIO` \e -> return (["."], [OtherError $ "Failed to read defaults file.\n" ++ show e])
getLibrariesFile :: Maybe FilePath -> IO FilePath
getLibrariesFile overrideLibFile = do
agdaDir <- getAgdaAppDir
let override = maybe [] (:[]) overrideLibFile
files <- (override ++) <$> filterM doesFileExist (map (agdaDir </>) defaultLibraryFiles)
case files of
file : _ -> return file
[] -> return (agdaDir </> last defaultLibraryFiles)
getInstalledLibraries :: Maybe FilePath -> LibM [AgdaLibFile]
getInstalledLibraries overrideLibFile = mkLibM [] $ do
file <- getLibrariesFile overrideLibFile
ifM (doesFileExist file) (do
ls <- stripCommentLines <$> readFile file
files <- sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]
parseLibFiles (Just file) files
) (return ([], []))
`catchIO` \e -> return ([], [OtherError $ "Failed to read installed libraries.\n" ++ show e])
parseLibFiles :: Maybe FilePath -> [(Int, FilePath)] -> IO ([AgdaLibFile], [LibError])
parseLibFiles libFile files = do
rs <- mapM (parseLibFile . snd) files
let loc line | Just f <- libFile = f ++ ":" ++ show line ++ ": "
| otherwise = ""
errs = [ if isPrefixOf "Failed to read" err
then OtherError $ loc line ++ err
else OtherError $ path ++ ":" ++ (if all isDigit (take 1 err) then "" else " ") ++ err
| ((line, path), Left err) <- zip files rs ]
return (rights rs, errs)
stripCommentLines :: String -> [(Int, String)]
stripCommentLines = concatMap strip . zip [1..] . lines
where
strip (i, s) = [ (i, s') | not $ null s' ]
where s' = stripComments $ dropWhile isSpace s
formatLibError :: [AgdaLibFile] -> LibError -> IO Doc
formatLibError installed (LibNotFound file lib) = do
return $ vcat $
[ text $ "Library '" ++ lib ++ "' not found."
, sep [ text "Add the path to its .agda-lib file to"
, nest 2 $ text $ "'" ++ file ++ "'"
, text "to install." ]
, text "Installed libraries:"
] ++
map (nest 2)
(if null installed then [text "(none)"]
else [ sep [ text $ libName l, nest 2 $ parens $ text $ libFile l ] | l <- installed ])
formatLibError _ (AmbiguousLib lib tgts) = return $
vcat $ sep [ text $ "Ambiguous library '" ++ lib ++ "'."
, text "Could refer to any one of" ]
: [ nest 2 $ text (libName l) <+> parens (text $ libFile l) | l <- tgts ]
formatLibError _ (OtherError err) = return $ text err
libraryIncludePaths :: Maybe FilePath -> [AgdaLibFile] -> [LibName] -> LibM [FilePath]
libraryIncludePaths overrideLibFile libs xs0 = mkLibM libs $ do
file <- getLibrariesFile overrideLibFile
return $ runWriter ((dot ++) . incs <$> find file [] xs)
where
xs = map trim $ delete "." xs0
trim = reverse . dropWhile isSpace . reverse . dropWhile isSpace
incs = nub . concatMap libIncludes
dot = [ "." | elem "." xs0 ]
find :: FilePath -> [LibName] -> [LibName] -> Writer [LibError] [AgdaLibFile]
find _ _ [] = pure []
find file visited (x : xs)
| elem x visited = find file visited xs
| otherwise =
case findLib x libs of
[l] -> (l :) <$> find file (x : visited) (libDepends l ++ xs)
[] -> tell [LibNotFound file x] >> find file (x : visited) xs
ls -> tell [AmbiguousLib x ls] >> find file (x : visited) xs
findLib :: LibName -> [AgdaLibFile] -> [AgdaLibFile]
findLib x libs =
case ls of
l : ls -> l : takeWhile ((== versionMeasure l) . versionMeasure) ls
[] -> []
where
ls = sortBy (flip compare `on` versionMeasure) [ l | l <- libs, matchLib x l ]
versionMeasure l = (rx, null vs, vs)
where
(rx, vs) = versionView (libName l)
matchLib :: LibName -> AgdaLibFile -> Bool
matchLib x l = rx == ry && (vx == vy || null vx)
where
(rx, vx) = versionView x
(ry, vy) = versionView $ libName l
versionView :: LibName -> (LibName, [Int])
versionView s =
case span (\ c -> isDigit c || c == '.') (reverse s) of
(v, '-' : x) | valid vs -> (reverse x, reverse $ map (read . reverse) vs)
where vs = chopWhen (== '.') v
valid [] = False
valid vs = not $ any null vs
_ -> (s, [])