{-# LANGUAGE OverloadedLists #-}

-- | 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 qualified Control.Exception as E
import Control.Monad          ( filterM, forM )
import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Writer   ( Writer, runWriter, WriterT(WriterT), runWriterT, tell )
import Control.Monad.IO.Class ( MonadIO(..) )

import Data.Char
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 Text.Printf

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, pattern (:|) )
import Agda.Utils.List2             ( List2 )
import qualified Agda.Utils.List1   as List1
import qualified Agda.Utils.List2   as List2
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.Singleton
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 -> [Char]
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
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, LineNumber -> VersionView -> ShowS
[VersionView] -> ShowS
VersionView -> [Char]
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [VersionView] -> ShowS
$cshowList :: [VersionView] -> ShowS
show :: VersionView -> [Char]
$cshow :: VersionView -> [Char]
showsPrec :: LineNumber -> VersionView -> ShowS
$cshowsPrec :: LineNumber -> VersionView -> ShowS
Show)

-- | Raise collected 'LibErrors' as exception.
--
mkLibM :: [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM :: forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [AgdaLibFile]
libs LibErrorIO a
m = do
  (a
x, LibErrWarns
ews) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT LibErrorIO a
m
  let ([LibError]
errs, [LibWarning]
warns) = forall a b. [Either a b] -> ([a], [b])
partitionEithers LibErrWarns
ews
  forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [LibWarning]
warns
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LibError]
errs) forall a b. (a -> b) -> a -> b
$ do
    let doc :: Doc
doc = forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ([AgdaLibFile] -> LibError -> Doc
formatLibError [AgdaLibFile]
libs) [LibError]
errs
    forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Doc
doc
  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 [Char]
getAgdaAppDir = do
  -- System-specific command to build the path to ~/.agda (Unix) or %APPDATA%\agda (Win)
  let agdaDir :: IO [Char]
agdaDir = [Char] -> IO [Char]
getAppUserDataDirectory [Char]
"agda"
  -- The default can be overwritten by setting the AGDA_DIR environment variable
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM ([Char] -> IO (Maybe [Char])
lookupEnv [Char]
"AGDA_DIR") IO [Char]
agdaDir forall a b. (a -> b) -> a -> b
$ \ [Char]
dir ->
      forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([Char] -> IO Bool
doesDirectoryExist [Char]
dir) ([Char] -> IO [Char]
canonicalizePath [Char]
dir) forall a b. (a -> b) -> a -> b
$ do
        [Char]
d <- IO [Char]
agdaDir
        [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"Warning: Environment variable AGDA_DIR points to non-existing directory " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
dir forall a. [a] -> [a] -> [a]
++ [Char]
", using " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Char]
d forall a. [a] -> [a] -> [a]
++ [Char]
" instead."
        forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
d

-- | Returns the absolute default lib dir. This directory is used to
-- store the Primitive.agda file.
getPrimitiveLibDir :: IO FilePath
getPrimitiveLibDir :: IO [Char]
getPrimitiveLibDir = do
  [Char]
libdir <- AbsolutePath -> [Char]
filePath forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> IO AbsolutePath
absolute forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Char] -> IO [Char]
getDataFileName [Char]
"lib")
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ([Char] -> IO Bool
doesDirectoryExist [Char]
libdir)
      (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char]
libdir [Char] -> ShowS
</> [Char]
"prim")
      (forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"The lib directory " forall a. [a] -> [a] -> [a]
++ [Char]
libdir forall a. [a] -> [a] -> [a]
++ [Char]
" 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.  The first file in this list that exists is actually used.
--
defaultLibraryFiles :: List1 FilePath
defaultLibraryFiles :: List1 [Char]
defaultLibraryFiles = ([Char]
"libraries-" forall a. [a] -> [a] -> [a]
++ [Char]
version) forall a. a -> [a] -> NonEmpty a
:| [Char]
"libraries" forall a. a -> [a] -> [a]
: []

-- | The @defaultsFile@ contains a list of library names relevant for each Agda project.
--
defaultsFile :: FilePath
defaultsFile :: [Char]
defaultsFile = [Char]
"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.  The first file in this list that exists is actually used.
--
defaultExecutableFiles :: List1 FilePath
defaultExecutableFiles :: List1 [Char]
defaultExecutableFiles = ([Char]
"executables-" forall a. [a] -> [a] -> [a]
++ [Char]
version) forall a. a -> [a] -> NonEmpty a
:| [Char]
"executables" forall a. a -> [a] -> [a]
: []

------------------------------------------------------------------------
-- * 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 :: [Char] -> LibM ProjectConfig
findProjectConfig [Char]
root = forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] forall a b. (a -> b) -> a -> b
$ [Char] -> LibErrorIO ProjectConfig
findProjectConfig' [Char]
root

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


