diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,21 @@ ## NEXT + +## 0.9.6.3.1 (2024-08-21) + +- Added support for ghc-9.10.1 +- Use `;` for comments in SMTParse (as done in SMTLIB) [#700](https://github.com/ucsd-progsys/liquid-fixpoint/pull/700). +- Extend SMTParser to support lits e.g. for bitvec [#698](https://github.com/ucsd-progsys/liquid-fixpoint/pull/698). +- refactor `Set->Array` elaboration [#696](https://github.com/ucsd-progsys/liquid-fixpoint/pull/696). +- Fixed the polymorphism-related crash caused by a restrictive Set theory encoding [#688](https://github.com/ucsd-progsys/liquid-fixpoint/pull/688). +- Do not constant-fold div by zero [#686](https://github.com/ucsd-progsys/liquid-fixpoint/issue/686). +- Copy over the HOF configuraration options in hornFInfo [#684](https://github.com/ucsd-progsys/liquid-fixpoint/pull/684). +- Use SMTLIB style serialization/deserialization for Horn queries [#683](https://github.com/ucsd-progsys/liquid-fixpoint/pull/683). +- Print SMT preamble to the logfile when constructing context [#681](https://github.com/ucsd-progsys/liquid-fixpoint/pull/681). +- Allow reading/saving horn queries from/to JSON [#680](https://github.com/ucsd-progsys/liquid-fixpoint/pull/680). +- Extend parser to allow boolean function arguments [#678](https://github.com/ucsd-progsys/liquid-fixpoint/pull/678). + ## 0.9.6.3 (2024-01-29) - For now we stopped folding constants that contain NaN [#670](https://github.com/ucsd-progsys/liquid-fixpoint/pull/670) @@ -29,27 +44,27 @@ ## 0.8.6.4 - Fix bugs in PLE -- Move to GHC 8.6.4 +- Move to GHC 8.6.4 - Add `fuel` parameter to debug unfolding in PLE -## 0.8.0.1 +## 0.8.0.1 - Support for HORN-NNF format clauses, see `tests/horn/{pos,neg}/*.smt2` - Support for "existential binders", see `tests/pos/ebind-*.fq` for example. This only works with `--eliminate`. -- Move to GHC 8.4.3 +- Move to GHC 8.4.3 ## 0.7.0.0 - New `eliminate` based solver (see ICFP 2017 paper for algorithm) - Proof by Logical Evaluation see `tests/proof` -- SMTLIB2 ADTs to make data constructors injective +- SMTLIB2 ADTs to make data constructors injective - Uniformly support polymorphic functions via `apply` and elaborate ## 0.3.0.0 - Make interpreted mul and div the default, when `solver = z3` -- Use `higherorder` flag to allow higher order binders into the environment +- Use `higherorder` flag to allow higher order binders into the environment ## 0.2.2.0 diff --git a/bin/Fixpoint.hs b/bin/Fixpoint.hs --- a/bin/Fixpoint.hs +++ b/bin/Fixpoint.hs @@ -24,7 +24,11 @@ | otherwise = solveFQ isHorn :: F.Config -> Bool -isHorn cfg = F.isExtFile F.Smt2 (F.srcFile cfg) || F.stdin cfg +isHorn cfg = F.isExtFile F.Smt2 file + || F.isExtFile F.Json file + || F.stdin cfg + where + file = F.srcFile cfg errorExit :: F.Error -> IO ExitCode errorExit e = do 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 +version: 0.9.6.3.1 synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description: This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint @@ -25,7 +25,7 @@ license: BSD-3-Clause license-file: LICENSE build-type: Simple -tested-with: GHC == 9.6.3, GHC == 9.4.7, GHC == 9.2.3 +tested-with: GHC == 9.10.1, GHC == 9.8.2, GHC == 9.6.5 extra-source-files: tests/neg/*.fq tests/pos/*.fq unix/Language/Fixpoint/Utils/*.hs @@ -66,6 +66,7 @@ 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 @@ -152,7 +153,6 @@ , parser-combinators , pretty >= 1.1.3.1 , process - , typed-process , rest-rewrite >= 0.3.0 , smtlib-backends >= 0.3 , smtlib-backends-process >= 0.3 @@ -174,6 +174,8 @@ if impl(ghc<9.6) ghc-options: -Wno-unused-imports + if impl(ghc>9.8) + ghc-options: -Wno-x-partial if flag(devel) ghc-options: -Werror if !os(windows) @@ -210,10 +212,9 @@ , mtl >= 2.2.2 , optparse-applicative , process - , typed-process , stm >= 2.4 , tagged - , tasty >= 0.10 && < 1.5 + , tasty ^>= 1.5 , tasty-ant-xml , tasty-hunit >= 0.9 , tasty-rerun >= 1.1.12 diff --git a/src/Language/Fixpoint/Horn/Info.hs b/src/Language/Fixpoint/Horn/Info.hs --- a/src/Language/Fixpoint/Horn/Info.hs +++ b/src/Language/Fixpoint/Horn/Info.hs @@ -6,6 +6,7 @@ ) where import Control.Monad (forM) +import Data.Ord (Down(..), comparing) import qualified Data.HashMap.Strict as M import qualified Data.List as L import qualified Data.Tuple as Tuple @@ -17,7 +18,7 @@ import qualified Language.Fixpoint.Horn.Types as H import qualified Data.Maybe as Mb -hornFInfo :: F.Config -> H.Query a -> F.FInfo a +hornFInfo :: (F.Fixpoint a, F.PPrint a) => F.Config -> H.Query a -> F.FInfo a hornFInfo cfg q = mempty { F.cm = cs , F.bs = be2 @@ -28,6 +29,7 @@ , F.dLits = F.fromMapSEnv $ H.qDis q , F.ae = axEnv cfg q cs , F.ddecls = H.qData q + , F.hoInfo = F.cfgHoInfo cfg } where be0 = F.emptyBindEnv @@ -119,7 +121,7 @@ err1 = F.panic ("Unknown Horn variable: " ++ F.showpp k) ---------------------------------------------------------------------------------- -hornWfs :: F.BindEnv a -> [H.Var a] -> (F.BindEnv a, KVEnv a) +hornWfs :: (F.PPrint a) => F.BindEnv a -> [H.Var a] -> (F.BindEnv a, KVEnv a) ---------------------------------------------------------------------------------- hornWfs be vars = (be', kve) where @@ -127,7 +129,7 @@ (be', is) = L.mapAccumL kvInfo be vars kname = H.hvName . kvVar -kvInfo :: F.BindEnv a -> H.Var a -> (F.BindEnv a, KVInfo a) +kvInfo :: (F.PPrint a) => F.BindEnv a -> H.Var a -> (F.BindEnv a, KVInfo a) kvInfo be k = (be', KVInfo k (Misc.fst3 <$> xts) wfc) where -- make the WfC @@ -224,7 +226,7 @@ ixts <- forM xs $ \x -> do (t, i) <- lookupBindEnv x env return (i, x, t) - return [ (x, t) | (_, x, t) <- reverse . L.sort $ ixts ] + return [ (x, t) | (_, x, t) <- L.sortBy (comparing Down) ixts ] -- ixts = [ (i, x, t) | x <- xs, (i, t) <- lookupBindEnv x env ] 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,6 +7,7 @@ , hPredP , hQualifierP , hVarP + , numericDeclP ) where import Language.Fixpoint.Parse @@ -17,11 +18,11 @@ import qualified Data.HashMap.Strict as M ------------------------------------------------------------------------------- -hornP :: Parser (H.TagQuery, [String]) +hornP :: Parser H.TagQuery ------------------------------------------------------------------------------- hornP = do hThings <- many hThingP - pure (mkQuery hThings, [ o | HOpt o <- hThings ]) + pure (mkQuery hThings) mkQuery :: [HThing a] -> H.Query a mkQuery things = H.Query @@ -33,6 +34,8 @@ , 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 ] } -- | A @HThing@ describes the kinds of things we may see, in no particular order @@ -50,7 +53,7 @@ | HMat F.Rewrite | HDat !F.DataDecl | HOpt !String - | HNum () + | HNum F.Symbol deriving (Functor) hThingP :: Parser (HThing H.Tag) @@ -67,10 +70,11 @@ <|> HDat <$> (reserved "data" *> dataDeclP) <|> HNum <$> (reserved "numeric" *> numericDeclP) -numericDeclP :: Parser () +numericDeclP :: Parser F.Symbol numericDeclP = do - sym <- locUpperIdP - addNumTyCon (F.val sym) + x <- F.val <$> locUpperIdP + addNumTyCon x + pure x ------------------------------------------------------------------------------- hCstrP :: Parser (H.Cstr H.Tag) diff --git a/src/Language/Fixpoint/Horn/SMTParse.hs b/src/Language/Fixpoint/Horn/SMTParse.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Horn/SMTParse.hs @@ -0,0 +1,348 @@ + +{-# 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.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 + | 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) + <|> 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.Any <$> (reserved "exists" *> 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 symbolP + <|> 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 + +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) + +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 "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) + <|> (sym "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 @@ -15,47 +15,74 @@ import qualified Language.Fixpoint.Types as F import qualified Language.Fixpoint.Types.Config as F 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 ) import Language.Fixpoint.Horn.Info ( hornFInfo ) import System.Console.CmdArgs.Verbosity ( whenLoud ) - +import qualified Data.Aeson as Aeson -- import Debug.Trace (traceM) ---------------------------------------------------------------------------------- solveHorn :: F.Config -> IO ExitCode ---------------------------------------------------------------------------------- solveHorn baseCfg = do - (q, opts) <- parseQuery baseCfg + q <- parseQuery baseCfg -- If you want to set --eliminate=none, you better make it a pragma cfgElim <- if F.eliminate baseCfg == F.None then pure (baseCfg { F.eliminate = F.Some }) else pure baseCfg - cfgPragmas <- F.withPragmas cfgElim opts + cfgPragmas <- F.withPragmas cfgElim (H.qOpts q) when (F.save cfgPragmas) (saveHornQuery cfgPragmas q) r <- solve cfgPragmas q Solver.resultExitCode cfgPragmas r -parseQuery :: F.Config -> IO (H.Query H.Tag, [String]) +parseQuery :: F.Config -> IO H.TagQuery parseQuery cfg - | F.stdin cfg = Parse.parseFromStdIn H.hornP - | otherwise = Parse.parseFromFile H.hornP (F.srcFile cfg) + | F.stdin cfg = Parse.parseFromStdIn hornP + | json = loadFromJSON file + | otherwise = Parse.parseFromFile 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 + r <- Aeson.eitherDecodeFileStrict f + case r of + Right v -> return v + Left err -> error ("Error in loadFromJSON: " ++ err) + saveHornQuery :: F.Config -> H.Query H.Tag -> IO () saveHornQuery cfg q = do + saveHornSMT2 cfg q + saveHornJSON cfg q + +saveHornSMT2 :: H.ToHornSMT a => F.Config -> a -> IO () +saveHornSMT2 cfg q = do let hq = F.queryFile Files.HSmt2 cfg putStrLn $ "Saving Horn Query: " ++ hq ++ "\n" Misc.ensurePath hq - writeFile hq $ render (F.pprint q) + writeFile hq $ render ({- F.pprint -} H.toHornSMT q) +saveHornJSON :: F.Config -> H.Query H.Tag -> IO () +saveHornJSON cfg q = do + let hjson = F.queryFile Files.HJSON cfg + putStrLn $ "Saving Horn Query: " ++ hjson ++ "\n" + Misc.ensurePath hjson + Aeson.encodeFile hjson q + ---------------------------------------------------------------------------------- -eliminate :: (F.PPrint a) => F.Config -> H.Query a -> IO (H.Query a) +eliminate :: (F.Fixpoint a, F.PPrint a) => F.Config -> H.Query a -> IO (H.Query a) ---------------------------------------------------------------------------------- eliminate cfg q | F.eliminate cfg == F.Existentials = do diff --git a/src/Language/Fixpoint/Horn/Transformations.hs b/src/Language/Fixpoint/Horn/Transformations.hs --- a/src/Language/Fixpoint/Horn/Transformations.hs +++ b/src/Language/Fixpoint/Horn/Transformations.hs @@ -23,7 +23,11 @@ import qualified Data.HashMap.Strict as M import Data.String (IsString (..)) import Data.Either (partitionEithers, rights) +#if MIN_VERSION_base(4,20,0) +import Data.List (nub) +#else import Data.List (nub, foldl') +#endif import qualified Data.Set as S import qualified Data.HashSet as HS import qualified Data.Graph as DG @@ -71,16 +75,19 @@ -- can depend on other ks, pis cannot directly depend on other pis -- - predicate for exists binder is `true`. (TODO: is this pre stale?) -solveEbs :: (F.PPrint a) => F.Config -> Query a -> IO (Query a) +solveEbs :: (F.Fixpoint a, F.PPrint a) => F.Config -> Query a -> IO (Query a) ------------------------------------------------------------------------------ -solveEbs cfg query@(Query qs vs cstr cons dist eqns mats dds) = do +solveEbs cfg query@(Query {}) = do + let cons = qCon query + let cstr = qCstr query + let dist = qDis query -- clean up let normalizedC = flatten . pruneTauts $ hornify cstr whenLoud $ putStrLn "Normalized EHC:" whenLoud $ putStrLn $ F.showpp normalizedC -- short circuit if no ebinds are present - if isNNF cstr then pure $ Query qs vs normalizedC cons dist eqns mats dds else do + if isNNF cstr then pure $ query{ qCstr = normalizedC } else do let kvars = boundKvars normalizedC whenLoud $ putStrLn "Skolemized:" @@ -129,7 +136,7 @@ let solvedSide = substPiSols solvedPiCstrs sideCut whenLoud $ putStrLn $ F.showpp solvedSide - pure (Query qs vs (CAnd [solvedHorn, solvedSide]) cons dist eqns mats dds) + pure (query { qCstr = CAnd [solvedHorn, solvedSide] }) -- | Collects the defining constraint for π -- that is, given `∀ Γ.∀ n.π => c`, returns `((π, n:Γ), c)` @@ -929,10 +936,10 @@ isNNF (All _ c) = isNNF c isNNF Any{} = False -calculateCuts :: F.Config -> Query a -> Cstr a -> S.Set F.Symbol -calculateCuts cfg (Query qs vs _ cons dist eqns mats dds) nnf = convert $ FG.depCuts deps +calculateCuts :: (F.Fixpoint a, F.PPrint a) => F.Config -> Query a -> Cstr a -> S.Set F.Symbol +calculateCuts cfg q@(Query {}) nnf = convert $ FG.depCuts deps where - (_, deps) = elimVars cfg (hornFInfo cfg $ Query qs vs nnf cons dist eqns mats dds) + (_, deps) = elimVars cfg (hornFInfo cfg $ q { qCstr = nnf }) convert hashset = S.fromList $ F.kv <$> HS.toList hashset forgetPiVars :: S.Set F.Symbol -> Cstr a -> Cstr a @@ -969,13 +976,32 @@ flatten :: a -> a instance Flatten (Cstr a) where - flatten (CAnd cstrs) = case flatten cstrs of - [c] -> c - cs -> CAnd cs - flatten (Head p a) = Head (flatten p) a - flatten (All (Bind x t p l) c) = All (Bind x t (flatten p) l) (flatten c) - flatten (Any (Bind x t p l) c) = Any (Bind x t (flatten p) l) (flatten c) + flatten c = case flattenCstr c of + Just c' -> c' + Nothing -> CAnd [] + -- flatten (CAnd cstrs) = case flatten cstrs of + -- [c] -> c + -- cs -> CAnd cs + -- flatten (Head p a) = Head (flatten p) a + -- flatten (All (Bind x t p l) c) = All (Bind x t (flatten p) l) (flatten c) + -- flatten (Any (Bind x t p l) c) = Any (Bind x t (flatten p) l) (flatten c) + +flattenCstr :: Cstr a -> Maybe (Cstr a) +flattenCstr = go + where + go (Head (PAnd []) _) = Nothing + go (Head (Reft p) _) + | F.isTautoPred p = Nothing + go (Head p a) = Just $ Head (flatten p) a + go (CAnd cs) = mk . concatMap splitAnd $ mapMaybe flattenCstr cs + go (All (Bind x t p l) c) = All (Bind x t (flatten p) l) <$> go c + go (Any (Bind x t p l) c) = Any (Bind x t (flatten p) l) <$> go c + + mk [] = Nothing + mk [c] = Just c + mk cs = Just (CAnd cs) + instance Flatten [Cstr a] where flatten (CAnd cs : xs) = flatten cs ++ flatten xs flatten (x:xs) @@ -984,6 +1010,12 @@ | otherwise = fx:flatten xs where fx = flatten x flatten [] = [] + + + +splitAnd :: Cstr a -> [Cstr a] +splitAnd (CAnd cs) = cs +splitAnd c = [c] instance Flatten Pred where flatten (PAnd preds) = case flatten preds of diff --git a/src/Language/Fixpoint/Horn/Types.hs b/src/Language/Fixpoint/Horn/Types.hs --- a/src/Language/Fixpoint/Horn/Types.hs +++ b/src/Language/Fixpoint/Horn/Types.hs @@ -8,6 +8,9 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ViewPatterns #-} module Language.Fixpoint.Horn.Types ( -- * Horn Constraints and their components @@ -30,6 +33,9 @@ -- * extract qualifiers , quals + + -- * SMTLIB style render + , ToHornSMT (..) ) where @@ -45,6 +51,7 @@ import qualified Text.PrettyPrint.HughesPJ.Compat as P import qualified Data.HashMap.Strict as M import Data.Aeson +import Data.Aeson.Types ------------------------------------------------------------------------------- -- | @HVar@ is a Horn variable @@ -54,7 +61,7 @@ , hvArgs :: ![F.Sort] {- len hvArgs > 0 -} -- ^ sorts of its parameters i.e. of the relation defined by the @HVar@ , hvMeta :: a -- ^ meta-data } - deriving (Eq, Ord, Data, Typeable, Generic, Functor) + deriving (Eq, Ord, Data, Typeable, Generic, Functor, ToJSON, FromJSON) ------------------------------------------------------------------------------- -- | @HPred@ is a Horn predicate that appears as LHS (body) or RHS (head) of constraints @@ -63,7 +70,7 @@ = Reft !F.Expr -- ^ r | Var !F.Symbol ![F.Symbol] -- ^ $k(y1..yn) | PAnd ![Pred] -- ^ p1 /\ .../\ pn - deriving (Data, Typeable, Generic, Eq) + deriving (Data, Typeable, Generic, Eq, ToJSON, FromJSON) instance Semigroup Pred where @@ -96,7 +103,7 @@ ------------------------------------------------------------------------------- quals :: Cstr a -> [F.Qualifier] ------------------------------------------------------------------------------- -quals = F.tracepp "horn.quals" . cstrQuals F.emptySEnv F.vv_ +quals = F.notracepp "horn.quals" . cstrQuals F.emptySEnv F.vv_ cstrQuals :: F.SEnv F.Sort -> F.Symbol -> Cstr a -> [F.Qualifier] cstrQuals = go @@ -152,13 +159,12 @@ , bPred :: !Pred , bMeta :: !a } - deriving (Data, Typeable, Generic, Functor, Eq) + deriving (Data, Typeable, Generic, Functor, Eq, ToJSON, FromJSON) instance F.Subable (Bind a) where syms (Bind x _ p _) = x : F.syms p substa f (Bind v t p a) = Bind (f v) t (F.substa f p) a substf f (Bind v t p a) = Bind v t (F.substf (F.substfExcept f [v]) p) a - -- subst su (Bind x t p) = (Bind x t (F.subst su p)) subst su (Bind v t p a) = Bind v t (F.subst (F.substExcept su [v]) p) a subst1 (Bind v t p a) su = Bind v t (F.subst1Except [v] p su) a @@ -168,7 +174,7 @@ | CAnd ![Cstr a] -- ^ c1 /\ ... /\ cn | All !(Bind a) !(Cstr a) -- ^ \all x:t. p => c | Any !(Bind a) !(Cstr a) -- ^ \exi x:t. p /\ c or is it \exi x:t. p => c? - deriving (Data, Typeable, Generic, Functor, Eq) + deriving (Data, Typeable, Generic, Functor, Eq, ToJSON, FromJSON) cLabel :: Cstr a -> a cLabel cstr = case go cstr of @@ -196,13 +202,15 @@ { qQuals :: ![F.Qualifier] -- ^ qualifiers over which to solve cstrs , qVars :: ![Var a] -- ^ kvars, with parameter-sorts , qCstr :: !(Cstr a) -- ^ list of constraints - , qCon :: M.HashMap F.Symbol F.Sort -- ^ list of constants (uninterpreted functions - , qDis :: M.HashMap F.Symbol F.Sort -- ^ list of constants (uninterpreted functions + , qCon :: M.HashMap F.Symbol F.Sort -- ^ list of constants (uninterpreted functions) + , qDis :: M.HashMap F.Symbol F.Sort -- ^ list of *distinct* constants (uninterpreted functions) , qEqns :: ![F.Equation] -- ^ list of equations , qMats :: ![F.Rewrite] -- ^ list of match-es - , qData :: ![F.DataDecl] -- ^ list of data-declarations + , qData :: ![F.DataDecl] -- ^ list of data-declarations + , qOpts :: ![String] -- ^ list of fixpoint options + , qNums :: ![F.Symbol] -- ^ list of numeric TyCon (?) } - deriving (Data, Typeable, Generic, Functor) + deriving (Data, Typeable, Generic, Functor, ToJSON, FromJSON) -- | Tag each query with a possible string denoting "provenance" @@ -228,23 +236,35 @@ toJSON NoTag = Null toJSON (Tag s) = String (T.pack s) +instance FromJSON Tag where + parseJSON Null = pure NoTag + parseJSON (String t) = pure (Tag (T.unpack t)) + parseJSON invalid = prependFailure "parsing `Tag` failed, " (typeMismatch "Object" invalid) + + + + + instance F.PPrint (Query a) where pprintPrec prec t q = P.vcat $ L.intersperse " " [ P.vcat (ppQual <$> qQuals q) , P.vcat [ppVar k | k <- qVars q] - , P.vcat [ppCon x sort' | (x, sort') <- M.toList (qCon q)] + , P.vcat [ppCon x (F.pprint sort') | (x, sort') <- M.toList (qCon q)] , ppThings Nothing (qEqns q) , ppThings (Just "data ") (qData q) , P.parens (P.vcat ["constraint", F.pprintPrec (prec+2) t (qCstr q)]) ] + + + ppThings :: F.PPrint a => Maybe P.Doc -> [a] -> P.Doc ppThings pfx qs = P.vcat [ P.parens $ prefix P.<-> F.pprint q | q <- qs] where prefix = fromMaybe "" pfx -ppCon :: F.Symbol -> F.Sort -> P.Doc -ppCon x t = P.parens ("constant" P.<+> F.pprint x P.<+> P.parens (F.pprint t)) +ppCon :: F.Symbol -> P.Doc -> P.Doc +ppCon x td = P.parens ("constant" P.<+> F.pprint x P.<+> P.parens td) ppQual :: F.Qualifier -> P.Doc ppQual (F.Q n xts p _) = P.parens ("qualif" P.<+> F.pprint n P.<+> ppBlanks (ppArg <$> xts) P.<+> P.parens (F.pprint p)) @@ -301,3 +321,161 @@ instance F.PPrint (Bind a) where pprintPrec _ _ b = P.ptext $ show b + + +----------------------------------------------------------------------------------------------------------------- +-- Human readable but robustly parseable SMT-LIB format pretty printer +----------------------------------------------------------------------------------------------------------------- +class ToHornSMT a where + toHornSMT :: a -> P.Doc + +instance ToHornSMT Tag where + toHornSMT NoTag = mempty + toHornSMT (Tag s) = P.text s + +instance ToHornSMT F.Symbol where + toHornSMT s = F.pprint s + +instance ToHornSMT (Var a) where + toHornSMT (HVar k ts _) = P.parens ("var" P.<+> "$" P.<-> F.pprint k P.<+> toHornSMT ts) + +instance ToHornSMT (Query a) where + toHornSMT q = P.vcat $ L.intersperse " " + [ P.vcat (toHornOpt <$> qOpts q) + , P.vcat (toHornNum <$> qNums q) + , P.vcat (toHornSMT <$> qQuals q) + , P.vcat (toHornSMT <$> qVars q) + , P.vcat [toHornCon x t | (x, t) <- M.toList (qCon q)] + , P.vcat (toHornSMT <$> qEqns q) + , P.vcat (toHornSMT <$> qData q) + , P.vcat (toHornSMT <$> qMats q) + , P.parens (P.vcat ["constraint", P.nest 1 (toHornSMT (qCstr q))]) + ] + where + toHornNum x = toHornMany ["numeric", toHornSMT x] + toHornOpt str = toHornMany ["fixpoint", P.text ("\"" ++ str ++ "\"")] + toHornCon x t = toHornMany ["constant", toHornSMT x, toHornSMT t] + +instance ToHornSMT F.Rewrite where + toHornSMT (F.SMeasure f d xs e) = P.parens ("match" P.<+> toHornSMT f P.<+> toHornSMT (d:xs) P.<+> toHornSMT e) + +instance ToHornSMT F.Qualifier where + toHornSMT (F.Q n xts p _) = P.parens ("qualif" P.<+> F.pprint n P.<+> toHornSMT xts P.<+> toHornSMT p) + +instance ToHornSMT F.QualParam where + toHornSMT qp = toHornSMT (F.qpSym qp, F.qpSort qp) + +instance ToHornSMT a => ToHornSMT (F.Symbol, a) where + toHornSMT (x, t) = P.parens $ F.pprint x P.<+> toHornSMT t + +instance ToHornSMT a => ToHornSMT [a] where + toHornSMT = toHornMany . fmap toHornSMT + +toHornMany :: [P.Doc] -> P.Doc +toHornMany = P.parens . P.sep -- Misc.intersperse " " + +toHornAnd :: (a -> P.Doc) -> [a] -> P.Doc +toHornAnd f xs = P.parens (P.vcat ("and" : (P.nest 1 . f <$> xs))) + +instance ToHornSMT F.Equation where + toHornSMT (F.Equ f xs e s _) = P.parens ("define" P.<+> F.pprint f P.<+> toHornSMT xs P.<+> toHornSMT s P.<+> toHornSMT e) + +instance ToHornSMT F.DataDecl where + toHornSMT (F.DDecl tc n ctors) = + P.parens $ P.vcat [ + P.text "datatype" P.<+> P.parens (toHornSMT tc P.<+> P.int n) + , P.parens (P.vcat (toHornSMT <$> ctors)) + ] + +instance ToHornSMT F.FTycon where + toHornSMT c + | c == F.listFTyCon = "list" + | otherwise = toHornSMT (F.symbol c) + +instance ToHornSMT a => ToHornSMT (F.Located a) where + toHornSMT = toHornSMT . F.val +instance ToHornSMT F.DataCtor where + toHornSMT (F.DCtor x flds) = P.parens (toHornSMT x P.<+> toHornSMT flds) + +instance ToHornSMT F.DataField where + toHornSMT (F.DField x t) = toHornSMT (F.val x, t) + +instance ToHornSMT F.Sort where + toHornSMT = toHornSort + +toHornSort :: F.Sort -> P.Doc +toHornSort (F.FVar i) = "@" P.<-> P.parens (P.int i) +toHornSort F.FInt = "Int" +toHornSort F.FReal = "Real" +toHornSort F.FFrac = "Frac" +toHornSort (F.FObj x) = toHornSMT x -- P.parens ("obj" P.<+> toHornSMT x) +toHornSort F.FNum = "num" +toHornSort t@(F.FAbs _ _) = toHornAbsApp t +toHornSort t@(F.FFunc _ _)= toHornAbsApp t +toHornSort (F.FTC c) = toHornSMT c +toHornSort t@(F.FApp _ _) = toHornFApp (F.unFApp t) + +toHornAbsApp :: F.Sort -> P.Doc +toHornAbsApp (F.functionSort -> Just (vs, ss, s)) = P.parens ("func" P.<+> P.int (length vs) P.<+> toHornSMT ss P.<+> toHornSMT s ) +toHornAbsApp _ = error "Unexpected nothing function sort" + +toHornFApp :: [F.Sort] -> P.Doc +toHornFApp [t] = toHornSMT t +toHornFApp ts = toHornSMT ts + +instance ToHornSMT F.Subst where + toHornSMT (F.Su m) = toHornSMT (Misc.hashMapToAscList m) + +instance ToHornSMT (Bind a) where + toHornSMT (Bind x t p _) = P.parens (toHornSMT (x, t) P.<+> toHornSMT p) + +instance ToHornSMT Pred where + toHornSMT (Reft p) = P.parens (toHornSMT p) + toHornSMT (Var k xs) = toHornMany (toHornSMT (F.KV k) : (toHornSMT <$> xs)) + toHornSMT (PAnd ps) = toHornMany ("and" : (toHornSMT <$> ps)) + +instance ToHornSMT F.KVar where + toHornSMT (F.KV k) = "$" P.<-> toHornSMT k + +instance ToHornSMT F.Expr where + toHornSMT = toHornExpr + +toHornExpr :: F.Expr -> P.Doc +toHornExpr (F.ESym c) = F.pprint c +toHornExpr (F.ECon c) = F.pprint c +toHornExpr (F.EVar s) = toHornSMT s +toHornExpr (F.ENeg e) = P.parens ("-" P.<+> toHornExpr e) +toHornExpr (F.EApp e1 e2) = toHornSMT [e1, e2] +toHornExpr (F.EBin o e1 e2) = toHornOp (F.toFix o) [e1, e2] +toHornExpr (F.EIte e1 e2 e3) = toHornOp "if" [e1, e2, e3] +toHornExpr (F.ECst e t) = toHornMany ["cast", toHornSMT e, toHornSMT t] +toHornExpr (F.PNot p) = toHornOp "not" [p] +toHornExpr (F.PImp e1 e2) = toHornOp "=>" [e1, e2] +toHornExpr (F.PIff e1 e2) = toHornOp "<=>" [e1, e2] +toHornExpr e@F.PTrue = F.pprint e +toHornExpr e@F.PFalse = F.pprint e +toHornExpr (F.PAnd es) = toHornOp "and" es +toHornExpr (F.POr es) = toHornOp "or" es +toHornExpr (F.PAtom r e1 e2) = toHornOp (F.toFix r) [e1, e2] +toHornExpr (F.PAll xts p) = toHornMany ["forall", toHornSMT xts, toHornSMT p] +toHornExpr (F.PExist xts p) = toHornMany ["exists", toHornSMT xts, toHornSMT p] +toHornExpr (F.ELam b e) = toHornMany ["lam", toHornSMT b, toHornSMT e] +toHornExpr (F.ECoerc a t e) = toHornMany ["coerce", toHornSMT a, toHornSMT t, toHornSMT e] +toHornExpr (F.PKVar k su) = toHornMany [toHornSMT k, toHornSMT su] +toHornExpr (F.ETApp e s) = toHornMany ["ETApp" , toHornSMT e, toHornSMT s] +toHornExpr (F.ETAbs e s) = toHornMany ["ETAbs" , toHornSMT e, toHornSMT s] +toHornExpr (F.PGrad k _ _ e) = toHornMany ["&&", toHornSMT e, toHornSMT k] + +toHornOp :: ToHornSMT a => P.Doc -> [a] -> P.Doc +toHornOp op es = toHornMany (op : (toHornSMT <$> es)) + +instance ToHornSMT (Cstr a) where + toHornSMT = toHornCstr + +toHornCstr :: Cstr a -> P.Doc +toHornCstr (Head p _) = toHornSMT p +toHornCstr (CAnd cs) = toHornAnd toHornCstr cs +toHornCstr (All b c) = P.parens (P.vcat ["forall" P.<+> toHornSMT b + , P.nest 1 (toHornCstr c)]) +toHornCstr (Any b c) = P.parens (P.vcat ["exists" P.<+> toHornSMT b + , P.nest 1 (toHornCstr c)]) diff --git a/src/Language/Fixpoint/Misc.hs b/src/Language/Fixpoint/Misc.hs --- a/src/Language/Fixpoint/Misc.hs +++ b/src/Language/Fixpoint/Misc.hs @@ -334,6 +334,9 @@ isRight (Right _) = True isRight _ = False +dbgFalse :: Bool +dbgFalse = 1 > (2 :: Int) + componentsWith :: (Ord c) => (a -> [(b, c, [c])]) -> a -> [[b]] componentsWith eF x = map (fst3 . f) <$> vss where @@ -436,4 +439,3 @@ fold1M _ [] = errorstar "fold1M with empty list" fold1M _ [x] = return x fold1M f (x1:x2:xs) = do { x <- f x1 x2; fold1M f (x:xs) } - diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs --- a/src/Language/Fixpoint/Parse.hs +++ b/src/Language/Fixpoint/Parse.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NoMonomorphismRestriction #-} @@ -15,6 +16,7 @@ -- * Some Important keyword and parsers , reserved, reservedOp + , reserved', reservedOp' , locReserved , parens , brackets, angles, braces , semi , comma @@ -22,18 +24,23 @@ , 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 @@ -68,8 +75,10 @@ , condIdR -- * Lexemes and lexemes with location + , lexeme' , lexeme , located + , locLexeme' , locLexeme , locLowerIdP , locUpperIdP @@ -98,7 +107,11 @@ , dataFieldP , dataCtorP , dataDeclP - + , fTyConP + , mkFTycon + , intP + , tvarP + , trueP, falseP, symconstP ) where import Control.Monad (unless, void) @@ -106,7 +119,9 @@ import qualified Data.IntMap.Strict as IM import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S +#if !MIN_VERSION_base(4,20,0) import Data.List (foldl') +#endif import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.Text as T import qualified Data.Text.IO as T @@ -320,26 +335,32 @@ -- 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. -- -- This is defined in such a way that it determines the actual source range -- 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 @@ -554,6 +575,11 @@ 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)) @@ -569,6 +595,11 @@ 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 @@ -742,6 +773,7 @@ expr0P = trueP -- constant "true" <|> falseP -- constant "false" + <|> (reservedOp "?" *> predP) <|> fastIfP EIte exprP -- "if-then-else", starts with "if" <|> coerceP exprP -- coercion, starts with "coerce" <|> (ESym <$> symconstP) -- string literal, starts with double-quote @@ -861,19 +893,19 @@ 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 @@ -924,6 +956,18 @@ , FInfix (Just 6) "+" (Just $ EBin Plus) AssocLeft , FInfix (Just 5) "mod" (Just $ EBin Mod) AssocLeft -- Haskell gives mod 7 , FInfix (Just 9) "." applyCompose AssocRight + -- -- + -- , FInfix (Just 4) "<" (Just $ PAtom Lt) AssocNone + -- , FInfix (Just 4) "==" (Just $ PAtom Eq) AssocNone + -- , FInfix (Just 4) "=" (Just $ PAtom Eq) AssocNone + -- , FInfix (Just 4) "~~" (Just $ PAtom Ueq) AssocNone + -- , FInfix (Just 4) "!=" (Just $ PAtom Ne) AssocNone + -- , FInfix (Just 4) "/=" (Just $ PAtom Ne) AssocNone + -- , FInfix (Just 4) "!~" (Just $ PAtom Une) AssocNone + -- , FInfix (Just 4) "<" (Just $ PAtom Lt) AssocNone + -- , FInfix (Just 4) "<=" (Just $ PAtom Le) AssocNone + -- , FInfix (Just 4) ">" (Just $ PAtom Gt) AssocNone + -- , FInfix (Just 4) ">=" (Just $ PAtom Ge) AssocNone ] applyCompose :: Maybe (Expr -> Expr -> Expr) applyCompose = (\f x y -> f `eApps` [x,y]) <$> cmpFun @@ -933,7 +977,7 @@ -- Andres, TODO: Why is this so complicated? -- funAppP :: Parser Expr -funAppP = litP <|> exprFunP <|> simpleAppP +funAppP = litP <|> exprFunP <|> simpleAppP where exprFunP = mkEApp <$> funSymbolP <*> funRhsP funRhsP = some expr0P @@ -1016,7 +1060,6 @@ = (reserved "int" >> return intFTyCon) <|> (reserved "Integer" >> return intFTyCon) <|> (reserved "Int" >> return intFTyCon) - -- <|> (reserved "int" >> return intFTyCon) -- TODO:AZ duplicate? <|> (reserved "real" >> return realFTyCon) <|> (reserved "bool" >> return boolFTyCon) <|> (reserved "num" >> return numFTyCon) diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs --- a/src/Language/Fixpoint/Smt/Interface.hs +++ b/src/Language/Fixpoint/Smt/Interface.hs @@ -245,7 +245,7 @@ hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64 me <- makeContext' cfg $ Just hLog pre <- smtPreamble cfg (solver cfg) me - mapM_ (SMTLIB.Backends.command_ (ctxSolver me)) pre + mapM_ (\l -> SMTLIB.Backends.command_ (ctxSolver me) l >> BS.hPutBuilder hLog l >> LBS.hPutStr hLog "\n") pre return me where smtFile = extFileName Smt2 f diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs --- a/src/Language/Fixpoint/Smt/Theories.hs +++ b/src/Language/Fixpoint/Smt/Theories.hs @@ -32,8 +32,12 @@ -- * Theories , setEmpty, setEmp, setCap, setSub, setAdd, setMem - , setCom, setCup, setDif, setSng, mapSel, mapCup, mapSto, mapDef + , setCom, setCup, setDif, setSng + , mapSel, mapCup, mapSto, mapDef + + , arrConst, arrStore, arrSelect, arrMapNot, arrMapOr, arrMapAnd, arrMapImp + -- * Query Theories , isSmt2App , axiomLiterals @@ -63,6 +67,8 @@ -- | Theory Symbols ------------------------------------------------------------ -------------------------------------------------------------------------------- +-- TODO drop all of Set and Map symbols when Map is handled through arrays + -- "set" is currently \"LSet\" instead of just \"Set\" because Z3 has its own -- \"Set\" since 4.8.5 elt, set, map :: Raw @@ -70,17 +76,8 @@ set = "LSet" map = "Map" -emp, sng, add, cup, cap, mem, dif, sub, com, sel, sto, mcup, mdef, mprj :: Raw +sel, sto, mcup, mdef, mprj :: Raw mToSet, mshift, mmax, mmin :: Raw -emp = "smt_set_emp" -sng = "smt_set_sng" -add = "smt_set_add" -cup = "smt_set_cup" -cap = "smt_set_cap" -mem = "smt_set_mem" -dif = "smt_set_dif" -sub = "smt_set_sub" -com = "smt_set_com" sel = "smt_map_sel" sto = "smt_map_sto" mcup = "smt_map_cup" @@ -146,8 +143,7 @@ bvSGtName = "bvsgt" bvSGeName = "bvsge" -setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup :: Symbol -setDif, setSng :: Symbol +setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a -- Symbol setEmpty = "Set_empty" setEmp = "Set_emp" setCap = "Set_cap" @@ -159,17 +155,43 @@ setDif = "Set_dif" setSng = "Set_sng" -mapSel, mapSto, mapCup, mapDef, mapPrj, mapToSet :: Symbol -mapMax, mapMin, mapShift :: Symbol +--- Array operations +arrConst, arrStore, arrSelect, arrMapNot, arrMapOr, arrMapAnd, arrMapImp :: Symbol +arrConst = "const" +arrStore = "store" +arrSelect = "select" +arrMapNot = "arr_map_not" +arrMapOr = "arr_map_or" +arrMapAnd = "arr_map_and" +arrMapImp = "arr_map_imp" + +mapSel, mapSto, mapCup, mapDef, mapMax, mapMin, mapShift :: Symbol mapSel = "Map_select" mapSto = "Map_store" mapCup = "Map_union" mapMax = "Map_union_max" mapMin = "Map_union_min" mapDef = "Map_default" -mapPrj = "Map_project" mapShift = "Map_shift" -- See [Map key shift] + +-- [Map key shift] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- Function mapShift: Add an integer to all keys in a map. Type signature: +-- mapShift : Int -> Map Int v -> Map Int v +-- Let's call the first argument (the shift amount) N, the second argument K1, +-- and the result K2. For all indices i, we have K2[i] = K1[i - N]. +-- This is implemented with Z3's lambda, which lets us construct an array +-- from a function. +-- +-- [Map max and min] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- Functions mapMax and mapMin: Union two maps, combining the elements by +-- taking either the greatest (mapMax) or the least (mapMin) of them. +-- mapMax, mapMin : Map v Int -> Map v Int -> Map v Int + +mapToSet, mapPrj :: Symbol mapToSet = "Map_to_set" +mapPrj = "Map_project" -- [Interaction between Map and Set] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -188,21 +210,6 @@ -- then the key (along with its associated value in the map) are preserved -- in the output. Keys not present in the set are mapped to zero. Keys not -- present in the set are mapped to zero. --- --- [Map key shift] --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ --- Function mapShift: Add an integer to all keys in a map. Type signature: --- mapShift : Int -> Map Int v -> Map Int v --- Let's call the first argument (the shift amount) N, the second argument K1, --- and the result K2. For all indices i, we have K2[i] = K1[i - N]. --- This is implemented with Z3's lambda, which lets us construct an array --- from a function. --- --- [Map max and min] --- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ --- Functions mapMax and mapMin: Union two maps, combining the elements by --- taking either the greatest (mapMax) or the least (mapMin) of them. --- mapMax, mapMin : Map v Int -> Map v Int -> Map v Int strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol strLen = "strLen" @@ -242,42 +249,6 @@ "Int" , bSort set (key2 "Array" (fromText elt) "Bool") - , bFun emp - [] - (fromText set) - (parens (key "as const" (fromText set) <+> "false")) - , bFun sng - [("x", fromText elt)] - (fromText set) - (key3 "store" (parens (key "as const" (fromText set) <+> "false")) "x" "true") - , bFun mem - [("x", fromText elt), ("s", fromText set)] - "Bool" - "(select s x)" - , bFun add - [("s", fromText set), ("x", fromText elt)] - (fromText set) - "(store s x true)" - , bFun cup - [("s1", fromText set), ("s2", fromText set)] - (fromText set) - "((_ map or) s1 s2)" - , bFun cap - [("s1", fromText set), ("s2", fromText set)] - (fromText set) - "((_ map and) s1 s2)" - , bFun com - [("s", fromText set)] - (fromText set) - "((_ map not) s)" - , bFun dif - [("s1", fromText set), ("s2", fromText set)] - (fromText set) - (key2 (fromText cap) "s1" (key (fromText com) "s2")) - , bFun sub - [("s1", fromText set), ("s2", fromText set)] - "Bool" - (key2 "=" (fromText emp) (key2 (fromText dif) "s1" "s2")) -- Maps , bSort map @@ -366,14 +337,6 @@ = [ bSort elt "Int" , bSort set "Int" , bSort string "Int" - , bFun' emp [] (fromText set) - , bFun' sng [fromText elt] (fromText set) - , bFun' add [fromText set, fromText elt] (fromText set) - , bFun' cup [fromText set, fromText set] (fromText set) - , bFun' cap [fromText set, fromText set] (fromText set) - , bFun' dif [fromText set, fromText set] (fromText set) - , bFun' sub [fromText set, fromText set] "Bool" - , bFun' mem [fromText elt, fromText set] "Bool" , bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)" ] @@ -423,6 +386,7 @@ smt2SmtSort SString = fromText string smt2SmtSort SSet = fromText set smt2SmtSort SMap = fromText map +smt2SmtSort (SArray a b) = key2 "Array" (smt2SmtSort a) (smt2SmtSort b) smt2SmtSort (SBitVec n) = key "_ BitVec" (bShow n) smt2SmtSort (SVar n) = "T" <> bShow n smt2SmtSort (SData c []) = symbolBuilder c @@ -437,13 +401,16 @@ -------------------------------------------------------------------------------- smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder -------------------------------------------------------------------------------- -smt2App _ _ (dropECst -> EVar f) [d] - | f == setEmpty = Just (fromText emp) - | f == setEmp = Just (key2 "=" (fromText emp) d) - | f == setSng = Just (key (fromText sng) d) -- Just (key2 (bb add) (bb emp) d) +smt2App _ env ex@(dropECst -> EVar f) [d] + | f == arrConst = Just (key (key "as const" (getTarget ex)) d) + where + getTarget :: Expr -> Builder + -- const is a function, but SMT expects only the output sort + getTarget (ECst _ t) = smt2SmtSort $ sortSmtSort True (seData env) (ffuncOut t) + getTarget e = bShow e -smt2App k env f (builder:builders) - | Just fb <- smt2AppArg k env f +smt2App k env ex (builder:builders) + | Just fb <- smt2AppArg k env ex = Just $ key fb (builder <> mconcat [ " " <> d | d <- builders]) smt2App _ _ _ _ = Nothing @@ -467,12 +434,8 @@ -------------------------------------------------------------------------------- isSmt2App :: SEnv TheorySymbol -> Expr -> Maybe Int -------------------------------------------------------------------------------- -isSmt2App g (dropECst -> EVar f) - | f == setEmpty = Just 1 - | f == setEmp = Just 1 - | f == setSng = Just 1 - | otherwise = lookupSEnv f g >>= thyAppInfo -isSmt2App _ _ = Nothing +isSmt2App g (dropECst -> EVar f) = lookupSEnv f g >>= thyAppInfo +isSmt2App _ _ = Nothing thyAppInfo :: TheorySymbol -> Maybe Int thyAppInfo ti = case tsInterp ti of @@ -507,17 +470,27 @@ interpSymbols :: [(Symbol, TheorySymbol)] -------------------------------------------------------------------------------- interpSymbols = - [ interpSym setEmp emp (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort) - , interpSym setEmpty emp (FAbs 0 $ FFunc intSort (setSort $ FVar 0)) - , interpSym setSng sng (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0)) - , interpSym setAdd add setAddSort - , interpSym setCup cup setBopSort - , interpSym setCap cap setBopSort - , interpSym setMem mem setMemSort - , interpSym setDif dif setBopSort - , interpSym setSub sub setCmpSort - , interpSym setCom com setCmpSort + [ + -- TODO we'll probably need two versions of these - one for sets and one for maps + interpSym arrConst "const" (FAbs 0 $ FFunc boolSort setArrSort) + , interpSym arrStore "store" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) $ FFunc boolSort setArrSort) + , interpSym arrSelect "select" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) boolSort) + , interpSym arrMapNot "(_ map not)" (FFunc setArrSort setArrSort) + , interpSym arrMapOr "(_ map or)" (FFunc setArrSort $ FFunc setArrSort setArrSort) + , interpSym arrMapAnd "(_ map and)" (FFunc setArrSort $ FFunc setArrSort setArrSort) + , interpSym arrMapImp "(_ map =>)" (FFunc setArrSort $ FFunc setArrSort setArrSort) + , interpSym setEmp setEmp (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort) + , interpSym setEmpty setEmpty (FAbs 0 $ FFunc intSort (setSort $ FVar 0)) + , interpSym setSng setSng (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0)) + , interpSym setAdd setAdd setAddSort + , interpSym setCup setCup setBopSort + , interpSym setCap setCap setBopSort + , interpSym setMem setMem setMemSort + , interpSym setDif setDif setBopSort + , interpSym setSub setSub setCmpSort + , interpSym setCom setCom setCmpSort + , interpSym mapSel sel mapSelSort , interpSym mapSto sto mapStoSort , interpSym mapCup mcup mapCupSort @@ -527,6 +500,7 @@ , interpSym mapPrj mprj mapPrjSort , interpSym mapShift mshift mapShiftSort , interpSym mapToSet mToSet mapToSetSort + -- , interpSym bvOrName "bvor" bvBopSort -- , interpSym bvAndName "bvand" bvBopSort -- , interpSym bvAddName "bvadd" bvBopSort @@ -589,14 +563,17 @@ ] where + setArrSort = arraySort (FVar 0) boolSort -- (sizedBitVecSort "Size1") bv32 = sizedBitVecSort "Size32" bv64 = sizedBitVecSort "Size64" boolInt = boolToIntName + setAddSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (FVar 0) (setSort $ FVar 0) setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0) setMemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort setCmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort + -- select :: forall i a. Map i a -> i -> a mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1)) $ FFunc (FVar 0) (FVar 1) 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 @@ -28,6 +28,7 @@ import qualified Data.HashMap.Strict as HashMap import qualified Data.Store as S import Data.Aeson (ToJSON, encode) +import qualified Data.List as L import qualified Data.Text.Lazy.IO as LT import qualified Data.Text.Lazy.Encoding as LT import System.Exit (ExitCode (..)) @@ -189,10 +190,17 @@ crashResult m err' = Result res mempty mempty mempty where res = Crash es msg - es = catMaybes [ findError m e | e <- errs err' ] - msg | null es = showpp err' - | otherwise = "Sorry, unexpected panic in liquid-fixpoint!" -- ++ showpp e + es = catMaybes [ findError m e | e <- ers ] + ers = errs err' + msg | null ers = "Sorry, unexpected panic in liquid-fixpoint!" + -- {-dbgFalse-} True = "Sorry, unexpected panic in liquid-fixpoint!\n" ++ crashMessage es + | otherwise = showpp err' +_crashMessage :: [((Integer, a), Maybe String) ] -> String +_crashMessage es = L.intercalate "\n" [ msg i s | ((i,_), Just s) <- es ] + where + msg i s = "Error in constraint " ++ show i ++ ":\n" ++ s + -- | Unpleasant hack to save meta-data that can be recovered from SrcSpan type ErrorMap a = HashMap.HashMap SrcSpan a @@ -234,13 +242,16 @@ -- rnf si1 `seq` donePhase Loud "Validated Constraints" graphStatistics cfg si1 let si2 = {- SCC "wfcUniqify" -} wfcUniqify $!! si1 + -- writeLoud $ "fq file after wfcUniqify: \n" ++ render (toFixpoint cfg si2) let si3 = {- SCC "renameAll" -} renameAll $!! si2 rnf si3 `seq` whenLoud $ donePhase Loud "Uniqify & Rename" loudDump 1 cfg si3 let si4 = {- SCC "defunction" -} defunctionalize cfg $!! si3 + -- writeLoud $ "fq file after defunc: \n" ++ render (toFixpoint cfg si4) -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4) loudDump 2 cfg si4 let si5 = {- SCC "elaborate" -} elaborate (atLoc dummySpan "solver") (symbolEnv cfg si4) si4 + -- writeLoud $ "fq file after elaborate: \n" ++ render (toFixpoint cfg si5) loudDump 3 cfg si5 let si6 = if extensionality cfg then {- SCC "expand" -} expand cfg si5 else si5 if rewriteAxioms cfg && noLazyPLE cfg diff --git a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs --- a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs +++ b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-} @@ -30,7 +30,11 @@ import qualified Data.HashMap.Strict as HashMap.Strict import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet +#if MIN_VERSION_base(4,20,0) +import Data.List (nub, partition) +#else import Data.List (foldl', nub, partition) +#endif import Data.Maybe (fromMaybe) import Data.ShareMap (ShareMap) import qualified Data.ShareMap as ShareMap diff --git a/src/Language/Fixpoint/Solver/Extensionality.hs b/src/Language/Fixpoint/Solver/Extensionality.hs --- a/src/Language/Fixpoint/Solver/Extensionality.hs +++ b/src/Language/Fixpoint/Solver/Extensionality.hs @@ -10,7 +10,9 @@ import Control.Monad.State import qualified Data.HashMap.Strict as M import Data.Maybe (fromMaybe) +#if !MIN_VERSION_base(4,20,0) import Data.List (foldl') +#endif import Language.Fixpoint.Types.Config import Language.Fixpoint.SortCheck @@ -201,7 +203,7 @@ where -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?) d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc tupConName)) 2 [ct] -#if MIN_TOOL_VERSION_ghc(9,6,0) +#if MIN_TOOL_VERSION_ghc(9,6,0) && !MIN_TOOL_VERSION_ghc(9,10,0) ct = DCtor (dummyLoc (symbol "GHC.Tuple.Prim.(,)")) [ DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$1")) (FVar 0) , DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$2")) (FVar 1) diff --git a/src/Language/Fixpoint/Solver/Interpreter.hs b/src/Language/Fixpoint/Solver/Interpreter.hs --- a/src/Language/Fixpoint/Solver/Interpreter.hs +++ b/src/Language/Fixpoint/Solver/Interpreter.hs @@ -17,8 +17,6 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ExistentialQuantification #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - module Language.Fixpoint.Solver.Interpreter ( instInterpreter @@ -62,25 +60,25 @@ instInterpreter cfg fi' subcIds = do let cs = M.filterWithKey (\i c -> isPleCstr aEnv i c && maybe True (i `L.elem`) subcIds) - (cm fi) + (cm info) let t = mkCTrie (M.toList cs) -- 1. BUILD the Trie res <- withProgress (1 + M.size cs) $ - pleTrie t $ instEnv fi cs sEnv -- 2. TRAVERSE Trie to compute InstRes - return $ resSInfo cfg sEnv fi res -- 3. STRENGTHEN SInfo using InstRes + pleTrie t $ instEnv info cs sEnv -- 2. TRAVERSE Trie to compute InstRes + return $ resSInfo cfg sEnv info res -- 3. STRENGTHEN SInfo using InstRes where - sEnv = symbolEnv cfg fi - aEnv = ae fi - fi = normalize fi' + sEnv = symbolEnv cfg info + aEnv = ae info + info = normalize fi' ------------------------------------------------------------------------------- -- | Step 1a: @instEnv@ sets up the incremental-PLE environment instEnv :: (Loc a) => SInfo a -> CMap (SimpC a) -> SymEnv -> InstEnv a -instEnv fi cs sEnv = InstEnv bEnv aEnv cs γ s0 +instEnv info cs sEnv = InstEnv bEnv aEnv cs γ s0 where csBinds = M.foldl' (\acc c -> unionIBindEnv acc (senv c)) emptyIBindEnv cs - bEnv = filterBindEnv (\i _ _ -> memberIBindEnv i csBinds) (bs fi) - aEnv = ae fi - γ = knowledge fi + bEnv = filterBindEnv (\i _ _ -> memberIBindEnv i csBinds) (bs info) + aEnv = ae info + γ = knowledge info s0 = EvalEnv sEnv mempty ---------------------------------------------------------------------------------------------- @@ -180,7 +178,7 @@ ---------------------------------------------------------------------------------------------- resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a -resSInfo cfg env fi res = strengthenBinds fi res' +resSInfo cfg env info res = strengthenBinds info res' where res' = M.fromList $ zip is ps'' ps'' = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps' @@ -288,12 +286,12 @@ , EVar x /= c ] makeCandidates :: Knowledge -> ICtx -> Expr -> [Expr] -makeCandidates γ ctx expr +makeCandidates k ctx exprs = mytracepp ("\n" ++ show (length cands) ++ " New Candidates") cands where cands = - filter (\e -> isRedex γ e && not (e `S.member` icSolved ctx)) (notGuardedApps expr) ++ - filter (\e -> hasConstructors γ e && not (e `S.member` icSolved ctx)) (largestApps expr) + filter (\e -> isRedex k e && not (e `S.member` icSolved ctx)) (notGuardedApps exprs) ++ + filter (\e -> hasConstructors k e && not (e `S.member` icSolved ctx)) (largestApps exprs) -- Constructor occurrences need to be considered as candidadates since -- they identify relevant measure equations. The function 'rewrite' @@ -323,7 +321,7 @@ getCstr env cid = Misc.safeLookup "Instantiate.getCstr" cid env isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool -isPleCstr aenv sid c = isTarget c && M.lookupDefault False sid (aenvExpand aenv) +isPleCstr aenv subid c = isTarget c && M.lookupDefault False subid (aenvExpand aenv) type EvAccum = S.HashSet (Expr, Expr) @@ -432,14 +430,14 @@ mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub mkCoSub env eTs xTs = M.fromList [ (x, unite ys) | (x, ys) <- Misc.groupList xys ] where - unite ts = Mb.fromMaybe (uError ts) (unifyTo1 senv ts) - senv = mkSearchEnv env + unite ts = Mb.fromMaybe (uError ts) (unifyTo1 symToSearch ts) + symToSearch = mkSearchEnv env uError ts = panic ("mkCoSub: cannot build CoSub for " ++ showpp xys ++ " cannot unify " ++ showpp ts) xys = Misc.sortNub $ concat $ zipWith matchSorts _xTs _eTs (_xTs,_eTs) = (xTs, eTs) matchSorts :: Sort -> Sort -> [(Symbol, Sort)] -matchSorts s1 s2 = go s1 s2 +matchSorts = go where go (FObj x) {-FObj-} y = [(x, y)] go (FAbs _ t1) (FAbs _ t2) = go t1 t2 @@ -465,18 +463,18 @@ interpret ie γ ctx env (EApp e1 e2) | isSetPred e1 = let e2' = interpret' ie γ ctx env e2 in applySetFolding e1 e2' -interpret ie γ ctx env e@(EApp _ _) = case splitEApp e of - (f, es) -> let g = interpret' ie γ ctx env in - interpretApp ie γ ctx env (g f) (map g es) +interpret cmap know ictx ssenv e@(EApp _ _) = case splitEApp e of + (exprs, exprses) -> let g = interpret' cmap know ictx ssenv in + interpretApp cmap know ictx ssenv (g exprs) (map g exprses) where interpretApp ie γ ctx env (EVar f) es | Just eq <- M.lookup f (knAms γ) , length (eqArgs eq) <= length es = let (es1,es2) = splitAt (length (eqArgs eq)) es ges = substEq env eq es1 - exp = unfoldExpr ie γ ctx env ges - exp' = eApps exp es2 in --exp' -- TODO undo - if eApps (EVar f) es == exp' then exp' else interpret' ie γ ctx env exp' + exp1 = unfoldExpr ie γ ctx env ges + exp2 = eApps exp1 es2 in --exp' -- TODO undo + if eApps (EVar f) es == exp2 then exp2 else interpret' ie γ ctx env exp2 interpretApp ie γ ctx env (EVar f) (e1:es) | (EVar dc, as) <- splitEApp e1 @@ -511,7 +509,7 @@ ELam (x, s) e' interpret ie γ ctx env (ETApp e1 t) = let e1' = interpret' ie γ ctx env e1 in ETApp e1' t interpret ie γ ctx env (ETAbs e1 sy) = let e1' = interpret' ie γ ctx env e1 in ETAbs e1' sy -interpret ie γ ctx env (PAnd es) = let es' = map (interpret' ie γ ctx env) es in go [] (reverse es') +interpret ie γ ctx env (PAnd exprses) = let es' = map (interpret' ie γ ctx env) exprses in go [] (reverse es') where go [] [] = PTrue go [p] [] = interpret' ie γ ctx env p @@ -519,7 +517,7 @@ go acc (PTrue:es) = go acc es go _ (PFalse:_) = PFalse go acc (e:es) = go (e:acc) es -interpret ie γ ctx env (POr es) = let es' = map (interpret' ie γ ctx env) es in go [] (reverse es') +interpret ie γ ctx env (POr exprses) = let es' = map (interpret' ie γ ctx env) exprses in go [] (reverse es') where go [] [] = PFalse go [p] [] = interpret' ie γ ctx env p @@ -575,20 +573,20 @@ } knowledge :: SInfo a -> Knowledge -knowledge si = KN +knowledge info = KN { knSims = M.fromList $ (\r -> ((smName r, smDC r), r)) <$> sims , knAms = M.fromList $ (\a -> (eqName a, a)) <$> aenvEqs aenv , knLams = [] , knSummary = ((\s -> (smName s, 1)) <$> sims) ++ ((\s -> (eqName s, length (eqArgs s))) <$> aenvEqs aenv) - , knDCs = S.fromList (smDC <$> sims) <> constNames si - , knAllDCs = S.fromList $ val . dcName <$> concatMap ddCtors (ddecls si) + , knDCs = S.fromList (smDC <$> sims) <> constNames info + , knAllDCs = S.fromList $ val . dcName <$> concatMap ddCtors (ddecls info) , knSels = M.fromList $ Mb.mapMaybe makeSel sims , knConsts = M.fromList $ Mb.mapMaybe makeCons sims } where sims = aenvSimpl aenv - aenv = ae si + aenv = ae info makeCons rw | null (syms $ smBody rw) @@ -631,9 +629,9 @@ instance Simplifiable Expr where - simplify γ ictx e = mytracepp ("simplification of " ++ show e) $ fix (Vis.mapExpr tx) e + simplify γ ictx exprs = mytracepp ("simplification of " ++ show exprs) $ fix' (Vis.mapExpr tx) exprs where - fix f e = if e == e' then e else fix f e' where e' = f e + fix' f e = if e == e' then e else fix' f e' where e' = f e tx e | Just e' <- M.lookup e (icSimpl ictx) = e' @@ -660,7 +658,7 @@ , (EVar dc', es) <- splitEApp a , dc == dc' = es!!i - tx (PAnd es) = go [] (reverse es) + tx (PAnd exprses) = go [] (reverse exprses) where go [] [] = PTrue go [p] [] = p @@ -669,7 +667,7 @@ | e == PTrue = go acc es | e == PFalse = PFalse | otherwise = go (e:acc) es - tx (POr es) = go [] (reverse es) + tx (POr exprses) = go [] (reverse exprses) where go [] [] = PFalse go [p] [] = p diff --git a/src/Language/Fixpoint/Solver/Monad.hs b/src/Language/Fixpoint/Solver/Monad.hs --- a/src/Language/Fixpoint/Solver/Monad.hs +++ b/src/Language/Fixpoint/Solver/Monad.hs @@ -89,7 +89,7 @@ file = C.srcFile cfg -- only linear arithmentic when: linear flag is on or solver /= Z3 -- lar = linear cfg || Z3 /= solver cfg - fi = (siQuery sI) {F.hoInfo = F.HOI (C.allowHO cfg) (C.allowHOqs cfg)} + fi = (siQuery sI) {F.hoInfo = F.cfgHoInfo cfg } -------------------------------------------------------------------------------- diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -16,8 +16,6 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ExistentialQuantification #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - module Language.Fixpoint.Solver.PLE ( instantiate @@ -78,31 +76,31 @@ instantiate cfg fi' subcIds = do let cs = M.filterWithKey (\i c -> isPleCstr aEnv i c && maybe True (i `L.elem`) subcIds) - (cm fi) + (cm info) let t = mkCTrie (M.toList cs) -- 1. BUILD the Trie res <- withRESTSolver $ \solver -> withProgress (1 + M.size cs) $ withCtx cfg file sEnv $ \ctx -> do - env <- instEnv cfg fi cs solver ctx + env <- instEnv cfg info cs solver ctx pleTrie t env -- 2. TRAVERSE Trie to compute InstRes - savePLEEqualities cfg fi sEnv res - return $ resSInfo cfg sEnv fi res -- 3. STRENGTHEN SInfo using InstRes + savePLEEqualities cfg info sEnv res + return $ resSInfo cfg sEnv info res -- 3. STRENGTHEN SInfo using InstRes where withRESTSolver :: (Maybe SolverHandle -> IO a) -> IO a withRESTSolver f | all null (M.elems $ aenvAutoRW aEnv) = f Nothing withRESTSolver f = withZ3 (f . Just) file = srcFile cfg ++ ".evals" - sEnv = symbolEnv cfg fi - aEnv = ae fi - fi = normalize fi' + sEnv = symbolEnv cfg info + aEnv = ae info + info = normalize fi' savePLEEqualities :: Config -> SInfo a -> SymEnv -> InstRes -> IO () -savePLEEqualities cfg fi sEnv res = when (save cfg) $ do +savePLEEqualities cfg info sEnv res = when (save cfg) $ do let fq = queryFile Files.Fq cfg ++ ".ple" putStrLn $ "\nSaving PLE equalities: " ++ fq ++ "\n" Misc.ensurePath fq let constraint_equalities = - map equalitiesPerConstraint $ Misc.hashMapToAscList $ cm fi + map equalitiesPerConstraint $ Misc.hashMapToAscList $ cm info writeFile fq $ render $ vcat $ map renderConstraintRewrite constraint_equalities where @@ -123,12 +121,12 @@ ------------------------------------------------------------------------------- -- | Step 1a: @instEnv@ sets up the incremental-PLE environment instEnv :: (Loc a) => Config -> SInfo a -> CMap (SimpC a) -> Maybe SolverHandle -> SMT.Context -> IO (InstEnv a) -instEnv cfg fi cs restSolver ctx = do +instEnv cfg info cs restSolver ctx = do refRESTCache <- newIORef mempty refRESTSatCache <- newIORef mempty let - restOC = FC.restOC cfg - oc0 = ordConstraints restOC $ Mb.fromJust restSolver + restOrd = FC.restOC cfg + oc0 = ordConstraints restOrd $ Mb.fromJust restSolver oc :: OCAlgebra OCType RuntimeTerm IO oc = oc0 { OC.isSat = cachedIsSat refRESTSatCache oc0 @@ -150,16 +148,16 @@ , evFuel = defFuelCount cfg , explored = Just et , restSolver = restSolver - , restOCA = restOC + , restOCA = restOrd , evOCAlgebra = oc } return $ InstEnv { ieCfg = cfg , ieSMT = ctx - , ieBEnv = bs fi - , ieAenv = ae fi + , ieBEnv = bs info + , ieAenv = ae info , ieCstrs = cs - , ieKnowl = knowledge cfg ctx fi + , ieKnowl = knowledge cfg ctx info , ieEvEnv = s0 } where @@ -342,7 +340,7 @@ ---------------------------------------------------------------------------------------------- resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a -resSInfo cfg env fi res = strengthenBinds fi res' +resSInfo cfg env info res = strengthenBinds info res' where res' = M.fromList $ zip is ps'' ps'' = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps' @@ -447,7 +445,7 @@ getCstr env cid = Misc.safeLookup "Instantiate.getCstr" cid env isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool -isPleCstr aenv sid c = isTarget c && M.lookupDefault False sid (aenvExpand aenv) +isPleCstr aenv subid c = isTarget c && M.lookupDefault False subid (aenvExpand aenv) type EvEqualities = S.HashSet (Expr, Expr) @@ -576,9 +574,9 @@ -- Just evaluate the arguments first, to give rewriting a chance to step in -- if necessary do - (es', fe) <- feSeq <$> mapM (eval γ ctx et) es + (es', finalExpand) <- feSeq <$> mapM (eval γ ctx et) es if es /= es' - then return (eApps f es', fe) + then return (eApps f es', finalExpand) else do (f', fe) <- eval γ ctx et f (me', fe') <- evalApp γ ctx f' es et @@ -679,7 +677,7 @@ evalRESTWithCache cacheRef γ ctx acc rp = do Just exploredTerms <- gets explored - se <- liftIO (shouldExploreTerm exploredTerms e) + se <- liftIO (shouldExploreTerm exploredTerms exprs) if se then do possibleRWs <- getRWs rws <- notVisitedFirst exploredTerms <$> filterM (liftIO . allowed) possibleRWs @@ -688,10 +686,10 @@ -- liftIO $ putStrLn $ (show $ length possibleRWs) ++ " rewrites allowed at path length " ++ (show $ (map snd $ path rp)) (e', FE fe) <- do - r@(ec, _) <- eval γ ctx FuncNormal e - if ec /= e + r@(ec, _) <- eval γ ctx FuncNormal exprs + if ec /= exprs then return r - else eval γ ctx RWNormal e + else eval γ ctx RWNormal exprs let evalIsNewExpr = e' `L.notElem` pathExprs let exprsToAdd = [e' | evalIsNewExpr] ++ map (\(_, e, _) -> e) rws @@ -704,7 +702,7 @@ st { evNewEqualities = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd , evSMTCache = smtCache , explored = Just $ ExploredTerms.insert - (Rewrite.convert e) + (Rewrite.convert exprs) (c rp) (S.insert (Rewrite.convert e') $ S.fromList (map (Rewrite.convert . (\(_, e, _) -> e)) possibleRWs)) (Mb.fromJust $ explored st) @@ -712,8 +710,8 @@ acc'' <- if evalIsNewExpr then if fe && any isRW (path rp) - then (:[]) . fst <$> eval γ (addConst (e, e')) NoRW e' - else evalRESTWithCache cacheRef γ (addConst (e, e')) acc' (rpEval newEqualities e') + then (:[]) . fst <$> eval γ (addConst (exprs, e')) NoRW e' + else evalRESTWithCache cacheRef γ (addConst (exprs, e')) acc' (rpEval newEqualities e') else return acc' foldM (\r rw -> evalRESTWithCache cacheRef γ ctx r (rpRW rw)) acc'' rws @@ -753,7 +751,7 @@ rpRW (_, e', c') = rp{path = path rp ++ [(e', RW)], c = c' } pathExprs = map fst (mytracepp "EVAL2: path" $ path rp) - e = last pathExprs + exprs = last pathExprs autorws = getAutoRws γ ctx rwArgs = RWArgs (isValid cacheRef γ) $ knRWTerminationOpts γ @@ -769,7 +767,7 @@ if ok then do - let e' = deANF ctx e + let e' = deANF ctx exprs let getRW e ar = Rewrite.getRewrite (oc rp) rwArgs (c rp) e ar let getRWs' s = Mb.catMaybes <$> mapM (liftIO . runMaybeT . getRW s) autorws concat <$> mapM getRWs' (subExprs e') @@ -909,13 +907,13 @@ mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub mkCoSub env eTs xTs = M.fromList [ (x, unite ys) | (x, ys) <- Misc.groupList xys ] where - unite ts = Mb.fromMaybe (uError ts) (unifyTo1 senv ts) - senv = mkSearchEnv env + unite ts = Mb.fromMaybe (uError ts) (unifyTo1 symToSearch ts) + symToSearch = mkSearchEnv env uError ts = panic ("mkCoSub: cannot build CoSub for " ++ showpp xys ++ " cannot unify " ++ showpp ts) xys = Misc.sortNub $ concat $ zipWith matchSorts xTs eTs matchSorts :: Sort -> Sort -> [(Symbol, Sort)] -matchSorts s1 s2 = go s1 s2 +matchSorts = go where go (FObj x) {-FObj-} y = [(x, y)] go (FAbs _ t1) (FAbs _ t2) = go t1 t2 @@ -1024,9 +1022,9 @@ inRewrites :: Symbol -> Bool inRewrites e = let - syms = Mb.mapMaybe (lhsHead . arLHS) (concat $ M.elems $ aenvAutoRW aenv) + symbs = Mb.mapMaybe (lhsHead . arLHS) (concat $ M.elems $ aenvAutoRW aenv) in - e `L.elem` syms + e `L.elem` symbs lhsHead :: Expr -> Maybe Symbol lhsHead e | (ef, _) <- splitEAppThroughECst e, EVar f <- dropECst ef = Just f @@ -1111,9 +1109,9 @@ isConstant dcs e = S.null (S.difference (exprSymbolsSet e) dcs) simplify :: Knowledge -> ICtx -> Expr -> Expr -simplify γ ictx e = mytracepp ("simplification of " ++ showpp e) $ fix (Vis.mapExprOnExpr tx) e +simplify γ ictx exprs = mytracepp ("simplification of " ++ showpp exprs) $ fix' (Vis.mapExprOnExpr tx) exprs where - fix f e = if e == e' then e else fix f e' where e' = f e + fix' f e = if e == e' then e else fix' f e' where e' = f e tx e | Just e' <- M.lookup e (icSimpl ictx) = e' @@ -1179,7 +1177,7 @@ -- | Normalize the given named expression if it is recursive. normalizeBody :: Symbol -> Expr -> Expr -normalizeBody f e | f `elem` syms e = go e +normalizeBody f exprs | f `elem` syms exprs = go exprs where -- @go@ performs this simplification: -- (c => e1) /\ ((not c) => e2) --> if c then e1 else e2 diff --git a/src/Language/Fixpoint/Solver/Prettify.hs b/src/Language/Fixpoint/Solver/Prettify.hs --- a/src/Language/Fixpoint/Solver/Prettify.hs +++ b/src/Language/Fixpoint/Solver/Prettify.hs @@ -3,8 +3,6 @@ {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - -- | Functions to make environments easier to read module Language.Fixpoint.Solver.Prettify (savePrettifiedQuery) where @@ -62,18 +60,18 @@ savePrettifiedQuery :: Fixpoint a => Config -> FInfo a -> IO () -savePrettifiedQuery cfg fi = do +savePrettifiedQuery cfg info = do let fq = queryFile Files.Fq cfg `addExtension` "prettified" putStrLn $ "Saving prettified Query: " ++ fq ++ "\n" ensurePath fq - writeFile fq $ render (prettyConstraints fi) + writeFile fq $ render (prettyConstraints info) prettyConstraints :: Fixpoint a => FInfo a -> Doc -prettyConstraints fi = +prettyConstraints info = vcat $ map - (prettyConstraint (bs fi) . snd) - (sortOn fst $ HashMap.toList (cm fi)) + (prettyConstraint (bs info) . snd) + (sortOn fst $ HashMap.toList (cm info)) prettyConstraint :: Fixpoint a @@ -163,11 +161,11 @@ :: HashMap Symbol SortedReft -> SubC a -> ([(Symbol, SortedReft)], SubC a) -shortenVarNames env c = +shortenVarNames env subc = let bindsRenameMap = proposeRenamings $ HashMap.keys env env' = map (renameBind bindsRenameMap) (HashMap.toList env) in - (env', renameSubC bindsRenameMap c) + (env', renameSubC bindsRenameMap subc) where renameSubC :: HashMap Symbol Symbol -> SubC a -> SubC a renameSubC symMap c = @@ -255,7 +253,7 @@ [(_sfx, ss)] -> renameWithAppendages pfx ("", ss) sfxs -> concatMap (renameWithAppendages pfx) sfxs - renameWithAppendages pfx (sfx, ss) = zip ss $ case ss of + renameWithAppendages pfx (sfx, xs) = zip xs $ case xs of [_s] -> [pfx `suffixIfNotNull` sfx] ss -> zipWith (rename pfx sfx) [1 :: Integer ..] ss diff --git a/src/Language/Fixpoint/Solver/Rewrite.hs b/src/Language/Fixpoint/Solver/Rewrite.hs --- a/src/Language/Fixpoint/Solver/Rewrite.hs +++ b/src/Language/Fixpoint/Solver/Rewrite.hs @@ -4,8 +4,6 @@ {-# LANGUAGE PatternGuards #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - module Language.Fixpoint.Solver.Rewrite ( getRewrite , subExprs @@ -85,7 +83,7 @@ asLPO (LPO t) = t asLPO _ = undefined -ordConstraints (RESTFuel n) _ = bimapConstraints Fuel asFuel $ fuelOC n +ordConstraints (RESTFuel m) _ = bimapConstraints Fuel asFuel $ fuelOC m where asFuel (Fuel n) = n asFuel _ = undefined diff --git a/src/Language/Fixpoint/Solver/Sanitize.hs b/src/Language/Fixpoint/Solver/Sanitize.hs --- a/src/Language/Fixpoint/Solver/Sanitize.hs +++ b/src/Language/Fixpoint/Solver/Sanitize.hs @@ -4,8 +4,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternGuards #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - module Language.Fixpoint.Solver.Sanitize ( -- * Transform FInfo to enforce invariants sanitize @@ -41,10 +39,7 @@ -------------------------------------------------------------------------------- sanitize :: Config -> F.SInfo a -> SanitizeM (F.SInfo a) -------------------------------------------------------------------------------- -sanitize cfg = -- banIllScopedKvars - -- Misc.fM dropAdtMeasures - -- >=> - banIrregularData +sanitize cfg = banIrregularData >=> Misc.fM dropFuncSortedShadowedBinders >=> Misc.fM sanitizeWfC >=> Misc.fM replaceDeadKvars @@ -335,14 +330,14 @@ prims = Thy.theorySymbols . F.ddecls $ fi cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol] -cNoFreeVars fi known c = if S.null fv then Nothing else Just (S.toList fv) +cNoFreeVars fi knownSym c = if S.null fv then Nothing else Just (S.toList fv) where be = F.bs fi ids = F.elemsIBindEnv $ F.senv c cDom = [Misc.fst3 $ F.lookupBindEnv i be | i <- ids] cRng = concat [S.toList . F.reftFreeVars . F.sr_reft . Misc.snd3 $ F.lookupBindEnv i be | i <- ids] ++ F.syms (F.crhs c) - fv = (`Misc.nubDiff` cDom) . filter (not . known) $ cRng + fv = (`Misc.nubDiff` cDom) . filter (not . knownSym) $ cRng badCs :: Misc.ListNE (F.SimpC a, [F.Symbol]) -> E.Error badCs = E.catErrors . map (E.errFreeVarInConstraint . Misc.mapFst F.subcId) @@ -410,7 +405,7 @@ tEnv = Thy.theorySymbols ds ds = F.ddecls si ts = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv]) - sEnv = (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts + sEnv = F.coerceSortEnv $ (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts xts = symbolSorts cfg si ++ alits lits = F.dLits si `F.unionSEnv'` F.fromListSEnv alits alits = litsAEnv $ F.ae si diff --git a/src/Language/Fixpoint/Solver/Simplify.hs b/src/Language/Fixpoint/Solver/Simplify.hs --- a/src/Language/Fixpoint/Solver/Simplify.hs +++ b/src/Language/Fixpoint/Solver/Simplify.hs @@ -8,8 +8,6 @@ {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE ViewPatterns #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - module Language.Fixpoint.Solver.Simplify (applyBooleanFolding, applyConstantFolding, applySetFolding, isSetPred) where import Language.Fixpoint.Types hiding (simplify) @@ -20,20 +18,20 @@ applyBooleanFolding :: Brel -> Expr -> Expr -> Expr -applyBooleanFolding brel e1 e2 = +applyBooleanFolding brel' e1 e2 = case (e1, e2) of (ECon (R left), ECon (R right)) -> - Mb.fromMaybe e (bfR brel left right) + Mb.fromMaybe e (bfR brel' left right) (ECon (R left), ECon (I right)) -> - Mb.fromMaybe e (bfR brel left (fromIntegral right)) + Mb.fromMaybe e (bfR brel' left (fromIntegral right)) (ECon (I left), ECon (R right)) -> - Mb.fromMaybe e (bfR brel (fromIntegral left) right) + Mb.fromMaybe e (bfR brel' (fromIntegral left) right) (ECon (I left), ECon (I right)) -> - Mb.fromMaybe e (bfI brel left right) + Mb.fromMaybe e (bfI brel' left right) _ -> if isTautoPred e then PTrue else if isContraPred e then PFalse else e where - e = PAtom brel e1 e2 + e = PAtom brel' e1 e2 getOp :: Ord a => Brel -> (a -> a -> Bool) getOp Gt = (>) @@ -55,28 +53,28 @@ -- | Replace constant integer and floating point expressions by constant values -- where possible. applyConstantFolding :: Bop -> Expr -> Expr -> Expr -applyConstantFolding bop e1 e2 = +applyConstantFolding bop' e1 e2 = case (dropECst e1, dropECst e2) of (ECon (R left), ECon (R right)) -> - Mb.fromMaybe e (cfR bop left right) + Mb.fromMaybe e (cfR bop' left right) (ECon (R left), ECon (I right)) -> - Mb.fromMaybe e (cfR bop left (fromIntegral right)) + Mb.fromMaybe e (cfR bop' left (fromIntegral right)) (ECon (I left), ECon (R right)) -> - Mb.fromMaybe e (cfR bop (fromIntegral left) right) + Mb.fromMaybe e (cfR bop' (fromIntegral left) right) (ECon (I left), ECon (I right)) -> - Mb.fromMaybe e (cfI bop left right) + Mb.fromMaybe e (cfI bop' left right) (EBin Mod _ _ , _) -> e (EBin bop1 e11 (dropECst -> ECon (R left)), ECon (R right)) - | bop == bop1 -> maybe e (EBin bop e11) (cfR (rop bop) left right) + | bop' == bop1 -> maybe e (EBin bop' e11) (cfR (rop bop') left right) | otherwise -> e (EBin bop1 e11 (dropECst -> ECon (R left)), ECon (I right)) - | bop == bop1 -> maybe e (EBin bop e11) (cfR (rop bop) left (fromIntegral right)) + | bop' == bop1 -> maybe e (EBin bop' e11) (cfR (rop bop') left (fromIntegral right)) | otherwise -> e (EBin bop1 e11 (dropECst -> ECon (I left)), ECon (R right)) - | bop == bop1 -> maybe e (EBin bop e11) (cfR (rop bop) (fromIntegral left) right) + | bop' == bop1 -> maybe e (EBin bop' e11) (cfR (rop bop') (fromIntegral left) right) | otherwise -> e (EBin bop1 e11 (dropECst -> ECon (I left)), ECon (I right)) - | bop == bop1 -> maybe e (EBin bop e11) (cfI (rop bop) left right) + | bop' == bop1 -> maybe e (EBin bop' e11) (cfI (rop bop') left right) | otherwise -> e _ -> e where @@ -90,7 +88,7 @@ rop RDiv = RTimes rop Mod = Mod - e = EBin bop e1 e2 + e = EBin bop' e1 e2 getOp :: Num a => Bop -> Maybe (a -> a -> a) getOp Minus = Just (-) @@ -108,16 +106,16 @@ else Nothing go Nothing = Nothing - getOp' Div = Just (/) - getOp' RDiv = Just (/) - getOp' op = getOp op + getOp' Div | right /= 0 = Just (/) + getOp' RDiv | right /= 0 = Just (/) + getOp' op = getOp op cfI :: Bop -> Integer -> Integer -> Maybe Expr cfI bop left right = fmap go (getOp' bop) where go f = ECon $ I $ f left right - getOp' Mod = Just mod + getOp' Mod | right /= 0 = Just mod getOp' op = getOp op isSetPred :: Expr -> Bool @@ -129,18 +127,18 @@ -- Note: this is currently limited to sets of integer constants applySetFolding :: Expr -> Expr -> Expr -applySetFolding e1 e2 = case e1 of +applySetFolding expr1 expr2 = case expr1 of (EVar s) | s == setEmp - -> maybe e (fromBool . S.null) (evalSetI e2) + -> maybe e (fromBool . S.null) (evalSetI expr2) (EApp (EVar s) e1') | s == setMem - -> maybe e fromBool (S.member <$> getInt e1' <*> evalSetI e2) + -> maybe e fromBool (S.member <$> getInt e1' <*> evalSetI expr2) | s == setEmp - -> maybe e (fromBool . S.null) (S.difference <$> evalSetI e1' <*> evalSetI e2) + -> maybe e (fromBool . S.null) (S.difference <$> evalSetI e1' <*> evalSetI expr2) | otherwise -> e _ -> e where - e = EApp e1 e2 + e = EApp expr1 expr2 fromBool True = PTrue fromBool False = PFalse diff --git a/src/Language/Fixpoint/Solver/Solution.hs b/src/Language/Fixpoint/Solver/Solution.hs --- a/src/Language/Fixpoint/Solver/Solution.hs +++ b/src/Language/Fixpoint/Solver/Solution.hs @@ -3,8 +3,6 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - module Language.Fixpoint.Solver.Solution ( -- * Create Initial Solution init @@ -48,7 +46,7 @@ -------------------------------------------------------------------------------- init :: (F.Fixpoint a) => Config -> F.SInfo a -> S.HashSet F.KVar -> Sol.Solution -------------------------------------------------------------------------------- -init cfg si ks_ = Sol.fromList senv mempty keqs [] mempty ebs xEnv +init cfg si ks_ = Sol.fromList symEnv mempty keqs [] mempty ebs xEnv where keqs = map (refine si qcs genv) ws `using` parList rdeepseq qcs = {- trace ("init-qs-size " ++ show (length ws, length qs_, M.keys qcs_)) $ -} qcs_ @@ -57,7 +55,7 @@ ws = [ w | (k, w) <- M.toList (F.ws si), not (isGWfc w), k `S.member` ks ] ks = {- trace ("init-ks-size" ++ show (S.size ks_)) $ -} ks_ genv = instConstants si - senv = symbolEnv cfg si + symEnv = symbolEnv cfg si ebs = ebindInfo si xEnv = F.fromListSEnv [ (x, (i, F.sr_sort sr)) | (i,(x,sr,_)) <- F.bindEnvToList (F.bs si)] @@ -83,10 +81,10 @@ -------------------------------------------------------------------------------- refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind) -refine fi qs genv w = refineK (allowHOquals fi) env qs (F.wrft w) +refine info qs genv w = refineK (allowHOquals info) env qs (F.wrft w) where - env = wenv <> genv - wenv = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs fi) (F.wenv w)) + env = wenvSort <> genv + wenvSort = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs info) (F.wenv w)) instConstants :: F.SInfo a -> F.SEnv F.Sort instConstants = F.fromListSEnv . filter notLit . F.toListSEnv . F.gLits @@ -126,16 +124,14 @@ -> QCSig -> [[F.Symbol]] instKSig _ _ _ _ [] = error "Empty qsig in Solution.instKSig" -instKSig ho env v t (qp:qps) = do - (su0, i0, qs0) <- candidatesP senv [(0, t, [v])] qp - ixs <- matchP senv tyss [(i0, qs0)] (applyQPP su0 <$> qps) - -- return $ F.notracepp msg (reverse ixs) +instKSig ho env v sort' (qp:qps) = do + (su0, i0, qs0) <- candidatesP symToSrch [(0, sort', [v])] qp + ixs <- matchP symToSrch tyss [(i0, qs0)] (applyQPP su0 <$> qps) ys <- instSymbol tyss (tail $ reverse ixs) return (v:ys) where - -- msg = "instKSig " ++ F.showpp qsig tyss = zipWith (\i (t, ys) -> (i, t, ys)) [1..] (instCands ho env) - senv = (`F.lookupSEnvWithDistance` env) + symToSrch = (`F.lookupSEnvWithDistance` env) instSymbol :: [(SortIdx, a, [F.Symbol])] -> [(SortIdx, QualPattern)] -> [[F.Symbol]] instSymbol tyss = go @@ -149,22 +145,6 @@ ys <- go [ (i', applyQPSubst qsu qp') | (i', qp') <- is] return (y:ys) --- instKQ :: Bool --- -> F.SEnv F.Sort --- -> F.Symbol --- -> F.Sort --- -> F.Qualifier --- -> [Sol.EQual] --- instKQ ho env v t q = do --- (su0, qsu0, v0) <- candidates senv [(t, [v])] qp --- xs <- match senv tyss [v0] (applyQP su0 qsu0 <$> qps) --- return $ Sol.eQual q (F.notracepp msg (reverse xs)) --- where --- msg = "instKQ " ++ F.showpp (F.qName q) ++ F.showpp (F.qParams q) --- qp : qps = F.qParams q --- tyss = instCands ho env --- senv = (`F.lookupSEnvWithDistance` env) - instCands :: Bool -> F.SEnv F.Sort -> [(F.Sort, [F.Symbol])] instCands ho env = filter isOk tyss where @@ -323,19 +303,19 @@ (x, sr, _) = F.lookupBindEnv i (ceBEnv g) ebSol :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> Maybe F.Expr -ebSol g s i = case M.lookup i sebds of +ebSol g sol bindId = case M.lookup bindId sebds of Just (Sol.EbSol p) -> Just p Just (Sol.EbDef cs _) -> Just $ F.PAnd (cSol <$> cs) _ -> Nothing where - sebds = Sol.sEbd s + sebds = Sol.sEbd sol ebReft s (i,c) = exElim (Sol.sxEnv s) (senv c) i (ebindReft g s c) cSol c = if sid c == ceCid g then F.PFalse - else ebReft s' (i, c) + else ebReft s' (bindId, c) - s' = s { Sol.sEbd = M.insert i Sol.EbIncr sebds } + s' = sol { Sol.sEbd = M.insert bindId Sol.EbIncr sebds } ebindReft :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.SimpC () -> F.Pred ebindReft g s c = F.pAnd [ fst $ apply g' s bs, F.crhs c ] @@ -495,7 +475,7 @@ sp = F.srcSpan g substSort :: F.SEnv F.Sort -> S.HashSet F.Symbol -> F.Symbol -> F.Sort -> F.Sort -substSort sEnv _frees x _t = fromMaybe (err x) $ F.lookupSEnv x sEnv +substSort sEnv _frees sym _t = fromMaybe (err sym) $ F.lookupSEnv sym sEnv where err x = error $ "Solution.mkSubst: unknown binder " ++ F.showpp x diff --git a/src/Language/Fixpoint/Solver/Solve.hs b/src/Language/Fixpoint/Solver/Solve.hs --- a/src/Language/Fixpoint/Solver/Solve.hs +++ b/src/Language/Fixpoint/Solver/Solve.hs @@ -40,7 +40,7 @@ --import Debug.Trace (trace) mytrace :: String -> a -> a -mytrace _ x = {- trace -} x +mytrace _ x = {- trace s -} x -------------------------------------------------------------------------------- solve :: (NFData a, F.Fixpoint a, Show a, F.Loc a) => Config -> F.SInfo a -> IO (F.Result (Integer, a)) @@ -54,11 +54,11 @@ -- print (numIter stat) return res where - act = solve_ cfg fi s0 ks wkl - sI = solverInfo cfg fi - wkl = W.init sI - s0 = siSol sI - ks = siVars sI + act = solve_ cfg fi s0 ks wkl + sI = solverInfo cfg fi + wkl = W.init sI + s0 = siSol sI + ks = siVars sI -------------------------------------------------------------------------------- @@ -118,7 +118,7 @@ -> SolveM a (F.Result (Integer, a), Stats) -------------------------------------------------------------------------------- solve_ cfg fi s0 ks wkl = do - let s1 = {-# SCC "sol-init" #-} S.init cfg fi ks + let s1 = F.notracepp "solve_ " $ {-# SCC "sol-init" #-} S.init cfg fi ks let s2 = mappend s0 s1 (s3, res0) <- sendConcreteBindingsToSMT F.emptyIBindEnv $ \bindingsInSmt -> do -- let s3 = solveEbinds fi s2 @@ -178,14 +178,14 @@ | Just (c, w', newScc, rnk) <- W.pop w = do i <- tickIter newScc (b, s') <- refineC bindingsInSmt i s c - lift $ writeLoud $ refineMsg i c b rnk + lift $ writeLoud $ refineMsg i c b rnk (showpp s') let w'' = if b then W.push c w' else w' refine bindingsInSmt s' w'' | otherwise = return s where -- DEBUG - refineMsg i c b rnk = printf "\niter=%d id=%d change=%s rank=%d\n" - i (F.subcId c) (show b) rnk + refineMsg i c b rnk s = printf "\niter=%d id=%d change=%s rank=%d s=%s\n" + i (F.subcId c) (show b) rnk s --------------------------------------------------------------------------- -- | Single Step Refinement ----------------------------------------------- @@ -311,7 +311,7 @@ -- lift $ printf "isUnsat %s" (show (F.subcId c)) _ <- tickIter True -- newScc be <- getBinds - let lp = S.lhsPred bindingsInSmt be s c + let lp = S.lhsPred bindingsInSmt (F.coerceBindEnv be) s c let rp = rhsPred c res <- not <$> isValid (cstrSpan c) lp rp lift $ whenLoud $ showUnsat res (F.subcId c) lp rp diff --git a/src/Language/Fixpoint/Solver/TrivialSort.hs b/src/Language/Fixpoint/Solver/TrivialSort.hs --- a/src/Language/Fixpoint/Solver/TrivialSort.hs +++ b/src/Language/Fixpoint/Solver/TrivialSort.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} @@ -14,7 +15,9 @@ import qualified Data.HashSet as S import Data.Hashable import qualified Data.HashMap.Strict as M +#if !MIN_VERSION_base(4,20,0) import Data.List (foldl') +#endif import qualified Data.Graph as G import Data.Maybe import Text.Printf diff --git a/src/Language/Fixpoint/Solver/UniqifyBinds.hs b/src/Language/Fixpoint/Solver/UniqifyBinds.hs --- a/src/Language/Fixpoint/Solver/UniqifyBinds.hs +++ b/src/Language/Fixpoint/Solver/UniqifyBinds.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PatternGuards #-} @@ -14,7 +15,9 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import qualified Data.List as L +#if !MIN_VERSION_base(4,20,0) import Data.Foldable (foldl') +#endif import Data.Maybe (catMaybes, mapMaybe, fromJust, isJust) import Data.Hashable (Hashable) import GHC.Generics (Generic) diff --git a/src/Language/Fixpoint/Solver/UniqifyKVars.hs b/src/Language/Fixpoint/Solver/UniqifyKVars.hs --- a/src/Language/Fixpoint/Solver/UniqifyKVars.hs +++ b/src/Language/Fixpoint/Solver/UniqifyKVars.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} {- | This module creates new bindings for each argument of each kvar. @@ -38,7 +39,9 @@ import Language.Fixpoint.Types import Language.Fixpoint.Types.Visitor (mapKVarSubsts) import qualified Data.HashMap.Strict as M +#if !MIN_VERSION_base(4,20,0) import Data.Foldable (foldl') +#endif -------------------------------------------------------------------------------- wfcUniqify :: SInfo a -> SInfo a diff --git a/src/Language/Fixpoint/SortCheck.hs b/src/Language/Fixpoint/SortCheck.hs --- a/src/Language/Fixpoint/SortCheck.hs +++ b/src/Language/Fixpoint/SortCheck.hs @@ -123,24 +123,24 @@ instance (Loc a) => Elaborate (SInfo a) where - elaborate x senv si = si - { F.cm = elaborate x senv <$> F.cm si - , F.bs = elaborate x senv $ F.bs si - , F.asserts = elaborate x senv <$> F.asserts si + elaborate msg senv si = si + { F.cm = elaborate msg senv <$> F.cm si + , F.bs = elaborate msg senv $ F.bs si + , F.asserts = elaborate msg senv <$> F.asserts si } instance (Elaborate e) => (Elaborate (Triggered e)) where - elaborate x env t = fmap (elaborate x env) t + elaborate msg env t = fmap (elaborate msg env) t instance (Elaborate a) => (Elaborate (Maybe a)) where - elaborate x env t = fmap (elaborate x env) t + elaborate msg env t = fmap (elaborate msg env) t instance Elaborate Sort where elaborate _ _ = go where go s | isString s = strSort - go (FAbs i s) = FAbs i (go s) + go (FAbs i s) = FAbs i (go s) go (FFunc s1 s2) = funSort (go s1) (go s2) go (FApp s1 s2) = FApp (go s1) (go s2) go s = s @@ -164,13 +164,15 @@ env' = insertsSymEnv env (eqArgs eq) instance Elaborate Expr where - elaborate msg env = elabNumeric . elabApply env . elabExpr msg env - + elaborate msg env = + elabNumeric . elabApply env' . elabExpr msg env' . elabFSet + where + env' = coerceEnv env skipElabExpr :: Located String -> SymEnv -> Expr -> Expr skipElabExpr msg env e = case elabExprE msg env e of Left _ -> e - Right e' -> elabNumeric . elabApply env $ e' + Right e' -> elabNumeric . elabApply env $ e' instance Elaborate (Symbol, Sort) where elaborate msg env (x, s) = (x, elaborate msg env s) @@ -193,20 +195,60 @@ = e instance Elaborate SortedReft where - elaborate x env (RR s (Reft (v, e))) = RR s (Reft (v, e')) + elaborate msg env (RR s (Reft (v, e))) = RR s (Reft (v, e')) where - e' = elaborate x env' e + e' = elaborate msg env' e env' = insertSymEnv v s env instance (Loc a) => Elaborate (BindEnv a) where elaborate msg env = mapBindEnv (\i (x, sr, l) -> (x, elaborate (msg' l i x sr) env sr, l)) where - msg' l i x sr = atLoc l (val msg ++ unwords [" elabBE", show i, show x, show sr]) + msg' l i x sr = atLoc l (val msg ++ unwords [" elabBE", show i, show x, show sr]) instance (Loc a) => Elaborate (SimpC a) where elaborate msg env c = c {_crhs = elaborate msg' env (_crhs c) } where msg' = atLoc c (val msg) + +--------------------------------------------------------------------------------- +-- | 'elabFSet' replaces all finset theory operations with array-based encodings. +--------------------------------------------------------------------------------- +elabFSet :: Expr -> Expr +elabFSet (EApp h@(EVar f) e) + | f == Thy.setEmpty = EApp (EVar Thy.arrConst) PFalse + | f == Thy.setEmp = PAtom Eq (EApp (EVar Thy.arrConst) PFalse) (elabFSet e) + | f == Thy.setSng = EApp (EApp (EApp (EVar Thy.arrStore) (EApp (EVar Thy.arrConst) PFalse)) (elabFSet e)) PTrue + | f == Thy.setCom = EApp (EVar Thy.arrMapNot) (elabFSet e) + | otherwise = EApp (elabFSet h) (elabFSet e) +elabFSet (EApp (EApp h@(EVar f) e1) e2) + | f == Thy.setMem = EApp (EApp (EVar Thy.arrSelect) (elabFSet e2)) (elabFSet e1) + | f == Thy.setCup = EApp (EApp (EVar Thy.arrMapOr) (elabFSet e1)) (elabFSet e2) + | f == Thy.setCap = EApp (EApp (EVar Thy.arrMapAnd) (elabFSet e1)) (elabFSet e2) + | f == Thy.setAdd = EApp (EApp (EApp (EVar Thy.arrStore) (elabFSet e1)) (elabFSet e2)) PTrue + -- A \ B == A /\ ~B == ~(A => B) + | f == Thy.setDif = EApp (EApp (EVar Thy.arrMapAnd) (elabFSet e1)) (EApp (EVar Thy.arrMapNot) (elabFSet e2)) + | f == Thy.setSub = PAtom Eq (EApp (EVar Thy.arrConst) PTrue) (EApp (EApp (EVar Thy.arrMapImp) (elabFSet e1)) (elabFSet e2)) + | otherwise = EApp (EApp (elabFSet h) (elabFSet e1)) (elabFSet e2) +elabFSet (EApp e1 e2) = EApp (elabFSet e1) (elabFSet e2) +elabFSet (ENeg e) = ENeg (elabFSet e) +elabFSet (EBin b e1 e2) = EBin b (elabFSet e1) (elabFSet e2) +elabFSet (EIte e1 e2 e3) = EIte (elabFSet e1) (elabFSet e2) (elabFSet e3) +elabFSet (ECst e t) = ECst (elabFSet e) t +elabFSet (ELam b e) = ELam b (elabFSet e) +elabFSet (ETApp e t) = ETApp (elabFSet e) t +elabFSet (ETAbs e t) = ETAbs (elabFSet e) t +elabFSet (PAnd es) = PAnd (elabFSet <$> es) +elabFSet (POr es) = POr (elabFSet <$> es) +elabFSet (PNot e) = PNot (elabFSet e) +elabFSet (PImp e1 e2) = PImp (elabFSet e1) (elabFSet e2) +elabFSet (PIff e1 e2) = PIff (elabFSet e1) (elabFSet e2) +elabFSet (PAtom r e1 e2) = PAtom r (elabFSet e1) (elabFSet e2) +elabFSet (PAll bs e) = PAll bs (elabFSet e) +elabFSet (PExist bs e) = PExist bs (elabFSet e) +elabFSet (PGrad k su i e) = PGrad k su i (elabFSet e) +elabFSet (ECoerc a t e) = ECoerc a t (elabFSet e) +elabFSet e = e + -------------------------------------------------------------------------------- -- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites. -------------------------------------------------------------------------------- @@ -422,11 +464,10 @@ instance Checkable Expr where check γ e = void $ checkExpr f e - where f = (`lookupSEnvWithDistance` γ) + where f = (`lookupSEnvWithDistance` coerceSortEnv γ) - checkSort γ s e = void $ checkExpr f (ECst e s) - where - f = (`lookupSEnvWithDistance` γ) + checkSort γ s e = void $ checkExpr f (ECst e (coerceSetToArray s)) + where f = (`lookupSEnvWithDistance` coerceSortEnv γ) instance Checkable SortedReft where check γ (RR s (Reft (v, ra))) = check γ' ra @@ -436,32 +477,32 @@ -------------------------------------------------------------------------------- -- | Checking Expressions ------------------------------------------------------ -------------------------------------------------------------------------------- -checkExpr :: Env -> Expr -> CheckM Sort -checkExpr _ (ESym _) = return strSort -checkExpr _ (ECon (I _)) = return FInt -checkExpr _ (ECon (R _)) = return FReal -checkExpr _ (ECon (L _ s)) = return s -checkExpr f (EVar x) = checkSym f x -checkExpr f (ENeg e) = checkNeg f e -checkExpr f (EBin o e1 e2) = checkOp f e1 o e2 -checkExpr f (EIte p e1 e2) = checkIte f p e1 e2 -checkExpr f (ECst e t) = checkCst f t e -checkExpr f (EApp g e) = checkApp f Nothing g e -checkExpr f (PNot p) = checkPred f p >> return boolSort -checkExpr f (PImp p p') = mapM_ (checkPred f) [p, p'] >> return boolSort -checkExpr f (PIff p p') = mapM_ (checkPred f) [p, p'] >> return boolSort -checkExpr f (PAnd ps) = mapM_ (checkPred f) ps >> return boolSort -checkExpr f (POr ps) = mapM_ (checkPred f) ps >> return boolSort -checkExpr f (PAtom r e e') = checkRel f r e e' >> return boolSort -checkExpr _ PKVar{} = return boolSort -checkExpr f (PGrad _ _ _ e) = checkPred f e >> return boolSort +checkExpr :: Env -> Expr -> CheckM Sort +checkExpr _ (ESym _) = return strSort +checkExpr _ (ECon (I _)) = return FInt +checkExpr _ (ECon (R _)) = return FReal +checkExpr _ (ECon (L _ s)) = return s +checkExpr f (EVar x) = checkSym f x +checkExpr f (ENeg e) = checkNeg f e +checkExpr f (EBin o e1 e2) = checkOp f e1 o e2 +checkExpr f (EIte p e1 e2) = checkIte f p e1 e2 +checkExpr f (ECst e t) = checkCst f t e +checkExpr f (EApp g e) = checkApp f Nothing g e +checkExpr f (PNot p) = checkPred f p >> return boolSort +checkExpr f (PImp p p') = mapM_ (checkPred f) [p, p'] >> return boolSort +checkExpr f (PIff p p') = mapM_ (checkPred f) [p, p'] >> return boolSort +checkExpr f (PAnd ps) = mapM_ (checkPred f) ps >> return boolSort +checkExpr f (POr ps) = mapM_ (checkPred f) ps >> return boolSort +checkExpr f (PAtom r e e') = checkRel f r e e' >> return boolSort +checkExpr _ PKVar{} = return boolSort +checkExpr f (PGrad _ _ _ e) = checkPred f e >> return boolSort -checkExpr f (PAll bs e ) = checkExpr (addEnv f bs) e -checkExpr f (PExist bs e) = checkExpr (addEnv f bs) e -checkExpr f (ELam (x,t) e) = FFunc t <$> checkExpr (addEnv f [(x,t)]) e -checkExpr f (ECoerc s t e) = checkExpr f (ECst e s) >> return t -checkExpr _ (ETApp _ _) = error "SortCheck.checkExpr: TODO: implement ETApp" -checkExpr _ (ETAbs _ _) = error "SortCheck.checkExpr: TODO: implement ETAbs" +checkExpr f (PAll bs e ) = checkExpr (addEnv f bs) e +checkExpr f (PExist bs e) = checkExpr (addEnv f bs) e +checkExpr f (ELam (x,t) e) = FFunc t <$> checkExpr (addEnv f [(x,t)]) e +checkExpr f (ECoerc s t e) = checkExpr f (ECst e s) >> return t +checkExpr _ (ETApp _ _) = error "SortCheck.checkExpr: TODO: implement ETApp" +checkExpr _ (ETAbs _ _) = error "SortCheck.checkExpr: TODO: implement ETAbs" addEnv :: Eq a => (a -> SESearch b) -> [(a, b)] -> a -> SESearch b addEnv f bs x @@ -562,12 +603,12 @@ elab f@(_,g) e@(PAtom eq e1 e2) | eq == Eq || eq == Ne = do t1 <- checkExpr g e1 t2 <- checkExpr g e2 - (t1',t2') <- unite g e t1 t2 `withError` errElabExpr e + (t1',t2') <- unite g e t1 t2 `withError` errElabExpr e e1' <- elabAs f t1' e1 e2' <- elabAs f t2' e2 e1'' <- eCstAtom f e1' t1' e2'' <- eCstAtom f e2' t2' - return (PAtom eq e1'' e2'' , boolSort) + return (PAtom eq e1'' e2'' , boolSort) elab f (PAtom r e1 e2) | r == Ueq || r == Une = do @@ -623,11 +664,11 @@ elabAddEnv (g, f) bs = (g, addEnv f bs) elabAs :: ElabEnv -> Sort -> Expr -> CheckM Expr -elabAs f t e = notracepp _msg <$> go e +elabAs f t e = notracepp _msg <$> go e where - _msg = "elabAs: t = " ++ showpp t ++ " e = " ++ showpp e - go (EApp e1 e2) = elabAppAs f t e1 e2 - go e' = fst <$> elab f e' + _msg = "elabAs: t = " ++ showpp t ++ "; e = " ++ showpp e + go (EApp e1 e2) = elabAppAs f t e1 e2 + go e' = fst <$> elab f e' -- DUPLICATION with `checkApp'` elabAppAs :: ElabEnv -> Sort -> Expr -> Expr -> CheckM Expr @@ -641,11 +682,11 @@ g' <- elabAs env tg g let te = apply su eT e' <- elabAs env te e - return $ EApp (ECst g' tg) (ECst e' te) + pure $ EApp (ECst g' tg) (ECst e' te) elabEApp :: ElabEnv -> Expr -> Expr -> CheckM (Expr, Sort, Expr, Sort, Sort) elabEApp f@(_, g) e1 e2 = do - (e1', s1) <- notracepp ("elabEApp1: e1 = " ++ showpp e1) <$> elab f e1 + (e1', s1) <- {- notracepp ("elabEApp: e1 = " ++ showpp e1) <$> -} elab f e1 (e2', s2) <- elab f e2 (e1'', e2'', s1', s2', s) <- elabAppSort g e1' e2' s1 s2 return (e1'', s1', e2'', s2', s) @@ -655,14 +696,14 @@ let e = Just (EApp e1 e2) (sIn, sOut, su) <- checkFunSort s1 su' <- unify1 f e su sIn s2 - return (applyExpr (Just su') e1, applyExpr (Just su') e2, apply su' s1, apply su' s2, apply su' sOut) + return (applyExpr (Just su') e1 , applyExpr (Just su') e2, apply su' s1, apply su' s2, apply su' sOut) -------------------------------------------------------------------------------- -- | defuncEApp monomorphizes function applications. -------------------------------------------------------------------------------- defuncEApp :: SymEnv -> Expr -> [(Expr, Sort)] -> Expr -defuncEApp _env e [] = e +defuncEApp _ e [] = e defuncEApp env e es = eCst (L.foldl' makeApplication e' es') (snd $ last es) where (e', es') = takeArgs (seTheory env) e es @@ -676,7 +717,8 @@ -- 'e1' is the function, 'e2' is the argument, 's' is the OUTPUT TYPE makeApplication :: Expr -> (Expr, Sort) -> Expr -makeApplication e1 (e2, s) = ECst (EApp (EApp f e1) e2) s +makeApplication e1 (e2, s) = + ECst (EApp (EApp f e1) e2) s where f = {- notracepp ("makeApplication: " ++ showpp (e2, t2)) $ -} applyAt t2 s t2 = exprSort "makeAppl" e2 @@ -751,7 +793,7 @@ are represented, in SMTLIB, as - (Eapp (EApp apply e1) e2) + (EApp (EApp apply e1) e2) where 'apply' is 'ECst (EVar "apply") t' and 't' is 'FFunc a b' @@ -782,7 +824,7 @@ FBool -> not b ``` -## The Problem +**The Problem** The problem is you cannot encode the body of `proj` as a well-sorted refinement: @@ -795,7 +837,7 @@ The catch is that `x` is being used BOTH as `Int` and as `Bool` which is not supported in SMTLIB. -## Approach: Uninterpreted Functions +**Approach: Uninterpreted Functions** We encode `coerce` as an explicit **uninterpreted function**: @@ -833,7 +875,7 @@ and the UIF nature of `coerce_int_int` renders the VC invalid. -## Solution: Eliminate Trivial Coercions +**Solution: Eliminate Trivial Coercions** HOWEVER, the solution here, may simply be to use UIFs when the coercion is non-trivial (e.g. `a ~ int`) but to eschew them when @@ -851,7 +893,7 @@ -------------------------------------------------------------------------------- applySorts :: Vis.Visitable t => t -> [Sort] -------------------------------------------------------------------------------- -applySorts = {- tracepp "applySorts" . -} (defs ++) . Vis.fold vis () [] +applySorts = {- notracepp "applySorts" . -} (defs ++) . Vis.fold vis () [] where defs = [FFunc t1 t2 | t1 <- basicSorts, t2 <- basicSorts] vis = (Vis.defaultVisitor :: Vis.Visitor [KVar] t) { Vis.accExpr = go } @@ -877,7 +919,7 @@ go (ELam (_, sx) e) = FFunc sx <$> go e go (EApp e ex) | Just (FFunc sx s) <- genSort <$> go e - = maybe s (`apply` s) <$> ((`unifySorts` sx) <$> go ex) + = maybe s (`apply` s) . (`unifySorts` sx) <$> go ex go _ = Nothing genSort :: Sort -> Sort @@ -891,7 +933,7 @@ throwErrorAt :: String -> CheckM a throwErrorAt ~err' = do -- Lazy pattern needed because we use LANGUAGE Strict in this module - -- See Note [Lazy error messages] + -- See Note [Lazy error messages] sp <- asks chSpan liftIO $ throwIO (ChError (\_ -> atLoc sp err')) @@ -922,8 +964,8 @@ (`apply` t1) <$> unifys f Nothing [t1] [t2] checkIteTy :: Env -> Expr -> Expr -> Expr -> Sort -> Sort -> CheckM Sort -checkIteTy f p e1 e2 t1 t2 - = ((`apply` t1) <$> unifys f e' [t1] [t2]) `withError` errIte e1 e2 t1 t2 +checkIteTy f p e1 e2 t1 t2 = + ((`apply` t1) <$> unifys f e' [t1] [t2]) `withError` errIte e1 e2 t1 t2 where e' = Just (EIte p e1 e2) @@ -933,7 +975,8 @@ = checkApp f (Just t) g e checkCst f t e = do t' <- checkExpr f e - ((`apply` t) <$> unifys f (Just e) [t] [t']) `withError` errCast e t' t + su <- unifys f (Just e) [t] [t'] `withError` errCast e t' t + pure (apply su t) checkApp :: Env -> Maybe Sort -> Expr -> Expr -> CheckM Sort checkApp f to g es @@ -945,7 +988,7 @@ checkExprAs f t e = do t' <- checkExpr f e θ <- unifys f (Just e) [t'] [t] - return $ apply θ t + pure $ apply θ t -- | Helper for checking uninterpreted function applications -- | Checking function application should be curried, e.g. 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 @@ -113,6 +113,7 @@ , noLazyPLE :: Bool , 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 } deriving (Eq,Data,Typeable,Show,Generic) instance Default Config where @@ -227,13 +228,13 @@ , eliminate = None &= help "Eliminate KVars [none = quals for all-kvars, cuts = quals for cut-kvars, all = eliminate all-kvars (TRUE for cuts)]" , scrape = def &= help "Scrape qualifiers from constraint (Horn format only) [ no = do not, head = scrape from heads, both = scrape from everywhere ]" , elimBound = Nothing &= name "elimBound" &= help "(alpha) Maximum eliminate-chain depth" - , smtTimeout = Nothing &= name "smtTimeout" &= help "smt timeout in msec" + , smtTimeout = Nothing &= name "smtTimeout" &= help "SMT timeout in msec" , elimStats = False &= help "(alpha) Print eliminate stats" , solverStats = False &= help "Print solver stats" , save = False &= help "Save Query as .fq and .bfq files" , metadata = False &= help "Print meta-data associated with constraints" , stats = False &= help "Compute constraint statistics" - , etaElim = False &= help "eta elimination in function definition" + , etaElim = False &= help "Eta elimination in function definition" , parts = False &= help "Partition constraints into indepdendent .fq files" , cores = def &= help "(numeric) Number of threads to use" , minPartSize = defaultMinPartSize &= help "(numeric) Minimum partition size when solving in parallel" @@ -247,7 +248,7 @@ , autoKuts = False &= help "Ignore given Kut vars, compute from scratch" , nonLinCuts = False &= help "Treat non-linear kvars as cuts" , noslice = False &= help "Disable non-concrete KVar slicing" - , rewriteAxioms = False &= help "allow axiom instantiation via rewriting (PLE)" + , rewriteAxioms = False &= name "ple" &= help "Allow axiom instantiation via rewriting (PLE)" , pleWithUndecidedGuards = False &= name "ple-with-undecided-guards" @@ -281,6 +282,7 @@ , restOrdering = "rpo" &= name "rest-ordering" &= help "Ordering Constraint Algebra to use for REST" + , noSmtHorn = False &= help "Do not use SMTLIB horn format" } &= verbosity &= program "fixpoint" diff --git a/src/Language/Fixpoint/Types/Constraints.hs b/src/Language/Fixpoint/Types/Constraints.hs --- a/src/Language/Fixpoint/Types/Constraints.hs +++ b/src/Language/Fixpoint/Types/Constraints.hs @@ -74,6 +74,7 @@ , HOInfo (..) , allowHO , allowHOquals + , cfgHoInfo -- * Axioms , AxiomEnv (..) @@ -99,9 +100,9 @@ import qualified Data.List as L -- (sort, nub, delete) import Data.Maybe (catMaybes) import Control.DeepSeq -import Control.Monad (void) +import Control.Monad (when, void) import Language.Fixpoint.Types.PrettyPrint -import Language.Fixpoint.Types.Config hiding (allowHO) +import qualified Language.Fixpoint.Types.Config as C import Language.Fixpoint.Types.Triggers import Language.Fixpoint.Types.Names import Language.Fixpoint.Types.Errors @@ -118,6 +119,8 @@ import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S import qualified Data.ByteString as B +import qualified Data.Text as T +import qualified Data.Text.IO as T import qualified Data.Binary as B -------------------------------------------------------------------------------- @@ -503,6 +506,18 @@ | PatExact !Symbol -- ^ str i.e. exactly match 'str' deriving (Eq, Ord, Show, Data, Typeable, Generic) +instance ToJSON Qualifier where +instance FromJSON Qualifier where +instance ToJSON QualParam where +instance FromJSON QualParam where +instance ToJSON QualPattern where +instance FromJSON QualPattern where +instance ToJSON Equation where +instance FromJSON Equation where +instance ToJSON Rewrite where +instance FromJSON Rewrite where + + trueQual :: Qualifier trueQual = Q (symbol ("QTrue" :: String)) [] mempty (dummyPos "trueQual") @@ -542,7 +557,6 @@ instance PPrint Qualifier where pprintTidy k q = "qualif" <+> pprintTidy k (qName q) <+> "defined at" <+> pprintTidy k (qPos q) - -- pprintTidy _ q = pprQual q pprQual :: Qualifier -> Doc pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <-> parens args <-> colon <+> parens (toFix p) <+> text "//" <+> toFix l @@ -698,6 +712,9 @@ } deriving (Eq, Show, Generic) +cfgHoInfo :: C.Config -> HOInfo +cfgHoInfo cfg = HOI (C.allowHO cfg) (C.allowHOqs cfg) + allowHO, allowHOquals :: GInfo c a -> Bool allowHO = hoBinds . hoInfo allowHOquals = hoQuals . hoInfo @@ -771,7 +788,7 @@ -------------------------------------------------------------------------- -- | Rendering Queries -------------------------------------------------------------------------- -toFixpoint :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> Doc +toFixpoint :: (Fixpoint a, Fixpoint (c a)) => C.Config -> GInfo c a -> Doc -------------------------------------------------------------------------- toFixpoint cfg x' = cfgDoc cfg $++$ declsDoc x' @@ -801,7 +818,7 @@ qualsDoc = vcat . map toFix . L.sort . quals aeDoc = toFix . ae metaDoc (i,d) = toFixMeta (text "bind" <+> toFix i) (toFix d) - mdata = metadata cfg + mdata = C.metadata cfg binfoDoc | mdata = vcat . map metaDoc . M.toList . bindInfo | otherwise = \_ -> text "\n" @@ -815,7 +832,7 @@ where kvD (c, so) = d <+> toFix c <+> ":" <+> parens (toFix so) -writeFInfo :: (Fixpoint a, Fixpoint (c a)) => Config -> GInfo c a -> FilePath -> IO () +writeFInfo :: (Fixpoint a, Fixpoint (c a)) => C.Config -> GInfo c a -> FilePath -> IO () writeFInfo cfg fq f = writeFile f (render $ toFixpoint cfg fq) -------------------------------------------------------------------------------- @@ -876,30 +893,29 @@ --------------------------------------------------------------------------- -- | Top level Solvers ---------------------------------------------------- --------------------------------------------------------------------------- -type Solver a = Config -> FInfo a -> IO (Result (Integer, a)) +type Solver a = C.Config -> FInfo a -> IO (Result (Integer, a)) -------------------------------------------------------------------------------- -saveQuery :: (Fixpoint a) => Config -> FInfo a -> IO () +saveQuery :: (Fixpoint a) => C.Config -> FInfo a -> IO () -------------------------------------------------------------------------------- -saveQuery cfg fi = {- when (save cfg) $ -} do +saveQuery cfg fi = when (C.save cfg) $ do let fi' = void fi saveBinaryQuery cfg fi' saveTextQuery cfg fi -saveBinaryQuery :: Config -> FInfo () -> IO () +saveBinaryQuery :: C.Config -> FInfo () -> IO () saveBinaryQuery cfg fi = do - let bfq = queryFile Files.BinFq cfg + let bfq = C.queryFile Files.BinFq cfg putStrLn $ "Saving Binary Query: " ++ bfq ++ "\n" ensurePath bfq B.writeFile bfq (S.encode fi) - -- B.encodeFile bfq fi -saveTextQuery :: Fixpoint a => Config -> FInfo a -> IO () +saveTextQuery :: Fixpoint a => C.Config -> FInfo a -> IO () saveTextQuery cfg fi = do - let fq = queryFile Files.Fq cfg + let fq = C.queryFile Files.Fq cfg putStrLn $ "Saving Text Query: " ++ fq ++ "\n" ensurePath fq - writeFile fq $ render (toFixpoint cfg fi) + T.writeFile fq $ T.pack $ render (toFixpoint cfg fi) --------------------------------------------------------------------------- -- | Axiom Instantiation Information -------------------------------------- diff --git a/src/Language/Fixpoint/Types/Environments.hs b/src/Language/Fixpoint/Types/Environments.hs --- a/src/Language/Fixpoint/Types/Environments.hs +++ b/src/Language/Fixpoint/Types/Environments.hs @@ -49,6 +49,8 @@ , bindEnvFromList, bindEnvToList, deleteBindEnv, elemsBindEnv , EBindEnv, splitByQuantifiers + , coerceBindEnv + -- * Information needed to lookup and update Solutions -- , SolEnv (..) @@ -73,6 +75,7 @@ import Language.Fixpoint.Types.PrettyPrint import Language.Fixpoint.Types.Names +import Language.Fixpoint.Types.Sorts import Language.Fixpoint.Types.Refinements import Language.Fixpoint.Types.Substitutions () import Language.Fixpoint.Misc @@ -360,3 +363,6 @@ where kIs = [ (k, i) | (i, ks) <- kPacks, k <- ks ] kPacks = zip [0..] . coalesce . fmap S.toList $ kvss + +coerceBindEnv :: BindEnv a -> BindEnv a +coerceBindEnv be = be { beBinds = M.map (\(s, sr, a) -> (s, sr { sr_sort = coerceSetToArray (sr_sort sr) } , a)) (beBinds be) } diff --git a/src/Language/Fixpoint/Types/Names.hs b/src/Language/Fixpoint/Types/Names.hs --- a/src/Language/Fixpoint/Types/Names.hs +++ b/src/Language/Fixpoint/Types/Names.hs @@ -93,12 +93,14 @@ , dummyName , preludeName , boolConName + , boolLConName , funConName , listConName , listLConName , tupConName , setConName , mapConName + , arrayConName , strConName , charConName , nilName @@ -150,6 +152,8 @@ import Language.Fixpoint.Utils.Builder as Builder (fromText) import Data.Functor.Contravariant (Contravariant(contramap)) import qualified Data.Binary as B +import qualified Data.Aeson as Aeson +import qualified Data.Aeson.Types as Aeson --------------------------------------------------------------- -- | Symbols -------------------------------------------------- @@ -176,7 +180,8 @@ = S { _symbolId :: !Id , symbolRaw :: T.Text , symbolEncoded :: T.Text - } deriving (Data, Typeable, Generic) + } + deriving (Data, Typeable, Generic) instance Eq Symbol where S i _ _ == S j _ _ = i == j @@ -212,9 +217,21 @@ size = contramap symbolText S.size instance B.Binary Symbol where - get = textSymbol <$> B.get - put = B.put . symbolText + get = textSymbol <$> B.get + put = B.put . symbolText +instance Aeson.ToJSON Symbol where + toJSON = Aeson.toJSON . symbolText + +instance Aeson.FromJSON Symbol where + parseJSON = fmap textSymbol . Aeson.parseJSON + +instance Aeson.ToJSONKey Symbol where + toJSONKey = Aeson.toJSONKeyText symbolText + +instance Aeson.FromJSONKey Symbol where + fromJSONKey = Aeson.FromJSONKeyText textSymbol + sCache :: Cache Symbol sCache = mkCache {-# NOINLINE sCache #-} @@ -624,19 +641,21 @@ coerceName :: Symbol coerceName = "coerce" -preludeName, dummyName, boolConName, funConName :: Symbol +preludeName, dummyName, boolConName, boolLConName, funConName :: Symbol preludeName = "Prelude" dummyName = "LIQUID$dummy" boolConName = "Bool" +boolLConName = "bool" funConName = "->" -listConName, listLConName, tupConName, propConName, _hpropConName, vvName, setConName, mapConName :: Symbol +listConName, listLConName, tupConName, propConName, _hpropConName, vvName, setConName, mapConName, arrayConName:: Symbol listConName = "[]" listLConName = "List" tupConName = "Tuple" setConName = "Set_Set" mapConName = "Map_t" +arrayConName = "Array_t" vvName = "VV" propConName = "Prop" _hpropConName = "HProp" @@ -708,6 +727,7 @@ , "Map_store" , "Map_union" , "Map_default" + , arrayConName -- Currently we parse X in "SizeX" to get the bitvec size -- so there is no finite set of names to add here... -- , size32Name diff --git a/src/Language/Fixpoint/Types/Refinements.hs b/src/Language/Fixpoint/Types/Refinements.hs --- a/src/Language/Fixpoint/Types/Refinements.hs +++ b/src/Language/Fixpoint/Types/Refinements.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} @@ -116,7 +117,11 @@ import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet import GHC.Generics (Generic) +#if MIN_VERSION_base(4,20,0) +import Data.List (partition) +#else import Data.List (foldl', partition) +#endif import qualified Data.Set as Set import Data.String import Data.Text (Text) @@ -131,6 +136,7 @@ import Language.Fixpoint.Misc import Text.PrettyPrint.HughesPJ.Compat import qualified Data.Binary as B +import Data.Aeson -- import Text.Printf (printf) @@ -236,7 +242,7 @@ -------------------------------------------------------------------------------- newtype KVar = KV { kv :: Symbol } - deriving (Eq, Ord, Data, Typeable, Generic, IsString) + deriving (Eq, Ord, Data, Typeable, Generic, IsString, ToJSON, FromJSON) intKvar :: Integer -> KVar intKvar = KV . intSymbol "k_" @@ -258,7 +264,7 @@ -- | Substitutions ------------------------------------------------------------- -------------------------------------------------------------------------------- newtype Subst = Su (M.HashMap Symbol Expr) - deriving (Eq, Data, Ord, Typeable, Generic) + deriving (Eq, Data, Ord, Typeable, Generic, ToJSON, FromJSON) instance Show Subst where show = showFix @@ -288,7 +294,7 @@ -- | Uninterpreted constants that are embedded as "constant symbol : Str" newtype SymConst = SL Text - deriving (Eq, Ord, Show, Data, Typeable, Generic) + deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) data Constant = I !Integer | R !Double @@ -302,6 +308,17 @@ deriving (Eq, Ord, Show, Data, Typeable, Generic) -- NOTE: For "Mod" 2nd expr should be a constant or a var *) +instance ToJSON Constant where +instance ToJSON Brel where +instance ToJSON Bop where +instance ToJSON Expr where + +instance FromJSON Constant where +instance FromJSON Brel where +instance FromJSON Bop where +instance FromJSON Expr where + + data Expr = ESym !SymConst | ECon !Constant | EVar !Symbol @@ -427,6 +444,9 @@ data GradInfo = GradInfo {gsrc :: SrcSpan, gused :: Maybe SrcSpan} deriving (Eq, Ord, Show, Data, Typeable, Generic) +instance ToJSON GradInfo +instance FromJSON GradInfo + srcGradInfo :: SourcePos -> GradInfo srcGradInfo src = GradInfo (SS src src) Nothing @@ -446,12 +466,12 @@ splitEAppThroughECst = go [] where go acc (dropECst -> (EApp f e)) = go (e:acc) f - go acc e = (e, acc) + go acc e = (e, acc) dropECst :: Expr -> Expr dropECst e = case e of ECst e' _ -> dropECst e' - _ -> e + _ -> e splitPAnd :: Expr -> [Expr] splitPAnd (PAnd es) = concatMap splitPAnd es @@ -462,7 +482,7 @@ -- | Eliminates redundant casts eCst :: Expr -> Sort -> Expr -eCst e t = ECst (dropECst e) t +eCst e s = ECst (dropECst e) s -------------------------------------------------------------------------------- debruijnIndex :: Expr -> Int @@ -914,7 +934,7 @@ pExist xts p = PExist xts p mkProp :: Expr -> Pred -mkProp = id -- EApp (EVar propConName) +mkProp = id -------------------------------------------------------------------------------- -- | Predicates ---------------------------------------------------------------- diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs --- a/src/Language/Fixpoint/Types/Sorts.hs +++ b/src/Language/Fixpoint/Types/Sorts.hs @@ -13,6 +13,7 @@ {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} +{-# LANGUAGE DeriveAnyClass #-} -- | This module contains the data types, operations and -- serialization functions for representing Fixpoint's @@ -37,6 +38,7 @@ , basicSorts, intSort, realSort, boolSort, strSort, funcSort -- , bitVec32Sort, bitVec64Sort , setSort, bitVecSort + , arraySort , sizedBitVecSort , mapSort, charSort , listFTyCon @@ -63,7 +65,7 @@ , sortSymbols , substSort - , isNumeric, isReal, isString, isPolyInst + , isBool, isNumeric, isReal, isString, isSet, isArray, isPolyInst -- * User-defined ADTs , DataField (..) @@ -80,16 +82,23 @@ , tceInsert , tceInsertWith , tceMap + + -- * Sort coercion for SMT theory encoding + , coerceSetToArray ) where import qualified Data.Store as S import Data.Generics (Data) import Data.Typeable (Typeable) import GHC.Generics (Generic) +import Data.Aeson + import Data.Hashable import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet +#if !MIN_VERSION_base(4,20,0) import Data.List (foldl') +#endif import Control.DeepSeq import Data.Maybe (fromMaybe) import Language.Fixpoint.Types.Names @@ -102,7 +111,7 @@ import qualified Data.Binary as B import Text.Read (readMaybe) -data FTycon = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic) +data FTycon = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) -- instance Show FTycon where -- show (TC s _) = show (val s) @@ -114,7 +123,7 @@ (TC s _) == (TC s' _) = val s == val s' data TCInfo = TCInfo { tc_isNum :: Bool, tc_isReal :: Bool, tc_isString :: Bool } - deriving (Eq, Ord, Show, Data, Typeable, Generic) + deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) mappendFTC :: FTycon -> FTycon -> FTycon mappendFTC (TC x i1) (TC _ i2) = TC x (mappend i1 i2) @@ -139,16 +148,16 @@ charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon :: FTycon strFTyCon, listFTyCon, mapFTyCon, setFTyCon :: FTycon -intFTyCon = TC (dummyLoc "int" ) numTcInfo -boolFTyCon = TC (dummyLoc "bool" ) defTcInfo -realFTyCon = TC (dummyLoc "real" ) realTcInfo -numFTyCon = TC (dummyLoc "num" ) numTcInfo -funcFTyCon = TC (dummyLoc "function" ) defTcInfo -strFTyCon = TC (dummyLoc strConName ) strTcInfo -listFTyCon = TC (dummyLoc listConName) defTcInfo -charFTyCon = TC (dummyLoc charConName) defTcInfo -setFTyCon = TC (dummyLoc setConName ) defTcInfo -mapFTyCon = TC (dummyLoc mapConName ) defTcInfo +intFTyCon = TC (dummyLoc "int" ) numTcInfo +boolFTyCon = TC (dummyLoc boolLConName) defTcInfo +realFTyCon = TC (dummyLoc "real" ) realTcInfo +numFTyCon = TC (dummyLoc "num" ) numTcInfo +funcFTyCon = TC (dummyLoc "function" ) defTcInfo +strFTyCon = TC (dummyLoc strConName ) strTcInfo +listFTyCon = TC (dummyLoc listConName ) defTcInfo +charFTyCon = TC (dummyLoc charConName ) defTcInfo +setFTyCon = TC (dummyLoc setConName ) defTcInfo +mapFTyCon = TC (dummyLoc mapConName ) defTcInfo isListConName :: LocSymbol -> Bool isListConName x = c == listConName || c == listLConName --"List" @@ -158,6 +167,22 @@ isListTC :: FTycon -> Bool isListTC (TC z _) = isListConName z +isSetConName :: LocSymbol -> Bool +isSetConName x = c == setConName + where + c = val x + +isSetTC :: FTycon -> Bool +isSetTC (TC z _) = isSetConName z + +isArrayConName :: LocSymbol -> Bool +isArrayConName x = c == arrayConName + where + c = val x + +isArrayTC :: FTycon -> Bool +isArrayTC (TC z _) = isArrayConName z + sizeBv :: FTycon -> Maybe Int sizeBv tc = do let s = val $ fTyconSymbol tc @@ -260,7 +285,7 @@ | FAbs !Int !Sort -- ^ type-abstraction | FTC !FTycon | FApp !Sort !Sort -- ^ constructed type - deriving (Eq, Ord, Show, Data, Typeable, Generic) + deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) instance PPrint Sort where pprintTidy _ = toFix @@ -284,18 +309,18 @@ data DataField = DField { dfName :: !LocSymbol -- ^ Field Name , dfSort :: !Sort -- ^ Field Sort - } deriving (Eq, Ord, Show, Data, Typeable, Generic) + } deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) data DataCtor = DCtor { dcName :: !LocSymbol -- ^ Ctor Name , dcFields :: ![DataField] -- ^ Ctor Fields - } deriving (Eq, Ord, Show, Data, Typeable, Generic) + } deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) data DataDecl = DDecl { ddTyCon :: !FTycon -- ^ Name of defined datatype , ddVars :: !Int -- ^ Number of type variables , ddCtors :: [DataCtor] -- ^ Datatype Ctors. Invariant: type variables bound in ctors are greater than ddVars - } deriving (Eq, Ord, Show, Data, Typeable, Generic) + } deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) instance Loc DataDecl where srcSpan (DDecl ty _ _) = srcSpan ty @@ -331,6 +356,10 @@ isFunction (FFunc _ _) = True isFunction _ = False +isBool :: Sort -> Bool +isBool (FTC (TC c _)) = val c == boolLConName +isBool _ = False + isNumeric :: Sort -> Bool isNumeric FInt = True isNumeric FReal = True @@ -346,7 +375,6 @@ isReal (FAbs _ s) = isReal s isReal _ = False - isString :: Sort -> Bool isString (FApp l c) = (isList l && isChar c) || isString l isString (FTC (TC c i)) = val c == strConName || tc_isString i @@ -357,6 +385,14 @@ isList (FTC c) = isListTC c isList _ = False +isSet :: Sort -> Bool +isSet (FTC c) = isSetTC c +isSet _ = False + +isArray :: Sort -> Bool +isArray (FTC c) = isArrayTC c +isArray _ = False + isChar :: Sort -> Bool isChar (FTC c) = c == charFTyCon isChar _ = False @@ -451,7 +487,7 @@ instance Fixpoint DataDecl where toFix (DDecl tc n ctors) = vcat ([header] ++ body ++ [footer]) where - header = {- text "data" <+> -} toFix tc <+> toFix n <+> text "= [" + header = toFix tc <+> toFix n <+> text "= [" body = [nest 2 (text "|" <+> toFix ct) | ct <- ctors] footer = text "]" @@ -480,7 +516,7 @@ funcSort = fTyconSort funcFTyCon setSort :: Sort -> Sort -setSort = FApp (FTC setFTyCon) +setSort = FApp (FTC setFTyCon) -- bitVecSort :: Sort -> Sort -- bitVecSort = FApp (FTC $ symbolFTycon' bitVecName) @@ -500,6 +536,9 @@ mapSort :: Sort -> Sort -> Sort mapSort = FApp . FApp (FTC (symbolFTycon' mapConName)) +arraySort :: Sort -> Sort -> Sort +arraySort = FApp . FApp (FTC (symbolFTycon' arrayConName)) + symbolFTycon' :: Symbol -> FTycon symbolFTycon' = symbolFTycon . dummyLoc @@ -625,3 +664,15 @@ tceMember :: (Eq a, Hashable a) => a -> TCEmb a -> Bool tceMember k (TCE m) = M.member k m + +------------------------------------------------------------------------------- +-- | Sort coercion for SMT theory encoding +------------------------------------------------------------------------------- + +coerceSetToArray :: Sort -> Sort +coerceSetToArray (FFunc sf sa) = FFunc (coerceSetToArray sf) (coerceSetToArray sa) +coerceSetToArray (FAbs i sa) = FAbs i (coerceSetToArray sa) +coerceSetToArray s@(FApp sf sa) + | isSet sf = arraySort (coerceSetToArray sa) boolSort + | otherwise = s +coerceSetToArray s = s diff --git a/src/Language/Fixpoint/Types/Spans.hs b/src/Language/Fixpoint/Types/Spans.hs --- a/src/Language/Fixpoint/Types/Spans.hs +++ b/src/Language/Fixpoint/Types/Spans.hs @@ -5,6 +5,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wno-orphans #-} +{-# LANGUAGE DeriveAnyClass #-} module Language.Fixpoint.Types.Spans ( @@ -56,6 +57,7 @@ import Text.Printf import Data.Functor.Contravariant (Contravariant(contramap)) import qualified Data.Binary as B +import Data.Aeson -- import Debug.Trace @@ -161,11 +163,16 @@ toFix = text . show -data Located a = Loc { loc :: !SourcePos -- ^ Start Position - , locE :: !SourcePos -- ^ End Position - , val :: !a - } deriving (Data, Typeable, Generic) +data Located a = Loc + { loc :: !SourcePos -- ^ Start Position + , locE :: !SourcePos -- ^ End Position + , val :: !a + } + deriving (Data, Typeable, Generic, ToJSON, FromJSON) +instance ToJSON SourcePos where +instance FromJSON SourcePos where + instance Loc (Located a) where srcSpan (Loc l l' _) = SS l l' @@ -215,6 +222,11 @@ instance (B.Binary a) => B.Binary (Located a) + +instance ToJSON Pos where + +instance FromJSON Pos where + srcLine :: (Loc a) => a -> Pos srcLine = sourceLine . sp_start . srcSpan @@ -224,7 +236,7 @@ data SrcSpan = SS { sp_start :: !SourcePos , sp_stop :: !SourcePos} - deriving (Eq, Ord, Show, Data, Typeable, Generic) + deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON) instance NFData SrcSpan instance S.Store SrcSpan diff --git a/src/Language/Fixpoint/Types/Theories.hs b/src/Language/Fixpoint/Types/Theories.hs --- a/src/Language/Fixpoint/Types/Theories.hs +++ b/src/Language/Fixpoint/Types/Theories.hs @@ -33,7 +33,9 @@ , symbolAtName , symbolAtSmtName - + -- * Coercing sorts in environments + , coerceEnv + , coerceSortEnv ) where @@ -228,8 +230,10 @@ | SBool | SReal | SString + -- TODO remove these now that we use SArray directly | SSet | SMap + | SArray !SmtSort !SmtSort | SBitVec !Int | SVar !Int | SData !FTycon ![SmtSort] @@ -271,6 +275,8 @@ | setConName == symbol c = SSet go (FTC c) _ | mapConName == symbol c = SMap + go (FTC c) [a, b] + | arrayConName == symbol c = SArray (sortSmtSort poly env a) (sortSmtSort poly env b) go (FTC bv) [FTC s] | bitVecName == symbol bv , Just n <- sizeBv s = SBitVec n @@ -294,6 +300,7 @@ pprintTidy _ SString = text "Str" pprintTidy _ SSet = text "Set" pprintTidy _ SMap = text "Map" + pprintTidy k (SArray a b) = ppParens k (text "Array") [a, b] pprintTidy _ (SBitVec n) = text "BitVec" <+> int n pprintTidy _ (SVar i) = text "@" <-> int i -- HKT pprintTidy k (SApp ts) = ppParens k (pprintTidy k tyAppName) ts @@ -301,3 +308,18 @@ ppParens :: (PPrint d) => Tidy -> Doc -> [d] -> Doc ppParens k d ds = parens $ Misc.intersperse (text "") (d : (pprintTidy k <$> ds)) + +-------------------------------------------------------------------------------- +-- | Coercing sorts inside environments for SMT theory encoding +-------------------------------------------------------------------------------- + +coerceSortEnv :: SEnv Sort -> SEnv Sort +coerceSortEnv ss = coerceSetToArray <$> ss + +coerceEnv :: SymEnv -> SymEnv +coerceEnv env = SymEnv { seSort = coerceSortEnv (seSort env) + , seTheory = seTheory env + , seData = seData env + , seLits = seLits env + , seAppls = seAppls env + } diff --git a/src/Language/Fixpoint/Types/Visitor.hs b/src/Language/Fixpoint/Types/Visitor.hs --- a/src/Language/Fixpoint/Types/Visitor.hs +++ b/src/Language/Fixpoint/Types/Visitor.hs @@ -470,9 +470,9 @@ instance (SymConsts (c a)) => SymConsts (GInfo c a) where symConsts fi = Misc.sortNub $ csLits ++ bsLits ++ qsLits where - csLits = concatMap symConsts $ M.elems $ cm fi - bsLits = symConsts $ bs fi - qsLits = concatMap symConsts $ qBody <$> quals fi + csLits = concatMap symConsts $ M.elems $ cm fi + bsLits = symConsts $ bs fi + qsLits = concatMap (symConsts . qBody) $ quals fi instance SymConsts (BindEnv a) where symConsts = concatMap (symConsts . Misc.snd3) . M.elems . beBinds diff --git a/src/Language/Fixpoint/Utils/Files.hs b/src/Language/Fixpoint/Utils/Files.hs --- a/src/Language/Fixpoint/Utils/Files.hs +++ b/src/Language/Fixpoint/Utils/Files.hs @@ -91,6 +91,7 @@ | BinFq -- ^ Binary representation of .fq / FInfo | Smt2 -- ^ SMTLIB2 query file | HSmt2 -- ^ Horn query file + | HJSON -- ^ Horn query JSON file | Min -- ^ filter constraints with delta debug | MinQuals -- ^ filter qualifiers with delta debug | MinKVars -- ^ filter kvars with delta debug @@ -124,6 +125,7 @@ go Cache = ".err" go Smt2 = ".smt2" go HSmt2 = ".horn.smt2" + go HJSON = ".horn.json" go (Auto n) = ".auto." ++ show n go Dot = ".dot" go BinFq = ".bfq" diff --git a/tests/pos/literals03.fq b/tests/pos/literals03.fq --- a/tests/pos/literals03.fq +++ b/tests/pos/literals03.fq @@ -12,5 +12,5 @@ constraint: env [ 1; 2 ] lhs {v : int | true } - rhs {v : int | Set_mem a (listElts things)} + rhs {v : int | Set_mem a (listElts things)} id 1 tag [] diff --git a/tests/pos/literals04.fq b/tests/pos/literals04.fq --- a/tests/pos/literals04.fq +++ b/tests/pos/literals04.fq @@ -12,5 +12,5 @@ constraint: env [ 1; 2 ] lhs {v : int | true } - rhs {v : int | Set_mem a (listElts things)} + rhs {v : int | Set_mem a (listElts things)} id 1 tag [] diff --git a/tests/pos/literals05.fq b/tests/pos/literals05.fq --- a/tests/pos/literals05.fq +++ b/tests/pos/literals05.fq @@ -2,13 +2,13 @@ constant Set_sng : (func(1, [@(0); (Set_Set @(0))])) bind 1 a : {a : Str | a == "director" } -bind 2 things : {v : LLChar | (listElts v == (Set_cup (Set_sng "year") - (Set_cup (Set_sng "star") - (Set_cup (Set_sng "director") +bind 2 things : {v : LLChar | (listElts v == (Set_cup (Set_sng "year") + (Set_cup (Set_sng "star") + (Set_cup (Set_sng "director") (Set_sng "title"))))) } constraint: env [ 1; 2 ] lhs {v : int | true } - rhs {v : int | Set_mem a (listElts things)} + rhs {v : int | Set_mem a (listElts things)} id 1 tag [] diff --git a/tests/pos/maps03.fq b/tests/pos/maps03.fq --- a/tests/pos/maps03.fq +++ b/tests/pos/maps03.fq @@ -1,10 +1,10 @@ bind 1 m1 : {v : Map_t Int Int | v = Map_default 0} -bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 30 3) 10 1) 20 2) } +bind 2 m2 : {v : Map_t Int Int | v = (Map_store (Map_store (Map_store m1 30 3) 10 1) 20 2) } bind 3 s1 : {v : Set_Set Int | v = (Set_cup (Set_sng 30) (Set_sng 20))} -bind 4 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 2) 30 3) } +bind 4 m3 : {v : Map_t Int Int | v = (Map_store (Map_store m1 20 2) 30 3) } constraint: env [ 1; 2; 3; 4 ] lhs {v : Map_t Int Int | v = Map_project s1 m2} - rhs {v : Map_t Int Int | v = m3 } + rhs {v : Map_t Int Int | v = m3 } id 1 tag [] diff --git a/tests/pos/polyset.fq b/tests/pos/polyset.fq new file mode 100644 --- /dev/null +++ b/tests/pos/polyset.fq @@ -0,0 +1,37 @@ +data PolySet.Lst 1 = [ + | PolySet.Cons {PolySet.Cons##lqdc##$select##PolySet.Cons##1 : @(0), PolySet.Cons##lqdc##$select##PolySet.Cons##2 : (PolySet.Lst @(0))} + | PolySet.Emp {} + ] + +constant PolySet.Cons##lqdc##$select##PolySet.Cons##1 : (func(1 , [(PolySet.Lst @(0)); + @(0)])) +constant PolySet.Cons##lqdc##$select##PolySet.Cons##2 : (func(1 , [(PolySet.Lst @(0)); + (PolySet.Lst @(0))])) +constant is$PolySet.Cons : (func(1 , [(PolySet.Lst @(0)); bool])) +constant is$PolySet.Emp : (func(1 , [(PolySet.Lst @(0)); bool])) +constant PolySet.Cons : (func(1 , [@(0); + (PolySet.Lst @(0)); + (PolySet.Lst @(0))])) +constant PolySet.lstHd : (func(1 , [(PolySet.Lst @(0)); + (Set_Set @(0))])) + +bind 1 PolySet.Emp : {VV : func(1 , [(PolySet.Lst @(0))]) | []} +bind 2 PolySet.Cons : {VV : func(1 , [@(0); + (PolySet.Lst @(0)); + (PolySet.Lst @(0))]) | []} +bind 3 p : {VV : (PolySet.Lst l##a1Uh) | []} + +constraint: + env [1; 2; 3] + lhs {VV : (PolySet.Lst (PolySet.Lst l##a1Uh)) | [(is$PolySet.Cons VV); + (~ ((is$PolySet.Emp VV))); + (VV = (PolySet.Cons p PolySet.Emp)); + ((PolySet.Cons##lqdc##$select##PolySet.Cons##1 VV) = + p); + ((PolySet.Cons##lqdc##$select##PolySet.Cons##2 VV) = + PolySet.Emp); + ((PolySet.lstHd VV) = (Set_sng p))]} + rhs {VV : (PolySet.Lst (PolySet.Lst l##a1Uh)) | [(VV = + (PolySet.Cons p PolySet.Emp))]} + id 4 tag [4] + diff --git a/tests/pos/sets01.fq b/tests/pos/sets01.fq --- a/tests/pos/sets01.fq +++ b/tests/pos/sets01.fq @@ -2,38 +2,38 @@ constant Set_sng : (func(1, [@(0); (Set_Set @(0))])) bind 1 m1 : {v : Set_Set Int | v = Set_empty 0} -bind 2 m2 : {v : Set_Set Int | v = (Set_cup (Set_cup m1 (Set_sng 10)) (Set_sng 20)) } -bind 3 m3 : {v : Set_Set Int | v = (Set_cup (Set_cup m1 (Set_sng 20)) (Set_sng 10)) } -bind 4 m4 : {v : Set_Set Int | v = (Set_cup m1 (Set_sng 10)) } -bind 5 m5 : {v : Set_Set Int | v = (Set_cup m1 (Set_sng 20)) } +bind 2 m2 : {v : Set_Set Int | v = (Set_cup (Set_cup m1 (Set_sng 10)) (Set_sng 20)) } +bind 3 m3 : {v : Set_Set Int | v = (Set_cup (Set_cup m1 (Set_sng 20)) (Set_sng 10)) } +bind 4 m4 : {v : Set_Set Int | v = (Set_cup m1 (Set_sng 10)) } +bind 5 m5 : {v : Set_Set Int | v = (Set_cup m1 (Set_sng 20)) } constraint: env [ 1 ] lhs {v : int | true } - rhs {v : int | not (Set_mem 100 m1) } + rhs {v : int | not (Set_mem 100 m1) } id 1 tag [] constraint: env [ 1; 2 ] - lhs {v : int | true } + lhs {v : int | true } rhs {v : int | not (Set_mem 100 m2) } id 2 tag [] constraint: env [ 1; 2 ] - lhs {v : int | true } + lhs {v : int | true } rhs {v : int | Set_mem 10 m2 } id 3 tag [] constraint: env [ 1; 2; 3 ] lhs {v : int | true } - rhs {v : int | m2 = m3 } + rhs {v : int | m2 = m3 } id 4 tag [] constraint: env [ 1; 2; 3; 4; 5 ] lhs {v : int | true } - rhs {v : int | m2 = Set_cup m4 m5 } + rhs {v : int | m2 = Set_cup m4 m5 } id 5 tag [] diff --git a/tests/tasty/Arbitrary.hs b/tests/tasty/Arbitrary.hs --- a/tests/tasty/Arbitrary.hs +++ b/tests/tasty/Arbitrary.hs @@ -89,9 +89,7 @@ arbitraryFiniteExpr zeroExprGen n = frequency [ (1, EApp <$> arbitraryExpr' <*> arbitraryExpr') , (1, ENeg <$> arbitraryExpr') - , (1, do - e <- EBin <$> arbitrary <*> arbitraryExpr' <*> arbitraryExpr' - return $ if divZero e then discard e else e) + , (1, EBin <$> arbitrary <*> arbitraryExpr' <*> arbitraryExpr') , (1, EIte <$> arbitraryExpr' <*> arbitraryExpr' <*> arbitraryExpr') , (1, ECst <$> arbitraryExpr' <*> arbitrary) , (1, ELam <$> arbitrary <*> arbitraryExpr') @@ -115,13 +113,6 @@ arbitraryList gen = choose (2, 3) >>= (`vectorOf` gen) arbitraryExprList = arbitraryList arbitraryExpr' - divZero :: Expr -> Bool - divZero (EBin Mod (ECon (I _)) (ECon (I 0))) = True - divZero (EBin Mod (ECon (R _)) (ECon (R 0.0))) = True - divZero (EBin Div (ECon (I _)) (ECon (I 0))) = True - divZero (EBin Div (ECon (R _)) (ECon (R 0.0))) = True - divZero _ = False - -- | Generates a finite expression, with the logarithm of the Int given -- suggesting the depth of the expression tree. arbitraryExpr :: Int -> Gen Expr @@ -375,7 +366,7 @@ prevSymExpr <- arbitraryExprInvolving prevSym n pure (sym, RR FInt (reft otherSym (PAtom Eq (EVar otherSym) prevSymExpr))) where - pairs xs = zip xs (tail xs) + pairs xs = zip xs (drop 1 xs) -- This is not random, but is simplified so that you can make chains more -- easily. diff --git a/tests/tasty/ParserTests.hs b/tests/tasty/ParserTests.hs --- a/tests/tasty/ParserTests.hs +++ b/tests/tasty/ParserTests.hs @@ -289,6 +289,12 @@ , testCase "funApp 3" $ show (doParse' predP "test" "f ([a; b])") @?= "EApp (EApp (EVar \"f\") (EVar \"a\")) (EVar \"b\")" + , testCase "funApp 4" $ + show (doParse' funAppP "" "f ?(x > 1)") @?= "EApp (EVar \"f\") (PAtom Gt (EVar \"x\") (ECon (I 1)))" + + , testCase "funApp 5" $ + show (doParse' predP "" "f ?(x > 1)") @?= "EApp (EVar \"f\") (PAtom Gt (EVar \"x\") (ECon (I 1)))" + , testCase "symbol" $ show (doParse' predP "test" "f") @?= "EVar \"f\"" diff --git a/tests/tasty/ShareMapReference.hs b/tests/tasty/ShareMapReference.hs --- a/tests/tasty/ShareMapReference.hs +++ b/tests/tasty/ShareMapReference.hs @@ -71,14 +71,14 @@ | otherwise -> let v0 = h HashMap.! k0 v1 = maybe v0 (f v0) $ HashMap.lookup k1 h - keys' = case break (HashSet.member k1) (before0 ++ after0) of + (kHead, keys') = case break (HashSet.member k1) (before0 ++ after0) of (before1, []) -> - HashSet.insert k1 keys0 : before1 + (HashSet.insert k1 keys0, before1) (before1, keys1 : after1)-> - HashSet.union keys0 keys1 : before1 ++ after1 + (HashSet.union keys0 keys1, before1 ++ after1) in sm { toHashMap = - HashSet.foldl' (\h' k' -> HashMap.insert k' v1 h') h (head keys') - , keyPartitions = keys' + HashSet.foldl' (\h' k' -> HashMap.insert k' v1 h') h kHead + , keyPartitions = kHead : keys' } mergeKeysWith _ _ _ sm = sm diff --git a/tests/tasty/ShareMapTests.hs b/tests/tasty/ShareMapTests.hs --- a/tests/tasty/ShareMapTests.hs +++ b/tests/tasty/ShareMapTests.hs @@ -1,9 +1,14 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} module ShareMapTests where import Data.HashMap.Lazy (HashMap) +#if MIN_VERSION_base(4,20,0) +import Data.List (nub) +#else import Data.List (foldl', nub) +#endif import qualified Data.ShareMap as ShareMap import qualified ShareMapReference as Reference import Test.Tasty diff --git a/tests/test.hs b/tests/test.hs --- a/tests/test.hs +++ b/tests/test.hs @@ -10,7 +10,7 @@ import Control.Monad (when) import qualified Control.Monad.State as State import Control.Monad.Trans.Class (lift) - +import Data.List (isSuffixOf) import Prelude hiding (log) import Data.Maybe (fromMaybe) import Data.Monoid (Sum(..)) @@ -76,15 +76,22 @@ , testGroup "elim-crash" <$> dirTests elimCmd "tests/crash" [] (ExitFailure 1) , testGroup "proof" <$> dirTests elimCmd "tests/proof" [] ExitSuccess , testGroup "rankN" <$> dirTests elimCmd "tests/rankNTypes" [] ExitSuccess - , testGroup "horn-pos-el" <$> dirTests elimCmd "tests/horn/pos" [] ExitSuccess - , testGroup "horn-neg-el" <$> dirTests elimCmd "tests/horn/neg" [] (ExitFailure 1) - , testGroup "horn-pos-na" <$> dirTests nativeCmd "tests/horn/pos" [] ExitSuccess - , testGroup "horn-neg-na" <$> dirTests nativeCmd "tests/horn/neg" [] (ExitFailure 1) - - -- , testGroup "todo" <$> dirTests elimCmd "tests/todo" [] (ExitFailure 1) - -- , testGroup "todo-crash" <$> dirTests elimCmd "tests/todo-crash" [] (ExitFailure 2) + , testGroup "horn-pos-el" <$> dirTests elimSaveCmd "tests/horn/pos" [] ExitSuccess + , testGroup "horn-neg-el" <$> dirTests elimSaveCmd "tests/horn/neg" [] (ExitFailure 1) + , testGroup "horn-json-pos-el" <$> dirJsonTests elimCmd "tests/horn/pos/.liquid" [] ExitSuccess + , testGroup "horn-json-neg-el" <$> dirJsonTests elimCmd "tests/horn/neg/.liquid" [] (ExitFailure 1) + , testGroup "horn-smt2-pos-el" <$> dirHornTests elimCmd "tests/horn/pos/.liquid" [] ExitSuccess + , testGroup "horn-smt2-neg-el" <$> dirHornTests elimCmd "tests/horn/neg/.liquid" [] (ExitFailure 1) + , testGroup "horn-pos-na" <$> dirTests nativeCmd "tests/horn/pos" [] ExitSuccess + , testGroup "horn-neg-na" <$> dirTests nativeCmd "tests/horn/neg" [] (ExitFailure 1) ] + where + dirTests = dirTests' isTest + dirJsonTests = dirTests' ("horn.json" `isSuffixOf`) + dirHornTests = dirTests' ("horn.smt2" `isSuffixOf`) +isTest :: FilePath -> Bool +isTest f = takeExtension f `elem` [".fq", ".smt2"] skipNativePos :: [FilePath] skipNativePos = ["NonLinear-pack.fq"] @@ -112,16 +119,15 @@ ) --------------------------------------------------------------------------- -dirTests :: TestCmd -> FilePath -> [FilePath] -> ExitCode -> IO [TestTree] +dirTests' :: (FilePath -> Bool) -> TestCmd -> FilePath -> [FilePath] -> ExitCode -> IO [TestTree] --------------------------------------------------------------------------- -dirTests testCmd root ignored code = do +dirTests' isT testCmd root ignored code = do files <- walkDirectory root - let tests = [ rel | f <- files, isTest f, let rel = makeRelative root f, rel `notElem` ignored ] + let tests = [ rel | f <- files, isT f, let rel = makeRelative root f, rel `notElem` ignored ] return $ mkTest testCmd code root <$> tests -isTest :: FilePath -> Bool -isTest f = takeExtension f `elem` [".fq", ".smt2"] + --------------------------------------------------------------------------- mkTest :: TestCmd -> ExitCode -> FilePath -> FilePath -> TestTree --------------------------------------------------------------------------- @@ -160,6 +166,11 @@ elimCmd (LO opts) bin dir file = printf "cd %s && %s --eliminate=some %s %s" dir bin opts file +elimSaveCmd :: TestCmd +elimSaveCmd (LO opts) bin dir file = + printf "cd %s && %s --save --eliminate=some %s %s" dir bin opts file + + ---------------------------------------------------------------------------------------- -- Generic Helpers ---------------------------------------------------------------------------------------- @@ -174,7 +185,7 @@ = do (ds,fs) <- partitionM doesDirectoryExist . candidates =<< (getDirectoryContents root `catchIOError` const (return [])) (fs++) <$> concatMapM walkDirectory ds where - candidates fs = [root f | f <- fs, not (isExtSeparator (head f))] + candidates fs = [root f | f@(c:_) <- fs, not (isExtSeparator c)] partitionM :: Monad m => (a -> m Bool) -> [a] -> m ([a],[a]) partitionM f = go [] [] @@ -223,7 +234,7 @@ Const summary <$ State.modify (+ 1) runGroup _ group' children = Traversal $ Functor.Compose $ do - Const soFar <- Functor.getCompose $ getTraversal children + Const soFar <- Functor.getCompose $ getTraversal $ mconcat children pure $ Const $ map (\(n,t,s) -> (group' n,t,s)) soFar computeFailures :: StatusMap -> IO Int