-- | 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.Lens
import Agda.Utils.List1            ( List1, toList )
import Agda.Utils.List2            ( List2, toList )
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)

-- | 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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'

-- | 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 (Show)

-- | 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.

-- ** 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 'Doc' exceptions, still collects 'LibWarning's.
type LibM = ExceptT Doc (WriterT [LibWarning] (StateT LibState IO))

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

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

-- | 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
E.displayException 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
E.displayException 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 ProjectConfig
instance NFData AgdaLibFile
instance NFData LibPositionInfo
instance NFData LibWarning
instance NFData LibWarning'