--------------------------------------------------------------------------------
-- | 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 #-}

{-# OPTIONS_GHC -Wno-name-shadowing    #-}

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.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 = 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 = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey
               (\SubcId
i SimpC a
c -> forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aEnv SubcId
i SimpC a
c Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds)
               (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi)
    let t :: CTrie
t  = forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId (SimpC a)
cs)                                          -- 1. BUILD the Trie
    InstRes
res   <- forall a. (Maybe SolverHandle -> IO a) -> IO a
withRESTSolver forall a b. (a -> b) -> a -> b
$ \Maybe SolverHandle
solver -> forall a. Int -> IO a -> IO a
withProgress (Int
1 forall a. Num a => a -> a -> a
+ forall k v. HashMap k v -> Int
M.size HashMap SubcId (SimpC a)
cs) forall a b. (a -> b) -> a -> b
$
               forall a. Config -> [Char] -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
sEnv forall a b. (a -> b) -> a -> b
$ \Context
ctx -> do
                  InstEnv a
env <- forall a.
Loc a =>
Config
-> SInfo a
-> CMap (SimpC a)
-> Maybe SolverHandle
-> Context
-> IO (InstEnv a)
instEnv Config
cfg SInfo a
fi HashMap SubcId (SimpC a)
cs Maybe SolverHandle
solver Context
ctx
                  forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t InstEnv a
env                                             -- 2. TRAVERSE Trie to compute InstRes
    forall a. Config -> SInfo a -> SymEnv -> InstRes -> IO ()
savePLEEqualities Config
cfg SInfo a
fi SymEnv
sEnv InstRes
res
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo Config
cfg SymEnv
sEnv SInfo a
fi 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 | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall k v. HashMap k v -> [v]
M.elems forall a b. (a -> b) -> a -> b
$ AxiomEnv -> HashMap SubcId [AutoRewrite]
aenvAutoRW AxiomEnv
aEnv) = Maybe SolverHandle -> IO a
f forall a. Maybe a
Nothing
    withRESTSolver Maybe SolverHandle -> IO a
f = forall (m :: * -> *) b. MonadIO m => (SolverHandle -> m b) -> m b
withZ3 (Maybe SolverHandle -> IO a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just)

    file :: [Char]
file   = Config -> [Char]
srcFile Config
cfg forall a. [a] -> [a] -> [a]
++ [Char]
".evals"
    sEnv :: SymEnv
sEnv   = forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi
    aEnv :: AxiomEnv
aEnv   = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
    fi :: SInfo a
fi     = 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
fi SymEnv
sEnv InstRes
res = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
save Config
cfg) forall a b. (a -> b) -> a -> b
$ do
    let fq :: [Char]
fq   = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg forall a. [a] -> [a] -> [a]
++ [Char]
".ple"
    [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"\nSaving PLE equalities: "   forall a. [a] -> [a] -> [a]
++ [Char]
fq forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
    [Char] -> IO ()
Misc.ensurePath [Char]
fq
    let constraint_equalities :: [(SubcId, [Expr])]
constraint_equalities =
          forall a b. (a -> b) -> [a] -> [b]
map forall {c :: * -> *} {a} {a}.
TaggedC c a =>
(a, c a) -> (a, [Expr])
equalitiesPerConstraint forall a b. (a -> b) -> a -> b
$ forall a b. Ord a => HashMap a b -> [(a, b)]
Misc.hashMapToAscList forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi
    [Char] -> [Char] -> IO ()
writeFile [Char]
fq forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map 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, forall a. Ord a => [a] -> [a]
L.sort [ Expr
e | Int
i <- IBindEnv -> [Int]
elemsIBindEnv (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv c a
c), Just Expr
e <- [forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i InstRes
res] ])
    renderConstraintRewrite :: (a, t Expr) -> Doc
renderConstraintRewrite (a
cid, t Expr
eqs) =
      Doc
"constraint id" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (forall a. Show a => a -> [Char]
show a
cid forall a. [a] -> [a] -> [a]
++ [Char]
":")
      Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2
           ([Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
L.intersperse Doc
"" forall a b. (a -> b) -> a -> b
$
            forall a b. (a -> b) -> [a] -> [b]
map (forall a. Fixpoint a => a -> Doc
toFix forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
unElab) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList 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
            forall a b. (a -> b) -> [a] -> [b]
map (Located [Char] -> SymEnv -> Expr -> Expr
elabExpr Located [Char]
"savePLEEqualities" SymEnv
sEnv) forall a b. (a -> b) -> a -> b
$
            forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
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
fi CMap (SimpC a)
cs Maybe SolverHandle
restSolver Context
ctx = do
    IORef (HashMap (OCType, OCType) Bool)
refRESTCache <- forall a. a -> IO (IORef a)
newIORef forall a. Monoid a => a
mempty
    IORef (HashMap OCType Bool)
refRESTSatCache <- forall a. a -> IO (IORef a)
newIORef forall a. Monoid a => a
mempty
    let
        restOC :: RESTOrdering
restOC = Config -> RESTOrdering
FC.restOC Config
cfg
        oc0 :: OCAlgebra OCType RuntimeTerm IO
oc0 = RESTOrdering -> SolverHandle -> OCAlgebra OCType RuntimeTerm IO
ordConstraints RESTOrdering
restOC forall a b. (a -> b) -> a -> b
$ 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
             { isSat :: OCType -> IO Bool
OC.isSat = forall {c} {a}.
Hashable c =>
IORef (HashMap c Bool) -> OCAlgebra c a IO -> c -> IO Bool
cachedIsSat IORef (HashMap OCType Bool)
refRESTSatCache OCAlgebra OCType RuntimeTerm IO
oc0
             , notStrongerThan :: OCType -> OCType -> IO Bool
OC.notStrongerThan = forall {c} {a}.
Hashable c =>
IORef (HashMap (c, c) Bool)
-> OCAlgebra c a IO -> c -> c -> IO Bool
cachedNotStrongerThan IORef (HashMap (OCType, OCType) Bool)
refRESTCache OCAlgebra OCType RuntimeTerm IO
oc0
             }
        et :: ExploredTerms RuntimeTerm OCType IO
        et :: ExploredTerms RuntimeTerm OCType IO
et = forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ExploredTerms.empty
               EF
                 { union :: OCType -> OCType -> OCType
ExploredTerms.union = 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 = 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 = 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
              , evPendingUnfoldings :: HashMap Expr Expr
evPendingUnfoldings = forall a. Monoid a => a
mempty
              , evNewEqualities :: EvEqualities
evNewEqualities = forall a. Monoid a => a
mempty
              , evSMTCache :: HashMap Expr Bool
evSMTCache = forall a. Monoid a => a
mempty
              , evFuel :: FuelCount
evFuel = Config -> FuelCount
defFuelCount Config
cfg
              , explored :: Maybe (ExploredTerms RuntimeTerm OCType IO)
explored = forall a. a -> Maybe a
Just ExploredTerms RuntimeTerm OCType IO
et
              , restSolver :: Maybe SolverHandle
restSolver = Maybe SolverHandle
restSolver
              , restOCA :: RESTOrdering
restOCA = RESTOrdering
restOC
              , evOCAlgebra :: OCAlgebra OCType RuntimeTerm IO
evOCAlgebra = OCAlgebra OCType RuntimeTerm IO
oc
              }
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ InstEnv
       { ieCfg :: Config
ieCfg = Config
cfg
       , ieSMT :: Context
ieSMT = Context
ctx
       , ieBEnv :: BindEnv a
ieBEnv = forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi
       , ieAenv :: AxiomEnv
ieAenv = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
       , ieCstrs :: CMap (SimpC a)
ieCstrs = CMap (SimpC a)
cs
       , ieKnowl :: Knowledge
ieKnowl = forall a. Config -> Context -> SInfo a -> Knowledge
knowledge Config
cfg Context
ctx SInfo a
fi
       , ieEvEnv :: EvalEnv
ieEvEnv = EvalEnv
s0
       }
  where
    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 <- forall a. IORef a -> IO a
readIORef IORef (HashMap (c, c) Bool)
refRESTCache
      case 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 <- forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra c a IO
oc c
a c
b
          forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap (c, c) Bool)
refRESTCache (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)
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
nst
        Just Bool
nst ->
          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 <- forall a. IORef a -> IO a
readIORef IORef (HashMap c Bool)
refRESTSatCache
      case 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 <- forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
OC.isSat OCAlgebra c a IO
oc c
a
          forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap c Bool)
