liquid-fixpoint-0.2.3.2: src/Language/Fixpoint/Parse.hs
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Fixpoint.Parse (
-- * Top Level Class for Parseable Values
Inputable (..)
-- * Top Level Class for Parseable Values
, Parser
-- * Lexer to add new tokens
, lexer
-- * Some Important keyword and parsers
, reserved, reservedOp
, parens , brackets, angles, braces
, semi , comma
, colon , dcolon
, whiteSpace
, blanks
-- * Parsing basic entities
, fTyConP -- Type constructors
, lowerIdP -- Lower-case identifiers
, upperIdP -- Upper-case identifiers
, symbolP -- Arbitrary Symbols
, constantP -- (Integer) Constants
, integer -- Integer
, bindP -- Binder (lowerIdP <* colon)
-- * Parsing recursive entities
, exprP -- Expressions
, predP -- Refinement Predicates
, funAppP -- Function Applications
, qualifierP -- Qualifiers
, refP -- (Sorted) Refinements
, refDefP -- (Sorted) Refinements with default binder
, refBindP -- (Sorted) Refinements with configurable sub-parsers
-- * Some Combinators
, condIdP -- condIdP :: [Char] -> (Text -> Bool) -> Parser Text
-- * Add a Location to a parsed value
, locParserP
, locLowerIdP
, locUpperIdP
-- * Getting a Fresh Integer while parsing
, freshIntP
-- * Parsing Function
, doParse'
, parseFromFile
, remainderP
) where
import Control.Applicative ((<$>), (<*), (<*>))
import Control.Monad
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.Text (Text)
import qualified Data.Text as T
import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.Language
import Text.Parsec.Pos
import Text.Parsec.String hiding (Parser, parseFromFile)
import qualified Text.Parsec.Token as Token
import Text.Printf (printf)
import Data.Char (isLower, toUpper)
import Language.Fixpoint.Bitvector
import Language.Fixpoint.Errors
import Language.Fixpoint.Misc hiding (dcolon)
import Language.Fixpoint.SmtLib2
import Language.Fixpoint.Types
import Data.Maybe (fromJust, maybe)
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"
--, "is"
, "&&", "||"
, "~", "=>", "==>", "<=>"
, "->"
, ":="
, "&", "^", "<<", ">>", "--"
, "?", "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
-- integer = Token.integer lexer
-- identifier = Token.identifier lexer
blanks = many (satisfy (`elem` [' ', '\t']))
integer = posInteger
-- try (char '-' >> (negate <$> posInteger))
-- <|> posInteger
posInteger = toI <$> (many1 digit <* spaces)
where
toI :: String -> Integer
toI = read
----------------------------------------------------------------
------------------------- Expressions --------------------------
----------------------------------------------------------------
locParserP :: Parser a -> Parser (Located a)
locParserP p = liftM2 Loc getPosition p
-- FIXME: we (LH) rely on this parser being dumb and *not* consuming trailing
-- whitespace, in order to avoid some parsers spanning multiple lines..
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
-- <|> try (parens $ condP EIte exprP)
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
where
exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P blanks)
exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma)
exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi)
funSymbolP = locParserP symbolP
-- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))
litP = do reserved "lit"
l <- stringLiteral
s <- try (bvSortP "Size32" S32) <|> bvSortP "Size64" S64
return $ ECon $ L (T.pack l) (mkSort s)
where
bvSortP ss s = do parens (reserved "BitVec" >> parens (reserved ss >> reserved "obj"))
return s
-- ORIG exprP :: Parser Expr
-- ORIG exprP = expr2P <|> lexprP
--
-- ORIG lexprP :: Parser Expr
-- ORIG lexprP
-- ORIG = try (parens exprP)
-- ORIG <|> try (parens exprCastP)
-- ORIG <|> try (parens $ condP EIte exprP)
-- ORIG <|> try exprFunP
-- ORIG <|> try (liftM (EVar . stringSymbol) upperIdP)
-- ORIG <|> liftM expr symbolP
-- ORIG <|> liftM ECon constantP
-- ORIG <|> liftM ESym symconstP
-- ORIG <|> (reserved "_|_" >> return EBot)
-- ORIG
-- ORIG exprFunP = (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP
-- ORIG where
-- ORIG exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces)
-- ORIG exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma)
-- ORIG exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi)
-- ORIG funSymbolP = locParserP symbolP -- liftM stringSymbol lowerIdP
parenBrackets = parens . brackets
-- ORIG expr2P = buildExpressionParser bops lexprP
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]
]
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"]
---------------------------------------------------------------------
-------------------------- Predicates -------------------------------
---------------------------------------------------------------------
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 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
----------------------------------------------------------------------------------
------------------------------------ BareTypes -----------------------------------
----------------------------------------------------------------------------------
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)
---------------------------------------------------------------------
-- | Parsing Qualifiers ---------------------------------------------
---------------------------------------------------------------------
-- qualifierP = mkQual <$> upperIdP <*> parens $ sepBy1 sortBindP comma <*> predP
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
---------------------------------------------------------------------
-- | Parsing Constraints (.fq files) --------------------------------
---------------------------------------------------------------------
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)
---------------------------------------------------------------------
-- | Interacting with Fixpoint --------------------------------------
---------------------------------------------------------------------
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
---------------------------------------------------------------------
-- Standalone SMTLIB2 commands --------------------------------------
---------------------------------------------------------------------
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
---------------------------------------------------------------------
-- Bundling Parsers into a Typeclass --------------------------------
---------------------------------------------------------------------
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
{-
---------------------------------------------------------------
--------------------------- Testing ---------------------------
---------------------------------------------------------------
-- A few tricky predicates for parsing
-- myTest1 = "((((v >= 56320) && (v <= 57343)) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o ((i - o) - 1)))) && (((numchars a o (i - (o -1))) >= 0) && (((i - o) - 1) >= 0)))) && ((not (((v >= 56320) && (v <= 57343)))) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o (i - o)))) && ((numchars a o (i - o)) >= 0))))"
--
-- myTest2 = "len x = len y - 1"
-- myTest3 = "len x y z = len a b c - 1"
-- myTest4 = "len x y z = len a b (c - 1)"
-- myTest5 = "x >= -1"
-- myTest6 = "(bLength v) = if n > 0 then n else 0"
-- myTest7 = "(bLength v) = (if n > 0 then n else 0)"
-- myTest8 = "(bLength v) = (n > 0 ? n : 0)"
sa = "0"
sb = "x"
sc = "(x0 + y0 + z0) "
sd = "(x+ y * 1)"
se = "_|_ "
sf = "(1 + x + _|_)"
sg = "f(x,y,z)"
sh = "(f((x+1), (y * a * b - 1), _|_))"
si = "(2 + f((x+1), (y * a * b - 1), _|_))"
s0 = "true"
s1 = "false"
s2 = "v > 0"
s3 = "(0 < v && v < 100)"
s4 = "(x < v && v < y+10 && v < z)"
s6 = "[(v > 0)]"
s6' = "x"
s7' = "(x <=> y)"
s8' = "(x <=> a = b)"
s9' = "(x <=> (a <= b && b < c))"
s7 = "{ v: Int | [(v > 0)] }"
s8 = "x:{ v: Int | v > 0 } -> {v : Int | v >= x}"
s9 = "v = x+y"
s10 = "{v: Int | v = x + y}"
s11 = "x:{v:Int | true } -> {v:Int | true }"
s12 = "y : {v:Int | true } -> {v:Int | v = x }"
s13 = "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}"
s14 = "x:{v:a | true} -> y:{v:b | true } -> {v:a | (x < v && v < y) }"
s15 = "x:Int -> Bool"
s16 = "x:Int -> y:Int -> {v:Int | v = x + y}"
s17 = "a"
s18 = "x:a -> Bool"
s20 = "forall a . x:Int -> Bool"
s21 = "x:{v : GHC.Prim.Int# | true } -> {v : Int | true }"
r0 = (rr s0) :: Pred
r0' = (rr s0) :: [Refa]
r1 = (rr s1) :: [Refa]
e1, e2 :: Expr
e1 = rr "(k_1 + k_2)"
e2 = rr "k_1"
o1, o2, o3 :: FixResult Integer
o1 = rr "SAT "
o2 = rr "UNSAT [1, 2, 9,10]"
o3 = rr "UNSAT []"
-- sol1 = doParse solution1P "solution: k_5 := [0 <= VV_int]"
-- sol2 = doParse solution1P "solution: k_4 := [(0 <= VV_int)]"
b0, b1, b2, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13 :: BareType
b0 = rr "Int"
b1 = rr "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}"
b2 = rr "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x - y}"
b4 = rr "forall a . x : a -> Bool"
b5 = rr "Int -> Int -> Int"
b6 = rr "(Int -> Int) -> Int"
b7 = rr "({v: Int | v > 10} -> Int) -> Int"
b8 = rr "(x:Int -> {v: Int | v > x}) -> {v: Int | v > 10}"
b9 = rr "x:Int -> {v: Int | v > x} -> {v: Int | v > 10}"
b10 = rr "[Int]"
b11 = rr "x:[Int] -> {v: Int | v > 10}"
b12 = rr "[Int] -> String"
b13 = rr "x:(Int, [Bool]) -> [(String, String)]"
-- b3 :: BareType
-- b3 = rr "x:Int -> y:Int -> {v:Bool | ((v is True) <=> x = y)}"
m1 = ["len :: [a] -> Int", "len (Nil) = 0", "len (Cons x xs) = 1 + len(xs)"]
m2 = ["tog :: LL a -> Int", "tog (Nil) = 100", "tog (Cons y ys) = 200"]
me1, me2 :: Measure.Measure BareType Symbol
me1 = (rr $ intercalate "\n" m1)
me2 = (rr $ intercalate "\n" m2)
-}