liquid-fixpoint 0.9.6.3.1 → 0.9.6.3.2

raw patch · 62 files changed

+2511/−1616 lines, 62 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGES.md +14/−0
• liquid-fixpoint.cabal +3/−1
• src/Language/Fixpoint/Defunctionalize.hs +35/−5
• src/Language/Fixpoint/Horn/Transformations.hs +20/−20
• src/Language/Fixpoint/Horn/Types.hs +0/−6
• src/Language/Fixpoint/Misc.hs +4/−35
• src/Language/Fixpoint/Parse.hs +206/−160
• src/Language/Fixpoint/Smt/Interface.hs +29/−21
• src/Language/Fixpoint/Smt/Serialize.hs +11/−12
• src/Language/Fixpoint/Smt/Theories.hs +201/−257
• src/Language/Fixpoint/Smt/Types.hs +2/−0
• src/Language/Fixpoint/Solver.hs +2/−2
• src/Language/Fixpoint/Solver/Common.hs +4/−4
• src/Language/Fixpoint/Solver/EnvironmentReduction.hs +11/−6
• src/Language/Fixpoint/Solver/Extensionality.hs +15/−9
• src/Language/Fixpoint/Solver/GradualSolution.hs +19/−13
• src/Language/Fixpoint/Solver/Instantiate.hs +15/−8
• src/Language/Fixpoint/Solver/Interpreter.hs +3/−2
• src/Language/Fixpoint/Solver/Monad.hs +3/−21
• src/Language/Fixpoint/Solver/PLE.hs +415/−153
• src/Language/Fixpoint/Solver/Prettify.hs +1/−1
• src/Language/Fixpoint/Solver/Rewrite.hs +2/−0
• src/Language/Fixpoint/Solver/Sanitize.hs +18/−30
• src/Language/Fixpoint/Solver/Solution.hs +135/−104
• src/Language/Fixpoint/Solver/Solve.hs +24/−14
• src/Language/Fixpoint/Solver/TrivialSort.hs +1/−1
• src/Language/Fixpoint/Solver/UniqifyBinds.hs +1/−1
• src/Language/Fixpoint/Solver/UniqifyKVars.hs +1/−1
• src/Language/Fixpoint/SortCheck.hs +322/−233
• src/Language/Fixpoint/Types/Config.hs +15/−1
• src/Language/Fixpoint/Types/Constraints.hs +55/−16
• src/Language/Fixpoint/Types/Environments.hs +11/−3
• src/Language/Fixpoint/Types/Graduals.hs +11/−11
• src/Language/Fixpoint/Types/Names.hs +15/−8
• src/Language/Fixpoint/Types/Refinements.hs +106/−92
• src/Language/Fixpoint/Types/Solutions.hs +18/−10
• src/Language/Fixpoint/Types/Sorts.hs +53/−23
• src/Language/Fixpoint/Types/Substitutions.hs +7/−55
• src/Language/Fixpoint/Types/Templates.hs +1/−0
• src/Language/Fixpoint/Types/Theories.hs +95/−38
• src/Language/Fixpoint/Types/Visitor.hs +267/−93
• tests/neg/localrw.fq +16/−0
• tests/neg/maps.fq +8/−15
• tests/pos/bags.fq +48/−0
• tests/pos/bags02.fq +39/−0
• tests/pos/eta_cons.fq +24/−0
• tests/pos/ext_double_unfold.fq +19/−0
• tests/pos/ext_lam.fq +14/−0
• tests/pos/ext_lam_multi.fq +14/−0
• tests/pos/localrw.fq +16/−0
• tests/pos/maps.fq +7/−15
• tests/pos/maps02.fq +23/−10
• tests/pos/maps03.fq +0/−10
• tests/pos/maps04.fq +0/−39
• tests/pos/maps05.fq +0/−9
• tests/pos/polybag.fq +37/−0
• tests/pos/polyset.fq +11/−16
• tests/tasty/Arbitrary.hs +1/−0
• tests/tasty/InterpretTests.hs +1/−1
• tests/tasty/SimplifyPLE.hs +10/−6
• tests/tasty/SimplifyTests.hs +1/−1
• tests/test.hs +51/−24

@@ -2,6 +2,20 @@  ## NEXT +## 0.9.6.3.2 (2025-03-06)++- Expose relatedSymbols from EnvironmentReduction. Needed for improving error+  messages in LH+  [#2346](https://github.com/ucsd-progsys/liquidhaskell/issues/2346).+- Support extensionality in PLE [#704](https://github.com/ucsd-progsys/liquid-fixpoint/pull/704)+- Add a new flag `--etabeta` to reason with lambdas in PLE [#705](https://github.com/ucsd-progsys/liquid-fixpoint/pull/705)+- Add support for reflected lambdas in PLE [#725](https://github.com/ucsd-progsys/liquid-fixpoint/pull/725)+- Implement Bags and Maps reasoning with Arrays [#703](https://github.com/ucsd-progsys/liquid-fixpoint/pull/703)+- Support conditional elaboration of theories for cvc5 [#734](https://github.com/ucsd-progsys/liquid-fixpoint/pull/734)+- Generate smt2 files only when using `--save` [#712](https://github.com/ucsd-progsys/liquid-fixpoint/pull/712)+- Parameterize Expr and Reft by the variable type [#708](https://github.com/ucsd-progsys/liquid-fixpoint/pull/721)+- Preserve location of operators in the parser [#721](https://github.com/ucsd-progsys/liquid-fixpoint/pull/721)+- Optimize elaboration [#736](https://github.com/ucsd-progsys/liquid-fixpoint/pull/736)  ## 0.9.6.3.1 (2024-08-21) 

@@ -1,6 +1,6 @@ cabal-version:      2.4 name:               liquid-fixpoint-version:            0.9.6.3.1+version:            0.9.6.3.2 synopsis:           Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description:   This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint@@ -176,6 +176,8 @@     ghc-options: -Wno-unused-imports   if impl(ghc>9.8)     ghc-options: -Wno-x-partial+  if impl(ghc>9.10)+    ghc-options: -Wno-deriving-typeable   if flag(devel)     ghc-options: -Werror   if !os(windows)

