module Language.Fixpoint.Parse (
Inputable (..)
, Parser
, lexer
, reserved, reservedOp
, parens , brackets, angles, braces
, semi , comma
, colon , dcolon
, whiteSpace
, blanks
, fTyConP
, lowerIdP
, upperIdP
, symbolP
, constantP
, integer
, bindP
, exprP
, predP
, funAppP
, qualifierP
, refP
, refDefP
, refBindP
, condIdP
, locParserP
, locLowerIdP
, locUpperIdP
, freshIntP
, doParse'
, parseFromFile
, remainderP
) where
import Control.Applicative ((<*>), (<$>), (<*))
import Control.Monad
import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.Pos
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 qualified Data.HashSet as S
import Data.Text (Text)
import qualified Data.Text as T
import Data.Char (isLower, toUpper)
import Language.Fixpoint.Misc hiding (dcolon)
import Language.Fixpoint.Types
import Language.Fixpoint.Errors
import Language.Fixpoint.SmtLib2
import Data.Maybe(maybe, fromJust)
import Data.Monoid (mempty)
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
angles = Token.angles lexer
semi = Token.semi lexer
colon = Token.colon lexer
comma = Token.comma lexer
whiteSpace = Token.whiteSpace lexer
stringLiteral = Token.stringLiteral lexer
braces = Token.braces lexer
double = Token.float lexer
blanks = many (satisfy (`elem` [' ', '\t']))
integer = posInteger
posInteger = toI <$> (many1 digit <* spaces)
where
toI :: String -> Integer
toI = read
locParserP :: Parser a -> Parser (Located a)
locParserP p = liftM2 Loc getPosition p
condIdP :: [Char] -> (String -> Bool) -> Parser Symbol
condIdP chars f
= do c <- letter
cs <- many (satisfy (`elem` chars))
blanks
if f (c:cs) then return (symbol $ T.pack $ c:cs) else parserZero
upperIdP :: Parser Symbol
upperIdP = condIdP symChars (not . isLower . head)
lowerIdP :: Parser Symbol
lowerIdP = condIdP symChars (isLower . head)
locLowerIdP = locParserP lowerIdP
locUpperIdP = locParserP upperIdP
symbolP :: Parser Symbol
symbolP = symbol <$> symCharsP
constantP :: Parser Constant
constantP = try (liftM R double) <|> liftM I integer
symconstP :: Parser SymConst
symconstP = SL . T.pack <$> stringLiteral
expr0P :: Parser Expr
expr0P
= (fastIfP EIte exprP)
<|> (ESym <$> symconstP)
<|> (ECon <$> constantP)
<|> (reserved "_|_" >> return EBot)
<|> try (parens exprP)
<|> try (parens exprCastP)
<|> (charsExpr <$> symCharsP)
charsExpr cs
| isLower (T.head t) = expr cs
| otherwise = EVar cs
where t = symbolText cs
fastIfP f bodyP
= do reserved "if"
p <- predP
reserved "then"
b1 <- bodyP
reserved "else"
b2 <- bodyP
return $ f p b1 b2
expr1P :: Parser Expr
expr1P
= try funAppP
<|> expr0P
exprP :: Parser Expr
exprP = buildExpressionParser bops expr1P
funAppP = (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP
where
exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P spaces)
exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma)
exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi)
funSymbolP = locParserP symbolP
parenBrackets = parens . brackets
bops = [ [ Prefix (reservedOp "-" >> return eMinus)]
, [ Infix (reservedOp "*" >> return (EBin Times)) AssocLeft
, Infix (reservedOp "/" >> return (EBin Div )) AssocLeft
]
, [ Infix (reservedOp "-" >> return (EBin Minus)) AssocLeft
, Infix (reservedOp "+" >> return (EBin Plus )) AssocLeft
]
, [Infix (reservedOp "mod" >> return (EBin Mod )) AssocLeft]
]
eMinus = EBin Minus (expr (0 :: Integer))
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 . symbol <$> lowerIdP)
<|> (fApp <$> (Left <$> fTyConP) <*> many sortP)
symCharsP = condIdP symChars (`notElem` keyWordSyms)
keyWordSyms = ["if", "then", "else", "mod"]
trueP = reserved "true" >> return PTrue
falseP = reserved "false" >> return PFalse
pred0P :: Parser Pred
pred0P = trueP
<|> falseP
<|> try (fastIfP pIte predP)
<|> try predrP
<|> try (parens predP)
<|> try (liftM PBexp funAppP)
<|> try (reservedOp "&&" >> liftM PAnd predsP)
<|> try (reservedOp "||" >> liftM POr predsP)
predP :: Parser Pred
predP = buildExpressionParser lops pred0P
predsP = brackets $ sepBy predP semi
qmP = reserved "?" <|> reserved "Bexp"
lops = [ [Prefix (reservedOp "~" >> return PNot)]
, [Prefix (reservedOp "not " >> 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 <- exprP
r <- brelP
e2 <- exprP
return $ r e1 e2
brelP :: Parser (Expr -> Expr -> Pred)
brelP = (reservedOp "==" >> return (PAtom Eq))
<|> (reservedOp "=" >> return (PAtom Eq))
<|> (reservedOp "~~" >> return (PAtom Ueq))
<|> (reservedOp "!=" >> return (PAtom Ne))
<|> (reservedOp "/=" >> return (PAtom Ne))
<|> (reservedOp "!~" >> return (PAtom Une))
<|> (reservedOp "<" >> return (PAtom Lt))
<|> (reservedOp "<=" >> return (PAtom Le))
<|> (reservedOp ">" >> return (PAtom Gt))
<|> (reservedOp ">=" >> return (PAtom Ge))
condP f bodyP
= try (condIteP f bodyP)
<|> (condQmP f bodyP)
condI = condIteP EIte
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
fTyConP
= (reserved "int" >> return intFTyCon)
<|> (reserved "bool" >> return boolFTyCon)
<|> (reserved "real" >> return realFTyCon)
<|> (symbolFTycon <$> locUpperIdP)
refasP :: Parser [Refa]
refasP = (try (brackets $ sepBy (RConc <$> predP) semi))
<|> liftM ((:[]) . RConc) predP
refBindP :: Parser Symbol -> Parser [Refa] -> Parser (Reft -> a) -> Parser a
refBindP bp rp kindP
= braces $ do
vv <- bp
t <- kindP
reserved "|"
ras <- rp <* spaces
return $ t (Reft (vv, ras))
bindP = liftM symbol (lowerIdP <* colon)
optBindP vv = try bindP <|> return vv
refP = refBindP bindP refasP
refDefP vv = refBindP (optBindP vv)
qualifierP = do pos <- getPosition
n <- upperIdP
params <- parens $ sepBy1 sortBindP comma
_ <- colon
body <- predP
return $ mkQual n params body pos
sortBindP = (,) <$> symbolP <* colon <*> sortP
mkQual n xts p pos = Q n ((vv, t) : yts) (subst su p) pos
where
(vv,t):zts = xts
yts = mapFst mkParam <$> zts
su = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts
mkParam s = symbol ('~' `T.cons` toUpper c `T.cons` cs)
where
Just (c,cs)= T.uncons $ symbolText s
fInfoP :: Parser (FInfo ())
fInfoP = defsFInfo <$> many defP
defP :: Parser (Def ())
defP = Srt <$> (reserved "sort" >> colon >> sortP)
<|> Axm <$> (reserved "axiom" >> colon >> predP)
<|> Cst <$> (reserved "constraint" >> colon >> subCP)
<|> Wfc <$> (reserved "wf" >> colon >> wfCP)
<|> Con <$> (reserved "constant" >> symbolP) <*> (colon >> sortP)
<|> Qul <$> (reserved "qualifier" >> qualifierP)
<|> Kut <$> (reserved "cut" >> symbolP)
<|> IBind <$> (reserved "bind" >> intP) <*> symbolP <*> (colon >> sortedReftP)
sortedReftP :: Parser SortedReft
sortedReftP = refP (RR <$> (sortP <* spaces))
wfCP :: Parser (WfC ())
wfCP = do reserved "env"
env <- envP
reserved "reft"
r <- sortedReftP
return $ wfC env r Nothing ()
subCP :: Parser (SubC ())
subCP = do reserved "env"
env <- envP
reserved "grd"
grd <- predP
reserved "lhs"
lhs <- sortedReftP
reserved "rhs"
rhs <- sortedReftP
reserved "id"
i <- (integer <* spaces)
tag <- tagP
return $ safeHead "subCP" $ subC env grd lhs rhs (Just i) tag ()
tagP :: Parser [Int]
tagP = try (reserved "tag" >> spaces >> (brackets $ sepBy intP semi))
<|> (return [])
envP :: Parser IBindEnv
envP = do binds <- brackets $ sepBy (intP <* spaces) semi
return $ insertsIBindEnv binds emptyIBindEnv
intP :: Parser Int
intP = fromInteger <$> integer
defsFInfo :: [Def a] -> FInfo a
defsFInfo defs = FI cm ws bs gs lts kts qs
where
cm = M.fromList [(cid c, c) | Cst c <- defs]
ws = [w | Wfc w <- defs]
bs = rawBindEnv [(n, x, r) | IBind n x r <- defs]
gs = fromListSEnv [(x, RR t mempty) | Con x t <- defs]
lts = [(x, t) | Con x t <- defs, notFun t]
kts = KS $ S.fromList [k | Kut k <- defs]
qs = [q | Qul q <- defs]
cid = fromJust . sid
notFun = not . isFunctionSortedReft . (`RR` trueReft)
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 <- getInput
pos <- getPosition
return (res, str, pos)
doParse' parser f s
= case runParser (remainderP (whiteSpace >> parser)) 0 f s of
Left e -> die $ err (errorSpan e) $ printf "parseError %s\n when parsing from %s\n" (show e) f
Right (r, "", _) -> r
Right (_, rem, l) -> die $ err (SS l l) $ printf "doParse has leftover when parsing: %s\nfrom file %s\n" rem f
errorSpan e = SS l l where l = errorPos e
parseFromFile :: Parser b -> SourceName -> IO b
parseFromFile p f = doParse' p f <$> readFile f
freshIntP :: Parser Integer
freshIntP = do n <- getState
updateState (+ 1)
return n
commandsP = sepBy commandP semi
commandP
= (reserved "var" >> cmdVarP)
<|> (reserved "push" >> return Push)
<|> (reserved "pop" >> return Pop)
<|> (reserved "check" >> return CheckSat)
<|> (reserved "assert" >> (Assert Nothing <$> predP))
<|> (reserved "distinct" >> (Distinct <$> (brackets $ sepBy exprP comma)))
cmdVarP
= do x <- bindP
t <- sortP
return $ Declare x [] t
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
instance Inputable (FInfo ()) where
rr' = doParse' fInfoP
instance Inputable Command where
rr' = doParse' commandP
instance Inputable [Command] where
rr' = doParse' commandsP