{-# LANGUAGE DeriveDataTypeable #-}
-- | Library management.
--
--   Sample use:
--
--   @
--     -- Get libraries as listed in @.agda/libraries@ file.
--     libs <- getInstalledLibraries Nothing
--
--     -- Get the libraries (and immediate paths) relevant for @projectRoot@.
--     -- This involves locating and processing the @.agda-lib@ file for the project.
--     (libNames, includePaths) <-  getDefaultLibraries projectRoot True
--
--     -- Get include paths of depended-on libraries.
--     resolvedPaths <- libraryIncludePaths Nothing libs libNames
--
--     let allPaths = includePaths ++ resolvedPaths
--   @
--
module Agda.Interaction.Library
  ( findProjectRoot
  , getDefaultLibraries
  , getInstalledLibraries
  , libraryIncludePaths
  , LibName
  , LibM
  , LibWarning(..)
  , LibPositionInfo(..)
  , libraryWarningName
  -- * Exported for testing
  , VersionView(..), versionView, unVersionView
  , findLib'
  ) where

import Control.Monad.Writer
import Data.Char
import Data.Data ( Data )
import Data.Either
import Data.Bifunctor ( first )
import Data.Foldable ( foldMap )
import Data.Function
import qualified Data.List as List
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, 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 )

import Agda.Version

------------------------------------------------------------------------
-- * Types and Monads
------------------------------------------------------------------------


data LibrariesFile = LibrariesFile
  { LibrariesFile -> FilePath
lfPath   :: FilePath
      -- ^ E.g. @~/.agda/libraries@.
  , LibrariesFile -> Bool
lfExists :: Bool
       -- ^ The libraries file might not exist,
       --   but we may print its assumed location in error messages.
  } deriving (Int -> LibrariesFile -> ShowS
[LibrariesFile] -> ShowS
LibrariesFile -> FilePath
(Int -> LibrariesFile -> ShowS)
-> (LibrariesFile -> FilePath)
-> ([LibrariesFile] -> ShowS)
-> Show LibrariesFile
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibrariesFile] -> ShowS
$cshowList :: [LibrariesFile] -> ShowS
show :: LibrariesFile -> FilePath
$cshow :: LibrariesFile -> FilePath
showsPrec :: Int -> LibrariesFile -> ShowS
$cshowsPrec :: Int -> LibrariesFile -> ShowS
Show)

-- | Library names are structured into the base name and a suffix of version
--   numbers, e.g. @mylib-1.2.3@.  The version suffix is optional.
data VersionView = VersionView
  { VersionView -> FilePath
vvBase    :: LibName
      -- ^ Actual library name.
  , VersionView -> [Integer]
vvNumbers :: [Integer]
      -- ^ Major version, minor version, subminor version, etc., all non-negative.
      --   Note: a priori, there is no reason why the version numbers should be @Int@s.
  } deriving (VersionView -> VersionView -> Bool
(VersionView -> VersionView -> Bool)
-> (VersionView -> VersionView -> Bool) -> Eq VersionView
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VersionView -> VersionView -> Bool
$c/= :: VersionView -> VersionView -> Bool
== :: VersionView -> VersionView -> Bool
$c== :: VersionView -> VersionView -> Bool
Eq, Int -> VersionView -> ShowS
[VersionView] -> ShowS
VersionView -> FilePath
(Int -> VersionView -> ShowS)
-> (VersionView -> FilePath)
-> ([VersionView] -> ShowS)
-> Show VersionView
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [VersionView] -> ShowS
$cshowList :: [VersionView] -> ShowS
show :: VersionView -> FilePath
$cshow :: VersionView -> FilePath
showsPrec :: Int -> VersionView -> ShowS
$cshowsPrec :: Int -> VersionView -> ShowS
Show)

-- | Raise collected 'LibErrors' as exception.
--
mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [AgdaLibFile]
libs LibErrorIO a
m = do
  (a
x, [Either LibError LibWarning]
ews) <- IO (a, [Either LibError LibWarning])
-> ExceptT
     Doc (WriterT [LibWarning] IO) (a, [Either LibError LibWarning])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (a, [Either LibError LibWarning])
 -> ExceptT
      Doc (WriterT [LibWarning] IO) (a, [Either LibError LibWarning]))
-> IO (a, [Either LibError LibWarning])
-> ExceptT
     Doc (WriterT [LibWarning] IO) (a, [Either LibError LibWarning])
forall a b. (a -> b) -> a -> b
$ LibErrorIO a -> IO (a, [Either LibError LibWarning])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT LibErrorIO a
m
  let ([LibError]
errs, [LibWarning]
warns) = [Either LibError LibWarning] -> ([LibError], [LibWarning])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either LibError LibWarning]
ews
  [LibWarning] -> ExceptT Doc (WriterT [LibWarning] IO) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [LibWarning]
warns
  Bool
-> ExceptT Doc (WriterT [LibWarning] IO) ()
-> ExceptT Doc (WriterT [LibWarning] IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([LibError] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LibError]
errs) (ExceptT Doc (WriterT [LibWarning] IO) ()
 -> ExceptT Doc (WriterT [LibWarning] IO) ())
-> ExceptT Doc (WriterT [LibWarning] IO) ()
-> ExceptT Doc (WriterT [LibWarning] IO) ()
forall a b. (a -> b) -> a -> b
$ do
    let doc :: Doc
doc = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (LibError -> Doc) -> [LibError] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([AgdaLibFile] -> LibError -> Doc
formatLibError [AgdaLibFile]
libs) [LibError]
errs
    Doc -> ExceptT Doc (WriterT [LibWarning] IO) ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Doc
doc
  a -> LibM a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x

------------------------------------------------------------------------
-- * Library warnings and errors
------------------------------------------------------------------------


data LibPositionInfo = LibPositionInfo
  { LibPositionInfo -> Maybe FilePath
libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file
  , LibPositionInfo -> Int
lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
  , LibPositionInfo -> FilePath
filePos    :: FilePath       -- ^ Library file
  }
  deriving (Int -> LibPositionInfo -> ShowS
[LibPositionInfo] -> ShowS
LibPositionInfo -> FilePath
(Int -> LibPositionInfo -> ShowS)
-> (LibPositionInfo -> FilePath)
-> ([LibPositionInfo] -> ShowS)
-> Show LibPositionInfo
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibPositionInfo] -> ShowS
$cshowList :: [LibPositionInfo] -> ShowS
show :: LibPositionInfo -> FilePath
$cshow :: LibPositionInfo -> FilePath
showsPrec :: Int -> LibPositionInfo -> ShowS
$cshowsPrec :: Int -> LibPositionInfo -> ShowS
Show, Typeable LibPositionInfo
DataType
Constr
Typeable LibPositionInfo
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibPositionInfo)
-> (LibPositionInfo -> Constr)
-> (LibPositionInfo -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibPositionInfo))
-> ((forall b. Data b => b -> b)
    -> LibPositionInfo -> LibPositionInfo)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> LibPositionInfo -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> LibPositionInfo -> m LibPositionInfo)
