--------------------------------------------------------------------------------
-- | 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 DeriveGeneric             #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE BangPatterns              #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE ViewPatterns              #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ExistentialQuantification #-}

module Language.Fixpoint.Solver.PLE (instantiate) 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 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.Sanitize        (symbolEnv)
import           Language.Fixpoint.Solver.Rewrite

import Language.REST.AbstractOC as OC
import Language.REST.ExploredTerms as ET
import Language.REST.RuntimeTerm as RT
import Language.REST.OrderingConstraints.ADT (ConstraintsADT)
import Language.REST.Op
import Language.REST.SMT (withZ3, SolverHandle)

import           Control.Monad.State
import           Control.Monad.Trans.Maybe
import           Data.Bifunctor (second)
import qualified Data.HashMap.Strict  as M
import qualified Data.HashSet         as S
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.Text            as Tx
import           Debug.Trace          (trace)
import           Text.PrettyPrint.HughesPJ.Compat

-- Type of Ordering Constraints for REST
type OCType = ConstraintsADT

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

traceE :: (Expr,Expr) -> (Expr,Expr)
traceE :: (Expr, Expr) -> (Expr, Expr)
traceE (Expr
e,Expr
e')
  | Bool
isEnabled
  , Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e'
  = String -> (Expr, Expr) -> (Expr, Expr)
forall a. String -> a -> a
trace (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ~> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e') (Expr
e,Expr
e')
  | Bool
otherwise
  = (Expr
e,Expr
e')
  where
    isEnabled :: Bool
    isEnabled :: Bool
isEnabled = Bool
False

--------------------------------------------------------------------------------
-- | Strengthen Constraint Environments via PLE 
--------------------------------------------------------------------------------
{-# SCC instantiate #-}
instantiate :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate :: 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 (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 -> String -> SymEnv -> (Context -> IO InstRes) -> IO InstRes
forall a. Config -> String -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg String
file SymEnv
sEnv (CTrie -> InstEnv a -> IO InstRes
forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t (InstEnv a -> IO InstRes)
-> (Context -> InstEnv a) -> Context -> IO InstRes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Config
-> SInfo a
-> HashMap SubcId (SimpC a)
-> Maybe SolverHandle
-> Context
-> InstEnv a
forall a.
Loc a =>
Config
-> SInfo a
-> CMap (SimpC a)
-> Maybe SolverHandle
-> Context
-> InstEnv a
instEnv Config
cfg SInfo a
fi HashMap SubcId (SimpC a)
cs Maybe SolverHandle
solver) -- 2. TRAVERSE Trie to compute InstRes
    Config -> SInfo a -> InstRes -> IO ()
forall a. Config -> SInfo a -> InstRes -> IO ()
savePLEEqualities Config
cfg SInfo a
fi InstRes
res
    SInfo a -> IO (SInfo 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 :: (Maybe SolverHandle -> IO a) -> IO a
withRESTSolver Maybe SolverHandle -> IO a
f | [AutoRewrite] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([[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) = Maybe SolverHandle -> IO a
f Maybe SolverHandle
forall a. Maybe a
Nothing
    withRESTSolver Maybe SolverHandle -> IO a
f | Bool
otherwise = (SolverHandle -> IO a) -> IO a
forall (m :: * -> *) b. MonadIO m => (SolverHandle -> m b) -> m b
withZ3 (\SolverHandle
z3 -> Maybe SolverHandle -> IO a
f (SolverHandle -> Maybe SolverHandle
forall a. a -> Maybe a
Just SolverHandle
z3))

    file :: String
file   = Config -> String
srcFile Config
cfg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".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 -> InstRes -> IO ()
savePLEEqualities :: Config -> SInfo a -> InstRes -> IO ()
savePLEEqualities Config
cfg SInfo a
fi 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 :: String
fq   = Ext -> Config -> String
queryFile Ext
Files.Fq Config
cfg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".ple"
    String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\nSaving PLE equalities: "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fq String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
    String -> IO ()
Misc.ensurePath String
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
    String -> String -> IO ()
writeFile String
fq (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
render (Doc -> String) -> Doc -> String
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. Show a => (a, [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, [Expr]) -> Doc
renderConstraintRewrite (a
cid, [Expr]
eqs) =
      Doc
"constraint id" Doc -> Doc -> Doc
<+> String -> Doc
text (a -> String
forall a. Show a => a -> String
show a
cid String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":")
      Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2 (Expr -> Doc
forall a. Fixpoint a => a -> Doc
toFix ([Expr] -> Expr
pAnd [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 -> InstEnv a
instEnv :: Config
-> SInfo a
-> CMap (SimpC a)
-> Maybe SolverHandle
-> Context
-> InstEnv a
instEnv Config
cfg SInfo a
fi CMap (SimpC a)
cs Maybe SolverHandle
restSolver Context
ctx = Config
-> Context
-> BindEnv
-> AxiomEnv
-> CMap (SimpC a)
-> Knowledge
-> EvalEnv
-> InstEnv a
forall a.
Config
-> Context
-> BindEnv
-> AxiomEnv
-> CMap (SimpC a)
-> Knowledge
-> EvalEnv
-> InstEnv a
InstEnv Config
cfg Context
ctx BindEnv
bEnv AxiomEnv
aEnv CMap (SimpC a)
cs Knowledge
γ EvalEnv
s0
  where
    bEnv :: BindEnv
bEnv              = SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs SInfo a
fi
    aEnv :: AxiomEnv
aEnv              = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
    γ :: Knowledge
γ                 = Config -> Context -> SInfo a -> Knowledge
forall a. Config -> Context -> SInfo a -> Knowledge
knowledge Config
cfg Context
ctx SInfo a
fi  
    s0 :: EvalEnv
s0                = SymEnv
-> EvAccum
-> FuelCount
-> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
-> Maybe SolverHandle
-> EvalEnv
EvalEnv (Context -> SymEnv
SMT.ctxSymEnv Context
ctx) EvAccum
forall a. Monoid a => a
mempty (Config -> FuelCount
defFuelCount Config
cfg) Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
forall term. Maybe (ExploredTerms term (OCType Op) IO)
et Maybe SolverHandle
restSolver
    et :: Maybe (ExploredTerms term (OCType Op) IO)
et                = (SolverHandle -> ExploredTerms term (OCType Op) IO)
-> Maybe SolverHandle -> Maybe (ExploredTerms term (OCType Op) IO)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SolverHandle -> ExploredTerms term (OCType Op) IO
forall term. SolverHandle -> ExploredTerms term (OCType Op) IO
makeET Maybe SolverHandle
restSolver
    makeET :: SolverHandle -> ExploredTerms term (OCType Op) IO
makeET SolverHandle
solver     =
      ExploreFuncs (OCType Op) IO -> ExploredTerms term (OCType Op) IO
forall c (m :: * -> *) term.
ExploreFuncs c m -> ExploredTerms term c m
ET.empty ((OCType Op -> OCType Op -> OCType Op)
-> (OCType Op -> OCType Op -> IO Bool)
-> ExploreFuncs (OCType Op) IO
forall c (m :: * -> *).
(c -> c -> c) -> (c -> c -> m Bool) -> ExploreFuncs c m
EF (AbstractOC (OCType Op) Expr IO
-> OCType Op -> OCType Op -> OCType Op
forall c a (m :: * -> *). AbstractOC c a m -> c -> c -> c
OC.union (SolverHandle -> AbstractOC (OCType Op) Expr IO
ordConstraints SolverHandle
solver)) (AbstractOC (OCType Op) Expr IO -> OCType Op -> OCType Op -> IO Bool
forall c a (m :: * -> *). AbstractOC c a m -> c -> c -> m Bool
OC.notStrongerThan (SolverHandle -> AbstractOC (OCType Op) Expr IO
ordConstraints SolverHandle
solver)))

---------------------------------------------------------------------------------------------- 
-- | 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 :: [(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 :: CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t InstEnv a
env = InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx0 [Int]
forall a. [a]
diff0 Maybe Int
forall a. Maybe a
Nothing InstRes
forall k v. HashMap k v
res0 CTrie
t 
  where 
    diff0 :: [a]
diff0        = []
    res0 :: HashMap k v
res0         = HashMap k v
forall k v. HashMap k v
M.empty 
    ctx0 :: ICtx
ctx0         = InstEnv a -> [(Expr, Expr)] -> ICtx
forall a. InstEnv a -> [(Expr, Expr)] -> ICtx
initCtx InstEnv a
env ((Equation -> (Expr, Expr)
mkEq (Equation -> (Expr, Expr)) -> [Equation] -> [(Expr, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Equation]
es0) [(Expr, Expr)] -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ (Rewrite -> (Expr, Expr)
mkEq' (Rewrite -> (Expr, Expr)) -> [Rewrite] -> [(Expr, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
es0'))
    es0 :: [Equation]
es0          = (Equation -> Bool) -> [Equation] -> [Equation]
forall a. (a -> Bool) -> [a] -> [a]
L.filter ([(Symbol, Sort)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(Symbol, Sort)] -> Bool)
-> (Equation -> [(Symbol, Sort)]) -> Equation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> [(Symbol, Sort)]
eqArgs) (AxiomEnv -> [Equation]
aenvEqs   (AxiomEnv -> [Equation])
-> (InstEnv a -> AxiomEnv) -> InstEnv a -> [Equation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstEnv a -> AxiomEnv
forall a. InstEnv a -> AxiomEnv
ieAenv (InstEnv a -> [Equation]) -> InstEnv a -> [Equation]
forall a b. (a -> b) -> a -> b
$ InstEnv a
env)
    es0' :: [Rewrite]
es0'         = (Rewrite -> Bool) -> [Rewrite] -> [Rewrite]
forall a. (a -> Bool) -> [a] -> [a]
L.filter ([Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Symbol] -> Bool) -> (Rewrite -> [Symbol]) -> Rewrite -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> [Symbol]
smArgs) (AxiomEnv -> [Rewrite]
aenvSimpl (AxiomEnv -> [Rewrite])
-> (InstEnv a -> AxiomEnv) -> InstEnv a -> [Rewrite]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstEnv a -> AxiomEnv
forall a. InstEnv a -> AxiomEnv
ieAenv (InstEnv a -> [Rewrite]) -> InstEnv a -> [Rewrite]
forall a b. (a -> b) -> a -> b
$ InstEnv a
env)
    mkEq :: Equation -> (Expr, Expr)
mkEq  Equation
eq     = (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Equation -> Symbol
eqName Equation
eq, Equation -> Expr
eqBody Equation
eq)
    mkEq' :: Rewrite -> (Expr, Expr)
mkEq' Rewrite
rw     = (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smDC Rewrite
rw), Rewrite -> Expr
smBody Rewrite
rw)

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 :: 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 (m :: * -> *) a. Monad m => a -> m a
return InstRes
res
  T.Node [Branch SubcId
b] -> InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
forall a.
InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx [Int]
delta Maybe Int
i InstRes
res Branch SubcId
b
  T.Node [Branch SubcId]
bs  -> InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> (ICtx -> IO InstRes)
-> IO InstRes
forall a b.
InstEnv a
-> ICtx -> [Int] -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx [Int]
delta Maybe SubcId
forall a. Maybe a
Nothing ((ICtx -> IO InstRes) -> IO InstRes)
-> (ICtx -> IO InstRes) -> IO InstRes
forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do 
                  (ICtx
ctx'', InstRes
res') <- InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstRes)
forall a.
InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, 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 :: InstEnv a
-> ICtx
-> [Int]
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx [Int]
delta Maybe Int
iMb InstRes
res Branch SubcId
b = case Branch SubcId
b of
  T.Bind Int
i CTrie
t -> InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
forall a.
InstEnv a
-> ICtx -> [Int] -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx (Int
iInt -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
delta) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) InstRes
res CTrie
t
  T.Val SubcId
cid  -> InstEnv a
-> ICtx
-> [Int]
-> Maybe SubcId
-> (ICtx -> IO InstRes)
-> IO InstRes
forall a b.
InstEnv a
-> ICtx -> [Int] -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx [Int]
delta (SubcId -> Maybe SubcId
forall a. a -> Maybe a
Just SubcId
cid) ((ICtx -> IO InstRes) -> IO InstRes)
-> (ICtx -> IO InstRes) -> IO InstRes
forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do 
                  IO ()
progressTick
                  ((ICtx, InstRes) -> InstRes
forall a b. (a, b) -> b
snd ((ICtx, InstRes) -> InstRes) -> IO (ICtx, InstRes) -> IO InstRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstRes)
forall a.
InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, 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@ plus rewrites that
-- candidates can use.
--
-- Sets the current constraint id in @ctx@ to @cidMb@.
--
-- Pushes assumptions from the modified context to the SMT solver, runs @act@,
-- and then pops the assumptions.
--
withAssms :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (ICtx -> IO b) -> IO b 
withAssms :: InstEnv a
-> ICtx -> [Int] -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms env :: InstEnv a
env@(InstEnv {CMap (SimpC a)
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv
ieSMT :: Context
ieCfg :: Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..}) ICtx
ctx [Int]
delta Maybe SubcId
cidMb ICtx -> IO b
act = do
  let ctx' :: ICtx
ctx'  = InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> ICtx
forall a. InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> ICtx
updCtx InstEnv a
env ICtx
ctx [Int]
delta Maybe SubcId
cidMb 
  let assms :: HashSet Expr
assms = ICtx -> HashSet Expr
icAssms ICtx
ctx'
  Context -> String -> IO b -> IO b
forall a. Context -> String -> IO a -> IO a
SMT.smtBracket Context
ieSMT  String
"PLE.evaluate" (IO b -> IO b) -> IO b -> IO b
forall a b. (a -> b) -> a -> b
$ do
    HashSet Expr -> (Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ HashSet Expr
assms (Context -> Expr -> IO ()
SMT.smtAssert Context
ieSMT) 
    ICtx -> IO b
act ICtx
ctx' { icAssms :: HashSet Expr
icAssms = HashSet Expr
forall a. Monoid a => a
mempty }

-- | @ple1@ performs the PLE at a single "node" in the Trie 
ple1 :: InstEnv a -> ICtx -> Maybe BindId -> InstRes -> IO (ICtx, InstRes)
ple1 :: InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstRes)
ple1 (InstEnv {CMap (SimpC a)
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..}) ICtx
ctx Maybe Int
i InstRes
res = 
  InstRes -> Maybe Int -> ICtx -> (ICtx, InstRes)
updCtxRes InstRes
res Maybe Int
i (ICtx -> (ICtx, InstRes)) -> IO ICtx -> IO (ICtx, InstRes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config -> ICtx -> Context -> Knowledge -> EvalEnv -> IO ICtx
evalCandsLoop Config
ieCfg ICtx
ctx Context
ieSMT Knowledge
ieKnowl EvalEnv
ieEvEnv


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

evalCandsLoop :: Config -> ICtx -> SMT.Context -> Knowledge -> EvalEnv -> IO ICtx 
evalCandsLoop :: Config -> ICtx -> Context -> Knowledge -> EvalEnv -> IO ICtx
evalCandsLoop Config
cfg ICtx
ictx0 Context
ctx Knowledge
γ EvalEnv
env = ICtx -> Int -> IO ICtx
go ICtx
ictx0 Int
0
  where
    withRewrites :: EvAccum -> EvAccum
withRewrites EvAccum
exprs =
      let
        rws :: [[(Expr, Expr)]]
rws = [Expr -> Map Symbol [Rewrite] -> [(Expr, Expr)]
rewrite Expr
e (Knowledge -> Map Symbol [Rewrite]
knSims Knowledge
γ) | Expr
e <- HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList ((Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd ((Expr, Expr) -> Expr) -> EvAccum -> HashSet Expr
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
exprs)]
      in 
        EvAccum
exprs EvAccum -> EvAccum -> EvAccum
forall a. Semigroup a => a -> a -> a
<> ([(Expr, Expr)] -> EvAccum
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Expr, Expr)] -> EvAccum) -> [(Expr, Expr)] -> EvAccum
forall a b. (a -> b) -> a -> b
$ [[(Expr, Expr)]] -> [(Expr, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Expr, Expr)]]
rws)
    go :: ICtx -> Int -> IO ICtx
go ICtx
ictx Int
_ | HashSet Expr -> Bool
forall a. HashSet a -> Bool
S.null (ICtx -> HashSet Expr
icCands ICtx
ictx) = ICtx -> IO ICtx
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
    go ICtx
ictx Int
i =  do
                  let cands :: HashSet Expr
cands = ICtx -> HashSet Expr
icCands ICtx
ictx
                  let env' :: EvalEnv
env' = EvalEnv
env { evAccum :: EvAccum
evAccum = ICtx -> EvAccum
icEquals ICtx
ictx EvAccum -> EvAccum -> EvAccum
forall a. Semigroup a => a -> a -> a
<> EvalEnv -> EvAccum
evAccum EvalEnv
env 
                                 , evFuel :: FuelCount
evFuel  = ICtx -> FuelCount
icFuel   ICtx
ictx 
                                 }
                  (ICtx
ictx', [EvAccum]
evalResults)  <- do
                               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 :: HashSet Expr
icAssms = HashSet Expr
forall a. Monoid a => a
mempty }
                               ((ICtx, [EvAccum]) -> Expr -> IO (ICtx, [EvAccum]))
-> (ICtx, [EvAccum]) -> [Expr] -> IO (ICtx, [EvAccum])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Knowledge
-> EvalEnv
-> Int
-> (ICtx, [EvAccum])
-> Expr
-> IO (ICtx, [EvAccum])
evalOneCandStep Knowledge
γ EvalEnv
env' Int
i) (ICtx
ictx', []) (HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList HashSet Expr
cands)
                               -- foldM (\ictx e -> undefined) 
                               -- mapM (evalOne γ env' ictx) (S.toList cands)
                  let us :: EvAccum
us = [EvAccum] -> EvAccum
forall a. Monoid a => [a] -> a
mconcat [EvAccum]
evalResults 
                  if EvAccum -> Bool
forall a. HashSet a -> Bool
S.null (EvAccum
us EvAccum -> EvAccum -> EvAccum
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` ICtx -> EvAccum
icEquals ICtx
ictx)
                        then ICtx -> IO ICtx
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx 
                        else do  let oks :: HashSet Expr
oks      = (Expr, Expr) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Expr) -> Expr) -> EvAccum -> HashSet Expr
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
us
                                 let us' :: EvAccum
us'      = EvAccum -> EvAccum
withRewrites EvAccum
us 
                                 let eqsSMT :: HashSet Expr
eqsSMT   = String -> Config -> Context -> (Expr, Expr) -> Expr
evalToSMT String
"evalCandsLoop" Config
cfg Context
ctx ((Expr, Expr) -> Expr) -> EvAccum -> HashSet Expr
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
us'
                                 let ictx'' :: ICtx
ictx''   = ICtx
ictx' { icSolved :: HashSet Expr
icSolved = ICtx -> HashSet Expr
icSolved ICtx
ictx HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Semigroup a => a -> a -> a
<> HashSet Expr
oks 
                                                      , icEquals :: EvAccum
icEquals = ICtx -> EvAccum
icEquals ICtx
ictx EvAccum -> EvAccum -> EvAccum
forall a. Semigroup a => a -> a -> a
<> EvAccum
us'
                                                      , icAssms :: HashSet Expr
icAssms  = (Expr -> Bool) -> HashSet Expr -> HashSet Expr
forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isTautoPred) HashSet Expr
eqsSMT }
                                 let newcands :: [Expr]
newcands = [[Expr]] -> [Expr]
forall a. Monoid a => [a] -> a
mconcat (Knowledge -> ICtx -> Expr -> [Expr]
makeCandidates Knowledge
γ ICtx
ictx'' (Expr -> [Expr]) -> [Expr] -> [[Expr]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList (HashSet Expr
cands HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Semigroup a => a -> a -> a
<> ((Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd ((Expr, Expr) -> Expr) -> EvAccum -> HashSet Expr
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
us)))
                                 ICtx -> Int -> IO ICtx
go (ICtx
ictx'' { icCands :: HashSet Expr
icCands = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Expr]
newcands}) (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
                                 
evalOneCandStep :: Knowledge -> EvalEnv -> Int -> (ICtx, [EvAccum]) -> Expr -> IO (ICtx, [EvAccum])
evalOneCandStep :: Knowledge
-> EvalEnv
-> Int
-> (ICtx, [EvAccum])
-> Expr
-> IO (ICtx, [EvAccum])
evalOneCandStep Knowledge
γ EvalEnv
env' Int
i (ICtx
ictx, [EvAccum]
acc) Expr
e = do
  (EvAccum
res, FuelCount
fm) <- Knowledge
-> EvalEnv -> ICtx -> Int -> Expr -> IO (EvAccum, FuelCount)
evalOne Knowledge
γ EvalEnv
env' ICtx
ictx Int
i Expr
e
  (ICtx, [EvAccum]) -> IO (ICtx, [EvAccum])
forall (m :: * -> *) a. Monad m => a -> m a
return (ICtx
ictx { icFuel :: FuelCount
icFuel = FuelCount
fm}, EvAccum
res EvAccum -> [EvAccum] -> [EvAccum]
forall a. a -> [a] -> [a]
: [EvAccum]
acc)

rewrite :: Expr -> Map Symbol [Rewrite] -> [(Expr,Expr)] 
rewrite :: Expr -> Map Symbol [Rewrite] -> [(Expr, Expr)]
rewrite Expr
e Map Symbol [Rewrite]
rwEnv = [[(Expr, Expr)]] -> [(Expr, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Expr, Expr)]] -> [(Expr, Expr)])
-> [[(Expr, Expr)]] -> [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ (Expr -> [(Expr, Expr)]) -> [Expr] -> [[(Expr, Expr)]]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Map Symbol [Rewrite] -> [(Expr, Expr)]
`rewriteTop` Map Symbol [Rewrite]
rwEnv) (Expr -> [Expr]
notGuardedApps Expr
e)

rewriteTop :: Expr -> Map Symbol [Rewrite] -> [(Expr,Expr)]
rewriteTop :: Expr -> Map Symbol [Rewrite] -> [(Expr, Expr)]
rewriteTop Expr
e Map Symbol [Rewrite]
rwEnv =
  [ (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))
  | (EVar Symbol
f, [Expr]
es) <- [Expr -> (Expr, [Expr])
splitEApp Expr
e]
  , Just [Rewrite]
rws <- [Symbol -> Map Symbol [Rewrite] -> Maybe [Rewrite]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
f Map Symbol [Rewrite]
rwEnv]
  , Rewrite
rw <- [Rewrite]
rws
  , [Expr] -> 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 (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
  ]

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

resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo :: 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 String -> SymEnv -> Expr -> Expr
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (SrcSpan -> String -> Located String
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan (String
"PLE1 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
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 
  { InstEnv a -> Config
ieCfg   :: !Config
  , InstEnv a -> Context
ieSMT   :: !SMT.Context
  , InstEnv a -> BindEnv
ieBEnv  :: !BindEnv
  , InstEnv a -> AxiomEnv
ieAenv  :: !AxiomEnv 
  , InstEnv a -> CMap (SimpC a)
ieCstrs :: !(CMap (SimpC a))
  , InstEnv a -> Knowledge
ieKnowl :: !Knowledge
  , 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 -> EvAccum
icEquals   :: EvAccum                   -- ^ Accumulated equalities
  , ICtx -> HashSet Expr
icSolved   :: S.HashSet Expr            -- ^ Terms that we have already expanded
  , ICtx -> ConstMap
icSimpl    :: !ConstMap                 -- ^ Map of expressions to constants
  , ICtx -> Maybe SubcId
icSubcId   :: Maybe SubcId              -- ^ Current subconstraint ID
  , ICtx -> FuelCount
icFuel     :: !FuelCount                -- ^ Current fuel-count
  , ICtx -> HashSet Expr
icANFs     :: S.HashSet Pred            -- 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

initCtx :: InstEnv a -> [(Expr,Expr)] -> ICtx
initCtx :: InstEnv a -> [(Expr, Expr)] -> ICtx
initCtx InstEnv a
env [(Expr, Expr)]
es   = ICtx :: HashSet Expr
-> HashSet Expr
-> EvAccum
-> HashSet Expr
-> ConstMap
-> Maybe SubcId
-> FuelCount
-> HashSet Expr
-> ICtx
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 :: EvAccum
icEquals = [(Expr, Expr)] -> EvAccum
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [(Expr, Expr)]
es
  , icSolved :: HashSet Expr
icSolved = HashSet Expr
forall a. Monoid a => a
mempty
  , icSimpl :: ConstMap
icSimpl  = ConstMap
forall a. Monoid a => a
mempty 
  , icSubcId :: Maybe SubcId
icSubcId = Maybe SubcId
forall a. Maybe a
Nothing
  , icFuel :: FuelCount
icFuel   = EvalEnv -> FuelCount
evFuel (InstEnv a -> EvalEnv
forall a. InstEnv a -> EvalEnv
ieEvEnv InstEnv a
env)
  , icANFs :: HashSet Expr
icANFs   = HashSet Expr
forall a. Monoid a => a
mempty
  }

equalitiesPred :: S.HashSet (Expr, Expr) -> [Expr]
equalitiesPred :: EvAccum -> [Expr]
equalitiesPred EvAccum
eqs = [ Expr -> Expr -> Expr
EEq Expr
e1 Expr
e2 | (Expr
e1, Expr
e2) <- EvAccum -> [(Expr, Expr)]
forall a. HashSet a -> [a]
S.toList EvAccum
eqs, Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2 ] 

updCtxRes :: InstRes -> Maybe BindId -> ICtx -> (ICtx, InstRes) 
updCtxRes :: InstRes -> Maybe Int -> ICtx -> (ICtx, InstRes)
updCtxRes InstRes
res Maybe Int
iMb ICtx
ctx = (ICtx
ctx, InstRes
res')
  where 
    res' :: InstRes
res' = InstRes -> Maybe Int -> Expr -> InstRes
updRes InstRes
res Maybe Int
iMb ([Expr] -> Expr
pAnd ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ EvAccum -> [Expr]
equalitiesPred (EvAccum -> [Expr]) -> EvAccum -> [Expr]
forall a b. (a -> b) -> a -> b
$ ICtx -> EvAccum
icEquals ICtx
ctx)


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 (String -> Expr -> Expr -> Expr
forall a. HasCallStack => String -> a
error String
"tree-like invariant broken in ple. See https://github.com/ucsd-progsys/liquid-fixpoint/issues/496") Int
i Expr
e InstRes
res
updRes InstRes
res  Maybe Int
Nothing Expr
_ = InstRes
res 

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

updCtx :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> ICtx
updCtx :: InstEnv a -> ICtx -> [Int] -> Maybe SubcId -> ICtx
updCtx InstEnv {CMap (SimpC a)
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..} ICtx
ctx [Int]
delta Maybe SubcId
cidMb 
              = ICtx
ctx { icAssms :: HashSet Expr
icAssms  = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isTautoPred) [Expr]
ctxEqs)  
                    , icCands :: HashSet Expr
icCands  = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Expr]
cands           HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Semigroup a => a -> a -> a
<> ICtx -> HashSet Expr
icCands  ICtx
ctx
                    , icEquals :: EvAccum
icEquals = EvAccum
initEqs                    EvAccum -> EvAccum -> EvAccum
forall a. Semigroup a => a -> a -> a
<> ICtx -> EvAccum
icEquals ICtx
ctx
                    , icSimpl :: ConstMap
icSimpl  = [(Expr, Expr)] -> ConstMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (EvAccum -> [(Expr, Expr)]
forall a. HashSet a -> [a]
S.toList EvAccum
sims) ConstMap -> ConstMap -> ConstMap
forall a. Semigroup a => a -> a -> a
<> ICtx -> ConstMap
icSimpl ICtx
ctx ConstMap -> ConstMap -> ConstMap
forall a. Semigroup a => a -> a -> a
<> ConstMap
econsts
                    , icSubcId :: Maybe SubcId
icSubcId = Maybe SubcId
cidMb
                    , icANFs :: HashSet Expr
icANFs   = HashSet Expr
anfs HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Semigroup a => a -> a -> a
<> ICtx -> HashSet Expr
icANFs ICtx
ctx
                    }
  where         
    initEqs :: EvAccum
initEqs   = [(Expr, Expr)] -> EvAccum
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Expr, Expr)] -> EvAccum) -> [(Expr, Expr)] -> EvAccum
forall a b. (a -> b) -> a -> b
$ [[(Expr, Expr)]] -> [(Expr, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Expr -> Map Symbol [Rewrite] -> [(Expr, Expr)]
rewrite Expr
e (Knowledge -> Map Symbol [Rewrite]
knSims Knowledge
ieKnowl) | Expr
e  <- [Expr]
cands]
    anfs :: HashSet Expr
anfs      = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT String
"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 [ (Symbol, SortedReft) -> Expr
forall a. Expression a => a -> Expr
expr (Symbol, SortedReft)
xr | (Symbol, SortedReft)
xr <- [(Symbol, SortedReft)]
bs ])
    cands :: [Expr]
cands     = (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Knowledge -> ICtx -> Expr -> [Expr]
makeCandidates Knowledge
ieKnowl ICtx
ctx) (Expr
rhsExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
es)
    sims :: EvAccum
sims      = ((Expr, Expr) -> Bool) -> EvAccum -> EvAccum
forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter (HashSet Symbol -> (Expr, Expr) -> Bool
isSimplification (Knowledge -> HashSet Symbol
knDCs Knowledge
ieKnowl)) (EvAccum
initEqs EvAccum -> EvAccum -> EvAccum
forall a. Semigroup a => a -> a -> a
<> ICtx -> EvAccum
icEquals ICtx
ctx)
    econsts :: ConstMap
econsts   = [(Expr, Expr)] -> ConstMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Expr, Expr)] -> ConstMap) -> [(Expr, Expr)] -> ConstMap
forall a b. (a -> b) -> a -> b
$ Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants Knowledge
ieKnowl [Expr]
es
    ctxEqs :: [Expr]
ctxEqs    = String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT String
"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]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                  [ EvAccum -> [Expr]
equalitiesPred EvAccum
initEqs 
                  , EvAccum -> [Expr]
equalitiesPred EvAccum
sims 
                  , EvAccum -> [Expr]
equalitiesPred (ICtx -> EvAccum
icEquals ICtx
ctx)
                  , [ (Symbol, SortedReft) -> Expr
forall a. Expression a => a -> Expr
expr (Symbol, SortedReft)
xr   | xr :: (Symbol, SortedReft)
xr@(Symbol
_, SortedReft
r) <- [(Symbol, SortedReft)]
bs, [KVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [KVar]
Vis.kvarsExpr (Expr -> [KVar]) -> Expr -> [KVar]
forall a b. (a -> b) -> a -> b
$ Reft -> Expr
reftPred (Reft -> Expr) -> Reft -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
r) ]
                  ])
    bs :: [(Symbol, SortedReft)]
bs        = (SortedReft -> SortedReft)
-> (Symbol, SortedReft) -> (Symbol, SortedReft)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SortedReft -> SortedReft
unElabSortedReft ((Symbol, SortedReft) -> (Symbol, SortedReft))
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds
    (Expr
rhs:[Expr]
es)  = Expr -> Expr
unElab (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr
eRhs Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: ((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)]
binds))
    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     = [ Int -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv Int
i BindEnv
ieBEnv | Int
i <- [Int]
delta ]
    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 ]

makeCandidates :: Knowledge -> ICtx -> Expr -> [Expr]
makeCandidates :: Knowledge -> ICtx -> Expr -> [Expr]
makeCandidates Knowledge
γ ICtx
ctx Expr
expr 
  = String -> [Expr] -> [Expr]
forall a. PPrint a => String -> a -> a
mytracepp (String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
cands) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" New Candidates") [Expr]
cands
  where 
    cands :: [Expr]
cands = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Expr
e -> Knowledge -> Expr -> Bool
isRedex Knowledge
γ Expr
e Bool -> Bool -> Bool
&& Bool -> Bool
not (Expr
e Expr -> HashSet Expr -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` ICtx -> HashSet Expr
icSolved ICtx
ctx)) (Expr -> [Expr]
notGuardedApps Expr
expr)

isRedex :: Knowledge -> Expr -> Bool 
isRedex :: Knowledge -> Expr -> Bool
isRedex Knowledge
γ Expr
e = Knowledge -> Expr -> Bool
isGoodApp Knowledge
γ Expr
e Bool -> Bool -> Bool
|| Expr -> Bool
isIte Expr
e 
  where 
    isIte :: Expr -> Bool
isIte EIte {} = Bool
True 
    isIte Expr
_       = Bool
False 


isGoodApp :: Knowledge -> Expr -> Bool 
isGoodApp :: Knowledge -> Expr -> Bool
isGoodApp Knowledge
γ Expr
e 
  | (EVar Symbol
f, [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
e
  , Just Int
i       <- Symbol -> [(Symbol, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
f (Knowledge -> [(Symbol, Int)]
knSummary Knowledge
γ)
  = [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
i
  | Bool
otherwise
  = Bool
False 
    



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

isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr :: 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 EvAccum = S.HashSet (Expr, Expr)

--------------------------------------------------------------------------------
data EvalEnv = EvalEnv
  { EvalEnv -> SymEnv
evEnv      :: !SymEnv
  , EvalEnv -> EvAccum
evAccum    :: EvAccum
  , EvalEnv -> FuelCount
evFuel     :: FuelCount

  -- REST parameters
  , EvalEnv -> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
explored   :: Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
  , EvalEnv -> Maybe SolverHandle
restSolver :: Maybe SolverHandle
  }

data FuelCount = FC 
  { FuelCount -> HashMap Symbol Int
fcMap :: M.HashMap Symbol Int
  , FuelCount -> Maybe Int
fcMax :: Maybe Int
  } 
  deriving (Int -> FuelCount -> String -> String
[FuelCount] -> String -> String
FuelCount -> String
(Int -> FuelCount -> String -> String)
-> (FuelCount -> String)
-> ([FuelCount] -> String -> String)
-> Show FuelCount
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [FuelCount] -> String -> String
$cshowList :: [FuelCount] -> String -> String
show :: FuelCount -> String
$cshow :: FuelCount -> String
showsPrec :: Int -> FuelCount -> String -> String
$cshowsPrec :: Int -> FuelCount -> String -> String
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
γ

evalOne :: Knowledge -> EvalEnv -> ICtx -> Int -> Expr -> IO (EvAccum, FuelCount)
evalOne :: Knowledge
-> EvalEnv -> ICtx -> Int -> Expr -> IO (EvAccum, FuelCount)
evalOne Knowledge
γ EvalEnv
env 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 (t :: * -> *) a. Foldable t => t a -> Bool
null (Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx) = do
    ((Expr
e', FinalExpand
_), EvalEnv
st) <- StateT EvalEnv IO (Expr, FinalExpand)
-> EvalEnv -> IO ((Expr, FinalExpand), EvalEnv)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
NoRW Expr
e) (EvalEnv
env { evFuel :: FuelCount
evFuel = ICtx -> FuelCount
icFuel ICtx
ctx })
    let evAcc' :: EvAccum
evAcc' = if (String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalOne: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e) Expr
e') Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e then EvalEnv -> EvAccum
evAccum EvalEnv
st else (Expr, Expr) -> EvAccum -> EvAccum
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Expr
e, Expr
e') (EvalEnv -> EvAccum
evAccum EvalEnv
st)
    (EvAccum, FuelCount) -> IO (EvAccum, FuelCount)
forall (m :: * -> *) a. Monad m => a -> m a
return (EvAccum
evAcc', EvalEnv -> FuelCount
evFuel EvalEnv
st) 
evalOne Knowledge
γ EvalEnv
env ICtx
ctx Int
_ Expr
e | Bool
otherwise = do
  EvalEnv
env' <- StateT EvalEnv IO () -> EvalEnv -> IO EvalEnv
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Knowledge -> ICtx -> RESTParams (OCType Op) -> StateT EvalEnv IO ()
evalREST Knowledge
γ ICtx
ctx RESTParams (OCType Op)
rp) (EvalEnv
env { evFuel :: FuelCount
evFuel = ICtx -> FuelCount
icFuel ICtx
ctx })
  (EvAccum, FuelCount) -> IO (EvAccum, FuelCount)
forall (m :: * -> *) a. Monad m => a -> m a
return (EvalEnv -> EvAccum
evAccum EvalEnv
env', EvalEnv -> FuelCount
evFuel EvalEnv
env')
  where
    oc :: AbstractOC (OCType Op) Expr IO
    oc :: AbstractOC (OCType Op) Expr IO
oc = SolverHandle -> AbstractOC (OCType Op) Expr IO
ordConstraints (Maybe SolverHandle -> SolverHandle
forall a. HasCallStack => Maybe a -> a
Mb.fromJust (Maybe SolverHandle -> SolverHandle)
-> Maybe SolverHandle -> SolverHandle
forall a b. (a -> b) -> a -> b
$ EvalEnv -> Maybe SolverHandle
restSolver EvalEnv
env)

    rp :: RESTParams (OCType Op)
rp = AbstractOC (OCType Op) Expr IO
-> [(Expr, TermOrigin)] -> OCType Op -> RESTParams (OCType Op)
forall oc.
AbstractOC oc Expr IO
-> [(Expr, TermOrigin)] -> oc -> RESTParams oc
RP AbstractOC (OCType Op) Expr IO
oc [(Expr
e, TermOrigin
PLE)] OCType Op
constraints
    constraints :: OCType Op
constraints = (OCType Op -> (Expr, Expr) -> OCType Op)
-> OCType Op -> [(Expr, Expr)] -> OCType Op
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OCType Op -> (Expr, Expr) -> OCType Op
go (AbstractOC (OCType Op) Expr IO -> OCType Op
forall c a (m :: * -> *). AbstractOC c a m -> c
OC.top AbstractOC (OCType Op) Expr IO
oc) []
      where
        go :: OCType Op -> (Expr, Expr) -> OCType Op
go OCType Op
c (Expr
t, Expr
u) = AbstractOC (OCType Op) Expr IO
-> OCType Op -> Expr -> Expr -> OCType Op
forall c a (m :: * -> *). AbstractOC c a m -> c -> a -> a -> c
refine AbstractOC (OCType Op) Expr IO
oc OCType Op
c Expr
t Expr
u


-- | @notGuardedApps e@ yields all the subexpressions that are
-- applications not under an if-then-else, lambda abstraction, type abstraction,
-- type application, or quantifier.
notGuardedApps :: Expr -> [Expr]
notGuardedApps :: Expr -> [Expr]
notGuardedApps = Expr -> [Expr]
go 
  where 
    go :: Expr -> [Expr]
go e :: Expr
e@(EApp Expr
e1 Expr
e2)  = [Expr
e] [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e1 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (PAnd [Expr]
es)       = (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
go [Expr]
es
    go (POr [Expr]
es)        = (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
go [Expr]
es
    go (PAtom Brel
_ Expr
e1 Expr
e2) = Expr -> [Expr]
go Expr
e1  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (PIff Expr
e1 Expr
e2)    = Expr -> [Expr]
go Expr
e1  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (PImp Expr
e1 Expr
e2)    = Expr -> [Expr]
go Expr
e1  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2 
    go (EBin  Bop
_ Expr
e1 Expr
e2) = Expr -> [Expr]
go Expr
e1  [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (PNot Expr
e)        = Expr -> [Expr]
go Expr
e
    go (ENeg Expr
e)        = Expr -> [Expr]
go Expr
e
    go e :: Expr
e@(EIte Expr
b Expr
_ Expr
_)  = Expr -> [Expr]
go Expr
b [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr
e] -- ++ go e1 ++ go e2  
    go (ECoerc Sort
_ Sort
_ Expr
e)  = Expr -> [Expr]
go Expr
e 
    go (ECst Expr
e Sort
_)      = Expr -> [Expr]
go Expr
e 
    go (ESym SymConst
_)        = []
    go (ECon Constant
_)        = []
    go (EVar Symbol
_)        = []
    go (ELam (Symbol, Sort)
_ Expr
_)      = []
    go (ETApp Expr
_ Sort
_)     = []
    go (ETAbs Expr
_ Symbol
_)     = []
    go (PKVar KVar
_ Subst
_)     = []
    go (PAll [(Symbol, Sort)]
_ Expr
_)      = []
    go (PExist [(Symbol, Sort)]
_ Expr
_)    = []
    go (PGrad{})       = []



-- 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
/= :: EvalType -> EvalType -> Bool
$c/= :: EvalType -> EvalType -> Bool
== :: EvalType -> EvalType -> Bool
$c== :: EvalType -> EvalType -> Bool
Eq)

-- Indicates whether or not the evaluation has expanded a function statement
-- into a conditional branch.
-- In this case, rewriting should stop
-- It's unclear whether or not rewriting in either branch makes sense,
-- since one branch could be an ill-formed expression.
newtype FinalExpand = FE Bool deriving (Int -> FinalExpand -> String -> String
[FinalExpand] -> String -> String
FinalExpand -> String
(Int -> FinalExpand -> String -> String)
-> (FinalExpand -> String)
-> ([FinalExpand] -> String -> String)
-> Show FinalExpand
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [FinalExpand] -> String -> String
$cshowList :: [FinalExpand] -> String -> String
show :: FinalExpand -> String
$cshow :: FinalExpand -> String
showsPrec :: Int -> FinalExpand -> String -> String
$cshowsPrec :: Int -> FinalExpand -> String -> String
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
$ (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bool -> Bool
forall a. a -> a
id ((FinalExpand -> Bool) -> [FinalExpand] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map FinalExpand -> Bool
feVal [FinalExpand]
xs)

(<|>) :: 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 expressions using rewrites and equations.
--
-- 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 folds constants.
--
-- Also adds to the monad state all the subexpressions that have been rewritten
-- as pairs @(original_subexpression, rewritten_subexpression)@.
--
eval :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand)
eval :: Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
_ ICtx
ctx EvalType
_ Expr
e
  | Just Expr
v <- Expr -> ConstMap -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Expr
e (ICtx -> ConstMap
icSimpl ICtx
ctx)
  = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
v, FinalExpand
noExpand)
  
eval Knowledge
γ ICtx
ctx EvalType
et Expr
e =
  do [(Expr, Expr)]
acc <- (EvalEnv -> [(Expr, Expr)]) -> StateT EvalEnv IO [(Expr, Expr)]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (EvAccum -> [(Expr, Expr)]
forall a. HashSet a -> [a]
S.toList (EvAccum -> [(Expr, Expr)])
-> (EvalEnv -> EvAccum) -> EvalEnv -> [(Expr, Expr)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalEnv -> EvAccum
evAccum)
     case Expr -> [(Expr, Expr)] -> Maybe Expr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Expr
e [(Expr, Expr)]
acc of
        -- If rewriting, don't lookup, as evAccum may contain loops
        Just Expr
e' | [AutoRewrite] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx) -> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
e'
        Maybe Expr
_ -> do
          (Expr
e0', FinalExpand
fe)  <- Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go Expr
e
          let e' :: Expr
e' = Knowledge -> ICtx -> Expr -> Expr
forall a. Simplifiable a => Knowledge -> ICtx -> a -> a
simplify Knowledge
γ ICtx
ctx Expr
e0'
          if Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e' 
            then
              case EvalType
et of
                EvalType
NoRW -> do
                  (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st { evAccum :: EvAccum
evAccum = (Expr, Expr) -> EvAccum -> EvAccum
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert ((Expr, Expr) -> (Expr, Expr)
traceE (Expr
e, Expr
e')) (EvalEnv -> EvAccum
evAccum EvalEnv
st) })
                  (Expr
e'',  FinalExpand
fe') <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ((Expr, Expr) -> ICtx -> ICtx
addConst (Expr
e,Expr
e') ICtx
ctx) EvalType
et Expr
e'
                  (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e'', FinalExpand
fe FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe')
                EvalType
_ -> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e', FinalExpand
fe)
            else 
              (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, FinalExpand
fe)
  where
    addConst :: (Expr, Expr) -> ICtx -> ICtx
addConst (Expr
e,Expr
e') ICtx
ctx = if HashSet Symbol -> Expr -> Bool
isConstant (Knowledge -> HashSet Symbol
knDCs Knowledge
γ) Expr
e'
                           then ICtx
ctx { icSimpl :: ConstMap
icSimpl = Expr -> Expr -> ConstMap -> ConstMap
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Expr
e Expr
e' (ConstMap -> ConstMap) -> ConstMap -> ConstMap
forall a b. (a -> b) -> a -> b
$ ICtx -> ConstMap
icSimpl ICtx
ctx} else ICtx
ctx 
    go :: Expr -> StateT EvalEnv IO (Expr, FinalExpand)
go (ELam (Symbol
x,Sort
s) Expr
e)   = (Expr -> Expr) -> (Expr, FinalExpand) -> (Expr, FinalExpand)
mapFE ((Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
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
<$> Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ' ICtx
ctx EvalType
et Expr
e where γ' :: Knowledge
γ' = Knowledge
γ { knLams :: [(Symbol, Sort)]
knLams = (Symbol
x, Sort
s) (Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
: Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ }
    go (EIte Expr
b Expr
e1 Expr
e2) = Knowledge
-> ICtx
-> EvalType
-> Expr
-> Expr
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
b Expr
e1 Expr
e2
    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])
splitEApp 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)
mapM (Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et) [Expr]
es
            (Expr, FinalExpand)
r <- if [Expr]
es [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Expr]
es'
              then (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
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
                (Expr
e', FinalExpand
fe') <- Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> StateT EvalEnv IO (Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx Expr
f' [Expr]
es EvalType
et
                (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr
e', FinalExpand
fe FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe')
            (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr, FinalExpand)
r
       (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)
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)
            (Expr
e', FinalExpand
fe') <- Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> StateT EvalEnv IO (Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx Expr
f' [Expr]
es' EvalType
et
            (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr
e', FinalExpand
fe FinalExpand -> FinalExpand -> FinalExpand
<|> FinalExpand
fe')

    go e :: Expr
e@(PAtom Brel
r Expr
e1 Expr
e2) = Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
evalBoolOr Expr
e ((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 (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ ((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 (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) -> Sort -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip 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) -> Symbol -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 e :: Expr
e@(PNot Expr
e')      = Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
evalBoolOr 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 e :: Expr
e@(PImp Expr
e1 Expr
e2)   = Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
evalBoolOr Expr
e ((Expr -> Expr -> Expr)
-> Expr -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
PImp Expr
e1 Expr
e2)
    go e :: Expr
e@(PIff Expr
e1 Expr
e2)   = Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
evalBoolOr Expr
e ((Expr -> Expr -> Expr)
-> Expr -> Expr -> StateT EvalEnv IO (Expr, FinalExpand)
binOp Expr -> Expr -> Expr
PIff Expr
e1 Expr
e2)
    go e :: Expr
e@(PAnd [Expr]
es)      = Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
evalBoolOr Expr
e (([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 (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [Expr]
es))
    go e :: Expr
e@(POr [Expr]
es)       = Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
evalBoolOr Expr
e (([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 (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [Expr]
es))
    go Expr
e                = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
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 (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 (m :: * -> *) a. Monad m => a -> m a
return ([Expr] -> a
f [Expr]
xs', FinalExpand
fe)

    evalBoolOr :: Expr -> EvalST (Expr, FinalExpand) -> EvalST (Expr, FinalExpand)
    evalBoolOr :: Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO (Expr, FinalExpand)
evalBoolOr Expr
ee StateT EvalEnv IO (Expr, FinalExpand)
fallback = do
      Maybe Expr
b <- Knowledge -> Expr -> EvalST (Maybe Expr)
evalBool Knowledge
γ Expr
ee
      case Maybe Expr
b of
        Just Expr
r  -> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
r, FinalExpand
noExpand)
        Maybe Expr
Nothing -> StateT EvalEnv IO (Expr, FinalExpand)
fallback

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

getANFSubs :: Expr -> [(Symbol, Expr)]
getANFSubs :: Expr -> [(Symbol, Expr)]
getANFSubs (PAnd [Expr]
es)                                   = (Expr -> [(Symbol, Expr)]) -> [Expr] -> [(Symbol, Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [(Symbol, Expr)]
getANFSubs [Expr]
es
getANFSubs (EEq Expr
lhs Expr
rhs) | (EVar Symbol
v) <- Expr -> Expr
unElab Expr
lhs
                           , Symbol
anfPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
v = [(Symbol
v, Expr -> Expr
unElab Expr
rhs)]
getANFSubs (EEq Expr
lhs Expr
rhs) | (EVar Symbol
v) <- Expr -> Expr
unElab Expr
rhs
                           , Symbol
anfPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
v = [(Symbol
v, Expr -> Expr
unElab Expr
lhs)]
getANFSubs Expr
_                                           = []

-- Reverse the ANF transformation
deANF :: ICtx -> Expr -> Expr
deANF :: ICtx -> Expr -> Expr
deANF ICtx
ctx Expr
e = Expr -> Expr
forall t. (Eq t, Subable t) => t -> t
subst' Expr
e where
  ints :: [(Symbol, Expr)]
ints  = (Expr -> [(Symbol, Expr)]) -> [Expr] -> [(Symbol, Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [(Symbol, Expr)]
getANFSubs (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
icANFs ICtx
ctx)
  ints' :: [(Symbol, Expr)]
ints' = ([(Symbol, Expr)] -> (Symbol, Expr))
-> [[(Symbol, Expr)]] -> [(Symbol, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map [(Symbol, Expr)] -> (Symbol, Expr)
forall a. [(a, Expr)] -> (a, Expr)
go (((Symbol, Expr) -> (Symbol, Expr) -> Bool)
-> [(Symbol, Expr)] -> [[(Symbol, Expr)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
L.groupBy (\(Symbol, Expr)
x (Symbol, Expr)
y -> (Symbol, Expr) -> Symbol
forall a b. (a, b) -> a
fst (Symbol, Expr)
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== (Symbol, Expr) -> Symbol
forall a b. (a, b) -> a
fst (Symbol, Expr)
y) ([(Symbol, Expr)] -> [[(Symbol, Expr)]])
-> [(Symbol, Expr)] -> [[(Symbol, Expr)]]
forall a b. (a -> b) -> a -> b
$ ((Symbol, Expr) -> Symbol) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
L.sortOn (Symbol, Expr) -> Symbol
forall a b. (a, b) -> a
fst ([(Symbol, Expr)] -> [(Symbol, Expr)])
-> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. Eq a => [a] -> [a]
L.nub [(Symbol, Expr)]
ints) where
    go :: [(a, Expr)] -> (a, Expr)
go ([(a
t, Expr
u)]) = (a
t, Expr
u)
    go [(a, Expr)]
ts         = ((a, Expr) -> a
forall a b. (a, b) -> a
fst ([(a, Expr)] -> (a, Expr)
forall a. [a] -> a
head [(a, Expr)]
ts), [Expr] -> Expr
getBest (((a, Expr) -> Expr) -> [(a, Expr)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (a, Expr) -> Expr
forall a b. (a, b) -> b
snd [(a, Expr)]
ts))
  su :: Subst
su          = HashMap Symbol Expr -> Subst
Su ([(Symbol, Expr)] -> HashMap Symbol Expr
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Symbol, Expr)]
ints')
  subst' :: t -> t
subst' t
ee =
    let
      ee' :: t
ee' = Subst -> t -> t
forall a. Subable a => Subst -> a -> a
subst Subst
su t
ee
    in
      if t
ee t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
ee'
        then t
ee
        else t -> t
subst' t
ee'

  getBest :: [Expr] -> Expr
getBest [Expr]
ts | Just Expr
t <- (Expr -> Bool) -> [Expr] -> Maybe Expr
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find Expr -> Bool
isVar [Expr]
ts = Expr
t
    where
      -- Hack : Vars starting with ds_ are probably constants
      isVar :: Expr -> Bool
isVar (EVar Symbol
t) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Bool
Tx.isPrefixOf Text
"ds_" (Symbol -> Text
symbolText Symbol
t)
      isVar Expr
_        = Bool
False

  -- If the only match is a ds_ var, use it
  getBest [Expr]
ts | Just Expr
t <- (Expr -> Bool) -> [Expr] -> Maybe Expr
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find Expr -> Bool
isVar [Expr]
ts = Expr
t
    where
      isVar :: Expr -> Bool
isVar (EVar Symbol
_) = Bool
True
      isVar Expr
_        = Bool
False

  getBest [Expr]
ts | Bool
otherwise = [Expr] -> Expr
forall a. [a] -> a
head [Expr]
ts

-- |
-- 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 Op) -> EvalST ()
evalREST :: Knowledge -> ICtx -> RESTParams (OCType Op) -> StateT EvalEnv IO ()
evalREST Knowledge
_ ICtx
ctx RESTParams (OCType Op)
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 (String -> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. PPrint a => String -> a -> a
mytracepp String
"EVAL1: path" ([(Expr, TermOrigin)] -> [(Expr, TermOrigin)])
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a b. (a -> b) -> a -> b
$ RESTParams (OCType Op) -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams (OCType Op)
rp)
  , Expr
e         <- [Expr] -> Expr
forall a. [a] -> a
last [Expr]
pathExprs
  , Just Expr
v    <- Expr -> ConstMap -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Expr
e (ICtx -> ConstMap
icSimpl ICtx
ctx)
  = 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 { evAccum :: EvAccum
evAccum = (Expr, Expr) -> EvAccum -> EvAccum
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Expr
e, Expr
v) (EvalEnv -> EvAccum
evAccum EvalEnv
st)})
        
evalREST Knowledge
γ ICtx
ctx RESTParams (OCType Op)
rp =
  do
    Just ExploredTerms RuntimeTerm (OCType Op) IO
exploredTerms <- (EvalEnv -> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO))
-> StateT
     EvalEnv IO (Maybe (ExploredTerms RuntimeTerm (OCType Op) IO))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
explored
    Bool
se <- IO Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (ExploredTerms RuntimeTerm (OCType Op) IO -> Expr -> IO Bool
forall (m :: * -> *).
Monad m =>
ExploredTerms RuntimeTerm (OCType Op) m -> Expr -> m Bool
shouldExploreTerm ExploredTerms RuntimeTerm (OCType Op) IO
exploredTerms Expr
e)
    Bool -> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
se (StateT EvalEnv IO () -> StateT EvalEnv IO ())
-> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$ do
      [(Expr, OCType Op)]
possibleRWs <- StateT EvalEnv IO [(Expr, OCType Op)]
getRWs
      [(Expr, OCType Op)]
rws <- ExploredTerms RuntimeTerm (OCType Op) IO
-> [(Expr, OCType Op)] -> [(Expr, OCType Op)]
forall c (m :: * -> *) b.
ExploredTerms RuntimeTerm c m -> [(Expr, b)] -> [(Expr, b)]
notVisitedFirst ExploredTerms RuntimeTerm (OCType Op) IO
exploredTerms ([(Expr, OCType Op)] -> [(Expr, OCType Op)])
-> StateT EvalEnv IO [(Expr, OCType Op)]
-> StateT EvalEnv IO [(Expr, OCType Op)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Expr, OCType Op) -> StateT EvalEnv IO Bool)
-> [(Expr, OCType Op)] -> StateT EvalEnv IO [(Expr, OCType Op)]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM (IO Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> StateT EvalEnv IO Bool)
-> ((Expr, OCType Op) -> IO Bool)
-> (Expr, OCType Op)
-> StateT EvalEnv IO Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, OCType Op) -> IO Bool
allowed) [(Expr, OCType Op)]
possibleRWs
      (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 (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, OCType Op) -> Expr) -> [(Expr, OCType Op)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, OCType Op) -> Expr
forall a b. (a, b) -> a
fst [(Expr, OCType Op)]
rws
      let evAccum' :: EvAccum
evAccum'      = [(Expr, Expr)] -> EvAccum
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(Expr, Expr)] -> EvAccum) -> [(Expr, Expr)] -> EvAccum
forall a b. (a -> b) -> a -> b
$ (Expr -> (Expr, Expr)) -> [Expr] -> [(Expr, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (Expr
e,) ([Expr] -> [(Expr, Expr)]) -> [Expr] -> [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ [Expr]
exprsToAdd

      (EvalEnv -> EvalEnv) -> StateT EvalEnv IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st ->
                EvalEnv
st {
                  evAccum :: EvAccum
evAccum  = EvAccum -> EvAccum -> EvAccum
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union EvAccum
evAccum' (EvalEnv -> EvAccum
evAccum EvalEnv
st)
                , explored :: Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
explored = ExploredTerms RuntimeTerm (OCType Op) IO
-> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
forall a. a -> Maybe a
Just (ExploredTerms RuntimeTerm (OCType Op) IO
 -> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO))
-> ExploredTerms RuntimeTerm (OCType Op) IO
-> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
forall a b. (a -> b) -> a -> b
$ RuntimeTerm
-> OCType Op
-> HashSet RuntimeTerm
-> ExploredTerms RuntimeTerm (OCType Op) IO
-> ExploredTerms RuntimeTerm (OCType Op) IO
forall term c (m :: * -> *).
(Eq term, Hashable term) =>
term
-> c
-> HashSet term
-> ExploredTerms term c m
-> ExploredTerms term c m
ET.insert
                  (Expr -> RuntimeTerm
convert Expr
e)
                  (RESTParams (OCType Op) -> OCType Op
forall oc. RESTParams oc -> oc
c RESTParams (OCType Op)
rp)
                  (RuntimeTerm -> HashSet RuntimeTerm -> HashSet RuntimeTerm
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (Expr -> RuntimeTerm
convert Expr
e') (HashSet RuntimeTerm -> HashSet RuntimeTerm)
-> HashSet RuntimeTerm -> HashSet RuntimeTerm
forall a b. (a -> b) -> a -> b
$ [RuntimeTerm] -> HashSet RuntimeTerm
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (((Expr, OCType Op) -> RuntimeTerm)
-> [(Expr, OCType Op)] -> [RuntimeTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> RuntimeTerm
convert (Expr -> RuntimeTerm)
-> ((Expr, OCType Op) -> Expr) -> (Expr, OCType Op) -> RuntimeTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr, OCType Op) -> Expr
forall a b. (a, b) -> a
fst) [(Expr, OCType Op)]
possibleRWs))
                  (Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
-> ExploredTerms RuntimeTerm (OCType Op) IO
forall a. HasCallStack => Maybe a -> a
Mb.fromJust (Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
 -> ExploredTerms RuntimeTerm (OCType Op) IO)
-> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
-> ExploredTerms RuntimeTerm (OCType Op) IO
forall a b. (a -> b) -> a -> b
$ EvalEnv -> Maybe (ExploredTerms RuntimeTerm (OCType Op) IO)
explored EvalEnv
st)
                })

      Bool -> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
evalIsNewExpr (StateT EvalEnv IO () -> StateT EvalEnv IO ())
-> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall a b. (a -> b) -> a -> b
$
        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 Op) -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams (OCType Op)
rp)
          then Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ((Expr, Expr) -> ICtx
addConst (Expr
e, Expr
e')) EvalType
NoRW Expr
e' StateT EvalEnv IO (Expr, FinalExpand)
-> StateT EvalEnv IO () -> StateT EvalEnv IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> StateT EvalEnv IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          else Knowledge -> ICtx -> RESTParams (OCType Op) -> StateT EvalEnv IO ()
evalREST Knowledge
γ ((Expr, Expr) -> ICtx
addConst (Expr
e, Expr
e')) (Expr -> RESTParams (OCType Op)
rpEval Expr
e')

      ((Expr, OCType Op) -> StateT EvalEnv IO ())
-> [(Expr, OCType Op)] -> StateT EvalEnv IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Expr, OCType Op)
rw -> Knowledge -> ICtx -> RESTParams (OCType Op) -> StateT EvalEnv IO ()
evalREST Knowledge
γ ICtx
ctx ((Expr, OCType Op) -> RESTParams (OCType Op)
rpRW (Expr, OCType Op)
rw)) [(Expr, OCType Op)]
rws
  where
    shouldExploreTerm :: ExploredTerms RuntimeTerm (OCType Op) m -> Expr -> m Bool
shouldExploreTerm ExploredTerms RuntimeTerm (OCType Op) m
et Expr
e =
      case RewriteArgs -> RWTerminationOpts
rwTerminationOpts RewriteArgs
rwArgs of
        RWTerminationOpts
RWTerminationCheckDisabled -> Bool -> m Bool
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 Op) m -> Bool
forall term c (m :: * -> *).
(Eq term, Hashable term) =>
term -> ExploredTerms term c m -> Bool
visited (Expr -> RuntimeTerm
convert Expr
e) ExploredTerms RuntimeTerm (OCType Op) m
et
        RWTerminationOpts
RWTerminationCheckEnabled  -> RuntimeTerm
-> OCType Op -> ExploredTerms RuntimeTerm (OCType Op) m -> m Bool
forall term c (m :: * -> *).
(Monad m, Show term, Eq term, Hashable term, Eq c, Show c) =>
term -> c -> ExploredTerms term c m -> m Bool
shouldExplore (Expr -> RuntimeTerm
convert Expr
e) (RESTParams (OCType Op) -> OCType Op
forall oc. RESTParams oc -> oc
c RESTParams (OCType Op)
rp) ExploredTerms RuntimeTerm (OCType Op) m
et

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

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

    rpEval :: Expr -> RESTParams (OCType Op)
rpEval Expr
e' =
      let
        c' :: OCType Op
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 Op) -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams (OCType Op)
rp)
            then AbstractOC (OCType Op) Expr IO
-> OCType Op -> Expr -> Expr -> OCType Op
forall c a (m :: * -> *). AbstractOC c a m -> c -> a -> a -> c
refine (RESTParams (OCType Op) -> AbstractOC (OCType Op) Expr IO
forall oc. RESTParams oc -> AbstractOC oc Expr IO
oc RESTParams (OCType Op)
rp) (RESTParams (OCType Op) -> OCType Op
forall oc. RESTParams oc -> oc
c RESTParams (OCType Op)
rp) Expr
e Expr
e'
            else RESTParams (OCType Op) -> OCType Op
forall oc. RESTParams oc -> oc
c RESTParams (OCType Op)
rp

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

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

    rpRW :: (Expr, OCType Op) -> RESTParams (OCType Op)
rpRW (Expr
e', OCType Op
c') = RESTParams (OCType Op)
rp{path :: [(Expr, TermOrigin)]
path = RESTParams (OCType Op) -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams (OCType Op)
rp [(Expr, TermOrigin)]
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. [a] -> [a] -> [a]
++ [(Expr
e', TermOrigin
RW)], c :: OCType Op
c = OCType Op
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 (String -> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. PPrint a => String -> a -> a
mytracepp String
"EVAL2: path" ([(Expr, TermOrigin)] -> [(Expr, TermOrigin)])
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a b. (a -> b) -> a -> b
$ RESTParams (OCType Op) -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams (OCType Op)
rp)
    e :: Expr
e               = [Expr] -> Expr
forall a. [a] -> a
last [Expr]
pathExprs
    autorws :: [AutoRewrite]
autorws         = Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx

    rwArgs :: RewriteArgs
rwArgs = (Expr -> IO Bool) -> RWTerminationOpts -> RewriteArgs
RWArgs (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ) (RWTerminationOpts -> RewriteArgs)
-> RWTerminationOpts -> RewriteArgs
forall a b. (a -> b) -> a -> b
$ Knowledge -> RWTerminationOpts
knRWTerminationOpts Knowledge
γ

    getRWs :: StateT EvalEnv IO [(Expr, OCType Op)]
getRWs =
      do
        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. [a] -> a
last (RESTParams (OCType Op) -> [(Expr, TermOrigin)]
forall oc. RESTParams oc -> [(Expr, TermOrigin)]
path RESTParams (OCType Op)
rp)) then (Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True) else (IO Bool -> StateT EvalEnv IO Bool
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 Op -> IO Bool
termCheck (RESTParams (OCType Op) -> OCType Op
forall oc. RESTParams oc -> oc
c RESTParams (OCType Op)
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, OCType Op)
getRW SubExpr
e AutoRewrite
ar = AbstractOC (OCType Op) Expr IO
-> RewriteArgs
-> OCType Op
-> SubExpr
-> AutoRewrite
-> MaybeT IO (Expr, OCType Op)
forall oc.
AbstractOC oc Expr IO
-> RewriteArgs
-> oc
-> SubExpr
-> AutoRewrite
-> MaybeT IO (Expr, oc)
getRewrite (RESTParams (OCType Op) -> AbstractOC (OCType Op) Expr IO
forall oc. RESTParams oc -> AbstractOC oc Expr IO
oc RESTParams (OCType Op)
rp) RewriteArgs
rwArgs (RESTParams (OCType Op) -> OCType Op
forall oc. RESTParams oc -> oc
c RESTParams (OCType Op)
rp) SubExpr
e AutoRewrite
ar
              let getRWs' :: SubExpr -> f [(Expr, OCType Op)]
getRWs' SubExpr
s  = [Maybe (Expr, OCType Op)] -> [(Expr, OCType Op)]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe (Expr, OCType Op)] -> [(Expr, OCType Op)])
-> f [Maybe (Expr, OCType Op)] -> f [(Expr, OCType Op)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AutoRewrite -> f (Maybe (Expr, OCType Op)))
-> [AutoRewrite] -> f [Maybe (Expr, OCType Op)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IO (Maybe (Expr, OCType Op)) -> f (Maybe (Expr, OCType Op))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Expr, OCType Op)) -> f (Maybe (Expr, OCType Op)))
-> (AutoRewrite -> IO (Maybe (Expr, OCType Op)))
-> AutoRewrite
-> f (Maybe (Expr, OCType Op))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT IO (Expr, OCType Op) -> IO (Maybe (Expr, OCType Op))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO (Expr, OCType Op) -> IO (Maybe (Expr, OCType Op)))
-> (AutoRewrite -> MaybeT IO (Expr, OCType Op))
-> AutoRewrite
-> IO (Maybe (Expr, OCType Op))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubExpr -> AutoRewrite -> MaybeT IO (Expr, OCType Op)
getRW SubExpr
s) [AutoRewrite]
autorws
              [[(Expr, OCType Op)]] -> [(Expr, OCType Op)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Expr, OCType Op)]] -> [(Expr, OCType Op)])
-> StateT EvalEnv IO [[(Expr, OCType Op)]]
-> StateT EvalEnv IO [(Expr, OCType Op)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubExpr -> StateT EvalEnv IO [(Expr, OCType Op)])
-> [SubExpr] -> StateT EvalEnv IO [[(Expr, OCType Op)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExpr -> StateT EvalEnv IO [(Expr, OCType Op)]
forall (f :: * -> *). MonadIO f => SubExpr -> f [(Expr, OCType Op)]
getRWs' (Expr -> [SubExpr]
subExprs Expr
e')
          else [(Expr, OCType Op)] -> StateT EvalEnv IO [(Expr, OCType Op)]
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 :: ConstMap
icSimpl = Expr -> Expr -> ConstMap -> ConstMap
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Expr
e Expr
e' (ConstMap -> ConstMap) -> ConstMap -> ConstMap
forall a b. (a -> b) -> a -> b
$ ICtx -> ConstMap
icSimpl ICtx
ctx} else ICtx
ctx 

(<$$>) :: (Monad m) => (a -> m b) -> [a] -> m [b]
a -> m b
f <$$> :: (a -> m b) -> [a] -> m [b]
<$$> [a]
xs = a -> m b
f (a -> m b) -> [a] -> m [b]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
Misc.<$$> [a]
xs


-- | @evalApp kn ctx e es@ unfolds expressions in @eApps e es@ using rewrites
-- and equations
evalApp :: Knowledge -> ICtx -> Expr -> [Expr] -> EvalType -> EvalST (Expr, FinalExpand)
evalApp :: Knowledge
-> ICtx
-> Expr
-> [Expr]
-> EvalType
-> StateT EvalEnv IO (Expr, FinalExpand)
evalApp Knowledge
γ ICtx
ctx (EVar Symbol
f) [Expr]
es EvalType
et
  | 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 (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 (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
                Symbol -> StateT EvalEnv IO ()
useFuel Symbol
f
                let ([Expr]
es1,[Expr]
es2) = Int -> [Expr] -> ([Expr], [Expr])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Symbol, Sort)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)) [Expr]
es
                Expr -> [Expr] -> StateT EvalEnv IO (Expr, FinalExpand)
shortcut (SEnv Sort -> Equation -> [Expr] -> Expr
substEq SEnv Sort
env Equation
eq [Expr]
es1) [Expr]
es2 -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter
         else (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr] -> Expr
eApps (Symbol -> Expr
EVar Symbol
f) [Expr]
es, FinalExpand
noExpand)
  where
    shortcut :: Expr -> [Expr] -> StateT EvalEnv IO (Expr, FinalExpand)
shortcut (EIte Expr
i Expr
e1 Expr
e2) [Expr]
es2 = do
      (Expr
b, FinalExpand
_) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
i
      Bool
b'  <- IO Bool -> StateT EvalEnv IO Bool
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
$ (String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalEIt POS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Expr, Expr) -> String
forall a. PPrint a => a -> String
showpp (Expr
i, Expr
b)) (Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
b)
      Bool
nb' <- IO Bool -> StateT EvalEnv IO Bool
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
$ (String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalEIt NEG " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Expr, Expr) -> String
forall a. PPrint a => a -> String
showpp (Expr
i, Expr -> Expr
PNot Expr
b)) (Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
b))
      (Expr, FinalExpand)
r <- if Bool
b' 
        then Expr -> [Expr] -> StateT EvalEnv IO (Expr, FinalExpand)
shortcut Expr
e1 [Expr]
es2
        else if Bool
nb' then Expr -> [Expr] -> StateT EvalEnv IO (Expr, FinalExpand)
shortcut Expr
e2 [Expr]
es2
        else (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr] -> Expr
eApps (Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2) [Expr]
es2, FinalExpand
expand)
      (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr, FinalExpand)
r
    shortcut Expr
e' [Expr]
es2 = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr] -> Expr
eApps Expr
e' [Expr]
es2, FinalExpand
noExpand)

evalApp Knowledge
γ ICtx
_ (EVar Symbol
f) (Expr
e:[Expr]
es) EvalType
_
  | (EVar Symbol
dc, [Expr]
as) <- Expr -> (Expr, [Expr])
splitEApp Expr
e
  , Just [Rewrite]
rws <- Symbol -> Map Symbol [Rewrite] -> Maybe [Rewrite]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
dc (Knowledge -> Map Symbol [Rewrite]
knSims Knowledge
γ)
  , Just Rewrite
rw <- (Rewrite -> Bool) -> [Rewrite] -> Maybe Rewrite
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\Rewrite
rw -> Rewrite -> Symbol
smName Rewrite
rw Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f) [Rewrite]
rws
  , [Expr] -> 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 (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
  = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (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, FinalExpand
noExpand)

evalApp Knowledge
_ ICtx
_ Expr
e [Expr]
es EvalType
_
  = (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr -> [Expr] -> Expr
eApps Expr
e [Expr]
es, FinalExpand
noExpand)

--------------------------------------------------------------------------------
-- | '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    = String -> SrcSpan
panicSpan String
"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 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   = String -> a
forall a. String -> a
panic (String
"mkCoSub: cannot build CoSub for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)] -> String
forall a. PPrint a => a -> String
showpp [(Symbol, Sort)]
xys String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" cannot unify " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. PPrint a => a -> String
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
    ([Sort]
_xTs,[Sort]
_eTs) = ([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

evalBool :: Knowledge -> Expr -> EvalST (Maybe Expr) 
evalBool :: Knowledge -> Expr -> EvalST (Maybe Expr)
evalBool Knowledge
γ Expr
e = do 
  Bool
bt <- IO Bool -> StateT EvalEnv IO Bool
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 -> Expr -> IO Bool
isValid Knowledge
γ Expr
e
  if Bool
bt then Maybe Expr -> EvalST (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> EvalST (Maybe Expr))
-> Maybe Expr -> EvalST (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
PTrue 
   else do 
    Bool
bf <- IO Bool -> StateT EvalEnv IO Bool
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 -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
e)
    if Bool
bf then Maybe Expr -> EvalST (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> EvalST (Maybe Expr))
-> Maybe Expr -> EvalST (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
PFalse 
          else Maybe Expr -> EvalST (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
               
evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> Expr -> Expr -> EvalST (Expr, FinalExpand)
evalIte :: Knowledge
-> ICtx
-> EvalType
-> Expr
-> Expr
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
evalIte Knowledge
γ ICtx
ctx EvalType
et Expr
b0 Expr
e1 Expr
e2 = do
  (Expr
b, FinalExpand
fe) <- Knowledge
-> ICtx
-> EvalType
-> Expr
-> StateT EvalEnv IO (Expr, FinalExpand)
eval Knowledge
γ ICtx
ctx EvalType
et Expr
b0
  Bool
b'  <- IO Bool -> StateT EvalEnv IO Bool
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
$ (String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalEIt POS " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
b) (Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
b)
  Bool
nb' <- IO Bool -> StateT EvalEnv IO Bool
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
$ (String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalEIt NEG " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp (Expr -> Expr
PNot Expr
b)) (Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
b))
  if Bool
b' 
    then (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e1, FinalExpand
noExpand)
    else if Bool
nb' then (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr
e2, FinalExpand
noExpand)
    else (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand))
-> (Expr, FinalExpand) -> StateT EvalEnv IO (Expr, FinalExpand)
forall a b. (a -> b) -> a -> b
$ (Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2, FinalExpand
fe)

--------------------------------------------------------------------------------
-- | Knowledge (SMT Interaction)
--------------------------------------------------------------------------------
data Knowledge = KN 
  { Knowledge -> Map Symbol [Rewrite]
knSims              :: Map Symbol [Rewrite]   -- ^ Rewrites rules came from match and data type definitions 
                                                  --   They are grouped by the data constructor that they unfold
  , 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 -> SelectorMap
knSels              :: !SelectorMap 
  , Knowledge -> ConstDCMap
knConsts            :: !ConstDCMap
  , Knowledge -> HashMap SubcId [AutoRewrite]
knAutoRWs           :: M.HashMap SubcId [AutoRewrite]
  , Knowledge -> RWTerminationOpts
knRWTerminationOpts :: RWTerminationOpts
  }

isValid :: Knowledge -> Expr -> IO Bool
isValid :: Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
e = do 
  Bool
contra <- Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds Knowledge
γ (Knowledge -> Context
knContext Knowledge
γ) (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ) Expr
PFalse
  if Bool
contra 
    then Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False 
    else Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds Knowledge
γ (Knowledge -> Context
knContext Knowledge
γ) (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ) Expr
e

knowledge :: Config -> SMT.Context -> SInfo a -> Knowledge
knowledge :: Config -> Context -> SInfo a -> Knowledge
knowledge Config
cfg Context
ctx SInfo a
si = KN :: Map Symbol [Rewrite]
-> Map Symbol Equation
-> Context
-> (Context -> [(Symbol, Sort)] -> Expr -> IO Bool)
-> [(Symbol, Sort)]
-> [(Symbol, Int)]
-> HashSet Symbol
-> SelectorMap
-> ConstDCMap
-> HashMap SubcId [AutoRewrite]
-> RWTerminationOpts
-> Knowledge
KN 
  { knSims :: Map Symbol [Rewrite]
knSims                     = ([Rewrite] -> [Rewrite] -> [Rewrite])
-> [(Symbol, [Rewrite])] -> Map Symbol [Rewrite]
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith [Rewrite] -> [Rewrite] -> [Rewrite]
forall a. [a] -> [a] -> [a]
(++) [ (Rewrite -> Symbol
smDC Rewrite
rw, [Rewrite
rw]) | Rewrite
rw <- [Rewrite]
sims]
  , 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 (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)
  , knSels :: SelectorMap
knSels                     = [Maybe (Symbol, (Symbol, Int))] -> SelectorMap
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe (Symbol, (Symbol, Int))] -> SelectorMap)
-> [Maybe (Symbol, (Symbol, Int))] -> SelectorMap
forall a b. (a -> b) -> a -> b
$ (Rewrite -> Maybe (Symbol, (Symbol, Int)))
-> [Rewrite] -> [Maybe (Symbol, (Symbol, Int))]
forall a b. (a -> b) -> [a] -> [b]
map Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel  [Rewrite]
sims 
  , knConsts :: ConstDCMap
knConsts                   = [Maybe (Symbol, (Symbol, Expr))] -> ConstDCMap
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe (Symbol, (Symbol, Expr))] -> ConstDCMap)
-> [Maybe (Symbol, (Symbol, Expr))] -> ConstDCMap
forall a b. (a -> b) -> a -> b
$ (Rewrite -> Maybe (Symbol, (Symbol, Expr)))
-> [Rewrite] -> [Maybe (Symbol, (Symbol, Expr))]
forall a b. (a -> b) -> [a] -> [b]
map 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 
    sims :: [Rewrite]
sims = AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv
    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 = [Maybe Symbol] -> [Symbol]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe Symbol] -> [Symbol]) -> [Maybe Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (AutoRewrite -> Maybe Symbol) -> [AutoRewrite] -> [Maybe Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (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] -> [Maybe Symbol])
-> [AutoRewrite] -> [Maybe Symbol]
forall a b. (a -> b) -> a -> b
$ [[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 (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 | (EVar Symbol
f, [Expr]
_) <- Expr -> (Expr, [Expr])
splitEApp Expr
e = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
f
    lhsHead Expr
_ | Bool
otherwise = 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 p. Num p => Sort -> p
getArity Sort
sort)

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



    makeCons :: Rewrite -> Maybe (Symbol, (Symbol, Expr))
makeCons Rewrite
rw 
      | [Symbol] -> 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 

askSMT :: Config -> SMT.Context -> [(Symbol, Sort)] -> Expr -> IO Bool
askSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
askSMT Config
cfg Context
ctx [(Symbol, Sort)]
bs Expr
e
--   | isContraPred e     = return False 
  | Expr -> Bool
isTautoPred  Expr
e     = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
  | [KVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [KVar]
Vis.kvarsExpr Expr
e) = Context -> [(Symbol, Sort)] -> Expr -> Expr -> IO Bool
SMT.checkValidWithContext Context
ctx [] Expr
PTrue Expr
e'
  | Bool
otherwise          = Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
  where 
    e' :: Expr
e'                 = String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT String
"askSMT" Config
cfg Context
ctx [(Symbol, Sort)]
bs Expr
e 

toSMT :: String ->  Config -> SMT.Context -> [(Symbol, Sort)] -> Expr -> Pred
toSMT :: String -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT String
msg Config
cfg Context
ctx [(Symbol, Sort)]
bs Expr
e = Config -> SymEnv -> Expr -> Expr
forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
senv (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located String -> SymEnv -> Expr -> Expr
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate Located String
"makeKnowledge" ([(Symbol, Sort)] -> SymEnv
elabEnv [(Symbol, Sort)]
bs) (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"toSMT from " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e)
                          (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e 
  where
    elabEnv :: [(Symbol, Sort)] -> SymEnv
elabEnv      = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
senv
    senv :: SymEnv
senv         = Context -> SymEnv
SMT.ctxSymEnv Context
ctx


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

withCtx :: Config -> FilePath -> SymEnv -> (SMT.Context -> IO a) -> IO a
withCtx :: Config -> String -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg String
file SymEnv
env Context -> IO a
k = do
  Context
ctx <- Config -> String -> SymEnv -> IO Context
SMT.makeContextWithSEnv Config
cfg String
file SymEnv
env
  ()
_   <- Context -> IO ()
SMT.smtPush Context
ctx
  a
res <- Context -> IO a
k Context
ctx
  ExitCode
_   <- Context -> IO ExitCode
SMT.cleanupContext Context
ctx
  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 

isSimplification :: S.HashSet LDataCon -> (Expr,Expr) -> Bool 
isSimplification :: HashSet Symbol -> (Expr, Expr) -> Bool
isSimplification HashSet Symbol
dcs (Expr
_,Expr
c) = HashSet Symbol -> Expr -> Bool
isConstant HashSet Symbol
dcs Expr
c 
  

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)

class Simplifiable a where 
  simplify :: Knowledge -> ICtx -> a -> a 


instance Simplifiable Expr where
  simplify :: Knowledge -> ICtx -> Expr -> Expr
simplify Knowledge
γ ICtx
ictx Expr
e = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"simplification of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
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 -> ConstMap -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Expr
e (ICtx -> ConstMap
icSimpl ICtx
ictx)
        = Expr
e' 
      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 (EVar Symbol
f) Expr
a)
        | 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
γ) 
        , (EVar Symbol
dc', [Expr]
_) <- Expr -> (Expr, [Expr])
splitEApp Expr
a
        , 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 (EVar Symbol
f) Expr
a)
        | 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
γ) 
        , (EVar Symbol
dc', [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
a
        , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc' 
        = [Expr]
es[Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!!Int
i
      tx Expr
e = Expr
e
      
applyConstantFolding :: Bop -> Expr -> Expr -> Expr
applyConstantFolding :: Bop -> Expr -> Expr -> Expr
applyConstantFolding Bop
bop Expr
e1 Expr
e2 =
  case (Expr
e1, Expr
e2) of
    ((ECon (R Double
left)), (ECon (R Double
right))) ->
      Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop Double
left Double
right)
    ((ECon (R Double
left)), (ECon (I SubcId
right))) ->
      Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop Double
left (SubcId -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral SubcId
right))
    ((ECon (I SubcId
left)), (ECon (R Double
right))) ->
      Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop (SubcId -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral SubcId
left) Double
right)
    ((ECon (I SubcId
left)), (ECon (I SubcId
right))) ->
      Expr -> Maybe Expr -> Expr
forall a. a -> Maybe a -> a
Mb.fromMaybe Expr
e (Bop -> SubcId -> SubcId -> Maybe Expr
cfI Bop
bop SubcId
left SubcId
right)
    (Expr, Expr)
_ -> Expr
e
  where
    
    e :: Expr
e = Bop -> Expr -> Expr -> Expr
EBin Bop
bop Expr
e1 Expr
e2
    
    getOp :: Num a => Bop -> Maybe (a -> a -> a)
    getOp :: Bop -> Maybe (a -> a -> a)
getOp Bop
Minus    = (a -> a -> a) -> Maybe (a -> a -> a)
forall a. a -> Maybe a
Just (-)
    getOp Bop
Plus     = (a -> a -> a) -> Maybe (a -> a -> a)
forall a. a -> Maybe a
Just a -> a -> a
forall a. Num a => a -> a -> a
(+)
    getOp Bop
Times    = (a -> a -> a) -> Maybe (a -> a -> a)
forall a. a -> Maybe a
Just a -> a -> a
forall a. Num a => a -> a -> a
(*)
    getOp Bop
RTimes   = (a -> a -> a) -> Maybe (a -> a -> a)
forall a. a -> Maybe a
Just a -> a -> a
forall a. Num a => a -> a -> a
(*)
    getOp Bop
_        = Maybe (a -> a -> a)
forall a. Maybe a
Nothing

    cfR :: Bop -> Double -> Double -> Maybe Expr
    cfR :: Bop -> Double -> Double -> Maybe Expr
cfR Bop
bop Double
left Double
right = ((Double -> Double -> Double) -> Expr)
-> Maybe (Double -> Double -> Double) -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Double -> Double -> Double) -> Expr
go (Bop -> Maybe (Double -> Double -> Double)
forall a. Fractional a => Bop -> Maybe (a -> a -> a)
getOp' Bop
bop)
      where
        go :: (Double -> Double -> Double) -> Expr
go Double -> Double -> Double
f = Constant -> Expr
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Double -> Constant
R (Double -> Constant) -> Double -> Constant
forall a b. (a -> b) -> a -> b
$ Double -> Double -> Double
f Double
left Double
right
        
        getOp' :: Bop -> Maybe (a -> a -> a)
getOp' Bop
Div      = (a -> a -> a) -> Maybe (a -> a -> a)
forall a. a -> Maybe a
Just a -> a -> a
forall a. Fractional a => a -> a -> a
(/)
        getOp' Bop
RDiv     = (a -> a -> a) -> Maybe (a -> a -> a)
forall a. a -> Maybe a
Just a -> a -> a
forall a. Fractional a => a -> a -> a
(/)
        getOp' Bop
op       = Bop -> Maybe (a -> a -> a)
forall a. Num a => Bop -> Maybe (a -> a -> a)
getOp Bop
op

    cfI :: Bop -> Integer -> Integer -> Maybe Expr
    cfI :: Bop -> SubcId -> SubcId -> Maybe Expr
cfI Bop
bop SubcId
left SubcId
right = ((SubcId -> SubcId -> SubcId) -> Expr)
-> Maybe (SubcId -> SubcId -> SubcId) -> Maybe Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SubcId -> SubcId -> SubcId) -> Expr
go (Bop -> Maybe (SubcId -> SubcId -> SubcId)
forall a. Integral a => Bop -> Maybe (a -> a -> a)
getOp' Bop
bop)
      where
        go :: (SubcId -> SubcId -> SubcId) -> Expr
go SubcId -> SubcId -> SubcId
f = Constant -> Expr
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ SubcId -> Constant
I (SubcId -> Constant) -> SubcId -> Constant
forall a b. (a -> b) -> a -> b
$ SubcId -> SubcId -> SubcId
f SubcId
left SubcId
right
        
        getOp' :: Bop -> Maybe (a -> a -> a)
getOp' Bop
Mod = (a -> a -> a) -> Maybe (a -> a -> a)
forall a. a -> Maybe a
Just a -> a -> a
forall a. Integral a => a -> a -> a
mod
        getOp' Bop
op  = Bop -> Maybe (a -> a -> a)
forall a. Num a => Bop -> Maybe (a -> a -> a)
getOp Bop
op


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

class Normalizable a where 
  normalize :: a -> a 

instance Normalizable (GInfo c a) where 
  normalize :: GInfo c a -> GInfo c a
normalize GInfo c a
si = GInfo c a
si {ae :: AxiomEnv
ae = AxiomEnv -> AxiomEnv
forall a. Normalizable a => a -> a
normalize (AxiomEnv -> AxiomEnv) -> AxiomEnv -> AxiomEnv
forall a b. (a -> b) -> a -> b
$ GInfo c a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
si}

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

instance Normalizable Rewrite where 
  normalize :: Rewrite -> Rewrite
normalize Rewrite
rw = Rewrite
rw { smArgs :: [Symbol]
smArgs = [Symbol]
xs', smBody :: Expr
smBody = Symbol -> Expr -> Expr
normalizeBody (Rewrite -> Symbol
smName Rewrite
rw) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Rewrite -> Expr
smBody Rewrite
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..]
      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 :: [(Symbol, Sort)]
eqArgs = [Symbol] -> [Sort] -> [(Symbol, Sort)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs' [Sort]
ss, eqBody :: Expr
eqBody = Symbol -> Expr -> Expr
normalizeBody (Equation -> Symbol
eqName Equation
eq) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst Subst
su (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Equation -> Expr
eqBody Equation
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..]
      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 


normalizeBody :: Symbol -> Expr -> Expr
normalizeBody :: Symbol -> Expr -> Expr
normalizeBody Symbol
f = Expr -> Expr
go   
  where 
    go :: Expr -> Expr
go Expr
e 
      | (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f) (Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
e) 
      = Expr -> Expr
go' Expr
e 
    go Expr
e 
      = Expr
e 
    
    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 

_splitBranches :: Symbol -> Expr -> [(Expr, Expr)]
_splitBranches :: Symbol -> Expr -> [(Expr, Expr)]
_splitBranches Symbol
f = Expr -> [(Expr, Expr)]
go   
  where 
    go :: Expr -> [(Expr, Expr)]
go (PAnd [Expr]
es) 
      | (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f) ([Expr] -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms [Expr]
es) 
      = Expr -> (Expr, Expr)
go' (Expr -> (Expr, Expr)) -> [Expr] -> [(Expr, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    go Expr
e 
      = [(Expr
PTrue, Expr
e)]

    go' :: Expr -> (Expr, Expr)
go' (PImp Expr
c Expr
e) = (Expr
c, Expr
e) 
    go' Expr
e          = (Expr
PTrue, Expr
e)

-- -- TODO:FUEL Config
-- maxFuel :: Int
-- maxFuel = 11 

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 :: FuelCount
evFuel = Symbol -> FuelCount -> FuelCount
useFuelCount Symbol
f (EvalEnv -> FuelCount
evFuel EvalEnv
st) })

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

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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True