--------------------------------------------------------------------------------
-- | 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 FlexibleContexts          #-}
{-# 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, Solution)
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.Solution (CombinedEnv(..), applyInSortedReft)
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.Monad (filterM, foldM, forM_, when, replicateM, zipWithM)
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 :: forall a. PPrint a => [Char] -> a -> a
mytracepp = [Char] -> a -> a
forall a. PPrint a => [Char] -> a -> a
notracepp

--------------------------------------------------------------------------------
-- | Strengthen Constraint Environments via PLE
--
-- @instantiate cfg fi subcIds@ yields @F.bs fi@ strengthened with the
-- unfoldings discovered by PLE on the constraints in @subcIds@ (or all
-- constraints if @subcIds == Nothing@).
{-# SCC instantiate #-}
instantiate :: (Loc a) => Config -> SInfo a -> Maybe Solution -> Maybe [SubcId] -> SmtM (BindEnv a)
instantiate :: forall a.
Loc a =>
Config
-> SInfo a -> Maybe Solution -> Maybe [SubcId] -> SmtM (BindEnv a)
instantiate Config
cfg SInfo a
fi' Maybe Solution
mSol Maybe [SubcId]
subcIds = do
    let cs :: HashMap SubcId (SimpC a)
cs = (SubcId -> SimpC a -> Bool)
-> HashMap SubcId (SimpC a) -> HashMap SubcId (SimpC a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey
               (\SubcId
i SimpC a
c -> AxiomEnv -> SubcId -> SimpC a -> Bool
forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aEnv SubcId
i SimpC a
c Bool -> Bool -> Bool
&& Bool -> ([SubcId] -> Bool) -> Maybe [SubcId] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i SubcId -> [SubcId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds)
               (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
info)
    let t :: CTrie
t  = [(SubcId, SimpC a)] -> CTrie
forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie (HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId (SimpC a)
cs)                                          -- 1. BUILD the Trie
    InstRes
res   <- (Maybe SolverHandle -> SmtM InstRes) -> SmtM InstRes
forall a. (Maybe SolverHandle -> SmtM a) -> SmtM a
withRESTSolver ((Maybe SolverHandle -> SmtM InstRes) -> SmtM InstRes)
-> (Maybe SolverHandle -> SmtM InstRes) -> SmtM InstRes
forall a b. (a -> b) -> a -> b
$ \Maybe SolverHandle
solver -> do
               Context
ctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
               (InstRes
res, Context
ctx') <- IO (InstRes, Context) -> StateT Context IO (InstRes, Context)
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (InstRes, Context) -> StateT Context IO (InstRes, Context))
-> IO (InstRes, Context) -> StateT Context IO (InstRes, Context)
forall a b. (a -> b) -> a -> b
$ (SmtM InstRes -> IO (InstRes, Context))
-> Int -> SmtM InstRes -> IO (InstRes, Context)
forall (m :: * -> *) a b. (m a -> IO b) -> Int -> m a -> IO b
withProgressM (SmtM InstRes -> Context -> IO (InstRes, Context)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` Context
ctx) (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ HashMap SubcId (SimpC a) -> Int
forall k v. HashMap k v -> Int
M.size HashMap SubcId (SimpC a)
cs) (SmtM InstRes -> IO (InstRes, Context))
-> SmtM InstRes -> IO (InstRes, Context)
forall a b. (a -> b) -> a -> b
$ do
                 InstEnv a
env <- Config
-> SInfo a
-> Maybe Solution
-> HashMap SubcId (SimpC a)
-> Maybe SolverHandle
-> SmtM (InstEnv a)
forall a.
Loc a =>
Config
-> SInfo a
-> Maybe Solution
-> CMap (SimpC a)
-> Maybe SolverHandle
-> SmtM (InstEnv a)
instEnv Config
cfg SInfo a
info Maybe Solution
mSol HashMap SubcId (SimpC a)
cs Maybe SolverHandle
solver
                 CTrie -> InstEnv a -> SmtM InstRes
forall a. Loc a => CTrie -> InstEnv a -> SmtM InstRes
pleTrie CTrie
t InstEnv a
env                                              -- 2. TRAVERSE Trie to compute InstRes
               Context -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Context
ctx'
               InstRes -> SmtM InstRes
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return InstRes
res
    IO () -> StateT Context IO ()
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ Config -> SInfo a -> SymEnv -> InstRes -> IO ()
forall a. Config -> SInfo a -> SymEnv -> InstRes -> IO ()
savePLEEqualities Config
cfg SInfo a
info SymEnv
sEnv InstRes
res
    BindEnv a -> SmtM (BindEnv a)
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (BindEnv a -> SmtM (BindEnv a)) -> BindEnv a -> SmtM (BindEnv a)
forall a b. (a -> b) -> a -> b
$ Config -> SymEnv -> SInfo a -> InstRes -> BindEnv a
forall a. Config -> SymEnv -> SInfo a -> InstRes -> BindEnv a
resSInfo Config
cfg SymEnv
sEnv SInfo a
info InstRes
res                                     -- 3. STRENGTHEN SInfo using InstRes
  where
    withRESTSolver :: (Maybe SolverHandle -> SmtM a) -> SmtM a
    withRESTSolver :: forall a. (Maybe SolverHandle -> SmtM a) -> SmtM a
withRESTSolver Maybe SolverHandle -> SmtM a
f | ([AutoRewrite] -> Bool) -> [[AutoRewrite]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all [AutoRewrite] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (HashMap SubcId [AutoRewrite] -> [[AutoRewrite]]
forall k v. HashMap k v -> [v]
M.elems (HashMap SubcId [AutoRewrite] -> [[AutoRewrite]])
-> HashMap SubcId [AutoRewrite] -> [[AutoRewrite]]
forall a b. (a -> b) -> a -> b
$ AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
aEnv) = Maybe SolverHandle -> SmtM a
f Maybe SolverHandle
forall a. Maybe a
Nothing
    withRESTSolver Maybe SolverHandle -> SmtM a
f = (SolverHandle -> SmtM a) -> SmtM a
forall (m :: * -> *) b. MonadIO m => (SolverHandle -> m b) -> m b
withZ3 (Maybe SolverHandle -> SmtM a
f (Maybe SolverHandle -> SmtM a)
-> (SolverHandle -> Maybe SolverHandle) -> SolverHandle -> SmtM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverHandle -> Maybe SolverHandle
forall a. a -> Maybe a
Just)

    sEnv :: SymEnv
sEnv = Config -> SInfo a -> SymEnv
forall a. HasCallStack => Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
info
    aEnv :: AxiomEnv
aEnv = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
info
    info :: SInfo a
info = SInfo a -> SInfo a
forall a. Normalizable a => a -> a
normalize SInfo a
fi'

savePLEEqualities :: Config -> SInfo a -> SymEnv -> InstRes -> IO ()
savePLEEqualities :: forall a. Config -> SInfo a -> SymEnv -> InstRes -> IO ()
savePLEEqualities Config
cfg SInfo a
info SymEnv
sEnv InstRes
res = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
save Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let fq :: [Char]
fq   = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
".ple"
    [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"\nSaving PLE equalities: "   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
    [Char] -> IO ()
Misc.ensurePath [Char]
fq
    let constraint_equalities :: [(SubcId, [Expr])]
constraint_equalities =
          ((SubcId, SimpC a) -> (SubcId, [Expr]))
-> [(SubcId, SimpC a)] -> [(SubcId, [Expr])]
forall a b. (a -> b) -> [a] -> [b]
map (SubcId, SimpC a) -> (SubcId, [Expr])
forall {c :: * -> *} {a} {a}.
TaggedC c a =>
(a, c a) -> (a, [Expr])
equalitiesPerConstraint ([(SubcId, SimpC a)] -> [(SubcId, [Expr])])
-> [(SubcId, SimpC a)] -> [(SubcId, [Expr])]
forall a b. (a -> b) -> a -> b
$ HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall a b. Ord a => HashMap a b -> [(a, b)]
Misc.hashMapToAscList (HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)])
-> HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
info
    [Char] -> [Char] -> IO ()
writeFile [Char]
fq ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      ((SubcId, [Expr]) -> Doc) -> [(SubcId, [Expr])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SubcId, [Expr]) -> Doc
forall {a} {t :: * -> *}.
(Show a, Foldable t) =>
(a, t Expr) -> Doc
renderConstraintRewrite [(SubcId, [Expr])]
constraint_equalities
  where
    equalitiesPerConstraint :: (a, c a) -> (a, [Expr])
equalitiesPerConstraint (a
cid, c a
c) =
      (a
cid, [Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
L.sort [ Expr
e | Int
i <- IBindEnv -> [Int]
elemsIBindEnv (c a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv c a
c), Just Expr
e <- [Int -> InstRes -> Maybe Expr
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Int
i InstRes
res] ])
    elabParam :: ElabParam
elabParam = ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (Config -> ElabFlags
solverFlags Config
cfg) Located [Char]
"savePLEEqualities" SymEnv
sEnv
    renderConstraintRewrite :: (a, t Expr) -> Doc
renderConstraintRewrite (a
cid, t Expr
eqs) =
      Doc
"constraint id" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (a -> [Char]
forall a. Show a => a -> [Char]
show a
cid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":")
      Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2
           ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
L.intersperse Doc
"" ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
            (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Expr -> Doc) -> (Expr -> Expr) -> Expr -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
unElab) ([Expr] -> [Doc]) -> [Expr] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Expr -> [Expr]
forall a. Set a -> [a]
Set.toList (Set Expr -> [Expr]) -> Set Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr] -> Set Expr
forall a. Ord a => [a] -> Set a
Set.fromList ([Expr] -> Set Expr) -> [Expr] -> Set Expr
forall a b. (a -> b) -> a -> b
$
            -- call elabExpr to try to bring equations that are missing
            -- some casts into a fully annotated form for comparison
            (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => ElabParam -> Maybe Sort -> Expr -> Expr
ElabParam -> Maybe Sort -> Expr -> Expr
elabExpr ElabParam
elabParam (Sort -> Maybe Sort
forall a. a -> Maybe a
Just Sort
boolSort)) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$
            (Expr -> [Expr]) -> t Expr -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts t Expr
eqs
           )
      Doc -> Doc -> Doc
$+$ Doc
""

-------------------------------------------------------------------------------
-- | Step 1a: @instEnv@ sets up the incremental-PLE environment
instEnv
  :: Loc a
  => Config
  -> SInfo a
  -> Maybe Solution
  -> CMap (SimpC a)
  -> Maybe SolverHandle
  -> SmtM (InstEnv a)
instEnv :: forall a.
Loc a =>
Config
-> SInfo a
-> Maybe Solution
-> CMap (SimpC a)
-> Maybe SolverHandle
-> SmtM (InstEnv a)
instEnv Config
cfg SInfo a
info Maybe Solution
s CMap (SimpC a)
cs Maybe SolverHandle
restSolver = do
    Context
ctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
    IORef (HashMap (OCType, OCType) Bool)
refRESTCache <- IO (IORef (HashMap (OCType, OCType) Bool))
-> StateT Context IO (IORef (HashMap (OCType, OCType) Bool))
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef (HashMap (OCType, OCType) Bool))
 -> StateT Context IO (IORef (HashMap (OCType, OCType) Bool)))
-> IO (IORef (HashMap (OCType, OCType) Bool))
-> StateT Context IO (IORef (HashMap (OCType, OCType) Bool))
forall a b. (a -> b) -> a -> b
$ HashMap (OCType, OCType) Bool
-> IO (IORef (HashMap (OCType, OCType) Bool))
forall a. a -> IO (IORef a)
newIORef HashMap (OCType, OCType) Bool
forall a. Monoid a => a
mempty
    IORef (HashMap OCType Bool)
refRESTSatCache <- IO (IORef (HashMap OCType Bool))
-> StateT Context IO (IORef (HashMap OCType Bool))
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef (HashMap OCType Bool))
 -> StateT Context IO (IORef (HashMap OCType Bool)))
-> IO (IORef (HashMap OCType Bool))
-> StateT Context IO (IORef (HashMap OCType Bool))
forall a b. (a -> b) -> a -> b
$ HashMap OCType Bool -> IO (IORef (HashMap OCType Bool))
forall a. a -> IO (IORef a)
newIORef HashMap OCType Bool
forall a. Monoid a => a
mempty
    let
        restOrd :: RESTOrdering
restOrd = Config -> RESTOrdering
FC.restOC Config
cfg
        oc0 :: OCAlgebra OCType RuntimeTerm IO
oc0 = RESTOrdering -> SolverHandle -> OCAlgebra OCType RuntimeTerm IO
ordConstraints RESTOrdering
restOrd (SolverHandle -> OCAlgebra OCType RuntimeTerm IO)
-> SolverHandle -> OCAlgebra OCType RuntimeTerm IO
forall a b. (a -> b) -> a -> b
$ Maybe SolverHandle -> SolverHandle
forall a. HasCallStack => Maybe a -> a
Mb.fromJust Maybe SolverHandle
restSolver
        oc :: OCAlgebra OCType RuntimeTerm IO
        oc :: OCAlgebra OCType RuntimeTerm IO
oc = OCAlgebra OCType RuntimeTerm IO
oc0
             { OC.isSat = cachedIsSat refRESTSatCache oc0
             , OC.notStrongerThan = cachedNotStrongerThan refRESTCache oc0
             }
        et :: ExploredTerms RuntimeTerm OCType IO
        et :: ExploredTerms RuntimeTerm OCType IO
et = ExploreFuncs RuntimeTerm OCType IO
-> ExploreStrategy -> ExploredTerms RuntimeTerm OCType IO
forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ExploredTerms.empty
               EF
                 { union :: OCType -> OCType -> OCType
ExploredTerms.union = OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
OC.union OCAlgebra OCType RuntimeTerm IO
oc
                 , subsumes :: OCType -> OCType -> IO Bool
ExploredTerms.subsumes = OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra OCType RuntimeTerm IO
oc
                 , exRefine :: OCType -> RuntimeTerm -> RuntimeTerm -> OCType
exRefine = OCAlgebra OCType RuntimeTerm IO
-> OCType -> RuntimeTerm -> RuntimeTerm -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
OC.refine OCAlgebra OCType RuntimeTerm IO
oc
                 }
                 ExploreStrategy
ExploreWhenNeeded
        s0 :: EvalEnv
s0 = EvalEnv
              { evEnv :: SymEnv
evEnv = Context -> SymEnv
SMT.ctxSymEnv Context
ctx
              , evElabF :: ElabFlags
evElabF = ElabFlags
ef
              , evKCtx :: Context
evKCtx = Context
ctx
              , evExScope :: ExScope
evExScope = []
              , evPendingUnfoldings :: HashMap ExScope (HashMap Expr Expr)
evPendingUnfoldings = HashMap ExScope (HashMap Expr Expr)
forall a. Monoid a => a
mempty
              , evNewEqualities :: EvEqualities
evNewEqualities = EvEqualities
forall a. Monoid a => a
mempty
              , evSMTCache :: HashMap Expr Bool
evSMTCache = HashMap Expr Bool
forall a. Monoid a => a
mempty
              , evFuel :: FuelCount
evFuel = Config -> FuelCount
defFuelCount Config
cfg
              , freshEtaNames :: Int
freshEtaNames = Int
0
              , explored :: Maybe (ExploredTerms RuntimeTerm OCType IO)
explored = ExploredTerms RuntimeTerm OCType IO
-> Maybe (ExploredTerms RuntimeTerm OCType IO)
forall a. a -> Maybe a
Just ExploredTerms RuntimeTerm OCType IO
et
              , restSolver :: Maybe SolverHandle
restSolver = Maybe SolverHandle
restSolver
              , restOCA :: RESTOrdering
restOCA = RESTOrdering
restOrd
              , evOCAlgebra :: OCAlgebra OCType RuntimeTerm IO
evOCAlgebra = OCAlgebra OCType RuntimeTerm IO
oc
              }
    InstEnv a -> SmtM (InstEnv a)
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (InstEnv a -> SmtM (InstEnv a)) -> InstEnv a -> SmtM (InstEnv a)
forall a b. (a -> b) -> a -> b
$ InstEnv
       { ieCfg :: Config
ieCfg = Config
cfg
       , ieBEnv :: BindEnv a
ieBEnv = SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
info
       , ieAenv :: AxiomEnv
ieAenv = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
info
       , ieCstrs :: CMap (SimpC a)
ieCstrs = CMap (SimpC a)
cs
       , ieKnowl :: Knowledge
ieKnowl = Config -> SInfo a -> Knowledge
forall a. Config -> SInfo a -> Knowledge
knowledge Config
cfg SInfo a
info
       , ieEvEnv :: EvalEnv
ieEvEnv = EvalEnv
s0
       , ieLRWs :: LocalRewritesEnv
ieLRWs  = SInfo a -> LocalRewritesEnv
forall (c :: * -> *) a. GInfo c a -> LocalRewritesEnv
lrws SInfo a
info
       , ieSol :: Maybe Solution
ieSol  = Maybe Solution
s
       }
  where
    ef :: ElabFlags
ef = Config -> ElabFlags
solverFlags Config
cfg

    cachedNotStrongerThan :: IORef (HashMap (c, c) Bool)
-> OCAlgebra c a IO -> c -> c -> IO Bool
cachedNotStrongerThan IORef (HashMap (c, c) Bool)
refRESTCache OCAlgebra c a IO
oc c
a c
b = do
      HashMap (c, c) Bool
m <- IORef (HashMap (c, c) Bool) -> IO (HashMap (c, c) Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap (c, c) Bool)
refRESTCache
      case (c, c) -> HashMap (c, c) Bool -> Maybe Bool
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup (c
a, c
b) HashMap (c, c) Bool
m of
        Maybe Bool
Nothing -> do
          Bool
nst <- OCAlgebra c a IO -> c -> c -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra c a IO
oc c
a c
b
          IORef (HashMap (c, c) Bool) -> HashMap (c, c) Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap (c, c) Bool)
refRESTCache ((c, c) -> Bool -> HashMap (c, c) Bool -> HashMap (c, c) Bool
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert (c
a, c
b) Bool
nst HashMap (c, c) Bool
m)
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
nst
        Just Bool
nst ->
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
nst

    cachedIsSat :: IORef (HashMap c Bool) -> OCAlgebra c a IO -> c -> IO Bool
cachedIsSat IORef (HashMap c Bool)
refRESTSatCache OCAlgebra c a IO
oc c
a = do
      HashMap c Bool
m <- IORef (HashMap c Bool) -> IO (HashMap c Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap c Bool)
refRESTSatCache
      case c -> HashMap c Bool -> Maybe Bool
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup c
a HashMap c Bool
m of
        Maybe Bool
Nothing -> do
          Bool
sat <- OCAlgebra c a IO -> c -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
OC.isSat OCAlgebra c a IO
oc c
a
          IORef (HashMap c Bool) -> HashMap c Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap c Bool)
refRESTSatCache (c -> Bool -> HashMap c Bool -> HashMap c Bool
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert c
a Bool
sat HashMap c Bool
m)
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
sat
        Just Bool
sat ->
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
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 :: forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
ics  = [([Int], SubcId)] -> CTrie
forall a. [([Int], a)] -> Trie a
T.fromList [ (SimpC a -> [Int]
cBinds SimpC a
c, SubcId
i) | (SubcId
i, SimpC a
c) <- [(SubcId, SimpC a)]
ics ]
  where
    cBinds :: SimpC a -> [Int]
cBinds   = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
L.sort ([Int] -> [Int]) -> (SimpC a -> [Int]) -> SimpC a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> [Int]
elemsIBindEnv (IBindEnv -> [Int]) -> (SimpC a -> IBindEnv) -> SimpC a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv

----------------------------------------------------------------------------------------------
-- | Step 2: @pleTrie@ walks over the @CTrie@ to actually do the incremental-PLE
pleTrie :: Loc a => CTrie -> InstEnv a -> SmtM InstRes
pleTrie :: forall a. Loc a => CTrie -> InstEnv a -> SmtM InstRes
pleTrie CTrie
t InstEnv a
env = InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> SmtM InstRes
forall a.
Loc a =>
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> SmtM InstRes
loopT InstEnv a
env ICtx
ctx0 [Int]
forall a. [a]
diff0 Maybe Int
forall a. Maybe a
Nothing InstRes
forall {k} {v}. HashMap k v
res0 CTrie
t
  where
    diff0 :: [a]
diff0        = []
    res0 :: HashMap k v
res0         = HashMap k v
forall {k} {v}. HashMap k v
M.empty
    ctx0 :: ICtx
ctx0         = ICtx
      { icAssms :: HashSet Expr
icAssms              = HashSet Expr
forall a. Monoid a => a
mempty
      , icCands :: HashMap ExScope (HashSet Expr)
icCands              = HashMap ExScope (HashSet Expr)
forall a. Monoid a => a
mempty
      , icEquals :: HashMap ExScope EvEqualities
icEquals             = HashMap ExScope EvEqualities
forall a. Monoid a => a
mempty
      , icSimpl :: HashMap Expr Expr
icSimpl              = HashMap Expr Expr
forall a. Monoid a => a
mempty
      , icSubcId :: Maybe SubcId
icSubcId             = Maybe SubcId
forall a. Maybe a
Nothing
      , icANFs :: [[(Symbol, SortedReft)]]
icANFs               = []
      , icLRWs :: LocalRewrites
icLRWs               = LocalRewrites
forall a. Monoid a => a
mempty
      , icBindIds :: IBindEnv
icBindIds            = IBindEnv
forall a. Monoid a => a
mempty
      , icEtaBetaFlag :: Bool
icEtaBetaFlag        = Config -> Bool
etabeta        (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ InstEnv a -> Config
forall a. InstEnv a -> Config
ieCfg InstEnv a
env
      , icExtensionalityFlag :: Bool
icExtensionalityFlag = Config -> Bool
extensionality (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ InstEnv a -> Config
forall a. InstEnv a -> Config
ieCfg InstEnv a
env
      , icLocalRewritesFlag :: Bool
icLocalRewritesFlag  = Config -> Bool
localRewrites  (Config -> Bool) -> Config -> Bool
forall a b. (a -> b) -> a -> b
$ InstEnv a -> Config
forall a. InstEnv a -> Config
ieCfg InstEnv a
env
      , icFreshExistentialCounter :: Int
icFreshExistentialCounter = Int
0
      , icInitialLHSs :: HashMap ExScope (HashSet Expr)
icInitialLHSs  = HashMap ExScope (HashSet Expr)
forall a. Monoid a => a
mempty
      }

loopT
  :: Loc a
  => 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 :: forall a.
Loc a =>
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> SmtM InstRes
loopT InstEnv a
env ICtx
ictx [Int]
delta Maybe Int
i InstRes
res CTrie
t = case CTrie
t of
  T.Node []  -> InstRes -> SmtM InstRes
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return InstRes
res
  T.Node [Branch SubcId
b] -> InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> SmtM InstRes
forall a.
Loc a =>
InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> SmtM InstRes
loopB InstEnv a
env ICtx
ictx [Int]
delta Maybe Int
i InstRes
res Branch SubcId
b
  T.Node [Branch SubcId]
bs  -> InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx -> SmtM InstRes)
-> SmtM InstRes
forall a b.
Loc a =>
InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx -> SmtM b)
-> SmtM b
withAssms InstEnv a
env ICtx
ictx [Int]
delta Maybe SubcId
forall a. Maybe a
Nothing (CTrie -> Maybe CTrie
forall a. a -> Maybe a
Just CTrie
t) ((ICtx -> SmtM InstRes) -> SmtM InstRes)
-> (ICtx -> SmtM InstRes) -> SmtM InstRes
forall a b. (a -> b) -> a -> b
$ \ICtx
ictx' -> do
                  (ICtx
ictx'', InstEnv a
env'', InstRes
res') <- InstEnv a
-> ICtx -> Maybe Int -> InstRes -> SmtM (ICtx, InstEnv a, InstRes)
forall a.
InstEnv a
-> ICtx -> Maybe Int -> InstRes -> SmtM (ICtx, InstEnv a, InstRes)
ple1 InstEnv a
env ICtx
ictx' Maybe Int
i InstRes
res
                  (InstRes -> Branch SubcId -> SmtM InstRes)
-> InstRes -> [Branch SubcId] -> SmtM InstRes
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> SmtM InstRes
forall a.
Loc a =>
InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> SmtM InstRes
loopB InstEnv a
env'' ICtx
ictx'' [] Maybe Int
i) InstRes
res' [Branch SubcId]
bs

loopB
  :: Loc a
  => 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 :: forall a.
Loc a =>
InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> SmtM InstRes
loopB InstEnv a
env ICtx
ictx [Int]
delta Maybe Int
iMb InstRes
res Branch SubcId
b = case Branch SubcId
b of
  T.Bind Int
i CTrie
t -> InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> SmtM InstRes
forall a.
Loc a =>
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> SmtM InstRes
loopT InstEnv a
env ICtx
ictx (Int
iInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
delta) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) InstRes
res CTrie
t
  T.Val SubcId
cid  -> InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx -> SmtM InstRes)
-> SmtM InstRes
forall a b.
Loc a =>
InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx -> SmtM b)
-> SmtM b
withAssms InstEnv a
env ICtx
ictx [Int]
delta (SubcId -> Maybe SubcId
forall a. a -> Maybe a
Just SubcId
cid) Maybe CTrie
forall a. Maybe a
Nothing ((ICtx -> SmtM InstRes) -> SmtM InstRes)
-> (ICtx -> SmtM InstRes) -> SmtM InstRes
forall a b. (a -> b) -> a -> b
$ \ICtx
ictx' -> do
                  IO () -> StateT Context IO ()
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
progressTick
                  (\(ICtx
_, InstEnv a
_, InstRes
r) -> InstRes
r) ((ICtx, InstEnv a, InstRes) -> InstRes)
-> StateT Context IO (ICtx, InstEnv a, InstRes) -> SmtM InstRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InstEnv a
-> ICtx
-> Maybe Int
-> InstRes
-> StateT Context IO (ICtx, InstEnv a, InstRes)
forall a.
InstEnv a
-> ICtx -> Maybe Int -> InstRes -> SmtM (ICtx, InstEnv a, InstRes)
ple1 InstEnv a
env ICtx
ictx' Maybe Int
iMb InstRes
res

collectConstraints :: CTrie -> [SubcId]
collectConstraints :: CTrie -> [SubcId]
collectConstraints = CTrie -> [SubcId]
forall {b}. Trie b -> [b]
go
  where
    go :: Trie b -> [b]
go (T.Node [Branch b]
bs) = (Branch b -> [b]) -> [Branch b] -> [b]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Branch b -> [b]
goB [Branch b]
bs
    goB :: Branch b -> [b]
goB (T.Bind Int
_ Trie b
t) = Trie b -> [b]
go Trie b
t
    goB (T.Val b
cid)  = [b
cid]

-- | 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
  :: Loc a
  => InstEnv a
  -> ICtx
  -> Diff
  -> Maybe SubcId
  -> Maybe CTrie
  -> (ICtx -> SmtM b)
  -> SmtM b
withAssms :: forall a b.
Loc a =>
InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx -> SmtM b)
-> SmtM b
withAssms InstEnv a
env ICtx
ctx [Int]
delta Maybe SubcId
cidMb Maybe CTrie
mCTrie ICtx -> SmtM b
act = do
  Context
sctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  let cfg :: Config
cfg = Context -> Config
SMT.config Context
sctx
  let (ICtx
ictx', ExScope
bs) = Config
-> InstEnv a
-> Context
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx, ExScope)
forall a.
Loc a =>
Config
-> InstEnv a
-> Context
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx, ExScope)
updCtx Config
cfg InstEnv a
env Context
sctx ICtx
ctx [Int]
delta Maybe SubcId
cidMb Maybe CTrie
mCTrie
  let assms :: HashSet Expr
assms = ICtx -> HashSet Expr
icAssms ICtx
ictx'

  [Char] -> SmtM b -> SmtM b
forall a. [Char] -> SmtM a -> SmtM a
SMT.smtBracket [Char]
"PLE.withAssms" (SmtM b -> SmtM b) -> SmtM b -> SmtM b
forall a b. (a -> b) -> a -> b
$ do
    -- See Note [Existential quantification when unfolding]
    ExScope -> StateT Context IO ()
SMT.smtDecls (ExScope -> StateT Context IO ())
-> ExScope -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ EvalEnv -> ExScope -> ExScope
forall {a}. Elaborate a => EvalEnv -> a -> a
elabBindings (InstEnv a -> EvalEnv
forall a. InstEnv a -> EvalEnv
ieEvEnv InstEnv a
env) ExScope
bs
    [Expr] -> (Expr -> StateT Context IO ()) -> StateT Context IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList HashSet Expr
assms) HasCallStack => Expr -> StateT Context IO ()
Expr -> StateT Context IO ()
SMT.smtAssertDecl
    ICtx -> SmtM b
act (ICtx -> SmtM b) -> ICtx -> SmtM b
forall a b. (a -> b) -> a -> b
$ ICtx
ictx' { icAssms = mempty }

  where
    elabBindings :: EvalEnv -> a -> a
elabBindings EvalEnv
eenv a
bs =
      ElabParam -> a -> a
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (EvalEnv -> ElabFlags
evElabF EvalEnv
eenv) Located [Char]
"withAssms: PExist Args" (EvalEnv -> SymEnv
evEnv EvalEnv
eenv)) a
bs

-- | @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 :: forall a.
InstEnv a
-> ICtx -> Maybe Int -> InstRes -> SmtM (ICtx, InstEnv a, InstRes)
ple1 ie :: InstEnv a
ie@InstEnv{Maybe Solution
CMap (SimpC a)
Config
BindEnv a
LocalRewritesEnv
AxiomEnv
Knowledge
EvalEnv
ieCfg :: forall a. InstEnv a -> Config
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieKnowl :: forall a. InstEnv a -> Knowledge
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieLRWs :: forall a. InstEnv a -> LocalRewritesEnv
ieSol :: forall a. InstEnv a -> Maybe Solution
ieCfg :: Config
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: CMap (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
ieLRWs :: LocalRewritesEnv
ieSol :: Maybe Solution
..} ICtx
ictx Maybe Int
i InstRes
res = do
  Context
ctx <- StateT Context IO Context
forall s (m :: * -> *). MonadState s m => m s
get
  (ICtx
ictx', EvalEnv
env) <- IO (ICtx, EvalEnv) -> StateT Context IO (ICtx, EvalEnv)
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ICtx, EvalEnv) -> StateT Context IO (ICtx, EvalEnv))
-> IO (ICtx, EvalEnv) -> StateT Context IO (ICtx, EvalEnv)
forall a b. (a -> b) -> a -> b
$ StateT EvalEnv IO ICtx -> EvalEnv -> IO (ICtx, EvalEnv)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Config -> ICtx -> Knowledge -> StateT EvalEnv IO ICtx
evalCandsLoop Config
ieCfg ICtx
ictx Knowledge
ieKnowl) (EvalEnv
ieEvEnv { evKCtx = ctx })
  Context -> StateT Context IO ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Context -> StateT Context IO ())
-> Context -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ EvalEnv -> Context
evKCtx EvalEnv
env
  let pendings :: HashMap ExScope EvEqualities
pendings = EvalEnv -> Maybe SubcId -> HashMap ExScope EvEqualities
forall {a}. EvalEnv -> Maybe a -> HashMap ExScope EvEqualities
collectPendingUnfoldings EvalEnv
env (ICtx -> Maybe SubcId
icSubcId ICtx
ictx)
      newEqs :: [Expr]
newEqs =
        HashMap ExScope (HashSet Expr) -> [Expr]
reconstructExistentials
          ((HashSet Expr -> HashSet Expr -> HashSet Expr)
-> HashMap ExScope (HashSet Expr)
-> HashMap ExScope (HashSet Expr)
-> HashMap ExScope (HashSet Expr)
forall k v1 v2 v3.
Eq k =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
M.intersectionWith HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (ICtx -> HashMap ExScope (HashSet Expr)
icInitialLHSs ICtx
ictx) (HashMap ExScope (HashSet Expr) -> HashMap ExScope (HashSet Expr))
-> HashMap ExScope (HashSet Expr) -> HashMap ExScope (HashSet Expr)
forall a b. (a -> b) -> a -> b
$         -- add original predicates
           (EvEqualities -> HashSet Expr)
-> HashMap ExScope EvEqualities -> HashMap ExScope (HashSet Expr)
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (((Expr, Expr) -> Expr) -> EvEqualities -> HashSet Expr
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
S.map (Expr, Expr) -> Expr
equalitiesPred) (HashMap ExScope EvEqualities -> HashMap ExScope (HashSet Expr))
-> HashMap ExScope EvEqualities -> HashMap ExScope (HashSet Expr)
forall a b. (a -> b) -> a -> b
$                            -- construct equalities
           (EvEqualities -> EvEqualities -> EvEqualities)
-> HashMap ExScope EvEqualities
-> HashMap ExScope EvEqualities
-> HashMap ExScope EvEqualities
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith EvEqualities -> EvEqualities -> EvEqualities
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashMap ExScope EvEqualities
pendings (HashMap ExScope EvEqualities -> HashMap ExScope EvEqualities)
-> HashMap ExScope EvEqualities -> HashMap ExScope EvEqualities
forall a b. (a -> b) -> a -> b
$                            -- pending unfoldings if any
           (EvEqualities -> EvEqualities -> EvEqualities)
-> HashMap ExScope EvEqualities
-> HashMap ExScope EvEqualities
-> HashMap ExScope EvEqualities
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith EvEqualities -> EvEqualities -> EvEqualities
forall a. Hashable a => HashSet a -> HashSet a -> HashSet a
S.difference (ICtx -> HashMap ExScope EvEqualities
icEquals ICtx
ictx') (ICtx -> HashMap ExScope EvEqualities
icEquals ICtx
ictx) -- new equalities only
          )
  (ICtx, InstEnv a, InstRes) -> SmtM (ICtx, InstEnv a, InstRes)
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ICtx
ictx', InstEnv a
ie { ieEvEnv = env }, InstRes -> Maybe Int -> [Expr] -> InstRes
updCtxRes InstRes
res Maybe Int
i [Expr]
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 :: EvalEnv -> Maybe a -> HashMap ExScope EvEqualities
collectPendingUnfoldings EvalEnv
env (Just a
_) | Config -> Bool
pleUndecGuards Config
ieCfg =
      (HashMap Expr Expr -> EvEqualities)
-> HashMap ExScope (HashMap Expr Expr)
-> HashMap ExScope EvEqualities
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map ([(Expr, Expr)] -> EvEqualities
forall a. Hashable a => [a] -> HashSet a
S.fromList ([(Expr, Expr)] -> EvEqualities)
-> (HashMap Expr Expr -> [(Expr, Expr)])
-> HashMap Expr Expr
-> EvEqualities
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap Expr Expr -> [(Expr, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList) (EvalEnv -> HashMap ExScope (HashMap Expr Expr)
evPendingUnfoldings EvalEnv
env)
    collectPendingUnfoldings EvalEnv
_ Maybe a
_ = HashMap ExScope EvEqualities
forall a. Monoid a => a
mempty

evalToSMT :: String -> Config -> SMT.Context -> [(Symbol, Sort)] -> (Expr, Expr) -> Pred
evalToSMT :: [Char] -> Config -> Context -> ExScope -> (Expr, Expr) -> Expr
evalToSMT [Char]
msg Config
cfg Context
ctx ExScope
bs (Expr
e1,Expr
e2) = HasCallStack =>
[Char] -> Config -> Context -> ExScope -> Expr -> Expr
[Char] -> Config -> Context -> ExScope -> Expr -> Expr
toSMT ([Char]
"evalToSMT:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) Config
cfg Context
ctx ExScope
bs (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EEq Expr
e1 Expr
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 :: Config -> ICtx -> Knowledge -> StateT EvalEnv IO ICtx
evalCandsLoop Config
cfg ICtx
ictx0 Knowledge
γ = ICtx -> Int -> StateT EvalEnv IO ICtx
go ICtx
ictx0 Int
0
  where
    go :: ICtx -> Int -> EvalST ICtx
    go :: ICtx -> Int -> StateT EvalEnv IO ICtx
go ICtx
ictx Int
_ | (HashSet Expr -> Bool) -> HashMap ExScope (HashSet Expr) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all HashSet Expr -> Bool
forall a. HashSet a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ICtx -> HashMap ExScope (HashSet Expr)
icCands ICtx
ictx) = ICtx -> StateT EvalEnv IO ICtx
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
    go ICtx
ictx Int
i = do
      Bool
inconsistentEnv <- EvalST Bool
testForInconsistentEnvironment
      if Bool
inconsistentEnv
        then ICtx -> StateT EvalEnv IO ICtx
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
        else do StateT Context IO () -> EvalST ()
forall a. SmtM a -> EvalST a
liftSMT (StateT Context IO () -> EvalST ())
-> StateT Context IO () -> EvalST ()
forall a b. (a -> b) -> a -> b
$ HasCallStack => Expr -> StateT Context IO ()
Expr -> StateT Context IO ()
SMT.smtAssertDecl (Expr -> StateT Context IO ()) -> Expr -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pAndNoDedup ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList (HashSet Expr -> [Expr]) -> HashSet Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ ICtx -> HashSet Expr
icAssms ICtx
ictx
                let ictx' :: ICtx
ictx' = ICtx
ictx { icAssms = mempty }
                    ([ExScope]
scopes, [HashSet Expr]
candSets) = [(ExScope, HashSet Expr)] -> ([ExScope], [HashSet Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(ExScope, HashSet Expr)] -> ([ExScope], [HashSet Expr]))
-> [(ExScope, HashSet Expr)] -> ([ExScope], [HashSet Expr])
forall a b. (a -> b) -> a -> b
$ HashMap ExScope (HashSet Expr) -> [(ExScope, HashSet Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap ExScope (HashSet Expr) -> [(ExScope, HashSet Expr)])
-> HashMap ExScope (HashSet Expr) -> [(ExScope, HashSet Expr)]
forall a b. (a -> b) -> a -> b
$ ICtx -> HashMap ExScope (HashSet Expr)
icCands ICtx
ictx
                    cands :: [[Expr]]
cands = (HashSet Expr -> [Expr]) -> [HashSet Expr] -> [[Expr]]
forall a b. (a -> b) -> [a] -> [b]
map HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList [HashSet Expr]
candSets
                ([[[Expr]]]
candss, [EvEqualities]
uss) <- [([[Expr]], EvEqualities)] -> ([[[Expr]]], [EvEqualities])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([[Expr]], EvEqualities)] -> ([[[Expr]]], [EvEqualities]))
-> StateT EvalEnv IO [([[Expr]], EvEqualities)]
-> StateT EvalEnv IO ([[[Expr]]], [EvEqualities])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ExScope -> [Expr] -> StateT EvalEnv IO ([[Expr]], EvEqualities))
-> [ExScope]
-> [[Expr]]
-> StateT EvalEnv IO [([[Expr]], EvEqualities)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (ICtx
-> Int
-> ExScope
-> [Expr]
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
evalCand ICtx
ictx' Int
i) [ExScope]
scopes [[Expr]]
cands
                let noCandidateChanged :: Bool
noCandidateChanged = ([Bool] -> Bool) -> [[Bool]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([[Bool]] -> Bool) -> [[Bool]] -> Bool
forall a b. (a -> b) -> a -> b
$ ([[Expr]] -> [Expr] -> [Bool])
-> [[[Expr]]] -> [[Expr]] -> [[Bool]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (([Expr] -> Expr -> Bool) -> [[Expr]] -> [Expr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Expr] -> Expr -> Bool
forall {a}. Eq a => [a] -> a -> Bool
eqCand) [[[Expr]]]
candss [[Expr]]
cands
                    unknownEqs :: HashMap ExScope EvEqualities
unknownEqs = (EvEqualities -> EvEqualities -> EvEqualities)
-> HashMap ExScope EvEqualities
-> HashMap ExScope EvEqualities
-> HashMap ExScope EvEqualities
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith EvEqualities -> EvEqualities -> EvEqualities
forall a. Hashable a => HashSet a -> HashSet a -> HashSet a
S.difference ([(ExScope, EvEqualities)] -> HashMap ExScope EvEqualities
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([ExScope] -> [EvEqualities] -> [(ExScope, EvEqualities)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ExScope]
scopes [EvEqualities]
uss)) (ICtx -> HashMap ExScope EvEqualities
icEquals ICtx
ictx)
                if (EvEqualities -> Bool) -> HashMap ExScope EvEqualities -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all EvEqualities -> Bool
forall a. HashSet a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null HashMap ExScope EvEqualities
unknownEqs Bool -> Bool -> Bool
&& Bool
noCandidateChanged then
                  ICtx -> StateT EvalEnv IO ICtx
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
                else do
                  Context
ctx' <- (EvalEnv -> Context) -> StateT EvalEnv IO Context
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> Context
evKCtx
                  let eqsSMT :: HashSet Expr
eqsSMT =
                        [HashSet Expr] -> HashSet Expr
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet Expr] -> HashSet Expr) -> [HashSet Expr] -> HashSet Expr
forall a b. (a -> b) -> a -> b
$ HashMap ExScope (HashSet Expr) -> [HashSet Expr]
forall k v. HashMap k v -> [v]
M.elems (HashMap ExScope (HashSet Expr) -> [HashSet Expr])
-> HashMap ExScope (HashSet Expr) -> [HashSet Expr]
forall a b. (a -> b) -> a -> b
$
                          (ExScope -> EvEqualities -> HashSet Expr)
-> HashMap ExScope EvEqualities -> HashMap ExScope (HashSet Expr)
forall k v1 v2. (k -> v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.mapWithKey
                            (\ExScope
scope -> ((Expr, Expr) -> Expr) -> EvEqualities -> HashSet Expr
forall b a. Hashable b => (a -> b) -> HashSet a -> HashSet b
S.map (((Expr, Expr) -> Expr) -> EvEqualities -> HashSet Expr)
-> ((Expr, Expr) -> Expr) -> EvEqualities -> HashSet Expr
forall a b. (a -> b) -> a -> b
$ [Char] -> Config -> Context -> ExScope -> (Expr, Expr) -> Expr
evalToSMT [Char]
"evalCandsLoop" Config
cfg Context
ctx' ExScope
scope)
                            HashMap ExScope EvEqualities
unknownEqs
                      ictx'' :: ICtx
ictx'' = ICtx
ictx
                        { icEquals = M.unionWith S.union (icEquals ictx) unknownEqs
                        , icAssms  = S.filter (not . isTautoPred) eqsSMT
                        }
                  ICtx -> Int -> StateT EvalEnv IO ICtx
go (ICtx
ictx'' { icCands = M.fromList $ zip scopes (map (S.fromList . concat) candss) }) (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

    testForInconsistentEnvironment :: EvalST Bool
    testForInconsistentEnvironment :: EvalST Bool
testForInconsistentEnvironment =
      Knowledge -> Expr -> EvalST Bool
knPredsEvalST Knowledge
γ Expr
forall v. ExprV v
PFalse

    eqCand :: [a] -> a -> Bool
eqCand [a
e0] a
e1 = a
e0 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
e1
    eqCand [a]
_ a
_ = Bool
False

    evalCand :: ICtx -> Int -> ExScope -> [Expr] -> EvalST ([[Expr]], S.HashSet (Expr, Expr))
    evalCand :: ICtx
-> Int
-> ExScope
-> [Expr]
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
evalCand ICtx
ictx Int
i ExScope
scope [Expr]
es = ExScope
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
forall a. ExScope -> EvalST a -> EvalST a
withExScope ExScope
scope (StateT EvalEnv IO ([[Expr]], EvEqualities)
 -> StateT EvalEnv IO ([[Expr]], EvEqualities))
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
forall a b. (a -> b) -> a -> b
$ (Expr -> StateT EvalEnv IO [Expr])
-> [Expr] -> StateT EvalEnv IO [[Expr]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Knowledge -> ICtx -> Int -> Expr -> StateT EvalEnv IO [Expr]
evalOne Knowledge
γ ICtx
ictx Int
i) [Expr]
es StateT EvalEnv IO [[Expr]]
-> ([[Expr]] -> StateT EvalEnv IO ([[Expr]], EvEqualities))
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
forall a b.
StateT EvalEnv IO a
-> (a -> StateT EvalEnv IO b) -> StateT EvalEnv IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [[Expr]] -> StateT EvalEnv IO ([[Expr]], EvEqualities)
collectEqs

    collectEqs :: [[Expr]] -> EvalST ([[Expr]], S.HashSet (Expr, Expr))
    collectEqs :: [[Expr]] -> StateT EvalEnv IO ([[Expr]], EvEqualities)
collectEqs [[Expr]]
es = do
      EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
      let newEqs :: EvEqualities
newEqs = EvalEnv -> EvEqualities
evNewEqualities EvalEnv
env
      (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { evNewEqualities = mempty }
      ([[Expr]], EvEqualities)
-> StateT EvalEnv IO ([[Expr]], EvEqualities)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Expr]]
es, EvEqualities
newEqs)

    withExScope :: ExScope -> EvalST a -> EvalST a
    withExScope :: forall a. ExScope -> EvalST a -> EvalST a
withExScope ExScope
s EvalST a
m = do
      EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
      EvalEnv -> EvalST ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalEnv -> EvalST ()) -> EvalEnv -> EvalST ()
forall a b. (a -> b) -> a -> b
$ EvalEnv
env { evExScope = s }
      a
r <- EvalST a
m
      (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { evExScope = evExScope env }
      a -> EvalST a
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r


----------------------------------------------------------------------------------------------
-- | Step 3: @resSInfo@ uses incremental PLE result @InstRes@ to produce the strengthened SInfo
----------------------------------------------------------------------------------------------

resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> BindEnv a
resSInfo :: forall a. Config -> SymEnv -> SInfo a -> InstRes -> BindEnv a
resSInfo Config
cfg SymEnv
env SInfo a
info InstRes
res = SInfo a -> InstRes -> BindEnv a
forall a. SInfo a -> InstRes -> BindEnv a
strengthenBinds SInfo a
info InstRes
res'
  where
    res' :: InstRes
res'     = [(Int, Expr)] -> InstRes
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([(Int, Expr)] -> InstRes) -> [(Int, Expr)] -> InstRes
forall a b. (a -> b) -> a -> b
$ [Int] -> [Expr] -> [(Int, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
is [Expr]
ps''
    ps'' :: [Expr]
ps''     = (Int -> Expr -> Expr) -> [Int] -> [Expr] -> [Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i -> ElabParam -> Expr -> Expr
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (Config -> ElabFlags
solverFlags Config
cfg) (SrcSpan -> [Char] -> Located [Char]
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan ([Char]
"PLE1 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) SymEnv
env)) [Int]
is [Expr]
ps'
    ps' :: [Expr]
ps'      = Config -> SymEnv -> [Expr] -> [Expr]
forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env [Expr]
ps
    ([Int]
is, [Expr]
ps) = [(Int, Expr)] -> ([Int], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip (InstRes -> [(Int, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList InstRes
res)

----------------------------------------------------------------------------------------------
-- | @InstEnv@ has the global information needed to do PLE
----------------------------------------------------------------------------------------------

data InstEnv a = InstEnv
  { forall a. InstEnv a -> Config
ieCfg   :: !Config
  , forall a. InstEnv a -> BindEnv a
ieBEnv  :: !(BindEnv a)
  , forall a. InstEnv a -> AxiomEnv
ieAenv  :: !AxiomEnv
  , forall a. InstEnv a -> CMap (SimpC a)
ieCstrs :: !(CMap (SimpC a))
  , forall a. InstEnv a -> Knowledge
ieKnowl :: !Knowledge
  , forall a. InstEnv a -> EvalEnv
ieEvEnv :: !EvalEnv
  , forall a. InstEnv a -> LocalRewritesEnv
ieLRWs  :: LocalRewritesEnv
  , forall a. InstEnv a -> Maybe Solution
ieSol :: Maybe Solution
  }

----------------------------------------------------------------------------------------------
-- | @ICtx@ is the local information -- at each trie node -- obtained by incremental PLE
----------------------------------------------------------------------------------------------

data ICtx    = ICtx
  { ICtx -> HashSet Expr
icAssms              :: S.HashSet Pred           -- ^ Equalities converted to SMT format
  , ICtx -> HashMap ExScope (HashSet Expr)
icCands              :: M.HashMap ExScope (S.HashSet Expr)  -- ^ "Candidates" for unfolding
  , ICtx -> HashMap ExScope EvEqualities
icEquals             :: M.HashMap ExScope EvEqualities      -- ^ Accumulated equalities
  , ICtx -> HashMap Expr Expr
icSimpl              :: !ConstMap                -- ^ Map of expressions to constants
  , ICtx -> Maybe SubcId
icSubcId             :: Maybe SubcId             -- ^ Current subconstraint ID
  , ICtx -> [[(Symbol, SortedReft)]]
icANFs               :: [[(Symbol, SortedReft)]] -- Hopefully contain only ANF things
  , ICtx -> LocalRewrites
icLRWs               :: LocalRewrites            -- ^ Local rewrites
  , ICtx -> IBindEnv
icBindIds            :: IBindEnv                 -- ^ Bind Ids in the current context
  , ICtx -> Bool
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].
  , ICtx -> Bool
icExtensionalityFlag :: Bool                     -- ^ True if the extensionality flag is turned on
  , ICtx -> Bool
icLocalRewritesFlag  :: Bool                     -- ^ True if the local rewrites flag is turned on
  , ICtx -> Int
icFreshExistentialCounter :: Int                 -- ^ Counter to generate fresh names for existentials
  , ICtx -> HashMap ExScope (HashSet Expr)
icInitialLHSs :: M.HashMap ExScope (S.HashSet Expr)
                                                     -- ^ LHS candidates before any unfoldings
  }

----------------------------------------------------------------------------------------------
-- | @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 :: (Expr, Expr) -> Expr
equalitiesPred (Expr
e1, Expr
e2)
  | Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2 = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EEq Expr
e1 Expr
e2
  | Bool
otherwise = Expr
forall v. ExprV v
PTrue

updCtxRes :: InstRes -> Maybe BindId -> [Expr] -> InstRes
updCtxRes :: InstRes -> Maybe Int -> [Expr] -> InstRes
updCtxRes InstRes
res Maybe Int
iMb = InstRes -> Maybe Int -> Expr -> InstRes
updRes InstRes
res Maybe Int
iMb (Expr -> InstRes) -> ([Expr] -> Expr) -> [Expr] -> InstRes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
pAndNoDedup


updRes :: InstRes -> Maybe BindId -> Expr -> InstRes
updRes :: InstRes -> Maybe Int -> Expr -> InstRes
updRes InstRes
res (Just Int
i) Expr
e = (Expr -> Expr -> Expr) -> Int -> Expr -> InstRes -> InstRes
forall k v.
Hashable k =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith ([Char] -> Expr -> Expr -> Expr
forall a. HasCallStack => [Char] -> a
error [Char]
"tree-like invariant broken in ple. See https://github.com/ucsd-progsys/liquid-fixpoint/issues/496") Int
i Expr
e InstRes
res
updRes InstRes
res  Maybe Int
Nothing Expr
_ = InstRes
res

----------------------------------------------------------------------------------------------
-- | @updCtx env ctx delta cidMb@ adds the assumptions and candidates from @delta@ and @cidMb@
--   to the context.
--
-- Yields the new context and a list of existential binders found in @delta@.
-- See Note [Existential quantification when unfolding].
----------------------------------------------------------------------------------------------

updCtx
  :: Loc a
  => Config
  -> InstEnv a
  -> SMT.Context
  -> ICtx
  -> Diff
  -> Maybe SubcId
  -> Maybe CTrie
  -> (ICtx, [(Symbol, Sort)])
updCtx :: forall a.
Loc a =>
Config
-> InstEnv a
-> Context
-> ICtx
-> [Int]
-> Maybe SubcId
-> Maybe CTrie
-> (ICtx, ExScope)
updCtx Config
cfg InstEnv{Maybe Solution
CMap (SimpC a)
Config
BindEnv a
LocalRewritesEnv
AxiomEnv
Knowledge
EvalEnv
ieCfg :: forall a. InstEnv a -> Config
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieKnowl :: forall a. InstEnv a -> Knowledge
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieLRWs :: forall a. InstEnv a -> LocalRewritesEnv
ieSol :: forall a. InstEnv a -> Maybe Solution
ieCfg :: Config
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: CMap (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
ieLRWs :: LocalRewritesEnv
ieSol :: Maybe Solution
..} Context
ieSMT ICtx
ictx [Int]
delta Maybe SubcId
cidMb Maybe CTrie
mCTrie =
    ( ICtx
ictx { icAssms  = S.fromList ctxEqs
           , icCands  = M.unionWith S.union candsPerExScope (icCands ictx)
           , icSimpl  = icSimpl ictx <> econsts
           , icSubcId = cidMb
           , icANFs   = anfBinds
           , icLRWs   = mconcat $ icLRWs ictx : newLRWs
           , icBindIds = ibinds
           , icFreshExistentialCounter = existentialCounter
           , icInitialLHSs = M.unionWith S.union candsPerExScopeNoRHS (icInitialLHSs ictx)
           }
    , ExScope
ebs
    )
  where
    ebs :: ExScope
ebs = [ExScope] -> ExScope
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (HashMap ExScope (HashSet Expr) -> [ExScope]
forall k v. HashMap k v -> [k]
M.keys HashMap ExScope (HashSet Expr)
candsPerExScope)
    ibinds :: IBindEnv
ibinds = [Int] -> IBindEnv -> IBindEnv
insertsIBindEnv [Int]
delta (ICtx -> IBindEnv
icBindIds ICtx
ictx)
    cands :: [Expr]
cands     = Expr
rhsExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
es
    anfBinds :: [[(Symbol, SortedReft)]]
anfBinds  = [(Symbol, SortedReft)]
bs [(Symbol, SortedReft)]
-> [[(Symbol, SortedReft)]] -> [[(Symbol, SortedReft)]]
forall a. a -> [a] -> [a]
: ICtx -> [[(Symbol, SortedReft)]]
icANFs ICtx
ictx
    econsts :: HashMap Expr Expr
econsts   = [(Expr, Expr)] -> HashMap Expr Expr
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ([(Expr, Expr)] -> HashMap Expr Expr)
-> [(Expr, Expr)] -> HashMap Expr Expr
forall a b. (a -> b) -> a -> b
$ Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants Knowledge
ieKnowl [Expr]
es
    ctxEqs :: [Expr]
ctxEqs    = HasCallStack =>
[Char] -> Config -> Context -> ExScope -> Expr -> Expr
[Char] -> Config -> Context -> ExScope -> Expr -> Expr
toSMT [Char]
"updCtx" Config
ieCfg Context
ieSMT ExScope
ebs (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a]
L.nub
                  [ Expr
c
                  | (ExScope
_, HashSet Expr
s) <- Int -> [(ExScope, HashSet Expr)] -> [(ExScope, HashSet Expr)]
forall a. Int -> [a] -> [a]
drop Int
1 [(ExScope, HashSet Expr)]
deANFedCands
                  , Expr
e <- HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList HashSet Expr
s
                  , Expr
c <- Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts Expr
e
                  , Bool -> Bool
not (Expr -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred Expr
c)
                  ]
    bs :: [(Symbol, SortedReft)]
bs        = (SortedReft -> SortedReft)
-> (Symbol, SortedReft) -> (Symbol, SortedReft)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SortedReft -> SortedReft
unApplySortedReft ((Symbol, SortedReft) -> (Symbol, SortedReft))
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds
    rhs :: Expr
rhs       = Expr -> Expr
unApply Expr
eRhs
    es :: [Expr]
es        = (Symbol, SortedReft) -> Expr
forall a. Expression a => a -> Expr
expr ((Symbol, SortedReft) -> Expr) -> [(Symbol, SortedReft)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
bs
    eRhs :: Expr
eRhs      = Expr -> (SimpC a -> Expr) -> Maybe (SimpC a) -> Expr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
forall v. ExprV v
PTrue SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs Maybe (SimpC a)
subMb

    ([(Symbol, SortedReft)]
binds, Int
existentialCounter) = [(Symbol, SortedReft)] -> Int -> ([(Symbol, SortedReft)], Int)
renameExistentialsInSortedRefts [(Symbol, SortedReft)]
binds0 (ICtx -> Int
icFreshExistentialCounter ICtx
ictx)

    binds0 :: [(Symbol, SortedReft)]
binds0    = [ (Symbol, SortedReft) -> (Symbol, SortedReft)
maybeApplyKVarSolutions (Symbol
x, SortedReft
y)
                | Int
i <- [Int]
delta
                , let (Symbol
x, SortedReft
y, a
_) = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv a
ieBEnv
                ]
    subMb :: Maybe (SimpC a)
subMb     = CMap (SimpC a) -> SubcId -> SimpC a
forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr CMap (SimpC a)
ieCstrs (SubcId -> SimpC a) -> Maybe SubcId -> Maybe (SimpC a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SubcId
cidMb
    newLRWs :: [LocalRewrites]
newLRWs   = (Int -> Maybe LocalRewrites) -> [Int] -> [LocalRewrites]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Int -> LocalRewritesEnv -> Maybe LocalRewrites
`lookupLocalRewrites` LocalRewritesEnv
ieLRWs) [Int]
delta

    candsPerExScopeNoRHS :: HashMap ExScope (HashSet Expr)
candsPerExScopeNoRHS = (HashSet Expr -> HashSet Expr -> HashSet Expr)
-> [(ExScope, HashSet Expr)] -> HashMap ExScope (HashSet Expr)
forall k v. Hashable k => (v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union ([(ExScope, HashSet Expr)] -> HashMap ExScope (HashSet Expr))
-> [(ExScope, HashSet Expr)] -> HashMap ExScope (HashSet Expr)
forall a b. (a -> b) -> a -> b
$ ([], HashSet Expr
forall a. HashSet a
S.empty) (ExScope, HashSet Expr)
-> [(ExScope, HashSet Expr)] -> [(ExScope, HashSet Expr)]
forall a. a -> [a] -> [a]
: Int -> [(ExScope, HashSet Expr)] -> [(ExScope, HashSet Expr)]
forall a. Int -> [a] -> [a]
drop Int
1 [(ExScope, HashSet Expr)]
deANFedCands
    -- ebs expects all keys to contain disjoint sets of bindings
    candsPerExScope :: HashMap ExScope (HashSet Expr)
candsPerExScope = (HashSet Expr -> HashSet Expr -> HashSet Expr)
-> HashMap ExScope (HashSet Expr)
-> HashMap ExScope (HashSet Expr)
-> HashMap ExScope (HashSet Expr)
forall k v.
Eq k =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashMap ExScope (HashSet Expr)
candsPerExScopeNoRHS (HashMap ExScope (HashSet Expr) -> HashMap ExScope (HashSet Expr))
-> HashMap ExScope (HashSet Expr) -> HashMap ExScope (HashSet Expr)
forall a b. (a -> b) -> a -> b
$ (HashSet Expr -> HashSet Expr -> HashSet Expr)
-> [(ExScope, HashSet Expr)] -> HashMap ExScope (HashSet Expr)
forall k v. Hashable k => (v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union (Int -> [(ExScope, HashSet Expr)] -> [(ExScope, HashSet Expr)]
forall a. Int -> [a] -> [a]
take Int
1 [(ExScope, HashSet Expr)]
deANFedCands)

    deANFedCands :: [(ExScope, HashSet Expr)]
deANFedCands = (Expr -> (ExScope, HashSet Expr))
-> [Expr] -> [(ExScope, HashSet Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> HashSet Expr)
-> (ExScope, Expr) -> (ExScope, HashSet Expr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Expr -> HashSet Expr
forall a. Hashable a => a -> HashSet a
S.singleton ((ExScope, Expr) -> (ExScope, HashSet Expr))
-> (Expr -> (ExScope, Expr)) -> Expr -> (ExScope, HashSet Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> (ExScope, Expr)
prenexExistentials) ([Expr] -> [(ExScope, HashSet Expr)])
-> [Expr] -> [(ExScope, HashSet Expr)]
forall a b. (a -> b) -> a -> b
$
      -- We only call 'deANF' if necessary.
      if Bool -> Bool
not ([AutoRewrite] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Knowledge -> Maybe SubcId -> [AutoRewrite]
getAutoRws Knowledge
ieKnowl Maybe SubcId
cidMb))
         Bool -> Bool -> Bool
|| ICtx -> Bool
icExtensionalityFlag ICtx
ictx
         Bool -> Bool -> Bool
|| ICtx -> Bool
icEtaBetaFlag ICtx
ictx then
        [[(Symbol, SortedReft)]] -> [Expr] -> [Expr]
deANF [[(Symbol, SortedReft)]]
anfBinds [Expr]
cands
      else
        [Expr]
cands

    maybeApplyKVarSolutions :: (Symbol, SortedReft) -> (Symbol, SortedReft)
maybeApplyKVarSolutions (Symbol, SortedReft)
xsr =
      case Maybe Solution
ieSol of
        Just Solution
sol -> Config
-> CombinedEnv a
-> Solution
-> (Symbol, SortedReft)
-> (Symbol, SortedReft)
forall ann.
Config
-> CombinedEnv ann
-> Solution
-> (Symbol, SortedReft)
-> (Symbol, SortedReft)
applyInSortedReft Config
cfg CombinedEnv a
g Solution
sol (Symbol, SortedReft)
xsr
        Maybe Solution
Nothing  -> (Symbol, SortedReft)
xsr
      where
        gCid :: Maybe SubcId
gCid = case CTrie -> [SubcId]
collectConstraints (CTrie -> [SubcId]) -> Maybe CTrie -> Maybe [SubcId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CTrie
mCTrie of
          Just (SubcId
c:[SubcId]
_) -> SubcId -> Maybe SubcId
forall a. a -> Maybe a
Just SubcId
c
          Maybe [SubcId]
_ -> Maybe SubcId
forall a. Maybe a
Nothing
        g :: CombinedEnv a
g = CEnv
          { ceCid :: Maybe SubcId
ceCid = Maybe SubcId
gCid
          , ceBEnv :: BindEnv a
ceBEnv = BindEnv a
ieBEnv
          , ceIEnv :: IBindEnv
ceIEnv = IBindEnv
ibinds
          , ceSpan :: SrcSpan
ceSpan = SrcSpan -> (SimpC a -> SrcSpan) -> Maybe (SimpC a) -> SrcSpan
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SrcSpan
dummySpan SimpC a -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan (Maybe (SimpC a) -> SrcSpan) -> Maybe (SimpC a) -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Maybe SubcId
gCid Maybe SubcId -> (SubcId -> Maybe (SimpC a)) -> Maybe (SimpC a)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SubcId -> CMap (SimpC a) -> Maybe (SimpC a)
forall k v. Hashable k => k -> HashMap k v -> Maybe v
`M.lookup` CMap (SimpC a)
ieCstrs)
          , ceBindingsInSmt :: IBindEnv
ceBindingsInSmt = IBindEnv
emptyIBindEnv
          }


findConstants :: Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants :: Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants Knowledge
γ [Expr]
es = [(Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
x, Expr
c) | (Symbol
x,Expr
c) <- [(Symbol, Expr)] -> [Expr] -> [(Symbol, Expr)]
go [] ((Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
splitPAnd [Expr]
es)]
  where
    go :: [(Symbol, Expr)] -> [Expr] -> [(Symbol, Expr)]
go [(Symbol, Expr)]
su [Expr]
ess = if [Expr]
ess [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr]
ess'
                  then [(Symbol, Expr)]
su
                  else [(Symbol, Expr)] -> [Expr] -> [(Symbol, Expr)]
go ([(Symbol, Expr)]
su [(Symbol, Expr)] -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Expr)]
su') [Expr]
ess'
       where ess' :: [Expr]
ess' = Subst -> Expr -> Expr
forall a. (Subable a, HasCallStack) => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol, Expr)]
su') (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
ess
             su' :: [(Symbol, Expr)]
su'  = [Expr] -> [(Symbol, Expr)]
makeSu [Expr]
ess
    makeSu :: [Expr] -> [(Symbol, Expr)]
makeSu [Expr]
exprs  = [(Symbol
x,Expr
c) | (EEq (EVar Symbol
x) Expr
c) <- [Expr]
exprs
                           , HashSet Symbol -> Expr -> Bool
isConstant (Knowledge -> HashSet Symbol
knDCs Knowledge
γ) Expr
c
                           , Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
c ]

getCstr :: M.HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr :: forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr HashMap SubcId (SimpC a)
env SubcId
cid = [Char] -> SubcId -> HashMap SubcId (SimpC a) -> SimpC a
forall k v.
(HasCallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
Misc.safeLookup [Char]
"Instantiate.getCstr" SubcId
cid HashMap SubcId (SimpC a)
env

isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr :: forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
subid SimpC a
c = SimpC a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c Bool -> Bool -> Bool
&& Bool -> SubcId -> HashMap SubcId Bool -> Bool
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault Bool
False SubcId
subid (AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
aenv)

type EvEqualities = S.HashSet (Expr, Expr)

--------------------------------------------------------------------------------
data EvalEnv = EvalEnv
  { EvalEnv -> SymEnv
evEnv      :: !SymEnv
  , EvalEnv -> ElabFlags
evElabF    :: ElabFlags
  , EvalEnv -> Context
evKCtx     :: SMT.Context
    -- | The current scope of existential variables.
    -- See Note [Existential quantification when unfolding].
  , EvalEnv -> ExScope
evExScope  :: ExScope
    -- | Equalities where we couldn't evaluate the guards, in a map which
    -- uses their existential scope as key.
    --
    -- See Note [Existential quantification when unfolding].
  , EvalEnv -> HashMap ExScope (HashMap Expr Expr)
evPendingUnfoldings :: M.HashMap ExScope (M.HashMap Expr Expr)
  , EvalEnv -> EvEqualities
evNewEqualities :: EvEqualities -- ^ Equalities discovered during a traversal of
                                    -- an expression
  , EvalEnv -> HashMap Expr Bool
evSMTCache :: M.HashMap Expr Bool -- ^ Whether an expression is valid or its negation
  , EvalEnv -> FuelCount
evFuel     :: FuelCount

  -- Eta expansion feature
  , EvalEnv -> Int
freshEtaNames :: Int -- ^ Keeps track of how many names we generated to perform eta
                         --   expansion, we use this to generate always fresh names
  -- REST parameters
  , EvalEnv -> Maybe (ExploredTerms RuntimeTerm OCType IO)
explored   :: Maybe (ExploredTerms RuntimeTerm OCType IO)
  , EvalEnv -> Maybe SolverHandle
restSolver :: Maybe SolverHandle
  , EvalEnv -> RESTOrdering
restOCA    :: RESTOrdering
  , EvalEnv -> OCAlgebra OCType RuntimeTerm IO
evOCAlgebra :: OCAlgebra OCType RuntimeTerm IO
  }

data FuelCount = FC
  { FuelCount -> HashMap Symbol Int
fcMap :: M.HashMap Symbol Int
  , FuelCount -> Maybe Int
fcMax :: Maybe Int
  }
  deriving (Int -> FuelCount -> [Char] -> [Char]
[FuelCount] -> [Char] -> [Char]
FuelCount -> [Char]
(Int -> FuelCount -> [Char] -> [Char])
-> (FuelCount -> [Char])
-> ([FuelCount] -> [Char] -> [Char])
-> Show FuelCount
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> FuelCount -> [Char] -> [Char]
showsPrec :: Int -> FuelCount -> [Char] -> [Char]
$cshow :: FuelCount -> [Char]
show :: FuelCount -> [Char]
$cshowList :: [FuelCount] -> [Char] -> [Char]
showList :: [FuelCount] -> [Char] -> [Char]
Show)

defFuelCount :: Config -> FuelCount
defFuelCount :: Config -> FuelCount
defFuelCount Config
cfg = HashMap Symbol Int -> Maybe Int -> FuelCount
FC HashMap Symbol Int
forall a. Monoid a => a
mempty (Config -> Maybe Int
fuel Config
cfg)

type EvalST a = StateT EvalEnv IO a

liftSMT :: SmtM a -> EvalST a
liftSMT :: forall a. SmtM a -> EvalST a
liftSMT SmtM a
k =
  do EvalEnv
es <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
     let ctx :: Context
ctx = EvalEnv -> Context
evKCtx EvalEnv
es
     (a
a, Context
ctx') <- IO (a, Context) -> StateT EvalEnv IO (a, Context)
forall (m :: * -> *) a. Monad m => m a -> StateT EvalEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (a, Context) -> StateT EvalEnv IO (a, Context))
-> IO (a, Context) -> StateT EvalEnv IO (a, Context)
forall a b. (a -> b) -> a -> b
$ SmtM a -> Context -> IO (a, Context)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT SmtM a
k Context
ctx
     EvalEnv -> EvalST ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalEnv
es {evKCtx = ctx'})
     a -> EvalST a
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

--------------------------------------------------------------------------------

getAutoRws :: Knowledge -> Maybe SubcId -> [AutoRewrite]
getAutoRws :: Knowledge -> Maybe SubcId -> [AutoRewrite]
getAutoRws Knowledge
γ Maybe SubcId
mSubcId =
  [AutoRewrite] -> Maybe [AutoRewrite] -> [AutoRewrite]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] (Maybe [AutoRewrite] -> [AutoRewrite])
-> Maybe [AutoRewrite] -> [AutoRewrite]
forall a b. (a -> b) -> a -> b
$ do
    SubcId
cid <- Maybe SubcId
mSubcId
    SubcId -> HashMap SubcId [AutoRewrite] -> Maybe [AutoRewrite]
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup SubcId
cid (HashMap SubcId [AutoRewrite] -> Maybe [AutoRewrite])
-> HashMap SubcId [AutoRewrite] -> Maybe [AutoRewrite]
forall a b. (a -> b) -> a -> b
$ Knowledge -> HashMap SubcId [AutoRewrite]
knAutoRWs Knowledge
γ

-- | 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 :: Knowledge -> ICtx -> Int -> Expr -> StateT EvalEnv IO [Expr]
evalOne Knowledge
γ ICtx
ctx Int
i Expr
e
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
|| [AutoRewrite] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Knowledge -> Maybe SubcId -> [AutoRewrite]
getAutoRws Knowledge
γ (ICtx -> Maybe SubcId
icSubcId ICtx
ctx)) = (Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[]) (Expr -> [Expr])
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ICtx
ctx EvalType
NoRW Expr
e
evalOne Knowledge
γ ICtx
ctx Int
_ Expr
e | Expr -> Bool
isExprRewritable Expr
e = do
    EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
    let oc :: OCAlgebra OCType RuntimeTerm IO
        oc :: OCAlgebra OCType RuntimeTerm IO
oc = EvalEnv -> OCAlgebra OCType RuntimeTerm IO
evOCAlgebra EvalEnv
env
        rp :: RESTParams OCType
rp = OCAlgebra OCType Expr IO
-> [(Expr, TermOrigin)] -> OCType -> RESTParams OCType
forall oc.
OCAlgebra oc Expr IO -> [(Expr, TermOrigin)] -> oc -> RESTParams oc
RP ((Expr -> RuntimeTerm)
-> OCAlgebra OCType RuntimeTerm IO -> OCAlgebra OCType Expr IO
forall c a b (m :: * -> *).
(b -> a) -> OCAlgebra c a m -> OCAlgebra c b m
contramap Expr -> RuntimeTerm
Rewrite.convert OCAlgebra OCType RuntimeTerm IO
oc) [(Expr
e, TermOrigin
PLE)] OCType
constraints
        constraints :: OCType
constraints = OCAlgebra OCType RuntimeTerm IO -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c
OC.top OCAlgebra OCType RuntimeTerm IO
oc
        emptyET :: ExploredTerms RuntimeTerm OCType IO
emptyET = ExploreFuncs RuntimeTerm OCType IO
-> ExploreStrategy -> ExploredTerms RuntimeTerm OCType IO
forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ExploredTerms.empty ((OCType -> OCType -> OCType)
-> (OCType -> OCType -> IO Bool)
-> (OCType -> RuntimeTerm -> RuntimeTerm -> OCType)
-> ExploreFuncs RuntimeTerm OCType IO
forall term c (m :: * -> *).
(c -> c -> c)
-> (c -> c -> m Bool)
-> (c -> term -> term -> c)
-> ExploreFuncs term c m
EF (OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
OC.union OCAlgebra OCType RuntimeTerm IO
oc) (OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra OCType RuntimeTerm IO
oc) (OCAlgebra OCType RuntimeTerm IO
-> OCType -> RuntimeTerm -> RuntimeTerm -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
OC.refine OCAlgebra OCType RuntimeTerm IO
oc)) ExploreStrategy
ExploreWhenNeeded
    [Expr]
es <- Knowledge -> ICtx -> RESTParams OCType -> StateT EvalEnv IO [Expr]
evalREST Knowledge
γ ICtx
ctx RESTParams OCType
rp
    (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { explored = Just emptyET }
    [Expr] -> StateT EvalEnv IO [Expr]
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
es
evalOne Knowledge
_ ICtx
_ Int
_ Expr
_ = [Expr] -> StateT EvalEnv IO [Expr]
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
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 (EvalType -> EvalType -> Bool
(EvalType -> EvalType -> Bool)
-> (EvalType -> EvalType -> Bool) -> Eq EvalType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EvalType -> EvalType -> Bool
== :: EvalType -> EvalType -> Bool
$c/= :: EvalType -> EvalType -> Bool
/= :: EvalType -> EvalType -> Bool
Eq)


-- | 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
eval :: Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ICtx
ctx EvalType
et = Expr -> StateT EvalEnv IO Expr
go
  where
    go :: Expr -> StateT EvalEnv IO Expr
go (ELam (Symbol
x,Sort
s) Expr
e)   = Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> StateT EvalEnv IO Expr
evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
x, Sort
s) Expr
e
    go e :: Expr
e@EIte{}         = Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e
    go (ECoerc Sort
s Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
s Sort
t (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go e :: Expr
e@(EApp Expr
_ Expr
_)     =
      case Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e of
       (Expr
f, [Expr]
es) | EvalType
et EvalType -> EvalType -> Bool
forall a. Eq a => a -> a -> Bool
== EvalType
RWNormal ->
          -- Just evaluate the arguments first, to give rewriting a chance to step in
          -- if necessary
          do
            [Expr]
es' <- (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ICtx
ctx EvalType
et) [Expr]
es
            if [Expr]
es [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Expr]
es'
              then Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
f [Expr]
es')
              else do
                Expr
f' <- case Expr -> Expr
dropECst Expr
f of
                  EVar Symbol
_ -> Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
f
                  Expr
_      -> Expr -> StateT EvalEnv IO Expr
go Expr
f
                Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
f' [Expr]
es') (Maybe Expr -> Expr)
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> StateT EvalEnv IO (Maybe Expr)
evalApp Knowledge
γ ICtx
ctx Expr
f' [Expr]
es EvalType
et
       (Expr
f, [Expr]
es) ->
          do
            Expr
f' <- case Expr -> Expr
dropECst Expr
f of
              EVar Symbol
_ -> Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
f
              Expr
_      -> Expr -> StateT EvalEnv IO Expr
go Expr
f
            [Expr]
es' <- (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ICtx
ctx EvalType
et) [Expr]
es
            Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
f' [Expr]
es') (Maybe Expr -> Expr)
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> StateT EvalEnv IO (Maybe Expr)
evalApp Knowledge
γ ICtx
ctx Expr
f' [Expr]
es' EvalType
et

    go (PAtom Brel
r Expr
e1 Expr
e2) = Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2
    go (ENeg Expr
e)         = Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go (EBin Bop
o Expr
e1 Expr
e2)   = Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2
    go (ETApp Expr
e Sort
t)      = (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ETApp` Sort
t) (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go (ETAbs Expr
e Symbol
s)      = (Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
`ETAbs` Symbol
s) (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go (PNot Expr
e')        = Expr -> Expr
forall v. ExprV v -> ExprV v
PNot (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e'
    go (PImp Expr
e1 Expr
e2)     = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2
    go (PIff Expr
e1 Expr
e2)     = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2
    go (PAnd [Expr]
es)        = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd ([Expr] -> Expr)
-> StateT EvalEnv IO [Expr] -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Expr -> StateT EvalEnv IO Expr
go [Expr]
es
    go (POr [Expr]
es)         = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr ([Expr] -> Expr)
-> StateT EvalEnv IO [Expr] -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse Expr -> StateT EvalEnv IO Expr
go [Expr]
es
    go Expr
e | EVar Symbol
_ <- Expr -> Expr
dropECst Expr
e = do
      Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Maybe Expr -> Expr)
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> StateT EvalEnv IO (Maybe Expr)
evalApp Knowledge
γ ICtx
ctx Expr
e [] EvalType
et
    go (ECst Expr
e Sort
t)       = (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
t) (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go (ELet Symbol
x Expr
e1 Expr
e2)   = Symbol -> Expr -> Expr -> Expr
forall v. Symbol -> ExprV v -> ExprV v -> ExprV v
ELet Symbol
x (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2

    go Expr
e                = Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e


-- | '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
evalELam :: Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> StateT EvalEnv IO Expr
evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
x, Sort
s) Expr
e
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> Bool
isEtaSymbol Symbol
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.
    [ Symbol
xFresh ] <- Int -> EvalST [Symbol]
makeFreshEtaNames Int
1
    let newBody :: Expr
newBody = Subst -> Expr -> Expr
forall a. (Subable a, HasCallStack) => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol
x, Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
xFresh)]) Expr
e

    (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
      { evNewEqualities
        = S.insert (ELam (x, s) e, ELam (xFresh, s) newBody)
                   (evNewEqualities st)
      }

    Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> StateT EvalEnv IO Expr
evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
xFresh, Sort
s) Expr
newBody
  where
    isEtaSymbol :: Symbol -> Bool
    isEtaSymbol :: Symbol -> Bool
isEtaSymbol = Symbol -> Symbol -> Bool
isPrefixOfSym Symbol
"eta"

evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
x, Sort
s) Expr
e = do
    HashMap ExScope (HashMap Expr Expr)
oldPendingUnfoldings <- (EvalEnv -> HashMap ExScope (HashMap Expr Expr))
-> StateT EvalEnv IO (HashMap ExScope (HashMap Expr Expr))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> HashMap ExScope (HashMap Expr Expr)
evPendingUnfoldings
    EvEqualities
oldEqs <- (EvalEnv -> EvEqualities) -> StateT EvalEnv IO EvEqualities
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities

    -- We need to declare the variable in the environment
    (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
      { evEnv = insertSymEnv x s $ evEnv st }

    Expr
e' <- Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval (Knowledge
γ { knLams = (x, s) : knLams γ }) ICtx
ctx EvalType
et Expr
e
    let e2' :: Expr
e2' = Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx Expr
e'
        elam :: Expr
elam = (Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, Sort
s) Expr
e
    -- Discard the old equalities which miss the lambda binding
    (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
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
      }
    Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Symbol, Sort) -> Expr -> Expr
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, Sort
s) Expr
e')

data RESTParams oc = RP
  { forall oc. RESTParams oc -> OCAlgebra oc Expr IO
oc   :: OCAlgebra oc Expr IO
  , forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path :: [(Expr, TermOrigin)]
  , forall oc. RESTParams oc -> oc
c    :: oc
  }

-- An expression is rewritable if it is in the domain of
-- Language.Fixpoint.Solver.Rewrite.convert
isExprRewritable :: Expr -> Bool
isExprRewritable :: Expr -> Bool
isExprRewritable (EIte Expr
i Expr
t Expr
e ) = Expr -> Bool
isExprRewritable Expr
i Bool -> Bool -> Bool
&& Expr -> Bool
isExprRewritable Expr
t Bool -> Bool -> Bool
&& Expr -> Bool
isExprRewritable Expr
e
isExprRewritable (EApp Expr
f Expr
e) = Expr -> Bool
isExprRewritable Expr
f Bool -> Bool -> Bool
&& Expr -> Bool
isExprRewritable Expr
e
isExprRewritable (EVar Symbol
_) = Bool
True
isExprRewritable (PNot Expr
e) = Expr -> Bool
isExprRewritable Expr
e
isExprRewritable (PAnd [Expr]
es) = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isExprRewritable [Expr]
es
isExprRewritable (POr [Expr]
es) = (Expr -> Bool) -> [Expr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Expr -> Bool
isExprRewritable [Expr]
es
isExprRewritable (PAtom Brel
_ Expr
l Expr
r) = Expr -> Bool
isExprRewritable Expr
l Bool -> Bool -> Bool
&& Expr -> Bool
isExprRewritable Expr
r
isExprRewritable (EBin Bop
_ Expr
l Expr
r) = Expr -> Bool
isExprRewritable Expr
l Bool -> Bool -> Bool
&& Expr -> Bool
isExprRewritable Expr
r
isExprRewritable (ECon Constant
_) = Bool
True
isExprRewritable (ESym SymConst
_) = Bool
True
isExprRewritable (ECst Expr
_ Sort
_) = Bool
True
isExprRewritable (PIff Expr
e0 Expr
e1) = Expr -> Bool
isExprRewritable (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
Eq Expr
e0 Expr
e1)
isExprRewritable (PImp Expr
e0 Expr
e1) = Expr -> Bool
isExprRewritable ([Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr [Expr -> Expr
forall v. ExprV v -> ExprV v
PNot Expr
e0, Expr
e1])
isExprRewritable Expr
_ = Bool
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 :: [[(Symbol, SortedReft)]] -> [Expr] -> [Expr]
deANF [[(Symbol, SortedReft)]]
binds = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Expr) -> [Expr] -> [Expr])
-> (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Symbol -> Maybe SortedReft) -> Expr -> Expr
inlineInExpr (Symbol -> HashMap Symbol SortedReft -> Maybe SortedReft
forall k v. Hashable k => k -> HashMap k v -> Maybe v
`HashMap.Lazy.lookup` HashMap Symbol SortedReft
bindEnv)
  where
    bindEnv :: HashMap Symbol SortedReft
bindEnv = Lens' SortedReft SortedReft
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
forall v.
Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANF (SortedReft -> f SortedReft) -> SortedReft -> f SortedReft
forall a. a -> a
Lens' SortedReft SortedReft
id
        (HashMap Symbol SortedReft -> HashMap Symbol SortedReft)
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> SortedReft -> Bool)
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
HashMap.Lazy.filterWithKey (\Symbol
sym SortedReft
_ -> Symbol
anfPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
sym)
        (HashMap Symbol SortedReft -> HashMap Symbol SortedReft)
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
forall a b. (a -> b) -> a -> b
$ [HashMap Symbol SortedReft] -> HashMap Symbol SortedReft
forall k v. Eq k => [HashMap k v] -> HashMap k v
HashMap.Lazy.unions ([HashMap Symbol SortedReft] -> HashMap Symbol SortedReft)
-> [HashMap Symbol SortedReft] -> HashMap Symbol SortedReft
forall a b. (a -> b) -> a -> b
$ ([(Symbol, SortedReft)] -> HashMap Symbol SortedReft)
-> [[(Symbol, SortedReft)]] -> [HashMap Symbol SortedReft]
forall a b. (a -> b) -> [a] -> [b]
map [(Symbol, SortedReft)] -> HashMap Symbol SortedReft
forall k v. Hashable k => [(k, v)] -> HashMap k v
HashMap.Lazy.fromList [[(Symbol, SortedReft)]]
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 :: Knowledge -> ICtx -> RESTParams OCType -> StateT EvalEnv IO [Expr]
evalREST Knowledge
γ ICtx
ctx RESTParams OCType
rp = do
  EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
  IORef (HashMap Expr Bool)
cacheRef <- IO (IORef (HashMap Expr Bool))
-> StateT EvalEnv IO (IORef (HashMap Expr Bool))
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef (HashMap Expr Bool))
 -> StateT EvalEnv IO (IORef (HashMap Expr Bool)))