-- | Get project root

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


-- | Get the contents of @.agda-lib@ files in the given project root.
getAgdaLibFiles' :: FilePath -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' :: [Char] -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' [Char]
path = [Char] -> LibErrorIO ProjectConfig
findProjectConfig' [Char]
path forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  ProjectConfig
DefaultProjectConfig    -> forall (m :: * -> *) a. Monad m => a -> m a
return []
  ProjectConfig [Char]
root [[Char]]
libs -> Maybe LibrariesFile
-> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
parseLibFiles forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map ((LineNumber
0,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
root [Char] -> ShowS
</>)) [[Char]]
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 :: [Char] -> Bool -> LibM ([[Char]], [[Char]])
getDefaultLibraries [Char]
root Bool
optDefaultLibs = forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] forall a b. (a -> b) -> a -> b
$ do
  [AgdaLibFile]
libs <- [Char] -> LibErrorIO [AgdaLibFile]
getAgdaLibFiles' [Char]
root
  if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AgdaLibFile]
libs
    then (,[]) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if Bool
optDefaultLibs then ([Char]
libNameForCurrentDir forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> WriterT LibErrWarns (StateT LibState IO) [[Char]]
readDefaultsFile else forall (m :: * -> *) a. Monad m => a -> m a
return []
    else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {t :: * -> *}.
Foldable t =>
t AgdaLibFile -> ([[Char]], [[Char]])
libsAndPaths [AgdaLibFile]
libs
  where
    libsAndPaths :: t AgdaLibFile -> ([[Char]], [[Char]])
libsAndPaths t AgdaLibFile
ls = ( forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [[Char]]
_libDepends t AgdaLibFile
ls
                      , forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a. a -> a
id (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [[Char]]
_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 LibErrWarns (StateT LibState IO) [[Char]]
readDefaultsFile = do
    [Char]
agdaDir <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [Char]
getAgdaAppDir
    let file :: [Char]
file = [Char]
agdaDir [Char] -> ShowS
</> [Char]
defaultsFile
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifNotM (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO Bool
doesFileExist [Char]
file) (forall (m :: * -> *) a. Monad m => a -> m a
return []) forall a b. (a -> b) -> a -> b
$ {-else-} do
      [[Char]]
ls <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [(LineNumber, [Char])]
stripCommentLines forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO [Char]
UTF8.readFile [Char]
file
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [Char] -> [[Char]]
splitCommas [[Char]]
ls
  forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibError' -> m ()
raiseErrors' [ IOException -> [Char] -> LibError'
ReadError IOException
e [Char]
"Failed to read defaults file." ]
    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.
--
--   If the user specified an alternative @libraries@ file which does not exist,
--   an exception is thrown containing the name of this file.
getLibrariesFile
  :: (MonadIO m, MonadError FilePath m)
  => Maybe FilePath -- ^ Override the default @libraries@ file?
  -> m LibrariesFile
getLibrariesFile :: forall (m :: * -> *).
(MonadIO m, MonadError [Char] m) =>
Maybe [Char] -> m LibrariesFile
getLibrariesFile (Just [Char]
overrideLibFile) = do
  -- A user-specified override file must exist.
  forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO Bool
doesFileExist [Char]
overrideLibFile)
    {-then-} (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> LibrariesFile
LibrariesFile [Char]
overrideLibFile Bool
True)
    {-else-} (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
overrideLibFile)
getLibrariesFile Maybe [Char]
Nothing = do
  [Char]
agdaDir <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ IO [Char]
getAgdaAppDir
  let defaults :: List1 [Char]
defaults = forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map ([Char]
agdaDir [Char] -> ShowS
</>) List1 [Char]
defaultLibraryFiles -- NB: very short list
  [[Char]]
files <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [Char] -> IO Bool
doesFileExist (forall l. IsList l => l -> [Item l]
List1.toList List1 [Char]
defaults)
  case [[Char]]
files of
    [Char]
file : [[Char]]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> LibrariesFile
LibrariesFile [Char]
file Bool
True
    []       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> LibrariesFile
LibrariesFile (forall a. NonEmpty a -> a
List1.last List1 [Char]
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 [Char] -> LibM [AgdaLibFile]
getInstalledLibraries Maybe [Char]
overrideLibFile = forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] forall a b. (a -> b) -> a -> b
$ do
    Either [Char] LibrariesFile
filem <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadIO m, MonadError [Char] m) =>
Maybe [Char] -> m LibrariesFile
getLibrariesFile Maybe [Char]
overrideLibFile
    case Either [Char] LibrariesFile
