-- | 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.Char                   ( isDigit )
import qualified Data.List         as List
import Data.Map                    ( Map )
import qualified Data.Map          as Map
import Data.Text                   ( Text, unpack )

import GHC.Generics                ( Generic )

import System.Directory
import System.FilePath

import Agda.Interaction.Options.Warnings

import Agda.Utils.FileName
import Agda.Utils.Lens
import Agda.Utils.List1            ( List1, toList )
import Agda.Utils.List2            ( List2, toList )
import Agda.Utils.Null
import Agda.Utils.Pretty

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

data LibrariesFile = LibrariesFile
  { LibrariesFile -> String
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 -> String
forall a.
(LineNumber -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LibrariesFile] -> ShowS
$cshowList :: [LibrariesFile] -> ShowS
show :: LibrariesFile -> String
$cshow :: LibrariesFile -> String
showsPrec :: LineNumber -> LibrariesFile -> ShowS
$cshowsPrec :: LineNumber -> LibrariesFile -> ShowS
Show)

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

data ExecutablesFile = ExecutablesFile
  { ExecutablesFile -> String
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 -> String
forall a.
(LineNumber -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExecutablesFile] -> ShowS
$cshowList :: [ExecutablesFile] -> ShowS
show :: ExecutablesFile -> String
$cshow :: ExecutablesFile -> String
showsPrec :: LineNumber -> ExecutablesFile -> ShowS
$cshowsPrec :: LineNumber -> ExecutablesFile -> ShowS
Show, 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
$cto :: forall x. Rep ExecutablesFile x -> ExecutablesFile
$cfrom :: forall x. ExecutablesFile -> Rep ExecutablesFile x
Generic)

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

-- | 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 -> String
configRoot         :: FilePath
    , ProjectConfig -> [String]
configAgdaLibFiles :: [FilePath]
    }
  | DefaultProjectConfig
  deriving 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
$cto :: forall x. Rep ProjectConfig x -> ProjectConfig
$cfrom :: forall x. ProjectConfig -> Rep ProjectConfig x
Generic

-- | Content of a @.agda-lib@ file.
--
data AgdaLibFile = AgdaLibFile
  { AgdaLibFile -> String
_libName     :: LibName     -- ^ The symbolic name of the library.
  , AgdaLibFile -> String
_libFile     :: FilePath    -- ^ Path to this @.agda-lib@ file (not content of the file).
  , AgdaLibFile -> [String]
_libIncludes :: [FilePath]  -- ^ Roots where to look for the modules of the library.
  , AgdaLibFile -> [String]
_libDepends  :: [LibName]   -- ^ Dependencies.
  , AgdaLibFile -> [String]
_libPragmas  :: [String]    -- ^ Default pragma options for all files in the library.
  }
  deriving (LineNumber -> AgdaLibFile -> ShowS
[AgdaLibFile] -> ShowS
AgdaLibFile -> String
forall a.
(LineNumber -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AgdaLibFile] -> ShowS
$cshowList :: [AgdaLibFile] -> ShowS
show :: AgdaLibFile -> String
$cshow :: AgdaLibFile -> String
showsPrec :: LineNumber -> AgdaLibFile -> ShowS
$cshowsPrec :: LineNumber -> AgdaLibFile -> ShowS
Show, 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
$cto :: forall x. Rep AgdaLibFile x -> AgdaLibFile
$cfrom :: forall x. AgdaLibFile -> Rep AgdaLibFile x
Generic)

emptyLibFile :: AgdaLibFile
emptyLibFile :: AgdaLibFile
emptyLibFile = AgdaLibFile
  { _libName :: String
_libName     = String
""
  , _libFile :: String
_libFile     = String
""
  , _libIncludes :: [String]
_libIncludes = []
  , _libDepends :: [String]
_libDepends  = []
  , _libPragmas :: [String]
_libPragmas  = []
  }

-- | Lenses for AgdaLibFile

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

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

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

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

libPragmas :: Lens' [String] AgdaLibFile
libPragmas :: Lens' [String] AgdaLibFile
libPragmas [String] -> f [String]
f AgdaLibFile
a = [String] -> f [String]
f (AgdaLibFile -> [String]
_libPragmas AgdaLibFile
a) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ [String]
x -> AgdaLibFile
a { _libPragmas :: [String]
_libPragmas = [String]
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 String
libFilePos :: Maybe FilePath -- ^ Name of @libraries@ file.
  , LibPositionInfo -> LineNumber
lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
  , LibPositionInfo -> String
filePos    :: FilePath       -- ^ Library file.
  }
  deriving (LineNumber -> LibPositionInfo -> ShowS
[LibPositionInfo] -> ShowS
LibPositionInfo -> String
forall a.
(LineNumber -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LibPositionInfo] -> ShowS
$cshowList :: [LibPositionInfo] -> ShowS
show :: LibPositionInfo -> String
$cshow :: LibPositionInfo -> String
showsPrec :: LineNumber -> LibPositionInfo -> ShowS
$cshowsPrec :: LineNumber -> LibPositionInfo -> ShowS
Show, 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
$cto :: forall x. Rep LibPositionInfo x -> LibPositionInfo
$cfrom :: forall x. LibPositionInfo -> Rep LibPositionInfo x
Generic)

-- ** Warnings

data LibWarning = LibWarning (Maybe LibPositionInfo) LibWarning'
  deriving (LineNumber -> LibWarning -> ShowS
[LibWarning] -> ShowS
LibWarning -> String
forall a.
(LineNumber -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LibWarning] -> ShowS
$cshowList :: [LibWarning] -> ShowS
show :: LibWarning -> String
$cshow :: LibWarning -> String
showsPrec :: LineNumber -> LibWarning -> ShowS
$cshowsPrec :: LineNumber -> LibWarning -> ShowS
Show, 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
$cto :: forall x. Rep LibWarning x -> LibWarning
$cfrom :: forall x. LibWarning -> Rep LibWarning x
Generic)

