-- | 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
  , getTrustedExecutables
  , libraryIncludePaths
  , getAgdaLibFiles'
  , getPrimitiveLibDir
  , LibName
  , AgdaLibFile(..)
  , ExeName
  , LibM
  , mkLibM
  , LibWarning(..)
  , LibPositionInfo(..)
  , libraryWarningName
  , ProjectConfig(..)
  -- * Exported for testing
  , VersionView(..), versionView, unVersionView
  , findLib'
  ) where

import Control.Arrow          ( first , second )
import Control.Monad          ( filterM, forM )
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Writer
import Control.Monad.IO.Class ( MonadIO(..) )

import Data.Char
import Data.Data ( Data )
import Data.Either
import Data.Function
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Maybe ( catMaybes, fromMaybe )
import qualified Data.List as List
import qualified Data.Text as T

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.FileName
import Agda.Utils.Functor ( (<&>) )
import Agda.Utils.IO ( catchIO )
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.List
import Agda.Utils.List1 ( List1 )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.String ( trim )

import Agda.Version

-- Paths_Agda.hs is in $(BUILD_DIR)/build/autogen/.
import Paths_Agda ( getDataFileName )

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

-- | 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 -> LibName
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 -> LibName
(Int -> VersionView -> ShowS)
-> (VersionView -> LibName)
-> ([VersionView] -> ShowS)
-> Show VersionView
forall a.
(Int -> a -> ShowS) -> (a -> LibName) -> ([a] -> ShowS) -> Show a
showList :: [VersionView] -> ShowS
$cshowList :: [VersionView] -> ShowS
show :: VersionView -> LibName
$cshow :: VersionView -> LibName
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) <- WriterT
  [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
-> ExceptT
     Doc
     (WriterT [LibWarning] (StateT LibState IO))
     (a, [Either LibError LibWarning])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT
   [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
 -> ExceptT
      Doc
      (WriterT [LibWarning] (StateT LibState IO))
      (a, [Either LibError LibWarning]))
-> WriterT
     [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
-> ExceptT
     Doc
     (WriterT [LibWarning] (StateT LibState IO))
     (a, [Either LibError LibWarning])
forall a b. (a -> b) -> a -> b
$ StateT LibState IO (a, [Either LibError LibWarning])
-> WriterT
     [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT LibState IO (a, [Either LibError LibWarning])
 -> WriterT
      [LibWarning]
      (StateT LibState IO)
      (a, [Either LibError LibWarning]))
-> StateT LibState IO (a, [Either LibError LibWarning])
-> WriterT
     [LibWarning] (StateT LibState IO) (a, [Either LibError LibWarning])
forall a b. (a -> b) -> a -> b
$ LibErrorIO a
-> StateT LibState 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] (StateT LibState IO)) ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [LibWarning]
warns
  Bool
-> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
-> ExceptT Doc (WriterT [LibWarning] (StateT LibState 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] (StateT LibState IO)) ()
 -> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ())
-> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
-> ExceptT Doc (WriterT [LibWarning] (StateT LibState IO)) ()
forall a b. (a -> b) -> a -> b
$ do
    let doc :: Doc
doc = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t 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] (StateT LibState 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

------------------------------------------------------------------------
-- * 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 LibName
getAgdaAppDir = do
  -- System-specific command to build the path to ~/.agda (Unix) or %APPDATA%\agda (Win)
  let agdaDir :: IO LibName
agdaDir = LibName -> IO LibName
getAppUserDataDirectory LibName
"agda"
  -- The default can be overwritten by setting the AGDA_DIR environment variable
  IO (Maybe LibName)
-> IO LibName -> (LibName -> IO LibName) -> IO LibName
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (LibName -> IO (Maybe LibName)
lookupEnv LibName
"AGDA_DIR") IO LibName
agdaDir ((LibName -> IO LibName) -> IO LibName)
-> (LibName -> IO LibName) -> IO LibName
forall a b. (a -> b) -> a -> b
$ \ LibName
dir ->
      IO Bool -> IO LibName -> IO LibName -> IO LibName
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (LibName -> IO Bool
doesDirectoryExist LibName
dir) (LibName -> IO LibName
canonicalizePath LibName
dir) (IO LibName -> IO LibName) -> IO LibName -> IO LibName
forall a b. (a -> b) -> a -> b
$ do
        LibName
d <- IO LibName
agdaDir
        LibName -> IO ()
putStrLn (LibName -> IO ()) -> LibName -> IO ()
forall a b. (a -> b) -> a -> b
$ LibName
"Warning: Environment variable AGDA_DIR points to non-existing directory " LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> LibName
show LibName
dir LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName
", using " LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> LibName
show LibName
d LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName
" instead."
        LibName -> IO LibName
forall (m :: * -> *) a. Monad m => a -> m a
return LibName
d

-- | Returns the absolute default lib dir. This directory is used to
-- store the Primitive.agda file.
getPrimitiveLibDir :: IO FilePath
getPrimitiveLibDir :: IO LibName
getPrimitiveLibDir = do
  LibName
libdir <- AbsolutePath -> LibName
filePath (AbsolutePath -> LibName) -> IO AbsolutePath -> IO LibName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LibName -> IO AbsolutePath
absolute (LibName -> IO AbsolutePath) -> IO LibName -> IO AbsolutePath
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< LibName -> IO LibName
getDataFileName LibName
"lib")
  IO Bool -> IO LibName -> IO LibName -> IO LibName
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (LibName -> IO Bool
doesDirectoryExist LibName
libdir)
      (LibName -> IO LibName
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName -> IO LibName) -> LibName -> IO LibName
forall a b. (a -> b) -> a -> b
$ LibName
libdir LibName -> ShowS
</> LibName
"prim")
      (LibName -> IO LibName
forall a. HasCallStack => LibName -> a
error (LibName -> IO LibName) -> LibName -> IO LibName
forall a b. (a -> b) -> a -> b
$ LibName
"The lib directory " LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName
libdir LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName
" does not exist")

-- | The @~/.agda/libraries@ file lists the libraries Agda should know about.
--   The content of @libraries@ is a list of paths 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 :: List1 FilePath
defaultLibraryFiles :: List1 LibName
defaultLibraryFiles = [LibName] -> List1 LibName
forall a. [a] -> NonEmpty a
List1.fromList [LibName
"libraries-" LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName
version, LibName
"libraries"]

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