-> IO (IORef (HashMap Expr Bool))
-> StateT EvalEnv IO (IORef (HashMap Expr Bool))
forall a b. (a -> b) -> a -> b
$ HashMap Expr Bool -> IO (IORef (HashMap Expr Bool))
forall a. a -> IO (IORef a)
newIORef (HashMap Expr Bool -> IO (IORef (HashMap Expr Bool)))
-> HashMap Expr Bool -> IO (IORef (HashMap Expr Bool))
forall a b. (a -> b) -> a -> b
$ EvalEnv -> HashMap Expr Bool
evSMTCache EvalEnv
env
  IORef (HashMap Expr Bool)
-> Knowledge
-> ICtx
-> [Expr]
-> RESTParams OCType
-> StateT EvalEnv IO [Expr]
evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
γ ICtx
ctx [] RESTParams OCType
rp

evalRESTWithCache
  :: IORef (M.HashMap Expr Bool) -> Knowledge -> ICtx -> [Expr] -> RESTParams OCType -> EvalST [Expr]
evalRESTWithCache :: IORef (HashMap Expr Bool)
-> Knowledge
-> ICtx
-> [Expr]
-> RESTParams OCType
-> StateT EvalEnv IO [Expr]
evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
_ ICtx
ctx [Expr]
acc RESTParams OCType
rp
  | [Expr]
