-- | 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, runWriterT, MonadWriter, tell )
import Control.Monad.IO.Class      ( MonadIO(..) )

import Data.Bifunctor              ( first , second )
import Data.Char                   ( isDigit )
import Data.Function               ( (&), on )
import Data.Hashable               ( Hashable )
import qualified Data.List         as List
import Data.Map                    ( Map )
import qualified Data.Map          as Map
import Data.Text                   ( Text, unpack )
import qualified Data.Text         as T

import GHC.Generics                ( Generic )

import System.Directory

import Agda.Interaction.Options.Warnings

import Agda.Syntax.Common.Pretty
import Agda.Syntax.Position

import Agda.Utils.IO               ( showIOException )
import Agda.Utils.Lens
import Agda.Utils.List             ( chopWhen )
import Agda.Utils.List1            ( List1, toList )
import Agda.Utils.List2            ( List2, toList )
import qualified Agda.Utils.List1  as List1
import Agda.Utils.Null

-- | A symbolic library name.
--
--   Library names are structured into the base name and a suffix of version
--   numbers, e.g. @mylib-1.2.3@.  The version suffix is optional.
data LibName = LibName
  { LibName -> Text
libNameBase    :: Text
      -- ^ Actual library name.
  , LibName -> [Integer]
libNameVersion :: [Integer]
      -- ^ Major version, minor version, subminor version, etc., all non-negative.
  } deriving (LibName -> LibName -> Bool
(LibName -> LibName -> Bool)
-> (LibName -> LibName -> Bool) -> Eq LibName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LibName -> LibName -> Bool
== :: LibName -> LibName -> Bool
$c/= :: LibName -> LibName -> Bool
/= :: LibName -> LibName -> Bool
Eq, Int -> LibName -> ShowS
[LibName] -> ShowS
LibName -> [Char]
(Int -> LibName -> ShowS)
-> (LibName -> [Char]) -> ([LibName] -> ShowS) -> Show LibName
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibName -> ShowS
showsPrec :: Int -> LibName -> ShowS
$cshow :: LibName -> [Char]
show :: LibName -> [Char]
$cshowList :: [LibName] -> ShowS
showList :: [LibName] -> ShowS
Show, (forall x. LibName -> Rep LibName x)
-> (forall x. Rep LibName x -> LibName) -> Generic LibName
forall x. Rep LibName x -> LibName
forall x. LibName -> Rep LibName x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibName -> Rep LibName x
from :: forall x. LibName -> Rep LibName x
$cto :: forall x. Rep LibName x -> LibName
to :: forall x. Rep LibName x -> LibName
Generic)

-- | In comparisons, a missing version number is assumed to be infinity.
--   E.g. @foo > foo-2.2 > foo-2.0.1 > foo-2 > foo-1.0@.
instance Ord LibName where
  compare :: LibName -> LibName -> Ordering