-- | The @~/.agda/executables@ file lists the executables Agda should know about.
--   The content of @executables@ is a list of paths to executables.
--
--   Agda honors also version specific @executables@ files, e.g. @executables-2.6.0@.
--
--   @defaultExecutablesFiles@ gives a list of all @executables@ Agda should process
--   by default.
--
defaultExecutableFiles :: List1 FilePath
defaultExecutableFiles :: List1 LibName
defaultExecutableFiles = [LibName] -> List1 LibName
forall a. [a] -> NonEmpty a
List1.fromList [LibName
"executables-" LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName
version, LibName
"executables"]

------------------------------------------------------------------------
-- * 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)
  -> LibM ProjectConfig                -- ^ Actual root and @.agda-lib@ files for this project
findProjectConfig :: LibName -> LibM ProjectConfig
findProjectConfig LibName
root = [AgdaLibFile] -> LibErrorIO ProjectConfig -> LibM ProjectConfig
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO ProjectConfig -> LibM ProjectConfig)
-> LibErrorIO ProjectConfig -> LibM ProjectConfig
forall a b. (a -> b) -> a -> b
$ LibName -> LibErrorIO ProjectConfig
findProjectConfig' LibName
root

findProjectConfig'
  :: FilePath                          -- ^ Candidate (init: the directory Agda was called in)
  -> LibErrorIO ProjectConfig          -- ^ Actual root and @.agda-lib@ files for this project
findProjectConfig' :: LibName -> LibErrorIO ProjectConfig
findProjectConfig' LibName
root = do
  LibName
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Maybe ProjectConfig)
forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
LibName -> m (Maybe ProjectConfig)
getCachedProjectConfig LibName
root WriterT
  [Either LibError LibWarning]
  (StateT LibState IO)
  (Maybe ProjectConfig)
-> (Maybe ProjectConfig -> LibErrorIO ProjectConfig)
-> LibErrorIO ProjectConfig
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just ProjectConfig
conf -> ProjectConfig -> LibErrorIO ProjectConfig
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
conf
    Maybe ProjectConfig
Nothing   -> do
      [LibName]
