--------------------------------------------------------------------------------
-- | 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 (filterM, foldM, forM_, when)
import           Control.Monad.State
import           Control.Monad.Trans.Maybe
import           Data.Bifunctor (second)
import qualified Data.HashMap.Strict  as M
import qualified Data.HashMap.Lazy  as HashMap.Lazy
import qualified Data.HashSet         as S
import           Data.IORef
import qualified Data.List            as L
import           Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.Maybe           as Mb
import qualified Data.Set as Set
import           Text.PrettyPrint.HughesPJ.Compat

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

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

    file :: [Char]
file   = Config -> [Char]
srcFile Config
cfg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
".evals"
    sEnv :: SymEnv
sEnv   = Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi
    aEnv :: AxiomEnv
aEnv   = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
    fi :: SInfo a
fi     = SInfo a -> SInfo a
forall a. Normalizable a => a -> a
normalize SInfo a
fi'

savePLEEqualities :: Config -> SInfo a -> SymEnv -> InstRes -> IO ()
savePLEEqualities :: forall a. Config -> SInfo a -> SymEnv -> InstRes -> IO ()
savePLEEqualities Config
cfg SInfo a
fi SymEnv
sEnv InstRes
res = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
save Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    let fq :: [Char]
fq   = Ext -> Config -> [Char]
queryFile Ext
Files.Fq Config
cfg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
".ple"
    [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"\nSaving PLE equalities: "   [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
fq [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
    [Char] -> IO ()
Misc.ensurePath [Char]
fq
    let constraint_equalities :: [(SubcId, [Expr])]
constraint_equalities =
          ((SubcId, SimpC a) -> (SubcId, [Expr]))
-> [(SubcId, SimpC a)] -> [(SubcId, [Expr])]
forall a b. (a -> b) -> [a] -> [b]
map (SubcId, SimpC a) -> (SubcId, [Expr])
forall {c :: * -> *} {a} {a}.
TaggedC c a =>
(a, c a) -> (a, [Expr])
equalitiesPerConstraint ([(SubcId, SimpC a)] -> [(SubcId, [Expr])])
-> [(SubcId, SimpC a)] -> [(SubcId, [Expr])]
forall a b. (a -> b) -> a -> b
$ HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall a b. Ord a => HashMap a b -> [(a, b)]
Misc.hashMapToAscList (HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)])
-> HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi
    [Char] -> [Char] -> IO ()
writeFile [Char]
fq ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
render (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
      ((SubcId, [Expr]) -> Doc) -> [(SubcId, [Expr])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SubcId, [Expr]) -> Doc
forall {a} {t :: * -> *}.
(Show a, Foldable t) =>
(a, t Expr) -> Doc
renderConstraintRewrite [(SubcId, [Expr])]
constraint_equalities
  where
    equalitiesPerConstraint :: (a, c a) -> (a, [Expr])
equalitiesPerConstraint (a
cid, c a
c) =
      (a
cid, [Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
L.sort [ Expr
e | Int
i <- IBindEnv -> [Int]
elemsIBindEnv (c a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv c a
c), Just Expr
e <- [Int -> InstRes -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i InstRes
res] ])
    renderConstraintRewrite :: (a, t Expr) -> Doc
renderConstraintRewrite (a
cid, t Expr
eqs) =
      Doc
"constraint id" Doc -> Doc -> Doc
<+> [Char] -> Doc
text (a -> [Char]
forall a. Show a => a -> [Char]
show a
cid [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":")
      Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2
           ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
L.intersperse Doc
"" ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
            (Expr -> Doc) -> [Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Expr -> Doc) -> (Expr -> Expr) -> Expr -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
unElab) ([Expr] -> [Doc]) -> [Expr] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Expr -> [Expr]
forall a. Set a -> [a]
Set.toList (Set Expr -> [Expr]) -> Set Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr] -> Set Expr
forall a. Ord a => [a] -> Set a
Set.fromList ([Expr] -> Set Expr) -> [Expr] -> Set Expr
forall a b. (a -> b) -> a -> b
$
            -- call elabExpr to try to bring equations that are missing
            -- some casts into a fully annotated form for comparison
            (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Located [Char] -> SymEnv -> Expr -> Expr
elabExpr Located [Char]
"savePLEEqualities" SymEnv
sEnv) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$
            (Expr -> [Expr]) -> t Expr -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
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 <- HashMap (OCType, OCType) Bool
-> IO (IORef (HashMap (OCType, OCType) Bool))
forall a. a -> IO (IORef a)
newIORef HashMap (OCType, OCType) Bool
forall a. Monoid a => a
mempty
    IORef (HashMap OCType Bool)
refRESTSatCache <- HashMap OCType Bool -> IO (IORef (HashMap OCType Bool))
forall a. a -> IO (IORef a)
newIORef HashMap OCType Bool
forall a. Monoid a => a
mempty
    let
        restOC :: RESTOrdering
restOC = Config -> RESTOrdering
FC.restOC Config
cfg
        oc0 :: OCAlgebra OCType RuntimeTerm IO
oc0 = RESTOrdering -> SolverHandle -> OCAlgebra OCType RuntimeTerm IO
ordConstraints RESTOrdering
restOC (SolverHandle -> OCAlgebra OCType RuntimeTerm IO)
-> SolverHandle -> OCAlgebra OCType RuntimeTerm IO
forall a b. (a -> b) -> a -> b
$ Maybe SolverHandle -> SolverHandle
forall a. HasCallStack => Maybe a -> a
Mb.fromJust Maybe SolverHandle
restSolver
        oc :: OCAlgebra OCType RuntimeTerm IO
        oc :: OCAlgebra OCType RuntimeTerm IO
oc = OCAlgebra OCType RuntimeTerm IO
oc0
             { OC.isSat = cachedIsSat refRESTSatCache oc0
             , OC.notStrongerThan = cachedNotStrongerThan refRESTCache oc0
             }
        et :: ExploredTerms RuntimeTerm OCType IO
        et :: ExploredTerms RuntimeTerm OCType IO
et = ExploreFuncs RuntimeTerm OCType IO
-> ExploreStrategy -> ExploredTerms RuntimeTerm OCType IO
forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ExploredTerms.empty
               EF
                 { union :: OCType -> OCType -> OCType
ExploredTerms.union = OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
OC.union OCAlgebra OCType RuntimeTerm IO
oc
                 , subsumes :: OCType -> OCType -> IO Bool
ExploredTerms.subsumes = OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra OCType RuntimeTerm IO
oc
                 , exRefine :: OCType -> RuntimeTerm -> RuntimeTerm -> OCType
exRefine = OCAlgebra OCType RuntimeTerm IO
-> OCType -> RuntimeTerm -> RuntimeTerm -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
OC.refine OCAlgebra OCType RuntimeTerm IO
oc
                 }
                 ExploreStrategy
ExploreWhenNeeded
        s0 :: EvalEnv
s0 = EvalEnv
              { evEnv :: SymEnv
evEnv = Context -> SymEnv
SMT.ctxSymEnv Context
ctx
              , evPendingUnfoldings :: HashMap Expr Expr
evPendingUnfoldings = HashMap Expr Expr
forall a. Monoid a => a
mempty
              , evNewEqualities :: EvEqualities
evNewEqualities = EvEqualities
forall a. Monoid a => a
mempty
              , evSMTCache :: HashMap Expr Bool
evSMTCache = HashMap Expr Bool
forall a. Monoid a => a
mempty
              , evFuel :: FuelCount
evFuel = Config -> FuelCount
defFuelCount Config
cfg
              , explored :: Maybe (ExploredTerms RuntimeTerm OCType IO)
explored = ExploredTerms RuntimeTerm OCType IO
-> Maybe (ExploredTerms RuntimeTerm OCType IO)
forall a. a -> Maybe a
Just ExploredTerms RuntimeTerm OCType IO
et
              , restSolver :: Maybe SolverHandle
restSolver = Maybe SolverHandle
restSolver
              , restOCA :: RESTOrdering
restOCA = RESTOrdering
restOC
              , evOCAlgebra :: OCAlgebra OCType RuntimeTerm IO
evOCAlgebra = OCAlgebra OCType RuntimeTerm IO
oc
              }
    InstEnv a -> IO (InstEnv a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (InstEnv a -> IO (InstEnv a)) -> InstEnv a -> IO (InstEnv a)
forall a b. (a -> b) -> a -> b
$ InstEnv
       { ieCfg :: Config
ieCfg = Config
cfg
       , ieSMT :: Context
ieSMT = Context
ctx
       , ieBEnv :: BindEnv a
ieBEnv = SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi
       , ieAenv :: AxiomEnv
ieAenv = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
       , ieCstrs :: CMap (SimpC a)
ieCstrs = CMap (SimpC a)
cs
       , ieKnowl :: Knowledge
ieKnowl = Config -> Context -> SInfo a -> Knowledge
forall a. Config -> Context -> SInfo a -> Knowledge
knowledge Config
cfg Context
ctx SInfo a
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 <- IORef (HashMap (c, c) Bool) -> IO (HashMap (c, c) Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap (c, c) Bool)
refRESTCache
      case (c, c) -> HashMap (c, c) Bool -> Maybe Bool
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (c
a, c
b) HashMap (c, c) Bool
m of
        Maybe Bool
Nothing -> do
          Bool
nst <- OCAlgebra c a IO -> c -> c -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra c a IO
oc c
a c
b
          IORef (HashMap (c, c) Bool) -> HashMap (c, c) Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap (c, c) Bool)
refRESTCache ((c, c) -> Bool -> HashMap (c, c) Bool -> HashMap (c, c) Bool
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (c
a, c
b) Bool
nst HashMap (c, c) Bool
m)
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
nst
        Just Bool
nst ->
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
nst

    cachedIsSat :: IORef (HashMap c Bool) -> OCAlgebra c a IO -> c -> IO Bool
cachedIsSat IORef (HashMap c Bool)
refRESTSatCache OCAlgebra c a IO
oc c
a = do
      HashMap c Bool
m <- IORef (HashMap c Bool) -> IO (HashMap c Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap c Bool)
refRESTSatCache
      case c -> HashMap c Bool -> Maybe Bool
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup c
a HashMap c Bool
m of
        Maybe Bool
Nothing -> do
          Bool
sat <- OCAlgebra c a IO -> c -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
OC.isSat OCAlgebra c a IO
oc c
a
          IORef (HashMap c Bool) -> HashMap c Bool -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (HashMap c Bool)
refRESTSatCache (c -> Bool -> HashMap c Bool -> HashMap c Bool
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert c
a Bool
sat HashMap c Bool
m)
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
sat
        Just Bool
sat ->
          Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
sat

----------------------------------------------------------------------------------------------
-- | Step 1b: @mkCTrie@ builds the @Trie@ of constraints indexed by their environments
--
-- The trie is a way to unfold the equalities a minimum number of times.
-- Say you have
--
-- > 1: [1, 2, 3, 4, 5] => p1
-- > 2: [1, 2, 3, 6, 7] => p2
--
-- Then you build the tree
--
-- >  1 -> 2 -> 3 -> 4 -> 5 — [Constraint 1]
-- >            | -> 6 -> 7 — [Constraint 2]
--
-- which you use to unfold everything in 1, 2, and 3 once (instead of twice)
-- and with the proper existing environment
--
mkCTrie :: [(SubcId, SimpC a)] -> CTrie
mkCTrie :: forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
ics  = [([Int], SubcId)] -> CTrie
forall a. [([Int], a)] -> Trie a
T.fromList [ (SimpC a -> [Int]
cBinds SimpC a
c, SubcId
i) | (SubcId
i, SimpC a
c) <- [(SubcId, SimpC a)]
ics ]
  where
    cBinds :: SimpC a -> [Int]
cBinds   = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
L.sort ([Int] -> [Int]) -> (SimpC a -> [Int]) -> SimpC a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> [Int]
elemsIBindEnv (IBindEnv -> [Int]) -> (SimpC a -> IBindEnv) -> SimpC a -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv

----------------------------------------------------------------------------------------------
-- | Step 2: @pleTrie@ walks over the @CTrie@ to actually do the incremental-PLE
pleTrie :: CTrie -> InstEnv a -> IO InstRes
pleTrie :: forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t InstEnv a
env = InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env' ICtx
ctx0 [Int]
forall {a}. [a]
diff0 Maybe Int
forall a. Maybe a
Nothing InstRes
forall {k} {v}. HashMap k v
res0 CTrie
t
  where
    env' :: InstEnv a
env'         = InstEnv a
env
    diff0 :: [a]
diff0        = []
    res0 :: HashMap k v
res0         = HashMap k v
forall {k} {v}. HashMap k v
M.empty
    ctx0 :: ICtx
ctx0         = ICtx
      { icAssms :: HashSet Expr
icAssms  = HashSet Expr
forall a. Monoid a => a
mempty
      , icCands :: HashSet Expr
icCands  = HashSet Expr
forall a. Monoid a => a
mempty
      , icEquals :: EvEqualities
icEquals = EvEqualities
forall a. Monoid a => a
mempty
      , icSimpl :: HashMap Expr Expr
icSimpl  = HashMap Expr Expr
forall a. Monoid a => a
mempty
      , icSubcId :: Maybe SubcId
icSubcId = Maybe SubcId
forall a. Maybe a
Nothing
      , icANFs :: [[(Symbol, SortedReft)]]
icANFs   = []
      }

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

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

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

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

evalToSMT :: String -> Config -> SMT.Context -> (Expr, Expr) -> Pred
evalToSMT :: [Char] -> Config -> Context -> (Expr, Expr) -> Expr
evalToSMT [Char]
msg Config
cfg Context
ctx (Expr
e1,Expr
e2) = [Char] -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT ([Char]
"evalToSMT:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg) Config
cfg Context
ctx [] (Expr -> Expr -> Expr
EEq Expr
e1 Expr
e2)

-- | Generate equalities for all function invocations in the candidates
-- in @ctx@ for which definitions are known. The function definitions are in
-- @ieKnowl@.
--
-- In pseudocode:
--
-- > do
-- >     for every candidate
-- >         discover equalities,
-- >         unfold function invocations,
-- >         update candidates with the unfolded expressions
-- >     send newly discovered equalities to the SMT solver
-- > until no new equalities are discovered
-- >       or the environment becomes inconsistent
--
evalCandsLoop :: Config -> ICtx -> SMT.Context -> Knowledge -> EvalST ICtx
evalCandsLoop :: Config -> ICtx -> Context -> Knowledge -> StateT EvalEnv IO ICtx
evalCandsLoop Config
cfg ICtx
ictx0 Context
ctx Knowledge
γ = ICtx -> Int -> StateT EvalEnv IO ICtx
go ICtx
ictx0 Int
0
  where
    go :: ICtx -> Int -> StateT EvalEnv IO ICtx
go ICtx
ictx Int
_ | HashSet Expr -> Bool
forall a. HashSet a -> Bool
S.null (ICtx -> HashSet Expr
icCands ICtx
ictx) = ICtx -> StateT EvalEnv IO ICtx
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
    go ICtx
ictx Int
i = do
      Bool
inconsistentEnv <- StateT EvalEnv IO Bool
testForInconsistentEnvironment
      if Bool
inconsistentEnv
        then ICtx -> StateT EvalEnv IO ICtx
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
        else do
                  IO () -> StateT EvalEnv IO ()
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> StateT EvalEnv IO ()) -> IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ Context -> Expr -> IO ()
SMT.smtAssert Context
ctx ([Expr] -> Expr
pAndNoDedup (HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList (HashSet Expr -> [Expr]) -> HashSet Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ ICtx -> HashSet Expr
icAssms ICtx
ictx))
                  let ictx' :: ICtx
ictx' = ICtx
ictx { icAssms = mempty }
                      cands :: [Expr]
cands = HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList (HashSet Expr -> [Expr]) -> HashSet Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ ICtx -> HashSet Expr
icCands ICtx
ictx
                  [[Expr]]
candss <- (Expr -> StateT EvalEnv IO [Expr])
-> [Expr] -> StateT EvalEnv IO [[Expr]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Knowledge -> ICtx -> Int -> Expr -> StateT EvalEnv IO [Expr]
evalOne Knowledge
γ ICtx
ictx' Int
i) [Expr]
cands
                  EvEqualities
us <- (EvalEnv -> EvEqualities) -> StateT EvalEnv IO EvEqualities
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
                  (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { evNewEqualities = mempty }
                  let noCandidateChanged :: Bool
noCandidateChanged = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (([Expr] -> Expr -> Bool) -> [[Expr]] -> [Expr] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith [Expr] -> Expr -> Bool
forall {a}. Eq a => [a] -> a -> Bool
eqCand [[Expr]]
candss [Expr]
cands)
                      unknownEqs :: EvEqualities
unknownEqs = EvEqualities
us EvEqualities -> EvEqualities -> EvEqualities
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` ICtx -> EvEqualities
icEquals ICtx
ictx
                  if EvEqualities -> Bool
forall a. HashSet a -> Bool
S.null EvEqualities
unknownEqs Bool -> Bool -> Bool
&& Bool
noCandidateChanged
                        then ICtx -> StateT EvalEnv IO ICtx
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
                        else do  let eqsSMT :: HashSet Expr
eqsSMT   = [Char] -> Config -> Context -> (Expr, Expr) -> Expr
evalToSMT [Char]
"evalCandsLoop" Config
cfg Context
ctx ((Expr, Expr) -> Expr) -> EvEqualities -> HashSet Expr
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvEqualities
unknownEqs
                                 let ictx'' :: ICtx
ictx''   = ICtx
ictx' { icEquals = icEquals ictx <> unknownEqs
                                                      , icAssms  = S.filter (not . isTautoPred) eqsSMT }
                                 ICtx -> Int -> StateT EvalEnv IO ICtx
go (ICtx
ictx'' { icCands = S.fromList (concat candss) }) (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

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

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

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

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

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

data InstEnv a = InstEnv
  { forall a. InstEnv a -> Config
ieCfg   :: !Config
  , forall a. InstEnv a -> Context
ieSMT   :: !SMT.Context
  , forall a. InstEnv a -> BindEnv a
ieBEnv  :: !(BindEnv a)
  , forall a. InstEnv a -> AxiomEnv
ieAenv  :: !AxiomEnv
  , forall a. InstEnv a -> CMap (SimpC a)
ieCstrs :: !(CMap (SimpC a))
  , forall a. InstEnv a -> Knowledge
ieKnowl :: !Knowledge
  , forall a. InstEnv a -> EvalEnv
ieEvEnv :: !EvalEnv
  }

----------------------------------------------------------------------------------------------
-- | @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 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2 ]

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


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

----------------------------------------------------------------------------------------------
-- | @updCtx env ctx delta cidMb@ adds the assumptions and candidates from @delta@ and @cidMb@
--   to the context.
----------------------------------------------------------------------------------------------

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


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

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

isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr :: forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
sid SimpC a
c = SimpC a -> Bool
forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c Bool -> Bool -> Bool
&& Bool -> SubcId -> HashMap SubcId Bool -> Bool
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Bool
False SubcId
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 -> [Char] -> [Char]
[FuelCount] -> [Char] -> [Char]
FuelCount -> [Char]
(Int -> FuelCount -> [Char] -> [Char])
-> (FuelCount -> [Char])
-> ([FuelCount] -> [Char] -> [Char])
-> Show FuelCount
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> FuelCount -> [Char] -> [Char]
showsPrec :: Int -> FuelCount -> [Char] -> [Char]
$cshow :: FuelCount -> [Char]
show :: FuelCount -> [Char]
$cshowList :: [FuelCount] -> [Char] -> [Char]
showList :: [FuelCount] -> [Char] -> [Char]
Show)

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

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

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

-- | Discover the equalities in an expression.
--
-- The discovered equalities are in the environment of the monad,
-- and the list of produced expressions contains the result of unfolding
-- definitions. When REST is in effect, more than one expression might
-- be returned because expressions can then be rewritten in more than one
-- way.
evalOne :: Knowledge -> ICtx -> Int -> Expr -> EvalST [Expr]
evalOne :: Knowledge -> ICtx -> Int -> Expr -> StateT EvalEnv IO [Expr]
evalOne Knowledge
γ ICtx
ctx Int
i Expr
e
  | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
|| [AutoRewrite] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx) = (Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[]) (Expr -> [Expr])
-> ((Expr, FinalExpand) -> Expr) -> (Expr, FinalExpand) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, FinalExpand) -> Expr
forall a b. (a, b) -> a
fst ((Expr, FinalExpand) -> [Expr])
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
NoRW Expr
e
evalOne Knowledge
γ ICtx
ctx Int
_ Expr
e = do
    EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
    let oc :: OCAlgebra OCType RuntimeTerm IO
        oc :: OCAlgebra OCType RuntimeTerm IO
oc = EvalEnv -> OCAlgebra OCType RuntimeTerm IO
evOCAlgebra EvalEnv
env
        rp :: RESTParams OCType
rp = OCAlgebra OCType Expr IO
-> [(Expr, TermOrigin)] -> OCType -> RESTParams OCType
forall oc.
OCAlgebra oc Expr IO -> [(Expr, TermOrigin)] -> oc -> RESTParams oc
RP ((Expr -> RuntimeTerm)
-> OCAlgebra OCType RuntimeTerm IO -> OCAlgebra OCType Expr IO
forall c a b (m :: * -> *).
(b -> a) -> OCAlgebra c a m -> OCAlgebra c b m
contramap Expr -> RuntimeTerm
Rewrite.convert OCAlgebra OCType RuntimeTerm IO
oc) [(Expr
e, TermOrigin
PLE)] OCType
constraints
        constraints :: OCType
constraints = OCAlgebra OCType RuntimeTerm IO -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c
OC.top OCAlgebra OCType RuntimeTerm IO
oc
        emptyET :: ExploredTerms RuntimeTerm OCType IO
emptyET = ExploreFuncs RuntimeTerm OCType IO
-> ExploreStrategy -> ExploredTerms RuntimeTerm OCType IO
forall term c (m :: * -> *).
ExploreFuncs term c m -> ExploreStrategy -> ExploredTerms term c m
ExploredTerms.empty ((OCType -> OCType -> OCType)
-> (OCType -> OCType -> IO Bool)
-> (OCType -> RuntimeTerm -> RuntimeTerm -> OCType)
-> ExploreFuncs RuntimeTerm OCType IO
forall term c (m :: * -> *).
(c -> c -> c)
-> (c -> c -> m Bool)
-> (c -> term -> term -> c)
-> ExploreFuncs term c m
EF (OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> c
OC.union OCAlgebra OCType RuntimeTerm IO
oc) (OCAlgebra OCType RuntimeTerm IO -> OCType -> OCType -> IO Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> c -> m Bool
OC.notStrongerThan OCAlgebra OCType RuntimeTerm IO
oc) (OCAlgebra OCType RuntimeTerm IO
-> OCType -> RuntimeTerm -> RuntimeTerm -> OCType
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
OC.refine OCAlgebra OCType RuntimeTerm IO
oc)) ExploreStrategy
ExploreWhenNeeded
    [Expr]
es <- Knowledge -> ICtx -> RESTParams OCType -> StateT EvalEnv IO [Expr]
evalREST Knowledge
γ ICtx
ctx RESTParams OCType
rp
    (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st { explored = Just emptyET }
    [Expr] -> StateT EvalEnv IO [Expr]
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
es

-- The FuncNormal and RWNormal evaluation strategies are used for REST
-- For example, consider the following function:
--   add(x, y) = if x == 0 then y else add(x - 1, y + 1)
-- And a rewrite rule:
--   forall a, b . add(a,b) -> add(b, a)
-- Then the expression add(t, add(2, 1)) would evaluate under NoRW to:
--   if t == 0 then 3 else add(t - 1, 4)
-- However, under FuncNormal, it would evaluate to: add(t, 3)
-- Thus, FuncNormal could engage the rewrite rule add(t, 3) = add(3, t)


data EvalType =
    NoRW       -- Normal PLE
  | FuncNormal -- REST: Expand function definitions only when the branch can be decided
  | RWNormal   -- REST: Fully Expand Defs in the context of rewriting (similar to NoRW)
  deriving (EvalType -> EvalType -> Bool
(EvalType -> EvalType -> Bool)
-> (EvalType -> EvalType -> Bool) -> Eq EvalType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EvalType -> EvalType -> Bool
== :: EvalType -> EvalType -> Bool
$c/= :: EvalType -> EvalType -> Bool
/= :: EvalType -> EvalType -> Bool
Eq)

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

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

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

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

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

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

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


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

-- | Unfolds function invocations in expressions.
--
-- Also reduces if-then-else when the boolean condition or the negation can be
-- proved valid. This is the actual implementation of guard-validation-before-unfolding
-- that is described in publications.
--
-- Also adds to the monad state all the unfolding equalities that have been
-- discovered as necessary.
--
eval :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval :: Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et = Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go
  where
    go :: Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go (ELam (Symbol
x,Sort
s) Expr
e)   = Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
x, Sort
s) Expr
e
    go e :: Expr
e@EIte{}         = Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e
    go (ECoerc Sort
s Sort
t Expr
e)   = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE (Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t)  ((Expr, FinalExpand) -> (Expr, FinalExpand))
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e
    go e :: Expr
e@(EApp Expr
_ Expr
_)     =
      case Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e of
       (Expr
f, [Expr]
es) | EvalType
et EvalType -> EvalType -> Bool
forall a. Eq a => a -> a -> Bool
== EvalType
RWNormal ->
          -- Just evaluate the arguments first, to give rewriting a chance to step in
          -- if necessary
          do
            ([Expr]
es', FinalExpand
fe) <- [(Expr, FinalExpand)] -> ([Expr], FinalExpand)
feSeq ([(Expr, FinalExpand)] -> ([Expr], FinalExpand))
-> StateT EvalEnv IO [(Expr, FinalExpand)]
-> StateT EvalEnv IO ([Expr], FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO (Expr, FinalExpand))
-> [Expr] -> StateT EvalEnv IO [(Expr, FinalExpand)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et) [Expr]
es
            if [Expr]
es [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Expr]
es'
              then (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Expr] -> Expr
eApps Expr
f [Expr]
es', FinalExpand
fe)
              else do
                (Expr
f', FinalExpand
fe)  <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (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
                (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe (Expr -> [Expr] -> Expr
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 ([(Expr, FinalExpand)] -> ([Expr], FinalExpand))
-> StateT EvalEnv IO [(Expr, FinalExpand)]
-> StateT EvalEnv IO ([Expr], FinalExpand)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO (Expr, FinalExpand))
-> [Expr] -> StateT EvalEnv IO [(Expr, FinalExpand)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et) (Expr
fExpr -> [Expr] -> [Expr]
forall 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
            (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe (Expr -> [Expr] -> Expr
eApps Expr
f' [Expr]
es') Maybe Expr
me', FinalExpand
fe FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe')

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

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

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

-- | 'evalELamb' produces equations that preserve the context of a rewrite
-- so equations include any necessary lambda bindings.
evalELam :: Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (Expr, FinalExpand)
evalELam :: Knowledge
-> ICtx
-> EvalType
-> (Symbol, Sort)
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalELam Knowledge
γ ICtx
ctx EvalType
et (Symbol
x, Sort
s) Expr
e = do
    HashMap Expr Expr
oldPendingUnfoldings <- (EvalEnv -> HashMap Expr Expr)
-> StateT EvalEnv IO (HashMap Expr Expr)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> HashMap Expr Expr
evPendingUnfoldings
    EvEqualities
oldEqs <- (EvalEnv -> EvEqualities) -> StateT EvalEnv IO EvEqualities
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
    (Expr
e', FinalExpand
fe) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval (Knowledge
γ { knLams = (x, s) : knLams γ }) ICtx
ctx EvalType
et Expr
e
    let e2' :: Expr
e2' = Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ctx Expr
e'
        elam :: Expr
elam = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
s) Expr
e
    -- Discard the old equalities which miss the lambda binding
    (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st -> EvalEnv
st
      { evPendingUnfoldings = oldPendingUnfoldings
      , evNewEqualities = S.insert (elam, ELam (x, s) e2') oldEqs
      }
    (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
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 (Symbol -> HashMap Symbol SortedReft -> Maybe SortedReft
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
`HashMap.Lazy.lookup` Lens' SortedReft SortedReft
-> HashMap Symbol SortedReft -> HashMap Symbol SortedReft
forall v.
Lens' v SortedReft -> HashMap Symbol v -> HashMap Symbol v
undoANF (SortedReft -> f SortedReft) -> SortedReft -> f SortedReft
forall a. a -> a
Lens' SortedReft SortedReft
id HashMap Symbol SortedReft
bindEnv)
  where
    bindEnv :: HashMap Symbol SortedReft
bindEnv = [HashMap Symbol SortedReft] -> HashMap Symbol SortedReft
forall k v. Eq k => [HashMap k v] -> HashMap k v
HashMap.Lazy.unions ([HashMap Symbol SortedReft] -> HashMap Symbol SortedReft)
-> [HashMap Symbol SortedReft] -> HashMap Symbol SortedReft
forall a b. (a -> b) -> a -> b
$ ([(Symbol, SortedReft)] -> HashMap Symbol SortedReft)
-> [[(Symbol, SortedReft)]] -> [HashMap Symbol SortedReft]
forall a b. (a -> b) -> [a] -> [b]
map [(Symbol, SortedReft)] -> HashMap Symbol SortedReft
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.Lazy.fromList ([[(Symbol, SortedReft)]] -> [HashMap Symbol SortedReft])
-> [[(Symbol, SortedReft)]] -> [HashMap Symbol SortedReft]
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 -> StateT EvalEnv IO [Expr]
evalREST Knowledge
γ ICtx
ctx RESTParams OCType
rp = do
  EvalEnv
env <- StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
  IORef (HashMap Expr Bool)
cacheRef <- IO (IORef (HashMap Expr Bool))
-> StateT EvalEnv IO (IORef (HashMap Expr Bool))
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (IORef (HashMap Expr Bool))
 -> StateT EvalEnv IO (IORef (HashMap Expr Bool)))
-> IO (IORef (HashMap Expr Bool))
-> StateT EvalEnv IO (IORef (HashMap Expr Bool))
forall a b. (a -> b) -> a -> b
$ HashMap Expr Bool -> IO (IORef (HashMap Expr Bool))
forall a. a -> IO (IORef a)
newIORef (HashMap Expr Bool -> IO (IORef (HashMap Expr Bool)))
-> HashMap Expr Bool -> IO (IORef (HashMap Expr Bool))
forall a b. (a -> b) -> a -> b
$ EvalEnv -> HashMap Expr Bool
evSMTCache EvalEnv
env
  IORef (HashMap Expr Bool)
-> Knowledge
-> ICtx
-> [Expr]
-> RESTParams OCType
-> StateT EvalEnv IO [Expr]
evalRESTWithCache IORef (HashMap Expr Bool)
cacheRef Knowledge
γ ICtx
ctx [] RESTParams OCType
rp

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

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

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

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

      EvEqualities
newEqualities <- (EvalEnv -> EvEqualities) -> StateT EvalEnv IO EvEqualities
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> EvEqualities
evNewEqualities
      HashMap Expr Bool
smtCache <- IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool)
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool))
-> IO (HashMap Expr Bool) -> StateT EvalEnv IO (HashMap Expr Bool)
forall a b. (a -> b) -> a -> b
$ IORef (HashMap Expr Bool) -> IO (HashMap Expr Bool)
forall a. IORef a -> IO a
readIORef IORef (HashMap Expr Bool)
cacheRef
      (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st ->
             EvalEnv
st { evNewEqualities  = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd
                , evSMTCache = smtCache
                , explored = Just $ ExploredTerms.insert
                  (Rewrite.convert e)
                  (c rp)
                  (S.insert (Rewrite.convert e') $ S.fromList (map (Rewrite.convert . (\((Expr, Expr)
_, Expr
e, OCType
_) -> Expr
e)) possibleRWs))
                  (Mb.fromJust $ explored st)
                })

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

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

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

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

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

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

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

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

    pathExprs :: [Expr]
pathExprs       = ((Expr, TermOrigin) -> Expr) -> [(Expr, TermOrigin)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, TermOrigin) -> Expr
forall a b. (a, b) -> a
fst ([Char] -> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"EVAL2: path" ([(Expr, TermOrigin)] -> [(Expr, TermOrigin)])
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a b. (a -> b) -> a -> b
$ RESTParams OCType -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams OCType
rp)
    e :: Expr
e               = [Expr] -> Expr
forall a. HasCallStack => [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
γ) (RWTerminationOpts -> RewriteArgs)
-> RWTerminationOpts -> RewriteArgs
forall a b. (a -> b) -> a -> b
$ Knowledge -> RWTerminationOpts
knRWTerminationOpts Knowledge
γ

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

    addConst :: (Expr, Expr) -> ICtx
addConst (Expr
e,Expr
e') = if HashSet Symbol -> Expr -> Bool
isConstant (Knowledge -> HashSet Symbol
knDCs Knowledge
γ) Expr
e'
                      then ICtx
ctx { icSimpl = M.insert e e' $ icSimpl ctx} else ICtx
ctx

-- | @evalApp kn ctx e es@ unfolds expressions in @eApps e es@ using rewrites
-- and equations
evalApp :: Knowledge -> ICtx -> Expr -> [Expr] -> EvalType -> EvalST (Maybe Expr, FinalExpand)
evalApp :: Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> EvalST (Maybe Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx Expr
e0 [Expr]
es EvalType
et
  | EVar Symbol
f <- Expr -> Expr
dropECst Expr
e0
  , Just Equation
eq <- Symbol -> Map Symbol Equation -> Maybe Equation
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
f (Knowledge -> Map Symbol Equation
knAms Knowledge
γ)
  , [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  = do
       SEnv Sort
env  <- (EvalEnv -> SEnv Sort) -> StateT EvalEnv IO (SEnv Sort)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort (SymEnv -> SEnv Sort)
-> (EvalEnv -> SymEnv) -> EvalEnv -> SEnv Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalEnv -> SymEnv
evEnv)
       Bool
okFuel <- Symbol -> StateT EvalEnv IO Bool
checkFuel Symbol
f
       if Bool
okFuel Bool -> Bool -> Bool
&& EvalType
et EvalType -> EvalType -> Bool
forall a. Eq a => a -> a -> Bool
/= EvalType
FuncNormal
         then do
                let ([Expr]
es1,[Expr]
es2) = Int -> [Expr] -> ([Expr], [Expr])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
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
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
newE -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
                let e2' :: Expr
e2' = Expr -> Expr
stripPLEUnfold Expr
e'
                    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
                    (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
                      EvalEnv
st {
                        evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st)
                      }
                    -- Don't unfold the expression if there is an if-then-else
                    -- guarding it, just to preserve the size of further
                    -- rewrites.
                    (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)
                  else do
                    Symbol -> StateT EvalEnv IO ()
useFuel Symbol
f
                    (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((EvalEnv -> EvalEnv) -> StateT EvalEnv IO ())
-> (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ \EvalEnv
st ->
                      EvalEnv
st
                        { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st)
                        , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st)
                        }
                    (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e2', FinalExpand
fe)
         else (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)
  where
    -- At the time of writing, any function application wrapping an
    -- if-statement would have the effect of unfolding the invocation.
    -- However, using pleUnfold still has the advantage of not generating
    -- extra equations to unfold pleUnfold itself. Using pleUnfold also
    -- makes the intention of the user rather explicit.
    stripPLEUnfold :: Expr -> Expr
stripPLEUnfold Expr
e
      | (Expr
ef, [Expr
arg]) <- Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e
      , EVar Symbol
f <- Expr -> Expr
dropECst Expr
ef
      , Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
"Language.Haskell.Liquid.ProofCombinators.pleUnfold"
      = Expr
arg
      | Bool
otherwise = Expr
e

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

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

evalApp Knowledge
_ ICtx
_ Expr
_e [Expr]
_es EvalType
_
  = (Maybe Expr, FinalExpand) -> EvalST (Maybe Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr
forall a. Maybe a
Nothing, FinalExpand
noExpand)

-- | Evaluates if-then-else statements until they can't be evaluated anymore
-- or some other expression is found.
evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
evalIte :: Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et (EIte Expr
i Expr
e1 Expr
e2) = do
      (Expr
b, FinalExpand
_) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
i
      Maybe Bool
b'  <- [Char] -> Maybe Bool -> Maybe Bool
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalEIt POS " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Expr, Expr) -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Expr
i, Expr
b)) (Maybe Bool -> Maybe Bool)
-> StateT EvalEnv IO (Maybe Bool) -> StateT EvalEnv IO (Maybe Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> Expr -> StateT EvalEnv IO (Maybe Bool)
isValidCached Knowledge
γ Expr
b
      case Maybe Bool
b' of
        Just Bool
True -> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e1
        Just Bool
False -> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
e2
        Maybe Bool
_ -> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2, FinalExpand
expand)
evalIte Knowledge
_ ICtx
_ EvalType
_ Expr
e' = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e', FinalExpand
noExpand)

-- | Creates equations that explain how to rewrite a given constructor
-- application with all measures that aren't user data measures
noUserDataMeasureEqs :: Knowledge -> Expr -> [(Expr,Expr)]
noUserDataMeasureEqs :: Knowledge -> Expr -> [(Expr, Expr)]
noUserDataMeasureEqs Knowledge
γ Expr
e =
  [ (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) Expr
e, Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
rw) [Expr]
es) (Rewrite -> Expr
smBody Rewrite
rw))
  | (Expr
ef, [Expr]
es) <- [Expr -> (Expr, [Expr])
splitEAppThroughECst Expr
e]
  , EVar Symbol
f <- [Expr -> Expr
dropECst Expr
ef]
  , Just [(Rewrite, IsUserDataSMeasure)]
rws <- [Symbol
-> Map Symbol [(Rewrite, IsUserDataSMeasure)]
-> Maybe [(Rewrite, IsUserDataSMeasure)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
f (Knowledge -> Map Symbol [(Rewrite, IsUserDataSMeasure)]
knSims Knowledge
γ)]
  , (Rewrite
rw, IsUserDataSMeasure
NoUserDataSMeasure) <- [(Rewrite, IsUserDataSMeasure)]
rws
  , [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
  ]

--------------------------------------------------------------------------------
-- | 'substEq' unfolds or instantiates an equation at a particular list of
--   argument values. We must also substitute the sort-variables that appear
--   as coercions. See tests/proof/ple1.fq
--------------------------------------------------------------------------------
substEq :: SEnv Sort -> Equation -> [Expr] -> Expr
substEq :: SEnv Sort -> Equation -> [Expr] -> Expr
substEq SEnv Sort
env Equation
eq [Expr]
es = Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su (SEnv Sort -> Equation -> [Expr] -> Expr
substEqCoerce SEnv Sort
env Equation
eq [Expr]
es)
  where su :: Subst
su = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Equation -> [Symbol]
eqArgNames Equation
eq) [Expr]
es

substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
substEqCoerce SEnv Sort
env Equation
eq [Expr]
es = CoSub -> Expr -> Expr
Vis.applyCoSub CoSub
coSub (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Equation -> Expr
eqBody Equation
eq
  where
    ts :: [Sort]
ts    = (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd    ((Symbol, Sort) -> Sort) -> [(Symbol, Sort)] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Equation -> [(Symbol, Sort)]
eqArgs Equation
eq
    sp :: SrcSpan
sp    = [Char] -> SrcSpan
panicSpan [Char]
"mkCoSub"
    eTs :: [Sort]
eTs   = SrcSpan -> SEnv Sort -> Expr -> Sort
sortExpr SrcSpan
sp SEnv Sort
env (Expr -> Sort) -> [Expr] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    coSub :: 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 = [(Symbol, Sort)] -> CoSub
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) <- [(Symbol, Sort)] -> [(Symbol, [Sort])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, Sort)]
xys ]
  where
    unite :: [Sort] -> Sort
unite [Sort]
ts    = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
Mb.fromMaybe ([Sort] -> Sort
forall {a} {a}. PPrint a => a -> a
uError [Sort]
ts) (Env -> [Sort] -> Maybe Sort
unifyTo1 Env
senv [Sort]
ts)
    senv :: Env
senv        = SEnv Sort -> Env
forall a. SEnv a -> Symbol -> SESearch a
mkSearchEnv SEnv Sort
env
    uError :: a -> a
uError a
ts   = [Char] -> a
forall a. [Char] -> a
panic ([Char]
"mkCoSub: cannot build CoSub for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)] -> [Char]
forall a. PPrint a => a -> [Char]
showpp [(Symbol, Sort)]
xys [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" cannot unify " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
showpp a
ts)
    xys :: [(Symbol, Sort)]
xys         = [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ [[(Symbol, Sort)]] -> [(Symbol, Sort)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Symbol, Sort)]] -> [(Symbol, Sort)])
-> [[(Symbol, Sort)]] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ (Sort -> Sort -> [(Symbol, Sort)])
-> [Sort] -> [Sort] -> [[(Symbol, Sort)]]
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 [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
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 [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ Sort -> Sort -> [(Symbol, Sort)]
go Sort
t1 Sort
t2
    go Sort
_             Sort
_             = []

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

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

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

    Maybe Bool
mb -> Maybe Bool -> StateT EvalEnv IO (Maybe Bool)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Bool
mb

--------------------------------------------------------------------------------
-- | Knowledge (SMT Interaction)
--------------------------------------------------------------------------------
data Knowledge = KN
  { -- | Rewrites rules came from match definitions
    --
    -- They are grouped by the data constructor that they unfold, and are
    -- augmented with an attribute that say whether they originate from a
    -- user data declaration.
    Knowledge -> Map Symbol [(Rewrite, IsUserDataSMeasure)]
knSims              :: Map Symbol [(Rewrite, IsUserDataSMeasure)]
  , Knowledge -> Map Symbol Equation
knAms               :: Map Symbol Equation -- ^ All function definitions
  , Knowledge -> Context
knContext           :: SMT.Context
  , Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds             :: SMT.Context -> [(Symbol, Sort)] -> Expr -> IO Bool
  , Knowledge -> [(Symbol, Sort)]
knLams              :: ![(Symbol, Sort)]
  , Knowledge -> [(Symbol, Int)]
knSummary           :: ![(Symbol, Int)]     -- ^ summary of functions to be evaluates (knSims and knAsms) with their arity
  , Knowledge -> HashSet Symbol
knDCs               :: !(S.HashSet Symbol)  -- ^ data constructors drawn from Rewrite
  , Knowledge -> HashMap Symbol DataCtor
knDataCtors         :: !(M.HashMap Symbol DataCtor) -- ^ data constructors by name
  , Knowledge -> SelectorMap
knSels              :: !SelectorMap
  , Knowledge -> ConstDCMap
knConsts            :: !ConstDCMap
  , Knowledge -> HashMap SubcId [AutoRewrite]
knAutoRWs           :: M.HashMap SubcId [AutoRewrite]
  , Knowledge -> RWTerminationOpts
knRWTerminationOpts :: RWTerminationOpts
  }

-- | A type to express whether SMeasures originate from data definitions.
-- That is whether they are constructor tests, selectors, or something else.
data IsUserDataSMeasure = NoUserDataSMeasure | UserDataSMeasure
  deriving (IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
(IsUserDataSMeasure -> IsUserDataSMeasure -> Bool)
-> (IsUserDataSMeasure -> IsUserDataSMeasure -> Bool)
-> Eq IsUserDataSMeasure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
== :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
$c/= :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
/= :: IsUserDataSMeasure -> IsUserDataSMeasure -> Bool
Eq, Int -> IsUserDataSMeasure -> [Char] -> [Char]
[IsUserDataSMeasure] -> [Char] -> [Char]
IsUserDataSMeasure -> [Char]
(Int -> IsUserDataSMeasure -> [Char] -> [Char])
-> (IsUserDataSMeasure -> [Char])
-> ([IsUserDataSMeasure] -> [Char] -> [Char])
-> Show IsUserDataSMeasure
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> IsUserDataSMeasure -> [Char] -> [Char]
showsPrec :: Int -> IsUserDataSMeasure -> [Char] -> [Char]
$cshow :: IsUserDataSMeasure -> [Char]
show :: IsUserDataSMeasure -> [Char]
$cshowList :: [IsUserDataSMeasure] -> [Char] -> [Char]
showList :: [IsUserDataSMeasure] -> [Char] -> [Char]
Show)

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

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

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


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

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



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

    makeSel :: Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel Rewrite
rw
      | EVar Symbol
x <- Rewrite -> Expr
smBody Rewrite
rw
      = (Rewrite -> Symbol
smName Rewrite
rw,) ((Symbol, Int) -> (Symbol, (Symbol, Int)))
-> (Int -> (Symbol, Int)) -> Int -> (Symbol, (Symbol, Int))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rewrite -> Symbol
smDC Rewrite
rw,) (Int -> (Symbol, (Symbol, Int)))
-> Maybe Int -> Maybe (Symbol, (Symbol, Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> [Symbol] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
L.elemIndex Symbol
x (Rewrite -> [Symbol]
smArgs Rewrite
rw)
      | Bool
otherwise
      = Maybe (Symbol, (Symbol, Int))
forall a. Maybe a
Nothing

-- | Partitions the input rewrites into constructor tests and others.
--
-- We don't need to deal in PLE with data constructor tests. That is,
-- functions of the form @isCons :: List a -> Bool@ or @isNil :: List a -> Bool@
-- when @List a@ is defined by the user.
--
-- The SMT solver knows about these functions when datatypes are declared to it,
-- so PLE doesn't need to unfold them.
--
-- Non-user defined datatypes like @[a]@ still need to have tests unfolded
-- because they are not declared as datatypes to the SMT solver.
--
-- Also, REST could need this functions unfolded since otherwise it may not
-- discover possible rewrites.
--
partitionUserDataConstructorTests :: [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorTests :: [DataDecl] -> [Rewrite] -> ([Rewrite], [Rewrite])
partitionUserDataConstructorTests [DataDecl]
dds [Rewrite]
rws = (Rewrite -> Bool) -> [Rewrite] -> ([Rewrite], [Rewrite])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition Rewrite -> Bool
isDataConstructorTest [Rewrite]
rws
  where
    isDataConstructorTest :: Rewrite -> Bool
isDataConstructorTest Rewrite
sm = Symbol -> Bool
isTestSymbol (Rewrite -> Symbol
smName Rewrite
sm) Bool -> Bool -> Bool
&& Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (Rewrite -> Symbol
smDC Rewrite
sm) HashSet Symbol
userDefinedDcs
    userDefinedDcs :: HashSet Symbol
userDefinedDcs =
      [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ Located Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (DataCtor -> Located Symbol
dcName DataCtor
dc) | DataDecl
dd <- [DataDecl]
dds, DataCtor
dc <- DataDecl -> [DataCtor]
ddCtors DataDecl
dd ]

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


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

withCtx :: Config -> FilePath -> SymEnv -> (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
  a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res


-- (sel_i, D, i), meaning sel_i (D x1 .. xn) = xi,
-- i.e., sel_i selects the ith value for the data constructor D
type SelectorMap = [(Symbol, (Symbol, Int))]
type ConstDCMap = [(Symbol, (Symbol, Expr))]

-- ValueMap maps expressions to constants (including data constructors)
type ConstMap = M.HashMap Expr Expr
type LDataCon = Symbol              -- Data Constructors

isConstant :: S.HashSet LDataCon -> Expr -> Bool
isConstant :: HashSet Symbol -> Expr -> Bool
isConstant HashSet Symbol
dcs Expr
e = HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference (Expr -> HashSet Symbol
exprSymbolsSet Expr
e) HashSet Symbol
dcs)

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

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

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


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

class Normalizable a where
  normalize :: a -> a

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

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

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


instance Normalizable Equation where
  normalize :: Equation -> Equation
normalize Equation
eq = Equation
eq {eqArgs = zip xs' ss, eqBody = normalizeBody (eqName eq) $ subst su $ eqBody eq }
    where
      su :: Subst
su      = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst) -> [(Symbol, Expr)] -> Subst
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> (Symbol, Expr))
-> [Symbol] -> [Symbol] -> [(Symbol, Expr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> Expr
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      ([Symbol]
xs,[Sort]
ss) = [(Symbol, Sort)] -> ([Symbol], [Sort])
forall a b. [(a, b)] -> ([a], [b])
unzip (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)
      xs' :: [Symbol]
xs'     = (Symbol -> SubcId -> Symbol) -> [Symbol] -> [SubcId] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> SubcId -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
mkSymbol [Symbol]
xs [SubcId
0 :: Integer ..]
      mkSymbol :: Symbol -> a -> Symbol
mkSymbol Symbol
x a
i = Symbol
x Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol -> a -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (Equation -> Symbol
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 Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
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 Expr -> Expr -> Bool
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
  (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st { evFuel = useFuelCount f (evFuel st) })

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

-- | Returns False if there is a fuel count in the evaluation environment and
-- the fuel count exceeds the maximum. Returns True otherwise.
checkFuel :: Symbol -> EvalST Bool
checkFuel :: Symbol -> StateT EvalEnv IO Bool
checkFuel Symbol
f = do
  FuelCount
fc <- (EvalEnv -> FuelCount) -> StateT EvalEnv IO FuelCount
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> FuelCount
evFuel
  case (Symbol -> HashMap Symbol Int -> Maybe Int
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f (FuelCount -> HashMap Symbol Int
fcMap FuelCount
fc), FuelCount -> Maybe Int
fcMax FuelCount
fc) of
    (Just Int
fk, Just Int
n) -> Bool -> StateT EvalEnv IO Bool
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
fk Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n)
    (Maybe Int, Maybe Int)
_                 -> Bool -> StateT EvalEnv IO Bool
forall a. a -> StateT EvalEnv IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True