module Agda.Interaction.Library.Parse
( parseLibFile
, splitCommas
, trimLineComment
, runP
) where
import Control.Monad
import Control.Monad.Except
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.IO ( catchIO )
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.Lens
import Agda.Utils.List ( duplicates )
import Agda.Utils.String ( ltrim )
type P = ExceptT String (Writer [LibWarning'])
runP :: P a -> (Either String a, [LibWarning'])
runP :: forall a. P a -> (Either String a, [LibWarning'])
runP = forall w a. Writer w a -> (a, w)
runWriter forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
warningP :: LibWarning' -> P ()
warningP :: LibWarning' -> P ()
warningP = forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure
type GenericFile = [GenericEntry]
data GenericEntry = GenericEntry
{ :: String
, GenericEntry -> [String]
_geContent :: [String]
}
data Field = forall a. Field
{ Field -> String
fName :: String
, Field -> Bool
fOptional :: Bool
, ()
fParse :: [String] -> P a
, ()
fSet :: LensSet a AgdaLibFile
}
optionalField :: String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField :: forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
str [String] -> P a
p Lens' a AgdaLibFile
l = forall a.
String
-> Bool -> ([String] -> P a) -> LensSet a AgdaLibFile -> Field
Field String
str Bool
True [String] -> P a
p (forall i o. Lens' i o -> LensSet i o
set Lens' a AgdaLibFile
l)
agdaLibFields :: [Field]
agdaLibFields :: [Field]
agdaLibFields =
[ forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
"name" [String] -> P String
parseName Lens' String AgdaLibFile
libName
, forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
"include" (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap String -> [String]
parsePaths) Lens' [String] AgdaLibFile
libIncludes
, forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
"depend" (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap String -> [String]
splitCommas) Lens' [String] AgdaLibFile
libDepends
, forall a.
String -> ([String] -> P a) -> Lens' a AgdaLibFile -> Field
optionalField String
"flags" (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap String -> [String]
parseFlags) Lens' [String] AgdaLibFile
libPragmas
]
where
parseName :: [String] -> P LibName
parseName :: [String] -> P String
parseName [String
s] | [String
name] <- String -> [String]
words String
s = forall (f :: * -> *) a. Applicative f => a -> f a
pure String
name
parseName [String]
ls = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"Bad library name: '" forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
ls forall a. [a] -> [a] -> [a]
++ String
"'"
parsePaths :: String -> [FilePath]
parsePaths :: String -> [String]
parsePaths = (String -> String) -> String -> [String]
go 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
fp) forall (f :: * -> *) a. Alternative f => Bool -> a -> f a
?$> t a
fp
go :: (String -> String) -> String -> [String]
go String -> String
acc [] = forall {f :: * -> *} {t :: * -> *} {a} {a}.
(Alternative f, Foldable t) =>
([a] -> t a) -> f (t a)
fixup String -> String
acc
go String -> String
acc (Char
'\\' : Char
' ' :String
cs) = (String -> String) -> String -> [String]
go (String -> String
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
' 'forall a. a -> [a] -> [a]
:)) String
cs
go String -> String
acc (Char
'\\' : Char
'\\' :String
cs) = (String -> String) -> String -> [String]
go (String -> String
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'\\'forall a. a -> [a] -> [a]
:)) String
cs
go String -> String
acc ( Char
' ' :String
cs) = forall {f :: * -> *} {t :: * -> *} {a} {a}.
(Alternative f, Foldable t) =>
([a] -> t a) -> f (t a)
fixup String -> String
acc forall a. [a] -> [a] -> [a]
++ (String -> String) -> String -> [String]
go forall a. a -> a
id String
cs
go String -> String
acc (Char
c :String
cs) = (String -> String) -> String -> [String]
go (String -> String
acc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
cforall a. a -> [a] -> [a]
:)) String
cs
parseFlags :: String -> [String]
parseFlags :: String -> [String]
parseFlags = String -> [String]
words
parseLibFile :: FilePath -> IO (P AgdaLibFile)
parseLibFile :: String -> IO (P AgdaLibFile)
parseLibFile String
file =
(forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap AgdaLibFile -> AgdaLibFile
setPath forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> P AgdaLibFile
parseLib forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
UTF8.readFile String
file) forall (m :: * -> *) a.
CatchIO m =>
m a -> (IOException -> m a) -> m a
`catchIO` \IOException
e ->
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"Failed to read library file " forall a. [a] -> [a] -> [a]
++ String
file forall a. [a] -> [a] -> [a]
++ String
"."
, String
"Reason: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show IOException
e
]
where
setPath :: AgdaLibFile -> AgdaLibFile
setPath AgdaLibFile
lib = String -> AgdaLibFile -> AgdaLibFile
unrelativise (String -> String
takeDirectory String
file) (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 = forall i o. Lens' i o -> LensMap i o
over Lens' [String] AgdaLibFile
libIncludes (forall a b. (a -> b) -> [a] -> [b]
map (String
dir String -> String -> String
</>))
parseLib :: String -> P AgdaLibFile
parseLib :: String -> P AgdaLibFile
parseLib String
s = GenericFile -> P AgdaLibFile
fromGeneric forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> P GenericFile
parseGeneric String
s
fromGeneric :: GenericFile -> P AgdaLibFile
fromGeneric :: GenericFile -> P AgdaLibFile
fromGeneric = [Field] -> GenericFile -> P AgdaLibFile
fromGeneric' [Field]
agdaLibFields
fromGeneric' :: [Field] -> GenericFile -> P AgdaLibFile
fromGeneric' :: [Field] -> GenericFile -> P AgdaLibFile
fromGeneric' [Field]
fields GenericFile
fs = do
[Field] -> [String] -> P ()
checkFields [Field]
fields (forall a b. (a -> b) -> [a] -> [b]
map GenericEntry -> String
geHeader GenericFile
fs)
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
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LensSet a AgdaLibFile
fSet a
x AgdaLibFile
l
Maybe Field
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return AgdaLibFile
l
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 forall a b. (a -> b) -> a -> b
$ Field -> Bool
fOptional Field
f ]
missing :: [String]
missing = [String]
mandatory forall a. Eq a => [a] -> [a] -> [a]
List.\\ [String]
fs
dup :: [String]
dup = forall a. Ord a => [a] -> [a]
duplicates [String]
fs
s :: t a -> a
s t a
xs = if forall (t :: * -> *) a. Foldable t => t a -> LineNumber
length t a
xs forall a. Ord a => a -> a -> Bool
> LineNumber
1 then a
"s" else a
""
list :: [String] -> String
list [String]
xs = forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " [ String
"'" forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
"'" | String
f <- [String]
xs ]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"Missing field" forall a. [a] -> [a] -> [a]
++ forall {t :: * -> *} {a} {a}. (Foldable t, IsString a) => t a -> a
s [String]
missing forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [String] -> String
list [String]
missing
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ String
"Duplicate field" forall a. [a] -> [a] -> [a]
++ forall {t :: * -> *} {a} {a}. (Foldable t, IsString a) => t a -> a
s [String]
dup forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [String] -> String
list [String]
dup
findField :: String -> [Field] -> P (Maybe Field)
findField :: String -> [Field] -> P (Maybe Field)
findField String
s [Field]
fs = forall b a. b -> (a -> b) -> Maybe a -> b
maybe P (Maybe Field)
err (forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find ((String
s forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Field -> String
fName) [Field]
fs
where err :: P (Maybe Field)
err = LibWarning' -> P ()
warningP (String -> LibWarning'
UnknownField String
s) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
parseGeneric :: String -> P GenericFile
parseGeneric :: String -> P GenericFile
parseGeneric String
s =
[GenericLine] -> P GenericFile
groupLines forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM LineNumber
-> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
parseLine [LineNumber
1..] (forall a b. (a -> b) -> [a] -> [b]
map String -> String
stripComments forall a b. (a -> b) -> a -> b
$ String -> [String]
lines String
s)
data GenericLine
= LineNumber String
| Content LineNumber String
deriving (LineNumber -> GenericLine -> String -> String
[GenericLine] -> String -> String
GenericLine -> String
forall a.
(LineNumber -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [GenericLine] -> String -> String
$cshowList :: [GenericLine] -> String -> String
show :: GenericLine -> String
$cshow :: GenericLine -> String
showsPrec :: LineNumber -> GenericLine -> String -> String
$cshowsPrec :: LineNumber -> GenericLine -> String -> String
Show)
parseLine :: LineNumber -> String -> P [GenericLine]
parseLine :: LineNumber
-> String -> ExceptT String (Writer [LibWarning']) [GenericLine]
parseLine LineNumber
_ String
"" = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
parseLine LineNumber
l s :: String
s@(Char
c:String
_)
| Char -> Bool
isSpace Char
c = forall (f :: * -> *) a. Applicative f => a -> f a
pure [LineNumber -> String -> GenericLine
Content LineNumber
l forall a b. (a -> b) -> a -> b
$ String -> String
ltrim String
s]
| Bool
otherwise =
case forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall a. Eq a => a -> a -> Bool
==Char
':') String
s of
(String
h, Char
':' : String
r) ->
case String -> [String]
words String
h of
[String
h] -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ LineNumber -> String -> GenericLine
Header LineNumber
l String
h forall a. a -> [a] -> [a]
: [LineNumber -> String -> GenericLine
Content LineNumber
l String
r' | let r' :: String
r' = String -> String
ltrim String
r, Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
r')]
[] -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show LineNumber
l forall a. [a] -> [a] -> [a]
++ String
": Missing field name"
[String]
hs -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show LineNumber
l forall a. [a] -> [a] -> [a]
++ String
": Bad field name " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
h
(String, String)
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show LineNumber
l forall a. [a] -> [a] -> [a]
++ String
": Missing ':' for field " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (String -> String
ltrim String
s)
groupLines :: [GenericLine] -> P GenericFile
groupLines :: [GenericLine] -> P GenericFile
groupLines [] = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
groupLines (Content LineNumber
l String
c : [GenericLine]
_) = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show LineNumber
l forall a. [a] -> [a] -> [a]
++ String
": Missing field"
groupLines (Header LineNumber
_ String
h : [GenericLine]
ls) = (String -> [String] -> GenericEntry
GenericEntry String
h [ String
c | Content LineNumber
_ String
c <- [GenericLine]
cs ] forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [GenericLine] -> P GenericFile
groupLines [GenericLine]
ls1
where
([GenericLine]
cs, [GenericLine]
ls1) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span GenericLine -> Bool
isContent [GenericLine]
ls
isContent :: GenericLine -> Bool
isContent Content{} = Bool
True
isContent Header{} = Bool
False
trimLineComment :: String -> String
= String -> String
stripComments forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
ltrim
splitCommas :: String -> [String]
splitCommas :: String -> [String]
splitCommas String
s = String -> [String]
words forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> if Char
c forall a. Eq a => a -> a -> Bool
== Char
',' then Char
' ' else Char
c) String
s
stripComments :: String -> String
String
"" = String
""
stripComments (Char
'-':Char
'-':Char
c:String
_) | Char -> Bool
isSpace Char
c = String
""
stripComments (Char
c : String
s) = Char -> String -> String
cons Char
c (String -> String
stripComments String
s)
where
cons :: Char -> String -> String
cons Char
c String
"" | Char -> Bool
isSpace Char
c = String
""
cons Char
c String
s = Char
c forall a. a -> [a] -> [a]
: String
s