{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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.
--     (project, libNames, includePaths) <-  getDefaultLibraries projectRoot True
--
--     -- Get include paths of depended-on libraries.
--     resolvedPaths <- libraryIncludePaths Nothing project libs libNames
--
--     let allPaths = includePaths ++ resolvedPaths
--   @
--
module Agda.Interaction.Library
  ( findProjectRoot
  , getDefaultLibraries
  , getInstalledLibraries
  , getTrustedExecutables
  , libraryIncludePaths
  , getAgdaLibFile
  , getPrimitiveLibDir
  , classifyBuiltinModule_
  , builtinModules
  , builtinModulesWithSafePostulates
  , builtinModulesWithUnsafePostulates
  , primitiveModules
  , LibName, parseLibName
  , OptionsPragma(..)
  , AgdaLibFile(..)
  , ExeName
  , LibM
  , mkLibM
  , LibWarning(..)
  , LibPositionInfo(..)
  , libraryWarningName
  , ProjectConfig(..)
  -- * Exported for testing
  , findLib'
  ) where

import qualified Control.Exception as E
import Control.Monad.Except   ( runExceptT, MonadError, throwError )
import Control.Monad.Writer   ( Writer, runWriterT, tell )
import Control.Monad.IO.Class ( MonadIO(..) )

import Data.Bifunctor ( first, second )
import Data.Either
import Data.Function (on)
import qualified Data.List as List
import Data.Map ( Map )
import qualified Data.Map as Map
import Data.Set ( Set )
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Tree ( Tree(Node) )

import System.Directory
import System.FilePath
import System.IO.Error ( isPermissionError )

import Agda.Interaction.Library.Base
import Agda.Interaction.Library.Parse

import Agda.Syntax.Common.Pretty ( prettyShow )

import Agda.TypeChecking.Monad.Base.Types ( IsBuiltinModule(..) )

import Agda.Utils.Environment
import Agda.Utils.FileName
import Agda.Utils.IO ( catchIO )
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1             ( List1, pattern (:|) )
import Agda.Utils.List2             ( pattern 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.Singleton
import Agda.Utils.Tuple ( secondM )

import Agda.Setup ( getDataFileName, getAgdaAppDir )
import Agda.Version

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

-- | 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
  (x, ews) <- WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
-> ExceptT
     LibErrors
     (WriterT [LibWarning] (StateT LibState IO))
     (a, LibErrWarns)
forall (m :: * -> *) a. Monad m => m a -> ExceptT LibErrors m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
 -> ExceptT
      LibErrors
      (WriterT [LibWarning] (StateT LibState IO))
      (a, LibErrWarns))
-> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
-> ExceptT
     LibErrors
     (WriterT [LibWarning] (StateT LibState IO))
     (a, LibErrWarns)
forall a b. (a -> b) -> a -> b
$ StateT LibState IO (a, LibErrWarns)
-> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
forall (m :: * -> *) a. Monad m => m a -> WriterT [LibWarning] m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT LibState IO (a, LibErrWarns)
 -> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns))
-> StateT LibState IO (a, LibErrWarns)
-> WriterT [LibWarning] (StateT LibState IO) (a, LibErrWarns)
forall a b. (a -> b) -> a -> b
$ LibErrorIO a -> StateT LibState IO (a, LibErrWarns)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT LibErrorIO a
m
  let (errs, warns) = partitionEithers ews
  tell warns
  () <- List1.unlessNull errs \ List1 LibError
errs -> LibErrors
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) ()
forall a.
LibErrors
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LibErrors
 -> ExceptT
      LibErrors (WriterT [LibWarning] (StateT LibState IO)) ())
-> LibErrors
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) ()
forall a b. (a -> b) -> a -> b
$ [AgdaLibFile] -> List1 LibError -> LibErrors
LibErrors [AgdaLibFile]
libs List1 LibError
errs
  return x

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

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

-- | The @$AGDA_DIR/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 :: NonEmpty FilePath
defaultLibraryFiles = (FilePath
"libraries-" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
version) FilePath -> [FilePath] -> NonEmpty FilePath
forall a. a -> [a] -> NonEmpty a
:| FilePath
"libraries" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: []

-- | The @$AGDA_DIR/defaults@ file lists the library names relevant for all
--   Agda projects.
--
--   Agda also honors version-specific @defaults@ files, e.g. @defaults-2.6.0@.
--
--   @defaultsFiles@ gives a list of all @defaults@ Agda should process
--   by default. The first file in this list that exists is actually used.
--
defaultsFiles :: List1 FilePath
defaultsFiles :: NonEmpty FilePath
defaultsFiles = (FilePath
"defaults-" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
version) FilePath -> [FilePath] -> NonEmpty FilePath
forall a. a -> [a] -> NonEmpty a
:| FilePath
"defaults" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: []

-- | The @$AGDA_DIR/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 :: NonEmpty FilePath
defaultExecutableFiles = (FilePath
"executables-" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
version) FilePath -> [FilePath] -> NonEmpty FilePath
forall a. a -> [a] -> NonEmpty a
:| FilePath
"executables" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: []

------------------------------------------------------------------------
-- * Agda builtin modules
------------------------------------------------------------------------

-- | Prefix path with @Agda.Builtin@.

agdaBuiltin :: FilePath -> FilePath
agdaBuiltin :: FilePath -> FilePath
agdaBuiltin = (FilePath
"Agda" FilePath -> FilePath -> FilePath
</>) (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath
"Builtin" FilePath -> FilePath -> FilePath
</>)

-- | The very magical, auto-imported modules.

agdaPrimitive :: FilePath
agdaPrimitive :: FilePath
agdaPrimitive = FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Primitive.agda"

agdaPrimitiveCubical :: FilePath
agdaPrimitiveCubical :: FilePath
agdaPrimitiveCubical = FilePath
"Agda" FilePath -> FilePath -> FilePath
</> FilePath
"Primitive" FilePath -> FilePath -> FilePath
</> FilePath
"Cubical.agda"