libFiles <- IO [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [LibName]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [LibName])
-> IO [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall a b. (a -> b) -> a -> b
$ (LibName -> Bool) -> [LibName] -> [LibName]
forall a. (a -> Bool) -> [a] -> [a]
filter ((LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
".agda-lib") (LibName -> Bool) -> ShowS -> LibName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
takeExtension) ([LibName] -> [LibName]) -> IO [LibName] -> IO [LibName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> IO [LibName]
getDirectoryContents LibName
root
      case [LibName]
libFiles of
        []     -> IO (Maybe LibName)
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) (Maybe LibName)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (LibName -> IO (Maybe LibName)
upPath LibName
root) WriterT
  [Either LibError LibWarning] (StateT LibState IO) (Maybe LibName)
-> (Maybe LibName -> LibErrorIO ProjectConfig)
-> LibErrorIO ProjectConfig
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just LibName
up -> do
            ProjectConfig
conf <- LibName -> LibErrorIO ProjectConfig
findProjectConfig' LibName
up
            LibName
-> ProjectConfig
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
LibName -> ProjectConfig -> m ()
storeCachedProjectConfig LibName
root ProjectConfig
conf
            ProjectConfig -> LibErrorIO ProjectConfig
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
conf
          Maybe LibName
Nothing -> ProjectConfig -> LibErrorIO ProjectConfig
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
DefaultProjectConfig
        [LibName]
files -> do
          let conf :: ProjectConfig
conf = LibName -> [LibName] -> ProjectConfig
ProjectConfig LibName
root [LibName]
files
          LibName
-> ProjectConfig
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
LibName -> ProjectConfig -> m ()
storeCachedProjectConfig LibName
root ProjectConfig
conf
          ProjectConfig -> LibErrorIO ProjectConfig
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
conf

  where
    -- Note that "going up" one directory is OS dependent
    -- if the directory is a symlink.
    --
    -- Quoting from https://hackage.haskell.org/package/directory-1.3.6.1/docs/System-Directory.html#v:canonicalizePath :
    --
    --   Note that on Windows parent directories .. are always fully
    --   expanded before the symbolic links, as consistent with the
    --   rest of the Windows API (such as GetFullPathName). In
    --   contrast, on POSIX systems parent directories .. are
    --   expanded alongside symbolic links from left to right. To
    --   put this more concretely: if L is a symbolic link for R/P,
    --   then on Windows L\.. refers to ., whereas on other
    --   operating systems L/.. refers to R.
    upPath :: FilePath -> IO (Maybe FilePath)
    upPath :: LibName -> IO (Maybe LibName)
upPath LibName
root = do
      LibName
up <- LibName -> IO LibName
canonicalizePath (LibName -> IO LibName) -> LibName -> IO LibName
forall a b. (a -> b) -> a -> b
$ LibName
root LibName -> ShowS
</> LibName
".."
      if LibName
up LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
root then Maybe LibName -> IO (Maybe LibName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe LibName
forall a. Maybe a
Nothing else Maybe LibName -> IO (Maybe LibName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe LibName -> IO (Maybe LibName))
-> Maybe LibName -> IO (Maybe LibName)
forall a b. (a -> b) -> a -> b
$ LibName -> Maybe LibName
forall a. a -> Maybe a
Just LibName
up


-- | Get project root

findProjectRoot :: FilePath -> LibM (Maybe FilePath)
findProjectRoot :: LibName -> LibM (Maybe LibName)
findProjectRoot LibName
root = LibName -> LibM ProjectConfig
findProjectConfig LibName
root LibM ProjectConfig
-> (ProjectConfig -> Maybe LibName) -> LibM (Maybe LibName)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
  ProjectConfig LibName
p [LibName]
_    -> LibName -> Maybe LibName
forall a. a -> Maybe a
Just LibName
p
  ProjectConfig
DefaultProjectConfig -> Maybe LibName
forall a. Maybe a
Nothing


-- | Get the contents of @.agda-lib@ files in the given project root.
getAgdaLibFiles' :: FilePath -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' :: LibName -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' LibName
path = LibName -> LibErrorIO ProjectConfig
findProjectConfig' LibName
path LibErrorIO ProjectConfig
-> (ProjectConfig -> LibErrorIO [AgdaLibFile])
-> LibErrorIO [AgdaLibFile]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  ProjectConfig
DefaultProjectConfig    -> [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  ProjectConfig LibName
root [LibName]
libs -> Maybe LibrariesFile -> [(Int, LibName)] -> LibErrorIO [AgdaLibFile]
parseLibFiles Maybe LibrariesFile
forall a. Maybe a
Nothing ([(Int, LibName)] -> LibErrorIO [AgdaLibFile])
-> [(Int, LibName)] -> LibErrorIO [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ (LibName -> (Int, LibName)) -> [LibName] -> [(Int, LibName)]
forall a b. (a -> b) -> [a] -> [b]
map ((Int
0,) (LibName -> (Int, LibName)) -> ShowS -> LibName -> (Int, LibName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LibName
root LibName -> ShowS
</>)) [LibName]
libs

-- | 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 :: LibName -> Bool -> LibM ([LibName], [LibName])
getDefaultLibraries LibName
root Bool
optDefaultLibs = [AgdaLibFile]
-> LibErrorIO ([LibName], [LibName]) -> LibM ([LibName], [LibName])
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO ([LibName], [LibName]) -> LibM ([LibName], [LibName]))
-> LibErrorIO ([LibName], [LibName]) -> LibM ([LibName], [LibName])
forall a b. (a -> b) -> a -> b
$ do
  [AgdaLibFile]
libs <- LibName -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' LibName
root
  if [AgdaLibFile] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AgdaLibFile]
libs
    then (,[]) ([LibName] -> ([LibName], [LibName]))
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> LibErrorIO ([LibName], [LibName])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if Bool
optDefaultLibs then (LibName
libNameForCurrentDir LibName -> [LibName] -> [LibName]
forall a. a -> [a] -> [a]
:) ([LibName] -> [LibName])
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT [Either LibError LibWarning] (StateT LibState IO) [LibName]
readDefaultsFile else [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (m :: * -> *) a. Monad m => a -> m a
return []
    else ([LibName], [LibName]) -> LibErrorIO ([LibName], [LibName])
forall (m :: * -> *) a. Monad m => a -> m a
return (([LibName], [LibName]) -> LibErrorIO ([LibName], [LibName]))
-> ([LibName], [LibName]) -> LibErrorIO ([LibName], [LibName])
forall a b. (a -> b) -> a -> b
$ [AgdaLibFile] -> ([LibName], [LibName])
forall (t :: * -> *).
Foldable t =>
t AgdaLibFile -> ([LibName], [LibName])
libsAndPaths [AgdaLibFile]
libs
  where
    libsAndPaths :: t AgdaLibFile -> ([LibName], [LibName])
libsAndPaths t AgdaLibFile
ls = ( (AgdaLibFile -> [LibName]) -> t AgdaLibFile -> [LibName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [LibName]
_libDepends t AgdaLibFile
ls
                      , ShowS -> [LibName] -> [LibName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn ShowS
forall a. a -> a
id ((AgdaLibFile -> [LibName]) -> t AgdaLibFile -> [LibName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [LibName]
_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] (StateT LibState IO) [LibName]
readDefaultsFile = do
    LibName
agdaDir <- IO LibName
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) LibName
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO LibName
getAgdaAppDir
    let file :: LibName
file = LibName
agdaDir LibName -> ShowS
</> LibName
defaultsFile
    WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (IO Bool
-> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool
 -> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool)
-> IO Bool
-> WriterT [Either LibError LibWarning] (StateT LibState IO) Bool
forall a b. (a -> b) -> a -> b
$ LibName -> IO Bool
doesFileExist LibName
file) ([LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (m :: * -> *) a. Monad m => a -> m a
return []) (WriterT
   [Either LibError LibWarning] (StateT LibState IO) [LibName]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [LibName])
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall a b. (a -> b) -> a -> b
$ {-else-} do
      [LibName]
ls <- IO [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [LibName]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [LibName])
-> IO [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall a b. (a -> b) -> a -> b
$ ((Int, LibName) -> LibName) -> [(Int, LibName)] -> [LibName]
forall a b. (a -> b) -> [a] -> [b]
map (Int, LibName) -> LibName
forall a b. (a, b) -> b
snd ([(Int, LibName)] -> [LibName])
-> (LibName -> [(Int, LibName)]) -> LibName -> [LibName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> [(Int, LibName)]
stripCommentLines (LibName -> [LibName]) -> IO LibName -> IO [LibName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> IO LibName
UTF8.readFile LibName
file
      [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (m :: * -> *) a. Monad m => a -> m a
return ([LibName]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [LibName])
-> [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall a b. (a -> b) -> a -> b
$ (LibName -> [LibName]) -> [LibName] -> [LibName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LibName -> [LibName]
splitCommas [LibName]
ls
  WriterT [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> (IOException
    -> WriterT
         [Either LibError LibWarning] (StateT LibState IO) [LibName])
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    [LibError']
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [ LibName -> LibError'
OtherError (LibName -> LibError') -> LibName -> LibError'
forall a b. (a -> b) -> a -> b
$ [LibName] -> LibName
unlines [LibName
"Failed to read defaults file.", IOException -> LibName
forall a. Show a => a -> LibName
show IOException
e] ]
    [LibName]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
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
  :: (MonadIO m, MonadError String m)
  => Maybe FilePath -- ^ Override the default @libraries@ file?
  -> m LibrariesFile
getLibrariesFile :: Maybe LibName -> m LibrariesFile
getLibrariesFile (Just LibName
overrideLibFile) = do
  -- A user-specified override file must exist.
  m Bool -> m LibrariesFile -> m LibrariesFile -> m LibrariesFile
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (IO Bool -> m Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> m Bool) -> IO Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ LibName -> IO Bool
doesFileExist LibName
overrideLibFile)
    {-then-} (LibrariesFile -> m LibrariesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> m LibrariesFile)
-> LibrariesFile -> m LibrariesFile
forall a b. (a -> b) -> a -> b
$ LibName -> Bool -> LibrariesFile
LibrariesFile LibName
overrideLibFile Bool
True)
    {-else-} (LibName -> m LibrariesFile
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LibName -> m LibrariesFile) -> LibName -> m LibrariesFile
forall a b. (a -> b) -> a -> b
$ LibName
"Libraries file not found: " LibName -> ShowS
forall a. [a] -> [a] -> [a]
++ LibName
overrideLibFile)
getLibrariesFile Maybe LibName
Nothing = do
  LibName
agdaDir <- IO LibName -> m LibName
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO LibName -> m LibName) -> IO LibName -> m LibName
forall a b. (a -> b) -> a -> b
$ IO LibName
getAgdaAppDir
  let defaults :: List1 LibName
defaults = ShowS -> List1 LibName -> List1 LibName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map (LibName
agdaDir LibName -> ShowS
</>) List1 LibName
defaultLibraryFiles -- NB: very short list
  [LibName]
files <- IO [LibName] -> m [LibName]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [LibName] -> m [LibName]) -> IO [LibName] -> m [LibName]
forall a b. (a -> b) -> a -> b
$ (LibName -> IO Bool) -> [LibName] -> IO [LibName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM LibName -> IO Bool
doesFileExist (List1 LibName -> [LibName]
forall a. NonEmpty a -> [a]
List1.toList List1 LibName
defaults)
  case [LibName]
files of
    LibName
file : [LibName]
_ -> LibrariesFile -> m LibrariesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> m LibrariesFile)
-> LibrariesFile -> m LibrariesFile
forall a b. (a -> b) -> a -> b
$ LibName -> Bool -> LibrariesFile
LibrariesFile LibName
file Bool
True
    []       -> LibrariesFile -> m LibrariesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> m LibrariesFile)
-> LibrariesFile -> m LibrariesFile
forall a b. (a -> b) -> a -> b
$ LibName -> Bool -> LibrariesFile
LibrariesFile (List1 LibName -> LibName
forall a. NonEmpty a -> a
List1.last List1 LibName
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 LibName -> LibM [AgdaLibFile]
getInstalledLibraries Maybe LibName
overrideLibFile = [AgdaLibFile] -> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile])
-> LibErrorIO [AgdaLibFile] -> LibM [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ do
    Either LibName LibrariesFile
filem <- IO (Either LibName LibrariesFile)
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either LibName LibrariesFile)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either LibName LibrariesFile)
 -> WriterT
      [Either LibError LibWarning]
      (StateT LibState IO)
      (Either LibName LibrariesFile))
-> IO (Either LibName LibrariesFile)
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either LibName LibrariesFile)
forall a b. (a -> b) -> a -> b
$ ExceptT LibName IO LibrariesFile
-> IO (Either LibName LibrariesFile)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT LibName IO LibrariesFile
 -> IO (Either LibName LibrariesFile))
-> ExceptT LibName IO LibrariesFile
-> IO (Either LibName LibrariesFile)
forall a b. (a -> b) -> a -> b
$ Maybe LibName -> ExceptT LibName IO LibrariesFile
forall (m :: * -> *).
(MonadIO m, MonadError LibName m) =>
Maybe LibName -> m LibrariesFile
getLibrariesFile Maybe LibName
overrideLibFile
    case Either LibName LibrariesFile
filem of
      Left LibName
err -> [LibError']
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [LibName -> LibError'
OtherError LibName
err] WriterT [Either LibError LibWarning] (StateT LibState IO) ()
-> LibErrorIO [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Right LibrariesFile
file -> do
        if Bool -> Bool
not (LibrariesFile -> Bool
lfExists LibrariesFile
file) then [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
          [(Int, LibName)]
ls    <- IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(Int, LibName)]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)])
-> IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall a b. (a -> b) -> a -> b
$ LibName -> [(Int, LibName)]
stripCommentLines (LibName -> [(Int, LibName)]) -> IO LibName -> IO [(Int, LibName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> IO LibName
UTF8.readFile (LibrariesFile -> LibName
lfPath LibrariesFile
file)
          [(Int, LibName)]
files <- IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(Int, LibName)]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)])
-> IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall a b. (a -> b) -> a -> b
$ [IO (Int, LibName)] -> IO [(Int, LibName)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Int
i, ) (LibName -> (Int, LibName)) -> IO LibName -> IO (Int, LibName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> IO LibName
expandEnvironmentVariables LibName
s | (Int
i, LibName
s) <- [(Int, LibName)]
ls ]
          Maybe LibrariesFile -> [(Int, LibName)] -> LibErrorIO [AgdaLibFile]
parseLibFiles (LibrariesFile -> Maybe LibrariesFile
forall a. a -> Maybe a
Just LibrariesFile
file) ([(Int, LibName)] -> LibErrorIO [AgdaLibFile])
-> [(Int, LibName)] -> LibErrorIO [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ ((Int, LibName) -> LibName) -> [(Int, LibName)] -> [(Int, LibName)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (Int, LibName) -> LibName
forall a b. (a, b) -> b
snd [(Int, LibName)]
files
  LibErrorIO [AgdaLibFile]
-> (IOException -> LibErrorIO [AgdaLibFile])
-> LibErrorIO [AgdaLibFile]
forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    [LibError']
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [ LibName -> LibError'
OtherError (LibName -> LibError') -> LibName -> LibError'
forall a b. (a -> b) -> a -> b
$ [LibName] -> LibName
unlines [LibName
"Failed to read installed libraries.", IOException -> LibName
forall a. Show a => a -> LibName
show IOException
e] ]
    [AgdaLibFile] -> LibErrorIO [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, LibName)] -> LibErrorIO [AgdaLibFile]
parseLibFiles Maybe LibrariesFile
mlibFile [(Int, LibName)]
files = do

  [(Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
  [LibWarning])]
anns <- [(Int, LibName)]
-> ((Int, LibName)
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
          [LibWarning]))
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     [(Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
       [LibWarning])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, LibName)]
files (((Int, LibName)
  -> WriterT
       [Either LibError LibWarning]
       (StateT LibState IO)
       (Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
        [LibWarning]))
 -> WriterT
      [Either LibError LibWarning]
      (StateT LibState IO)
      [(Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
        [LibWarning])])
-> ((Int, LibName)
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
          [LibWarning]))
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     [(Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
       [LibWarning])]
forall a b. (a -> b) -> a -> b
$ \(Int
ln, LibName
file) -> do
    LibName
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Maybe AgdaLibFile)
forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
LibName -> m (Maybe AgdaLibFile)
getCachedAgdaLibFile LibName
file WriterT
  [Either LibError LibWarning]
  (StateT LibState IO)
  (Maybe AgdaLibFile)
