liquid-fixpoint 0.9.6.3 → 0.9.6.3.1

raw patch · 50 files changed

+1387/−519 lines, 50 filesdep −typed-processdep ~tastyPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: typed-process

Dependency ranges changed: tasty

API changes (from Hackage documentation)

Files

• CHANGES.md +20/−5
• bin/Fixpoint.hs +5/−1
• liquid-fixpoint.cabal +6/−5
• src/Language/Fixpoint/Horn/Info.hs +6/−4
• src/Language/Fixpoint/Horn/Parse.hs +10/−6
• src/Language/Fixpoint/Horn/SMTParse.hs +348/−0
• src/Language/Fixpoint/Horn/Solve.hs +35/−8
• src/Language/Fixpoint/Horn/Transformations.hs +45/−13
• src/Language/Fixpoint/Horn/Types.hs +191/−13
• src/Language/Fixpoint/Misc.hs +3/−1
• src/Language/Fixpoint/Parse.hs +61/−18
• src/Language/Fixpoint/Smt/Interface.hs +1/−1
• src/Language/Fixpoint/Smt/Theories.hs +74/−97
• src/Language/Fixpoint/Solver.hs +14/−3
• src/Language/Fixpoint/Solver/EnvironmentReduction.hs +5/−1
• src/Language/Fixpoint/Solver/Extensionality.hs +3/−1
• src/Language/Fixpoint/Solver/Interpreter.hs +34/−36
• src/Language/Fixpoint/Solver/Monad.hs +1/−1
• src/Language/Fixpoint/Solver/PLE.hs +37/−39
• src/Language/Fixpoint/Solver/Prettify.hs +8/−10
• src/Language/Fixpoint/Solver/Rewrite.hs +1/−3
• src/Language/Fixpoint/Solver/Sanitize.hs +4/−9
• src/Language/Fixpoint/Solver/Simplify.hs +25/−27
• src/Language/Fixpoint/Solver/Solution.hs +14/−34
• src/Language/Fixpoint/Solver/Solve.hs +11/−11
• src/Language/Fixpoint/Solver/TrivialSort.hs +3/−0
• src/Language/Fixpoint/Solver/UniqifyBinds.hs +3/−0
• src/Language/Fixpoint/Solver/UniqifyKVars.hs +3/−0
• src/Language/Fixpoint/SortCheck.hs +107/−64
• src/Language/Fixpoint/Types/Config.hs +5/−3
• src/Language/Fixpoint/Types/Constraints.hs +31/−15
• src/Language/Fixpoint/Types/Environments.hs +6/−0
• src/Language/Fixpoint/Types/Names.hs +25/−5
• src/Language/Fixpoint/Types/Refinements.hs +27/−7
• src/Language/Fixpoint/Types/Sorts.hs +71/−20
• src/Language/Fixpoint/Types/Spans.hs +17/−5
• src/Language/Fixpoint/Types/Theories.hs +23/−1
• src/Language/Fixpoint/Types/Visitor.hs +3/−3
• src/Language/Fixpoint/Utils/Files.hs +2/−0
• tests/pos/literals03.fq +1/−1
• tests/pos/literals04.fq +1/−1
• tests/pos/literals05.fq +4/−4
• tests/pos/maps03.fq +3/−3
• tests/pos/polyset.fq +37/−0
• tests/pos/sets01.fq +9/−9
• tests/tasty/Arbitrary.hs +2/−11
• tests/tasty/ParserTests.hs +6/−0
• tests/tasty/ShareMapReference.hs +5/−5
• tests/tasty/ShareMapTests.hs +5/−0
• tests/test.hs +26/−15

@@ -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 

@@ -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

@@ -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

@@ -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 ] 

@@ -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)

@@ -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)

@@ -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

@@ -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

@@ -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)])

@@ -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) }-

@@ -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)

@@ -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

@@ -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)

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -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 }   --------------------------------------------------------------------------------

@@ -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

@@ -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 

@@ -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

@@ -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

@@ -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

@@ -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 

@@ -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

@@ -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

@@ -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)

@@ -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

@@ -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.

@@ -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"

@@ -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 --------------------------------------

@@ -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) }

@@ -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

@@ -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 ----------------------------------------------------------------

@@ -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

@@ -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

@@ -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+                       }

@@ -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

@@ -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"

@@ -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 []

@@ -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 []

@@ -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 []

@@ -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 []

@@ -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]+

@@ -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 [] 

@@ -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.

@@ -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\"" 

@@ -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

@@ -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

@@ -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