primitiveModules :: Set FilePath
primitiveModules :: Set FilePath
primitiveModules = [FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
Set.fromList [FilePath
Item [FilePath]
agdaPrimitive, FilePath
Item [FilePath]
agdaPrimitiveCubical]

-- | These builtins may use postulates, and are still considered @--safe@.

builtinModulesWithSafePostulates :: Set FilePath
builtinModulesWithSafePostulates :: Set FilePath
builtinModulesWithSafePostulates =
  (Set FilePath
primitiveModules Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
`Set.union`) (Set FilePath -> Set FilePath) -> Set FilePath -> Set FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
Set.fromList ([FilePath] -> Set FilePath) -> [FilePath] -> Set FilePath
forall a b. (a -> b) -> a -> b
$
  (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> FilePath
agdaBuiltin ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$
    [ FilePath
Item [FilePath]
"Bool.agda"
    , FilePath
Item [FilePath]
"Char.agda"
    , FilePath
"Char" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
    , FilePath
Item [FilePath]
"Coinduction.agda"
    , FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Equiv.agda"
    , FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Glue.agda"
    , FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"HCompU.agda"
    , FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Id.agda"
    , FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Path.agda"
    , FilePath
"Cubical" FilePath -> FilePath -> FilePath
</> FilePath
"Sub.agda"
    , FilePath
"Equality" FilePath -> FilePath -> FilePath
</> FilePath
"Erase.agda"
    , FilePath
Item [FilePath]
"Equality.agda"
    , FilePath
"Erased" FilePath -> FilePath -> FilePath
</> FilePath
"Box-cong.agda"
    , FilePath
"Erased" FilePath -> FilePath -> FilePath
</> FilePath
"Erased.agda"
    , FilePath
"Erased" FilePath -> FilePath -> FilePath
</> FilePath
"Funext.agda"
    , FilePath
"Erased" FilePath -> FilePath -> FilePath
</> FilePath
"Propext.agda"
    , FilePath
"Erased" FilePath -> FilePath -> FilePath
</> FilePath
"Quotient.agda"
    , FilePath
Item [FilePath]
"Float.agda"
    , FilePath
"Float" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
    , FilePath
Item [FilePath]
"FromNat.agda"
    , FilePath
Item [FilePath]
"FromNeg.agda"
    , FilePath
Item [FilePath]
"FromString.agda"
    , FilePath
Item [FilePath]
"Int.agda"
    , FilePath
Item [FilePath]
"IO.agda"
    , FilePath
Item [FilePath]
"List.agda"
    , FilePath
Item [FilePath]
"Maybe.agda"
    , FilePath
Item [FilePath]
"Nat.agda"
    , FilePath
Item [FilePath]
"Reflection.agda"
    , FilePath
"Reflection" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
    , FilePath
"Reflection" FilePath -> FilePath -> FilePath
</> FilePath
"External.agda"
    , FilePath
Item [FilePath]
"Sigma.agda"
    , FilePath
Item [FilePath]
"Size.agda"
    , FilePath
Item [FilePath]
"Strict.agda"
    , FilePath
Item [FilePath]
"String.agda"
    , FilePath
"String" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
    , FilePath
Item [FilePath]
"Unit.agda"
    , FilePath
Item [FilePath]
"Word.agda"
    , FilePath
"Word" FilePath -> FilePath -> FilePath
</> FilePath
"Properties.agda"
    ]

-- | These builtins may not use postulates under @--safe@. They are not
--   automatically unsafe, but will be if they use an unsafe feature.

builtinModulesWithUnsafePostulates :: Set FilePath
builtinModulesWithUnsafePostulates :: Set FilePath
builtinModulesWithUnsafePostulates = [FilePath] -> Set FilePath
forall a. Ord a => [a] -> Set a
Set.fromList ([FilePath] -> Set FilePath) -> [FilePath] -> Set FilePath
forall a b. (a -> b) -> a -> b
$
  (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> FilePath
agdaBuiltin ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$
    [ FilePath
Item [FilePath]
"TrustMe.agda"
    , FilePath
"Equality" FilePath -> FilePath -> FilePath
</> FilePath
"Rewrite.agda"
    ]

-- | All builtin modules.

builtinModules :: Set FilePath
builtinModules :: Set FilePath
builtinModules = Set FilePath
builtinModulesWithSafePostulates Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
`Set.union`
                 Set FilePath
builtinModulesWithUnsafePostulates

-- | Determine whether the second absolute path refers to one of Agda's primitive modules.
--   The first argument should be the result of 'getPrimitiveLibDir'.
--
classifyBuiltinModule_ :: AbsolutePath -> AbsolutePath -> Maybe IsBuiltinModule
classifyBuiltinModule_ :: AbsolutePath -> AbsolutePath -> Maybe IsBuiltinModule
classifyBuiltinModule_ AbsolutePath
primLibDir AbsolutePath
fp = do
  f <- AbsolutePath -> AbsolutePath -> Maybe FilePath
relativizeAbsolutePath AbsolutePath
fp AbsolutePath
primLibDir
  guard $ f `Set.member` builtinModules
  if f `Set.member` builtinModulesWithUnsafePostulates then return IsBuiltinModule
  else if f == agdaPrimitive then pure IsAgdaPrimitive
  else if f == agdaPrimitiveCubical then pure IsAgdaPrimitiveCubical
  else pure IsBuiltinModuleWithSafePostulates

------------------------------------------------------------------------
-- * 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 (initially: the directory Agda was called in).
  -> LibM ProjectConfig
       -- ^ Actual root and @.agda-lib@ file for this project.
findProjectConfig :: FilePath -> LibM ProjectConfig
findProjectConfig FilePath
root = do
  FilePath
-> ExceptT
     LibErrors
     (WriterT [LibWarning] (StateT LibState IO))
     (Maybe ProjectConfig)
forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
FilePath -> m (Maybe ProjectConfig)
getCachedProjectConfig FilePath
root ExceptT
  LibErrors
  (WriterT [LibWarning] (StateT LibState IO))
  (Maybe ProjectConfig)
-> (Maybe ProjectConfig -> LibM ProjectConfig)
-> LibM ProjectConfig
forall a b.
ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
-> (a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b)
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just ProjectConfig
conf -> ProjectConfig -> LibM ProjectConfig
forall a.
a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
conf
    Maybe ProjectConfig
Nothing   -> LibM ProjectConfig -> LibM ProjectConfig
handlePermissionException do
      libFiles <- IO [FilePath]
-> ExceptT
     LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
forall a.
IO a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [FilePath]
 -> ExceptT
      LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath])
-> IO [FilePath]
-> ExceptT
     LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> IO [FilePath]
getDirectoryContents FilePath
root IO [FilePath] -> ([FilePath] -> IO [FilePath]) -> IO [FilePath]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
        (FilePath -> IO Bool) -> [FilePath] -> IO [FilePath]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (\FilePath
file -> IO Bool -> IO Bool -> IO Bool
forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
and2M
          (Bool -> IO Bool
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
takeExtension FilePath
file FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
".agda-lib")
          (FilePath -> IO Bool
doesFileExist (FilePath
root FilePath -> FilePath -> FilePath
</> FilePath
file)))
#if defined(wasm32_HOST_ARCH)
      -- During tests, wasmtime sometimes reports duplicate entries in a directory.
      -- This extra step workarounds the quirky behavior; see comments in PR #8205.
      let libFiles' = case libFiles of
            []        -> []
            [file]    -> [file]
            (f:files)
              | all (== f) files -> [f]  -- All entries are duplicates of the same file
              | otherwise        -> libFiles
#else
      let libFiles' = [FilePath]
libFiles
#endif
      case libFiles' of
        []     -> IO (Maybe FilePath)
-> ExceptT
     LibErrors
     (WriterT [LibWarning] (StateT LibState IO))
     (Maybe FilePath)
forall a.
IO a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (FilePath -> IO (Maybe FilePath)
upPath FilePath
root) ExceptT
  LibErrors
  (WriterT [LibWarning] (StateT LibState IO))
  (Maybe FilePath)
-> (Maybe FilePath -> LibM ProjectConfig) -> LibM ProjectConfig
forall a b.
ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
-> (a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b)
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          Just FilePath
up -> do
            conf <- ASetter ProjectConfig ProjectConfig Int Int
-> (Int -> Int) -> ProjectConfig -> ProjectConfig
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ASetter ProjectConfig ProjectConfig Int Int
Lens' ProjectConfig Int
lensConfigAbove (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (ProjectConfig -> ProjectConfig)
-> LibM ProjectConfig -> LibM ProjectConfig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> LibM ProjectConfig
findProjectConfig FilePath
up
            storeCachedProjectConfig root conf
            return conf
          Maybe FilePath
Nothing -> ProjectConfig -> LibM ProjectConfig
forall a.
a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
DefaultProjectConfig
        [Item [FilePath]
file] -> do
          let conf :: ProjectConfig
conf = FilePath -> FilePath -> Int -> ProjectConfig
ProjectConfig FilePath
root FilePath
Item [FilePath]
file Int
0
          FilePath
-> ProjectConfig
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) ()
forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
FilePath -> ProjectConfig -> m ()
storeCachedProjectConfig FilePath
root ProjectConfig
conf
          ProjectConfig -> LibM ProjectConfig
forall a.
a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
conf
        FilePath
f1:FilePath
f2:[FilePath]
files -> LibErrors -> LibM ProjectConfig
forall a.
LibErrors
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (LibErrors -> LibM ProjectConfig)
-> LibErrors -> LibM ProjectConfig
forall a b. (a -> b) -> a -> b
$ [AgdaLibFile] -> List1 LibError -> LibErrors
LibErrors [] (List1 LibError -> LibErrors) -> List1 LibError -> LibErrors
forall a b. (a -> b) -> a -> b
$ LibError -> List1 LibError
forall el coll. Singleton el coll => el -> coll
singleton (LibError -> List1 LibError) -> LibError -> List1 LibError
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
$
          FilePath -> List2 FilePath -> LibError'
SeveralAgdaLibFiles FilePath
root (List2 FilePath -> LibError') -> List2 FilePath -> LibError'
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> [FilePath] -> List2 FilePath
forall a. a -> a -> [a] -> List2 a
List2 FilePath
f1 FilePath
f2 [FilePath]
files

  where
    -- Andreas, 2024-06-26, issue #7331:
    -- In case of missing permission we terminate our search for the project file
    -- with the default value.
    handlePermissionException :: LibM ProjectConfig -> LibM ProjectConfig
    handlePermissionException :: LibM ProjectConfig -> LibM ProjectConfig
handlePermissionException = (LibM ProjectConfig
 -> (IOException -> LibM ProjectConfig) -> LibM ProjectConfig)
-> (IOException -> LibM ProjectConfig)
-> LibM ProjectConfig
-> LibM ProjectConfig
forall a b c. (a -> b -> c) -> b -> a -> c
flip LibM ProjectConfig
-> (IOException -> LibM ProjectConfig) -> LibM ProjectConfig
forall e a.
Exception e =>
ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
-> (e
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a)
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) e a.
(CatchIO m, Exception e) =>
m a -> (e -> m a) -> m a
catchIO \ IOException
e ->
      if IOException -> Bool
isPermissionError IOException
e then ProjectConfig -> LibM ProjectConfig
forall a.
a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return ProjectConfig
DefaultProjectConfig else IO ProjectConfig -> LibM ProjectConfig
forall a.
IO a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProjectConfig -> LibM ProjectConfig)
-> IO ProjectConfig -> LibM ProjectConfig
forall a b. (a -> b) -> a -> b
$ IOException -> IO ProjectConfig
forall e a. (HasCallStack, Exception e) => e -> IO a
E.throwIO IOException
e

    -- 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 :: FilePath -> IO (Maybe FilePath)
