{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Interaction.Library
( getDefaultLibraries
, getInstalledLibraries
, libraryIncludePaths
, LibName
, LibM
, LibWarning(..)
, LibPositionInfo(..)
, libraryWarningName
, VersionView(..), versionView, unVersionView
, findLib'
) where
import Control.Arrow ( (***) )
import Control.Exception
import Control.Monad.Writer
import Data.Char
import Data.Data ( Data )
import Data.Either
import Data.Bifunctor ( first )
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.Interaction.Options.Warnings
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)
mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM libs m = do
(x, ews) <- liftIO $ runWriterT m
let (errs, warns) = partitionEithers ews
tell warns
unless (null errs) $ do
let doc = vcat $ map (formatLibError libs) errs
throwError doc
return x
data LibPositionInfo = LibPositionInfo
{ libFilePos :: Maybe FilePath
, lineNumPos :: LineNumber
, filePos :: FilePath
}
deriving (Show, Data)
data LibWarning = LibWarning LibPositionInfo LibWarning'
deriving (Show, Data)
data LibError = LibError (Maybe LibPositionInfo) LibError'
libraryWarningName :: LibWarning -> WarningName
libraryWarningName (LibWarning c (UnknownField{})) = LibUnknownField_
data LibError'
= LibNotFound LibrariesFile LibName
| AmbiguousLib LibName [AgdaLibFile]
| OtherError String
deriving (Show)
type LibErrorIO = WriterT [Either LibError LibWarning] IO
type LibM = ExceptT Doc (WriterT [LibWarning] IO)
warnings :: MonadWriter [Either LibError LibWarning] m => [LibWarning] -> m ()
warnings = tell . map Right
warning :: MonadWriter [Either LibError LibWarning] m => LibWarning -> m ()
warning = warnings . pure
raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m ()
raiseErrors' = tell . map (Left . (LibError Nothing))
raiseErrors :: MonadWriter [Either LibError LibWarning] m => [LibError] -> m ()
raiseErrors = tell . map Left
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, List.nub (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
raiseErrors' [ 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) $ List.nubBy ((==) `on` snd) files
`catchIO` \ e -> do
raiseErrors' [ OtherError $ unlines ["Failed to read installed libraries.", show e] ]
return []
parseLibFiles
:: Maybe LibrariesFile
-> [(LineNumber, FilePath)]
-> LibErrorIO [AgdaLibFile]
parseLibFiles mlibFile files = do
rs' <- lift $ mapM (parseLibFile . snd) files
let ann (ln, fp) (e, ws) = (first (Just pos,) e, map (LibWarning pos) ws)
where pos = LibPositionInfo (lfPath <$> mlibFile) ln fp
let (xs, warns) = unzip $ zipWith ann files (map runP rs')
(errs, als) = partitionEithers xs
unless (null warns) $ warnings $ concat warns
unless (null errs) $
raiseErrors $ map (\(mc,s) -> LibError mc $ OtherError s) errs
return $ List.nubBy ((==) `on` libFile) $ als
stripCommentLines :: String -> [(LineNumber, String)]
stripCommentLines = concatMap strip . zip [1..] . lines
where
strip (i, s) = [ (i, s') | not $ null s' ]
where s' = trimLineComment s
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 [Either LibError LibWarning] [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)
[] -> raiseErrors' [LibNotFound file x] >> find file (x : visited) xs
ls -> raiseErrors' [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)
formatLibPositionInfo :: LibPositionInfo -> String -> Doc
formatLibPositionInfo (LibPositionInfo libFile lineNum file) err = text $
let loc | Just lf <- libFile = lf ++ ":" ++ show lineNum ++ ": "
| otherwise = ""
in if List.isPrefixOf "Failed to read" err
then loc
else file ++ ":" ++ (if all isDigit (take 1 err) then "" else " ")
formatLibError :: [AgdaLibFile] -> LibError -> Doc
formatLibError installed (LibError mc e) = prefix <+> body where
prefix = case mc of
Nothing -> ""
Just c | OtherError err <- e -> formatLibPositionInfo c err
_ -> ""
body = case e of
LibNotFound file lib -> vcat $
[ text $ "Library '" ++ lib ++ "' not found."
, sep [ "Add the path to its .agda-lib file to"
, nest 2 $ text $ "'" ++ lfPath file ++ "'"
, "to install."
]
, "Installed libraries:"
] ++
map (nest 2)
(if null installed then ["(none)"]
else [ sep [ text $ libName l, nest 2 $ parens $ text $ libFile l ]
| l <- installed ])
AmbiguousLib lib tgts -> vcat $
[ sep [ text $ "Ambiguous library '" ++ lib ++ "'."
, "Could refer to any one of" ]
] ++ [ nest 2 $ text (libName l) <+> parens (text $ libFile l) | l <- tgts ]
OtherError err -> text err
instance Pretty LibWarning where
pretty (LibWarning c w) = formatLibPositionInfo c "" <+> pretty w
instance Pretty LibWarning' where
pretty (UnknownField s) = text $ "Unknown field '" ++ s ++ "'"