module Agda.Interaction.Library
( getDefaultLibraries
, getInstalledLibraries
, libraryIncludePaths
, LibName
, LibM
, VersionView(..), versionView, unVersionView
, findLib'
) where
import Control.Arrow (first, second)
import Control.Exception
import Control.Monad.Writer
import Data.Char
import Data.Either
import Data.Function
import qualified Data.List as List
import Data.Maybe
import System.Directory ( getAppUserDataDirectory )
import System.Directory
import System.FilePath
import System.Environment
import Agda.Interaction.Library.Base
import Agda.Interaction.Library.Parse
import Agda.Utils.Environment
import Agda.Utils.Except ( ExceptT, runExceptT, MonadError(throwError) )
import Agda.Utils.IO ( catchIO )
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.String ( trim, ltrim )
import Agda.Version
data LibrariesFile = LibrariesFile
{ lfPath :: FilePath
, lfExists :: Bool
} deriving (Show)
data VersionView = VersionView
{ vvBase :: LibName
, vvNumbers :: [Integer]
} deriving (Eq, Show)
data LibError
= LibNotFound LibrariesFile LibName
| AmbiguousLib LibName [AgdaLibFile]
| OtherError String
deriving (Show)
type LibErrorIO = WriterT [LibError] IO
type LibM = ExceptT Doc IO
mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM libs m = do
(x, err) <- lift $ runWriterT m
case err of
[] -> return x
_ -> throwError =<< do lift $ vcat <$> mapM (formatLibError libs) err
getAgdaAppDir :: IO FilePath
getAgdaAppDir = do
let agdaDir = getAppUserDataDirectory "agda"
caseMaybeM (lookupEnv "AGDA_DIR") agdaDir $ \ dir ->
ifM (doesDirectoryExist dir) (canonicalizePath dir) $ do
d <- agdaDir
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"
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
-> Bool
-> LibM ([LibName], [FilePath])
getDefaultLibraries root optDefaultLibs = mkLibM [] $ do
libs <- lift $ findAgdaLibFiles root
if null libs
then (,[]) <$> if optDefaultLibs then (libNameForCurrentDir :) <$> readDefaultsFile else return []
else libsAndPaths <$> parseLibFiles Nothing (map (0,) libs)
where
libsAndPaths ls = (concatMap libDepends ls, concatMap libIncludes ls)
readDefaultsFile :: LibErrorIO [LibName]
readDefaultsFile = do
agdaDir <- lift $ getAgdaAppDir
let file = agdaDir </> defaultsFile
ifNotM (lift $ doesFileExist file) (return []) $ do
ls <- lift $ map snd . stripCommentLines <$> readFile file
return $ concatMap splitCommas ls
`catchIO` \ e -> do
tell [ OtherError $ unlines ["Failed to read defaults file.", show e] ]
return []
getLibrariesFile
:: Maybe FilePath
-> IO LibrariesFile
getLibrariesFile (Just overrideLibFile) =
return $ LibrariesFile overrideLibFile True
getLibrariesFile Nothing = do
agdaDir <- getAgdaAppDir
let defaults = map (agdaDir </>) defaultLibraryFiles
files <- filterM doesFileExist defaults
case files of
file : _ -> return $ LibrariesFile file True
[] -> return $ LibrariesFile (last defaults) False
getInstalledLibraries
:: Maybe FilePath
-> LibM [AgdaLibFile]
getInstalledLibraries overrideLibFile = mkLibM [] $ do
file <- lift $ getLibrariesFile overrideLibFile
if not (lfExists file) then return [] else do
ls <- lift $ stripCommentLines <$> readFile (lfPath file)
files <- lift $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]
parseLibFiles (Just file) files
`catchIO` \ e -> do
tell [ OtherError $ unlines ["Failed to read installed libraries.", show e] ]
return []
parseLibFiles
:: Maybe LibrariesFile
-> [(LineNumber, FilePath)]
-> LibErrorIO [AgdaLibFile]
parseLibFiles libFile files = do
rs <- lift $ mapM (parseLibFile . snd) files
let loc line | Just f <- libFile = lfPath f ++ ":" ++ show line ++ ": "
| otherwise = ""
tell [ OtherError $ pos ++ err
| ((line, path), Left err) <- zip files rs
, let pos = if List.isPrefixOf "Failed to read" err
then loc line
else path ++ ":" ++ (if all isDigit (take 1 err) then "" else " ")
]
return $ rights rs
stripCommentLines :: String -> [(LineNumber, String)]
stripCommentLines = concatMap strip . zip [1..] . lines
where
strip (i, s) = [ (i, s') | not $ null s' ]
where s' = trimLineComment s
formatLibError :: [AgdaLibFile] -> LibError -> IO Doc
formatLibError installed = \case
LibNotFound file lib -> return $ vcat $
[ text $ "Library '" ++ lib ++ "' not found."
, sep [ text "Add the path to its .agda-lib file to"
, nest 2 $ text $ "'" ++ lfPath 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 ])
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 ]
OtherError err -> return $ text err
libraryIncludePaths
:: Maybe FilePath
-> [AgdaLibFile]
-> [LibName]
-> LibM [FilePath]
libraryIncludePaths overrideLibFile libs xs0 = mkLibM libs $ WriterT $ do
file <- getLibrariesFile overrideLibFile
return $ runWriter $ (dot ++) . incs <$> find file [] xs
where
(dots, xs) = List.partition (== libNameForCurrentDir) $ map trim xs0
incs = List.nub . concatMap libIncludes
dot = [ "." | not $ null dots ]
find
:: LibrariesFile
-> [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 = findLib' libName
findLib' :: (a -> LibName) -> LibName -> [a] -> [a]
findLib' libName x libs =
case ls of
l : ls' -> l : takeWhile (((==) `on` versionMeasure) l) ls'
[] -> []
where
ls = List.sortBy (flip compare `on` versionMeasure) [ l | l <- libs, x `hasMatch` libName l ]
versionMeasure l = (rx, null vs, vs)
where
VersionView rx vs = versionView (libName l)
hasMatch :: LibName -> LibName -> Bool
hasMatch x y = rx == ry && (vx == vy || null vx)
where
VersionView rx vx = versionView x
VersionView ry vy = versionView y
versionView :: LibName -> VersionView
versionView s =
case span (\ c -> isDigit c || c == '.') (reverse s) of
(v, '-' : x) | valid vs ->
VersionView (reverse x) $ reverse $ map (read . reverse) vs
where vs = chopWhen (== '.') v
valid [] = False
valid vs = not $ any null vs
_ -> VersionView s []
unVersionView :: VersionView -> LibName
unVersionView = \case
VersionView base [] -> base
VersionView base vs -> base ++ "-" ++ List.intercalate "." (map show vs)