upPath FilePath
root = do
      up <- FilePath -> IO FilePath
canonicalizePath (FilePath -> IO FilePath) -> FilePath -> IO FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
root FilePath -> FilePath -> FilePath
</> FilePath
".."
      if up == root then return Nothing else return $ Just up


-- | Get project root

findProjectRoot :: FilePath -> LibM (Maybe FilePath)
findProjectRoot :: FilePath
-> ExceptT
     LibErrors
     (WriterT [LibWarning] (StateT LibState IO))
     (Maybe FilePath)
findProjectRoot FilePath
root = FilePath -> LibM ProjectConfig
findProjectConfig FilePath
root LibM ProjectConfig
-> (ProjectConfig -> Maybe FilePath)
-> ExceptT
     LibErrors
     (WriterT [LibWarning] (StateT LibState IO))
     (Maybe FilePath)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
  ProjectConfig FilePath
p FilePath
_ Int
_  -> FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
p
  ProjectConfig
DefaultProjectConfig -> Maybe FilePath
forall a. Maybe a
Nothing


-- | Get the content of the @.agda-lib@ file in the given project root.
getAgdaLibFile :: FilePath -> LibM [AgdaLibFile]
getAgdaLibFile :: FilePath -> LibM [AgdaLibFile]
getAgdaLibFile FilePath
path = FilePath -> LibM ProjectConfig
findProjectConfig FilePath
path LibM ProjectConfig
-> (ProjectConfig -> LibM [AgdaLibFile]) -> LibM [AgdaLibFile]
forall a b.
ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
-> (a
    -> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b)
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  ProjectConfig
DefaultProjectConfig          -> [AgdaLibFile] -> LibM [AgdaLibFile]
forall a.
a
-> ExceptT LibErrors (WriterT [LibWarning] (StateT LibState IO)) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
  ProjectConfig FilePath
root FilePath
file Int
above -> [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
$
    (AgdaLibFile -> AgdaLibFile) -> [AgdaLibFile] -> [AgdaLibFile]
forall a b. (a -> b) -> [a] -> [b]
map (ASetter AgdaLibFile AgdaLibFile Int Int
-> Int -> AgdaLibFile -> AgdaLibFile
forall s t a b. ASetter s t a b -> b -> s -> t
set ASetter AgdaLibFile AgdaLibFile Int Int
Lens' AgdaLibFile Int
libAbove Int
above) ([AgdaLibFile] -> [AgdaLibFile])
-> LibErrorIO [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    Maybe LibrariesFile
-> [(Int, FilePath)] -> LibErrorIO [AgdaLibFile]
parseLibFiles Maybe LibrariesFile
forall a. Maybe a
Nothing [(Int
0, FilePath
root FilePath -> FilePath -> FilePath
</> FilePath
file)]

-- | 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).
--
--   Also returns the @.agda-lib@ file of the project, if any.
--
getDefaultLibraries
  :: FilePath  -- ^ Project root.
  -> Bool      -- ^ Use @defaults@ if no @.agda-lib@ file exists for this project?
  -> LibM (Maybe AgdaLibFile, [LibName], [FilePath])
       -- ^ The returned @LibName@s are all non-empty strings.
getDefaultLibraries :: FilePath -> Bool -> LibM (Maybe AgdaLibFile, [LibName], [FilePath])
getDefaultLibraries FilePath
root Bool
optDefaultLibs = do
  libs <- FilePath -> LibM [AgdaLibFile]
getAgdaLibFile FilePath
root
  if null libs
    then (Nothing,,[]) <$> if optDefaultLibs then mkLibM [] $ (libNameForCurrentDir :) <$> readDefaultsFile else return []
    else return $ libsAndPaths libs
  where
    libsAndPaths :: [AgdaLibFile] -> (Maybe AgdaLibFile, [LibName], [FilePath])
libsAndPaths [AgdaLibFile]
ls = ( [AgdaLibFile] -> Maybe AgdaLibFile
forall a. [a] -> Maybe a
listToMaybe [AgdaLibFile]
ls
                      , (AgdaLibFile -> [LibName]) -> [AgdaLibFile] -> [LibName]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [LibName]
_libDepends [AgdaLibFile]
ls
                      , (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn FilePath -> FilePath
forall a. a -> a
id ((AgdaLibFile -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [FilePath]
_libIncludes [AgdaLibFile]
ls)
                      )

-- | Return list of libraries to be used by default.
--
--   None if the @defaults@ file does not exist.
--
readDefaultsFile :: LibErrorIO [LibName]
readDefaultsFile :: LibErrorIO [LibName]
readDefaultsFile = do
    agdaDir <- IO FilePath -> WriterT LibErrWarns (StateT LibState IO) FilePath
forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
getAgdaAppDir
    let defaults = (FilePath -> FilePath) -> NonEmpty FilePath -> NonEmpty FilePath
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map (FilePath
agdaDir FilePath -> FilePath -> FilePath
</>) NonEmpty FilePath
defaultsFiles -- NB: very short list
    files <- liftIO $ filterM doesFileExist (List1.toList defaults)
    case files of
      []       -> [LibName] -> LibErrorIO [LibName]
forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      FilePath
file : [FilePath]
_ -> do
        ls <- IO [FilePath]
-> WriterT LibErrWarns (StateT LibState IO) [FilePath]
forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [FilePath]
 -> WriterT LibErrWarns (StateT LibState IO) [FilePath])
-> IO [FilePath]
-> WriterT LibErrWarns (StateT LibState IO) [FilePath]
forall a b. (a -> b) -> a -> b
$ ((Int, FilePath) -> FilePath) -> [(Int, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Int, FilePath) -> FilePath
forall a b. (a, b) -> b
snd ([(Int, FilePath)] -> [FilePath])
-> (FilePath -> [(Int, FilePath)]) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [(Int, FilePath)]
stripCommentLines (FilePath -> [FilePath]) -> IO FilePath -> IO [FilePath]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
UTF8.readFile FilePath
file
        return $ map parseLibName $ concatMap splitCommas ls
  LibErrorIO [LibName]
-> (IOException -> LibErrorIO [LibName]) -> LibErrorIO [LibName]
forall e a.
Exception e =>
WriterT LibErrWarns (StateT LibState IO) a
-> (e -> WriterT LibErrWarns (StateT LibState IO) a)
-> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) e a.
(CatchIO m, Exception e) =>
m a -> (e -> m a) -> m a
`catchIO` \ IOException
e -> do
    NonEmpty LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' [ IOException -> FilePath -> LibError'
ReadError IOException
e FilePath
"Failed to read defaults file." ]
    [LibName] -> LibErrorIO [LibName]
forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
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 FilePath m) =>
Maybe FilePath -> m LibrariesFile
getLibrariesFile (Just FilePath
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 a. IO a -> m a
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
$ FilePath -> IO Bool
doesFileExist FilePath
overrideLibFile)
    {-then-} (LibrariesFile -> m LibrariesFile
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> m LibrariesFile)
-> LibrariesFile -> m LibrariesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> LibrariesFile
LibrariesFile FilePath
overrideLibFile Bool
True)
    {-else-} (FilePath -> m LibrariesFile
forall a. FilePath -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError FilePath
overrideLibFile)
getLibrariesFile Maybe FilePath
Nothing = do
  agdaDir <- IO FilePath -> m FilePath
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO FilePath -> m FilePath) -> IO FilePath -> m FilePath
forall a b. (a -> b) -> a -> b
$ IO FilePath
getAgdaAppDir
  let defaults = (FilePath -> FilePath) -> NonEmpty FilePath -> NonEmpty FilePath
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map (FilePath
agdaDir FilePath -> FilePath -> FilePath
</>) NonEmpty FilePath
defaultLibraryFiles -- NB: very short list
  files <- liftIO $ filterM doesFileExist (List1.toList defaults)
  case files of
    FilePath