refRESTSatCache (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)
          forall (m :: * -> *) a. Monad m => a -> m a
return Bool
sat
        Just Bool
sat ->
          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  = 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   = forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> [Int]
elemsIBindEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env' ICtx
ctx0 forall {a}. [a]
diff0 forall a. Maybe a
Nothing forall {k} {v}. HashMap k v
res0 CTrie
t
  where
    env' :: InstEnv a
env'         = InstEnv a
env
    diff0 :: [a]
diff0        = []
    res0 :: HashMap k v
res0         = forall {k} {v}. HashMap k v
M.empty
    ctx0 :: ICtx
ctx0         = ICtx
      { icAssms :: HashSet Expr
icAssms  = forall a. Monoid a => a
mempty
      , icCands :: HashSet Expr
icCands  = forall a. Monoid a => a
mempty
      , icEquals :: EvEqualities
icEquals = forall a. Monoid a => a
mempty
      , icSimpl :: HashMap Expr Expr
icSimpl  = forall a. Monoid a => a
mempty
      , icSubcId :: Maybe SubcId
icSubcId = forall a. Maybe a
Nothing
      , icANFs :: [[(Symbol, SortedReft)]]
icANFs   = []
      }

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 []  -> forall (m :: * -> *) a. Monad m => a -> m a
return InstRes
res
  T.Node [Branch SubcId
b] -> 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  -> forall a b.
InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> (InstEnv a -> ICtx -> IO b)
-> IO b
withAssms InstEnv a
env ICtx
ctx [Int]
delta forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \InstEnv a
env' ICtx
ctx' -> do
                  (ICtx
ctx'', InstEnv a
env'', InstRes
res') <- forall a.
InstEnv a
-> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstEnv a, InstRes)
ple1 InstEnv a
env' ICtx
ctx' Maybe Int
i InstRes
res
                  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (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 -> forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx (Int
iforall a. a -> [a] -> [a]
:[Int]
delta) (forall a. a -> Maybe a
Just Int
i) InstRes
res CTrie
t
  T.Val SubcId
cid  -> forall a b.
InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> (InstEnv a -> ICtx -> IO b)
-> IO b
withAssms InstEnv a
env ICtx
ctx [Int]
delta (forall a. a -> Maybe a
Just SubcId
cid) forall a b. (a -> b) -> a -> b
$ \InstEnv a
env' ICtx
ctx' -> do
                  IO ()
progressTick
                  (\(ICtx
_, InstEnv a
_, InstRes
r) -> InstRes
r) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> (InstEnv a -> ICtx -> IO b) -> IO b
withAssms :: forall a b.
InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> (InstEnv a -> ICtx -> IO b)
-> IO b
withAssms env :: InstEnv a
env@InstEnv{CMap (SimpC a)
Config
BindEnv a
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
..} ICtx
ctx [Int]
delta Maybe SubcId
cidMb InstEnv a -> ICtx -> IO b
act = do
  let (ICtx
ctx', InstEnv a
env')  = forall a.
InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> (ICtx, InstEnv a)
updCtx InstEnv a
env ICtx
ctx [Int]
delta Maybe SubcId
cidMb
  let assms :: HashSet Expr
assms = ICtx -> HashSet Expr
icAssms ICtx
ctx'
  forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ieSMT  [Char]
"PLE.evaluate" forall a b. (a -> b) -> a -> b
$ do
    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)
    InstEnv a -> ICtx -> IO b
act InstEnv a
env' ICtx
ctx' { icAssms :: HashSet Expr
icAssms = forall a. Monoid a => a
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
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
..} ICtx
ctx Maybe Int
i InstRes
res = do
  (ICtx
ctx', EvalEnv
env) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Config -> ICtx -> Context -> Knowledge -> EvalST ICtx
evalCandsLoop Config
ieCfg ICtx
ctx Context
ieSMT Knowledge
ieKnowl) EvalEnv
ieEvEnv
  let pendings :: [(Expr, Expr)]
pendings = forall {a}. EvalEnv -> Maybe a -> [(Expr, Expr)]
collectPendingUnfoldings EvalEnv
env (ICtx -> Maybe SubcId
icSubcId ICtx
ctx)
      newEqs :: [(Expr, Expr)]
newEqs = [(Expr, Expr)]
pendings forall a. [a] -> [a] -> [a]
++ forall a. HashSet a -> [a]
S.toList (forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference (ICtx -> EvEqualities
icEquals ICtx
ctx') (ICtx -> EvEqualities
icEquals ICtx
ctx))
  forall (m :: * -> *) a. Monad m => a -> m a
