From fb280d49a83005f69f9f0e5c1fdd95b049f84435 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 6 Aug 2024 14:26:47 -0700 Subject: [PATCH 1/3] pull out FP dependency in SMTParse --- src/Language/Fixpoint/Horn/SMTParse.hs | 258 ++++++++++++++----------- tests/horn/pos/mod00.smt2 | 3 +- 2 files changed, 150 insertions(+), 111 deletions(-) diff --git a/src/Language/Fixpoint/Horn/SMTParse.hs b/src/Language/Fixpoint/Horn/SMTParse.hs index 2d2b96487..561c01c2b 100644 --- a/src/Language/Fixpoint/Horn/SMTParse.hs +++ b/src/Language/Fixpoint/Horn/SMTParse.hs @@ -19,8 +19,46 @@ import Text.Megaparsec.Char (string, char) import qualified Data.HashMap.Strict as M import qualified Data.Text as T +type FParser = FP.Parser + +fReserved :: String -> FParser () +fReserved = FP.reserved +fReservedOp :: String -> FParser () +fReservedOp = FP.reservedOp +fParens :: FParser a -> FParser a +fParens = FP.parens +fStringLiteral :: FParser String +fStringLiteral = FP.stringLiteral +fSymbolP :: FParser F.Symbol +fSymbolP = FP.symbolP +fIntP :: FP.Parser Int +fIntP = FP.intP +fLocUpperIdP :: FP.Parser F.LocSymbol +fLocUpperIdP = FP.locUpperIdP +fLocSymbolP :: FP.Parser F.LocSymbol +fLocSymbolP = FP.locSymbolP +fAddNumTyCon :: F.Symbol -> FP.Parser () +fAddNumTyCon = FP.addNumTyCon +fSym :: String -> FP.Parser String +fSym = FP.sym +fUpperIdP :: FP.Parser F.Symbol +fUpperIdP = FP.upperIdP +fLowerIdP :: FP.Parser F.Symbol +fLowerIdP = FP.lowerIdP +ffTyConP :: FP.Parser F.FTycon +ffTyConP = FP.fTyConP + +fTrueP :: FP.Parser F.Expr +fTrueP = FP.trueP +fFalseP :: FP.Parser F.Expr +fFalseP = FP.falseP +fSymconstP :: FP.Parser F.SymConst +fSymconstP = FP.symconstP +fConstantP :: FP.Parser F.Constant +fConstantP = FP.constantP + ------------------------------------------------------------------------------- -hornP :: FP.Parser H.TagQuery +hornP :: FParser H.TagQuery ------------------------------------------------------------------------------- hornP = do hThings <- many hThingP @@ -58,62 +96,62 @@ data HThing a | HNum F.Symbol deriving (Functor) -hThingP :: FP.Parser (HThing H.Tag) -hThingP = FP.parens body +hThingP :: FParser (HThing H.Tag) +hThingP = fParens body where - body = HQual <$> (FP.reserved "qualif" *> hQualifierP) - <|> HCstr <$> (FP.reserved "constraint" *> hCstrP) - <|> HVar <$> (FP.reserved "var" *> hVarP) - <|> HOpt <$> (FP.reserved "fixpoint" *> FP.stringLiteral) - <|> HCon <$> (FP.reserved "constant" *> FP.symbolP) <*> sortP - <|> HDis <$> (FP.reserved "distinct" *> FP.symbolP) <*> sortP - <|> HDef <$> (FP.reserved "define" *> defineP) - <|> HMat <$> (FP.reserved "match" *> matchP) - <|> HDat <$> (FP.reserved "datatype" *> dataDeclP) - <|> HNum <$> (FP.reserved "numeric" *> numericDeclP) - -numericDeclP :: FP.Parser F.Symbol + body = HQual <$> (fReserved "qualif" *> hQualifierP) + <|> HCstr <$> (fReserved "constraint" *> hCstrP) + <|> HVar <$> (fReserved "var" *> hVarP) + <|> HOpt <$> (fReserved "fixpoint" *> fStringLiteral) + <|> HCon <$> (fReserved "constant" *> fSymbolP) <*> sortP + <|> HDis <$> (fReserved "distinct" *> fSymbolP) <*> sortP + <|> HDef <$> (fReserved "define" *> defineP) + <|> HMat <$> (fReserved "match" *> matchP) + <|> HDat <$> (fReserved "datatype" *> dataDeclP) + <|> HNum <$> (fReserved "numeric" *> numericDeclP) + +numericDeclP :: FParser F.Symbol numericDeclP = do - x <- F.val <$> FP.locUpperIdP - FP.addNumTyCon x + x <- F.val <$> fLocUpperIdP + fAddNumTyCon x pure x ------------------------------------------------------------------------------- -hCstrP :: FP.Parser (H.Cstr H.Tag) +hCstrP :: FParser (H.Cstr H.Tag) ------------------------------------------------------------------------------- -hCstrP = try (FP.parens body) +hCstrP = try (fParens body) <|> H.Head <$> hPredP <*> pure H.NoTag where - body = H.CAnd <$> (FP.reserved "and" *> many hCstrP) - <|> H.All <$> (FP.reserved "forall" *> hBindP) <*> hCstrP - <|> H.Any <$> (FP.reserved "exists" *> hBindP) <*> hCstrP - <|> H.Head <$> (FP.reserved "tag" *> hPredP) <*> (H.Tag <$> FP.stringLiteral) + body = H.CAnd <$> (fReserved "and" *> many hCstrP) + <|> H.All <$> (fReserved "forall" *> hBindP) <*> hCstrP + <|> H.Any <$> (fReserved "exists" *> hBindP) <*> hCstrP + <|> H.Head <$> (fReserved "tag" *> hPredP) <*> (H.Tag <$> fStringLiteral) -hBindP :: FP.Parser (H.Bind H.Tag) -hBindP = FP.parens $ do +hBindP :: FParser (H.Bind H.Tag) +hBindP = fParens $ do (x, t) <- symSortP H.Bind x t <$> hPredP <*> pure H.NoTag ------------------------------------------------------------------------------- -hPredP :: FP.Parser H.Pred +hPredP :: FParser H.Pred ------------------------------------------------------------------------------- -hPredP = FP.parens body +hPredP = fParens body where - body = H.Var <$> kvSymP <*> some FP.symbolP - <|> H.PAnd <$> (FP.reserved "and" *> some hPredP) + body = H.Var <$> kvSymP <*> some fSymbolP + <|> H.PAnd <$> (fReserved "and" *> some hPredP) <|> H.Reft <$> exprP -kvSymP :: FP.Parser F.Symbol -kvSymP = char '$' *> FP.symbolP +kvSymP :: FParser F.Symbol +kvSymP = char '$' *> fSymbolP ------------------------------------------------------------------------------- -- | Qualifiers ------------------------------------------------------------------------------- -hQualifierP :: FP.Parser F.Qualifier +hQualifierP :: FParser F.Qualifier hQualifierP = do pos <- getSourcePos - n <- FP.upperIdP - params <- FP.parens (some symSortP) + n <- fUpperIdP + params <- fParens (some symSortP) body <- exprP return $ F.mkQual n (mkParam <$> params) body pos @@ -124,66 +162,66 @@ mkParam (x, t) = F.QP x F.PatNone t -- | Horn Variables ------------------------------------------------------------------------------- -hVarP :: FP.Parser (H.Var H.Tag) -hVarP = H.HVar <$> kvSymP <*> FP.parens (some sortP) <*> pure H.NoTag +hVarP :: FParser (H.Var H.Tag) +hVarP = H.HVar <$> kvSymP <*> fParens (some sortP) <*> pure H.NoTag ------------------------------------------------------------------------------- -- | Helpers ------------------------------------------------------------------------------- -sPairP :: FP.Parser a -> FP.Parser b -> FP.Parser (a, b) -sPairP aP bP = FP.parens ((,) <$> aP <*> bP) +sPairP :: FParser a -> FParser b -> FParser (a, b) +sPairP aP bP = fParens ((,) <$> aP <*> bP) -sMany :: FP.Parser a -> FP.Parser [a] -sMany p = FP.parens (many p) +sMany :: FParser a -> FParser [a] +sMany p = fParens (many p) -symSortP :: FP.Parser (F.Symbol, F.Sort) -symSortP = sPairP FP.symbolP sortP --- symSortP = FP.parens ((,) <$> FP.symbolP <*> sortP) +symSortP :: FParser (F.Symbol, F.Sort) +symSortP = sPairP fSymbolP sortP +-- symSortP = fParens ((,) <$> fSymbolP <*> sortP) -dataDeclP :: FP.Parser F.DataDecl +dataDeclP :: FParser F.DataDecl dataDeclP = do - (tc, n) <- sPairP FP.fTyConP FP.intP + (tc, n) <- sPairP ffTyConP fIntP ctors <- sMany dataCtorP pure $ F.DDecl tc n ctors -dataCtorP :: FP.Parser F.DataCtor -dataCtorP = FP.parens (F.DCtor <$> FP.locSymbolP <*> sMany dataFieldP) +dataCtorP :: FParser F.DataCtor +dataCtorP = fParens (F.DCtor <$> fLocSymbolP <*> sMany dataFieldP) -dataFieldP :: FP.Parser F.DataField -dataFieldP = uncurry F.DField <$> sPairP FP.locSymbolP sortP +dataFieldP :: FParser F.DataField +dataFieldP = uncurry F.DField <$> sPairP fLocSymbolP sortP -bindsP :: FP.Parser [(F.Symbol, F.Sort)] +bindsP :: FParser [(F.Symbol, F.Sort)] bindsP = sMany bindP -bindP :: FP.Parser (F.Symbol, F.Sort) -bindP = sPairP FP.symbolP sortP +bindP :: FParser (F.Symbol, F.Sort) +bindP = sPairP fSymbolP sortP -defineP :: FP.Parser F.Equation +defineP :: FParser F.Equation defineP = do - name <- FP.symbolP + name <- fSymbolP xts <- bindsP s <- sortP body <- exprP return $ F.mkEquation name xts body s -matchP :: FP.Parser F.Rewrite +matchP :: FParser F.Rewrite matchP = do - f <- FP.symbolP - d:xs <- FP.parens (some FP.symbolP) + f <- fSymbolP + d:xs <- fParens (some fSymbolP) F.SMeasure f d xs <$> exprP -sortP :: FP.Parser F.Sort -sortP = (string "@" >> (F.FVar <$> FP.parens FP.intP)) - <|> (FP.reserved "Int" >> return F.FInt) - <|> (FP.reserved "Real" >> return F.FReal) - <|> (FP.reserved "Frac" >> return F.FFrac) - <|> (FP.reserved "num" >> return F.FNum) - <|> (F.fAppTC <$> FP.fTyConP <*> pure []) - <|> (F.FObj . F.symbol <$> FP.lowerIdP) - <|> try (FP.parens (FP.reserved "func" >> (mkFunc <$> FP.intP <*> sMany sortP <*> sortP))) - <|> try (FP.parens (FP.reserved "list" >> (mkList <$> sortP))) - <|> FP.parens (F.fAppTC <$> FP.fTyConP <*> many sortP) +sortP :: FParser F.Sort +sortP = (string "@" >> (F.FVar <$> fParens fIntP)) + <|> (fReserved "Int" >> return F.FInt) + <|> (fReserved "Real" >> return F.FReal) + <|> (fReserved "Frac" >> return F.FFrac) + <|> (fReserved "num" >> return F.FNum) + <|> (F.fAppTC <$> ffTyConP <*> pure []) + <|> (F.FObj . F.symbol <$> fLowerIdP) + <|> try (fParens (fReserved "func" >> (mkFunc <$> fIntP <*> sMany sortP <*> sortP))) + <|> try (fParens (fReserved "list" >> (mkList <$> sortP))) + <|> fParens (F.fAppTC <$> ffTyConP <*> many sortP) mkFunc :: Int -> [F.Sort] -> F.Sort -> F.Sort mkFunc n ss s = F.mkFFunc n (ss ++ [s]) @@ -191,34 +229,34 @@ mkFunc n ss s = F.mkFFunc n (ss ++ [s]) mkList :: F.Sort -> F.Sort mkList s = F.fAppTC F.listFTyCon [s] -exprP :: FP.Parser F.Expr +exprP :: FParser F.Expr exprP - = FP.trueP - <|> FP.falseP - <|> (F.ESym <$> FP.symconstP) - <|> (F.ECon <$> FP.constantP) - <|> (F.EVar <$> FP.symbolP) - <|> FP.parens pExprP - -pExprP :: FP.Parser F.Expr + = fTrueP + <|> fFalseP + <|> (F.ESym <$> fSymconstP) + <|> (F.ECon <$> fConstantP) + <|> (F.EVar <$> fSymbolP) + <|> fParens pExprP + +pExprP :: FParser F.Expr pExprP - = (FP.reserved "if" >> (F.EIte <$> exprP <*> exprP <*> exprP)) - <|> (FP.reserved "lit" >> (mkLit <$> FP.stringLiteral <*> sortP)) - <|> (FP.reserved "cast" >> (F.ECst <$> exprP <*> sortP)) - <|> (FP.reserved "not" >> (F.PNot <$> exprP)) - <|> (FP.reservedOp "=>" >> (F.PImp <$> exprP <*> exprP)) - <|> (FP.reservedOp "<=>" >> (F.PIff <$> exprP <*> exprP)) - <|> (FP.reserved "and" >> (F.PAnd <$> many exprP)) - <|> (FP.reserved "or" >> (F.POr <$> many exprP)) - <|> (FP.reserved "forall" >> (F.PAll <$> bindsP <*> exprP)) - <|> (FP.reserved "exists" >> (F.PExist <$> bindsP <*> exprP)) - <|> (FP.reserved "lam" >> (F.ELam <$> bindP <*> exprP)) - <|> (FP.reserved "coerce" >> (F.ECoerc <$> sortP <*> sortP <*> exprP)) - <|> (FP.reserved "ETApp" >> (F.ETApp <$> exprP <*> sortP)) - <|> (FP.reserved "ETAbs" >> (F.ETAbs <$> exprP <*> FP.symbolP)) + = (fReserved "if" >> (F.EIte <$> exprP <*> exprP <*> exprP)) + <|> (fReserved "lit" >> (mkLit <$> fStringLiteral <*> sortP)) + <|> (fReserved "cast" >> (F.ECst <$> exprP <*> sortP)) + <|> (fReserved "not" >> (F.PNot <$> exprP)) + <|> (fReservedOp "=>" >> (F.PImp <$> exprP <*> exprP)) + <|> (fReservedOp "<=>" >> (F.PIff <$> exprP <*> exprP)) + <|> (fReserved "and" >> (F.PAnd <$> many exprP)) + <|> (fReserved "or" >> (F.POr <$> many exprP)) + <|> (fReserved "forall" >> (F.PAll <$> bindsP <*> exprP)) + <|> (fReserved "exists" >> (F.PExist <$> bindsP <*> exprP)) + <|> (fReserved "lam" >> (F.ELam <$> bindP <*> exprP)) + <|> (fReserved "coerce" >> (F.ECoerc <$> sortP <*> sortP <*> exprP)) + <|> (fReserved "ETApp" >> (F.ETApp <$> exprP <*> sortP)) + <|> (fReserved "ETAbs" >> (F.ETAbs <$> exprP <*> fSymbolP)) <|> try (F.EBin <$> bopP <*> exprP <*> exprP) <|> try (F.PAtom <$> brelP <*> exprP <*> exprP) - <|> try (FP.sym "-" >> (F.ENeg <$> exprP)) + <|> try (fSym "-" >> (F.ENeg <$> exprP)) <|> (mkApp <$> some exprP) mkLit :: String -> F.Sort -> F.Expr @@ -228,23 +266,23 @@ mkApp :: [F.Expr] -> F.Expr mkApp (e:es) = F.eApps e es mkApp _ = error "impossible" -bopP :: FP.Parser F.Bop +bopP :: FParser F.Bop bopP - = (FP.sym "+" >> return F.Plus) - <|> (FP.sym "-" >> return F.Minus) - <|> (FP.sym "*" >> return F.Times) - <|> (FP.sym "/" >> return F.Div) - <|> (FP.sym "mod" >> return F.Mod) - <|> (FP.sym "*." >> return F.RTimes) - <|> (FP.sym "/." >> return F.RDiv) - -brelP :: FP.Parser F.Brel + = (fSym "+" >> return F.Plus) + <|> (fSym "-" >> return F.Minus) + <|> (fSym "*" >> return F.Times) + <|> (fSym "/" >> return F.Div) + <|> (fSym "mod" >> return F.Mod) + <|> (fSym "*." >> return F.RTimes) + <|> (fSym "/." >> return F.RDiv) + +brelP :: FParser F.Brel brelP - = (FP.sym "=" >> return F.Eq) - <|> (FP.sym "!=" >> return F.Ne) - <|> (FP.sym "~~" >> return F.Ueq) - <|> (FP.sym "!~" >> return F.Une) - <|> (FP.sym ">=" >> return F.Ge) - <|> (FP.sym ">" >> return F.Gt) - <|> (FP.sym "<=" >> return F.Le) - <|> (FP.sym "<" >> return F.Lt) \ No newline at end of file + = (fSym "=" >> return F.Eq) + <|> (fSym "!=" >> return F.Ne) + <|> (fSym "~~" >> return F.Ueq) + <|> (fSym "!~" >> return F.Une) + <|> (fSym ">=" >> return F.Ge) + <|> (fSym ">" >> return F.Gt) + <|> (fSym "<=" >> return F.Le) + <|> (fSym "<" >> return F.Lt) \ No newline at end of file diff --git a/tests/horn/pos/mod00.smt2 b/tests/horn/pos/mod00.smt2 index a808974e8..87a1ee522 100644 --- a/tests/horn/pos/mod00.smt2 +++ b/tests/horn/pos/mod00.smt2 @@ -1,7 +1,8 @@ (var $k0 (int)) + (constraint - (and + (and // this is a random comment (and (forall ((a0 int) ((= a0 4))) ($k0 a0) From 374e0053e1ce883b486a5cb712c0ff9183a9c29e Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 6 Aug 2024 15:15:03 -0700 Subject: [PATCH 2/3] use ; for comments in SMTParser (as in SMTLIB) --- src/Language/Fixpoint/Horn/SMTParse.hs | 277 +++++++++++++++---------- src/Language/Fixpoint/Parse.hs | 54 +++-- tests/horn/pos/mod00.smt2 | 8 +- 3 files changed, 212 insertions(+), 127 deletions(-) diff --git a/src/Language/Fixpoint/Horn/SMTParse.hs b/src/Language/Fixpoint/Horn/SMTParse.hs index 561c01c2b..acc4cad2a 100644 --- a/src/Language/Fixpoint/Horn/SMTParse.hs +++ b/src/Language/Fixpoint/Horn/SMTParse.hs @@ -11,51 +11,110 @@ module Language.Fixpoint.Horn.SMTParse ( , sortP ) where -import qualified Language.Fixpoint.Parse as FP +import qualified Language.Fixpoint.Parse as FP (Parser, addNumTyCon, lexeme', locLexeme', reserved', reservedOp', symbolR, upperIdR, lowerIdR, stringR, naturalR, mkFTycon) import qualified Language.Fixpoint.Types as F import qualified Language.Fixpoint.Horn.Types as H import Text.Megaparsec hiding (State) -import Text.Megaparsec.Char (string, char) +import Text.Megaparsec.Char (space1, string, char) import qualified Data.HashMap.Strict as M import qualified Data.Text as T +import qualified Text.Megaparsec.Char.Lexer as L type FParser = FP.Parser -fReserved :: String -> FParser () -fReserved = FP.reserved -fReservedOp :: String -> FParser () -fReservedOp = FP.reservedOp -fParens :: FParser a -> FParser a -fParens = FP.parens -fStringLiteral :: FParser String -fStringLiteral = FP.stringLiteral -fSymbolP :: FParser F.Symbol -fSymbolP = FP.symbolP -fIntP :: FP.Parser Int -fIntP = FP.intP -fLocUpperIdP :: FP.Parser F.LocSymbol -fLocUpperIdP = FP.locUpperIdP -fLocSymbolP :: FP.Parser F.LocSymbol -fLocSymbolP = FP.locSymbolP fAddNumTyCon :: F.Symbol -> FP.Parser () fAddNumTyCon = FP.addNumTyCon -fSym :: String -> FP.Parser String -fSym = FP.sym -fUpperIdP :: FP.Parser F.Symbol -fUpperIdP = FP.upperIdP -fLowerIdP :: FP.Parser F.Symbol -fLowerIdP = FP.lowerIdP -ffTyConP :: FP.Parser F.FTycon -ffTyConP = FP.fTyConP + +lexeme :: FParser a -> FParser a +lexeme = FP.lexeme' spaces + +locLexeme :: FP.Parser a -> FP.Parser (F.Located a) +locLexeme = FP.locLexeme' spaces + +-- | Consumes all whitespace, including LH comments. +-- +-- Should not be used directly, but primarily via 'lexeme'. +-- +-- The only "valid" use case for spaces is in top-level parsing +-- function, to consume initial spaces. +-- +spaces :: FParser () +spaces = + L.space + space1 + lineComment + blockComment + +lineComment :: FParser () +lineComment = L.skipLineComment "; " + +blockComment :: FParser () +blockComment = L.skipBlockComment "/* " "*/" + +reserved :: String -> FParser () +reserved = FP.reserved' spaces + +reservedOp :: String -> FParser () +reservedOp = FP.reservedOp' spaces + +sym :: String -> FParser String +sym x = lexeme (string x) + +parens :: FParser a -> FParser a +parens = between (sym "(") (sym ")") + +stringLiteral :: FParser String +stringLiteral = lexeme FP.stringR "string literal" + +symbolP :: FParser F.Symbol +symbolP = lexeme FP.symbolR "identifier" + +fIntP :: FParser Int +fIntP = fromInteger <$> natural + +natural :: FParser Integer +natural = lexeme FP.naturalR "nat literal" + +double :: FParser Double +double = lexeme L.float "float literal" + + +locUpperIdP, locSymbolP :: FParser F.LocSymbol +locUpperIdP = locLexeme FP.upperIdR +locSymbolP = locLexeme FP.symbolR + +upperIdP :: FP.Parser F.Symbol +upperIdP = lexeme FP.upperIdR "upperIdP" + +lowerIdP :: FP.Parser F.Symbol +lowerIdP = lexeme FP.lowerIdR "upperIdP" + +fTyConP :: FParser F.FTycon +fTyConP + = (reserved "int" >> return F.intFTyCon) + <|> (reserved "Integer" >> return F.intFTyCon) + <|> (reserved "Int" >> return F.intFTyCon) + <|> (reserved "real" >> return F.realFTyCon) + <|> (reserved "bool" >> return F.boolFTyCon) + <|> (reserved "num" >> return F.numFTyCon) + <|> (reserved "Str" >> return F.strFTyCon) + <|> (FP.mkFTycon =<< locUpperIdP) + fTrueP :: FP.Parser F.Expr -fTrueP = FP.trueP +fTrueP = reserved "true" >> return F.PTrue + fFalseP :: FP.Parser F.Expr -fFalseP = FP.falseP +fFalseP = reserved "false" >> return F.PFalse + fSymconstP :: FP.Parser F.SymConst -fSymconstP = FP.symconstP -fConstantP :: FP.Parser F.Constant -fConstantP = FP.constantP +fSymconstP = F.SL . T.pack <$> stringLiteral + +-- | Parser for literal numeric constants: floats or integers without sign. +constantP :: FParser F.Constant +constantP = + try (F.R <$> double) -- float literal + <|> F.I <$> natural -- nat literal ------------------------------------------------------------------------------- hornP :: FParser H.TagQuery @@ -97,52 +156,52 @@ data HThing a deriving (Functor) hThingP :: FParser (HThing H.Tag) -hThingP = fParens body +hThingP = parens body where - body = HQual <$> (fReserved "qualif" *> hQualifierP) - <|> HCstr <$> (fReserved "constraint" *> hCstrP) - <|> HVar <$> (fReserved "var" *> hVarP) - <|> HOpt <$> (fReserved "fixpoint" *> fStringLiteral) - <|> HCon <$> (fReserved "constant" *> fSymbolP) <*> sortP - <|> HDis <$> (fReserved "distinct" *> fSymbolP) <*> sortP - <|> HDef <$> (fReserved "define" *> defineP) - <|> HMat <$> (fReserved "match" *> matchP) - <|> HDat <$> (fReserved "datatype" *> dataDeclP) - <|> HNum <$> (fReserved "numeric" *> numericDeclP) + body = HQual <$> (reserved "qualif" *> hQualifierP) + <|> HCstr <$> (reserved "constraint" *> hCstrP) + <|> HVar <$> (reserved "var" *> hVarP) + <|> HOpt <$> (reserved "fixpoint" *> stringLiteral) + <|> HCon <$> (reserved "constant" *> symbolP) <*> sortP + <|> HDis <$> (reserved "distinct" *> symbolP) <*> sortP + <|> HDef <$> (reserved "define" *> defineP) + <|> HMat <$> (reserved "match" *> matchP) + <|> HDat <$> (reserved "datatype" *> dataDeclP) + <|> HNum <$> (reserved "numeric" *> numericDeclP) numericDeclP :: FParser F.Symbol numericDeclP = do - x <- F.val <$> fLocUpperIdP + x <- F.val <$> locUpperIdP fAddNumTyCon x pure x ------------------------------------------------------------------------------- hCstrP :: FParser (H.Cstr H.Tag) ------------------------------------------------------------------------------- -hCstrP = try (fParens body) +hCstrP = try (parens body) <|> H.Head <$> hPredP <*> pure H.NoTag where - body = H.CAnd <$> (fReserved "and" *> many hCstrP) - <|> H.All <$> (fReserved "forall" *> hBindP) <*> hCstrP - <|> H.Any <$> (fReserved "exists" *> hBindP) <*> hCstrP - <|> H.Head <$> (fReserved "tag" *> hPredP) <*> (H.Tag <$> fStringLiteral) + body = H.CAnd <$> (reserved "and" *> many hCstrP) + <|> H.All <$> (reserved "forall" *> hBindP) <*> hCstrP + <|> H.Any <$> (reserved "exists" *> hBindP) <*> hCstrP + <|> H.Head <$> (reserved "tag" *> hPredP) <*> (H.Tag <$> stringLiteral) hBindP :: FParser (H.Bind H.Tag) -hBindP = fParens $ do +hBindP = parens $ do (x, t) <- symSortP H.Bind x t <$> hPredP <*> pure H.NoTag ------------------------------------------------------------------------------- hPredP :: FParser H.Pred ------------------------------------------------------------------------------- -hPredP = fParens body +hPredP = parens body where - body = H.Var <$> kvSymP <*> some fSymbolP - <|> H.PAnd <$> (fReserved "and" *> some hPredP) + body = H.Var <$> kvSymP <*> some symbolP + <|> H.PAnd <$> (reserved "and" *> some hPredP) <|> H.Reft <$> exprP kvSymP :: FParser F.Symbol -kvSymP = char '$' *> fSymbolP +kvSymP = char '$' *> symbolP ------------------------------------------------------------------------------- -- | Qualifiers @@ -150,8 +209,8 @@ kvSymP = char '$' *> fSymbolP hQualifierP :: FParser F.Qualifier hQualifierP = do pos <- getSourcePos - n <- fUpperIdP - params <- fParens (some symSortP) + n <- upperIdP + params <- parens (some symSortP) body <- exprP return $ F.mkQual n (mkParam <$> params) body pos @@ -163,43 +222,43 @@ mkParam (x, t) = F.QP x F.PatNone t ------------------------------------------------------------------------------- hVarP :: FParser (H.Var H.Tag) -hVarP = H.HVar <$> kvSymP <*> fParens (some sortP) <*> pure H.NoTag +hVarP = H.HVar <$> kvSymP <*> parens (some sortP) <*> pure H.NoTag ------------------------------------------------------------------------------- -- | Helpers ------------------------------------------------------------------------------- sPairP :: FParser a -> FParser b -> FParser (a, b) -sPairP aP bP = fParens ((,) <$> aP <*> bP) +sPairP aP bP = parens ((,) <$> aP <*> bP) sMany :: FParser a -> FParser [a] -sMany p = fParens (many p) +sMany p = parens (many p) symSortP :: FParser (F.Symbol, F.Sort) -symSortP = sPairP fSymbolP sortP +symSortP = sPairP symbolP sortP -- symSortP = fParens ((,) <$> fSymbolP <*> sortP) dataDeclP :: FParser F.DataDecl dataDeclP = do - (tc, n) <- sPairP ffTyConP fIntP + (tc, n) <- sPairP fTyConP fIntP ctors <- sMany dataCtorP pure $ F.DDecl tc n ctors dataCtorP :: FParser F.DataCtor -dataCtorP = fParens (F.DCtor <$> fLocSymbolP <*> sMany dataFieldP) +dataCtorP = parens (F.DCtor <$> locSymbolP <*> sMany dataFieldP) dataFieldP :: FParser F.DataField -dataFieldP = uncurry F.DField <$> sPairP fLocSymbolP sortP +dataFieldP = uncurry F.DField <$> sPairP locSymbolP sortP bindsP :: FParser [(F.Symbol, F.Sort)] bindsP = sMany bindP bindP :: FParser (F.Symbol, F.Sort) -bindP = sPairP fSymbolP sortP +bindP = sPairP symbolP sortP defineP :: FParser F.Equation defineP = do - name <- fSymbolP + name <- symbolP xts <- bindsP s <- sortP body <- exprP @@ -207,21 +266,21 @@ defineP = do matchP :: FParser F.Rewrite matchP = do - f <- fSymbolP - d:xs <- fParens (some fSymbolP) + f <- symbolP + d:xs <- parens (some symbolP) F.SMeasure f d xs <$> exprP sortP :: FParser F.Sort -sortP = (string "@" >> (F.FVar <$> fParens fIntP)) - <|> (fReserved "Int" >> return F.FInt) - <|> (fReserved "Real" >> return F.FReal) - <|> (fReserved "Frac" >> return F.FFrac) - <|> (fReserved "num" >> return F.FNum) - <|> (F.fAppTC <$> ffTyConP <*> pure []) - <|> (F.FObj . F.symbol <$> fLowerIdP) - <|> try (fParens (fReserved "func" >> (mkFunc <$> fIntP <*> sMany sortP <*> sortP))) - <|> try (fParens (fReserved "list" >> (mkList <$> sortP))) - <|> fParens (F.fAppTC <$> ffTyConP <*> many sortP) +sortP = (string "@" >> (F.FVar <$> parens fIntP)) + <|> (reserved "Int" >> return F.FInt) + <|> (reserved "Real" >> return F.FReal) + <|> (reserved "Frac" >> return F.FFrac) + <|> (reserved "num" >> return F.FNum) + <|> (F.fAppTC <$> fTyConP <*> pure []) + <|> (F.FObj . F.symbol <$> lowerIdP) + <|> try (parens (reserved "func" >> (mkFunc <$> fIntP <*> sMany sortP <*> sortP))) + <|> try (parens (reserved "list" >> (mkList <$> sortP))) + <|> parens (F.fAppTC <$> fTyConP <*> many sortP) mkFunc :: Int -> [F.Sort] -> F.Sort -> F.Sort mkFunc n ss s = F.mkFFunc n (ss ++ [s]) @@ -234,29 +293,29 @@ exprP = fTrueP <|> fFalseP <|> (F.ESym <$> fSymconstP) - <|> (F.ECon <$> fConstantP) - <|> (F.EVar <$> fSymbolP) - <|> fParens pExprP + <|> (F.ECon <$> constantP) + <|> (F.EVar <$> symbolP) + <|> parens pExprP pExprP :: FParser F.Expr pExprP - = (fReserved "if" >> (F.EIte <$> exprP <*> exprP <*> exprP)) - <|> (fReserved "lit" >> (mkLit <$> fStringLiteral <*> sortP)) - <|> (fReserved "cast" >> (F.ECst <$> exprP <*> sortP)) - <|> (fReserved "not" >> (F.PNot <$> exprP)) - <|> (fReservedOp "=>" >> (F.PImp <$> exprP <*> exprP)) - <|> (fReservedOp "<=>" >> (F.PIff <$> exprP <*> exprP)) - <|> (fReserved "and" >> (F.PAnd <$> many exprP)) - <|> (fReserved "or" >> (F.POr <$> many exprP)) - <|> (fReserved "forall" >> (F.PAll <$> bindsP <*> exprP)) - <|> (fReserved "exists" >> (F.PExist <$> bindsP <*> exprP)) - <|> (fReserved "lam" >> (F.ELam <$> bindP <*> exprP)) - <|> (fReserved "coerce" >> (F.ECoerc <$> sortP <*> sortP <*> exprP)) - <|> (fReserved "ETApp" >> (F.ETApp <$> exprP <*> sortP)) - <|> (fReserved "ETAbs" >> (F.ETAbs <$> exprP <*> fSymbolP)) + = (reserved "if" >> (F.EIte <$> exprP <*> exprP <*> exprP)) + <|> (reserved "lit" >> (mkLit <$> stringLiteral <*> sortP)) + <|> (reserved "cast" >> (F.ECst <$> exprP <*> sortP)) + <|> (reserved "not" >> (F.PNot <$> exprP)) + <|> (reservedOp "=>" >> (F.PImp <$> exprP <*> exprP)) + <|> (reservedOp "<=>" >> (F.PIff <$> exprP <*> exprP)) + <|> (reserved "and" >> (F.PAnd <$> many exprP)) + <|> (reserved "or" >> (F.POr <$> many exprP)) + <|> (reserved "forall" >> (F.PAll <$> bindsP <*> exprP)) + <|> (reserved "exists" >> (F.PExist <$> bindsP <*> exprP)) + <|> (reserved "lam" >> (F.ELam <$> bindP <*> exprP)) + <|> (reserved "coerce" >> (F.ECoerc <$> sortP <*> sortP <*> exprP)) + <|> (reserved "ETApp" >> (F.ETApp <$> exprP <*> sortP)) + <|> (reserved "ETAbs" >> (F.ETAbs <$> exprP <*> symbolP)) <|> try (F.EBin <$> bopP <*> exprP <*> exprP) <|> try (F.PAtom <$> brelP <*> exprP <*> exprP) - <|> try (fSym "-" >> (F.ENeg <$> exprP)) + <|> try (sym "-" >> (F.ENeg <$> exprP)) <|> (mkApp <$> some exprP) mkLit :: String -> F.Sort -> F.Expr @@ -268,21 +327,21 @@ mkApp _ = error "impossible" bopP :: FParser F.Bop bopP - = (fSym "+" >> return F.Plus) - <|> (fSym "-" >> return F.Minus) - <|> (fSym "*" >> return F.Times) - <|> (fSym "/" >> return F.Div) - <|> (fSym "mod" >> return F.Mod) - <|> (fSym "*." >> return F.RTimes) - <|> (fSym "/." >> return F.RDiv) + = (sym "+" >> return F.Plus) + <|> (sym "-" >> return F.Minus) + <|> (sym "*" >> return F.Times) + <|> (sym "/" >> return F.Div) + <|> (sym "mod" >> return F.Mod) + <|> (sym "*." >> return F.RTimes) + <|> (sym "/." >> return F.RDiv) brelP :: FParser F.Brel brelP - = (fSym "=" >> return F.Eq) - <|> (fSym "!=" >> return F.Ne) - <|> (fSym "~~" >> return F.Ueq) - <|> (fSym "!~" >> return F.Une) - <|> (fSym ">=" >> return F.Ge) - <|> (fSym ">" >> return F.Gt) - <|> (fSym "<=" >> return F.Le) - <|> (fSym "<" >> return F.Lt) \ No newline at end of file + = (sym "=" >> return F.Eq) + <|> (sym "!=" >> return F.Ne) + <|> (sym "~~" >> return F.Ueq) + <|> (sym "!~" >> return F.Une) + <|> (sym ">=" >> return F.Ge) + <|> (sym ">" >> return F.Gt) + <|> (sym "<=" >> return F.Le) + <|> (sym "<" >> return F.Lt) \ No newline at end of file diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs index be72c67e6..20cca23d6 100644 --- a/src/Language/Fixpoint/Parse.hs +++ b/src/Language/Fixpoint/Parse.hs @@ -15,6 +15,7 @@ module Language.Fixpoint.Parse ( -- * Some Important keyword and parsers , reserved, reservedOp + , reserved', reservedOp' , locReserved , parens , brackets, angles, braces , semi , comma @@ -22,19 +23,23 @@ module Language.Fixpoint.Parse ( , dot , pairP , stringLiteral + , stringR , locStringLiteral , sym -- * Parsing basic entities -- fTyConP -- Type constructors - , lowerIdP -- Lower-case identifiers - , upperIdP -- Upper-case identifiers - -- , infixIdP -- String Haskell infix Id - , symbolP -- Arbitrary Symbols + , lowerIdP + , lowerIdR -- Lower-case identifiers + , upperIdP + , upperIdR -- Upper-case identifiers + , symbolP + , symbolR -- Arbitrary Symbols , locSymbolP , constantP -- (Integer) Constants - , natural -- Non-negative integer + , natural + , naturalR -- Non-negative integer , locNatural , bindP -- Binder (lowerIdP <* colon) , sortP -- Sort @@ -69,8 +74,10 @@ module Language.Fixpoint.Parse ( , condIdR -- * Lexemes and lexemes with location + , lexeme' , lexeme , located + , locLexeme' , locLexeme , locLowerIdP , locUpperIdP @@ -100,6 +107,7 @@ module Language.Fixpoint.Parse ( , dataCtorP , dataDeclP , fTyConP + , mkFTycon , intP , tvarP , trueP, falseP, symconstP @@ -324,10 +332,13 @@ strictGuardLayout = do -- whether we are in a position permitted by the layout stack. -- After the token, consume whitespace and potentially change state. -- -lexeme :: Parser a -> Parser a -lexeme p = do +lexeme' :: Parser () -> Parser a -> Parser a +lexeme' spacesP p = do after <- guardLayout - p <* spaces <* after + p <* spacesP <* after + +lexeme :: Parser a -> Parser a +lexeme = lexeme' spaces -- | Indentation-aware located lexeme parser. -- @@ -335,15 +346,18 @@ lexeme p = do -- covered by the identifier. I.e., it consumes additional whitespace in the -- end, but that is not part of the source range reported for the identifier. -- -locLexeme :: Parser a -> Parser (Located a) -locLexeme p = do +locLexeme' :: Parser () -> Parser a -> Parser (Located a) +locLexeme' spacesP p = do after <- guardLayout l1 <- getSourcePos x <- p l2 <- getSourcePos - spaces <* after + spacesP <* after pure (Loc l1 l2 x) +locLexeme :: Parser a -> Parser (Located a) +locLexeme = locLexeme' spaces + -- | Make a parser location-aware. -- -- This is at the cost of an imprecise span because we still @@ -558,6 +572,11 @@ reserved :: String -> Parser () reserved x = void $ lexeme (try (string x <* notFollowedBy identLetter)) +reserved' :: Parser () -> String -> Parser () +reserved' spacesP x = + void $ lexeme' spacesP (try (string x <* notFollowedBy identLetter)) + + locReserved :: String -> Parser (Located String) locReserved x = locLexeme (try (string x <* notFollowedBy identLetter)) @@ -573,6 +592,11 @@ reservedOp :: String -> Parser () reservedOp x = void $ lexeme (try (string x <* notFollowedBy opLetter)) +reservedOp' :: Parser () -> String -> Parser () +reservedOp' spacesP x = + void $ lexeme' spacesP (try (string x <* notFollowedBy opLetter)) + + -- | Parser that consumes the given symbol. -- -- The difference with 'reservedOp' is that the given symbol is seen @@ -866,19 +890,19 @@ addNumTyCon tc = modify $ \s -> s{ numTyCons = S.insert tc (numTyCons s) } infixSymbolP :: Parser Symbol infixSymbolP = do ops <- gets infixOps - choice (reserved' <$> ops) + choice (resX <$> ops) where infixOps st = [s | FInfix _ s _ _ <- fixityOps st] - reserved' x = reserved x >> return (symbol x) + resX x = reserved x >> return (symbol x) -- | Located version of 'infixSymbolP'. locInfixSymbolP :: Parser (Located Symbol) locInfixSymbolP = do ops <- gets infixOps - choice (reserved' <$> ops) + choice (resX <$> ops) where infixOps st = [s | FInfix _ s _ _ <- fixityOps st] - reserved' x = locReserved x >>= \ (Loc l1 l2 _) -> return (Loc l1 l2 (symbol x)) + resX x = locReserved x >>= \ (Loc l1 l2 _) -> return (Loc l1 l2 (symbol x)) -- | Helper function that turns an associativity into the right constructor for 'Operator'. mkInfix :: Assoc -> parser (expr -> expr -> expr) -> Operator parser expr diff --git a/tests/horn/pos/mod00.smt2 b/tests/horn/pos/mod00.smt2 index 87a1ee522..8ca59273e 100644 --- a/tests/horn/pos/mod00.smt2 +++ b/tests/horn/pos/mod00.smt2 @@ -1,19 +1,21 @@ (var $k0 (int)) - +; this is a comment (constraint - (and // this is a random comment + (and ; this is a random comment (and (forall ((a0 int) ((= a0 4))) ($k0 a0) ) (forall ((a1 int) ((= a1 10))) + ; and yet another comment ($k0 a1) ) ) (forall ((a2 int) (true)) + ; sprinkle sprinkle (forall ((_ int) (and ($k0 a2) ((>= a2 4)) ((>= a2 10)))) - (tag ((= ((mod a2 2)) 0)) "0") + (tag ((= ((mod a2 2)) 0)) "0") ; lets stick a comment here too! ) ) ) From 530a7c184b43bd5bac193fa537f12e94aa7d4796 Mon Sep 17 00:00:00 2001 From: Ranjit Jhala Date: Tue, 6 Aug 2024 15:36:57 -0700 Subject: [PATCH 3/3] fiddle --- src/Language/Fixpoint/Horn/SMTParse.hs | 5 +- tests/horn/pos/comment.smt2 | 106 +++++++++++++++++++++++++ tests/horn/pos/mod00.smt2 | 3 + 3 files changed, 112 insertions(+), 2 deletions(-) create mode 100644 tests/horn/pos/comment.smt2 diff --git a/src/Language/Fixpoint/Horn/SMTParse.hs b/src/Language/Fixpoint/Horn/SMTParse.hs index acc4cad2a..15122aa11 100644 --- a/src/Language/Fixpoint/Horn/SMTParse.hs +++ b/src/Language/Fixpoint/Horn/SMTParse.hs @@ -46,7 +46,7 @@ spaces = blockComment lineComment :: FParser () -lineComment = L.skipLineComment "; " +lineComment = L.skipLineComment ";" blockComment :: FParser () blockComment = L.skipBlockComment "/* " "*/" @@ -120,6 +120,7 @@ constantP = hornP :: FParser H.TagQuery ------------------------------------------------------------------------------- hornP = do + spaces hThings <- many hThingP pure (mkQuery hThings) @@ -156,7 +157,7 @@ data HThing a deriving (Functor) hThingP :: FParser (HThing H.Tag) -hThingP = parens body +hThingP = spaces >> parens body where body = HQual <$> (reserved "qualif" *> hQualifierP) <|> HCstr <$> (reserved "constraint" *> hCstrP) diff --git a/tests/horn/pos/comment.smt2 b/tests/horn/pos/comment.smt2 new file mode 100644 index 000000000..5503d7432 --- /dev/null +++ b/tests/horn/pos/comment.smt2 @@ -0,0 +1,106 @@ +;; Tag 0: Ret at 16:5: 16:11 + +(qualif EqZero ((v int)) ((= v 0))) +(qualif GtZero ((v int)) ((> v 0))) +(qualif GeZero ((v int)) ((>= v 0))) +(qualif LtZero ((v int)) ((< v 0))) +(qualif LeZero ((v int)) ((<= v 0))) +(qualif Eq ((a int) (b int)) ((= a b))) +(qualif Gt ((a int) (b int)) ((> a b))) +(qualif Ge ((a int) (b int)) ((>= a b))) +(qualif Lt ((a int) (b int)) ((< a b))) +(qualif Le ((a int) (b int)) ((<= a b))) +(qualif Le1 ((a int) (b int)) ((<= a ((- b 1))))) +(constant gt (func 1 (@(0) @(0) ) bool)) +(constant ge (func 1 (@(0) @(0) ) bool)) +(constant lt (func 1 (@(0) @(0) ) bool)) +(constant le (func 1 (@(0) @(0) ) bool)) +(var $k0 (int int int bool)) ;; orig: $k4 +(var $k1 (int int bool)) ;; orig: $k0 +(var $k2 (int int int bool)) ;; orig: $k1 +(var $k3 (int int int bool)) ;; orig: $k2 +(var $k4 (int int int bool)) ;; orig: $k3 +(var $k5 (int int int bool)) ;; orig: $k5 + +(constraint + (forall ((a0 int) (true)) + (forall ((a1 int) (true)) + (forall ((a2 bool) (true)) + (forall ((_ int) ((< a0 a1))) + (and + (forall ((_ int) ((not a2))) + (and + ($k0 a1 a0 a1 a2) + ($k1 a0 a1 a2) + ($k2 a0 a0 a1 a2) + (forall ((a3 int) (true)) + (forall ((_ int) ($k0 a3 a0 a1 a2)) + ($k3 a3 a0 a1 a2) + ) + ) + (forall ((a4 int) (true)) + (forall ((_ int) ($k0 a4 a0 a1 a2)) + ($k4 a4 a0 a1 a2) + ) + ) + (forall ((a5 int) (true)) + (forall ((_ int) ($k4 a5 a0 a1 a2)) + ($k0 a5 a0 a1 a2) + ) + ) + ) + ) + (forall ((_ int) (a2)) + (and + ($k5 a0 a0 a1 a2) + ($k1 a0 a1 a2) + (forall ((a6 int) (true)) + (forall ((_ int) ($k5 a6 a0 a1 a2)) + ($k2 a6 a0 a1 a2) + ) + ) + ($k3 a1 a0 a1 a2) + (forall ((a7 int) (true)) + (forall ((_ int) ($k5 a7 a0 a1 a2)) + ($k4 a7 a0 a1 a2) + ) + ) + (forall ((a8 int) (true)) + (forall ((_ int) ($k4 a8 a0 a1 a2)) + ($k5 a8 a0 a1 a2) + ) + ) + ) + ) + (forall ((_ int) ($k1 a0 a1 a2)) + (forall ((a9 int) (true)) + (forall ((_ int) ($k4 a9 a0 a1 a2)) + (and + (forall ((a10 int) ((= a10 ((+ a9 1))))) + ($k4 a10 a0 a1 a2) + ) + (forall ((a11 int) (true)) + (forall ((_ int) ($k4 a11 a0 a1 a2)) + (forall ((a12 int) (true)) + (forall ((_ int) ($k2 a12 a0 a1 a2)) + (forall ((a13 int) (true)) + (forall ((_ int) ($k3 a13 a0 a1 a2)) + (tag ((<= 0 ((- a11 a0)))) "0") + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) + +;; more junk \ No newline at end of file diff --git a/tests/horn/pos/mod00.smt2 b/tests/horn/pos/mod00.smt2 index 8ca59273e..f70693837 100644 --- a/tests/horn/pos/mod00.smt2 +++ b/tests/horn/pos/mod00.smt2 @@ -1,5 +1,8 @@ +; this is a comment too. + (var $k0 (int)) + ; this is a comment (constraint (and ; this is a random comment