filem of
      Left [Char]
theOverrideLibFile -> do
        forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibError' -> m ()
raiseErrors' [ [Char] -> LibError'
LibrariesFileNotFound [Char]
theOverrideLibFile ]
        forall (m :: * -> *) a. Monad m => a -> m a
return []
      Right LibrariesFile
file -> do
        if Bool -> Bool
not (LibrariesFile -> Bool
lfExists LibrariesFile
file) then forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
          [(LineNumber, [Char])]
ls    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> [(LineNumber, [Char])]
stripCommentLines forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO [Char]
UTF8.readFile (LibrariesFile -> [Char]
lfPath LibrariesFile
file)
          [(LineNumber, [Char])]
files <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (LineNumber
i, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO [Char]
expandEnvironmentVariables [Char]
s | (LineNumber
i, [Char]
s) <- [(LineNumber, [Char])]
ls ]
          Maybe LibrariesFile
-> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
parseLibFiles (forall a. a -> Maybe a
Just LibrariesFile
file) forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a b. (a, b) -> b
snd [(LineNumber, [Char])]
files
  forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibError' -> m ()
raiseErrors' [ IOException -> [Char] -> LibError'
ReadError IOException
e [Char]
"Failed to read installed libraries." ]
    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
-> [(LineNumber, [Char])] -> LibErrorIO [AgdaLibFile]
parseLibFiles Maybe LibrariesFile
mlibFile [(LineNumber, [Char])]
files = do

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

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

  forall m a. Null m => [a] -> (List1 a -> m) -> m
List1.unlessNull (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[LibWarning]]
warns) forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibWarning -> m ()
warnings
  forall m a. Null m => [a] -> (List1 a -> m) -> m
List1.unlessNull [(Maybe LibPositionInfo, LibParseError)]
errs forall a b. (a -> b) -> a -> b
$ \ List1 (Maybe LibPositionInfo, LibParseError)
errs1 ->
    forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibError -> m ()
raiseErrors forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ (Maybe LibPositionInfo
mc, LibParseError
err) -> Maybe LibPositionInfo -> LibError' -> LibError
LibError Maybe LibPositionInfo
mc forall a b. (a -> b) -> a -> b
$ LibParseError -> LibError'
LibParseError LibParseError
err) List1 (Maybe LibPositionInfo, LibParseError)
errs1

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

-- | Remove trailing white space and line comments.
--
stripCommentLines :: String -> [(LineNumber, String)]
stripCommentLines :: [Char] -> [(LineNumber, [Char])]
stripCommentLines = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a}. (a, [Char]) -> [(a, [Char])]
strip forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [LineNumber
1..] forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
lines
  where
    strip :: (a, [Char]) -> [(a, [Char])]
strip (a
i, [Char]
s) = [ (a
i, [Char]
s') | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
s' ]
      where s' :: [Char]
s' = ShowS
trimLineComment [Char]
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
  [Char]
agdaDir <- IO [Char]
getAgdaAppDir
  let defaults :: List1 [Char]
defaults = forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map ([Char]
agdaDir [Char] -> ShowS
</>) List1 [Char]
defaultExecutableFiles  -- NB: very short list
  [[Char]]
files <- forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM [Char] -> IO Bool
doesFileExist (forall l. IsList l => l -> [Item l]
List1.toList List1 [Char]
defaults)
  case [[Char]]
files of
    [Char]
file : [[Char]]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> ExecutablesFile
ExecutablesFile [Char]
file Bool
True
    []       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Char] -> Bool -> ExecutablesFile
ExecutablesFile (forall a. NonEmpty a -> a
List1.last List1 [Char]
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 [Char])
getTrustedExecutables = forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] forall a b. (a -> b) -> a -> b
$ do
    ExecutablesFile