compare = (Text, Bool, [Integer]) -> (Text, Bool, [Integer]) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((Text, Bool, [Integer]) -> (Text, Bool, [Integer]) -> Ordering)
-> (LibName -> (Text, Bool, [Integer]))
-> LibName
-> LibName
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` LibName -> (Text, Bool, [Integer])
versionMeasure
    where
      versionMeasure :: LibName -> (Text, Bool, [Integer])
      versionMeasure :: LibName -> (Text, Bool, [Integer])
versionMeasure (LibName Text
rx [Integer]
vs) = (Text
rx, [Integer] -> Bool
forall a. Null a => a -> Bool
null [Integer]
vs, [Integer]
vs)

instance Pretty LibName where
  pretty :: LibName -> Doc Aspects
pretty = \case
    LibName Text
base [] -> Text -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Text
base
    LibName Text
base [Integer]
vs -> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
hcat [ Text -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty Text
base, Doc Aspects
"-", [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"." ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (Integer -> [Char]) -> [Integer] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> [Char]
forall a. Show a => a -> [Char]
show [Integer]
vs ]

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

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

data ExecutablesFile = ExecutablesFile
  { ExecutablesFile -> [Char]
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 (Int -> ExecutablesFile -> ShowS
[ExecutablesFile] -> ShowS
ExecutablesFile -> [Char]
(Int -> ExecutablesFile -> ShowS)
-> (ExecutablesFile -> [Char])
-> ([ExecutablesFile] -> ShowS)
-> Show ExecutablesFile
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ExecutablesFile -> ShowS
showsPrec :: Int -> ExecutablesFile -> ShowS
$cshow :: ExecutablesFile -> [Char]
show :: ExecutablesFile -> [Char]
$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 :: LibName
libNameForCurrentDir = Text -> [Integer] -> LibName
LibName Text
"." []

-- | A file can either belong to a project located at a given root
--   containing an .agda-lib file, or be part of the default project.
data ProjectConfig
  = ProjectConfig
    { ProjectConfig -> [Char]
configRoot         :: FilePath
        -- ^ Directory which contains the @.agda-lib@ file for the current project.
    , ProjectConfig -> [Char]
configAgdaLibFile  :: FilePath
        -- ^ @.agda-lib@ file relative to 'configRoot' (filename only, no directory).
    , ProjectConfig -> Int
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 -> [[Char]]
pragmaStrings :: [String]
    -- ^ The options.
  , OptionsPragma -> Range
pragmaRange :: Range
    -- ^ The range of the options in the pragma (not including things
    -- like an @OPTIONS@ keyword).
  }
  deriving Int -> OptionsPragma -> ShowS
[OptionsPragma] -> ShowS
OptionsPragma -> [Char]
(Int -> OptionsPragma -> ShowS)
-> (OptionsPragma -> [Char])
-> ([OptionsPragma] -> ShowS)
-> Show OptionsPragma
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> OptionsPragma -> ShowS
showsPrec :: Int -> OptionsPragma -> ShowS
$cshow :: OptionsPragma -> [Char]
show :: OptionsPragma -> [Char]
$cshowList :: [OptionsPragma] -> ShowS
showList :: [OptionsPragma] -> ShowS
Show

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

instance Monoid OptionsPragma where
  mempty :: OptionsPragma
mempty  = OptionsPragma { pragmaStrings :: [[Char]]
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 [[Char]]
a Range
_) = [[Char]] -> ()
forall a. NFData a => a -> ()
rnf [[Char]]
a

-- | Content of a @.agda-lib@ file.
--
data AgdaLibFile = AgdaLibFile
  { AgdaLibFile -> LibName
_libName     :: LibName     -- ^ The symbolic name of the library.
  , AgdaLibFile -> [Char]
_libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
  , AgdaLibFile -> Int
_libAbove    :: !Int        -- ^ How many directories above the
                                --   Agda file is the @.agda-lib@ file
                                --   located?
  , AgdaLibFile -> [[Char]]
_libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
  , AgdaLibFile -> [LibName]
_libDepends  :: [LibName]   -- ^ Dependencies.
  , AgdaLibFile -> OptionsPragma
_libPragmas  :: OptionsPragma
                                -- ^ Default pragma options for all files in the library.
  }
  deriving (Int -> AgdaLibFile -> ShowS
[AgdaLibFile] -> ShowS
AgdaLibFile -> [Char]
(Int -> AgdaLibFile -> ShowS)
-> (AgdaLibFile -> [Char])
-> ([AgdaLibFile] -> ShowS)
-> Show AgdaLibFile
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AgdaLibFile -> ShowS
showsPrec :: Int -> AgdaLibFile -> ShowS
$cshow :: AgdaLibFile -> [Char]
show :: AgdaLibFile -> [Char]
$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 :: LibName
_libName     = LibName
forall a. Null a => a
empty
  , _libFile :: [Char]
_libFile     = [Char]
""
  , _libAbove :: Int
_libAbove    = Int
0
  , _libIncludes :: [[Char]]
_libIncludes = []
  , _libDepends :: [LibName]
_libDepends  = []
  , _libPragmas :: OptionsPragma
_libPragmas  = OptionsPragma
forall a. Monoid a => a
mempty
  }

---------------------------------------------------------------------------
-- * Lenses
---------------------------------------------------------------------------

-- ** Lenses for 'ProjectConfig'

lensConfigAbove :: Lens' ProjectConfig Int
lensConfigAbove :: Lens' ProjectConfig Int
lensConfigAbove Int -> f Int
f = \case
  ProjectConfig
DefaultProjectConfig -> ProjectConfig
DefaultProjectConfig ProjectConfig -> f Int -> f ProjectConfig
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Int -> f Int
f Int
0
  c :: ProjectConfig
c@ProjectConfig{} -> Int -> f Int
f (ProjectConfig -> Int
configAbove ProjectConfig
c) f Int -> (Int -> ProjectConfig) -> f ProjectConfig
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ !Int
i -> ProjectConfig
c{ configAbove = i }

-- ** Lenses for 'AgdaLibFile'

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

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

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

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

libDepends :: Lens' AgdaLibFile [LibName]
libDepends :: Lens' AgdaLibFile [LibName]
libDepends [LibName] -> f [LibName]
f AgdaLibFile
a = [LibName] -> f [LibName]
f (AgdaLibFile -> [LibName]
_libDepends AgdaLibFile
a) f [LibName] -> ([LibName] -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ [LibName]
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 [Char]
libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file.
  , LibPositionInfo -> Int
lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
  , LibPositionInfo -> [Char]
filePos    :: FilePath       -- ^ Library file.
  }
  deriving (Int -> LibPositionInfo -> ShowS
[LibPositionInfo] -> ShowS
LibPositionInfo -> [Char]
(Int -> LibPositionInfo -> ShowS)
-> (LibPositionInfo -> [Char])
-> ([LibPositionInfo] -> ShowS)
-> Show LibPositionInfo
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibPositionInfo -> ShowS
showsPrec :: Int -> LibPositionInfo -> ShowS
$cshow :: LibPositionInfo -> [Char]
show :: LibPositionInfo -> [Char]
$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 (Int -> LibWarning -> ShowS
[LibWarning] -> ShowS
LibWarning -> [Char]
(Int -> LibWarning -> ShowS)
-> (LibWarning -> [Char])
-> ([LibWarning] -> ShowS)
-> Show LibWarning
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibWarning -> ShowS
showsPrec :: Int -> LibWarning -> ShowS
$cshow :: LibWarning -> [Char]
show :: LibWarning -> [Char]
$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 (Int -> LibWarning' -> ShowS
[LibWarning'] -> ShowS
LibWarning' -> [Char]
(Int -> LibWarning' -> ShowS)
-> (LibWarning' -> [Char])
-> ([LibWarning'] -> ShowS)
-> Show LibWarning'
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibWarning' -> ShowS
showsPrec :: Int -> LibWarning' -> ShowS
$cshow :: LibWarning' -> [Char]
show :: LibWarning' -> [Char]
$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 (Int -> LibError -> ShowS
[LibError] -> ShowS
LibError -> [Char]
(Int -> LibError -> ShowS)
-> (LibError -> [Char]) -> ([LibError] -> ShowS) -> Show LibError
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibError -> ShowS
showsPrec :: Int -> LibError -> ShowS
$cshow :: LibError -> [Char]
show :: LibError -> [Char]
$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 (List2 AgdaLibFile)
      -- ^ Raised when a library name is defined in several @.agda-lib files@.
  | SeveralAgdaLibFiles FilePath (List2 FilePath)
      -- ^ The given project root contains more than one @.agda-lib@ file.
  | 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 (Int -> LibError' -> ShowS
[LibError'] -> ShowS
LibError' -> [Char]
(Int -> LibError' -> ShowS)
-> (LibError' -> [Char])
-> ([LibError'] -> ShowS)
-> Show LibError'
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibError' -> ShowS
showsPrec :: Int -> LibError' -> ShowS
$cshow :: LibError' -> [Char]
show :: LibError' -> [Char]
$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 (Int -> LibParseError -> ShowS
[LibParseError] -> ShowS
LibParseError -> [Char]
(Int -> LibParseError -> ShowS)
-> (LibParseError -> [Char])
-> ([LibParseError] -> ShowS)
-> Show LibParseError
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibParseError -> ShowS
showsPrec :: Int -> LibParseError -> ShowS
$cshow :: LibParseError -> [Char]
show :: LibParseError -> [Char]
$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 =>
NonEmpty LibError -> m ()
raiseErrors = LibErrWarns -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (LibErrWarns -> m ())
-> (NonEmpty LibError -> LibErrWarns) -> NonEmpty 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)
-> (NonEmpty LibError -> [LibError])
-> NonEmpty LibError
-> LibErrWarns
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty LibError -> [Item (NonEmpty LibError)]
NonEmpty 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))

type LibState = LibCache

-- | Cache locations of project configurations and parsed @.agda-lib@ files.
data LibCache = LibCache
  { LibCache -> Map [Char] ProjectConfig
projectConfigs :: !(Map FilePath ProjectConfig)
      -- ^ Map from directories to paths of closest enclosing @.agda-lib@
      --   files (or 'DefaultProjectConfig' if there are none).
  , LibCache -> Map [Char] AgdaLibFile
agdaLibFiles   :: !(Map FilePath AgdaLibFile)
      -- ^ Contents of @.agda-lib@ files that have already been parsed.
  }
  deriving ((forall x. LibCache -> Rep LibCache x)
-> (forall x. Rep LibCache x -> LibCache) -> Generic LibCache
forall x. Rep LibCache x -> LibCache
forall x. LibCache -> Rep LibCache x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. LibCache -> Rep LibCache x
from :: forall x. LibCache -> Rep LibCache x
$cto :: forall x. Rep LibCache x -> LibCache
to :: forall x. Rep LibCache x -> LibCache
Generic)

-- | Collected errors when processing an @.agda-lib@ file.
--
data LibErrors = LibErrors
  { LibErrors -> [AgdaLibFile]
libErrorsInstalledLibraries :: [AgdaLibFile]
  , LibErrors -> NonEmpty LibError
libErrors                   :: List1 LibError
  } deriving (Int -> LibErrors -> ShowS
[LibErrors] -> ShowS
LibErrors -> [Char]
(Int -> LibErrors -> ShowS)
-> (LibErrors -> [Char])
-> ([LibErrors] -> ShowS)
-> Show LibErrors
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LibErrors -> ShowS
showsPrec :: Int -> LibErrors -> ShowS
$cshow :: LibErrors -> [Char]
show :: LibErrors -> [Char]
$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)

runLibM :: LibM a -> LibState -> IO ((Either LibErrors a, [LibWarning]), LibState)
runLibM :: forall a.
LibM a
-> LibCache -> IO ((Either LibErrors a, [LibWarning]), LibCache)
runLibM LibM a
m LibCache
s = LibM a
m LibM a
-> (LibM a
    -> WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a))
-> WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
forall a b. a -> (a -> b) -> b
& LibM a
-> WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
-> (WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
    -> StateT LibCache IO (Either LibErrors a, [LibWarning]))
-> StateT LibCache IO (Either LibErrors a, [LibWarning])
forall a b. a -> (a -> b) -> b
& WriterT [LibWarning] (StateT LibCache IO) (Either LibErrors a)
-> StateT LibCache IO (Either LibErrors a, [LibWarning])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT StateT LibCache IO (Either LibErrors a, [LibWarning])
-> (StateT LibCache IO (Either LibErrors a, [LibWarning])
    -> IO ((Either LibErrors a, [LibWarning]), LibCache))
-> IO ((Either LibErrors a, [LibWarning]), LibCache)
forall a b. a -> (a -> b) -> b
& (StateT LibCache IO (Either LibErrors a, [LibWarning])
-> LibCache -> IO ((Either LibErrors a, [LibWarning]), LibCache)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` LibCache
s)