@@ -24,14 +24,17 @@  import qualified Data.HashMap.Strict as M import           Data.Hashable+import           Data.Bifunctor (bimap) import           Control.Monad ((>=>)) import           Control.Monad.State-import           Language.Fixpoint.Misc            (fM, secondM, mapSnd)+import           Language.Fixpoint.Misc            (fM, secondM) import           Language.Fixpoint.Solver.Sanitize (symbolEnv) import           Language.Fixpoint.Types        hiding (GInfo(..), allowHO, fi) import qualified Language.Fixpoint.Types           as Types (GInfo(..)) import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types.Visitor   (mapMExpr)++ -- import Debug.Trace (trace)  defunctionalize :: (Fixpoint a) => Config -> SInfo a -> SInfo a@@ -68,11 +71,12 @@ -- is surrounded with a cast.  normalizeLams :: Expr -> Expr-normalizeLams e = snd $ normalizeLamsFromTo 1 e+normalizeLams = snd . normalizeLamsFromTo 1  normalizeLamsFromTo :: Int -> Expr -> (Int, Expr) normalizeLamsFromTo i   = go   where+    go :: Expr -> (Int, Expr)     go (ELam (y, sy) e) = (i' + 1, shiftLam i' y sy e') where (i', e') = go e                           -- let (i', e') = go e                           --    y'       = lamArgSymbol i'  -- SHIFTLAM@@ -80,8 +84,34 @@     go (EApp e1 e2)     = let (i1, e1') = go e1                               (i2, e2') = go e2                           in (max i1 i2, EApp e1' e2')-    go (ECst e s)       = mapSnd (`ECst` s) (go e)-    go (PAll bs e)      = mapSnd (PAll bs) (go e)+    go (ECst e s)       = fmap (`ECst` s) (go e)+    go (EIte e1 e2 e3)  = let (i1, e1') = go e1+                              (i2, e2') = go e2+                              (i3, e3') = go e3+                          in (maximum [i1, i2, i3], EIte e1' e2' e3')+    go (ENeg e)         = fmap ENeg (go e)+    go (EBin op e1 e2)  = let (i1, e1') = go e1+                              (i2, e2') = go e2+                          in (max i1 i2, EBin op e1' e2')+    go (ETApp e s)      = fmap (`ETApp` s) (go e)+    go (ETAbs e s)      = fmap (`ETAbs` s) (go e)+    go (PAnd [])        = (i, PAnd [])+    go (POr [])         = (i, POr  [])+    go (PAnd es)        = bimap maximum PAnd $ unzip $ fmap go es+    go (POr es)         = bimap maximum POr  $ unzip $ fmap go es+    go (PNot e)         = fmap PNot (go e)+    go (PImp e1 e2)     = let (i1, e1') = go e1+                              (i2, e2') = go e2+                          in (max i1 i2, PImp e1' e2')+    go (PIff e1 e2)     = let (i1, e1') = go e1+                              (i2, e2') = go e2+                          in (max i1 i2, PIff e1' e2')+    go (PAtom r e1 e2)  = let (i1, e1') = go e1+                              (i2, e2') = go e2+                          in (max i1 i2, PAtom r e1' e2')+    go (PAll bs e)      = fmap (PAll bs) (go e)+    go (PExist bs e)    = fmap (PExist bs) (go e)+    go (ECoerc s1 s2 e) = fmap (ECoerc s1 s2) (go e)     go e                = (i, e)  @@ -179,7 +209,7 @@   , dfLams  :: ![Expr]      -- ^ lambda expressions appearing in the expressions   , dfRedex :: ![Expr]      -- ^ redexes appearing in the expressions   , dfBinds :: !(SEnv Sort) -- ^ sorts of new lambda-binders-  }+  } deriving Show  makeDFState :: Config -> SymEnv -> IBindEnv -> DFST makeDFState cfg env ibind = DFST

@@ -125,7 +125,7 @@   whenLoud $ printPiSols piSols    whenLoud $ putStrLn "solved pis:"-  let solvedPiCstrs = solPis (S.fromList $ M.keys cons ++ M.keys dist) piSols+  let solvedPiCstrs = solPis cfg (S.fromList $ M.keys cons ++ M.keys dist) piSols   whenLoud $ putStrLn $ F.showpp solvedPiCstrs    whenLoud $ putStrLn "solved horn:"@@ -164,18 +164,18 @@ map3 f (x, y, z) = (x, y, f z)  -- | Solve out the given pivars-solPis :: S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> M.HashMap F.Symbol Pred-solPis measures piSolsMap = go (M.toList piSolsMap) piSolsMap+solPis :: F.Config -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> M.HashMap F.Symbol Pred+solPis cfg measures piSolsMap = go (M.toList piSolsMap) piSolsMap   where     go ((pi', ((n, xs), c)):pis) piSols = M.insert pi' solved $ go pis piSols-      where solved = solPi measures pi' n (S.fromList xs) piSols c+      where solved = solPi cfg measures pi' n (S.fromList xs) piSols c     go [] _ = mempty  -- TODO: rewrite to use CC-solPi :: S.Set F.Symbol -> F.Symbol -> F.Symbol -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> Cstr a -> Pred-solPi measures basePi n args piSols cstr = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp cstr <> "\n\n") $ PAnd rewritten+solPi :: F.Config -> S.Set F.Symbol -> F.Symbol -> F.Symbol -> S.Set F.Symbol -> M.HashMap F.Symbol ((F.Symbol, [F.Symbol]), Cstr a) -> Cstr a -> Pred+solPi cfg measures basePi n args piSols cstr = trace ("\n\nsolPi: " <> F.showpp basePi <> "\n\n" <> F.showpp n <> "\n" <> F.showpp (S.toList args) <> "\n" <> F.showpp ((\(a, _, c) -> (a, c)) <$> edges) <> "\n" <> F.showpp (sols n) <> "\n" <> F.showpp rewritten <> "\n" <> F.showpp cstr <> "\n\n") $ PAnd rewritten   where-    rewritten = rewriteWithEqualities measures n args equalities+    rewritten = rewriteWithEqualities cfg measures n args equalities     equalities = (nub . fst) $ go (S.singleton basePi) cstr     edges = eqEdges args mempty equalities     (eGraph, vf, lookupVertex) = DG.graphFromEdges edges@@ -543,7 +543,7 @@ -- exists in the positive positions (which will stay exists when we go to -- prenex) may give us a lot of trouble during _quantifier elimination_ -- tx :: F.Symbol -> [[Bind]] -> Pred -> Pred--- tx k bss = trans (defaultVisitor { txExpr = existentialPackage, ctxExpr = ctxKV }) M.empty ()+-- tx k bss = trans (defaultFolder { txExpr = existentialPackage, ctxExpr = ctxKV }) M.empty () --   where --   splitBinds xs = unzip $ (\(Bind x t p) -> ((x,t),p)) <$> xs --   cubeSol su (Bind _ _ (Reft eqs):xs)@@ -564,16 +564,16 @@ --   ctxKV m _ = m  -- Visitor only visit Exprs in Pred!-instance V.Visitable Pred where-  visit v c (PAnd ps) = PAnd <$> mapM (visit v c) ps-  visit v c (Reft e) = Reft <$> visit v c e-  visit _ _ var      = pure var+instance V.Foldable Pred where+  foldE v c (PAnd ps) = PAnd <$> mapM (foldE v c) ps+  foldE v c (Reft e) = Reft <$> foldE v c e+  foldE _ _ var      = pure var -instance V.Visitable (Cstr a) where-  visit v c (CAnd cs) = CAnd <$> mapM (visit v c) cs-  visit v c (Head p a) = Head <$> visit v c p <*> pure a-  visit v ctx (All (Bind x t p l) c) = All <$> (Bind x t <$> visit v ctx p <*> pure l) <*> visit v ctx c-  visit v ctx (Any (Bind x t p l) c) = All <$> (Bind x t <$> visit v ctx p <*> pure l) <*> visit v ctx c+instance V.Foldable (Cstr a) where+  foldE v c (CAnd cs) = CAnd <$> mapM (foldE v c) cs+  foldE v c (Head p a) = Head <$> foldE v c p <*> pure a+  foldE v ctx (All (Bind x t p l) c) = All <$> (Bind x t <$> foldE v ctx p <*> pure l) <*> foldE v ctx c+  foldE v ctx (Any (Bind x t p l) c) = All <$> (Bind x t <$> foldE v ctx p <*> pure l) <*> foldE v ctx c  ------------------------------------------------------------------------------ -- | Quantifier elimination for use with implicit solver@@ -630,8 +630,8 @@ --     equalities = collectEqualities c --     ps = rewriteWithEqualities n args equalities -rewriteWithEqualities :: S.Set F.Symbol -> F.Symbol -> S.Set F.Symbol -> [(F.Symbol, F.Expr)] -> [Pred]-rewriteWithEqualities measures n args equalities = preds+rewriteWithEqualities :: F.Config -> S.Set F.Symbol -> F.Symbol -> S.Set F.Symbol -> [(F.Symbol, F.Expr)] -> [Pred]+rewriteWithEqualities cfg measures n args equalities = preds   where     (eGraph, vf, lookupVertex) = DG.graphFromEdges $ eqEdges args mempty equalities @@ -647,7 +647,7 @@       Nothing -> []       Just vertex -> nub $ filter (/= F.EVar x) $ mconcat [es | ((_, es), _, _) <- vf <$> DG.reachable eGraph vertex] -    argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols []) `S.union`measures+    argsAndPrims = args `S.union` S.fromList (map fst $ F.toListSEnv $ F.theorySymbols (F.solver cfg) []) `S.union`measures      isWellFormed :: F.Expr -> Bool     isWellFormed e = S.fromList (F.syms e) `S.isSubsetOf` argsAndPrims

@@ -73,12 +73,6 @@   deriving (Data, Typeable, Generic, Eq, ToJSON, FromJSON)  -instance Semigroup Pred where-  p1 <> p2 = PAnd [p1, p2]--instance Monoid Pred where-  mempty = Reft mempty- instance F.Subable Pred where   syms (Reft e)   = F.syms e   syms (Var _ xs) = xs

@@ -43,6 +43,10 @@ import Prelude hiding (undefined) import GHC.Stack +infixl 9 ==>+(==>) :: Bool -> Bool -> Bool+p ==> q = not p || q+ type (|->) a b = M.HashMap a b  firstMaybe :: (a -> Maybe b) -> [a] -> Maybe b@@ -322,18 +326,6 @@   b <- c   if b then t else e -mapEither :: (a -> Either b c) -> [a] -> ([b], [c])-mapEither _ []     = ([], [])-mapEither f (x:xs) = case f x of-                       Left y  -> (y:ys, zs)-                       Right z -> (ys, z:zs)-                     where-                       (ys, zs) = mapEither f xs--isRight :: Either a b -> Bool-isRight (Right _) = True-isRight _         = False- dbgFalse :: Bool dbgFalse = 1 > (2 :: Int) @@ -390,21 +382,6 @@     vus           = swap <$> uvs     uvs           = [ (u, v) | (u : vs) <- vss, v <- vs ] -{--exitColorStrLn :: Moods -> String -> IO ()-exitColorStrLn c s = do-  writeIORef pbRef Nothing --(Just pr)-  putStrLn "\n"-  colorStrLn c s--}--mapFst :: (a -> c) -> (a, b) -> (c, b)-mapFst f (x, y) = (f x, y)--mapSnd :: (b -> c) -> (a, b) -> (a, c)-mapSnd f (x, y) = (x, f y)-- {-@ allCombinations :: xss:[[a]] -> [{v:[a]| len v == len xss}] @-} allCombinations :: [[a]] -> [[a]] allCombinations xs = assert (all ((length xs == ) . length)) $ go xs@@ -418,14 +395,6 @@  powerset :: [a] -> [[a]] powerset xs = filterM (const [False, True]) xs--infixl 9 =>>-(=>>) :: Monad m => m b -> (b -> m a) -> m b-(=>>) m f = m >>= (\x -> f x >> return x)--infixl 9 <<=-(<<=) :: Monad m => (b -> m a) -> m b -> m b-(<<=) = flip (=>>)  -- Null if first is a subset of second nubDiff :: (Eq a, Hashable a) => [a] -> [a] -> S.HashSet a

@@ -5,6 +5,7 @@ {-# LANGUAGE UndecidableInstances      #-} {-# LANGUAGE DeriveGeneric             #-} {-# LANGUAGE OverloadedStrings         #-}+{-# LANGUAGE ScopedTypeVariables       #-}  module Language.Fixpoint.Parse ( @@ -13,6 +14,8 @@    -- * Top Level Class for Parseable Values   , Parser+  , ParserV+  , ParseableV (..)    -- * Some Important keyword and parsers   , reserved, reservedOp@@ -49,16 +52,17 @@   , locInfixSymbolP    -- * Parsing recursive entities-  , exprP       -- Expressions-  , predP       -- Refinement Predicates-  , funAppP     -- Function Applications-  , qualifierP  -- Qualifiers-  , refaP       -- Refa-  , refP        -- (Sorted) Refinements-  , refDefP     -- (Sorted) Refinements with default binder-  , refBindP    -- (Sorted) Refinements with configurable sub-parsers-  , defineP     -- function definition equations (PLE)-  , matchP      -- measure definition equations (PLE)+  , exprP        -- Expressions+  , predP        -- Refinement Predicates+  , funAppP      -- Function Applications+  , qualifierP   -- Qualifiers+  , refaP        -- Refa+  , refP         -- (Sorted) Refinements+  , refDefP      -- (Sorted) Refinements with default binder+  , refBindP     -- (Sorted) Refinements with configurable sub-parsers+  , defineP      -- function definition equations (PLE)+  , defineLocalP -- local function definition equations (PLE)+  , matchP       -- measure definition equations (PLE)    -- * Layout   , indentedBlock@@ -97,7 +101,7 @@   , isSmall   , isNotReserved -  , initPState, PState (..)+  , initPState, PState, PStateV (..)    , LayoutStack(..)   , Fixity(..), Assoc(..), addOperatorP, addNumTyCon@@ -136,7 +140,7 @@ import           Language.Fixpoint.Types.Errors import qualified Language.Fixpoint.Misc      as Misc import           Language.Fixpoint.Smt.Types-import           Language.Fixpoint.Types hiding    (mapSort, fi, params, GInfo(..))+import           Language.Fixpoint.Types hiding    (mapSort, fi, GInfo(..)) import qualified Language.Fixpoint.Types     as Types (GInfo(FI)) import           Text.PrettyPrint.HughesPJ         (text, vcat, (<+>), Doc) @@ -198,7 +202,8 @@ -- Note that this is in deviation from what the old LH parser did, -- but I think that was plainly wrong. -type Parser = StateT PState (Parsec Void String)+type Parser = ParserV Symbol+type ParserV v = StateT (PStateV v) (Parsec Void String)  -- | The parser state. --@@ -213,14 +218,21 @@ -- -- Finally, we keep track of the layout stack. ---data PState = PState { fixityTable :: OpTable-                     , fixityOps   :: [Fixity]-                     , empList     :: Maybe Expr-                     , singList    :: Maybe (Expr -> Expr)+data PStateV v = PState { fixityTable :: OpTable v+                     , fixityOps   :: [Fixity v]+                      -- | An expression to use whenever an empty list is parsed (@[]@)+                      --+                      -- Receives the location of the empty list+                     , empList     :: Maybe (Located () -> ExprV v)+                      -- | An expression to use whenever a singleton list is parsed (@[e]@)+                      --+                      -- Receives the location of the singleton list and the inner expression+                     , singList    :: Maybe (Located () -> ExprV v -> ExprV v)                      , supply      :: !Integer                      , layoutStack :: LayoutStack                      , numTyCons   :: !(S.HashSet Symbol)                      }+type PState = PStateV Symbol  -- | The layout stack tracks columns at which layout blocks -- have started.@@ -240,12 +252,12 @@ popLayoutStack (After _ s) = s  -- | Modify the layout stack using the given function.-modifyLayoutStack :: (LayoutStack -> LayoutStack) -> Parser ()+modifyLayoutStack :: (LayoutStack -> LayoutStack) -> ParserV v () modifyLayoutStack f =   modify (\ s -> s { layoutStack = f (layoutStack s) })  -- | Start a new layout block at the current indentation level.-setLayout :: Parser ()+setLayout :: ParserV v () setLayout = do   i <- L.indentLevel   -- traceShow ("setLayout", i) $ pure ()@@ -254,13 +266,13 @@ -- | Temporarily reset the layout information, because we enter -- a block with explicit separators. ---resetLayout :: Parser ()+resetLayout :: ParserV v () resetLayout = do   -- traceShow ("resetLayout") $ pure ()   modifyLayoutStack Reset  -- | Remove the topmost element from the layout stack.-popLayout :: Parser ()+popLayout :: ParserV v () popLayout = do   -- traceShow ("popLayout") $ pure ()   modifyLayoutStack popLayoutStack@@ -272,7 +284,7 @@ -- The only "valid" use case for spaces is in top-level parsing -- function, to consume initial spaces. ---spaces :: Parser ()+spaces :: ParserV v () spaces =   L.space     space1@@ -285,7 +297,7 @@ -- This is a variant of 'indentGuard' provided by megaparsec, -- only that it does not consume whitespace. ---guardIndentLevel :: Ordering -> Pos -> Parser ()+guardIndentLevel :: Ordering -> Pos -> ParserV v () guardIndentLevel ord ref = do   actual <- L.indentLevel   -- traceShow ("guardIndentLevel", actual, ord, ref) $ pure ()@@ -300,7 +312,7 @@ -- to check whether the next token is valid within the current -- block. ---guardLayout :: Parser (Parser ())+guardLayout :: ParserV v (ParserV v ()) guardLayout = do   stack <- gets layoutStack   -- traceShow ("guardLayout", stack) $ pure ()@@ -321,7 +333,7 @@ -- a new, nested, layout block, which should be indented further -- than the surrounding blocks. ---strictGuardLayout :: Parser ()+strictGuardLayout :: ParserV v () strictGuardLayout = do   stack <- gets layoutStack   -- traceShow ("strictGuardLayout", stack) $ pure ()@@ -335,12 +347,12 @@ -- whether we are in a position permitted by the layout stack. -- After the token, consume whitespace and potentially change state. ---lexeme' :: Parser () -> Parser a -> Parser a+lexeme' :: ParserV v () -> ParserV v a -> ParserV v a lexeme' spacesP p = do   after <- guardLayout   p <* spacesP <* after -lexeme :: Parser a -> Parser a+lexeme :: ParserV v a -> ParserV v a lexeme = lexeme' spaces  -- | Indentation-aware located lexeme parser.@@ -349,7 +361,7 @@ -- covered by the identifier. I.e., it consumes additional whitespace in the -- end, but that is not part of the source range reported for the identifier. ---locLexeme' :: Parser () -> Parser a -> Parser (Located a)+locLexeme' :: ParserV v () -> ParserV v a -> ParserV v (Located a) locLexeme' spacesP p = do   after <- guardLayout   l1 <- getSourcePos@@ -358,7 +370,7 @@   spacesP <* after   pure (Loc l1 l2 x) -locLexeme :: Parser a -> Parser (Located a)+locLexeme :: ParserV v a -> ParserV v (Located a) locLexeme = locLexeme' spaces  -- | Make a parser location-aware.@@ -366,7 +378,7 @@ -- This is at the cost of an imprecise span because we still -- consume spaces in the end first. ---located :: Parser a -> Parser (Located a)+located :: ParserV v a -> ParserV v (Located a) located p = do   l1 <- getSourcePos   x <- p@@ -379,7 +391,7 @@ -- -- Assumes that the parser for items does not accept the empty string. ---indentedBlock :: Parser a -> Parser [a]+indentedBlock :: ParserV v a -> ParserV v [a] indentedBlock p =       strictGuardLayout *> setLayout *> many (p <* popLayout) <* popLayout       -- We have to pop after every p, because the first successful@@ -390,7 +402,7 @@       -- layout check fails, we still want to accept this as an empty block.  -- | Parse a single line that may be continued via layout.-indentedLine :: Parser a -> Parser a+indentedLine :: ParserV v a -> ParserV v a indentedLine p =   setLayout *> p <* popLayout <* popLayout   -- We have to pop twice, because the first successful token@@ -401,7 +413,7 @@ -- -- Assumes that the parser for items does not accept the empty string. ---indentedOrExplicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]+indentedOrExplicitBlock :: ParserV v open -> ParserV v close -> ParserV v sep -> ParserV v a -> ParserV v [a] indentedOrExplicitBlock open close sep p =       explicitBlock open close sep p   <|> (concat <$> indentedBlock (sepEndBy1 p sep))@@ -409,21 +421,16 @@ -- | Parse a block of items that are delimited via explicit delimiters. -- Layout is disabled/reset for the scope of this block. ---explicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]+explicitBlock :: ParserV v open -> ParserV v close -> ParserV v sep -> ParserV v a -> ParserV v [a] explicitBlock open close sep p =   resetLayout *> open *> sepEndBy p sep <* close <* popLayout  -- | Symbolic lexeme. Stands on its own.-sym :: String -> Parser String+sym :: String -> ParserV v String sym x =   lexeme (string x) --- | Located variant of 'sym'.-locSym :: String -> Parser (Located String)-locSym x =-  locLexeme (string x)--semi, comma, colon, dcolon, dot :: Parser String+semi, comma, colon, dcolon, dot :: ParserV v String semi   = sym ";" comma  = sym "," colon  = sym ":" -- Note: not a reserved symbol; use with care@@ -439,14 +446,14 @@ -- end, and multiple subsequent semicolons, so the resulting parser -- provides the illusion of allowing empty items. ---block :: Parser a -> Parser [a]+block :: ParserV v a -> ParserV v [a] block =   indentedOrExplicitBlock (sym "{" *> many semi) (sym "}") (some semi)  -- | Parses a block with explicit braces and commas as separator. -- Used for record constructors in datatypes. ---explicitCommaBlock :: Parser a -> Parser [a]+explicitCommaBlock :: ParserV v a -> ParserV v [a] explicitCommaBlock =   explicitBlock (sym "{") (sym "}") comma @@ -491,6 +498,7 @@   , "class"   , "data"   , "define"+  , "defineLocal"   , "defined"   , "embed"   , "expression"@@ -545,22 +553,22 @@ -}  -- | Consumes a line comment.-lhLineComment :: Parser ()+lhLineComment :: ParserV v () lhLineComment =   L.skipLineComment "// "  -- | Consumes a block comment.-lhBlockComment :: Parser ()+lhBlockComment :: ParserV v () lhBlockComment =   L.skipBlockComment "/* " "*/"  -- | Parser that consumes a single char within an identifier (not start of identifier).-identLetter :: Parser Char+identLetter :: ParserV v Char identLetter =   alphaNumChar <|> oneOf ("_" :: String)  -- | Parser that consumes a single char within an operator (not start of operator).-opLetter :: Parser Char+opLetter :: ParserV v Char opLetter =   oneOf (":!#$%&*+./<=>?@\\^|-~'" :: String) @@ -571,7 +579,7 @@ -- NOTE: we currently don't double-check that the reserved word is in the -- list of reserved words. ---reserved :: String -> Parser ()+reserved :: String -> ParserV v () reserved x =   void $ lexeme (try (string x <* notFollowedBy identLetter)) @@ -580,7 +588,7 @@   void $ lexeme' spacesP (try (string x <* notFollowedBy identLetter))  -locReserved :: String -> Parser (Located String)+locReserved :: String -> ParserV v (Located String) locReserved x =   locLexeme (try (string x <* notFollowedBy identLetter)) @@ -591,7 +599,7 @@ -- NOTE: we currently don't double-check that the reserved operator is in the -- list of reserved operators. ---reservedOp :: String -> Parser ()+reservedOp :: String -> ParserV v () reservedOp x =   void $ lexeme (try (string x <* notFollowedBy opLetter)) @@ -610,34 +618,30 @@ -- symbol x = --   L.symbol spaces (string x) -parens, brackets, angles, braces :: Parser a -> Parser a+parens, brackets, angles, braces :: ParserV v a -> ParserV v a parens   = between (sym "(") (sym ")") brackets = between (sym "[") (sym "]") angles   = between (sym "<") (sym ">") braces   = between (sym "{") (sym "}") -locParens :: Parser a -> Parser (Located a)-locParens p =-  (\ (Loc l1 _ _) a (Loc _ l2 _) -> Loc l1 l2 a) <$> locSym "(" <*> p <*> locSym ")"- -- | Parses a string literal as a lexeme. This is based on megaparsec's -- 'charLiteral' parser, which claims to handle all the single-character -- escapes defined by the Haskell grammar. ---stringLiteral :: Parser String+stringLiteral :: ParserV v String stringLiteral =   lexeme stringR <?> "string literal" -locStringLiteral :: Parser (Located String)+locStringLiteral :: ParserV v (Located String) locStringLiteral =   locLexeme stringR <?> "string literal" -stringR :: Parser String+stringR :: ParserV v String stringR =   char '\"' *> manyTill L.charLiteral (char '\"')  -- | Consumes a float literal lexeme.-double :: Parser Double+double :: ParserV v Double double = lexeme L.float <?> "float literal"  -- identifier :: Parser String@@ -649,15 +653,15 @@ -- This does not parse negative integers. Unary minus is available -- as an operator in the expression language. ---natural :: Parser Integer+natural :: ParserV v Integer natural =   lexeme naturalR <?> "nat literal" -locNatural :: Parser (Located Integer)+locNatural :: ParserV v (Located Integer) locNatural =   locLexeme naturalR <?> "nat literal" -naturalR :: Parser Integer+naturalR :: ParserV v Integer naturalR =       try (char '0' *> char' 'x') *> L.hexadecimal   <|> try (char '0' *> char' 'o') *> L.octal@@ -672,7 +676,7 @@ -- * a check for the entire identifier to be applied in the end, -- * an error message to display if the final check fails. ---condIdR :: Parser Char -> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol+condIdR :: ParserV v Char -> (Char -> Bool) -> (String -> Bool) -> String -> ParserV v Symbol condIdR initial okChars condition msg = do   s <- (:) <$> initial <*> takeWhileP Nothing okChars   if condition s@@ -685,7 +689,7 @@ -- -- See Note [symChars]. ---upperIdR :: Parser Symbol+upperIdR :: ParserV v Symbol upperIdR =   condIdR upperChar (`S.member` symChars) (const True) "unexpected" @@ -693,7 +697,7 @@ -- -- See Note [symChars]. ---lowerIdR :: Parser Symbol+lowerIdR :: ParserV v Symbol lowerIdR =   condIdR (lowerChar <|> char '_') (`S.member` symChars) isNotReserved "unexpected reserved word" @@ -701,7 +705,7 @@ -- -- See Note [symChars]. ---symbolR :: Parser Symbol+symbolR :: ParserV v Symbol symbolR =   condIdR (letterChar <|> char '_') (`S.member` symChars) isNotReserved "unexpected reserved word" @@ -728,13 +732,13 @@  -- | Lexeme version of 'upperIdR'. ---upperIdP :: Parser Symbol+upperIdP :: ParserV v Symbol upperIdP  =   lexeme upperIdR <?> "upperIdP"  -- | Lexeme version of 'lowerIdR'. ---lowerIdP :: Parser Symbol+lowerIdP :: ParserV v Symbol lowerIdP  =   lexeme lowerIdR <?> "lowerIdP" @@ -744,32 +748,47 @@ -- -- Lexeme version of 'symbolR'. ---symbolP :: Parser Symbol+symbolP :: ParserV v Symbol symbolP =   lexeme symbolR <?> "identifier"  -- The following are located versions of the lexeme identifier parsers. -locSymbolP, locLowerIdP, locUpperIdP :: Parser LocSymbol+locSymbolP, locLowerIdP, locUpperIdP :: ParserV v LocSymbol locLowerIdP = locLexeme lowerIdR locUpperIdP = locLexeme upperIdR locSymbolP  = locLexeme symbolR  -- | Parser for literal numeric constants: floats or integers without sign.-constantP :: Parser Constant+constantP :: ParserV v Constant constantP =      try (R <$> double)   -- float literal  <|> I <$> natural        -- nat literal  -- | Parser for literal string contants.-symconstP :: Parser SymConst+symconstP :: ParserV v SymConst symconstP = SL . T.pack <$> stringLiteral +-- | A class to parse symbols+--+-- liquid-fixpoint parses Symbol and LiquidHaskell instantiates this to+-- LocSymbol for more precise error messages. If liquid-fixpoint is adapted to+-- 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+  vFromString :: Located String -> v++instance ParseableV Symbol where+  parseV = symbolP+  mkSu = mkSubst+  vFromString = symbol+ -- | Parser for "atomic" expressions. -- -- This parser is reused by Liquid Haskell. ---expr0P :: Parser Expr+expr0P :: ParseableV v => ParserV v (ExprV v) expr0P   =  trueP -- constant "true"  <|> falseP -- constant "false"@@ -783,9 +802,9 @@  <|> try tupleP -- tuple expressions, starts with "("  <|> try (parens exprP) -- parenthesised expression, starts with "("  <|> try (parens exprCastP) -- explicit type annotation, starts with "(", TODO: should be an operator rather than require parentheses?- <|> EVar <$> symbolP -- identifier, starts with any letter or underscore- <|> try (brackets (pure ()) >> emptyListP) -- empty list, start with "["- <|> try (brackets exprP >>= singletonListP) -- singleton list, starts with "["+ <|> EVar <$> parseV  -- identifier, starts with any letter or underscore+ <|> try (located (brackets (pure ())) >>= emptyListP) -- empty list, start with "["+ <|> try (located (brackets exprP) >>= singletonListP) -- singleton list, starts with "["  --  -- Note:  --@@ -793,28 +812,28 @@  -- are prefixed with "try". This is because expr0P itself is chained with  -- additional parsers in funAppP ... -emptyListP :: Parser Expr-emptyListP = do+emptyListP :: Located () -> ParserV v (ExprV v)+emptyListP lx = do   e <- gets empList   case e of     Nothing -> fail "No parsing support for empty lists"-    Just s  -> return s+    Just s  -> return $ s lx -singletonListP :: Expr -> Parser Expr+singletonListP :: Located (ExprV v) -> ParserV v (ExprV v) singletonListP e = do   f <- gets singList   case f of     Nothing -> fail "No parsing support for singleton lists"-    Just s  -> return $ s e+    Just s  -> return $ s (void e) (val e)  -- | Parser for an explicitly type-annotated expression.-exprCastP :: Parser Expr+exprCastP :: ParseableV v => ParserV v (ExprV v) exprCastP   = do e  <- exprP        _ <- try dcolon <|> colon -- allow : or :: *and* allow following symbols        ECst e <$> sortP -fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a+fastIfP :: ParseableV v => (ExprV v -> a -> a -> a) -> ParserV v a -> ParserV v a fastIfP f bodyP   = do reserved "if"        p <- predP@@ -823,7 +842,7 @@        reserved "else"        f p b1 <$> bodyP -coerceP :: Parser Expr -> Parser Expr+coerceP :: ParserV v (ExprV v) -> ParserV v (ExprV v) coerceP p = do   reserved "coerce"   (s, t) <- parens (pairP sortP (reservedOp "~") sortP)@@ -846,13 +865,14 @@ -- -- Base parser used in 'exprP' which adds in other operators. ---expr1P :: Parser Expr+expr1P :: ParseableV v => ParserV v (ExprV v) expr1P   =  try funAppP  <|> expr0P  -- | Expressions-exprP :: Parser Expr++exprP :: ParseableV v => ParserV v (ExprV v) exprP =   do     table <- gets fixityTable@@ -860,26 +880,26 @@  data Assoc = AssocNone | AssocLeft | AssocRight -data Fixity-  = FInfix   {fpred :: Maybe Int, fname :: String, fop2 :: Maybe (Expr -> Expr -> Expr), fassoc :: Assoc}-  | FPrefix  {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}-  | FPostfix {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}+data Fixity v+  = FInfix   {fpred :: Maybe Int, fname :: String, fop2 :: Maybe (Located String -> ExprV v -> ExprV v -> ExprV v), fassoc :: Assoc}+  | FPrefix  {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Located String -> ExprV v -> ExprV v)}+  | FPostfix {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Located String -> ExprV v -> ExprV v)}   -- | An OpTable stores operators by their fixity. -- -- Fixity levels range from 9 (highest) to 0 (lowest).-type OpTable = IM.IntMap [Operator Parser Expr] -- [[Operator Parser Expr]]+type OpTable v = IM.IntMap [Operator (ParserV v) (ExprV v)] -- [[Operator Parser Expr]]  -- | Transform an operator table to the form expected by 'makeExprParser', -- which wants operators sorted by decreasing priority. ---flattenOpTable :: OpTable -> [[Operator Parser Expr]]+flattenOpTable :: OpTable v -> [[Operator (ParserV v) (ExprV v)]] flattenOpTable =   (snd <$>) <$> IM.toDescList  -- | Add an operator to the parsing state.-addOperatorP :: Fixity -> Parser ()+addOperatorP :: ParseableV v => Fixity v -> ParserV v () addOperatorP op   = modify $ \s -> s{ fixityTable = addOperator op (fixityTable s)                     , fixityOps   = op:fixityOps s@@ -899,7 +919,7 @@     resX x = reserved x >> return (symbol x)  -- | Located version of 'infixSymbolP'.-locInfixSymbolP :: Parser (Located Symbol)+locInfixSymbolP :: ParserV v (Located Symbol) locInfixSymbolP = do   ops <- gets infixOps   choice (resX <$> ops)@@ -913,14 +933,17 @@ mkInfix AssocRight = InfixR mkInfix AssocNone  = InfixN +locReservedOp :: String -> ParserV v (Located String)+locReservedOp s = (s <$) <$> located (reservedOp s)+ -- | Add the given operator to the operator table.-addOperator :: Fixity -> OpTable -> OpTable+addOperator :: ParseableV v => Fixity v -> OpTable v -> OpTable v addOperator (FInfix p x f assoc) ops- = insertOperator (makePrec p) (mkInfix assoc (reservedOp x >> return (makeInfixFun x f))) ops+ = insertOperator (makePrec p) (mkInfix assoc (makeInfixFun f <$> locReservedOp x)) ops addOperator (FPrefix p x f) ops- = insertOperator (makePrec p) (Prefix (reservedOp x >> return (makePrefixFun x f))) ops+ = insertOperator (makePrec p) (Prefix (makePrefixFun f <$> locReservedOp x)) ops addOperator (FPostfix p x f) ops- = insertOperator (makePrec p) (Postfix (reservedOp x >> return (makePrefixFun x f))) ops+ = insertOperator (makePrec p) (Postfix (makePrefixFun f <$> locReservedOp x)) ops  -- | Helper function for computing the priority of an operator. --@@ -929,32 +952,32 @@ makePrec :: Maybe Int -> Int makePrec = fromMaybe 9 -makeInfixFun :: String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr-makeInfixFun x = fromMaybe (\e1 e2 -> EApp (EApp (EVar $ symbol x) e1) e2)+makeInfixFun :: ParseableV v => Maybe (Located String -> ExprV v -> ExprV v -> ExprV v) -> Located String -> ExprV v -> ExprV v -> ExprV v+makeInfixFun = fromMaybe (\lx e1 e2 -> EApp (EApp (EVar $ vFromString lx) e1) e2) -makePrefixFun :: String -> Maybe (Expr -> Expr) -> Expr -> Expr-makePrefixFun x = fromMaybe (EApp (EVar $ symbol x))+makePrefixFun :: ParseableV v => Maybe (Located String -> ExprV v -> ExprV v) -> Located String -> ExprV v -> ExprV v+makePrefixFun = fromMaybe (EApp . EVar . vFromString)  -- | Add an operator at the given priority to the operator table.-insertOperator :: Int -> Operator Parser Expr -> OpTable -> OpTable+insertOperator :: Int -> Operator (ParserV v) (ExprV v) -> OpTable v -> OpTable v insertOperator i op = IM.alter (Just . (op :) . fromMaybe []) i  -- | The initial (empty) operator table.-initOpTable :: OpTable+initOpTable :: OpTable v initOpTable = IM.empty  -- | Built-in operator table, parameterised over the composition function.-bops :: Maybe Expr -> OpTable+bops :: forall v. ParseableV v => Maybe (Located String -> ExprV v) -> OpTable v bops cmpFun = foldl' (flip addOperator) initOpTable builtinOps   where     -- Built-in Haskell operators, see https://www.haskell.org/onlinereport/decls.html#fixity-    builtinOps :: [Fixity]-    builtinOps = [ FPrefix (Just 9) "-"   (Just ENeg)-                 , FInfix  (Just 7) "*"   (Just $ EBin Times) AssocLeft-                 , FInfix  (Just 7) "/"   (Just $ EBin Div)   AssocLeft-                 , FInfix  (Just 6) "-"   (Just $ EBin Minus) AssocLeft-                 , FInfix  (Just 6) "+"   (Just $ EBin Plus)  AssocLeft-                 , FInfix  (Just 5) "mod" (Just $ EBin Mod)   AssocLeft -- Haskell gives mod 7+    builtinOps :: [Fixity v]+    builtinOps = [ FPrefix (Just 9) "-"   (Just $ const ENeg)+                 , FInfix  (Just 7) "*"   (Just $ const $ EBin Times) AssocLeft+                 , FInfix  (Just 7) "/"   (Just $ const $ EBin Div)   AssocLeft+                 , FInfix  (Just 6) "-"   (Just $ const $ EBin Minus) AssocLeft+                 , FInfix  (Just 6) "+"   (Just $ const $ EBin Plus)  AssocLeft+                 , FInfix  (Just 5) "mod" (Just $ const $ EBin Mod)   AssocLeft -- Haskell gives mod 7                  , FInfix  (Just 9) "."   applyCompose        AssocRight                 --  --                 --  , FInfix  (Just 4) "<"   (Just $ PAtom Lt)  AssocNone@@ -969,41 +992,42 @@                 --  , FInfix  (Just 4) ">"   (Just $ PAtom Gt)  AssocNone                 --  , FInfix  (Just 4) ">="  (Just $ PAtom Ge)  AssocNone                  ]-    applyCompose :: Maybe (Expr -> Expr -> Expr)-    applyCompose = (\f x y -> f `eApps` [x,y]) <$> cmpFun+    applyCompose :: Maybe (Located String -> ExprV v -> ExprV v -> ExprV v)+    applyCompose = (\f lop x y -> f lop `eApps` [x,y]) <$> cmpFun  -- | Parser for function applications. -- -- Andres, TODO: Why is this so complicated? ---funAppP :: Parser Expr+funAppP :: ParseableV v => ParserV v (ExprV v) funAppP      =  litP <|> exprFunP <|> simpleAppP   where-    exprFunP = mkEApp <$> funSymbolP <*> funRhsP+    exprFunP = eApps <$> funSymbolP <*> funRhsP     funRhsP  =  some expr0P             <|> parens innerP     innerP   = brackets (sepBy exprP semi)      -- TODO:AZ the parens here should be superfluous, but it hits an infinite loop if removed     simpleAppP     = EApp <$> parens exprP <*> parens exprP-    funSymbolP     = locSymbolP+    funSymbolP     = EVar <$> parseV  -- | Parser for tuple expressions (two or more components).-tupleP :: Parser Expr+tupleP :: ParseableV v => ParserV v (ExprV v) tupleP = do-  Loc l1 l2 (first, rest) <- locParens ((,) <$> exprP <* comma <*> sepBy1 exprP comma) -- at least two components necessary-  let cons = symbol $ "(" ++ replicate (length rest) ',' ++ ")" -- stored in prefix form-  return $ mkEApp (Loc l1 l2 cons) (first : rest)+  lp <- located $ parens ((,) <$> exprP <* comma <*> sepBy1 exprP comma) -- at least two components necessary+  let (first, rest) = val lp+      cons = vFromString $ ("(" ++ replicate (length rest) ',' ++ ")") <$ lp -- stored in prefix form+  return $ eApps (EVar cons) (first : rest)   -- | Parser for literals of all sorts.-litP :: Parser Expr+litP :: ParserV v (ExprV v) litP = do reserved "lit"           l <- stringLiteral           ECon . L (T.pack l) <$> sortP  -- | Parser for lambda abstractions.-lamP :: Parser Expr+lamP :: ParseableV v => ParserV v (ExprV v) lamP   = do reservedOp "\\"        x <- symbolP@@ -1012,22 +1036,22 @@        reservedOp "->"        ELam (x, t) <$> exprP -varSortP :: Parser Sort+varSortP :: ParserV v Sort varSortP  = FVar  <$> parens intP  -- | Parser for function sorts without the "func" keyword.-funcSortP :: Parser Sort+funcSortP :: ParserV v Sort funcSortP = parens $ mkFFunc <$> intP <* comma <*> sortsP -sortsP :: Parser [Sort]+sortsP :: ParserV v [Sort] sortsP = try (brackets (sepBy sortP semi))       <|> brackets (sepBy sortP comma)  -- | Parser for sorts (types).-sortP    :: Parser Sort+sortP    :: ParserV v Sort sortP    = sortP' (many sortArgP) -sortArgP :: Parser Sort+sortArgP :: ParserV v Sort sortArgP = sortP' (return [])  {-@@ -1041,7 +1065,7 @@ -- -- TODO, Andres: document the parameter better. ---sortP' :: Parser [Sort] -> Parser Sort+sortP' :: ParserV v [Sort] -> ParserV v Sort sortP' appArgsP    =  parens sortP -- parenthesised sort, starts with "("   <|> (reserved "func" >> funcSortP) -- function sort, starts with "func"@@ -1049,13 +1073,13 @@   <|> (fAppTC <$> fTyConP <*> appArgsP)   <|> (fApp   <$> tvarP   <*> appArgsP) -tvarP :: Parser Sort+tvarP :: ParserV v Sort tvarP    =  (string "@" >> varSortP)   <|> (FObj . symbol <$> lowerIdP)  -fTyConP :: Parser FTycon+fTyConP :: ParserV v FTycon fTyConP   =   (reserved "int"     >> return intFTyCon)   <|> (reserved "Integer" >> return intFTyCon)@@ -1066,7 +1090,7 @@   <|> (reserved "Str"     >> return strFTyCon)   <|> (mkFTycon          =<<  locUpperIdP) -mkFTycon :: LocSymbol -> Parser FTycon+mkFTycon :: LocSymbol -> ParserV v FTycon mkFTycon locSymbol = do   nums  <- gets numTyCons   return (symbolNumInfoFTyCon locSymbol (val locSymbol `S.member` nums) False)@@ -1080,7 +1104,7 @@ -- -- This parser is reused by Liquid Haskell. ---pred0P :: Parser Expr+pred0P :: ParseableV v => ParserV v (ExprV v) pred0P =  trueP -- constant "true"       <|> falseP -- constant "false"       <|> (reservedOp "??" >> makeUniquePGrad)@@ -1090,33 +1114,33 @@       <|> parens predP -- parenthesised predicate, starts with "("       <|> (reservedOp "?" *> exprP)       <|> try funAppP-      <|> EVar <$> symbolP -- identifier, starts with any letter or underscore+      <|> EVar <$> parseV -- identifier, starts with any letter or underscore       <|> (reservedOp "&&" >> pGAnds <$> predsP) -- built-in prefix and       <|> (reservedOp "||" >> POr  <$> predsP) -- built-in prefix or -makeUniquePGrad :: Parser Expr+makeUniquePGrad :: ParserV v (ExprV v) makeUniquePGrad   = do uniquePos <- getSourcePos-       return $ PGrad (KV $ symbol $ show uniquePos) mempty (srcGradInfo uniquePos) mempty+       return $ PGrad (KV $ symbol $ show uniquePos) (Su mempty) (srcGradInfo uniquePos) PTrue  -- qmP    = reserved "?" <|> reserved "Bexp"  -- | Parser for the reserved constant "true".-trueP :: Parser Expr+trueP :: ParserV v (ExprV v) trueP  = reserved "true"  >> return PTrue  -- | Parser for the reserved constant "false".-falseP :: Parser Expr+falseP :: ParserV v (ExprV v) falseP = reserved "false" >> return PFalse -kvarPredP :: Parser Expr+kvarPredP :: ParseableV v => ParserV v (ExprV v) kvarPredP = PKVar <$> kvarP <*> substP -kvarP :: Parser KVar+kvarP :: ParserV v KVar kvarP = KV <$> lexeme (char '$' *> symbolR) -substP :: Parser Subst-substP = mkSubst <$> many (brackets $ pairP symbolP aP exprP)+substP :: ParseableV v => ParserV v (SubstV v)+substP = mkSu <$> many (brackets $ pairP symbolP aP exprP)   where     aP = reservedOp ":=" @@ -1125,14 +1149,14 @@ -- Used as the argument of the prefix-versions of conjunction and -- disjunction. ---predsP :: Parser [Expr]+predsP :: ParseableV v => ParserV v [ExprV v] predsP = brackets $ sepBy predP semi  -- | Parses a predicate. -- -- Unlike for expressions, there is a built-in operator list. ---predP  :: Parser Expr+predP  :: ParseableV v => ParserV v (ExprV v) predP  = makeExprParser pred0P lops   where     lops = [ [Prefix (reservedOp "~"    >> return PNot)]@@ -1147,14 +1171,14 @@            , [InfixR (reservedOp "/="   >> return pNotIff)]            ] -pNotIff :: Expr -> Expr -> Expr+pNotIff :: ExprV v -> ExprV v -> ExprV v pNotIff x y = PNot (PIff x y)  -- | Parses a relation predicate. -- -- Binary relations connect expressions and predicates. ---predrP :: Parser Expr+predrP :: ParseableV v => ParserV v (ExprV v) predrP =   (\ e1 r e2 -> r e1 e2) <$> exprP <*> brelP <*> exprP @@ -1162,7 +1186,7 @@ -- -- There is a built-in table of available relations. ---brelP ::  Parser (Expr -> Expr -> Expr)+brelP ::  ParserV v (ExprV v -> ExprV v -> ExprV v) brelP =  (reservedOp "==" >> return (PAtom Eq))      <|> (reservedOp "="  >> return (PAtom Eq))      <|> (reservedOp "~~" >> return (PAtom Ueq))@@ -1179,7 +1203,7 @@ --------------------------------------------------------------------------------  -- | Refa-refaP :: Parser Expr+refaP :: ParseableV v => ParserV v (ExprV v) refaP =  try (pAnd <$> brackets (sepBy predP semi))      <|> predP @@ -1197,7 +1221,7 @@  -- bindP      = symbol    <$> (lowerIdP <* colon) -- | Binder (lowerIdP <* colon)-bindP :: Parser Symbol+bindP :: ParserV v Symbol bindP = symbolP <* colon  optBindP :: Symbol -> Parser Symbol@@ -1231,7 +1255,7 @@ --------------------------------------------------------------------------------  -- | Qualifiers-qualifierP :: Parser Sort -> Parser Qualifier+qualifierP :: ParseableV v => ParserV v Sort -> ParserV v (QualifierV v) qualifierP tP = do   pos    <- getSourcePos   n      <- upperIdP@@ -1240,32 +1264,32 @@   body   <- predP   return  $ mkQual n params body pos -qualParamP :: Parser Sort -> Parser QualParam+qualParamP :: ParserV v Sort -> ParserV v QualParam qualParamP tP = do   x     <- symbolP   pat   <- qualPatP   _     <- colon   QP x pat <$> tP -qualPatP :: Parser QualPattern+qualPatP :: ParserV v QualPattern qualPatP    =  (reserved "as" >> qualStrPatP)   <|> return PatNone -qualStrPatP :: Parser QualPattern+qualStrPatP :: ParserV v QualPattern qualStrPatP    = (PatExact <$> symbolP)   <|> parens (    (uncurry PatPrefix <$> pairP symbolP dot qpVarP)               <|> (uncurry PatSuffix <$> pairP qpVarP  dot symbolP) )  -qpVarP :: Parser Int+qpVarP :: ParserV v Int qpVarP = char '$' *> intP  symBindP :: Parser a -> Parser (Symbol, a) symBindP = pairP symbolP colon -pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)+pairP :: ParserV v a -> ParserV v z -> ParserV v b -> ParserV v (a, b) pairP xP sepP yP = (,) <$> xP <* sepP <*> yP  ---------------------------------------------------------------------@@ -1293,6 +1317,19 @@                )   return  $ mkEquation name params body sort +defineLocalP :: Parser (Int, [(Symbol, Expr)])+defineLocalP = do+  bid <- intP+  rews <- brackets $ sepBy rewriteP $ reserved ";"+  pure (bid, rews)++rewriteP :: Parser (Symbol, Expr)+rewriteP = do+        x <- symbolP+        reserved ":="+        e <- exprP+        return (x, e)+ matchP :: Parser Rewrite matchP = SMeasure <$> symbolP <*> symbolP <*> many symbolP <*> (reserved "=" >> exprP) @@ -1316,6 +1353,7 @@   | EBind !Int !Symbol !Sort !a   | Opt !String   | Def !Equation+  | LDef !(Int, [(Symbol, Expr)])   | Mat !Rewrite   | Expand ![(Int,Bool)]   | Adt  !DataDecl@@ -1345,6 +1383,7 @@     <|> IBind <$> (reserved "bind"         >> intP) <*> symbolP <*> (colon >> sortedReftP)  <*> pure ()     <|> Opt    <$> (reserved "fixpoint"    >> stringLiteral)     <|> Def    <$> (reserved "define"      >> defineP)+    <|> LDef   <$> (reserved "defineLocal" >> defineLocalP)     <|> Mat    <$> (reserved "match"       >> matchP)     <|> Expand <$> (reserved "expand"      >> pairsP intP boolP)     <|> Adt    <$> (reserved "data"        >> dataDeclP)@@ -1402,7 +1441,7 @@ envP  = do binds <- brackets $ sepBy (intP <* spaces) semi            return $ insertsIBindEnv binds emptyIBindEnv -intP :: Parser Int+intP :: ParserV v Int intP = fromInteger <$> natural  boolP :: Parser Bool@@ -1410,7 +1449,7 @@     <|> (reserved "False" >> return False)  defsFInfo :: [Def a] -> FInfo a-defsFInfo defs = {- SCC "defsFI" -} Types.FI cm ws bs ebs lts dts kts qs binfo adts mempty mempty ae+defsFInfo defs = {- SCC "defsFI" -} Types.FI cm ws bs ebs lts dts kts qs binfo adts mempty mempty ae lrws   where     cm         = Misc.safeFromList                    "defs-cm"        [(cid c, c)         | Cst c       <- defs]@@ -1418,7 +1457,7 @@                    "defs-ws"        [(i, w)              | Wfc w    <- defs, let i = Misc.thd3 (wrft w)]     bs         = bindEnvFromList  $ exBinds ++ [(n,(x,r,a)) | IBind n x r a <- defs]     ebs        =                    [ n                  | (n,_) <- exBinds]-    exBinds    =                    [(n, (x, RR t mempty, a)) | EBind n x t a <- defs]+    exBinds    =                    [(n, (x, RR t trueReft, a)) | EBind n x t a <- defs]     lts        = fromListSEnv       [(x, t)             | Con x t     <- defs]     dts        = fromListSEnv       [(x, t)             | Dis x t     <- defs]     kts        = KS $ S.fromList    [k                  | Kut k       <- defs]@@ -1439,6 +1478,7 @@                          map'     cid        = fromJust . sid     ae         = AEnv eqs rews expand rwMap+    lrws       = LocalRewritesMap $ M.fromList [ (bid, LocalRewrites $ M.fromList rws) | LDef (bid, rws) <- defs ]     adts       =                    [d                  | Adt d       <- defs]     -- msg    = show $ "#Lits = " ++ (show $ length consts) @@ -1493,7 +1533,13 @@        return (res, str, pos)  -- | Initial parser state.-initPState :: Maybe Expr -> PState+initPState+  :: ParseableV v+  -- The expression to produce when the composition operator is parsed (@f . g@)+  --+  -- Receives the location of the composition operator.+  => Maybe (Located String -> ExprV v)+  -> PStateV v initPState cmpFun = PState { fixityTable = bops cmpFun                            , empList     = Nothing                            , singList    = Nothing@@ -1537,7 +1583,7 @@ parseFromStdIn p = doParse' p "stdin" . T.unpack <$> T.getContents  -- | Obtain a fresh integer during the parsing process.-freshIntP :: Parser Integer+freshIntP :: ParserV v Integer freshIntP = do n <- gets supply                modify (\ s -> s{supply = n + 1})                return n

@@ -59,12 +59,8 @@      ) where -import           Language.Fixpoint.Types.Config ( SMTSolver (..)-                                                , Config-                                                , solver-                                                , smtTimeout-                                                , gradual-                                                , stringTheory)+import           Language.Fixpoint.Types.Config ( SMTSolver (..), solverFlags+                                                , Config (solver, smtTimeout, gradual, stringTheory, save)) import qualified Language.Fixpoint.Misc          as Misc import           Language.Fixpoint.Types.Errors import           Language.Fixpoint.Utils.Files@@ -160,7 +156,7 @@ {-# SCC command #-} command              :: Context -> Command -> IO Response ---------------------------------------------------------------------------------command Ctx {..} !cmd       = do+command Ctx{..} !cmd       = do   -- whenLoud $ do LTIO.appendFile debugFile (s <> "\n")   --               LTIO.putStrLn ("CMD-RAW:" <> s <> ":CMD-RAW:DONE")   forM_ ctxLog $ \h -> do@@ -240,12 +236,18 @@ makeContext :: Config -> FilePath -> IO Context -------------------------------------------------------------------------- makeContext cfg f-  = do createDirectoryIfMissing True $ takeDirectory smtFile-       hLog <- openFile smtFile WriteMode-       hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64-       me   <- makeContext' cfg $ Just hLog+  = do mb_hLog <- if not (save cfg) then pure Nothing else do+           createDirectoryIfMissing True $ takeDirectory smtFile+           hLog <- openFile smtFile WriteMode+           hSetBuffering hLog $ BlockBuffering $ Just $ 1024 * 1024 * 64+           return $ Just hLog+       me   <- makeContext' cfg mb_hLog        pre  <- smtPreamble cfg (solver cfg) me-       mapM_ (\l -> SMTLIB.Backends.command_ (ctxSolver me) l >> BS.hPutBuilder hLog l >> LBS.hPutStr hLog "\n") pre+       forM_ pre $ \line -> do+           SMTLIB.Backends.command_ (ctxSolver me) line+           forM_ mb_hLog $ \hLog -> do+               BS.hPutBuilder hLog line+               LBS.hPutStr hLog "\n"        return me     where        smtFile = extFileName Smt2 f@@ -284,7 +286,8 @@  makeContext' :: Config -> Maybe Handle -> IO Context makeContext' cfg ctxLog-  = do (backend, closeIO) <- case solver cfg of+  = do let slv = solver cfg+       (backend, closeIO) <- case slv of          Z3      ->            {- "z3 -smt2 -in"                   -}            {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -}@@ -300,13 +303,18 @@                       Process.defaultConfig                              { Process.exe = "cvc4"                              , Process.args = ["--incremental", "-L", "smtlib2"] }+         Cvc5    -> makeProcess ctxLog $+                      Process.defaultConfig+                             { Process.exe = "cvc5"+                             , Process.args = ["--incremental", "-L", "smtlib2"] }        solver <- SMTLIB.Backends.initSolver SMTLIB.Backends.Queuing backend        loud <- isLoud-       return Ctx { ctxSolver  = solver-                  , ctxClose   = closeIO-                  , ctxLog     = ctxLog-                  , ctxVerbose = loud-                  , ctxSymEnv  = mempty+       return Ctx { ctxSolver    = solver+                  , ctxElabF     = solverFlags slv+                  , ctxClose     = closeIO+                  , ctxLog       = ctxLog+                  , ctxVerbose   = loud+                  , ctxSymEnv    = mempty                   }  -- | Close file handles and release the solver backend's resources.@@ -394,7 +402,7 @@    ans _   = False  smtAssert :: Context -> Expr -> IO ()-smtAssert me p  = interact' me (Assert Nothing p)+smtAssert me p = interact' me (Assert Nothing p)  smtDefineFunc :: Context -> Symbol -> [(Symbol, F.Sort)] -> F.Sort -> Expr -> IO () smtDefineFunc me name symList rsort e =@@ -472,10 +480,10 @@     ess        = distinctLiterals  lts     axs        = Thy.axiomLiterals lts     thyXTs     =                    filter (isKind 1) xts-    qryXTs     = Misc.mapSnd tx <$> filter (isKind 2) xts+    qryXTs     = fmap tx <$> filter (isKind 2) xts     isKind n   = (n ==)  . symKind env . fst     xts        = {- tracepp "symbolSorts" $ -} symbolSorts (F.seSort env)-    tx         = elaborate    "declare" env+    tx         = elaborate (ElabParam (ctxElabF me) "declare" env)     ats        = funcSortVars env  symbolSorts :: F.SEnv F.Sort -> [(F.Symbol, F.Sort)]

@@ -42,8 +42,8 @@  smt2data' :: SymEnv -> [DataDecl] -> Builder smt2data' env ds = seqs [ parens $ smt2many (smt2dataname env <$> ds)-                         , parens $ smt2many (smt2datactors env <$> ds)-                         ]+                        , parens $ smt2many (smt2datactors env <$> ds)+                        ]   smt2dataname :: SymEnv -> DataDecl -> Builder@@ -54,18 +54,17 @@   smt2datactors :: SymEnv -> DataDecl -> Builder-smt2datactors env (DDecl _ as cs) = parenSeqs ["par", parens tvars, parens ds]+smt2datactors env (DDecl _ as cs)+  | as > 0       = parenSeqs ["par", parens tvars, parens ds]+  | otherwise    =                                 parens ds   where     tvars        = smt2many (smt2TV <$> [0..(as-1)])     smt2TV       = smt2 env . SVar     ds           = smt2many (smt2ctor env as <$> cs)  smt2ctor :: SymEnv -> Int -> DataCtor -> Builder-smt2ctor env _  (DCtor c [])  = smt2 env c-smt2ctor env as (DCtor c fs)  = parenSeqs [smt2 env c, fields] -  where-    fields                 = smt2many (smt2field env as <$> fs)+smt2ctor env as (DCtor c fs)  = parenSeqs (smt2 env c : (smt2field env as <$> fs))  smt2field :: SymEnv -> Int -> DataField -> Builder smt2field env as d@(DField x t) = parenSeqs [smt2 env x, smt2SortPoly d env $ mkPoly as t]@@ -148,7 +147,7 @@   smt2 env (PAnd ps)        = parenSeqs ["and", smt2s env ps]   smt2 _   (POr [])         = "false"   smt2 env (POr ps)         = parenSeqs ["or", smt2s env ps]-  smt2 env (PNot p)         = parenSeqs ["not", smt2  env p]+  smt2 env (PNot p)         = parenSeqs ["not", smt2 env p]   smt2 env (PImp p q)       = parenSeqs ["=>", smt2 env p, smt2 env q]   smt2 env (PIff p q)       = parenSeqs ["=", smt2 env p, smt2 env q]   smt2 env (PExist [] p)    = smt2 env p@@ -156,7 +155,7 @@   smt2 env (PAll   [] p)    = smt2 env p   smt2 env (PAll   xs p)    = parenSeqs ["forall", parens (smt2s env xs), smt2 env p]   smt2 env (PAtom r e1 e2)  = mkRel env r e1 e2-  smt2 env (ELam b e)       = smt2Lam   env b e+  smt2 env (ELam b e)       = smt2Lam env b e   smt2 env (ECoerc t1 t2 e) = smt2Coerc env t1 t2 e   smt2 _   e                = panic ("smtlib2 Pred  " ++ show e) @@ -183,10 +182,10 @@ smt2VarAs env x t = parenSeqs ["as", smt2 env x, smt2SortMono x env t]  smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder-smt2Lam env (x, xT) (ECst e eT) = parenSeqs [Builder.fromText lambda, x', smt2 env e]+smt2Lam env (x, xT) full@(ECst _ eT) = parenSeqs [Builder.fromText lambda, x', smt2 env full]   where-    x'                          = smtLamArg env x xT-    lambda                      = symbolAtName lambdaName env () (FFunc xT eT)+    x'     = smtLamArg env x xT+    lambda = symbolAtName lambdaName env () (FFunc xT eT)  smt2Lam _ _ e   = panic ("smtlib2: Cannot serialize unsorted lambda: " ++ showpp e)

@@ -7,6 +7,7 @@ {-# LANGUAGE ViewPatterns              #-}  {-# OPTIONS_GHC -Wno-orphans           #-}+{-# LANGUAGE TupleSections #-}  module Language.Fixpoint.Smt.Theories      (@@ -29,15 +30,24 @@      , theorySymbols      , dataDeclSymbols -        -- * Theories-     , setEmpty, setEmp, setCap, setSub, setAdd, setMem-     , setCom, setCup, setDif, setSng+     , setEmpty, setEmp, setSng, setAdd, setMem+     , setCom, setCap, setCup, setDif, setSub -     , mapSel, mapCup, mapSto, mapDef+     , mapDef, mapSel, mapSto -     , arrConst, arrStore, arrSelect, arrMapNot, arrMapOr, arrMapAnd, arrMapImp+     , bagEmpty, bagSng, bagCount, bagSub, bagCup, bagMax, bagMin +     -- * Z3 theory array encodings++     , arrConstM, arrStoreM, arrSelectM++     , arrConstS, arrStoreS, arrSelectS+     , arrMapNotS, arrMapOrS, arrMapAndS, arrMapImpS++     , arrConstB, arrStoreB, arrSelectB+     , arrMapPlusB, arrMapLeB, arrMapGtB, arrMapIteB+       -- * Query Theories      , isSmt2App      , axiomLiterals@@ -55,6 +65,7 @@ -- import           Data.Text.Format import qualified Data.Text import           Data.String                 (IsString(..))+import Text.Printf (printf) import Language.Fixpoint.Utils.Builder  {- | [NOTE:Adding-Theories] To add new (SMTLIB supported) theories to@@ -67,27 +78,6 @@ -- | Theory Symbols ------------------------------------------------------------ -------------------------------------------------------------------------------- --- TODO drop all of Set and Map symbols when Map is handled through arrays---- "set" is currently \"LSet\" instead of just \"Set\" because Z3 has its own--- \"Set\" since 4.8.5-elt, set, map :: Raw-elt  = "Elt"-set  = "LSet"-map  = "Map"--sel, sto, mcup, mdef, mprj :: Raw-mToSet, mshift, mmax, mmin :: Raw-sel   = "smt_map_sel"-sto   = "smt_map_sto"-mcup  = "smt_map_cup"-mmax  = "smt_map_max"-mmin  = "smt_map_min"-mdef  = "smt_map_def"-mprj  = "smt_map_prj"-mshift = "smt_map_shift"-mToSet = "smt_map_to_set"- ---- Size changes bvConcatName, bvExtractName, bvRepeatName, bvZeroExtName, bvSignExtName :: Symbol bvConcatName   = "concat"@@ -143,7 +133,12 @@ bvSGtName  = "bvsgt" bvSGeName  = "bvsge" -setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a -- Symbol+mapDef, mapSel, mapSto :: (IsString a) => a+mapDef   = "Map_default"+mapSel   = "Map_select"+mapSto   = "Map_store"++setEmpty, setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: (IsString a) => a setEmpty = "Set_empty" setEmp   = "Set_emp" setCap   = "Set_cap"@@ -155,71 +150,59 @@ setDif   = "Set_dif" setSng   = "Set_sng" ---- Array operations-arrConst, arrStore, arrSelect, arrMapNot, arrMapOr, arrMapAnd, arrMapImp :: Symbol-arrConst  = "const"-arrStore  = "store"-arrSelect = "select"-arrMapNot = "arr_map_not"-arrMapOr  = "arr_map_or"-arrMapAnd = "arr_map_and"-arrMapImp = "arr_map_imp"--mapSel, mapSto, mapCup, mapDef, mapMax, mapMin, mapShift :: Symbol-mapSel   = "Map_select"-mapSto   = "Map_store"-mapCup   = "Map_union"-mapMax   = "Map_union_max"-mapMin   = "Map_union_min"-mapDef   = "Map_default"-mapShift = "Map_shift" -- See [Map key shift]+bagEmpty, bagSng, bagCount, bagSub, bagCup, bagMax, bagMin :: (IsString a) => a+bagEmpty = "Bag_empty"+bagSng   = "Bag_sng"+bagCount = "Bag_count"+bagSub   = "Bag_sub"+bagCup   = "Bag_union"+bagMax   = "Bag_union_max" -- See [Bag max and min]+bagMin   = "Bag_inter_min" --- [Map key shift]--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~--- Function mapShift: Add an integer to all keys in a map. Type signature:---   mapShift : Int -> Map Int v -> Map Int v--- Let's call the first argument (the shift amount) N, the second argument K1,--- and the result K2. For all indices i, we have K2[i] = K1[i - N].--- This is implemented with Z3's lambda, which lets us construct an array--- from a function.------ [Map max and min]+-- [Bag max and min] -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~--- Functions mapMax and mapMin: Union two maps, combining the elements by--- taking either the greatest (mapMax) or the least (mapMin) of them.---   mapMax, mapMin : Map v Int -> Map v Int -> Map v Int+-- Functions bagMax and bagMin: Union/intersect two bags, combining the elements by+-- taking either the greatest (bagMax) or the least (bagMin) of them.+--   bagMax, bagMin : Map v Int -> Map v Int -> Map v Int -mapToSet, mapPrj :: Symbol-mapToSet = "Map_to_set"-mapPrj   = "Map_project"+--- Array operations for polymorphic maps+arrConstM, arrStoreM, arrSelectM :: Symbol+arrConstM  = "arr_const_m"+arrStoreM  = "arr_store_m"+arrSelectM = "arr_select_m" --- [Interaction between Map and Set]--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~--- Function mapToSet: Convert a map to a set. The map's key may be of--- any type and is preserved as the set's element type. More precisely:---   mapToSet : Map k Int -> Set k--- The element type must be Int. All non-positive elements are mapped--- to False, and all positive elements are mapped to True. In practice,--- negative elements should not exist because Map is intended to be used--- as a bag, so the element is a non-negative number representing--- the occurrences of its corresponding key.------ Function mapPrj: Project a subset of a map. Type signature:---   mapPrj : Set k -> Map k Int -> Map k Int--- If the key is present in both the argument set and the argument map,--- then the key (along with its associated value in the map) are preserved--- in the output. Keys not present in the set are mapped to zero. Keys not--- present in the set are mapped to zero.+--- Array operations for sets (Z3)+arrConstS, arrStoreS, arrSelectS, arrMapNotS, arrMapOrS, arrMapAndS, arrMapImpS :: Symbol+arrConstS  = "arr_const_s"+arrStoreS  = "arr_store_s"+arrSelectS = "arr_select_s" +arrMapNotS = "arr_map_not"+arrMapOrS  = "arr_map_or"+arrMapAndS = "arr_map_and"+arrMapImpS = "arr_map_imp"++--- Array operations for bags (Z3)+arrConstB, arrStoreB, arrSelectB :: Symbol+arrConstB  = "arr_const_b"+arrStoreB  = "arr_store_b"+arrSelectB = "arr_select_b"++arrMapPlusB, arrMapLeB, arrMapGtB, arrMapIteB :: Symbol+arrMapPlusB = "arr_map_plus"+arrMapLeB   = "arr_map_le"+arrMapGtB   = "arr_map_gt"+arrMapIteB   = "arr_map_ite"+ strLen, strSubstr, strConcat :: (IsString a) => a -- Symbol strLen    = "strLen" strSubstr = "subString" strConcat = "concatString" -z3strlen, z3strsubstr, z3strconcat :: Raw-z3strlen    = "str.len"-z3strsubstr = "str.substr"-z3strconcat = "str.++"+smtlibStrLen, smtlibStrSubstr, smtlibStrConcat :: Raw+smtlibStrLen    = "str.len"+smtlibStrSubstr = "str.substr"+smtlibStrConcat = "str.++"  strLenSort, substrSort, concatstrSort :: Sort strLenSort    = FFunc strSort intSort@@ -242,132 +225,65 @@ bSort :: Raw -> Builder -> Builder bSort name def = key "define-sort" (fromText name <+> "()" <+> def) -z3Preamble :: Config -> [Builder]-z3Preamble u-  = stringPreamble u ++-    [ bSort elt-        "Int"-    , bSort set-        (key2 "Array" (fromText elt) "Bool") -    -- Maps-    , bSort map-        (key2 "Array" (fromText elt) (fromText elt))-    , bFun sel-        [("m", fromText map), ("k", fromText elt)]-        (fromText elt)-        "(select m k)"-    , bFun sto-        [("m", fromText map), ("k", fromText elt), ("v", fromText elt)]-        (fromText map)-        "(store m k v)"-    , bFun mcup-        [("m1", fromText map), ("m2", fromText map)]-        (fromText map)-        (key2 (key "_ map" (key2 "+" (parens (fromText elt <+> fromText elt)) (fromText elt))) "m1" "m2")-    , bFun mprj -- See [Interaction Between Map and Set]-        [("s", fromText set), ("m", fromText map)]-        (fromText map)-        (key3-          (key "_ map"-            (key2 "ite"-              (parens ("Bool" <+> fromText elt <+> fromText elt))-              (fromText elt)-            )-          )-          "s"-          "m"-          (parens (key "as const" (key2 "Array" (fromText elt) (fromText elt)) <+> "0"))-        )-    , bFun mToSet -- See [Interaction Between Map and Set]-        [("m", fromText map)]-        (fromText set)-        (key2-          (key "_ map"-            (key2 ">"-              (parens (fromText elt <+> fromText elt))-              "Bool"-            )-          )-          "m"-          (parens (key "as const" (key2 "Array" (fromText elt) (fromText elt)) <+> "0"))-        )-    , bFun mmax -- See [Map max and min]-        [("m1", fromText map),("m2", fromText map)]-        (fromText map)-        "(lambda ((i Int)) (ite (> (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"-    , bFun mmin -- See [Map max and min]-        [("m1", fromText map),("m2", fromText map)]-        (fromText map)-        "(lambda ((i Int)) (ite (< (select m1 i) (select m2 i)) (select m1 i) (select m2 i)))"-    , bFun mshift -- See [Map key shift]-        [("n", "Int"),("m", fromText map)]-        (fromText map)-        "(lambda ((i Int)) (select m (- i n)))"-    , bFun mdef-        [("v", fromText elt)]-        (fromText map)-        (key (key "as const" (parens (fromText map))) "v")-    , bFun boolToIntName-        [("b", "Bool")]-        "Int"-        "(ite b 1 0)" -    , uifDef u (symbolText mulFuncName) "*"-    , uifDef u (symbolText divFuncName) "div"-    ]- -- RJ: Am changing this to `Int` not `Real` as (1) we usually want `Int` and -- (2) have very different semantics. TODO: proper overloading, post genEApp uifDef :: Config -> Data.Text.Text -> Data.Text.Text -> Builder uifDef cfg f op-  | linear cfg || Z3 /= solver cfg+  | onlyLinearArith cfg -- linear cfg || Z3 /= solver cfg   = bFun' f ["Int", "Int"] "Int"   | otherwise   = bFun f [("x", "Int"), ("y", "Int")] "Int" (key2 (fromText op) "x" "y") -cvc4Preamble :: Config -> [Builder]-cvc4Preamble z-  = [        "(set-logic ALL_SUPPORTED)"]-  ++ commonPreamble z-  ++ cvc4MapPreamble z+onlyLinearArith :: Config -> Bool+onlyLinearArith cfg = linear cfg || solver cfg `notElem` [Z3, Cvc5] -commonPreamble :: Config -> [Builder]-commonPreamble _ --TODO use uif flag u (see z3Preamble)-  = [ bSort elt    "Int"-    , bSort set    "Int"-    , bSort string "Int"-    , bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)"-    ]+preamble :: Config -> SMTSolver -> [Builder]+preamble cfg s = snd <$> filter (matchesCondition s . fst) (solverPreamble cfg) -cvc4MapPreamble :: Config -> [Builder]-cvc4MapPreamble _ =-    [ bSort map    (key2 "Array" (fromText elt) (fromText elt))-    , bFun sel [("m", fromText map), ("k", fromText elt)]                (fromText elt) "(select m k)"-    , bFun sto [("m", fromText map), ("k", fromText elt), ("v", fromText elt)] (fromText map) "(store m k v)"-    ] -smtlibPreamble :: Config -> [Builder]-smtlibPreamble z --TODO use uif flag u (see z3Preamble)-  = commonPreamble z- ++ [ bSort map "Int"-    , bFun' sel [fromText map, fromText elt] (fromText elt)-    , bFun' sto [fromText map, fromText elt, fromText elt] (fromText map)-    ]+matchesCondition :: SMTSolver -> PreambleCondition -> Bool+matchesCondition _ SAll       = True+matchesCondition s (SOnly ss) = s `elem` ss -stringPreamble :: Config -> [Builder]+solverPreamble :: Config -> [Preamble]+solverPreamble cfg+  =  [(SOnly [Cvc4], "(set-logic ALL_SUPPORTED)")]+  ++ [(SOnly [Cvc5], "(set-logic ALL)")]+  ++ boolPreamble cfg+  ++ arithPreamble cfg+  ++ stringPreamble cfg++type Preamble = (PreambleCondition, Builder)++data PreambleCondition = SAll | SOnly [SMTSolver]+  deriving (Eq, Show)+++boolPreamble :: Config -> [Preamble]+boolPreamble _+  = [ (SAll, bFun boolToIntName [("b", "Bool")] "Int" "(ite b 1 0)") ]++arithPreamble :: Config -> [Preamble]+arithPreamble cfg = (SAll,) <$>+ [ uifDef cfg (symbolText mulFuncName) "*"+ , uifDef cfg (symbolText divFuncName) "div"+ ]++stringPreamble :: Config -> [Preamble] stringPreamble cfg | stringTheory cfg-  = [ bSort string "String"-    , bFun strLen [("s", fromText string)] "Int" (key (fromText z3strlen) "s")-    , bFun strSubstr [("s", fromText string), ("i", "Int"), ("j", "Int")] (fromText string) (key (fromText z3strsubstr) "s i j")-    , bFun strConcat [("x", fromText string), ("y", fromText string)] (fromText string) (key (fromText z3strconcat) "x y")+  = [ (SAll, bSort string "String")+    , (SAll, bFun strLen [("s", fromText string)] "Int" (key (fromText smtlibStrLen) "s"))+    , (SAll, bFun strSubstr [("s", fromText string), ("i", "Int"), ("j", "Int")] (fromText string) (key (fromText smtlibStrSubstr) "s i j"))+    , (SAll, bFun strConcat [("x", fromText string), ("y", fromText string)] (fromText string) (key (fromText smtlibStrConcat) "x y"))     ]  stringPreamble _-  = [ bSort string "Int"-    , bFun' strLen [fromText string] "Int"-    , bFun' strSubstr [fromText string, "Int", "Int"] (fromText string)-    , bFun' strConcat [fromText string, fromText string] (fromText string)+  = [ (SAll, bSort string "Int")+    , (SAll, bFun' strLen [fromText string] "Int")+    , (SAll, bFun' strSubstr [fromText string, "Int", "Int"] (fromText string))+    , (SAll, bFun' strConcat [fromText string, fromText string] (fromText string))     ]  --------------------------------------------------------------------------------@@ -384,8 +300,8 @@ smt2SmtSort SReal        = "Real" smt2SmtSort SBool        = "Bool" smt2SmtSort SString      = fromText string-smt2SmtSort SSet         = fromText set-smt2SmtSort SMap         = fromText map+smt2SmtSort (SSet a)     = key "Set" (smt2SmtSort a)+smt2SmtSort (SBag a)     = key "Bag" (smt2SmtSort a) smt2SmtSort (SArray a b) = key2 "Array" (smt2SmtSort a) (smt2SmtSort b) smt2SmtSort (SBitVec n)  = key "_ BitVec" (bShow n) smt2SmtSort (SVar n)     = "T" <> bShow n@@ -402,7 +318,11 @@ smt2App :: VarAs -> SymEnv -> Expr -> [Builder] -> Maybe Builder -------------------------------------------------------------------------------- smt2App _ env ex@(dropECst -> EVar f) [d]-  | f == arrConst = Just (key (key "as const" (getTarget ex)) d)+  | f == arrConstS = Just (key (key "as const" (getTarget ex)) d)+  | f == arrConstB = Just (key (key "as const" (getTarget ex)) d)+  | f == arrConstM = Just (key (key "as const" (getTarget ex)) d)+  | f == setEmpty  = Just (key "as set.empty" (getTarget ex))+  | f == bagEmpty  = Just (key "as bag.empty" (getTarget ex))   where     getTarget :: Expr -> Builder     -- const is a function, but SMT expects only the output sort@@ -447,11 +367,8 @@   Just (_, ts) -> Just (length ts - 1)   Nothing      -> Nothing -preamble :: Config -> SMTSolver -> [Builder]-preamble u Z3   = z3Preamble u-preamble u Cvc4 = cvc4Preamble u-preamble u _    = smtlibPreamble u + -------------------------------------------------------------------------------- -- | Theory Symbols : `uninterpSEnv` should be disjoint from see `interpSEnv` --   to avoid duplicate SMT definitions.  `uninterpSEnv` is for uninterpreted@@ -460,47 +377,50 @@  -- | `theorySymbols` contains the list of ALL SMT symbols with interpretations, --   i.e. which are given via `define-fun` (as opposed to `declare-fun`)-theorySymbols :: [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol-theorySymbols ds = fromListSEnv $  -- SHIFTLAM uninterpSymbols-                                  interpSymbols+theorySymbols :: SMTSolver -> [DataDecl] -> SEnv TheorySymbol -- M.HashMap Symbol TheorySymbol+theorySymbols cfg ds = fromListSEnv $  -- SHIFTLAM uninterpSymbols+                                  interpSymbols cfg                                ++ concatMap dataDeclSymbols ds   ---------------------------------------------------------------------------------interpSymbols :: [(Symbol, TheorySymbol)]+interpSymbols :: SMTSolver -> [(Symbol, TheorySymbol)] ---------------------------------------------------------------------------------interpSymbols =+interpSymbols cfg =   [-  -- TODO we'll probably need two versions of these - one for sets and one for maps-    interpSym arrConst  "const"       (FAbs 0 $ FFunc boolSort setArrSort)-  , interpSym arrStore  "store"       (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) $ FFunc boolSort setArrSort)-  , interpSym arrSelect "select"      (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) boolSort)-  , interpSym arrMapNot "(_ map not)" (FFunc setArrSort setArrSort)-  , interpSym arrMapOr  "(_ map or)"  (FFunc setArrSort $ FFunc setArrSort setArrSort)-  , interpSym arrMapAnd "(_ map and)" (FFunc setArrSort $ FFunc setArrSort setArrSort)-  , interpSym arrMapImp "(_ map =>)"  (FFunc setArrSort $ FFunc setArrSort setArrSort)+    -- maps -  , interpSym setEmp   setEmp   (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)-  , interpSym setEmpty setEmpty (FAbs 0 $ FFunc intSort (setSort $ FVar 0))-  , interpSym setSng   setSng   (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0))-  , interpSym setAdd   setAdd   setAddSort-  , interpSym setCup   setCup   setBopSort-  , interpSym setCap   setCap   setBopSort-  , interpSym setMem   setMem   setMemSort-  , interpSym setDif   setDif   setBopSort-  , interpSym setSub   setSub   setCmpSort-  , interpSym setCom   setCom   setCmpSort+    interpSym mapDef   mapDef  mapDefSort+  , interpSym mapSel   mapSel  mapSelSort+  , interpSym mapSto   mapSto  mapStoSort -  , interpSym mapSel   sel   mapSelSort-  , interpSym mapSto   sto   mapStoSort-  , interpSym mapCup   mcup  mapCupSort-  , interpSym mapMax   mmax  mapMaxSort-  , interpSym mapMin   mmin  mapMinSort-  , interpSym mapDef   mdef  mapDefSort-  , interpSym mapPrj   mprj  mapPrjSort-  , interpSym mapShift mshift mapShiftSort-  , interpSym mapToSet mToSet mapToSetSort+  , interpSym arrConstM  "const"  (FAbs 0 $ FFunc (FVar 1) mapArrSort)+  , interpSym arrSelectM "select" (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) (FVar 1))+  , interpSym arrStoreM  "store"  (FAbs 0 $ FFunc mapArrSort $ FFunc (FVar 0) $ FFunc (FVar 1) mapArrSort) +  -- CVC5 sets++  , interpSym setEmp   "set.is_empty"   (FAbs 0 $ FFunc (setSort $ FVar 0) boolSort)+  , interpSym setEmpty "set.empty"      (FAbs 0 $ FFunc intSort (setSort $ FVar 0))+  , interpSym setSng   "set.singleton"  (FAbs 0 $ FFunc (FVar 0) (setSort $ FVar 0))+  , interpSym setAdd   "set.insert"     (FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0))+  , interpSym setMem   "set.member"     (FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort)+  , interpSym setCup   "set.union"      setBopSort+  , interpSym setCap   "set.inter"      setBopSort+  , interpSym setDif   "set.minus"      setBopSort+  , interpSym setSub   "set.subset"     (FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort)+  , interpSym setCom   "set.complement" (FAbs 0 $ FFunc (setSort $ FVar 0) (setSort $ FVar 0))++  -- CVC5 bags++  , interpSym bagEmpty "bag.empty"          (FAbs 0 $ FFunc intSort (bagSort $ FVar 0))+  , interpSym bagSng   "bag"                (FAbs 0 $ FFunc (FVar 0) $ FFunc intSort (bagSort $ FVar 0))+  , interpSym bagCount "bag.count"          (FAbs 0 $ FFunc (FVar 0) $ FFunc (bagSort $ FVar 0) intSort)+  , interpSym bagCup   "bag.union_disjoint" bagBopSort+  , interpSym bagMax   "bag.union_max"      bagBopSort+  , interpSym bagMin   "bag.inter_min"      bagBopSort+  , interpSym bagSub   "bag.subbag"         (FAbs 0 $ FFunc (bagSort $ FVar 0) $ FFunc (bagSort $ FVar 0) boolSort)+   -- , interpSym bvOrName  "bvor"  bvBopSort   -- , interpSym bvAndName "bvand" bvBopSort   -- , interpSym bvAddName "bvadd" bvBopSort@@ -555,50 +475,68 @@   , interpBvCmp bvSLeName   , interpBvCmp bvSGtName   , interpBvCmp bvSGeName+  , interpSym intbv32Name   "(_ int2bv 32)" (FFunc intSort bv32)+  , interpSym intbv64Name   "(_ int2bv 64)" (FFunc intSort bv64)+  , interpSym bv32intName   (bv2i cfg 32) (FFunc bv32    intSort)+  , interpSym bv64intName   (bv2i cfg 64) (FFunc bv64    intSort)+  -- , interpSym bv32intName   "(_ bv2int 32)" (FFunc bv32    intSort)+  -- , interpSym bv64intName   "(_ bv2int 64)" (FFunc bv64    intSort)+  ]+  +++  if cfg == Z3 || cfg == Z3mem+  then+  [+    -- Z3 sets (arrays of bools) -  , interpSym intbv32Name "(_ int2bv 32)"   (FFunc intSort bv32)-  , interpSym intbv64Name "(_ int2bv 64)"   (FFunc intSort bv64)-  , interpSym bv32intName  "(_ bv2int 32)"  (FFunc bv32    intSort)-  , interpSym bv64intName   "(_ bv2int 64)" (FFunc bv64    intSort)+    interpSym arrConstS  "const"  (FAbs 0 $ FFunc boolSort setArrSort)+  , interpSym arrSelectS "select" (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) boolSort)+  , interpSym arrStoreS  "store"  (FAbs 0 $ FFunc setArrSort $ FFunc (FVar 0) $ FFunc boolSort setArrSort) -  ]+  , interpSym arrMapNotS "(_ map not)" (FAbs 0 $ FFunc setArrSort setArrSort)+  , interpSym arrMapOrS  "(_ map or)"  (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)+  , interpSym arrMapAndS "(_ map and)" (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)+  , interpSym arrMapImpS "(_ map =>)"  (FAbs 0 $ FFunc setArrSort $ FFunc setArrSort setArrSort)++    -- Z3 bags (arrays of ints)++  , interpSym arrConstB  "const"  (FAbs 0 $ FFunc intSort bagArrSort)+  , interpSym arrSelectB "select" (FAbs 0 $ FFunc bagArrSort $ FFunc (FVar 0) intSort)+  , interpSym arrStoreB  "store"  (FAbs 0 $ FFunc bagArrSort $ FFunc (FVar 0) $ FFunc intSort bagArrSort)++  , interpSym arrMapPlusB "(_ map (+ (Int Int) Int))"        (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)+  , interpSym arrMapLeB   "(_ map (<= (Int Int) Bool))"      (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort setArrSort)+  , interpSym arrMapGtB   "(_ map (> (Int Int) Bool))"       (FAbs 0 $ FFunc bagArrSort $ FFunc bagArrSort setArrSort)+  , interpSym arrMapIteB  "(_ map (ite (Bool Int Int) Int))" (FAbs 0 $ FFunc setArrSort $ FFunc bagArrSort $ FFunc bagArrSort bagArrSort)+  ] else []   where++    mapArrSort = arraySort (FVar 0) (FVar 1)     setArrSort = arraySort (FVar 0) boolSort+    bagArrSort = arraySort (FVar 0) intSort     -- (sizedBitVecSort "Size1")     bv32       = sizedBitVecSort "Size32"     bv64       = sizedBitVecSort "Size64"     boolInt    = boolToIntName -    setAddSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (FVar 0)           (setSort $ FVar 0)-    setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)-    setMemSort = FAbs 0 $ FFunc (FVar 0) $ FFunc (setSort $ FVar 0) boolSort-    setCmpSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) boolSort--    -- select :: forall i a. Map i a -> i -> a+    mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1)+                                         (mapSort (FVar 0) (FVar 1))+    -- select :: forall k v. Map k v -> k -> v     mapSelSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))                                  $ FFunc (FVar 0) (FVar 1)-    -- cup :: forall i. Map i Int -> Map i Int -> Map i Int-    mapCupSort = FAbs 0          $ FFunc (mapSort (FVar 0) intSort)-                                 $ FFunc (mapSort (FVar 0) intSort)-                                         (mapSort (FVar 0) intSort)-    mapMaxSort = mapCupSort-    mapMinSort = mapCupSort-    mapPrjSort = FAbs 0          $ FFunc (setSort (FVar 0))-                                 $ FFunc (mapSort (FVar 0) intSort)-                                         (mapSort (FVar 0) intSort)-    mapShiftSort = FAbs 0        $ FFunc intSort-                                 $ FFunc (mapSort intSort (FVar 0))-                                         (mapSort intSort (FVar 0))-    mapToSetSort = FAbs 0        $ FFunc (mapSort (FVar 0) intSort) (setSort (FVar 0))-    -- store :: forall i a. Map i a -> i -> a -> Map i a+    -- store :: forall k v. Map k v -> k -> v -> Map k v     mapStoSort = FAbs 0 $ FAbs 1 $ FFunc (mapSort (FVar 0) (FVar 1))                                  $ FFunc (FVar 0)                                  $ FFunc (FVar 1)                                          (mapSort (FVar 0) (FVar 1))-    mapDefSort = FAbs 0 $ FAbs 1 $ FFunc (FVar 1)-                                         (mapSort (FVar 0) (FVar 1)) +    setBopSort = FAbs 0 $ FFunc (setSort $ FVar 0) $ FFunc (setSort $ FVar 0) (setSort $ FVar 0)+    bagBopSort = FAbs 0 $ FFunc (bagSort $ FVar 0) $ FFunc (bagSort $ FVar 0) (bagSort $ FVar 0) +bv2i :: SMTSolver -> Int -> Raw+bv2i Cvc4 _ = "bv2nat"+bv2i Cvc5 _ = "bv2nat"+bv2i _    n = Data.Text.pack $ printf "(_ bv2nat %d)" n+ interpBvUop :: Symbol -> (Symbol, TheorySymbol) interpBvUop name = interpSym' name bvUopSort interpBvBop :: Symbol -> (Symbol, TheorySymbol)@@ -678,8 +616,14 @@ interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol) interpSym x n t = (x, Thy x n t Theory) +-- This variable is uded to generate the lambda names `lam_arg$n` in+-- `Interface.hs` that will be used during defunctionalization in+-- `Defunctionalize.hs`, is a pretty gross hack as if the user typees in the+-- program or ple generates a term that has more than `maxLamArg` lambda binders+-- one inside the other, the smt will crash complaining that+-- `lam_arg${maxLamArg}` was not declared. maxLamArg :: Int-maxLamArg = 7+maxLamArg = 20  axiomLiterals :: [(Symbol, Sort)] -> [Expr] axiomLiterals lts = catMaybes [ lenAxiom l <$> litLen l | (l, t) <- lts, isString t ]

@@ -29,6 +29,7 @@  import           Data.ByteString.Builder (Builder) import           Language.Fixpoint.Types+import           Language.Fixpoint.Types.Config (ElabFlags) import qualified Data.Text                as T import           Text.PrettyPrint.HughesPJ import qualified SMTLIB.Backends@@ -95,6 +96,7 @@   {   -- | The high-level interface for interacting with the SMT solver backend.     ctxSolver  :: SMTLIB.Backends.Solver+  , ctxElabF   :: ElabFlags   -- | The close operation of the SMT solver backend.   , ctxClose   :: IO ()   , ctxLog     :: !(Maybe Handle)

@@ -41,7 +41,7 @@ import           Language.Fixpoint.Solver.Sanitize  (symbolEnv, sanitize) import           Language.Fixpoint.Solver.UniqifyBinds (renameAll) import           Language.Fixpoint.Defunctionalize (defunctionalize)-import           Language.Fixpoint.SortCheck            (Elaborate (..), unElab)+import           Language.Fixpoint.SortCheck            (ElabParam (..), Elaborate (..), unElab) import           Language.Fixpoint.Solver.Extensionality (expand) import           Language.Fixpoint.Solver.Prettify (savePrettifiedQuery) import           Language.Fixpoint.Solver.UniqifyKVars (wfcUniqify)@@ -250,7 +250,7 @@   -- writeLoud $ "fq file after defunc: \n" ++ render (toFixpoint cfg si4)   -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)   loudDump 2 cfg si4-  let si5  = {- SCC "elaborate" -} elaborate (atLoc dummySpan "solver") (symbolEnv cfg si4) si4+  let si5  = {- SCC "elaborate" -} elaborate (ElabParam (solverFlags $ solver cfg) (atLoc dummySpan "solver") (symbolEnv cfg si4)) si4   -- writeLoud $ "fq file after elaborate: \n" ++ render (toFixpoint cfg si5)   loudDump 3 cfg si5   let si6 = if extensionality cfg then {- SCC "expand" -} expand cfg si5 else si5

@@ -2,12 +2,12 @@  module Language.Fixpoint.Solver.Common (askSMT, toSMT) where -import Language.Fixpoint.Types.Config (Config)+import Language.Fixpoint.Types.Config (Config, solver, solverFlags) import Language.Fixpoint.Smt.Interface (Context(..), checkValidWithContext) import Language.Fixpoint.Types import Language.Fixpoint.Types.Visitor (kvarsExpr) import Language.Fixpoint.Defunctionalize (defuncAny)-import Language.Fixpoint.SortCheck (elaborate)+import Language.Fixpoint.SortCheck (ElabParam(..), elaborate)  mytracepp :: (PPrint a) => String -> a -> a mytracepp = notracepp@@ -16,7 +16,7 @@ askSMT cfg ctx xs e --   | isContraPred e  = return False   | isTautoPred  e     = return True-  | null (kvarsExpr e) = checkValidWithContext ctx [] PTrue e'+  | null (kvarsExpr e) = checkValidWithContext ctx xs PTrue e'   | otherwise          = return False   where     e' = toSMT "askSMT" cfg ctx xs e@@ -24,7 +24,7 @@ toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Pred toSMT msg cfg ctx xs e =     defuncAny cfg symenv .-        elaborate (dummyLoc msg) (elabEnv xs) .+        elaborate (ElabParam (solverFlags $ solver cfg) (dummyLoc msg) (elabEnv xs)) .             mytracepp ("toSMT from " ++ msg ++ showpp e) $                 e   where

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE PatternSynonyms #-}@@ -11,6 +12,7 @@   ( reduceEnvironments   , simplifyBindings   , dropLikelyIrrelevantBindings+  , relatedSymbols   , inlineInExpr   , inlineInSortedReft   , mergeDuplicatedBindings@@ -70,10 +72,12 @@ import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Refinements   ( Brel(..)-  , Expr(..)+  , ExprV(..)+  , Expr   , KVar(..)   , SortedReft(..)-  , Subst(..)+  , Subst+  , SubstV(..)   , pattern PTrue   , pattern PFalse   , dropECst@@ -744,7 +748,8 @@   -> HashMap Symbol SortedReft dropLikelyIrrelevantBindings ss env = HashMap.filterWithKey relevant env   where-    relatedSyms = relatedSymbols ss env+    directlyUses = HashMap.map (exprSymbolsSet . reftPred . sr_reft) env+    relatedSyms = relatedSymbols ss directlyUses     relevant s _sr =       (not (capitalizedSym s) || prefixOfSym s /= s) && s `HashSet.member` relatedSyms     capitalizedSym = Text.all isUpper . Text.take 1 . symbolText@@ -760,10 +765,10 @@ -- @a@ uses @b@. Because the predicate of @c@ relates @b@ with @d@, -- @d@ can also influence the validity of the predicate of @a@, and therefore -- we include both @b@, @c@, and @d@ in the set of related symbols.-relatedSymbols :: HashSet Symbol -> HashMap Symbol SortedReft -> HashSet Symbol-relatedSymbols ss0 env = go HashSet.empty ss0+relatedSymbols+  :: HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol+relatedSymbols ss0 directlyUses = go HashSet.empty ss0   where-    directlyUses = HashMap.map (exprSymbolsSet . reftPred . sr_reft) env     usedBy = HashMap.fromListWith HashSet.union                [ (x, HashSet.singleton s)                | (s, xs) <- HashMap.toList directlyUses

@@ -24,9 +24,9 @@ mytracepp = notracepp  expand :: Config -> SInfo a -> SInfo a-expand cfg si = evalState (ext si) $ initST (symbolEnv cfg si) (ddecls si)+expand cfg si = evalState (ext si) $ initST (symbolEnv cfg si) (ddecls si) (solverFlags $ solver cfg)   where-    ext ::SInfo a -> Ex a (SInfo a)+    ext :: SInfo a -> Ex a (SInfo a)     ext = extend  @@ -42,7 +42,7 @@     return $ si{ cm = cm' , bs = bs' }  instance (Extend ann a) => Extend ann (M.HashMap SubcId a) where-  extend h = M.fromList <$> mapM extend (M.toList h)+  extend h  = M.fromList <$> mapM extend (M.toList h)  instance (Extend ann a, Extend ann b) => Extend ann (a,b) where   extend (a,b) = (,) <$> extend a <*> extend b@@ -100,11 +100,12 @@     Left dds -> mapM (freshArgDD ann) dds     Right s  -> (\x -> [EVar x]) <$> freshArgOne ann s -makeEq :: Brel-> Expr -> Expr -> Expr -> Ex ann Expr+makeEq :: Brel -> Expr -> Expr -> Expr -> Ex ann Expr makeEq b e1 e2 e = do   env <- gets exenv-  let elab = elaborate (dummyLoc "extensionality") env-  return $ PAtom b (elab $ EApp (unElab e1) e)  (elab $ EApp (unElab e2) e)+  slv <- gets elabf+  let elab = elaborate (ElabParam slv (dummyLoc "extensionality") env)+  return $ PAtom b (elab $ EApp (unElab e1) e) (elab $ EApp (unElab e2) e)  instantiate :: a -> [DataDecl]  -> Sort -> Ex a [Expr] instantiate ann ds s = instantiateOne ann (breakSort ds s)@@ -196,13 +197,18 @@   , exbenv  :: BindEnv a   , exbinds :: IBindEnv   , excbs   :: [(Symbol, Sort)]+  , elabf   :: ElabFlags   } -initST :: SymEnv -> [DataDecl]  -> ExSt ann-initST env dd = ExSt 0 (d:dd) env mempty mempty mempty+initST :: SymEnv -> [DataDecl] -> ElabFlags -> ExSt ann+initST env dd ef = ExSt 0 (d:dd) env mempty mempty mempty ef   where     -- NV: hardcore Haskell pairs because they do not appear in DataDecl (why?)-    d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc tupConName)) 2 [ct]+#if MIN_TOOL_VERSION_ghc(9,10,1)+    d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc $ symbol "Tuple2")) 2 [ct]+#else+    d = mytracepp "Tuple DataDecl" $ DDecl (symbolFTycon (dummyLoc $ symbol "Tuple")) 2 [ct]+#endif #if MIN_TOOL_VERSION_ghc(9,6,0) && !MIN_TOOL_VERSION_ghc(9,10,0)     ct = DCtor (dummyLoc (symbol "GHC.Tuple.Prim.(,)")) [             DField (dummyLoc (symbol "lqdc$select$GHC.Tuple.Prim.(,)$1")) (FVar 0)