return (ICtx
ctx', InstEnv a
ie { ieEvEnv :: EvalEnv
ieEvEnv = EvalEnv
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 =
      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:" forall a. [a] -> [a] -> [a]
++ [Char]
msg) Config
cfg Context
ctx [] (Expr -> Expr -> Expr
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 -> EvalST ICtx
evalCandsLoop Config
cfg ICtx
ictx0 Context
ctx Knowledge
γ = ICtx -> Int -> EvalST ICtx
go ICtx
ictx0 Int
0
  where
    go :: ICtx -> Int -> EvalST ICtx
go ICtx
ictx Int
_ | forall a. HashSet a -> Bool
S.null (ICtx -> HashSet Expr
icCands ICtx
ictx) = 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 forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
        else do
                  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Context -> Expr -> IO ()
SMT.smtAssert Context
ctx ([Expr] -> Expr
pAndNoDedup (forall a. HashSet a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ ICtx -> HashSet Expr
icAssms ICtx
ictx))
                  let ictx' :: ICtx
ictx' = ICtx
ictx { icAssms :: HashSet Expr
icAssms = forall a. Monoid a => a
mempty }
                      cands :: [Expr]
cands = forall a. HashSet a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ ICtx -> HashSet Expr
icCands ICtx
ictx
                  [[Expr]]
candss <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> ICtx -> Int -> Expr -> EvalST [Expr]
evalOne Knowledge
γ ICtx
ictx' Int
i) [Expr]
cands
                  EvEqualities
us <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
                  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { evNewEqualities :: EvEqualities
evNewEqualities = forall a. Monoid a => a
mempty }
                  let noCandidateChanged :: Bool
noCandidateChanged = forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {a}. Eq a => [a] -> a -> Bool
eqCand [[Expr]]
candss [Expr]
cands)
                      unknownEqs :: EvEqualities