file : [FilePath]
_ -> LibrariesFile -> m LibrariesFile
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> m LibrariesFile)
-> LibrariesFile -> m LibrariesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> LibrariesFile
LibrariesFile FilePath
file Bool
True
    []       -> LibrariesFile -> m LibrariesFile
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (LibrariesFile -> m LibrariesFile)
-> LibrariesFile -> m LibrariesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> LibrariesFile
LibrariesFile (NonEmpty FilePath -> FilePath
forall a. NonEmpty a -> a
List1.last NonEmpty FilePath
defaults) Bool
False -- doesn't exist, but that's ok

-- | Parse the descriptions of the libraries Agda knows about.
--
--   Returns none if there is no @libraries@ file.
--
getInstalledLibraries
  :: Maybe FilePath     -- ^ Override the default @libraries@ file?
  -> LibM [AgdaLibFile] -- ^ Content of library files.  (Might have empty @LibName@s.)
getInstalledLibraries :: Maybe FilePath -> LibM [AgdaLibFile]
getInstalledLibraries Maybe FilePath
overrideLibFile = [AgdaLibFile] -> 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
    filem <- IO (Either FilePath LibrariesFile)
-> WriterT
     LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either FilePath LibrariesFile)
 -> WriterT
      LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile))
-> IO (Either FilePath LibrariesFile)
-> WriterT
     LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
forall a b. (a -> b) -> a -> b
$ ExceptT FilePath IO LibrariesFile
-> IO (Either FilePath LibrariesFile)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT FilePath IO LibrariesFile
 -> IO (Either FilePath LibrariesFile))
-> ExceptT FilePath IO LibrariesFile
-> IO (Either FilePath LibrariesFile)
forall a b. (a -> b) -> a -> b
$ Maybe FilePath -> ExceptT FilePath IO LibrariesFile
forall (m :: * -> *).
(MonadIO m, MonadError FilePath m) =>
Maybe FilePath -> m LibrariesFile
getLibrariesFile Maybe FilePath
overrideLibFile
    case filem of
      Left FilePath
theOverrideLibFile -> do
        NonEmpty LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' [ FilePath -> LibError'
LibrariesFileNotFound FilePath
theOverrideLibFile ]
        [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
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 a. a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
          ls    <- IO [(Int, FilePath)]
-> WriterT LibErrWarns (StateT LibState IO) [(Int, FilePath)]
forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(Int, FilePath)]
 -> WriterT LibErrWarns (StateT LibState IO) [(Int, FilePath)])
-> IO [(Int, FilePath)]
-> WriterT LibErrWarns (StateT LibState IO) [(Int, FilePath)]
forall a b. (a -> b) -> a -> b
$ FilePath -> [(Int, FilePath)]
stripCommentLines (FilePath -> [(Int, FilePath)])
-> IO FilePath -> IO [(Int, FilePath)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
UTF8.readFile (LibrariesFile -> FilePath
lfPath LibrariesFile
file)
          files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]
          parseLibFiles (Just file) $ nubOn snd files
  LibErrorIO [AgdaLibFile]
-> (IOException -> LibErrorIO [AgdaLibFile])
-> LibErrorIO [AgdaLibFile]
forall e a.
Exception e =>
WriterT LibErrWarns (StateT LibState IO) a
-> (e -> WriterT LibErrWarns (StateT LibState IO) a)
-> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) e a.
(CatchIO m, Exception e) =>
m a -> (e -> m a) -> m a
`catchIO` \ IOException
e -> do
    NonEmpty LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' [ IOException -> FilePath -> LibError'
ReadError IOException
e FilePath
"Failed to read installed libraries." ]
    [AgdaLibFile] -> LibErrorIO [AgdaLibFile]
forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Parse the given library files.
--
parseLibFiles
  :: Maybe LibrariesFile       -- ^ Name of @libraries@ file for error reporting.
  -> [(LineNumber, FilePath)]  -- ^ Library files paired with their line number in @libraries@.
  -> LibErrorIO [AgdaLibFile]  -- ^ Content of library files.  (Might have empty @LibName@s.)
parseLibFiles :: Maybe LibrariesFile
-> [(Int, FilePath)] -> LibErrorIO [AgdaLibFile]
parseLibFiles Maybe LibrariesFile
mlibFile [(Int, FilePath)]
files = do

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

  let (xs, warns) = unzip anns
      (errs, als) = partitionEithers xs

  List1.unlessNull (concat warns) warnings
  List1.unlessNull errs $ \ List1 (Maybe LibPositionInfo, LibParseError)