pathExprs <- ((Expr, TermOrigin) -> Expr) -> [(Expr, TermOrigin)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, TermOrigin) -> Expr
forall a b. (a, b) -> a
fst ([Char] -> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"EVAL1: path" ([(Expr, TermOrigin)] -> [(Expr, TermOrigin)])
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a b. (a -> b) -> a -> b
$ RESTParams OCType -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
  , Expr
e         <- [Expr] -> Expr
forall a. HasCallStack => [a] -> a
last [Expr]
pathExprs
  , Just Expr
v    <- Expr -> HashMap Expr Expr -> Maybe Expr
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Expr
e (ICtx -> HashMap Expr Expr
icSimpl ICtx
ctx)
  = do
    HashMap Expr Bool
smtCache <- IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool)
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool))
-> IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool)
forall a b. (a -> b) -> a -> b
$ IORef (HashMap Expr Bool) -> IO (HashMap Expr Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap Expr Bool)
cacheRef
    Bool -> EvalST () -> EvalST ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Expr
v Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e) (EvalST () -> EvalST ()) -> EvalST () -> EvalST ()
forall a b. (a -> b) -> a -> b
$ (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st
      { evNewEqualities = S.insert (e, v) (evNewEqualities st)
      , evSMTCache = smtCache
      })
    [Expr] -> StateT EvalEnv IO [Expr]
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
v Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
acc)

evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
γ ICtx
ctx [Expr]
acc RESTParams OCType
rp =
  do
    Maybe (ExploredTerms RuntimeTerm OCType IO)
mexploredTerms <- (EvalEnv -> Maybe (ExploredTerms RuntimeTerm OCType IO))
-> StateT EvalEnv IO (Maybe (ExploredTerms RuntimeTerm OCType IO))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> Maybe (ExploredTerms RuntimeTerm OCType IO)
explored
    ExScope
ebs <- (EvalEnv -> ExScope) -> StateT EvalEnv IO ExScope
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> ExScope
evExScope
    case Maybe (ExploredTerms RuntimeTerm OCType IO)
mexploredTerms of
      Maybe (ExploredTerms RuntimeTerm OCType IO)
Nothing -> [Expr] -> StateT EvalEnv IO [Expr]
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
acc
      Just ExploredTerms RuntimeTerm OCType IO
exploredTerms -> do
        Bool
se <- IO Bool -> EvalST Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ExScope -> ExploredTerms RuntimeTerm OCType IO -> Expr -> IO Bool
forall {m :: * -> *}.
Monad m =>
ExScope -> ExploredTerms RuntimeTerm OCType m -> Expr -> m Bool
shouldExploreTerm ExScope
ebs ExploredTerms RuntimeTerm OCType IO
exploredTerms Expr
exprs)
        if Bool