@@ -7,6 +7,7 @@   ) where  import           Control.Parallel.Strategies+import           Control.Monad.Reader import qualified Data.HashMap.Strict            as M import qualified Data.List                      as L import           Data.Maybe                     (maybeToList, isNothing)@@ -26,7 +27,7 @@ -------------------------------------------------------------------------------- init :: (F.Fixpoint a) => Config -> F.SInfo a -> [(F.KVar, (F.GWInfo, [F.Expr]))] ---------------------------------------------------------------------------------init cfg si = map (elab . refineG si qs genv) gs `using` parList rdeepseq+init cfg si = map elab (runReader (traverse (refineG si qs genv) gs) ef) `using` parList rdeepseq   where     qs         = F.quals si     gs         = snd <$> gs0@@ -34,19 +35,20 @@      gs0        = L.filter (Cons.isGWfc . snd) $ M.toList (F.ws si) -    elab (k, (x,es)) = (k, (x, elaborate (F.atLoc F.dummySpan "init") (sEnv (Cons.gsym x) (Cons.gsort x)) <$> es))+    elab (k, (x,es)) = (k, (x, elaborate (ElabParam ef (F.atLoc F.dummySpan "init") (sEnv (Cons.gsym x) (Cons.gsort x))) <$> es))      sEnv x s    = isEnv {F.seSort = F.insertSEnv x s (F.seSort isEnv)}     isEnv       = symbolEnv cfg si+    ef          = solverFlags $ solver cfg   ---------------------------------------------------------------------------------refineG :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, (F.GWInfo, [F.Expr]))-refineG fi qs genv w = (k, (F.gwInfo w, Sol.qbExprs qb))-  where-    (k, qb) = refine fi qs genv w+refineG :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> ElabM (F.KVar, (F.GWInfo, [F.Expr]))+refineG fi qs genv w =+  do (k, qb) <- refine fi qs genv w+     pure (k, (F.gwInfo w, Sol.qbExprs qb)) -refine :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)+refine :: F.SInfo a -> [F.Qualifier] -> F.SEnv F.Sort -> F.WfC a -> ElabM (F.KVar, Sol.QBind) refine fi qs genv w = refineK (Cons.allowHOquals fi) env qs $ F.wrft w   where     env             = wenv <> genv@@ -58,12 +60,14 @@     notLit    = not . F.isLitSymbol . fst  -refineK :: Bool -> F.SEnv F.Sort -> [F.Qualifier] -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)-refineK ho env qs (v, t, k) = (k, eqs')+refineK :: Bool -> F.SEnv F.Sort -> [F.Qualifier] -> (F.Symbol, F.Sort, F.KVar) -> ElabM (F.KVar, Sol.QBind)+refineK ho env qs (v, t, k) =+  do eqs' <- Sol.qbFilterM (okInst env v t) eqs+     pure (k, eqs')    where     eqs                     = instK ho env v t qs-    eqs'                    = Sol.qbFilter (okInst env v t) eqs + -------------------------------------------------------------------------------- instK :: Bool       -> F.SEnv F.Sort@@ -118,12 +122,14 @@     mono = So.isMono tx  ---------------------------------------------------------------------------------okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool+okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> ElabM Bool ---------------------------------------------------------------------------------okInst env v t eq = isNothing tc+okInst env v t eq =+  do tc <- So.checkSorted F.dummySpan env sr+     pure $ isNothing tc   where     sr            = F.RR t (F.Reft (v, p))     p             = Sol.eqPred eq-    tc            = So.checkSorted F.dummySpan env sr+  

@@ -35,13 +35,13 @@ import           Language.Fixpoint.Solver.Common          (askSMT) import           Control.Monad ((>=>), foldM, forM, forM_, join) import           Control.Monad.State-import           Data.Bifunctor (second)+import           Data.Bifunctor (first, second) import qualified Data.Text            as T import qualified Data.HashMap.Strict  as M import qualified Data.HashSet         as S import qualified Data.List            as L import qualified Data.Maybe           as Mb -- (isNothing, catMaybes, fromMaybe)-import           Data.Char            (isUpper)+import           Data.Char            (isDigit, isUpper) -- import           Debug.Trace          (trace) -- import           Text.Printf (printf) @@ -181,7 +181,7 @@ resSInfo cfg env info res = strengthenBinds info res'   where     res'     = M.fromList $ mytracepp  "ELAB-INST:  " $ zip is ps''-    ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'+    ps''     = zipWith (\i -> elaborate (ElabParam (solverFlags $ solver cfg) (atLoc dummySpan ("PLE1 " ++ show i)) env)) is ps'     ps'      = defuncAny cfg env ps     (is, ps) = unzip (M.toList res) @@ -311,7 +311,7 @@   where     (is, ps)         = unzip ips     ps'              = defuncAny cfg env ps-    ps''             = zipWith (\(i, sp) -> elaborate (atLoc sp ("PLE1 " ++ show i)) env) is ps'+    ps''             = zipWith (\(i, sp) -> elaborate (ElabParam (solverFlags $ solver cfg) (atLoc sp ("PLE1 " ++ show i)) env)) is ps'  instSimpC :: Config -> SMT.Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr instSimpC cfg ctx bds aenv subId sub@@ -558,7 +558,7 @@     ts    = snd    <$> eqArgs eq     sp    = panicSpan "mkCoSub"     eTs   = sortExpr sp env <$> es-    coSub = mytracepp  ("substEqCoerce" ++ showpp (eqName eq, es, eTs, ts)) $ mkCoSub env eTs ts+    coSub = mytracepp ("substEqCoerce" ++ showpp (eqName eq, es, eTs, ts)) $ mkCoSub env eTs ts  mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub mkCoSub env eTs xTs = M.fromList [ (x, unite ys) | (x, ys) <- Misc.groupList xys ]@@ -728,8 +728,8 @@   | otherwise   = Nothing   where-    (f1, es1) = Misc.mapFst (getDC sEnv) (splitEApp e1)-    (f2, es2) = Misc.mapFst (getDC sEnv) (splitEApp e2)+    (f1, es1) = first (getDC sEnv) (splitEApp e1)+    (f2, es2) = first (getDC sEnv) (splitEApp e2)  -- TODO: Stringy hacks getDC :: SymEnv -> Expr -> Maybe Symbol@@ -749,9 +749,16 @@   where     mungeNames _ _ ""  = ""     mungeNames f d s'@(symbolText -> s)-      | s' == tupConName = tupConName+      | isTupleSymbol s' = s'       | otherwise        = f $ T.splitOn d $ stripParens s     stripParens t = Mb.fromMaybe t ((T.stripPrefix "(" >=> T.stripSuffix ")") t)++    -- TODO: Remove this code which is LH specific+    isTupleSymbol :: Symbol -> Bool+    isTupleSymbol s =+      let t = symbolText s+       in T.isPrefixOf "Tuple" t &&+          T.all isDigit (T.drop 5 t)  -------------------------------------------------------------------------------- -- | Creating Measure Info

@@ -12,6 +12,7 @@ {-# LANGUAGE OverloadedStrings         #-} {-# LANGUAGE PartialTypeSignatures     #-} {-# LANGUAGE TupleSections             #-}+{-# LANGUAGE FlexibleContexts          #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE PatternGuards             #-} {-# LANGUAGE RecordWildCards           #-}@@ -181,7 +182,7 @@ resSInfo cfg env info res = strengthenBinds info res'   where     res'     = M.fromList $ zip is ps''-    ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'+    ps''     = zipWith (\i -> elaborate (ElabParam (solverFlags $ solver cfg) (atLoc dummySpan ("PLE1 " ++ show i)) env)) is ps'     ps'      = defuncAny cfg env ps     (is, ps) = unzip (M.toList res) @@ -472,7 +473,7 @@         , length (eqArgs eq) <= length es         = let (es1,es2) = splitAt (length (eqArgs eq)) es               ges       = substEq env eq es1-              exp1       = unfoldExpr ie γ ctx env ges+              exp1      = unfoldExpr ie γ ctx env ges               exp2      = eApps exp1 es2 in  --exp' -- TODO undo             if eApps (EVar f) es == exp2 then exp2 else interpret' ie γ ctx env exp2 

@@ -11,6 +11,7 @@           -- * Get Binds        , getBinds+       , getContext           -- * SMT Query        , filterRequired@@ -84,10 +85,10 @@     act'     = assumesAxioms (F.asserts fi) >> act     release  = cleanupContext     acquire  = makeContextWithSEnv cfg file initEnv-    initEnv  = symbolEnv   cfg fi+    initEnv  = symbolEnv cfg fi     be       = F.bs fi     file     = C.srcFile cfg-    -- only linear arithmentic when: linear flag is on or solver /= Z3+    -- only linear arithmetic when: linear flag is on or solver /= Z3     -- lar     = linear cfg || Z3 /= solver cfg     fi       = (siQuery sI) {F.hoInfo = F.cfgHoInfo cfg } @@ -161,25 +162,6 @@ filterRequired :: F.Cand a -> F.Expr -> SolveM ann [a] -------------------------------------------------------------------------------- filterRequired = error "TBD:filterRequired"--{--(set-option :produce-unsat-cores true)-(declare-fun x () Int)-(declare-fun y () Int)-(declare-fun z () Int)--; Z3 will only track assertions that are named.--(assert (< 0 x))-(assert (! (< 0 y)       :named b2))-(assert (! (< x 10)      :named b3))-(assert (! (< y 10)      :named b4))-(assert (! (< (+ x y) 0) :named bR))-(check-sat)-(get-unsat-core)--> unsat (b2 bR)--}  -------------------------------------------------------------------------------- -- | `filterValid p [(q1, x1),...,(qn, xn)]` returns the list `[ xi | p => qi]`

@@ -15,6 +15,7 @@ {-# LANGUAGE PatternGuards             #-} {-# LANGUAGE RecordWildCards           #-} {-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE DoAndIfThenElse           #-}  module Language.Fixpoint.Solver.PLE   ( instantiate@@ -50,7 +51,7 @@ import Language.REST.RuntimeTerm as RT import Language.REST.SMT (withZ3, SolverHandle) -import           Control.Monad (filterM, foldM, forM_, when)+import           Control.Monad (filterM, foldM, forM_, when, replicateM) import           Control.Monad.State import           Control.Monad.Trans.Maybe import           Data.Bifunctor (second)@@ -89,10 +90,10 @@     withRESTSolver f | all null (M.elems $ aenvAutoRW aEnv) = f Nothing     withRESTSolver f = withZ3 (f . Just) -    file   = srcFile cfg ++ ".evals"-    sEnv   = symbolEnv cfg info-    aEnv   = ae info-    info   = normalize fi'+    file = srcFile cfg ++ ".evals"+    sEnv = symbolEnv cfg info+    aEnv = ae info+    info = normalize fi'  savePLEEqualities :: Config -> SInfo a -> SymEnv -> InstRes -> IO () savePLEEqualities cfg info sEnv res = when (save cfg) $ do@@ -113,7 +114,7 @@             map (toFix . unElab) $ Set.toList $ Set.fromList $             -- call elabExpr to try to bring equations that are missing             -- some casts into a fully annotated form for comparison-            map (elabExpr "savePLEEqualities" sEnv) $+            map (elabExpr (ElabParam (solverFlags $ solver cfg) "savePLEEqualities" sEnv)) $             concatMap conjuncts eqs            )       $+$ ""@@ -142,10 +143,12 @@                  ExploreWhenNeeded         s0 = EvalEnv               { evEnv = SMT.ctxSymEnv ctx+              , evElabF = ef               , evPendingUnfoldings = mempty               , evNewEqualities = mempty               , evSMTCache = mempty               , evFuel = defFuelCount cfg+              , freshEtaNames = 0               , explored = Just et               , restSolver = restSolver               , restOCA = restOrd@@ -154,13 +157,16 @@     return $ InstEnv        { ieCfg = cfg        , ieSMT = ctx-       , ieBEnv = bs info+       , ieBEnv = coerceBindEnv ef (bs info)        , ieAenv = ae info        , ieCstrs = cs        , ieKnowl = knowledge cfg ctx info        , ieEvEnv = s0+       , ieLRWs  = lrws info        }   where+    ef = solverFlags $ solver cfg+     cachedNotStrongerThan refRESTCache oc a b = do       m <- readIORef refRESTCache       case M.lookup (a, b) m of@@ -206,18 +212,21 @@ ---------------------------------------------------------------------------------------------- -- | Step 2: @pleTrie@ walks over the @CTrie@ to actually do the incremental-PLE pleTrie :: CTrie -> InstEnv a -> IO InstRes-pleTrie t env = loopT env' ctx0 diff0 Nothing res0 t+pleTrie t env = loopT env ctx0 diff0 Nothing res0 t   where-    env'         = env     diff0        = []     res0         = M.empty     ctx0         = ICtx-      { icAssms  = mempty-      , icCands  = mempty-      , icEquals = mempty-      , icSimpl  = mempty-      , icSubcId = Nothing-      , icANFs   = []+      { icAssms              = mempty+      , icCands              = mempty+      , icEquals             = mempty+      , icSimpl              = mempty+      , icSubcId             = Nothing+      , icANFs               = []+      , icLRWs               = mempty+      , icEtaBetaFlag        = etabeta        $ ieCfg env+      , icExtensionalityFlag = extensionality $ ieCfg env+      , icLocalRewritesFlag  = localRewrites  $ ieCfg env       }  loopT@@ -232,8 +241,8 @@ loopT env ctx delta i res t = case t of   T.Node []  -> return res   T.Node [b] -> loopB env ctx delta i res b-  T.Node bs  -> withAssms env ctx delta Nothing $ \env' ctx' -> do-                  (ctx'', env'', res') <- ple1 env' ctx' i res+  T.Node bs  -> withAssms env ctx delta Nothing $ \ctx' -> do+                  (ctx'', env'', res') <- ple1 env ctx' i res                   foldM (loopB env'' ctx'' [] i) res' bs  loopB@@ -247,9 +256,9 @@   -> IO InstRes loopB env ctx delta iMb res b = case b of   T.Bind i t -> loopT env ctx (i:delta) (Just i) res t-  T.Val cid  -> withAssms env ctx delta (Just cid) $ \env' ctx' -> do+  T.Val cid  -> withAssms env ctx delta (Just cid) $ \ctx' -> do                   progressTick-                  (\(_, _, r) -> r) <$> ple1 env' ctx' iMb res+                  (\(_, _, r) -> r) <$> ple1 env ctx' iMb res  -- | Adds to @ctx@ candidate expressions to unfold from the bindings in @delta@ -- and the rhs of @cidMb@.@@ -261,13 +270,14 @@ -- Pushes assumptions from the modified context to the SMT solver, runs @act@, -- and then pops the assumptions. ---withAssms :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (InstEnv a -> ICtx -> IO b) -> IO b+withAssms :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (ICtx -> IO b) -> IO b withAssms env@InstEnv{..} ctx delta cidMb act = do-  let (ctx', env')  = updCtx env ctx delta cidMb+  let ctx' = updCtx env ctx delta cidMb   let assms = icAssms ctx'-  SMT.smtBracket ieSMT  "PLE.evaluate" $ do++  SMT.smtBracket ieSMT "PLE.evaluate" $ do     forM_ assms (SMT.smtAssert ieSMT)-    act env' ctx' { icAssms = mempty }+    act ctx' { icAssms = mempty }  -- | @ple1@ performs the PLE at a single "node" in the Trie --@@ -275,7 +285,7 @@ -- in @ctx@ for which definitions are known. The function definitions are in -- @ieKnowl@. ple1 :: InstEnv a -> ICtx -> Maybe BindId -> InstRes -> IO (ICtx, InstEnv a, InstRes)-ple1 ie@InstEnv {..} ctx i res = do+ple1 ie@InstEnv{..} ctx i res = do   (ctx', env) <- runStateT (evalCandsLoop ieCfg ctx ieSMT ieKnowl) ieEvEnv   let pendings = collectPendingUnfoldings env (icSubcId ctx)       newEqs = pendings ++ S.toList (S.difference (icEquals ctx') (icEquals ctx))@@ -313,21 +323,20 @@       inconsistentEnv <- testForInconsistentEnvironment       if inconsistentEnv         then return ictx-        else do-                  liftIO $ SMT.smtAssert ctx (pAndNoDedup (S.toList $ icAssms ictx))-                  let ictx' = ictx { icAssms = mempty }-                      cands = S.toList $ icCands ictx-                  candss <- mapM (evalOne γ ictx' i) cands-                  us <- gets evNewEqualities-                  modify $ \st -> st { evNewEqualities = mempty }-                  let noCandidateChanged = and (zipWith eqCand candss cands)-                      unknownEqs = us `S.difference` icEquals ictx-                  if S.null unknownEqs && noCandidateChanged-                        then return ictx-                        else do  let eqsSMT   = evalToSMT "evalCandsLoop" cfg ctx `S.map` unknownEqs-                                 let ictx''   = ictx' { icEquals = icEquals ictx <> unknownEqs-                                                      , icAssms  = S.filter (not . isTautoPred) eqsSMT }-                                 go (ictx'' { icCands = S.fromList (concat candss) }) (i + 1)+        else do liftIO $ SMT.smtAssert ctx (pAndNoDedup (S.toList $ icAssms ictx))+                let ictx' = ictx { icAssms = mempty }+                    cands = S.toList $ icCands ictx+                candss <- mapM (evalOne γ ictx' i) cands+                us <- gets evNewEqualities+                modify $ \st -> st { evNewEqualities = mempty }+                let noCandidateChanged = and (zipWith eqCand candss cands)+                    unknownEqs = us `S.difference` icEquals ictx+                if S.null unknownEqs && noCandidateChanged+                      then return ictx+                      else do let eqsSMT = evalToSMT "evalCandsLoop" cfg ctx `S.map` unknownEqs+                              let ictx'' = ictx' { icEquals = icEquals ictx <> unknownEqs+                                                 , icAssms  = S.filter (not . isTautoPred) eqsSMT }+                              go (ictx'' { icCands = S.fromList (concat candss) }) (i + 1)      testForInconsistentEnvironment =       liftIO $ knPreds γ (knContext γ) (knLams γ) PFalse@@ -343,7 +352,7 @@ resSInfo cfg env info res = strengthenBinds info res'   where     res'     = M.fromList $ zip is ps''-    ps''     = zipWith (\i -> elaborate (atLoc dummySpan ("PLE1 " ++ show i)) env) is ps'+    ps''     = zipWith (\i -> elaborate (ElabParam (solverFlags $ solver cfg) (atLoc dummySpan ("PLE1 " ++ show i)) env)) is ps'     ps'      = defuncAny cfg env ps     (is, ps) = unzip (M.toList res) @@ -359,6 +368,7 @@   , ieCstrs :: !(CMap (SimpC a))   , ieKnowl :: !Knowledge   , ieEvEnv :: !EvalEnv+  , ieLRWs  :: LocalRewritesEnv   }  ----------------------------------------------------------------------------------------------@@ -366,12 +376,19 @@ ----------------------------------------------------------------------------------------------  data ICtx    = ICtx-  { icAssms    :: S.HashSet Pred            -- ^ Equalities converted to SMT format-  , icCands    :: S.HashSet Expr            -- ^ "Candidates" for unfolding-  , icEquals   :: EvEqualities              -- ^ Accumulated equalities-  , icSimpl    :: !ConstMap                 -- ^ Map of expressions to constants-  , icSubcId   :: Maybe SubcId              -- ^ Current subconstraint ID-  , icANFs     :: [[(Symbol, SortedReft)]]  -- Hopefully contain only ANF things+  { icAssms              :: S.HashSet Pred           -- ^ Equalities converted to SMT format+  , icCands              :: S.HashSet Expr           -- ^ "Candidates" for unfolding+  , icEquals             :: EvEqualities             -- ^ Accumulated equalities+  , icSimpl              :: !ConstMap                -- ^ Map of expressions to constants+  , icSubcId             :: Maybe SubcId             -- ^ Current subconstraint ID+  , icANFs               :: [[(Symbol, SortedReft)]] -- Hopefully contain only ANF things+  , icLRWs               :: LocalRewrites            -- ^ Local rewrites+  , icEtaBetaFlag        :: Bool                     -- ^ True if the etabeta flag is turned on, needed+                                                     -- for the eta expansion reasoning as its going to+                                                     -- generate ho constraints+                                                     -- See Note [Eta expansion].+  , icExtensionalityFlag :: Bool                     -- ^ True if the extensionality flag is turned on+  , icLocalRewritesFlag  :: Bool                     -- ^ True if the local rewrites flag is turned on   }  ----------------------------------------------------------------------------------------------@@ -406,18 +423,18 @@ --   to the context. ---------------------------------------------------------------------------------------------- -updCtx :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (ICtx, InstEnv a)-updCtx env@InstEnv{..} ctx delta cidMb-            = ( ctx { icAssms  = S.fromList (filter (not . isTautoPred) ctxEqs)-                    , icCands  = S.fromList cands           <> icCands  ctx-                    , icSimpl  = icSimpl ctx <> econsts-                    , icSubcId = cidMb-                    , icANFs   = bs : icANFs ctx-                    }-              , env-              )+updCtx :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> ICtx+updCtx InstEnv{..} ctx delta cidMb+            = ctx { icAssms  = S.fromList (filter (not . isTautoPred) ctxEqs)+                  , icCands  = S.fromList deANFedCands <> icCands  ctx+                  , icSimpl  = icSimpl ctx <> econsts+                  , icSubcId = cidMb+                  , icANFs   = anfBinds+                  , icLRWs   = mconcat $ icLRWs ctx : newLRWs+                  }   where     cands     = rhs:es+    anfBinds  = bs : icANFs ctx     econsts   = M.fromList $ findConstants ieKnowl es     ctxEqs    = toSMT "updCtx" ieCfg ieSMT [] <$> L.nub                   [ c | xr <- bs, c <- conjuncts (expr xr), null (Vis.kvarsExpr c) ]@@ -425,10 +442,20 @@     rhs       = unApply eRhs     es        = expr <$> bs     eRhs      = maybe PTrue crhs subMb-    binds     = [ (x, y) | i <- delta, let (x, y, _) =  lookupBindEnv i ieBEnv]+    binds     = [ (x, y) | i <- delta, let (x, y, _) = lookupBindEnv i ieBEnv]     subMb     = getCstr ieCstrs <$> cidMb+    newLRWs   = Mb.mapMaybe (`lookupLocalRewrites` ieLRWs) delta +    deANFedCands =+      -- We only call 'deANF' if necessary.+      if not (null (getAutoRws ieKnowl cidMb))+         || icExtensionalityFlag ctx+         || icEtaBetaFlag ctx then+        deANF anfBinds cands+      else+        cands + findConstants :: Knowledge -> [Expr] -> [(Expr, Expr)] findConstants γ es = [(EVar x, c) | (x,c) <- go [] (concatMap splitPAnd es)]   where@@ -452,6 +479,7 @@ -------------------------------------------------------------------------------- data EvalEnv = EvalEnv   { evEnv      :: !SymEnv+  , evElabF    :: ElabFlags     -- | Equalities where we couldn't evaluate the guards   , evPendingUnfoldings :: M.HashMap Expr Expr   , evNewEqualities :: EvEqualities -- ^ Equalities discovered during a traversal of@@ -459,6 +487,9 @@   , evSMTCache :: M.HashMap Expr Bool -- ^ Whether an expression is valid or its negation   , evFuel     :: FuelCount +  -- Eta expansion feature+  , freshEtaNames :: Int -- ^ Keeps track of how many names we generated to perform eta+                         --   expansion, we use this to generate always fresh names   -- REST parameters   , explored   :: Maybe (ExploredTerms RuntimeTerm OCType IO)   , restSolver :: Maybe SolverHandle@@ -478,10 +509,10 @@ type EvalST a = StateT EvalEnv IO a -------------------------------------------------------------------------------- -getAutoRws :: Knowledge -> ICtx -> [AutoRewrite]-getAutoRws γ ctx =+getAutoRws :: Knowledge -> Maybe SubcId -> [AutoRewrite]+getAutoRws γ mSubcId =   Mb.fromMaybe [] $ do-    cid <- icSubcId ctx+    cid <- mSubcId     M.lookup cid $ knAutoRWs γ  -- | Discover the equalities in an expression.@@ -493,8 +524,8 @@ -- way. evalOne :: Knowledge -> ICtx -> Int -> Expr -> EvalST [Expr] evalOne γ ctx i e-  | i > 0 || null (getAutoRws γ ctx) = (:[]) . fst <$> eval γ ctx NoRW e-evalOne γ ctx _ e = do+  | i > 0 || null (getAutoRws γ (icSubcId ctx)) = (:[]) . fst <$> eval γ ctx NoRW e+evalOne γ ctx _ e | isExprRewritable e = do     env <- get     let oc :: OCAlgebra OCType RuntimeTerm IO         oc = evOCAlgebra env@@ -504,6 +535,7 @@     es <- evalREST γ ctx rp     modify $ \st -> st { explored = Just emptyET }     return es+evalOne _ _ _ _ = return []  -- The FuncNormal and RWNormal evaluation strategies are used for REST -- For example, consider the following function:@@ -561,7 +593,6 @@ -- -- Also adds to the monad state all the unfolding equalities that have been -- discovered as necessary.--- eval :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand) eval γ ctx et = go   where@@ -578,20 +609,26 @@             if es /= es'               then return (eApps f es', finalExpand)               else do-                (f', fe)  <- eval γ ctx et f+                (f', fe) <- case dropECst f of+                  EVar _ -> pure (f, noExpand)+                  _      -> go f                 (me', fe') <- evalApp γ ctx f' es et                 return (Mb.fromMaybe (eApps f' es') me', fe <|> fe')        (f, es) ->           do-            (f':es', fe) <- feSeq <$> mapM (eval γ ctx et) (f:es)+            (f', fe1) <- case dropECst f of+              EVar _ -> pure (f, noExpand)+              _      -> go f+            (es', fe2) <- feSeq <$> mapM (eval γ ctx et) es+            let fe = fe1 <|> fe2             (me', fe') <- evalApp γ ctx f' es' et             return (Mb.fromMaybe (eApps f' es') me', fe <|> fe')      go (PAtom r e1 e2) = binOp (PAtom r) e1 e2-    go (ENeg e)         = do (e', fe)  <- eval γ ctx et e+    go (ENeg e)         = do (e', fe)  <- go e                              return (ENeg e', fe)-    go (EBin o e1 e2)   = do (e1', fe1) <- eval γ ctx et e1-                             (e2', fe2) <- eval γ ctx et e2+    go (EBin o e1 e2)   = do (e1', fe1) <- go e1+                             (e2', fe2) <- go e2                              return (EBin o e1' e2', fe1 <|> fe2)     go (ETApp e t)      = mapFE (`ETApp` t) <$> go e     go (ETAbs e s)      = mapFE (`ETAbs` s) <$> go e@@ -603,7 +640,7 @@     go e | EVar _ <- dropECst e = do       (me', fe) <- evalApp γ ctx e [] et       return (Mb.fromMaybe e me', fe)-    go (ECst e t)       = do (e', fe) <- eval γ ctx et e+    go (ECst e t)       = do (e', fe) <- go e                              return (ECst e' t, fe)     go e                = return (e, noExpand) @@ -620,9 +657,34 @@ -- | 'evalELamb' produces equations that preserve the context of a rewrite -- so equations include any necessary lambda bindings. evalELam :: Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (Expr, FinalExpand)+evalELam γ ctx et (x, s) e+  | not $ isEtaSymbol x = do+    -- We need to refresh it as for some reason names bound by lambdas+    -- present in the source code are getting declared twice.+    -- Maybe we should define a new type of identifier for this kind of fresh+    -- variables and not reuse the etabeta ones.+    [ xFresh ] <- makeFreshEtaNames 1+    let newBody = subst (mkSubst [(x, EVar xFresh)]) e++    modify $ \st -> st+      { evNewEqualities+        = S.insert (ELam (x, s) e, ELam (xFresh, s) newBody)+                   (evNewEqualities st)+      }++    evalELam γ ctx et (xFresh, s) newBody+  where+    isEtaSymbol :: Symbol -> Bool+    isEtaSymbol = isPrefixOfSym "eta"+ evalELam γ ctx et (x, s) e = do     oldPendingUnfoldings <- gets evPendingUnfoldings     oldEqs <- gets evNewEqualities++    -- We need to declare the variable in the environment+    modify $ \st -> st+      { evEnv = insertSymEnv x s $ evEnv st }+     (e', fe) <- eval (γ { knLams = (x, s) : knLams γ }) ctx et e     let e2' = simplify γ ctx e'         elam = ELam (x, s) e@@ -630,8 +692,10 @@     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, fe)+    return (ELam (x, s) e', fe)  data RESTParams oc = RP   { oc   :: OCAlgebra oc Expr IO@@ -639,11 +703,64 @@   , c    :: oc   } --- Reverse the ANF transformation-deANF :: ICtx -> Expr -> Expr-deANF ctx = inlineInExpr (`HashMap.Lazy.lookup` undoANF id bindEnv)+-- An expression is rewritable if it is in the domain of+-- Language.Fixpoint.Solver.Rewrite.convert+isExprRewritable :: Expr -> Bool+isExprRewritable (EIte i t e ) = isExprRewritable i && isExprRewritable t && isExprRewritable e+isExprRewritable (EApp f e) = isExprRewritable f && isExprRewritable e+isExprRewritable (EVar _) = True+isExprRewritable (PNot e) = isExprRewritable e+isExprRewritable (PAnd es) = all isExprRewritable es+isExprRewritable (POr es) = all isExprRewritable es+isExprRewritable (PAtom _ l r) = isExprRewritable l && isExprRewritable r+isExprRewritable (EBin _ l r) = isExprRewritable l && isExprRewritable r+isExprRewritable (ECon _) = True+isExprRewritable (ESym _) = True+isExprRewritable (ECst _ _) = True+isExprRewritable (PIff e0 e1) = isExprRewritable (PAtom Eq e0 e1)+isExprRewritable (PImp e0 e1) = isExprRewritable (POr [PNot e0, e1])+isExprRewritable _ = False++-- | Reverse the ANF transformation+--+-- This is necessary for REST rewrites, beta reduction, and PLE to discover+-- redexes.+--+-- In the case of REST, ANF bindings could hide compositions that are+-- rewriteable. For instance,+--+-- > let anf1 = map g x+-- >  in map f anf1+--+-- could miss a rewrite like @map f (map g x) ~> map (f . g) x@.+--+-- Similarly, ANF bindings could miss beta reductions. For instance,+--+-- > let anf1 = \a b -> b+-- >  in anf1 x y+--+-- could only be reduced by PLE if @anf1@ is inlined.+--+-- Lastly, in the following example PLE cannot unfold @reflectedFun@ unless the+-- ANF binding is inlined.+--+-- > f g = g 0+-- > reflectedFun x y = if y == 0 then x else y+-- >+-- > let anf2 = (\eta1 -> reflectedFun x eta1)+-- >  in f anf2+--+-- unfolding @f@+--+-- > let anf2 = (\eta1 -> reflectedFun x eta1)+-- >  in anf2 0+--+deANF :: [[(Symbol, SortedReft)]] -> [Expr] -> [Expr]+deANF binds = map $ inlineInExpr (`HashMap.Lazy.lookup` bindEnv)   where-    bindEnv = HashMap.Lazy.unions $ map HashMap.Lazy.fromList $ icANFs ctx+    bindEnv = undoANF id+        $ HashMap.Lazy.filterWithKey (\sym _ -> anfPrefix `isPrefixOfSym` sym)+        $ HashMap.Lazy.unions $ map HashMap.Lazy.fromList binds  -- | -- Adds to the monad state all the subexpressions that have been rewritten@@ -676,47 +793,54 @@  evalRESTWithCache cacheRef γ ctx acc rp =   do-    Just exploredTerms <- gets explored-    se <- liftIO (shouldExploreTerm exploredTerms exprs)-    if se then do-      possibleRWs <- getRWs-      rws <- notVisitedFirst exploredTerms <$> filterM (liftIO . allowed) possibleRWs-      oldEqualities <- gets evNewEqualities-      modify $ \st -> st { evNewEqualities = mempty }+    mexploredTerms <- gets explored+    case mexploredTerms of+      Nothing -> return acc+      Just exploredTerms -> do+        se <- liftIO (shouldExploreTerm exploredTerms exprs)+        if se then do+          possibleRWs <- getRWs+          rws <- notVisitedFirst exploredTerms <$> filterM (liftIO . allowed) possibleRWs+          oldEqualities <- gets evNewEqualities+          modify $ \st -> st { evNewEqualities = mempty } -      -- liftIO $ putStrLn $ (show $ length possibleRWs) ++ " rewrites allowed at path length " ++ (show $ (map snd $ path rp))-      (e', FE fe) <- do-        r@(ec, _) <- eval γ ctx FuncNormal exprs-        if ec /= exprs-          then return r-          else eval γ ctx RWNormal exprs+          -- liftIO $ putStrLn $ (show $ length possibleRWs) ++ " rewrites allowed at path length " ++ (show $ (map snd $ path rp))+          (e', FE fe) <- do+            r@(ec, _) <- eval γ ctx FuncNormal exprs+            if ec /= exprs+              then return r+              else eval γ ctx RWNormal exprs -      let evalIsNewExpr = e' `L.notElem` pathExprs-      let exprsToAdd    = [e' | evalIsNewExpr]  ++ map (\(_, e, _) -> e) rws-          acc' = exprsToAdd ++ acc-          eqnToAdd = [ (e1, simplify γ ctx e2) | ((e1, e2), _, _) <- rws ]+          let evalIsNewExpr = e' `L.notElem` pathExprs+          let exprsToAdd    = [e' | evalIsNewExpr]  ++ map (\(_, e, _) -> e) rws+              acc' = exprsToAdd ++ acc+              eqnToAdd = [ (e1, simplify γ ctx e2) | ((e1, e2), _, _) <- rws ] -      newEqualities <- gets evNewEqualities-      smtCache <- liftIO $ readIORef cacheRef-      modify (\st ->-             st { evNewEqualities  = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd-                , evSMTCache = smtCache-                , explored = Just $ ExploredTerms.insert-                  (Rewrite.convert exprs)-                  (c rp)-                  (S.insert (Rewrite.convert e') $ S.fromList (map (Rewrite.convert . (\(_, e, _) -> e)) possibleRWs))-                  (Mb.fromJust $ explored st)-                })+          let explored' st =+                if isExprRewritable e' && isExprRewritable exprs+                  then Just $ ExploredTerms.insert (Rewrite.convert exprs) (c rp)+                                                  (S.insert (Rewrite.convert e')+                            $ S.fromList (map (Rewrite.convert . (\(_, e, _) -> e)) possibleRWs))+                                        (Mb.fromJust $ explored st)+                  else Nothing -      acc'' <- if evalIsNewExpr-        then if fe && any isRW (path rp)-          then (:[]) . fst <$> eval γ (addConst (exprs, e')) NoRW e'-          else evalRESTWithCache cacheRef γ (addConst (exprs, e')) acc' (rpEval newEqualities e')-        else return acc'+          newEqualities <- gets evNewEqualities+          smtCache <- liftIO $ readIORef cacheRef+          modify $ \st -> st+            { evNewEqualities  = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd+            , evSMTCache = smtCache+            , explored = explored' st+            } -      foldM (\r rw -> evalRESTWithCache cacheRef γ ctx r (rpRW rw)) acc'' rws-     else-      return acc+          acc'' <- if evalIsNewExpr+            then if fe && any isRW (path rp)+              then (:[]) . fst <$> eval γ (addConst (exprs, e')) NoRW e'+              else evalRESTWithCache cacheRef γ (addConst (exprs, e')) acc' (rpEval newEqualities e')+            else return acc'++          foldM (\r rw -> evalRESTWithCache cacheRef γ ctx r (rpRW rw)) acc'' rws+        else+          return acc   where     shouldExploreTerm exploredTerms e | Vis.isConc e =       case rwTerminationOpts rwArgs of@@ -752,7 +876,7 @@      pathExprs       = map fst (mytracepp "EVAL2: path" $ path rp)     exprs           = last pathExprs-    autorws         = getAutoRws γ ctx+    autorws         = getAutoRws γ (icSubcId ctx)      rwArgs = RWArgs (isValid cacheRef γ) $ knRWTerminationOpts γ @@ -767,15 +891,58 @@         if ok           then             do-              let e'         = deANF ctx exprs               let getRW e ar = Rewrite.getRewrite (oc rp) rwArgs (c rp) e ar               let getRWs' s  = Mb.catMaybes <$> mapM (liftIO . runMaybeT . getRW s) autorws-              concat <$> mapM getRWs' (subExprs e')+              concat <$> mapM getRWs' (subExprs exprs)           else return []      addConst (e,e') = if isConstant (knDCs γ) e'                       then ctx { icSimpl = M.insert e e' $ icSimpl ctx} else ctx +-- Note [Eta expansion]+-- ~~~~~~~~~~~~~~~~~~~~+--+-- Without eta expansion PLE could not prove that terms @f@ and @(\x -> f x)@+-- have the same meaning. But sometimes we want to rewrite @f@ into the+-- expanded form, in order to unfold @f@.+--+-- For instance, suppose we have a function @const@ defined as:+--+-- > define f (x : int, y : int) : int = {(x)}+--+-- And we need to prove some constraint of this shape+--+-- > { const a = \x:Int -> a }+--+-- At first, PLE cannot unfold @const@ since it is not fully applied.+-- But if instead perform eta expansion on the left hand side we obtain the+-- following equality+--+-- > { \y:Int -> const a y = \x:Int -> a}+--+-- And now PLE can unfold @const@ as the application is saturated+--+-- > { \y:Int -> a = \x:Int -> a}+--+-- We need the higerorder flag active as we are generating lambdas in+-- the equalities.+++-- Note [Elaboration for eta expansion]+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~+--+-- Eta expansion needs to determine the arity and the type of arguments of a+-- function. For this sake, we make sure that when unfolding introduces new+-- expressions, these expressions get annotated with their types by calling+-- @elaborateExpr@.+--+-- This elaboration cannot be done ahead of time on equations, because then+-- type variables are instantiated to rigid constants that cannot be unified.+-- For instance, @id :: forall a. a -> a@ would be elaborated to+-- @id :: a#1 -> a#1@, and when used in an expression like @id True@, @a#1@+-- would not unify with @Bool@.++ -- | @evalApp kn ctx e es@ unfolds expressions in @eApps e es@ using rewrites -- and equations evalApp :: Knowledge -> ICtx -> Expr -> [Expr] -> EvalType -> EvalST (Maybe Expr, FinalExpand)@@ -784,38 +951,37 @@   , Just eq <- Map.lookup f (knAms γ)   , length (eqArgs eq) <= length es   = do-       env  <- gets (seSort . evEnv)+       env <- gets (seSort . evEnv)        okFuel <- checkFuel f-       if okFuel && et /= FuncNormal-         then do-                let (es1,es2) = splitAt (length (eqArgs eq)) es-                    newE = substEq env eq es1-                (e', fe) <- evalIte γ ctx et newE -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter-                let e2' = stripPLEUnfold e'-                    e3' = simplify γ ctx (eApps e2' es2) -- reduces a bit the equations-                    undecidedGuards = case e' of-                      EIte{} -> True-                      _ -> False+       if okFuel && et /= FuncNormal then do+         let (es1, es2) = splitAt (length (eqArgs eq)) es+         -- See Note [Elaboration for eta expansion].+         let newE = substEq env eq es1+         newE' <- if icEtaBetaFlag ctx+                    then elaborateExpr "EvalApp unfold full: " newE+                    else pure newE -                if undecidedGuards-                  then do-                    modify $ \st ->-                      st {-                        evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)-                      }-                    -- Don't unfold the expression if there is an if-then-else-                    -- guarding it, just to preserve the size of further-                    -- rewrites.-                    return (Nothing, noExpand)-                  else do-                    useFuel f-                    modify $ \st ->-                      st-                        { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)-                        , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)-                        }-                    return (Just e2', fe)-         else return (Nothing, noExpand)+         (e', fe) <- evalIte γ ctx et newE'        -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter+         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+           -- 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+           modify $ \st -> st+             { evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)+             }+           return (Nothing, noExpand)+         else do+           useFuel f+           modify $ \st -> st+             { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)+             , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)+             }+           return (Just $ eApps e2' es2, fe)+       else return (Nothing, noExpand)   where     -- At the time of writing, any function application wrapping an     -- if-statement would have the effect of unfolding the invocation.@@ -829,6 +995,12 @@       = arg       | otherwise = e +    hasUndecidedGuard EIte{} = True+    hasUndecidedGuard _ = False++    guardOf (EIte g _ _) = Just g+    guardOf _ = Nothing+ evalApp γ ctx e0 args@(e:es) _   | EVar f <- dropECst e0   , (d, as) <- splitEAppThroughECst e@@ -841,10 +1013,8 @@   = do     let newE = eApps (subst (mkSubst $ zip (smArgs rw) as) (smBody rw)) es     when (isUserDataSMeasure == NoUserDataSMeasure) $-      modify $ \st ->-        st { evNewEqualities =-               S.insert (eApps e0 args, simplify γ ctx newE) (evNewEqualities st)-           }+      modify $ \st -> st+        { evNewEqualities = S.insert (eApps e0 args, simplify γ ctx newE) (evNewEqualities st) }     return (Just newE, noExpand)  evalApp γ ctx e0 es _et@@ -855,12 +1025,87 @@          st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }        return (Nothing, noExpand) -evalApp _ _ _e _es _-  = return (Nothing, noExpand)+evalApp γ ctx e0 es et+  | ELam (argName, _) body <- dropECst e0+  , lambdaArg:remArgs <- es+  , icEtaBetaFlag ctx || icExtensionalityFlag ctx+  = do+      isFuelOk <- checkFuel argName+      if isFuelOk+        then do+          useFuel argName+          let argSubst = mkSubst [(argName, lambdaArg)]+          let body' = subst argSubst body+          (body'', fe) <- evalIte γ ctx et body'+          let simpBody = simplify γ ctx (eApps body'' remArgs)+          modify $ \st ->+            st { evNewEqualities = S.insert (eApps e0 es, simpBody) (evNewEqualities st) }+          return (Just $ eApps body'' remArgs, fe)+        else do+          return (Nothing, noExpand) +evalApp _ ctx e0 es _+  | icLocalRewritesFlag ctx+  , EVar f <- dropECst e0+  , Just rw <- lookupRewrite f $ icLRWs ctx+  = do+      -- expandedTerm <- elaborateExpr "EvalApp rewrite local:" $ eApps rw es+      let expandedTerm = eApps rw es+      modify $ \st -> st+        { evNewEqualities = S.insert (eApps e0 es, expandedTerm) (evNewEqualities st) }+      return (Just expandedTerm, expand)++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+  -- we have an uninterpreted function @f@, and we want to prove that+  -- @f == \a -> f a@. We can use eta expansion on the left-hand side to prove+  -- this.+  --+  -- Second, we need the type of the new arguments, which for some reason are+  -- sometimes instantiated in the equations to rigid types that we cannot+  -- instantiate to the types needed at the call site.+  -- See Note [Elaboration for eta expansion].+  --+  -- See Note [Eta expansion].+  --+  | ECst (EVar _f) sortAnnotation@FFunc{} <- e0+  , icEtaBetaFlag ctx+  , let expectedArgs = unpackFFuncs sortAnnotation+  , let nProvidedArgs = length es+  , let nArgsMissing = length expectedArgs - nProvidedArgs+  , nArgsMissing > 0+  = do+    let etaArgsType = drop nProvidedArgs expectedArgs+    -- Fresh names for the eta expansion+    etaNames <- makeFreshEtaNames nArgsMissing++    let etaVars = zipWith (\name ty -> ECst (EVar name) ty) etaNames etaArgsType+    let fullBody = eApps e0 (es ++ etaVars)+    let etaExpandedTerm = mkLams fullBody (zip etaNames etaArgsType)++    -- Note: we should always add the equality as etaNames is always non empty because the+    -- only way for etaNames to be empty is if the function is fully applied, but that case+    -- is already handled by the previous case of evalApp+    modify $ \st -> st+      { evNewEqualities = S.insert (eApps e0 es, etaExpandedTerm) (evNewEqualities st) }+    return (Just etaExpandedTerm, expand)+  where+    unpackFFuncs (FFunc t ts) = t : unpackFFuncs ts+    unpackFFuncs _ = []++    mkLams subject binds = foldr ELam subject binds++evalApp _ _ctx _e0 _es _ = do+  return (Nothing, noExpand)+ -- | Evaluates if-then-else statements until they can't be evaluated anymore -- or some other expression is found. evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)+evalIte γ ctx et (ECst e t) = do+  (e', fe) <- evalIte γ ctx et e+  return (ECst e' t, fe) evalIte γ ctx et (EIte i e1 e2) = do       (b, _) <- eval γ ctx et i       b'  <- mytracepp ("evalEIt POS " ++ showpp (i, b)) <$> isValidCached γ b@@ -892,7 +1137,7 @@   where su = mkSubst $ zip (eqArgNames eq) es  substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr-substEqCoerce env eq es = Vis.applyCoSub coSub $ eqBody eq+substEqCoerce env eq es = Vis.applyCoSubV coSub $ eqBody eq   where     ts    = snd    <$> eqArgs eq     sp    = panicSpan "mkCoSub"@@ -904,18 +1149,20 @@ -- -- The variables in the domain of the substitution are those that appear -- as @FObj symbol@ in @xTs@.-mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub+mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSubV mkCoSub env eTs xTs = M.fromList [ (x, unite ys) | (x, ys) <- Misc.groupList xys ]   where     unite ts    = Mb.fromMaybe (uError ts) (unifyTo1 symToSearch ts)     symToSearch = mkSearchEnv env     uError ts   = panic ("mkCoSub: cannot build CoSub for " ++ showpp xys ++ " cannot unify " ++ showpp ts)+    xys :: [(Sort, Sort)]     xys         = Misc.sortNub $ concat $ zipWith matchSorts xTs eTs -matchSorts :: Sort -> Sort -> [(Symbol, Sort)]+matchSorts :: Sort -> Sort -> [(Sort, Sort)] matchSorts = go   where-    go (FObj x)      {-FObj-} y    = [(x, y)]+    go x@(FObj _)    {-FObj-} y    = [(x, y)]+    go x@(FVar _)    {-FObj-} y    = [(x, y)]     go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2     go (FFunc s1 t1) (FFunc s2 t2) = go s1 s2 ++ go t1 t2     go (FApp s1 t1)  (FApp s2 t2)  = go s1 s2 ++ go t1 t2@@ -1206,6 +1453,21 @@   where     k             = M.lookupDefault 0 f m     m             = fcMap fc++makeFreshEtaNames :: Int -> EvalST [Symbol]+makeFreshEtaNames n = replicateM n makeFreshName+  where+    makeFreshName = do+      ident <- gets freshEtaNames+      modify $ \st -> st { freshEtaNames = 1 + freshEtaNames st }+      pure $ etaExpSymbol ident++elaborateExpr :: String -> Expr -> EvalST Expr+elaborateExpr msg e = do+  let elabSpan = atLoc dummySpan msg+  symEnv' <- gets evEnv+  ef <- gets evElabF+  pure $ unApply $ elaborate (ElabParam ef elabSpan symEnv') e  -- | Returns False if there is a fuel count in the evaluation environment and -- the fuel count exceeds the maximum. Returns True otherwise.

@@ -38,7 +38,7 @@   ) import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Refinements-  ( Expr(..)+  ( ExprV(..)   , pattern PFalse   , Reft   , SortedReft(..)

@@ -89,6 +89,8 @@     asFuel _        = undefined  +-- Note: if you change the domain of this function, you need to change+-- also Language.Fixpoint.Solver.PLE.isExprRewritable convert :: Expr -> RT.RuntimeTerm convert (EIte i t e)   = RT.App "$ite" $ map convert [i,t,e] convert e@EApp{}       | (f, terms) <- splitEAppThroughECst e, EVar fName <- dropECst f

@@ -17,15 +17,17 @@  import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Visitor-import           Language.Fixpoint.SortCheck     (elaborate, applySorts, isFirstOrder)+import           Language.Fixpoint.SortCheck     (ElabParam(..), elaborate, applySorts, isFirstOrder) -- import           Language.Fixpoint.Defunctionalize+import           Language.Fixpoint.Misc ((==>)) import qualified Language.Fixpoint.Misc                            as Misc import qualified Language.Fixpoint.Types                           as F-import           Language.Fixpoint.Types.Config (Config)+import           Language.Fixpoint.Types.Config (Config, solverFlags) import qualified Language.Fixpoint.Types.Config as Cfg import qualified Language.Fixpoint.Types.Errors                    as E import qualified Language.Fixpoint.Smt.Theories                    as Thy import           Language.Fixpoint.Graph (kvEdges, CVertex (..))+import qualified Data.Bifunctor as Bifunctor (first) import qualified Data.HashMap.Strict                               as M import qualified Data.HashSet                                      as S import qualified Data.List                                         as L@@ -46,12 +48,10 @@          >=> Misc.fM (dropDeadSubsts . restrictKVarDomain)          >=>         banMixedRhs          >=>         banQualifFreeVars-         >=>         banConstraintFreeVars+         >=>         banConstraintFreeVars cfg          >=> Misc.fM addLiterals          >=> Misc.fM (eliminateEta cfg)-         >=> Misc.fM cancelCoercion - -------------------------------------------------------------------------------- -- | 'dropAdtMeasures' removes all the measure definitions that correspond to --   constructor, selector or test names for declared datatypes, as these are@@ -81,16 +81,6 @@   where     lits'      = M.fromList [ (F.symbol x, F.strSort) | x <- symConsts si ] ---cancelCoercion :: F.SInfo a -> F.SInfo a-cancelCoercion = mapExpr (trans (defaultVisitor { txExpr = go }) () ())-  where-    go _ (F.ECoerc t1 t2 (F.ECoerc t2' t1' e))-      | t1 == t1' && t2 == t2'-      = e-    go _ e = e- -------------------------------------------------------------------------------- -- | `eliminateEta` converts equations of the form f x = g x into f = g --------------------------------------------------------------------------------@@ -162,7 +152,7 @@       splitApp (fvar, arg:args)     fapp' e = pure (e, []) -    theorySymbols = F.notracepp "theorySymbols" $ Thy.theorySymbols $ F.ddecls si+    theorySymbols = F.notracepp "theorySymbols" $ Thy.theorySymbols (Cfg.solver cfg) $ F.ddecls si      splitApp (e, es)       | isNothing $ F.notracepp ("isSmt2App? " ++ showpp e) $ Thy.isSmt2App theorySymbols $ stripCasts e@@ -316,18 +306,18 @@ -------------------------------------------------------------------------------- -- | check that no constraint has free variables (ignores kvars) ---------------------------------------------------------------------------------banConstraintFreeVars :: F.SInfo a -> SanitizeM (F.SInfo a)-banConstraintFreeVars fi0 = Misc.applyNonNull (Right fi0) (Left . badCs) bads+banConstraintFreeVars :: Config -> F.SInfo a -> SanitizeM (F.SInfo a)+banConstraintFreeVars cfg fi0 = Misc.applyNonNull (Right fi0) (Left . badCs) bads   where     fi      = mapKVars (const $ Just F.PTrue) fi0     bads    = [(c, fs) | c <- M.elems $ F.cm fi, Just fs <- [cNoFreeVars fi k c]]-    k       = known fi+    k       = known cfg fi -known :: F.SInfo a -> F.Symbol -> Bool-known fi  = \x -> F.memberSEnv x lits || F.memberSEnv x prims+known :: Config -> F.SInfo a -> F.Symbol -> Bool+known cfg fi  = \x -> F.memberSEnv x lits || F.memberSEnv x prims   where     lits  = F.gLits fi-    prims = Thy.theorySymbols . F.ddecls $ fi+    prims = Thy.theorySymbols (Cfg.solver cfg) . F.ddecls $ fi  cNoFreeVars :: F.SInfo a -> (F.Symbol -> Bool) -> F.SimpC a -> Maybe [F.Symbol] cNoFreeVars fi knownSym c = if S.null fv then Nothing else Just (S.toList fv)@@ -340,7 +330,7 @@     fv   = (`Misc.nubDiff` cDom) . filter (not . knownSym) $ cRng  badCs :: Misc.ListNE (F.SimpC a, [F.Symbol]) -> E.Error-badCs = E.catErrors . map (E.errFreeVarInConstraint . Misc.mapFst F.subcId)+badCs = E.catErrors . map (E.errFreeVarInConstraint . Bifunctor.first F.subcId)  -------------------------------------------------------------------------------- -- | check that every DataDecl is regular@@ -400,12 +390,14 @@ symbolEnv cfg si = F.symEnv sEnv tEnv ds lits (ts ++ ts')   where     ts'          = applySorts ae'-    ae'          = elaborate (F.atLoc E.dummySpan "symbolEnv") env0 (F.ae si)+    ae'          = elaborate (ElabParam ef (F.atLoc E.dummySpan "symbolEnv") env0) (F.ae si)     env0         = F.symEnv sEnv tEnv ds lits ts-    tEnv         = Thy.theorySymbols ds+    tEnv         = Thy.theorySymbols slv ds     ds           = F.ddecls si     ts           = Misc.setNub (applySorts si ++ [t | (_, t) <- F.toListSEnv sEnv])-    sEnv         = F.coerceSortEnv $ (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts+    sEnv         = F.coerceSortEnv ef $ (F.tsSort <$> tEnv) `mappend` F.fromListSEnv xts+    slv          = Cfg.solver cfg+    ef           = solverFlags slv     xts          = symbolSorts cfg si ++ alits     lits         = F.dLits si `F.unionSEnv'` F.fromListSEnv alits     alits        = litsAEnv $ F.ae si@@ -486,10 +478,6 @@   where     ok x t  = M.member x defs ==> (F.allowHO fi || isFirstOrder t)     defs    = M.fromList $ F.toListSEnv $ F.gLits fi--infixl 9 ==>-(==>) :: Bool -> Bool -> Bool-p ==> q = not p || q  -------------------------------------------------------------------------------- -- | Drop irrelevant binders from WfC Environments

@@ -10,7 +10,7 @@     -- * Update Solution   , Sol.update -  -- * Lookup Solution+    -- * Lookup Solution   , lhsPred    , nonCutsResult@@ -19,6 +19,7 @@ import           Control.Parallel.Strategies import           Control.Arrow (second, (***)) import           Control.Monad (void)+import           Control.Monad.Reader import qualified Data.HashSet                   as S import qualified Data.HashMap.Strict            as M import qualified Data.List                      as L@@ -26,6 +27,7 @@ import qualified Data.Bifunctor                 as Bifunctor (second) 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 qualified Language.Fixpoint.Misc               as Misc import           Language.Fixpoint.Types.Config@@ -48,7 +50,7 @@ -------------------------------------------------------------------------------- init cfg si ks_ = Sol.fromList symEnv mempty keqs [] mempty ebs xEnv   where-    keqs       = map (refine si qcs genv) ws `using` parList rdeepseq+    keqs       = runReader (traverse (refine si qcs genv) ws) (solverFlags $ solver cfg) `using` parList rdeepseq     qcs        = {- trace ("init-qs-size " ++ show (length ws, length qs_, M.keys qcs_)) $ -} qcs_     qcs_       = mkQCluster qs_     qs_        = F.quals si@@ -80,7 +82,7 @@  -------------------------------------------------------------------------------- -refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> (F.KVar, Sol.QBind)+refine :: F.SInfo a -> QCluster -> F.SEnv F.Sort -> F.WfC a -> ElabM (F.KVar, Sol.QBind) refine info qs genv w = refineK (allowHOquals info) env qs (F.wrft w)   where     env             = wenvSort <> genv@@ -92,11 +94,13 @@     notLit    = not . F.isLitSymbol . fst  -refineK :: Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> (F.KVar, Sol.QBind)-refineK ho env qs (v, t, k) = F.notracepp _msg (k, eqs')+refineK :: Bool -> F.SEnv F.Sort -> QCluster -> (F.Symbol, F.Sort, F.KVar) -> ElabM (F.KVar, Sol.QBind)+refineK ho env qs (v, t, k) =+  do eqs' <- Sol.qbFilterM (okInst env v t) eqs+     pure $ F.notracepp _msg (k, eqs')    where     eqs                     = instK ho env v t qs-    eqs'                    = Sol.qbFilter (okInst env v t) eqs+     _msg                    = printf "\n\nrefineK: k = %s, eqs = %s" (F.showpp k) (F.showpp eqs)  --------------------------------------------------------------------------------@@ -231,13 +235,15 @@   = p  ---------------------------------------------------------------------------------okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> Bool+okInst :: F.SEnv F.Sort -> F.Symbol -> F.Sort -> Sol.EQual -> ElabM Bool ---------------------------------------------------------------------------------okInst env v t eq = isNothing tc+okInst env v t eq =+  do tc <- So.checkSorted (F.srcSpan eq) env sr+     pure $ isNothing tc   where     sr            = F.RR t (F.Reft (v, p))     p             = Sol.eqPred eq-    tc            = So.checkSorted (F.srcSpan eq) env sr+     -- _msg          = printf "okInst: t = %s, eq = %s, env = %s" (F.showpp t) (F.showpp eq) (F.showpp env)  @@ -251,8 +257,10 @@   -> F.BindEnv a   -> Sol.Solution   -> F.SimpC a-  -> F.Expr-lhsPred bindingsInSmt be s c = F.notracepp _msg $ fst $ apply g s bs+  -> ElabM F.Expr+lhsPred bindingsInSmt be s c =+  do ap <- apply g s bs+     pure $ F.notracepp _msg $ fst ap   where     g          = CEnv ci be bs (F.srcSpan c) bindingsInSmt     bs         = F.senv c@@ -276,49 +284,54 @@ type Cid         = Maybe Integer type ExprInfo    = (F.Expr, KInfo) -apply :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ExprInfo-apply g s bs      = (F.conj (pks:ps), kI)   -- see [NOTE: pAnd-SLOW]-  where-    -- Clear the "known" bindings for applyKVars, since it depends on-    -- using the fully expanded representation of the predicates to bind their-    -- variables with quantifiers.-    (pks, kI)     = applyKVars g {ceBindingsInSmt = F.emptyIBindEnv} s ks-    (ps,  ks, _)  = envConcKVars g s bs+apply :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ElabM ExprInfo+apply g s bs      =+  -- Clear the "known" bindings for applyKVars, since it depends on+  -- using the fully expanded representation of the predicates to bind their+  -- variables with quantifiers.+  do (ps,  ks, _) <- envConcKVars g s bs+     (pks, kI) <- applyKVars g {ceBindingsInSmt = F.emptyIBindEnv} s ks+     pure (F.conj (pks:ps), kI)   -- see [NOTE: pAnd-SLOW]  -envConcKVars :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ([F.Expr], [F.KVSub], [F.KVSub])-envConcKVars g s bs = (concat pss, concat kss, L.nubBy (\x y -> F.ksuKVar x == F.ksuKVar y) $ concat gss)+envConcKVars :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.IBindEnv -> ElabM ([F.Expr], [F.KVSub], [F.KVSub])+envConcKVars g s bs =+  do xrs <- traverse (lookupBindEnvExt g s) is+     let (pss, kss, gss) = unzip3 [ F.notracepp ("sortedReftConcKVars" ++ F.showpp sr) $ F.sortedReftConcKVars x sr | (x, sr) <- xrs ]+     pure (concat pss, concat kss, L.nubBy (\x y -> F.ksuKVar x == F.ksuKVar y) $ concat gss)   where-    (pss, kss, gss) = unzip3 [ F.notracepp ("sortedReftConcKVars" ++ F.showpp sr) $ F.sortedReftConcKVars x sr | (x, sr) <- xrs ]-    xrs             = lookupBindEnvExt g s <$> is-    is              = F.elemsIBindEnv bs+    is = F.elemsIBindEnv bs -lookupBindEnvExt :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> (F.Symbol, F.SortedReft)-lookupBindEnvExt g s i-  | Just p <- ebSol g {ceBindingsInSmt = F.emptyIBindEnv} s i = (x, sr { F.sr_reft = F.Reft (x, p) })-  | F.memberIBindEnv i (ceBindingsInSmt g) =-      (x, sr { F.sr_reft = F.Reft (x, F.EVar (F.bindSymbol (fromIntegral i)))})-  | otherwise             = (x, sr)+lookupBindEnvExt :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> ElabM (F.Symbol, F.SortedReft)+lookupBindEnvExt g s i =+  do msol <- ebSol (g {ceBindingsInSmt = F.emptyIBindEnv}) s i+     pure (x, case msol of+                Just p -> sr { F.sr_reft = F.Reft (x, p) }+                Nothing -> if F.memberIBindEnv i (ceBindingsInSmt g)+                              then sr { F.sr_reft = F.Reft (x, F.EVar (F.bindSymbol (fromIntegral i)))}+                              else sr)    where       (x, sr, _)              = F.lookupBindEnv i (ceBEnv g) -ebSol :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> Maybe F.Expr-ebSol g sol bindId = case  M.lookup bindId sebds of-  Just (Sol.EbSol p)    -> Just p-  Just (Sol.EbDef cs _) -> Just $ F.PAnd (cSol <$> cs)-  _                     -> Nothing+ebSol :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.BindId -> ElabM (Maybe F.Expr)+ebSol g sol bindId = case M.lookup bindId sebds of+  Just (Sol.EbSol p)    -> pure $ Just p+  Just (Sol.EbDef cs _) ->+    do let cSol c = if sid c == ceCid g+                       then pure F.PFalse+                       else do p <- ebindReft g s' c+                               pure $ exElim (Sol.sxEnv s') (senv c) bindId p+       exps <- traverse cSol cs+       pure $ Just $ F.PAnd exps+  _                     -> pure Nothing   where     sebds = Sol.sEbd sol--    ebReft s (i,c) = exElim (Sol.sxEnv s) (senv c) i (ebindReft g s c)-    cSol c = if sid c == ceCid g-                then F.PFalse-                else ebReft s' (bindId, c)-     s' = sol { Sol.sEbd = M.insert bindId Sol.EbIncr sebds } -ebindReft :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.SimpC () -> F.Pred-ebindReft g s c = F.pAnd [ fst $ apply g' s bs, F.crhs c ]+ebindReft :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.SimpC () -> ElabM F.Pred+ebindReft g s c =+  do a <- apply g' s bs+     pure $ F.pAnd [ fst a , F.crhs c ]   where     g'          = g { ceCid = sid c, ceIEnv = bs }     bs          = F.senv c@@ -332,23 +345,28 @@                             , xi < yi                             , yi `F.memberIBindEnv` ienv                  ] -applyKVars :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> [F.KVSub] -> ExprInfo-applyKVars g s = mrExprInfos (applyKVar g s) F.pAndNoDedup mconcat+applyKVars :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> [F.KVSub] -> ElabM ExprInfo+applyKVars g s ks =+  mrExprInfosM (applyKVar g s) F.pAndNoDedup mconcat ks -applyKVar :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> ExprInfo+applyKVar :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> ElabM ExprInfo applyKVar g s ksu = case Sol.lookup s (F.ksuKVar ksu) of   Left cs   -> hypPred g s ksu cs-  Right eqs -> (F.pAndNoDedup $ fst <$> Sol.qbPreds msg s (F.ksuSubst ksu) eqs, mempty) -- TODO: don't initialize kvars that have a hyp solution+  Right eqs -> do qbp <- Sol.qbPreds msg s (F.ksuSubst ksu) eqs+                  pure (F.pAndNoDedup $ fst <$> qbp, mempty) -- TODO: don't initialize kvars that have a hyp solution   where     msg     = "applyKVar: " ++ show (ceCid g) -nonCutsResult :: F.BindEnv ann -> Sol.Sol a Sol.QBind -> M.HashMap F.KVar F.Expr-nonCutsResult be s =-  let g = CEnv Nothing be F.emptyIBindEnv F.dummySpan F.emptyIBindEnv-   in M.mapWithKey (mkNonCutsExpr g) $ Sol.sHyp s+mkNonCutsExpr :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Hyp -> ElabM F.Expr+mkNonCutsExpr ce s k cs = do bcps <- traverse (bareCubePred ce s k) cs+                             pure $ F.pOr bcps++nonCutsResult :: F.BindEnv ann -> Sol.Sol a Sol.QBind -> ElabM (M.HashMap F.KVar F.Expr)+nonCutsResult be s = M.traverseWithKey (mkNonCutsExpr g s) $ Sol.sHyp s   where-    mkNonCutsExpr g k cs = F.pOr $ map (bareCubePred g s k) cs+    g = CEnv Nothing be F.emptyIBindEnv F.dummySpan F.emptyIBindEnv + -- | Produces a predicate from a constraint defining a kvar. -- -- This is written in imitation of 'cubePred'. However, there are some@@ -366,20 +384,23 @@ --    particular use of the KVar. Thus @cubePred@ produces a different --    expression for every use site of the kvar, while here we produce one --    expression for all the uses.-bareCubePred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Cube -> F.Expr+bareCubePred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVar -> Sol.Cube -> ElabM F.Expr bareCubePred g s k c =-  let bs = Sol.cuBinds c-      su = Sol.cuSubst c-      g' = addCEnv  g bs-      bs' = delCEnv s k bs-      yts = symSorts g bs'-      sEnv = F.seSort (Sol.sEnv s)-      (xts, psu) = substElim (Sol.sEnv s) sEnv g' k su-      (p, _kI) = apply g' s bs'-   in F.pExist (xts ++ yts) (psu &.& p)+  do (xts, psu) <- substElim (Sol.sEnv s) sEnv g' k su+     (p, _kI) <- apply g' s bs'+     pure $ F.pExist (xts ++ yts) (psu &.& p)+  where+    bs = Sol.cuBinds c+    su = Sol.cuSubst c+    g' = addCEnv  g bs+    bs' = delCEnv s k bs+    yts = symSorts g bs'+    sEnv = F.seSort (Sol.sEnv s) -hypPred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp  -> ExprInfo-hypPred g s ksu hyp = F.pOr *** mconcatPlus $ unzip $ cubePred g s ksu <$> hyp+hypPred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Hyp -> ElabM ExprInfo+hypPred g s ksu hyp =+  do cs <- traverse (cubePred g s ksu) hyp+     pure $ F.pOr *** mconcatPlus $ unzip cs  {- | `cubePred g s k su c` returns the predicate for @@ -396,21 +417,25 @@   -} -elabExist :: F.SrcSpan -> Sol.Sol a Sol.QBind -> [(F.Symbol, F.Sort)] -> F.Expr -> F.Expr-elabExist sp s xts p = F.pExist xts' p+elabExist :: F.SrcSpan -> Sol.Sol a Sol.QBind -> [(F.Symbol, F.Sort)] -> F.Expr -> ElabM F.Expr+elabExist sp s xts p =+  do ef <- ask+     let elab = So.elaborate (So.ElabParam ef (F.atLoc sp "elabExist") env)+     let xts' = [ (x, elab t) | (x, t) <- xts]+     pure $ F.pExist xts' p   where-    xts'        = [ (x, elab t) | (x, t) <- xts]-    elab        = So.elaborate (F.atLoc sp "elabExist") env-    env         = Sol.sEnv s+    env = Sol.sEnv s -cubePred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> ExprInfo-cubePred g s ksu c    = (F.notracepp "cubePred" $ elabExist sp s xts (psu &.& p), kI)+cubePred :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> ElabM ExprInfo+cubePred g s ksu c    =+  do ((xts,psu,p), kI) <- cubePredExc g s ksu c bs'+     e <- F.notracepp "cubePred" <$> elabExist sp s xts (psu &.& p)+     pure (e , kI)   where-    sp                = F.srcSpan g-    ((xts,psu,p), kI) = cubePredExc g s ksu c bs'-    bs'               = delCEnv s k bs-    bs                = Sol.cuBinds c-    k                 = F.ksuKVar ksu+    sp  = F.srcSpan g+    bs' = delCEnv s k bs+    bs  = Sol.cuBinds c+    k   = F.ksuKVar ksu  type Binders = [(F.Symbol, F.Sort)] @@ -419,17 +444,19 @@ --   we want is `Exists xts. (psu /\ p)`.  cubePredExc :: CombinedEnv ann -> Sol.Sol a Sol.QBind -> F.KVSub -> Sol.Cube -> F.IBindEnv-            -> ((Binders, F.Pred, F.Pred), KInfo)--cubePredExc g s ksu c bs' = (cubeP, extendKInfo kI (Sol.cuTag c))+            -> ElabM ((Binders, F.Pred, F.Pred), KInfo)+cubePredExc g s ksu c bs' =+  do (xts, psu)  <- substElim (Sol.sEnv s) sEnv g  k su+     (_  , psu') <- substElim (Sol.sEnv s) sEnv g' k su'+     (p', kI)    <- apply g' s bs'+     cubeE       <- elabExist sp s yts' (F.pAndNoDedup [p', psu'])+     let cubeP = (xts, psu, cubeE)+     pure (cubeP, extendKInfo kI (Sol.cuTag c))   where-    cubeP           = (xts, psu, elabExist sp s yts' (F.pAndNoDedup [p', psu']) )+     sp              = F.srcSpan g     yts'            = symSorts g bs'     g'              = addCEnv  g bs-    (p', kI)        = apply g' s bs'-    (_  , psu')     = substElim (Sol.sEnv s) sEnv g' k su'-    (xts, psu)      = substElim (Sol.sEnv s) sEnv g  k su     su'             = Sol.cuSubst c     bs              = Sol.cuBinds c     k               = F.ksuKVar   ksu@@ -462,37 +489,41 @@      2. are binders corresponding to sorts (e.g. `a : num`, currently used         to hack typeclasses current.)  -}-substElim :: F.SymEnv -> F.SEnv F.Sort -> CombinedEnv a -> F.KVar -> F.Subst -> ([(F.Symbol, F.Sort)], F.Pred)-substElim syEnv sEnv g _ (F.Su m) = (xts, p)+substElim :: F.SymEnv -> F.SEnv F.Sort -> CombinedEnv a -> F.KVar -> F.Subst -> ElabM ([(F.Symbol, F.Sort)], F.Pred)+substElim syEnv sEnv g _ (F.Su m) =+    do p <- traverse (\(x, e ,t) -> mkSubst sp syEnv x (substSort sEnv x) e t) xets+       pure (xts, F.pAnd p)   where-    p      = F.pAnd [ mkSubst sp syEnv x (substSort sEnv frees x t) e t | (x, e, t) <- xets  ]     xts    = [ (x, t)    | (x, _, t) <- xets, not (S.member x frees) ]     xets   = [ (x, e, t) | (x, e)    <- xes, t <- sortOf e, not (isClass t)]-    xes    = M.toList m-    env    = combinedSEnv g     frees  = S.fromList (concatMap (F.syms . snd) xes)     sortOf = maybeToList . So.checkSortExpr sp env     sp     = F.srcSpan g+    xes    = M.toList m+    env    = combinedSEnv g -substSort :: F.SEnv F.Sort -> S.HashSet F.Symbol -> F.Symbol -> F.Sort -> F.Sort-substSort sEnv _frees sym _t = fromMaybe (err sym) $ F.lookupSEnv sym sEnv+substSort :: F.SEnv F.Sort -> F.Symbol -> F.Sort+substSort sEnv sym = fromMaybe (err sym) $ F.lookupSEnv sym sEnv   where-    err x            = error $ "Solution.mkSubst: unknown binder " ++ F.showpp x+    err x = error $ "Solution.substSort: unknown binder " ++ F.showpp x   -- LH #1091-mkSubst :: F.SrcSpan -> F.SymEnv -> F.Symbol -> F.Sort -> F.Expr -> F.Sort -> F.Expr+mkSubst :: F.SrcSpan -> F.SymEnv -> F.Symbol -> F.Sort -> F.Expr -> F.Sort -> ElabM F.Expr mkSubst sp env x tx ey ty-  | tx == ty    = F.EEq ex ey-  | otherwise   = {- F.tracepp _msg -} F.EEq ex' ey'+  | tx == ty    = pure $ F.EEq ex ey+  | otherwise   = do ex' <- elabToInt sp env ex tx+                     ey' <- elabToInt sp env ey ty+                     pure $ {- F.tracepp _msg $ -} F.EEq ex' ey'   where-    _msg         = "mkSubst-DIFF:" ++ F.showpp (tx, ty) ++ F.showpp (ex', ey')+    -- _msg        = "mkSubst-DIFF: tx = " ++ F.showpp tx ++ " ty = " ++ F.showpp ty+    --                                     ++ " ex' = " ++ F.showpp ex' ++ " ey' = " ++ F.showpp ey'     ex          = F.expr x-    ex'         = elabToInt sp env ex tx-    ey'         = elabToInt sp env ey ty -elabToInt :: F.SrcSpan -> F.SymEnv -> F.Expr -> F.Sort -> F.Expr-elabToInt sp env e s = So.elaborate (F.atLoc sp "elabToInt") env (So.toInt env e s)+elabToInt :: F.SrcSpan -> F.SymEnv -> F.Expr -> F.Sort -> ElabM F.Expr+elabToInt sp env e s =+  do ef <- ask+     pure $ So.elaborate (So.ElabParam ef (F.atLoc sp "elabToInt") env) (So.toInt env e s)  isClass :: F.Sort -> Bool isClass F.FNum  = True@@ -552,11 +583,11 @@ extendKInfo ki t = ki { kiTags  = appendTags [t] (kiTags  ki)                       , kiDepth = 1  +            kiDepth ki } --- mrExprInfos :: (a -> ExprInfo) -> ([F.Expr] -> F.Expr) -> ([KInfo] -> KInfo) -> [a] -> ExprInfo-mrExprInfos :: (a -> (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> (b1, c1)-mrExprInfos mF erF irF xs = (erF es, irF is)-  where-    (es, is)              = unzip $ map mF xs+mrExprInfosM :: Monad m => (a -> m (b, c)) -> ([b] -> b1) -> ([c] -> c1) -> [a] -> m (b1, c1)+mrExprInfosM mF erF irF xs =+  do bcs <- traverse mF xs+     let (es, is) = unzip bcs+     pure (erF es, irF is)  -------------------------------------------------------------------------------- -- | `ebindInfo` constructs the information about the "ebind-definitions".

@@ -12,14 +12,17 @@ module Language.Fixpoint.Solver.Solve (solve, solverInfo) where  import           Control.Monad (when, filterM)-import           Control.Monad.State.Strict (liftIO, modify, lift)+import           Control.Monad.Reader+import           Control.Monad.State.Strict (modify) import           Language.Fixpoint.Misc import qualified Language.Fixpoint.Misc            as Misc import qualified Language.Fixpoint.Types           as F import qualified Language.Fixpoint.Types.Solutions as Sol import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Config hiding (stats)+import           Language.Fixpoint.SortCheck          (ElabM) import qualified Language.Fixpoint.Solver.Solution  as S+import qualified Language.Fixpoint.Smt.Types as T import qualified Language.Fixpoint.Solver.Worklist  as W import qualified Language.Fixpoint.Solver.Eliminate as E import           Language.Fixpoint.Solver.Monad@@ -199,26 +202,31 @@   -> F.SimpC a   -> SolveM a (Bool, Sol.Solution) ----------------------------------------------------------------------------refineC bindingsInSmt _i s c-  | null rhs  = return (False, s)-  | otherwise = do be     <- getBinds-                   let lhs = S.lhsPred bindingsInSmt be s c-                   kqs    <- filterValid (cstrSpan c) lhs rhs-                   return  $ S.update s ks kqs+refineC bindingsInSmt _i s c =+  do ef <- T.ctxElabF <$> getContext+     let (ks, rhs) = runReader (rhsCands s c) ef+     if null rhs+        then return (False, s)+        else do be     <- getBinds+                let lhs = runReader (S.lhsPred bindingsInSmt (F.coerceBindEnv ef be) s c) ef+                kqs    <- filterValid (cstrSpan c) lhs rhs+                return  $ S.update s ks kqs   where     _ci       = F.subcId c-    (ks, rhs) = rhsCands s c     -- msg       = printf "refineC: iter = %d, sid = %s, soln = \n%s\n"     --               _i (show (F.sid c)) (showpp s)     _msg ks xs ys = printf "refineC: iter = %d, sid = %s, s = %s, rhs = %d, rhs' = %d \n"                      _i (show _ci) (showpp ks) (length xs) (length ys) -rhsCands :: Sol.Solution -> F.SimpC a -> ([F.KVar], Sol.Cand (F.KVar, Sol.EQual))-rhsCands s c    = (fst <$> ks, kqs)+rhsCands :: Sol.Solution -> F.SimpC a -> ElabM ([F.KVar], Sol.Cand (F.KVar, Sol.EQual))+rhsCands s c    =+  do pq <- traverse cnd ks+     pure (fst <$> ks, concat pq)   where-    kqs         = [ (p, (k, q)) | (k, su) <- ks, (p, q)  <- cnd k su ]+    cnd :: (F.KVar, F.Subst) -> ElabM [(F.Pred, (F.KVar, Sol.EQual))]+    cnd (k, su) = map (\(p , q) -> (p , (k , q))) <$> Sol.qbPreds msg s su (Sol.lookupQBind s k)     ks          = predKs . F.crhs $ c-    cnd k su    = Sol.qbPreds msg s su (Sol.lookupQBind s k)+     msg         = "rhsCands: " ++ show (F.sid c)  predKs :: F.Expr -> [(F.KVar, F.Subst)]@@ -254,7 +262,8 @@ solNonCutsResult :: Sol.Solution -> SolveM ann (M.HashMap F.KVar F.Expr) solNonCutsResult s = do   be <- getBinds-  return $ S.nonCutsResult be s+  ef <- T.ctxElabF <$> getContext+  pure $ runReader (S.nonCutsResult be s) ef  result_   :: (F.Loc a, NFData a)@@ -311,7 +320,8 @@   -- lift   $ printf "isUnsat %s" (show (F.subcId c))   _     <- tickIter True -- newScc   be    <- getBinds-  let lp = S.lhsPred bindingsInSmt (F.coerceBindEnv be) s c+  ef <- T.ctxElabF <$> getContext+  let lp = runReader (S.lhsPred bindingsInSmt (F.coerceBindEnv ef be) s c) ef   let rp = rhsPred        c   res   <- not <$> isValid (cstrSpan c) lp rp   lift   $ whenLoud $ showUnsat res (F.subcId c) lp rp

@@ -173,7 +173,7 @@ simplifySortedReft :: NonTrivSorts -> SortedReft -> SortedReft simplifySortedReft tm sr   | nonTrivial = sr-  | otherwise  = sr { sr_reft = mempty }+  | otherwise  = sr { sr_reft = trueReft }   where     nonTrivial = isNonTrivialSort tm (sr_sort sr) 

@@ -47,7 +47,7 @@     -- _tx i (x, r)     -- | isUsed i    = (x, r)     -- | otherwise   = (x, top r)-    isUsed i _x r  = {- tracepp (unwords ["isUsed", show i, showpp _x]) $ -} memberIBindEnv i usedBinds || isTauto r+    isUsed i _x r  = memberIBindEnv i usedBinds || isTautoReft (sr_reft r)     usedBinds      = L.foldl' unionIBindEnv emptyIBindEnv (cEnvs ++ wEnvs)     wEnvs          = wenv <$> M.elems (ws fi)     cEnvs          = senv <$> M.elems (cm fi)

@@ -105,7 +105,7 @@ newTopBind :: Symbol -> SortedReft -> a -> SInfo a -> (BindId, SInfo a) newTopBind x sr a fi = (i', fi {bs = be'})   where-    (i', be')        = insertBindEnv x (top sr) a (bs fi)+    (i', be')        = insertBindEnv x (sr {sr_reft = trueReft}) a (bs fi)  -------------------------------------------------------------- 

@@ -46,6 +46,8 @@   , strSort    -- * Sort-Directed Transformations+  , ElabM+  , ElabParam (..)   , Elaborate (..)   , applySorts   , elabApply@@ -62,7 +64,7 @@   , isFirstOrder   , isMono -  , runCM0+--  , runCM0   ) where  --  import           Control.DeepSeq@@ -70,14 +72,17 @@ import           Control.Monad import           Control.Monad.Reader -import qualified Data.HashMap.Strict       as M+import           Data.Bifunctor (first)+import qualified Data.IntMap.Strict       as M+import qualified Data.HashSet              as S import           Data.IORef import qualified Data.List                 as L-import           Data.Maybe                (mapMaybe, fromMaybe, catMaybes, isJust)+import           Data.Maybe                (mapMaybe, fromMaybe, isJust)  import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Misc import           Language.Fixpoint.Types hiding   (subst, GInfo(..), senv)+import qualified Language.Fixpoint.Types.Config as Cfg import qualified Language.Fixpoint.Types.Visitor  as Vis import qualified Language.Fixpoint.Smt.Theories   as Thy import           Text.PrettyPrint.HughesPJ.Compat@@ -118,26 +123,35 @@ --   KVars. THIS IS NOW MANDATORY as sort-variables can be --   instantiated to `int` and `bool`. --------------------------------------------------------------------------------++type ElabM = Reader Cfg.ElabFlags++data ElabParam = ElabParam+  { epFlags :: Cfg.ElabFlags+  , epMsg   :: Located String+  , epEnv   :: SymEnv+  }+ class Elaborate a where-  elaborate :: Located String -> SymEnv -> a -> a+  elaborate :: ElabParam -> a -> a   instance (Loc a) => Elaborate (SInfo a) where-  elaborate msg senv si = si-    { F.cm      = elaborate msg senv <$> F.cm      si-    , F.bs      = elaborate msg senv  $  F.bs      si-    , F.asserts = elaborate msg senv <$> F.asserts si+  elaborate ep si = si+    { F.cm      = elaborate ep <$> F.cm      si+    , F.bs      = elaborate ep  $  F.bs      si+    , F.asserts = elaborate ep <$> F.asserts si     }   instance (Elaborate e) => (Elaborate (Triggered e)) where-  elaborate msg env t = fmap (elaborate msg env) t+  elaborate ep t = elaborate ep <$> t  instance (Elaborate a) => (Elaborate (Maybe a)) where-  elaborate msg env t = fmap (elaborate msg env) t+  elaborate ep t = elaborate ep <$> t  instance Elaborate Sort where-  elaborate _ _ = go+  elaborate _ = go    where       go s | isString s = strSort       go (FAbs i s)    = FAbs i  (go s)@@ -148,37 +162,37 @@       funSort = FApp . FApp funcSort  instance Elaborate AxiomEnv where-  elaborate msg env ae = ae-    { aenvEqs   = elaborate msg env (aenvEqs ae)+  elaborate ep ae = ae+    { aenvEqs   = elaborate ep (aenvEqs ae)     -- MISSING SORTS OOPS, aenvSimpl = elaborate msg env (aenvSimpl ae)     }  instance Elaborate Rewrite where-  elaborate msg env rw = rw { smBody = skipElabExpr msg env' (smBody rw) }+  elaborate ep rw = rw { smBody = skipElabExpr ep' (smBody rw) }     where-      env' = insertsSymEnv env undefined+      ep' = ep { epEnv = insertsSymEnv (epEnv ep) undefined }  instance Elaborate Equation where-  elaborate msg env eq = eq { eqBody = skipElabExpr msg env' (eqBody eq) }+  elaborate ep eq = eq { eqBody = skipElabExpr ep' (eqBody eq) }     where-      env' = insertsSymEnv env (eqArgs eq)+      ep' = ep { epEnv = insertsSymEnv (epEnv ep) (eqArgs eq) }  instance Elaborate Expr where-  elaborate msg env =-    elabNumeric . elabApply env' . elabExpr msg env' . elabFSet+  elaborate (ElabParam ef msg env) =+    elabNumeric . elabApply env' . elabExpr (ElabParam ef msg env') . elabFMap . (if Cfg.elabSetBag ef then elabFSetBagZ3 else id)       where-        env' = coerceEnv env+        env' = coerceEnv ef env -skipElabExpr :: Located String -> SymEnv -> Expr -> Expr-skipElabExpr msg env e = case elabExprE msg env e of+skipElabExpr :: ElabParam -> Expr -> Expr+skipElabExpr ep e = case elabExprE ep e of   Left _   -> e-  Right e' -> elabNumeric . elabApply env $ e'+  Right e' -> elabNumeric . elabApply (epEnv ep) $ e'  instance Elaborate (Symbol, Sort) where-  elaborate msg env (x, s) = (x, elaborate msg env s)+  elaborate ep (x, s) = (x, elaborate ep s)  instance Elaborate a => Elaborate [a]  where-  elaborate msg env xs = elaborate msg env <$> xs+  elaborate ep xs = elaborate ep <$> xs  elabNumeric :: Expr -> Expr elabNumeric = Vis.mapExprOnExpr go@@ -195,75 +209,120 @@       = e  instance Elaborate SortedReft where-  elaborate msg env (RR s (Reft (v, e))) = RR s (Reft (v, e'))+  elaborate ep (RR s (Reft (v, e))) = RR s (Reft (v, e'))     where-      e'   = elaborate msg env' e-      env' = insertSymEnv v s env+      e'   = elaborate ep' e+      ep' = ep { epEnv = insertSymEnv v s (epEnv ep) }  instance (Loc a) => Elaborate (BindEnv a) where-  elaborate msg env = mapBindEnv (\i (x, sr, l) -> (x, elaborate (msg' l i x sr) env sr, l))+  elaborate ep = mapBindEnv (\i (x, sr, l) -> (x, elaborate (ep { epMsg = msg' l i x sr }) sr, l))     where-      msg' l i x sr = atLoc l (val msg ++ unwords [" elabBE", show i, show x, show sr])+      msg' l i x sr = atLoc l (val (epMsg ep) ++ unwords [" elabBE", show i, show x, show sr])  instance (Loc a) => Elaborate (SimpC a) where-  elaborate msg env c = c {_crhs = elaborate msg' env (_crhs c) }-    where msg'        = atLoc c (val msg)+  elaborate ep c = c {_crhs = elaborate ep' (_crhs c) }+    where+      ep' = ep { epMsg = atLoc c (val $ epMsg ep) } +-----------------------------------------------------------------------------------+-- | Replace all finset/finmap/finbag theory operations with array-based encodings.+----------------------------------------------------------------------------------- ------------------------------------------------------------------------------------- | 'elabFSet' replaces all finset theory operations with array-based encodings.-----------------------------------------------------------------------------------elabFSet :: Expr -> Expr-elabFSet (EApp h@(EVar f) e)-  | f == Thy.setEmpty      = EApp (EVar Thy.arrConst) PFalse-  | f == Thy.setEmp        = PAtom Eq (EApp (EVar Thy.arrConst) PFalse) (elabFSet e)-  | f == Thy.setSng        = EApp (EApp (EApp (EVar Thy.arrStore) (EApp (EVar Thy.arrConst) PFalse)) (elabFSet e)) PTrue-  | f == Thy.setCom        = EApp (EVar Thy.arrMapNot) (elabFSet e)-  | otherwise              = EApp (elabFSet h) (elabFSet e)-elabFSet (EApp (EApp h@(EVar f) e1) e2)-  | f == Thy.setMem        = EApp (EApp (EVar Thy.arrSelect) (elabFSet e2)) (elabFSet e1)-  | f == Thy.setCup        = EApp (EApp (EVar Thy.arrMapOr) (elabFSet e1)) (elabFSet e2)-  | f == Thy.setCap        = EApp (EApp (EVar Thy.arrMapAnd) (elabFSet e1)) (elabFSet e2)-  | f == Thy.setAdd        = EApp (EApp (EApp (EVar Thy.arrStore) (elabFSet e1)) (elabFSet e2)) PTrue+-- TODO abstract into a visitor for EApp?++-- TODO there's no actual elaboration happening here, just symbol renaming+elabFMap :: Expr -> Expr+elabFMap (EApp h@(EVar f) e)+  | f == Thy.mapDef        = EApp (EVar Thy.arrConstM) (elabFMap e)+  | otherwise              = EApp (elabFMap h) (elabFMap e)+elabFMap (EApp (EApp h@(EVar f) e1) e2)+  | f == Thy.mapSel        = EApp (EApp (EVar Thy.arrSelectM) (elabFMap e1)) (elabFMap e2)+  | otherwise              = EApp (EApp (elabFMap h) (elabFMap e1)) (elabFMap e2)+elabFMap (EApp (EApp (EApp h@(EVar f) e1) e2) e3)+  | f == Thy.mapSto        = EApp (EApp (EApp (EVar Thy.arrStoreM) (elabFMap e1)) (elabFMap e2)) (elabFMap e3)+  | otherwise              = EApp (EApp (EApp (elabFMap h) (elabFMap e1)) (elabFMap e2)) (elabFMap e3)+elabFMap (EApp e1 e2)      = EApp (elabFMap e1) (elabFMap e2)+elabFMap (ENeg e)          = ENeg (elabFMap e)+elabFMap (EBin b e1 e2)    = EBin b (elabFMap e1) (elabFMap e2)+elabFMap (EIte e1 e2 e3)   = EIte (elabFMap e1) (elabFMap e2) (elabFMap e3)+elabFMap (ECst e t)        = ECst (elabFMap e) t+elabFMap (ELam b e)        = ELam b (elabFMap e)+elabFMap (ETApp e t)       = ETApp (elabFMap e) t+elabFMap (ETAbs e t)       = ETAbs (elabFMap e) t+elabFMap (PAnd es)         = PAnd (elabFMap <$> es)+elabFMap (POr es)          = POr (elabFMap <$> es)+elabFMap (PNot e)          = PNot (elabFMap e)+elabFMap (PImp e1 e2)      = PImp (elabFMap e1) (elabFMap e2)+elabFMap (PIff e1 e2)      = PIff (elabFMap e1) (elabFMap e2)+elabFMap (PAtom r e1 e2)   = PAtom r (elabFMap e1) (elabFMap e2)+elabFMap (PAll   bs e)     = PAll bs (elabFMap e)+elabFMap (PExist bs e)     = PExist bs (elabFMap e)+elabFMap (PGrad  k su i e) = PGrad k su i (elabFMap e)+elabFMap (ECoerc a t e)    = ECoerc a t (elabFMap e)+elabFMap e                 = e++elabFSetBagZ3 :: Expr -> Expr+elabFSetBagZ3 (EApp h@(EVar f) e)+  | f == Thy.setEmpty         = EApp (EVar Thy.arrConstS) PFalse+  | f == Thy.setEmp           = PAtom Eq (EApp (EVar Thy.arrConstS) PFalse) (elabFSetBagZ3 e)+  | f == Thy.setSng           = EApp (EApp (EApp (EVar Thy.arrStoreS) (EApp (EVar Thy.arrConstS) PFalse)) (elabFSetBagZ3 e)) PTrue+  | f == Thy.setCom           = EApp (EVar Thy.arrMapNotS) (elabFSetBagZ3 e)+  | f == Thy.bagEmpty         = EApp (EVar Thy.arrConstB) (ECon (I 0))+  | otherwise                 = EApp (elabFSetBagZ3 h) (elabFSetBagZ3 e)+elabFSetBagZ3 (EApp (EApp h@(EVar f) e1) e2)+  | f == Thy.setMem           = EApp (EApp (EVar Thy.arrSelectS) (elabFSetBagZ3 e2)) (elabFSetBagZ3 e1)+  | f == Thy.setCup           = EApp (EApp (EVar Thy.arrMapOrS) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)+  | f == Thy.setCap           = EApp (EApp (EVar Thy.arrMapAndS) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)+  | f == Thy.setAdd           = EApp (EApp (EApp (EVar Thy.arrStoreS) (elabFSetBagZ3 e2)) (elabFSetBagZ3 e1)) PTrue   -- A \ B == A /\ ~B == ~(A => B)-  | f == Thy.setDif        = EApp (EApp (EVar Thy.arrMapAnd) (elabFSet e1)) (EApp (EVar Thy.arrMapNot) (elabFSet e2))-  | f == Thy.setSub        = PAtom Eq (EApp (EVar Thy.arrConst) PTrue) (EApp (EApp (EVar Thy.arrMapImp) (elabFSet e1)) (elabFSet e2))-  | otherwise              = EApp (EApp (elabFSet h) (elabFSet e1)) (elabFSet e2)-elabFSet (EApp e1 e2)      = EApp (elabFSet e1) (elabFSet e2)-elabFSet (ENeg e)          = ENeg (elabFSet e)-elabFSet (EBin b e1 e2)    = EBin b (elabFSet e1) (elabFSet e2)-elabFSet (EIte e1 e2 e3)   = EIte (elabFSet e1) (elabFSet e2) (elabFSet e3)-elabFSet (ECst e t)        = ECst (elabFSet e) t-elabFSet (ELam b e)        = ELam b (elabFSet e)-elabFSet (ETApp e t)       = ETApp (elabFSet e) t-elabFSet (ETAbs e t)       = ETAbs (elabFSet e) t-elabFSet (PAnd es)         = PAnd (elabFSet <$> es)-elabFSet (POr es)          = POr (elabFSet <$> es)-elabFSet (PNot e)          = PNot (elabFSet e)-elabFSet (PImp e1 e2)      = PImp (elabFSet e1) (elabFSet e2)-elabFSet (PIff e1 e2)      = PIff (elabFSet e1) (elabFSet e2)-elabFSet (PAtom r e1 e2)   = PAtom r (elabFSet e1) (elabFSet e2)-elabFSet (PAll   bs e)     = PAll bs (elabFSet e)-elabFSet (PExist bs e)     = PExist bs (elabFSet e)-elabFSet (PGrad  k su i e) = PGrad k su i (elabFSet e)-elabFSet (ECoerc a t e)    = ECoerc a t (elabFSet e)-elabFSet e                 = e+  | f == Thy.setDif           = EApp (EApp (EVar Thy.arrMapAndS) (elabFSetBagZ3 e1)) (EApp (EVar Thy.arrMapNotS) (elabFSetBagZ3 e2))+  | f == Thy.setSub           = PAtom Eq (EApp (EVar Thy.arrConstS) PTrue) (EApp (EApp (EVar Thy.arrMapImpS) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))+  | f == Thy.bagCount         = EApp (EApp (EVar Thy.arrSelectB) (elabFSetBagZ3 e2)) (elabFSetBagZ3 e1)+  | f == Thy.bagSng           = EApp (EApp (EApp (EVar Thy.arrStoreB) (EApp (EVar Thy.arrConstB) (ECon (I 0)))) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)+  | f == Thy.bagCup           = EApp (EApp (EVar Thy.arrMapPlusB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)+  | f == Thy.bagSub           = PAtom Eq (EApp (EVar Thy.arrConstS) PTrue) (EApp (EApp (EVar Thy.arrMapLeB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))+  | f == Thy.bagMax           = EApp (EApp (EApp (EVar Thy.arrMapIteB) (EApp (EApp (EVar Thy.arrMapGtB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)+  | f == Thy.bagMin           = EApp (EApp (EApp (EVar Thy.arrMapIteB) (EApp (EApp (EVar Thy.arrMapLeB) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2))) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)+  | otherwise                 = EApp (EApp (elabFSetBagZ3 h) (elabFSetBagZ3 e1)) (elabFSetBagZ3 e2)+elabFSetBagZ3 (EApp e1 e2)      = EApp (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)+elabFSetBagZ3 (ENeg e)          = ENeg (elabFSetBagZ3 e)+elabFSetBagZ3 (EBin b e1 e2)    = EBin b (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)+elabFSetBagZ3 (EIte e1 e2 e3)   = EIte (elabFSetBagZ3 e1) (elabFSetBagZ3 e2) (elabFSetBagZ3 e3)+elabFSetBagZ3 (ECst e t)        = ECst (elabFSetBagZ3 e) t+elabFSetBagZ3 (ELam b e)        = ELam b (elabFSetBagZ3 e)+elabFSetBagZ3 (ETApp e t)       = ETApp (elabFSetBagZ3 e) t+elabFSetBagZ3 (ETAbs e t)       = ETAbs (elabFSetBagZ3 e) t+elabFSetBagZ3 (PAnd es)         = PAnd (elabFSetBagZ3 <$> es)+elabFSetBagZ3 (POr es)          = POr (elabFSetBagZ3 <$> es)+elabFSetBagZ3 (PNot e)          = PNot (elabFSetBagZ3 e)+elabFSetBagZ3 (PImp e1 e2)      = PImp (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)+elabFSetBagZ3 (PIff e1 e2)      = PIff (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)+elabFSetBagZ3 (PAtom r e1 e2)   = PAtom r (elabFSetBagZ3 e1) (elabFSetBagZ3 e2)+elabFSetBagZ3 (PAll   bs e)     = PAll bs (elabFSetBagZ3 e)+elabFSetBagZ3 (PExist bs e)     = PExist bs (elabFSetBagZ3 e)+elabFSetBagZ3 (PGrad  k su i e) = PGrad k su i (elabFSetBagZ3 e)+elabFSetBagZ3 (ECoerc a t e)    = ECoerc a t (elabFSetBagZ3 e)+elabFSetBagZ3 e                 = e  -------------------------------------------------------------------------------- -- | 'elabExpr' adds "casts" to decorate polymorphic instantiation sites. ---------------------------------------------------------------------------------elabExpr :: Located String -> SymEnv -> Expr -> Expr-elabExpr msg env e = case elabExprE msg env e of+elabExpr :: ElabParam -> Expr -> Expr+elabExpr ep e = case elabExprE ep e of   Left ex  -> die ex   Right e' -> F.notracepp ("elabExp " ++ showpp e) e' -elabExprE :: Located String -> SymEnv -> Expr -> Either Error Expr-elabExprE msg env e =-  case runCM0 (srcSpan msg) (elab (env, envLookup) e) of+elabExprE :: ElabParam -> Expr -> Either Error Expr+elabExprE (ElabParam ef msg env) e =+  case runCM0 (srcSpan msg) (Just ef) $ do+    (!e', _) <- elab (env, envLookup) e+    finalThetaRef <- asks chTVSubst+    finalTheta <- liftIO $ readIORef finalThetaRef+    return (applyExpr finalTheta e') of     Left (ChError f') ->       let e' = f' ()        in Left $ err (srcSpan e') (d (val e'))-    Right s  -> Right (fst s)+    Right s  -> Right s   where     sEnv = seSort env     envLookup = (`lookupSEnvWithDistance` sEnv)@@ -283,7 +342,7 @@   where     go e                  = case splitArgs e of                              (e', []) -> step e'-                             (f , es) -> defuncEApp env (go f) (mapFst go <$> es)+                             (f , es) -> defuncEApp env (go f) (first go <$> es)     step (PAnd [])        = PTrue     step (POr [])         = PFalse     step (ENeg e)         = ENeg (go  e)@@ -313,7 +372,7 @@ -- | Sort Inference ------------------------------------------------------------ -------------------------------------------------------------------------------- sortExpr :: SrcSpan -> SEnv Sort -> Expr -> Sort-sortExpr l γ e = case runCM0 l (checkExpr f e) of+sortExpr l γ e = case runCM0 l Nothing (checkExpr f e) of     Left (ChError f') -> die $ err l (d (val (f' ())))     Right s -> s   where@@ -327,7 +386,7 @@                ]  checkSortExpr :: SrcSpan -> SEnv Sort -> Expr -> Maybe Sort-checkSortExpr sp γ e = case runCM0 sp (checkExpr f e) of+checkSortExpr sp γ e = case runCM0 sp Nothing (checkExpr f e) of     Left _   -> Nothing     Right s  -> Just s   where@@ -357,7 +416,11 @@   show (ChError f) = show (f ()) instance Exception ChError where -data ChState = ChS { chCount :: IORef Int, chSpan :: SrcSpan }+data ChState = ChS { chCount :: IORef Int+                   , chSpan  :: SrcSpan+                   , chElabF :: Cfg.ElabFlags+                   , chTVSubst :: IORef (Maybe TVSubst)+                   }  type Env      = Symbol -> SESearch Sort type ElabEnv  = (SymEnv, Env)@@ -390,9 +453,10 @@ -- function is not referentially transparent. -- Each evaluation of the function starts with a different -- value of counter.-runCM0 :: SrcSpan -> CheckM a -> Either ChError a-runCM0 sp act = unsafePerformIO $ do-  try (runReaderT act (ChS varCounterRef sp))+runCM0 :: SrcSpan -> Maybe Cfg.ElabFlags -> CheckM a -> Either ChError a+runCM0 sp mef act = unsafePerformIO $ do+  ref <- newIORef Nothing+  try (runReaderT act (ChS varCounterRef sp (fromMaybe (Cfg.ElabFlags False) mef) ref))  fresh :: CheckM Int fresh = do@@ -409,27 +473,30 @@     unknowns              = [ x | x <- syms sr, x `notElem` v : xs, not (x `memberSEnv` env)]     Reft (v,_)            = sr_reft sr -checkSortedReftFull :: Checkable a => SrcSpan -> SEnv SortedReft -> a -> Maybe Doc+checkSortedReftFull :: Checkable a => SrcSpan -> SEnv SortedReft -> a -> ElabM (Maybe Doc) checkSortedReftFull sp γ t =-  case runCM0 sp (check γ' t) of-    Left (ChError f)  -> Just (text (val (f ())))-    Right _ -> Nothing+  do ef <- ask+     pure $ case runCM0 sp (Just ef) (check γ' t) of+              Left (ChError f)  -> Just (text (val (f ())))+              Right _ -> Nothing   where     γ' = sr_sort <$> γ -checkSortFull :: Checkable a => SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc+checkSortFull :: Checkable a => SrcSpan -> SEnv SortedReft -> Sort -> a -> ElabM (Maybe Doc) checkSortFull sp γ s t =-  case runCM0 sp (checkSort γ' s t) of-    Left (ChError f)  -> Just (text (val (f ())))-    Right _ -> Nothing+  do ef <- ask+     pure $ case runCM0 sp (Just ef) (checkSort γ' s t) of+              Left (ChError f)  -> Just (text (val (f ())))+              Right _ -> Nothing   where       γ' = sr_sort <$> γ -checkSorted :: Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc+checkSorted :: Checkable a => SrcSpan -> SEnv Sort -> a -> ElabM (Maybe Doc) checkSorted sp γ t =-  case runCM0 sp (check γ t) of-    Left (ChError f)  -> Just (text (val (f ())))-    Right _  -> Nothing+  do ef <- ask+     pure $ case runCM0 sp (Just ef) (check γ t) of+              Left (ChError f) -> Just (text (val (f ())))+              Right _  -> Nothing  pruneUnsortedReft :: SEnv Sort -> Templates -> SortedReft -> SortedReft pruneUnsortedReft _ t r@@ -452,7 +519,7 @@ checkPred' :: Env -> Expr -> Maybe Expr checkPred' f p = res -- traceFix ("checkPred: p = " ++ showFix p) $ res   where-    res        = case runCM0 dummySpan (checkPred f p) of+    res        = case runCM0 dummySpan Nothing (checkPred f p) of                    Left _err -> notracepp ("Removing" ++ showpp p) Nothing                    Right _   -> Just p @@ -463,11 +530,18 @@   checkSort γ _ = check γ  instance Checkable Expr where-  check γ e = void $ checkExpr f e-   where f = (`lookupSEnvWithDistance` coerceSortEnv γ)+  check γ e =+    do ef <- asks chElabF+       _ <- checkExpr (`lookupSEnvWithDistance` coerceSortEnv ef γ) e+       pure () -  checkSort γ s e = void $ checkExpr f (ECst e (coerceSetToArray s))-   where f = (`lookupSEnvWithDistance` coerceSortEnv γ)+  checkSort γ s e =+    do ef <- asks chElabF+       _ <- checkExpr (`lookupSEnvWithDistance` coerceSortEnv ef γ)+                      (ECst e (if Cfg.elabSetBag ef then coerceSetBagToArray s' else s'))+       pure ()+   where+      s' = coerceMapToArray s  instance Checkable SortedReft where   check γ (RR s (Reft (v, ra))) = check γ' ra@@ -516,142 +590,140 @@ {-# SCC elab #-} elab :: ElabEnv -> Expr -> CheckM (Expr, Sort) ---------------------------------------------------------------------------------elab f@(_, g) e@(EBin o e1 e2) = do-  (e1', s1) <- elab f e1-  (e2', s2) <- elab f e2-  s <- checkOpTy g e s1 s2-  return (EBin o (eCst e1' s1) (eCst e2' s2), s)--elab f (EApp e1@(EApp _ _) e2) = do-  (e1', _, e2', s2, s) <- notracepp "ELAB-EAPP" <$> elabEApp f e1 e2-  let e = eAppC s e1' (eCst e2' s2)-  let θ = unifyExpr (snd f) e-  return (applyExpr θ e, maybe s (`apply` s) θ)+elab f@(!_, !g) e@(EBin !o !e1 !e2) = do+  (!e1', !s1) <- elab f e1+  (!e2', !s2) <- elab f e2+  !s <- checkOpTy g e s1 s2+  let !result = EBin o (eCst e1' s1) (eCst e2' s2)+  return (result, s) -elab f (EApp e1 e2) = do-  (e1', s1, e2', s2, s) <- elabEApp f e1 e2-  let e = eAppC s (eCst e1' s1) (eCst e2' s2)-  let θ = unifyExpr (snd f) e-  return (applyExpr θ e, maybe s (`apply` s) θ)+elab !f (EApp !e1 !e2) = do+  (!e1', !s1, !e2', !s2, !s) <- elabEApp f e1 e2+  let !e = eAppC s (eCst e1' s1) (eCst e2' s2)+  return (e, s) -elab _ e@(ESym _) =+elab !_ e@(ESym _) =   return (e, strSort) -elab _ e@(ECon (I _)) =+elab !_ e@(ECon (I _)) =   return (e, FInt) -elab _ e@(ECon (R _)) =+elab !_ e@(ECon (R _)) =   return (e, FReal) -elab _ e@(ECon (L _ s)) =+elab !_ e@(ECon (L _ !s)) =   return (e, s) -elab _ e@(PKVar _ _) =+elab !_ e@(PKVar _ _) =   return (e, boolSort) -elab f (PGrad k su i e) =-  (, boolSort) . PGrad k su i . fst <$> elab f e+elab !f (PGrad !k !su !i !e) = do+  (!e', !_) <- elab f e+  return (PGrad k su i e', boolSort) -elab (_, f) e@(EVar x) =-  (e,) <$> checkSym f x+elab (!_, !f) e@(EVar !x) = do+  !cs <- checkSym f x+  return (e, cs) -elab f (ENeg e) = do-  (e', s) <- elab f e+elab !f (ENeg !e) = do+  (!e', !s) <- elab f e   return (ENeg e', s) -elab f@(_,g) (ECst (EIte p e1 e2) t) = do-  (p', _)   <- elab f p-  (e1', s1) <- elab f (eCst e1 t)-  (e2', s2) <- elab f (eCst e2 t)-  s         <- checkIteTy g p e1' e2' s1 s2+elab f@(!_,!g) (ECst (EIte !p !e1 !e2) !t) = do+  (!p', !_)   <- elab f p+  (!e1', !s1) <- elab f (eCst e1 t)+  (!e2', !s2) <- elab f (eCst e2 t)+  !s          <- checkIteTy g p e1' e2' s1 s2   return (EIte p' (eCst e1' s) (eCst e2' s), t) -elab f@(_,g) (EIte p e1 e2) = do-  t <- getIte g e1 e2-  (p', _)   <- elab f p-  (e1', s1) <- elab f (eCst e1 t)-  (e2', s2) <- elab f (eCst e2 t)-  s         <- checkIteTy g p e1' e2' s1 s2+elab f@(!_,!g) (EIte !p !e1 !e2) = do+  !t <- getIte g e1 e2+  (!p', !_)   <- elab f p+  (!e1', !s1) <- elab f (eCst e1 t)+  (!e2', !s2) <- elab f (eCst e2 t)+  !s          <- checkIteTy g p e1' e2' s1 s2   return (EIte p' (eCst e1' s) (eCst e2' s), s) -elab f (ECst e t) = do-  (e', _) <- elab f e+elab !f (ECst !e !t) = do+  (!e', !_) <- elab f e   return (eCst e' t, t) -elab f (PNot p) = do-  (e', _) <- elab f p+elab !f (PNot !p) = do+  (!e', !_) <- elab f p   return (PNot e', boolSort) -elab f (PImp p1 p2) = do-  (p1', _) <- elab f p1-  (p2', _) <- elab f p2+elab !f (PImp !p1 !p2) = do+  (!p1', !_) <- elab f p1+  (!p2', !_) <- elab f p2   return (PImp p1' p2', boolSort) -elab f (PIff p1 p2) = do-  (p1', _) <- elab f p1-  (p2', _) <- elab f p2+elab !f (PIff !p1 !p2) = do+  (!p1', !_) <- elab f p1+  (!p2', !_) <- elab f p2   return (PIff p1' p2', boolSort) -elab f (PAnd ps) = do-  ps' <- mapM (elab f) ps+elab !f (PAnd !ps) = do+  !ps' <- mapM (elab f) ps   return (PAnd (fst <$> ps'), boolSort) -elab f (POr ps) = do-  ps' <- mapM (elab f) ps+elab !f (POr !ps) = do+  !ps' <- mapM (elab f) ps   return (POr (fst <$> ps'), boolSort) -elab f@(_,g) e@(PAtom eq e1 e2) | eq == Eq || eq == Ne = do-  t1        <- checkExpr g e1-  t2        <- checkExpr g e2-  (t1',t2') <- unite g e t1 t2 `withError` errElabExpr e-  e1'       <- elabAs f t1' e1-  e2'       <- elabAs f t2' e2-  e1''      <- eCstAtom f e1' t1'-  e2''      <- eCstAtom f e2' t2'-  return (PAtom eq e1'' e2'' , boolSort)+elab f@(!_,!g) e@(PAtom !eq !e1 !e2) | eq == Eq || eq == Ne = do+  !t1        <- checkExpr g e1+  !t2        <- checkExpr g e2+  (!t1',!t2') <- unite g e t1 t2 `withError` errElabExpr e+  !e1'       <- elabAs f t1' e1+  !e2'       <- elabAs f t2' e2+  !e1''      <- eCstAtom f e1' t1'+  !e2''      <- eCstAtom f e2' t2'+  return (PAtom eq e1'' e2'', boolSort) -elab f (PAtom r e1 e2)+elab !f (PAtom !r !e1 !e2)   | r == Ueq || r == Une = do-  (e1', _) <- elab f e1-  (e2', _) <- elab f e2+  (!e1', !_) <- elab f e1+  (!e2', !_) <- elab f e2   return (PAtom r e1' e2', boolSort) -elab f@(env,_) (PAtom r e1 e2) = do-  e1' <- uncurry (toInt env) <$> elab f e1-  e2' <- uncurry (toInt env) <$> elab f e2+elab f@(!env,!_) (PAtom !r !e1 !e2) = do+  !e1' <- uncurry (toInt env) <$> elab f e1+  !e2' <- uncurry (toInt env) <$> elab f e2   return (PAtom r e1' e2', boolSort) -elab f (PExist bs e) = do-  (e', s) <- elab (elabAddEnv f bs) e-  let bs' = elaborate "PExist Args" mempty bs+elab !f (PExist !bs !e) = do+  (!e', !s) <- elab (elabAddEnv f bs) e+  !ef <- asks chElabF+  let !bs' = elaborate (ElabParam ef "PExist Args" mempty) bs   return (PExist bs' e', s) -elab f (PAll bs e) = do-  (e', s) <- elab (elabAddEnv f bs) e-  let bs' = elaborate "PAll Args" mempty bs+elab !f (PAll !bs !e) = do+  (!e', !s) <- elab (elabAddEnv f bs) e+  !ef <- asks chElabF+  let !bs' = elaborate (ElabParam ef "PAll Args" mempty) bs   return (PAll bs' e', s) -elab f (ELam (x,t) e) = do-  (e', s) <- elab (elabAddEnv f [(x, t)]) e-  let t' = elaborate "ELam Arg" mempty t+elab !f (ELam (!x,!t) !e) = do+  (!e', !s) <- elab (elabAddEnv f [(x, t)]) e+  !ef <- asks chElabF+  let !t' = elaborate (ElabParam ef "ELam Arg" mempty) t   return (ELam (x, t') (eCst e' s), FFunc t s) -elab f (ECoerc s t e) = do-  (e', _) <- elab f e-  return     (ECoerc s t e', t)+elab !f (ECoerc !s !t !e) = do+  (!e', !_) <- elab f e+  return (ECoerc s t e', t) -elab _ (ETApp _ _) =+elab !_ (ETApp _ _) =   error "SortCheck.elab: TODO: implement ETApp"-elab _ (ETAbs _ _) =+elab !_ (ETAbs _ _) =   error "SortCheck.elab: TODO: implement ETAbs" - -- | 'eCstAtom' is to support tests like `tests/pos/undef00.fq` eCstAtom :: ElabEnv -> Expr -> Sort -> CheckM Expr eCstAtom f@(sym,g) (EVar x) t   | Found s <- g x   , isUndef s-  , not (isInt sym t) = (`ECst` t) <$> elabAs f t (EApp (eVar tyCastName) (eVar x))+  , not (isNum sym t) = (`ECst` t) <$> elabAs f t (EApp (eVar tyCastName) (eVar x)) eCstAtom _ e t = return (ECst e t)  isUndef :: Sort -> Bool@@ -686,8 +758,8 @@  elabEApp  :: ElabEnv -> Expr -> Expr -> CheckM (Expr, Sort, Expr, Sort, Sort) elabEApp f@(_, g) e1 e2 = do-  (e1', s1)     <- {- notracepp ("elabEApp: e1 = " ++ showpp e1) <$> -} elab f e1-  (e2', s2)     <- elab f e2+  (e1', s1)     <- {- notracepp ("elabEApp: e1 = " ++ show e1) <$> -} elab f e1+  (e2', s2)     <- {- notracepp ("elabEApp: e2 = " ++ show e2) <$> -} elab f e2   (e1'', e2'', s1', s2', s) <- elabAppSort g e1' e2' s1 s2   return           (e1'', s1', e2'', s2', s) @@ -696,7 +768,9 @@   let e            = Just (EApp e1 e2)   (sIn, sOut, su) <- checkFunSort s1   su'             <- unify1 f e su sIn s2-  return (applyExpr (Just su') e1 , applyExpr (Just su') e2, apply su' s1, apply su' s2, apply su' sOut)+  composeTVSubst (Just su)+  composeTVSubst (Just su')+  return (e1 , e2, apply su' s1, apply su' s2, apply su' sOut)   --------------------------------------------------------------------------------@@ -720,8 +794,8 @@ makeApplication e1 (e2, s) =   ECst (EApp (EApp f e1) e2) s   where-    f                      = {- notracepp ("makeApplication: " ++ showpp (e2, t2)) $ -} applyAt t2 s-    t2                     = exprSort "makeAppl" e2+    f  = {- notracepp ("makeApplication: " ++ showpp (e2, t2)) $ -} applyAt t2 s+    t2 = exprSort "makeAppl" e2  applyAt :: Sort -> Sort -> Expr applyAt s t = ECst (EVar applyName) (FFunc s t)@@ -735,11 +809,11 @@   | isSmtInt  = e   | otherwise = ECst (EApp f (ECst e s)) FInt   where-    isSmtInt  = isInt env s+    isSmtInt  = isNum env s     f         = toIntAt s -isInt :: SymEnv -> Sort -> Bool-isInt env s = case sortSmtSort False (seData env) s of+isNum :: SymEnv -> Sort -> Bool+isNum env s = case sortSmtSort False (seData env) s of   SInt    -> True   SString -> True   SReal   -> True@@ -891,12 +965,12 @@ -}  ---------------------------------------------------------------------------------applySorts :: Vis.Visitable t => t -> [Sort]+applySorts :: Vis.Foldable t => t -> [Sort] ---------------------------------------------------------------------------------applySorts = {- notracepp "applySorts" . -} (defs ++) . Vis.fold vis () []+applySorts = {- tracepp "applySorts" . -} (defs ++) . Vis.fold vis () []   where     defs   = [FFunc t1 t2 | t1 <- basicSorts, t2 <- basicSorts]-    vis    = (Vis.defaultVisitor :: Vis.Visitor [KVar] t) { Vis.accExpr = go }+    vis    = (Vis.defaultFolder :: Vis.Folder [KVar] t) { Vis.accExpr = go }     go _ (EApp (ECst (EVar f) t) _)   -- get types needed for [NOTE:apply-monomorphism]            | f == applyName            = [t]@@ -946,9 +1020,26 @@ -- | Helper for checking symbol occurrences checkSym :: Env -> Symbol -> CheckM Sort checkSym f x = case f x of-  Found s -> instantiate s+  Found s -> refreshNegativeTyVars s >>= instantiate   Alts xs -> throwErrorAt (errUnboundAlts x xs) +-- Negative type variables are implictly universally quantified type variables+refreshNegativeTyVars :: Sort -> CheckM Sort+refreshNegativeTyVars s = do+    let negativeSorts = negSort s+    freshVars <- mapM pair $ S.toList negativeSorts+    pure $ foldr (uncurry subst) s freshVars+  where+    pair i = do+      f <- fresh+      pure (i, FVar f)++    negSort (FVar i) | i < 0 = S.singleton i+    negSort (FAbs _ s')      = negSort s'+    negSort (FFunc s1 s2)    = negSort s1 `S.union` negSort s2+    negSort (FApp s1 s2)     = negSort s1 `S.union` negSort s2+    negSort _                = S.empty+ -- | Helper for checking if-then-else expressions checkIte :: Env -> Expr -> Expr -> Expr -> CheckM Sort checkIte f p e1 e2 = do@@ -1071,7 +1162,7 @@ -------------------------------------------------------------------------------- -- | Checking Predicates ------------------------------------------------------- ---------------------------------------------------------------------------------checkPred                  :: Env -> Expr -> CheckM ()+checkPred :: Env -> Expr -> CheckM () checkPred f e = checkExpr f e >>= checkBoolSort e  checkBoolSort :: Expr -> Sort -> CheckM ()@@ -1119,32 +1210,7 @@     b1            = s1 == boolSort     b2            = s2 == boolSort ------------------------------------------------------------------------------------ | Sort Unification on Expressions--------------------------------------------------------------------------------- -{-# SCC unifyExpr #-}-unifyExpr :: Env -> Expr -> Maybe TVSubst-unifyExpr f (EApp e1 e2) = Just $ mconcat $ catMaybes [θ1, θ2, θ]-  where-   θ1 = unifyExpr f e1-   θ2 = unifyExpr f e2-   θ  = unifyExprApp f e1 e2-unifyExpr f (ECst e _)-  = unifyExpr f e-unifyExpr _ _-  = Nothing--unifyExprApp :: Env -> Expr -> Expr -> Maybe TVSubst-unifyExprApp f e1 e2 = do-  t1 <- getArg $ exprSortMaybe e1-  t2 <- exprSortMaybe e2-  unify f (Just $ EApp e1 e2) t1 t2-  where-    getArg (Just (FFunc t1 _)) = Just t1-    getArg _                   = Nothing-- -------------------------------------------------------------------------------- -- | Sort Unification --------------------------------------------------------------------------------@@ -1152,7 +1218,7 @@ unify :: Env -> Maybe Expr -> Sort -> Sort -> Maybe TVSubst -------------------------------------------------------------------------------- unify f e t1 t2-  = case runCM0 dummySpan (unify1 f e emptySubst t1 t2) of+  = case runCM0 dummySpan Nothing (unify1 f e emptySubst t1 t2) of       Left _   -> Nothing       Right su -> Just su @@ -1160,7 +1226,7 @@ unifyTo1 :: Env -> [Sort] -> Maybe Sort -------------------------------------------------------------------------------- unifyTo1 f ts-  = case runCM0 dummySpan (unifyTo1M f ts) of+  = case runCM0 dummySpan Nothing (unifyTo1M f ts) of       Left _  -> Nothing       Right t -> Just t @@ -1180,7 +1246,7 @@ -------------------------------------------------------------------------------- unifySorts :: Sort -> Sort -> Maybe TVSubst ---------------------------------------------------------------------------------unifySorts   = unifyFast False emptyEnv+unifySorts = unifyFast False emptyEnv   where     emptyEnv x = die $ err dummySpan $ "SortCheck: lookup in Empty Env: " <> pprint x @@ -1192,8 +1258,8 @@ -------------------------------------------------------------------------------- unifyFast False f t1 t2 = unify f Nothing t1 t2 unifyFast True  _ t1 t2-  | t1 == t2        = Just emptySubst-  | otherwise           = Nothing+  | t1 == t2  = Just emptySubst+  | otherwise = Nothing  {- eqFast :: Sort -> Sort -> Bool@@ -1305,9 +1371,9 @@ instantiate !t = go t   where     go (FAbs !i !t') = do-      !t''    <- instantiate t'+      !t''   <- instantiate t'       !v     <- fresh-      return  $ subst i (FVar v) t''+      return $ subst i (FVar v) t''     go !t' =       return t' @@ -1323,22 +1389,45 @@       Just !t'       -> if t == t' then return θ else unify1 f e θ t t'       Nothing        -> return (updateVar i t θ) + --------------------------------------------------------------------------------+-- | Update global subst to be applied to expressions+--------------------------------------------------------------------------------++updateTVSubst :: TVSubst -> CheckM ()+updateTVSubst theta = do+  refTheta <- asks chTVSubst+  liftIO $ atomicModifyIORef' refTheta $ const (Just theta, ())++-- local (\s -> s {chTVSubst = theta}) (return ())++mergeTVSubst :: TVSubst -> Maybe TVSubst -> TVSubst+mergeTVSubst (Th m1) Nothing = Th m1+mergeTVSubst (Th m1) (Just (Th m2)) = Th m1 <> Th m2++composeTVSubst :: Maybe TVSubst -> CheckM ()+composeTVSubst Nothing = return ()+composeTVSubst (Just theta1) = do+  refTheta <- asks chTVSubst+  theta <- liftIO $ readIORef refTheta+  updateTVSubst (mergeTVSubst theta1 theta)++-------------------------------------------------------------------------------- -- | Applying a Type Substitution ---------------------------------------------- -------------------------------------------------------------------------------- apply :: TVSubst -> Sort -> Sort ---------------------------------------------------------------------------------apply θ          = Vis.mapSort f+apply !θ          = Vis.mapSort f   where-    f t@(FVar i) = fromMaybe t (lookupVar i θ)-    f t          = t+    f t@(FVar !i) = fromMaybe t (lookupVar i θ)+    f !t          = t  applyExpr :: Maybe TVSubst -> Expr -> Expr applyExpr Nothing e  = e applyExpr (Just θ) e = Vis.mapExprOnExpr f e   where-    f (ECst e' s) = ECst e' (apply θ s)-    f e'          = e'+    f (ECst !e' !s) = ECst e' (apply θ s)+    f !e'          = e'  -------------------------------------------------------------------------------- _applyCoercion :: Symbol -> Sort -> Sort -> Sort@@ -1365,7 +1454,7 @@ -- | API for manipulating Sort Substitutions ----------------------------------- -------------------------------------------------------------------------------- -newtype TVSubst = Th (M.HashMap Int Sort) deriving (Show)+newtype TVSubst = Th (M.IntMap Sort) deriving (Show)  instance Semigroup TVSubst where   (Th s1) <> (Th s2) = Th (s1 <> s2)

@@ -13,6 +13,8 @@    -- * SMT Solver options   , SMTSolver (..)+  , solverFlags+  , ElabFlags (..)    -- REST Options   , RESTOrdering (..)@@ -99,6 +101,8 @@   , noslice          :: Bool           -- ^ Disable non-concrete KVar slicing   , rewriteAxioms    :: Bool           -- ^ Allow axiom instantiation via rewriting   , pleWithUndecidedGuards :: 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   , interpreter      :: Bool           -- ^ Do not use the interpreter to assist PLE   , oldPLE           :: Bool           -- ^ Use old version of PLE   , noIncrPle        :: Bool           -- ^ Use incremental PLE@@ -144,9 +148,16 @@  --------------------------------------------------------------------------------------- -data SMTSolver = Z3 | Z3mem | Cvc4 | Mathsat+data SMTSolver = Z3 | Z3mem | Cvc4 | Cvc5 | Mathsat                  deriving (Eq, Data, Typeable, Generic) +newtype ElabFlags = ElabFlags { elabSetBag :: Bool }++solverFlags :: SMTSolver -> ElabFlags+solverFlags Z3    = ElabFlags True+solverFlags Z3mem = ElabFlags True+solverFlags _     = ElabFlags False+ instance Default SMTSolver where   def = if Conditional.Z3.builtWithZ3AsALibrary then Z3mem else Z3 @@ -154,6 +165,7 @@   show Z3      = "z3"   show Z3mem   = "z3 API"   show Cvc4    = "cvc4"+  show Cvc5    = "cvc5"   show Mathsat = "mathsat"  instance S.Store SMTSolver@@ -259,6 +271,8 @@         &= name "interpreter"         &= help "Use the interpreter to assist PLE"   , oldPLE                   = False &= help "Use old version of PLE"+  , etabeta                  = False &= help "Use eta expansion and beta reduction to aid PLE"+  , localRewrites            = False &= name "local-rewrites" &= help "Perform local rewrites inside PLE"   , noIncrPle                = False &= help "Don't use incremental PLE"   , noEnvironmentReduction   =       False

@@ -1,7 +1,7 @@ {-# LANGUAGE CPP                        #-} {-# LANGUAGE DeriveDataTypeable         #-}-{-# LANGUAGE DeriveFunctor              #-} {-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DeriveTraversable          #-} {-# LANGUAGE FlexibleContexts           #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -50,7 +50,8 @@   , gwInfo, GWInfo (..)    -- * Qualifiers-  , Qualifier   (..)+  , Qualifier+  , QualifierV  (..)   , QualParam   (..)   , QualPattern (..)   , trueQual@@ -78,11 +79,17 @@    -- * Axioms   , AxiomEnv (..)-  , Equation (..)+  , Equation+  , EquationV (..)   , mkEquation   , Rewrite  (..)   , AutoRewrite (..)   , dedupAutoRewrites+  , LocalRewritesEnv (..)+  , LocalRewrites (..)+  , lookupRewrite+  , lookupLocalRewrites+  , insertRewrites    -- * Misc  [should be elsewhere but here due to dependencies]   , substVars@@ -405,7 +412,7 @@  instance NFData QualPattern instance NFData QualParam-instance NFData Qualifier+instance NFData v => NFData (QualifierV v) instance NFData Kuts instance NFData HOInfo instance NFData GFixSolution@@ -417,14 +424,15 @@ instance (NFData (c a), NFData a) => NFData (GInfo c a) instance (NFData a) => NFData (Result a) -instance Hashable Qualifier+instance Hashable v => Hashable (QualifierV v) instance Hashable QualPattern instance Hashable QualParam-instance Hashable Equation+instance Hashable v => Hashable (EquationV v)  instance B.Binary QualPattern instance B.Binary QualParam-instance B.Binary Qualifier+instance B.Binary v => B.Binary (QualifierV v)+instance B.Binary v => B.Binary (EquationV v)  --------------------------------------------------------------------------- -- | "Smart Constructors" for Constraints ---------------------------------@@ -484,13 +492,14 @@ -------------------------------------------------------------------------------- -- | Qualifiers ---------------------------------------------------------------- ---------------------------------------------------------------------------------data Qualifier = Q+type Qualifier = QualifierV Symbol+data QualifierV v = Q   { qName   :: !Symbol     -- ^ Name   , qParams :: [QualParam] -- ^ Parameters-  , qBody   :: !Expr       -- ^ Predicate+  , qBody   :: !(ExprV v)  -- ^ Predicate   , qPos    :: !SourcePos  -- ^ Source Location   }-  deriving (Eq, Ord, Show, Data, Typeable, Generic)+  deriving (Eq, Ord, Show, Data, Typeable, Generic, Functor, Foldable, Traversable)  data QualParam = QP   { qpSym  :: !Symbol@@ -519,7 +528,7 @@   trueQual :: Qualifier-trueQual = Q (symbol ("QTrue" :: String)) [] mempty (dummyPos "trueQual")+trueQual = Q (symbol ("QTrue" :: String)) [] PTrue (dummyPos "trueQual")  instance Loc Qualifier where   srcSpan q = SS l l@@ -555,7 +564,7 @@ instance Fixpoint Qualifier where   toFix = pprQual -instance PPrint Qualifier where+instance PPrint (QualifierV v) where   pprintTidy k q = "qualif" <+> pprintTidy k (qName q) <+> "defined at" <+> pprintTidy k (qPos q)  pprQual :: Qualifier -> Doc@@ -591,7 +600,7 @@ remakeQual q = mkQual (qName q) (qParams q) (qBody q) (qPos q)  -- | constructing qualifiers-mkQual :: Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier+mkQual :: Symbol -> [QualParam] -> ExprV v -> SourcePos -> QualifierV v mkQual n qps p = Q n qps' p   where     qps'       = zipWith (\qp t' -> qp { qpSort = t'}) qps ts'@@ -688,6 +697,7 @@        , ae       = axe        , ddecls   = adts        , ebinds   = ebs+       , lrws = mempty        }   where     --TODO handle duplicates gracefully instead (merge envs by intersect?)@@ -733,6 +743,7 @@   , hoInfo   :: !HOInfo                    -- ^ Higher Order info   , asserts  :: ![Triggered Expr]          -- ^ TODO: what is this?   , ae       :: AxiomEnv                   -- ^ Information about reflected function defs+  , lrws     :: LocalRewritesEnv           -- ^ Local rewrites   }   deriving (Eq, Show, Functor, Generic) @@ -761,6 +772,7 @@                 , hoInfo   = hoInfo i1   <> hoInfo i2                 , asserts  = asserts i1  <> asserts i2                 , ae       = ae i1       <> ae i2+                , lrws     = lrws i1     <> lrws i2                 }  @@ -778,6 +790,7 @@                      , hoInfo   = mempty                      , asserts  = mempty                      , ae       = mempty+                     , lrws     = mempty                      }  instance PTable (SInfo a) where@@ -793,6 +806,7 @@ toFixpoint cfg x' =    cfgDoc   cfg                   $++$ declsDoc x'                   $++$ aeDoc    x'+                  $++$ lrwsDoc  x'                   $++$ qualsDoc x'                   $++$ kutsDoc  x'                 --   $++$ packsDoc x'@@ -817,6 +831,7 @@                $++$ toFix    ebs     qualsDoc      = vcat     . map toFix . L.sort . quals     aeDoc         = toFix    . ae+    lrwsDoc       = toFix    . lrws     metaDoc (i,d) = toFixMeta (text "bind" <+> toFix i) (toFix d)     mdata         = C.metadata cfg     binfoDoc@@ -927,6 +942,22 @@   , aenvAutoRW   :: M.HashMap SubcId [AutoRewrite]   } deriving (Eq, Show, Generic) +newtype LocalRewrites = LocalRewrites (M.HashMap Symbol Expr)+  deriving (Eq, Show, Generic, Semigroup, Monoid, NFData, S.Store)++newtype LocalRewritesEnv = LocalRewritesMap (M.HashMap BindId LocalRewrites)+  deriving (Eq, Show, Generic, Semigroup, Monoid, NFData, S.Store)++lookupRewrite :: Symbol -> LocalRewrites -> Maybe Expr+lookupRewrite x (LocalRewrites m) = M.lookup x m++lookupLocalRewrites :: BindId -> LocalRewritesEnv -> Maybe LocalRewrites+lookupLocalRewrites i (LocalRewritesMap m) = M.lookup i m++insertRewrites :: BindId -> LocalRewrites -> LocalRewritesEnv -> LocalRewritesEnv+insertRewrites i rws (LocalRewritesMap m) = LocalRewritesMap $ M.insertWith (<>) i rws m++ instance S.Store AutoRewrite instance S.Store AxiomEnv instance S.Store Rewrite@@ -954,14 +985,15 @@ instance PPrint AxiomEnv where   pprintTidy _ = text . show -data Equation = Equ+type Equation = EquationV Symbol+data EquationV v = Equ   { eqName :: !Symbol           -- ^ name of reflected function   , eqArgs :: [(Symbol, Sort)]  -- ^ names of parameters-  , eqBody :: !Expr             -- ^ definition of body+  , eqBody :: !(ExprV v)        -- ^ definition of body   , eqSort :: !Sort             -- ^ sort of body   , eqRec  :: !Bool             -- ^ is this a recursive definition   }-  deriving (Data, Eq, Ord, Show, Generic)+  deriving (Data, Eq, Ord, Show, Generic, Functor)  mkEquation :: Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation mkEquation f xts e out = Equ f xts e out (f `elem` syms e)@@ -1037,6 +1069,13 @@  instance Fixpoint Equation where   toFix (Equ f xs e s _) = "define" <+> toFix f <+> ppArgs xs <+> ":" <+> toFix s <+> text "=" <+> braces (parens (toFix e))++instance Fixpoint LocalRewritesEnv where+  toFix (LocalRewritesMap rws) = vcat $ uncurry toFixLocal <$> M.toList rws+    where+      toFixLocal bid (LocalRewrites rws) = text "defineLocal" <+> toFix bid +        <+> brackets (vcat $ punctuate ";" $ uncurry toFixRewrite <$> M.toList rws)+      toFixRewrite sym eq = toFix sym <+> text ":=" <+> toFix eq  instance Fixpoint Rewrite where   toFix (SMeasure f d xs e)

@@ -44,7 +44,7 @@   , BindEnv, beBinds   , emptyBindEnv   , fromListBindEnv-  , insertBindEnv, lookupBindEnv+  , insertBindEnv, lookupBindEnv, bindEnvSize   , filterBindEnv, mapBindEnv, mapWithKeyMBindEnv, adjustBindEnv   , bindEnvFromList, bindEnvToList, deleteBindEnv, elemsBindEnv   , EBindEnv, splitByQuantifiers@@ -73,6 +73,7 @@ import           Text.PrettyPrint.HughesPJ.Compat import           Control.DeepSeq +import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types.Sorts@@ -178,6 +179,7 @@   data SESearch a = Found a | Alts [Symbol]+  deriving Show  -- | Functions for Indexed Bind Environment @@ -210,6 +212,9 @@ insertBindEnv :: Symbol -> SortedReft -> a -> BindEnv a -> (BindId, BindEnv a) insertBindEnv x r a (BE n m) = (n, BE (n + 1) (M.insert n (x, r, a) m)) +bindEnvSize :: BindEnv a -> Int+bindEnvSize (BE n _) = n+ fromListBindEnv :: [(BindId, (Symbol, SortedReft, a))] -> BindEnv a fromListBindEnv xs = BE (length xs) (M.fromList xs) @@ -364,5 +369,8 @@     kIs       = [ (k, i) | (i, ks) <- kPacks, k <- ks ]     kPacks    = zip [0..] . coalesce . fmap S.toList $ kvss -coerceBindEnv :: BindEnv a -> BindEnv a-coerceBindEnv be = be { beBinds = M.map (\(s, sr, a) -> (s, sr { sr_sort = coerceSetToArray (sr_sort sr) } , a)) (beBinds be) }+coerceBindEnv :: ElabFlags -> BindEnv a -> BindEnv a+coerceBindEnv ef be = be { beBinds = M.map (\(s, sr, a) ->+                                                let srs = coerceMapToArray (sr_sort sr) in+                                                (s, sr { sr_sort = if elabSetBag ef then coerceSetBagToArray srs else srs } , a))+                                            (beBinds be) }

@@ -230,30 +230,30 @@ -------------------------------------------------------------------------------  class Gradual a where-  gsubst :: GSol -> a -> a+  gsubst :: ElabFlags -> GSol -> a -> a  instance Gradual Expr where-  gsubst (GSol env m) e   = mapGVars' (\(k, _) -> Just (fromMaybe (err k) (mknew k))) e+  gsubst ef (GSol env m) e   = mapGVars' (\(k, _) -> Just (fromMaybe (err k) (mknew k))) e     where-      mknew k = So.elaborate "initBGind.mkPred" env $ fst <$> M.lookup k m+      mknew k = So.elaborate (So.ElabParam ef "initBGind.mkPred" env) $ fst <$> M.lookup k m       err   k = errorstar ("gradual substitution: Cannot find " ++ showpp k)  instance Gradual Reft where-  gsubst su (Reft (x, e)) = Reft (x, gsubst su e)+  gsubst ef su (Reft (x, e)) = Reft (x, gsubst ef su e)  instance Gradual SortedReft where-  gsubst su r = r {sr_reft = gsubst su (sr_reft r)}+  gsubst ef su r = r {sr_reft = gsubst ef su (sr_reft r)}  instance Gradual (SimpC a) where-  gsubst su c = c {_crhs = gsubst su (_crhs c)}+  gsubst ef su c = c {_crhs = gsubst ef su (_crhs c)}  instance Gradual (BindEnv a) where-  gsubst su = mapBindEnv (\_ (x, r, l) -> (x, gsubst su r, l))+  gsubst ef su = mapBindEnv (\_ (x, r, l) -> (x, gsubst ef su r, l))  instance Gradual v => Gradual (M.HashMap k v) where-  gsubst su = M.map (gsubst su)+  gsubst ef su = M.map (gsubst ef su)  instance Gradual (SInfo a) where-  gsubst su fi = fi { bs = gsubst su (bs fi)-                    , cm = gsubst su (cm fi)-                    }+  gsubst ef su fi = fi { bs = gsubst ef su (bs fi)+                        , cm = gsubst ef su (cm fi)+                        }

@@ -97,9 +97,9 @@   , funConName   , listConName   , listLConName-  , tupConName   , setConName   , mapConName+  , bagConName   , arrayConName   , strConName   , charConName@@ -119,14 +119,14 @@   , divFuncName    -- * Casting function names-  , setToIntName, bitVecToIntName, mapToIntName, boolToIntName, realToIntName, toIntName, tyCastName+  , setToIntName, bitVecToIntName, mapToIntName, bagToIntName, boolToIntName, realToIntName, toIntName, tyCastName   , setApplyName, bitVecApplyName, mapApplyName, boolApplyName, realApplyName, intApplyName   , applyName   , coerceName    , lambdaName   , lamArgSymbol-  , isLamArgSymbol+  , isLamArgSymbol, etaExpSymbol  ) where @@ -610,16 +610,23 @@ lamArgPrefix :: Symbol lamArgPrefix = "lam_arg" +etaExpPrefix :: Symbol+etaExpPrefix = "eta"++etaExpSymbol :: Int -> Symbol+etaExpSymbol = intSymbol etaExpPrefix+ lamArgSymbol :: Int -> Symbol lamArgSymbol = intSymbol lamArgPrefix  isLamArgSymbol :: Symbol -> Bool isLamArgSymbol = isPrefixOfSym lamArgPrefix -setToIntName, bitVecToIntName, mapToIntName, realToIntName, toIntName, tyCastName :: Symbol+setToIntName, bitVecToIntName, mapToIntName, bagToIntName, realToIntName, toIntName, tyCastName :: Symbol setToIntName    = "set_to_int" bitVecToIntName = "bitvec_to_int" mapToIntName    = "map_to_int"+bagToIntName    = "bag_to_int" realToIntName   = "real_to_int" toIntName       = "cast_as_int" tyCastName      = "cast_as"@@ -649,12 +656,12 @@ funConName   = "->"  -listConName, listLConName, tupConName, propConName, _hpropConName, vvName, setConName, mapConName, arrayConName:: Symbol+listConName, listLConName, propConName, _hpropConName, vvName, setConName, mapConName, bagConName, arrayConName:: Symbol listConName  = "[]" listLConName = "List"-tupConName   = "Tuple" setConName   = "Set_Set" mapConName   = "Map_t"+bagConName   = "Bag_t" arrayConName = "Array_t" vvName       = "VV" propConName  = "Prop"@@ -695,8 +702,8 @@   mulFuncName, divFuncName :: Symbol-mulFuncName  = "Z3_OP_MUL"-divFuncName  = "Z3_OP_DIV"+mulFuncName  = "SMTLIB_OP_MUL"+divFuncName  = "SMTLIB_OP_DIV"  isPrim :: Symbol -> Bool isPrim x = S.member x prims

@@ -1,6 +1,7 @@ {-# LANGUAGE CPP                        #-} {-# LANGUAGE DeriveDataTypeable         #-} {-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DeriveTraversable          #-} {-# LANGUAGE FlexibleContexts           #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}@@ -25,15 +26,18 @@   , Constant (..)   , Bop (..)   , Brel (..)-  , Expr (..), Pred+  , ExprV (..), Pred+  , Expr   , GradInfo (..)   , pattern PTrue, pattern PTop, pattern PFalse, pattern EBot   , pattern ETimes, pattern ERTimes, pattern EDiv, pattern ERDiv   , pattern EEq   , KVar (..)-  , Subst (..)+  , Subst+  , SubstV (..)   , KVSub (..)-  , Reft (..)+  , Reft+  , ReftV (..)   , SortedReft (..)    -- * Constructing Terms@@ -51,7 +55,6 @@   , Expression (..)   , Predicate (..)   , Subable (..)-  , Reftable (..)    -- * Constructors   , reft                    -- "smart@@ -72,6 +75,7 @@   , isNonTrivial   , isContraPred   , isTautoPred+  , isTautoReft   , isSingletonExpr   , isSingletonReft   , isFalse@@ -91,6 +95,7 @@   , reftConjuncts   , sortedReftSymbols   , substSortInExpr+  , sortSubstInExpr    -- * Transforming   , mapPredReft@@ -142,14 +147,14 @@   instance NFData KVar-instance NFData Subst+instance NFData v => NFData (SubstV v) instance NFData GradInfo instance NFData Constant instance NFData SymConst instance NFData Brel instance NFData Bop-instance NFData Expr-instance NFData Reft+instance NFData v => NFData (ExprV v)+instance NFData v => NFData (ReftV v) instance NFData SortedReft  -- instance (Hashable k, Eq k, S.Store k, S.Store v) => S.Store (M.HashMap k v) where@@ -180,9 +185,9 @@   put = B.put . M.toList   get = M.fromList <$> B.get -instance B.Binary Subst-instance B.Binary Expr-instance B.Binary Reft+instance B.Binary v => B.Binary (SubstV v)+instance B.Binary v => B.Binary (ExprV v)+instance B.Binary v => B.Binary (ReftV v)   reftConjuncts :: Reft -> [Reft]@@ -256,25 +261,29 @@ instance Hashable SymConst instance Hashable Constant instance Hashable GradInfo-instance Hashable Subst-instance Hashable Expr-instance Hashable Reft+instance Hashable v => Hashable (SubstV v)+instance Hashable v => Hashable (ExprV v)+instance Hashable v => Hashable (ReftV v)  -------------------------------------------------------------------------------- -- | Substitutions ------------------------------------------------------------- ---------------------------------------------------------------------------------newtype Subst = Su (M.HashMap Symbol Expr)-                deriving (Eq, Data, Ord, Typeable, Generic, ToJSON, FromJSON)+type Subst = SubstV Symbol+newtype SubstV v = Su (M.HashMap Symbol (ExprV v))+                deriving (Eq, Data, Ord, Typeable, Generic, Functor, Foldable, Traversable) -instance Show Subst where+instance ToJSON Subst+instance FromJSON Subst++instance (Fixpoint v, Ord v, Show v) => Show (SubstV v) where   show = showFix -instance Fixpoint Subst where+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 PPrint Subst where+instance (Ord v, Fixpoint v) => PPrint (SubstV v) where   pprintTidy _ = toFix  data KVSub = KVS@@ -319,29 +328,32 @@ instance FromJSON Expr      where  -data Expr = ESym !SymConst+type Expr = ExprV Symbol++data ExprV v+          = ESym !SymConst           | ECon !Constant-          | EVar !Symbol-          | EApp !Expr !Expr-          | ENeg !Expr-          | EBin !Bop !Expr !Expr-          | EIte !Expr !Expr !Expr-          | ECst !Expr !Sort-          | ELam !(Symbol, Sort)   !Expr-          | ETApp !Expr !Sort-          | ETAbs !Expr !Symbol-          | PAnd   ![Expr]-          | POr    ![Expr]-          | PNot   !Expr-          | PImp   !Expr !Expr-          | PIff   !Expr !Expr-          | PAtom  !Brel  !Expr !Expr-          | PKVar  !KVar !Subst-          | PAll   ![(Symbol, Sort)] !Expr-          | PExist ![(Symbol, Sort)] !Expr-          | PGrad  !KVar !Subst !GradInfo !Expr-          | ECoerc !Sort !Sort !Expr-          deriving (Eq, Show, Ord, Data, Typeable, Generic)+          | EVar !v+          | EApp !(ExprV v) !(ExprV v)+          | ENeg !(ExprV v)+          | EBin !Bop !(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)+          | PGrad  !KVar !(SubstV v) !GradInfo !(ExprV v)+          | ECoerc !Sort !Sort !(ExprV v)+          deriving (Eq, Show, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable)  onEverySubexpr :: (Expr -> Expr) -> Expr -> Expr onEverySubexpr = everywhereOnA@@ -356,31 +368,31 @@  type Pred = Expr -pattern PTrue :: Expr+pattern PTrue :: ExprV v pattern PTrue = PAnd [] -pattern PTop :: Expr+pattern PTop :: ExprV v pattern PTop = PAnd [] -pattern PFalse :: Expr+pattern PFalse :: ExprV v pattern PFalse = POr  [] -pattern EBot :: Expr+pattern EBot :: ExprV v pattern EBot = POr  [] -pattern EEq :: Expr -> Expr -> Expr+pattern EEq :: ExprV v -> ExprV v -> ExprV v pattern EEq e1 e2 = PAtom Eq    e1 e2 -pattern ETimes :: Expr -> Expr -> Expr+pattern ETimes :: ExprV v -> ExprV v -> ExprV v pattern ETimes e1 e2 = EBin Times  e1 e2 -pattern ERTimes :: Expr -> Expr -> Expr+pattern ERTimes :: ExprV v -> ExprV v -> ExprV v pattern ERTimes e1 e2 = EBin RTimes e1 e2 -pattern EDiv :: Expr -> Expr -> Expr+pattern EDiv :: ExprV v -> ExprV v -> ExprV v pattern EDiv e1 e2 = EBin Div    e1 e2 -pattern ERDiv :: Expr -> Expr -> Expr+pattern ERDiv :: ExprV v -> ExprV v -> ExprV v pattern ERDiv e1 e2 = EBin RDiv   e1 e2  exprSymbolsSet :: Expr -> HashSet Symbol@@ -417,6 +429,18 @@       ECoerc t0 t1 e -> ECoerc (substSort f t0) (substSort f t1) e       e -> e ++sortSubstInExpr :: SortSubst -> Expr -> Expr+sortSubstInExpr f = onEverySubexpr go+  where+    go = \case+      ELam (x, t) e -> ELam (x, sortSubst f t) e+      PAll xts e -> PAll (second (sortSubst f) <$> xts) e+      PExist xts e -> PExist (second (sortSubst f) <$> xts) e+      ECst e t -> ECst e (sortSubst f t)+      ECoerc t0 t1 e -> ECoerc (sortSubst f t0) (sortSubst f t1) e+      e -> e+ exprKVars :: Expr -> HashMap KVar [Subst] exprKVars = go   where@@ -453,10 +477,10 @@ mkEApp :: LocSymbol -> [Expr] -> Expr mkEApp = eApps . EVar . val -eApps :: Expr -> [Expr] -> Expr+eApps :: ExprV v -> [ExprV v] -> ExprV v eApps f es  = foldl' EApp f es -splitEApp :: Expr -> (Expr, [Expr])+splitEApp :: ExprV v -> (ExprV v, [ExprV v]) splitEApp = go []   where     go acc (EApp f e) = go (e:acc) f@@ -511,11 +535,13 @@     go (PGrad _ _ _ e) = go e     go (ECoerc _ _ e)  = go e --- | Parsed refinement of @Symbol@ as @Expr@---   e.g. in '{v: _ | e }' v is the @Symbol@ and e the @Expr@-newtype Reft = Reft (Symbol, Expr)-               deriving (Eq, Ord, Data, Typeable, Generic)+type Reft = ReftV Symbol +-- | 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)+    deriving (Eq, Ord, Data, Typeable, Generic, Functor, Foldable, Traversable)+ data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft }                   deriving (Eq, Ord, Data, Typeable, Generic) @@ -576,7 +602,7 @@   toFix RDiv   = text "/."   toFix Mod    = text "mod" -instance Fixpoint Expr where+instance (Ord v, Fixpoint v) => Fixpoint (ExprV v) where   toFix (ESym c)       = toFix c   toFix (ECon c)       = toFix c   toFix (EVar s)       = toFix s@@ -611,7 +637,7 @@     where       dedup = Set.toList . Set.fromList -simplifyExpr :: ([Expr] -> [Expr]) -> Expr -> Expr+simplifyExpr :: Eq v => ([ExprV v] -> [ExprV v]) -> ExprV v -> ExprV v simplifyExpr dedup = go   where     go (POr  [])     = PFalse@@ -660,7 +686,7 @@       | isTautoPred  p     = PTrue       | otherwise          = p -isContraPred   :: Expr -> Bool+isContraPred   :: Eq v => ExprV v -> Bool isContraPred z = eqC z || (z `elem` contras)   where     contras    = [PFalse]@@ -675,7 +701,7 @@                = x == y     eqC _      = False -isTautoPred   :: Expr -> Bool+isTautoPred   :: Eq v => ExprV v -> Bool isTautoPred z  = z == PTop || z == PTrue || eqT z   where     eqT (PAnd [])@@ -747,7 +773,7 @@ opPrec Div    = 7 opPrec RDiv   = 7 -instance PPrint Expr where+instance (Ord v, Fixpoint v, PPrint v) => PPrint (ExprV v) where   pprintPrec _ k (ESym c)        = pprintTidy k c   pprintPrec _ k (ECon c)        = pprintTidy k c   pprintPrec _ k (EVar s)        = pprintTidy k s@@ -807,7 +833,9 @@   pprintPrec _ _ (ETAbs e s)     = "ETAbs" <+> toFix e <+> toFix s   pprintPrec z k (PGrad x _ _ e) = pprintPrec z k e <+> "&&" <+> toFix x -- "??" -pprintQuant :: Tidy -> Doc -> [(Symbol, Sort)] -> Expr -> Doc+pprintQuant+  :: (Ord v, Fixpoint v, PPrint v)+  => Tidy -> Doc -> [(Symbol, Sort)] -> ExprV v -> Doc pprintQuant k d xts p = (d <+> toFix xts)                         $+$                         ("  ." <+> pprintTidy k p)@@ -827,7 +855,7 @@ vIntersperse _ [d]    = d vIntersperse s (d:ds) = vcat (d : ((s <+>) <$> ds)) -pprintReft :: Tidy -> Reft -> Doc+pprintReft :: (PPrint v, Ord v, Fixpoint v) => Tidy -> ReftV v -> Doc pprintReft k (Reft (_,ra)) = pprintBin z k trueD andD flat   where     flat = flattenRefas [ra]@@ -910,7 +938,7 @@ --   so they SHOULD NOT be used inside the solver loop. Instead, use 'conj' which ensures --   some basic things but is faster. -pAnd, pOr     :: ListNE Pred -> Pred+pAnd, pOr     :: (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v pAnd          = simplify . PAnd  pAndNoDedup :: ListNE Pred -> Pred@@ -926,10 +954,10 @@ (|.|) :: Pred -> Pred -> Pred (|.|) p q = pOr [p, q] -pIte :: Pred -> Expr -> Expr -> Expr+pIte :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v -> ExprV v pIte p1 p2 p3 = pAnd [p1 `PImp` p2, PNot p1 `PImp` p3] -pExist :: [(Symbol, Sort)] -> Pred -> Pred+pExist :: [(Symbol, Sort)] -> ExprV v -> ExprV v pExist []  p = p pExist xts p = PExist xts p @@ -957,7 +985,7 @@ predReft      :: (Predicate a) => a -> Reft predReft p    = Reft (vv_, prop p) -reft :: Symbol -> Expr -> Reft+reft :: Symbol -> ExprV v -> ReftV v reft v p = Reft (v, p)  mapPredReft :: (Expr -> Expr) -> Reft -> Reft@@ -970,22 +998,25 @@ isFunctionSortedReft :: SortedReft -> Bool isFunctionSortedReft = isJust . functionSort . sr_sort -isNonTrivial :: Reftable r => r -> Bool-isNonTrivial = not . isTauto+isNonTrivial :: SortedReft -> Bool+isNonTrivial = not . isTautoReft . sr_reft -reftPred :: Reft -> Expr+isTautoReft :: Eq v => ReftV v -> Bool+isTautoReft = all isTautoPred . conjuncts . reftPred++reftPred :: ReftV v -> ExprV v reftPred (Reft (_, p)) = p -reftBind :: Reft -> Symbol+reftBind :: ReftV v -> Symbol reftBind (Reft (x, _)) = x  ------------------------------------------------------------ -- | Gradual Type Manipulation  ---------------------------- -------------------------------------------------------------pGAnds :: [Expr] -> Expr+pGAnds :: (Fixpoint v, Ord v) => [ExprV v] -> ExprV v pGAnds = foldl' pGAnd PTrue -pGAnd :: Expr -> Expr -> Expr+pGAnd :: (Fixpoint v, Ord v) => ExprV v -> ExprV v -> ExprV v pGAnd (PGrad k su i p) q = PGrad k su i (pAnd [p, q]) pGAnd p (PGrad k su i q) = PGrad k su i (pAnd [p, q]) pGAnd p q              = pAnd [p,q]@@ -1006,18 +1037,18 @@ trueSortedReft :: Sort -> SortedReft trueSortedReft = (`RR` trueReft) -trueReft, falseReft :: Reft+trueReft, falseReft :: ReftV v trueReft  = Reft (vv_, PTrue) falseReft = Reft (vv_, PFalse) -flattenRefas :: [Expr] -> [Expr]+flattenRefas :: [ExprV v] -> [ExprV 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 :: Expr -> [Expr]+conjuncts :: Eq v => ExprV v -> [ExprV v] conjuncts (PAnd ps) = concatMap conjuncts ps conjuncts p   | isTautoPred p   = []@@ -1057,23 +1088,6 @@   substa f (Loc l l' x) = Loc l l' (substa f x)   substf f (Loc l l' x) = Loc l l' (substf f x)   subst su (Loc l l' x) = Loc l l' (subst su x)---class (Monoid r, Subable r) => Reftable r where-  isTauto :: r -> Bool-  ppTy    :: r -> Doc -> Doc--  top     :: r -> r-  top _   =  mempty--  bot     :: r -> r--  meet    :: r -> r -> r-  meet    = mappend--  toReft  :: r -> Reft-  ofReft  :: Reft -> r-  params  :: r -> [Symbol]          -- ^ parameters for Reft, vv + others  instance Fixpoint Doc where   toFix = id

@@ -60,9 +60,10 @@   , qb   , qbPreds   , qbFilter-+  , qbFilterM   , gbFilterM +   -- * Conversion for client   , result, resultGradual @@ -76,6 +77,7 @@ import           Prelude hiding (lookup) import           GHC.Generics import           Control.DeepSeq+import           Control.Monad.Reader import           Data.Hashable import qualified Data.Maybe                 as Mb import qualified Data.HashMap.Strict        as M@@ -85,6 +87,7 @@ import           Control.Monad (filterM) import           Language.Fixpoint.Misc import           Language.Fixpoint.Types.PrettyPrint+-- import           Language.Fixpoint.Types.Config  as Cfg import           Language.Fixpoint.Types.Spans import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types.Sorts@@ -93,7 +96,7 @@ import           Language.Fixpoint.Types.Environments import           Language.Fixpoint.Types.Constraints import           Language.Fixpoint.Types.Substitutions-import           Language.Fixpoint.SortCheck (elaborate)+import           Language.Fixpoint.SortCheck (ElabM, ElabParam(..), elaborate) import           Text.PrettyPrint.HughesPJ.Compat  --------------------------------------------------------------------------------@@ -171,6 +174,9 @@ qbFilter :: (EQual -> Bool) -> QBind -> QBind qbFilter f (QB eqs) = QB (filter f eqs) +qbFilterM :: Monad m => (EQual -> m Bool) -> QBind -> m QBind+qbFilterM f (QB eqs) = QB <$> filterM f eqs+ instance NFData QBind instance NFData GBind @@ -306,15 +312,17 @@     ebm = M.fromList ebs  ---------------------------------------------------------------------------------qbPreds :: String -> Sol a QBind -> Subst -> QBind -> [(Pred, EQual)]+qbPreds :: String -> Sol a QBind -> Subst -> QBind -> ElabM [(Pred, EQual)] ---------------------------------------------------------------------------------qbPreds msg s su (QB eqs) = [ (elabPred eq, eq) | eq <- eqs ]+qbPreds msg s su (QB eqs) =+  do ef <- ask+     pure [ (elabPred ef eq, eq) | eq <- eqs ]   where-    elabPred eq           = elaborate (atLoc eq $ "qbPreds:" ++ msg) env-                          . subst su-                          . eqPred-                          $ eq-    env                   = sEnv s+    elabPred ef eq = elaborate (ElabParam ef (atLoc eq $ "qbPreds:" ++ msg) env)+                   . subst su+                   . eqPred+                   $ eq+    env            = sEnv s  -------------------------------------------------------------------------------- -- | Read / Write Solution at KVar ---------------------------------------------@@ -381,7 +389,7 @@   srcSpan = srcSpan . eqQual  trueEqual :: EQual-trueEqual = EQL trueQual mempty []+trueEqual = EQL trueQual PTrue []  instance PPrint EQual where   pprintTidy k = pprintTidy k . eqPred

@@ -37,7 +37,7 @@   , mapFVar   , basicSorts, intSort, realSort, boolSort, strSort, funcSort   -- , bitVec32Sort, bitVec64Sort-  , setSort, bitVecSort+  , setSort, bitVecSort, bagSort   , arraySort   , sizedBitVecSort   , mapSort, charSort@@ -57,6 +57,7 @@    , mkSortSubst   , sortSubst+  , SortSubst   , functionSort   , mkFFunc   , bkFFunc@@ -65,7 +66,7 @@   , sortSymbols   , substSort -  , isBool, isNumeric, isReal, isString, isSet, isArray, isPolyInst+  , isBool, isNumeric, isReal, isString, isSet, isMap, isBag, isArray, isPolyInst    -- * User-defined ADTs   , DataField (..)@@ -84,7 +85,8 @@   , tceMap    -- * Sort coercion for SMT theory encoding-  , coerceSetToArray+  , coerceMapToArray+  , coerceSetBagToArray   ) where  import qualified Data.Store as S@@ -92,6 +94,7 @@ import           Data.Typeable             (Typeable) import           GHC.Generics              (Generic) import           Data.Aeson+import           Data.Bifunctor (first)  import           Data.Hashable import           Data.HashSet (HashSet)@@ -147,7 +150,7 @@ defStrInfo  = False  charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon :: FTycon-strFTyCon, listFTyCon, mapFTyCon, setFTyCon :: FTycon+strFTyCon, listFTyCon, mapFTyCon, bagFTyCon, setFTyCon :: FTycon intFTyCon  = TC (dummyLoc "int"       ) numTcInfo boolFTyCon = TC (dummyLoc boolLConName) defTcInfo realFTyCon = TC (dummyLoc "real"      ) realTcInfo@@ -158,6 +161,7 @@ charFTyCon = TC (dummyLoc charConName ) defTcInfo setFTyCon  = TC (dummyLoc setConName  ) defTcInfo mapFTyCon  = TC (dummyLoc mapConName  ) defTcInfo+bagFTyCon  = TC (dummyLoc bagConName  ) defTcInfo  isListConName :: LocSymbol -> Bool isListConName x = c == listConName || c == listLConName --"List"@@ -175,6 +179,22 @@ isSetTC :: FTycon -> Bool isSetTC (TC z _) = isSetConName z +isMapConName :: LocSymbol -> Bool+isMapConName x = c == mapConName+  where+    c           = val x++isMapTC :: FTycon -> Bool+isMapTC (TC z _) = isMapConName z++isBagConName :: LocSymbol -> Bool+isBagConName x = c == bagConName+  where+    c           = val x++isBagTC :: FTycon -> Bool+isBagTC (TC z _) = isBagConName z+ isArrayConName :: LocSymbol -> Bool isArrayConName x = c == arrayConName   where@@ -389,6 +409,14 @@ isSet (FTC c) = isSetTC c isSet _       = False +isMap :: Sort -> Bool+isMap (FTC c) = isMapTC c+isMap _       = False++isBag :: Sort -> Bool+isBag (FTC c) = isBagTC c+isBag _       = False+ isArray :: Sort -> Bool isArray (FTC c) = isArrayTC c isArray _       = False@@ -533,6 +561,9 @@ sizedBitVecSort :: Symbol -> Sort sizedBitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FTC $ symbolFTycon' i) +bagSort :: Sort -> Sort+bagSort = FApp (FTC bagFTyCon)+ mapSort :: Sort -> Sort -> Sort mapSort = FApp . FApp (FTC (symbolFTycon' mapConName)) @@ -594,17 +625,6 @@ instance NFData DataDecl instance NFData Sub -instance Semigroup Sort where-  t1 <> t2-    | t1 == mempty  = t2-    | t2 == mempty  = t1-    | t1 == t2      = t1-    | otherwise     = errorstar $ "mappend-sort: conflicting sorts t1 =" ++ show t1 ++ " t2 = " ++ show t2--instance Monoid Sort where-  mempty  = FObj "any"-  mappend = (<>)- ------------------------------------------------------------------------------- -- | Embedding stuff as Sorts -------------------------------------------------------------------------------@@ -654,7 +674,7 @@   tceMap :: (Eq b, Hashable b) => (a -> b) -> TCEmb a -> TCEmb b-tceMap f = tceFromList . fmap (mapFst f) . tceToList+tceMap f = tceFromList . fmap (first f) . tceToList  tceFromList :: (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a tceFromList = TCE . M.fromList@@ -669,10 +689,20 @@ -- | Sort coercion for SMT theory encoding ------------------------------------------------------------------------------- -coerceSetToArray :: Sort -> Sort-coerceSetToArray   (FFunc sf sa) = FFunc (coerceSetToArray sf) (coerceSetToArray sa)-coerceSetToArray   (FAbs i sa)   = FAbs i (coerceSetToArray sa)-coerceSetToArray s@(FApp sf sa)-  | isSet sf = arraySort (coerceSetToArray sa) boolSort-  | otherwise = s-coerceSetToArray s = s+coerceMapToArray :: Sort -> Sort+coerceMapToArray (FFunc sf sa) = FFunc (coerceMapToArray sf) (coerceMapToArray sa)+coerceMapToArray (FAbs i sa)   = FAbs i (coerceMapToArray sa)+coerceMapToArray (FApp (FApp sf sa) sb)+  | isMap sf = arraySort (coerceMapToArray sa) (coerceMapToArray sb)+  | otherwise = FApp (FApp (coerceMapToArray sf) (coerceMapToArray sa)) (coerceMapToArray sb)+coerceMapToArray (FApp sf sa) = FApp (coerceMapToArray sf) (coerceMapToArray sa)+coerceMapToArray s = s++coerceSetBagToArray :: Sort -> Sort+coerceSetBagToArray (FFunc sf sa) = FFunc (coerceSetBagToArray sf) (coerceSetBagToArray sa)+coerceSetBagToArray (FAbs i sa)   = FAbs i (coerceSetBagToArray sa)+coerceSetBagToArray (FApp sf sa)+  | isSet sf = arraySort (coerceSetBagToArray sa) boolSort+  | isBag sf = arraySort (coerceSetBagToArray sa) intSort+  | otherwise = FApp (coerceSetBagToArray sf) (coerceSetBagToArray sa)+coerceSetBagToArray s = s

@@ -16,6 +16,8 @@   , filterSubst   , catSubst   , exprSymbolsSet+  , meetReft+  , pprReft   ) where  import           Data.Maybe@@ -177,33 +179,11 @@     suSyms = S.fromList $ syms (M.elems su) ++ syms (M.keys su)     bsSyms = S.fromList $ syms $ fst <$> bs -instance Semigroup Expr where-  p <> q = pAnd [p, q]--instance Monoid Expr where-  mempty  = PTrue-  mappend = (<>)-  mconcat = pAnd--instance Semigroup Reft where-  (<>) = meetReft--instance Monoid Reft where-  mempty  = trueReft-  mappend = (<>)- meetReft :: Reft -> Reft -> Reft meetReft (Reft (v, ra)) (Reft (v', ra'))-  | v == v'          = Reft (v , ra  `mappend` ra')-  | v == dummySymbol = Reft (v', ra' `mappend` (ra `subst1`  (v , EVar v')))-  | otherwise        = Reft (v , ra  `mappend` (ra' `subst1` (v', EVar v )))--instance Semigroup SortedReft where-  t1 <> t2 = RR (mappend (sr_sort t1) (sr_sort t2)) (mappend (sr_reft t1) (sr_reft t2))--instance Monoid SortedReft where-  mempty  = RR mempty mempty-  mappend = (<>)+  | v == v'          = Reft (v , pAnd [ra, ra'])+  | v == dummySymbol = Reft (v', pAnd [ra', ra `subst1`  (v , EVar v')])+  | otherwise        = Reft (v , pAnd [ra, ra' `subst1` (v', EVar v )])  instance Subable Reft where   syms (Reft (v, ras))      = v : syms ras@@ -218,25 +198,6 @@   substf f (RR so r) = RR so $ substf f r   substa f (RR so r) = RR so $ substa f r -instance Reftable () where-  isTauto _ = True-  ppTy _  d = d-  top  _    = ()-  bot  _    = ()-  meet _ _  = ()-  toReft _  = mempty-  ofReft _  = mempty-  params _  = []--instance Reftable Reft where-  isTauto  = all isTautoPred . conjuncts . reftPred-  ppTy     = pprReft-  toReft   = id-  ofReft   = id-  params _ = []-  bot    _        = falseReft-  top (Reft(v,_)) = Reft (v, mempty)- pprReft :: Reft -> Doc -> Doc pprReft (Reft (v, p)) d   | isTautoPred p@@ -244,19 +205,10 @@   | otherwise   = braces (toFix v <+> colon <+> d <+> text "|" <+> ppRas [p]) -instance Reftable SortedReft where-  isTauto  = isTauto . toReft-  ppTy     = ppTy . toReft-  toReft   = sr_reft-  ofReft   = errorstar "No instance of ofReft for SortedReft"-  params _ = []-  bot s    = s { sr_reft = falseReft }-  top s    = s { sr_reft = trueReft }- -- RJ: this depends on `isTauto` hence, here.-instance PPrint Reft where+instance (PPrint v, Fixpoint v, Ord v) => PPrint (ReftV v) where   pprintTidy k r-    | isTauto r        = text "true"+    | isTautoReft r        = text "true"     | otherwise        = pprintReft k r  instance PPrint SortedReft where

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleInstances #-} module Language.Fixpoint.Types.Templates (    anything, Templates, makeTemplates,

@@ -29,6 +29,7 @@     , symEnvSort     , symEnvTheory     , insertSymEnv+    , deleteSymEnv     , insertsSymEnv     , symbolAtName     , symbolAtSmtName@@ -44,6 +45,7 @@ import           Data.Hashable import           GHC.Generics              (Generic) import           Control.DeepSeq+import           Language.Fixpoint.Types.Config import           Language.Fixpoint.Types.PrettyPrint import           Language.Fixpoint.Types.Names import           Language.Fixpoint.Types.Sorts@@ -67,11 +69,11 @@ -- | 'SymEnv' is used to resolve the 'Sort' and 'Sem' of each 'Symbol' -------------------------------------------------------------------------------- data SymEnv = SymEnv-  { seSort    :: !(SEnv Sort)              -- ^ Sorts of *all* defined symbols-  , seTheory  :: !(SEnv TheorySymbol)      -- ^ Information about theory-specific Symbols-  , seData    :: !(SEnv DataDecl)          -- ^ User-defined data-declarations-  , seLits    :: !(SEnv Sort)              -- ^ Distinct Constant symbols-  , seAppls   :: !(M.HashMap FuncSort Int) -- ^ Types at which `apply` was used;+  { seSort   :: !(SEnv Sort)              -- ^ Sorts of *all* defined symbols+  , seTheory :: !(SEnv TheorySymbol)      -- ^ Information about theory-specific Symbols+  , seData   :: !(SEnv DataDecl)          -- ^ User-defined data-declarations+  , seLits   :: !(SEnv Sort)              -- ^ Distinct Constant symbols+  , seAppls  :: !(M.HashMap FuncSort Int) -- ^ Types at which `apply` was used;                                            --   see [NOTE:apply-monomorphization]   }   deriving (Eq, Show, Data, Typeable, Generic)@@ -97,13 +99,13 @@ symEnv :: SEnv Sort -> SEnv TheorySymbol -> [DataDecl] -> SEnv Sort -> [Sort] -> SymEnv symEnv xEnv fEnv ds ls ts = SymEnv xEnv' fEnv dEnv ls sortMap   where-    xEnv'                 = unionSEnv xEnv wiredInEnv-    dEnv                  = fromListSEnv [(symbol d, d) | d <- ds]-    sortMap               = M.fromList (zip smts [0..])-    smts                  = funcSorts dEnv ts+    xEnv'   = unionSEnv xEnv wiredInEnv+    dEnv    = fromListSEnv [(symbol d, d) | d <- ds]+    sortMap = M.fromList (zip smts [0..])+    smts    = funcSorts dEnv ts  -- | These are "BUILT-in" polymorphic functions which are---   UNININTERPRETED but POLYMORPHIC, hence need to go through+--   UNINTERPRETED but POLYMORPHIC, hence need to go through --   the apply-defunc stuff. wiredInEnv :: M.HashMap Symbol Sort wiredInEnv = M.fromList@@ -112,9 +114,9 @@   ]  --- | 'smtSorts' attempts to compute a list of all the input-output sorts+-- | 'funcSorts' attempts to compute a list of all the input-output sorts --   at which applications occur. This is a gross hack; as during unfolding---   we may create _new_ terms with wierd new sorts. Ideally, we MUST allow+--   we may create _new_ terms with weird new sorts. Ideally, we MUST allow --   for EXTENDING the apply-sorts with those newly created terms. --   the solution is perhaps to *preface* each VC query of the form --@@ -138,10 +140,61 @@ funcSorts :: SEnv DataDecl -> [Sort] -> [FuncSort] funcSorts dEnv ts = [ (t1, t2) | t1 <- smts, t2 <- smts]   where-    smts         = Misc.sortNub $ concat [ [tx t1, tx t2] | FFunc t1 t2 <- ts]-    tx           = applySmtSort dEnv+    smts = Misc.sortNub $ concat $ [ tx t1 ++ tx t2 | FFunc t1 t2 <- ts ]+    tx   = inlineArrSetBag False dEnv +-- Related to the above, after merging #688, we now allow types other than+-- Int to which Arrays/Sets/Bags can be applied.+-- However, the `sortSmtSort` function below, previously used in `funcSorts`,+-- only instantiates type variables at Ints. This causes the solver to crash+-- when PLE generates apply queries for polymorphic sets (see+-- https://github.com/ucsd-progsys/liquidhaskell/issues/2438). The following+-- pair of functions is a temporary fix for this - it generates additional+-- array/set/bag sorts instantiated at all user types for a "polymorphic depth 1"+-- (i.e., `Array (Foo Int) Int` but not `Array (Foo (Foo Int)) Int`, to keep+-- the applys table from blowing up exponentially). Ultimately, a general+-- solution should be implemented for generating ad-hoc sets of applys on the+-- fly, as described above. +inlineArrSetBag :: Bool -> SEnv DataDecl -> Sort -> [SmtSort]+inlineArrSetBag isASB env t = go . unAbs $ t+  where+    m = sortAbs t+    go (FFunc _ _)    = [SInt]+    go FInt           = [SInt]+    go FReal          = [SReal]+    go t+      | t == boolSort = [SBool]+      | isString t    = [SString]+    go (FVar _)+      | isASB     = SInt : map (\q -> let dd = snd q in+                                      SData (ddTyCon dd) (replicate (ddVars dd) SInt))+                               (M.toList $ seBinds env)+      | otherwise = [SInt]+    go t+      | (ct:ts) <- unFApp t = inlineArrSetBagFApp m env ct ts+      | otherwise = error "Unexpected empty 'unFApp t'"++inlineArrSetBagFApp :: Int -> SEnv DataDecl -> Sort -> [Sort] -> [SmtSort]+inlineArrSetBagFApp m env = go+  where+    go (FTC c) [a]+      | setConName == symbol c   = SSet <$> inlineArrSetBag True env a+    go (FTC c) [a]+      | bagConName == symbol c   = SBag <$> inlineArrSetBag True env a+    go (FTC c) [a, b]+      | arrayConName == symbol c = SArray <$> inlineArrSetBag True env a <*> inlineArrSetBag True env b+    go (FTC bv) [FTC s]+      | bitVecName == symbol bv+      , Just n <- sizeBv s      = [SBitVec n]+    go s []+      | isString s              = [SString]+    go (FTC c) ts+      | Just n <- tyArgs c env+      , let i = n - length ts   = [SData c ((inlineArrSetBag False env . FAbs m =<< ts) ++ replicate i SInt)]+    go _ _                      = [SInt]++ symEnvTheory :: Symbol -> SymEnv -> Maybe TheorySymbol symEnvTheory x env = lookupSEnv x (seTheory env) @@ -151,6 +204,9 @@ insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv insertSymEnv x t env = env { seSort = insertSEnv x t (seSort env) } +deleteSymEnv :: Symbol -> SymEnv -> SymEnv+deleteSymEnv x env = env { seSort = deleteSEnv x (seSort env) }+ insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv insertsSymEnv = L.foldl' (\env (x, s) -> insertSymEnv x s env) @@ -159,15 +215,15 @@ {-# SCC symbolAtName #-}  symbolAtSmtName :: (PPrint a) => Symbol -> SymEnv -> a -> FuncSort -> Text-symbolAtSmtName mkSym env e s =+symbolAtSmtName mkSym env e =   -- formerly: intSymbol mkSym . funcSortIndex env e-  appendSymbolText mkSym $ Text.pack (show (funcSortIndex env e s))+  appendSymbolText mkSym . Text.pack . show . funcSortIndex env e {-# SCC symbolAtSmtName #-}  funcSortIndex :: (PPrint a) => SymEnv -> a -> FuncSort -> Int-funcSortIndex env e z = M.lookupDefault err z (seAppls env)+funcSortIndex env e fs = M.lookupDefault err fs (seAppls env)   where-    err               = panic ("Unknown func-sort: " ++ showpp z ++ " for " ++ showpp e)+    err = panic ("Unknown func-sort: " ++ show fs ++ " for " ++ showpp e)  ffuncSort :: SymEnv -> Sort -> FuncSort ffuncSort env t      = {- tracepp ("ffuncSort " ++ showpp (t1,t2)) -} (tx t1, tx t2)@@ -213,7 +269,7 @@  data Sem   = Uninterp      -- ^ for UDF: `len`, `height`, `append`-  | Ctor         -- ^ for ADT constructor and tests: `cons`, `nil`+  | Ctor          -- ^ for ADT constructor and tests: `cons`, `nil`   | Test          -- ^ for ADT tests : `is$cons`   | Field         -- ^ for ADT field: `hd`, `tl`   | Theory        -- ^ for theory ops: mem, cup, select@@ -230,9 +286,8 @@   | SBool   | SReal   | SString-  -- TODO remove these now that we use SArray directly-  | SSet-  | SMap+  | SSet !SmtSort+  | SBag !SmtSort   | SArray !SmtSort !SmtSort   | SBitVec !Int   | SVar    !Int@@ -251,7 +306,7 @@ --   '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) else id) $ -}  go . unAbs $ t+sortSmtSort poly env t = {- tracepp ("sortSmtSort: " ++ showpp t) $ -} go . unAbs $ t   where     m = sortAbs t     go (FFunc _ _)    = SInt@@ -271,10 +326,11 @@ fappSmtSort poly m env = go   where -- HKT    go t@(FVar _) ts            = SApp (sortSmtSort poly env <$> (t:ts))-    go (FTC c) _-      | setConName == symbol c  = SSet-    go (FTC c) _-      | mapConName == symbol c  = SMap++    go (FTC c) [a]+      | setConName == symbol c  = SSet (sortSmtSort poly env a)+    go (FTC c) [a]+      | bagConName == symbol c  = SBag (sortSmtSort poly env a)     go (FTC c) [a, b]       | arrayConName == symbol c = SArray (sortSmtSort poly env a) (sortSmtSort poly env b)     go (FTC bv) [FTC s]@@ -298,8 +354,8 @@   pprintTidy _ SBool        = text "Bool"   pprintTidy _ SReal        = text "Real"   pprintTidy _ SString      = text "Str"-  pprintTidy _ SSet         = text "Set"-  pprintTidy _ SMap         = text "Map"+  pprintTidy k (SSet a)     = ppParens k (text "Set") [a]+  pprintTidy k (SBag a)     = ppParens k (text "Bag") [a]   pprintTidy k (SArray a b) = ppParens k (text "Array") [a, b]   pprintTidy _ (SBitVec n)  = text "BitVec" <+> int n   pprintTidy _ (SVar i)     = text "@" <-> int i@@ -313,13 +369,14 @@ -- | Coercing sorts inside environments for SMT theory encoding -------------------------------------------------------------------------------- -coerceSortEnv :: SEnv Sort -> SEnv Sort-coerceSortEnv ss = coerceSetToArray <$> ss+coerceSortEnv :: ElabFlags -> SEnv Sort -> SEnv Sort+coerceSortEnv ef ss = (if elabSetBag ef then coerceSetBagToArray else id) . coerceMapToArray <$> ss -coerceEnv :: SymEnv -> SymEnv-coerceEnv env = SymEnv { seSort   = coerceSortEnv (seSort env)-                       , seTheory = seTheory env-                       , seData   = seData   env-                       , seLits   = seLits   env-                       , seAppls  = seAppls  env-                       }+coerceEnv :: ElabFlags -> SymEnv -> SymEnv+coerceEnv slv env =+  SymEnv { seSort   = coerceSortEnv slv (seSort env)+         , seTheory = seTheory env+         , seData   = seData   env+         , seLits   = seLits   env+         , seAppls  = seAppls  env+         }

@@ -6,17 +6,19 @@ {-# LANGUAGE BangPatterns  #-}  {-# OPTIONS_GHC -Wno-name-shadowing #-}+{-# LANGUAGE InstanceSigs #-}  module Language.Fixpoint.Types.Visitor (   -- * Visitor-     Visitor (..)+     Folder (..)+  ,  Foldable (..)   ,  Visitable (..)    -- * Extracting Symbolic Constants (String Literals)   ,  SymConsts (..)    -- * Default Visitor-  , defaultVisitor+  , defaultFolder    -- * Transformers   , trans@@ -37,6 +39,8 @@   -- * Coercion Substitutions   , CoSub   , applyCoSub+  , CoSubV+  , applyCoSubV    -- * Predicates on Constraints   , isConcC , isConc, isKvarC@@ -55,11 +59,15 @@ import qualified Data.List           as L import           Language.Fixpoint.Types hiding (mapSort) import qualified Language.Fixpoint.Misc as Misc+import Control.Monad.Reader+import GHC.IO (unsafePerformIO)+import Data.IORef (newIORef, readIORef, IORef, modifyIORef')+import Prelude hiding (Foldable)    -data Visitor acc ctx = Visitor {+data Folder acc ctx = Visitor {  -- | Context @ctx@ is built in a "top-down" fashion; not "across" siblings     ctxExpr :: ctx -> Expr -> ctx @@ -71,9 +79,9 @@   }  ----------------------------------------------------------------------------------defaultVisitor :: (Monoid acc) => Visitor acc ctx+defaultFolder :: (Monoid acc) => Folder acc ctx ----------------------------------------------------------------------------------defaultVisitor = Visitor+defaultFolder = Visitor   { ctxExpr    = const   , txExpr     = \_ x -> x   , accExpr    = \_ _ -> mempty@@ -81,81 +89,164 @@  ------------------------------------------------------------------------ -fold         :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a-fold v c a t = snd $ execVisitM v c a visit t--trans        :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t-trans v c _ z = fst $ execVisitM v c mempty visit z--execVisitM :: Visitor a ctx -> ctx -> a -> (Visitor a ctx -> ctx -> t -> State a t) -> t -> (t, a)-execVisitM v c a f x = runState (f v c x) a--type VisitM acc = State acc+fold         :: (Foldable t, Monoid a) => Folder a ctx -> ctx -> a -> t -> a+fold v c a t = snd $ execVisitM v c a foldE t -accum :: (Monoid a) => a -> VisitM a ()-accum !z = modify (mappend z)-  -- do-  -- !cur <- get-  -- put ((mappend $!! z) $!! cur)+-- trans is always passed () () for a and t so we don't need to use the visitor pattern+-- trans        :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t+-- trans !v !c !_ !z = fst $ execVisitM v c mempty visit z  class Visitable t where-  visit :: (Monoid a) => Visitor a c -> c -> t -> VisitM a t+  transE :: (Expr -> Expr) -> t -> t +trans :: Visitable t => (Expr -> Expr) -> t -> t+trans f t = transE f t+ instance Visitable Expr where-  visit = visitExpr+  transE f = vE+    where+      vE e = step e' where e' = f e+      step e@(ESym _)       = e+      step e@(ECon _)       = e+      step e@(EVar _)       = e+      step (EApp e1 e2)       = EApp (vE e1) (vE e2)+      step (ENeg e)         = ENeg (vE e)+      step (EBin o e1 e2)   = EBin o (vE e1) (vE e2)+      step (EIte p e1 e2)   = EIte (vE p) (vE e1) (vE e2)+      step (ECst e t)       = ECst (vE e) t+      step (PAnd ps)        = PAnd (map vE ps)+      step (POr ps)         = POr (map vE ps)+      step (PNot p)         = PNot (vE p)+      step (PImp p1 p2)     = PImp (vE p1) (vE p2)+      step (PIff p1 p2)     = PIff (vE p1) (vE p2)+      step (PAtom r e1 e2)  = PAtom r (vE e1) (vE e2)+      step (PAll xts p)     = PAll xts (vE p)+      step (ELam (x,t) e)   = ELam (x,t) (vE e)+      step (ECoerc a t e)   = ECoerc a t (vE e)+      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 (PGrad k su i e) = PGrad k su i (vE e)  instance Visitable Reft where-  visit v c (Reft (x, ra)) = Reft . (x, ) <$> visit v c ra+  transE v (Reft (x, ra)) = Reft (x, transE v ra)  instance Visitable SortedReft where-  visit v c (RR t r) = RR t <$> visit v c r+  transE v (RR t r) = RR t (transE v r)  instance Visitable (Symbol, SortedReft, a) where-  visit v c (sym, sr, a) = (sym, ,a) <$> visit v c sr+  transE f (sym, sr, a) = (sym, transE f sr, a)  instance Visitable (BindEnv a) where-  visit v c = mapM (visit v c)+  transE v be = be { beBinds = M.map (transE v) (beBinds be) } +instance (Visitable (c a)) => Visitable (GInfo c a) where+  transE f x = x {+    cm = transE f <$> cm x+    , bs = transE f (bs x)+    , ae = transE f (ae x)+    }++instance Visitable (SimpC a) where+  transE v x = x {+    _crhs = transE v (_crhs x)+  }++instance Visitable (SubC a) where+  transE v x = x {+    slhs = transE v (slhs x),+    srhs = transE v (srhs x)+  }++instance Visitable AxiomEnv where+  transE v x = x {+    aenvEqs = transE v <$> aenvEqs x,+    aenvSimpl = transE v <$> aenvSimpl x+  }+    +instance Visitable Equation where+  transE v eq = eq {+    eqBody = transE v (eqBody eq)+  }++instance Visitable Rewrite where+  transE v rw = rw {+    smBody = transE v (smBody rw)+  }++execVisitM :: Folder a ctx -> ctx -> a -> (Folder a ctx -> ctx -> t -> FoldM a t) -> t -> (t, a)+execVisitM !v !c !a !f !x = unsafePerformIO $ do+  rn <- newIORef a+  result <- runReaderT (f v c x) rn+  finalAcc <- readIORef rn+  return (result, finalAcc) ++type FoldM acc = ReaderT (IORef acc) IO++accum :: (Monoid a) => a -> FoldM a ()+accum !z = do +  ref <- ask+  liftIO $ modifyIORef' ref (mappend z)++class Foldable t where+  foldE :: (Monoid a) => Folder a c -> c -> t -> FoldM a t++instance Foldable Expr where+  foldE = foldExpr++instance Foldable Reft where+  foldE v c (Reft (x, ra)) = Reft . (x, ) <$> foldE v c ra++instance Foldable SortedReft where+  foldE v c (RR t r) = RR t <$> foldE v c r++instance Foldable (Symbol, SortedReft, a) where+  foldE v c (sym, sr, a) = (sym, ,a) <$> foldE v c sr++instance Foldable (BindEnv a) where+  foldE v c = mapM (foldE v c)+ --------------------------------------------------------------------------------- -- WARNING: these instances were written for mapKVars over GInfos only; -- check that they behave as expected before using with other clients.-instance Visitable (SimpC a) where-  visit v c x = do-    rhs' <- visit v c (_crhs x)+instance Foldable (SimpC a) where+  foldE v c x = do+    rhs' <- foldE v c (_crhs x)     return x { _crhs = rhs' } -instance Visitable (SubC a) where-  visit v c x = do-    lhs' <- visit v c (slhs x)-    rhs' <- visit v c (srhs x)+instance Foldable (SubC a) where+  foldE v c x = do+    lhs' <- foldE v c (slhs x)+    rhs' <- foldE v c (srhs x)     return x { slhs = lhs', srhs = rhs' } -instance (Visitable (c a)) => Visitable (GInfo c a) where-  visit v c x = do-    cm' <- mapM (visit v c) (cm x)-    bs' <- visit v c (bs x)-    ae' <- visit v c (ae x)+instance (Foldable (c a)) => Foldable (GInfo c a) where+  foldE v c x = do+    cm' <- mapM (foldE v c) (cm x)+    bs' <- foldE v c (bs x)+    ae' <- foldE v c (ae x)     return x { cm = cm', bs = bs', ae = ae' } -instance Visitable AxiomEnv where-  visit v c x = do-    eqs'    <- mapM (visit v c) (aenvEqs   x)-    simpls' <- mapM (visit v c) (aenvSimpl x)+instance Foldable AxiomEnv where+  foldE v c x = do+    eqs'    <- mapM (foldE v c) (aenvEqs   x)+    simpls' <- mapM (foldE v c) (aenvSimpl x)     return x { aenvEqs = eqs' , aenvSimpl = simpls'} -instance Visitable Equation where-  visit v c eq = do-    body' <- visit v c (eqBody eq)+instance Foldable Equation where+  foldE v c eq = do+    body' <- foldE v c (eqBody eq)     return eq { eqBody = body' } -instance Visitable Rewrite where-  visit v c rw = do-    body' <- visit v c (smBody rw)+instance Foldable Rewrite where+  foldE v c rw = do+    body' <- foldE v c (smBody rw)     return rw { smBody = body' }  ----------------------------------------------------------------------------------visitExpr :: (Monoid a) => Visitor a ctx -> ctx -> Expr -> VisitM a Expr-visitExpr !v    = vE+foldExpr :: (Monoid a) => Folder a ctx -> ctx -> Expr -> FoldM a Expr+foldExpr !v    = vE   where     vE !c !e    = do {- SCC "visitExpr.vE.accum" -} accum acc                      {- SCC "visitExpr.vE.step" -}  step c' e'@@ -191,57 +282,125 @@     f' (kv', _) = f kv'  mapKVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t-mapKVars' f            = trans kvVis () ()+mapKVars' f = trans txK   where-    kvVis              = defaultVisitor { txExpr = txK }-    txK _ (PKVar k su)+    txK (PKVar k su)       | Just p' <- f (k, su) = subst su p'-    txK _ (PGrad k su _ _)+    txK (PGrad k su _ _)       | Just p' <- f (k, su) = subst su p'-    txK _ p            = p+    txK p = p    mapGVars' :: Visitable t => ((KVar, Subst) -> Maybe Expr) -> t -> t-mapGVars' f            = trans kvVis () ()+mapGVars' f            = trans txK   where-    kvVis              = defaultVisitor { txExpr = txK }-    txK _ (PGrad k su _ _)+    txK (PGrad k su _ _)       | Just p' <- f (k, su) = subst su p'-    txK _ p            = p+    txK p            = p  mapExpr :: Visitable t => (Expr -> Expr) -> t -> t-mapExpr f = trans (defaultVisitor {txExpr = const f}) () ()+mapExpr f = trans f  -- | Specialized and faster version of mapExpr for expressions mapExprOnExpr :: (Expr -> Expr) -> Expr -> Expr mapExprOnExpr f = go   where-    go e0 = f $ case e0 of-      EApp f e -> EApp (go f) (go e)-      ENeg e -> ENeg (go e)-      EBin o e1 e2 ->  EBin o (go e1) (go e2)-      EIte p e1 e2 -> EIte (go p) (go e1) (go e2)-      ECst e t -> ECst (go e) t-      PAnd ps -> PAnd (map go ps)-      POr ps -> POr (map go ps)-      PNot p -> PNot (go p)-      PImp p1 p2 -> PImp (go p1) (go p2)-      PIff p1 p2 -> PIff (go p1) (go p2)-      PAtom r e1 e2 -> PAtom r (go e1) (go e2)-      PAll xts p -> PAll xts (go p)-      ELam (x,t) e -> ELam (x,t) (go e)-      ECoerc a t e -> ECoerc a t (go e)-      PExist xts p -> PExist xts (go p)-      ETApp e s -> ETApp (go e) s-      ETAbs e s -> ETAbs (go e) s-      PGrad k su i e -> PGrad k su i (go e)+    go !e0 = f $! case e0 of+      EApp f e ->+        let !f' = go f+            !e' = go e+        in EApp f' e'+      ENeg e ->+        let !e' = go e+        in ENeg e'+      EBin o e1 e2 ->+        let !e1' = go e1+            !e2' = go e2+        in EBin o e1' e2'+      EIte p e1 e2 ->+        let !p' = go p+            !e1' = go e1+            !e2' = go e2+        in EIte p' e1' e2'+      ECst e t ->+        let !e' = go e+        in ECst e' t+      PAnd ps ->+        let !ps' = map go ps+        in PAnd ps'+      POr ps ->+        let !ps' = map go ps+        in POr ps'+      PNot p ->+        let !p' = go p+        in PNot p'+      PImp p1 p2 ->+        let !p1' = go p1+            !p2' = go p2+        in PImp p1' p2'+      PIff p1 p2 ->+        let !p1' = go p1+            !p2' = go p2+        in PIff p1' p2'+      PAtom r e1 e2 ->+        let !e1' = go e1+            !e2' = go e2+        in PAtom r e1' e2'+      PAll xts p ->+        let !p' = go p+        in PAll xts p'+      ELam (x,t) e ->+        let !e' = go e+        in ELam (x,t) e'+      ECoerc a t e ->+        let !e' = go e+        in ECoerc a t e'+      PExist xts p ->+        let !p' = go p+        in PExist xts p'+      ETApp e s ->+        let !e' = go e+        in ETApp e' s+      ETAbs e s ->+        let !e' = go e+        in ETAbs e' s+      PGrad k su i e ->+        let !e' = go e+        in PGrad k su i e'       e@PKVar{} -> e       e@EVar{} -> e       e@ESym{} -> e       e@ECon{} -> e +-- mapExprOnExpr :: (Expr -> Expr) -> Expr -> Expr+-- mapExprOnExpr f = go+--   where+--     go !e0 = f $! case e0 of+--       EApp f e -> EApp !(go f) !(go e)+--       ENeg e -> ENeg (go e)+--       EBin o e1 e2 ->  EBin o (go e1) (go e2)+--       EIte p e1 e2 -> EIte (go p) (go e1) (go e2)+--       ECst e t -> ECst (go e) t+--       PAnd ps -> PAnd (map go ps)+--       POr ps -> POr (map go ps)+--       PNot p -> PNot (go p)+--       PImp p1 p2 -> PImp (go p1) (go p2)+--       PIff p1 p2 -> PIff (go p1) (go p2)+--       PAtom r e1 e2 -> PAtom r (go e1) (go e2)+--       PAll xts p -> PAll xts (go p)+--       ELam (x,t) e -> ELam (x,t) (go e)+--       ECoerc a t e -> ECoerc a t (go e)+--       PExist xts p -> PExist xts (go p)+--       ETApp e s -> ETApp (go e) s+--       ETAbs e s -> ETAbs (go e) s+--       PGrad k su i e -> PGrad k su i (go e)+--       e@PKVar{} -> e+--       e@EVar{} -> e+--       e@ESym{} -> e+--       e@ECon{} -> e + mapMExpr :: (Monad m) => (Expr -> m Expr) -> Expr -> m Expr mapMExpr f = go   where@@ -269,12 +428,11 @@     go (POr ps)        = f . POr =<< (go `traverse` ps)  mapKVarSubsts :: Visitable t => (KVar -> Subst -> Subst) -> t -> t-mapKVarSubsts f          = trans kvVis () ()+mapKVarSubsts f          = trans txK   where-    kvVis                = defaultVisitor { txExpr = txK }-    txK _ (PKVar k su)   = PKVar k (f k su)-    txK _ (PGrad k su i e) = PGrad k (f k su) i e-    txK _ p              = p+    txK (PKVar k su)   = PKVar k (f k su)+    txK (PGrad k su i e) = PGrad k (f k su) i e+    txK p              = p  newtype MInt = MInt Integer -- deriving (Eq, NFData) @@ -283,32 +441,33 @@  instance Monoid MInt where   mempty  = MInt 0+  mappend :: MInt -> MInt -> MInt   mappend = (<>) -size :: Visitable t => t -> Integer+size :: Foldable t => t -> Integer size t    = n   where     MInt n = fold szV () mempty t-    szV    = (defaultVisitor :: Visitor MInt t) { accExpr = \ _ _ -> MInt 1 }+    szV    = (defaultFolder :: Folder MInt t) { accExpr = \ _ _ -> MInt 1 }  -lamSize :: Visitable t => t -> Integer+lamSize :: Foldable t => t -> Integer lamSize t    = n   where     MInt n = fold szV () mempty t-    szV    = (defaultVisitor :: Visitor MInt t) { accExpr = accum }+    szV    = (defaultFolder :: Folder MInt t) { accExpr = accum }     accum _ (ELam _ _) = MInt 1     accum _ _          = MInt 0 -eapps :: Visitable t => t -> [Expr]+eapps :: Foldable t => t -> [Expr] eapps                 = fold eappVis () []   where-    eappVis              = (defaultVisitor :: Visitor [KVar] t) { accExpr = eapp' }+    eappVis              = (defaultFolder :: Folder [KVar] t) { accExpr = eapp' }     eapp' _ e@(EApp _ _) = [e]     eapp' _ _            = []  {-# SCC kvarsExpr #-}-kvarsExpr :: Expr -> [KVar]+kvarsExpr :: ExprV v -> [KVar] kvarsExpr = go []   where     go acc e0 = case e0 of@@ -395,6 +554,21 @@     fS t              = t     txV a             = M.lookupDefault (FObj a) a coSub ++type CoSubV = M.HashMap Sort Sort++applyCoSubV :: CoSubV -> Expr -> Expr+applyCoSubV coSub = 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 e              = e++    txS               = mapSortOnlyOnce fS++    fS t              = M.lookupDefault t t coSub+ --------------------------------------------------------------------------------- -- | Visitors over @Sort@ ---------------------------------------------------------------------------------@@ -494,9 +668,9 @@ instance SymConsts Expr where   symConsts = getSymConsts -getSymConsts :: Visitable t => t -> [SymConst]+getSymConsts :: Foldable t => t -> [SymConst] getSymConsts         = fold scVis () []   where-    scVis            = (defaultVisitor :: Visitor [SymConst] t)  { accExpr = sc }+    scVis            = (defaultFolder :: Folder [SymConst] t)  { accExpr = sc }     sc _ (ESym c)    = [c]     sc _ _           = []