file <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ExecutablesFile
getExecutablesFile
    if Bool -> Bool
not (ExecutablesFile -> Bool
efExists ExecutablesFile
file) then forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
Map.empty else do
      [(LineNumber, [Char])]
es    <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> [(LineNumber, [Char])]
stripCommentLines forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO [Char]
UTF8.readFile (ExecutablesFile -> [Char]
efPath ExecutablesFile
file)
      [(LineNumber, [Char])]
files <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (LineNumber
i, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO [Char]
expandEnvironmentVariables [Char]
s | (LineNumber
i, [Char]
s) <- [(LineNumber, [Char])]
es ]
      Map ExeName [Char]
tmp   <- ExecutablesFile
-> [(LineNumber, [Char])]
-> WriterT LibErrWarns (StateT LibState IO) (Map ExeName [Char])
parseExecutablesFile ExecutablesFile
file forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn forall a b. (a, b) -> b
snd [(LineNumber, [Char])]
files
      forall (m :: * -> *) a. Monad m => a -> m a
return Map ExeName [Char]
tmp
  forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \ IOException
e -> do
    forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibError' -> m ()
raiseErrors' [ IOException -> [Char] -> LibError'
ReadError IOException
e [Char]
"Failed to read trusted executables." ]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall k a. Map k a
Map.empty

-- | Parse the @executables@ file.
--
parseExecutablesFile
  :: ExecutablesFile
  -> [(LineNumber, FilePath)]
  -> LibErrorIO (Map ExeName FilePath)
parseExecutablesFile :: ExecutablesFile
-> [(LineNumber, [Char])]
-> WriterT LibErrWarns (StateT LibState IO) (Map ExeName [Char])
parseExecutablesFile ExecutablesFile
ef [(LineNumber, [Char])]
files = do
  [(ExeName, [Char])]
executables <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(LineNumber, [Char])]
files forall a b. (a -> b) -> a -> b
$ \(LineNumber
ln, [Char]
fp) -> do
    -- Compute canonical executable name and absolute filepath.
    let strExeName :: [Char]
strExeName  = ShowS
takeFileName [Char]
fp
    let strExeName' :: [Char]
strExeName' = forall a. a -> Maybe a -> a
fromMaybe [Char]
strExeName forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> Maybe [Char]
stripExtension [Char]
exeExtension [Char]
strExeName
    let txtExeName :: ExeName
txtExeName  = [Char] -> ExeName
T.pack [Char]
strExeName'
    [Char]
exePath <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO [Char]
makeAbsolute [Char]
fp
    forall (m :: * -> *) a. Monad m => a -> m a
return (ExeName
txtExeName, [Char]
exePath)

  -- Create a map from executable names to their location(s).
  let exeMap1 :: Map ExeName (List1 FilePath)
      exeMap1 :: Map ExeName (List1 [Char])
exeMap1 = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Semigroup a => a -> a -> a
(<>) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall el coll. Singleton el coll => el -> coll
singleton) [(ExeName, [Char])]
executables

  -- Separate non-ambiguous from ambiguous mappings.
  let (Map ExeName [Char]
exeMap, Map ExeName (List2 [Char])
duplicates) = forall a b c k. (a -> Either b c) -> Map k a -> (Map k b, Map k c)
Map.mapEither forall a. List1 a -> Either a (List2 a)
List2.fromList1Either Map ExeName (List1 [Char])
exeMap1

  -- Report ambiguous mappings.
  forall m a. Null m => [a] -> (List1 a -> m) -> m
List1.unlessNull (forall k a. Map k a -> [(k, a)]
Map.toList Map ExeName (List2 [Char])
duplicates) forall a b. (a -> b) -> a -> b
$ \ List1 (ExeName, List2 [Char])
duplicates1 ->
    forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibError' -> m ()
raiseErrors' forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. (a -> b) -> a -> b
$ [Char] -> ExeName -> List2 [Char] -> LibError'
DuplicateExecutable forall a b. (a -> b) -> a -> b
$ ExecutablesFile -> [Char]
efPath ExecutablesFile
ef) List1 (ExeName, List2 [Char])
duplicates1

  -- Return non-ambiguous mappings.
  forall (m :: * -> *) a. Monad m => a -> m a
return Map ExeName [Char]
exeMap

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

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

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