se then do
          [((Expr, Expr), Expr, OCType)]
possibleRWs <- SmtM [((Expr, Expr), Expr, OCType)]
-> EvalST [((Expr, Expr), Expr, OCType)]
forall a. SmtM a -> EvalST a
liftSMT (ExScope -> SmtM [((Expr, Expr), Expr, OCType)]
getRWs ExScope
ebs)
          [((Expr, Expr), Expr, OCType)]
rws <- ExploredTerms RuntimeTerm OCType IO
-> [((Expr, Expr), Expr, OCType)] -> [((Expr, Expr), Expr, OCType)]
forall {c} {m :: * -> *} {a} {c}.
ExploredTerms RuntimeTerm c m -> [(a, Expr, c)] -> [(a, Expr, c)]
notVisitedFirst ExploredTerms RuntimeTerm OCType IO
exploredTerms ([((Expr, Expr), Expr, OCType)] -> [((Expr, Expr), Expr, OCType)])
-> EvalST [((Expr, Expr), Expr, OCType)]
-> EvalST [((Expr, Expr), Expr, OCType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Expr, Expr), Expr, OCType) -> EvalST Bool)
-> [((Expr, Expr), Expr, OCType)]
-> EvalST [((Expr, Expr), Expr, OCType)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IO Bool -> EvalST Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> EvalST Bool)
-> (((Expr, Expr), Expr, OCType) -> IO Bool)
-> ((Expr, Expr), Expr, OCType)
-> EvalST Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExScope -> ((Expr, Expr), Expr, OCType) -> IO Bool
forall {a}. ExScope -> (a, Expr, OCType) -> IO Bool
allowed ExScope
ebs) [((Expr, Expr), Expr, OCType)]
possibleRWs
          EvEqualities