errs1 ->
    List1 LibError -> WriterT LibErrWarns (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibError -> m ()
raiseErrors (List1 LibError -> WriterT LibErrWarns (StateT LibState IO) ())
-> List1 LibError -> WriterT LibErrWarns (StateT LibState IO) ()
forall a b. (a -> b) -> a -> b
$ ((Maybe LibPositionInfo, LibParseError) -> LibError)
-> List1 (Maybe LibPositionInfo, LibParseError) -> List1 LibError
forall a b. (a -> b) -> NonEmpty a -> NonEmpty 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 (LibError' -> LibError) -> LibError' -> LibError
forall a b. (a -> b) -> a -> b
$ LibParseError -> LibError'
LibParseError LibParseError
err) List1 (Maybe LibPositionInfo, LibParseError)
errs1

  return $ nubOn _libFile als

-- | Remove trailing white space and line comments.
--
stripCommentLines :: String -> [(LineNumber, String)]
stripCommentLines :: FilePath -> [(Int, FilePath)]
stripCommentLines = ((Int, FilePath) -> [(Int, FilePath)])
-> [(Int, FilePath)] -> [(Int, FilePath)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, FilePath) -> [(Int, FilePath)]
forall {a}. (a, FilePath) -> [(a, FilePath)]
strip ([(Int, FilePath)] -> [(Int, FilePath)])
-> (FilePath -> [(Int, FilePath)]) -> FilePath -> [(Int, FilePath)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [FilePath] -> [(Int, FilePath)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
Item [Int]
1..] ([FilePath] -> [(Int, FilePath)])
-> (FilePath -> [FilePath]) -> FilePath -> [(Int, FilePath)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
lines
  where
    strip :: (a, FilePath) -> [(a, FilePath)]
strip (a
i, FilePath
s) = [ (a
i, FilePath
s') | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
s' ]
      where s' :: FilePath
s' = FilePath -> FilePath
trimLineComment FilePath
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
  agdaDir <- IO FilePath
getAgdaAppDir
  let defaults = (FilePath -> FilePath) -> NonEmpty FilePath -> NonEmpty FilePath
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
List1.map (FilePath
agdaDir FilePath -> FilePath -> FilePath
</>) NonEmpty FilePath
defaultExecutableFiles  -- NB: very short list
  findM doesFileExist defaults >>= \case
    Just FilePath
file -> ExecutablesFile -> IO ExecutablesFile
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecutablesFile -> IO ExecutablesFile)
-> ExecutablesFile -> IO ExecutablesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> ExecutablesFile
ExecutablesFile FilePath
file Bool
True
    Maybe FilePath
Nothing   -> ExecutablesFile -> IO ExecutablesFile
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExecutablesFile -> IO ExecutablesFile)
-> ExecutablesFile -> IO ExecutablesFile
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> ExecutablesFile
ExecutablesFile (NonEmpty FilePath -> FilePath
forall a. NonEmpty a -> a
List1.last NonEmpty FilePath
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 Text FilePath)
getTrustedExecutables = [AgdaLibFile]
-> LibErrorIO (Map Text FilePath) -> LibM (Map Text FilePath)
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [] (LibErrorIO (Map Text FilePath) -> LibM (Map Text FilePath))
-> LibErrorIO (Map Text FilePath) -> LibM (Map Text FilePath)
forall a b. (a -> b) -> a -> b
$ do
    file <- IO ExecutablesFile
-> WriterT LibErrWarns (StateT LibState IO) ExecutablesFile
forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ExecutablesFile
getExecutablesFile
    if not (efExists file) then return Map.empty else do
      es    <- liftIO $ stripCommentLines <$> UTF8.readFile (efPath file)
      lines <- liftIO $ mapM (secondM expandEnvironmentVariables) es
      parseExecutablesFile file lines
  LibErrorIO (Map Text FilePath)
-> (IOException -> LibErrorIO (Map Text FilePath))
-> LibErrorIO (Map Text FilePath)
forall e a.
Exception e =>
WriterT LibErrWarns (StateT LibState IO) a
-> (e -> WriterT LibErrWarns (StateT LibState IO) a)
-> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) e a.
(CatchIO m, Exception e) =>
m a -> (e -> m a) -> m a
`catchIO` \ IOException
e -> do
    NonEmpty LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' [ IOException -> FilePath -> LibError'
ReadError IOException
e FilePath
"Failed to read trusted executables." ]
    Map Text FilePath -> LibErrorIO (Map Text FilePath)
forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Map Text FilePath
forall k a. Map k a
Map.empty

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

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

  -- Separate non-ambiguous from ambiguous mappings.
  let (exeMap, duplicates) = Map.mapEither List2.fromList1Either exeMap1

  -- Report ambiguous mappings with line numbers.
  List1.unlessNull (Map.toList duplicates) $ \ List1 (Text, List2 (Int, FilePath))
duplicates1 ->
    NonEmpty LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' (NonEmpty LibError' -> WriterT LibErrWarns (StateT LibState IO) ())
-> NonEmpty LibError'
-> WriterT LibErrWarns (StateT LibState IO) ()
forall a b. (a -> b) -> a -> b
$ ((Text, List2 (Int, FilePath)) -> LibError')
-> List1 (Text, List2 (Int, FilePath)) -> NonEmpty LibError'
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Text -> List2 (Int, FilePath) -> LibError')
-> (Text, List2 (Int, FilePath)) -> LibError'
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Text -> List2 (Int, FilePath) -> LibError')
 -> (Text, List2 (Int, FilePath)) -> LibError')
-> (Text -> List2 (Int, FilePath) -> LibError')
-> (Text, List2 (Int, FilePath))
-> LibError'
forall a b. (a -> b) -> a -> b
$ FilePath -> Text -> List2 (Int, FilePath) -> LibError'
DuplicateExecutable (FilePath -> Text -> List2 (Int, FilePath) -> LibError')
-> FilePath -> Text -> List2 (Int, FilePath) -> LibError'
forall a b. (a -> b) -> a -> b
$ ExecutablesFile -> FilePath
efPath ExecutablesFile
ef) List1 (Text, List2 (Int, FilePath))
duplicates1

  -- Return non-ambiguous mappings without line numbers.
  return $ fmap snd exeMap

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

-- | Get all include pathes for a list of libraries to use.
--
--   Warns if a library is depended on in different versions
--   (see 'libraryVersionConflicts').
libraryIncludePaths
  :: Maybe FilePath     -- ^ @libraries@ file (error reporting only).
  -> Maybe AgdaLibFile  -- ^ The project the libraries are used by, if any (warnings only).
  -> [AgdaLibFile]      -- ^ Libraries Agda knows about.
  -> [LibName]          -- ^ (Non-empty) library names to be resolved to (lists of) pathes.
  -> LibM [FilePath]    -- ^ Resolved pathes (no duplicates).  Contains "." if @[LibName]@ does.
libraryIncludePaths :: Maybe FilePath
-> Maybe AgdaLibFile
-> [AgdaLibFile]
-> [LibName]
-> ExceptT
     LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
libraryIncludePaths Maybe FilePath
overrideLibFile Maybe AgdaLibFile
root [AgdaLibFile]
libs [LibName]
xs0 = [AgdaLibFile]
-> WriterT LibErrWarns (StateT LibState IO) [FilePath]
-> ExceptT
     LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
forall a. [AgdaLibFile] -> LibErrorIO a -> LibM a
mkLibM [AgdaLibFile]
libs (WriterT LibErrWarns (StateT LibState IO) [FilePath]
 -> ExceptT
      LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath])
-> WriterT LibErrWarns (StateT LibState IO) [FilePath]
-> ExceptT
     LibErrors (WriterT [LibWarning] (StateT LibState IO)) [FilePath]
forall a b. (a -> b) -> a -> b
$ do
    efile <- IO (Either FilePath LibrariesFile)
-> WriterT
     LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
forall a. IO a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either FilePath LibrariesFile)
 -> WriterT
      LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile))
-> IO (Either FilePath LibrariesFile)
-> WriterT
     LibErrWarns (StateT LibState IO) (Either FilePath LibrariesFile)
forall a b. (a -> b) -> a -> b
$ ExceptT FilePath IO LibrariesFile
-> IO (Either FilePath LibrariesFile)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT FilePath IO LibrariesFile
 -> IO (Either FilePath LibrariesFile))
-> ExceptT FilePath IO LibrariesFile
-> IO (Either FilePath LibrariesFile)
forall a b. (a -> b) -> a -> b
$ Maybe FilePath -> ExceptT FilePath IO LibrariesFile
forall (m :: * -> *).
(MonadIO m, MonadError FilePath m) =>
Maybe FilePath -> m LibrariesFile
getLibrariesFile Maybe FilePath
overrideLibFile
    case efile of
      Left FilePath
theOverrideLibFile -> do
        NonEmpty LibError' -> WriterT LibErrWarns (StateT LibState IO) ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' [ FilePath -> LibError'
LibrariesFileNotFound FilePath
theOverrideLibFile ]
        [FilePath] -> WriterT LibErrWarns (StateT LibState IO) [FilePath]
forall a. a -> WriterT LibErrWarns (StateT LibState IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Right LibrariesFile
file -> do
        (ls, resolved) <- Writer LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
-> WriterT
     LibErrWarns
     (StateT LibState IO)
     ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
forall (m :: * -> *) w a. Monad m => Writer w a -> WriterT w m a
embedWriter (Writer
   LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
 -> WriterT
      LibErrWarns
      (StateT LibState IO)
      ([AgdaLibFile], Map LibName (Maybe AgdaLibFile)))
-> Writer
     LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
-> WriterT
     LibErrWarns
     (StateT LibState IO)
     ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
forall a b. (a -> b) -> a -> b
$ LibrariesFile
-> Map LibName (Maybe AgdaLibFile)
-> [LibName]
-> Writer
     LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
find LibrariesFile
file Map LibName (Maybe AgdaLibFile)
forall k a. Map k a
Map.empty [LibName]
xs
        ws <- liftIO $ libraryVersionConflicts root xs $ Map.mapMaybe id resolved
        List1.unlessNull ws warnings'
        return $ dot ++ incs ls
  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]
xs0
    incs :: [AgdaLibFile] -> [FilePath]
incs       = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn FilePath -> FilePath
forall a. a -> a
id ([FilePath] -> [FilePath])
-> ([AgdaLibFile] -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AgdaLibFile -> [FilePath]) -> [AgdaLibFile] -> [FilePath]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap AgdaLibFile -> [FilePath]
_libIncludes
    dot :: [FilePath]