-> (Maybe AgdaLibFile
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
          [LibWarning]))
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either (Maybe LibPositionInfo, LibName) AgdaLibFile, [LibWarning])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just AgdaLibFile
lib -> (Either (Maybe LibPositionInfo, LibName) AgdaLibFile, [LibWarning])
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either (Maybe LibPositionInfo, LibName) AgdaLibFile, [LibWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return (AgdaLibFile -> Either (Maybe LibPositionInfo, LibName) AgdaLibFile
forall a b. b -> Either a b
Right AgdaLibFile
lib, [])
      Maybe AgdaLibFile
Nothing  -> do
        (Either LibName AgdaLibFile
e, [LibWarning']
ws) <- IO (Either LibName AgdaLibFile, [LibWarning'])
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either LibName AgdaLibFile, [LibWarning'])
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either LibName AgdaLibFile, [LibWarning'])
 -> WriterT
      [Either LibError LibWarning]
      (StateT LibState IO)
      (Either LibName AgdaLibFile, [LibWarning']))
-> IO (Either LibName AgdaLibFile, [LibWarning'])
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either LibName AgdaLibFile, [LibWarning'])
forall a b. (a -> b) -> a -> b
$ P AgdaLibFile -> (Either LibName AgdaLibFile, [LibWarning'])
forall a. P a -> (Either LibName a, [LibWarning'])
runP (P AgdaLibFile -> (Either LibName AgdaLibFile, [LibWarning']))
-> IO (P AgdaLibFile)
-> IO (Either LibName AgdaLibFile, [LibWarning'])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> IO (P AgdaLibFile)
parseLibFile LibName
file
        let pos :: LibPositionInfo
pos = Maybe LibName -> Int -> LibName -> LibPositionInfo
LibPositionInfo (LibrariesFile -> LibName
lfPath (LibrariesFile -> LibName) -> Maybe LibrariesFile -> Maybe LibName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe LibrariesFile
mlibFile) Int
ln LibName
file
            ws' :: [LibWarning]
ws' = (LibWarning' -> LibWarning) -> [LibWarning'] -> [LibWarning]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe LibPositionInfo -> LibWarning' -> LibWarning
LibWarning (LibPositionInfo -> Maybe LibPositionInfo
forall a. a -> Maybe a
Just LibPositionInfo
pos)) [LibWarning']
ws
        case Either LibName AgdaLibFile
e of
          Left LibName
err -> do
            (Either (Maybe LibPositionInfo, LibName) AgdaLibFile, [LibWarning])
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either (Maybe LibPositionInfo, LibName) AgdaLibFile, [LibWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Maybe LibPositionInfo, LibName)
-> Either (Maybe LibPositionInfo, LibName) AgdaLibFile
forall a b. a -> Either a b
Left (LibPositionInfo -> Maybe LibPositionInfo
forall a. a -> Maybe a
Just LibPositionInfo
pos, LibName
err), [LibWarning]
ws')
          Right AgdaLibFile
lib -> do
            LibName
-> AgdaLibFile
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
LibName -> AgdaLibFile -> m ()
storeCachedAgdaLibFile LibName
file AgdaLibFile
lib
            (Either (Maybe LibPositionInfo, LibName) AgdaLibFile, [LibWarning])
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Either (Maybe LibPositionInfo, LibName) AgdaLibFile, [LibWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return (AgdaLibFile -> Either (Maybe LibPositionInfo, LibName) AgdaLibFile
forall a b. b -> Either a b
Right AgdaLibFile
lib, [LibWarning]
ws')

  let ([Either (Maybe LibPositionInfo, LibName) AgdaLibFile]
xs, [[LibWarning]]
warns) = [(Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
  [LibWarning])]
-> ([Either (Maybe LibPositionInfo, LibName) AgdaLibFile],
    [[LibWarning]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Either (Maybe LibPositionInfo, LibName) AgdaLibFile,
  [LibWarning])]
anns
      ([(Maybe LibPositionInfo, LibName)]
errs, [AgdaLibFile]
als) = [Either (Maybe LibPositionInfo, LibName) AgdaLibFile]
-> ([(Maybe LibPositionInfo, LibName)], [AgdaLibFile])
forall a b. [Either a b] -> ([a], [b])
partitionEithers [Either (Maybe LibPositionInfo, LibName) AgdaLibFile]
xs

  Bool
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
-> WriterT [Either LibError LibWarning] (StateT LibState 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] (StateT LibState IO) ()
 -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall a b. (a -> b) -> a -> b
$ [LibWarning]
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibWarning] -> m ()
warnings ([LibWarning]
 -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
-> [LibWarning]
-> WriterT [Either LibError LibWarning] (StateT LibState 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] (StateT LibState IO) ()
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Maybe LibPositionInfo, LibName)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Maybe LibPositionInfo, LibName)]
errs)  (WriterT [Either LibError LibWarning] (StateT LibState IO) ()
 -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall a b. (a -> b) -> a -> b
$
    [LibError]
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError] -> m ()
raiseErrors ([LibError]
 -> WriterT [Either LibError LibWarning] (StateT LibState IO) ())
-> [LibError]
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall a b. (a -> b) -> a -> b
$ ((Maybe LibPositionInfo, LibName) -> LibError)
-> [(Maybe LibPositionInfo, LibName)] -> [LibError]
forall a b. (a -> b) -> [a] -> [b]
map (\(Maybe LibPositionInfo
mc,LibName
s) -> Maybe LibPositionInfo -> LibError' -> LibError
LibError Maybe LibPositionInfo
mc (LibError' -> LibError) -> LibError' -> LibError
forall a b. (a -> b) -> a -> b
$ LibName -> LibError'
OtherError LibName
s) [(Maybe LibPositionInfo, LibName)]
errs

  [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall (m :: * -> *) a. Monad m => a -> m a
return ([AgdaLibFile] -> LibErrorIO [AgdaLibFile])
-> [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ (AgdaLibFile -> LibName) -> [AgdaLibFile] -> [AgdaLibFile]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn AgdaLibFile -> LibName
_libFile [AgdaLibFile]
als

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

-- | Returns the path of the @executables@ file which lists the trusted executables Agda knows about.
--
--   Note: file may not exist.
--
getExecutablesFile
  :: IO ExecutablesFile
getExecutablesFile :: IO ExecutablesFile
getExecutablesFile = do
  LibName
agdaDir <- IO LibName
getAgdaAppDir
  let defaults :: List1 LibName
defaults = ShowS -> List1 LibName -> List1 LibName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map (LibName
agdaDir LibName -> ShowS
</>) List1 LibName
defaultExecutableFiles  -- NB: very short list
  [LibName]
files <- (LibName -> IO Bool) -> [LibName] -> IO [LibName]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM LibName -> IO Bool
doesFileExist (List1 LibName -> [LibName]
forall a. NonEmpty a -> [a]
List1.toList List1 LibName
defaults)
  case [LibName]
files of
    LibName
file : [LibName]
_ -> ExecutablesFile -> IO ExecutablesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecutablesFile -> IO ExecutablesFile)
-> ExecutablesFile -> IO ExecutablesFile
forall a b. (a -> b) -> a -> b
$ LibName -> Bool -> ExecutablesFile
ExecutablesFile LibName
file Bool
True
    []       -> ExecutablesFile -> IO ExecutablesFile
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecutablesFile -> IO ExecutablesFile)
-> ExecutablesFile -> IO ExecutablesFile
forall a b. (a -> b) -> a -> b
$ LibName -> Bool -> ExecutablesFile
ExecutablesFile (List1 LibName -> LibName
forall a. NonEmpty a -> a
List1.last List1 LibName
defaults) Bool
False -- doesn't exist, but that's ok

-- | Return the trusted executables Agda knows about.
--
--   Returns none if there is no @executables@ file.
--
getTrustedExecutables
  :: LibM (Map ExeName FilePath)  -- ^ Content of @executables@ files.
getTrustedExecutables :: LibM (Map ExeName LibName)
getTrustedExecutables = [AgdaLibFile]
-> LibErrorIO (Map ExeName LibName) -> LibM (Map ExeName LibName)
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO (Map ExeName LibName) -> LibM (Map ExeName LibName))
-> LibErrorIO (Map ExeName LibName) -> LibM (Map ExeName LibName)
forall a b. (a -> b) -> a -> b
$ do
    ExecutablesFile
file <- IO ExecutablesFile
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) ExecutablesFile
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ExecutablesFile
getExecutablesFile
    if Bool -> Bool
not (ExecutablesFile -> Bool
efExists ExecutablesFile
file) then Map ExeName LibName -> LibErrorIO (Map ExeName LibName)
forall (m :: * -> *) a. Monad m => a -> m a
return Map ExeName LibName
forall k a. Map k a
Map.empty else do
      [(Int, LibName)]
es    <- IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(Int, LibName)]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)])
-> IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall a b. (a -> b) -> a -> b
$ LibName -> [(Int, LibName)]
stripCommentLines (LibName -> [(Int, LibName)]) -> IO LibName -> IO [(Int, LibName)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> IO LibName
UTF8.readFile (ExecutablesFile -> LibName
efPath ExecutablesFile
file)
      [(Int, LibName)]
files <- IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(Int, LibName)]
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)])
-> IO [(Int, LibName)]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [(Int, LibName)]
forall a b. (a -> b) -> a -> b
$ [IO (Int, LibName)] -> IO [(Int, LibName)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Int
i, ) (LibName -> (Int, LibName)) -> IO LibName -> IO (Int, LibName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> IO LibName
expandEnvironmentVariables LibName
s | (Int
i, LibName
s) <- [(Int, LibName)]
es ]
      Map ExeName LibName
tmp   <- ExecutablesFile
-> [(Int, LibName)] -> LibErrorIO (Map ExeName LibName)
parseExecutablesFile ExecutablesFile
file ([(Int, LibName)] -> LibErrorIO (Map ExeName LibName))
-> [(Int, LibName)] -> LibErrorIO (Map ExeName LibName)
forall a b. (a -> b) -> a -> b
$ ((Int, LibName) -> LibName) -> [(Int, LibName)] -> [(Int, LibName)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (Int, LibName) -> LibName
forall a b. (a, b) -> b
snd [(Int, LibName)]
files
      Map ExeName LibName -> LibErrorIO (Map ExeName LibName)
forall (m :: * -> *) a. Monad m => a -> m a
return Map ExeName LibName
tmp
  LibErrorIO (Map ExeName LibName)
-> (IOException -> LibErrorIO (Map ExeName LibName))
-> LibErrorIO (Map ExeName LibName)
forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    [LibError']
-> WriterT [Either LibError LibWarning] (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter [Either LibError LibWarning] m =>
[LibError'] -> m ()
raiseErrors' [ LibName -> LibError'
OtherError (LibName -> LibError') -> LibName -> LibError'
forall a b. (a -> b) -> a -> b
$ [LibName] -> LibName
unlines [LibName
"Failed to read trusted executables.", IOException -> LibName
forall a. Show a => a -> LibName
show IOException
e] ]
    Map ExeName LibName -> LibErrorIO (Map ExeName LibName)
forall (m :: * -> *) a. Monad m => a -> m a
return Map ExeName LibName
forall k a. Map k a
Map.empty

-- | Parse the @executables@ file.
--
parseExecutablesFile
  :: ExecutablesFile
  -> [(LineNumber, FilePath)]
  -> LibErrorIO (Map ExeName FilePath)
parseExecutablesFile :: ExecutablesFile
-> [(Int, LibName)] -> LibErrorIO (Map ExeName LibName)
parseExecutablesFile ExecutablesFile
ef [(Int, LibName)]
files =
  ([Maybe (ExeName, LibName)] -> Map ExeName LibName)
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     [Maybe (ExeName, LibName)]
-> LibErrorIO (Map ExeName LibName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(ExeName, LibName)] -> Map ExeName LibName
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(ExeName, LibName)] -> Map ExeName LibName)
-> ([Maybe (ExeName, LibName)] -> [(ExeName, LibName)])
-> [Maybe (ExeName, LibName)]
-> Map ExeName LibName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (ExeName, LibName)] -> [(ExeName, LibName)]
forall a. [Maybe a] -> [a]
catMaybes) (WriterT
   [Either LibError LibWarning]
   (StateT LibState IO)
   [Maybe (ExeName, LibName)]
 -> LibErrorIO (Map ExeName LibName))
-> (((Int, LibName)
     -> WriterT
          [Either LibError LibWarning]
          (StateT LibState IO)
          (Maybe (ExeName, LibName)))
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         [Maybe (ExeName, LibName)])
-> ((Int, LibName)
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Maybe (ExeName, LibName)))
-> LibErrorIO (Map ExeName LibName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, LibName)]
-> ((Int, LibName)
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Maybe (ExeName, LibName)))
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     [Maybe (ExeName, LibName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Int, LibName)]
files (((Int, LibName)
  -> WriterT
       [Either LibError LibWarning]
       (StateT LibState IO)
       (Maybe (ExeName, LibName)))
 -> LibErrorIO (Map ExeName LibName))
-> ((Int, LibName)
    -> WriterT
         [Either LibError LibWarning]
         (StateT LibState IO)
         (Maybe (ExeName, LibName)))
-> LibErrorIO (Map ExeName LibName)
forall a b. (a -> b) -> a -> b
$ \(Int
ln, LibName
fp) -> do

    -- Compute canonical executable name and absolute filepath.
    let strExeName :: LibName
strExeName  = ShowS
takeFileName LibName
fp
    let strExeName' :: LibName
strExeName' = LibName -> Maybe LibName -> LibName
forall a. a -> Maybe a -> a
fromMaybe LibName
strExeName (Maybe LibName -> LibName) -> Maybe LibName -> LibName
forall a b. (a -> b) -> a -> b
$ LibName -> LibName -> Maybe LibName
stripExtension LibName
exeExtension LibName
strExeName
    let txtExeName :: ExeName
txtExeName  = LibName -> ExeName
T.pack LibName
strExeName'
    LibName
exePath <- IO LibName
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) LibName
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO LibName
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) LibName)
-> IO LibName
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) LibName
forall a b. (a -> b) -> a -> b
$ LibName -> IO LibName
makeAbsolute LibName
fp
    Maybe (ExeName, LibName)
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Maybe (ExeName, LibName))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (ExeName, LibName)
 -> WriterT
      [Either LibError LibWarning]
      (StateT LibState IO)
      (Maybe (ExeName, LibName)))
-> Maybe (ExeName, LibName)
-> WriterT
     [Either LibError LibWarning]
     (StateT LibState IO)
     (Maybe (ExeName, LibName))
forall a b. (a -> b) -> a -> b
$ (ExeName, LibName) -> Maybe (ExeName, LibName)
forall a. a -> Maybe a
Just (ExeName
txtExeName, LibName
exePath)

------------------------------------------------------------------------
-- * 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 LibName -> [AgdaLibFile] -> [LibName] -> LibM [LibName]
libraryIncludePaths Maybe LibName
overrideLibFile [AgdaLibFile]
libs [LibName]
xs0 = [AgdaLibFile]
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> LibM [LibName]
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [AgdaLibFile]
libs (WriterT
   [Either LibError LibWarning] (StateT LibState IO) [LibName]
 -> LibM [LibName])
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
-> LibM [LibName]
forall a b. (a -> b) -> a -> b
$ StateT LibState IO ([LibName], [Either LibError LibWarning])
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (StateT LibState IO ([LibName], [Either LibError LibWarning])
 -> WriterT
      [Either LibError LibWarning] (StateT LibState IO) [LibName])
-> StateT LibState IO ([LibName], [Either LibError LibWarning])
-> WriterT
     [Either LibError LibWarning] (StateT LibState IO) [LibName]
forall a b. (a -> b) -> a -> b
$ do
    Either LibName LibrariesFile
efile <- IO (Either LibName LibrariesFile)
-> StateT LibState IO (Either LibName LibrariesFile)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either LibName LibrariesFile)
 -> StateT LibState IO (Either LibName LibrariesFile))