getCachedProjectConfig
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> m (Maybe ProjectConfig)
getCachedProjectConfig :: forall (m :: * -> *).
(MonadState LibCache m, MonadIO m) =>
[Char] -> m (Maybe ProjectConfig)
getCachedProjectConfig [Char]
path = do
  path <- IO [Char] -> m [Char]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Char] -> m [Char]) -> IO [Char] -> m [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> IO [Char]
canonicalizePath [Char]
path
  Map.lookup path <$> gets projectConfigs

storeCachedProjectConfig
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> ProjectConfig -> m ()
storeCachedProjectConfig :: forall (m :: * -> *).
(MonadState LibCache m, MonadIO m) =>
[Char] -> ProjectConfig -> m ()
storeCachedProjectConfig [Char]
path ProjectConfig
conf = do
  path <- IO [Char] -> m [Char]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Char] -> m [Char]) -> IO [Char] -> m [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> IO [Char]
canonicalizePath [Char]
path
  modify \ LibCache
s -> LibCache
s { projectConfigs = Map.insert path conf $ projectConfigs s }

getCachedAgdaLibFile
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> m (Maybe AgdaLibFile)
getCachedAgdaLibFile :: forall (m :: * -> *).
(MonadState LibCache m, MonadIO m) =>
[Char] -> m (Maybe AgdaLibFile)
getCachedAgdaLibFile [Char]
path = do
  path <- IO [Char] -> m [Char]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Char] -> m [Char]) -> IO [Char] -> m [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> IO [Char]
canonicalizePath [Char]
path
  Map.lookup path <$> gets agdaLibFiles

storeCachedAgdaLibFile
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> AgdaLibFile -> m ()
storeCachedAgdaLibFile :: forall (m :: * -> *).
(MonadState LibCache m, MonadIO m) =>
[Char] -> AgdaLibFile -> m ()
storeCachedAgdaLibFile [Char]
path AgdaLibFile
lib = do
  path <- IO [Char] -> m [Char]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [Char] -> m [Char]) -> IO [Char] -> m [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> IO [Char]
canonicalizePath [Char]
path
  modify \ LibCache
s -> LibCache
s { agdaLibFiles = Map.insert path lib $ agdaLibFiles s }

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

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


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

-- | Does a parse error contain a line number?
hasLineNumber :: LibParseError -> Maybe LineNumber
hasLineNumber :: LibParseError -> Maybe Int
hasLineNumber = \case
  BadLibraryName       [Char]
_   -> Maybe Int
forall a. Maybe a
Nothing
  ReadFailure          [Char]
_ IOException
_ -> Maybe Int
forall a. Maybe a
Nothing
  MissingFields        NonEmpty [Char]
_   -> Maybe Int
forall a. Maybe a
Nothing
  DuplicateFields      NonEmpty [Char]
_   -> Maybe Int
forall a. Maybe a
Nothing
  MissingFieldName     Int
l   -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l
  BadFieldName         Int
l [Char]
_ -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l
  MissingColonForField Int
l [Char]
_ -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l
  ContentWithoutField  Int
l   -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
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 Aspects
formatLibPositionInfo (LibPositionInfo Maybe [Char]
libFile Int
lineNum [Char]
file) = \case

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

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

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

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

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

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

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

    AmbiguousLib LibName
lib List2 AgdaLibFile
tgts -> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$
      [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
hcat [ Doc Aspects
"Ambiguous library '", LibName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty LibName
lib, Doc Aspects
"'." ]
            , Doc Aspects
"Could refer to any one of"
          ]
        Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall a. a -> [a] -> [a]
: [ Int -> Doc Aspects -> Doc Aspects
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ LibName -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty (AgdaLibFile -> LibName
_libName AgdaLibFile
l) Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> Doc Aspects -> Doc Aspects
parens ([Char] -> Doc Aspects
forall a. [Char] -> Doc a
text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> [Char]
_libFile AgdaLibFile
l) | AgdaLibFile
l <- List2 AgdaLibFile -> [Item (List2 AgdaLibFile)]
forall l. IsList l => l -> [Item l]
toList List2 AgdaLibFile
tgts ]

    SeveralAgdaLibFiles [Char]
root List2 [Char]
files -> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$
      [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Doc Aspects
"The project root", [Char] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [Char]
root ]
        Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall a. a -> [a] -> [a]
: Doc Aspects
"may contain only one .agda-lib file, but I found several:"
        Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall a. a -> [a] -> [a]
: ([Char] -> Doc Aspects) -> [[Char]] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc Aspects
"-" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc Aspects -> Doc Aspects)
-> ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty) ([[Char]] -> [[Char]]
forall a. Ord a => [a] -> [a]
List.sort ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ List2 [Char] -> [Item (List2 [Char])]
forall l. IsList l => l -> [Item l]
toList List2 [Char]
files)

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

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

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

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

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

    MissingFields   NonEmpty [Char]
