--------------------------------------------------------------------------------
-- | This module implements "Proof by Logical Evaluation" where we
--   unfold function definitions if they *must* be unfolded, to strengthen
--   the environments with function-definition-equalities.
--   The algorithm is discussed at length in:
--
--     1. "Refinement Reflection", POPL 2018, https://arxiv.org/pdf/1711.03842
--     2. "Reasoning about Functions", VMCAI 2018, https://ranjitjhala.github.io/static/reasoning-about-functions.pdf
--------------------------------------------------------------------------------

{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE DoAndIfThenElse           #-}

module Language.Fixpoint.Solver.PLE
  ( instantiate

  -- The following exports are for property testing.
  , FuelCount(..)
  , ICtx(..)
  , Knowledge(..)
  , simplify
  )
  where

import           Language.Fixpoint.Types hiding (simplify)
import           Language.Fixpoint.Types.Config  as FC
import           Language.Fixpoint.Types.Solutions (CMap)
import qualified Language.Fixpoint.Types.Visitor as Vis
import qualified Language.Fixpoint.Misc          as Misc
import qualified Language.Fixpoint.Smt.Interface as SMT
import           Language.Fixpoint.Defunctionalize
import           Language.Fixpoint.Solver.EnvironmentReduction (inlineInExpr, undoANF)
import qualified Language.Fixpoint.Utils.Files   as Files
import qualified Language.Fixpoint.Utils.Trie    as T
import           Language.Fixpoint.Utils.Progress
import           Language.Fixpoint.SortCheck
import           Language.Fixpoint.Graph.Deps             (isTarget)
import           Language.Fixpoint.Solver.Common          (askSMT, toSMT)
import           Language.Fixpoint.Solver.Sanitize        (symbolEnv)
import           Language.Fixpoint.Solver.Simplify
import           Language.Fixpoint.Solver.Rewrite as Rewrite

import Language.REST.OCAlgebra as OC
import Language.REST.ExploredTerms as ExploredTerms
import Language.REST.RuntimeTerm as RT
import Language.REST.SMT (withZ3, SolverHandle)

import           Control.Monad (filterM, foldM, forM_, when, replicateM)
import           Control.Monad.State
import           Control.Monad.Trans.Maybe
import           Data.Bifunctor (second)
import qualified Data.HashMap.Strict  as M
import qualified Data.HashMap.Lazy  as HashMap.Lazy
import qualified Data.HashSet         as S
import           Data.IORef
import qualified Data.List            as L
import           Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Maybe           as Mb
import qualified Data.Set as Set
import           Text.PrettyPrint.HughesPJ.Compat

mytracepp :: (PPrint a) => String -> a -> a
mytracepp :: forall a. PPrint a => [Char] -> a -> a
mytracepp = [Char] -> a -> a
forall a. PPrint a => [Char] -> a -> a
notracepp

--------------------------------------------------------------------------------
-- | Strengthen Constraint Environments via PLE
--------------------------------------------------------------------------------
{-# SCC instantiate #-}
instantiate :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate :: forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate Config
cfg SInfo a
fi' 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 -> IO InstRes) -> IO InstRes
forall a. (Maybe SolverHandle -> IO a) -> IO a
withRESTSolver ((Maybe SolverHandle -> IO InstRes) -> IO InstRes)
-> (Maybe SolverHandle -> IO InstRes) -> IO InstRes
forall a b. (a -> b) -> a -> b
$ \Maybe SolverHandle
solver -> Int -> IO InstRes -> IO InstRes
forall a. Int -> IO a -> IO a
withProgress (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) (IO InstRes -> IO InstRes) -> IO InstRes -> IO InstRes
forall a b. (a -> b) -> a -> b
$
               Config
-> [Char]
-> SymEnv
-> [Equation]
-> (Context -> IO InstRes)
-> IO InstRes
forall a.
Config
-> [Char] -> SymEnv -> [Equation] -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
sEnv (SInfo a -> [Equation]
forall (c :: * -> *) a. GInfo c a -> [Equation]
defns SInfo a
fi') ((Context -> IO InstRes) -> IO InstRes)
-> (Context -> IO InstRes) -> IO InstRes
forall a b. (a -> b) -> a -> b
$ \Context
ctx -> do
                  InstEnv a
env <- Config
-> SInfo a
-> HashMap SubcId (SimpC a)
-> Maybe SolverHandle
-> Context
-> IO (InstEnv a)
forall a.
Loc a =>
Config
-> SInfo a
-> CMap (SimpC a)
-> Maybe SolverHandle
-> Context
-> IO (InstEnv a)
instEnv Config
cfg SInfo a
info HashMap SubcId (SimpC a)
cs Maybe SolverHandle
solver Context
ctx
                  CTrie -> InstEnv a -> IO InstRes
forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t InstEnv a
env                                             -- 2. TRAVERSE Trie to compute InstRes
    Config -> SInfo a -> SymEnv -> InstRes -> IO ()
forall a. Config -> SInfo a -> SymEnv -> InstRes -> IO ()
savePLEEqualities Config
cfg SInfo a
info SymEnv
sEnv InstRes
res
    SInfo a -> IO (SInfo a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SInfo a -> IO (SInfo a)) -> SInfo a -> IO (SInfo a)
forall a b. (a -> b) -> a -> b
$ Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
forall a. Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo Config
cfg SymEnv
sEnv SInfo a
info InstRes
res                                     -- 3. STRENGTHEN SInfo using InstRes
  where
    withRESTSolver :: (Maybe SolverHandle -> IO a) -> IO a
    withRESTSolver :: forall a. (Maybe SolverHandle -> IO a) -> IO a
withRESTSolver Maybe SolverHandle -> IO 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 -> IO a
f Maybe SolverHandle
forall a. Maybe a
Nothing
    withRESTSolver Maybe SolverHandle -> IO a
f = (SolverHandle -> IO a) -> IO a
forall (m :: * -> *) b. MonadIO m => (SolverHandle -> m b) -> m b
withZ3 (Maybe SolverHandle -> IO a
f (Maybe SolverHandle -> IO a)
-> (SolverHandle -> Maybe SolverHandle) -> SolverHandle -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SolverHandle -> Maybe SolverHandle
forall a. a -> Maybe a
Just)

    file :: [Char]
file = Config -> [Char]
srcFile Config
cfg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
".evals"
    sEnv :: SymEnv
sEnv = Config -> SInfo a -> SymEnv
forall a. 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. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i InstRes
res] ])
    elabParam :: ElabParam
