{-# LANGUAGE NoMonomorphismRestriction, FlexibleInstances, UndecidableInstances, TypeSynonymInstances, TupleSections #-} 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 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" --, "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 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 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 -- 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 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"] --------------------------------------------------------------------- -------------------------- 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 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) -}