oldEqualities <- (EvalEnv -> EvEqualities) -> StateT EvalEnv IO EvEqualities
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
          (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { evNewEqualities = mempty }

          -- liftIO $ putStrLn $ (show $ length possibleRWs) ++ " rewrites allowed at path length " ++ (show $ (map snd $ path rp))
          Expr
e' <- do
            Expr
ec <- Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ICtx
ctx EvalType
FuncNormal Expr
exprs
            if Expr
ec Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
exprs
              then Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
ec
              else Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ICtx
ctx EvalType
RWNormal Expr
exprs

          let evalIsNewExpr :: Bool
evalIsNewExpr = Expr
e' Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.notElem` [Expr]
pathExprs
          let exprsToAdd :: [Expr]
exprsToAdd    = [Expr
e' | Bool
evalIsNewExpr]  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ (((Expr, Expr), Expr, OCType) -> Expr)
-> [((Expr, Expr), Expr, OCType)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (\((Expr, Expr)
_, Expr
e, OCType
_) -> Expr
e) [((Expr, Expr), Expr, OCType)]
rws
              acc' :: [Expr]
acc' = [Expr]
exprsToAdd [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
acc
              eqnToAdd :: [(Expr, Expr)]
eqnToAdd = [ (Expr
e1, Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx Expr
e2) | ((Expr
e1, Expr
e2), Expr
_, OCType
_) <- [((Expr, Expr), Expr, OCType)]
rws ]

          let explored' :: EvalEnv -> Maybe (ExploredTerms RuntimeTerm OCType IO)
explored' EvalEnv
st =
                if Expr -> Bool
isExprRewritable Expr
e' Bool -> Bool -> Bool
&& Expr -> Bool
isExprRewritable Expr
exprs
                  then ExploredTerms RuntimeTerm OCType IO
-> Maybe (ExploredTerms RuntimeTerm OCType IO)
forall a. a -> Maybe a
Just (ExploredTerms RuntimeTerm OCType IO
 -> Maybe (ExploredTerms RuntimeTerm OCType IO))
-> ExploredTerms RuntimeTerm OCType IO
-> Maybe (ExploredTerms RuntimeTerm OCType IO)
forall a b. (a -> b) -> a -> b
$ RuntimeTerm
-> OCType
-> HashSet RuntimeTerm
-> ExploredTerms RuntimeTerm OCType IO
-> ExploredTerms RuntimeTerm OCType IO
forall term c (m :: * -> *).
(Eq term, Hashable term) =>
term
-> c
-> HashSet term
-> ExploredTerms term c m
-> ExploredTerms term c m
ExploredTerms.insert (Expr -> RuntimeTerm
Rewrite.convert Expr
exprs) (RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp)
                                                  (RuntimeTerm -> HashSet RuntimeTerm -> HashSet RuntimeTerm
forall a. Hashable a => a -> HashSet a -> HashSet a
S.insert (Expr -> RuntimeTerm
Rewrite.convert Expr
e')
                            (HashSet RuntimeTerm -> HashSet RuntimeTerm)
-> HashSet RuntimeTerm -> HashSet RuntimeTerm
forall a b. (a -> b) -> a -> b
$ [RuntimeTerm] -> HashSet RuntimeTerm
forall a. Hashable a => [a] -> HashSet a
S.fromList ((((Expr, Expr), Expr, OCType) -> RuntimeTerm)
-> [((Expr, Expr), Expr, OCType)] -> [RuntimeTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> RuntimeTerm
Rewrite.convert (Expr -> RuntimeTerm)
-> (((Expr, Expr), Expr, OCType) -> Expr)
-> ((Expr, Expr), Expr, OCType)
-> RuntimeTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((Expr, Expr)
_, Expr
e, OCType
_) -> Expr
e)) [((Expr, Expr), Expr, OCType)]
possibleRWs))
                                        (Maybe (ExploredTerms RuntimeTerm OCType IO)
-> ExploredTerms RuntimeTerm OCType IO
forall a. HasCallStack => Maybe a -> a
Mb.fromJust (Maybe (ExploredTerms RuntimeTerm OCType IO)
 -> ExploredTerms RuntimeTerm OCType IO)
-> Maybe (ExploredTerms RuntimeTerm OCType IO)
-> ExploredTerms RuntimeTerm OCType IO
forall a b. (a -> b) -> a -> b
$ EvalEnv -> Maybe (ExploredTerms RuntimeTerm OCType IO)
explored EvalEnv
st)
                  else Maybe (ExploredTerms RuntimeTerm OCType IO)
forall a. Maybe a
Nothing

          EvEqualities
newEqualities <- (EvalEnv -> EvEqualities) -> StateT EvalEnv IO EvEqualities
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
          HashMap Expr Bool
smtCache <- IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool)
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool))
-> IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool)
forall a b. (a -> b) -> a -> b
$ IORef (HashMap Expr Bool) -> IO (HashMap Expr Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap Expr Bool)
cacheRef
          (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
            { evNewEqualities  = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd
            , evSMTCache = smtCache
            , explored = explored' st
            }

          [Expr]
acc'' <- if Bool
evalIsNewExpr
            then if Expr
e' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
exprs Bool -> Bool -> Bool
&& ((Expr, TermOrigin) -> Bool) -> [(Expr, TermOrigin)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr, TermOrigin) -> Bool
forall {a}. (a, TermOrigin) -> Bool
isRW (RESTParams OCType -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
              then (Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[]) (Expr -> [Expr])
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ((Expr, Expr) -> ICtx
addConst (Expr
exprs, Expr
e')) EvalType
NoRW Expr
e'
              else IORef (HashMap Expr Bool)
-> Knowledge
-> ICtx
-> [Expr]
-> RESTParams OCType
-> StateT EvalEnv IO [Expr]
evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
γ ((Expr, Expr) -> ICtx
addConst (Expr
exprs, Expr
e')) [Expr]
acc' (EvEqualities -> Expr -> RESTParams OCType
rpEval EvEqualities
newEqualities Expr
e')
            else [Expr] -> StateT EvalEnv IO [Expr]
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
acc'

          ([Expr]
 -> ((Expr, Expr), Expr, OCType) -> StateT EvalEnv IO [Expr])
-> [Expr]
-> [((Expr, Expr), Expr, OCType)]
-> StateT EvalEnv IO [Expr]
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\[Expr]
r ((Expr, Expr), Expr, OCType)
rw -> IORef (HashMap Expr Bool)
-> Knowledge
-> ICtx
-> [Expr]
-> RESTParams OCType
-> StateT EvalEnv IO [Expr]
evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
γ ICtx
ctx [Expr]
r (((Expr, Expr), Expr, OCType) -> RESTParams OCType
forall {a}. (a, Expr, OCType) -> RESTParams OCType
rpRW ((Expr, Expr), Expr, OCType)
rw)) [Expr]
acc'' [((Expr, Expr), Expr, OCType)]
rws
        else
          [Expr] -> StateT EvalEnv IO [Expr]
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
acc
  where
    shouldExploreTerm :: ExScope -> ExploredTerms RuntimeTerm OCType m -> Expr -> m Bool
shouldExploreTerm ExScope
ebs ExploredTerms RuntimeTerm OCType m
exploredTerms Expr
e | Expr -> Bool
Vis.isConc Expr
e =
      case RewriteArgs -> RWTerminationOpts
rwTerminationOpts (ExScope -> RewriteArgs
rwArgs ExScope
ebs) of
        RWTerminationOpts
RWTerminationCheckDisabled ->
          Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ RuntimeTerm -> ExploredTerms RuntimeTerm OCType m -> Bool
forall term c (m :: * -> *).
(Eq term, Hashable term) =>
term -> ExploredTerms term c m -> Bool
ExploredTerms.visited (Expr -> RuntimeTerm
Rewrite.convert Expr
e) ExploredTerms RuntimeTerm OCType m
exploredTerms
        RWTerminationOpts
RWTerminationCheckEnabled  ->
          RuntimeTerm
-> OCType -> ExploredTerms RuntimeTerm OCType m -> m Bool
forall term c (m :: * -> *).
(Monad m, Eq term, Hashable term, Eq c, Show c, Hashable c) =>
term -> c -> ExploredTerms term c m -> m Bool
ExploredTerms.shouldExplore (Expr -> RuntimeTerm
Rewrite.convert Expr
e) (RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp) ExploredTerms RuntimeTerm OCType m
exploredTerms
    shouldExploreTerm ExScope
_ ExploredTerms RuntimeTerm OCType m
_ Expr
_ = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    allowed :: ExScope -> (a, Expr, OCType) -> IO Bool
allowed ExScope
_ebs (a
_, Expr
rwE, OCType
_) | Expr
rwE Expr -> [Expr] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
pathExprs = Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    allowed ExScope
ebs (a
_, Expr
_, OCType
c)   = ExScope -> OCType -> IO Bool
termCheck ExScope
ebs OCType
c
    termCheck :: ExScope -> OCType -> IO Bool
termCheck ExScope
ebs OCType
c = OCAlgebra OCType Expr IO -> RewriteArgs -> OCType -> IO Bool
forall oc a. OCAlgebra oc a IO -> RewriteArgs -> oc -> IO Bool
Rewrite.passesTerminationCheck (RESTParams OCType -> OCAlgebra OCType Expr IO
forall oc. RESTParams oc -> OCAlgebra oc Expr IO
oc RESTParams OCType
rp) (ExScope -> RewriteArgs
rwArgs ExScope
ebs) OCType
c

    notVisitedFirst :: ExploredTerms RuntimeTerm c m -> [(a, Expr, c)] -> [(a, Expr, c)]
notVisitedFirst ExploredTerms RuntimeTerm c m
exploredTerms [(a, Expr, c)]
rws =
      let
        ([(a, Expr, c)]
v, [(a, Expr, c)]
nv) = ((a, Expr, c) -> Bool)
-> [(a, Expr, c)] -> ([(a, Expr, c)], [(a, Expr, c)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (\(a
_, Expr
e, c
_) -> RuntimeTerm -> ExploredTerms RuntimeTerm c m -> Bool
forall term c (m :: * -> *).
(Eq term, Hashable term) =>
term -> ExploredTerms term c m -> Bool
ExploredTerms.visited (Expr -> RuntimeTerm
Rewrite.convert Expr
e) ExploredTerms RuntimeTerm c m
exploredTerms) [(a, Expr, c)]
rws
      in
        [(a, Expr, c)]
nv [(a, Expr, c)] -> [(a, Expr, c)] -> [(a, Expr, c)]
forall a. [a] -> [a] -> [a]
++ [(a, Expr, c)]
v

    rpEval :: EvEqualities -> Expr -> RESTParams OCType
rpEval EvEqualities
newEqualities Expr
e' =
      let
        c' :: OCType
c' =
          if ((Expr, TermOrigin) -> Bool) -> [(Expr, TermOrigin)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr, TermOrigin) -> Bool
forall {a}. (a, TermOrigin) -> Bool
isRW (RESTParams OCType -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
            then ((Expr, Expr) -> OCType -> OCType)
-> OCType -> [(Expr, Expr)] -> OCType
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Expr
e1, Expr
e2) OCType
ctrs -> OCAlgebra OCType Expr IO -> OCType -> Expr -> Expr -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine (RESTParams OCType -> OCAlgebra OCType Expr IO
forall oc. RESTParams oc -> OCAlgebra oc Expr IO
oc RESTParams OCType
rp) OCType
ctrs Expr
e1 Expr
e2) (RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp) (EvEqualities -> [(Expr, Expr)]
forall a. HashSet a -> [a]
S.toList EvEqualities
newEqualities)
            else RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp

      in
        RESTParams OCType
rp{path = path rp ++ [(e', PLE)], c = c'}

    isRW :: (a, TermOrigin) -> Bool
isRW (a
_, TermOrigin
r) = TermOrigin
r TermOrigin -> TermOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== TermOrigin
RW

    rpRW :: (a, Expr, OCType) -> RESTParams OCType
rpRW (a
_, Expr
e', OCType
c') = RESTParams OCType
rp{path = path rp ++ [(e', RW)], c = c' }

    pathExprs :: [Expr]
pathExprs       = ((Expr, TermOrigin) -> Expr) -> [(Expr, TermOrigin)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, TermOrigin) -> Expr
forall a b. (a, b) -> a
fst ([Char] -> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"EVAL2: path" ([(Expr, TermOrigin)] -> [(Expr, TermOrigin)])
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a b. (a -> b) -> a -> b
$ RESTParams OCType -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
    exprs :: Expr
exprs           = [Expr] -> Expr
forall a. HasCallStack => [a] -> a
last [Expr]
pathExprs
    autorws :: [AutoRewrite]
autorws         = Knowledge -> Maybe SubcId -> [AutoRewrite]
getAutoRws Knowledge
γ (ICtx -> Maybe SubcId
icSubcId ICtx
ctx)

    rwArgs :: ExScope -> RewriteArgs
rwArgs ExScope
ebs = (Expr -> SmtM Bool) -> RWTerminationOpts -> RewriteArgs
RWArgs (IORef (HashMap Expr Bool)
-> ExScope -> Knowledge -> Expr -> SmtM Bool
isValid IORef (HashMap Expr Bool)
cacheRef ExScope
ebs Knowledge
γ) (RWTerminationOpts -> RewriteArgs)
-> RWTerminationOpts -> RewriteArgs
forall a b. (a -> b) -> a -> b
$ Knowledge -> RWTerminationOpts
knRWTerminationOpts Knowledge
γ

    getRWs :: ExScope -> SmtM [((Expr, Expr), Expr, OCType)]
getRWs ExScope
ebs =
      do
        -- Optimization: If we got here via rewriting, then the current constraints
        -- are satisfiable; otherwise double-check that rewriting is still allowed
        Bool
ok <-
          if (Expr, TermOrigin) -> Bool
forall {a}. (a, TermOrigin) -> Bool
isRW ((Expr, TermOrigin) -> Bool) -> (Expr, TermOrigin) -> Bool
forall a b. (a -> b) -> a -> b
$ [(Expr, TermOrigin)] -> (Expr, TermOrigin)
forall a. HasCallStack => [a] -> a
last (RESTParams OCType -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
            then Bool -> SmtM Bool
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            else IO Bool -> SmtM Bool
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> SmtM Bool) -> IO Bool -> SmtM Bool
forall a b. (a -> b) -> a -> b
$ ExScope -> OCType -> IO Bool
termCheck ExScope
ebs (RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp)
        if Bool
ok
          then
            do
              let getRW :: SubExpr
-> AutoRewrite
-> MaybeT (StateT Context IO) ((Expr, Expr), Expr, OCType)
getRW SubExpr
e AutoRewrite
ar = OCAlgebra OCType Expr IO
-> RewriteArgs
-> OCType
-> SubExpr
-> AutoRewrite
-> MaybeT (StateT Context IO) ((Expr, Expr), Expr, OCType)
forall oc.
OCAlgebra oc Expr IO
-> RewriteArgs
-> oc
-> SubExpr
-> AutoRewrite
-> MaybeT (StateT Context IO) ((Expr, Expr), Expr, oc)
Rewrite.getRewrite (RESTParams OCType -> OCAlgebra OCType Expr IO
forall oc. RESTParams oc -> OCAlgebra oc Expr IO
oc RESTParams OCType
rp) (ExScope -> RewriteArgs
rwArgs ExScope
ebs) (RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp) SubExpr
e AutoRewrite
ar
              let getRWs' :: SubExpr -> SmtM [((Expr, Expr), Expr, OCType)]
getRWs' SubExpr
s  = [Maybe ((Expr, Expr), Expr, OCType)]
-> [((Expr, Expr), Expr, OCType)]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe ((Expr, Expr), Expr, OCType)]
 -> [((Expr, Expr), Expr, OCType)])
-> SmtM [Maybe ((Expr, Expr), Expr, OCType)]
-> SmtM [((Expr, Expr), Expr, OCType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AutoRewrite -> SmtM (Maybe ((Expr, Expr), Expr, OCType)))
-> [AutoRewrite] -> SmtM [Maybe ((Expr, Expr), Expr, OCType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (MaybeT (StateT Context IO) ((Expr, Expr), Expr, OCType)
-> SmtM (Maybe ((Expr, Expr), Expr, OCType))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (StateT Context IO) ((Expr, Expr), Expr, OCType)
 -> SmtM (Maybe ((Expr, Expr), Expr, OCType)))
-> (AutoRewrite
    -> MaybeT (StateT Context IO) ((Expr, Expr), Expr, OCType))
-> AutoRewrite
-> SmtM (Maybe ((Expr, Expr), Expr, OCType))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpr
-> AutoRewrite
-> MaybeT (StateT Context IO) ((Expr, Expr), Expr, OCType)
getRW SubExpr
s) [AutoRewrite]
autorws
              [[((Expr, Expr), Expr, OCType)]] -> [((Expr, Expr), Expr, OCType)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[((Expr, Expr), Expr, OCType)]]
 -> [((Expr, Expr), Expr, OCType)])
-> StateT Context IO [[((Expr, Expr), Expr, OCType)]]
-> SmtM [((Expr, Expr), Expr, OCType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubExpr -> SmtM [((Expr, Expr), Expr, OCType)])
-> [SubExpr] -> StateT Context IO [[((Expr, Expr), Expr, OCType)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SubExpr -> SmtM [((Expr, Expr), Expr, OCType)]
getRWs' (Expr -> [SubExpr]
subExprs Expr
exprs)
          else [((Expr, Expr), Expr, OCType)]
-> SmtM [((Expr, Expr), Expr, OCType)]
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []

    addConst :: (Expr, Expr) -> ICtx
addConst (Expr
e,Expr
e') = if HashSet Symbol -> Expr -> Bool
isConstant (Knowledge -> HashSet Symbol
knDCs Knowledge
γ) Expr
e'
                      then ICtx
ctx { icSimpl = M.insert e e' $ icSimpl ctx} else ICtx
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)
evalApp :: Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> StateT EvalEnv IO (Maybe Expr)
evalApp Knowledge
γ ICtx
ctx Expr
e0 [Expr]
es EvalType
et
  | EVar Symbol
f <- Expr -> Expr
dropECst Expr
e0
  , Just Equation
eq <- Symbol -> Map Symbol Equation -> Maybe Equation
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
f (Knowledge -> Map Symbol Equation
knAms Knowledge
γ)
  , ExScope -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> ExScope
forall v. EquationV v -> ExScope
eqArgs Equation
eq) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  = do
       SEnv Sort
env <- (EvalEnv -> SEnv Sort) -> StateT EvalEnv IO (SEnv Sort)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort (SymEnv -> SEnv Sort)
-> (EvalEnv -> SymEnv) -> EvalEnv -> SEnv Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalEnv -> SymEnv
evEnv)
       Bool
okFuel <- Symbol -> EvalST Bool
checkFuel Symbol
f
       if Bool
okFuel Bool -> Bool -> Bool
&& EvalType
et EvalType -> EvalType -> Bool
forall a. Eq a => a -> a -> Bool
/= EvalType
FuncNormal then do
         let ([Expr]
es1, [Expr]
es2) = Int -> [Expr] -> ([Expr], [Expr])
forall a. Int -> [a] -> ([a], [a])
splitAt (ExScope -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> ExScope
forall v. EquationV v -> ExScope
eqArgs Equation
eq)) [Expr]
es
         -- See Note [Elaboration for eta expansion].
         let newE :: Expr
newE = SEnv Sort -> Equation -> [Expr] -> Expr
substEq SEnv Sort
env Equation
eq [Expr]
es1
         Expr
newE' <- if ICtx -> Bool
icEtaBetaFlag ICtx
ctx
                    then [Char] -> Expr -> StateT EvalEnv IO Expr
elaborateExpr [Char]
"EvalApp unfold full: " Expr
newE
                    else Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
newE

         Expr
e' <- Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
newE'        -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
         let e2' :: Expr
e2' = Expr -> Expr
stripPLEUnfold Expr
e'
         let e3' :: Expr
e3' = Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
e2' [Expr]
es2)  -- reduces a bit the equations

         if Expr -> Bool
forall {v}. ExprV v -> Bool
hasUndecidedGuard Expr
e' Bool -> Bool -> Bool
&& Expr -> Maybe Expr
forall {v}. ExprV v -> Maybe (ExprV v)
guardOf Expr
e' Maybe Expr -> Maybe Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> Maybe Expr
forall {v}. ExprV v -> Maybe (ExprV v)
guardOf Expr
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
           (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
             { evPendingUnfoldings =
                 M.insertWith M.union (evExScope st) (M.singleton (eApps e0 es) e3') (evPendingUnfoldings st)
             }
           Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
         else do
           Symbol -> EvalST ()
useFuel Symbol
f
           (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
             { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)
             , evPendingUnfoldings = M.adjust (M.delete (eApps e0 es)) (evExScope st) (evPendingUnfoldings st)
             }
           Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
e2' [Expr]
es2)
       else Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
  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 :: Expr -> Expr
stripPLEUnfold Expr
e
      | (Expr
ef, [Expr
arg]) <- Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e
      , EVar Symbol
f <- Expr -> Expr
dropECst Expr
ef
      , Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"Language.Haskell.Liquid.ProofCombinators.pleUnfold"
      = Expr
arg
      | Bool
otherwise = Expr
e

    hasUndecidedGuard :: ExprV v -> Bool
hasUndecidedGuard EIte{} = Bool
True
    hasUndecidedGuard ExprV v
_ = Bool
False

    guardOf :: ExprV v -> Maybe (ExprV v)
guardOf (EIte ExprV v
g ExprV v
_ ExprV v
_) = ExprV v -> Maybe (ExprV v)
forall a. a -> Maybe a
Just ExprV v
g
    guardOf ExprV v
_ = Maybe (ExprV v)
forall a. Maybe a
Nothing

evalApp Knowledge
γ ICtx
ctx Expr
e0 args :: [Expr]
args@(Expr
e:[Expr]
es) EvalType
_
  | EVar Symbol
f <- Expr -> Expr
dropECst Expr
e0
  , (Expr
d, [Expr]
as) <- Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e
  , EVar Symbol
dc <- Expr -> Expr
dropECst Expr
d
  , Just [(Rewrite, IsUserDataSMeasure)]
rws <- Symbol
-> Map Symbol [(Rewrite, IsUserDataSMeasure)]
-> Maybe [(Rewrite, IsUserDataSMeasure)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
dc (Knowledge -> Map Symbol [(Rewrite, IsUserDataSMeasure)]
knSims Knowledge
γ)
    -- User data measures aren't sent to the SMT solver because
    -- it knows already about selectors and constructor tests.
  , Just (Rewrite
rw, IsUserDataSMeasure
isUserDataSMeasure) <- ((Rewrite, IsUserDataSMeasure) -> Bool)
-> [(Rewrite, IsUserDataSMeasure)]
-> Maybe (Rewrite, IsUserDataSMeasure)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\(Rewrite
rw, IsUserDataSMeasure
_) -> Rewrite -> Symbol
smName Rewrite
rw Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f) [(Rewrite, IsUserDataSMeasure)]
rws
  , [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
  = do
    let newE :: Expr
newE = Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (Subst -> Expr -> Expr
forall a. (Subable a, HasCallStack) => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
rw) [Expr]
as) (Rewrite -> Expr
smBody Rewrite
rw)) [Expr]
es
    Bool -> EvalST () -> EvalST ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IsUserDataSMeasure
isUserDataSMeasure IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
forall a. Eq a => a -> a -> Bool
== IsUserDataSMeasure
NoUserDataSMeasure) (EvalST () -> EvalST ()) -> EvalST () -> EvalST ()
forall a b. (a -> b) -> a -> b
$
      (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
        { evNewEqualities = S.insert (eApps e0 args, simplify γ ctx newE) (evNewEqualities st) }
    Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
newE)

evalApp Knowledge
γ ICtx
ctx Expr
e0 [Expr]
es EvalType
_et
  | eqs :: [(Expr, Expr)]
eqs@((Expr, Expr)
_:[(Expr, Expr)]
_) <- Knowledge -> Expr -> [(Expr, Expr)]
noUserDataMeasureEqs Knowledge
γ (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
e0 [Expr]
es)
  = do
       let eqs' :: [(Expr, Expr)]
eqs' = ((Expr, Expr) -> (Expr, Expr)) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Expr) -> (Expr, Expr) -> (Expr, Expr)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ((Expr -> Expr) -> (Expr, Expr) -> (Expr, Expr))
-> (Expr -> Expr) -> (Expr, Expr) -> (Expr, Expr)
forall a b. (a -> b) -> a -> b
$ Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx) [(Expr, Expr)]
eqs
       (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
         EvalEnv
st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }
       Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

evalApp Knowledge
γ ICtx
ctx Expr
e0 [Expr]
es EvalType
et
  | ELam (Symbol
argName, Sort
_) Expr
body <- Expr -> Expr
dropECst Expr
e0
  , Expr
lambdaArg:[Expr]
remArgs <- [Expr]
es
  , ICtx -> Bool
icEtaBetaFlag ICtx
ctx Bool -> Bool -> Bool
|| ICtx -> Bool
icExtensionalityFlag ICtx
ctx
  = do
      Bool
isFuelOk <- Symbol -> EvalST Bool
checkFuel Symbol
argName
      if Bool
isFuelOk
        then do
          Symbol -> EvalST ()
useFuel Symbol
argName
          let argSubst :: Subst
argSubst = [(Symbol, Expr)] -> Subst
mkSubst [(Symbol
argName, Expr
lambdaArg)]
          let body' :: Expr
body' = Subst -> Expr -> Expr
forall a. (Subable a, HasCallStack) => Subst -> a -> a
subst Subst
argSubst Expr
body
          Expr
body'' <- Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
body'
          let simpBody :: Expr
simpBody = Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
body'' [Expr]
remArgs)
          (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
            EvalEnv
st { evNewEqualities = S.insert (eApps e0 es, simpBody) (evNewEqualities st) }
          Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> Expr -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
body'' [Expr]
remArgs)
        else do
          Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

evalApp Knowledge
_ ICtx
ctx Expr
e0 [Expr]
es EvalType
_
  | ICtx -> Bool
icLocalRewritesFlag ICtx
ctx
  , EVar Symbol
f <- Expr -> Expr
dropECst Expr
e0
  , Just Expr
rw <- Symbol -> LocalRewrites -> Maybe Expr
lookupRewrite Symbol
f (LocalRewrites -> Maybe Expr) -> LocalRewrites -> Maybe Expr
forall a b. (a -> b) -> a -> b
$ ICtx -> LocalRewrites
icLRWs ICtx
ctx
  = do
      -- expandedTerm <- elaborateExpr "EvalApp rewrite local:" $ eApps rw es
      let expandedTerm :: Expr
expandedTerm = Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
rw [Expr]
es
      (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
        { evNewEqualities = S.insert (eApps e0 es, expandedTerm) (evNewEqualities st) }
      Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
expandedTerm)

evalApp Knowledge
_γ ICtx
ctx Expr
e0 [Expr]
es EvalType
_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 Symbol
_f) sortAnnotation :: Sort
sortAnnotation@FFunc{} <- Expr
e0
  , ICtx -> Bool
icEtaBetaFlag ICtx
ctx
  , let expectedArgs :: [Sort]
expectedArgs = Sort -> [Sort]
unpackFFuncs Sort
sortAnnotation
  , let nProvidedArgs :: Int
nProvidedArgs = [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  , let nArgsMissing :: Int
nArgsMissing = [Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
expectedArgs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nProvidedArgs
  , Int
nArgsMissing Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
  = do
    let etaArgsType :: [Sort]
etaArgsType = Int -> [Sort] -> [Sort]
forall a. Int -> [a] -> [a]
drop Int
nProvidedArgs [Sort]
expectedArgs
    -- Fresh names for the eta expansion
    [Symbol]
etaNames <- Int -> EvalST [Symbol]
makeFreshEtaNames Int
nArgsMissing

    let etaVars :: [Expr]
etaVars = (Symbol -> Sort -> Expr) -> [Symbol] -> [Sort] -> [Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
name Sort
ty -> Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst (Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
name) Sort
ty) [Symbol]
etaNames [Sort]
etaArgsType
    let fullBody :: Expr
fullBody = Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
e0 ([Expr]
es [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
etaVars)
    let etaExpandedTerm :: Expr
etaExpandedTerm = Expr -> ExScope -> Expr
forall {t :: * -> *} {v}.
Foldable t =>
ExprV v -> t (Symbol, Sort) -> ExprV v
mkLams Expr
fullBody ([Symbol] -> [Sort] -> ExScope
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
etaNames [Sort]
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
    (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
      { evNewEqualities = S.insert (eApps e0 es, etaExpandedTerm) (evNewEqualities st) }
    Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
etaExpandedTerm)
  where
    unpackFFuncs :: Sort -> [Sort]
unpackFFuncs (FFunc Sort
t Sort
ts) = Sort
t Sort -> [Sort] -> [Sort]
forall a. a -> [a] -> [a]
: Sort -> [Sort]
unpackFFuncs Sort
ts
    unpackFFuncs Sort
_ = []

    mkLams :: ExprV v -> t (Symbol, Sort) -> ExprV v
mkLams ExprV v
subject t (Symbol, Sort)
binds = ((Symbol, Sort) -> ExprV v -> ExprV v)
-> ExprV v -> t (Symbol, Sort) -> ExprV v
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Symbol, Sort) -> ExprV v -> ExprV v
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam ExprV v
subject t (Symbol, Sort)
binds

evalApp Knowledge
_ ICtx
_ctx Expr
_e0 [Expr]
_es EvalType
_ = do
  Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing

-- | 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
evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx EvalType
et (ECst Expr
e Sort
t) = do
  (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ECst` Sort
t) (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e
evalIte Knowledge
γ ICtx
ctx EvalType
et (EIte Expr
i Expr
e1 Expr
e2) = do
      Expr
b <- Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ ICtx
ctx EvalType
et Expr
i
      Maybe Bool
b'  <- [Char] -> Maybe Bool -> Maybe Bool
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalEIt POS " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Expr, Expr) -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Expr
i, Expr
b)) (Maybe Bool -> Maybe Bool)
-> StateT EvalEnv IO (Maybe Bool) -> StateT EvalEnv IO (Maybe Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> Expr -> StateT EvalEnv IO (Maybe Bool)
isValidCached Knowledge
γ Expr
b
      case Maybe Bool
b' of
        Just Bool
True -> Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e1
        Just Bool
False -> Knowledge -> ICtx -> EvalType -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e2
        Maybe Bool
_ -> Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte Expr
b Expr
e1 Expr
e2)
evalIte Knowledge
_ ICtx
_ EvalType
_ Expr
e' = Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'

-- | 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 :: Knowledge -> Expr -> [(Expr, Expr)]
noUserDataMeasureEqs Knowledge
γ Expr
e =
  [ (Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) Expr
e, Subst -> Expr -> Expr
forall a. (Subable a, HasCallStack) => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
rw) [Expr]
es) (Rewrite -> Expr
smBody Rewrite
rw))
  | (Expr
ef, [Expr]
es) <- [Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e]
  , EVar Symbol
f <- [Expr -> Expr
dropECst Expr
ef]
  , Just [(Rewrite, IsUserDataSMeasure)]
rws <- [Symbol
-> Map Symbol [(Rewrite, IsUserDataSMeasure)]
-> Maybe [(Rewrite, IsUserDataSMeasure)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
f (Knowledge -> Map Symbol [(Rewrite, IsUserDataSMeasure)]
knSims Knowledge
γ)]
  , (Rewrite
rw, IsUserDataSMeasure
NoUserDataSMeasure) <- [(Rewrite, IsUserDataSMeasure)]
rws
  , [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
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 :: SEnv Sort -> Equation -> [Expr] -> Expr
substEq SEnv Sort
env Equation
eq [Expr]
es = Subst -> Expr -> Expr
forall a. (Subable a, HasCallStack) => Subst -> a -> a
subst Subst
su (SEnv Sort -> Equation -> [Expr] -> Expr
substEqCoerce SEnv Sort
env Equation
eq [Expr]
es)
  where su :: Subst
su = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Equation -> [Symbol]
eqArgNames Equation
eq) [Expr]
es

substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
substEqCoerce SEnv Sort
env Equation
eq [Expr]
es = CoSubV -> Expr -> Expr
Vis.applyCoSubV CoSubV
coSub (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Equation -> Expr
forall v. EquationV v -> ExprV v
eqBody Equation
eq
  where
    ts :: [Sort]
ts    = (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd    ((Symbol, Sort) -> Sort) -> ExScope -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Equation -> ExScope
forall v. EquationV v -> ExScope
eqArgs Equation
eq
    sp :: SrcSpan
sp    = [Char] -> SrcSpan
panicSpan [Char]
"mkCoSub"
    eTs :: [Sort]
eTs   = SrcSpan -> SEnv Sort -> Expr -> Sort
sortExpr SrcSpan
sp SEnv Sort
env (Expr -> Sort) -> [Expr] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    coSub :: CoSubV
coSub = SEnv Sort -> [Sort] -> [Sort] -> CoSubV
mkCoSub SEnv Sort
env [Sort]
eTs [Sort]
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 :: SEnv Sort -> [Sort] -> [Sort] -> CoSubV
mkCoSub SEnv Sort
env [Sort]
eTs [Sort]
xTs = [(Sort, Sort)] -> CoSubV
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [ (Sort
x, [Sort] -> Sort
unite [Sort]
ys) | (Sort
x, [Sort]
ys) <- [(Sort, Sort)] -> [(Sort, [Sort])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Sort, Sort)]
xys ]
  where
    unite :: [Sort] -> Sort
unite [Sort]
ts    = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
Mb.fromMaybe ([Sort] -> Sort
forall {a} {a}. PPrint a => a -> a
uError [Sort]
ts) (Env -> [Sort] -> Maybe Sort
unifyTo1 Env
symToSearch [Sort]
ts)
    symToSearch :: Env
symToSearch = SEnv Sort -> Env
forall a. SEnv a -> Symbol -> SESearch a
mkSearchEnv SEnv Sort
env
    uError :: a -> a
uError a
ts   = [Char] -> a
forall a. HasCallStack => [Char] -> a
panic ([Char]
"mkCoSub: cannot build CoSub for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Sort, Sort)] -> [Char]
forall a. PPrint a => a -> [Char]
showpp [(Sort, Sort)]
xys [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" cannot unify " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
showpp a
ts)
    xys :: [(Sort, Sort)]
    xys :: [(Sort, Sort)]
xys         = [(Sort, Sort)] -> [(Sort, Sort)]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([(Sort, Sort)] -> [(Sort, Sort)])
-> [(Sort, Sort)] -> [(Sort, Sort)]
forall a b. (a -> b) -> a -> b
$ [[(Sort, Sort)]] -> [(Sort, Sort)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Sort, Sort)]] -> [(Sort, Sort)])
-> [[(Sort, Sort)]] -> [(Sort, Sort)]
forall a b. (a -> b) -> a -> b
$ (Sort -> Sort -> [(Sort, Sort)])
-> [Sort] -> [Sort] -> [[(Sort, Sort)]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Sort -> Sort -> [(Sort, Sort)]
matchSorts [Sort]
xTs [Sort]
eTs

matchSorts :: Sort -> Sort -> [(Sort, Sort)]
matchSorts :: Sort -> Sort -> [(Sort, Sort)]
matchSorts = Sort -> Sort -> [(Sort, Sort)]
go
  where
    go :: Sort -> Sort -> [(Sort, Sort)]
go x :: Sort
x@(FObj Symbol
_)    {-FObj-} Sort
y    = [(Sort
x, Sort
y)]
    go x :: Sort
x@(FVar Int
_)    {-FObj-} Sort
y    = [(Sort
x, Sort
y)]
    go (FAbs Int
_ Sort
t1)   (FAbs Int
_ Sort
t2)   = Sort -> Sort -> [(Sort, Sort)]
go Sort
t1 Sort
t2
    go (FFunc Sort
s1 Sort
t1) (FFunc Sort
s2 Sort
t2) = Sort -> Sort -> [(Sort, Sort)]
go Sort
s1 Sort
s2 [(Sort, Sort)] -> [(Sort, Sort)] -> [(Sort, Sort)]
forall a. [a] -> [a] -> [a]
++ Sort -> Sort -> [(Sort, Sort)]
go Sort
t1 Sort
t2
    go (FApp Sort
s1 Sort
t1)  (FApp Sort
s2 Sort
t2)  = Sort -> Sort -> [(Sort, Sort)]
go Sort
s1 Sort
s2 [(Sort, Sort)] -> [(Sort, Sort)] -> [(Sort, Sort)]
forall a. [a] -> [a] -> [a]
++ Sort -> Sort -> [(Sort, Sort)]
go Sort
t1 Sort
t2
    go Sort
_             Sort
_             = []

--------------------------------------------------------------------------------

eqArgNames :: Equation -> [Symbol]
eqArgNames :: Equation -> [Symbol]
eqArgNames = ((Symbol, Sort) -> Symbol) -> ExScope -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst (ExScope -> [Symbol])
-> (Equation -> ExScope) -> Equation -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> ExScope
forall v. EquationV v -> ExScope
eqArgs

isValidCached :: Knowledge -> Expr -> EvalST (Maybe Bool)
isValidCached :: Knowledge -> Expr -> StateT EvalEnv IO (Maybe Bool)
isValidCached Knowledge
γ Expr
e = do
  EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
  case Expr -> HashMap Expr Bool -> Maybe Bool
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Expr
e (EvalEnv -> HashMap Expr Bool
evSMTCache EvalEnv
env) of
    Maybe Bool
Nothing -> do
      let isFreeInE :: (Symbol, b) -> Bool
isFreeInE (Symbol
s, b
_) = Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member Symbol
s (Expr -> HashSet Symbol
exprSymbolsSet Expr
e))
      Bool
b <- Knowledge -> Expr -> EvalST Bool
knPredsEvalST Knowledge
γ Expr
e
      if Bool
b
        then do
          Bool -> EvalST () -> EvalST ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (((Symbol, Sort) -> Bool) -> ExScope -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol, Sort) -> Bool
forall {b}. (Symbol, b) -> Bool
isFreeInE (Knowledge -> ExScope
knLams Knowledge
γ)) (EvalST () -> EvalST ()) -> EvalST () -> EvalST ()
forall a b. (a -> b) -> a -> b
$
            EvalEnv -> EvalST ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalEnv
env { evSMTCache = M.insert e True (evSMTCache env) })
          Maybe Bool -> StateT EvalEnv IO (Maybe Bool)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)
        else do
          Bool
b2 <- Knowledge -> Expr -> EvalST Bool
knPredsEvalST Knowledge
γ (Expr -> Expr
forall v. ExprV v -> ExprV v
PNot Expr
e)
          if Bool
b2
            then do
              Bool -> EvalST () -> EvalST ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (((Symbol, Sort) -> Bool) -> ExScope -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol, Sort) -> Bool
forall {b}. (Symbol, b) -> Bool
isFreeInE (Knowledge -> ExScope
knLams Knowledge
γ)) (EvalST () -> EvalST ()) -> EvalST () -> EvalST ()
forall a b. (a -> b) -> a -> b
$
                EvalEnv -> EvalST ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalEnv
env { evSMTCache = M.insert e False (evSMTCache env) })
              Maybe Bool -> StateT EvalEnv IO (Maybe Bool)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False)
            else
              Maybe Bool -> StateT EvalEnv IO (Maybe Bool)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
forall a. Maybe a
Nothing

    Maybe Bool
mb -> Maybe Bool -> StateT EvalEnv IO (Maybe Bool)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
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.
    Knowledge -> Map Symbol [(Rewrite, IsUserDataSMeasure)]
knSims              :: Map Symbol [(Rewrite, IsUserDataSMeasure)]
  , Knowledge -> Map Symbol Equation
knAms               :: Map Symbol Equation -- ^ All function definitions
    -- | @knPreds γ bsInSMT xs e@ checks whether @e@ is valid under the
    -- assumptions that all variables in @bsInSMT@ are in the SMT solver,
    -- and that all variables in @xs@ need tp be declared in the SMT solver.
  , Knowledge -> ExScope -> ExScope -> Expr -> SmtM Bool
knPreds             :: [(Symbol, Sort)] -> [(Symbol, Sort)] -> Expr -> SmtM Bool
  , Knowledge -> ExScope
knLams              :: ![(Symbol, Sort)]
  , Knowledge -> [(Symbol, Int)]
knSummary           :: ![(Symbol, Int)]     -- ^ summary of functions to be evaluates (knSims and knAsms) with their arity
  , Knowledge -> HashSet Symbol
knDCs               :: !(S.HashSet Symbol)  -- ^ data constructors drawn from Rewrite
  , Knowledge -> HashMap Symbol DataCtor
knDataCtors         :: !(M.HashMap Symbol DataCtor) -- ^ data constructors by name
  , Knowledge -> SelectorMap
knSels              :: !SelectorMap
  , Knowledge -> ConstDCMap
knConsts            :: !ConstDCMap
  , Knowledge -> HashMap SubcId [AutoRewrite]
knAutoRWs           :: M.HashMap SubcId [AutoRewrite]
  , Knowledge -> RWTerminationOpts
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 (IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
(IsUserDataSMeasure -> IsUserDataSMeasure -> Bool)
-> (IsUserDataSMeasure -> IsUserDataSMeasure -> Bool)
-> Eq IsUserDataSMeasure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
== :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
$c/= :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
/= :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
Eq, Int -> IsUserDataSMeasure -> [Char] -> [Char]
[IsUserDataSMeasure] -> [Char] -> [Char]
IsUserDataSMeasure -> [Char]
(Int -> IsUserDataSMeasure -> [Char] -> [Char])
-> (IsUserDataSMeasure -> [Char])
-> ([IsUserDataSMeasure] -> [Char] -> [Char])
-> Show IsUserDataSMeasure
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> IsUserDataSMeasure -> [Char] -> [Char]
showsPrec :: Int -> IsUserDataSMeasure -> [Char] -> [Char]
$cshow :: IsUserDataSMeasure -> [Char]
show :: IsUserDataSMeasure -> [Char]
$cshowList :: [IsUserDataSMeasure] -> [Char] -> [Char]
showList :: [IsUserDataSMeasure] -> [Char] -> [Char]
Show)

knPredsEvalST :: Knowledge -> Expr -> EvalST Bool
knPredsEvalST :: Knowledge -> Expr -> EvalST Bool
knPredsEvalST Knowledge
γ Expr
e = do
    EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
    SmtM Bool -> EvalST Bool
forall a. SmtM a -> EvalST a
liftSMT (SmtM Bool -> EvalST Bool) -> SmtM Bool -> EvalST Bool
forall a b. (a -> b) -> a -> b
$ Knowledge -> ExScope -> ExScope -> Expr -> SmtM Bool
knPreds Knowledge
γ (EvalEnv -> ExScope
evExScope EvalEnv
env) (Knowledge -> ExScope
knLams Knowledge
γ) Expr
e

isValid :: IORef (M.HashMap Expr Bool) -> [(Symbol, Sort)] -> Knowledge -> Expr -> SmtM Bool
isValid :: IORef (HashMap Expr Bool)
-> ExScope -> Knowledge -> Expr -> SmtM Bool
isValid IORef (HashMap Expr Bool)
cacheRef ExScope
bs Knowledge
γ Expr
e = do
    HashMap Expr Bool
smtCache <- IO (HashMap Expr Bool) -> StateT Context IO (HashMap Expr Bool)
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (HashMap Expr Bool) -> StateT Context IO (HashMap Expr Bool))
-> IO (HashMap Expr Bool) -> StateT Context IO (HashMap Expr Bool)
forall a b. (a -> b) -> a -> b
$ IORef (HashMap Expr Bool) -> IO (HashMap Expr Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap Expr Bool)
cacheRef
    case Expr -> HashMap Expr Bool -> Maybe Bool
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Expr
e HashMap Expr Bool
smtCache of
      Maybe Bool
Nothing -> do
        Bool
b <- Knowledge -> ExScope -> ExScope -> Expr -> SmtM Bool
knPreds Knowledge
γ ExScope
bs (Knowledge -> ExScope
knLams Knowledge
γ) Expr
e
        Bool -> StateT Context IO () -> StateT Context IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (StateT Context IO () -> StateT Context IO ())
-> StateT Context IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$
          IO () -> StateT Context IO ()
forall a. IO a -> StateT Context IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT Context IO ()) -> IO () -> StateT Context IO ()
forall a b. (a -> b) -> a -> b
$ IORef (HashMap Expr Bool) -> HashMap Expr Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap Expr Bool)
cacheRef (Expr -> Bool -> HashMap Expr Bool -> HashMap Expr Bool
forall k v. Hashable k => k -> v -> HashMap k v -> HashMap k v
M.insert Expr
e Bool
True HashMap Expr Bool
smtCache)
        Bool -> SmtM Bool
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
      Just Bool
b -> Bool -> SmtM Bool
forall a. a -> StateT Context IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b

knowledge :: Config -> SInfo a -> Knowledge
knowledge :: forall a. Config -> SInfo a -> Knowledge
knowledge Config
cfg SInfo a
si = KN
  { knSims :: Map Symbol [(Rewrite, IsUserDataSMeasure)]
knSims                     = ([(Rewrite, IsUserDataSMeasure)]
 -> [(Rewrite, IsUserDataSMeasure)]
 -> [(Rewrite, IsUserDataSMeasure)])
-> [(Symbol, [(Rewrite, IsUserDataSMeasure)])]
-> Map Symbol [(Rewrite, IsUserDataSMeasure)]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [(Rewrite, IsUserDataSMeasure)]
-> [(Rewrite, IsUserDataSMeasure)]
-> [(Rewrite, IsUserDataSMeasure)]
forall a. [a] -> [a] -> [a]
(++) ([(Symbol, [(Rewrite, IsUserDataSMeasure)])]
 -> Map Symbol [(Rewrite, IsUserDataSMeasure)])
-> [(Symbol, [(Rewrite, IsUserDataSMeasure)])]
-> Map Symbol [(Rewrite, IsUserDataSMeasure)]
forall a b. (a -> b) -> a -> b
$
                                   [ (Rewrite -> Symbol
smDC Rewrite
rw, [(Rewrite
rw, IsUserDataSMeasure
NoUserDataSMeasure)]) | Rewrite
rw <- [Rewrite]
sims ] [(Symbol, [(Rewrite, IsUserDataSMeasure)])]
-> [(Symbol, [(Rewrite, IsUserDataSMeasure)])]
-> [(Symbol, [(Rewrite, IsUserDataSMeasure)])]
forall a. [a] -> [a] -> [a]
++
                                   [ (Rewrite -> Symbol
smDC Rewrite
rw, [(Rewrite
rw, IsUserDataSMeasure
UserDataSMeasure)]) | Rewrite
rw <- [Rewrite]
dataSims ]
  , knAms :: Map Symbol Equation
knAms                      = [(Symbol, Equation)] -> Map Symbol Equation
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Equation -> Symbol
forall v. EquationV v -> Symbol
eqName Equation
eq, Equation
eq) | Equation
eq <- AxiomEnv -> [Equation]
aenvEqs AxiomEnv
aenv]
  , knPreds :: ExScope -> ExScope -> Expr -> SmtM Bool
knPreds                    = HasCallStack => Config -> ExScope -> ExScope -> Expr -> SmtM Bool
Config -> ExScope -> ExScope -> Expr -> SmtM Bool
askSMT Config
cfg
  , knLams :: ExScope
knLams                     = []
  , knSummary :: [(Symbol, Int)]
knSummary                  =    ((\Rewrite
s -> (Rewrite -> Symbol
smName Rewrite
s, Int
1)) (Rewrite -> (Symbol, Int)) -> [Rewrite] -> [(Symbol, Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)
                                 [(Symbol, Int)] -> [(Symbol, Int)] -> [(Symbol, Int)]
forall a. [a] -> [a] -> [a]
++ ((\Equation
s -> (Equation -> Symbol
forall v. EquationV v -> Symbol
eqName Equation
s, ExScope -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> ExScope
forall v. EquationV v -> ExScope
eqArgs Equation
s))) (Equation -> (Symbol, Int)) -> [Equation] -> [(Symbol, Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Equation]
aenvEqs AxiomEnv
aenv)
                                 [(Symbol, Int)] -> [(Symbol, Int)] -> [(Symbol, Int)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Int)]
rwSyms
  , knDCs :: HashSet Symbol
knDCs                      = [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList (Rewrite -> Symbol
smDC (Rewrite -> Symbol) -> [Rewrite] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)
  , knDataCtors :: HashMap Symbol DataCtor
knDataCtors                = [(Symbol, DataCtor)] -> HashMap Symbol DataCtor
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [ (Located Symbol -> Symbol
forall a. Located a -> a
val (DataCtor -> Located Symbol
dcName DataCtor
dc), DataCtor
dc) | DataDecl
dd <- SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si, DataCtor
dc <- DataDecl -> [DataCtor]
ddCtors DataDecl
dd ]
  , knSels :: SelectorMap
knSels                     = (Rewrite -> Maybe (Symbol, (Symbol, Int)))
-> [Rewrite] -> SelectorMap
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel  [Rewrite]
sims
  , knConsts :: ConstDCMap
knConsts                   = (Rewrite -> Maybe (Symbol, (Symbol, Expr)))
-> [Rewrite] -> ConstDCMap
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Rewrite -> Maybe (Symbol, (Symbol, Expr))
makeCons [Rewrite]
sims
  , knAutoRWs :: HashMap SubcId [AutoRewrite]
knAutoRWs                  = AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
aenv
  , knRWTerminationOpts :: RWTerminationOpts
knRWTerminationOpts        =
      if Config -> Bool
rwTermination Config
cfg
      then RWTerminationOpts
RWTerminationCheckEnabled
      else RWTerminationOpts
RWTerminationCheckDisabled
  }
  where
    ([Rewrite]
simDCTests, [Rewrite]
sims0) =
      [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorTests (SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si) ([Rewrite] -> ([Rewrite], [Rewrite]))
-> [Rewrite] -> ([Rewrite], [Rewrite])
forall a b. (a -> b) -> a -> b
$ AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv
    ([Rewrite]
simDCSelectors, [Rewrite]
sims) =
      [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorSelectors (SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si) [Rewrite]
sims0
    dataSims :: [Rewrite]
dataSims = [Rewrite]
simDCTests [Rewrite] -> [Rewrite] -> [Rewrite]
forall a. [a] -> [a] -> [a]
++ [Rewrite]
simDCSelectors
    aenv :: AxiomEnv
aenv = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
si

    inRewrites :: Symbol -> Bool
    inRewrites :: Symbol -> Bool
inRewrites Symbol
e =
      let
        symbs :: [Symbol]
symbs = (AutoRewrite -> Maybe Symbol) -> [AutoRewrite] -> [Symbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (Expr -> Maybe Symbol
lhsHead (Expr -> Maybe Symbol)
-> (AutoRewrite -> Expr) -> AutoRewrite -> Maybe Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AutoRewrite -> Expr
arLHS) ([[AutoRewrite]] -> [AutoRewrite]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[AutoRewrite]] -> [AutoRewrite])
-> [[AutoRewrite]] -> [AutoRewrite]
forall a b. (a -> b) -> a -> b
$ HashMap SubcId [AutoRewrite] -> [[AutoRewrite]]
forall k v. HashMap k v -> [v]
M.elems (HashMap SubcId [AutoRewrite] -> [[AutoRewrite]])
-> HashMap SubcId [AutoRewrite] -> [[AutoRewrite]]
forall a b. (a -> b) -> a -> b
$ AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
aenv)
      in
        Symbol
e Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem` [Symbol]
symbs

    lhsHead :: Expr -> Maybe Symbol
    lhsHead :: Expr -> Maybe Symbol
lhsHead Expr
e | (Expr
ef, [Expr]
_) <- Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e, EVar Symbol
f <- Expr -> Expr
dropECst Expr
ef = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
f
    lhsHead Expr
_ = Maybe Symbol
forall a. Maybe a
Nothing


    rwSyms :: [(Symbol, Int)]
rwSyms = ((Symbol, Int) -> Bool) -> [(Symbol, Int)] -> [(Symbol, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol -> Bool
inRewrites (Symbol -> Bool)
-> ((Symbol, Int) -> Symbol) -> (Symbol, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Int) -> Symbol
forall a b. (a, b) -> a
fst) ([(Symbol, Int)] -> [(Symbol, Int)])
-> [(Symbol, Int)] -> [(Symbol, Int)]
forall a b. (a -> b) -> a -> b
$ ((Symbol, Sort) -> (Symbol, Int)) -> ExScope -> [(Symbol, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> (Symbol, Int)
forall {b} {a}. Num b => (a, Sort) -> (a, b)
toSum (SEnv Sort -> ExScope
forall a. SEnv a -> [(Symbol, a)]
toListSEnv (SInfo a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits SInfo a
si))
      where
        toSum :: (a, Sort) -> (a, b)
toSum (a
sym, Sort
sort)      = (a
sym, Sort -> b
forall {a}. Num a => Sort -> a
getArity Sort
sort)

        getArity :: Sort -> a
getArity (FFunc Sort
_ Sort
rhs) = a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ Sort -> a
getArity Sort
rhs
        getArity Sort
_             = a
0



    makeCons :: Rewrite -> Maybe (Symbol, (Symbol, Expr))
makeCons Rewrite
rw
      | [Symbol] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (Expr -> [Symbol]) -> Expr -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Rewrite -> Expr
smBody Rewrite
rw)
      = (Symbol, (Symbol, Expr)) -> Maybe (Symbol, (Symbol, Expr))
forall a. a -> Maybe a
Just (Rewrite -> Symbol
smName Rewrite
rw, (Rewrite -> Symbol
smDC Rewrite
rw, Rewrite -> Expr
smBody Rewrite
rw))
      | Bool
otherwise
      = Maybe (Symbol, (Symbol, Expr))
forall a. Maybe a
Nothing

    makeSel :: Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel Rewrite
rw
      | EVar Symbol
x <- Rewrite -> Expr
smBody Rewrite
rw
      = (Rewrite -> Symbol
smName Rewrite
rw,) ((Symbol, Int) -> (Symbol, (Symbol, Int)))
-> (Int -> (Symbol, Int)) -> Int -> (Symbol, (Symbol, Int))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rewrite -> Symbol
smDC Rewrite
rw,) (Int -> (Symbol, (Symbol, Int)))
-> Maybe Int -> Maybe (Symbol, (Symbol, Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> [Symbol] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
L.elemIndex Symbol
x (Rewrite -> [Symbol]
smArgs Rewrite
rw)
      | Bool
otherwise
      = Maybe (Symbol, (Symbol, Int))
forall a. Maybe a
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 :: [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorTests [DataDecl]
dds [Rewrite]
rws = (Rewrite -> Bool) -> [Rewrite] -> ([Rewrite], [Rewrite])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition Rewrite -> Bool
isDataConstructorTest [Rewrite]
rws
  where
    isDataConstructorTest :: Rewrite -> Bool
isDataConstructorTest Rewrite
sm = Symbol -> Bool
isTestSymbol (Rewrite -> Symbol
smName Rewrite
sm) Bool -> Bool -> Bool
&& Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member (Rewrite -> Symbol
smDC Rewrite
sm) HashSet Symbol
userDefinedDcs
    userDefinedDcs :: HashSet Symbol
userDefinedDcs =
      [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList [ Located Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (DataCtor -> Located Symbol
dcName DataCtor
dc) | DataDecl
dd <- [DataDecl]
dds, DataCtor
dc <- DataDecl -> [DataCtor]
ddCtors DataDecl
dd ]

-- | Like 'partitionUserDataConstructorTests' but for selectors.
partitionUserDataConstructorSelectors :: [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorSelectors :: [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorSelectors [DataDecl]
dds [Rewrite]
rws = (Rewrite -> Bool) -> [Rewrite] -> ([Rewrite], [Rewrite])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition Rewrite -> Bool
isSelector [Rewrite]
rws
  where
    isSelector :: Rewrite -> Bool
isSelector Rewrite
sm = Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member (Rewrite -> Symbol
smName Rewrite
sm) HashSet Symbol
userDefinedDcFieldsSelectors
    userDefinedDcFieldsSelectors :: HashSet Symbol
userDefinedDcFieldsSelectors =
      [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList [ DataField -> Symbol
forall a. Symbolic a => a -> Symbol
symbol DataField
dcf | DataDecl
dd <- [DataDecl]
dds, DataCtor
dc <- DataDecl -> [DataCtor]
ddCtors DataDecl
dd, DataField
dcf <- DataCtor -> [DataField]
dcFields DataCtor
dc ]


--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

-- (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 :: HashSet Symbol -> Expr -> Bool
isConstant HashSet Symbol
dcs Expr
e = HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Hashable a => HashSet a -> HashSet a -> HashSet a
S.difference (Expr -> HashSet Symbol
exprSymbolsSet Expr
e) HashSet Symbol
dcs)

simplify :: Knowledge -> ICtx -> Expr -> Expr
simplify :: Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ictx Expr
exprs = [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"simplification of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
showpp Expr
exprs) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr) -> Expr -> Expr
forall {t}. Eq t => (t -> t) -> t -> t
fix' ((Expr -> Expr) -> Expr -> Expr
Vis.mapExprOnExpr Expr -> Expr
tx) Expr
exprs
    where
      fix' :: (t -> t) -> t -> t
fix' t -> t
f t
e = if t
e t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
e' then t
e else (t -> t) -> t -> t
fix' t -> t
f t
e' where e' :: t
e' = t -> t
f t
e
      tx :: Expr -> Expr
tx Expr
e
        | Just Expr
e' <- Expr -> HashMap Expr Expr -> Maybe Expr
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Expr
e (ICtx -> HashMap Expr Expr
icSimpl ICtx
ictx)
        = Expr
e'

      tx (PAtom Brel
rel Expr
e1 Expr
e2) = Brel -> Expr -> Expr -> Expr
applyBooleanFolding Brel
rel Expr
e1 Expr
e2
      tx (EBin Bop
bop Expr
e1 Expr
e2) = Bop -> Expr -> Expr -> Expr
applyConstantFolding Bop
bop Expr
e1 Expr
e2
      tx (ENeg Expr
e)         = Bop -> Expr -> Expr -> Expr
applyConstantFolding Bop
Minus (Constant -> Expr
forall v. Constant -> ExprV v
ECon (SubcId -> Constant
I SubcId
0)) Expr
e
      tx (EApp Expr
e1 Expr
e2)
        | Expr -> Bool
isSetPred Expr
e1    = Expr -> Expr -> Expr
applySetFolding Expr
e1 Expr
e2

      tx (EApp Expr
ef Expr
a)
        | EVar Symbol
f <- Expr -> Expr
dropECst Expr
ef
        , Just (Symbol
dc, Expr
c)  <- Symbol -> ConstDCMap -> Maybe (Symbol, Expr)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
f (Knowledge -> ConstDCMap
knConsts Knowledge
γ)
        , (Expr
ed, [Expr]
_) <- Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
a
        , EVar Symbol
dc' <- Expr -> Expr
dropECst Expr
ed
        , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc'
        = Expr
c
      tx (EIte Expr
b Expr
e1 Expr
e2)
        | Expr -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred Expr
b  = Expr
e1
        | Expr -> Bool
forall v. Eq v => ExprV v -> Bool
isContraPred Expr
b = Expr
e2
      tx (ECoerc Sort
s Sort
t Expr
e)
        | Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t = Expr
e
      tx (EApp Expr
ef Expr
a)
        | EVar Symbol
f <- Expr -> Expr
dropECst Expr
ef
        , Just (Symbol
dc, Int
i)  <- Symbol -> SelectorMap -> Maybe (Symbol, Int)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
f (Knowledge -> SelectorMap
knSels Knowledge
γ)
        , (Expr
ed, [Expr]
es) <- Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
a
        , EVar Symbol
dc' <- Expr -> Expr
dropECst Expr
ed
        , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc'
        = [Expr]
es[Expr] -> Int -> Expr
forall a. HasCallStack => [a] -> Int -> a
!!Int
i
      tx Expr
e = Expr
e


-------------------------------------------------------------------------------
-- | Normalization of Equation: make their arguments unique -------------------
-------------------------------------------------------------------------------

class Normalizable a where
  normalize :: a -> a

instance Normalizable (GInfo c a) where
  normalize :: GInfo c a -> GInfo c a
normalize GInfo c a
si = GInfo c a
si {ae = normalize $ ae si}

instance Normalizable AxiomEnv where
  normalize :: AxiomEnv -> AxiomEnv
normalize AxiomEnv
aenv = AxiomEnv
aenv { aenvEqs   = mytracepp "aenvEqs"  (normalize <$> aenvEqs   aenv)
                        , aenvSimpl = mytracepp "aenvSimpl" (normalize <$> aenvSimpl aenv) }

instance Normalizable Rewrite where
  normalize :: Rewrite -> Rewrite
normalize Rewrite
rw = Rewrite
rw { smArgs = xs', smBody = normalizeBody (smName rw) $ subst su $ smBody rw }
    where
      su :: Subst
su  = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> (Symbol, Expr))
-> [Symbol] -> [Symbol] -> [(Symbol, Expr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      xs :: [Symbol]
xs  = Rewrite -> [Symbol]
smArgs Rewrite
rw
      xs' :: [Symbol]
xs' = (Symbol -> SubcId -> Symbol) -> [Symbol] -> [SubcId] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> SubcId -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
mkSymbol [Symbol]
xs [SubcId
0 :: Integer ..]
      mkSymbol :: Symbol -> a -> Symbol
mkSymbol Symbol
x a
i = Symbol
x Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol -> a -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (Rewrite -> Symbol
smName Rewrite
rw) a
i


instance Normalizable Equation where
  normalize :: Equation -> Equation
normalize Equation
eq = Equation
eq {eqArgs = zip xs' ss, eqBody = normalizeBody (eqName eq) $ subst su $ eqBody eq }
    where
      su :: Subst
su      = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> (Symbol, Expr))
-> [Symbol] -> [Symbol] -> [(Symbol, Expr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      ([Symbol]
xs,[Sort]
ss) = ExScope -> ([Symbol], [Sort])
forall a b. [(a, b)] -> ([a], [b])
unzip (Equation -> ExScope
forall v. EquationV v -> ExScope
eqArgs Equation
eq)
      xs' :: [Symbol]
xs'     = (Symbol -> SubcId -> Symbol) -> [Symbol] -> [SubcId] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> SubcId -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
mkSymbol [Symbol]
xs [SubcId
0 :: Integer ..]
      mkSymbol :: Symbol -> a -> Symbol
mkSymbol Symbol
x a
i = Symbol
x Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol -> a -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (Equation -> Symbol
forall v. EquationV v -> Symbol
eqName Equation
eq) a
i

-- | Normalize the given named expression if it is recursive.
normalizeBody :: Symbol -> Expr -> Expr
normalizeBody :: Symbol -> Expr -> Expr
normalizeBody Symbol
f Expr
exprs | Symbol
f Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
exprs = Expr -> Expr
forall {v}. Eq v => ExprV v -> ExprV v
go Expr
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 :: ExprV v -> ExprV v
go (PAnd [PImp ExprV v
c ExprV v
e1, PImp (PNot ExprV v
c') ExprV v
e2]) | ExprV v
c ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
c' = ExprV v -> ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte ExprV v
c ExprV v
e1 (ExprV v -> ExprV v
go ExprV v
e2)
    go ExprV v
e                                               = ExprV v
e
normalizeBody Symbol
_ Expr
e = Expr
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 :: Symbol -> EvalST ()
useFuel Symbol
f = do
  (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st { evFuel = useFuelCount f (evFuel st) })

-- | Increment the fuel count.
useFuelCount :: Symbol -> FuelCount -> FuelCount
useFuelCount :: Symbol -> FuelCount -> FuelCount
useFuelCount Symbol
f FuelCount
fc = FuelCount
fc { fcMap = M.insert f (k + 1) m }
  where
    k :: Int
k             = Int -> Symbol -> HashMap Symbol Int -> Int
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault Int
0 Symbol
f HashMap Symbol Int
m
    m :: HashMap Symbol Int
m             = FuelCount -> HashMap Symbol Int
fcMap FuelCount
fc

makeFreshEtaNames :: Int -> EvalST [Symbol]
makeFreshEtaNames :: Int -> EvalST [Symbol]
makeFreshEtaNames Int
n = Int -> StateT EvalEnv IO Symbol -> EvalST [Symbol]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n StateT EvalEnv IO Symbol
makeFreshName
  where
    makeFreshName :: StateT EvalEnv IO Symbol
makeFreshName = do
      Int
ident <- (EvalEnv -> Int) -> StateT EvalEnv IO Int
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> Int
freshEtaNames
      (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> EvalST ())
-> (EvalEnv -> EvalEnv) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { freshEtaNames = 1 + freshEtaNames st }
      Symbol -> StateT EvalEnv IO Symbol
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Symbol -> StateT EvalEnv IO Symbol)
-> Symbol -> StateT EvalEnv IO Symbol
forall a b. (a -> b) -> a -> b
$ Int -> Symbol
etaExpSymbol Int
ident

elaborateExpr :: String -> Expr -> EvalST Expr
elaborateExpr :: [Char] -> Expr -> StateT EvalEnv IO Expr
elaborateExpr [Char]
msg Expr
e = do
  let elabSpan :: Located [Char]
elabSpan = SrcSpan -> [Char] -> Located [Char]
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan [Char]
msg
  EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
  let symEnv' :: SymEnv
symEnv' = SymEnv -> ExScope -> SymEnv
insertsSymEnv (EvalEnv -> SymEnv
evEnv EvalEnv
env) (EvalEnv -> ExScope
evExScope EvalEnv
env)
  ElabFlags
ef <- (EvalEnv -> ElabFlags) -> StateT EvalEnv IO ElabFlags
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> ElabFlags
evElabF
  Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
unApply (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ ElabParam -> Expr -> Expr
forall a. (Elaborate a, HasCallStack) => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam ElabFlags
ef Located [Char]
elabSpan SymEnv
symEnv') Expr
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 :: Symbol -> EvalST Bool
checkFuel Symbol
f = do
  FuelCount
fc <- (EvalEnv -> FuelCount) -> StateT EvalEnv IO FuelCount
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> FuelCount
evFuel
  case (Symbol -> HashMap Symbol Int -> Maybe Int
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup Symbol
f (FuelCount -> HashMap Symbol Int
fcMap FuelCount
fc), FuelCount -> Maybe Int
fcMax FuelCount
fc) of
    (Just Int
fk, Just Int
n) -> Bool -> EvalST Bool
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
fk Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n)
    (Maybe Int, Maybe Int)
_                 -> Bool -> EvalST Bool
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True


-- Note [Existential quantification when unfolding]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- After FUSION is performed, some predicates, which previously used kvars, may
-- contain existential quantifications.
--
-- When the unfoldings are searched by PLE in expressions with existentials,
-- we make sure that the produced unfoldings still have the existential
-- bindings in scope.
--
-- The procedure is as follows:
-- 1. First, we rename the existential variables in the predicates of the bindings
--    to make them unique ('renameExistentialsInSortedRefts').
--
--    @exists x y. f x y || (exists x. g x y)@
--
--    becomes
--
--    @exists v0 v1. f v0 v1 || (exists v2. g v2 v1)@
--
-- 2. We extract the nested existentials to prenex form, and we store the bodies of
--    the existentials in a map with the existential binders as keys
--    ('prenexExistentials' and 'updCtx').
--
--    @exists v0 v1. f v0 v1 || (exists v2. g v2 v1)@
--
--    produces the map
--
--    @[v0, v1, v2] -> f v0 v1 || g v2 v1@
--
-- 3. We declare to the SMT solver the existential variables in every scope
--    (in 'withAssms').
--
-- 4. We then look for unfoldings in each of the subexpressions. Whenever
--    we find an unfolding, we record the scope in which it was found.
--
--    @[v0, v1, v3] -> (f v0 v1 = v0 < v1) && (g v2 = v2 > v1)@
--
-- 5. When PLE is finished, we create for every scope an existential
--    quantification whose body contains all the corresponding unfoldings
--    and the original subexpressions in the scope ('reconstructExistentials').
--
--    @exists v0 v1 v0.
--       (f v0 v 1 = v0 < v1) && (g v2 = v2 > v1) &&
--       (f v0 v1 || g v2 v1)@
--
--    This is the expression that PLE returns.


-- | Renames existential variables in the predicates of the given bindings to
-- make them unique.
--
-- Rather than looking for all existential bindings, this function only renames
-- the superficial existentials which can be introduced by KVar solutions.
--
-- These superficial existentials appear in conjunctions, disjunctions and in the
-- body of other existentials only.
renameExistentialsInSortedRefts
  :: [(Symbol, SortedReft)]
  -> Int
  -> ([(Symbol, SortedReft)], Int)
renameExistentialsInSortedRefts :: [(Symbol, SortedReft)] -> Int -> ([(Symbol, SortedReft)], Int)
renameExistentialsInSortedRefts [(Symbol, SortedReft)]
binds0 Int
existentialCounter =
    let
        binds :: [(Symbol, SortedReft)]
binds = [ (Symbol
x, SortedReft
sr { sr_reft = mapPredReft (const p) (sr_reft sr) }) | ((Symbol
x, SortedReft
sr), Expr
p) <- [(Symbol, SortedReft)] -> [Expr] -> [((Symbol, SortedReft), Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Symbol, SortedReft)]
binds0 [Expr]
preds ]
        ([Expr]
preds, Int
existentialCounter') =
          [Expr] -> Int -> ([Expr], Int)
renameKVarExistentials (((Symbol, SortedReft) -> Expr) -> [(Symbol, SortedReft)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Reft -> Expr
forall v. ReftV v -> ExprV v
reftPred (Reft -> Expr)
-> ((Symbol, SortedReft) -> Reft) -> (Symbol, SortedReft) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortedReft -> Reft
sr_reft (SortedReft -> Reft)
-> ((Symbol, SortedReft) -> SortedReft)
-> (Symbol, SortedReft)
-> Reft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft) -> SortedReft
forall a b. (a, b) -> b
snd) [(Symbol, SortedReft)]
binds0) Int
existentialCounter
     in
        ([(Symbol, SortedReft)]
binds, Int
existentialCounter')

renameKVarExistentials :: [Expr] -> Int -> ([Expr], Int)
renameKVarExistentials :: [Expr] -> Int -> ([Expr], Int)
renameKVarExistentials = State Int [Expr] -> Int -> ([Expr], Int)
forall s a. State s a -> s -> (a, s)
runState (State Int [Expr] -> Int -> ([Expr], Int))
-> ([Expr] -> State Int [Expr]) -> [Expr] -> Int -> ([Expr], Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> StateT Int Identity Expr) -> [Expr] -> State Int [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> StateT Int Identity Expr
forall {f :: * -> *}. MonadState Int f => Expr -> f Expr
go
  where
    go :: Expr -> f Expr
go (POr [Expr]
es) = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr ([Expr] -> Expr) -> f [Expr] -> f Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> f Expr) -> [Expr] -> f [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> f Expr
go [Expr]
es
    go (PAnd [Expr]
es) = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd ([Expr] -> Expr) -> f [Expr] -> f Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> f Expr) -> [Expr] -> f [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Expr -> f Expr
go [Expr]
es
    go (PExist ExScope
bs Expr
e0) = do
      Int
i1 <- f Int
forall s (m :: * -> *). MonadState s m => m s
get
      let i2 :: Int
i2 = Int
i1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ExScope -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ExScope
bs
      Int -> f ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Int
i2
      let vs :: [Symbol]
vs = ((Symbol, Sort) -> Symbol) -> ExScope -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ExScope
bs
          vs' :: [Symbol]
vs' = [ Symbol -> SubcId -> Symbol
existSymbol Symbol
v (Int -> SubcId
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) | (Symbol
v, Int
i) <- [Symbol] -> [Int] -> [(Symbol, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs [Int
i1..] ]
          bs' :: ExScope
bs' = [Symbol] -> [Sort] -> ExScope
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs' (((Symbol, Sort) -> Sort) -> ExScope -> [Sort]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd ExScope
bs)
          su :: Subst
su = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
vs ((Symbol -> Expr) -> [Symbol] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Expr
forall v. v -> ExprV v
EVar [Symbol]
vs')
      ExScope -> Expr -> Expr
forall v. ExScope -> ExprV v -> ExprV v
PExist ExScope
bs' (Expr -> Expr) -> f Expr -> f Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> f Expr
go (HashSet Symbol -> Subst -> Expr -> Expr
rapierSubstExpr ([Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList [Symbol]
vs') Subst
su Expr
e0)
    go Expr
e = Expr -> f Expr
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e

-- ^ Scopes of existential binders identifying the location of sub-expressions
type ExScope = [(Symbol, Sort)]


-- | Extracts nested existentials from an expression.
--
-- For example, the expression
--
-- > exists [x1 : t1]. e1 == e2 &&
-- > exists [x2 : t2]. e3 == 2 &&
-- > exists [x3 : t3]. e3 < e4
--
-- would be flattened into
--
-- > (e1 == e2 && e3 == 2 && e3 < e4, [x1 : t1, x2 : t2, x3 : t3])
--
-- Precondition: the existential binding names are unique.
--
prenexExistentials :: Expr -> (ExScope, Expr)
prenexExistentials :: Expr -> (ExScope, Expr)
prenexExistentials = Expr -> (ExScope, Expr)
go
  where
    go :: Expr -> (ExScope, Expr)
    go :: Expr -> (ExScope, Expr)
go (PExist ExScope
bs Expr
e) =
      let (ExScope
bs', Expr
e') = Expr -> (ExScope, Expr)
go Expr
e
      in (ExScope
bs ExScope -> ExScope -> ExScope
forall a. [a] -> [a] -> [a]
++ ExScope
bs', Expr
e')
    go (PAnd [Expr]
es) =
      let ([ExScope]
bss, [Expr]
es') = [(ExScope, Expr)] -> ([ExScope], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Expr -> (ExScope, Expr)) -> [Expr] -> [(ExScope, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> (ExScope, Expr)
go [Expr]
es)
      in ([ExScope] -> ExScope
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ExScope]
bss, [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd [Expr]
es')
    go (POr [Expr]
es) =
      let ([ExScope]
bss, [Expr]
es') = [(ExScope, Expr)] -> ([ExScope], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip ((Expr -> (ExScope, Expr)) -> [Expr] -> [(ExScope, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> (ExScope, Expr)
go [Expr]
es)
      in ([ExScope] -> ExScope
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ExScope]
bss, [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr [Expr]
es')
    go Expr
e = ([], Expr
e)


-- | Reconstructs expressions with existentials from a map
-- of existential scopes to their bodies.
reconstructExistentials :: M.HashMap ExScope (S.HashSet Expr) -> [Expr]
reconstructExistentials :: HashMap ExScope (HashSet Expr) -> [Expr]
reconstructExistentials HashMap ExScope (HashSet Expr)
m = [ ExScope -> Expr -> Expr
forall v. ExScope -> ExprV v -> ExprV v
pExist ExScope
s ([Expr] -> Expr
pAndNoDedup ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList HashSet Expr
es) | (ExScope
s, HashSet Expr
es) <- HashMap ExScope (HashSet Expr) -> [(ExScope, HashSet Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap ExScope (HashSet Expr)
m, Bool -> Bool
not (HashSet Expr -> Bool
forall a. HashSet a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null HashSet Expr
es) ]