liquid-fixpoint 0.9.6.3.5 → 0.9.6.3.6

raw patch · 48 files changed

+936/−458 lines, 48 filesdep −lens-familyPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: lens-family

API changes (from Hackage documentation)

Files

• CHANGES.md +19/−0
• README.md +11/−4
• bin/Fixpoint.hs +0/−0
• liquid-fixpoint.cabal +3/−3
• src/Language/Fixpoint/Graph/Deps.hs +3/−2
• src/Language/Fixpoint/Horn/Info.hs +5/−3
• src/Language/Fixpoint/Horn/Parse.hs +7/−2
• src/Language/Fixpoint/Horn/Transformations.hs +1/−1
• src/Language/Fixpoint/Horn/Types.hs +1/−0
• src/Language/Fixpoint/Misc.hs +3/−3
• src/Language/Fixpoint/Parse.hs +24/−7
• src/Language/Fixpoint/Smt/Interface.hs +2/−2
• src/Language/Fixpoint/Smt/Serialize.hs +15/−1
• src/Language/Fixpoint/Solver.hs +9/−28
• src/Language/Fixpoint/Solver/Eliminate.hs +3/−3
• src/Language/Fixpoint/Solver/EnvironmentReduction.hs +25/−9
• src/Language/Fixpoint/Solver/Extensionality.hs +2/−2
• src/Language/Fixpoint/Solver/Interpreter.hs +13/−7
• src/Language/Fixpoint/Solver/PLE.hs +54/−22
• src/Language/Fixpoint/Solver/Prettify.hs +32/−2
• src/Language/Fixpoint/Solver/Sanitize.hs +8/−8
• src/Language/Fixpoint/Solver/Solution.hs +80/−21
• src/Language/Fixpoint/Solver/Solve.hs +6/−4
• src/Language/Fixpoint/Solver/UniqifyKVars.hs +6/−5
• src/Language/Fixpoint/SortCheck.hs +35/−29
• src/Language/Fixpoint/Types.hs +2/−1
• src/Language/Fixpoint/Types/Binders.hs +10/−0
• src/Language/Fixpoint/Types/Config.hs +12/−1
• src/Language/Fixpoint/Types/Constraints.hs +30/−27
• src/Language/Fixpoint/Types/Environments.hs +35/−30
• src/Language/Fixpoint/Types/Names.hs +7/−1
• src/Language/Fixpoint/Types/PrettyPrint.hs +6/−0
• src/Language/Fixpoint/Types/Refinements.hs +184/−88
• src/Language/Fixpoint/Types/SMTPrint.hs +3/−2
• src/Language/Fixpoint/Types/Solutions.hs +9/−13
• src/Language/Fixpoint/Types/Sorts.hs +25/−1
• src/Language/Fixpoint/Types/Spans.hs +3/−3
• src/Language/Fixpoint/Types/Substitutions.hs +93/−54
• src/Language/Fixpoint/Types/Theories.hs +22/−10
• src/Language/Fixpoint/Types/Utils.hs +1/−1
• src/Language/Fixpoint/Types/Visitor.hs +37/−11
• src/Language/Fixpoint/Utils/Files.hs +7/−0
• tests/pos/frac.fq +18/−0
• tests/tasty/Arbitrary.hs +12/−2
• tests/tasty/ParserTests.hs +7/−4
• tests/tasty/SimplifyInterpreter.hs +1/−1
• tests/tasty/SimplifyTests.hs +1/−1
• tests/test.hs +44/−39

@@ -2,6 +2,25 @@  ## NEXT +## 0.9.6.3.6 (2026-05-06)++- Drop dependency on lens-family [#841](http://github.com/ucsd-progsys/liquid-fixpoint/pull/841)+- Add sort-compatibility check for measure application in PLE [#840](https://github.com/ucsd-progsys/liquid-fixpoint/pull/840)+- Eagerly expand the body of eta-expanded terms [#838](https://github.com/ucsd-progsys/liquid-fixpoint/pull/838)+- Add polymorphic kvar type variable substitution [#837](https://github.com/ucsd-progsys/liquid-fixpoint/pull/837)+- Show wf constraints in prettified fixpoint queries [#836](https://github.com/ucsd-progsys/liquid-fixpoint/pull/836)+- Unapply solutions in fqout files for readability [#835](https://github.com/ucsd-progsys/liquid-fixpoint/pull/835)+- Wildcard literals in qualifiers in horn constraints. [#834](https://github.com/ucsd-progsys/liquid-fixpoint/pull/834)+- Produce a fqout file before PLE [#835](https://github.com/ucsd-progsys/liquid-fixpoint/pull/835)+- Add `--save-dir` flag to specify output directory for generated files [#832](https://github.com/ucsd-progsys/liquid-fixpoint/pull/832)+- Add `--save-bfq-on-error` flag to collect .bfq files on verification failure [#831](https://github.com/ucsd-progsys/liquid-fixpoint/pull/831)+- Escape SMT string literals [#828](https://github.com/ucsd-progsys/liquid-fixpoint/pull/828)+- Add `cut` support to Horn query parser [#827](https://github.com/ucsd-progsys/liquid-fixpoint/pull/827)+- Fix name captures in substitution of PExist and PAll [#826](https://github.com/ucsd-progsys/liquid-fixpoint/pull/826)+- Don't require a space after the comment start [#825](https://github.com/ucsd-progsys/liquid-fixpoint/pull/825)+- Add support for fractional literals [#822](https://github.com/ucsd-progsys/liquid-fixpoint/pull/822) [#824](https://github.com/ucsd-progsys/liquid-fixpoint/pull/824)+- Generalize expressions and substitutions over binding types [#763](https://github.com/ucsd-progsys/liquid-fixpoint/pull/763)+ ## 0.9.6.3.5 (2026-01-14)  - Implement `--sortedsolution` to keep elaborated sorts in fqout/solution [#821](https:://github.com/ucsd-progsys/liquid-fixpoint/pull/821)

@@ -250,19 +250,18 @@   The important bit is that a `KVar` i.e. terms of the form  ```-     $k1[x1:=y1][x2:=y2]...[xn:=yn]+    $k1[@a:=b;a2:=b2][x1:=y1][x2:=y2]...[xn:=yn] ``` -  That is represented in the `Expr` type as+  that is represented in the `Expr` type as  ```-  | PKVar  !KVar !Subst+  | PKVar  KVar TyVarSubst Subst ```    must appear _only_ at the **top-level** that is not under _any_   other operators, i.e. not as a sub-`Expr` of other expressions. - - This is basically a predicate that needs to be "well sorted"   with respect to the `BindId`, intuitively @@ -306,6 +305,14 @@  ```     $k_##42 [x:=e1][y:=e2][v:=e3]+```++Additionally the `KVar` could have a substitution of type variables if it appears+in the return type of a type application (e.g. `f @b` with+`f : forall a. {v1:[a] | $k_##42[v:=v1]}`).++```+  f @b : {v1:[b] | $k_##42[@a:=b][v:=v1] } ```  ### Global vs. Distinct Literals

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquid-fixpoint-version:            0.9.6.3.5+version:            0.9.6.3.6 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.12.2, GHC == 9.10.1, GHC == 9.8.2+tested-with:        GHC == 9.14.1, GHC == 9.12.2, GHC == 9.10.1, GHC == 9.8.2 extra-source-files: tests/neg/*.fq                     tests/pos/*.fq                     unix/Language/Fixpoint/Utils/*.hs@@ -98,6 +98,7 @@                     Language.Fixpoint.Solver.Worklist                     Language.Fixpoint.SortCheck                     Language.Fixpoint.Types+                    Language.Fixpoint.Types.Binders                     Language.Fixpoint.Types.Config                     Language.Fixpoint.Types.Constraints                     Language.Fixpoint.Types.Environments@@ -144,7 +145,6 @@                   , gitrev              >= 1.3.1                   , hashable                   , intern-                  , lens-family                   , megaparsec           >= 7.0.0 && < 10                   , mtl                   , parser-combinators

@@ -352,11 +352,12 @@ -------------------------------------------------------------------------------- type EdgeRank = M.HashMap F.KVar Integer --------------------------------------------------------------------------------+-- | Builds a map from KVar to the _smallest_ ConstraintID that KVar appears in LHS of edgeRank :: [CEdge] -> EdgeRank edgeRank es = minimum . (n :) <$> kiM   where-    n       = 1 + maximum [ i | (Cstr i, _)     <- es ]-    kiM     = group [ (k, i) | (KVar k, Cstr i) <- es ]+    n       = 1 + maximum [ i | (Cstr i, _)     <- es ] -- number larger than maximum constraint id+    kiM     = group [ (k, i) | (KVar k, Cstr i) <- es ] -- map each `k` to cstrs in which it appears on LHS  edgeRankCut :: EdgeRank -> Cutter CVertex edgeRankCut km vs = case ks of

@@ -7,6 +7,7 @@  import           Data.Ord (Down(..), comparing) import qualified Data.HashMap.Strict            as M+import qualified Data.HashSet                   as S import qualified Data.List                      as L import qualified Data.Tuple                     as Tuple import           GHC.Generics                   (Generic)@@ -28,6 +29,7 @@   , F.ddecls    = H.qData q   , F.hoInfo    = F.cfgHoInfo cfg   , F.defns     = F.MkDefinedFuns (H.qDefs q)+  , F.kuts      = F.KS (S.fromList (H.qKuts q))   }   where     be0         = F.emptyBindEnv@@ -104,9 +106,9 @@     go (H.PAnd  ps) = F.PAnd (go <$> ps)  kvApp :: KVEnv a -> F.Symbol -> [F.Expr] -> F.Expr-kvApp kve k ys = F.PKVar (F.KV k) su+kvApp kve k ys = F.PKVar (F.KV k) M.empty su   where-    su         = F.mkSubst (zip params ys)+    su         = F.mkKVarSubst (zip params ys)     params     = maybe err1 kvParams (M.lookup k kve)     err1       = F.panic ("Unknown Horn variable: " ++ F.showpp k) @@ -123,7 +125,7 @@ kvInfo be k       = (be', KVInfo k (Misc.fst3 <$> xts) wfc)   where     -- make the WfC-    wfc           = F.WfC wenv wrft  (H.hvMeta k)+    wfc           = F.WfC wenv wrft (H.hvMeta k)     wenv          = F.fromListIBindEnv ids     wrft          = (x, t, F.KV (H.hvName k))     -- add the binders

@@ -11,7 +11,7 @@   , 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.Parse        as FP (Parser, addNumTyCon, lexeme', locLexeme', reserved', reservedOp', symbolR, upperIdR, lowerIdR, stringR, naturalR, mkFTycon, kvarP) import qualified Language.Fixpoint.Types        as F import qualified Language.Fixpoint.Horn.Types   as H import           Text.Megaparsec                hiding (State)@@ -137,6 +137,7 @@   , H.qData  =              [ dd    | HDat dd  <- things ]   , H.qOpts  =              [ o     | HOpt o   <- things ]   , H.qNums  =              [ s     | HNum s   <- things ]+  , H.qKuts  =              [ k     | HKut k   <- things ]   }  -- | A @HThing@ describes the kinds of things we may see, in no particular order@@ -156,6 +157,7 @@   | HDat !F.DataDecl   | HOpt !String   | HNum  F.Symbol+  | HKut  F.KVar   deriving (Functor)  hThingP :: FParser (HThing H.Tag)@@ -172,6 +174,7 @@         <|> HMat  <$> (reserved "match"      *> matchP)         <|> HDat  <$> (reserved "datatype"   *> dataDeclP)         <|> HNum  <$> (reserved "numeric"    *> numericDeclP)+        <|> HKut  <$> (reserved "cut"        *> FP.kvarP)  numericDeclP :: FParser F.Symbol numericDeclP = do@@ -218,7 +221,9 @@   return  $ F.mkQual n (mkParam <$> params) body pos  mkParam :: (F.Symbol, F.Sort) -> F.QualParam-mkParam (x, t) = F.QP x F.PatNone t+mkParam (x, t) = case F.stripSuffix (F.symbol (T.pack "#")) x of+  Just x' -> F.QP x' F.PatLit  t+  Nothing -> F.QP x  F.PatNone t  ------------------------------------------------------------------------------- -- | Horn Variables

@@ -476,7 +476,7 @@  predToExpr :: Pred -> F.Expr predToExpr (Reft e) = e-predToExpr (Var k xs) = F.PKVar (F.KV k) (F.Su $ M.fromList su)+predToExpr (Var k xs) = F.PKVar (F.KV k) M.empty (F.toKVarSubst $ M.fromList su)   where su = zip (kargs k) xs predToExpr (PAnd ps) = F.PAnd $ predToExpr <$> ps 

@@ -217,6 +217,7 @@   , qData  :: ![F.DataDecl]              -- ^ list of data-declarations   , qOpts  :: ![String]                  -- ^ list of fixpoint options   , qNums  :: ![F.Symbol]                -- ^ list of numeric TyCon (?)+  , qKuts  :: ![F.KVar]                  -- ^ list of cut variables   }   deriving (Data, Typeable, Generic, Functor, ToJSON, FromJSON) 

@@ -85,9 +85,9 @@ -- | Edit Distance -------------------------------------------- --------------------------------------------------------------- -{-# SCC editDistance #-}-editDistance :: Eq a => [a] -> [a] -> Int-editDistance xs ys = table ! (m, n)+{-# SCC levenshteinDistance #-}+levenshteinDistance :: Eq a => [a] -> [a] -> Int+levenshteinDistance xs ys = table ! (m, n)     where     (m,n) = (length xs, length ys)     x     = array (1,m) (zip [1..] xs)

@@ -49,6 +49,7 @@   , mkQual      -- constructing qualifiers   , infixSymbolP -- parse infix symbols   , locInfixSymbolP+  , kvarP    -- * Parsing recursive entities   , exprP        -- Expressions@@ -555,12 +556,12 @@ -- | Consumes a line comment. lhLineComment :: ParserV v () lhLineComment =-  L.skipLineComment "// "+  L.skipLineComment "//"  -- | Consumes a block comment. lhBlockComment :: ParserV v () lhBlockComment =-  L.skipBlockComment "/* " "*/"+  L.skipBlockCommentNested "/*" "*/"  -- | Parser that consumes a single char within an identifier (not start of identifier). identLetter :: ParserV v Char@@ -776,12 +777,12 @@ -- parse names as LocSymbol as well, this class can be eliminated. class (Fixpoint v, Ord v) => ParseableV v where   parseV :: ParserV v v-  mkSu :: [(Symbol, ExprV v)] -> SubstV v+  mkSu :: [(Symbol, ExprV v)] -> KVarSubst Symbol v   vFromString :: Located String -> v  instance ParseableV Symbol where   parseV = symbolP-  mkSu = mkSubst+  mkSu = mkKVarSubst   vFromString = symbol  -- | Parser for "atomic" expressions.@@ -1073,6 +1074,7 @@   <|> (reserved "real"    >> return realFTyCon)   <|> (reserved "bool"    >> return boolFTyCon)   <|> (reserved "num"     >> return numFTyCon)+  <|> (reserved "frac"    >> return fracFTyCon)   <|> (reserved "Str"     >> return strFTyCon)   <|> (mkFTycon          =<<  locUpperIdP) @@ -1095,16 +1097,32 @@ falseP = reserved "false" >> return PFalse  kvarPredP :: ParseableV v => ParserV v (ExprV v)-kvarPredP = PKVar <$> kvarP <*> substP+kvarPredP = do+  k   <- kvarP+  tsu <- tySubP+  PKVar k tsu <$> substP  kvarP :: ParserV v KVar kvarP = KV <$> lexeme (char '$' *> symbolR) -substP :: ParseableV v => ParserV v (SubstV v)+substP :: ParseableV v => ParserV v (KVarSubst Symbol v) substP = mkSu <$> many (brackets $ pairP symbolP aP exprP)   where     aP = reservedOp ":=" +-- | Parses the type-variable substitution section of a PKVar expression.+-- An empty section looks like @[@]@; a non-empty one like @[\@sym:=sort;...]@.+-- Returns an empty map if neither form is found (backward compat).+tySubP :: ParserV v (M.HashMap Symbol Sort)+tySubP = try tySub <|> pure M.empty+  where+    tySub = brackets (char '@' >> (M.fromList <$> sepBy1 tyPairP (sym ";")))+    tyPairP = do+      s <- symbolP+      _ <- reservedOp ":="+      t <- sortP+      return (s, t)+ -- | Parses a semicolon-separated bracketed list of predicates. -- -- Used as the argument of the prefix-versions of conjunction and@@ -1558,4 +1576,3 @@  instance Inputable [Command] where   rr' = doParse' commandsP-

@@ -65,7 +65,7 @@     ) where  import           Language.Fixpoint.Types.Config ( SMTSolver (..), solverFlags-                                                , Config (solver, smtTimeout, noStringTheory, save, allowHO))+                                                , Config (solver, smtTimeout, noStringTheory, save, saveDir, allowHO)) import qualified Language.Fixpoint.Misc          as Misc import           Language.Fixpoint.Types.Errors import           Language.Fixpoint.Utils.Files@@ -278,7 +278,7 @@                LBS.hPutStr hLog "\n"        return me     where-       smtFile = extFileName Smt2 f+       smtFile = extFileNameR' (saveDir cfg) Smt2 f  makeContextWithSEnv :: Config -> FilePath -> SymEnv -> DefinedFuns -> IO Context makeContextWithSEnv cfg f env defns = do

@@ -25,6 +25,8 @@ -- import           Data.Text.Format import           Language.Fixpoint.Misc (sortNub, errorstar) import           Language.Fixpoint.Utils.Builder as Builder+import qualified Data.Text as T+import Data.Text (Text) -- import Debug.Trace (trace)  instance SMTLIB2 (Symbol, Sort) where@@ -125,7 +127,19 @@   smt2 = smt2 . val  instance SMTLIB2 SymConst where-  smt2 = smt2 . symbol+  smt2 c@(SL t) = do+    seStr <- gets seString+    if seStr+      then pure $ quotes $ fromText $ smtEscape t  -- emit "hello" not lit$36$hello+      else smt2 (symbol c)++-- | Per https://smt-lib.org/theories-UnicodeStrings.shtml+-- "SMT-LIB 2.6 has one escape sequence of its own for string literals. Two+--  double quotes ("") are used to represent the double-quote character within+--  a string literal"++smtEscape :: Text -> Text+smtEscape = T.replace "\"" "\"\""  instance SMTLIB2 Constant where   smt2 (I n)   = pure $ bShow n