unknownEqs = EvEqualities
us forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` ICtx -> EvEqualities
icEquals ICtx
ictx
                  if forall a. HashSet a -> Bool
S.null EvEqualities
unknownEqs Bool -> Bool -> Bool
&& Bool
noCandidateChanged
                        then 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 forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvEqualities
unknownEqs
                                 let ictx'' :: ICtx
ictx''   = ICtx
ictx' { icEquals :: EvEqualities
icEquals = ICtx -> EvEqualities
icEquals ICtx
ictx forall a. Semigroup a => a -> a -> a
<> EvEqualities
unknownEqs
                                                      , icAssms :: HashSet Expr
icAssms  = forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isTautoPred) HashSet Expr
eqsSMT }
                                 ICtx -> Int -> EvalST ICtx
go (ICtx
ictx'' { icCands :: HashSet Expr
icCands = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Expr]]
candss) }) (Int
i forall a. Num a => a -> a -> a
+ Int
1)

    testForInconsistentEnvironment :: StateT EvalEnv IO Bool
testForInconsistentEnvironment =
      forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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
PFalse

    eqCand :: [a] -> a -> Bool
eqCand [a
e0] a
e1 = a
e0 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
fi InstRes
res = forall a. SInfo a -> InstRes -> SInfo a
strengthenBinds SInfo a
fi InstRes
res'
  where
    res' :: InstRes
res'     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
is [Expr]
ps''
    ps'' :: [Expr]
ps''     = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i -> forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate (forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan ([Char]
"PLE1 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i)) SymEnv
env) [Int]
is [Expr]
ps'
    ps' :: [Expr]
ps'      = forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env [Expr]
ps
    ([Int]
is, [Expr]
ps) = forall a b. [(a, b)] -> ([a], [b])
unzip (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
  }

----------------------------------------------------------------------------------------------
-- | @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
  }

----------------------------------------------------------------------------------------------
-- | @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
EEq Expr
e1 Expr
e2 | (Expr
e1, Expr
e2) <- [(Expr, Expr)]
eqs, Expr
e1 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
pAndNoDedup 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 = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith (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, InstEnv a)
updCtx :: forall a.
InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> (ICtx, InstEnv a)
updCtx env :: InstEnv a
env@InstEnv{CMap (SimpC a)
Config
BindEnv a
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
..} ICtx
ctx [Int]
delta Maybe SubcId
cidMb
            = ( ICtx
ctx { icAssms :: HashSet Expr
icAssms  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isTautoPred) [Expr]
ctxEqs)
                    , icCands :: HashSet Expr
icCands  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Expr]
cands           forall a. Semigroup a => a -> a -> a
<> ICtx -> HashSet Expr
icCands  ICtx
ctx
                    , icSimpl :: HashMap Expr Expr
icSimpl  = ICtx -> HashMap Expr Expr
icSimpl ICtx
ctx forall a. Semigroup a => a -> a -> a
<> HashMap Expr Expr
econsts
                    , icSubcId :: Maybe SubcId
icSubcId = Maybe SubcId
cidMb
                    , icANFs :: [[(Symbol, SortedReft)]]
icANFs   = [(Symbol, SortedReft)]
bs forall a. a -> [a] -> [a]
: ICtx -> [[(Symbol, SortedReft)]]
icANFs ICtx
ctx
                    }
              , InstEnv a
env
              )
  where
    cands :: [Expr]
cands     = Expr
rhsforall a. a -> [a] -> [a]
:[Expr]
es
    econsts :: HashMap Expr Expr
econsts   = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList 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 [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eq a => [a] -> [a]
L.nub
                  [ Expr
c | (Symbol, SortedReft)
xr <- [(Symbol, SortedReft)]
bs, Expr
c <- Expr -> [Expr]
conjuncts (forall a. Expression a => a -> Expr
expr (Symbol, SortedReft)
xr), forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [KVar]
Vis.kvarsExpr Expr
c) ]
    bs :: [(Symbol, SortedReft)]
bs        = forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SortedReft -> SortedReft
unApplySortedReft 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        = forall a. Expression a => a -> Expr
expr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
bs
    eRhs :: Expr
eRhs      = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
PTrue 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
_) =  forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv a
ieBEnv]
    subMb :: Maybe (SimpC a)
subMb     = forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr CMap (SimpC a)
ieCstrs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SubcId
cidMb


findConstants :: Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants :: Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants Knowledge
γ [Expr]
es = [(Symbol -> Expr
EVar Symbol
x, Expr
c) | (Symbol
x,Expr
c) <- [(Symbol, Expr)] -> [Expr] -> [(Symbol, Expr)]
go [] (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 forall a. Eq a => a -> a -> Bool
== [Expr]
ess'
                  then [(Symbol, Expr)]
su
                  else [(Symbol, Expr)] -> [Expr] -> [(Symbol, Expr)]
go ([(Symbol, Expr)]
su forall a. [a] -> [a] -> [a]
++ [(Symbol, Expr)]
su') [Expr]
ess'
       where ess' :: [Expr]
ess' = forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol, Expr)]
su') 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
EVar Symbol
x 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 = 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
sid SimpC a
c = forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c Bool -> Bool -> Bool
&& forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Bool
False SubcId
sid (AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
aenv)

type EvEqualities = S.HashSet (Expr, Expr)

--------------------------------------------------------------------------------
data EvalEnv = EvalEnv
  { EvalEnv -> SymEnv
evEnv      :: !SymEnv
    -- | 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

  -- 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 -> ShowS
[FuelCount] -> ShowS
FuelCount -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [FuelCount] -> ShowS
$cshowList :: [FuelCount] -> ShowS
show :: FuelCount -> [Char]
$cshow :: FuelCount -> [Char]
showsPrec :: Int -> FuelCount -> ShowS
$cshowsPrec :: Int -> FuelCount -> ShowS
Show)

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

type EvalST a = StateT EvalEnv IO a
--------------------------------------------------------------------------------

getAutoRws :: Knowledge -> ICtx -> [AutoRewrite]
getAutoRws :: Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx =
  forall a. a -> Maybe a -> a
Mb.fromMaybe [] forall a b. (a -> b) -> a -> b
$ do
    SubcId
cid <- ICtx -> Maybe SubcId
icSubcId ICtx
ctx
    forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SubcId
cid 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 -> EvalST [Expr]
evalOne Knowledge
γ ICtx
ctx Int
i Expr
e
  | Int
i forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx) = (forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
NoRW Expr
e
evalOne Knowledge
γ ICtx
ctx Int
_ Expr
e = do
    EvalEnv
env <- 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 = forall oc.
OCAlgebra oc Expr IO -> [(Expr, TermOrigin)] -> oc -> RESTParams oc
RP (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 = forall c a (m :: * -> *). OCAlgebra c a m -> c
OC.top OCAlgebra OCType RuntimeTerm IO
oc
        emptyET :: ExploredTerms RuntimeTerm OCType IO
emptyET = forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ExploredTerms.empty (forall term c (m :: * -> *).
(c -> c -> c)
-> (c -> c -> m Bool)
-> (c -> term -> term -> c)
-> ExploreFuncs term c m
EF (forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
OC.union OCAlgebra OCType RuntimeTerm IO
oc) (forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra OCType RuntimeTerm IO
oc) (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 -> EvalST [Expr]
evalREST Knowledge
γ ICtx
ctx RESTParams OCType
rp
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { explored :: Maybe (ExploredTerms RuntimeTerm OCType IO)
explored = forall a. a -> Maybe a
Just ExploredTerms RuntimeTerm OCType IO
emptyET }
    forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
es

-- 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EvalType -> EvalType -> Bool
$c/= :: EvalType -> EvalType -> Bool
== :: EvalType -> EvalType -> Bool
$c== :: 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 -> ShowS
[FinalExpand] -> ShowS
FinalExpand -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [FinalExpand] -> ShowS
$cshowList :: [FinalExpand] -> ShowS
show :: FinalExpand -> [Char]
$cshow :: FinalExpand -> [Char]
showsPrec :: Int -> FinalExpand -> ShowS
$cshowsPrec :: Int -> FinalExpand -> ShowS
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 forall a b. (a -> b) -> a -> b
$ 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 = (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Expr, FinalExpand)]
xs, [FinalExpand] -> FinalExpand
feAny (forall a b. (a -> b) -> [a] -> [b]
map 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 -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et = Expr -> EvalST (Expr, FinalExpand)
go
  where
    go :: Expr -> EvalST (Expr, FinalExpand)
go (ELam (Symbol
x,Sort
s) Expr
e)   = Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> EvalST (Expr, FinalExpand)
evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
x, Sort
s) Expr
e
    go e :: Expr
e@EIte{}         = Knowledge -> ICtx -> EvalType -> Expr -> EvalST (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
ECoerc Sort
s Sort
t)  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST (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 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
fe) <- [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et) [Expr]
es
            if [Expr]
es forall a. Eq a => a -> a -> Bool
/= [Expr]
es'
              then forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Expr] -> Expr
eApps Expr
f [Expr]
es', FinalExpand
fe)
              else do
                (Expr
f', FinalExpand
fe)  <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et 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
                forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a -> a
Mb.fromMaybe (Expr -> [Expr] -> Expr
eApps Expr
f' [Expr]
es') Maybe Expr
me', FinalExpand
fe FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe')
       (Expr
f, [Expr]
es) ->
          do
            (Expr
f':[Expr]
es', FinalExpand
fe) <- [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et) (Expr
fforall a. a -> [a] -> [a]
:[Expr]
es)
            (Maybe Expr
me', FinalExpand
fe') <- Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> EvalST (Maybe Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx Expr
f' [Expr]
es' EvalType
et
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a -> a
Mb.fromMaybe (Expr -> [Expr] -> Expr
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 -> EvalST (Expr, FinalExpand)
binOp (Brel -> Expr -> Expr -> Expr
PAtom Brel
r) Expr
e1 Expr
e2
    go (ENeg Expr
e)         = do (Expr
e', FinalExpand
fe)  <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
e
                             forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
ENeg Expr
e', FinalExpand
fe)
    go (EBin Bop
o Expr
e1 Expr
e2)   = do (Expr
e1', FinalExpand
fe1) <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
e1
                             (Expr
e2', FinalExpand
fe2) <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
e2
                             forall (m :: * -> *) a. Monad m => a -> m a
return (Bop -> Expr -> Expr -> Expr
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
`ETApp` Sort
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST (Expr, FinalExpand)
go Expr
e
    go (ETAbs Expr
e Symbol
s)      = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE (Expr -> Symbol -> Expr
`ETAbs` Symbol
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST (Expr, FinalExpand)
go Expr
e
    go (PNot Expr
e')        = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE Expr -> Expr
PNot forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST (Expr, FinalExpand)
go Expr
e'
    go (PImp Expr
e1 Expr
e2)     = (Expr -> Expr -> Expr)
-> Expr -> Expr -> EvalST (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
PImp Expr
e1 Expr
e2
    go (PIff Expr
e1 Expr
e2)     = (Expr -> Expr -> Expr)
-> Expr -> Expr -> EvalST (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
PIff Expr
e1 Expr
e2
    go (PAnd [Expr]
es)        = forall {m :: * -> *} {a}.
Monad m =>
([Expr] -> a) -> m [(Expr, FinalExpand)] -> m (a, FinalExpand)
efAll [Expr] -> Expr
PAnd (Expr -> EvalST (Expr, FinalExpand)
go forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
es)
    go (POr [Expr]
es)         = forall {m :: * -> *} {a}.
Monad m =>
([Expr] -> a) -> m [(Expr, FinalExpand)] -> m (a, FinalExpand)
efAll [Expr] -> Expr
POr (Expr -> EvalST (Expr, FinalExpand)
go forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (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) <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
e
                             forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Sort -> Expr
ECst Expr
e' Sort
t, FinalExpand
fe)
    go Expr
e                = forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, FinalExpand
noExpand)

    binOp :: (Expr -> Expr -> Expr)
-> Expr -> Expr -> EvalST (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
f Expr
e1 Expr
e2 = do
      (Expr
e1', FinalExpand
fe1) <- Expr -> EvalST (Expr, FinalExpand)
go Expr
e1
      (Expr
e2', FinalExpand
fe2) <- Expr -> EvalST (Expr, FinalExpand)
go Expr
e2
      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
      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
-> EvalST (Expr, FinalExpand)
evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
x, Sort
s) Expr
e = do
    HashMap Expr Expr
oldPendingUnfoldings <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> HashMap Expr Expr
evPendingUnfoldings
    EvEqualities
oldEqs <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
    (Expr
e', FinalExpand
fe) <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval (Knowledge
γ { knLams :: [(Symbol, Sort)]
knLams = (Symbol
x, Sort
s) forall a. a -> [a] -> [a]
: Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ }) 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
ELam (Symbol
x, Sort
s) Expr
e
    -- Discard the old equalities which miss the lambda binding
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
      { evPendingUnfoldings :: HashMap Expr Expr
evPendingUnfoldings = HashMap Expr Expr
oldPendingUnfoldings
      , evNewEqualities :: EvEqualities
evNewEqualities = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Expr
elam, (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
s) Expr
e2') EvEqualities
oldEqs
      }
    forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
elam, 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
  }

-- Reverse the ANF transformation
deANF :: ICtx -> Expr -> Expr
deANF :: ICtx -> Expr -> Expr
deANF ICtx
ctx = (Symbol -> Maybe SortedReft) -> Expr -> Expr
inlineInExpr (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
`HashMap.Lazy.lookup` forall v.
Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANF forall a. a -> a
id HashMap Symbol SortedReft
bindEnv)
  where
    bindEnv :: HashMap Symbol SortedReft
bindEnv = forall k v. (Eq k, Hashable k) => [HashMap k v] -> HashMap k v
HashMap.Lazy.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.Lazy.fromList forall a b. (a -> b) -> a -> b
$ ICtx -> [[(Symbol, SortedReft)]]
icANFs ICtx
ctx

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

evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
γ ICtx
ctx [Expr]
acc RESTParams OCType
rp =
  do
    Just ExploredTerms RuntimeTerm OCType IO
exploredTerms <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> Maybe (ExploredTerms RuntimeTerm OCType IO)
explored
    Bool
se <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (forall {m :: * -> *}.
Monad m =>
ExploredTerms RuntimeTerm OCType m -> Expr -> m Bool
shouldExploreTerm ExploredTerms RuntimeTerm OCType IO
exploredTerms Expr
e)
    if Bool
se then do
      [((Expr, Expr), Expr, OCType)]
possibleRWs <- StateT EvalEnv IO [((Expr, Expr), Expr, OCType)]
getRWs
      [((Expr, Expr), Expr, OCType)]
rws <- forall {c} {m :: * -> *} {a} {c}.
ExploredTerms RuntimeTerm c m -> [(a, Expr, c)] -> [(a, Expr, c)]
notVisitedFirst ExploredTerms RuntimeTerm OCType IO
exploredTerms forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. (a, Expr, OCType) -> IO Bool
allowed) [((Expr, Expr), Expr, OCType)]
possibleRWs
      EvEqualities
oldEqualities <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { evNewEqualities :: EvEqualities
evNewEqualities = forall a. Monoid a => a
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 -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
FuncNormal Expr
e
        if Expr
ec forall a. Eq a => a -> a -> Bool
/= Expr
e
          then forall (m :: * -> *) a. Monad m => a -> m a
return (Expr, FinalExpand)
r
          else Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
RWNormal Expr
e

      let evalIsNewExpr :: Bool
evalIsNewExpr = Expr
e' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.notElem` [Expr]
pathExprs
      let exprsToAdd :: [Expr]
