-- | Basic data types for library management.

module Agda.Interaction.Library.Base where

import Prelude hiding (null)

import Control.DeepSeq
import qualified Control.Exception as E

import Control.Monad.Except
import Control.Monad.State
import Control.Monad.Writer        ( WriterT, MonadWriter, tell )
import Control.Monad.IO.Class      ( MonadIO(..) )

import Data.Bifunctor              ( first , second )
import Data.Map                    ( Map )
import qualified Data.Map          as Map
import Data.Semigroup              ( Semigroup(..) )
import Data.Text                   ( Text, unpack )

import GHC.Generics                ( Generic )

import System.Directory

import Agda.Interaction.Options.Warnings

import Agda.Syntax.Position

import Agda.Utils.IO               ( showIOException )
import Agda.Utils.Lens
import Agda.Utils.List1            ( List1, toList )
import Agda.Utils.List2            ( List2, toList )
import qualified Agda.Utils.List1  as List1
import Agda.Utils.Null
import Agda.Syntax.Common.Pretty

-- | A symbolic library name.
--
type LibName = String

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

-- | A symbolic executable name.
--
type ExeName = Text

data ExecutablesFile = ExecutablesFile
  { ExecutablesFile -> FilePath
efPath   :: FilePath
      -- ^ E.g. @~/.agda/executables@.
  , ExecutablesFile -> Bool
efExists :: Bool
       -- ^ The executables file might not exist,
       --   but we may print its assumed location in error messages.
  } deriving (LineNumber -> ExecutablesFile -> ShowS
[ExecutablesFile] -> ShowS
ExecutablesFile -> FilePath
(LineNumber -> ExecutablesFile -> ShowS)
-> (ExecutablesFile -> FilePath)
-> ([ExecutablesFile] -> ShowS)
-> Show ExecutablesFile
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> ExecutablesFile -> ShowS
showsPrec :: LineNumber -> ExecutablesFile -> ShowS
$cshow :: ExecutablesFile -> FilePath
show :: ExecutablesFile -> FilePath
$cshowList :: [ExecutablesFile] -> ShowS
showList :: [ExecutablesFile] -> ShowS
Show, (forall x. ExecutablesFile -> Rep ExecutablesFile x)
-> (forall x. Rep ExecutablesFile x -> ExecutablesFile)
-> Generic ExecutablesFile
forall x. Rep ExecutablesFile x -> ExecutablesFile
forall x. ExecutablesFile -> Rep ExecutablesFile x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ExecutablesFile -> Rep ExecutablesFile x
from :: forall x. ExecutablesFile -> Rep ExecutablesFile x
$cto :: forall x. Rep ExecutablesFile x -> ExecutablesFile
to :: forall x. Rep ExecutablesFile x -> ExecutablesFile
Generic)

-- | The special name @\".\"@ is used to indicated that the current directory
--   should count as a project root.
--
libNameForCurrentDir :: LibName
libNameForCurrentDir :: FilePath
libNameForCurrentDir = FilePath
"."

-- | A file can either belong to a project located at a given root
--   containing one or more .agda-lib files, or be part of the default
--   project.
data ProjectConfig
  = ProjectConfig
    { ProjectConfig -> FilePath
configRoot         :: FilePath
    , ProjectConfig -> [FilePath]
configAgdaLibFiles :: [FilePath]
    , ProjectConfig -> LineNumber
configAbove        :: !Int
      -- ^ How many directories above the Agda file is the @.agda-lib@
      -- file located?
    }
  | DefaultProjectConfig
  deriving (forall x. ProjectConfig -> Rep ProjectConfig x)
-> (forall x. Rep ProjectConfig x -> ProjectConfig)
-> Generic ProjectConfig
forall x. Rep ProjectConfig x -> ProjectConfig
forall x. ProjectConfig -> Rep ProjectConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ProjectConfig -> Rep ProjectConfig x
from :: forall x. ProjectConfig -> Rep ProjectConfig x
$cto :: forall x. Rep ProjectConfig x -> ProjectConfig
to :: forall x. Rep ProjectConfig x -> ProjectConfig
Generic

-- | The options from an @OPTIONS@ pragma (or a @.agda-lib@ file).
--
-- In the future it might be nice to switch to a more structured
-- representation. Note that, currently, there is not a one-to-one
-- correspondence between list elements and options.
data OptionsPragma = OptionsPragma
  { OptionsPragma -> [FilePath]
pragmaStrings :: [String]
    -- ^ The options.
  , OptionsPragma -> Range
pragmaRange :: Range
    -- ^ The range of the options in the pragma (not including things
    -- like an @OPTIONS@ keyword).
  }
  deriving LineNumber -> OptionsPragma -> ShowS
[OptionsPragma] -> ShowS
OptionsPragma -> FilePath
(LineNumber -> OptionsPragma -> ShowS)
-> (OptionsPragma -> FilePath)
-> ([OptionsPragma] -> ShowS)
-> Show OptionsPragma
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> OptionsPragma -> ShowS
showsPrec :: LineNumber -> OptionsPragma -> ShowS
$cshow :: OptionsPragma -> FilePath
show :: OptionsPragma -> FilePath
$cshowList :: [OptionsPragma] -> ShowS
showList :: [OptionsPragma] -> ShowS
Show