elabParam = ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver 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 (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 -> CMap (SimpC a) -> Maybe SolverHandle -> SMT.Context -> IO (InstEnv a)
instEnv :: forall a.
Loc a =>
Config
-> SInfo a
-> CMap (SimpC a)
-> Maybe SolverHandle
-> Context
-> IO (InstEnv a)
instEnv Config
cfg SInfo a
info CMap (SimpC a)
cs Maybe SolverHandle
restSolver Context
ctx = do
    IORef (HashMap (OCType, OCType) Bool)
refRESTCache <- 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 <- 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
              , evPendingUnfoldings :: HashMap Expr Expr
evPendingUnfoldings = 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 -> IO (InstEnv a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (InstEnv a -> IO (InstEnv a)) -> InstEnv a -> IO (InstEnv a)
forall a b. (a -> b) -> a -> b
$ InstEnv
       { ieCfg :: Config
ieCfg = Config
cfg
       , ieSMT :: Context
ieSMT = Context
ctx
       , ieBEnv :: BindEnv a
ieBEnv = ElabFlags -> BindEnv a -> BindEnv a
forall a. ElabFlags -> BindEnv a -> BindEnv a
coerceBindEnv ElabFlags
ef (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 -> Context -> SInfo a -> Knowledge
forall a. Config -> Context -> SInfo a -> Knowledge
knowledge Config
cfg Context
ctx 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
       }
  where
    ef :: ElabFlags
ef = SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver 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. (Eq k, 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.
(Eq k, 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. (Eq k, 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.
(Eq k, 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 :: CTrie -> InstEnv a -> IO InstRes
pleTrie :: forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t InstEnv a
env = InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO 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 :: HashSet Expr
icCands              = HashSet Expr
forall a. Monoid a => a
mempty
      , icEquals :: EvEqualities
icEquals             = 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
      , 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
      }

loopT
  :: InstEnv a
  -> ICtx
  -> Diff         -- ^ The longest path suffix without forks in reverse order
  -> Maybe BindId -- ^ bind id of the branch ancestor of the trie if any.
                  --   'Nothing' when this is the top-level trie.
  -> InstRes
  -> CTrie
  -> IO InstRes
loopT :: forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx [Int]
delta Maybe Int
i InstRes
res CTrie
t = case CTrie
t of
  T.Node []  -> InstRes -> IO InstRes
forall a. a -> 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
-> IO InstRes
forall a.
InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx [Int]
delta Maybe Int
i InstRes
res Branch SubcId
b
  T.Node [Branch SubcId]
bs  -> InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> (ICtx -> IO InstRes)
-> IO InstRes
forall a b.
InstEnv a
-> ICtx -> [Int] -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx [Int]
delta Maybe SubcId
forall a. Maybe a
Nothing ((ICtx -> IO InstRes) -> IO InstRes)
-> (ICtx -> IO InstRes) -> IO InstRes
forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do
                  (ICtx
ctx'', InstEnv a
env'', InstRes
res') <- InstEnv a
-> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstEnv a, InstRes)
forall a.
InstEnv a
-> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstEnv a, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
i InstRes
res
                  (InstRes -> Branch SubcId -> IO InstRes)
-> InstRes -> [Branch SubcId] -> IO 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
-> IO InstRes
forall a.
InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env'' ICtx
ctx'' [] Maybe Int
i) InstRes
res' [Branch SubcId]
bs

loopB
  :: InstEnv a
  -> ICtx
  -> Diff         -- ^ The longest path suffix without forks in reverse order
  -> Maybe BindId -- ^ bind id of the branch ancestor of the branch if any.
                  --   'Nothing' when this is a branch of the top-level trie.
  -> InstRes
  -> CBranch
  -> IO InstRes
loopB :: forall a.
InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx [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 -> IO InstRes
forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx (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
-> (ICtx -> IO InstRes)
-> IO InstRes
forall a b.
InstEnv a
-> ICtx -> [Int] -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx [Int]
delta (SubcId -> Maybe SubcId
forall a. a -> Maybe a
Just SubcId
cid) ((ICtx -> IO InstRes) -> IO InstRes)
-> (ICtx -> IO InstRes) -> IO InstRes
forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do
                  IO ()
progressTick
                  (\(ICtx
_, InstEnv a
_, InstRes
r) -> InstRes
r) ((ICtx, InstEnv a, InstRes) -> InstRes)
-> IO (ICtx, InstEnv a, InstRes) -> IO InstRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InstEnv a
-> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstEnv a, InstRes)
forall a.
InstEnv a
-> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstEnv a, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
iMb InstRes
res

-- | Adds to @ctx@ candidate expressions to unfold from the bindings in @delta@
-- and the rhs of @cidMb@.
--
-- Adds to @ctx@ assumptions from @env@ and @delta@.
--
-- Sets the current constraint id in @ctx@ to @cidMb@.
--
-- Pushes assumptions from the modified context to the SMT solver, runs @act@,
-- and then pops the assumptions.
--
withAssms :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms :: forall a b.
InstEnv a
-> ICtx -> [Int] -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms env :: InstEnv a
env@InstEnv{CMap (SimpC a)
Config
BindEnv a
LocalRewritesEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieCfg :: forall a. InstEnv a -> Config
ieSMT :: forall a. InstEnv a -> Context
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
ieCfg :: Config
ieSMT :: Context
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: CMap (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
ieLRWs :: LocalRewritesEnv
..} ICtx
ctx [Int]
delta Maybe SubcId
cidMb ICtx -> IO b
act = do
  let ctx' :: ICtx
ctx' = InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> ICtx
forall a. InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> ICtx
updCtx InstEnv a
env ICtx
ctx [Int]
delta Maybe SubcId
cidMb
  let assms :: HashSet Expr
assms = ICtx -> HashSet Expr
icAssms ICtx
ctx'

  Context -> [Char] -> IO b -> IO b
forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ieSMT [Char]
"PLE.evaluate" (IO b -> IO b) -> IO b -> IO b
forall a b. (a -> b) -> a -> b
$ do
    HashSet Expr -> (Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ HashSet Expr
assms (Context -> Expr -> IO ()
SMT.smtAssert Context
ieSMT)
    ICtx -> IO b
act ICtx
ctx' { icAssms = mempty }

-- | @ple1@ performs the PLE at a single "node" in the Trie
--
-- It will generate equalities for all function invocations in the candidates
-- in @ctx@ for which definitions are known. The function definitions are in
-- @ieKnowl@.
ple1 :: InstEnv a -> ICtx -> Maybe BindId -> InstRes -> IO (ICtx, InstEnv a, InstRes)
ple1 :: forall a.
InstEnv a
-> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstEnv a, InstRes)
ple1 ie :: InstEnv a
ie@InstEnv{CMap (SimpC a)
Config
BindEnv a
LocalRewritesEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieCfg :: forall a. InstEnv a -> Config
ieSMT :: forall a. InstEnv a -> Context
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
ieCfg :: Config
ieSMT :: Context
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: CMap (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
ieLRWs :: LocalRewritesEnv
..} ICtx
ctx Maybe Int
i InstRes
res = do
  (ICtx
ctx', EvalEnv
env) <- StateT EvalEnv IO ICtx -> EvalEnv -> IO (ICtx, EvalEnv)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Config -> ICtx -> Context -> Knowledge -> StateT EvalEnv IO ICtx
evalCandsLoop Config
ieCfg ICtx
ctx Context
ieSMT Knowledge
ieKnowl) EvalEnv
ieEvEnv
  let pendings :: [(Expr, Expr)]
pendings = EvalEnv -> Maybe SubcId -> [(Expr, Expr)]
forall {a}. EvalEnv -> Maybe a -> [(Expr, Expr)]
collectPendingUnfoldings EvalEnv
env (ICtx -> Maybe SubcId
icSubcId ICtx
ctx)
      newEqs :: [(Expr, Expr)]
newEqs = [(Expr, Expr)]
pendings [(Expr, Expr)] -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ EvEqualities -> [(Expr, Expr)]
forall a. HashSet a -> [a]
S.toList (EvEqualities -> EvEqualities -> EvEqualities
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference (ICtx -> EvEqualities
icEquals ICtx
ctx') (ICtx -> EvEqualities
icEquals ICtx
ctx))
  (ICtx, InstEnv a, InstRes) -> IO (ICtx, InstEnv a, InstRes)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ICtx
ctx', InstEnv a
ie { ieEvEnv = env }, InstRes -> Maybe Int -> [(Expr, Expr)] -> InstRes
updCtxRes InstRes
res Maybe Int
i [(Expr, 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 -> [(Expr, Expr)]
collectPendingUnfoldings EvalEnv
env (Just a
_) | Config -> Bool
pleWithUndecidedGuards Config
ieCfg =
      HashMap Expr Expr -> [(Expr, Expr)]
forall k v. HashMap k v -> [(k, v)]
M.toList (EvalEnv -> HashMap Expr Expr
evPendingUnfoldings EvalEnv
env)
    collectPendingUnfoldings EvalEnv
_ Maybe a
_ = []

evalToSMT :: String -> Config -> SMT.Context -> (Expr, Expr) -> Pred
evalToSMT :: [Char] -> Config -> Context -> (Expr, Expr) -> Expr
evalToSMT [Char]
msg Config
cfg Context
ctx (Expr
e1,Expr
e2) = [Char] -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT ([Char]
"evalToSMT:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) Config
cfg Context
ctx [] (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 -> SMT.Context -> Knowledge -> EvalST ICtx
evalCandsLoop :: Config -> ICtx -> Context -> Knowledge -> StateT EvalEnv IO ICtx
evalCandsLoop Config
cfg ICtx
ictx0 Context
ctx Knowledge
γ = ICtx -> Int -> StateT EvalEnv IO ICtx
go ICtx
ictx0 Int
0
  where
    go :: ICtx -> Int -> StateT EvalEnv IO ICtx
go ICtx
ictx Int
_ | HashSet Expr -> Bool
forall a. HashSet a -> Bool
S.null (ICtx -> 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 <- StateT EvalEnv IO 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 IO () -> StateT EvalEnv IO ()
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT EvalEnv IO ()) -> IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Expr -> IO ()
SMT.smtAssert Context
ctx ([Expr] -> Expr
pAndNoDedup (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 }
                    cands :: [Expr]
cands = 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
icCands ICtx
ictx
                [[Expr]]
candss <- (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]
cands
                EvEqualities
us <- (EvalEnv -> EvEqualities) -> StateT EvalEnv IO EvEqualities
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
                (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { evNewEqualities = mempty }
                let noCandidateChanged :: Bool
noCandidateChanged = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (([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 :: EvEqualities
unknownEqs = EvEqualities
us EvEqualities -> EvEqualities -> EvEqualities
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` ICtx -> EvEqualities
icEquals ICtx
ictx
                if EvEqualities -> Bool
forall a. HashSet a -> Bool
S.null 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 let eqsSMT :: HashSet Expr
eqsSMT = [Char] -> Config -> Context -> (Expr, Expr) -> Expr
evalToSMT [Char]
"evalCandsLoop" Config
cfg Context
ctx ((Expr, Expr) -> Expr) -> EvEqualities -> HashSet Expr
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvEqualities
unknownEqs
                              let ictx'' :: ICtx
ictx'' = ICtx
ictx' { icEquals = icEquals ictx <> unknownEqs
                                                 , icAssms  = S.filter (not . isTautoPred) eqsSMT }
                              ICtx -> Int -> StateT EvalEnv IO ICtx
go (ICtx
ictx'' { icCands = S.fromList (concat candss) }) (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

    testForInconsistentEnvironment :: StateT EvalEnv IO Bool
testForInconsistentEnvironment =
      IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> StateT EvalEnv IO Bool)
-> IO Bool -> StateT EvalEnv IO Bool
forall a b. (a -> b) -> a -> b
$ Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds Knowledge
γ (Knowledge -> Context
knContext Knowledge
γ) (Knowledge -> [(Symbol, Sort)]
knLams 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

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

resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo :: forall a. Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo Config
cfg SymEnv
env SInfo a
info InstRes
res = SInfo a -> InstRes -> SInfo a
forall a. SInfo a -> InstRes -> SInfo a
strengthenBinds SInfo a
info InstRes
res'
  where
    res' :: InstRes
res'     = [(Int, Expr)] -> InstRes
forall k v. (Eq k, 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 => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver 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 -> Context
ieSMT   :: !SMT.Context
  , 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
  }

----------------------------------------------------------------------------------------------
-- | @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 -> HashSet Expr
icCands              :: S.HashSet Expr           -- ^ "Candidates" for unfolding
  , ICtx -> EvEqualities
icEquals             :: 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 -> 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
  }

----------------------------------------------------------------------------------------------
-- | @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, Expr)]
eqs = [ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EEq Expr
e1 Expr
e2 | (Expr
e1, Expr
e2) <- [(Expr, Expr)]
eqs, Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2 ]

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


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.
(Eq k, 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.
----------------------------------------------------------------------------------------------

updCtx :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> ICtx
updCtx :: forall a. InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> ICtx
updCtx InstEnv{CMap (SimpC a)
Config
BindEnv a
LocalRewritesEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieCfg :: forall a. InstEnv a -> Config
ieSMT :: forall a. InstEnv a -> Context
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
ieCfg :: Config
ieSMT :: Context
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: CMap (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
ieLRWs :: LocalRewritesEnv
..} ICtx
ctx [Int]
delta Maybe SubcId
cidMb
            = ICtx
ctx { icAssms  = S.fromList (filter (not . isTautoPred) ctxEqs)
                  , icCands  = S.fromList deANFedCands <> icCands  ctx
                  , icSimpl  = icSimpl ctx <> econsts
                  , icSubcId = cidMb
                  , icANFs   = anfBinds
                  , icLRWs   = mconcat $ icLRWs ctx : newLRWs
                  }
  where
    cands :: [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
ctx
    econsts :: HashMap Expr Expr
econsts   = [(Expr, Expr)] -> HashMap Expr Expr
forall k v. (Eq k, 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    = [Char] -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT [Char]
"updCtx" Config
ieCfg Context
ieSMT [] (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 | (Symbol, SortedReft)
xr <- [(Symbol, SortedReft)]
bs, Expr
c <- Expr -> [Expr]
forall v. Eq v => ExprV v -> [ExprV v]
conjuncts ((Symbol, SortedReft) -> Expr
forall a. Expression a => a -> Expr
expr (Symbol, SortedReft)
xr), [KVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [KVar]
forall v. ExprV v -> [KVar]
Vis.kvarsExpr 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
    binds :: [(Symbol, SortedReft)]
binds     = [ (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

    deANFedCands :: [Expr]
deANFedCands =
      -- 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
ctx
         Bool -> Bool -> Bool
|| ICtx -> Bool
icEtaBetaFlag ICtx
ctx then
        [[(Symbol, SortedReft)]] -> [Expr] -> [Expr]
deANF [[(Symbol, SortedReft)]]
anfBinds [Expr]
cands
      else
        [Expr]
cands


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 => 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. (Eq k, 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
    -- | Equalities where we couldn't evaluate the guards
  , EvalEnv -> HashMap Expr Expr
evPendingUnfoldings :: 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
--------------------------------------------------------------------------------

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. (Eq k, 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])
-> ((Expr, FinalExpand) -> Expr) -> (Expr, FinalExpand) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, FinalExpand) -> Expr
forall a b. (a, b) -> a
fst ((Expr, FinalExpand) -> [Expr])
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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)

-- Indicates whether or not the evaluation has expanded a function statement
-- into a conditional branch.
-- In this case, rewriting should stop
-- It's unclear whether or not rewriting in either branch makes sense,
-- since one branch could be an ill-formed expression.
newtype FinalExpand = FE Bool deriving (Int -> FinalExpand -> [Char] -> [Char]
[FinalExpand] -> [Char] -> [Char]
FinalExpand -> [Char]
(Int -> FinalExpand -> [Char] -> [Char])
-> (FinalExpand -> [Char])
-> ([FinalExpand] -> [Char] -> [Char])
-> Show FinalExpand
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> FinalExpand -> [Char] -> [Char]
showsPrec :: Int -> FinalExpand -> [Char] -> [Char]
$cshow :: FinalExpand -> [Char]
show :: FinalExpand -> [Char]
$cshowList :: [FinalExpand] -> [Char] -> [Char]
showList :: [FinalExpand] -> [Char] -> [Char]
Show)

noExpand :: FinalExpand
noExpand :: FinalExpand
noExpand = Bool -> FinalExpand
FE Bool
False

expand :: FinalExpand
expand :: FinalExpand
expand = Bool -> FinalExpand
FE Bool
True

mapFE :: (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE :: (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE Expr -> Expr
f (Expr
e, FinalExpand
fe) = (Expr -> Expr
f Expr
e, FinalExpand
fe)

feVal :: FinalExpand -> Bool
feVal :: FinalExpand -> Bool
feVal (FE Bool
f) = Bool
f

feAny :: [FinalExpand] -> FinalExpand
feAny :: [FinalExpand] -> FinalExpand
feAny [FinalExpand]
xs = Bool -> FinalExpand
FE (Bool -> FinalExpand) -> Bool -> FinalExpand
forall a b. (a -> b) -> a -> b
$ (FinalExpand -> Bool) -> [FinalExpand] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FinalExpand -> Bool
feVal [FinalExpand]
xs

infixl 9 <|>
(<|>) :: FinalExpand -> FinalExpand -> FinalExpand
<|> :: FinalExpand -> FinalExpand -> FinalExpand
(<|>) (FE Bool
True) FinalExpand
_ = FinalExpand
expand
(<|>) FinalExpand
_         FinalExpand
f = FinalExpand
f


feSeq :: [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq :: [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq [(Expr, FinalExpand)]
xs = (((Expr, FinalExpand) -> Expr) -> [(Expr, FinalExpand)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, FinalExpand) -> Expr
forall a b. (a, b) -> a
fst [(Expr, FinalExpand)]
xs, [FinalExpand] -> FinalExpand
feAny (((Expr, FinalExpand) -> FinalExpand)
-> [(Expr, FinalExpand)] -> [FinalExpand]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, FinalExpand) -> FinalExpand
forall a b. (a, b) -> b
snd [(Expr, FinalExpand)]
xs))

-- | Unfolds function invocations in expressions.
--
-- Also reduces if-then-else when the boolean condition or the negation can be
-- proved valid. This is the actual implementation of guard-validation-before-unfolding
-- that is described in publications.
--
-- Also adds to the monad state all the unfolding equalities that have been
-- discovered as necessary.
eval :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval :: Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et = Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go
  where
    go :: Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go (ELam (Symbol
x,Sort
s) Expr
e)   = Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e
    go (ECoerc Sort
s Sort
t Expr
e)   = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE (Sort -> Sort -> Expr -> Expr
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
s Sort
t)  ((Expr, FinalExpand) -> (Expr, FinalExpand))
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
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', FinalExpand
finalExpand) <- [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq ([(Expr, FinalExpand)] -> ([Expr], FinalExpand))
-> StateT EvalEnv IO [(Expr, FinalExpand)]
-> StateT EvalEnv IO ([Expr], FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO (Expr, FinalExpand))
-> [Expr] -> StateT EvalEnv IO [(Expr, FinalExpand)]
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, FinalExpand)
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, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
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', FinalExpand
finalExpand)
              else do
                (Expr
f', FinalExpand
fe) <- case Expr -> Expr
dropECst Expr
f of
                  EVar Symbol
_ -> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
f, FinalExpand
noExpand)
                  Expr
_      -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
f
                (Maybe Expr
me', FinalExpand
fe') <- Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> EvalST (Maybe Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx Expr
f' [Expr]
es EvalType
et
                (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (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
me', FinalExpand
fe FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe')
       (Expr
f, [Expr]
es) ->
          do
            (Expr
f', FinalExpand
fe1) <- case Expr -> Expr
dropECst Expr
f of
              EVar Symbol
_ -> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr
f, FinalExpand
noExpand)
              Expr
_      -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
f
            ([Expr]
es', FinalExpand
fe2) <- [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq ([(Expr, FinalExpand)] -> ([Expr], FinalExpand))
-> StateT EvalEnv IO [(Expr, FinalExpand)]
-> StateT EvalEnv IO ([Expr], FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO (Expr, FinalExpand))
-> [Expr] -> StateT EvalEnv IO [(Expr, FinalExpand)]
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, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et) [Expr]
es
            let fe :: FinalExpand
fe = FinalExpand
fe1 FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe2
            (Maybe Expr
me', FinalExpand
fe') <- Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> EvalST (Maybe Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx Expr
f' [Expr]
es' EvalType
et
            (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (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
me', FinalExpand
fe FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe')

    go (PAtom Brel
r Expr
e1 Expr
e2) = (Expr -> Expr -> Expr)
-> Expr -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
binOp (Brel -> Expr -> Expr -> Expr
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
PAtom Brel
r) Expr
e1 Expr
e2
    go (ENeg Expr
e)         = do (Expr
e', FinalExpand
fe)  <- Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e
                             (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
forall v. ExprV v -> ExprV v
ENeg Expr
e', FinalExpand
fe)
    go (EBin Bop
o Expr
e1 Expr
e2)   = do (Expr
e1', FinalExpand
fe1) <- Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e1
                             (Expr
e2', FinalExpand
fe2) <- Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e2
                             (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bop -> Expr -> Expr -> Expr
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
EBin Bop
o Expr
e1' Expr
e2', FinalExpand
fe1 FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe2)
    go (ETApp Expr
e Sort
t)      = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
`ETApp` Sort
t) ((Expr, FinalExpand) -> (Expr, FinalExpand))
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e
    go (ETAbs Expr
e Symbol
s)      = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE (Expr -> Symbol -> Expr
forall v. ExprV v -> Symbol -> ExprV v
`ETAbs` Symbol
s) ((Expr, FinalExpand) -> (Expr, FinalExpand))
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e
    go (PNot Expr
e')        = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE Expr -> Expr
forall v. ExprV v -> ExprV v
PNot ((Expr, FinalExpand) -> (Expr, FinalExpand))
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e'
    go (PImp Expr
e1 Expr
e2)     = (Expr -> Expr -> Expr)
-> Expr -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PImp Expr
e1 Expr
e2
    go (PIff Expr
e1 Expr
e2)     = (Expr -> Expr -> Expr)
-> Expr -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
PIff Expr
e1 Expr
e2
    go (PAnd [Expr]
es)        = ([Expr] -> Expr)
-> StateT EvalEnv IO [(Expr, FinalExpand)]
-> StateT EvalEnv IO (Expr, FinalExpand)
forall {m :: * -> *} {a}.
Monad m =>
([Expr] -> a) -> m [(Expr, FinalExpand)] -> m (a, FinalExpand)
efAll [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
PAnd (Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go (Expr -> StateT EvalEnv IO (Expr, FinalExpand))
-> [Expr] -> StateT EvalEnv IO [(Expr, FinalExpand)]
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]
es)
    go (POr [Expr]
es)         = ([Expr] -> Expr)
-> StateT EvalEnv IO [(Expr, FinalExpand)]
-> StateT EvalEnv IO (Expr, FinalExpand)
forall {m :: * -> *} {a}.
Monad m =>
([Expr] -> a) -> m [(Expr, FinalExpand)] -> m (a, FinalExpand)
efAll [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
POr (Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go (Expr -> StateT EvalEnv IO (Expr, FinalExpand))
-> [Expr] -> StateT EvalEnv IO [(Expr, FinalExpand)]
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]
es)
    go Expr
e | EVar Symbol
_ <- Expr -> Expr
dropECst Expr
e = do
      (Maybe Expr
me', FinalExpand
fe) <- Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> EvalST (Maybe Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx Expr
e [] EvalType
et
      (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e Maybe Expr
me', FinalExpand
fe)
    go (ECst Expr
e Sort
t)       = do (Expr
e', FinalExpand
fe) <- Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e
                             (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
e' Sort
t, FinalExpand
fe)
    go Expr
e                = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, FinalExpand
noExpand)

    binOp :: (Expr -> Expr -> Expr)
-> Expr -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
f Expr
e1 Expr
e2 = do
      (Expr
e1', FinalExpand
fe1) <- Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e1
      (Expr
e2', FinalExpand
fe2) <- Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e2
      (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
f Expr
e1' Expr
e2', FinalExpand
fe1 FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe2)

    efAll :: ([Expr] -> a) -> m [(Expr, FinalExpand)] -> m (a, FinalExpand)
efAll [Expr] -> a
f m [(Expr, FinalExpand)]
mes = do
      [(Expr, FinalExpand)]
xs <- m [(Expr, FinalExpand)]
mes
      let ([Expr]
xs', FinalExpand
fe) = [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq [(Expr, FinalExpand)]
xs
      (a, FinalExpand) -> m (a, FinalExpand)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> a
f [Expr]
xs', FinalExpand
fe)

-- | 'evalELamb' produces equations that preserve the context of a rewrite
-- so equations include any necessary lambda bindings.
evalELam :: Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (Expr, FinalExpand)
evalELam :: Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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 => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol
x, Symbol -> Expr
forall v. v -> ExprV v
EVar Symbol
xFresh)]) Expr
e

    (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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, FinalExpand)
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 Expr Expr
oldPendingUnfoldings <- (EvalEnv -> HashMap Expr Expr)
-> StateT EvalEnv IO (HashMap Expr Expr)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> 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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
      { evEnv = insertSymEnv x s $ evEnv st }

    (Expr
e', FinalExpand
fe) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
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', FinalExpand
fe)

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. (Eq k, 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. (Eq k, 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. (Eq k, 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 -> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Expr
v Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e) (StateT EvalEnv IO () -> StateT EvalEnv IO ())
-> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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
    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 -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ExploredTerms RuntimeTerm OCType IO -> Expr -> IO Bool
forall {m :: * -> *}.
Monad m =>
ExploredTerms RuntimeTerm OCType m -> Expr -> m Bool
shouldExploreTerm ExploredTerms RuntimeTerm OCType IO
exploredTerms Expr
exprs)
        if Bool
se then do
          [((Expr, Expr), Expr, OCType)]
possibleRWs <- StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
getRWs
          [((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)])
-> StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
-> StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((Expr, Expr), Expr, OCType) -> StateT EvalEnv IO Bool)
-> [((Expr, Expr), Expr, OCType)]
-> StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> StateT EvalEnv IO Bool)
-> (((Expr, Expr), Expr, OCType) -> IO Bool)
-> ((Expr, Expr), Expr, OCType)
-> StateT EvalEnv IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, Expr), Expr, OCType) -> IO Bool
forall {a}. (a, Expr, OCType) -> IO Bool
allowed) [((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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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', FE Bool
fe) <- do
            r :: (Expr, FinalExpand)
r@(Expr
ec, FinalExpand
_) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr, FinalExpand)
r
              else Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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. (Eq 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. (Eq 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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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 Bool
fe 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])
-> ((Expr, FinalExpand) -> Expr) -> (Expr, FinalExpand) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, FinalExpand) -> Expr
forall a b. (a, b) -> a
fst ((Expr, FinalExpand) -> [Expr])
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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 :: ExploredTerms RuntimeTerm OCType m -> Expr -> m Bool
shouldExploreTerm ExploredTerms RuntimeTerm OCType m
exploredTerms Expr
e | Expr -> Bool
Vis.isConc Expr
e =
      case RewriteArgs -> RWTerminationOpts
rwTerminationOpts RewriteArgs
rwArgs 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 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 :: (a, Expr, OCType) -> IO Bool
allowed (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 (a
_, Expr
_, OCType
c)   = OCType -> IO Bool
termCheck OCType
c
    termCheck :: OCType -> IO Bool
termCheck 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) RewriteArgs
rwArgs 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 :: RewriteArgs
rwArgs = (Expr -> IO Bool) -> RWTerminationOpts -> RewriteArgs
RWArgs (IORef (HashMap Expr Bool) -> Knowledge -> Expr -> IO Bool
isValid IORef (HashMap Expr Bool)
cacheRef Knowledge
γ) (RWTerminationOpts -> RewriteArgs)
-> RWTerminationOpts -> RewriteArgs
forall a b. (a -> b) -> a -> b
$ Knowledge -> RWTerminationOpts
knRWTerminationOpts Knowledge
γ

    getRWs :: StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
getRWs =
      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 -> StateT EvalEnv IO Bool
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            else IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> StateT EvalEnv IO Bool)
-> IO Bool -> StateT EvalEnv IO Bool
forall a b. (a -> b) -> a -> b
$ OCType -> IO Bool
termCheck (RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp)
        if Bool
ok
          then
            do
              let getRW :: SubExpr -> AutoRewrite -> MaybeT IO ((Expr, Expr), Expr, OCType)
getRW SubExpr
e AutoRewrite
ar = OCAlgebra OCType Expr IO
-> RewriteArgs
-> OCType
-> SubExpr
-> AutoRewrite
-> MaybeT IO ((Expr, Expr), Expr, OCType)
forall oc.
OCAlgebra oc Expr IO
-> RewriteArgs
-> oc
-> SubExpr
-> AutoRewrite
-> MaybeT 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) RewriteArgs
rwArgs (RESTParams OCType -> OCType
forall oc. RESTParams oc -> oc
c RESTParams OCType
rp) SubExpr
e AutoRewrite
ar
              let getRWs' :: SubExpr -> f [((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)])
-> f [Maybe ((Expr, Expr), Expr, OCType)]
-> f [((Expr, Expr), Expr, OCType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AutoRewrite -> f (Maybe ((Expr, Expr), Expr, OCType)))
-> [AutoRewrite] -> f [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 (IO (Maybe ((Expr, Expr), Expr, OCType))
-> f (Maybe ((Expr, Expr), Expr, OCType))
forall a. IO a -> f a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe ((Expr, Expr), Expr, OCType))
 -> f (Maybe ((Expr, Expr), Expr, OCType)))
-> (AutoRewrite -> IO (Maybe ((Expr, Expr), Expr, OCType)))
-> AutoRewrite
-> f (Maybe ((Expr, Expr), Expr, OCType))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT IO ((Expr, Expr), Expr, OCType)
-> IO (Maybe ((Expr, Expr), Expr, OCType))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO ((Expr, Expr), Expr, OCType)
 -> IO (Maybe ((Expr, Expr), Expr, OCType)))
-> (AutoRewrite -> MaybeT IO ((Expr, Expr), Expr, OCType))
-> AutoRewrite
-> IO (Maybe ((Expr, Expr), Expr, OCType))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpr -> AutoRewrite -> MaybeT 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 EvalEnv IO [[((Expr, Expr), Expr, OCType)]]
-> StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubExpr -> StateT EvalEnv IO [((Expr, Expr), Expr, OCType)])
-> [SubExpr] -> StateT EvalEnv 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 -> StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
forall {f :: * -> *}.
MonadIO f =>
SubExpr -> f [((Expr, Expr), Expr, OCType)]
getRWs' (Expr -> [SubExpr]
subExprs Expr
exprs)
          else [((Expr, Expr), Expr, OCType)]
-> StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
forall a. a -> StateT EvalEnv 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, FinalExpand)
evalApp :: Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> EvalST (Maybe Expr, FinalExpand)
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
γ)
  , [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
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 -> StateT EvalEnv IO 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 ([(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
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 -> EvalST Expr
elaborateExpr [Char]
"EvalApp unfold full: " Expr
newE
                    else Expr -> EvalST Expr
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
newE

         (Expr
e', FinalExpand
fe) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
             { evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)
             }
           (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)
         else do
           Symbol -> StateT EvalEnv IO ()
useFuel Symbol
f
           (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
             { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)
             , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)
             }
           (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
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, FinalExpand
fe)
       else (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)
  where
    -- At the time of writing, any function application wrapping an
    -- if-statement would have the effect of unfolding the invocation.
    -- However, using pleUnfold still has the advantage of not generating
    -- extra equations to unfold pleUnfold itself. Using pleUnfold also
    -- makes the intention of the user rather explicit.
    stripPLEUnfold :: 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 => 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 -> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IsUserDataSMeasure
isUserDataSMeasure IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
forall a. Eq a => a -> a -> Bool
== IsUserDataSMeasure
NoUserDataSMeasure) (StateT EvalEnv IO () -> StateT EvalEnv IO ())
-> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$
      (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
        { evNewEqualities = S.insert (eApps e0 args, simplify γ ctx newE) (evNewEqualities st) }
    (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
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, FinalExpand
noExpand)

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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
         EvalEnv
st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' }
       (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)

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 -> StateT EvalEnv IO Bool
checkFuel Symbol
argName
      if Bool
isFuelOk
        then do
          Symbol -> StateT EvalEnv IO ()
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 => Subst -> a -> a
subst Subst
argSubst Expr
body
          (Expr
body'', FinalExpand
fe) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
            EvalEnv
st { evNewEqualities = S.insert (eApps e0 es, simpBody) (evNewEqualities st) }
          (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
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, FinalExpand
fe)
        else do
          (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)

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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
        { evNewEqualities = S.insert (eApps e0 es, expandedTerm) (evNewEqualities st) }
      (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
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, FinalExpand
expand)

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 -> [(Symbol, Sort)] -> Expr
forall {t :: * -> *} {v}.
Foldable t =>
ExprV v -> t (Symbol, Sort) -> ExprV v
mkLams Expr
fullBody ([Symbol] -> [Sort] -> [(Symbol, Sort)]
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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
      { evNewEqualities = S.insert (eApps e0 es, etaExpandedTerm) (evNewEqualities st) }
    (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
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, FinalExpand
expand)
  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, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)

-- | Evaluates if-then-else statements until they can't be evaluated anymore
-- or some other expression is found.
evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
evalIte :: Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et (ECst Expr
e Sort
t) = do
  (Expr
e', FinalExpand
fe) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e
  (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Sort -> Expr
forall v. ExprV v -> Sort -> ExprV v
ECst Expr
e' Sort
t, FinalExpand
fe)
evalIte Knowledge
γ ICtx
ctx EvalType
et (EIte Expr
i Expr
e1 Expr
e2) = do
      (Expr
b, FinalExpand
_) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
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, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e1
        Just Bool
False -> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e2
        Maybe Bool
_ -> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
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, FinalExpand
expand)
evalIte Knowledge
_ ICtx
_ EvalType
_ Expr
e' = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e', FinalExpand
noExpand)

-- | Creates equations that explain how to rewrite a given constructor
-- application with all measures that aren't user data measures
noUserDataMeasureEqs :: Knowledge -> Expr -> [(Expr,Expr)]
noUserDataMeasureEqs :: 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 => 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 => 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) -> [(Symbol, Sort)] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
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. (Eq k, 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. [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) -> [(Symbol, Sort)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, Sort)] -> [Symbol])
-> (Equation -> [(Symbol, Sort)]) -> Equation -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
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. (Eq k, 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. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
s (Expr -> HashSet Symbol
exprSymbolsSet Expr
e))
      Bool
b <- IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> StateT EvalEnv IO Bool)
-> IO Bool -> StateT EvalEnv IO Bool
forall a b. (a -> b) -> a -> b
$ Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds Knowledge
γ (Knowledge -> Context
knContext Knowledge
γ) (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ) Expr
e
      if Bool
b
        then do
          Bool -> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol, Sort) -> Bool
forall {b}. (Symbol, b) -> Bool
isFreeInE (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ)) (StateT EvalEnv IO () -> StateT EvalEnv IO ())
-> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$
            EvalEnv -> StateT EvalEnv IO ()
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 <- IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> StateT EvalEnv IO Bool)
-> IO Bool -> StateT EvalEnv IO Bool
forall a b. (a -> b) -> a -> b
$ Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds Knowledge
γ (Knowledge -> Context
knContext Knowledge
γ) (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ) (Expr -> Expr
forall v. ExprV v -> ExprV v
PNot Expr
e)
          if Bool
b2
            then do
              Bool -> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Symbol, Sort) -> Bool
forall {b}. (Symbol, b) -> Bool
isFreeInE (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ)) (StateT EvalEnv IO () -> StateT EvalEnv IO ())
-> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$
                EvalEnv -> StateT EvalEnv IO ()
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
  , Knowledge -> Context
knContext           :: SMT.Context
  , Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds             :: SMT.Context -> [(Symbol, Sort)] -> Expr -> IO Bool
  , Knowledge -> [(Symbol, Sort)]
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)

isValid :: IORef (M.HashMap Expr Bool) -> Knowledge -> Expr -> IO Bool
isValid :: IORef (HashMap Expr Bool) -> Knowledge -> Expr -> IO Bool
isValid IORef (HashMap Expr Bool)
cacheRef Knowledge
γ Expr
e = do
    HashMap Expr Bool
smtCache <- 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. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Expr
e HashMap Expr Bool
smtCache of
      Maybe Bool
Nothing -> do
        Bool
b <- Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds Knowledge
γ (Knowledge -> Context
knContext Knowledge
γ) (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ) Expr
e
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b (IO () -> IO ()) -> IO () -> 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.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Expr
e Bool
True HashMap Expr Bool
smtCache)
        Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
      Maybe Bool
mb -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Bool
mb Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True)

knowledge :: Config -> SMT.Context -> SInfo a -> Knowledge
knowledge :: forall a. Config -> Context -> SInfo a -> Knowledge
knowledge Config
cfg Context
ctx 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]
  , knContext :: Context
knContext                  = Context
ctx
  , knPreds :: Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds                    = Config -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
askSMT  Config
cfg
  , knLams :: [(Symbol, Sort)]
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, [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
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. (Eq 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. (Eq k, 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
rwTerminationCheck 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))
-> [(Symbol, Sort)] -> [(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 -> [(Symbol, Sort)]
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. (Eq 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. (Eq 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. (Eq 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. (Eq 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 ]


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

withCtx :: Config -> FilePath -> SymEnv -> [Equation] -> (SMT.Context -> IO a) -> IO a
withCtx :: forall a.
Config
-> [Char] -> SymEnv -> [Equation] -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
env [Equation]
defns Context -> IO a
k = do
  Context
ctx <- Config -> [Char] -> SymEnv -> [Equation] -> IO Context
SMT.makeContextWithSEnv Config
cfg [Char]
file SymEnv
env [Equation]
defns
  ()
_   <- Context -> IO ()
SMT.smtPush Context
ctx
  a
res <- Context -> IO a
k Context
ctx
  Context -> IO ()
SMT.cleanupContext Context
ctx
  a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res


-- (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. (Eq 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. (Eq k, 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) = [(Symbol, Sort)] -> ([Symbol], [Sort])
forall a b. [(a, b)] -> ([a], [b])
unzip (Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
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 -> StateT EvalEnv IO ()
useFuel Symbol
f = do
  (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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. (Eq k, 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) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
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 -> EvalST 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
  SymEnv
symEnv' <- (EvalEnv -> SymEnv) -> StateT EvalEnv IO SymEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> SymEnv
evEnv
  ElabFlags
ef <- (EvalEnv -> ElabFlags) -> StateT EvalEnv IO ElabFlags
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> ElabFlags
evElabF
  Expr -> EvalST Expr
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr -> EvalST Expr) -> Expr -> EvalST 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 => 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 -> StateT EvalEnv IO 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. (Eq k, 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 -> StateT EvalEnv IO 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 -> StateT EvalEnv IO Bool
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True