exprsToAdd    = [Expr
e' | Bool
evalIsNewExpr]  forall a. [a] -> [a] -> [a]
++ 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 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 ]

      EvEqualities
newEqualities <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
      HashMap Expr Bool
smtCache <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (HashMap Expr Bool)
cacheRef
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st ->
             EvalEnv
st { evNewEqualities :: EvEqualities
evNewEqualities  = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union EvEqualities
newEqualities EvEqualities
oldEqualities) [(Expr, Expr)]
eqnToAdd
                , evSMTCache :: HashMap Expr Bool
evSMTCache = HashMap Expr Bool
smtCache
                , explored :: Maybe (ExploredTerms RuntimeTerm OCType IO)
explored = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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
e)
                  (forall oc. RESTParams oc -> oc
c RESTParams OCType
rp)
                  (forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Expr -> RuntimeTerm
Rewrite.convert Expr
e') forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map (Expr -> RuntimeTerm
Rewrite.convert forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\((Expr, Expr)
_, Expr
e, OCType
_) -> Expr
e)) [((Expr, Expr), Expr, OCType)]
possibleRWs))
                  (forall a. HasCallStack => Maybe a -> a
Mb.fromJust forall a b. (a -> b) -> a -> b
$ EvalEnv -> Maybe (ExploredTerms RuntimeTerm OCType IO)
explored EvalEnv
st)
                })

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

      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
-> EvalST [Expr]
evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
γ ICtx
ctx [Expr]
r (forall {a}. (a, Expr, OCType) -> RESTParams OCType
rpRW ((Expr, Expr), Expr, OCType)
rw)) [Expr]
acc'' [((Expr, Expr), Expr, OCType)]
rws
     else
      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 ->
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ 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  ->
          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) (forall oc. RESTParams oc -> oc
c RESTParams OCType
rp) ExploredTerms RuntimeTerm OCType m
exploredTerms
    shouldExploreTerm ExploredTerms RuntimeTerm OCType m
_ Expr
_ = forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

    allowed :: (a, Expr, OCType) -> IO Bool
