diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -2,7 +2,7 @@ ## NEXT -## 0.9.6.3.4 (2026-01-14) +## 0.9.6.3.5 (2026-01-14) - Implement `--sortedsolution` to keep elaborated sorts in fqout/solution [#821](https:://github.com/ucsd-progsys/liquid-fixpoint/pull/821) - Retire old parser for horn queries [#820](https:://github.com/ucsd-progsys/liquid-fixpoint/pull/820) diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquid-fixpoint -version: 0.9.6.3.4 +version: 0.9.6.3.5 synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description: This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint @@ -67,7 +67,6 @@ Language.Fixpoint.Graph.Types Language.Fixpoint.Horn.Info Language.Fixpoint.Horn.Parse - Language.Fixpoint.Horn.SMTParse Language.Fixpoint.Horn.Solve Language.Fixpoint.Horn.Transformations Language.Fixpoint.Horn.Types diff --git a/src/Language/Fixpoint/Horn/Parse.hs b/src/Language/Fixpoint/Horn/Parse.hs --- a/src/Language/Fixpoint/Horn/Parse.hs +++ b/src/Language/Fixpoint/Horn/Parse.hs @@ -7,36 +7,136 @@ , hPredP , hQualifierP , hVarP - , numericDeclP + , exprP + , sortP ) where -import Language.Fixpoint.Parse +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 (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 + +fAddNumTyCon :: F.Symbol -> FP.Parser () +fAddNumTyCon = FP.addNumTyCon + +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 = reserved "true" >> return F.PTrue + +fFalseP :: FP.Parser F.Expr +fFalseP = reserved "false" >> return F.PFalse + +fSymconstP :: FP.Parser F.SymConst +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 :: Parser H.TagQuery +hornP :: FParser H.TagQuery ------------------------------------------------------------------------------- hornP = do + spaces hThings <- many hThingP pure (mkQuery hThings) mkQuery :: [HThing a] -> H.Query a mkQuery things = H.Query - { H.qQuals = [ q | HQual q <- things ] - , H.qVars = [ k | HVar k <- things ] - , H.qCstr = H.CAnd [ c | HCstr c <- things ] - , H.qCon = M.fromList [ (x,t) | HCon x t <- things ] - , H.qDis = M.fromList [ (x,t) | HDis x t <- things ] - , H.qEqns = [ e | HDef e <- things ] - , H.qMats = [ m | HMat m <- things ] - , H.qData = [ dd | HDat dd <- things ] - , H.qOpts = [ o | HOpt o <- things ] - , H.qNums = [ n | HNum n <- things ] - , H.qDefs = [] + { H.qQuals = [ q | HQual q <- things ] + , H.qVars = [ k | HVar k <- things ] + , H.qCstr = H.CAnd [ c | HCstr c <- things ] + , H.qCon = M.fromList [ (x,t) | HCon x t <- things ] + , H.qDis = M.fromList [ (x,t) | HDis x t <- things ] + , H.qEqns = [ e | HDef e <- things ] + , H.qDefs = [ e | HDfn e <- things ] + , H.qMats = [ m | HMat m <- things ] + , H.qData = [ dd | HDat dd <- things ] + , H.qOpts = [ o | HOpt o <- things ] + , H.qNums = [ s | HNum s <- things ] } -- | A @HThing@ describes the kinds of things we may see, in no particular order @@ -51,14 +151,15 @@ | HCon F.Symbol F.Sort | HDis F.Symbol F.Sort | HDef F.Equation + | HDfn F.Equation | HMat F.Rewrite | HDat !F.DataDecl | HOpt !String | HNum F.Symbol deriving (Functor) -hThingP :: Parser (HThing H.Tag) -hThingP = parens body +hThingP :: FParser (HThing H.Tag) +hThingP = spaces >> parens body where body = HQual <$> (reserved "qualif" *> hQualifierP) <|> HCstr <$> (reserved "constraint" *> hCstrP) @@ -67,52 +168,53 @@ <|> HCon <$> (reserved "constant" *> symbolP) <*> sortP <|> HDis <$> (reserved "distinct" *> symbolP) <*> sortP <|> HDef <$> (reserved "define" *> defineP) + <|> HDfn <$> (reserved "define_fun" *> defineP) <|> HMat <$> (reserved "match" *> matchP) - <|> HDat <$> (reserved "data" *> dataDeclP) + <|> HDat <$> (reserved "datatype" *> dataDeclP) <|> HNum <$> (reserved "numeric" *> numericDeclP) -numericDeclP :: Parser F.Symbol +numericDeclP :: FParser F.Symbol numericDeclP = do x <- F.val <$> locUpperIdP - addNumTyCon x + fAddNumTyCon x pure x ------------------------------------------------------------------------------- -hCstrP :: Parser (H.Cstr H.Tag) +hCstrP :: FParser (H.Cstr H.Tag) ------------------------------------------------------------------------------- -hCstrP = parens body +hCstrP = try (parens body) + <|> H.Head <$> hPredP <*> pure H.NoTag where body = H.CAnd <$> (reserved "and" *> many hCstrP) - <|> H.All <$> (reserved "forall" *> hBindP) <*> hCstrP - <|> H.Head <$> (reserved "tag" *> hPredP) <*> (H.Tag <$> stringLiteral) - <|> H.Head <$> hPredP <*> pure H.NoTag + <|> H.All <$> (reserved "forall" *> hBindP) <*> hCstrP + <|> H.Head <$> (reserved "tag" *> hPredP) <*> (H.Tag <$> stringLiteral) -hBindP :: Parser (H.Bind H.Tag) +hBindP :: FParser (H.Bind H.Tag) hBindP = parens $ do (x, t) <- symSortP H.Bind x t <$> hPredP <*> pure H.NoTag ------------------------------------------------------------------------------- -hPredP :: Parser H.Pred +hPredP :: FParser H.Pred ------------------------------------------------------------------------------- hPredP = parens body where - body = H.Var <$> kvSymP <*> some predP + body = H.Var <$> kvSymP <*> some exprP <|> H.PAnd <$> (reserved "and" *> some hPredP) - <|> H.Reft <$> predP + <|> H.Reft <$> exprP -kvSymP :: Parser F.Symbol +kvSymP :: FParser F.Symbol kvSymP = char '$' *> symbolP ------------------------------------------------------------------------------- -- | Qualifiers ------------------------------------------------------------------------------- -hQualifierP :: Parser F.Qualifier +hQualifierP :: FParser F.Qualifier hQualifierP = do pos <- getSourcePos n <- upperIdP params <- parens (some symSortP) - body <- parens predP + body <- exprP return $ F.mkQual n (mkParam <$> params) body pos mkParam :: (F.Symbol, F.Sort) -> F.QualParam @@ -122,12 +224,139 @@ -- | Horn Variables ------------------------------------------------------------------------------- -hVarP :: Parser (H.Var H.Tag) -hVarP = H.HVar <$> kvSymP <*> parens (some (parens sortP)) <*> pure H.NoTag +hVarP :: FParser (H.Var H.Tag) +hVarP = H.HVar <$> kvSymP <*> parens (some sortP) <*> pure H.NoTag ------------------------------------------------------------------------------- -- | Helpers ------------------------------------------------------------------------------- +sPairP :: FParser a -> FParser b -> FParser (a, b) +sPairP aP bP = parens ((,) <$> aP <*> bP) -symSortP :: Parser (F.Symbol, F.Sort) -symSortP = parens ((,) <$> symbolP <*> sortP) +sMany :: FParser a -> FParser [a] +sMany p = parens (many p) + + +symSortP :: FParser (F.Symbol, F.Sort) +symSortP = sPairP symbolP sortP +-- symSortP = fParens ((,) <$> fSymbolP <*> sortP) + +dataDeclP :: FParser F.DataDecl +dataDeclP = do + (tc, n) <- sPairP fTyConP fIntP + ctors <- sMany dataCtorP + pure $ F.DDecl tc n ctors + +dataCtorP :: FParser F.DataCtor +dataCtorP = parens (F.DCtor <$> locSymbolP <*> sMany dataFieldP) + +dataFieldP :: FParser F.DataField +dataFieldP = uncurry F.DField <$> sPairP locSymbolP sortP + +bindsP :: FParser [(F.Symbol, F.Sort)] +bindsP = sMany bindP + +bindP :: FParser (F.Symbol, F.Sort) +bindP = sPairP symbolP sortP + +-- | We only support lets with a single binder, but we parse this as a "singleton list" +-- to be forward compatible with multiple binders. Note that the semantics of multiple +-- binders in smtlib is *simulatenous substitution*, so they cannot be desugared to nested +-- lets. +exprBindsP :: FParser (F.Symbol, F.Expr) +exprBindsP = parens exprBindP + +exprBindP :: FParser (F.Symbol, F.Expr) +exprBindP = sPairP symbolP exprP + +defineP :: FParser F.Equation +defineP = do + name <- symbolP + xts <- bindsP + s <- sortP + body <- exprP + return $ F.mkEquation name xts body s + +matchP :: FParser F.Rewrite +matchP = do + f <- symbolP + d:xs <- parens (some symbolP) + F.SMeasure f d xs <$> exprP + +sortP :: FParser F.Sort +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) + <|> (F.FNatNum <$> natural) + +mkFunc :: Int -> [F.Sort] -> F.Sort -> F.Sort +mkFunc n ss s = F.mkFFunc n (ss ++ [s]) + +mkList :: F.Sort -> F.Sort +mkList s = F.fAppTC F.listFTyCon [s] + +exprP :: FParser F.Expr +exprP + = fTrueP + <|> fFalseP + <|> (F.ESym <$> fSymconstP) + <|> (F.ECon <$> constantP) + <|> (F.EVar <$> symbolP) + <|> parens pExprP + +pExprP :: FParser F.Expr +pExprP + = (reserved "if" >> (F.EIte <$> exprP <*> exprP <*> exprP)) + <|> (reserved "let" >> (uncurry F.ELet <$> exprBindsP <*> 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 (sym "-" >> (F.ENeg <$> exprP)) + <|> (mkApp <$> some exprP) + +mkLit :: String -> F.Sort -> F.Expr +mkLit l t = F.ECon (F.L (T.pack l) t) + +mkApp :: [F.Expr] -> F.Expr +mkApp (e:es) = F.eApps e es +mkApp _ = error "impossible" + +bopP :: FParser F.Bop +bopP + = (sym "+" >> return F.Plus) + <|> (sym "-" >> return F.Minus) + <|> (sym "*" >> return F.Times) + <|> (sym "/" >> return F.Div) + <|> (reserved "mod" >> return F.Mod) + <|> (sym "*." >> return F.RTimes) + <|> (sym "/." >> return F.RDiv) + +brelP :: FParser F.Brel +brelP + = (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) diff --git a/src/Language/Fixpoint/Horn/SMTParse.hs b/src/Language/Fixpoint/Horn/SMTParse.hs deleted file mode 100644 --- a/src/Language/Fixpoint/Horn/SMTParse.hs +++ /dev/null @@ -1,362 +0,0 @@ - -{-# LANGUAGE DeriveFunctor #-} - -module Language.Fixpoint.Horn.SMTParse ( - hornP - , hCstrP - , hPredP - , hQualifierP - , hVarP - , exprP - , sortP -) where - -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 (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 - -fAddNumTyCon :: F.Symbol -> FP.Parser () -fAddNumTyCon = FP.addNumTyCon - -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 = reserved "true" >> return F.PTrue - -fFalseP :: FP.Parser F.Expr -fFalseP = reserved "false" >> return F.PFalse - -fSymconstP :: FP.Parser F.SymConst -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 -------------------------------------------------------------------------------- -hornP = do - spaces - hThings <- many hThingP - pure (mkQuery hThings) - -mkQuery :: [HThing a] -> H.Query a -mkQuery things = H.Query - { H.qQuals = [ q | HQual q <- things ] - , H.qVars = [ k | HVar k <- things ] - , H.qCstr = H.CAnd [ c | HCstr c <- things ] - , H.qCon = M.fromList [ (x,t) | HCon x t <- things ] - , H.qDis = M.fromList [ (x,t) | HDis x t <- things ] - , H.qEqns = [ e | HDef e <- things ] - , H.qDefs = [ e | HDfn e <- things ] - , H.qMats = [ m | HMat m <- things ] - , H.qData = [ dd | HDat dd <- things ] - , H.qOpts = [ o | HOpt o <- things ] - , H.qNums = [ s | HNum s <- things ] - } - --- | A @HThing@ describes the kinds of things we may see, in no particular order --- in a .smt2 query file. - -data HThing a - = HQual !F.Qualifier - | HVar !(H.Var a) - | HCstr !(H.Cstr a) - - -- for uninterpred functions and ADT constructors - | HCon F.Symbol F.Sort - | HDis F.Symbol F.Sort - | HDef F.Equation - | HDfn F.Equation - | HMat F.Rewrite - | HDat !F.DataDecl - | HOpt !String - | HNum F.Symbol - deriving (Functor) - -hThingP :: FParser (HThing H.Tag) -hThingP = spaces >> parens body - where - 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) - <|> HDfn <$> (reserved "define_fun" *> defineP) - <|> HMat <$> (reserved "match" *> matchP) - <|> HDat <$> (reserved "datatype" *> dataDeclP) - <|> HNum <$> (reserved "numeric" *> numericDeclP) - -numericDeclP :: FParser F.Symbol -numericDeclP = do - x <- F.val <$> locUpperIdP - fAddNumTyCon x - pure x - -------------------------------------------------------------------------------- -hCstrP :: FParser (H.Cstr H.Tag) -------------------------------------------------------------------------------- -hCstrP = try (parens body) - <|> H.Head <$> hPredP <*> pure H.NoTag - where - body = H.CAnd <$> (reserved "and" *> many hCstrP) - <|> H.All <$> (reserved "forall" *> hBindP) <*> hCstrP - <|> H.Head <$> (reserved "tag" *> hPredP) <*> (H.Tag <$> stringLiteral) - -hBindP :: FParser (H.Bind H.Tag) -hBindP = parens $ do - (x, t) <- symSortP - H.Bind x t <$> hPredP <*> pure H.NoTag - -------------------------------------------------------------------------------- -hPredP :: FParser H.Pred -------------------------------------------------------------------------------- -hPredP = parens body - where - body = H.Var <$> kvSymP <*> some exprP - <|> H.PAnd <$> (reserved "and" *> some hPredP) - <|> H.Reft <$> exprP - -kvSymP :: FParser F.Symbol -kvSymP = char '$' *> symbolP - -------------------------------------------------------------------------------- --- | Qualifiers -------------------------------------------------------------------------------- -hQualifierP :: FParser F.Qualifier -hQualifierP = do - pos <- getSourcePos - n <- upperIdP - params <- parens (some symSortP) - body <- exprP - return $ F.mkQual n (mkParam <$> params) body pos - -mkParam :: (F.Symbol, F.Sort) -> F.QualParam -mkParam (x, t) = F.QP x F.PatNone t - -------------------------------------------------------------------------------- --- | Horn Variables -------------------------------------------------------------------------------- - -hVarP :: FParser (H.Var H.Tag) -hVarP = H.HVar <$> kvSymP <*> parens (some sortP) <*> pure H.NoTag - -------------------------------------------------------------------------------- --- | Helpers -------------------------------------------------------------------------------- -sPairP :: FParser a -> FParser b -> FParser (a, b) -sPairP aP bP = parens ((,) <$> aP <*> bP) - -sMany :: FParser a -> FParser [a] -sMany p = parens (many p) - - -symSortP :: FParser (F.Symbol, F.Sort) -symSortP = sPairP symbolP sortP --- symSortP = fParens ((,) <$> fSymbolP <*> sortP) - -dataDeclP :: FParser F.DataDecl -dataDeclP = do - (tc, n) <- sPairP fTyConP fIntP - ctors <- sMany dataCtorP - pure $ F.DDecl tc n ctors - -dataCtorP :: FParser F.DataCtor -dataCtorP = parens (F.DCtor <$> locSymbolP <*> sMany dataFieldP) - -dataFieldP :: FParser F.DataField -dataFieldP = uncurry F.DField <$> sPairP locSymbolP sortP - -bindsP :: FParser [(F.Symbol, F.Sort)] -bindsP = sMany bindP - -bindP :: FParser (F.Symbol, F.Sort) -bindP = sPairP symbolP sortP - --- | We only support lets with a single binder, but we parse this as a "singleton list" --- to be forward compatible with multiple binders. Note that the semantics of multiple --- binders in smtlib is *simulatenous substitution*, so they cannot be desugared to nested --- lets. -exprBindsP :: FParser (F.Symbol, F.Expr) -exprBindsP = parens exprBindP - -exprBindP :: FParser (F.Symbol, F.Expr) -exprBindP = sPairP symbolP exprP - -defineP :: FParser F.Equation -defineP = do - name <- symbolP - xts <- bindsP - s <- sortP - body <- exprP - return $ F.mkEquation name xts body s - -matchP :: FParser F.Rewrite -matchP = do - f <- symbolP - d:xs <- parens (some symbolP) - F.SMeasure f d xs <$> exprP - -sortP :: FParser F.Sort -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) - <|> (F.FNatNum <$> natural) - -mkFunc :: Int -> [F.Sort] -> F.Sort -> F.Sort -mkFunc n ss s = F.mkFFunc n (ss ++ [s]) - -mkList :: F.Sort -> F.Sort -mkList s = F.fAppTC F.listFTyCon [s] - -exprP :: FParser F.Expr -exprP - = fTrueP - <|> fFalseP - <|> (F.ESym <$> fSymconstP) - <|> (F.ECon <$> constantP) - <|> (F.EVar <$> symbolP) - <|> parens pExprP - -pExprP :: FParser F.Expr -pExprP - = (reserved "if" >> (F.EIte <$> exprP <*> exprP <*> exprP)) - <|> (reserved "let" >> (uncurry F.ELet <$> exprBindsP <*> 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 (sym "-" >> (F.ENeg <$> exprP)) - <|> (mkApp <$> some exprP) - -mkLit :: String -> F.Sort -> F.Expr -mkLit l t = F.ECon (F.L (T.pack l) t) - -mkApp :: [F.Expr] -> F.Expr -mkApp (e:es) = F.eApps e es -mkApp _ = error "impossible" - -bopP :: FParser F.Bop -bopP - = (sym "+" >> return F.Plus) - <|> (sym "-" >> return F.Minus) - <|> (sym "*" >> return F.Times) - <|> (sym "/" >> return F.Div) - <|> (reserved "mod" >> return F.Mod) - <|> (sym "*." >> return F.RTimes) - <|> (sym "/." >> return F.RDiv) - -brelP :: FParser F.Brel -brelP - = (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) diff --git a/src/Language/Fixpoint/Horn/Solve.hs b/src/Language/Fixpoint/Horn/Solve.hs --- a/src/Language/Fixpoint/Horn/Solve.hs +++ b/src/Language/Fixpoint/Horn/Solve.hs @@ -17,7 +17,6 @@ import qualified Language.Fixpoint.Horn.Types as H import qualified Language.Fixpoint.Horn.Parse as H -import qualified Language.Fixpoint.Horn.SMTParse as SH import qualified Language.Fixpoint.Horn.Transformations as Tx import Text.PrettyPrint.HughesPJ.Compat ( render ) @@ -47,13 +46,12 @@ parseQuery :: F.Config -> IO H.TagQuery parseQuery cfg - | F.stdin cfg = Parse.parseFromStdIn hornP + | F.stdin cfg = Parse.parseFromStdIn H.hornP | json = loadFromJSON file - | otherwise = Parse.parseFromFile hornP file + | otherwise = Parse.parseFromFile H.hornP file where json = Files.isExtFile Files.Json file file = F.srcFile cfg - hornP = if F.noSmtHorn cfg then H.hornP else SH.hornP loadFromJSON :: FilePath -> IO H.TagQuery loadFromJSON f = do diff --git a/src/Language/Fixpoint/Solver.hs b/src/Language/Fixpoint/Solver.hs --- a/src/Language/Fixpoint/Solver.hs +++ b/src/Language/Fixpoint/Solver.hs @@ -336,6 +336,7 @@ , resNonCutsSolution = HashMap.map (fmap simplifyKVar') (resNonCutsSolution res) } where - simplifyKVar' = unElabSets . unElab . Sol.simplifyKVar HashSet.empty + simplifyKVar' = unElabSets . unElab' . Sol.simplifyKVar HashSet.empty sets = elabSetBag . solverFlags $ cfg unElabSets = if sets then unElabFSetBagZ3 else id + unElab' = if sortedSolution cfg then id else unElab diff --git a/src/Language/Fixpoint/Types/Config.hs b/src/Language/Fixpoint/Types/Config.hs --- a/src/Language/Fixpoint/Types/Config.hs +++ b/src/Language/Fixpoint/Types/Config.hs @@ -114,9 +114,9 @@ , json :: Bool -- ^ Render output in JSON format , fuel :: Maybe Int -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite) , restOrdering :: String -- ^ Term ordering for use in REST - , noSmtHorn :: Bool -- ^ Do not use (new) SMTLIB horn parser , noStringTheory :: Bool -- ^ disable interpretation of string theory by SMT , explicitKvars :: Bool -- ^ use explicitly declared kvars (horn style) which disables several "defensive simplifications" + , sortedSolution :: Bool -- ^ leave sorts in the solution } deriving (Eq,Data,Typeable,Show,Generic) instance Default Config where @@ -287,8 +287,8 @@ , json = False &= help "Render result in JSON" , fuel = Nothing &= help "Maximum fuel (per-function unfoldings) for PLE" , restOrdering = "rpo" &= help "Ordering Constraint Algebra to use for REST" - , noSmtHorn = False &= help "Do not use SMTLIB horn format" , explicitKvars = False &= help "Use explicitly declared kvars (horn style) which disables several defensive simplifications" + , sortedSolution = False &= help "Leave elaborated sorts in the solution (only for machine consumption)" } &= verbosity &= program "fixpoint"