-> IO (Either LibName LibrariesFile)
-> StateT LibState IO (Either LibName LibrariesFile)
forall a b. (a -> b) -> a -> b
$ ExceptT LibName IO LibrariesFile
-> IO (Either LibName LibrariesFile)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT LibName IO LibrariesFile
 -> IO (Either LibName LibrariesFile))
-> ExceptT LibName IO LibrariesFile
-> IO (Either LibName LibrariesFile)
forall a b. (a -> b) -> a -> b
$ Maybe LibName -> ExceptT LibName IO LibrariesFile
forall (m :: * -> *).
(MonadIO m, MonadError LibName m) =>
Maybe LibName -> m LibrariesFile
getLibrariesFile Maybe LibName
overrideLibFile
    case Either LibName LibrariesFile
efile of
      Left LibName
err -> ([LibName], [Either LibError LibWarning])
-> StateT LibState IO ([LibName], [Either LibError LibWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [LibError -> Either LibError LibWarning
forall a b. a -> Either a b
Left (LibError -> Either LibError LibWarning)
-> LibError -> Either LibError LibWarning
forall a b. (a -> b) -> a -> b
$ Maybe LibPositionInfo -> LibError' -> LibError
LibError Maybe LibPositionInfo
forall a. Maybe a
Nothing (LibError' -> LibError) -> LibError' -> LibError
forall a b. (a -> b) -> a -> b
$ LibName -> LibError'
OtherError LibName
err])
      Right LibrariesFile
file -> ([LibName], [Either LibError LibWarning])
-> StateT LibState IO ([LibName], [Either LibError LibWarning])
forall (m :: * -> *) a. Monad m => a -> m a
return (([LibName], [Either LibError LibWarning])
 -> StateT LibState IO ([LibName], [Either LibError LibWarning]))
-> ([LibName], [Either LibError LibWarning])
-> StateT LibState IO ([LibName], [Either LibError LibWarning])
forall a b. (a -> b) -> a -> b
$ Writer [Either LibError LibWarning] [LibName]
-> ([LibName], [Either LibError LibWarning])
forall w a. Writer w a -> (a, w)
runWriter (Writer [Either LibError LibWarning] [LibName]
 -> ([LibName], [Either LibError LibWarning]))
-> Writer [Either LibError LibWarning] [LibName]
-> ([LibName], [Either LibError LibWarning])
forall a b. (a -> b) -> a -> b
$ ([LibName]
dot [LibName] -> [LibName] -> [LibName]
forall a. [a] -> [a] -> [a]
++) ([LibName] -> [LibName])
-> ([AgdaLibFile] -> [LibName]) -> [AgdaLibFile] -> [LibName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [AgdaLibFile] -> [LibName]
incs ([AgdaLibFile] -> [LibName])
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
-> Writer [Either LibError LibWarning] [LibName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibrariesFile
-> [LibName]
-> [LibName]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
file [] [LibName]
xs
  where
    ([LibName]
dots, [LibName]
xs) = (LibName -> Bool) -> [LibName] -> ([LibName], [LibName])
forall a. (a -> Bool) -> [a] -> ([a], [a])
List.partition (LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
libNameForCurrentDir) ([LibName] -> ([LibName], [LibName]))
-> [LibName] -> ([LibName], [LibName])
forall a b. (a -> b) -> a -> b
$ ShowS -> [LibName] -> [LibName]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
trim [LibName]
xs0
    incs :: [AgdaLibFile] -> [LibName]
incs       = ShowS -> [LibName] -> [LibName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn ShowS
forall a. a -> a
id ([LibName] -> [LibName])
-> ([AgdaLibFile] -> [LibName]) -> [AgdaLibFile] -> [LibName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AgdaLibFile -> [LibName]) -> [AgdaLibFile] -> [LibName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [LibName]
_libIncludes
    dot :: [LibName]
dot        = [ LibName
"." | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [LibName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LibName]
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
-> [LibName]
-> [LibName]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
_ [LibName]
_ [] = [AgdaLibFile]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    find LibrariesFile
file [LibName]
visited (LibName
x : [LibName]
xs)
      | LibName
x LibName -> [LibName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [LibName]
visited = LibrariesFile
-> [LibName]
-> [LibName]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
file [LibName]
visited [LibName]
xs
      | Bool
otherwise = do
          -- May or may not find the library
          Maybe AgdaLibFile
ml <- case LibName -> [AgdaLibFile] -> [AgdaLibFile]
findLib LibName
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 -> LibName -> LibError'
LibNotFound LibrariesFile
file LibName
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' [LibName -> [AgdaLibFile] -> LibError'
AmbiguousLib LibName
x [AgdaLibFile]
ls]
          -- If it is found, add its dependencies to work list
          let xs' :: [LibName]
xs' = (AgdaLibFile -> [LibName]) -> Maybe AgdaLibFile -> [LibName]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap AgdaLibFile -> [LibName]
_libDepends Maybe AgdaLibFile
ml [LibName] -> [LibName] -> [LibName]
forall a. [a] -> [a] -> [a]
++ [LibName]
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
-> [LibName]
-> [LibName]
-> WriterT [Either LibError LibWarning] Identity [AgdaLibFile]
find LibrariesFile
file (LibName
x LibName -> [LibName] -> [LibName]
forall a. a -> [a] -> [a]
: [LibName]
visited) [LibName]
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 :: LibName -> [AgdaLibFile] -> [AgdaLibFile]
findLib = (AgdaLibFile -> LibName)
-> LibName -> [AgdaLibFile] -> [AgdaLibFile]
forall a. (a -> LibName) -> LibName -> [a] -> [a]
findLib' AgdaLibFile -> LibName
_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 -> LibName) -> LibName -> [a] -> [a]
findLib' a -> LibName
libName LibName
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 (((LibName, Bool, [Integer]) -> (LibName, Bool, [Integer]) -> Bool
forall a. Eq a => a -> a -> Bool
(==) ((LibName, Bool, [Integer]) -> (LibName, Bool, [Integer]) -> Bool)
-> (a -> (LibName, Bool, [Integer])) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> (LibName, 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 (((LibName, Bool, [Integer])
 -> (LibName, Bool, [Integer]) -> Ordering)
-> (LibName, Bool, [Integer])
-> (LibName, Bool, [Integer])
-> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip (LibName, Bool, [Integer])
-> (LibName, Bool, [Integer]) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((LibName, Bool, [Integer])
 -> (LibName, Bool, [Integer]) -> Ordering)
-> (a -> (LibName, Bool, [Integer])) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> (LibName, Bool, [Integer])
versionMeasure)
                     [ a
l | a
l <- [a]
libs, LibName
x LibName -> LibName -> Bool
`hasMatch` a -> LibName
libName a
l ]

    -- foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0
    versionMeasure :: a -> (LibName, Bool, [Integer])
versionMeasure a
l = (LibName
rx, [Integer] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Integer]
vs, [Integer]
vs)
      where
        VersionView LibName
rx [Integer]
vs = LibName -> VersionView
versionView (a -> LibName
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 :: LibName -> LibName -> Bool
hasMatch LibName
x LibName
y = LibName
rx LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
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 LibName
rx [Integer]
vx = LibName -> VersionView
versionView LibName
x
    VersionView LibName
ry [Integer]
vy = LibName -> VersionView
versionView LibName
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 :: LibName -> VersionView
versionView LibName
s =
  case (Char -> Bool) -> LibName -> (LibName, LibName)
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 LibName
s) of
    (LibName
v, Char
'-' : LibName
x) | [LibName] -> Bool
forall (t :: * -> *) a. Foldable t => [t a] -> Bool
valid [LibName]
vs ->
      LibName -> [Integer] -> VersionView
VersionView (ShowS
forall a. [a] -> [a]
reverse LibName
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
$ (LibName -> Integer) -> [LibName] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map (LibName -> Integer
forall a. Read a => LibName -> a
read (LibName -> Integer) -> ShowS -> LibName -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse) [LibName]
vs
      where vs :: [LibName]
vs = (Char -> Bool) -> LibName -> [LibName]
forall a. (a -> Bool) -> [a] -> [[a]]
chopWhen (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.') LibName
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
    (LibName, LibName)
_ -> LibName -> [Integer] -> VersionView
VersionView LibName
s []

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