module Agda.Interaction.Library.Parse ( parseLibFile, splitCommas, trimLineComment, LineNumber ) where
import Control.Exception
import Control.Monad
import Data.Char
import qualified Data.List as List
import System.FilePath
import Agda.Interaction.Library.Base
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.IO ( catchIO )
import Agda.Utils.String ( ltrim )
type P = Either String
type GenericFile = [GenericEntry]
data GenericEntry = GenericEntry
{ geHeader :: String
, geContent :: [String]
}
data Field = forall a. Field
{ fName :: String
, fOptional :: Bool
, fParse :: [String] -> P a
, fSet :: a -> AgdaLibFile -> AgdaLibFile
}
agdaLibFields :: [Field]
agdaLibFields =
[ Field "name" True parseName $ \ name l -> l { libName = name }
, Field "include" True (pure . concatMap words) $ \ inc l -> l { libIncludes = inc }
, Field "depend" True (pure . concatMap splitCommas) $ \ ds l -> l { libDepends = ds }
]
where
parseName [s] | [name] <- words s = pure name
parseName ls = throwError $ "Bad library name: '" ++ unwords ls ++ "'"
parseLibFile :: FilePath -> IO (P AgdaLibFile)
parseLibFile file =
(fmap setPath . parseLib <$> readFile file) `catchIO` \e ->
return (Left $ "Failed to read library file " ++ file ++ ".\nReason: " ++ show e)
where
setPath lib = unrelativise (takeDirectory file) lib{ libFile = file }
unrelativise dir lib = lib { libIncludes = map (dir </>) (libIncludes lib) }
parseLib :: String -> P AgdaLibFile
parseLib s = fromGeneric =<< parseGeneric s
fromGeneric :: GenericFile -> P AgdaLibFile
fromGeneric = fromGeneric' agdaLibFields
fromGeneric' :: [Field] -> GenericFile -> P AgdaLibFile
fromGeneric' fields fs = do
checkFields fields (map geHeader fs)
foldM upd emptyLibFile fs
where
upd :: AgdaLibFile -> GenericEntry -> P AgdaLibFile
upd l (GenericEntry h cs) = do
Field{..} <- findField h fields
x <- fParse cs
return $ fSet x l
checkFields :: [Field] -> [String] -> P ()
checkFields fields fs = do
let mandatory = [ fName f | f <- fields, not $ fOptional f ]
missing = mandatory List.\\ fs
dup = fs List.\\ List.nub fs
s xs = if length xs > 1 then "s" else ""
list xs = List.intercalate ", " [ "'" ++ f ++ "'" | f <- xs ]
when (not $ null missing) $ throwError $ "Missing field" ++ s missing ++ " " ++ list missing
when (not $ null dup) $ throwError $ "Duplicate field" ++ s dup ++ " " ++ list dup
findField :: String -> [Field] -> P Field
findField s fs = maybe err return $ List.find ((s ==) . fName) fs
where err = throwError $ "Unknown field '" ++ s ++ "'"
parseGeneric :: String -> P GenericFile
parseGeneric s =
groupLines =<< concat <$> mapM (uncurry parseLine) (zip [1..] $ map stripComments $ lines s)
type LineNumber = Int
data GenericLine
= Header LineNumber String
| Content LineNumber String
deriving (Show)
parseLine :: LineNumber -> String -> P [GenericLine]
parseLine _ "" = pure []
parseLine l s@(c:_)
| isSpace c = pure [Content l $ ltrim s]
| otherwise =
case break (==':') s of
(h, ':' : r) ->
case words h of
[h] -> pure $ [Header l h] ++ [Content l r' | let r' = ltrim r, not (null r')]
[] -> throwError $ show l ++ ": Missing field name"
hs -> throwError $ show l ++ ": Bad field name " ++ show h
_ -> throwError $ show l ++ ": Missing ':' for field " ++ show (ltrim s)
groupLines :: [GenericLine] -> P GenericFile
groupLines [] = pure []
groupLines (Content l c : _) = throwError $ show l ++ ": Missing field"
groupLines (Header _ h : ls) = (GenericEntry h [ c | Content _ c <- cs ] :) <$> groupLines ls1
where
(cs, ls1) = span isContent ls
isContent Content{} = True
isContent Header{} = False
trimLineComment :: String -> String
trimLineComment = stripComments . ltrim
splitCommas :: String -> [String]
splitCommas s = words $ map (\c -> if c == ',' then ' ' else c) s
stripComments :: String -> String
stripComments "" = ""
stripComments ('-':'-':_) = ""
stripComments (c : s) = cons c (stripComments s)
where
cons c "" | isSpace c = ""
cons c s = c : s