-- | Library Warnings.
data LibWarning'
  = UnknownField String
  deriving (LineNumber -> LibWarning' -> ShowS
[LibWarning'] -> ShowS
LibWarning' -> String
forall a.
(LineNumber -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LibWarning'] -> ShowS
$cshowList :: [LibWarning'] -> ShowS
show :: LibWarning' -> String
$cshow :: LibWarning' -> String
showsPrec :: LineNumber -> LibWarning' -> ShowS
$cshowsPrec :: LineNumber -> LibWarning' -> ShowS
Show, 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
$cto :: forall x. Rep LibWarning' x -> LibWarning'
$cfrom :: forall x. LibWarning' -> Rep LibWarning' x
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 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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe LibPositionInfo -> LibWarning' -> LibWarning
LibWarning forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe LibPositionInfo -> LibError' -> LibError
LibError forall a. Maybe a
Nothing)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) =>
String -> m (Maybe ProjectConfig)
getCachedProjectConfig String
path = do
  String
path <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO String
canonicalizePath String
path
  Map String ProjectConfig
cache <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a, b) -> a
fst
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
path Map String ProjectConfig
cache

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

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

storeCachedAgdaLibFile
  :: (MonadState LibState m, MonadIO m)
  => FilePath -> AgdaLibFile -> m ()
storeCachedAgdaLibFile :: forall (m :: * -> *).
(MonadState LibState m, MonadIO m) =>
String -> AgdaLibFile -> m ()
storeCachedAgdaLibFile String
path AgdaLibFile
lib = do
  String
path <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO String
canonicalizePath String
path
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
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) -> forall (t :: * -> *). Foldable t => t Doc -> Doc
sep  [ LibPositionInfo -> LibParseError -> Doc
formatLibPositionInfo LibPositionInfo
c LibParseError
err, forall a. Pretty a => a -> Doc
pretty LibError'
e ]
    (Maybe LibPositionInfo
_     , LibNotFound{}    ) -> forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ forall a. Pretty a => a -> Doc
pretty LibError'
e, [AgdaLibFile] -> Doc
prettyInstalledLibraries [AgdaLibFile]
installed ]
    (Maybe LibPositionInfo, LibError')
_ -> 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       String
_   -> forall a. Maybe a
Nothing
  ReadFailure          String
_ IOException
_ -> forall a. Maybe a
Nothing
  MissingFields        List1 String
_   -> forall a. Maybe a
Nothing
  DuplicateFields      List1 String
_   -> forall a. Maybe a
Nothing
  MissingFieldName     LineNumber
l   -> forall a. a -> Maybe a
Just LineNumber
l
  BadFieldName         LineNumber
l String
_ -> forall a. a -> Maybe a
Just LineNumber
l
  MissingColonForField LineNumber
l String
_ -> forall a. a -> Maybe a
Just LineNumber
l
  ContentWithoutField  LineNumber
l   -> 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 String
libFile LineNumber
lineNum String
file) = \case

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

prettyInstalledLibraries :: [AgdaLibFile] -> Doc
prettyInstalledLibraries :: [AgdaLibFile] -> Doc
prettyInstalledLibraries [AgdaLibFile]
installed =
  forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat forall a b. (a -> b) -> a -> b
$ (Doc
"Installed libraries:" forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$
    forall a b. (a -> b) -> [a] -> [b]
map (LineNumber -> Doc -> Doc
nest LineNumber
2) forall a b. (a -> b) -> a -> b
$
    if forall a. Null a => a -> Bool
null [AgdaLibFile]
installed then [Doc
"(none)"]
    else [ forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ String -> Doc
text forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> String
_libName AgdaLibFile
l, LineNumber -> Doc -> Doc
nest LineNumber
2 forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens forall a b. (a -> b) -> a -> b
$ String -> Doc
text forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> String
_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 String
path -> forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
      [ String -> Doc
text String
"Libraries file not found:"
      , String -> Doc
text String
path
      ]

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

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

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

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

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

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

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

    MissingFields   List1 String
xs -> Doc
"Missing"   Doc -> Doc -> Doc
<+> List1 String -> Doc
listFields List1 String
xs
    DuplicateFields List1 String
xs -> Doc
"Duplicate" Doc -> Doc -> Doc
<+> List1 String -> Doc
listFields List1 String
xs

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

    where
    listFields :: List1 String -> Doc
listFields List1 String
xs = forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep forall a b. (a -> b) -> a -> b
$ forall {a} {c}. (Sized a, IsString c) => a -> c
fieldS List1 String
xs forall a. a -> [a] -> [a]
: List1 String -> [Doc]
list List1 String
xs
    fieldS :: a -> c
fieldS a
xs     = forall a c. Sized a => a -> c -> c -> c
singPlural a
xs c
"field:" c
"fields:"
    list :: List1 String -> [Doc]
list          = forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
quotes forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l. IsList l => l -> [Item l]
toList
    atLine :: p -> a -> a
atLine p
l      = 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 -> forall a. Pretty a => a -> Doc
pretty LibWarning'
w
      Just (LibPositionInfo Maybe String
_ LineNumber
_ String
file) -> forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ String -> Doc
text String
file, Doc
":"] Doc -> Doc -> Doc
<+> forall a. Pretty a => a -> Doc
pretty LibWarning'
w

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

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

instance NFData ExecutablesFile
instance NFData ProjectConfig
instance NFData AgdaLibFile
instance NFData LibPositionInfo
instance NFData LibWarning
instance NFData LibWarning'