dot        = [ FilePath
"." | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [LibName] -> Bool
forall a. [a] -> 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.
      -> Map LibName (Maybe AgdaLibFile)
                        -- Already processed libraries and what they resolved to.
      -> [LibName]      -- Work list: libraries left to be resolved.
      -> Writer LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
    find :: LibrariesFile
-> Map LibName (Maybe AgdaLibFile)
-> [LibName]
-> Writer
     LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
find LibrariesFile
_ Map LibName (Maybe AgdaLibFile)
visited [] = ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
-> Writer
     LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
forall a. a -> WriterT LibErrWarns Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], Map LibName (Maybe AgdaLibFile)
visited)
    find LibrariesFile
file Map LibName (Maybe AgdaLibFile)
visited (LibName
x : [LibName]
xs)
      | LibName
x LibName -> Map LibName (Maybe AgdaLibFile) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map LibName (Maybe AgdaLibFile)
visited = LibrariesFile
-> Map LibName (Maybe AgdaLibFile)
-> [LibName]
-> Writer
     LibErrWarns ([AgdaLibFile], Map LibName (Maybe AgdaLibFile))
find LibrariesFile
file Map LibName (Maybe AgdaLibFile)
visited [LibName]
xs
      | Bool
otherwise = do
          -- May or may not find the library
          ml <- case LibName -> [AgdaLibFile] -> [AgdaLibFile]
findLib LibName
x [AgdaLibFile]
libs of
            [Item [AgdaLibFile]
l] -> Maybe AgdaLibFile
-> WriterT LibErrWarns Identity (Maybe AgdaLibFile)
forall a. a -> WriterT LibErrWarns Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AgdaLibFile -> Maybe AgdaLibFile
forall a. a -> Maybe a
Just Item [AgdaLibFile]
AgdaLibFile
l)
            []  -> Maybe AgdaLibFile
forall a. Maybe a
Nothing Maybe AgdaLibFile
-> WriterT LibErrWarns Identity ()
-> WriterT LibErrWarns Identity (Maybe AgdaLibFile)
forall a b.
a
-> WriterT LibErrWarns Identity b -> WriterT LibErrWarns Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NonEmpty LibError' -> WriterT LibErrWarns Identity ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' [LibrariesFile -> LibName -> LibError'
LibNotFound LibrariesFile
file LibName
x]
            AgdaLibFile
l1 : AgdaLibFile
l2 : [AgdaLibFile]
ls  -> Maybe AgdaLibFile
forall a. Maybe a
Nothing Maybe AgdaLibFile
-> WriterT LibErrWarns Identity ()
-> WriterT LibErrWarns Identity (Maybe AgdaLibFile)
forall a b.
a
-> WriterT LibErrWarns Identity b -> WriterT LibErrWarns Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ NonEmpty LibError' -> WriterT LibErrWarns Identity ()
forall (m :: * -> *).
MonadWriter LibErrWarns m =>
NonEmpty LibError' -> m ()
raiseErrors' [LibName -> List2 AgdaLibFile -> LibError'
AmbiguousLib LibName
x (List2 AgdaLibFile -> LibError') -> List2 AgdaLibFile -> LibError'
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> AgdaLibFile -> [AgdaLibFile] -> List2 AgdaLibFile
forall a. a -> a -> [a] -> List2 a
List2 AgdaLibFile
l1 AgdaLibFile
l2 [AgdaLibFile]
ls]
          -- If it is found, add its dependencies to work list
          let xs' = (AgdaLibFile -> [LibName]) -> Maybe AgdaLibFile -> [LibName]
forall m a. Monoid m => (a -> m) -> Maybe a -> m
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
          first (mcons ml) <$> find file (Map.insert x ml visited) xs'