@@ -59,6 +59,7 @@ import qualified Language.Fixpoint.Types as Types (GInfo(..)) import           Language.Fixpoint.Minimize (minQuery, minQuals, minKvars) import           Control.DeepSeq+import           Data.Functor                        (void) import qualified Data.ByteString as B import Data.Maybe (catMaybes) import qualified Text.PrettyPrint.HughesPJ as PJ@@ -116,11 +117,13 @@   :: (PPrint a, NFData a, Fixpoint a, Show a, Loc a)   => Config -> FInfo a -> IO (Result (Integer, a)) solve' cfg q = do-  when (save cfg) $ saveQuery   cfg q-  if multicore cfg then-    solvePar cfg q-  else-    solveNative cfg (slice cfg q)+    when (save cfg) $ saveQuery cfg q+    res <- if multicore cfg then+             solvePar cfg q+           else+             solveNative cfg (slice cfg q)+    when (saveBfqOnError cfg && isUnsafe res) $ saveBinaryQuery cfg (void q)+    return res  -------------------------------------------------------------------------------- readFInfo :: FilePath -> IO (FInfo (), [String])@@ -287,7 +290,7 @@   -- rnf soln `seq` donePhase Loud "Solve2"   --let stat = resStatus res   -- saveSolution cfg res-  when (save cfg) $ saveSolution cfg res+  when (save cfg) $ Sol.saveSolution cfg "" res   -- writeLoud $ "\nSolution:\n"  ++ showpp (resSolution res)   -- colorStrLn (colorResult stat) (show stat)   return res@@ -306,28 +309,6 @@   return $ mempty { Types.quals = Types.quals  fi                   , Types.gLits = Types.gLits  fi                   , Types.dLits = Types.dLits  fi }--saveSolution :: Config -> Result a -> IO ()-saveSolution cfg res = when (save cfg) $ do-  let f = queryFile Out cfg-  putStrLn $ "Saving Solution: " ++ f ++ "\n"-  ensurePath f-  writeFile f $ unlines $-    [ ""-    , "Solution:"-    , scopedRender (resSolution  res)-    ] ++-    [ ""-    , ""-    , "Non-cut kvars:"-    , ""-    , scopedRender (HashMap.map forceDelayed $ resNonCutsSolution res)-    ]-    where-      scopedRender = PJ.render . PJ.vcat . map ncDoc . scoped-      scoped sol = [ (k, scope k, e) | (k, e) <- HashMap.toList sol]-      scope k = HashMap.lookupDefault [] k $ resSorts res-      ncDoc (k, xts, e) = PJ.hsep [ pprint k PJ.<> pprint xts, ":=", pprint e ]  simplifyResult :: Config -> Result a -> Result a simplifyResult cfg res =

@@ -111,12 +111,12 @@     cs            = getSubC   si <$> M.lookupDefault [] k kI  nonCutCube :: SimpC a -> Sol.Cube-nonCutCube c = Sol.Cube (senv c) (rhsSubst c) (subcId c) (stag c)+nonCutCube c = Sol.Cube (senv c) (substFromKSubst $ rhsSubst c) (subcId c) (stag c) -rhsSubst :: SimpC a -> Subst+rhsSubst :: SimpC a -> KVarSubst Symbol Symbol rhsSubst             = rsu . crhs   where-    rsu (PKVar _ su) = su+    rsu (PKVar _ _ su) = su     rsu _            = errorstar "Eliminate.rhsSubst called on bad input"  getSubC :: SInfo a -> Integer -> SimpC a

@@ -37,6 +37,8 @@ #else import           Data.List (foldl', partition) #endif+import           Data.Functor.Const (Const(..))+import           Data.Functor.Identity (Identity(..)) import           Data.Maybe (fromMaybe) import           Data.ShareMap (ShareMap) import qualified Data.ShareMap as ShareMap@@ -72,12 +74,11 @@ import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Refinements   ( Brel(..)-  , ExprV(..)+  , ExprBV(..)   , Expr   , KVar(..)   , SortedReft(..)-  , Subst-  , SubstV(..)+  , KVarSubst   , pattern PTrue   , pattern PFalse   , dropECst@@ -91,11 +92,10 @@   , reftPred   , sortedReftSymbols   , subst1+  , fromKVarSubst   ) import           Language.Fixpoint.Types.Sorts (boolSort, sortSymbols) import           Language.Fixpoint.Types.Visitor (mapExprOnExpr)-import           Lens.Family2 (Lens', view, (%~))-import           Lens.Family2.Stock (_2) import Language.Fixpoint.Misc (snd3)  -- | Strips from all the constraint environments the bindings that are@@ -399,7 +399,7 @@    in       (bindIdsByKVar, substsByKVar, kvarsBySubC)   where-    kvarsByBindId :: HashMap BindId (HashMap KVar [Subst])+    kvarsByBindId :: HashMap BindId (HashMap KVar [KVarSubst Symbol Symbol])     kvarsByBindId =       HashMap.map (exprKVars . reftPred . sr_reft . snd3) $ beBinds bindEnv @@ -408,9 +408,8 @@     kvarBindsFromSubC :: ReducedConstraint a -> HashMap KVar (HashSet Symbol)     kvarBindsFromSubC sc =       let c = originalConstraint sc-          unSubst (Su su) = su           substsToHashSet =-            HashSet.fromMap . HashMap.map (const ()) . HashMap.unions . map unSubst+            HashSet.fromMap . HashMap.map (const ()) . HashMap.unions . map fromKVarSubst        in foldl' (HashMap.unionWith HashSet.union) HashMap.empty $           map (HashMap.map substsToHashSet) $           (exprKVars (reftPred $ sr_reft $ srhs c) :) $@@ -572,6 +571,23 @@           ]         ) +-- lens+--+-- We use internally the following lens to modify the SortedReft in the+-- environment. This was imported from lens-family, but we don't want to depend+-- on the whole library for just these few definitions.++type Lens' s a = forall f. Functor f => (a -> f a) -> s -> f s++_2 :: Lens' (a, b) b+_2 f (a, b) = fmap (a,) (f b)++view :: Lens' s a -> s -> a+view l s = getConst (l Const s)++(%~) :: Lens' s a -> (a -> a) -> s -> s+(%~) l f s = runIdentity (l (Identity . f) s)+ -- | Inlines some of the bindings whose symbol satisfies a given predicate. -- -- Only works if the bindings don't form cycles.@@ -584,7 +600,7 @@ substBindingsSimplifyingWith simplifier vLens p env =     -- Circular program here. This should terminate as long as the     -- bindings introduced by ANF don't form cycles.-    let env' = HashMap.map (vLens %~ simplifier . inlineInSortedReft (srLookup filteredEnv)) env+    let env' = HashMap.map (vLens %~ (simplifier . inlineInSortedReft (srLookup filteredEnv))) env         filteredEnv = HashMap.filterWithKey (\sym _v -> p sym) env'      in env'   where

@@ -137,7 +137,7 @@     go p e@(ESym _)      = f p e     go p e@(ECon _)      = f p e     go p e@(EVar _)      = f p e-    go p e@(PKVar _ _)   = f p e+    go p e@(PKVar {})      = f p e     go p (ENeg e)        = f p . ENeg =<< go p e     go p (ECst e t)      = f p . (`ECst` t) =<< go p e     go p (ECoerc a t e)  = f p . ECoerc a t =<< go p e@@ -169,7 +169,7 @@     go e@(ESym _)        = e     go e@(ECon _)        = e     go e@(EVar _)        = e-    go e@(PKVar _ _)     = e+    go e@(PKVar {})        = e     go e@(ENeg _)        = e     go (PNot e)          = PImp e PFalse     go e@(ECst _ _)      = e

