{-# LANGUAGE DeriveDataTypeable #-}
-- | Parser for @.agda-lib@ files.
--
--   Example file:
--
--   @
--     name: Main
--     depend:
--       standard-library
--     include: .
--       src more-src
--
--   @
--
--   Should parse as:
--
--   @
--     AgdaLib
--       { libName     = "Main"
--       , libFile     = path_to_this_file
--       , libIncludes = [ "." , "src" , "more-src" ]
--       , libDepends  = [ "standard-library" ]
--       }
--   @
--
module Agda.Interaction.Library.Parse
  ( parseLibFile
  , splitCommas
  , trimLineComment
  , LineNumber
  , runP
  , LibWarning'(..)
  ) where

import Control.Monad
import Control.Monad.Writer
import Data.Char
import Data.Data
import qualified Data.List as List
import System.FilePath

import Agda.Interaction.Library.Base

import Agda.Utils.Applicative
import Agda.Utils.Except ( MonadError(throwError), ExceptT, runExceptT )
import Agda.Utils.IO ( catchIO )
import Agda.Utils.Lens
import Agda.Utils.List   ( duplicates )
import Agda.Utils.String ( ltrim )

-- | Parser monad: Can throw @String@ error messages, and collects
-- @LibWarning'@s library warnings.
type P = ExceptT String (Writer [LibWarning'])

runP :: P a -> (Either String a, [LibWarning'])
runP :: P a -> (Either String a, [LibWarning'])
runP = Writer [LibWarning'] (Either String a)
-> (Either String a, [LibWarning'])
forall w a. Writer w a -> (a, w)
runWriter (Writer [LibWarning'] (Either String a)
 -> (Either String a, [LibWarning']))
-> (P a -> Writer [LibWarning'] (Either String a))
-> P a
-> (Either String a, [LibWarning'])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. P a -> Writer [LibWarning'] (Either String a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT

-- | Library Warnings.
data LibWarning'
  = UnknownField String
  deriving (Int -> LibWarning' -> ShowS
[LibWarning'] -> ShowS
LibWarning' -> String
(Int -> LibWarning' -> ShowS)
-> (LibWarning' -> String)
-> ([LibWarning'] -> ShowS)
-> Show LibWarning'
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LibWarning'] -> ShowS
$cshowList :: [LibWarning'] -> ShowS
show :: LibWarning' -> String
$cshow :: LibWarning' -> String
showsPrec :: Int -> LibWarning' -> ShowS
$cshowsPrec :: Int -> LibWarning' -> ShowS
Show, Typeable LibWarning'
DataType
Constr
Typeable LibWarning'
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> LibWarning' -> c LibWarning')
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c LibWarning')
-> (LibWarning' -> Constr)
-> (LibWarning' -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c LibWarning'))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c LibWarning'))
-> ((forall b. Data b => b -> b) -> LibWarning' -> LibWarning')
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> LibWarning' -> r)
-> (forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> LibWarning' -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning')
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning')
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning')
-> Data LibWarning'
LibWarning' -> DataType
LibWarning' -> Constr
(forall b. Data b => b -> b) -> LibWarning' -> LibWarning'
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning'
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> LibWarning' -> u
forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning'
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LibWarning')
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LibWarning')
$cUnknownField :: Constr
$tLibWarning' :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
gmapMp :: (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
gmapM :: (forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> LibWarning' -> m LibWarning'
gmapQi :: Int -> (forall d. Data d => d -> u) -> LibWarning' -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> LibWarning' -> u
gmapQ :: (forall d. Data d => d -> u) -> LibWarning' -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> LibWarning' -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> LibWarning' -> r
gmapT :: (forall b. Data b => b -> b) -> LibWarning' -> LibWarning'
$cgmapT :: (forall b. Data b => b -> b) -> LibWarning' -> LibWarning'
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LibWarning')
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c LibWarning')
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c LibWarning')
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c LibWarning')
dataTypeOf :: LibWarning' -> DataType
$cdataTypeOf :: LibWarning' -> DataType
toConstr :: LibWarning' -> Constr
$ctoConstr :: LibWarning' -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning'
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c LibWarning'
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> LibWarning' -> c LibWarning'
$cp1Data :: Typeable LibWarning'
Data)

warningP :: LibWarning' -> P ()
warningP :: LibWarning' -> P ()
warningP = [LibWarning'] -> P ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell ([LibWarning'] -> P ())
-> (LibWarning' -> [LibWarning']) -> LibWarning' -> P ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibWarning' -> [LibWarning']
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | The config files we parse have the generic structure of a sequence
--   of @field : content@ entries.
type GenericFile = [GenericEntry]

data GenericEntry = GenericEntry
  { GenericEntry -> String
geHeader   :: String   -- ^ E.g. field name.    @trim@med.
  , GenericEntry -> [String]
_geContent :: [String] -- ^ E.g. field content. @trim@med.
  }

-- | Library file field format format [sic!].
data Field = forall a. Field
  { Field -> String
fName     :: String            -- ^ Name of the field.
  , Field -> Bool
fOptional :: Bool              -- ^ Is it optional?
  , ()
fParse    :: [String] -> P a   -- ^ Content parser for this field.
  , ()
fSet      :: LensSet a AgdaLibFile
    -- ^ Sets parsed content in 'AgdaLibFile' structure.
  }

optionalField :: String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField :: String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
str [String] -> P a
p Lens' a AgdaLibFile
l = String
-> Bool -> ([String] -> P a) -> LensSet a AgdaLibFile -> Field
forall a.
String
-> Bool -> ([String] -> P a) -> LensSet a AgdaLibFile -> Field
Field String
str Bool
True [String] -> P a
p (Lens' a AgdaLibFile -> LensSet a AgdaLibFile
forall i o. Lens' i o -> LensSet i o
set Lens' a AgdaLibFile
l)

-- | @.agda-lib@ file format with parsers and setters.
agdaLibFields :: [Field]
agdaLibFields :: [Field]
agdaLibFields =
  -- Andreas, 2017-08-23, issue #2708, field "name" is optional.
  [ String
-> ([String] -> P String) -> Lens' String AgdaLibFile -> Field
forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
"name"    [String] -> P String
parseName                      Lens' String AgdaLibFile
libName
  , String
-> ([String] -> P [String]) -> Lens' [String] AgdaLibFile -> Field
forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
"include" ([String] -> P [String]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> P [String])
-> ([String] -> [String]) -> [String] -> P [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [String]) -> [String] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap String -> [String]
parsePaths)  Lens' [String] AgdaLibFile
libIncludes
  , String
-> ([String] -> P [String]) -> Lens' [String] AgdaLibFile -> Field
forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
"depend"  ([String] -> P [String]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([String] -> P [String])
-> ([String] -> [String]) -> [String] -> P [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [String]) -> [String] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap String -> [String]
splitCommas) Lens' [String] AgdaLibFile
libDepends
  ]
  where
    parseName :: [String] -> P LibName
    parseName :: [String] -> P String
parseName [String
s] | [String
name] <- String -> [String]
words String
s = String -> P String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
name
    parseName [String]
ls = String -> P String
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> P String) -> String -> P String
forall a b. (a -> b) -> a -> b
$ String
"Bad library name: '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
ls String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'"

    parsePaths :: String -> [FilePath]
    parsePaths :: String -> [String]
parsePaths = ShowS -> String -> [String]
go ShowS
forall a. a -> a
id where
      fixup :: ([a] -> t a) -> f (t a)
fixup [a] -> t a
acc = let fp :: t a
fp = [a] -> t a
acc [] in Bool -> Bool
not (t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
fp) Bool -> t a -> f (t a)
forall (f :: * -> *) a. Alternative f => Bool -> a -> f a
?$> t a
fp
      go :: ShowS -> String -> [String]
go ShowS
acc []           = ShowS -> [String]
forall (f :: * -> *) (t :: * -> *) a a.
(Alternative f, Foldable t) =>
([a] -> t a) -> f (t a)
fixup ShowS
acc
      go ShowS
acc (Char
'\\' : Char
' '  :String
cs) = ShowS -> String -> [String]
go (ShowS
acc ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
' 'Char -> ShowS
forall a. a -> [a] -> [a]
:)) String
cs
      go ShowS
acc (Char
'\\' : Char
'\\' :String
cs) = ShowS -> String -> [String]
go (ShowS
acc ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'\\'Char -> ShowS
forall a. a -> [a] -> [a]
:)) String
cs
      go ShowS
acc (       Char
' '  :String
cs) = ShowS -> [String]
forall (f :: * -> *) (t :: * -> *) a a.
(Alternative f, Foldable t) =>
([a] -> t a) -> f (t a)
fixup ShowS
acc [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ShowS -> String -> [String]
go ShowS
forall a. a -> a
id String
cs
      go ShowS
acc (Char
c           :String
cs) = ShowS -> String -> [String]
go (ShowS
acc ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:)) String
cs

-- | Parse @.agda-lib@ file.
--
-- Sets 'libFile' name and turn mentioned include directories into absolute
-- pathes (provided the given 'FilePath' is absolute).
--
parseLibFile :: FilePath -> IO (P AgdaLibFile)
parseLibFile :: String -> IO (P AgdaLibFile)
parseLibFile String
file =
  ((AgdaLibFile -> AgdaLibFile) -> P AgdaLibFile -> P AgdaLibFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AgdaLibFile -> AgdaLibFile
setPath (P AgdaLibFile -> P AgdaLibFile)
-> (String -> P AgdaLibFile) -> String -> P AgdaLibFile
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> P AgdaLibFile
parseLib (String -> P AgdaLibFile) -> IO String -> IO (P AgdaLibFile)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
readFile String
file) IO (P AgdaLibFile)
-> (IOException -> IO (P AgdaLibFile)) -> IO (P AgdaLibFile)
forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \IOException
e ->
    P AgdaLibFile -> IO (P AgdaLibFile)
forall (m :: * -> *) a. Monad m => a -> m a
return (P AgdaLibFile -> IO (P AgdaLibFile))
-> P AgdaLibFile -> IO (P AgdaLibFile)
forall a b. (a -> b) -> a -> b
$ String -> P AgdaLibFile
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> P AgdaLibFile) -> String -> P AgdaLibFile
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"Failed to read library file " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
file String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
      , String
"Reason: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ IOException -> String
forall a. Show a => a -> String
show IOException
e
      ]
  where
    setPath :: AgdaLibFile -> AgdaLibFile
setPath      AgdaLibFile
lib = String -> AgdaLibFile -> AgdaLibFile
unrelativise (ShowS
takeDirectory String
file) (Lens' String AgdaLibFile -> String -> AgdaLibFile -> AgdaLibFile
forall i o. Lens' i o -> LensSet i o
set Lens' String AgdaLibFile
libFile String
file AgdaLibFile
lib)
    unrelativise :: String -> AgdaLibFile -> AgdaLibFile
unrelativise String
dir = Lens' [String] AgdaLibFile -> LensMap [String] AgdaLibFile
forall i o. Lens' i o -> LensMap i o
over Lens' [String] AgdaLibFile
libIncludes (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
dir String -> ShowS
</>))

-- | Parse file contents.
parseLib :: String -> P AgdaLibFile
parseLib :: String -> P AgdaLibFile
parseLib String
s = GenericFile -> P AgdaLibFile
fromGeneric (GenericFile -> P AgdaLibFile)
-> ExceptT String (Writer [LibWarning']) GenericFile
-> P AgdaLibFile
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> ExceptT String (Writer [LibWarning']) GenericFile
parseGeneric String
s

-- | Parse 'GenericFile' with 'agdaLibFields' descriptors.
fromGeneric :: GenericFile -> P AgdaLibFile
fromGeneric :: GenericFile -> P AgdaLibFile
fromGeneric = [Field] -> GenericFile -> P AgdaLibFile
fromGeneric' [Field]
agdaLibFields

-- | Given a list of 'Field' descriptors (with their custom parsers),
--   parse a 'GenericFile' into the 'AgdaLibFile' structure.
--
--   Checks mandatory fields are present;
--   no duplicate fields, no unknown fields.

fromGeneric' :: [Field] -> GenericFile -> P AgdaLibFile
fromGeneric' :: [Field] -> GenericFile -> P AgdaLibFile
fromGeneric' [Field]
fields GenericFile
fs = do
  [Field] -> [String] -> P ()
checkFields [Field]
fields ((GenericEntry -> String) -> GenericFile -> [String]
forall a b. (a -> b) -> [a] -> [b]
map GenericEntry -> String
geHeader GenericFile
fs)
  (AgdaLibFile -> GenericEntry -> P AgdaLibFile)
-> AgdaLibFile -> GenericFile -> P AgdaLibFile
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM AgdaLibFile -> GenericEntry -> P AgdaLibFile
upd AgdaLibFile
emptyLibFile GenericFile
fs
  where
    upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
    upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
upd AgdaLibFile
l (GenericEntry String
h [String]
cs) = do
      Maybe Field
mf <- String -> [Field] -> P (Maybe Field)
findField String
h [Field]
fields
      case Maybe Field
mf of
        Just Field{Bool
String
LensSet a AgdaLibFile
[String] -> P a
fSet :: LensSet a AgdaLibFile
fParse :: [String] -> P a
fOptional :: Bool
fName :: String
fSet :: ()
fParse :: ()
fOptional :: Field -> Bool
fName :: Field -> String
..} -> do
          a
x <- [String] -> P a
fParse [String]
cs
          AgdaLibFile -> P AgdaLibFile
forall (m :: * -> *) a. Monad m => a -> m a
return (AgdaLibFile -> P AgdaLibFile) -> AgdaLibFile -> P AgdaLibFile
forall a b. (a -> b) -> a -> b
$ LensSet a AgdaLibFile
fSet a
x AgdaLibFile
l
        Maybe Field
Nothing -> AgdaLibFile -> P AgdaLibFile
forall (m :: * -> *) a. Monad m => a -> m a
return AgdaLibFile
l

-- | Ensure that there are no duplicate fields and no mandatory fields are missing.
checkFields :: [Field] -> [String] -> P ()
checkFields :: [Field] -> [String] -> P ()
checkFields [Field]
fields [String]
fs = do
  let mandatory :: [String]
mandatory = [ Field -> String
fName Field
f | Field
f <- [Field]
fields, Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Field -> Bool
fOptional Field
f ]
      -- Missing fields.
      missing :: [String]
missing   = [String]
mandatory [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [String]
fs
      -- Duplicate fields.
      dup :: [String]
dup       = [String] -> [String]
forall a. Ord a => [a] -> [a]
duplicates [String]
fs
      -- Plural s for error message.
      s :: t a -> p
s t a
xs      = if t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 then p
"s" else p
""
      list :: [String] -> String
list [String]
xs   = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " [ String
"'" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"'" | String
f <- [String]
xs ]
  Bool -> P () -> P ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing) (P () -> P ()) -> P () -> P ()
forall a b. (a -> b) -> a -> b
$ String -> P ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> P ()) -> String -> P ()
forall a b. (a -> b) -> a -> b
$ String
"Missing field" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) p a. (Foldable t, IsString p) => t a -> p
s [String]
missing String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
list [String]
missing
  Bool -> P () -> P ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup)     (P () -> P ()) -> P () -> P ()
forall a b. (a -> b) -> a -> b
$ String -> P ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> P ()) -> String -> P ()
forall a b. (a -> b) -> a -> b
$ String
"Duplicate field" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) p a. (Foldable t, IsString p) => t a -> p
s [String]
dup String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
list [String]
dup

-- | Find 'Field' with given 'fName', throw error if unknown.
findField :: String -> [Field] -> P (Maybe Field)
findField :: String -> [Field] -> P (Maybe Field)
findField String
s [Field]
fs = P (Maybe Field)
-> (Field -> P (Maybe Field)) -> Maybe Field -> P (Maybe Field)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe P (Maybe Field)
forall a. ExceptT String (Writer [LibWarning']) (Maybe a)
err (Maybe Field -> P (Maybe Field)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Field -> P (Maybe Field))
-> (Field -> Maybe Field) -> Field -> P (Maybe Field)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Field -> Maybe Field
forall a. a -> Maybe a
Just) (Maybe Field -> P (Maybe Field)) -> Maybe Field -> P (Maybe Field)
forall a b. (a -> b) -> a -> b
$ (Field -> Bool) -> [Field] -> Maybe Field
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (Field -> String) -> Field -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Field -> String
fName) [Field]
fs
  where err :: ExceptT String (Writer [LibWarning']) (Maybe a)
err = LibWarning' -> P ()
warningP (String -> LibWarning'
UnknownField String
s) P ()
-> ExceptT String (Writer [LibWarning']) (Maybe a)
-> ExceptT String (Writer [LibWarning']) (Maybe a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe a -> ExceptT String (Writer [LibWarning']) (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing

-- Generic file parser ----------------------------------------------------

-- | Example:
--
-- @
--     parseGeneric "name:Main--BLA\ndepend:--BLA\n  standard-library--BLA\ninclude : . --BLA\n  src more-src   \n"
--     == Right [("name",["Main"]),("depend",["standard-library"]),("include",[".","src more-src"])]
-- @
parseGeneric :: String -> P GenericFile
parseGeneric :: String -> ExceptT String (Writer [LibWarning']) GenericFile
parseGeneric String
s =
  [GenericLine] -> ExceptT String (Writer [LibWarning']) GenericFile
groupLines ([GenericLine]
 -> ExceptT String (Writer [LibWarning']) GenericFile)
-> ExceptT String (Writer [LibWarning']) [GenericLine]
-> ExceptT String (Writer [LibWarning']) GenericFile
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [[GenericLine]] -> [GenericLine]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[GenericLine]] -> [GenericLine])
-> ExceptT String (Writer [LibWarning']) [[GenericLine]]
-> ExceptT String (Writer [LibWarning']) [GenericLine]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, String)
 -> ExceptT String (Writer [LibWarning']) [GenericLine])
-> [(Int, String)]
-> ExceptT String (Writer [LibWarning']) [[GenericLine]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Int
 -> String -> ExceptT String (Writer [LibWarning']) [GenericLine])
-> (Int, String)
-> ExceptT String (Writer [LibWarning']) [GenericLine]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int
-> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
parseLine) ([Int] -> [String] -> [(Int, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] ([String] -> [(Int, String)]) -> [String] -> [(Int, String)]
forall a b. (a -> b) -> a -> b
$ ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowS
stripComments ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
s)

type LineNumber = Int

-- | Lines with line numbers.
data GenericLine
  = Header  LineNumber String
      -- ^ Header line, like a field name, e.g. "include :".  Cannot be indented.
      --   @String@ is 'trim'med.
  | Content LineNumber String
      -- ^ Other line.  Must be indented.
      --   @String@ is 'trim'med.
  deriving (Int -> GenericLine -> ShowS
[GenericLine] -> ShowS
GenericLine -> String
(Int -> GenericLine -> ShowS)
-> (GenericLine -> String)
-> ([GenericLine] -> ShowS)
-> Show GenericLine
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GenericLine] -> ShowS
$cshowList :: [GenericLine] -> ShowS
show :: GenericLine -> String
$cshow :: GenericLine -> String
showsPrec :: Int -> GenericLine -> ShowS
$cshowsPrec :: Int -> GenericLine -> ShowS
Show)

-- | Parse line into 'Header' and 'Content' components.
--
--   Precondition: line comments and trailing whitespace have been stripped away.
--
--   Example file:
--
--   @
--     name: Main
--     depend:
--       standard-library
--     include: .
--       src more-src
--   @
--
--   This should give
--
--   @
--     [ Header  1 "name"
--     , Content 1 "Main"
--     , Header  2 "depend"
--     , Content 3 "standard-library"
--     , Header  4 "include"
--     , Content 4 "."
--     , Content 5 "src more-src"
--     ]
--   @
parseLine :: LineNumber -> String -> P [GenericLine]
parseLine :: Int
-> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
parseLine Int
_ String
"" = [GenericLine]
-> ExceptT String (Writer [LibWarning']) [GenericLine]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
parseLine Int
l s :: String
s@(Char
c:String
_)
    -- Indented lines are 'Content'.
  | Char -> Bool
isSpace Char
c   = [GenericLine]
-> ExceptT String (Writer [LibWarning']) [GenericLine]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Int -> String -> GenericLine
Content Int
l (String -> GenericLine) -> String -> GenericLine
forall a b. (a -> b) -> a -> b
$ ShowS
ltrim String
s]
    -- Non-indented lines are 'Header'.
  | Bool
otherwise   =
    case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
':') String
s of
      -- Headers are single words followed by a colon.
      -- Anything after the colon that is not whitespace is 'Content'.
      (String
h, Char
':' : String
r) ->
        case String -> [String]
words String
h of
          [String
h] -> [GenericLine]
-> ExceptT String (Writer [LibWarning']) [GenericLine]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([GenericLine]
 -> ExceptT String (Writer [LibWarning']) [GenericLine])
-> [GenericLine]
-> ExceptT String (Writer [LibWarning']) [GenericLine]
forall a b. (a -> b) -> a -> b
$ [Int -> String -> GenericLine
Header Int
l String
h] [GenericLine] -> [GenericLine] -> [GenericLine]
forall a. [a] -> [a] -> [a]
++ [Int -> String -> GenericLine
Content Int
l String
r' | let r' :: String
r' = ShowS
ltrim String
r, Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
r')]
          []  -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String (Writer [LibWarning']) [GenericLine])
-> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": Missing field name"
          [String]
hs  -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String (Writer [LibWarning']) [GenericLine])
-> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": Bad field name " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
h
      (String, String)
_ -> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String (Writer [LibWarning']) [GenericLine])
-> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": Missing ':' for field " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show (ShowS
ltrim String
s)

-- | Collect 'Header' and subsequent 'Content's into 'GenericEntry'.
--
--   Tailing 'Content's?  That's an error.
--
groupLines :: [GenericLine] -> P GenericFile
groupLines :: [GenericLine] -> ExceptT String (Writer [LibWarning']) GenericFile
groupLines [] = GenericFile -> ExceptT String (Writer [LibWarning']) GenericFile
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
groupLines (Content Int
l String
c : [GenericLine]
_) = String -> ExceptT String (Writer [LibWarning']) GenericFile
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> ExceptT String (Writer [LibWarning']) GenericFile)
-> String -> ExceptT String (Writer [LibWarning']) GenericFile
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": Missing field"
groupLines (Header Int
_ String
h : [GenericLine]
ls) = (String -> [String] -> GenericEntry
GenericEntry String
h [ String
c | Content Int
_ String
c <- [GenericLine]
cs ] GenericEntry -> GenericFile -> GenericFile
forall a. a -> [a] -> [a]
:) (GenericFile -> GenericFile)
-> ExceptT String (Writer [LibWarning']) GenericFile
-> ExceptT String (Writer [LibWarning']) GenericFile
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GenericLine] -> ExceptT String (Writer [LibWarning']) GenericFile
groupLines [GenericLine]
ls1
  where
    ([GenericLine]
cs, [GenericLine]
ls1) = (GenericLine -> Bool)
-> [GenericLine] -> ([GenericLine], [GenericLine])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span GenericLine -> Bool
isContent [GenericLine]
ls
    isContent :: GenericLine -> Bool
isContent Content{} = Bool
True
    isContent Header{} = Bool
False

-- | Remove leading whitespace and line comment.
trimLineComment :: String -> String
trimLineComment :: ShowS
trimLineComment = ShowS
stripComments ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
ltrim

-- | Break a comma-separated string.  Result strings are @trim@med.
splitCommas :: String -> [String]
splitCommas :: String -> [String]
splitCommas String
s = String -> [String]
words (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
',' then Char
' ' else Char
c) String
s

-- | ...and trailing, but not leading, whitespace.
stripComments :: String -> String
stripComments :: ShowS
stripComments String
"" = String
""
stripComments (Char
'-':Char
'-':String
_) = String
""
stripComments (Char
c : String
s)     = Char -> ShowS
cons Char
c (ShowS
stripComments String
s)
  where
    cons :: Char -> ShowS
cons Char
c String
"" | Char -> Bool
isSpace Char
c = String
""
    cons Char
c String
s = Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: String
s