xs -> Doc Aspects
"Missing"   Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> NonEmpty [Char] -> Doc Aspects
listFields NonEmpty [Char]
xs
    DuplicateFields NonEmpty [Char]
xs -> Doc Aspects
"Duplicate" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> NonEmpty [Char] -> Doc Aspects
listFields NonEmpty [Char]
xs

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

    where
    listFields :: NonEmpty [Char] -> Doc Aspects
listFields NonEmpty [Char]
xs = [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
hsep ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ NonEmpty [Char] -> Doc Aspects
forall {a} {c}. (Sized a, IsString c) => a -> c
fieldS NonEmpty [Char]
xs Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall a. a -> [a] -> [a]
: NonEmpty [Char] -> [Doc Aspects]
list NonEmpty [Char]
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 :: NonEmpty [Char] -> [Doc Aspects]
list          = Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall (t :: * -> *).
Foldable t =>
Doc Aspects -> t (Doc Aspects) -> [Doc Aspects]
punctuate Doc Aspects
comma ([Doc Aspects] -> [Doc Aspects])
-> (NonEmpty [Char] -> [Doc Aspects])
-> NonEmpty [Char]
-> [Doc Aspects]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Doc Aspects) -> [[Char]] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map (Doc Aspects -> Doc Aspects
quotes (Doc Aspects -> Doc Aspects)
-> ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text) ([[Char]] -> [Doc Aspects])
-> (NonEmpty [Char] -> [[Char]])
-> NonEmpty [Char]
-> [Doc Aspects]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty [Char] -> [[Char]]
NonEmpty [Char] -> [Item (NonEmpty [Char])]
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 Aspects
pretty (LibWarning Maybe LibPositionInfo
mc LibWarning'
w) =
    case Maybe LibPositionInfo
