module Language.Fixpoint.Parse (
Inputable (..)
, Parser
, lexer
, reserved, reservedOp
, parens , brackets, angles, braces
, semi , comma
, colon , dcolon
, whiteSpace
, blanks
, pairP
, lowerIdP
, upperIdP
, symbolP
, constantP
, integer
, bindP
, sortP
, mkQual
, exprP
, predP
, funAppP
, qualifierP
, refaP
, refP
, refDefP
, refBindP
, bvSortP
, condIdP
, locParserP
, locLowerIdP
, locUpperIdP
, freshIntP
, doParse'
, parseFromFile
, remainderP
, isSmall
) where
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.Text as T
import Data.Maybe (fromJust)
import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.Language (emptyDef)
import qualified Text.Parsec.Token as Token
import GHC.Generics (Generic)
import Data.Char (isLower)
import Language.Fixpoint.Smt.Bitvector
import Language.Fixpoint.Types.Errors
import Language.Fixpoint.Misc (tshow, sortNub, thd3)
import Language.Fixpoint.Smt.Types
import Language.Fixpoint.Types.Visitor (foldSort, mapSort)
import Language.Fixpoint.Types hiding (mapSort)
import Text.PrettyPrint.HughesPJ (text, nest, vcat, (<+>))
type Parser = Parsec String Integer
languageDef =
emptyDef { Token.commentStart = "/* "
, Token.commentEnd = " */"
, Token.commentLine = "//"
, Token.identStart = satisfy (const False)
, Token.identLetter = satisfy (const 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 = do l1 <- getPosition
x <- p
l2 <- getPosition
return $ Loc l1 l2 x
condIdP :: S.HashSet Char -> (String -> Bool) -> Parser Symbol
condIdP chars f
= do c <- letter <|> char '_'
cs <- many (satisfy (`S.member` chars))
blanks
if f (c:cs) then return (symbol $ c:cs) else parserZero
upperIdP :: Parser Symbol
upperIdP = condIdP symChars (not . isSmall . head)
lowerIdP :: Parser Symbol
lowerIdP = condIdP symChars (isSmall . head)
isSmall :: Char -> Bool
isSmall c = isLower c || c == '_'
symCharsP :: Parser Symbol
symCharsP = condIdP symChars (`notElem` keyWordSyms)
locLowerIdP = locParserP lowerIdP
locUpperIdP = locParserP upperIdP
symbolP :: Parser Symbol
symbolP = symbol <$> symCharsP
constantP :: Parser Constant
constantP = try (R <$> double)
<|> I <$> integer
symconstP :: Parser SymConst
symconstP = SL . T.pack <$> stringLiteral
expr0P :: Parser Expr
expr0P
= (fastIfP EIte exprP)
<|> (ESym <$> symconstP)
<|> (ECon <$> constantP)
<|> (reserved "_|_" >> return EBot)
<|> lamP
<|> try (parens exprP)
<|> try (parens exprCastP)
<|> (charsExpr <$> symCharsP)
charsExpr cs
| isSmall (headSym cs) = expr cs
| otherwise = EVar 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 litP) <|> (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP <|> simpleAppP
where
exprFunSpacesP = mkEApp <$> funSymbolP <*> sepBy1 expr0P blanks
exprFunCommasP = mkEApp <$> funSymbolP <*> parens (sepBy exprP comma)
exprFunSemisP = mkEApp <$> funSymbolP <*> parenBrackets (sepBy exprP semi)
simpleAppP = EApp <$> (parens exprP) <*> (parens exprP)
funSymbolP = locParserP symbolP
litP = do reserved "lit"
l <- stringLiteral
t <- sortP
return $ ECon $ L (T.pack l) t
parenBrackets = parens . brackets
bops = [ [ Prefix (reservedOp "-" >> return ENeg)]
, [ 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]
]
exprCastP
= do e <- exprP
(try dcolon) <|> colon
so <- sortP
return $ ECst e so
lamP
= do reserved "\\"
x <- symbolP
colon
t <- sortP
reserved "->"
e <- exprP
return $ ELam (x, t) e
dcolon = string "::" <* spaces
varSortP = FVar <$> parens intP
funcSortP = parens $ mkFFunc <$> intP <* comma <*> sortsP
sortsP = brackets $ sepBy sortP semi
sortP :: Parser Sort
sortP = sortP' (sepBy sortArgP blanks)
sortArgP :: Parser Sort
sortArgP = sortP' (return [])
sortP' :: Parser [Sort] -> Parser Sort
sortP' appArgsP
= try (parens sortP)
<|> try (string "func" >> funcSortP)
<|> try (fAppTC listFTyCon . single <$> brackets sortP)
<|> try bvSortP
<|> try (fAppTC <$> fTyConP <*> appArgsP)
<|> try (fApp <$> tvarP <*> appArgsP)
single x = [x]
tvarP :: Parser Sort
tvarP
= try (string "@" >> varSortP)
<|> (FObj . symbol <$> lowerIdP)
fTyConP :: Parser FTycon
fTyConP
= (reserved "int" >> return intFTyCon)
<|> (reserved "Integer" >> return intFTyCon)
<|> (reserved "Int" >> return intFTyCon)
<|> (reserved "int" >> return intFTyCon)
<|> (reserved "real" >> return realFTyCon)
<|> (reserved "bool" >> return boolFTyCon)
<|> (reserved "num" >> return numFTyCon)
<|> (symbolFTycon <$> locUpperIdP)
bvSortP
= mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64)
bvSizeP ss s = do
parens (reserved "BitVec" >> reserved ss)
return s
keyWordSyms = ["if", "then", "else", "mod"]
pred0P :: Parser Expr
pred0P = trueP
<|> falseP
<|> try (reserved "??" >> return PGrad)
<|> try kvarPredP
<|> try (fastIfP pIte predP)
<|> try predrP
<|> try (parens predP)
<|> try (reserved "?" *> exprP)
<|> try funAppP
<|> try (reservedOp "&&" >> PAnd <$> predsP)
<|> try (reservedOp "||" >> POr <$> predsP)
trueP, falseP :: Parser Expr
trueP = reserved "true" >> return PTrue
falseP = reserved "false" >> return PFalse
kvarPredP :: Parser Expr
kvarPredP = PKVar <$> kvarP <*> substP
kvarP :: Parser KVar
kvarP = KV <$> (char '$' *> symbolP <* spaces)
substP :: Parser Subst
substP = mkSubst <$> many (brackets $ pairP symbolP aP exprP)
where
aP = reserved ":="
predP :: Parser Expr
predP = buildExpressionParser lops pred0P
predsP = brackets $ sepBy predP semi
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 PImp) AssocRight]
, [Infix (reservedOp "<=>" >> return PIff) AssocRight]]
predrP = do e1 <- exprP
r <- brelP
e2 <- exprP
return $ r e1 e2
brelP :: Parser (Expr -> Expr -> Expr)
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))
refaP :: Parser Expr
refaP = try (pAnd <$> brackets (sepBy predP semi))
<|> predP
refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP bp rp kindP
= braces $ do
x <- bp
t <- kindP
reserved "|"
ra <- rp <* spaces
return $ t (Reft (x, ra))
bindP = symbolP <* colon
optBindP x = try bindP <|> return x
refP = refBindP bindP refaP
refDefP x = refBindP (optBindP x)
qualifierP tP = do
pos <- getPosition
n <- upperIdP
params <- parens $ sepBy1 (sortBindP tP) comma
_ <- colon
body <- predP
return $ mkQual n params body pos
sortBindP = pairP symbolP colon
pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP xP sepP yP = (,) <$> xP <* sepP <*> yP
mkQual :: Symbol -> [(Symbol, Sort)] -> Expr -> SourcePos -> Qualifier
mkQual n xts p = Q n ((v, t) : yts) (subst su p)
where
(v, t):zts = gSorts xts
yts = zts
su = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts
gSorts :: [(a, Sort)] -> [(a, Sort)]
gSorts xts = [(x, substVars su t) | (x, t) <- xts]
where
su = (`zip` [0..]) . sortNub . concatMap (sortVars . snd) $ xts
substVars :: [(Symbol, Int)] -> Sort -> Sort
substVars su = mapSort tx
where
tx (FObj x)
| Just i <- lookup x su = FVar i
tx t = t
sortVars :: Sort -> [Symbol]
sortVars = foldSort go []
where
go b (FObj x) = x : b
go b _ = b
data Def a
= Srt Sort
| Axm Expr
| Cst (SubC a)
| Wfc (WfC a)
| Con Symbol Sort
| Qul Qualifier
| Kut KVar
| IBind Int Symbol SortedReft
deriving (Show, Generic)
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 "qualif" >> qualifierP sortP)
<|> Kut <$> (reserved "cut" >> kvarP)
<|> 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
let [w] = wfC env r ()
return w
subCP :: Parser (SubC ())
subCP = do pos <- getPosition
reserved "env"
env <- envP
reserved "lhs"
lhs <- sortedReftP
reserved "rhs"
rhs <- sortedReftP
reserved "id"
i <- integer <* spaces
tag <- tagP
pos' <- getPosition
return $ subC' env lhs rhs i tag pos pos'
subC' env lhs rhs i tag l l'
= case cs of
[c] -> c
_ -> die $ err sp $ "RHS without single conjunct at" <+> pprint l'
where
cs = subC env lhs rhs (Just i) tag ()
sp = SS l l'
tagP :: Parser [Int]
tagP = reserved "tag" >> spaces >> brackets (sepBy intP semi)
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 lts kts qs mempty mempty False
where
cm = M.fromList [(cid c, c) | Cst c <- defs]
ws = M.fromList [(thd3 $ wrft w, w) | Wfc w <- defs]
bs = bindEnvFromList [(n, x, r) | IBind n x r <- defs]
lts = fromListSEnv [(x, t) | Con x t <- defs]
kts = KS $ S.fromList [k | Kut k <- defs]
qs = [q | Qul q <- defs]
cid = fromJust . sid
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 <- kvP
reserved ":="
ps <- brackets $ sepBy predSolP semi
return (k, simplify $ PAnd ps)
where
kvP = try kvarP <|> (KV <$> symbolP)
solutionP :: Parser (M.HashMap KVar Expr)
solutionP
= M.fromList <$> sepBy solution1P whiteSpace
solutionFileP
= (,) <$> 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) (dErr e)
Right (r, "", _) -> r
Right (_, r, l) -> die $ err (SS l l) (dRem r)
where
dErr e = vcat [ "parseError" <+> tshow e
, "when parsing from" <+> text f ]
dRem r = vcat [ "doParse has leftover"
, nest 4 (text r)
, "when parsing from" <+> text 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 Expr where
rr' = doParse' exprP
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