allowed (a
_, Expr
rwE, OCType
_) | Expr
rwE forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
pathExprs = 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 = forall oc a. OCAlgebra oc a IO -> RewriteArgs -> oc -> IO Bool
Rewrite.passesTerminationCheck (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) = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (\(a
_, Expr
e, c
_) -> 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 forall a. [a] -> [a] -> [a]
++ [(a, Expr, c)]
v

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

      in
        RESTParams OCType
rp{path :: [(Expr, TermOrigin)]
path = forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp forall a. [a] -> [a] -> [a]
++ [(Expr
e', TermOrigin
PLE)], c :: OCType
c = OCType
c'}

    isRW :: (a, TermOrigin) -> Bool
isRW (a
_, TermOrigin
r) = TermOrigin
r 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 :: [(Expr, TermOrigin)]
path = forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp forall a. [a] -> [a] -> [a]
++ [(Expr
e', TermOrigin
RW)], c :: OCType
c = OCType
c' }

    pathExprs :: [Expr]
pathExprs       = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"EVAL2: path" forall a b. (a -> b) -> a -> b
$ forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
    e :: Expr
e               = forall a. [a] -> a
last [Expr]
pathExprs
    autorws :: [AutoRewrite]
autorws         = Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ 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
γ) 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 forall {a}. (a, TermOrigin) -> Bool
isRW forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last (forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
            then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
            else forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ OCType -> IO Bool
termCheck (forall oc. RESTParams oc -> oc
c RESTParams OCType
rp)
        if Bool
ok
          then
            do
              let e' :: Expr
e'         = ICtx -> Expr -> Expr
deANF ICtx
ctx Expr
e
              let getRW :: SubExpr -> AutoRewrite -> MaybeT IO ((Expr, Expr), Expr, OCType)
getRW SubExpr
e AutoRewrite
ar = forall oc.
OCAlgebra oc Expr IO
-> RewriteArgs
-> oc
-> SubExpr
-> AutoRewrite
-> MaybeT IO ((Expr, Expr), Expr, oc)
Rewrite.getRewrite (forall oc. RESTParams oc -> OCAlgebra oc Expr IO
oc RESTParams OCType
rp) RewriteArgs
rwArgs (forall oc. RESTParams oc -> oc
c RESTParams OCType
rp) SubExpr
e AutoRewrite
ar
              let getRWs' :: SubExpr -> f [((Expr, Expr), Expr, OCType)]
getRWs' SubExpr
s  = forall a. [Maybe a] -> [a]
Mb.catMaybes forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpr -> AutoRewrite -> MaybeT IO ((Expr, Expr), Expr, OCType)
getRW SubExpr
s) [AutoRewrite]
autorws
              forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {f :: * -> *}.
MonadIO f =>
SubExpr -> f [((Expr, Expr), Expr, OCType)]
getRWs' (Expr -> [SubExpr]
subExprs Expr
e')
          else 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 :: HashMap Expr Expr
icSimpl = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Expr
e Expr
e' forall a b. (a -> b) -> a -> b
$ ICtx -> HashMap Expr Expr
icSimpl ICtx
ctx} else ICtx
ctx

-- | @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 <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
f (Knowledge -> Map Symbol Equation
knAms Knowledge
γ)
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq) forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  = do
       SEnv Sort
env  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort 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 forall a. Eq a => a -> a -> Bool
/= EvalType
FuncNormal
         then do
                let ([Expr]
es1,[Expr]
es2) = forall a. Int -> [a] -> ([a], [a])
splitAt (forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)) [Expr]
es
                    newE :: Expr
newE = SEnv Sort -> Equation -> [Expr] -> Expr
substEq SEnv Sort
env Equation
eq [Expr]
es1
                (Expr
e', FinalExpand
fe) <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (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'
                    e3' :: Expr
e3' = Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx (Expr -> [Expr] -> Expr
eApps Expr
e2' [Expr]
es2) -- reduces a bit the equations
                    undecidedGuards :: Bool
undecidedGuards = case Expr
e' of
                      EIte{} -> Bool
True
                      Expr
_ -> Bool
False

                if Bool
undecidedGuards
                  then do
                    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
                      EvalEnv
st {
                        evPendingUnfoldings :: HashMap Expr Expr
evPendingUnfoldings = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (Expr -> [Expr] -> Expr
eApps Expr
e0 [Expr]
es) Expr
e3' (EvalEnv -> HashMap Expr Expr
evPendingUnfoldings EvalEnv
st)
                      }
                    -- Don't unfold the expression if there is an if-then-else
                    -- guarding it, just to preserve the size of further
                    -- rewrites.
                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, FinalExpand
noExpand)
                  else do
                    Symbol -> StateT EvalEnv IO ()
useFuel Symbol
f
                    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
                      EvalEnv
st
                        { evNewEqualities :: EvEqualities
evNewEqualities = forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Expr -> [Expr] -> Expr
eApps Expr
e0 [Expr]
es, Expr
e3') (EvalEnv -> EvEqualities
evNewEqualities EvalEnv
st)
                        , evPendingUnfoldings :: HashMap Expr Expr
evPendingUnfoldings = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (Expr -> [Expr] -> Expr
eApps Expr
e0 [Expr]
es) (EvalEnv -> HashMap Expr Expr
evPendingUnfoldings EvalEnv
st)
                        }
                    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Expr
e2', FinalExpand
fe)
         else forall (m :: * -> *) a. Monad m => a -> m a
return (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 forall a. Eq a => a -> a -> Bool
== Symbol
"Language.Haskell.Liquid.ProofCombinators.pleUnfold"
      = Expr
arg
      | Bool
otherwise = Expr
e

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 <- 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) <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\(Rewrite
rw, IsUserDataSMeasure
_) -> Rewrite -> Symbol
smName Rewrite
rw forall a. Eq a => a -> a -> Bool
== Symbol
f) [(Rewrite, IsUserDataSMeasure)]
rws
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
as forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
  = do
    let newE :: Expr
newE = Expr -> [Expr] -> Expr
eApps (forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
rw) [Expr]
as) (Rewrite -> Expr
smBody Rewrite
rw)) [Expr]
es
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (IsUserDataSMeasure
isUserDataSMeasure forall a. Eq a => a -> a -> Bool
== IsUserDataSMeasure
NoUserDataSMeasure) forall a b. (a -> b) -> a -> b
$
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
        EvalEnv
st { evNewEqualities :: EvEqualities
evNewEqualities =
               forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Expr -> [Expr] -> Expr
eApps Expr
e0 [Expr]
args, Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx Expr
newE) (EvalEnv -> EvEqualities
evNewEqualities EvalEnv
st)
           }
    forall (m :: * -> *) a. Monad m => a -> m a
return (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
eApps Expr
e0 [Expr]
es)
  = do
       let eqs' :: [(Expr, Expr)]
eqs' = forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second forall a b. (a -> b) -> a -> b
$ Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx) [(Expr, Expr)]
eqs
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
         EvalEnv
st { evNewEqualities :: EvEqualities
evNewEqualities = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (EvalEnv -> EvEqualities
evNewEqualities EvalEnv
st) [(Expr, Expr)]
eqs' }
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, FinalExpand
noExpand)

evalApp Knowledge
_ ICtx
_ Expr
_e [Expr]
_es EvalType
_
  = forall (m :: * -> *) a. Monad m => a -> m a