instance Semigroup OptionsPragma where
  OptionsPragma { pragmaStrings :: OptionsPragma -> [FilePath]
pragmaStrings = [FilePath]
ss1, pragmaRange :: OptionsPragma -> Range
pragmaRange = Range
r1 } <> :: OptionsPragma -> OptionsPragma -> OptionsPragma
<>
    OptionsPragma { pragmaStrings :: OptionsPragma -> [FilePath]
pragmaStrings = [FilePath]
ss2, pragmaRange :: OptionsPragma -> Range
pragmaRange = Range
r2 } =
    OptionsPragma
      { pragmaStrings :: [FilePath]
pragmaStrings = [FilePath]
ss1 [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
ss2
      , pragmaRange :: Range
pragmaRange   = Range -> Range -> Range
forall a. Ord a => Range' a -> Range' a -> Range' a
fuseRanges Range
r1 Range
r2
      }

instance Monoid OptionsPragma where
  mempty :: OptionsPragma
mempty  = OptionsPragma { pragmaStrings :: [FilePath]
pragmaStrings = [], pragmaRange :: Range
pragmaRange = Range
forall a. Range' a
noRange }
  mappend :: OptionsPragma -> OptionsPragma -> OptionsPragma
mappend = OptionsPragma -> OptionsPragma -> OptionsPragma
forall a. Semigroup a => a -> a -> a
(<>)

-- | Ranges are not forced.

instance NFData OptionsPragma where
  rnf :: OptionsPragma -> ()
rnf (OptionsPragma [FilePath]
a Range
_) = [FilePath] -> ()
forall a. NFData a => a -> ()
rnf [FilePath]
a

-- | Content of a @.agda-lib@ file.
--
data AgdaLibFile = AgdaLibFile
  { AgdaLibFile -> FilePath
_libName     :: LibName     -- ^ The symbolic name of the library.
  , AgdaLibFile -> FilePath
_libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
  , AgdaLibFile -> LineNumber
_libAbove    :: !Int        -- ^ How many directories above the
                                --   Agda file is the @.agda-lib@ file
                                --   located?
  , AgdaLibFile -> [FilePath]
_libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
  , AgdaLibFile -> [FilePath]
_libDepends  :: [LibName]   -- ^ Dependencies.
  , AgdaLibFile -> OptionsPragma
_libPragmas  :: OptionsPragma
                                -- ^ Default pragma options for all files in the library.
  }
  deriving (LineNumber -> AgdaLibFile -> ShowS
[AgdaLibFile] -> ShowS
AgdaLibFile -> FilePath
(LineNumber -> AgdaLibFile -> ShowS)
-> (AgdaLibFile -> FilePath)
-> ([AgdaLibFile] -> ShowS)
-> Show AgdaLibFile
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> AgdaLibFile -> ShowS
showsPrec :: LineNumber -> AgdaLibFile -> ShowS
$cshow :: AgdaLibFile -> FilePath
show :: AgdaLibFile -> FilePath
$cshowList :: [AgdaLibFile] -> ShowS
showList :: [AgdaLibFile] -> ShowS
Show, (forall x. AgdaLibFile -> Rep AgdaLibFile x)
-> (forall x. Rep AgdaLibFile x -> AgdaLibFile)
-> Generic AgdaLibFile
forall x. Rep AgdaLibFile x -> AgdaLibFile
forall x. AgdaLibFile -> Rep AgdaLibFile x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. AgdaLibFile -> Rep AgdaLibFile x
from :: forall x. AgdaLibFile -> Rep AgdaLibFile x
$cto :: forall x. Rep AgdaLibFile x -> AgdaLibFile
to :: forall x. Rep AgdaLibFile x -> AgdaLibFile
Generic)

emptyLibFile :: AgdaLibFile
emptyLibFile :: AgdaLibFile
emptyLibFile = AgdaLibFile
  { _libName :: FilePath
_libName     = FilePath
""
  , _libFile :: FilePath
_libFile     = FilePath
""
  , _libAbove :: LineNumber
_libAbove    = LineNumber
0
  , _libIncludes :: [FilePath]
_libIncludes = []
  , _libDepends :: [FilePath]
_libDepends  = []
  , _libPragmas :: OptionsPragma
_libPragmas  = OptionsPragma
forall a. Monoid a => a
mempty
  }

-- | Lenses for AgdaLibFile

libName :: Lens' AgdaLibFile LibName
libName :: Lens' AgdaLibFile FilePath
libName FilePath -> f FilePath
f AgdaLibFile
a = FilePath -> f FilePath
f (AgdaLibFile -> FilePath
_libName AgdaLibFile
a) f FilePath -> (FilePath -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ FilePath
x -> AgdaLibFile
a { _libName = x }

libFile :: Lens' AgdaLibFile FilePath
libFile :: Lens' AgdaLibFile FilePath
libFile FilePath -> f FilePath
f AgdaLibFile
a = FilePath -> f FilePath
f (AgdaLibFile -> FilePath
_libFile AgdaLibFile
a) f FilePath -> (FilePath -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ FilePath
x -> AgdaLibFile
a { _libFile = x }

libAbove :: Lens' AgdaLibFile Int
libAbove :: Lens' AgdaLibFile LineNumber
libAbove LineNumber -> f LineNumber
f AgdaLibFile
a = LineNumber -> f LineNumber
f (AgdaLibFile -> LineNumber
_libAbove AgdaLibFile
a) f LineNumber -> (LineNumber -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ LineNumber
x -> AgdaLibFile
a { _libAbove = x }

libIncludes :: Lens' AgdaLibFile [FilePath]
libIncludes :: Lens' AgdaLibFile [FilePath]
libIncludes [FilePath] -> f [FilePath]
f AgdaLibFile
a = [FilePath] -> f [FilePath]
f (AgdaLibFile -> [FilePath]
_libIncludes AgdaLibFile
a) f [FilePath] -> ([FilePath] -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [FilePath]
x -> AgdaLibFile
a { _libIncludes = x }

libDepends :: Lens' AgdaLibFile [LibName]
libDepends :: Lens' AgdaLibFile [FilePath]
libDepends [FilePath] -> f [FilePath]
f AgdaLibFile
a = [FilePath] -> f [FilePath]
f (AgdaLibFile -> [FilePath]
_libDepends AgdaLibFile
a) f [FilePath] -> ([FilePath] -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [FilePath]
x -> AgdaLibFile
a { _libDepends = x }

libPragmas :: Lens' AgdaLibFile OptionsPragma
libPragmas :: Lens' AgdaLibFile OptionsPragma
libPragmas OptionsPragma -> f OptionsPragma
f AgdaLibFile
a = OptionsPragma -> f OptionsPragma
f (AgdaLibFile -> OptionsPragma
_libPragmas AgdaLibFile
a) f OptionsPragma -> (OptionsPragma -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ OptionsPragma
x -> AgdaLibFile
a { _libPragmas = x }


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

-- ** Position information

type LineNumber = Int

-- | Information about which @.agda-lib@ file we are reading
--   and from where in the @libraries@ file it came from.

data LibPositionInfo = LibPositionInfo
  { LibPositionInfo -> Maybe FilePath
libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file.
  , LibPositionInfo -> LineNumber
lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
  , LibPositionInfo -> FilePath
filePos    :: FilePath       -- ^ Library file.
  }
  deriving (LineNumber -> LibPositionInfo -> ShowS
[LibPositionInfo] -> ShowS
LibPositionInfo -> FilePath
(LineNumber -> LibPositionInfo -> ShowS)
-> (LibPositionInfo -> FilePath)
-> ([LibPositionInfo] -> ShowS)
-> Show LibPositionInfo
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibPositionInfo -> ShowS
showsPrec :: LineNumber -> LibPositionInfo -> ShowS
$cshow :: LibPositionInfo -> FilePath
show :: LibPositionInfo -> FilePath
$cshowList :: [LibPositionInfo] -> ShowS
showList :: [LibPositionInfo] -> ShowS
Show, (forall x. LibPositionInfo -> Rep LibPositionInfo x)
-> (forall x. Rep LibPositionInfo x -> LibPositionInfo)
-> Generic LibPositionInfo
forall x. Rep LibPositionInfo x -> LibPositionInfo
forall x. LibPositionInfo -> Rep LibPositionInfo x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibPositionInfo -> Rep LibPositionInfo x
from :: forall x. LibPositionInfo -> Rep LibPositionInfo x
$cto :: forall x. Rep LibPositionInfo x -> LibPositionInfo
to :: forall x. Rep LibPositionInfo x -> LibPositionInfo
Generic)

-- ** Warnings

data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
  deriving (LineNumber -> LibWarning -> ShowS
[LibWarning] -> ShowS
LibWarning -> FilePath
(LineNumber -> LibWarning -> ShowS)
-> (LibWarning -> FilePath)
-> ([LibWarning] -> ShowS)
-> Show LibWarning
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibWarning -> ShowS
showsPrec :: LineNumber -> LibWarning -> ShowS
$cshow :: LibWarning -> FilePath
show :: LibWarning -> FilePath
$cshowList :: [LibWarning] -> ShowS
showList :: [LibWarning] -> ShowS
Show, (forall x. LibWarning -> Rep LibWarning x)
-> (forall x. Rep LibWarning x -> LibWarning) -> Generic LibWarning
forall x. Rep LibWarning x -> LibWarning
forall x. LibWarning -> Rep LibWarning x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibWarning -> Rep LibWarning x
from :: forall x. LibWarning -> Rep LibWarning x
$cto :: forall x. Rep LibWarning x -> LibWarning
to :: forall x. Rep LibWarning x -> LibWarning
Generic)

-- | Library Warnings.
data LibWarning'
  = UnknownField String
  deriving (LineNumber -> LibWarning' -> ShowS
[LibWarning'] -> ShowS
LibWarning' -> FilePath
(LineNumber -> LibWarning' -> ShowS)
-> (LibWarning' -> FilePath)
-> ([LibWarning'] -> ShowS)
-> Show LibWarning'
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibWarning' -> ShowS
showsPrec :: LineNumber -> LibWarning' -> ShowS
$cshow :: LibWarning' -> FilePath
show :: LibWarning' -> FilePath
$cshowList :: [LibWarning'] -> ShowS
showList :: [LibWarning'] -> ShowS
Show, (forall x. LibWarning' -> Rep LibWarning' x)
-> (forall x. Rep LibWarning' x -> LibWarning')
-> Generic LibWarning'
forall x. Rep LibWarning' x -> LibWarning'
forall x. LibWarning' -> Rep LibWarning' x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibWarning' -> Rep LibWarning' x
from :: forall x. LibWarning' -> Rep LibWarning' x
$cto :: forall x. Rep LibWarning' x -> LibWarning'
to :: forall x. Rep LibWarning' x -> LibWarning'
Generic)

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

-- * Errors

data LibError = LibError (Maybe LibPositionInfo) LibError'
  deriving (LineNumber -> LibError -> ShowS
[LibError] -> ShowS
LibError -> FilePath
(LineNumber -> LibError -> ShowS)
-> (LibError -> FilePath) -> ([LibError] -> ShowS) -> Show LibError
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibError -> ShowS
showsPrec :: LineNumber -> LibError -> ShowS
$cshow :: LibError -> FilePath
show :: LibError -> FilePath
$cshowList :: [LibError] -> ShowS
showList :: [LibError] -> ShowS
Show, (forall x. LibError -> Rep LibError x)
-> (forall x. Rep LibError x -> LibError) -> Generic LibError
forall x. Rep LibError x -> LibError
forall x. LibError -> Rep LibError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibError -> Rep LibError x
from :: forall x. LibError -> Rep LibError x
$cto :: forall x. Rep LibError x -> LibError
to :: forall x. Rep LibError x -> LibError
Generic)

-- | Collected errors while processing library files.
--
data LibError'
  = LibrariesFileNotFound FilePath
      -- ^ The user specified replacement for the default @libraries@ file does not exist.
  | LibNotFound LibrariesFile LibName
      -- ^ Raised when a library name could not successfully be resolved
      --   to an @.agda-lib@ file.
      --
  | AmbiguousLib LibName [AgdaLibFile]
      -- ^ Raised when a library name is defined in several @.agda-lib files@.
  | LibParseError LibParseError
      -- ^ The @.agda-lib@ file could not be parsed.
  | ReadError
      -- ^ An I/O Error occurred when reading a file.
      E.IOException
        -- ^ The caught exception
      String
        -- ^ Explanation when this error occurred.
  | DuplicateExecutable
      -- ^ The @executables@ file contains duplicate entries.
      FilePath
        -- ^ Name of the @executables@ file.
      Text
        -- ^ Name of the executable that is defined twice.
      (List2 (LineNumber, FilePath))
        -- ^ The resolutions of the executable.
  deriving (LineNumber -> LibError' -> ShowS
[LibError'] -> ShowS
LibError' -> FilePath
(LineNumber -> LibError' -> ShowS)
-> (LibError' -> FilePath)
-> ([LibError'] -> ShowS)
-> Show LibError'
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibError' -> ShowS
showsPrec :: LineNumber -> LibError' -> ShowS
$cshow :: LibError' -> FilePath
show :: LibError' -> FilePath
$cshowList :: [LibError'] -> ShowS
showList :: [LibError'] -> ShowS
Show, (forall x. LibError' -> Rep LibError' x)
-> (forall x. Rep LibError' x -> LibError') -> Generic LibError'
forall x. Rep LibError' x -> LibError'
forall x. LibError' -> Rep LibError' x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibError' -> Rep LibError' x
from :: forall x. LibError' -> Rep LibError' x
$cto :: forall x. Rep LibError' x -> LibError'
to :: forall x. Rep LibError' x -> LibError'
Generic)

-- | Exceptions thrown by the @.agda-lib@ parser.
--
data LibParseError
  = BadLibraryName String
      -- ^ An invalid library name, e.g., containing spaces.
  | ReadFailure FilePath E.IOException
      -- ^ I/O error while reading file.
  | MissingFields (List1 String)
      -- ^ Missing these mandatory fields.
  | DuplicateFields (List1 String)
      -- ^ These fields occur each more than once.
  | MissingFieldName LineNumber
      -- ^ At the given line number, a field name is missing before the @:@.
  | BadFieldName LineNumber String
      -- ^ At the given line number, an invalid field name is encountered before the @:@.
      --   (E.g., containing spaces.)
  | MissingColonForField LineNumber String
      -- ^ At the given line number, the given field is not followed by @:@.
  | ContentWithoutField LineNumber
      -- ^ At the given line number, indented text (content) is not preceded by a field.
  deriving (LineNumber -> LibParseError -> ShowS
[LibParseError] -> ShowS
LibParseError -> FilePath
(LineNumber -> LibParseError -> ShowS)
-> (LibParseError -> FilePath)
-> ([LibParseError] -> ShowS)
-> Show LibParseError
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibParseError -> ShowS
showsPrec :: LineNumber -> LibParseError -> ShowS
$cshow :: LibParseError -> FilePath
show :: LibParseError -> FilePath
$cshowList :: [LibParseError] -> ShowS
showList :: [LibParseError] -> ShowS
Show, (forall x. LibParseError -> Rep LibParseError x)
-> (forall x. Rep LibParseError x -> LibParseError)
-> Generic LibParseError
forall x. Rep LibParseError x -> LibParseError
forall x. LibParseError -> Rep LibParseError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibParseError -> Rep LibParseError x
from :: forall x. LibParseError -> Rep LibParseError x
$cto :: forall x. Rep LibParseError x -> LibParseError
to :: forall x. Rep LibParseError x -> LibParseError
Generic)

-- ** Raising warnings and errors

-- | Collection of 'LibError's and 'LibWarning's.
--
type LibErrWarns = [Either LibError LibWarning]

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

warnings' :: MonadWriter LibErrWarns m => List1 LibWarning' -> m ()
warnings' :: forall (m :: * -> *).
MonadWriter LibErrWarns m =>
List1 LibWarning' -> m ()
warnings' = LibErrWarns -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (LibErrWarns -> m ())
-> (List1 LibWarning' -> LibErrWarns) -> List1 LibWarning' -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LibWarning' -> Either LibError LibWarning)
-> [LibWarning'] -> LibErrWarns
forall a b. (a -> b) -> [a] -> [b]
map (LibWarning -> Either LibError LibWarning
forall a b. b -> Either a b
Right (LibWarning -> Either LibError LibWarning)
-> (LibWarning' -> LibWarning)
-> LibWarning'
-> Either LibError LibWarning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe LibPositionInfo -> LibWarning' -> LibWarning
LibWarning Maybe LibPositionInfo
forall a. Maybe a
Nothing) ([LibWarning'] -> LibErrWarns)
-> (List1 LibWarning' -> [LibWarning'])
-> List1 LibWarning'
-> LibErrWarns
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 LibWarning' -> [Item (List1 LibWarning')]
List1 LibWarning' -> [LibWarning']
forall l. IsList l => l -> [Item l]
toList

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

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


------------------------------------------------------------------------
-- * Library Monad
------------------------------------------------------------------------

-- | Collects 'LibError's and 'LibWarning's.
--
type LibErrorIO = WriterT LibErrWarns (StateT LibState IO)

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

-- | Cache locations of project configurations and parsed @.agda-lib@ files.
type LibState =
  ( Map FilePath ProjectConfig
  , Map FilePath AgdaLibFile
  )

-- | Collected errors when processing an @.agda-lib@ file.
--
data LibErrors = LibErrors
  { LibErrors -> [AgdaLibFile]
libErrorsInstalledLibraries :: [AgdaLibFile]
  , LibErrors -> List1 LibError
libErrors                   :: List1 LibError
  } deriving (LineNumber -> LibErrors -> ShowS
[LibErrors] -> ShowS
LibErrors -> FilePath
(LineNumber -> LibErrors -> ShowS)
-> (LibErrors -> FilePath)
-> ([LibErrors] -> ShowS)
-> Show LibErrors
forall a.
(LineNumber -> a -> ShowS)
-> (a -> FilePath) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibErrors -> ShowS
showsPrec :: LineNumber -> LibErrors -> ShowS
$cshow :: LibErrors -> FilePath
show :: LibErrors -> FilePath
$cshowList :: [LibErrors] -> ShowS
showList :: [LibErrors] -> ShowS
Show, (forall x. LibErrors -> Rep LibErrors x)
-> (forall x. Rep LibErrors x -> LibErrors) -> Generic LibErrors
forall x. Rep LibErrors x -> LibErrors
forall x. LibErrors -> Rep LibErrors x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibErrors -> Rep LibErrors x
from :: forall x. LibErrors -> Rep LibErrors x
$cto :: forall x. Rep LibErrors x -> LibErrors
to :: forall x. Rep LibErrors x -> LibErrors
Generic)

getCachedProjectConfig
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> m (Maybe ProjectConfig)
getCachedProjectConfig :: forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
FilePath -> m (Maybe ProjectConfig)
getCachedProjectConfig FilePath
path = do
  FilePath
path <- 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
$ FilePath -> IO FilePath
canonicalizePath FilePath
path
  Map FilePath ProjectConfig
cache <- (LibState -> Map FilePath ProjectConfig)
-> m (Map FilePath ProjectConfig)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets LibState -> Map FilePath ProjectConfig
forall a b. (a, b) -> a
fst
  Maybe ProjectConfig -> m (Maybe ProjectConfig)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ProjectConfig -> m (Maybe ProjectConfig))
-> Maybe ProjectConfig -> m (Maybe ProjectConfig)
forall a b. (a -> b) -> a -> b
$ FilePath -> Map FilePath ProjectConfig -> Maybe ProjectConfig
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FilePath
path Map FilePath ProjectConfig
cache

storeCachedProjectConfig
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> ProjectConfig -> m ()
storeCachedProjectConfig :: forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
FilePath -> ProjectConfig -> m ()
storeCachedProjectConfig FilePath
path ProjectConfig
conf = do
  FilePath
path <- 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
$ FilePath -> IO FilePath
canonicalizePath FilePath
path
  (LibState -> LibState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((LibState -> LibState) -> m ()) -> (LibState -> LibState) -> m ()
forall a b. (a -> b) -> a -> b
$ (Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
-> LibState -> LibState
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
 -> LibState -> LibState)
-> (Map FilePath ProjectConfig -> Map FilePath ProjectConfig)
-> LibState
-> LibState
forall a b. (a -> b) -> a -> b
$ FilePath
-> ProjectConfig
-> Map FilePath ProjectConfig
-> Map FilePath ProjectConfig
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FilePath
path ProjectConfig
conf

getCachedAgdaLibFile
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> m (Maybe AgdaLibFile)
getCachedAgdaLibFile :: forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
FilePath -> m (Maybe AgdaLibFile)
getCachedAgdaLibFile FilePath
path = do
  FilePath
path <- 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
$ FilePath -> IO FilePath
canonicalizePath FilePath
path
  (LibState -> Maybe AgdaLibFile) -> m (Maybe AgdaLibFile)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((LibState -> Maybe AgdaLibFile) -> m (Maybe AgdaLibFile))
-> (LibState -> Maybe AgdaLibFile) -> m (Maybe AgdaLibFile)
forall a b. (a -> b) -> a -> b
$ FilePath -> Map FilePath AgdaLibFile -> Maybe AgdaLibFile
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FilePath
path (Map FilePath AgdaLibFile -> Maybe AgdaLibFile)
-> (LibState -> Map FilePath AgdaLibFile)
-> LibState
-> Maybe AgdaLibFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibState -> Map FilePath AgdaLibFile
forall a b. (a, b) -> b
snd

storeCachedAgdaLibFile
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> AgdaLibFile -> m ()
storeCachedAgdaLibFile :: forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
FilePath -> AgdaLibFile -> m ()
storeCachedAgdaLibFile FilePath
path AgdaLibFile
lib = do
  FilePath
path <- 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
$ FilePath -> IO FilePath
canonicalizePath FilePath
path
  (LibState -> LibState) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((LibState -> LibState) -> m ()) -> (LibState -> LibState) -> m ()
forall a b. (a -> b) -> a -> b
$ (Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile)
-> LibState -> LibState
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 ((Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile)
 -> LibState -> LibState)
-> (Map FilePath AgdaLibFile -> Map FilePath AgdaLibFile)
-> LibState
-> LibState
forall a b. (a -> b) -> a -> b
$ FilePath
-> AgdaLibFile
-> Map FilePath AgdaLibFile
-> Map FilePath AgdaLibFile
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FilePath
path AgdaLibFile
lib

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

-- | Pretty-print 'LibError'.
formatLibError :: [AgdaLibFile] -> LibError -> Doc
formatLibError :: [AgdaLibFile] -> LibError -> Doc
formatLibError [AgdaLibFile]
installed (LibError Maybe LibPositionInfo
mc LibError'
e) =
  case (Maybe LibPositionInfo
mc, LibError'
e) of
    (Just LibPositionInfo
c, LibParseError LibParseError
err) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep  [ LibPositionInfo -> LibParseError -> Doc
formatLibPositionInfo LibPositionInfo
c LibParseError
err, LibError' -> Doc
forall a. Pretty a => a -> Doc
pretty LibError'
e ]
    (Maybe LibPositionInfo
_     , LibNotFound{}    ) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ LibError' -> Doc
forall a. Pretty a => a -> Doc
pretty LibError'
e, [AgdaLibFile] -> Doc
prettyInstalledLibraries [AgdaLibFile]
installed ]
    (Maybe LibPositionInfo, LibError')
_ -> LibError' -> Doc
forall a. Pretty a => a -> Doc
pretty LibError'
e


-- | Pretty-print 'LibErrors'.
formatLibErrors :: LibErrors -> Doc
formatLibErrors :: LibErrors -> Doc
formatLibErrors (LibErrors [AgdaLibFile]
libs List1 LibError
errs) =
  [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$  (LibError -> Doc) -> [LibError] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([AgdaLibFile] -> LibError -> Doc
formatLibError [AgdaLibFile]
libs) ([LibError] -> [Doc]) -> [LibError] -> [Doc]
forall a b. (a -> b) -> a -> b
$ List1 LibError -> [Item (List1 LibError)]
forall l. IsList l => l -> [Item l]
List1.toList List1 LibError
errs

-- | Does a parse error contain a line number?
hasLineNumber :: LibParseError -> Maybe LineNumber
hasLineNumber :: LibParseError -> Maybe LineNumber
hasLineNumber = \case
  BadLibraryName       FilePath
_   -> Maybe LineNumber
forall a. Maybe a
Nothing
  ReadFailure          FilePath
_ IOException
_ -> Maybe LineNumber
forall a. Maybe a
Nothing
  MissingFields        List1 FilePath
_   -> Maybe LineNumber
forall a. Maybe a
Nothing
  DuplicateFields      List1 FilePath
_   -> Maybe LineNumber
forall a. Maybe a
Nothing
  MissingFieldName     LineNumber
l   -> LineNumber -> Maybe LineNumber
forall a. a -> Maybe a
Just LineNumber
l
  BadFieldName         LineNumber
l FilePath
_ -> LineNumber -> Maybe LineNumber
forall a. a -> Maybe a
Just LineNumber
l
  MissingColonForField LineNumber
l FilePath
_ -> LineNumber -> Maybe LineNumber
forall a. a -> Maybe a
Just LineNumber
l
  ContentWithoutField  LineNumber
l   -> LineNumber -> Maybe LineNumber
forall a. a -> Maybe a
Just LineNumber
l

-- UNUSED:
-- -- | Does a parse error contain the name of the parsed file?
-- hasFilePath :: LibParseError -> Maybe FilePath
-- hasFilePath = \case
--   BadLibraryName       _   -> Nothing
--   ReadFailure          f _ -> Just f
--   MissingFields        _   -> Nothing
--   DuplicateFields      _   -> Nothing
--   MissingFieldName     _   -> Nothing
--   BadFieldName         _ _ -> Nothing
--   MissingColonForField _ _ -> Nothing
--   ContentWithoutField  _   -> Nothing

-- | Compute a position position prefix.
--
--   Depending on the error to be printed, it will
--
--   - either give the name of the @libraries@ file and a line inside it,
--
--   - or give the name of the @.agda-lib@ file.
--
formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc
formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc
formatLibPositionInfo (LibPositionInfo Maybe FilePath
libFile LineNumber
lineNum FilePath
file) = \case

  -- If we couldn't even read the @.agda-lib@ file, report error in the @libraries@ file.
  ReadFailure FilePath
_ IOException
_
    | Just FilePath
lf <- Maybe FilePath
libFile
      -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
lf, Doc
":", LineNumber -> Doc
forall a. Pretty a => a -> Doc
pretty LineNumber
lineNum, Doc
":" ]
    | Bool
otherwise
      -> Doc
forall a. Null a => a
empty

  -- If the parse error comes with a line number, print it here.
  LibParseError
e | Just LineNumber
l <- LibParseError -> Maybe LineNumber
hasLineNumber LibParseError
e
      -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
file, Doc
":", LineNumber -> Doc
forall a. Pretty a => a -> Doc
pretty LineNumber
l, Doc
":" ]
    | Bool
otherwise
      -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
file, Doc
":" ]

prettyInstalledLibraries :: [AgdaLibFile] -> Doc
prettyInstalledLibraries :: [AgdaLibFile] -> Doc
prettyInstalledLibraries [AgdaLibFile]
installed =
  [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc
"Installed libraries:" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
    (Doc -> Doc) -> [Doc] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (LineNumber -> Doc -> Doc
forall a. LineNumber -> Doc a -> Doc a
nest LineNumber
2) ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
    if [AgdaLibFile] -> Bool
forall a. Null a => a -> Bool
null [AgdaLibFile]
installed then [Doc
"(none)"]
    else [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ FilePath -> Doc
forall a. FilePath -> Doc a
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libName AgdaLibFile
l, LineNumber -> Doc -> Doc
forall a. LineNumber -> Doc a -> Doc a
nest LineNumber
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
forall a. FilePath -> Doc a
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> FilePath
_libFile AgdaLibFile
l ]
         | AgdaLibFile
l <- [AgdaLibFile]
installed
         ]

-- | Pretty-print library management error without position info.

instance Pretty LibError' where
  pretty :: LibError' -> Doc
pretty = \case

    LibrariesFileNotFound FilePath
path -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
      [ FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
"Libraries file not found:"
      , FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
path
      ]

    LibNotFound LibrariesFile
file FilePath
lib -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      [ FilePath -> Doc
forall a. FilePath -> Doc a
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"Library '" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
lib FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"' not found."
      , [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"Add the path to its .agda-lib file to"
            , LineNumber -> Doc -> Doc
forall a. LineNumber -> Doc a -> Doc a
nest LineNumber
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
forall a. FilePath -> Doc a
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
"'" FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ LibrariesFile -> FilePath
lfPath LibrariesFile
file FilePath -> ShowS
forall a. [a] -> [a] -> [a]
++ FilePath
"'"
            , Doc
"to install."
            ]
      ]

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

    LibParseError LibParseError
err -> LibParseError -> Doc
forall a. Pretty a => a -> Doc
pretty LibParseError
err

    ReadError IOException
e FilePath
msg -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ FilePath -> Doc
forall a. FilePath -> Doc a
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ FilePath
msg
      , FilePath -> Doc
forall a. FilePath -> Doc a
text (FilePath -> Doc) -> FilePath -> Doc
forall a b. (a -> b) -> a -> b
$ IOException -> FilePath
forall e. Exception e => e -> FilePath
showIOException IOException
e
      ]

    DuplicateExecutable FilePath
exeFile Text
exe List2 (LineNumber, FilePath)
paths -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Doc
"Duplicate entries for executable '", (FilePath -> Doc
forall a. FilePath -> Doc a
text (FilePath -> Doc) -> (Text -> FilePath) -> Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
unpack) Text
exe, Doc
"' in ", FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
exeFile, Doc
":" ] Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
      ((LineNumber, FilePath) -> Doc)
-> [(LineNumber, FilePath)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (LineNumber
ln, FilePath
fp) -> LineNumber -> Doc -> Doc
forall a. LineNumber -> Doc a -> Doc a
nest LineNumber
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (LineNumber -> Doc
forall a. Pretty a => a -> Doc
pretty LineNumber
ln Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
colon) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
fp) (List2 (LineNumber, FilePath)
-> [Item (List2 (LineNumber, FilePath))]
forall l. IsList l => l -> [Item l]
toList List2 (LineNumber, FilePath)
paths)

-- | Print library file parse error without position info.
--
instance Pretty LibParseError where
  pretty :: LibParseError -> Doc
pretty = \case

    BadLibraryName FilePath
s -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
      [ Doc
"Bad library name:", Doc -> Doc
quotes (FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
s) ]
    ReadFailure FilePath
file IOException
e -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
      [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep [ Doc
"Failed to read library file", FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
file Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"." ]
      , Doc
"Reason:" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc
forall a. FilePath -> Doc a
text (IOException -> FilePath
forall e. Exception e => e -> FilePath
showIOException IOException
e)
      ]

    MissingFields   List1 FilePath
xs -> Doc
"Missing"   Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> List1 FilePath -> Doc
listFields List1 FilePath
xs
    DuplicateFields List1 FilePath
xs -> Doc
"Duplicate" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> List1 FilePath -> Doc
listFields List1 FilePath
xs

    MissingFieldName     LineNumber
l   -> LineNumber -> Doc -> Doc
forall {p} {a}. p -> a -> a
atLine LineNumber
l (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Missing field name"
    BadFieldName         LineNumber
l FilePath
s -> LineNumber -> Doc -> Doc
forall {p} {a}. p -> a -> a
atLine LineNumber
l (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Bad field name" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc
forall a. FilePath -> Doc a
text (ShowS
forall a. Show a => a -> FilePath
show FilePath
s)
    MissingColonForField LineNumber
l FilePath
s -> LineNumber -> Doc -> Doc
forall {p} {a}. p -> a -> a
atLine LineNumber
l (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Missing ':' for field " Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> FilePath -> Doc
forall a. FilePath -> Doc a
text (ShowS
forall a. Show a => a -> FilePath
show FilePath
s)
    ContentWithoutField  LineNumber
l   -> LineNumber -> Doc -> Doc
forall {p} {a}. p -> a -> a
atLine LineNumber
l (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Missing field"

    where
    listFields :: List1 FilePath -> Doc
listFields List1 FilePath
xs = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ List1 FilePath -> Doc
forall {a} {c}. (Sized a, IsString c) => a -> c
fieldS List1 FilePath
xs Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: List1 FilePath -> [Doc]
list List1 FilePath
xs
    fieldS :: a -> c
fieldS a
xs     = a -> c -> c -> c
forall a c. Sized a => a -> c -> c -> c
singPlural a
xs c
"field:" c
"fields:"
    list :: List1 FilePath -> [Doc]
list          = Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc])
-> (List1 FilePath -> [Doc]) -> List1 FilePath -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> Doc) -> [FilePath] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
quotes (Doc -> Doc) -> (FilePath -> Doc) -> FilePath -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Doc
forall a. FilePath -> Doc a
text) ([FilePath] -> [Doc])
-> (List1 FilePath -> [FilePath]) -> List1 FilePath -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 FilePath -> [FilePath]
List1 FilePath -> [Item (List1 FilePath)]
forall l. IsList l => l -> [Item l]
toList
    atLine :: p -> a -> a
atLine p
l      = a -> a
forall a. a -> a
id
    -- The line number will be printed by 'formatLibPositionInfo'!
    -- atLine l doc  = hsep [ text (show l) <> ":", doc ]


instance Pretty LibWarning where
  pretty :: LibWarning -> Doc
pretty (LibWarning Maybe LibPositionInfo
mc LibWarning'
w) =
    case Maybe LibPositionInfo
mc of
      Maybe LibPositionInfo
Nothing -> LibWarning' -> Doc
forall a. Pretty a => a -> Doc
pretty LibWarning'
w
      Just (LibPositionInfo Maybe FilePath
_ LineNumber
_ FilePath
file) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ FilePath -> Doc
forall a. FilePath -> Doc a
text FilePath
file, Doc
":"] Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> LibWarning' -> Doc
forall a. Pretty a => a -> Doc
pretty LibWarning'
w

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

------------------------------------------------------------------------
-- NFData instances
------------------------------------------------------------------------

instance NFData ExecutablesFile
instance NFData LibrariesFile
instance NFData ProjectConfig
instance NFData AgdaLibFile
instance NFData LibPositionInfo
instance NFData LibWarning
instance NFData LibWarning'
instance NFData LibError
instance NFData LibError'
instance NFData LibErrors
instance NFData LibParseError
instance NFData E.IOException where rnf :: IOException -> ()
rnf IOException
_ = ()