mc of
      Maybe LibPositionInfo
Nothing -> LibWarning' -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty LibWarning'
w
      Just (LibPositionInfo Maybe [Char]
_ Int
_ [Char]
file) -> [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
hcat [ [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text [Char]
file, Doc Aspects
":"] Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> LibWarning' -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty LibWarning'
w

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

------------------------------------------------------------------------
-- Hashable instances
------------------------------------------------------------------------

instance Hashable LibName

------------------------------------------------------------------------
-- Null instances
------------------------------------------------------------------------

instance Null LibName where
  empty :: LibName
empty = Text -> [Integer] -> LibName
LibName Text
forall a. Null a => a
empty [Integer]
forall a. Null a => a
empty
  null :: LibName -> Bool
null (LibName Text
a [Integer]
b) = Text -> Bool
forall a. Null a => a -> Bool
null Text
a Bool -> Bool -> Bool
&& [Integer] -> Bool
forall a. Null a => a -> Bool
null [Integer]
b

instance Null LibCache where
  empty :: LibCache
empty = Map [Char] ProjectConfig -> Map [Char] AgdaLibFile -> LibCache
LibCache Map [Char] ProjectConfig
forall a. Null a => a
empty Map [Char] AgdaLibFile
forall a. Null a => a
empty
  null :: LibCache -> Bool
null (LibCache Map [Char] ProjectConfig
a Map [Char] AgdaLibFile
b) = Map [Char] ProjectConfig -> Bool
forall a. Null a => a -> Bool
null Map [Char] ProjectConfig
a Bool -> Bool -> Bool
&& Map [Char] AgdaLibFile -> Bool
forall a. Null a => a -> Bool
null Map [Char] AgdaLibFile
b

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

instance NFData ExecutablesFile
instance NFData LibrariesFile
instance NFData ProjectConfig
instance NFData AgdaLibFile
instance NFData LibName
instance NFData LibCache
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
_ = ()