-> Data LibPositionInfo
LibPositionInfo -> DataType
LibPositionInfo -> Constr
(forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibPositionInfo
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
forall u. (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibPositionInfo
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LibPositionInfo)
$cLibPositionInfo :: Constr
$tLibPositionInfo :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
gmapMp :: (forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
gmapM :: (forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> LibPositionInfo -> m LibPositionInfo
gmapQi :: Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> LibPositionInfo -> u
gmapQ :: (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibPositionInfo -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibPositionInfo -> r
gmapT :: (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo
$cgmapT :: (forall b. Data b => b -> b) -> LibPositionInfo -> LibPositionInfo
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LibPositionInfo)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LibPositionInfo)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LibPositionInfo)
dataTypeOf :: LibPositionInfo -> DataType
$cdataTypeOf :: LibPositionInfo -> DataType
toConstr :: LibPositionInfo -> Constr
$ctoConstr :: LibPositionInfo -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibPositionInfo
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibPositionInfo
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibPositionInfo -> c LibPositionInfo
$cp1Data :: Typeable LibPositionInfo
Data)

data LibWarning = LibWarning LibPositionInfo LibWarning'
  deriving (Int -> LibWarning -> ShowS
[LibWarning] -> ShowS
LibWarning -> FilePath
(Int -> LibWarning -> ShowS)
-> (LibWarning -> FilePath)
-> ([LibWarning] -> ShowS)
-> Show LibWarning
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibWarning] -> ShowS
$cshowList :: [LibWarning] -> ShowS
show :: LibWarning -> FilePath
$cshow :: LibWarning -> FilePath
showsPrec :: Int -> LibWarning -> ShowS
$cshowsPrec :: Int -> LibWarning -> ShowS
Show, Typeable LibWarning
DataType
Constr
Typeable LibWarning
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning -> c LibWarning)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning)
-> (LibWarning -> Constr)
-> (LibWarning -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibWarning))
-> ((forall b. Data b => b -> b) -> LibWarning -> LibWarning)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning -> r)
-> (forall u. (forall d. Data d => d -> u) -> LibWarning -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LibWarning -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning)
-> Data LibWarning
LibWarning -> DataType
LibWarning -> Constr
(forall b. Data b => b -> b) -> LibWarning -> LibWarning
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning -> c LibWarning
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LibWarning -> u
forall u. (forall d. Data d => d -> u) -> LibWarning -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning -> c LibWarning
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LibWarning)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning)
$cLibWarning :: Constr
$tLibWarning :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
gmapMp :: (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
gmapM :: (forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LibWarning -> m LibWarning
gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LibWarning -> u
gmapQ :: (forall d. Data d => d -> u) -> LibWarning -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning -> r
gmapT :: (forall b. Data b => b -> b) -> LibWarning -> LibWarning
$cgmapT :: (forall b. Data b => b -> b) -> LibWarning -> LibWarning
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LibWarning)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LibWarning)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LibWarning)
dataTypeOf :: LibWarning -> DataType
$cdataTypeOf :: LibWarning -> DataType
toConstr :: LibWarning -> Constr
$ctoConstr :: LibWarning -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning -> c LibWarning
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning -> c LibWarning
$cp1Data :: Typeable LibWarning
Data)

data LibError = LibError (Maybe LibPositionInfo) LibError'

libraryWarningName :: LibWarning -> WarningName
libraryWarningName :: LibWarning -> WarningName
libraryWarningName (LibWarning LibPositionInfo
c (UnknownField{})) = WarningName
LibUnknownField_