-- | Detect libraries that are depended on in different versions (issue #8875).
--
--   For each such library, we return a 'LibraryVersionConflict' warning
--   containing the dependency tree pruned to the paths leading to the conflicting versions.
--
libraryVersionConflicts
  :: Maybe AgdaLibFile        -- ^ The project, if any.
  -> [LibName]                -- ^ The libraries the project depends on.
  -> Map LibName AgdaLibFile  -- ^ What the (transitively) depended-on libraries resolved to.
  -> IO [LibWarning']
libraryVersionConflicts :: Maybe AgdaLibFile
-> [LibName] -> Map LibName AgdaLibFile -> IO [LibWarning']
libraryVersionConflicts Maybe AgdaLibFile
root [LibName]
roots Map LibName AgdaLibFile
resolved = do
  -- We identify libraries by the canonical path of their @.agda-lib@ file.
  -- Also, the canonical paths are absolute, so the Emacs mode can make them clickable.
  let canon :: AgdaLibFile -> IO AgdaLibFile
canon AgdaLibFile
l = do
        f <- FilePath -> IO FilePath
canonicalizePath (AgdaLibFile -> FilePath
_libFile AgdaLibFile
l) IO FilePath -> (IOException -> IO FilePath) -> IO FilePath
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
forall (m :: * -> *) e a.
(CatchIO m, Exception e) =>
m a -> (e -> m a) -> m a
`catchIO` \ (IOException
_ :: E.IOException) -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (AgdaLibFile -> FilePath
_libFile AgdaLibFile
l)
        pure l{ _libFile = f }
  root     <- (AgdaLibFile -> IO AgdaLibFile)
-> Maybe AgdaLibFile -> IO (Maybe AgdaLibFile)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse AgdaLibFile -> IO AgdaLibFile
canon Maybe AgdaLibFile
root
  resolved <- traverse canon resolved
  pure $ libraryVersionConflicts' root roots resolved

-- | Pure part of 'libraryVersionConflicts'.
libraryVersionConflicts'
  :: Maybe AgdaLibFile        -- ^ The project, if any.
  -> [LibName]                -- ^ The libraries the project depends on.
  -> Map LibName AgdaLibFile  -- ^ What the (transitively) depended-on libraries resolved to.
  -> [LibWarning']
libraryVersionConflicts' :: Maybe AgdaLibFile
-> [LibName] -> Map LibName AgdaLibFile -> [LibWarning']
libraryVersionConflicts' Maybe AgdaLibFile
root [LibName]
roots Map LibName AgdaLibFile
resolved =
  [ Text -> Set FilePath -> LibWarning'
conflict Text
b Set FilePath
fs | (Text
b, Set FilePath
fs) <- Map Text (Set FilePath) -> [(Text, Set FilePath)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Text (Set FilePath)
groups, Set FilePath -> Int
forall a. Set a -> Int
Set.size Set FilePath
fs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 ]
  where
  -- The distinct library files, grouped by the base name of their library.
  groups :: Map T.Text (Set FilePath)
  groups :: Map Text (Set FilePath)
groups = (Set FilePath -> Set FilePath -> Set FilePath)
-> [(Text, Set FilePath)] -> Map Text (Set FilePath)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Set FilePath -> Set FilePath -> Set FilePath
forall a. Ord a => Set a -> Set a -> Set a
Set.union
    [ (Text
b, FilePath -> Set FilePath
forall a. a -> Set a
Set.singleton (FilePath -> Set FilePath) -> FilePath -> Set FilePath
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libFile AgdaLibFile
l)
    | AgdaLibFile
l <- Maybe AgdaLibFile -> [AgdaLibFile]
forall a. Maybe a -> [a]
maybeToList Maybe AgdaLibFile
root [AgdaLibFile] -> [AgdaLibFile] -> [AgdaLibFile]
forall a. [a] -> [a] -> [a]
++ Map LibName AgdaLibFile -> [AgdaLibFile]
forall k a. Map k a -> [a]
Map.elems Map LibName AgdaLibFile
resolved
    , let b :: Text
b = LibName -> Text
libNameBase (LibName -> Text) -> LibName -> Text
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> LibName
_libName AgdaLibFile
l
    , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> Bool
T.null Text
b
    ]

  -- The dependencies of a library.
  deps :: LibName -> [LibName]
  deps :: LibName -> [LibName]
deps LibName
x = (LibName -> LibName) -> [LibName] -> [LibName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn LibName -> LibName
forall a. a -> a
id ([LibName] -> [LibName]) -> [LibName] -> [LibName]
forall a b. (a -> b) -> a -> b
$ (AgdaLibFile -> [LibName]) -> Maybe AgdaLibFile -> [LibName]
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap AgdaLibFile -> [LibName]
_libDepends (Maybe AgdaLibFile -> [LibName]) -> Maybe AgdaLibFile -> [LibName]
forall a b. (a -> b) -> a -> b
$ LibName -> Map LibName AgdaLibFile -> Maybe AgdaLibFile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
x Map LibName AgdaLibFile
resolved

  label :: LibName -> T.Text
  label :: LibName -> Text
label = FilePath -> Text
T.pack (FilePath -> Text) -> (LibName -> FilePath) -> LibName -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibName -> FilePath
forall a. Pretty a => a -> FilePath
prettyShow

  rootLabel :: T.Text
  rootLabel :: Text
rootLabel = case Maybe AgdaLibFile
root of
    Just AgdaLibFile
l | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> Bool
T.null (Text -> Bool) -> Text -> Bool
forall a b. (a -> b) -> a -> b
$ LibName -> Text
libNameBase (LibName -> Text) -> LibName -> Text
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> LibName
_libName AgdaLibFile
l -> LibName -> Text
label (LibName -> Text) -> LibName -> Text
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> LibName
_libName AgdaLibFile
l
    Maybe AgdaLibFile
_ -> Text
libDepRootLabel

  -- The name a library resolved to, if different from the requested name.
  resolvedAs :: LibName -> Maybe T.Text
  resolvedAs :: LibName -> Maybe Text
resolvedAs LibName
x = case AgdaLibFile -> LibName
_libName (AgdaLibFile -> LibName) -> Maybe AgdaLibFile -> Maybe LibName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LibName -> Map LibName AgdaLibFile -> Maybe AgdaLibFile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
x Map LibName AgdaLibFile
resolved of
    Just LibName
y | LibName
y LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
/= LibName
x -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ LibName -> Text
label LibName
y
    Maybe LibName
_ -> Maybe Text
forall a. Maybe a
Nothing

  conflict :: T.Text -> Set FilePath -> LibWarning'
  conflict :: Text -> Set FilePath -> LibWarning'
conflict Text
b Set FilePath
fs = Text
-> LibDepTree
-> [(Text, FilePath, Maybe LibFilePos)]
-> LibWarning'
LibraryVersionConflict Text
b LibDepTree
tree [(Text, FilePath, Maybe LibFilePos)]
files
    where
    -- The libraries resolving to a conflicting version or depending on such.
    relevant :: Set LibName
    relevant :: Set LibName
relevant = Set LibName -> Set LibName
saturate (Set LibName -> Set LibName) -> Set LibName -> Set LibName
forall a b. (a -> b) -> a -> b
$ Map LibName AgdaLibFile -> Set LibName
forall k a. Map k a -> Set k
Map.keysSet (Map LibName AgdaLibFile -> Set LibName)
-> Map LibName AgdaLibFile -> Set LibName
forall a b. (a -> b) -> a -> b
$ (AgdaLibFile -> Bool)
-> Map LibName AgdaLibFile -> Map LibName AgdaLibFile
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter ((FilePath -> Set FilePath -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set FilePath
fs) (FilePath -> Bool)
-> (AgdaLibFile -> FilePath) -> AgdaLibFile -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaLibFile -> FilePath
_libFile) Map LibName AgdaLibFile
resolved

    saturate :: Set LibName -> Set LibName
    saturate :: Set LibName -> Set LibName
saturate Set LibName
s
      | Set LibName -> Int
forall a. Set a -> Int
Set.size Set LibName
s' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Set LibName -> Int
forall a. Set a -> Int
Set.size Set LibName
s = Set LibName
s
      | Bool
otherwise                 = Set LibName -> Set LibName
saturate Set LibName
s'
      where
        s' :: Set LibName
s' = Set LibName -> Set LibName -> Set LibName
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set LibName
s (Set LibName -> Set LibName) -> Set LibName -> Set LibName
forall a b. (a -> b) -> a -> b
$ Map LibName AgdaLibFile -> Set LibName
forall k a. Map k a -> Set k
Map.keysSet (Map LibName AgdaLibFile -> Set LibName)
-> Map LibName AgdaLibFile -> Set LibName
forall a b. (a -> b) -> a -> b
$
               (LibName -> AgdaLibFile -> Bool)
-> Map LibName AgdaLibFile -> Map LibName AgdaLibFile
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ LibName
x AgdaLibFile
_ -> (LibName -> Bool) -> [LibName] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (LibName -> Set LibName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set LibName
s) ([LibName] -> Bool) -> [LibName] -> Bool
forall a b. (a -> b) -> a -> b
$ LibName -> [LibName]
deps LibName
x) Map LibName AgdaLibFile
resolved

    relevantOnly :: [LibName] -> [LibName]
    relevantOnly :: [LibName] -> [LibName]
relevantOnly = (LibName -> Bool) -> [LibName] -> [LibName]
forall a. (a -> Bool) -> [a] -> [a]
filter (LibName -> Set LibName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set LibName
relevant)

    -- A library resolving to one of the conflicting versions.
    conflicting :: LibName -> Bool
    conflicting :: LibName -> Bool
conflicting LibName
x = Bool -> (AgdaLibFile -> Bool) -> Maybe AgdaLibFile -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((FilePath -> Set FilePath -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set FilePath
fs) (FilePath -> Bool)
-> (AgdaLibFile -> FilePath) -> AgdaLibFile -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaLibFile -> FilePath
_libFile) (Maybe AgdaLibFile -> Bool) -> Maybe AgdaLibFile -> Bool
forall a b. (a -> b) -> a -> b
$ LibName -> Map LibName AgdaLibFile -> Maybe AgdaLibFile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
x Map LibName AgdaLibFile
resolved

    tree :: LibDepTree
    tree :: LibDepTree
tree = LibDepNode -> [LibDepTree] -> LibDepTree
forall a. a -> [Tree a] -> Tree a
Node (Text -> Maybe Text -> LibDepNode
LibDepNode Text
rootLabel Maybe Text
forall a. Maybe a
Nothing) ([LibDepTree] -> LibDepTree) -> [LibDepTree] -> LibDepTree
forall a b. (a -> b) -> a -> b
$ (Set LibName, [LibDepTree]) -> [LibDepTree]
forall a b. (a, b) -> b
snd ((Set LibName, [LibDepTree]) -> [LibDepTree])
-> (Set LibName, [LibDepTree]) -> [LibDepTree]
forall a b. (a -> b) -> a -> b
$
      Set LibName -> [LibName] -> (Set LibName, [LibDepTree])
expand Set LibName
forall a. Set a
Set.empty ([LibName] -> (Set LibName, [LibDepTree]))
-> [LibName] -> (Set LibName, [LibDepTree])
forall a b. (a -> b) -> a -> b
$ [LibName] -> [LibName]
relevantOnly ([LibName] -> [LibName]) -> [LibName] -> [LibName]
forall a b. (a -> b) -> a -> b
$ (LibName -> LibName) -> [LibName] -> [LibName]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn LibName -> LibName
forall a. a -> a
id [LibName]
roots

    -- Expand the given siblings from left to right.
    expand :: Set LibName -> [LibName] -> (Set LibName, [LibDepTree])
    expand :: Set LibName -> [LibName] -> (Set LibName, [LibDepTree])
expand Set LibName
seen = ([Maybe LibDepTree] -> [LibDepTree])
-> (Set LibName, [Maybe LibDepTree]) -> (Set LibName, [LibDepTree])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [Maybe LibDepTree] -> [LibDepTree]
forall a. [Maybe a] -> [a]
catMaybes ((Set LibName, [Maybe LibDepTree]) -> (Set LibName, [LibDepTree]))
-> ([LibName] -> (Set LibName, [Maybe LibDepTree]))
-> [LibName]
-> (Set LibName, [LibDepTree])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set LibName -> LibName -> (Set LibName, Maybe LibDepTree))
-> Set LibName -> [LibName] -> (Set LibName, [Maybe LibDepTree])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
List.mapAccumL Set LibName -> LibName -> (Set LibName, Maybe LibDepTree)
visit Set LibName
seen

    -- A library that has been visited before is omitted.
    -- So is a library which does not lead to a conflicting version not shown before.
    visit :: Set LibName -> LibName -> (Set LibName, Maybe LibDepTree)
    visit :: Set LibName -> LibName -> (Set LibName, Maybe LibDepTree)
visit Set LibName
seen LibName
x
      | LibName
x LibName -> Set LibName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set LibName
seen = (Set LibName
seen, Maybe LibDepTree
forall a. Maybe a
Nothing)
      | Bool
otherwise           = ([LibDepTree] -> Maybe LibDepTree)
-> (Set LibName, [LibDepTree]) -> (Set LibName, Maybe LibDepTree)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [LibDepTree] -> Maybe LibDepTree
prune ((Set LibName, [LibDepTree]) -> (Set LibName, Maybe LibDepTree))
-> (Set LibName, [LibDepTree]) -> (Set LibName, Maybe LibDepTree)
forall a b. (a -> b) -> a -> b
$ Set LibName -> [LibName] -> (Set LibName, [LibDepTree])
expand (LibName -> Set LibName -> Set LibName
forall a. Ord a => a -> Set a -> Set a
Set.insert LibName
x Set LibName
seen) ([LibName] -> (Set LibName, [LibDepTree]))
-> [LibName] -> (Set LibName, [LibDepTree])
forall a b. (a -> b) -> a -> b
$ [LibName] -> [LibName]
relevantOnly ([LibName] -> [LibName]) -> [LibName] -> [LibName]
forall a b. (a -> b) -> a -> b
$ LibName -> [LibName]
deps LibName
x
      where
        prune :: [LibDepTree] -> Maybe LibDepTree
prune [LibDepTree]
ts
          | [LibDepTree] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LibDepTree]
ts Bool -> Bool -> Bool
&& Bool -> Bool
not (LibName -> Bool
conflicting LibName
x) = Maybe LibDepTree
forall a. Maybe a
Nothing
          | Bool
otherwise                      = LibDepTree -> Maybe LibDepTree
forall a. a -> Maybe a
Just (LibDepTree -> Maybe LibDepTree) -> LibDepTree -> Maybe LibDepTree
forall a b. (a -> b) -> a -> b
$ LibDepNode -> [LibDepTree] -> LibDepTree
forall a. a -> [Tree a] -> Tree a
Node (Text -> Maybe Text -> LibDepNode
LibDepNode (LibName -> Text
label LibName
x) (LibName -> Maybe Text
resolvedAs LibName
x)) [LibDepTree]
ts

    -- The files of the libraries mentioned in the tree, in order of first occurrence,
    -- with the position of the first dependency shown in the tree.
    files :: [(T.Text, FilePath, Maybe LibFilePos)]
    files :: [(Text, FilePath, Maybe LibFilePos)]
files = ((Text, FilePath, Maybe LibFilePos) -> (Text, FilePath))
-> [(Text, FilePath, Maybe LibFilePos)]
-> [(Text, FilePath, Maybe LibFilePos)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOn (\ (Text
l, FilePath
f, Maybe LibFilePos
_) -> (Text
l, FilePath
f)) ([(Text, FilePath, Maybe LibFilePos)]
 -> [(Text, FilePath, Maybe LibFilePos)])
-> [(Text, FilePath, Maybe LibFilePos)]
-> [(Text, FilePath, Maybe LibFilePos)]
forall a b. (a -> b) -> a -> b
$
      [ (Text
rootLabel, AgdaLibFile -> FilePath
_libFile AgdaLibFile
l, AgdaLibFile -> [LibDepTree] -> Maybe LibFilePos
firstDepPos AgdaLibFile
l [LibDepTree]
ts) | AgdaLibFile
l <- Maybe AgdaLibFile -> [AgdaLibFile]
forall a. Maybe a -> [a]
maybeToList Maybe AgdaLibFile
root ] [(Text, FilePath, Maybe LibFilePos)]
-> [(Text, FilePath, Maybe LibFilePos)]
-> [(Text, FilePath, Maybe LibFilePos)]
forall a. [a] -> [a] -> [a]
++
      (LibDepTree -> [(Text, FilePath, Maybe LibFilePos)])
-> [LibDepTree] -> [(Text, FilePath, Maybe LibFilePos)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LibDepTree -> [(Text, FilePath, Maybe LibFilePos)]
entries [LibDepTree]
ts
      where Node LibDepNode
_ [LibDepTree]
ts = LibDepTree
tree

    entries :: LibDepTree -> [(T.Text, FilePath, Maybe LibFilePos)]
    entries :: LibDepTree -> [(Text, FilePath, Maybe LibFilePos)]
entries (Node LibDepNode
n [LibDepTree]
ts) =
      [ (LibDepNode -> Text
depLabel LibDepNode
n, AgdaLibFile -> FilePath
_libFile AgdaLibFile
l, AgdaLibFile -> [LibDepTree] -> Maybe LibFilePos
firstDepPos AgdaLibFile
l [LibDepTree]
ts) | AgdaLibFile
l <- Maybe AgdaLibFile -> [AgdaLibFile]
forall a. Maybe a -> [a]
maybeToList (Maybe AgdaLibFile -> [AgdaLibFile])
-> Maybe AgdaLibFile -> [AgdaLibFile]
forall a b. (a -> b) -> a -> b
$ Text -> Map Text AgdaLibFile -> Maybe AgdaLibFile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibDepNode -> Text
depLabel LibDepNode
n) Map Text AgdaLibFile
libOf ] [(Text, FilePath, Maybe LibFilePos)]
-> [(Text, FilePath, Maybe LibFilePos)]
-> [(Text, FilePath, Maybe LibFilePos)]
forall a. [a] -> [a] -> [a]
++
      (LibDepTree -> [(Text, FilePath, Maybe LibFilePos)])
-> [LibDepTree] -> [(Text, FilePath, Maybe LibFilePos)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap LibDepTree -> [(Text, FilePath, Maybe LibFilePos)]
entries [LibDepTree]
ts

    -- Where the first of the given dependencies is mentioned in the given library file.
    firstDepPos :: AgdaLibFile -> [LibDepTree] -> Maybe LibFilePos
    firstDepPos :: AgdaLibFile -> [LibDepTree] -> Maybe LibFilePos
firstDepPos AgdaLibFile
l = \case
      Node LibDepNode
n [LibDepTree]
_ : [LibDepTree]
_ -> Text -> Map Text LibFilePos -> Maybe LibFilePos
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (LibDepNode -> Text
depLabel LibDepNode
n) (Map Text LibFilePos -> Maybe LibFilePos)
-> Map Text LibFilePos -> Maybe LibFilePos
forall a b. (a -> b) -> a -> b
$ (LibName -> Text) -> Map LibName LibFilePos -> Map Text LibFilePos
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys LibName -> Text
label (Map LibName LibFilePos -> Map Text LibFilePos)
-> Map LibName LibFilePos -> Map Text LibFilePos
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> Map LibName LibFilePos
_libDependsPos AgdaLibFile
l
      [] -> Maybe LibFilePos
forall a. Maybe a
Nothing

    libOf :: Map T.Text AgdaLibFile
    libOf :: Map Text AgdaLibFile
libOf = [(Text, AgdaLibFile)] -> Map Text AgdaLibFile
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (LibName -> Text
label LibName
x, AgdaLibFile
l) | (LibName
x, AgdaLibFile
l) <- Map LibName AgdaLibFile -> [(LibName, AgdaLibFile)]
forall k a. Map k a -> [(k, a)]
Map.toList Map LibName AgdaLibFile
resolved ]

-- | @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' :: forall a. (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 -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
(==) (LibName -> LibName -> Bool) -> (a -> LibName) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> LibName
libName) 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 -> LibName -> Ordering) -> LibName -> LibName -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip LibName -> LibName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LibName -> LibName -> Ordering)
-> (a -> LibName) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> LibName
libName) [ 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

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