content: --------------------------------------------------------------------------------
  -- | This module implements "Proof by Logical Evaluation" where we
  --   unfold function definitions if they *must* be unfolded, to strengthen
  --   the environments with function-definition-equalities.
  --   The algorithm is discussed at length in:
  --
  --     1. "Refinement Reflection", POPL 2018, https://arxiv.org/pdf/1711.03842
  --     2. "Reasoning about Functions", VMCAI 2018, https://ranjitjhala.github.io/static/reasoning-about-functions.pdf
  --------------------------------------------------------------------------------
  
  {-# LANGUAGE OverloadedStrings         #-}
  {-# LANGUAGE PartialTypeSignatures     #-}
  {-# LANGUAGE TupleSections             #-}
  {-# LANGUAGE FlexibleInstances         #-}
  {-# LANGUAGE PatternGuards             #-}
  {-# LANGUAGE RecordWildCards           #-}
  {-# LANGUAGE ExistentialQuantification #-}
  {-# LANGUAGE DoAndIfThenElse           #-}
  
  module Language.Fixpoint.Solver.PLE
    ( instantiate
  
    -- The following exports are for property testing.
    , FuelCount(..)
    , ICtx(..)
    , Knowledge(..)
    , simplify
    )
    where
  
  import           Language.Fixpoint.Types hiding (simplify)
  import           Language.Fixpoint.Types.Config  as FC
  import           Language.Fixpoint.Types.Solutions (CMap)
  import qualified Language.Fixpoint.Types.Visitor as Vis
  import qualified Language.Fixpoint.Misc          as Misc
  import qualified Language.Fixpoint.Smt.Interface as SMT
  import           Language.Fixpoint.Smt.Types (SmtM)
  import           Language.Fixpoint.Defunctionalize
  import           Language.Fixpoint.Solver.EnvironmentReduction (inlineInExpr, undoANF)
  import qualified Language.Fixpoint.Utils.Files   as Files
  import qualified Language.Fixpoint.Utils.Trie    as T
  import           Language.Fixpoint.Utils.Progress
  import           Language.Fixpoint.SortCheck
  import           Language.Fixpoint.Graph.Deps             (isTarget)
  import           Language.Fixpoint.Solver.Common          (askSMT, toSMT)
  import           Language.Fixpoint.Solver.Sanitize        (symbolEnv)
  import           Language.Fixpoint.Solver.Simplify
  import           Language.Fixpoint.Solver.Rewrite as Rewrite
  
  import Language.REST.OCAlgebra as OC
  import Language.REST.ExploredTerms as ExploredTerms
  import Language.REST.RuntimeTerm as RT
  import Language.REST.SMT (withZ3, SolverHandle)
  
  import           Control.Exception.Base (bracket)
  import           Control.Monad (filterM, foldM, forM_, when, replicateM)
  import           Control.Monad.State
  import           Control.Monad.Trans.Maybe
  import           Data.Bifunctor (second)
  import qualified Data.HashMap.Strict  as M
  import qualified Data.HashMap.Lazy  as HashMap.Lazy
  import qualified Data.HashSet         as S
  import           Data.IORef
  import qualified Data.List            as L
  import           Data.Map (Map)
  import qualified Data.Map as Map
  import qualified Data.Maybe           as Mb
  import qualified Data.Set as Set
  import           Text.PrettyPrint.HughesPJ.Compat
  
  mytracepp :: (PPrint a) => String -> a -> a
  mytracepp = notracepp
  
  --------------------------------------------------------------------------------
  -- | Strengthen Constraint Environments via PLE
  --------------------------------------------------------------------------------
  {-# SCC instantiate #-}
  instantiate :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
  instantiate cfg fi' subcIds = do
      let cs = M.filterWithKey
                 (\i c -> isPleCstr aEnv i c && maybe True (i `L.elem`) subcIds)
                 (cm info)
      let t  = mkCTrie (M.toList cs)                                          -- 1. BUILD the Trie
      res   <- withRESTSolver $ \solver ->
                 withProgress (1 + M.size cs) $
                 withCtx cfg file sEnv (defns fi') $
                 do env <- instEnv cfg info cs solver
                    pleTrie t env                                             -- 2. TRAVERSE Trie to compute InstRes
      liftIO $ savePLEEqualities cfg info sEnv res
      return $ resSInfo cfg sEnv info res                                     -- 3. STRENGTHEN SInfo using InstRes
    where
      withRESTSolver :: (Maybe SolverHandle -> IO a) -> IO a
      withRESTSolver f | all null (M.elems $ aenvAutoRW aEnv) = f Nothing
      withRESTSolver f = withZ3 (f . Just)
  
      file = srcFile cfg ++ ".evals"
      sEnv = symbolEnv cfg info
      aEnv = ae info
      info = normalize fi'
  
  savePLEEqualities :: Config -> SInfo a -> SymEnv -> InstRes -> IO ()
  savePLEEqualities cfg info sEnv res = when (save cfg) $ do
      let fq   = queryFile Files.Fq cfg ++ ".ple"
      putStrLn $ "\nSaving PLE equalities: "   ++ fq ++ "\n"
      Misc.ensurePath fq
      let constraint_equalities =
            map equalitiesPerConstraint $ Misc.hashMapToAscList $ cm info
      writeFile fq $ render $ vcat $
        map renderConstraintRewrite constraint_equalities
    where
      equalitiesPerConstraint (cid, c) =
        (cid, L.sort [ e | i <- elemsIBindEnv (senv c), Just e <- [M.lookup i res] ])
      elabParam = ElabParam (solverFlags $ solver cfg) "savePLEEqualities" sEnv
      renderConstraintRewrite (cid, eqs) =
        "constraint id" <+> text (show cid ++ ":")
        $+$ nest 2
             (vcat $ L.intersperse "" $
              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 elabParam (Just boolSort)) $
              concatMap conjuncts eqs
             )
        $+$ ""
  
  -------------------------------------------------------------------------------
  -- | Step 1a: @instEnv@ sets up the incremental-PLE environment
  instEnv :: (Loc a) => Config -> SInfo a -> CMap (SimpC a) -> Maybe SolverHandle -> SmtM (InstEnv a)
  instEnv cfg info cs restSolver = do
      ctx <- get
      refRESTCache <- liftIO $ newIORef mempty
      refRESTSatCache <- liftIO $ newIORef mempty
      let
          restOrd = FC.restOC cfg
          oc0 = ordConstraints restOrd $ Mb.fromJust restSolver
          oc :: OCAlgebra OCType RuntimeTerm IO
          oc = oc0
               { OC.isSat = cachedIsSat refRESTSatCache oc0
               , OC.notStrongerThan = cachedNotStrongerThan refRESTCache oc0
               }
          et :: ExploredTerms RuntimeTerm OCType IO
          et = ExploredTerms.empty
                 EF
                   { ExploredTerms.union = OC.union oc
                   , ExploredTerms.subsumes = OC.notStrongerThan oc
                   , exRefine = OC.refine oc
                   }
                   ExploreWhenNeeded
          s0 = EvalEnv
                { evEnv = SMT.ctxSymEnv ctx
                , evElabF = ef
                , evKCtx = ctx
                , evPendingUnfoldings = mempty
                , evNewEqualities = mempty
                , evSMTCache = mempty
                , evFuel = defFuelCount cfg
                , freshEtaNames = 0
                , explored = Just et
                , restSolver = restSolver
                , restOCA = restOrd
                , evOCAlgebra = oc
                }
      return $ InstEnv
         { ieCfg = cfg
         , ieBEnv = bs info
         , ieAenv = ae info
         , ieCstrs = cs
         , ieKnowl = knowledge cfg 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
          Nothing -> do
            nst <- OC.notStrongerThan oc a b
            writeIORef refRESTCache (M.insert (a, b) nst m)
            return nst
          Just nst ->
            return nst
  
      cachedIsSat refRESTSatCache oc a = do
        m <- readIORef refRESTSatCache
        case M.lookup a m of
          Nothing -> do
            sat <- OC.isSat oc a
            writeIORef refRESTSatCache (M.insert a sat m)
            return sat
          Just sat ->
            return sat
  
  ----------------------------------------------------------------------------------------------
  -- | Step 1b: @mkCTrie@ builds the @Trie@ of constraints indexed by their environments
  --
  -- The trie is a way to unfold the equalities a minimum number of times.
  -- Say you have
  --
  -- > 1: [1, 2, 3, 4, 5] => p1
  -- > 2: [1, 2, 3, 6, 7] => p2
  --
  -- Then you build the tree
  --
  -- >  1 -> 2 -> 3 -> 4 -> 5 — [Constraint 1]
  -- >            | -> 6 -> 7 — [Constraint 2]
  --
  -- which you use to unfold everything in 1, 2, and 3 once (instead of twice)
  -- and with the proper existing environment
  --
  mkCTrie :: [(SubcId, SimpC a)] -> CTrie
  mkCTrie ics  = T.fromList [ (cBinds c, i) | (i, c) <- ics ]
    where
      cBinds   = L.sort . elemsIBindEnv . senv
  
  ----------------------------------------------------------------------------------------------
  -- | Step 2: @pleTrie@ walks over the @CTrie@ to actually do the incremental-PLE
  pleTrie :: CTrie -> InstEnv a -> SmtM InstRes
  pleTrie t env = loopT env ctx0 diff0 Nothing res0 t
    where
      diff0        = []
      res0         = M.empty
      ctx0         = ICtx
        { 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
    :: InstEnv a
    -> ICtx
    -> Diff         -- ^ The longest path suffix without forks in reverse order
    -> Maybe BindId -- ^ bind id of the branch ancestor of the trie if any.
                    --   'Nothing' when this is the top-level trie.
    -> InstRes
    -> CTrie
    -> SmtM InstRes
  loopT env ictx delta i res t = case t of
    T.Node []  -> return res
    T.Node [b] -> loopB env ictx delta i res b
    T.Node bs  -> withAssms env ictx delta Nothing $ \ictx' -> do
                    (ictx'', env'', res') <- ple1 env ictx' i res
                    foldM (loopB env'' ictx'' [] i) res' bs
  
  loopB
    :: InstEnv a
    -> ICtx
    -> Diff         -- ^ The longest path suffix without forks in reverse order
    -> Maybe BindId -- ^ bind id of the branch ancestor of the branch if any.
                    --   'Nothing' when this is a branch of the top-level trie.
    -> InstRes
    -> CBranch
    -> SmtM InstRes
  loopB env ictx delta iMb res b = case b of
    T.Bind i t -> loopT env ictx (i:delta) (Just i) res t
    T.Val cid  -> withAssms env ictx delta (Just cid) $ \ictx' -> do
                    liftIO progressTick
                    (\(_, _, r) -> r) <$> ple1 env ictx' iMb res
  
  -- | Adds to @ctx@ candidate expressions to unfold from the bindings in @delta@
  -- and the rhs of @cidMb@.
  --
  -- Adds to @ctx@ assumptions from @env@ and @delta@.
  --
  -- Sets the current constraint id in @ctx@ to @cidMb@.
  --
  -- Pushes assumptions from the modified context to the SMT solver, runs @act@,
  -- and then pops the assumptions.
  --
  withAssms :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (ICtx -> SmtM b) -> SmtM b
  withAssms env ctx delta cidMb act = do
    sctx <- get
    let ictx' = updCtx env sctx ctx delta cidMb
    let assms = icAssms ictx'
  
    SMT.smtBracket "PLE.withAssms" $ do
      forM_ assms SMT.smtAssertDecl
      act $ ictx' { icAssms = mempty }
  
  -- | @ple1@ performs the PLE at a single "node" in the Trie
  --
  -- It will generate equalities for all function invocations in the candidates
  -- in @ctx@ for which definitions are known. The function definitions are in
  -- @ieKnowl@.
  ple1 :: InstEnv a -> ICtx -> Maybe BindId -> InstRes -> SmtM (ICtx, InstEnv a, InstRes)
  ple1 ie@InstEnv{..} ictx i res = do
    ctx <- get
    (ictx', env) <- liftIO $ runStateT (evalCandsLoop ieCfg ictx ieKnowl) (ieEvEnv { evKCtx = ctx })
    put $ evKCtx env
    let pendings = collectPendingUnfoldings env (icSubcId ictx)
        newEqs = pendings ++ S.toList (S.difference (icEquals ictx') (icEquals ictx))
    return (ictx', ie { ieEvEnv = env }, updCtxRes res i newEqs)
    where
      -- Pending unfoldings (i.e. with undecided guards) are collected only
      -- when we reach a leaf in the Trie, and only if the user asked for them.
      collectPendingUnfoldings env (Just _) | pleUndecGuards ieCfg =
        M.toList (evPendingUnfoldings env)
      collectPendingUnfoldings _ _ = []
  
  evalToSMT :: String -> Config -> SMT.Context -> (Expr, Expr) -> Pred
  evalToSMT msg cfg ctx (e1,e2) = toSMT ("evalToSMT:" ++ msg) cfg ctx [] (EEq e1 e2)
  
  -- | Generate equalities for all function invocations in the candidates
  -- in @ctx@ for which definitions are known. The function definitions are in
  -- @ieKnowl@.
  --
  -- In pseudocode:
  --
  -- > do
  -- >     for every candidate
  -- >         discover equalities,
  -- >         unfold function invocations,
  -- >         update candidates with the unfolded expressions
  -- >     send newly discovered equalities to the SMT solver
  -- > until no new equalities are discovered
  -- >       or the environment becomes inconsistent
  --
  evalCandsLoop :: Config -> ICtx -> Knowledge -> EvalST ICtx
  evalCandsLoop cfg ictx0 γ = go ictx0 0
    where
      go :: ICtx -> Int -> EvalST ICtx
      go ictx _ | S.null (icCands ictx) = return ictx
      go ictx i = do
        inconsistentEnv <- testForInconsistentEnvironment
        if inconsistentEnv
          then return ictx
          else do liftSMT $ SMT.smtAssertDecl (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 ctx' <- gets evKCtx
                                let eqsSMT = evalToSMT "evalCandsLoop" cfg ctx' `S.map` unknownEqs
                                    ictx'' = ictx { icEquals = icEquals ictx <> unknownEqs
                                                   , icAssms  = S.filter (not . isTautoPred) eqsSMT }
                                go (ictx'' { icCands = S.fromList (concat candss) }) (i + 1)
  
      testForInconsistentEnvironment :: EvalST Bool
      testForInconsistentEnvironment =
        liftSMT $ knPreds γ (knLams γ) PFalse
  
      eqCand [e0] e1 = e0 == e1
      eqCand _ _ = False
  
  ----------------------------------------------------------------------------------------------
  -- | Step 3: @resSInfo@ uses incremental PLE result @InstRes@ to produce the strengthened SInfo
  ----------------------------------------------------------------------------------------------
  
  resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
  resSInfo cfg env info res = strengthenBinds info res'
    where
      res'     = M.fromList $ zip 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)
  
  ----------------------------------------------------------------------------------------------
  -- | @InstEnv@ has the global information needed to do PLE
  ----------------------------------------------------------------------------------------------
  
  data InstEnv a = InstEnv
    { ieCfg   :: !Config
    , ieBEnv  :: !(BindEnv a)
    , ieAenv  :: !AxiomEnv
    , ieCstrs :: !(CMap (SimpC a))
    , ieKnowl :: !Knowledge
    , ieEvEnv :: !EvalEnv
    , ieLRWs  :: LocalRewritesEnv
    }
  
  ----------------------------------------------------------------------------------------------
  -- | @ICtx@ is the local information -- at each trie node -- obtained by incremental PLE
  ----------------------------------------------------------------------------------------------
  
  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
    , 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
    }
  
  ----------------------------------------------------------------------------------------------
  -- | @InstRes@ is the final result of PLE; a map from @BindId@ to the equations "known" at that BindId
  ----------------------------------------------------------------------------------------------
  
  type InstRes = M.HashMap BindId Expr
  
  ----------------------------------------------------------------------------------------------
  -- | @Unfold is the result of running PLE at a single equality;
  --     (e, [(e1, e1')...]) is the source @e@ and the (possible empty)
  --   list of PLE-generated equalities (e1, e1') ...
  ----------------------------------------------------------------------------------------------
  
  type CTrie   = T.Trie   SubcId
  type CBranch = T.Branch SubcId
  type Diff    = [BindId]    -- ^ in "reverse" order
  
  equalitiesPred :: [(Expr, Expr)] -> [Expr]
  equalitiesPred eqs = [ EEq e1 e2 | (e1, e2) <- eqs, e1 /= e2 ]
  
  updCtxRes :: InstRes -> Maybe BindId -> [(Expr, Expr)] -> InstRes
  updCtxRes res iMb = updRes res iMb . pAndNoDedup . equalitiesPred
  
  
  updRes :: InstRes -> Maybe BindId -> Expr -> InstRes
  updRes res (Just i) e = M.insertWith (error "tree-like invariant broken in ple. See https://github.com/ucsd-progsys/liquid-fixpoint/issues/496") i e res
  updRes res  Nothing _ = res
  
  ----------------------------------------------------------------------------------------------
  -- | @updCtx env ctx delta cidMb@ adds the assumptions and candidates from @delta@ and @cidMb@
  --   to the context.
  ----------------------------------------------------------------------------------------------
  
  updCtx :: InstEnv a -> SMT.Context -> ICtx -> Diff -> Maybe SubcId -> ICtx
  updCtx InstEnv{..} ieSMT ictx delta cidMb =
    ictx { icAssms  = S.fromList (filter (not . isTautoPred) ctxEqs)
         , icCands  = S.fromList deANFedCands <> icCands ictx
         , icSimpl  = icSimpl ictx <> econsts
         , icSubcId = cidMb
         , icANFs   = anfBinds
         , icLRWs   = mconcat $ icLRWs ictx : newLRWs
         }
    where
      cands     = rhs:es
      anfBinds  = bs : icANFs ictx
      econsts   = M.fromList $ findConstants ieKnowl es
      ctxEqs    = toSMT "updCtx" ieCfg ieSMT [] <$> L.nub
                    [ c | xr <- bs, c <- conjuncts (expr xr), null (Vis.kvarsExpr c) ]
      bs        = second unApplySortedReft <$> binds
      rhs       = unApply eRhs
      es        = expr <$> bs
      eRhs      = maybe PTrue crhs subMb
      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 ictx
           || icEtaBetaFlag ictx then
          deANF anfBinds cands
        else
          cands
  
  
  findConstants :: Knowledge -> [Expr] -> [(Expr, Expr)]
  findConstants γ es = [(EVar x, c) | (x,c) <- go [] (concatMap splitPAnd es)]
    where
      go su ess = if ess == ess'
                    then su
                    else go (su ++ su') ess'
         where ess' = subst (mkSubst su') <$> ess
               su'  = makeSu ess
      makeSu exprs  = [(x,c) | (EEq (EVar x) c) <- exprs
                             , isConstant (knDCs γ) c
                             , EVar x /= c ]
  
  getCstr :: M.HashMap SubcId (SimpC a) -> SubcId -> SimpC a
  getCstr env cid = Misc.safeLookup "Instantiate.getCstr" cid env
  
  isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool
  isPleCstr aenv subid c = isTarget c && M.lookupDefault False subid (aenvExpand aenv)
  
  type EvEqualities = S.HashSet (Expr, Expr)
  
  --------------------------------------------------------------------------------
  data EvalEnv = EvalEnv
    { evEnv      :: !SymEnv
    , evElabF    :: ElabFlags
    , evKCtx     :: SMT.Context
      -- | Equalities where we couldn't evaluate the guards
    , evPendingUnfoldings :: M.HashMap Expr Expr
    , evNewEqualities :: EvEqualities -- ^ Equalities discovered during a traversal of
                                      -- an expression
    , 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
    , restOCA    :: RESTOrdering
    , evOCAlgebra :: OCAlgebra OCType RuntimeTerm IO
    }
  
  data FuelCount = FC
    { fcMap :: M.HashMap Symbol Int
    , fcMax :: Maybe Int
    }
    deriving (Show)
  
  defFuelCount :: Config -> FuelCount
  defFuelCount cfg = FC mempty (fuel cfg)
  
  type EvalST a = StateT EvalEnv IO a
  
  liftSMT :: SmtM a -> EvalST a
  liftSMT k =
    do es <- get
       let ctx = evKCtx es
       (a, ctx') <- lift $ runStateT k ctx
       put (es {evKCtx = ctx'})
       pure a
  
  --------------------------------------------------------------------------------
  
  getAutoRws :: Knowledge -> Maybe SubcId -> [AutoRewrite]
  getAutoRws γ mSubcId =
    Mb.fromMaybe [] $ do
      cid <- mSubcId
      M.lookup cid $ knAutoRWs γ
  
  -- | Discover the equalities in an expression.
  --
  -- The discovered equalities are in the environment of the monad,
  -- and the list of produced expressions contains the result of unfolding
  -- definitions. When REST is in effect, more than one expression might
  -- be returned because expressions can then be rewritten in more than one
  -- way.
  evalOne :: Knowledge -> ICtx -> Int -> Expr -> EvalST [Expr]
  evalOne γ ctx i e
    | 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
          rp = RP (contramap Rewrite.convert oc) [(e, PLE)] constraints
          constraints = OC.top oc
          emptyET = ExploredTerms.empty (EF (OC.union oc) (OC.notStrongerThan oc) (OC.refine oc)) ExploreWhenNeeded
      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:
  --   add(x, y) = if x == 0 then y else add(x - 1, y + 1)
  -- And a rewrite rule:
  --   forall a, b . add(a,b) -> add(b, a)
  -- Then the expression add(t, add(2, 1)) would evaluate under NoRW to:
  --   if t == 0 then 3 else add(t - 1, 4)
  -- However, under FuncNormal, it would evaluate to: add(t, 3)
  -- Thus, FuncNormal could engage the rewrite rule add(t, 3) = add(3, t)
  
  
  data EvalType =
      NoRW       -- Normal PLE
    | FuncNormal -- REST: Expand function definitions only when the branch can be decided
    | RWNormal   -- REST: Fully Expand Defs in the context of rewriting (similar to NoRW)
    deriving (Eq)
  
  -- Indicates whether or not the evaluation has expanded a function statement
  -- into a conditional branch.
  -- In this case, rewriting should stop
  -- It's unclear whether or not rewriting in either branch makes sense,
  -- since one branch could be an ill-formed expression.
  newtype FinalExpand = FE Bool deriving (Show)
  
  noExpand :: FinalExpand
  noExpand = FE False
  
  expand :: FinalExpand
  expand = FE True
  
  mapFE :: (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
  mapFE f (e, fe) = (f e, fe)
  
  feVal :: FinalExpand -> Bool
  feVal (FE f) = f
  
  feAny :: [FinalExpand] -> FinalExpand
  feAny xs = FE $ any feVal xs
  
  infixl 9 <|>
  (<|>) :: FinalExpand -> FinalExpand -> FinalExpand
  (<|>) (FE True) _ = expand
  (<|>) _         f = f
  
  
  feSeq :: [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
  feSeq xs = (map fst xs, feAny (map snd xs))
  
  -- | Unfolds function invocations in expressions.
  --
  -- Also reduces if-then-else when the boolean condition or the negation can be
  -- proved valid. This is the actual implementation of guard-validation-before-unfolding
  -- that is described in publications.
  --
  -- 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
      go (ELam (x,s) e)   = evalELam γ ctx et (x, s) e
      go e@EIte{}         = evalIte γ ctx et e
      go (ECoerc s t e)   = mapFE (ECoerc s t)  <$> go e
      go e@(EApp _ _)     =
        case splitEAppThroughECst e of
         (f, es) | et == RWNormal ->
            -- Just evaluate the arguments first, to give rewriting a chance to step in
            -- if necessary
            do
              (es', finalExpand) <- feSeq <$> mapM (eval γ ctx et) es
              if es /= es'
                then return (eApps f es', finalExpand)
                else do
                  (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', 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)  <- go e
                               return (ENeg e', fe)
      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
      go (PNot e')        = mapFE PNot <$> go e'
      go (PImp e1 e2)     = binOp PImp e1 e2
      go (PIff e1 e2)     = binOp PIff e1 e2
      go (PAnd es)        = efAll PAnd (go `traverse` es)
      go (POr es)         = efAll POr (go `traverse` es)
      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) <- go e
                               return (ECst e' t, fe)
      go (ELet x e1 e2)   = do (e1', fe1) <- go e1
                               (e2', fe2) <- go e2
                               return (ELet x e1' e2', fe1 <|> fe2)
  
      go e                = return (e, noExpand)
  
      binOp f e1 e2 = do
        (e1', fe1) <- go e1
        (e2', fe2) <- go e2
        return (f e1' e2', fe1 <|> fe2)
  
      efAll f mes = do
        xs <- mes
        let (xs', fe) = feSeq xs
        return (f xs', fe)
  
  -- | 'evalELam' 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
      -- Discard the old equalities which miss the lambda binding
      modify $ \st -> st
        { evPendingUnfoldings = oldPendingUnfoldings
        , evNewEqualities = S.insert (elam, ELam (x, s) e2') oldEqs
        -- Leaving the scope thus we need to get rid of it
        , evEnv = deleteSymEnv x $ evEnv st
        }
      return (ELam (x, s) e', fe)
  
  data RESTParams oc = RP
    { oc   :: OCAlgebra oc Expr IO
    , path :: [(Expr, TermOrigin)]
    , c    :: oc
    }
  
  -- 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 = 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
  -- as pairs @(original_subexpression, rewritten_subexpression)@.
  --
  -- Also folds constants.
  --
  -- The main difference with 'eval' is that 'evalREST' takes into account
  -- autorewrites.
  --
  evalREST :: Knowledge -> ICtx -> RESTParams OCType -> EvalST [Expr]
  evalREST γ ctx rp = do
    env <- get
    cacheRef <- liftIO $ newIORef $ evSMTCache env
    evalRESTWithCache cacheRef γ ctx [] rp
  
  evalRESTWithCache
    :: IORef (M.HashMap Expr Bool) -> Knowledge -> ICtx -> [Expr] -> RESTParams OCType -> EvalST [Expr]
  evalRESTWithCache cacheRef _ ctx acc rp
    | pathExprs <- map fst (mytracepp "EVAL1: path" $ path rp)
    , e         <- last pathExprs
    , Just v    <- M.lookup e (icSimpl ctx)
    = do
      smtCache <- liftIO $ readIORef cacheRef
      when (v /= e) $ modify (\st -> st
        { evNewEqualities = S.insert (e, v) (evNewEqualities st)
        , evSMTCache = smtCache
        })
      return (v : acc)
  
  evalRESTWithCache cacheRef γ ctx acc rp =
    do
      mexploredTerms <- gets explored
      case mexploredTerms of
        Nothing -> return acc
        Just exploredTerms -> do
          se <- liftIO (shouldExploreTerm exploredTerms exprs)
          if se then do
            possibleRWs <- liftSMT 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
  
            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 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
  
            newEqualities <- gets evNewEqualities
            smtCache <- liftIO $ readIORef cacheRef
            modify $ \st -> st
              { evNewEqualities  = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd
              , evSMTCache = smtCache
              , explored = explored' st
              }
  
            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
          RWTerminationCheckDisabled ->
            return $ not $ ExploredTerms.visited (Rewrite.convert e) exploredTerms
          RWTerminationCheckEnabled  ->
            ExploredTerms.shouldExplore (Rewrite.convert e) (c rp) exploredTerms
      shouldExploreTerm _ _ = return False
  
      allowed (_, rwE, _) | rwE `elem` pathExprs = return False
      allowed (_, _, c)   = termCheck c
      termCheck c = Rewrite.passesTerminationCheck (oc rp) rwArgs c
  
      notVisitedFirst exploredTerms rws =
        let
          (v, nv) = L.partition (\(_, e, _) -> ExploredTerms.visited (Rewrite.convert e) exploredTerms) rws
        in
          nv ++ v
  
      rpEval newEqualities e' =
        let
          c' =
            if any isRW (path rp)
              then foldr (\(e1, e2) ctrs -> refine (oc rp) ctrs e1 e2) (c rp) (S.toList newEqualities)
              else c rp
  
        in
          rp{path = path rp ++ [(e', PLE)], c = c'}
  
      isRW (_, r) = r == RW
  
      rpRW (_, e', c') = rp{path = path rp ++ [(e', RW)], c = c' }
  
      pathExprs       = map fst (mytracepp "EVAL2: path" $ path rp)
      exprs           = last pathExprs
      autorws         = getAutoRws γ (icSubcId ctx)
  
      rwArgs = RWArgs (isValid cacheRef γ) $ knRWTerminationOpts γ
  
      getRWs =
        do
          -- Optimization: If we got here via rewriting, then the current constraints
          -- are satisfiable; otherwise double-check that rewriting is still allowed
          ok <-
            if isRW $ last (path rp)
              then return True
              else liftIO $ termCheck (c rp)
          if ok
            then
              do
                let getRW e ar = Rewrite.getRewrite (oc rp) rwArgs (c rp) e ar
                let getRWs' s  = Mb.catMaybes <$> mapM (runMaybeT . getRW s) autorws
                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)
  evalApp γ ctx e0 es et
    | EVar f <- dropECst e0
    , Just eq <- Map.lookup f (knAms γ)
    , length (eqArgs eq) <= length es
    = do
         env <- gets (seSort . evEnv)
         okFuel <- checkFuel f
         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
  
           (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.
      -- However, using pleUnfold still has the advantage of not generating
      -- extra equations to unfold pleUnfold itself. Using pleUnfold also
      -- makes the intention of the user rather explicit.
      stripPLEUnfold e
        | (ef, [arg]) <- splitEAppThroughECst e
        , EVar f <- dropECst ef
        , f == "Language.Haskell.Liquid.ProofCombinators.pleUnfold"
        = 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
    , EVar dc <- dropECst d
    , Just rws <- Map.lookup dc (knSims γ)
      -- User data measures aren't sent to the SMT solver because
      -- it knows already about selectors and constructor tests.
    , Just (rw, isUserDataSMeasure) <- L.find (\(rw, _) -> smName rw == f) rws
    , length as == length (smArgs rw)
    = 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) }
      return (Just newE, noExpand)
  
  evalApp γ ctx e0 es _et
    | eqs@(_:_) <- noUserDataMeasureEqs γ (eApps e0 es)
    = do
         let eqs' = map (second $ simplify γ ctx) eqs
         modify $ \st ->
           st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }
         return (Nothing, 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
        case b' of
          Just True -> evalIte γ ctx et e1
          Just False -> evalIte γ ctx et e2
          _ -> return (EIte b e1 e2, expand)
  evalIte _ _ _ e' = return (e', noExpand)
  
  -- | Creates equations that explain how to rewrite a given constructor
  -- application with all measures that aren't user data measures
  noUserDataMeasureEqs :: Knowledge -> Expr -> [(Expr,Expr)]
  noUserDataMeasureEqs γ e =
    [ (EApp (EVar $ smName rw) e, subst (mkSubst $ zip (smArgs rw) es) (smBody rw))
    | (ef, es) <- [splitEAppThroughECst e]
    , EVar f <- [dropECst ef]
    , Just rws <- [Map.lookup f (knSims γ)]
    , (rw, NoUserDataSMeasure) <- rws
    , length es == length (smArgs rw)
    ]
  
  --------------------------------------------------------------------------------
  -- | 'substEq' unfolds or instantiates an equation at a particular list of
  --   argument values. We must also substitute the sort-variables that appear
  --   as coercions. See tests/proof/ple1.fq
  --------------------------------------------------------------------------------
  substEq :: SEnv Sort -> Equation -> [Expr] -> Expr
  substEq env eq es = subst su (substEqCoerce env eq es)
    where su = mkSubst $ zip (eqArgNames eq) es
  
  substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
  substEqCoerce env eq es = Vis.applyCoSubV coSub $ eqBody eq
    where
      ts    = snd    <$> eqArgs eq
      sp    = panicSpan "mkCoSub"
      eTs   = sortExpr sp env <$> es
      coSub = mkCoSub env eTs ts
  
  -- | @mkCoSub senv eTs xTs = su@ creates a substitution @su@ such that
  -- @subst su xTs == eTs@.
  --
  -- The variables in the domain of the substitution are those that appear
  -- as @FObj symbol@ in @xTs@.
  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 -> [(Sort, Sort)]
  matchSorts = go
    where
      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
      go _             _             = []
  
  --------------------------------------------------------------------------------
  
  eqArgNames :: Equation -> [Symbol]
  eqArgNames = map fst . eqArgs
  
  isValidCached :: Knowledge -> Expr -> EvalST (Maybe Bool)
  isValidCached γ e = do
    env <- get
    case M.lookup e (evSMTCache env) of
      Nothing -> do
        let isFreeInE (s, _) = not (S.member s (exprSymbolsSet e))
        b <- liftSMT $ knPreds γ (knLams γ) e
        if b
          then do
            when (all isFreeInE (knLams γ)) $
              put (env { evSMTCache = M.insert e True (evSMTCache env) })
            return (Just True)
          else do
            b2 <- liftSMT $ knPreds γ (knLams γ) (PNot e)
            if b2
              then do
                when (all isFreeInE (knLams γ)) $
                  put (env { evSMTCache = M.insert e False (evSMTCache env) })
                return (Just False)
              else
                return Nothing
  
      mb -> return mb
  
  --------------------------------------------------------------------------------
  -- | Knowledge (SMT Interaction)
  --------------------------------------------------------------------------------
  data Knowledge = KN
    { -- | Rewrites rules came from match definitions
      --
      -- They are grouped by the data constructor that they unfold, and are
      -- augmented with an attribute that say whether they originate from a
      -- user data declaration.
      knSims              :: Map Symbol [(Rewrite, IsUserDataSMeasure)]
    , knAms               :: Map Symbol Equation -- ^ All function definitions
    , knPreds             :: [(Symbol, Sort)] -> Expr -> SmtM Bool
    , knLams              :: ![(Symbol, Sort)]
    , knSummary           :: ![(Symbol, Int)]     -- ^ summary of functions to be evaluates (knSims and knAsms) with their arity
    , knDCs               :: !(S.HashSet Symbol)  -- ^ data constructors drawn from Rewrite
    , knDataCtors         :: !(M.HashMap Symbol DataCtor) -- ^ data constructors by name
    , knSels              :: !SelectorMap
    , knConsts            :: !ConstDCMap
    , knAutoRWs           :: M.HashMap SubcId [AutoRewrite]
    , knRWTerminationOpts :: RWTerminationOpts
    }
  
  -- | A type to express whether SMeasures originate from data definitions.
  -- That is whether they are constructor tests, selectors, or something else.
  data IsUserDataSMeasure = NoUserDataSMeasure | UserDataSMeasure
    deriving (Eq, Show)
  
  isValid :: IORef (M.HashMap Expr Bool) -> Knowledge -> Expr -> SmtM Bool
  isValid cacheRef γ e = do
      smtCache <- liftIO $ readIORef cacheRef
      case M.lookup e smtCache of
        Nothing -> do
          b <- knPreds γ (knLams γ) e
          when b $
            liftIO $ writeIORef cacheRef (M.insert e True smtCache)
          return b
        Just b -> return b
  
  knowledge :: Config -> SInfo a -> Knowledge
  knowledge cfg si = KN
    { knSims                     = Map.fromListWith (++) $
                                     [ (smDC rw, [(rw, NoUserDataSMeasure)]) | rw <- sims ] ++
                                     [ (smDC rw, [(rw, UserDataSMeasure)]) | rw <- dataSims ]
    , knAms                      = Map.fromList [(eqName eq, eq) | eq <- aenvEqs aenv]
    , knPreds                    = askSMT cfg
    , knLams                     = []
    , knSummary                  =    ((\s -> (smName s, 1)) <$> sims)
                                   ++ ((\s -> (eqName s, length (eqArgs s))) <$> aenvEqs aenv)
                                   ++ rwSyms
    , knDCs                      = S.fromList (smDC <$> sims)
    , knDataCtors                = M.fromList [ (val (dcName dc), dc) | dd <- ddecls si, dc <- ddCtors dd ]
    , knSels                     = Mb.mapMaybe makeSel  sims
    , knConsts                   = Mb.mapMaybe makeCons sims
    , knAutoRWs                  = aenvAutoRW aenv
    , knRWTerminationOpts        =
        if rwTermination cfg
        then RWTerminationCheckEnabled
        else RWTerminationCheckDisabled
    }
    where
      (simDCTests, sims0) =
        partitionUserDataConstructorTests (ddecls si) $ aenvSimpl aenv
      (simDCSelectors, sims) =
        partitionUserDataConstructorSelectors (ddecls si) sims0
      dataSims = simDCTests ++ simDCSelectors
      aenv = ae si
  
      inRewrites :: Symbol -> Bool
      inRewrites e =
        let
          symbs = Mb.mapMaybe (lhsHead . arLHS) (concat $ M.elems $ aenvAutoRW aenv)
        in
          e `L.elem` symbs
  
      lhsHead :: Expr -> Maybe Symbol
      lhsHead e | (ef, _) <- splitEAppThroughECst e, EVar f <- dropECst ef = Just f
      lhsHead _ = Nothing
  
  
      rwSyms = filter (inRewrites . fst) $ map toSum (toListSEnv (gLits si))
        where
          toSum (sym, sort)      = (sym, getArity sort)
  
          getArity (FFunc _ rhs) = 1 + getArity rhs
          getArity _             = 0
  
  
  
      makeCons rw
        | null (syms $ smBody rw)
        = Just (smName rw, (smDC rw, smBody rw))
        | otherwise
        = Nothing
  
      makeSel rw
        | EVar x <- smBody rw
        = (smName rw,) . (smDC rw,) <$> L.elemIndex x (smArgs rw)
        | otherwise
        = Nothing
  
  -- | Partitions the input rewrites into constructor tests and others.
  --
  -- We don't need to deal in PLE with data constructor tests. That is,
  -- functions of the form @isCons :: List a -> Bool@ or @isNil :: List a -> Bool@
  -- when @List a@ is defined by the user.
  --
  -- The SMT solver knows about these functions when datatypes are declared to it,
  -- so PLE doesn't need to unfold them.
  --
  -- Non-user defined datatypes like @[a]@ still need to have tests unfolded
  -- because they are not declared as datatypes to the SMT solver.
  --
  -- Also, REST could need this functions unfolded since otherwise it may not
  -- discover possible rewrites.
  --
  partitionUserDataConstructorTests :: [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
  partitionUserDataConstructorTests dds rws = L.partition isDataConstructorTest rws
    where
      isDataConstructorTest sm = isTestSymbol (smName sm) && S.member (smDC sm) userDefinedDcs
      userDefinedDcs =
        S.fromList [ symbol (dcName dc) | dd <- dds, dc <- ddCtors dd ]
  
  -- | Like 'partitionUserDataConstructorTests' but for selectors.
  partitionUserDataConstructorSelectors :: [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
  partitionUserDataConstructorSelectors dds rws = L.partition isSelector rws
    where
      isSelector sm = S.member (smName sm) userDefinedDcFieldsSelectors
      userDefinedDcFieldsSelectors =
        S.fromList [ symbol dcf | dd <- dds, dc <- ddCtors dd, dcf <- dcFields dc ]
  
  
  --------------------------------------------------------------------------------
  --------------------------------------------------------------------------------
  --------------------------------------------------------------------------------
  
  withCtx :: Config -> FilePath -> SymEnv -> DefinedFuns -> SmtM a -> IO a
  withCtx cfg file env defns k =
    bracket acquire release $
      evalStateT $ SMT.smtPush >> k   -- TODO why is there no pop?
    where
      acquire = SMT.makeContextWithSEnv cfg file env defns
      release = SMT.cleanupContext
  
  -- (sel_i, D, i), meaning sel_i (D x1 .. xn) = xi,
  -- i.e., sel_i selects the ith value for the data constructor D
  type SelectorMap = [(Symbol, (Symbol, Int))]
  type ConstDCMap = [(Symbol, (Symbol, Expr))]
  
  -- ValueMap maps expressions to constants (including data constructors)
  type ConstMap = M.HashMap Expr Expr
  type LDataCon = Symbol              -- Data Constructors
  
  isConstant :: S.HashSet LDataCon -> Expr -> Bool
  isConstant dcs e = S.null (S.difference (exprSymbolsSet e) dcs)
  
  simplify :: Knowledge -> ICtx -> Expr -> Expr
  simplify γ ictx exprs = mytracepp ("simplification of " ++ showpp exprs) $ fix' (Vis.mapExprOnExpr tx) exprs
      where
        fix' f e = if e == e' then e else fix' f e' where e' = f e
        tx e
          | Just e' <- M.lookup e (icSimpl ictx)
          = e'
  
        tx (PAtom rel e1 e2) = applyBooleanFolding rel e1 e2
        tx (EBin bop e1 e2) = applyConstantFolding bop e1 e2
        tx (ENeg e)         = applyConstantFolding Minus (ECon (I 0)) e
        tx (EApp e1 e2)
          | isSetPred e1    = applySetFolding e1 e2
  
        tx (EApp ef a)
          | EVar f <- dropECst ef
          , Just (dc, c)  <- L.lookup f (knConsts γ)
          , (ed, _) <- splitEAppThroughECst a
          , EVar dc' <- dropECst ed
          , dc == dc'
          = c
        tx (EIte b e1 e2)
          | isTautoPred b  = e1
          | isContraPred b = e2
        tx (ECoerc s t e)
          | s == t = e
        tx (EApp ef a)
          | EVar f <- dropECst ef
          , Just (dc, i)  <- L.lookup f (knSels γ)
          , (ed, es) <- splitEAppThroughECst a
          , EVar dc' <- dropECst ed
          , dc == dc'
          = es!!i
        tx e = e
  
  
  -------------------------------------------------------------------------------
  -- | Normalization of Equation: make their arguments unique -------------------
  -------------------------------------------------------------------------------
  
  class Normalizable a where
    normalize :: a -> a
  
  instance Normalizable (GInfo c a) where
    normalize si = si {ae = normalize $ ae si}
  
  instance Normalizable AxiomEnv where
    normalize aenv = aenv { aenvEqs   = mytracepp "aenvEqs"  (normalize <$> aenvEqs   aenv)
                          , aenvSimpl = mytracepp "aenvSimpl" (normalize <$> aenvSimpl aenv) }
  
  instance Normalizable Rewrite where
    normalize rw = rw { smArgs = xs', smBody = normalizeBody (smName rw) $ subst su $ smBody rw }
      where
        su  = mkSubst $ zipWith (\x y -> (x,EVar y)) xs xs'
        xs  = smArgs rw
        xs' = zipWith mkSymbol xs [0 :: Integer ..]
        mkSymbol x i = x `suffixSymbol` intSymbol (smName rw) i
  
  
  instance Normalizable Equation where
    normalize eq = eq {eqArgs = zip xs' ss, eqBody = normalizeBody (eqName eq) $ subst su $ eqBody eq }
      where
        su      = mkSubst $ zipWith (\x y -> (x,EVar y)) xs xs'
        (xs,ss) = unzip (eqArgs eq)
        xs'     = zipWith mkSymbol xs [0 :: Integer ..]
        mkSymbol x i = x `suffixSymbol` intSymbol (eqName eq) i
  
  -- | Normalize the given named expression if it is recursive.
  normalizeBody :: Symbol -> Expr -> Expr
  normalizeBody f exprs | f `elem` syms exprs = go exprs
    where
      -- @go@ performs this simplification:
      --     (c => e1) /\ ((not c) => e2) --> if c then e1 else e2
      -- and then recurses into  e2.
      --
      -- The expressions originate from Haskell's reflect annotations, so we know
      -- that e1 is a conjunction of data constructor checkers and we do not need
      -- to recurse into e1.
      go (PAnd [PImp c e1, PImp (PNot c') e2]) | c == c' = EIte c e1 (go e2)
      go e                                               = e
  normalizeBody _ e = e -- The expression is not recursive, return it unchanged.
  
  -- -- TODO:FUEL Config
  -- maxFuel :: Int
  -- maxFuel = 11
  
  -- | Increment the fuel count of the given symbol in the current evaluation
  -- environment.
  useFuel :: Symbol -> EvalST ()
  useFuel f = do
    modify (\st -> st { evFuel = useFuelCount f (evFuel st) })
  
  -- | Increment the fuel count.
  useFuelCount :: Symbol -> FuelCount -> FuelCount
  useFuelCount f fc = fc { fcMap = M.insert f (k + 1) m }
    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.
  checkFuel :: Symbol -> EvalST Bool
  checkFuel f = do
    fc <- gets evFuel
    case (M.lookup f (fcMap fc), fcMax fc) of
      (Just fk, Just n) -> pure (fk <= n)
      _                 -> pure True
  