@@ -136,7 +136,8 @@   where     withRewrites exprs =       let-        rws = [rewrite e rw | rw <- snd <$> M.toList (knSims γ)+        sortEnv = seSort (evEnv env)+        rws = [rewrite sortEnv e rw | rw <- snd <$> M.toList (knSims γ)                             ,  e <- S.toList (snd `S.map` exprs)]       in         exprs <> S.fromList (concat rws)@@ -162,8 +163,8 @@   res <- evalOne env γ env' ictx e   return (ictx, res : acc) -rewrite :: Expr -> Rewrite -> [(Expr,Expr)]-rewrite e rw = Mb.mapMaybe (`rewriteTop` rw) (notGuardedApps e)+rewrite :: SEnv Sort -> Expr -> Rewrite -> [(Expr,Expr)]+rewrite env e rw = filter (wellSorted env . fst) $ Mb.mapMaybe (`rewriteTop` rw) (notGuardedApps e)  rewriteTop :: Expr -> Rewrite -> Maybe (Expr,Expr) rewriteTop e rw@@ -174,6 +175,10 @@   | otherwise   = Nothing +-- | Check that an expression is well-sorted+wellSorted :: SEnv Sort -> Expr -> Bool+wellSorted env = Mb.isJust . checkSortExpr dummySpan env+ ---------------------------------------------------------------------------------------------- -- | Step 3: @resSInfo@ uses incremental PLE result @InstRes@ to produce the strengthened SInfo ----------------------------------------------------------------------------------------------@@ -262,8 +267,9 @@           , icSubcId = cidMb -- fst <$> L.find (\(_, b) -> (head delta) `memberIBindEnv` (_cenv b)) ieCstrs           }                  -- eliminate above if nothing broken   where-    initEqs   = S.fromList $ concat [rewrite e rw | e  <- cands ++ (snd <$> S.toList (icEquals ctx))+    initEqs   = S.fromList $ concat [rewrite sortEnv e rw | e  <- cands ++ (snd <$> S.toList (icEquals ctx))                                                   , rw <- snd <$> M.toList (knSims ieKnowl)]+    sortEnv   = seSort (evEnv ieEvEnv)     cands     = concatMap (makeCandidates ieKnowl ctx) (rhs:es)     sims      = S.filter (isSimplification (knDCs ieKnowl)) (initEqs <> icEquals ctx)     econsts   = M.fromList $ findConstants ieKnowl es@@ -365,7 +371,7 @@       ELam _ _ -> acc       ETApp _ _ -> acc       ETAbs _ _ -> acc-      PKVar _ _ -> acc+      PKVar {} -> acc       PAll _ _ -> acc       PExist _ _ -> acc @@ -392,7 +398,7 @@       ELam _ _ -> acc       ETApp _ _ -> acc       ETAbs _ _ -> acc-      PKVar _ _ -> acc+      PKVar {} -> acc       PAll _ _ -> acc       PExist _ _ -> acc @@ -547,7 +553,7 @@ interpret ie γ ctx env (PAtom o e1 e2)  = let e1' = interpret' ie γ ctx env e1                                               e2' = interpret' ie γ ctx env e2 in                                             applyBooleanFolding o e1' e2'-interpret _  _ _   _   e@(PKVar _ _)    = e+interpret _  _ _   _   e@(PKVar {})       = e interpret ie γ ctx env e@(PAll xss e1)  = case xss of   [] -> interpret' ie γ ctx env e1   _  -> e

@@ -705,6 +705,8 @@  data EvalType =     NoRW       -- Normal PLE+  | NoRWEta    -- Like Normal PLE but we keep track that we are in an eta+               -- expansion context   | FuncNormal -- REST: Expand function definitions only when the branch can be decided   | RWNormal   -- REST: Fully Expand Defs in the context of rewriting (similar to NoRW)   deriving (Eq)@@ -788,24 +790,30 @@     isEtaSymbol = isPrefixOfSym "eta"  evalELam γ ctx et (x, s) e = do-    oldPendingUnfoldings <- gets evPendingUnfoldings-    oldEqs <- gets evNewEqualities+  e' <- evalInExtendedEnv [(x, s)] γ ctx et e+  let elam = ELam (x, s) e+  modify $ \st -> st+    { evNewEqualities = S.insert (elam, ELam (x, s) e') (evNewEqualities st) }+  return (ELam (x, s) e') -    -- We need to declare the variable in the environment-    modify $ \st -> st-      { evEnv = insertSymEnv x s $ evEnv st }+evalInExtendedEnv :: [(Symbol, Sort)] -> Knowledge -> ICtx -> EvalType -> Expr -> EvalST Expr+evalInExtendedEnv binds γ ctx et e = do+  oldPendingUnfoldings <- gets evPendingUnfoldings+  oldEqs               <- gets evNewEqualities+  -- We need to declare the variables in the environment+  modify $ \st -> st+    { evEnv = insertsSymEnv (evEnv st) binds }+  e' <- eval (γ { knLams = binds ++ knLams γ }) ctx et e+  let e'' = simplify γ ctx e'+  -- Discard the old equalities which miss the lambda binding+  modify $ \st -> st+    { evPendingUnfoldings = oldPendingUnfoldings+    , evNewEqualities = oldEqs+    -- Leaving the scope thus we need to get rid of it+    , evEnv = deletesSymEnv (evEnv st) (map fst binds)+    }+  pure e'' -    e' <- eval (γ { knLams = (x, s) : knLams γ }) ctx et e-    let e2' = simplify γ ctx e'-        elam = ELam (x, s) e-    -- Discard the old equalities which miss the lambda binding-    modify $ \st -> st-      { evPendingUnfoldings = oldPendingUnfoldings-      , evNewEqualities = S.insert (elam, ELam (x, s) e2') oldEqs-      -- Leaving the scope thus we need to get rid of it-      , evEnv = deleteSymEnv x $ evEnv st-      }-    return (ELam (x, s) e')  data RESTParams oc = RP   { oc   :: OCAlgebra oc Expr IO@@ -1076,11 +1084,15 @@          let e2' = stripPLEUnfold e'          let e3' = simplify γ ctx (eApps e2' es2)  -- reduces a bit the equations -         if hasUndecidedGuard e' && guardOf e' == guardOf newE' then do+         if hasUndecidedGuard e' && guardOf e' == guardOf newE' && et /= NoRWEta then do            -- Don't unfold the expression if there is an if-then-else guarding            -- it, just to preserve the size of further rewrites.            -- If evalIte does any modifications, though, we do unfold in order            -- to allow analysis of the resulting expression+           -- Note(Alessio): this optimization make sense only if the+           -- function is already fully applied in the original+           -- program and not because of eta expansion, otherwise we might+           -- miss redexes. See https://github.com/ucsd-progsys/liquidhaskell/issues/2652            modify $ \st -> st              { evPendingUnfoldings =                  M.insertWith M.union (evExScope st) (M.singleton (eApps e0 es) e3') (evPendingUnfoldings st)@@ -1132,10 +1144,17 @@ evalApp γ ctx e0 es _et   | eqs@(_:_) <- noUserDataMeasureEqs γ (eApps e0 es)   = do-       let eqs' = map (second $ simplify γ ctx) eqs-       modify $ \st ->-         st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }-       return Nothing+       env <- gets (seSort . evEnv)+       -- Only well-sorted LHSs should be considered. For instance, a measure+       -- expecting an argument of type [[Int]] should not be applied to a value+       -- of type [Int].+       let eqs' = map (second $ simplify γ ctx) $+                    filter (wellSorted env . fst) eqs+       if null eqs' then return Nothing+       else do+         modify $ \st ->+           st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }+         return Nothing  evalApp γ ctx e0 es et   | ELam (argName, _) body <- dropECst e0@@ -1167,7 +1186,7 @@         { evNewEqualities = S.insert (eApps e0 es, expandedTerm) (evNewEqualities st) }       return (Just expandedTerm) -evalApp _γ ctx e0 es _et+evalApp γ ctx e0 es _et   -- We check the annotation instead of the equations in γ for two reasons.   --   -- First, we want to eta expand functions that might not be reflected. Suppose@@ -1202,6 +1221,15 @@     -- is already handled by the previous case of evalApp     modify $ \st -> st       { evNewEqualities = S.insert (eApps e0 es, etaExpandedTerm) (evNewEqualities st) }++    -- We also try to unfold the definition of the function in the eta+    -- expanded body, as it might give us more information to generate+    -- better equalities. Note that we pass NoRWEta to skip the optimization+    redBody <- evalInExtendedEnv (zip etaNames etaArgsType) γ ctx NoRWEta fullBody+    let etaExpandedRedBody = mkLams redBody (zip etaNames etaArgsType)+    modify $ \st -> st+      { evNewEqualities = S.insert (eApps e0 es, etaExpandedRedBody) (evNewEqualities st) }+     return (Just etaExpandedTerm)   where     unpackFFuncs (FFunc t ts) = t : unpackFFuncs ts@@ -1237,6 +1265,10 @@   , (rw, NoUserDataSMeasure) <- rws   , length es == length (smArgs rw)   ]++-- | Check that an expression is well-sorted+wellSorted :: SEnv Sort -> Expr -> Bool+wellSorted env = Mb.isJust . checkSortExpr dummySpan env  -------------------------------------------------------------------------------- -- | 'substEq' unfolds or instantiates an equation at a particular list of

@@ -9,9 +9,10 @@ import           Data.Bifunctor (first) import           Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as HashMap+import qualified Data.HashMap.Strict as M import           Data.HashSet (HashSet) import qualified Data.HashSet as HashSet-import           Data.List (intersperse, sortOn)+import           Data.List (group, intersperse, sortOn) import           Data.Maybe (fromMaybe) import           Data.Text (Text) import qualified Data.Text as Text@@ -38,9 +39,11 @@   ) import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Refinements-  ( ExprV(..)+  ( ExprBV(..)   , pattern PFalse+  , pattern PKVar   , Reft+  , ReftBV(..)   , SortedReft(..)   , conjuncts   , expr@@ -72,6 +75,10 @@   map     (prettyConstraint (bs info) . snd)     (sortOn fst $ HashMap.toList (cm info))+  +++  map+    (prettyWfConstraint (bs info) . snd)+    (sortOn fst $ HashMap.toList (ws info))  prettyConstraint   :: Fixpoint a@@ -130,6 +137,29 @@       , sr_sort sr       , reftPred $ sr_reft sr       )++prettyWfConstraint+  :: Fixpoint a+  => BindEnv a+  -> WfC a+  -> Doc+prettyWfConstraint bindEnv wfc =+  let prettyEnv =+        concatMap (take 1) $+        group $   -- eliminate duplicates+        sortOn fst+          [ (s, sr_sort sr)+          | bId <- elemsIBindEnv $ wenv wfc+          , let (s, sr, _a) = lookupBindEnv bId bindEnv+          ]+      (v, t, k) = wrft wfc+   in hang (text "\n\nwf:") 2 $+          hang (text "env:") 2+            (vcat $ map prettyBind prettyEnv)+      $+$ text "reft" <+> toFix (RR t (Reft (v, PKVar k M.empty mempty)))+      $+$ toFixMeta (text "wf") (toFix (winfo wfc))+  where+    prettyBind (s, srt) = toFix s <+> ":" <+> toFix srt  pprId :: Show a => Maybe a -> Doc pprId (Just i)  = "id" <+> text (show i)

@@ -189,7 +189,7 @@ -- | `dropDeadSubsts` removes dead `K[x := e]` where `x` NOT in the domain of K. -------------------------------------------------------------------------------- dropDeadSubsts :: F.SInfo a -> F.SInfo a-dropDeadSubsts si = mapKVarSubsts (F.filterSubst . f) si+dropDeadSubsts si = mapKVarSubsts (\k su -> F.toKVarSubst $ M.filterWithKey (f k) $ F.fromKVarSubst su) si   where     kvsM          = M.mapWithKey (\k _ -> kvDom k) (F.ws si)     kvDom         = S.fromList . F.kvarDomain si@@ -244,9 +244,9 @@ badParams :: F.SInfo a -> F.SimpC a -> M.HashMap F.KVar [F.Symbol] badParams si c = Misc.group bads   where-    bads       = [ (k, x) | (v, k, F.Su su) <- subcKSubs xsrs c+    bads       = [ (k, x) | (v, k, su) <- subcKSubs xsrs c                           , let vEnv = maybe sEnv (`S.insert` sEnv) v-                          , (x, e)          <- M.toList su+                          , (x, e)          <- M.toList (F.fromKVarSubst su)                           , badArg vEnv e                  ]     sEnv       = S.fromList (fst <$> xsrs)@@ -256,16 +256,16 @@ badArg sEnv (F.EVar y) = not (y `S.member` sEnv) badArg _    _          = True -type KSub = (Maybe F.Symbol, F.KVar, F.Subst)+type KSub = (Maybe F.Symbol, F.KVar, F.KVarSubst F.Symbol F.Symbol)  subcKSubs :: [(F.Symbol, F.SortedReft)] -> F.SimpC a -> [KSub] subcKSubs xsrs c = rhs ++ lhs   where     lhs          = [ (Just v, k, su) | (_, sr) <- xsrs                                      , let rs   = F.reftConjuncts (F.sr_reft sr)-                                     , F.Reft (v, F.PKVar k su) <- rs+                                     , F.Reft (v, F.PKVar k _ su) <- rs                    ]-    rhs          = [(Nothing, k, su) | F.PKVar k su <- [F.crhs c]]+    rhs          = [(Nothing, k, su) | F.PKVar k _ su <- [F.crhs c]]   initKvarEnv :: F.SInfo a -> KvDom@@ -361,11 +361,11 @@ --   it makes it hard to actually find the fundefs within (breaking PLE.) -------------------------------------------------------------------------------- symbolEnv :: HasCallStack => Config -> F.SInfo a -> F.SymEnv-symbolEnv cfg si = F.symEnv sEnv thyEnv ds lits (ts ++ ts')+symbolEnv cfg si = F.symEnv cfg sEnv thyEnv ds lits (ts ++ ts')   where     ts'          = applySorts ae'     ae'          = elaborate (ElabParam ef (F.atLoc E.dummySpan "symbolEnv") env0) (F.ae si)-    env0         = F.symEnv sEnv thyEnv ds lits ts+    env0         = F.symEnv cfg sEnv thyEnv ds lits ts     thyEnv       = theoryEnv cfg si     ds           = F.ddecls si     ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])

@@ -14,29 +14,36 @@     -- * Apply Solution   , applyInSortedReft   , CombinedEnv(..)+  , qbPreds      -- * Lookup Solution   , lhsPred    , nonCutsResult +    -- * Save Solution+  , saveSolution+     -- * Exported for Testing   , simplifyKVar   , alphaEq   ) where  import           Control.Arrow (second, (***))-import           Control.Monad                  (guard, mplus)+import           Control.Monad                  (guard, mplus, when) import           Control.Monad.Reader import qualified Data.HashSet                   as S import qualified Data.HashMap.Strict            as M import qualified Data.List                      as List import           Data.Maybe                     (maybeToList, isJust, isNothing)+import qualified Text.PrettyPrint.HughesPJ      as PJ import           Language.Fixpoint.Types.PrettyPrint () import           Language.Fixpoint.Types.Visitor      as V import           Language.Fixpoint.SortCheck          (ElabM) import qualified Language.Fixpoint.SortCheck          as So+import           Language.Fixpoint.Misc               (ensurePath) import qualified Language.Fixpoint.Misc               as Misc+import qualified Language.Fixpoint.Utils.Files        as Files import           Language.Fixpoint.Types.Config import qualified Language.Fixpoint.Types              as F import qualified Language.Fixpoint.Types.Solutions    as Sol@@ -85,10 +92,11 @@ --------------------------------------------------------------------------------  refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> ElabM Sol.QBind-refine info qs genv w = refineK (allowHOquals info) env qs (F.wrft w)+refine info qs genv w = refineK (allowHOquals info) env lits qs (F.wrft w)   where     env             = wenvSort <> genv     wenvSort        = F.sr_sort <$> F.fromListSEnv (F.envCs (F.bs info) (F.wenv w))+    lits            = getConstants info  instConstants :: F.SInfo a -> F.SEnv F.Sort instConstants = F.fromListSEnv . filter notLit . F.toListSEnv . F.gLits@@ -96,26 +104,43 @@     notLit    = not . F.isLitSymbol . fst  -refineK :: Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> ElabM Sol.QBind-refineK ho env qs (v, t, _k) = Sol.qbFilterM (okInst env v t) eqs+refineK :: Bool -> F.SEnv F.Sort -> [F.Constant] -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> ElabM Sol.QBind+refineK ho env lits qs (v, t, _k) = Sol.qbFilterM (okInst env v t) eqs    where-    eqs = instK ho env v t qs+    eqs = instK ho env lits v t qs  -------------------------------------------------------------------------------- instK :: Bool       -> F.SEnv F.Sort+      -> [F.Constant]       -> F.Symbol       -> F.Sort       -> QCluster       -> Sol.QBind ---------------------------------------------------------------------------------instK ho env v t qc = Sol.qb . unique $-  [ Sol.eQual q xs+instK ho env lits v t qc = Sol.qb . unique $+  [ Sol.eQual q xs ls       | (sig, qs) <- M.toList qc-      , xs        <- instKSig ho env v t sig+      , let (varSig, litSig) =  splitSig sig+      , xs        <- instKSig ho env v t varSig+      , ls        <- instLitSig lits litSig       , q         <- qs   ] +-- split the QCSig into the parts that are for regular variables vs for wildcard-literals that are defined as `a#`, `b#` etc.+-- e.g. see tests/horn/pos/wild_lits*.smt2+splitSig :: QCSig -> (QCSig, QCSig)+splitSig = List.partition (\qp -> qpPat qp /= PatLit)++instLitSig :: [F.Constant] -> QCSig -> [[F.Constant]]+instLitSig lits sig = sequence [ filter (matchSort (qpSort qp)) lits | qp <- sig ]++matchSort :: F.Sort -> F.Constant -> Bool+matchSort F.FInt  (F.I _)    = True+matchSort F.FReal (F.R _)    = True+matchSort s       (F.L _ s') = s == s'+matchSort _       _          = False+ unique :: [Sol.EQual] -> [Sol.EQual] unique qs = M.elems $ M.fromList [ (Sol.eqPred q, q) | q <- qs ] @@ -219,6 +244,7 @@   F.PatSuffix i s -> JustSub i <$> F.stripSuffix s y   F.PatNone       -> Just NoSub   F.PatExact s    -> if s == y then Just NoSub else Nothing+  F.PatLit        -> Nothing   where     y             =  F.unKArgSymbol y' @@ -241,8 +267,7 @@   where     sr            = F.RR t (F.Reft (v, p))     p             = Sol.eqPred eq--    -- _msg          = printf "okInst: t = %s, eq = %s, env = %s" (F.showpp t) (F.showpp eq) (F.showpp env)+    -- _msg          = printf "okInst: t = %s, eq = %s" (F.showpp t) (F.showpp eq)   --------------------------------------------------------------------------------@@ -328,13 +353,19 @@ applyKVar :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVSub -> ExprInfo applyKVar cfg  g s ksu = case Sol.lookup s (F.ksuKVar ksu) of   Left cs   -> hypPred cfg g s ksu cs-  Right eqs -> let qbp = Sol.qbPreds (F.ksuSubst ksu) eqs-                in (F.pAndNoDedup $ fst <$> qbp, mempty) -- TODO: don't initialize kvars that have a hyp solution+  Right eqs -> let qbp = qbPreds+                           (F.substFromKSubst $ F.ksuSubst ksu)+                           (F.ksuTySub ksu)+                           eqs+                   preds = fst <$> qbp+                in (F.pAndNoDedup preds, mempty) -- TODO: don't initialize kvars that have a hyp solution +qbPreds :: F.Subst -> F.TyVarSubst -> Sol.QBind -> [(F.Pred, Sol.EQual)]+qbPreds su tvsu (Sol.QB eqs) =+  [ (F.subst su $ V.applyCoSub tvsu $ Sol.eqPred eq, eq) | eq <- eqs ]+ mkNonCutsExpr :: Config -> CombinedEnv ann -> Sol.Sol Sol.QBind -> F.KVar -> Sol.Hyp -> F.Expr-mkNonCutsExpr cfg ce s k cs =-  let bcps = map (bareCubePred cfg ce s k) cs-   in F.pOr bcps+mkNonCutsExpr cfg ce s k cs = F.pOr (bareCubePred cfg ce s k <$> cs)  nonCutsResult :: Config -> F.BindEnv ann -> Sol.Sol Sol.QBind -> FixDelayedSolution nonCutsResult cfg be s = M.mapWithKey (\k -> Delayed . mkNonCutsExpr cfg g s k) $ Sol.sHyp s@@ -368,11 +399,11 @@         (p, _kI) = apply cfg g' s bs      in F.pExist yts (p F.&.& psu)   where-    bs = Sol.cuBinds c+    bs     = Sol.cuBinds c     F.Su m = dropUnsortedExprs cfg g' (Sol.cuSubst c)-    g' = addCEnv  g bs-    bs' = F.diffIBindEnv bs (Misc.safeLookup "sScp" k (Sol.sScp s))-    yts = symSorts g bs'+    g'     = addCEnv  g bs+    bs'    = F.diffIBindEnv bs (Misc.safeLookup "sScp" k (Sol.sScp s))+    yts    = symSorts g bs'  -- | At the moment, the liquid-fixpoint implementation allows for unsorted -- expressions in substitutions. See the discussion in@@ -417,12 +448,14 @@         -- Free variables in p should not colide with those generated by         -- the rapier substitution. If that were the case, perhaps we would         -- need to include @combinedSEnv g@ in the scope set.-     in (F.rapierSubstExpr (F.substSymbolsSet su) su p, kI)+        p' = F.rapierSubstExpr (F.substSymbolsSet su) su $+             V.applyCoSub (F.ksuTySub ksu) p+     in (p', kI)   where     bs' = F.diffIBindEnv bs (Misc.safeLookup "sScp" k (Sol.sScp s))     bs  = Sol.cuBinds c     k   = F.ksuKVar ksu-    su = dropUnsortedExprs cfg g (F.ksuSubst  ksu)+    su = dropUnsortedExprs cfg g (F.substFromKSubst $ F.ksuSubst  ksu)  -- | @cubePredExc@ computes the predicate for the subset of binders bs'. --@@ -644,3 +677,29 @@     isVarIn (F.EVar s) vs       | elem s vs = Just s     isVarIn _ _vs = Nothing++--------------------------------------------------------------------------------+-- | Save Solution to File -----------------------------------------------------+--------------------------------------------------------------------------------++saveSolution :: Config -> String -> Result a -> IO ()+saveSolution cfg sfx res = when (save cfg) $ do+  let f = Files.tempFileName (srcFile cfg ++ sfx ++ ".fqout")+  putStrLn $ "Saving Solution: " ++ f ++ "\n"+  ensurePath f+  writeFile f $ unlines $+    [ ""+    , "Solution:"+    , scopedRender (resSolution  res)+    ] +++    [ ""+    , ""+    , "Non-cut kvars:"+    , ""+    , scopedRender (M.map forceDelayed $ resNonCutsSolution res)+    ]+    where+      scopedRender = PJ.render . PJ.vcat . map ncDoc . scoped+      scoped sol = [ (k, scope k, So.unApply e) | (k, e) <- M.toList sol]+      scope k = M.lookupDefault [] k $ resSorts res+      ncDoc (k, xts, e) = PJ.hsep [ F.pprint k PJ.<> F.pprint xts, PJ.text ":=", F.pprint e ]

@@ -153,6 +153,8 @@    res2  <- case resStatus res1 of  {- then run normal PLE on remaining unsolved constraints -}     Unsafe _ bads2 | rewriteAxioms cfg -> do+      when (save cfg) $+        liftIO $ S.saveSolution cfg ".pre-ple" res1       liftSMT $ smtComment "solve: ple"       bs <- liftSMT $ PLE.instantiate cfg fi1 (Just s3) (Just $ map fst bads2)       -- Check the constraints one last time after PLE@@ -268,12 +270,12 @@     rhsCands s = M.toList $ M.fromList $ map cnd ks       where         ks          = predKs . F.crhs $ c-        cnd :: (F.KVar, F.Subst) -> (F.KVar , Sol.Cand Sol.EQual)-        cnd (k, su) = (k, Sol.qbPreds su (Sol.lookupQBind s k))+        cnd :: (F.KVar, F.Subst, F.TyVarSubst) -> (F.KVar , Sol.Cand Sol.EQual)+        cnd (k, su, tvsu) = (k, S.qbPreds su tvsu (Sol.lookupQBind s k)) -predKs :: F.Expr -> [(F.KVar, F.Subst)]+predKs :: F.Expr -> [(F.KVar, F.Subst, F.TyVarSubst)] predKs (F.PAnd ps)    = concatMap predKs ps-predKs (F.PKVar k su) = [(k, su)]+predKs (F.PKVar k tvsu su) = [(k, F.substFromKSubst su, tvsu)] predKs _              = []  --------------------------------------------------------------------------------

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP                    #-}+{-# LANGUAGE ViewPatterns           #-} {-# OPTIONS_GHC -Wno-name-shadowing #-}  {- | This module creates new bindings for each argument of each kvar.@@ -56,14 +57,14 @@ -------------------------------------------------------------------------------- remakeSubsts fi = mapKVarSubsts (remakeSubst fi) fi -remakeSubst :: SInfo a -> KVar -> Subst -> Subst+remakeSubst :: SInfo a -> KVar -> KVarSubst Symbol Symbol -> KVarSubst Symbol Symbol remakeSubst fi k su = foldl' (updateSubst k) su (kvarDomain fi k) -updateSubst :: KVar -> Subst -> Symbol -> Subst-updateSubst k (Su su) sym+updateSubst :: KVar -> KVarSubst Symbol Symbol -> Symbol -> KVarSubst Symbol Symbol+updateSubst k (fromKVarSubst -> su) sym   = case M.lookup sym su of-      Just z  -> Su $ M.delete sym $ M.insert ksym z          su-      Nothing -> Su $                M.insert ksym (eVar sym) su+      Just z  -> toKVarSubst $ M.delete sym $ M.insert ksym z          su+      Nothing -> toKVarSubst $                M.insert ksym (eVar sym) su     where       kx      = kv k       ksym    = kArgSymbol sym kx

@@ -8,6 +8,7 @@ {-# LANGUAGE PatternGuards         #-} {-# LANGUAGE BangPatterns          #-} {-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeOperators         #-} {-# LANGUAGE InstanceSigs #-}  -- | This module has the functions that perform sort-checking, and related@@ -206,14 +207,14 @@  elaborateExpr :: HasCallStack => ElabParam -> Expr -> Maybe Sort -> Expr elaborateExpr (ElabParam ef msg env) e t =-  elabNumeric . elabApply env' . elabExpr (ElabParam ef msg env') t .  elabSorts ef . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id) $ e+  elabNumeric env' . elabApply env' . elabExpr (ElabParam ef msg env') t .  elabSorts ef . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id) $ e     where       env' = coerceEnv ef env  skipElabExpr :: ElabParam -> Expr -> Expr skipElabExpr ep e = case elabExprE ep Nothing e of   Left _   -> e-  Right e' -> elabNumeric . elabApply (epEnv ep) $ e'+  Right e' -> elabNumeric (epEnv ep) . elabApply (epEnv ep) $ e'  instance Elaborate (Symbol, Sort) where   elaborate ep (x, s) = (x, elaborate ep s)@@ -221,17 +222,17 @@ instance Elaborate a => Elaborate [a]  where   elaborate ep xs = elaborate ep <$> xs -elabNumeric :: Expr -> Expr-elabNumeric = Vis.mapExprOnExpr go+elabNumeric :: SymEnv -> Expr -> Expr+elabNumeric env = Vis.mapExprOnExpr go   where     go (ETimes e1 e2)-      | exprSort "txn1" e1 == FReal-      , exprSort "txn2" e2 == FReal+      | isFractional env (exprSort ("txn3: " ++ showpp e1) e1)+      , isFractional env (exprSort "txn4" e2)       = ERTimes e1 e2     go (EDiv   e1 e2)-      | exprSort ("txn3: " ++ showpp e1) e1 == FReal-      , exprSort "txn4" e2 == FReal-      = ERDiv   e1 e2+      | isFractional env (exprSort ("txn3: " ++ showpp e1) e1)+      , isFractional env (exprSort "txn4" e2)+      = ERDiv e1 e2     go e       = e @@ -286,7 +287,7 @@ elabFMap (PAll   bs e)     = PAll bs (elabFMap e) elabFMap (PExist bs e)     = PExist bs (elabFMap e) elabFMap (ECoerc a t e)    = ECoerc a t (elabFMap e)-elabFMap (PKVar k (Su m))  = PKVar k (Su (elabFMap <$> m))+elabFMap (PKVar k tsu su)      = PKVar k tsu (mapKVarSubst elabFMap su) elabFMap e                 = e  @@ -333,7 +334,7 @@     go (PAll   bs e)      = PAll bs (go e)     go (PExist bs e)      = PExist bs (go e)     go (ECoerc a t e)     = ECoerc a t (go e)-    go (PKVar k (Su m))   = PKVar k (Su (go <$> m))+    go (PKVar k tsu su)       = PKVar k tsu (mapKVarSubst go su)     go e                  = e  -- | Reverse transformation of elabFSetBagZ3: converts array representations back to set/bag operations@@ -412,7 +413,7 @@     go (PAll   bs e)      = PAll bs (go e)     go (PExist bs e)      = PExist bs (go e)     go (ECoerc a t e)     = ECoerc a t (go e)-    go (PKVar k (Su m))   = PKVar k (Su (go <$> m))+    go (PKVar k tsu su)       = PKVar k tsu (mapKVarSubst go su)     go e                  = e  @@ -435,7 +436,7 @@ elabSorts ef (PAll   bs e)     = PAll bs (elabSorts ef e) elabSorts ef (PExist bs e)     = PExist bs (elabSorts ef e) elabSorts ef (ECoerc s1 s2 e)  = ECoerc (coerceSort ef s1) (coerceSort ef s2) (elabSorts ef e)-elabSorts ef (PKVar k (Su m))  = PKVar k (Su (elabSorts ef <$> m))+elabSorts ef (PKVar k tsu su)      = PKVar k tsu (mapKVarSubst (elabSorts ef) su) elabSorts _ e                 = e  --------------------------------------------------------------------------------@@ -502,7 +503,7 @@     step e@EApp {}        = go e     step (ELam b e)       = ELam b       (go e)     step (ECoerc a t e)   = ECoerc a t   (go e)-    step (PKVar k (Su m)) = PKVar k (Su (go <$> m))+    step (PKVar k tsu su)     = PKVar k tsu (mapKVarSubst go su)     step e@ESym{}         = e     step e@ECon{}         = e     step e@EVar{}         = e@@ -535,7 +536,7 @@             Just z  -> Found z             Nothing -> Alts [] -subEnv :: (Subable e) => SEnv a -> e -> SEnv a+subEnv :: (Subable e, Variable e ~ Symbol) => SEnv a -> e -> SEnv a subEnv g e = intersectWithSEnv const g g'   where     g' = fromListSEnv $ (, ()) <$> syms e@@ -759,14 +760,14 @@ -- TODO: the guard below is because some LH tests generate PKVar with ill-sorted substitutions. -- However, a cleaner solution could be to modify `Sanitize.restrictKVarDomain` to simply -- those ill-sorted substitutions right up at the outset.-elab !f e@(PKVar k (Su m)) = do+elab !f e@(PKVar k tsu su) = do   expKvars <- asks (elabExplicitKvars . chElabF)   if expKvars     then do-      xargs' <- forM (HashMap.toList m) $ \(x, arg) -> do+      xargs' <- forM (HashMap.toList $ fromKVarSubst su) $ \(x, arg) -> do         (arg', _) <- elab f arg         return (x, arg')-      return (PKVar k (Su (HashMap.fromList xargs')), boolSort)+      return (PKVar k tsu (toKVarSubst (HashMap.fromList xargs')), boolSort)     else       return (e, boolSort) @@ -972,6 +973,13 @@   SReal   -> True   _       -> False +isFractional :: SymEnv -> Sort -> Bool+isFractional env (FObj l)+  = lookupSEnv l (seSort env) `elem` [Just FFrac, Just realSort]+isFractional _ s = isReal s+++ toIntAt :: Sort -> Expr toIntAt s = ECst (EVar toIntName) (FFunc s FInt) @@ -1299,7 +1307,7 @@ checkFractional :: Env -> Sort -> CheckM () checkFractional f s@(FObj l)   = do t <- checkSym f l-       unless (t == FFrac) $ throwErrorAt (errNonFractional s)+       unless (t `elem` [FFrac, realSort]) (throwErrorAt $ errNonFractional s) checkFractional _ s   = unless (isReal s) $ throwErrorAt (errNonFractional s) @@ -1499,6 +1507,14 @@   checkNumeric f t `withError` errUnify e FInt t   return θ +unify1 f e !θ !t FReal = do+  checkFractional f t `withError` errUnify e t FReal+  return θ++unify1 f e !θ FReal !t = do+  checkFractional f t `withError` errUnify e FReal t+  return θ+ unify1 f e !θ (FFunc !t1 !t2) (FFunc !t1' !t2') =   unifyMany f e θ [t1, t2] [t1', t2'] @@ -1601,16 +1617,6 @@   where     f (ECst !e' !s) = ECst e' (apply θ s)     f !e'          = e'-----------------------------------------------------------------------------------_applyCoercion :: Symbol -> Sort -> Sort -> Sort----------------------------------------------------------------------------------_applyCoercion a t = Vis.mapSort f-  where-    f (FObj b)-      | a == b    = t-    f s           = s-  -------------------------------------------------------------------------------- -- | Deconstruct a function-sort -----------------------------------------------

@@ -5,7 +5,7 @@  module Language.Fixpoint.Types (module X) where -import Language.Fixpoint.Types.SMTPrint      as X+import Language.Fixpoint.Types.SMTPrint         as X import Language.Fixpoint.Types.PrettyPrint      as X import Language.Fixpoint.Types.Names            as X import Language.Fixpoint.Types.Errors           as X@@ -19,3 +19,4 @@ import Language.Fixpoint.Types.Triggers         as X import Language.Fixpoint.Types.Theories         as X import Language.Fixpoint.Types.Templates        as X+import Language.Fixpoint.Types.Binders          as X

@@ -0,0 +1,10 @@+module Language.Fixpoint.Types.Binders where++import Data.Hashable (Hashable)++class (Eq b, Ord b, Hashable b) => Binder b where+  wildcard :: b+  editDistance :: b -> b -> Int+  editDistance b1 b2+    | b1 == b2  = 0+    | otherwise = maxBound

@@ -103,6 +103,7 @@   , pleUndecGuards   :: Bool           -- ^ Unfold invocations with undecided guards in PLE   , etabeta          :: Bool           -- ^ Eta expand and beta reduce terms to aid PLE   , localRewrites    :: Bool           -- ^ Eta expand and beta reduce terms to aid PLE+  , saveBfqOnError   :: Bool           -- ^ save FInfo as .bfq only on verification failure   , interpreter      :: Bool           -- ^ Do not use the interpreter to assist PLE   , noEnvReduction   :: Bool     -- ^ Don't use environment reduction   , inlineANFBinds   :: Bool          -- ^ Inline ANF bindings.@@ -117,6 +118,7 @@   , noStringTheory :: Bool             -- ^ disable interpretation of string theory by SMT   , explicitKvars  :: Bool             -- ^ use explicitly declared kvars (horn style) which disables several "defensive simplifications"   , sortedSolution :: Bool             -- ^ leave sorts in the solution+  , saveDir        :: Maybe FilePath    -- ^ output directory for --save generated files (default: .liquid/ next to source)   } deriving (Eq,Data,Typeable,Show,Generic)  instance Default Config where@@ -248,6 +250,15 @@   , elimStats                = False   &= help "(alpha) Print eliminate stats"   , solverStats              = False   &= help "Print solver stats"   , save                     = False   &= help "Save Query as .fq and .bfq files"+  , saveBfqOnError           = False   &= help "Save Query as .bfq file only when verification fails"+                                       &= name "save-bfq-on-error"+                                       &= explicit+  , saveDir                  = Nothing+      &= name "save-dir"+      &= help "Output directory for --save generated files (default: .liquid/ next to source)"+      &= opt (Nothing :: Maybe FilePath)+      &= explicit+      &= typDir   , metadata                 = False   &= help "Print meta-data associated with constraints"   , stats                    = False   &= help "Compute constraint statistics"   , etaElim                  = False   &= help "Eta elimination in function definition"@@ -322,4 +333,4 @@ multicore cfg = cores cfg /= Just 1  queryFile :: Ext -> Config -> FilePath-queryFile e = extFileName e . srcFile+queryFile e cfg = extFileNameR' (saveDir cfg) e (srcFile cfg)

@@ -28,6 +28,7 @@   , toFixpoint   , writeFInfo   , saveQuery+  , saveBinaryQuery   , saveSInfo     -- * Constructing Queries@@ -121,7 +122,7 @@ import           Language.Fixpoint.Types.Spans import           Language.Fixpoint.Types.Sorts import           Language.Fixpoint.Types.Refinements-import           Language.Fixpoint.Types.Substitutions+import           Language.Fixpoint.Types.Substitutions() import           Language.Fixpoint.Types.Environments import qualified Language.Fixpoint.Utils.Files as Files import qualified Language.Fixpoint.Solver.Stats as Solver@@ -393,7 +394,7 @@   toFix w     = hang (text "\n\nwf:") 2 bd     where bd  =   toFix (wenv w)               -- NOTE: this next line is printed this way for compatability with the OCAML solver-              $+$ text "reft" <+> toFix (RR t (Reft (v, PKVar k mempty)))+              $+$ text "reft" <+> toFix (RR t (Reft (v, PKVar k M.empty mempty)))               $+$ toFixMeta (text "wf") (toFix (winfo w))           (v, t, k) = wrft w @@ -442,7 +443,7 @@ ---------------------------------------------------------------------------  wfC :: (Fixpoint a) => IBindEnv -> SortedReft -> a -> [WfC a]-wfC be sr x = if all isEmptySubst sus -- ++ gsus)+wfC be sr x = if all isEmptyKVarSubst sus -- ++ gsus)                  -- NV TO RJ This tests fails with [LT:=GHC.Types.LT][EQ:=GHC.Types.EQ][GT:=GHC.Types.GT]]                  -- NV TO RJ looks like a resolution issue                 then [WfC be (v, sr_sort sr, k) x      | k         <- ks ]@@ -452,10 +453,11 @@     Reft (v, ras)   = sr_reft sr     (ks, sus)       = unzip $ go ras -    go (PKVar k su) = [(k, su)]-    go (PAnd es)    = [(k, su) | PKVar k su <- es]+    go (PKVar k _ su) = [(k, su)]+    go (PAnd es)    = [(k, su) | PKVar k _ su <- es]     go _            = [] + mkSubC :: IBindEnv -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> SubC a mkSubC = SubC @@ -514,6 +516,7 @@   | PatPrefix !Symbol !Int  -- ^ str . $i  i.e. match prefix 'str' with suffix bound to $i   | PatSuffix !Int !Symbol  -- ^ $i . str  i.e. match suffix 'str' with prefix bound to $i   | PatExact  !Symbol       -- ^ str       i.e. exactly match 'str'+  | PatLit                  -- ^ match literals of the given sort   deriving (Eq, Ord, Show, Data, Typeable, Generic)  instance ToJSON   Qualifier   where@@ -566,6 +569,7 @@   pprintTidy k (PatPrefix s i) = "as" <+> pprintTidy k s <+> ("$" <-> pprint i)   pprintTidy k (PatSuffix s i) = "as" <+> ("$" <-> pprint i) <+> pprintTidy k s   pprintTidy k (PatExact  s  ) = "~"  <+> pprintTidy k s+  pprintTidy _ PatLit          = "as lit"  instance Fixpoint Qualifier where   toFix = pprQual@@ -1059,29 +1063,28 @@  instance Hashable AutoRewrite --instance Fixpoint (M.HashMap SubcId [AutoRewrite]) where-  toFix autoRW =-    vcat $-    map fixRW rewrites ++-    rwsMapping-    where-      rewrites = dedupAutoRewrites autoRW+autoRWToFix :: M.HashMap SubcId [AutoRewrite] -> Doc+autoRWToFix autoRW =+  vcat $+  map fixRW rewrites +++  rwsMapping+  where+    rewrites = dedupAutoRewrites autoRW -      fixRW rw@(AutoRewrite args lhs rhs) =-          text ("autorewrite " ++ show (hash rw))-          <+> hsep (map toFix args)-          <+> text "="-          <+> text "{"-          <+> toFix lhs-          <+> text "="-          <+> toFix rhs-          <+> text "}"+    fixRW rw@(AutoRewrite args lhs rhs) =+        text ("autorewrite " ++ show (hash rw))+        <+> hsep (map toFix args)+        <+> text "="+        <+> text "{"+        <+> toFix lhs+        <+> text "="+        <+> toFix rhs+        <+> text "}" -      rwsMapping = do-        (cid, rws) <- M.toList autoRW-        rw         <-  rws-        return $ "rewrite" <+> brackets (text $ show cid ++ " : " ++ show (hash rw))+    rwsMapping = do+      (cid, rws) <- M.toList autoRW+      rw         <-  rws+      return $ "rewrite" <+> brackets (text $ show cid ++ " : " ++ show (hash rw))   @@ -1103,7 +1106,7 @@ instance Fixpoint AxiomEnv where   toFix axe = vcat ((toFix <$> L.sort (aenvEqs axe)) ++ (toFix <$> L.sort (aenvSimpl axe)))               $+$ renderExpand (pairdoc <$> L.sort (M.toList $ aenvExpand axe))-              $+$ toFix (aenvAutoRW axe)+              $+$ autoRWToFix (aenvAutoRW axe)     where       pairdoc (x,y) = text $ show x ++ " : " ++ show y       renderExpand [] = empty

@@ -14,8 +14,10 @@ module Language.Fixpoint.Types.Environments (    -- * Environments-    SEnv(..)-  , SESearch(..)+    SEnv+  , SEnvB(..)+  , SESearch+  , SESearchB(..)   , emptySEnv, toListSEnv, fromListSEnv, fromMapSEnv   , mapSEnvWithKey, mapSEnv, mapMSEnv   , insertSEnv, deleteSEnv, memberSEnv, lookupSEnv, unionSEnv, unionSEnv'@@ -66,6 +68,7 @@ import           Data.Generics             (Data) import           Data.Typeable             (Typeable) import           GHC.Generics              (Generic)+import           Data.Hashable             (Hashable) import qualified Data.HashMap.Strict       as M import qualified Data.HashSet              as S import           Data.Maybe@@ -75,6 +78,7 @@  import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types.PrettyPrint+import           Language.Fixpoint.Types.Binders import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types.Sorts import           Language.Fixpoint.Types.Refinements@@ -89,8 +93,9 @@ instance PPrint IBindEnv where   pprintTidy _ = pprint . L.sort . elemsIBindEnv -newtype SEnv a     = SE { seBinds :: M.HashMap Symbol a }-                     deriving (Eq, Data, Typeable, Generic, Foldable, Traversable)+type SEnv a = SEnvB Symbol a+newtype SEnvB b a = SE { seBinds :: M.HashMap b a }+                    deriving (Eq, Data, Typeable, Generic, Foldable, Traversable)  data SizedEnv a    = BE { _beSize  :: !Int                         , beBinds :: !(BindMap a)@@ -111,74 +116,74 @@ -- data SolEnv        = SolEnv { soeBinds :: !BindEnv } --                     deriving (Eq, Show, Generic) -instance PPrint a => PPrint (SEnv a) where+instance (Ord b, PPrint b, PPrint a) => PPrint (SEnvB b a) where   pprintTidy k = pprintKVs k . L.sortBy (compare `on` fst) . toListSEnv  {-# SCC toListSEnv #-}-toListSEnv              ::  SEnv a -> [(Symbol, a)]+toListSEnv              ::  SEnvB b a -> [(b, a)] toListSEnv (SE env)     = M.toList env -fromListSEnv            ::  [(Symbol, a)] -> SEnv a+fromListSEnv            ::  Hashable b => [(b, a)] -> SEnvB b a fromListSEnv            = SE . M.fromList -fromMapSEnv             ::  M.HashMap Symbol a -> SEnv a+fromMapSEnv             ::  M.HashMap b a -> SEnvB b a fromMapSEnv             = SE -mapSEnv                 :: (a -> b) -> SEnv a -> SEnv b+mapSEnv                 :: (a₁ -> a₂) -> SEnvB b a₁ -> SEnvB b a₂ mapSEnv f (SE env)      = SE (fmap f env) -mapMSEnv                :: (Monad m) => (a -> m b) -> SEnv a -> m (SEnv b)+mapMSEnv                :: (Monad m, Hashable b) => (a₁ -> m a₂) -> SEnvB b a₁ -> m (SEnvB b a₂) mapMSEnv f env          = fromListSEnv <$> mapM (secondM f) (toListSEnv env) -mapSEnvWithKey          :: ((Symbol, a) -> (Symbol, b)) -> SEnv a -> SEnv b+mapSEnvWithKey          :: Hashable b => ((b, a₁) -> (b, a₂)) -> SEnvB b a₁ -> SEnvB b a₂ mapSEnvWithKey f        = fromListSEnv . fmap f . toListSEnv -deleteSEnv :: Symbol -> SEnv a -> SEnv a+deleteSEnv :: Hashable b => b -> SEnvB b a -> SEnvB b a deleteSEnv x (SE env)   = SE (M.delete x env) -insertSEnv :: Symbol -> a -> SEnv a -> SEnv a+insertSEnv :: Hashable b => b -> a -> SEnvB b a -> SEnvB b a insertSEnv x v (SE env) = SE (M.insert x v env)  {-# SCC lookupSEnv #-}-lookupSEnv :: Symbol -> SEnv a -> Maybe a+lookupSEnv :: Hashable b => b -> SEnvB b a -> Maybe a lookupSEnv x (SE env)   = M.lookup x env -emptySEnv :: SEnv a+emptySEnv :: SEnvB b a emptySEnv               = SE M.empty -memberSEnv :: Symbol -> SEnv a -> Bool+memberSEnv :: Hashable b => b -> SEnvB b a -> Bool memberSEnv x (SE env)   = M.member x env -intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a+intersectWithSEnv :: Eq b => (a₁ -> a₂ -> a) -> SEnvB b a₁ -> SEnvB b a₂ -> SEnvB b a intersectWithSEnv f (SE m1) (SE m2) = SE (M.intersectionWith f m1 m2) -differenceSEnv :: SEnv a -> SEnv w -> SEnv a+differenceSEnv :: Hashable b => SEnvB b a -> SEnvB b w -> SEnvB b a differenceSEnv (SE m1) (SE m2) = SE (M.difference m1 m2) -filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a+filterSEnv :: (a -> Bool) -> SEnvB b a -> SEnvB b a filterSEnv f (SE m)     = SE (M.filter f m) -unionSEnv :: SEnv a -> M.HashMap Symbol a -> SEnv a+unionSEnv :: Eq b => SEnvB b a -> M.HashMap b a -> SEnvB b a unionSEnv (SE m1) m2    = SE (M.union m1 m2) -unionSEnv' :: SEnv a -> SEnv a -> SEnv a+unionSEnv' :: Eq b => SEnvB b a -> SEnvB b a -> SEnvB b a unionSEnv' (SE m1) (SE m2)    = SE (M.union m1 m2)  {-# SCC lookupSEnvWithDistance #-}-lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a+lookupSEnvWithDistance :: Binder b => b -> SEnvB b a -> SESearchB b a lookupSEnvWithDistance x (SE env)   = case M.lookup x env of      Just z  -> Found z-     Nothing -> Alts $ symbol <$> alts+     Nothing -> Alts alts   where-    alts       = takeMin $ zip (editDistance x' <$> ss) ss-    ss         = symbolString . fst <$> M.toList env-    x'         = symbolString x+    alts       = takeMin $ zip (editDistance x <$> ss) ss+    ss         = fst <$> M.toList env     takeMin xs = [z | (d, z) <- xs, d == getMin xs]     getMin     = minimum . (fst <$>)  -data SESearch a = Found a | Alts [Symbol]+type SESearch a = SESearchB Symbol a+data SESearchB b a = Found a | Alts [b]   deriving Show  -- | Functions for Indexed Bind Environment@@ -283,7 +288,7 @@ deleteBindEnv :: BindId -> BindEnv a -> BindEnv a deleteBindEnv i (BE n m) = BE n $ M.delete i m -instance Functor SEnv where+instance Functor (SEnvB b) where   fmap = mapSEnv  instance Fixpoint (EBindEnv a) where@@ -302,10 +307,10 @@ instance Fixpoint (SEnv a) => Show (SEnv a) where   show = render . toFix -instance Semigroup (SEnv a) where+instance Eq b => Semigroup (SEnvB b a) where   s1 <> s2 = SE $ M.union (seBinds s1) (seBinds s2) -instance Monoid (SEnv a) where+instance Eq b => Monoid (SEnvB b a) where   mempty        = SE M.empty  instance Semigroup (BindEnv a) where

@@ -148,6 +148,8 @@ import qualified GHC.Arr                     as Arr import           GHC.Generics                (Generic) import           Text.PrettyPrint.HughesPJ   (text)+import           Language.Fixpoint.Misc+import           Language.Fixpoint.Types.Binders import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Spans import           Language.Fixpoint.Utils.Builder as Builder (fromText)@@ -209,6 +211,10 @@   -- NOTE: hash based on original text rather than id   hashWithSalt s (S _ t _) = hashWithSalt s t +instance Binder Symbol where+  wildcard = vv Nothing+  editDistance s1 s2 = levenshteinDistance (symbolString s1) (symbolString s2)+ instance NFData Symbol where   rnf S {} = () @@ -256,7 +262,7 @@   toFix = text . T.unpack  {- | [NOTE: SymbolText]-	Use `symbolSafeText` if you want it to machine-readable,+        Use `symbolSafeText` if you want it to machine-readable,         but `symbolText`     if you want it to be human-readable.  -} 

@@ -31,6 +31,12 @@   toFix xs = brackets $ sep $ punctuate ";" (toFix <$> L.sort (S.toList xs))   simplify = S.fromList . map simplify . S.toList +instance (Ord k, Hashable k, Fixpoint k, Fixpoint v) => Fixpoint (M.HashMap k v) where+  toFix m = case hashMapToAscList m of+              []  -> empty+              xys -> hcat $ map (\(x,y) -> brackets $ toFix x <-> text ":=" <-> toFix y) xys+  simplify = M.map simplify . M.mapKeys simplify+ instance Fixpoint () where   toFix _ = "()" 

@@ -14,6 +14,7 @@ {-# LANGUAGE GADTs                      #-} {-# LANGUAGE PatternSynonyms            #-} {-# LANGUAGE ViewPatterns               #-}+{-# LANGUAGE TypeFamilies               #-}  {-# OPTIONS_GHC -Wno-orphans            #-} @@ -26,7 +27,8 @@   , Constant (..)   , Bop (..)   , Brel (..)-  , ExprV (..), Pred+  , ExprBV (..)+  , ExprV, Pred   , Expr   , pattern PTrue, pattern PTop, pattern PFalse, pattern EBot   , pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv@@ -34,10 +36,13 @@   , KVar (..)   , Subst   , SubstV (..)+  , KVarSubst   , KVSub (..)   , Reft-  , ReftV (..)+  , ReftV+  , ReftBV (..)   , SortedReft (..)+  , TyVarSubst    -- * Constructing Terms   , eVar, elit@@ -68,6 +73,7 @@   , predReft                -- any pred : p   , reftPred   , reftBind+  , toKVarSubst    -- * Predicates   , isFunctionSortedReft, functionSort@@ -95,18 +101,24 @@   , sortedReftSymbols   , substSortInExpr   , sortSubstInExpr+  , fromKVarSubst+  , isEmptyKVarSubst    -- * Transforming   , mapPredReft   , onEverySubexpr+  , mapBindExpr   , pprintReft+  , mapKVarSubst+  , mapBindKVarSubst+  , mapBindReft    , debruijnIndex    ) where  import           Prelude hiding ((<>))-import           Data.Bifunctor (second)+import           Data.Bifunctor (first, second) import qualified Data.Store as S import           Data.Generics             (Data, gmapT, mkT, extT) import           Data.Typeable             (Typeable)@@ -130,6 +142,7 @@ import           Control.DeepSeq import           Data.Maybe                (isJust) import           Language.Fixpoint.Types.Names+import           Language.Fixpoint.Types.Binders import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Spans import           Language.Fixpoint.Types.Sorts@@ -147,7 +160,8 @@ instance NFData SymConst instance NFData Brel instance NFData Bop-instance NFData v => NFData (ExprV v)+instance (NFData b, NFData v) => NFData (KVarSubst b v)+instance (NFData b, NFData v) => NFData (ExprBV b v) instance NFData v => NFData (ReftV v) instance NFData SortedReft @@ -161,6 +175,7 @@ instance S.Store SymConst instance S.Store Brel instance S.Store Bop+instance S.Store (KVarSubst Symbol Symbol) instance S.Store Expr instance S.Store Reft instance S.Store SortedReft@@ -177,8 +192,9 @@   put = B.put . M.toList   get = M.fromList <$> B.get -instance B.Binary v => B.Binary (SubstV v)-instance B.Binary v => B.Binary (ExprV v)+instance (B.Binary v, Hashable v) => B.Binary (SubstV v)+instance (B.Binary b, B.Binary v) => B.Binary (KVarSubst b v)+instance (B.Binary b, B.Binary v) => B.Binary (ExprBV b v) instance B.Binary v => B.Binary (ReftV v)  @@ -195,7 +211,7 @@ concConjuncts e = filter isConc (conjuncts e)  isKvar :: Expr -> Bool-isKvar (PKVar _ _) = True+isKvar (PKVar {}) = True isKvar _           = False  --------------------------------------------------------------------------------@@ -219,35 +235,62 @@ instance Hashable SymConst instance Hashable Constant instance Hashable v => Hashable (SubstV v)-instance Hashable v => Hashable (ExprV v)+instance (Hashable b, Hashable v) => Hashable (KVarSubst b v)+instance (Hashable b, Hashable v) => Hashable (ExprBV b v) instance Hashable v => Hashable (ReftV v)  -------------------------------------------------------------------------------- -- | Substitutions ------------------------------------------------------------- -------------------------------------------------------------------------------- type Subst = SubstV Symbol-newtype SubstV v = Su (M.HashMap Symbol (ExprV v))-                deriving (Eq, Data, Ord, Typeable, Generic, Functor, Foldable, Traversable)+newtype SubstV v = Su (M.HashMap v (ExprBV v v))+                deriving (Eq, Data, Ord, Typeable, Generic)  instance ToJSON Subst instance FromJSON Subst -instance (Fixpoint v, Ord v, Show v) => Show (SubstV v) where+instance (Fixpoint v, Ord v, Hashable v, Show v) => Show (SubstV v) where   show = showFix -instance (Ord v, Fixpoint v) => Fixpoint (SubstV v) where-  toFix (Su m) = case hashMapToAscList m of-                   []  -> empty-                   xys -> hcat $ map (\(x,y) -> brackets $ toFix x <-> text ":=" <-> toFix y) xys+instance (Ord v, Hashable v, Fixpoint v) => Fixpoint (SubstV v) where+  toFix (Su m) = toFix m -instance (Ord v, Fixpoint v) => PPrint (SubstV v) where+instance (Ord v, Hashable v, Fixpoint v) => PPrint (SubstV v) where   pprintTidy _ = toFix +newtype KVarSubst b v = KSu [(b, ExprBV b v)]+  deriving (Eq, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable)++fromKVarSubst :: Hashable b => KVarSubst b v -> M.HashMap b (ExprBV b v)+fromKVarSubst (KSu su) = M.fromList su++toKVarSubst :: M.HashMap b (ExprBV b v) -> KVarSubst b v+toKVarSubst = KSu . M.toList++mapKVarSubst :: (ExprBV b v -> ExprBV b v) -> KVarSubst b v -> KVarSubst b v+mapKVarSubst f (KSu su) = KSu $ fmap (fmap f) su++mapBindKVarSubst :: (Hashable b, Hashable b') => (b -> b') -> KVarSubst b v -> KVarSubst b' v+mapBindKVarSubst f = toKVarSubst . fmap (mapBindExpr f) . M.mapKeys f . fromKVarSubst++isEmptyKVarSubst :: KVarSubst b v -> Bool+isEmptyKVarSubst (KSu su) = null su++instance (Ord v, Fixpoint v, Ord b, Fixpoint b, Hashable b) => Show (KVarSubst b v) where+  show = showFix++instance (Ord v, Fixpoint v, Ord b, Fixpoint b, Hashable b) => Fixpoint (KVarSubst b v) where+  toFix = toFix . fromKVarSubst++instance (Ord v, Fixpoint v, Ord b, Fixpoint b, Hashable b) => PPrint (KVarSubst b v) where+  pprintTidy _ = toFix+ data KVSub = KVS   { ksuVV    :: Symbol   , ksuSort  :: Sort   , ksuKVar  :: KVar-  , ksuSubst :: Subst+  , ksuSubst :: KVarSubst Symbol Symbol+  , ksuTySub :: M.HashMap Symbol Sort  -- ^ Type variable substitution   } deriving (Eq, Data, Typeable, Generic, Show)  instance PPrint KVSub where@@ -277,39 +320,46 @@ instance ToJSON Constant  where instance ToJSON Brel      where instance ToJSON Bop       where+instance ToJSON (KVarSubst Symbol Symbol) where instance ToJSON Expr      where  instance FromJSON Constant  where instance FromJSON Brel      where instance FromJSON Bop       where+instance FromJSON (KVarSubst Symbol Symbol) where instance FromJSON Expr      where   type Expr = ExprV Symbol+type ExprV v = ExprBV Symbol v+type TyVarSubst = M.HashMap Symbol Sort -data ExprV v+data ExprBV b v           = ESym !SymConst           | ECon !Constant           | EVar !v-          | EApp !(ExprV v) !(ExprV v)-          | ENeg !(ExprV v)-          | EBin !Bop !(ExprV v) !(ExprV v)-          | ELet !Symbol !(ExprV v) !(ExprV v)-          | EIte !(ExprV v) !(ExprV v) !(ExprV v)-          | ECst !(ExprV v) !Sort-          | ELam !(Symbol, Sort)   !(ExprV v)-          | ETApp !(ExprV v) !Sort-          | ETAbs !(ExprV v) !Symbol-          | PAnd   ![ExprV v]-          | POr    ![ExprV v]-          | PNot   !(ExprV v)-          | PImp   !(ExprV v) !(ExprV v)-          | PIff   !(ExprV v) !(ExprV v)-          | PAtom  !Brel  !(ExprV v) !(ExprV v)-          | PKVar  !KVar !(SubstV v)-          | PAll   ![(Symbol, Sort)] !(ExprV v)-          | PExist ![(Symbol, Sort)] !(ExprV v)-          | ECoerc !Sort !Sort !(ExprV v)+          | EApp !(ExprBV b v) !(ExprBV b v)+          | ENeg !(ExprBV b v)+          | EBin !Bop !(ExprBV b v) !(ExprBV b v)+          | ELet !b !(ExprBV b v) !(ExprBV b v)+          | EIte !(ExprBV b v) !(ExprBV b v) !(ExprBV b v)+          | ECst !(ExprBV b v) !Sort+          | ELam !(b, Sort)   !(ExprBV b v)+          | ETApp !(ExprBV b v) !Sort+          | ETAbs !(ExprBV b v) !b+          | PAnd   ![ExprBV b v]+          | POr    ![ExprBV b v]+          | PNot   !(ExprBV b v)+          | PImp   !(ExprBV b v) !(ExprBV b v)+          | PIff   !(ExprBV b v) !(ExprBV b v)+          | PAtom  !Brel  !(ExprBV b v) !(ExprBV b v)+            -- | In @PKVar k su tsu@, @k@ is the KVar, @su@ is the substitution+            -- for that KVar, and @tsu@ indicates how to instantiate type+            -- variables that could appear in the KVar solution.+          | PKVar  !KVar !TyVarSubst !(KVarSubst b v)+          | PAll   ![(b, Sort)] !(ExprBV b v)+          | PExist ![(b, Sort)] !(ExprBV b v)+          | ECoerc !Sort !Sort !(ExprBV b v)           deriving (Eq, Show, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable)  onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr@@ -325,34 +375,60 @@  type Pred = Expr -pattern PTrue :: ExprV v+pattern PTrue :: ExprBV b v pattern PTrue = PAnd [] -pattern PTop :: ExprV v+pattern PTop :: ExprBV b v pattern PTop = PAnd [] -pattern PFalse :: ExprV v+pattern PFalse :: ExprBV b v pattern PFalse = POr  [] -pattern EBot :: ExprV v+pattern EBot :: ExprBV b v pattern EBot = POr  [] -pattern EEq :: ExprV v -> ExprV v -> ExprV v+pattern EEq :: ExprBV b v -> ExprBV b v -> ExprBV b v pattern EEq e1 e2 = PAtom Eq    e1 e2 -pattern ETimes :: ExprV v -> ExprV v -> ExprV v+pattern ETimes :: ExprBV b v -> ExprBV b v -> ExprBV b v pattern ETimes e1 e2 = EBin Times  e1 e2 -pattern ERTimes :: ExprV v -> ExprV v -> ExprV v+pattern ERTimes :: ExprBV b v -> ExprBV b v -> ExprBV b v pattern ERTimes e1 e2 = EBin RTimes e1 e2 -pattern EDiv :: ExprV v -> ExprV v -> ExprV v+pattern EDiv :: ExprBV b v -> ExprBV b v -> ExprBV b v pattern EDiv e1 e2 = EBin Div    e1 e2 -pattern ERDiv :: ExprV v -> ExprV v -> ExprV v+pattern ERDiv :: ExprBV b v -> ExprBV b v -> ExprBV b v pattern ERDiv e1 e2 = EBin RDiv   e1 e2 -exprSymbolsSet :: Expr -> HashSet Symbol+mapBindExpr :: (Hashable b, Hashable b') => (b -> b') -> ExprBV b v -> ExprBV b' v+mapBindExpr f = go+  where+    go (ESym c) = ESym c+    go (ECon c) = ECon c+    go (EVar v) = EVar v+    go (EApp e1 e2) = EApp (go e1) (go e2)+    go (ENeg e) = ENeg (go e)+    go (EBin op e1 e2) = EBin op (go e1) (go e2)+    go (ELet b e1 e2) = ELet (f b) (go e1) (go e2)+    go (EIte e1 e2 e3) = EIte (go e1) (go e2) (go e3)+    go (ECst e s) = ECst (go e) s+    go (ELam (b, s) e) = ELam (f b, s) (go e)+    go (ETApp e s) = ETApp (go e) s+    go (ETAbs e b) = ETAbs (go e) (f b)+    go (PAnd es) = PAnd (go <$> es)+    go (POr es) = POr (go <$> es)+    go (PNot e) = PNot (go e)+    go (PImp e1 e2) = PImp (go e1) (go e2)+    go (PIff e1 e2) = PIff (go e1) (go e2)+    go (PAtom rel e1 e2) = PAtom rel (go e1) (go e2)+    go (PKVar k tsu su) = PKVar k tsu (mapBindKVarSubst f su)+    go (PAll bs e) = PAll (first f <$> bs) (go e)+    go (PExist bs e) = PExist (first f <$> bs) (go e)+    go (ECoerc s1 s2 e) = ECoerc s1 s2 (go e)++exprSymbolsSet :: (Eq v, Hashable v) => ExprBV v v -> HashSet v exprSymbolsSet = go   where     gos es                = HashSet.unions (go <$> es)@@ -371,7 +447,7 @@     go (PIff p1 p2)       = gos [p1, p2]     go (PImp p1 p2)       = gos [p1, p2]     go (PAtom _ e1 e2)    = gos [e1, e2]-    go (PKVar _ (Su su))  = HashSet.unions $ map exprSymbolsSet (M.elems su)+    go (PKVar _ _ su)       = HashSet.unions $ map exprSymbolsSet (M.elems $ fromKVarSubst su)     go (PAll xts p)       = go p `HashSet.difference` HashSet.fromList (fst <$> xts)     go (PExist xts p)     = go p `HashSet.difference` HashSet.fromList (fst <$> xts)     go _                  = HashSet.empty@@ -399,7 +475,7 @@       ECoerc t0 t1 e -> ECoerc (sortSubst f t0) (sortSubst f t1) e       e -> e -exprKVars :: Expr -> HashMap KVar [Subst]+exprKVars :: Expr -> HashMap KVar [KVarSubst Symbol Symbol] exprKVars = go   where     gos es                = HashMap.unions (go <$> es)@@ -418,19 +494,19 @@     go (PIff p1 p2)       = gos [p1, p2]     go (PImp p1 p2)       = gos [p1, p2]     go (PAtom _ e1 e2)    = gos [e1, e2]-    go (PKVar k substs@(Su su))  =-      HashMap.insertWith (++) k [substs] $ HashMap.unions $ map exprKVars (M.elems su)+    go (PKVar k _ su) =+      HashMap.insertWith (++) k [su] $ HashMap.unions $ map exprKVars (M.elems $ fromKVarSubst su)     go (PAll _xts p)       = go p     go (PExist _xts p)     = go p     go _                  = HashMap.empty -mkEApp :: LocSymbol -> [Expr] -> Expr+mkEApp :: Located v -> [ExprBV b v] -> ExprBV b v mkEApp = eApps . EVar . val -eApps :: ExprV v -> [ExprV v] -> ExprV v+eApps :: ExprBV b v -> [ExprBV b v] -> ExprBV b v eApps f es  = foldl' EApp f es -splitEApp :: ExprV v -> (ExprV v, [ExprV v])+splitEApp :: ExprBV b v -> (ExprBV b v, [ExprBV b v]) splitEApp = go []   where     go acc (EApp f e) = go (e:acc) f@@ -482,16 +558,20 @@     go (PAtom _ e1 e2) = go e1 + go e2     go (PAll _ e)      = go e     go (PExist _ e)    = go e-    go (PKVar _ _)     = 1+    go (PKVar {})        = 1     go (ECoerc _ _ e)  = go e  type Reft = ReftV Symbol+type ReftV v = ReftBV Symbol v  -- | Refinement of @v@ satisfying a predicate --   e.g. in '{x: _ | e }' x is the @Symbol@ and e the @ExprV v@-newtype ReftV v = Reft (Symbol, ExprV v)+newtype ReftBV b v = Reft (b, ExprBV b v)     deriving (Eq, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable) +mapBindReft :: (Hashable b, Hashable b') => (b -> b') -> ReftBV b v -> ReftBV b' v+mapBindReft f (Reft (b, e)) = Reft (f b, mapBindExpr f e)+ data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft }                   deriving (Eq, Ord, Data, Typeable, Generic) @@ -549,7 +629,7 @@   toFix RDiv   = text "/."   toFix Mod    = text "mod" -instance (Ord v, Fixpoint v) => Fixpoint (ExprV v) where+instance (Ord b, Fixpoint b, Hashable b, Ord v, Fixpoint v) => Fixpoint (ExprBV b v) where   toFix (ESym c)       = toFix c   toFix (ECon c)       = toFix c   toFix (EVar s)       = toFix s@@ -570,7 +650,7 @@   toFix (PAnd ps)      = text "&&" <+> toFix ps   toFix (POr  ps)      = text "||" <+> toFix ps   toFix (PAtom r e1 e2)  = parens $ sep [ toFix e1 <+> toFix r, nest 2 (toFix e2)]-  toFix (PKVar k su)     = toFix k <-> toFix su+  toFix (PKVar k tsu su)   = toFix k <-> toFixTySub tsu <-> toFix su   toFix (PAll xts p)     = parens $ "forall" <+> (toFix xts                                         $+$ ("." <+> toFix p))   toFix (PExist xts p)   = parens $ "exists" <+> (toFix xts@@ -580,11 +660,23 @@   toFix (ECoerc a t e)   = parens (text "coerce" <+> toFix a <+> text "~" <+> toFix t <+> text "in" <+> toFix e)   toFix (ELam (x,s) e)   = parens (char '\\' <+> toFix x <+> ":" <+> toFix s <+> "->" <+> toFix e) -  simplify = simplifyExpr dedup-    where-      dedup = Set.toList . Set.fromList+  simplify = simplifyExprDefault -simplifyExpr :: Eq v => ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v+-- | Serialize a type-variable substitution for PKVar in .fq files.+-- An empty substitution is rendered as @[@]@, and a non-empty one as+-- @[\@sym:=sort;...]@.+toFixTySub :: M.HashMap Symbol Sort -> Doc+toFixTySub tsu+  | M.null tsu = empty+  | otherwise  = brackets (text "@" <->  tyPairs)+  where+    tyPairs = hcat $ punctuate (text ";") (toFixTyPair <$> hashMapToAscList tsu)+    toFixTyPair (s, srt) = toFix s <-> text ":=" <-> toFix srt++simplifyExprDefault :: (Ord b, Ord v) => ExprBV b v -> ExprBV b v+simplifyExprDefault = simplifyExpr (Set.toList . Set.fromList)++simplifyExpr :: (Eq b, Eq v) => ([ExprBV b v] -> [ExprBV b v]) -> ExprBV b v -> ExprBV b v simplifyExpr dedup = go   where     go (POr  [])     = PFalse@@ -629,7 +721,7 @@       | isTautoPred  p     = PTrue       | otherwise          = p -isContraPred   :: Eq v => ExprV v -> Bool+isContraPred   :: (Eq b, Eq v) => ExprBV b v -> Bool isContraPred z = eqC z || (z `elem` contras)   where     contras    = [PFalse]@@ -644,7 +736,7 @@                = x == y     eqC _      = False -isTautoPred   :: Eq v => ExprV v -> Bool+isTautoPred   :: (Eq b, Eq v) => ExprBV b v -> Bool isTautoPred z  = z == PTop || z == PTrue || eqT z   where     eqT (PAnd [])@@ -716,7 +808,7 @@ opPrec Div    = 7 opPrec RDiv   = 7 -instance (Ord v, Fixpoint v, PPrint v) => PPrint (ExprV v) where+instance (Ord b, Fixpoint b, Hashable b, PPrint b, Ord v, Fixpoint v, PPrint v) => PPrint (ExprBV b v) where   pprintPrec _ k (ESym c)        = pprintTidy k c   pprintPrec _ k (ECon c)        = pprintTidy k c   pprintPrec _ k (EVar s)        = pprintTidy k s@@ -780,8 +872,8 @@   pprintPrec _ _ (ETAbs e s)     = "ETAbs" <+> toFix e <+> toFix s  pprintQuant-  :: (Ord v, Fixpoint v, PPrint v)-  => Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc+  :: (Ord b, Fixpoint b, Hashable b, PPrint b, Ord v, Fixpoint v, PPrint v)+  => Tidy -> Doc -> [(b, Sort)] -> ExprBV b v -> Doc pprintQuant k d xts p = (d <+> pprintTidy k xts)                         $+$                         ("  ." <+> pprintTidy k p)@@ -884,13 +976,13 @@ --   so they SHOULD NOT be used inside the solver loop. Instead, use 'conj' which ensures --   some basic things but is faster. -pAnd, pOr     :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v-pAnd          = simplify . PAnd+pAnd, pOr     :: (Ord b, Hashable b, Ord v) => ListNE (ExprBV b v) -> ExprBV b v+pAnd          = simplifyExprDefault . PAnd  pAndNoDedup :: ListNE Pred -> Pred pAndNoDedup = simplifyExpr id . PAnd -pOr           = simplify . POr+pOr           = simplifyExprDefault . POr  infixl 9 &.& (&.&) :: Pred -> Pred -> Pred@@ -900,10 +992,10 @@ (|.|) :: Pred -> Pred -> Pred (|.|) p q = pOr [p, q] -pIte :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v -> ExprV v+pIte :: (Fixpoint b, Ord b, Hashable b, Fixpoint v, Ord v) => ExprBV b v -> ExprBV b v -> ExprBV b v -> ExprBV b v pIte p1 p2 p3 = pAnd [p1 `PImp` p2, PNot p1 `PImp` p3] -pExist :: [(Symbol, Sort)] -> ExprV v -> ExprV v+pExist :: [(b, Sort)] -> ExprBV b v -> ExprBV b v pExist []  p = p pExist xts p = PExist xts p @@ -947,13 +1039,13 @@ isNonTrivial :: SortedReft -> Bool isNonTrivial = not . isTautoReft . sr_reft -isTautoReft :: Eq v => ReftV v -> Bool+isTautoReft :: (Eq b, Eq v) => ReftBV b v -> Bool isTautoReft = all isTautoPred . conjuncts . reftPred -reftPred :: ReftV v -> ExprV v+reftPred :: ReftBV b v -> ExprBV b v reftPred (Reft (_, p)) = p -reftBind :: ReftV v -> Symbol+reftBind :: ReftBV b v -> b reftBind (Reft (x, _)) = x  ------------------------------------------------------------@@ -972,18 +1064,18 @@ trueSortedReft :: Sort -> SortedReft trueSortedReft = (`RR` trueReft) -trueReft, falseReft :: ReftV v-trueReft  = Reft (vv_, PTrue)-falseReft = Reft (vv_, PFalse)+trueReft, falseReft :: Binder b => ReftBV b v+trueReft  = Reft (wildcard, PTrue)+falseReft = Reft (wildcard, PFalse) -flattenRefas :: [ExprV v] -> [ExprV v]+flattenRefas :: [ExprBV b v] -> [ExprBV b v] flattenRefas        = flatP []   where     flatP acc (PAnd ps:xs) = flatP (flatP acc xs) ps     flatP acc (p:xs)       = p : flatP acc xs     flatP acc []           = acc -conjuncts :: Eq v => ExprV v -> [ExprV v]+conjuncts :: (Eq b, Eq v) => ExprBV b v -> [ExprBV b v] conjuncts (PAnd ps) = concatMap conjuncts ps conjuncts p   | isTautoPred p   = []@@ -997,28 +1089,32 @@ class Falseable a where   isFalse :: a -> Bool -instance Falseable Expr where+instance Falseable (ExprBV b v) where   isFalse PFalse = True   isFalse _      = False -instance Falseable Reft where+instance Falseable (ReftBV b v) where   isFalse (Reft (_, ra)) = isFalse ra  ------------------------------------------------------------------------- -- | Class Predicates for Valid Refinements ----------------------------- ------------------------------------------------------------------------- -class Subable a where-  syms   :: a -> [Symbol]                   -- ^ free symbols of a-  substa :: (Symbol -> Symbol) -> a -> a+class (Eq (Variable a), Hashable (Variable a)) => Subable a where+  type Variable a+  type Variable a = Symbol++  syms   :: a -> [Variable a]                   -- ^ free symbols of a+  substa :: (Variable a -> Variable a) -> a -> a   -- substa f  = substf (EVar . f) -  substf :: (Symbol -> Expr) -> a -> a-  subst  :: HasCallStack => Subst -> a -> a-  subst1 :: a -> (Symbol, Expr) -> a+  substf :: (Variable a -> ExprBV (Variable a) (Variable a)) -> a -> a+  subst  :: HasCallStack => SubstV (Variable a) -> a -> a+  subst1 :: a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a   subst1 y (x, e) = subst (Su $ M.fromList [(x,e)]) y  instance Subable a => Subable (Located a) where+  type Variable (Located a) = Variable a   syms (Loc _ _ x)   = syms x   substa f (Loc l l' x) = Loc l l' (substa f x)   substf f (Loc l l' x) = Loc l l' (substf f x)

@@ -92,7 +92,8 @@ instance ToHornSMT F.Subst where   toHornSMT (F.Su m) = toHornSMT (Misc.hashMapToAscList m) -+instance ToHornSMT (F.KVarSubst F.Symbol F.Symbol) where+  toHornSMT = toHornSMT . Misc.hashMapToAscList . F.fromKVarSubst  instance ToHornSMT F.KVar where   toHornSMT (F.KV k) = "$" P.<-> toHornSMT k@@ -122,7 +123,7 @@ 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.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] 

@@ -47,13 +47,12 @@    -- * Manipulating QBind   , qb-  , qbPreds   , qbFilter   , qbFilterM     -- * Conversion for client-  , result +  , result    -- * "Fast" Solver (DEPRECATED as unsound)   , Index  (..)@@ -186,13 +185,7 @@ -------------------------------------------------------------------------------- result s = pAnd . fmap eqPred . qbEQuals <$> sMap s - ---------------------------------------------------------------------------------qbPreds :: Subst -> QBind -> [(Pred, EQual)]----------------------------------------------------------------------------------qbPreds su (QB eqs) =  [ (subst su $ eqPred eq, eq) | eq <- eqs ]---------------------------------------------------------------------------------- -- | Read / Write Solution at KVar --------------------------------------------- -------------------------------------------------------------------------------- lookupQBind :: Sol QBind -> KVar -> QBind@@ -249,13 +242,16 @@  instance NFData EQual --- | @eQual q xs@ instantiates @q@ with the arguments in @xs@-eQual :: Qualifier -> [Symbol] -> EQual-eQual q xs = {- tracepp "eQual" $ -} EQL q p es+-- | @eQual q xs ls@ instantiates @q@ with variable arguments @xs@ and literal arguments @ls@+eQual :: Qualifier -> [Symbol] -> [Constant] -> EQual+eQual q xs ls = {- tracepp "eQual" $ -} EQL q p es   where     p      = subst su $  qBody q-    su     = mkSubst  $  safeZip "eQual" qxs es-    es     = eVar    <$> xs+    su     = mkSubst  $  safeZip "eQual" qxs (reverse es)+    (es, _, _) = L.foldl' go ([], xs, ls) (qParams q)+    go (acc, x:xs', cs   ) qp | qpPat qp /= PatLit = (eVar x : acc, xs', cs)+    go (acc, xs',   c:cs') qp | qpPat qp == PatLit = (ECon c : acc, xs', cs')+    go _                   _                       = error "eQual: mismatched params"     qxs    = qpSym   <$> qParams q  --------------------------------------------------------------------------------

@@ -31,6 +31,7 @@   , boolFTyCon   , realFTyCon   , numFTyCon+  , fracFTyCon   , strFTyCon   , setFTyCon   , mapFTyCon -- TODO: hide these@@ -67,6 +68,7 @@   , mkPoly   , sortSymbols   , substSort+  , matchSortsTyVars    , isBool, isNumeric, isReal, isString, isSet, isMap, isBag, isArray, isFinfield, isPolyInst @@ -153,12 +155,13 @@ defRealInfo = False defStrInfo  = False -charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon :: FTycon+charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon, fracFTyCon :: FTycon strFTyCon, listFTyCon, mapFTyCon, bagFTyCon, setFTyCon, ffldFTyCon :: FTycon intFTyCon  = TC (dummyLoc "int"       ) numTcInfo boolFTyCon = TC (dummyLoc boolLConName) defTcInfo realFTyCon = TC (dummyLoc "real"      ) realTcInfo numFTyCon  = TC (dummyLoc "num"       ) numTcInfo+fracFTyCon = TC (dummyLoc "frac"      ) realTcInfo funcFTyCon = TC (dummyLoc "function"  ) defTcInfo strFTyCon  = TC (dummyLoc strConName  ) strTcInfo listFTyCon = TC (dummyLoc listConName ) defTcInfo@@ -268,6 +271,7 @@ sortFTycon :: Sort -> Maybe FTycon sortFTycon FInt    = Just intFTyCon sortFTycon FReal   = Just realFTyCon+sortFTycon FFrac   = Just fracFTyCon sortFTycon FNum    = Just numFTyCon sortFTycon (FTC c) = Just c sortFTycon _       = Nothing@@ -341,6 +345,25 @@   FAbs i t -> FAbs i (substSort f t)   t -> t +-- | @matchSortsTyVars tvs wfSort useSiteSort@ structurally matches two sorts and+-- extracts a mapping from type variable symbols (in @tvs@) to their+-- instantiation at the use site. For example:+--+-- > matchSortsTyVars ["a"] (FApp listTC (FObj "a")) (FApp listTC (FObj "b"))+-- >   == HashMap.fromList [("a", FObj "b")]+matchSortsTyVars :: [Symbol] -> Sort -> Sort -> M.HashMap Symbol Sort+matchSortsTyVars tvs wfSort useSiteSort+  | null tvs  = M.empty+  | otherwise = go M.empty wfSort useSiteSort+  where+    tvSet = HashSet.fromList tvs+    go acc (FObj s) t+      | HashSet.member s tvSet = if FObj s /= t then M.insert s t acc else acc+    go acc (FFunc a1 a2) (FFunc b1 b2) = go (go acc a1 b1) a2 b2+    go acc (FApp a1 a2) (FApp b1 b2) = go (go acc a1 b1) a2 b2+    go acc (FAbs _ a) (FAbs _ b) = go acc a b+    go acc _ _ = acc+ data DataField = DField   { dfName :: !LocSymbol          -- ^ Field Name   , dfSort :: !Sort               -- ^ Field Sort@@ -600,6 +623,7 @@ fTyconSort c   | c == intFTyCon  = FInt   | c == realFTyCon = FReal+  | c == fracFTyCon = FFrac   | c == numFTyCon  = FNum   | otherwise       = FTC c 

@@ -163,11 +163,11 @@   toFix = text . show  -data Located a = Loc +data Located a = Loc   { loc  :: !SourcePos -- ^ Start Position   , locE :: !SourcePos -- ^ End Position   , val  :: !a-  } +  }   deriving (Data, Typeable, Generic, ToJSON, FromJSON)  instance ToJSON SourcePos where@@ -223,7 +223,7 @@ instance (B.Binary a) => B.Binary (Located a)  -instance ToJSON Pos where +instance ToJSON Pos where  instance FromJSON Pos where 

@@ -1,5 +1,7 @@ {-# LANGUAGE CPP               #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeFamilies      #-}+{-# LANGUAGE TypeOperators     #-}  {-# OPTIONS_GHC -Wno-orphans   #-} {-# LANGUAGE InstanceSigs #-}@@ -9,11 +11,16 @@ --   be in the same place as the @Term@ definitions. module Language.Fixpoint.Types.Substitutions (     mkSubst+  , mkKVarSubst+  , substFromKSubst+  , kSubstFromSubst+  , ksubst   , isEmptySubst   , substExcept   , substfExcept   , subst1Except   , substSymbolsSet+  , Refreshable(..)   , rapierSubstExpr   , targetSubstSyms   , filterSubst@@ -26,8 +33,10 @@  import           Data.List                 as List import           Data.Maybe+import           Data.Hashable             (Hashable) import qualified Data.HashMap.Strict       as M import qualified Data.HashSet              as S+import           Language.Fixpoint.Types.Binders import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types.Sorts@@ -36,37 +45,56 @@ import           Text.PrettyPrint.HughesPJ.Compat import           Text.Printf               (printf) -instance Semigroup Subst where+instance (Eq v, Hashable v) => Semigroup (SubstV v) where   (<>) = catSubst -instance Monoid Subst where+instance (Eq v, Hashable v) => Monoid (SubstV v) where   mempty  = emptySubst   mappend = (<>) -filterSubst :: (Symbol -> Expr -> Bool) -> Subst -> Subst+instance Semigroup (KVarSubst Symbol Symbol) where+  su1 <> su2 = kSubstFromSubst $ substFromKSubst su1 <> substFromKSubst su2++instance Monoid (KVarSubst Symbol Symbol) where+  mempty = kSubstFromSubst mempty+  mappend = (<>)++substFromKSubst :: Hashable v => KVarSubst v v -> SubstV v+substFromKSubst = Su . fromKVarSubst++kSubstFromSubst :: SubstV v -> KVarSubst v v+kSubstFromSubst (Su m) = toKVarSubst m++ksubst :: KVarSubst Symbol Symbol -> Expr -> Expr+ksubst = subst . substFromKSubst++filterSubst :: (v -> ExprBV v v -> Bool) -> SubstV v -> SubstV v filterSubst f (Su m) = Su (M.filterWithKey f m) -emptySubst :: Subst+emptySubst :: SubstV v emptySubst = Su M.empty -catSubst :: Subst -> Subst -> Subst+catSubst :: (Eq v, Hashable v) => SubstV v -> SubstV v -> SubstV v catSubst (Su s1) θ2@(Su s2) = Su $ M.union s1' s2   where     s1'                     = subst θ2 <$> s1 -mkSubst :: [(Symbol, Expr)] -> Subst+mkSubst :: Hashable v => [(v, ExprBV v v)] -> SubstV v mkSubst = Su . M.fromList . reverse . filter notTrivial   where     notTrivial (x, EVar y) = x /= y     notTrivial _           = True -isEmptySubst :: Subst -> Bool+mkKVarSubst :: [(Symbol, Expr)] -> KVarSubst Symbol Symbol+mkKVarSubst = kSubstFromSubst . mkSubst++isEmptySubst :: SubstV v -> Bool isEmptySubst (Su xes) = M.null xes -targetSubstSyms :: Subst -> [Symbol]+targetSubstSyms :: (Eq v, Hashable v) => SubstV v -> [v] targetSubstSyms (Su ms) = syms $ M.elems ms -substSymbolsSet :: Subst -> S.HashSet Symbol+substSymbolsSet :: (Eq v, Hashable v) => SubstV v -> S.HashSet v substSymbolsSet (Su m) = S.unions $ map exprSymbolsSet (M.elems m)  instance Subable () where@@ -75,19 +103,22 @@   substf _ () = ()   substa _ () = () -instance (Subable a, Subable b) => Subable (a,b) where+instance (Subable a, Subable b, Variable a ~ Variable b) => Subable (a,b) where+  type Variable (a, b) = Variable a   syms  (x, y)   = syms x ++ syms y   subst su (x,y) = (subst su x, subst su y)   substf f (x,y) = (substf f x, substf f y)   substa f (x,y) = (substa f x, substa f y)  instance Subable a => Subable [a] where+  type Variable [a] = Variable a   syms   = concatMap syms   subst  = fmap . subst   substf = fmap . substf   substa = fmap . substa  instance Subable a => Subable (Maybe a) where+  type Variable (Maybe a) = Variable a   syms   = concatMap syms . maybeToList   subst  = fmap . subst   substf = fmap . substf@@ -95,20 +126,21 @@   instance Subable a => Subable (M.HashMap k a) where+  type Variable (M.HashMap k a) = Variable a   syms   = syms . M.elems   subst  = M.map . subst   substf = M.map . substf   substa = M.map . substa -subst1Except :: (Subable a) => [Symbol] -> a -> (Symbol, Expr) -> a+subst1Except :: Subable a => [Variable a] -> a -> (Variable a, ExprBV (Variable a) (Variable a)) -> a subst1Except xs z su@(x, _)   | x `elem` xs = z   | otherwise   = subst1 z su -substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr+substfExcept :: Eq v => (v -> ExprBV b v) -> [v] -> v -> ExprBV b v substfExcept f xs y = if y `elem` xs then EVar y else f y -substExcept  :: Subst -> [Symbol] -> Subst+substExcept  :: Eq v => SubstV v -> [v] -> SubstV v -- substExcept  (Su m) xs = Su (foldr M.delete m xs) substExcept (Su xes) xs = Su $ M.filterWithKey (const . not . (`elem` xs)) xes @@ -118,21 +150,22 @@   subst su x               = subSymbol (Just $ appSubst su x) x -- subSymbol (M.lookup x s) x   syms x                   = [x] -appSubst :: Subst -> Symbol -> Expr+appSubst :: (Eq v, Hashable v) => SubstV v -> v -> ExprBV v v appSubst (Su s) x = fromMaybe (EVar x) (M.lookup x s) -subSymbol :: Maybe Expr -> Symbol -> Symbol+subSymbol :: (Ord v, Hashable v, Fixpoint v) => Maybe (ExprBV v v) -> v -> v subSymbol (Just (EVar y)) _ = y subSymbol Nothing         x = x subSymbol a               b = errorstar (printf "Cannot substitute symbol %s with expression %s" (showFix b) (showFix a)) -captureAvoiding :: Symbol -> (Symbol -> Expr) -> Symbol -> Expr+captureAvoiding :: Eq v => v -> (v -> ExprBV b v) -> v -> ExprBV b v captureAvoiding x f y = if y == x then EVar x else f y -instance Subable Expr where+instance (Eq v, Hashable v) => Subable (ExprBV v v) where+  type Variable (ExprBV v v) = v   syms                     = exprSymbols   substa f                 = substf (EVar . f)-  substf :: (Symbol -> Expr) -> Expr -> Expr+  substf :: (v -> ExprBV v v) -> ExprBV v v -> ExprBV v v   substf f (EApp s e)      = EApp (substf f s) (substf f e)   substf f (ELam (x,t) e)  = ELam (x, t) (substf (captureAvoiding x f) e)   substf f (ECoerc a t e)  = ECoerc a t (substf f e)@@ -148,7 +181,7 @@   substf f (PImp p1 p2)    = PImp (substf f p1) (substf f p2)   substf f (PIff p1 p2)    = PIff (substf f p1) (substf f p2)   substf f (PAtom r e1 e2) = PAtom r (substf f e1) (substf f e2)-  substf f (PKVar k (Su su)) = PKVar k (Su $ M.map (substf f) su)+  substf f (PKVar k tsu su)    = PKVar k tsu (mapKVarSubst (substf f) su)   substf _ (PAll _ _)      = errorstar "substf: FORALL"   substf f (PExist xts e)  = PExist xts (substf f e)   substf _  p              = p@@ -192,39 +225,45 @@           PIff (go su p1) (go su p2)         PAtom r e1 e2 ->           PAtom r (go su e1) (go su e2)-        PKVar k su' ->-          PKVar k $ su' `catSubst` su+        PKVar k tsu su' ->+          PKVar k tsu (kSubstFromSubst $ substFromKSubst su' `catSubst` su)         PAll bs p-          | disjoint su bs ->-            PAll bs $ go su p --(substExcept su (fst <$> bs)) p+          | disjointRange su' bs ->+            PAll bs $ go su' p           | otherwise ->-            errorstar $ unlines-              [ "subst: FORALL without disjoint binds"-              , "su: " ++ showpp su-              , "expr: " ++ showpp e0-              ]+            errorstar "subst: PAll (without disjoint binds)"+          where+            su' = substExcept su (map fst bs)+         PExist bs p-          | disjoint su bs ->-            PExist bs $ go su p --(substExcept su (fst <$> bs)) p+          | disjointRange su' bs ->+            PExist bs $ go su' p           | otherwise ->-            errorstar $ unlines-              [ "subst: EXISTS without disjoint binds"-              , "su: " ++ showpp su-              , "expr: " ++ showpp e0-              ]+            errorstar "subst: EXISTS without disjoint binds"+          where+            su' = substExcept su (map fst bs)         p ->           p -removeSubst :: Subst -> Symbol -> Subst+removeSubst :: (Eq v, Hashable v) => SubstV v -> v -> SubstV v removeSubst (Su su) x = Su $ M.delete x su +-- | Variable names for which we can propose variations to avoid name captures+class Refreshable v where+  -- | Variations of a variable name. They must contain at least a fresh name in+  -- the contexts where @candidates@ is used.+  candidates :: v -> [v]++instance Refreshable Symbol where+  candidates x = [ renameSubstSymbol x i | i <- [0..] ]+ -- | Rapier style capture-avoiding substitution -- -- The scope set parameter must contain any symbols that are expected -- to appear free in the result expression. Typically, this is the set of -- symbols that are free in the range of the substitution, plus any symbols -- that are already free in the input expression.-rapierSubstExpr :: S.HashSet Symbol -> Subst -> Expr -> Expr+rapierSubstExpr :: (Hashable v, Refreshable v) => S.HashSet v -> SubstV v -> ExprBV v v -> ExprBV v v rapierSubstExpr s su e0 =   let go = rapierSubstExpr    in case e0 of@@ -257,7 +296,7 @@     PImp p1 p2 -> PImp (go s su p1) (go s su p2)     PIff p1 p2 -> PIff (go s su p1) (go s su p2)     PAtom r e1 e2 -> PAtom r (go s su e1) (go s su e2)-    PKVar k su' -> PKVar k $ catSubstGo su' su+    PKVar k tsu su' -> PKVar k tsu (catSubstGo su' su)     PAll bs p ->       let mfs = map (maybeFresh . fst) bs           fs = map (either (\x -> (x, x)) id) mfs@@ -276,38 +315,38 @@           PExist bs' $ go s' su' p     p -> p   where-    fresh :: Symbol -> Symbol-    fresh x = head $ dropWhile (`S.member` s) candidates-      where-        candidates = [ renameSubstSymbol x i | i <- [0..] ]+    fresh x = head $ dropWhile (`S.member` s) (candidates x)      maybeFresh x =       if x `S.member` s then Right (x, fresh x) else Left x -    catSubstGo :: Subst -> Subst -> Subst-    catSubstGo (Su s1) su2@(Su s2) = Su $ M.union s1' s2+    catSubstGo su1 su2@(Su s2) = toKVarSubst $ M.union s1 s2       where-        s1' = rapierSubstExpr s su2 <$> s1+        s1 = rapierSubstExpr s su2 <$> fromKVarSubst su1 -extendSubst :: Subst -> Symbol -> Expr -> Subst+extendSubst :: Hashable v => SubstV v -> v -> ExprBV v v -> SubstV v extendSubst (Su m) x e = Su $ M.insert x e m -disjoint :: Subst -> [(Symbol, Sort)] -> Bool-disjoint (Su su) bs = S.null $ suSyms `S.intersection` bsSyms+disjointRange :: (Eq v, Hashable v) => SubstV v -> [(v, Sort)] -> Bool+disjointRange (Su su) bs = S.null $ suSyms `S.intersection` bsSyms   where-    suSyms = S.fromList $ syms (M.elems su) ++ M.keys su+    suSyms = S.fromList $ syms (M.elems su)     bsSyms = S.fromList $ fst <$> bs -meetReft :: Reft -> Reft -> Reft+meetReft :: Binder v => ReftBV v v -> ReftBV v v -> ReftBV v v meetReft (Reft (v, ra)) (Reft (v', ra'))   | v == v'          = Reft (v , pAnd [ra, ra'])-  | v == dummySymbol = Reft (v', pAnd [ra', ra `subst1`  (v , EVar v')])+  | v == wildcard    = Reft (v', pAnd [ra', ra `subst1`  (v , EVar v')])   | otherwise        = Reft (v , pAnd [ra, ra' `subst1` (v', EVar v )]) -instance Subable Reft where+instance (Eq v, Hashable v, Refreshable v) => Subable (ReftBV v v) where+  type Variable (ReftBV v v) = v   syms (Reft (v, ras))      = v : syms ras   substa f (Reft (v, ras))  = Reft (f v, substa f ras)-  subst su (Reft (v, ras))  = Reft (v, subst (substExcept su [v]) ras)+  subst su (Reft (v, ras))  =+    let su' = substExcept su [v]+        s = S.union (substSymbolsSet su') (exprSymbolsSet ras)+     in Reft (v, rapierSubstExpr s su' ras)   substf f (Reft (v, ras))  = Reft (v, substf (substfExcept f [v]) ras)   subst1 (Reft (v, ras)) su = Reft (v, subst1Except [v] ras su) @@ -385,7 +424,7 @@     -- go _                  = []  -exprSymbols :: Expr -> [Symbol]+exprSymbols :: (Eq v, Hashable v) => ExprBV v v -> [v] exprSymbols = S.toList . exprSymbolsSet  instance Expression (Symbol, SortedReft) where

@@ -38,6 +38,7 @@     , insertSymEnv     , deleteSymEnv     , insertsSymEnv+    , deletesSymEnv     , symbolAtName     , symbolAtSortIndex @@ -133,6 +134,7 @@     -- 'seAppls' stack, and @seApplsCur@ is cleared.   , seApplsCur :: !(M.HashMap FuncSort Int)   , seIx       :: !Int                      -- ^ Largest unused index for sorts+  , seString   :: !Bool                     -- ^ Use string literals   }   deriving (Eq, Show, Data, Typeable, Generic) @@ -157,17 +159,19 @@                     , seAppls    = zipWith (<>) (seAppls e1) (seAppls e2)                     , seApplsCur = seApplsCur e1 <> seApplsCur e2                     , seIx       = seIx       e1 `max` seIx    e2+                    , seString   = seString e1 && seString e2                     }  instance Monoid SymEnv where-  mempty        = SymEnv emptySEnv emptySEnv emptySEnv emptySEnv [] mempty 0+  mempty        = SymEnv emptySEnv emptySEnv emptySEnv emptySEnv [] mempty 0 True   mappend       = (<>) -symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv-symEnv xEnv fEnv ds ls _ = SymEnv xEnv' fEnv dEnv ls [] mempty 0+symEnv :: Config -> SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv+symEnv cfg xEnv fEnv ds ls _ = SymEnv xEnv' fEnv dEnv ls [] mempty 0 seStr   where     xEnv'   = unionSEnv xEnv wiredInEnv     dEnv    = fromListSEnv [(symbol d, d) | d <- ds]+    seStr   = not (noStringTheory cfg)  -- | These are "BUILT-in" polymorphic functions which are --   UNINTERPRETED but POLYMORPHIC, hence need to go through@@ -193,6 +197,9 @@ insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv insertsSymEnv = L.foldl' (\env (x, s) -> insertSymEnv x s env) +deletesSymEnv :: SymEnv -> [Symbol] -> SymEnv+deletesSymEnv = L.foldl' (\env x -> deleteSymEnv x env)+ symbolAtSortIndex :: Symbol -> Int -> Text symbolAtSortIndex mkSym si = appendSymbolText mkSym . Text.pack . show $ si @@ -308,9 +315,13 @@ --   'smtSort True  msg t' serializes a sort 't' using type variables, --   'smtSort False msg t' serializes a sort 't' using 'Int' instead of tyvars. sortSmtSort :: Bool -> SEnv DataDecl -> Sort -> SmtSort-sortSmtSort poly env t = {- tracepp ("sortSmtSort: " ++ showpp t) $ -} go . unAbs $ t+sortSmtSort poly env t = sortSmtSort' poly env m t   where     m = sortAbs t++sortSmtSort' :: Bool -> SEnv DataDecl -> Int -> Sort -> SmtSort+sortSmtSort' poly env m t = go . unAbs $ t+  where     go (FFunc _ _)    = SInt     go FInt           = SInt     go FReal          = SReal@@ -327,16 +338,16 @@ fappSmtSort :: Bool -> Int -> SEnv DataDecl -> Sort -> [Sort] -> SmtSort fappSmtSort poly m env = go   where--- HKT    go t@(FVar _) ts            = SApp (sortSmtSort poly env <$> (t:ts))-+    -- See https://github.com/ucsd-progsys/liquid-fixpoint/pull/839 for why+    -- @FAbs m@ is re-added.     go (FTC c) [a]-      | setConName == symbol c   = SSet (sortSmtSort poly env a)+      | setConName == symbol c   = SSet (sortSmtSort' poly env m a)     go (FTC c) [a]-      | bagConName == symbol c   = SBag (sortSmtSort poly env a)+      | bagConName == symbol c   = SBag (sortSmtSort' poly env m a)     go (FTC c) [FNatNum n]       | ffldConName == symbol c  = SFFld n     go (FTC c) [a, b]-      | arrayConName == symbol c = SArray (sortSmtSort poly env a) (sortSmtSort poly env b)+      | arrayConName == symbol c = SArray (sortSmtSort' poly env m a) (sortSmtSort' poly env m b)     go (FTC bv) [FTC s]       | bitVecName == symbol bv       , Just n <- sizeBv s      = SBitVec n@@ -344,7 +355,7 @@       | isString s              = SString     go (FTC c) ts       | Just n <- tyArgs c env-      , let i = n - length ts   = SData c ((sortSmtSort poly env . FAbs m <$> ts) ++ pad i)+      , let i = n - length ts   = SData c ((sortSmtSort' poly env m <$> ts) ++ pad i)     go _ _                      = SInt      pad i | poly                = []@@ -389,4 +400,5 @@          , seAppls    = seAppls  env          , seApplsCur = seApplsCur env          , seIx       = seIx     env+         , seString   = seString env          }

@@ -60,7 +60,7 @@     rs                   = reftConjuncts (sr_reft sr)     t                    = sr_sort sr -    go ps ks ((v, PKVar k su    ):xs) = go ps (KVS v t k su:ks) xs+    go ps ks ((v, PKVar k tsu su):xs) = go ps (KVS v t k su tsu:ks) xs     go ps ks ((_, p):xs)              = go (p:ps) ks xs     go ps ks []                       = (ps, ks) 

@@ -16,6 +16,7 @@    -- * Extracting Symbolic Constants (String Literals)   ,  SymConsts (..)+  ,  getConstants    -- * Default Visitor   , defaultFolder@@ -41,6 +42,7 @@   , applyCoSub   , CoSubV   , applyCoSubV+  , applyCoercion    -- * Predicates on Constraints   , isConcC , isConc, isKvarC@@ -63,6 +65,7 @@ import GHC.IO (unsafePerformIO) import Data.IORef (newIORef, readIORef, IORef, modifyIORef') import Prelude hiding (Foldable)+import Data.Containers.ListUtils (nubOrd)   @@ -127,7 +130,7 @@       step (PExist xts p)   = PExist xts (vE p)       step (ETApp e s)      = ETApp (vE e) s       step (ETAbs e s)      = ETAbs (vE e) s-      step p@(PKVar _ _)    = p+      step p@(PKVar {})       = p  instance Visitable Reft where   transE v (Reft (x, ra)) = Reft (x, transE v ra)@@ -274,18 +277,19 @@     step !c (PExist xts p)  = PExist xts  <$> vE c p     step !c (ETApp e s)     = (`ETApp` s) <$> vE c e     step !c (ETAbs e s)     = (`ETAbs` s) <$> vE c e-    step _  p@(PKVar _ _)   = return p+    step _  p@(PKVar {})    = return p  mapKVars :: Visitable t => (KVar -> Maybe Expr) -> t -> t mapKVars f = mapKVars' f'   where     f' (kv', _) = f kv' -mapKVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t+mapKVars' :: Visitable t => ((KVar, KVarSubst Symbol Symbol) -> Maybe Expr) -> t -> t mapKVars' f = trans txK   where-    txK (PKVar k su)-      | Just p' <- f (k, su) = subst su p'+    txK (PKVar k tsu su)+      | Just p' <- f (k, su) = ksubst su p'+      | otherwise = PKVar k tsu su     txK p = p  @@ -359,7 +363,7 @@       ETAbs e s ->         let !e' = go e         in ETAbs e' s-      PKVar k (Su m) -> PKVar k (Su (go <$>m))+      PKVar k tsu su -> PKVar k tsu (mapKVarSubst go su)       e@EVar{} -> e       e@ESym{} -> e       e@ECon{} -> e@@ -398,7 +402,7 @@     go e@(ESym _)      = f e     go e@(ECon _)      = f e     go e@(EVar _)      = f e-    go e@(PKVar _ _)   = f e+    go e@(PKVar {})      = f e     go (ENeg e)        = f . ENeg =<< go e     go (PNot p)        = f . PNot =<< go p     go (ECst e t)      = f . (`ECst` t) =<< go e@@ -418,10 +422,10 @@     go (PAnd ps)       = f . PAnd =<< (go `traverse` ps)     go (POr ps)        = f . POr =<< (go `traverse` ps) -mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t+mapKVarSubsts :: Visitable t => (KVar -> KVarSubst Symbol Symbol -> KVarSubst Symbol Symbol) -> t -> t mapKVarSubsts f          = trans txK   where-    txK (PKVar k su)   = PKVar k (f k su)+    txK (PKVar k tsu su)   = PKVar k tsu (f k su)     txK p              = p  newtype MInt = MInt Integer -- deriving (Eq, NFData)@@ -464,7 +468,7 @@       ESym _ -> acc       ECon _ -> acc       EVar _ -> acc-      PKVar k _ -> k : acc+      PKVar k _ _ -> k : acc       ENeg e -> go acc e       PNot p -> go acc p       ECst e _t -> go acc e@@ -532,11 +536,15 @@ type CoSub = M.HashMap Symbol Sort  applyCoSub :: CoSub -> Expr -> Expr-applyCoSub coSub = mapExprOnExpr fE+applyCoSub coSub+   | M.null coSub = id+   | otherwise = mapExprOnExpr fE   where     fE (ECoerc s t e) = ECoerc  (txS s) (txS t) e     fE (ELam (x,t) e) = ELam (x, txS t)         e     fE (ECst e t)     = ECst e (txS t)+    fE (PExist xts p) = PExist (map (fmap txS) xts) (fE p)+    fE (PAll xts p) = PAll (map (fmap txS) xts) (fE p)     fE e              = e     txS               = mapSortOnlyOnce fS     fS (FObj a)       = {- FObj -} txV a@@ -558,6 +566,13 @@      fS t              = M.lookupDefault t t coSub +applyCoercion :: Symbol -> Sort -> Sort -> Sort+applyCoercion a t = mapSortOnlyOnce f+  where+    f (FObj b)+      | a == b    = t+    f s           = s+ --------------------------------------------------------------------------------- -- | Visitors over @Sort@ ---------------------------------------------------------------------------------@@ -663,3 +678,14 @@     scVis            = (defaultFolder :: Folder [SymConst] t)  { accExpr = sc }     sc _ (ESym c)    = [c]     sc _ _           = []++getConstants' :: Foldable t => t -> [Constant]+getConstants' = nubOrd . fold cVis () []+  where+    cVis           = (defaultFolder :: Folder [Constant] t) { accExpr = ac }+    ac _ (ECon c)  = [c]+    ac _ _         = []++-- | getConstants returns both the vanilla constants AND the sym-constants as str-literals+getConstants :: Foldable t => t -> [Constant]+getConstants z = nubOrd $ getConstants' z ++ [ L t strSort | SL t <- getSymConsts z]

@@ -13,6 +13,7 @@     Ext (..)   , extFileName   , extFileNameR+  , extFileNameR'   , tempDirectory   , tempFileName   , extModuleName@@ -158,6 +159,12 @@  extFileNameR     :: Ext -> FilePath -> FilePath extFileNameR ext = (`addExtension` extMap ext)++-- | Like 'extFileName' but uses a custom output directory when provided.+-- When 'Nothing', falls back to the default @.liquid/@ directory behavior.+extFileNameR' :: Maybe FilePath -> Ext -> FilePath -> FilePath+extFileNameR' Nothing  e f = extFileName e f+extFileNameR' (Just d) e f = d </> takeFileName (addExtension f (extMap e))  isExtFile ::  Ext -> FilePath -> Bool isExtFile ext = (extMap ext ==) . takeExtension

@@ -0,0 +1,18 @@+bind 0 alpha : {v : frac | true}+bind 1 x : {VV : alpha | []}+bind 2 y : {VV : alpha | [(VV != 0.0)]}++++constraint:+  env [0]+  lhs {v : alpha | (v = 10.0)}+  rhs {v : alpha | (v < 11.0)}+  id 1 tag []+++constraint:+  env [0;1;2]+  lhs {v : int | []}+  rhs {v : int | [(((x / y) * y) = x)]}+  id 2 tag []

@@ -72,7 +72,7 @@ subexprs (PImp e0 e1)    = [e0, e1] subexprs (PIff e0 e1)    = [e0, e1] subexprs (PAtom _ e0 e1) = [e0, e1]-subexprs (PKVar _ _)     = []+subexprs (PKVar _ _ _)   = [] subexprs (PAll _ e)      = [e] subexprs (PExist _ e)    = [e] subexprs (ECoerc _ _ e)  = [e]@@ -101,7 +101,7 @@   , (1, PImp <$> arbitraryExpr' <*> arbitraryExpr')   , (1, PIff <$> arbitraryExpr' <*> arbitraryExpr')   , (1, PAtom <$> arbitrary <*> arbitraryExpr' <*> arbitraryExpr')-  , (1, PKVar <$> arbitrary <*> arbitrary)+  , (1, PKVar <$> arbitrary <*> pure mempty <*> arbitrary)   , (1, PAll <$> arbitraryList arbitrary <*> arbitraryExpr')   , (1, PExist <$> arbitraryList arbitrary <*> arbitraryExpr')   , (1, ECoerc <$> arbitrary <*> arbitrary <*> arbitraryExpr')@@ -138,6 +138,16 @@     l <- vectorOf n arbitrary     return $ Su $ M.fromList l   shrink _ = mempty++instance Arbitrary (KVarSubst Symbol Symbol) where+  arbitrary = do+    n <- choose (0, 3)+    l <- vectorOf n arbitrary+    return $ toKVarSubst $ M.fromList l++instance Arbitrary (M.HashMap Symbol Sort) where+  arbitrary = M.fromList <$> arbitrary+  shrink = map M.fromList . shrink . M.toList  -- | This instance only creates `FVar` when they would be in scope from an -- enclosing `FAbs`, and does not create `FObj`s

@@ -2,7 +2,7 @@  module ParserTests (tests) where -import Language.Fixpoint.Types (showFix)+import Language.Fixpoint.Types (showpp, showFix) import Language.Fixpoint.Parse import Test.Tasty import Test.Tasty.HUnit@@ -214,13 +214,16 @@    --   "PGrad $\"\\\"test\\\" (line 1, column 3)\"  (GradInfo {gsrc = SS {sp_start = \"test\" (line 1, column 3), sp_stop = \"test\" (line 1, column 3)}, gused = Nothing}) (PAnd [])"      , testCase "kvarPred empty" $-        show (doParse' predP "test" "$foo") @?= "PKVar $\"foo\" "+        show (doParse' predP "test" "$foo") @?= "PKVar $\"foo\" (fromList []) "      , testCase "kvarPred one" $-        show (doParse' predP "test" "$foo  [x := 1]") @?= "PKVar $\"foo\" [x:=1]"+        show (doParse' predP "test" "$foo  [x := 1]") @?= "PKVar $\"foo\" (fromList []) [x:=1]"      , testCase "kvarPred two" $-        show (doParse' predP "test" "$foo  [x := 1] [ y := true ]") @?= "PKVar $\"foo\" [x:=1][y:=true]"+        show (doParse' predP "test" "$foo  [x := 1] [ y := true ]") @?= "PKVar $\"foo\" (fromList []) [x:=1][y:=true]"++    , testCase "kvarPred tyvar subst" $+        showpp (doParse' predP "test" "$foo[@a:=b;c:=d] [x := 1] [ y := true ]") @?= "$foo[@a:=b;c:=d][x:=1][y:=true]"      , testCase "fastIf" $         show (doParse' predP "test" "if true then true else false" ) @?=

@@ -4,7 +4,7 @@ import qualified Data.HashSet as S import Language.Fixpoint.Solver.Interpreter (ICtx (..), Knowledge (..)) import qualified Language.Fixpoint.Solver.Interpreter as Interpreter-import Language.Fixpoint.Types.Environments (SEnv (..))+import Language.Fixpoint.Types.Environments (SEnvB (..)) import Language.Fixpoint.Types.Refinements (Expr)  interpret' :: Expr -> Expr

@@ -1,7 +1,7 @@ module SimplifyTests (tests) where  import Arbitrary (subexprs)-import Language.Fixpoint.Types.Refinements (Bop (Minus), Constant (I), Expr, ExprV (..))+import Language.Fixpoint.Types.Refinements (Bop (Minus), Constant (I), Expr, ExprBV (..)) import qualified SimplifyInterpreter import qualified SimplifyPLE import Test.Tasty

@@ -85,41 +85,48 @@ combineReporters _ _ = error "combineReporters needs TestReporters"  unitTests :: FilePath -> IO TestTree-unitTests lfDir-  = group "Unit" [-      testGroup "native-pos"       <$> dirTests     nativeCmd   "tests/pos"              skipNativePos  ExitSuccess-    , testGroup "native-neg"       <$> dirTests     nativeCmd   "tests/neg"              ["float.fq"]  (ExitFailure 1)-    , testGroup "elim-crash"       <$> dirTests     nativeCmd   "tests/crash"            []            (ExitFailure 1)-    , testGroup "elim-pos1"        <$> dirTests     elimCmd     "tests/pos"              []             ExitSuccess-    , testGroup "elim-pos2"        <$> dirTests     elimCmd     "tests/elim"             []             ExitSuccess-    , testGroup "elim-neg"         <$> dirTests     elimCmd     "tests/neg"              ["float.fq"]  (ExitFailure 1)-    , testGroup "elim-crash"       <$> dirTests     elimCmd     "tests/crash"            []            (ExitFailure 1)-    , testGroup "cvc5-pos"         <$> dirTests     cvc5Cmd     "tests/pos"              skipNativePos  ExitSuccess-    , testGroup "cvc5-spec"        <$> dirTests     cvc5Cmd     "tests/cvc5"             skipNativePos  ExitSuccess-    , testGroup "proof"            <$> dirTests     elimCmd     "tests/proof"            []             ExitSuccess-    , testGroup "rankN"            <$> dirTests     elimCmd     "tests/rankNTypes"       []             ExitSuccess-    , testGroup "horn-pos-el"      <$> dirTests     elimSaveCmd "tests/horn/pos"         []             ExitSuccess-    , testGroup "horn-pos-cvc5"    <$> dirTests     cvc5Cmd     "tests/horn/pos"         []             ExitSuccess-    , testGroup "horn-neg-el"      <$> dirTests     elimSaveCmd "tests/horn/neg"         []            (ExitFailure 1)-    , testGroup "horn-neg-cvc5"    <$> dirTests     cvc5Cmd     "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`)+unitTests lfDir =+    group "All"+      [ group "original"+        [ dirTests "native-pos"           nativeCmd   "tests/pos"              posOptions skipNativePos  ExitSuccess+        , dirTests "native-neg"           nativeCmd   "tests/neg"              [] ["float.fq"]  (ExitFailure 1)+        , dirTests "elim-crash"           nativeCmd   "tests/crash"            posOptions []            (ExitFailure 1)+        , dirTests "elim-pos1"            elimCmd     "tests/pos"              posOptions []             ExitSuccess+        , dirTests "elim-pos2"            elimCmd     "tests/elim"             posOptions []             ExitSuccess+        , dirTests "elim-neg"             elimCmd     "tests/neg"              [] ["float.fq"]  (ExitFailure 1)+        , dirTests "elim-crash"           elimCmd     "tests/crash"            []                      []            (ExitFailure 1)+        , dirTests "cvc5-pos"             cvc5Cmd     "tests/pos"              posOptions skipNativePos  ExitSuccess+        , dirTests "cvc5-spec"            cvc5Cmd     "tests/cvc5"             posOptions skipNativePos  ExitSuccess+        , dirTests "proof"                elimCmd     "tests/proof"            posOptions []             ExitSuccess+        , dirTests "rankN"                elimCmd     "tests/rankNTypes"       posOptions []             ExitSuccess+        , dirTests "horn-pos-el"          elimSaveCmd "tests/horn/pos"         posOptions []             ExitSuccess+        , dirTests "horn-pos-cvc5"        cvc5Cmd     "tests/horn/pos"         posOptions []             ExitSuccess+        , dirTests "horn-neg-el"          elimSaveCmd "tests/horn/neg"         []         []            (ExitFailure 1)+        , dirTests "horn-neg-cvc5"        cvc5Cmd     "tests/horn/neg"         []         []            (ExitFailure 1)+        , dirTests "horn-pos-na"          nativeCmd   "tests/horn/pos"         posOptions []             ExitSuccess+        , dirTests "horn-neg-na"          nativeCmd   "tests/horn/neg"         []         []            (ExitFailure 1)+        ]+      , after AllSucceed "original" <$> group "saved"+        [ dirJsonTests "horn-json-pos-el" elimCmd     "tests/logs/cur/horn-pos-el" []         []             ExitSuccess+        , dirJsonTests "horn-json-neg-el" elimCmd     "tests/logs/cur/horn-neg-el" []         []            (ExitFailure 1)+        , dirHornTests "horn-smt2-pos-el" elimCmd     "tests/logs/cur/horn-pos-el" []         []             ExitSuccess+        , dirHornTests "horn-smt2-neg-el" elimCmd     "tests/logs/cur/horn-neg-el" []         []            (ExitFailure 1)+        ]+      ]+  where+    posOptions = ["--save-bfq-on-error"] -    dirTests' :: (FilePath -> Bool) -> TestCmd -> FilePath -> [FilePath] -> ExitCode -> IO [TestTree]-    dirTests' isT testCmd root ignored code = do+    dirTests     n a b c d e = testGroup n <$> dirTests' n isTest a b c d e+    dirJsonTests n a b c d e = testGroup n <$> dirTests' n ("horn.json" `isSuffixOf`) a b c d e+    dirHornTests n a b c d e = testGroup n <$> dirTests' n ("horn.smt2" `isSuffixOf`) a b c d e++    dirTests' :: String -> (FilePath -> Bool) -> TestCmd -> FilePath -> [String] -> [FilePath] -> ExitCode -> IO [TestTree]+    dirTests' testName isT testCmd root extraOpts ignored code = do       let absRoot = lfDir </> root       files    <- walkDirectory absRoot       let tests = [ rel | f <- files, isT f, let rel = makeRelative absRoot f, rel `notElem` ignored ]-      return    $ mkTest testCmd code absRoot <$> tests+          saveDir = "--save-dir=" ++ lfDir </> "tests" </> "logs" </> "cur" </> testName+      return $ mkTest testName testCmd code (saveDir : extraOpts) absRoot <$> tests  isTest   :: FilePath -> Bool isTest f = takeExtension f `elem` [".fq", ".smt2"]@@ -150,9 +157,9 @@       )  ----------------------------------------------------------------------------mkTest :: TestCmd -> ExitCode -> FilePath -> FilePath -> TestTree+mkTest :: String -> TestCmd -> ExitCode -> [String] -> FilePath -> FilePath -> TestTree ----------------------------------------------------------------------------mkTest testCmd code dir file+mkTest testName testCmd code extraOpts dir file   =     askOption $ \opts ->     testCase file $@@ -163,7 +170,7 @@       else do         createDirectoryIfMissing True $ takeDirectory log         c <- withFile log WriteMode $ \h -> do-          let cmd     = testCmd opts "fixpoint" dir file+          let cmd     = testCmd (LO (unwords extraOpts) <> opts) "fixpoint" dir file           (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}           waitForProcess ph         when (code /= c) $@@ -172,7 +179,9 @@    where     test = dir </> file-    log  = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log"+    -- select a file name that is unique to the test, as the tests might run+    -- in parallel.+    log  = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> testName </> f <.> "harness.log"  knownToFail :: [a] knownToFail = []@@ -194,10 +203,6 @@ cvc5Cmd :: TestCmd cvc5Cmd (LO opts) bin dir file =   printf "cd %s && %s --solver=cvc5 %s %s" dir bin opts file--cvc5SaveCmd :: TestCmd-cvc5SaveCmd (LO opts) bin dir file =-  printf "cd %s && %s --save --solver=cvc5 %s %s" dir bin opts file  ---------------------------------------------------------------------------------------- -- Generic Helpers