return (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 -> EvalST (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et (EIte Expr
i Expr
e1 Expr
e2) = do
      (Expr
b, FinalExpand
_) <- Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
i
      Maybe Bool
b'  <- forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalEIt POS " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (Expr
i, Expr
b)) 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 -> EvalST (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e1
        Just Bool
False -> Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e2
        Maybe Bool
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2, FinalExpand
expand)
evalIte Knowledge
_ ICtx
_ EvalType
_ Expr
e' = 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
EApp (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) Expr
e, forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ 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 <- [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
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es forall a. Eq a => a -> a -> Bool
== 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 = 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 forall a b. (a -> b) -> a -> b
$ 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 = CoSub -> Expr -> Expr
Vis.applyCoSub CoSub
coSub forall a b. (a -> b) -> a -> b
$ Equation -> Expr
eqBody Equation
eq
  where
    ts :: [Sort]
ts    = forall a b. (a, b) -> b
snd    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Equation -> [(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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    coSub :: CoSub
coSub = SEnv Sort -> [Sort] -> [Sort] -> CoSub
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.CoSub
mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> CoSub
mkCoSub SEnv Sort
env [Sort]
eTs [Sort]
xTs = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x, [Sort] -> Sort
unite [Sort]
ys) | (Symbol
x, [Sort]
ys) <- forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, Sort)]
xys ]
  where
    unite :: [Sort] -> Sort
unite [Sort]
ts    = forall a. a -> Maybe a -> a
Mb.fromMaybe (forall {a} {a}. PPrint a => a -> a
uError [Sort]
ts) (Env -> [Sort] -> Maybe Sort
unifyTo1 Env
senv [Sort]
ts)
    senv :: Env
senv        = forall a. SEnv a -> Symbol -> SESearch a
mkSearchEnv SEnv Sort
env
    uError :: a -> a
uError a
ts   = forall a. [Char] -> a
panic ([Char]
"mkCoSub: cannot build CoSub for " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp [(Symbol, Sort)]
xys forall a. [a] -> [a] -> [a]
++ [Char]
" cannot unify " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp a
ts)
    xys :: [(Symbol, Sort)]
xys         = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Sort -> Sort -> [(Symbol, Sort)]
matchSorts [Sort]
xTs [Sort]
eTs

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

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

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

isValidCached :: Knowledge -> Expr -> EvalST (Maybe Bool)
isValidCached :: Knowledge -> Expr -> StateT EvalEnv IO (Maybe Bool)
isValidCached Knowledge
γ Expr
e = do
  EvalEnv
env <- forall s (m :: * -> *). MonadState s m => m s
get
  case 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 (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
s (Expr -> HashSet Symbol
exprSymbolsSet Expr
e))
      Bool
b <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {b}. (Symbol, b) -> Bool
isFreeInE (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ)) forall a b. (a -> b) -> a -> b
$
            forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalEnv
env { evSMTCache :: HashMap Expr Bool
evSMTCache = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Expr
e Bool
True (EvalEnv -> HashMap Expr Bool
evSMTCache EvalEnv
env) })
          forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
True)
        else do
          Bool
b2 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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
PNot Expr
e)
          if Bool
b2
            then do
              forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall {b}. (Symbol, b) -> Bool
isFreeInE (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ)) forall a b. (a -> b) -> a -> b
$
                forall s (m :: * -> *). MonadState s m => s -> m ()
put (EvalEnv
env { evSMTCache :: HashMap Expr Bool
evSMTCache = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Expr
e Bool
False (EvalEnv -> HashMap Expr Bool
evSMTCache EvalEnv
env) })
              forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just Bool
False)
            else
              forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

    Maybe Bool
mb -> 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
$c/= :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
== :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
$c== :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
Eq, Int -> IsUserDataSMeasure -> ShowS
[IsUserDataSMeasure] -> ShowS
IsUserDataSMeasure -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [IsUserDataSMeasure] -> ShowS
$cshowList :: [IsUserDataSMeasure] -> ShowS
show :: IsUserDataSMeasure -> [Char]
$cshow :: IsUserDataSMeasure -> [Char]
showsPrec :: Int -> IsUserDataSMeasure -> ShowS
$cshowsPrec :: Int -> IsUserDataSMeasure -> ShowS
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 <- forall a. IORef a -> IO a
readIORef IORef (HashMap Expr Bool)
cacheRef
    case 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
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b forall a b. (a -> b) -> a -> b
$
          forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap Expr Bool)
cacheRef (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)
        forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b
      Maybe Bool
mb -> forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Bool
mb forall a. Eq a => a -> a -> 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                     = forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. [a] -> [a] -> [a]
(++) forall a b. (a -> b) -> a -> b
$
                                   [ (Rewrite -> Symbol
smDC Rewrite
rw, [(Rewrite
rw, IsUserDataSMeasure
NoUserDataSMeasure)]) | Rewrite
rw <- [Rewrite]
sims ] forall a. [a] -> [a] -> [a]
++
                                   [ (Rewrite -> Symbol
smDC Rewrite
rw, [(Rewrite
rw, IsUserDataSMeasure
UserDataSMeasure)]) | Rewrite
rw <- [Rewrite]
dataSims ]
  , knAms :: Map Symbol Equation
knAms                      = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Equation -> 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)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)
                                 forall a. [a] -> [a] -> [a]
++ ((\Equation
s -> (Equation -> Symbol
eqName Equation
s, forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
s))) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Equation]
aenvEqs AxiomEnv
aenv)
                                 forall a. [a] -> [a] -> [a]
++ [(Symbol, Int)]
rwSyms
  , knDCs :: HashSet Symbol
knDCs                      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (Rewrite -> Symbol
smDC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)
  , knDataCtors :: HashMap Symbol DataCtor
knDataCtors                = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (forall a. Located a -> a
val (DataCtor -> LocSymbol
dcName DataCtor
dc), DataCtor
dc) | DataDecl
dd <- forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si, DataCtor
dc <- DataDecl -> [DataCtor]
ddCtors DataDecl
dd ]
  , knSels :: SelectorMap
knSels                     = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel  [Rewrite]
sims
  , knConsts :: ConstDCMap
