module Language.Fixpoint.Parse (
Inputable (..)
, Parser
, lexer
, reserved, reservedOp
, parens , brackets
, semi , comma
, colon , dcolon
, whiteSpace, blanks
, fTyConP
, lowerIdP
, upperIdP
, symbolP
, constantP
, integer
, exprP
, predP
, qualifierP
, condIdP
, freshIntP
, doParse'
, parseFromFile
, remainderP
) where
import Control.Applicative ((<*>), (<$>), (<*))
import Control.Monad
import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.Language
import Text.Parsec.String hiding (Parser, parseFromFile)
import Text.Printf (printf)
import qualified Text.Parsec.Token as Token
import qualified Data.HashMap.Strict as M
import Data.Char (isLower, toUpper)
import Language.Fixpoint.Misc hiding (dcolon)
import Language.Fixpoint.Types
import Data.Maybe(maybe)
type Parser = Parsec String Integer
languageDef =
emptyDef { Token.commentStart = "/* "
, Token.commentEnd = " */"
, Token.commentLine = "--"
, Token.identStart = satisfy (\_ -> False)
, Token.identLetter = satisfy (\_ -> False)
, Token.reservedNames = [ "SAT"
, "UNSAT"
, "true"
, "false"
, "mod"
, "data"
, "Bexp"
, "forall"
, "exists"
, "assume"
, "measure"
, "module"
, "spec"
, "where"
, "True"
, "Int"
, "import"
, "_|_"
, "|"
, "if", "then", "else"
]
, Token.reservedOpNames = [ "+", "-", "*", "/", "\\"
, "<", ">", "<=", ">=", "=", "!=" , "/="
, "mod", "and", "or"
, "&&", "||"
, "~", "=>", "<=>"
, "->"
, ":="
, "&", "^", "<<", ">>", "--"
, "?", "Bexp"
]
}
lexer = Token.makeTokenParser languageDef
reserved = Token.reserved lexer
reservedOp = Token.reservedOp lexer
parens = Token.parens lexer
brackets = Token.brackets lexer
semi = Token.semi lexer
colon = Token.colon lexer
comma = Token.comma lexer
whiteSpace = Token.whiteSpace lexer
stringLiteral = Token.stringLiteral lexer
blanks = many (satisfy (`elem` [' ', '\t']))
integer = try (liftM toInt is)
<|> liftM (negate . toInt) (char '-' >> is)
where is = liftM2 (\is _ -> is) (many1 digit) blanks
toInt s = (read s) :: Integer
condIdP :: [Char] -> (String -> Bool) -> Parser String
condIdP chars f
= do c <- letter
cs <- many (satisfy (`elem` chars))
blanks
if f (c:cs) then return (c:cs) else parserZero
upperIdP :: Parser String
upperIdP = condIdP symChars (not . isLower . head)
lowerIdP :: Parser String
lowerIdP = condIdP symChars (isLower . head)
symbolP :: Parser Symbol
symbolP = liftM stringSymbol symCharsP
constantP :: Parser Constant
constantP = liftM I integer
symconstP :: Parser SymConst
symconstP = SL <$> stringLiteral
exprP :: Parser Expr
exprP = expr2P <|> lexprP
lexprP :: Parser Expr
lexprP
= try (parens exprP)
<|> try (parens exprCastP)
<|> try (parens $ condP EIte exprP)
<|> try exprFunP
<|> try (liftM (EVar . stringSymbol) upperIdP)
<|> liftM expr symbolP
<|> liftM ECon constantP
<|> liftM ESym symconstP
<|> (reserved "_|_" >> return EBot)
exprFunP = (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP
where
exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces)
exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma)
exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi)
funSymbolP = symbolP
parenBrackets = parens . brackets
expr2P = buildExpressionParser bops lexprP
bops = [ [Infix (reservedOp "*" >> return (EBin Times)) AssocLeft]
, [Infix (reservedOp "/" >> return (EBin Div )) AssocLeft]
, [Infix (reservedOp "+" >> return (EBin Plus )) AssocLeft]
, [Infix (reservedOp "-" >> return (EBin Minus)) AssocLeft]
, [Infix (reservedOp "mod" >> return (EBin Mod )) AssocLeft]
]
exprCastP
= do e <- exprP
((try dcolon) <|> colon)
so <- sortP
return $ ECst e so
dcolon = string "::" <* spaces
sortP
= try (string "Integer" >> return FInt)
<|> try (string "Int" >> return FInt)
<|> try (string "int" >> return FInt)
<|> try (FObj . stringSymbol <$> lowerIdP)
<|> (FApp <$> fTyConP <*> many sortP )
symCharsP = (condIdP symChars (\_ -> True))
predP :: Parser Pred
predP = try (parens pred2P)
<|> try (parens $ condP pIte predP)
<|> try (reservedOp "not" >> liftM PNot predP)
<|> try (reservedOp "&&" >> liftM PAnd predsP)
<|> try (reservedOp "||" >> liftM POr predsP)
<|> (qmP >> liftM PBexp exprP)
<|> (reserved "true" >> return PTrue)
<|> (reserved "false" >> return PFalse)
<|> (try predrP)
<|> (try (liftM PBexp exprFunP))
qmP = reserved "?" <|> reserved "Bexp"
pred2P = buildExpressionParser lops predP
predsP = brackets $ sepBy predP semi
lops = [ [Prefix (reservedOp "~" >> return PNot)]
, [Infix (reservedOp "&&" >> return (\x y -> PAnd [x,y])) AssocRight]
, [Infix (reservedOp "||" >> return (\x y -> POr [x,y])) AssocRight]
, [Infix (reservedOp "=>" >> return PImp) AssocRight]
, [Infix (reservedOp "<=>" >> return PIff) AssocRight]]
predrP = do e1 <- expr2P
r <- brelP
e2 <- expr2P
return $ r e1 e2
brelP :: Parser (Expr -> Expr -> Pred)
brelP = (reservedOp "==" >> return (PAtom Eq))
<|> (reservedOp "=" >> return (PAtom Eq))
<|> (reservedOp "!=" >> return (PAtom Ne))
<|> (reservedOp "/=" >> return (PAtom Ne))
<|> (reservedOp "<" >> return (PAtom Lt))
<|> (reservedOp "<=" >> return (PAtom Le))
<|> (reservedOp ">" >> return (PAtom Gt))
<|> (reservedOp ">=" >> return (PAtom Ge))
condIteP f bodyP
= do reserved "if"
p <- predP
reserved "then"
b1 <- bodyP
reserved "else"
b2 <- bodyP
return $ f p b1 b2
condQmP f bodyP
= do p <- predP
reserved "?"
b1 <- bodyP
colon
b2 <- bodyP
return $ f p b1 b2
condP f bodyP
= try (condIteP f bodyP)
<|> (condQmP f bodyP)
fTyConP
= (reserved "int" >> return intFTyCon)
<|> (reserved "bool" >> return boolFTyCon)
<|> (stringFTycon <$> upperIdP)
refasP :: Parser [Refa]
refasP = (try (brackets $ sepBy (RConc <$> predP) semi))
<|> liftM ((:[]) . RConc) predP
qualifierP = do n <- upperIdP
params <- parens $ sepBy1 sortBindP comma
_ <- colon
body <- predP
return $ mkQual n params body
sortBindP = (,) <$> symbolP <* colon <*> sortP
mkQual n xts p = Q n ((vv, t) : yts) (subst su p)
where
(vv,t):zts = xts
yts = mapFst mkParam <$> zts
su = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts
mkParam s = stringSymbolRaw ('~' : toUpper c : cs)
where
(c:cs) = symbolString s
fixResultP :: Parser a -> Parser (FixResult a)
fixResultP pp
= (reserved "SAT" >> return Safe)
<|> (reserved "UNSAT" >> Unsafe <$> (brackets $ sepBy pp comma))
<|> (reserved "CRASH" >> crashP pp)
crashP pp
= do i <- pp
msg <- many anyChar
return $ Crash [i] msg
predSolP
= parens $ (predP <* (comma >> iQualP))
iQualP
= upperIdP >> (parens $ sepBy symbolP comma)
solution1P
= do reserved "solution:"
k <- symbolP
reserved ":="
ps <- brackets $ sepBy predSolP semi
return (k, simplify $ PAnd ps)
solutionP :: Parser (M.HashMap Symbol Pred)
solutionP
= M.fromList <$> sepBy solution1P whiteSpace
solutionFileP
= liftM2 (,) (fixResultP integer) solutionP
remainderP p
= do res <- p
str <- stateInput <$> getParserState
return (res, str)
doParse' parser f s
= case runParser (remainderP p) 0 f s of
Left e -> errorstar $ printf "parseError %s\n when parsing from %s\n"
(show e) f
Right (r, "") -> r
Right (_, rem) -> errorstar $ printf "doParse has leftover when parsing: %s\nfrom file %s\n"
rem f
where p = whiteSpace >> parser
parseFromFile :: Parser b -> SourceName -> IO b
parseFromFile p f = doParse' p f <$> readFile f
freshIntP :: Parser Integer
freshIntP = do n <- stateUser <$> getParserState
updateState (+ 1)
return n
class Inputable a where
rr :: String -> a
rr' :: String -> String -> a
rr' = \_ -> rr
rr = rr' ""
instance Inputable Symbol where
rr' = doParse' symbolP
instance Inputable Constant where
rr' = doParse' constantP
instance Inputable Pred where
rr' = doParse' predP
instance Inputable Expr where
rr' = doParse' exprP
instance Inputable [Refa] where
rr' = doParse' refasP
instance Inputable (FixResult Integer) where
rr' = doParse' $ fixResultP integer
instance Inputable (FixResult Integer, FixSolution) where
rr' = doParse' solutionFileP