-- | 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.Semigroup              ( Semigroup(..) )
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, LineNumber -> LibName -> ShowS
[LibName] -> ShowS
LibName -> [Char]
(LineNumber -> LibName -> ShowS)
-> (LibName -> [Char]) -> ([LibName] -> ShowS) -> Show LibName
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibName -> ShowS
showsPrec :: LineNumber -> 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
pretty = \case
    LibName Text
base [] -> Text -> Doc
forall a. Pretty a => a -> Doc
pretty Text
base
    LibName Text
base [Integer]
vs -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Text -> Doc
forall a. Pretty a => a -> Doc
pretty Text
base, Doc
"-", [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
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 (LineNumber -> LibrariesFile -> ShowS
[LibrariesFile] -> ShowS
LibrariesFile -> [Char]
(LineNumber -> LibrariesFile -> ShowS)
-> (LibrariesFile -> [Char])
-> ([LibrariesFile] -> ShowS)
-> Show LibrariesFile
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibrariesFile -> ShowS
showsPrec :: LineNumber -> 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 (LineNumber -> ExecutablesFile -> ShowS
[ExecutablesFile] -> ShowS
ExecutablesFile -> [Char]
(LineNumber -> ExecutablesFile -> ShowS)
-> (ExecutablesFile -> [Char])
-> ([ExecutablesFile] -> ShowS)
-> Show ExecutablesFile
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> ExecutablesFile -> ShowS
showsPrec :: LineNumber -> 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 -> 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 -> [[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 LineNumber -> OptionsPragma -> ShowS
[OptionsPragma] -> ShowS
OptionsPragma -> [Char]
(LineNumber -> OptionsPragma -> ShowS)
-> (OptionsPragma -> [Char])
-> ([OptionsPragma] -> ShowS)
-> Show OptionsPragma
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> OptionsPragma -> ShowS
showsPrec :: LineNumber -> 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. Ord 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 -> LineNumber
_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 (LineNumber -> AgdaLibFile -> ShowS
[AgdaLibFile] -> ShowS
AgdaLibFile -> [Char]
(LineNumber -> AgdaLibFile -> ShowS)
-> (AgdaLibFile -> [Char])
-> ([AgdaLibFile] -> ShowS)
-> Show AgdaLibFile
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> AgdaLibFile -> ShowS
showsPrec :: LineNumber -> 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 :: LineNumber
_libAbove    = LineNumber
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 LineNumber
lensConfigAbove LineNumber -> f LineNumber
f = \case
  ProjectConfig
DefaultProjectConfig -> ProjectConfig
DefaultProjectConfig ProjectConfig -> f LineNumber -> f ProjectConfig
forall a b. a -> f b -> f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ LineNumber -> f LineNumber
f LineNumber
0
  c :: ProjectConfig
c@ProjectConfig{} -> LineNumber -> f LineNumber
f (ProjectConfig -> LineNumber
configAbove ProjectConfig
c) f LineNumber -> (LineNumber -> ProjectConfig) -> f ProjectConfig
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ !LineNumber
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 LineNumber
libAbove LineNumber -> f LineNumber
f AgdaLibFile
a = LineNumber -> f LineNumber
f (AgdaLibFile -> LineNumber
_libAbove AgdaLibFile
a) f LineNumber -> (LineNumber -> AgdaLibFile) -> f AgdaLibFile
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ LineNumber
x -> AgdaLibFile
a { _libAbove = x }

libIncludes :: Lens' AgdaLibFile [FilePath]
libIncludes :: Lens' AgdaLibFile [[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 -> LineNumber
lineNumPos :: LineNumber     -- ^ Line number in @libraries@ file.
  , LibPositionInfo -> [Char]
filePos    :: FilePath       -- ^ Library file.
  }
  deriving (LineNumber -> LibPositionInfo -> ShowS
[LibPositionInfo] -> ShowS
LibPositionInfo -> [Char]
(LineNumber -> LibPositionInfo -> ShowS)
-> (LibPositionInfo -> [Char])
-> ([LibPositionInfo] -> ShowS)
-> Show LibPositionInfo
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibPositionInfo -> ShowS
showsPrec :: LineNumber -> 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 (LineNumber -> LibWarning -> ShowS
[LibWarning] -> ShowS
LibWarning -> [Char]
(LineNumber -> LibWarning -> ShowS)
-> (LibWarning -> [Char])
-> ([LibWarning] -> ShowS)
-> Show LibWarning
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibWarning -> ShowS
showsPrec :: LineNumber -> 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 (LineNumber -> LibWarning' -> ShowS
[LibWarning'] -> ShowS
LibWarning' -> [Char]
(LineNumber -> LibWarning' -> ShowS)
-> (LibWarning' -> [Char])
-> ([LibWarning'] -> ShowS)
-> Show LibWarning'
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibWarning' -> ShowS
showsPrec :: LineNumber -> 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 (LineNumber -> LibError -> ShowS
[LibError] -> ShowS
LibError -> [Char]
(LineNumber -> LibError -> ShowS)
-> (LibError -> [Char]) -> ([LibError] -> ShowS) -> Show LibError
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibError -> ShowS
showsPrec :: LineNumber -> 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 (LineNumber -> LibError' -> ShowS
[LibError'] -> ShowS
LibError' -> [Char]
(LineNumber -> LibError' -> ShowS)
-> (LibError' -> [Char])
-> ([LibError'] -> ShowS)
-> Show LibError'
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibError' -> ShowS
showsPrec :: LineNumber -> 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 (LineNumber -> LibParseError -> ShowS
[LibParseError] -> ShowS
LibParseError -> [Char]
(LineNumber -> LibParseError -> ShowS)
-> (LibParseError -> [Char])
-> ([LibParseError] -> ShowS)
-> Show LibParseError
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibParseError -> ShowS
showsPrec :: LineNumber -> 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 =>
List1 LibError -> m ()
raiseErrors = LibErrWarns -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (LibErrWarns -> m ())
-> (List1 LibError -> LibErrWarns) -> List1 LibError -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LibError -> Either LibError LibWarning)
-> [LibError] -> LibErrWarns
forall a b. (a -> b) -> [a] -> [b]
map LibError -> Either LibError LibWarning
forall a b. a -> Either a b
Left ([LibError] -> LibErrWarns)
-> (List1 LibError -> [LibError]) -> List1 LibError -> LibErrWarns
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 LibError -> [Item (List1 LibError)]
List1 LibError -> [LibError]
forall l. IsList l => l -> [Item l]
toList


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

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

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

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 -> List1 LibError
libErrors                   :: List1 LibError
  } deriving (LineNumber -> LibErrors -> ShowS
[LibErrors] -> ShowS
LibErrors -> [Char]
(LineNumber -> LibErrors -> ShowS)
-> (LibErrors -> [Char])
-> ([LibErrors] -> ShowS)
-> Show LibErrors
forall a.
(LineNumber -> a -> ShowS)
-> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: LineNumber -> LibErrors -> ShowS
showsPrec :: LineNumber -> 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
formatLibError [AgdaLibFile]
installed (LibError Maybe LibPositionInfo
mc LibError'
e) =
  case (Maybe LibPositionInfo
mc, LibError'
e) of
    (Just LibPositionInfo
c, LibParseError LibParseError
err) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep  [ LibPositionInfo -> LibParseError -> Doc
formatLibPositionInfo LibPositionInfo
c LibParseError
err, LibError' -> Doc
forall a. Pretty a => a -> Doc
pretty LibError'
e ]
    (Maybe LibPositionInfo
_     , LibNotFound{}    ) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [ LibError' -> Doc
forall a. Pretty a => a -> Doc
pretty LibError'
e, [AgdaLibFile] -> Doc
prettyInstalledLibraries [AgdaLibFile]
installed ]
    (Maybe LibPositionInfo, LibError')
_ -> LibError' -> Doc
forall a. Pretty a => a -> Doc
pretty LibError'
e


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

-- | Does a parse error contain a line number?
hasLineNumber :: LibParseError -> Maybe LineNumber
hasLineNumber :: LibParseError -> Maybe LineNumber
hasLineNumber = \case
  BadLibraryName       [Char]
_   -> Maybe LineNumber
forall a. Maybe a
Nothing
  ReadFailure          [Char]
_ IOException
_ -> Maybe LineNumber
forall a. Maybe a
Nothing
  MissingFields        List1 [Char]
_   -> Maybe LineNumber
forall a. Maybe a
Nothing
  DuplicateFields      List1 [Char]
_   -> Maybe LineNumber
forall a. Maybe a
Nothing
  MissingFieldName     LineNumber
l   -> LineNumber -> Maybe LineNumber
forall a. a -> Maybe a
Just LineNumber
l
  BadFieldName         LineNumber
l [Char]
_ -> LineNumber -> Maybe LineNumber
forall a. a -> Maybe a
Just LineNumber
l
  MissingColonForField LineNumber
l [Char]
_ -> 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 [Char]
libFile LineNumber
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] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
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 [ [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
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 [ [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
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 [ LibName -> Doc
forall a. Pretty a => a -> Doc
pretty (LibName -> Doc) -> LibName -> Doc
forall a b. (a -> b) -> a -> b
$ AgdaLibFile -> LibName
_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
$ [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
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
pretty = \case

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

    LibNotFound LibrariesFile
file LibName
lib -> [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
"Library '", LibName -> Doc
forall a. Pretty a => a -> Doc
pretty LibName
lib, Doc
"' 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
$ [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
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
"to install."
            ]
      ]

    AmbiguousLib LibName
lib List2 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 [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ Doc
"Ambiguous library '", LibName -> Doc
forall a. Pretty a => a -> Doc
pretty LibName
lib, Doc
"'." ]
            , 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
$ LibName -> Doc
forall a. Pretty a => a -> Doc
pretty (AgdaLibFile -> LibName
_libName AgdaLibFile
l) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc -> Doc
parens ([Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
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] -> 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 [ Doc
"The project root", [Char] -> Doc
forall a. Pretty a => a -> Doc
pretty [Char]
root ]
        Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: Doc
"may contain only one .agda-lib file, but I found several:"
        Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: ([Char] -> Doc) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"-" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc -> Doc) -> ([Char] -> Doc) -> [Char] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
forall a. Pretty a => a -> Doc
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
forall a. Pretty a => a -> Doc
pretty LibParseError
err

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

    DuplicateExecutable [Char]
exeFile Text
exe List2 (LineNumber, [Char])
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 '", ([Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> (Text -> [Char]) -> Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> [Char]
unpack) Text
exe, Doc
"' in ", [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
exeFile, Doc
":" ] Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:
      ((LineNumber, [Char]) -> Doc) -> [(LineNumber, [Char])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (LineNumber
ln, [Char]
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
<+> [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
fp) (List2 (LineNumber, [Char]) -> [Item (List2 (LineNumber, [Char]))]
forall l. IsList l => l -> [Item l]
toList List2 (LineNumber, [Char])
paths)

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

    BadLibraryName [Char]
s -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep
      [ Doc
"Bad library name:", Doc -> Doc
quotes ([Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
s) ]
    ReadFailure [Char]
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", [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
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
<+> [Char] -> Doc
forall a. [Char] -> Doc a
text (IOException -> [Char]
forall e. Exception e => e -> [Char]
showIOException IOException
e)
      ]

    MissingFields   List1 [Char]
xs -> Doc
"Missing"   Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> List1 [Char] -> Doc
listFields List1 [Char]
xs
    DuplicateFields List1 [Char]
xs -> Doc
"Duplicate" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> List1 [Char] -> Doc
listFields List1 [Char]
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 [Char]
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
<+> [Char] -> Doc
forall a. [Char] -> Doc a
text (ShowS
forall a. Show a => a -> [Char]
show [Char]
s)
    MissingColonForField LineNumber
l [Char]
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
<+> [Char] -> Doc
forall a. [Char] -> Doc a
text (ShowS
forall a. Show a => a -> [Char]
show [Char]
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 [Char] -> Doc
listFields List1 [Char]
xs = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ List1 [Char] -> Doc
forall {a} {c}. (Sized a, IsString c) => a -> c
fieldS List1 [Char]
xs Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: List1 [Char] -> [Doc]
list List1 [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 :: List1 [Char] -> [Doc]
list          = Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc])
-> (List1 [Char] -> [Doc]) -> List1 [Char] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> Doc) -> [[Char]] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
quotes (Doc -> Doc) -> ([Char] -> Doc) -> [Char] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Doc
forall a. [Char] -> Doc a
text) ([[Char]] -> [Doc])
-> (List1 [Char] -> [[Char]]) -> List1 [Char] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 [Char] -> [[Char]]
List1 [Char] -> [Item (List1 [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
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 [Char]
_ LineNumber
_ [Char]
file) -> [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
hcat [ [Char] -> Doc
forall a. [Char] -> Doc a
text [Char]
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 [Char]
s) = [Char] -> Doc
forall a. [Char] -> Doc a
text ([Char] -> Doc) -> [Char] -> Doc
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
_ = ()