knConsts                   = 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 (forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si) forall a b. (a -> b) -> a -> b
$ AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv
    ([Rewrite]
simDCSelectors, [Rewrite]
sims) =
      [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorSelectors (forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si) [Rewrite]
sims0
    dataSims :: [Rewrite]
dataSims = [Rewrite]
simDCTests forall a. [a] -> [a] -> [a]
++ [Rewrite]
simDCSelectors
    aenv :: AxiomEnv
aenv = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
si

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

    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 = forall a. a -> Maybe a
Just Symbol
f
    lhsHead Expr
_ = forall a. Maybe a
Nothing


    rwSyms :: [(Symbol, Int)]
rwSyms = forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol -> Bool
inRewrites forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {b} {a}. Num b => (a, Sort) -> (a, b)
toSum (forall a. SEnv a -> [(Symbol, a)]
toListSEnv (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, forall {a}. Num a => Sort -> a
getArity Sort
sort)

        getArity :: Sort -> a
getArity (FFunc Sort
_ Sort
rhs) = a
1 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
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a. Subable a => a -> [Symbol]
syms forall a b. (a -> b) -> a -> b
$ Rewrite -> Expr
smBody Rewrite
rw)
      = forall a. a -> Maybe a
Just (Rewrite -> Symbol
smName Rewrite
rw, (Rewrite -> Symbol
smDC Rewrite
rw, Rewrite -> Expr
smBody Rewrite
rw))
      | Bool
otherwise
      = 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,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rewrite -> Symbol
smDC Rewrite
rw,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Eq a => a -> [a] -> Maybe Int
L.elemIndex Symbol
x (Rewrite -> [Symbol]
smArgs Rewrite
rw)
      | Bool
otherwise
      = 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 = 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
&& forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (Rewrite -> Symbol
smDC Rewrite
sm) HashSet Symbol
userDefinedDcs
    userDefinedDcs :: HashSet Symbol
userDefinedDcs =
      forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ forall a. Symbolic a => a -> Symbol
symbol (DataCtor -> LocSymbol
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 = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition Rewrite -> Bool
isSelector [Rewrite]
rws
  where
    isSelector :: Rewrite -> Bool
isSelector Rewrite
sm = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (Rewrite -> Symbol
smName Rewrite
sm) HashSet Symbol
userDefinedDcFieldsSelectors
    userDefinedDcFieldsSelectors :: HashSet Symbol
userDefinedDcFieldsSelectors =
      forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ 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 -> (SMT.Context -> IO a) -> IO a
withCtx :: forall a. Config -> [Char] -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
env Context -> IO a
k = do
  Context
ctx <- Config -> [Char] -> SymEnv -> IO Context
SMT.makeContextWithSEnv Config
cfg [Char]
file SymEnv
env
  ()
_   <- Context -> IO ()
SMT.smtPush Context
ctx
  a
res <- Context -> IO a
k Context
ctx
  Context -> IO ()
SMT.cleanupContext Context
ctx
  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 = forall a. HashSet a -> Bool
S.null (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
e = forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"simplification of " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Expr
e) forall a b. (a -> b) -> a -> b
$ forall {t}. Eq t => (t -> t) -> t -> t
fix ((Expr -> Expr) -> Expr -> Expr
Vis.mapExprOnExpr Expr -> Expr
tx) Expr
e
    where
      fix :: (t -> t) -> t -> t
fix t -> t
f t
e = if t
e 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' <- 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
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)  <- 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 forall a. Eq a => a -> a -> Bool
== Symbol
dc'
        = Expr
c
      tx (EIte Expr
b Expr
e1 Expr
e2)
        | Expr -> Bool
isTautoPred Expr
b  = Expr
e1
        | Expr -> Bool
isContraPred Expr
b = Expr
e2
      tx (ECoerc Sort
s Sort
t Expr
e)
        | Sort
s 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)  <- 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 forall a. Eq a => a -> a -> Bool
== Symbol
dc'
        = [Expr]
esforall a. [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 :: AxiomEnv
ae = forall a. Normalizable a => a -> a
normalize forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
si}

instance Normalizable AxiomEnv where
  normalize :: AxiomEnv -> AxiomEnv
normalize AxiomEnv
aenv = AxiomEnv
aenv { aenvEqs :: [Equation]
aenvEqs   = forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"aenvEqs"  (forall a. Normalizable a => a -> a
normalize forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Equation]
aenvEqs   AxiomEnv
aenv)
                        , aenvSimpl :: [Rewrite]
aenvSimpl = forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"aenvSimpl" (forall a. Normalizable a => a -> a
normalize forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv) }

instance Normalizable Rewrite where
  normalize :: Rewrite -> Rewrite
normalize Rewrite
rw = Rewrite
rw { smArgs :: [Symbol]
smArgs = [Symbol]
xs', smBody :: Expr
smBody = Symbol -> Expr -> Expr
normalizeBody (Rewrite -> Symbol
smName Rewrite
rw) forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su forall a b. (a -> b) -> a -> b
$ Rewrite -> Expr
smBody Rewrite
rw }
    where
      su :: Subst
su  = [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> Expr
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      xs :: [Symbol]
xs  = Rewrite -> [Symbol]
smArgs Rewrite
rw
      xs' :: [Symbol]
xs' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith 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` 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 :: [(Symbol, Sort)]
eqArgs = forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs' [Sort]
ss, eqBody :: Expr
eqBody = Symbol -> Expr -> Expr
normalizeBody (Equation -> Symbol
eqName Equation
eq) forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su forall a b. (a -> b) -> a -> b
$ Equation -> Expr
eqBody Equation
eq }
    where
      su :: Subst
su      = [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> Expr
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      ([Symbol]
xs,[Sort]
ss) = forall a b. [(a, b)] -> ([a], [b])
unzip (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)
      xs' :: [Symbol]
xs'     = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith 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` forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (Equation -> 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
e | Symbol
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall a. Subable a => a -> [Symbol]
syms Expr
e = Expr -> Expr
go Expr
e
  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 :: Expr -> Expr
go (PAnd [PImp Expr
c Expr
e1, PImp (PNot Expr
c') Expr
e2]) | Expr
c forall a. Eq a => a -> a -> Bool
== Expr
c' = Expr -> Expr -> Expr -> Expr
EIte Expr
c Expr
e1 (Expr -> Expr
go Expr
e2)
    go Expr
e                                               = Expr
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
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st { evFuel :: FuelCount
evFuel = Symbol -> FuelCount -> FuelCount
useFuelCount Symbol
f (EvalEnv -> FuelCount
evFuel EvalEnv
st) })

-- | Increment the fuel count.
useFuelCount :: Symbol -> FuelCount -> FuelCount
useFuelCount :: Symbol -> FuelCount -> FuelCount
useFuelCount Symbol
f FuelCount
fc = FuelCount
fc { fcMap :: HashMap Symbol Int
fcMap = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Symbol
f (Int
k forall a. Num a => a -> a -> a
+ Int
1) HashMap Symbol Int
m }
  where
    k :: Int
k             = 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

-- | 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> FuelCount
evFuel
  case (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) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
fk forall a. Ord a => a -> a -> Bool
<= Int
n)
    (Maybe Int, Maybe Int)
_                 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True