-- | Collected errors while processing library files.
--
data LibError'
  = LibNotFound LibrariesFile LibName
      -- ^ Raised when a library name could no successfully be resolved
      --   to an @.agda-lib@ file.
      --
  | AmbiguousLib LibName [AgdaLibFile]
      -- ^ Raised when a library name is defined in several @.agda-lib files@.
  | OtherError String
      -- ^ Generic error.
  deriving (Int -> LibError' -> ShowS
[LibError'] -> ShowS
LibError' -> FilePath
(Int -> LibError' -> ShowS)
-> (LibError' -> FilePath)
-> ([LibError'] -> ShowS)
-> Show LibError'
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [LibError'] -> ShowS
$cshowList :: [LibError'] -> ShowS
show :: LibError' -> FilePath
$cshow :: LibError' -> FilePath
showsPrec :: Int -> LibError' -> ShowS
$cshowsPrec :: Int -> LibError' -> ShowS
Show)

-- | Collects 'LibError's and 'LibWarning's.
--
type LibErrorIO = WriterT [Either LibError LibWarning] IO

-- | Throws 'Doc' exceptions, still collects 'LibWarning's.
type LibM = ExceptT Doc (WriterT [LibWarning] IO)

warnings :: MonadWriter [Either LibError LibWarning] m => [LibWarning] -> m ()
warnings :: [LibWarning] -> m ()
warnings = [Either LibError LibWarning] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ([Either LibError LibWarning] -> m ())
-> ([LibWarning] -> [Either LibError LibWarning])
-> [LibWarning]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LibWarning -> Either LibError LibWarning)
-> [LibWarning] -> [Either LibError LibWarning]
forall a b. (a -> b) -> [a] -> [b]
map LibWarning -> Either LibError LibWarning
forall a b. b -> Either a b
Right

-- UNUSED Liang-Ting Chen 2019-07-16
--warning :: MonadWriter [Either LibError LibWarning] m => LibWarning -> m ()
--warning = warnings . pure

raiseErrors' :: MonadWriter [Either LibError LibWarning] m => [LibError'] -> m ()
raiseErrors' :: [LibError'] -> m ()
raiseErrors' = [Either LibError LibWarning] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ([Either LibError LibWarning] -> m ())
-> ([LibError'] -> [Either LibError LibWarning])
-> [LibError']
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LibError' -> Either LibError LibWarning)
-> [LibError'] -> [Either LibError LibWarning]
forall a b. (a -> b) -> [a] -> [b]
map (LibError -> Either LibError LibWarning
forall a b. a -> Either a b
Left (LibError -> Either LibError LibWarning)
-> (LibError' -> LibError)
-> LibError'
-> Either LibError LibWarning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe LibPositionInfo -> LibError' -> LibError
LibError Maybe LibPositionInfo
forall a. Maybe a
Nothing))

raiseErrors :: MonadWriter [Either LibError LibWarning] m => [LibError] -> m ()
raiseErrors :: [LibError] -> m ()
raiseErrors = [Either LibError LibWarning] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ([Either LibError LibWarning] -> m ())
-> ([LibError] -> [Either LibError LibWarning])
-> [LibError]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LibError -> Either LibError LibWarning)
-> [LibError] -> [Either LibError LibWarning]
forall a b. (a -> b) -> [a] -> [b]
map LibError -> Either LibError LibWarning
forall a b. a -> Either a b
Left

------------------------------------------------------------------------
-- * Resources
------------------------------------------------------------------------

-- | Get the path to @~/.agda@ (system-specific).
--   Can be overwritten by the @AGDA_DIR@ environment variable.
--
--   (This is not to be confused with the directory for the data files
--   that Agda needs (e.g. the primitive modules).)
--
getAgdaAppDir :: IO FilePath
getAgdaAppDir :: IO FilePath
getAgdaAppDir = do
  -- System-specific command to build the path to ~/.agda (Unix) or %APPDATA%\agda (Win)
  let agdaDir :: IO FilePath
agdaDir = FilePath -> IO FilePath
getAppUserDataDirectory FilePath
"agda"
  -- The default can be overwritten by setting the AGDA_DIR environment variable
  IO (Maybe FilePath)
-> IO FilePath -> (FilePath -> IO FilePath) -> IO FilePath
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (FilePath -> IO (Maybe FilePath)
lookupEnv FilePath
"AGDA_DIR") IO FilePath
agdaDir ((FilePath -> IO FilePath) -> IO FilePath)
-> (FilePath -> IO FilePath) -> IO FilePath
forall a b. (a -> b) -> a -> b
$ \ FilePath
dir ->
      IO Bool -> IO FilePath -> IO FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (FilePath -> IO Bool
doesDirectoryExist FilePath
dir) (FilePath -> IO FilePath
canonicalizePath FilePath
dir) (IO FilePath -> IO FilePath) -> IO FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ do
        FilePath
d <- IO FilePath
agdaDir
        FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath
"Warning: Environment variable AGDA_DIR points to non-existing directory " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
dir FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
", using " FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> FilePath
show FilePath
d FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
" instead."
        FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
d

-- | The @~/.agda/libraries@ file lists the libraries Agda should know about.
--   The content of @libraries@ is is a list of pathes to @.agda-lib@ files.
--
--   Agda honors also version specific @libraries@ files, e.g. @libraries-2.6.0@.
--
--   @defaultLibraryFiles@ gives a list of all @libraries@ files Agda should process
--   by default.
--
defaultLibraryFiles :: [FilePath]
defaultLibraryFiles :: [FilePath]
defaultLibraryFiles = [FilePath
"libraries-" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
version, FilePath
"libraries"]

-- | The @defaultsFile@ contains a list of library names relevant for each Agda project.
--
defaultsFile :: FilePath
defaultsFile :: FilePath
defaultsFile = FilePath
"defaults"

------------------------------------------------------------------------
-- * Get the libraries for the current project
------------------------------------------------------------------------

-- | Find project root by looking for @.agda-lib@ files.
--
--   If there are none, look in the parent directories until one is found.

findProjectConfig
  :: FilePath                          -- ^ Candidate (init: the directory Agda was called in)
  -> IO (Maybe (FilePath, [FilePath])) -- ^ Actual root and @.agda-lib@ files for this project
findProjectConfig :: FilePath -> IO (Maybe (FilePath, [FilePath]))
findProjectConfig FilePath
root = do
  [FilePath]
libs <- ShowS -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath
root FilePath -> ShowS
</>) ([FilePath] -> [FilePath])
-> ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter ((FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
".agda-lib") (FilePath -> Bool) -> ShowS -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
takeExtension) ([FilePath] -> [FilePath]) -> IO [FilePath] -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO [FilePath]
getDirectoryContents FilePath
root
  case [FilePath]
libs of
    []    -> do
      FilePath
up <- FilePath -> IO FilePath
canonicalizePath (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
root FilePath -> ShowS
</> FilePath
".."
      if FilePath
up FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
root then Maybe (FilePath, [FilePath]) -> IO (Maybe (FilePath, [FilePath]))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (FilePath, [FilePath])
forall a. Maybe a
Nothing else FilePath -> IO (Maybe (FilePath, [FilePath]))
findProjectConfig FilePath
up
    [FilePath]
files -> Maybe (FilePath, [FilePath]) -> IO (Maybe (FilePath, [FilePath]))
forall (m :: * -> *) a. Monad m => a -> m a
return ((FilePath, [FilePath]) -> Maybe (FilePath, [FilePath])
forall a. a -> Maybe a
Just (FilePath
root, [FilePath]
files))

-- | Get project root

findProjectRoot :: FilePath -> IO (Maybe FilePath)
findProjectRoot :: FilePath -> IO (Maybe FilePath)
findProjectRoot FilePath
root = ((FilePath, [FilePath]) -> FilePath)
-> Maybe (FilePath, [FilePath]) -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath, [FilePath]) -> FilePath
forall a b. (a, b) -> a
fst (Maybe (FilePath, [FilePath]) -> Maybe FilePath)
-> IO (Maybe (FilePath, [FilePath])) -> IO (Maybe FilePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO (Maybe (FilePath, [FilePath]))
findProjectConfig FilePath
root

-- | Get pathes of @.agda-lib@ files in given project root.

findAgdaLibFiles
  :: FilePath       -- ^ Project root.
  -> IO [FilePath]  -- ^ Pathes of @.agda-lib@ files for this project (if any).
findAgdaLibFiles :: FilePath -> IO [FilePath]
findAgdaLibFiles FilePath
root = [FilePath] -> Maybe [FilePath] -> [FilePath]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [FilePath] -> [FilePath])
-> (Maybe (FilePath, [FilePath]) -> Maybe [FilePath])
-> Maybe (FilePath, [FilePath])
-> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((FilePath, [FilePath]) -> [FilePath])
-> Maybe (FilePath, [FilePath]) -> Maybe [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath, [FilePath]) -> [FilePath]
forall a b. (a, b) -> b
snd (Maybe (FilePath, [FilePath]) -> [FilePath])
-> IO (Maybe (FilePath, [FilePath])) -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO (Maybe (FilePath, [FilePath]))
findProjectConfig FilePath
root

-- | Get dependencies and include paths for given project root:
--
--   Look for @.agda-lib@ files according to 'findAgdaLibFiles'.
--   If none are found, use default dependencies (according to @defaults@ file)
--   and current directory (project root).
--
getDefaultLibraries
  :: FilePath  -- ^ Project root.
  -> Bool      -- ^ Use @defaults@ if no @.agda-lib@ file exists for this project?
  -> LibM ([LibName], [FilePath])  -- ^ The returned @LibName@s are all non-empty strings.
getDefaultLibraries :: FilePath -> Bool -> LibM ([FilePath], [FilePath])
getDefaultLibraries FilePath
root Bool
optDefaultLibs = [AgdaLibFile]
-> LibErrorIO ([FilePath], [FilePath])
-> LibM ([FilePath], [FilePath])
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO ([FilePath], [FilePath])
 -> LibM ([FilePath], [FilePath]))
-> LibErrorIO ([FilePath], [FilePath])
-> LibM ([FilePath], [FilePath])
forall a b. (a -> b) -> a -> b
$ do
  [FilePath]
libs <- IO [FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [FilePath]
 -> WriterT [Either LibError LibWarning] IO [FilePath])
-> IO [FilePath]
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> IO [FilePath]
findAgdaLibFiles FilePath
root
  if [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
libs
    then (,[]) ([FilePath] -> ([FilePath], [FilePath]))
-> WriterT [Either LibError LibWarning] IO [FilePath]
-> LibErrorIO ([FilePath], [FilePath])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if Bool
optDefaultLibs then (FilePath
libNameForCurrentDir FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
:) ([FilePath] -> [FilePath])
-> WriterT [Either LibError LibWarning] IO [FilePath]
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT [Either LibError LibWarning] IO [FilePath]
readDefaultsFile else [FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    else [AgdaLibFile] -> ([FilePath], [FilePath])
forall (t :: * -> *).
Foldable t =>
t AgdaLibFile -> ([FilePath], [FilePath])
libsAndPaths ([AgdaLibFile] -> ([FilePath], [FilePath]))
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
-> LibErrorIO ([FilePath], [FilePath])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe LibrariesFile
-> [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
parseLibFiles Maybe LibrariesFile
forall a. Maybe a
Nothing ((FilePath -> (Int, FilePath)) -> [FilePath] -> [(Int, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map (Int
0,) [FilePath]
libs)
  where
    libsAndPaths :: t AgdaLibFile -> ([FilePath], [FilePath])
libsAndPaths t AgdaLibFile
ls = ( (AgdaLibFile -> [FilePath]) -> t AgdaLibFile -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [FilePath]
_libDepends t AgdaLibFile
ls
                      , ShowS -> [FilePath] -> [FilePath]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn ShowS
forall a. a -> a
id ((AgdaLibFile -> [FilePath]) -> t AgdaLibFile -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [FilePath]
_libIncludes t AgdaLibFile
ls)
                      )

-- | Return list of libraries to be used by default.
--
--   None if the @defaults@ file does not exist.
--
readDefaultsFile :: LibErrorIO [LibName]
readDefaultsFile :: WriterT [Either LibError LibWarning] IO [FilePath]
readDefaultsFile = do
    FilePath
agdaDir <- IO FilePath -> WriterT [Either LibError LibWarning] IO FilePath
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO FilePath -> WriterT [Either LibError LibWarning] IO FilePath)
-> IO FilePath -> WriterT [Either LibError LibWarning] IO FilePath
forall a b. (a -> b) -> a -> b
$ IO FilePath
getAgdaAppDir
    let file :: FilePath
file = FilePath
agdaDir FilePath -> ShowS
</> FilePath
defaultsFile
    WriterT [Either LibError LibWarning] IO Bool
-> WriterT [Either LibError LibWarning] IO [FilePath]
-> WriterT [Either LibError LibWarning] IO [FilePath]
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (IO Bool -> WriterT [Either LibError LibWarning] IO Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> WriterT [Either LibError LibWarning] IO Bool)
-> IO Bool -> WriterT [Either LibError LibWarning] IO Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> IO Bool
doesFileExist FilePath
file) ([FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (WriterT [Either LibError LibWarning] IO [FilePath]
 -> WriterT [Either LibError LibWarning] IO [FilePath])
-> WriterT [Either LibError LibWarning] IO [FilePath]
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall a b. (a -> b) -> a -> b
$ {-else-} do
      [FilePath]
ls <- IO [FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [FilePath]
 -> WriterT [Either LibError LibWarning] IO [FilePath])
-> IO [FilePath]
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall a b. (a -> b) -> a -> b
$ ((Int, FilePath) -> FilePath) -> [(Int, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Int, FilePath) -> FilePath
forall a b. (a, b) -> b
snd ([(Int, FilePath)] -> [FilePath])
-> (FilePath -> [(Int, FilePath)]) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [(Int, FilePath)]
stripCommentLines (FilePath -> [FilePath]) -> IO FilePath -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
readFile FilePath
file
      [FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath])
-> [FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath]
forall a b. (a -> b) -> a -> b
$ (FilePath -> [FilePath]) -> [FilePath] -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FilePath -> [FilePath]
splitCommas [FilePath]
ls
  WriterT [Either LibError LibWarning] IO [FilePath]
-> (IOException
    -> WriterT [Either LibError LibWarning] IO [FilePath])
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    [LibError'] -> WriterT [Either LibError LibWarning] IO ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [ FilePath -> LibError'
OtherError (FilePath -> LibError') -> FilePath -> LibError'
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [FilePath
"Failed to read defaults file.", IOException -> FilePath
forall a. Show a => a -> FilePath
show IOException
e] ]
    [FilePath] -> WriterT [Either LibError LibWarning] IO [FilePath]
forall (m :: * -> *) a. Monad m => a -> m a
return []

------------------------------------------------------------------------
-- * Reading the installed libraries
------------------------------------------------------------------------

-- | Returns the path of the @libraries@ file which lists the libraries Agda knows about.
--
--   Note: file may not exist.
--
getLibrariesFile
  :: Maybe FilePath -- ^ Override the default @libraries@ file?
  -> IO LibrariesFile
getLibrariesFile :: Maybe FilePath -> IO LibrariesFile
getLibrariesFile (Just FilePath
overrideLibFile) =
  LibrariesFile -> IO LibrariesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> IO LibrariesFile)
-> LibrariesFile -> IO LibrariesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> LibrariesFile
LibrariesFile FilePath
overrideLibFile Bool
True  -- Existence checked in cmdline option parser.
getLibrariesFile Maybe FilePath
Nothing = do
  FilePath
agdaDir <- IO FilePath
getAgdaAppDir
  let defaults :: [FilePath]
defaults = ShowS -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath
agdaDir FilePath -> ShowS
</>) [FilePath]
defaultLibraryFiles  -- NB: non-empty list
  [FilePath]
files <- (FilePath -> IO Bool) -> [FilePath] -> IO [FilePath]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM FilePath -> IO Bool
doesFileExist [FilePath]
defaults
  case [FilePath]
files of
    FilePath
file : [FilePath]
_ -> LibrariesFile -> IO LibrariesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> IO LibrariesFile)
-> LibrariesFile -> IO LibrariesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> LibrariesFile
LibrariesFile FilePath
file Bool
True
    []       -> LibrariesFile -> IO LibrariesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> IO LibrariesFile)
-> LibrariesFile -> IO LibrariesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> LibrariesFile
LibrariesFile ([FilePath] -> FilePath
forall a. [a] -> a
last [FilePath]
defaults) Bool
False -- doesn't exist, but that's ok

-- | Parse the descriptions of the libraries Agda knows about.
--
--   Returns none if there is no @libraries@ file.
--
getInstalledLibraries
  :: Maybe FilePath     -- ^ Override the default @libraries@ file?
  -> LibM [AgdaLibFile] -- ^ Content of library files.  (Might have empty @LibName@s.)
getInstalledLibraries :: Maybe FilePath -> LibM [AgdaLibFile]
getInstalledLibraries Maybe FilePath
overrideLibFile = [AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
-> LibM [AgdaLibFile]
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (WriterT [Either LibError LibWarning] IO [AgdaLibFile]
 -> LibM [AgdaLibFile])
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
-> LibM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ do
    LibrariesFile
file <- IO LibrariesFile
-> WriterT [Either LibError LibWarning] IO LibrariesFile
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO LibrariesFile
 -> WriterT [Either LibError LibWarning] IO LibrariesFile)
-> IO LibrariesFile
-> WriterT [Either LibError LibWarning] IO LibrariesFile
forall a b. (a -> b) -> a -> b
$ Maybe FilePath -> IO LibrariesFile
getLibrariesFile Maybe FilePath
overrideLibFile
    if Bool -> Bool
not (LibrariesFile -> Bool
lfExists LibrariesFile
file) then [AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
      [(Int, FilePath)]
ls    <- IO [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [(Int, FilePath)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [(Int, FilePath)]
 -> WriterT [Either LibError LibWarning] IO [(Int, FilePath)])
-> IO [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [(Int, FilePath)]
forall a b. (a -> b) -> a -> b
$ FilePath -> [(Int, FilePath)]
stripCommentLines (FilePath -> [(Int, FilePath)])
-> IO FilePath -> IO [(Int, FilePath)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
readFile (LibrariesFile -> FilePath
lfPath LibrariesFile
file)
      [(Int, FilePath)]
files <- IO [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [(Int, FilePath)]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [(Int, FilePath)]
 -> WriterT [Either LibError LibWarning] IO [(Int, FilePath)])
-> IO [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [(Int, FilePath)]
forall a b. (a -> b) -> a -> b
$ [IO (Int, FilePath)] -> IO [(Int, FilePath)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Int
i, ) (FilePath -> (Int, FilePath)) -> IO FilePath -> IO (Int, FilePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
expandEnvironmentVariables FilePath
s | (Int
i, FilePath
s) <- [(Int, FilePath)]
ls ]
      Maybe LibrariesFile
-> [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
parseLibFiles (LibrariesFile -> Maybe LibrariesFile
forall a. a -> Maybe a
Just LibrariesFile
file) ([(Int, FilePath)]
 -> WriterT [Either LibError LibWarning] IO [AgdaLibFile])
-> [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ ((Int, FilePath) -> FilePath)
-> [(Int, FilePath)] -> [(Int, FilePath)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (Int, FilePath) -> FilePath
forall a b. (a, b) -> b
snd [(Int, FilePath)]
files
  WriterT [Either LibError LibWarning] IO [AgdaLibFile]
-> (IOException
    -> WriterT [Either LibError LibWarning] IO [AgdaLibFile])
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    [LibError'] -> WriterT [Either LibError LibWarning] IO ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [ FilePath -> LibError'
OtherError (FilePath -> LibError') -> FilePath -> LibError'
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [FilePath
"Failed to read installed libraries.", IOException -> FilePath
forall a. Show a => a -> FilePath
show IOException
e] ]
    [AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Parse the given library files.
--
parseLibFiles
  :: Maybe LibrariesFile       -- ^ Name of @libraries@ file for error reporting.
  -> [(LineNumber, FilePath)]  -- ^ Library files paired with their line number in @libraries@.
  -> LibErrorIO [AgdaLibFile]  -- ^ Content of library files.  (Might have empty @LibName@s.)
parseLibFiles :: Maybe LibrariesFile
-> [(Int, FilePath)]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
parseLibFiles Maybe LibrariesFile
mlibFile [(Int, FilePath)]
files = do
  [P AgdaLibFile]
rs' <- IO [P AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [P AgdaLibFile]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO [P AgdaLibFile]
 -> WriterT [Either LibError LibWarning] IO [P AgdaLibFile])
-> IO [P AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [P AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ ((Int, FilePath) -> IO (P AgdaLibFile))
-> [(Int, FilePath)] -> IO [P AgdaLibFile]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FilePath -> IO (P AgdaLibFile)
parseLibFile (FilePath -> IO (P AgdaLibFile))
-> ((Int, FilePath) -> FilePath)
-> (Int, FilePath)
-> IO (P AgdaLibFile)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, FilePath) -> FilePath
forall a b. (a, b) -> b
snd) [(Int, FilePath)]
files
  let ann :: (Int, FilePath)
-> (p t c, [LibWarning'])
-> (p (Maybe LibPositionInfo, t) c, [LibWarning])
ann (Int
ln, FilePath
fp) (p t c
e, [LibWarning']
ws) = ((t -> (Maybe LibPositionInfo, t))
-> p t c -> p (Maybe LibPositionInfo, t) c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (LibPositionInfo -> Maybe LibPositionInfo
forall a. a -> Maybe a
Just LibPositionInfo
pos,) p t c
e, (LibWarning' -> LibWarning) -> [LibWarning'] -> [LibWarning]
forall a b. (a -> b) -> [a] -> [b]
map (LibPositionInfo -> LibWarning' -> LibWarning
LibWarning LibPositionInfo
pos) [LibWarning']
ws)
        where pos :: LibPositionInfo
pos = Maybe FilePath -> Int -> FilePath -> LibPositionInfo
LibPositionInfo (LibrariesFile -> FilePath
lfPath (LibrariesFile -> FilePath)
-> Maybe LibrariesFile -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe LibrariesFile
mlibFile) Int
ln FilePath
fp
  let ([Either (Maybe LibPositionInfo, FilePath) AgdaLibFile]
xs, [[LibWarning]]
warns) = [(Either (Maybe LibPositionInfo, FilePath) AgdaLibFile,
  [LibWarning])]
-> ([Either (Maybe LibPositionInfo, FilePath) AgdaLibFile],
    [[LibWarning]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Either (Maybe LibPositionInfo, FilePath) AgdaLibFile,
   [LibWarning])]
 -> ([Either (Maybe LibPositionInfo, FilePath) AgdaLibFile],
     [[LibWarning]]))
-> [(Either (Maybe LibPositionInfo, FilePath) AgdaLibFile,
     [LibWarning])]
-> ([Either (Maybe LibPositionInfo, FilePath) AgdaLibFile],
    [[LibWarning]])
forall a b. (a -> b) -> a -> b
$ ((Int, FilePath)
 -> (Either FilePath AgdaLibFile, [LibWarning'])
 -> (Either (Maybe LibPositionInfo, FilePath) AgdaLibFile,
     [LibWarning]))
-> [(Int, FilePath)]
-> [(Either FilePath AgdaLibFile, [LibWarning'])]
-> [(Either (Maybe LibPositionInfo, FilePath) AgdaLibFile,
     [LibWarning])]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Int, FilePath)
-> (Either FilePath AgdaLibFile, [LibWarning'])
-> (Either (Maybe LibPositionInfo, FilePath) AgdaLibFile,
    [LibWarning])
forall (p :: * -> * -> *) t c.
Bifunctor p =>
(Int, FilePath)
-> (p t c, [LibWarning'])
-> (p (Maybe LibPositionInfo, t) c, [LibWarning])
ann [(Int, FilePath)]
files ((P AgdaLibFile -> (Either FilePath AgdaLibFile, [LibWarning']))
-> [P AgdaLibFile]
-> [(Either FilePath AgdaLibFile, [LibWarning'])]
forall a b. (a -> b) -> [a] -> [b]
map P AgdaLibFile -> (Either FilePath AgdaLibFile, [LibWarning'])
forall a. P a -> (Either FilePath a, [LibWarning'])
runP [P AgdaLibFile]
rs')
      ([(Maybe LibPositionInfo, FilePath)]
errs, [AgdaLibFile]
als) = [Either (Maybe LibPositionInfo, FilePath) AgdaLibFile]
-> ([(Maybe LibPositionInfo, FilePath)], [AgdaLibFile])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (Maybe LibPositionInfo, FilePath) AgdaLibFile]
xs

  Bool
-> WriterT [Either LibError LibWarning] IO ()
-> WriterT [Either LibError LibWarning] IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([[LibWarning]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[LibWarning]]
warns) (WriterT [Either LibError LibWarning] IO ()
 -> WriterT [Either LibError LibWarning] IO ())
-> WriterT [Either LibError LibWarning] IO ()
-> WriterT [Either LibError LibWarning] IO ()
forall a b. (a -> b) -> a -> b
$ [LibWarning] -> WriterT [Either LibError LibWarning] IO ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibWarning] -> m ()
warnings ([LibWarning] -> WriterT [Either LibError LibWarning] IO ())
-> [LibWarning] -> WriterT [Either LibError LibWarning] IO ()
forall a b. (a -> b) -> a -> b
$ [[LibWarning]] -> [LibWarning]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[LibWarning]]
warns
  Bool
-> WriterT [Either LibError LibWarning] IO ()
-> WriterT [Either LibError LibWarning] IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Maybe LibPositionInfo, FilePath)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Maybe LibPositionInfo, FilePath)]
errs)  (WriterT [Either LibError LibWarning] IO ()
 -> WriterT [Either LibError LibWarning] IO ())
-> WriterT [Either LibError LibWarning] IO ()
-> WriterT [Either LibError LibWarning] IO ()
forall a b. (a -> b) -> a -> b
$
    [LibError] -> WriterT [Either LibError LibWarning] IO ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError] -> m ()
raiseErrors ([LibError] -> WriterT [Either LibError LibWarning] IO ())
-> [LibError] -> WriterT [Either LibError LibWarning] IO ()
forall a b. (a -> b) -> a -> b
$ ((Maybe LibPositionInfo, FilePath) -> LibError)
-> [(Maybe LibPositionInfo, FilePath)] -> [LibError]
forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe LibPositionInfo
mc,FilePath
s) -> Maybe LibPositionInfo -> LibError' -> LibError
LibError Maybe LibPositionInfo
mc (LibError' -> LibError) -> LibError' -> LibError
forall a b. (a -> b) -> a -> b
$ FilePath -> LibError'
OtherError FilePath
s) [(Maybe LibPositionInfo, FilePath)]
errs

  [AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return ([AgdaLibFile]
 -> WriterT [Either LibError LibWarning] IO [AgdaLibFile])
-> [AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ (AgdaLibFile -> FilePath) -> [AgdaLibFile] -> [AgdaLibFile]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn AgdaLibFile -> FilePath
_libFile [AgdaLibFile]
als

-- | Remove trailing white space and line comments.
--
stripCommentLines :: String -> [(LineNumber, String)]
stripCommentLines :: FilePath -> [(Int, FilePath)]
stripCommentLines = ((Int, FilePath) -> [(Int, FilePath)])
-> [(Int, FilePath)] -> [(Int, FilePath)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, FilePath) -> [(Int, FilePath)]
forall a. (a, FilePath) -> [(a, FilePath)]
strip ([(Int, FilePath)] -> [(Int, FilePath)])
-> (FilePath -> [(Int, FilePath)]) -> FilePath -> [(Int, FilePath)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [FilePath] -> [(Int, FilePath)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] ([FilePath] -> [(Int, FilePath)])
-> (FilePath -> [FilePath]) -> FilePath -> [(Int, FilePath)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines
  where
    strip :: (a, FilePath) -> [(a, FilePath)]
strip (a
i, FilePath
s) = [ (a
i, FilePath
s') | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
s' ]
      where s' :: FilePath
s' = ShowS
trimLineComment FilePath
s

------------------------------------------------------------------------
-- * Resolving library names to include pathes
------------------------------------------------------------------------

-- | Get all include pathes for a list of libraries to use.
libraryIncludePaths
  :: Maybe FilePath  -- ^ @libraries@ file (error reporting only).
  -> [AgdaLibFile]   -- ^ Libraries Agda knows about.
  -> [LibName]       -- ^ (Non-empty) library names to be resolved to (lists of) pathes.
  -> LibM [FilePath] -- ^ Resolved pathes (no duplicates).  Contains "." if @[LibName]@ does.
libraryIncludePaths :: Maybe FilePath -> [AgdaLibFile] -> [FilePath] -> LibM [FilePath]
libraryIncludePaths Maybe FilePath
overrideLibFile [AgdaLibFile]
libs [FilePath]
xs0 = [AgdaLibFile]
-> WriterT [Either LibError LibWarning] IO [FilePath]
-> LibM [FilePath]
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [AgdaLibFile]
libs (WriterT [Either LibError LibWarning] IO [FilePath]
 -> LibM [FilePath])
-> WriterT [Either LibError LibWarning] IO [FilePath]
-> LibM [FilePath]
forall a b. (a -> b) -> a -> b
$ IO ([FilePath], [Either LibError LibWarning])
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (IO ([FilePath], [Either LibError LibWarning])
 -> WriterT [Either LibError LibWarning] IO [FilePath])
-> IO ([FilePath], [Either LibError LibWarning])
-> WriterT [Either LibError LibWarning] IO [FilePath]
forall a b. (a -> b) -> a -> b
$ do
    LibrariesFile
file <- Maybe FilePath -> IO LibrariesFile
getLibrariesFile Maybe FilePath
overrideLibFile
    ([FilePath], [Either LibError LibWarning])
-> IO ([FilePath], [Either LibError LibWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return (([FilePath], [Either LibError LibWarning])
 -> IO ([FilePath], [Either LibError LibWarning]))
-> ([FilePath], [Either LibError LibWarning])
-> IO ([FilePath], [Either LibError LibWarning])
forall a b. (a -> b) -> a -> b
$ Writer [Either LibError LibWarning] [FilePath]
-> ([FilePath], [Either LibError LibWarning])
forall w a. Writer w a -> (a, w)
runWriter (Writer [Either LibError LibWarning] [FilePath]
 -> ([FilePath], [Either LibError LibWarning]))
-> Writer [Either LibError LibWarning] [FilePath]
-> ([FilePath], [Either LibError LibWarning])
forall a b. (a -> b) -> a -> b
$ ([FilePath]
dot [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++) ([FilePath] -> [FilePath])
-> ([AgdaLibFile] -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AgdaLibFile] -> [FilePath]
incs ([AgdaLibFile] -> [FilePath])
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
-> Writer [Either LibError LibWarning] [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibrariesFile
-> [FilePath]
-> [FilePath]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
file [] [FilePath]
xs
  where
    ([FilePath]
dots, [FilePath]
xs) = (FilePath -> Bool) -> [FilePath] -> ([FilePath], [FilePath])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
libNameForCurrentDir) ([FilePath] -> ([FilePath], [FilePath]))
-> [FilePath] -> ([FilePath], [FilePath])
forall a b. (a -> b) -> a -> b
$ ShowS -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
trim [FilePath]
xs0
    incs :: [AgdaLibFile] -> [FilePath]
incs       = ShowS -> [FilePath] -> [FilePath]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn ShowS
forall a. a -> a
id ([FilePath] -> [FilePath])
-> ([AgdaLibFile] -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AgdaLibFile -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [FilePath]
_libIncludes
    dot :: [FilePath]
dot        = [ FilePath
"." | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
dots ]

    -- | Due to library dependencies, the work list may grow temporarily.
    find
      :: LibrariesFile  -- ^ Only for error reporting.
      -> [LibName]      -- ^ Already resolved libraries.
      -> [LibName]      -- ^ Work list: libraries left to be resolved.
      -> Writer [Either LibError LibWarning] [AgdaLibFile]
    find :: LibrariesFile
-> [FilePath]
-> [FilePath]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
_ [FilePath]
_ [] = [AgdaLibFile]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    find LibrariesFile
file [FilePath]
visited (FilePath
x : [FilePath]
xs)
      | FilePath
x FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
visited = LibrariesFile
-> [FilePath]
-> [FilePath]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
file [FilePath]
visited [FilePath]
xs
      | Bool
otherwise = do
          -- May or may not find the library
          Maybe AgdaLibFile
ml <- case FilePath -> [AgdaLibFile] -> [AgdaLibFile]
findLib FilePath
x [AgdaLibFile]
libs of
            [AgdaLibFile
l] -> Maybe AgdaLibFile
-> WriterT
     [Either LibError LibWarning] Identity (Maybe AgdaLibFile)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AgdaLibFile -> Maybe AgdaLibFile
forall a. a -> Maybe a
Just AgdaLibFile
l)
            []  -> Maybe AgdaLibFile
forall a. Maybe a
Nothing Maybe AgdaLibFile
-> WriterT [Either LibError LibWarning] Identity ()
-> WriterT
     [Either LibError LibWarning] Identity (Maybe AgdaLibFile)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [LibError'] -> WriterT [Either LibError LibWarning] Identity ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [LibrariesFile -> FilePath -> LibError'
LibNotFound LibrariesFile
file FilePath
x]
            [AgdaLibFile]
ls  -> Maybe AgdaLibFile
forall a. Maybe a
Nothing Maybe AgdaLibFile
-> WriterT [Either LibError LibWarning] Identity ()
-> WriterT
     [Either LibError LibWarning] Identity (Maybe AgdaLibFile)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [LibError'] -> WriterT [Either LibError LibWarning] Identity ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [FilePath -> [AgdaLibFile] -> LibError'
AmbiguousLib FilePath
x [AgdaLibFile]
ls]
          -- If it is found, add its dependencies to work list
          let xs' :: [FilePath]
xs' = (AgdaLibFile -> [FilePath]) -> Maybe AgdaLibFile -> [FilePath]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap AgdaLibFile -> [FilePath]
_libDepends Maybe AgdaLibFile
ml [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
xs
          Maybe AgdaLibFile -> [AgdaLibFile] -> [AgdaLibFile]
forall a. Maybe a -> [a] -> [a]
mcons Maybe AgdaLibFile
ml ([AgdaLibFile] -> [AgdaLibFile])
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibrariesFile
-> [FilePath]
-> [FilePath]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
file (FilePath
x FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
visited) [FilePath]
xs'

-- | @findLib x libs@ retrieves the matches for @x@ from list @libs@.
--
--   1. Case @x@ is unversioned:
--      If @x@ is contained in @libs@, then that match is returned.
--      Otherwise, the matches with the highest version number are returned.
--
--   2. Case @x@ is versioned: the matches with the highest version number are returned.
--
--   Examples, see 'findLib''.
--
findLib :: LibName -> [AgdaLibFile] -> [AgdaLibFile]
findLib :: FilePath -> [AgdaLibFile] -> [AgdaLibFile]
findLib = (AgdaLibFile -> FilePath)
-> FilePath -> [AgdaLibFile] -> [AgdaLibFile]
forall a. (a -> FilePath) -> FilePath -> [a] -> [a]
findLib' AgdaLibFile -> FilePath
_libName

-- | Generalized version of 'findLib' for testing.
--
--   > findLib' id "a"   [ "a-1", "a-02", "a-2", "b" ] == [ "a-02", "a-2" ]
--
--   > findLib' id "a"   [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a" ]
--   > findLib' id "a-1" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-1", "a-01" ]
--   > findLib' id "a-2" [ "a", "a-1", "a-01", "a-2", "b" ] == [ "a-2" ]
--   > findLib' id "c"   [ "a", "a-1", "a-01", "a-2", "b" ] == []
--
findLib' :: (a -> LibName) -> LibName -> [a] -> [a]
findLib' :: (a -> FilePath) -> FilePath -> [a] -> [a]
findLib' a -> FilePath
libName FilePath
x [a]
libs =
  case [a]
ls of
    -- Take the first and all exact matches (modulo leading zeros in version numbers).
    a
l : [a]
ls' -> a
l a -> [a] -> [a]
forall a. a -> [a] -> [a]
: (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (((FilePath, Bool, [Integer]) -> (FilePath, Bool, [Integer]) -> Bool
forall a. Eq a => a -> a -> Bool
(==) ((FilePath, Bool, [Integer])
 -> (FilePath, Bool, [Integer]) -> Bool)
-> (a -> (FilePath, Bool, [Integer])) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> (FilePath, Bool, [Integer])
versionMeasure) a
l) [a]
ls'
    []      -> []
  where
    -- @LibName@s that match @x@, sorted descendingly.
    -- The unversioned LibName, if any, will come first.
    ls :: [a]
ls = (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (((FilePath, Bool, [Integer])
 -> (FilePath, Bool, [Integer]) -> Ordering)
-> (FilePath, Bool, [Integer])
-> (FilePath, Bool, [Integer])
-> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip (FilePath, Bool, [Integer])
-> (FilePath, Bool, [Integer]) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((FilePath, Bool, [Integer])
 -> (FilePath, Bool, [Integer]) -> Ordering)
-> (a -> (FilePath, Bool, [Integer])) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> (FilePath, Bool, [Integer])
versionMeasure)
                     [ a
l | a
l <- [a]
libs, FilePath
x FilePath -> FilePath -> Bool
`hasMatch` a -> FilePath
libName a
l ]

    -- foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0
    versionMeasure :: a -> (FilePath, Bool, [Integer])
versionMeasure a
l = (FilePath
rx, [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Integer]
vs, [Integer]
vs)
      where
        VersionView FilePath
rx [Integer]
vs = FilePath -> VersionView
versionView (a -> FilePath
libName a
l)

-- | @x `hasMatch` y@ if @x@ and @y@ have the same @vvBase@ and
--   either @x@ has no version qualifier or the versions also match.
hasMatch :: LibName -> LibName -> Bool
hasMatch :: FilePath -> FilePath -> Bool
hasMatch FilePath
x FilePath
y = FilePath
rx FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
ry Bool -> Bool -> Bool
&& ([Integer]
vx [Integer] -> [Integer] -> Bool
forall a. Eq a => a -> a -> Bool
== [Integer]
vy Bool -> Bool -> Bool
|| [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Integer]
vx)
  where
    VersionView FilePath
rx [Integer]
vx = FilePath -> VersionView
versionView FilePath
x
    VersionView FilePath
ry [Integer]
vy = FilePath -> VersionView
versionView FilePath
y

-- | Split a library name into basename and a list of version numbers.
--
--   > versionView "foo-1.2.3"    == VersionView "foo" [1, 2, 3]
--   > versionView "foo-01.002.3" == VersionView "foo" [1, 2, 3]
--
--   Note that because of leading zeros, @versionView@ is not injective.
--   (@unVersionView . versionView@ would produce a normal form.)
versionView :: LibName -> VersionView
versionView :: FilePath -> VersionView
versionView FilePath
s =
  case (Char -> Bool) -> FilePath -> (FilePath, FilePath)
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\ Char
c -> Char -> Bool
isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.') (ShowS
forall a. [a] -> [a]
reverse FilePath
s) of
    (FilePath
v, Char
'-' : FilePath
x) | [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => [t a] -> Bool
valid [FilePath]
vs ->
      FilePath -> [Integer] -> VersionView
VersionView (ShowS
forall a. [a] -> [a]
reverse FilePath
x) ([Integer] -> VersionView) -> [Integer] -> VersionView
forall a b. (a -> b) -> a -> b
$ [Integer] -> [Integer]
forall a. [a] -> [a]
reverse ([Integer] -> [Integer]) -> [Integer] -> [Integer]
forall a b. (a -> b) -> a -> b
$ (FilePath -> Integer) -> [FilePath] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> Integer
forall a. Read a => FilePath -> a
read (FilePath -> Integer) -> ShowS -> FilePath -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse) [FilePath]
vs
      where vs :: [FilePath]
vs = (Char -> Bool) -> FilePath -> [FilePath]
forall a. (a -> Bool) -> [a] -> [[a]]
chopWhen (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.') FilePath
v
            valid :: [t a] -> Bool
valid [] = Bool
False
            valid [t a]
vs = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (t a -> Bool) -> [t a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [t a]
vs
    (FilePath, FilePath)
_ -> FilePath -> [Integer] -> VersionView
VersionView FilePath
s []

-- | Print a @VersionView@, inverse of @versionView@ (modulo leading zeros).
unVersionView :: VersionView -> LibName
unVersionView :: VersionView -> FilePath
unVersionView = \case
  VersionView FilePath
base [] -> FilePath
base
  VersionView FilePath
base [Integer]
vs -> FilePath
base FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"-" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
List.intercalate FilePath
"." ((Integer -> FilePath) -> [Integer] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> FilePath
forall a. Show a => a -> FilePath
show [Integer]
vs)

------------------------------------------------------------------------
-- * Prettyprinting errors and warnings
------------------------------------------------------------------------

formatLibPositionInfo :: LibPositionInfo -> String -> Doc
formatLibPositionInfo :: LibPositionInfo -> FilePath -> Doc
formatLibPositionInfo (LibPositionInfo Maybe FilePath
libFile Int
lineNum FilePath
file) FilePath
err = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$
  let loc :: FilePath
loc | Just FilePath
lf <- Maybe FilePath
libFile = FilePath
lf FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
":" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
lineNum FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
": "
          | Bool
otherwise = FilePath
""
  in if FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
List.isPrefixOf FilePath
"Failed to read" FilePath
err
     then FilePath
loc
     else FilePath
file FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
":" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ (if (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit (Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
1 FilePath
err) then FilePath
"" else FilePath
" ")

-- | Pretty-print 'LibError'.
formatLibError :: [AgdaLibFile] -> LibError -> Doc
formatLibError :: [AgdaLibFile] -> LibError -> Doc
formatLibError [AgdaLibFile]
installed (LibError Maybe LibPositionInfo
mc LibError'
e) = Doc
prefix Doc -> Doc -> Doc
<+> Doc
body where
  prefix :: Doc
prefix = case Maybe LibPositionInfo
mc of
    Maybe LibPositionInfo
Nothing                      -> Doc
""
    Just LibPositionInfo
c | OtherError FilePath
err <- LibError'
e -> LibPositionInfo -> FilePath -> Doc
formatLibPositionInfo LibPositionInfo
c FilePath
err
    Maybe LibPositionInfo
_                            -> Doc
""

  body :: Doc
body = case LibError'
e of
    LibNotFound LibrariesFile
file FilePath
lib -> [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      [ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"Library '" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
lib FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"' not found."
      , [Doc] -> Doc
sep [ Doc
"Add the path to its .agda-lib file to"
            , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"'" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ LibrariesFile -> FilePath
lfPath LibrariesFile
file FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"'"
            , Doc
"to install."
            ]
      , Doc
"Installed libraries:"
      ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++
      (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Doc -> Doc
nest Int
2)
         (if [AgdaLibFile] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AgdaLibFile]
installed then [Doc
"(none)"]
          else [ [Doc] -> Doc
sep [ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libName AgdaLibFile
l, Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libFile AgdaLibFile
l ]
               | AgdaLibFile
l <- [AgdaLibFile]
installed ])

    AmbiguousLib FilePath
lib [AgdaLibFile]
tgts -> [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      [ [Doc] -> Doc
sep [ FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"Ambiguous library '" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
lib FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"'."
            , Doc
"Could refer to any one of" ]
      ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [ Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text (AgdaLibFile -> FilePath
_libName AgdaLibFile
l) Doc -> Doc -> Doc
<+> Doc -> Doc
parens (FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libFile AgdaLibFile
l)
           | AgdaLibFile
l <- [AgdaLibFile]
tgts ]

    OtherError FilePath
err -> FilePath -> Doc
text FilePath
err

instance Pretty LibWarning where
  pretty :: LibWarning -> Doc
pretty (LibWarning LibPositionInfo
c LibWarning'
w) = LibPositionInfo -> FilePath -> Doc
formatLibPositionInfo LibPositionInfo
c FilePath
"" Doc -> Doc -> Doc
<+> LibWarning' -> Doc
forall a. Pretty a => a -> Doc
pretty LibWarning'
w

instance Pretty LibWarning' where
  pretty :: LibWarning' -> Doc
pretty (UnknownField FilePath
s) = FilePath -> Doc
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"Unknown field '" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"'"