--------------------------------------------------------------------------------
-- | 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 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.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           Control.Monad.State
import           Control.Monad.Trans.Maybe
import qualified Data.HashMap.Strict  as M
import qualified Data.HashSet         as S
import qualified Data.List            as L
import qualified Data.Maybe           as Mb
import           Debug.Trace          (trace)

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
False -- True 
  , 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')

--------------------------------------------------------------------------------
-- | Strengthen Constraint Environments via PLE 
--------------------------------------------------------------------------------
instantiate :: (Loc a) => Config -> SInfo a -> IO (SInfo a)
instantiate :: Config -> SInfo a -> IO (SInfo a)
instantiate Config
cfg SInfo a
fi' = do 
    let cs :: [(SubcId, SimpC a)]
cs = [ (SubcId
i, SimpC a
c) | (SubcId
i, SimpC a
c) <- HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi), AxiomEnv -> SubcId -> SimpC a -> Bool
forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aEnv SubcId
i SimpC a
c ] 
    let t :: CTrie
t  = [(SubcId, SimpC a)] -> CTrie
forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
cs                                               -- 1. BUILD the Trie
    InstRes
res   <- 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
+ [(SubcId, SimpC a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(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 -> [(SubcId, SimpC a)] -> Context -> InstEnv a
forall a.
Loc a =>
Config -> SInfo a -> [(SubcId, SimpC a)] -> Context -> InstEnv a
instEnv Config
cfg SInfo a
fi [(SubcId, SimpC a)]
cs)  -- 2. TRAVERSE Trie to compute InstRes
    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
    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' 



------------------------------------------------------------------------------- 
-- | Step 1a: @instEnv@ sets up the incremental-PLE environment 
instEnv :: (Loc a) => Config -> SInfo a -> [(SubcId, SimpC a)] -> SMT.Context -> InstEnv a 
instEnv :: Config -> SInfo a -> [(SubcId, SimpC a)] -> Context -> InstEnv a
instEnv Config
cfg SInfo a
fi [(SubcId, SimpC a)]
cs Context
ctx = Config
-> Context
-> BindEnv
-> AxiomEnv
-> [(SubcId, SimpC a)]
-> Knowledge
-> EvalEnv
-> InstEnv a
forall a.
Config
-> Context
-> BindEnv
-> AxiomEnv
-> [(SubcId, SimpC a)]
-> Knowledge
-> EvalEnv
-> InstEnv a
InstEnv Config
cfg Context
ctx BindEnv
bEnv AxiomEnv
aEnv [(SubcId, 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 -> EvalEnv
EvalEnv (Context -> SymEnv
SMT.ctxSymEnv Context
ctx) EvAccum
forall a. Monoid a => a
mempty

---------------------------------------------------------------------------------------------- 
-- | Step 1b: @mkCTrie@ builds the @Trie@ of constraints indexed by their environments 
mkCTrie :: [(SubcId, SimpC a)] -> CTrie 
mkCTrie :: [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
ics  = [(Path, SubcId)] -> CTrie
forall a. [(Path, a)] -> Trie a
T.fromList [ (SimpC a -> Path
cBinds SimpC a
c, SubcId
i) | (SubcId
i, SimpC a
c) <- [(SubcId, SimpC a)]
ics ]
  where
    cBinds :: SimpC a -> Path
cBinds   = Path -> Path
forall a. Ord a => [a] -> [a]
L.sort (Path -> Path) -> (SimpC a -> Path) -> SimpC a -> Path
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> Path
elemsIBindEnv (IBindEnv -> Path) -> (SimpC a -> IBindEnv) -> SimpC a -> Path
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 -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
forall a.
InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx0 Path
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         = [(Expr, Expr)] -> ICtx
initCtx ([(Expr, Expr)] -> ICtx) -> [(Expr, Expr)] -> ICtx
forall a b. (a -> b) -> a -> b
$ ((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 -> Maybe BindId -> InstRes -> CTrie -> IO InstRes
loopT :: InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx Path
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
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
forall a.
InstEnv a
-> ICtx
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx Path
delta Maybe Int
i InstRes
res Branch SubcId
b
  T.Node [Branch SubcId]
bs  -> InstEnv a
-> ICtx
-> Path
-> Maybe SubcId
-> (ICtx -> IO InstRes)
-> IO InstRes
forall a b.
InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx Path
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
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
forall a.
InstEnv a
-> ICtx
-> Path
-> 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 -> Maybe BindId -> InstRes -> CBranch -> IO InstRes
loopB :: InstEnv a
-> ICtx
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx Path
delta Maybe Int
iMb InstRes
res Branch SubcId
b = case Branch SubcId
b of 
  T.Bind Int
i CTrie
t -> InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
forall a.
InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx (Int
iInt -> Path -> Path
forall a. a -> [a] -> [a]
:Path
delta) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) InstRes
res CTrie
t
  T.Val SubcId
cid  -> InstEnv a
-> ICtx
-> Path
-> Maybe SubcId
-> (ICtx -> IO InstRes)
-> IO InstRes
forall a b.
InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx Path
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) 


withAssms :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (ICtx -> IO b) -> IO b 
withAssms :: InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms env :: InstEnv a
env@(InstEnv {[(SubcId, 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 -> [(SubcId, 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 :: [(SubcId, SimpC a)]
ieAenv :: AxiomEnv
ieBEnv :: BindEnv
ieSMT :: Context
ieCfg :: Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..}) ICtx
ctx Path
delta Maybe SubcId
cidMb ICtx -> IO b
act = do 
  let ctx' :: ICtx
ctx'  = InstEnv a -> ICtx -> Path -> Maybe SubcId -> ICtx
forall a. InstEnv a -> ICtx -> Path -> Maybe SubcId -> ICtx
updCtx InstEnv a
env ICtx
ctx Path
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'

-- | @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 {[(SubcId, SimpC a)]
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: [(SubcId, 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 -> [(SubcId, 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 -> IO ICtx
go ICtx
ictx0 
  where
    withRewrites :: EvAccum -> EvAccum
withRewrites EvAccum
exprs =
      let
        rws :: [[(Expr, Expr)]]
rws = [Expr -> Rewrite -> [(Expr, Expr)]
rewrite Expr
e Rewrite
rw | Rewrite
rw <- Knowledge -> [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 -> IO ICtx
go ICtx
ictx | 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 =  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 }
                  [EvAccum]
evalResults   <- Context -> String -> IO [EvAccum] -> IO [EvAccum]
forall a. Context -> String -> IO a -> IO a
SMT.smtBracket Context
ctx String
"PLE.evaluate" (IO [EvAccum] -> IO [EvAccum]) -> IO [EvAccum] -> IO [EvAccum]
forall a b. (a -> b) -> a -> b
$ do
                               Context -> Expr -> IO ()
SMT.smtAssert Context
ctx ([Expr] -> Expr
pAnd (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)) 
                               (Expr -> IO EvAccum) -> [Expr] -> IO [EvAccum]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> EvalEnv -> ICtx -> Expr -> IO EvAccum
evalOne Knowledge
γ EvalEnv
env' ICtx
ictx) (HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList HashSet Expr
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  = ICtx -> HashSet Expr
icAssms  ICtx
ictx HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Semigroup a => a -> a -> a
<> (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 -> 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})
                                 


rewrite :: Expr -> Rewrite -> [(Expr,Expr)] 
rewrite :: Expr -> Rewrite -> [(Expr, Expr)]
rewrite Expr
e Rewrite
rw = [Maybe (Expr, Expr)] -> [(Expr, Expr)]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe (Expr, Expr)] -> [(Expr, Expr)])
-> [Maybe (Expr, Expr)] -> [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ (Expr -> Maybe (Expr, Expr)) -> [Expr] -> [Maybe (Expr, Expr)]
forall a b. (a -> b) -> [a] -> [b]
map (Expr -> Rewrite -> Maybe (Expr, Expr)
`rewriteTop` Rewrite
rw) (Expr -> [Expr]
notGuardedApps Expr
e)

rewriteTop :: Expr -> Rewrite -> Maybe (Expr,Expr) 
rewriteTop :: Expr -> Rewrite -> Maybe (Expr, Expr)
rewriteTop Expr
e Rewrite
rw
  | (EVar Symbol
f, [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
e
  , Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Rewrite -> Symbol
smDC Rewrite
rw
  , [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)
  = (Expr, Expr) -> Maybe (Expr, Expr)
forall a. a -> Maybe a
Just (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))
  | Bool
otherwise
  = Maybe (Expr, Expr)
forall a. Maybe a
Nothing

---------------------------------------------------------------------------------------------- 
-- | 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
$ Path -> [Expr] -> [(Int, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip Path
is [Expr]
ps''
    ps'' :: [Expr]
ps''     = (Int -> Expr -> Expr) -> Path -> [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) Path
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
    (Path
is, [Expr]
ps) = [(Int, Expr)] -> (Path, [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 -> [(SubcId, SimpC a)]
ieCstrs :: ![(SubcId, 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
  } 

---------------------------------------------------------------------------------------------- 
-- | @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 :: [(Expr,Expr)] -> ICtx
initCtx :: [(Expr, Expr)] -> ICtx
initCtx [(Expr, Expr)]
es = ICtx :: HashSet Expr
-> HashSet Expr
-> EvAccum
-> HashSet Expr
-> ConstMap
-> Maybe SubcId
-> 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
  }

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 = Int -> Expr -> InstRes -> InstRes
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert 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 -> Path -> Maybe SubcId -> ICtx
updCtx InstEnv {[(SubcId, SimpC a)]
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: [(SubcId, 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 -> [(SubcId, 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 Path
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 = (SubcId, SimpC a) -> SubcId
forall a b. (a, b) -> a
fst ((SubcId, SimpC a) -> SubcId)
-> Maybe (SubcId, SimpC a) -> Maybe SubcId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((SubcId, SimpC a) -> Bool)
-> [(SubcId, SimpC a)] -> Maybe (SubcId, SimpC a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\(SubcId
_, SimpC a
b) -> (Path -> Int
forall a. [a] -> a
head Path
delta) Int -> IBindEnv -> Bool
`memberIBindEnv` (SimpC a -> IBindEnv
forall a. SimpC a -> IBindEnv
_cenv SimpC a
b)) [(SubcId, SimpC a)]
ieCstrs
                    }
  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 -> Rewrite -> [(Expr, Expr)]
rewrite Expr
e Rewrite
rw | Expr
e  <- ([Expr]
cands [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((Expr, Expr) -> Expr
forall a b. (a, b) -> b
snd ((Expr, Expr) -> Expr) -> [(Expr, Expr)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvAccum -> [(Expr, Expr)]
forall a. HashSet a -> [a]
S.toList (ICtx -> EvAccum
icEquals ICtx
ctx)))
                                                  , Rewrite
rw <- Knowledge -> [Rewrite]
knSims Knowledge
ieKnowl]
    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 (SortedReft -> [KVar]
forall t. Visitable t => t -> [KVar]
Vis.kvars SortedReft
r) ] 
                  ])
    bs :: [(Symbol, SortedReft)]
bs        = (Symbol, SortedReft) -> (Symbol, SortedReft)
forall t. Visitable t => t -> t
unElab ((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
forall t. Visitable t => t -> t
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 <- Path
delta ] 
    subMb :: Maybe (SimpC a)
subMb     = HashMap SubcId (SimpC a) -> SubcId -> SimpC a
forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr ([(SubcId, SimpC a)] -> HashMap SubcId (SimpC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(SubcId, 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 Expr
_ Expr
_ Expr
_) = 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.
(?callStack::CallStack, 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
  }

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 -> Expr -> IO EvAccum
evalOne :: Knowledge -> EvalEnv -> ICtx -> Expr -> IO EvAccum
evalOne Knowledge
γ EvalEnv
env ICtx
ctx Expr
e | [AutoRewrite] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([AutoRewrite] -> Bool) -> [AutoRewrite] -> Bool
forall a b. (a -> b) -> a -> b
$ Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx = do
    (Expr
e',EvalEnv
st) <- StateT EvalEnv IO Expr -> EvalEnv -> IO (Expr, EvalEnv)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx Expr
e) EvalEnv
env 
    EvAccum -> IO EvAccum
forall (m :: * -> *) a. Monad m => a -> m a
return (EvAccum -> IO EvAccum) -> EvAccum -> IO EvAccum
forall a b. (a -> b) -> a -> b
$ if 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)
evalOne Knowledge
γ EvalEnv
env ICtx
ctx Expr
e =
  EvalEnv -> EvAccum
evAccum (EvalEnv -> EvAccum) -> IO EvalEnv -> IO EvAccum
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT EvalEnv IO () -> EvalEnv -> IO EvalEnv
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Knowledge -> ICtx -> [(Expr, TermOrigin)] -> StateT EvalEnv IO ()
eval Knowledge
γ ICtx
ctx [(Expr
e, TermOrigin
PLE)]) EvalEnv
env

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{})       = []



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

fastEval :: Knowledge -> ICtx -> Expr -> EvalST Expr
fastEval :: Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
_ ICtx
ctx 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 -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
v
  
fastEval Knowledge
γ ICtx
ctx Expr
e =
  do [(Expr, Expr)]
acc       <- 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 (EvalEnv -> [(Expr, Expr)])
-> StateT EvalEnv IO EvalEnv -> StateT EvalEnv IO [(Expr, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT EvalEnv IO EvalEnv
forall s (m :: * -> *). MonadState s m => m s
get
     case Expr -> [(Expr, Expr)] -> Maybe Expr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Expr
e [(Expr, Expr)]
acc of
        Just Expr
e' -> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx Expr
e'
        Maybe Expr
_ -> do
          Expr
e'  <- Knowledge -> ICtx -> Expr -> Expr
forall a. Simplifiable a => Knowledge -> ICtx -> a -> a
simplify Knowledge
γ ICtx
ctx (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
          if Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e'
            then 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)
                                      })
                    Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ((Expr, Expr) -> ICtx -> ICtx
addConst (Expr
e,Expr
e') ICtx
ctx) Expr
e'
            else Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
  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
go (ELam (Symbol
x,Sort
s) Expr
e)   = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
s) (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ' ICtx
ctx 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 e :: Expr
e@(EIte Expr
b Expr
e1 Expr
e2) = Knowledge
-> ICtx -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
fastEvalIte Knowledge
γ ICtx
ctx Expr
e Expr
b Expr
e1 Expr
e2
    go (ECoerc Sort
s Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t  (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go e :: Expr
e@(EApp Expr
_ Expr
_)     = case Expr -> (Expr, [Expr])
splitEApp Expr
e of 
                           (Expr
f, [Expr]
es) -> do (Expr
f':[Expr]
es') <- (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx) (Expr
fExpr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
es) 
                                         Knowledge
-> ICtx -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalApp Knowledge
γ ICtx
ctx (Expr -> [Expr] -> Expr
eApps Expr
f' [Expr]
es) (Expr
f',[Expr]
es')
    go e :: Expr
e@(PAtom Brel
r Expr
e1 Expr
e2) = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Brel -> Expr -> Expr -> Expr
PAtom Brel
r (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
    go (ENeg Expr
e)         = do Expr
e'  <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx Expr
e
                             Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
ENeg Expr
e'
    go (EBin Bop
o Expr
e1 Expr
e2)   = do Expr
e1' <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx Expr
e1 
                             Expr
e2' <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx Expr
e2 
                             Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
o Expr
e1' Expr
e2'
    go (ETApp Expr
e Sort
t)      = (Expr -> Sort -> Expr) -> Sort -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Sort -> Expr
ETApp Sort
t (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go (ETAbs Expr
e Symbol
s)      = (Expr -> Symbol -> Expr) -> Symbol -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Symbol -> Expr
ETAbs Symbol
s (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go e :: Expr
e@(PNot Expr
e')      = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Expr -> Expr
PNot (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e')           (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
    go e :: Expr
e@(PImp Expr
e1 Expr
e2)   = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Expr -> Expr -> Expr
PImp (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
    go e :: Expr
e@(PIff Expr
e1 Expr
e2)   = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Expr -> Expr -> Expr
PIff (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> StateT EvalEnv IO Expr
go Expr
e2) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
    go e :: Expr
e@(PAnd [Expr]
es)      = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM ([Expr] -> Expr
PAnd ([Expr] -> Expr)
-> StateT EvalEnv IO [Expr] -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO Expr
go  (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [Expr]
es))   (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
    go e :: Expr
e@(POr [Expr]
es)       = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM ([Expr] -> Expr
POr  ([Expr] -> Expr)
-> StateT EvalEnv IO [Expr] -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> StateT EvalEnv IO Expr
go (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [Expr]
es))    (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
    go Expr
e                = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

eval :: Knowledge -> ICtx -> [(Expr, TermOrigin)] -> EvalST ()
eval :: Knowledge -> ICtx -> [(Expr, TermOrigin)] -> StateT EvalEnv IO ()
eval Knowledge
_ ICtx
ctx [(Expr, TermOrigin)]
path
  | [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 [(Expr, TermOrigin)]
path
  , 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)})
        
eval Knowledge
γ ICtx
ctx [(Expr, TermOrigin)]
path =
  do
    [(Expr, TermOrigin)]
rws <- EvalST [(Expr, TermOrigin)]
getRWs 
    Expr
e'  <- Knowledge -> ICtx -> Expr -> Expr
forall a. Simplifiable a => Knowledge -> ICtx -> a -> a
simplify Knowledge
γ ICtx
ctx (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e
    let evalIsNewExpr :: Bool
evalIsNewExpr = Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
L.notElem Expr
e' [Expr]
pathExprs
    let exprsToAdd :: [Expr]
exprsToAdd    = (if Bool
evalIsNewExpr then [Expr
e'] else []) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ ((Expr, TermOrigin) -> Expr) -> [(Expr, TermOrigin)] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Expr, TermOrigin) -> Expr
forall a b. (a, b) -> a
fst [(Expr, TermOrigin)]
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)})
    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
$ Knowledge -> ICtx -> [(Expr, TermOrigin)] -> StateT EvalEnv IO ()
eval Knowledge
γ ((Expr, Expr) -> ICtx
addConst (Expr
e, Expr
e')) ([(Expr, TermOrigin)]
path [(Expr, TermOrigin)]
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. [a] -> [a] -> [a]
++ [(Expr
e', TermOrigin
PLE)])
    ((Expr, TermOrigin) -> StateT EvalEnv IO ())
-> [(Expr, TermOrigin)] -> StateT EvalEnv IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Expr, TermOrigin)
rw -> (Knowledge -> ICtx -> [(Expr, TermOrigin)] -> StateT EvalEnv IO ()
eval Knowledge
γ ICtx
ctx) ([(Expr, TermOrigin)]
path [(Expr, TermOrigin)]
-> [(Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. [a] -> [a] -> [a]
++ [(Expr, TermOrigin)
rw])) [(Expr, TermOrigin)]
rws
  where
    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 [(Expr, TermOrigin)]
path
    e :: Expr
e         = [Expr] -> Expr
forall a. [a] -> a
last [Expr]
pathExprs
    autorws :: [AutoRewrite]
autorws   = Knowledge -> ICtx -> [AutoRewrite]
getAutoRws Knowledge
γ ICtx
ctx

    getRWs :: EvalST [(Expr, TermOrigin)]
    getRWs :: EvalST [(Expr, TermOrigin)]
getRWs =
      let
        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)]
subsFromAssm (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
ctx)
        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)
        e' :: Expr
e'        = Expr -> Expr
forall t. (Eq t, Subable t) => t -> t
subst' Expr
e
        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'
        rwArgs :: RewriteArgs
rwArgs = (Expr -> IO Bool) -> RWTerminationOpts -> RewriteArgs
RWArgs (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ) (Knowledge -> RWTerminationOpts
knRWTerminationOpts Knowledge
γ)
        getRWs' :: SubExpr -> f [(Expr, TermOrigin)]
getRWs' SubExpr
s = 
          [Maybe (Expr, TermOrigin)] -> [(Expr, TermOrigin)]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe (Expr, TermOrigin)] -> [(Expr, TermOrigin)])
-> f [Maybe (Expr, TermOrigin)] -> f [(Expr, TermOrigin)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (AutoRewrite -> f (Maybe (Expr, TermOrigin)))
-> [AutoRewrite] -> f [Maybe (Expr, TermOrigin)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IO (Maybe (Expr, TermOrigin)) -> f (Maybe (Expr, TermOrigin))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe (Expr, TermOrigin)) -> f (Maybe (Expr, TermOrigin)))
-> (AutoRewrite -> IO (Maybe (Expr, TermOrigin)))
-> AutoRewrite
-> f (Maybe (Expr, TermOrigin))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT IO (Expr, TermOrigin) -> IO (Maybe (Expr, TermOrigin))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT IO (Expr, TermOrigin) -> IO (Maybe (Expr, TermOrigin)))
-> (AutoRewrite -> MaybeT IO (Expr, TermOrigin))
-> AutoRewrite
-> IO (Maybe (Expr, TermOrigin))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteArgs
-> [(Expr, TermOrigin)]
-> SubExpr
-> AutoRewrite
-> MaybeT IO (Expr, TermOrigin)
getRewrite RewriteArgs
rwArgs [(Expr, TermOrigin)]
path SubExpr
s) [AutoRewrite]
autorws
      in [[(Expr, TermOrigin)]] -> [(Expr, TermOrigin)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Expr, TermOrigin)]] -> [(Expr, TermOrigin)])
-> StateT EvalEnv IO [[(Expr, TermOrigin)]]
-> EvalST [(Expr, TermOrigin)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SubExpr -> EvalST [(Expr, TermOrigin)])
-> [SubExpr] -> StateT EvalEnv IO [[(Expr, TermOrigin)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SubExpr -> EvalST [(Expr, TermOrigin)]
forall (f :: * -> *).
MonadIO f =>
SubExpr -> f [(Expr, TermOrigin)]
getRWs' (Expr -> [SubExpr]
subExprs Expr
e')
          
    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 

evalStep :: Knowledge -> ICtx -> Expr -> EvalST Expr
evalStep :: Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx (ELam (Symbol
x,Sort
s) Expr
e)   = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
s) (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ' ICtx
ctx 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
γ }
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(EIte Expr
b Expr
e1 Expr
e2) = Knowledge
-> ICtx -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx Expr
e Expr
b Expr
e1 Expr
e2
evalStep Knowledge
γ ICtx
ctx (ECoerc Sort
s Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(EApp Expr
_ Expr
_)     = case Expr -> (Expr, [Expr])
splitEApp Expr
e of 
  (Expr
f, [Expr]
es) ->
    do
      Expr
f' <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
f
      if Expr
f' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
f
        then Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Expr] -> Expr
eApps Expr
f' [Expr]
es)
        else
          do
            [Expr]
es' <- (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx) [Expr]
es
            if [Expr]
es [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Expr]
es'
              then Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Expr] -> Expr
eApps Expr
f' [Expr]
es')
              else Knowledge
-> ICtx -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalApp Knowledge
γ ICtx
ctx (Expr -> [Expr] -> Expr
eApps Expr
f' [Expr]
es') (Expr
f',[Expr]
es')
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(PAtom Brel
r Expr
e1 Expr
e2) =
  StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Brel -> Expr -> Expr -> Expr
PAtom Brel
r (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e2) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
evalStep Knowledge
γ ICtx
ctx (ENeg Expr
e) = Expr -> Expr
ENeg (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e
evalStep Knowledge
γ ICtx
ctx (EBin Bop
o Expr
e1 Expr
e2)   = do
  Expr
e1' <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e1
  if Expr
e1' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e1
    then Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Bop -> Expr -> Expr -> Expr
EBin Bop
o Expr
e1' Expr
e2)
    else Bop -> Expr -> Expr -> Expr
EBin Bop
o Expr
e1 (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e2
evalStep Knowledge
γ ICtx
ctx (ETApp Expr
e Sort
t)      = (Expr -> Sort -> Expr) -> Sort -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Sort -> Expr
ETApp Sort
t (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e
evalStep Knowledge
γ ICtx
ctx (ETAbs Expr
e Symbol
s)      = (Expr -> Symbol -> Expr) -> Symbol -> Expr -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Symbol -> Expr
ETAbs Symbol
s (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(PNot Expr
e')      = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Expr -> Expr
PNot (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e') (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(PImp Expr
e1 Expr
e2)   = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Expr -> Expr -> Expr
PImp (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e2) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(PIff Expr
e1 Expr
e2)   = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (Expr -> Expr -> Expr
PIff (Expr -> Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e1 StateT EvalEnv IO (Expr -> Expr)
-> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
e2) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(PAnd [Expr]
es)      = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM ([Expr] -> Expr
PAnd ([Expr] -> Expr)
-> StateT EvalEnv IO [Expr] -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [Expr]
es)) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
evalStep Knowledge
γ ICtx
ctx e :: Expr
e@(POr [Expr]
es)       = StateT EvalEnv IO Expr
-> StateT EvalEnv IO (Maybe Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM ([Expr] -> Expr
POr  ([Expr] -> Expr)
-> StateT EvalEnv IO [Expr] -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx (Expr -> StateT EvalEnv IO Expr)
-> [Expr] -> StateT EvalEnv IO [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
<$$> [Expr]
es)) (Knowledge -> Expr -> StateT EvalEnv IO (Maybe Expr)
evalBool Knowledge
γ Expr
e)
evalStep Knowledge
_ ICtx
_   Expr
e                = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

fromMaybeM :: (Monad m) => m a -> m (Maybe a) -> m a 
fromMaybeM :: m a -> m (Maybe a) -> m a
fromMaybeM m a
a m (Maybe a)
ma = do 
  Maybe a
mx <- m (Maybe a)
ma 
  case Maybe a
mx of 
    Just a
x  -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x 
    Maybe a
Nothing -> m a
a  

(<$$>) :: (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 :: Knowledge -> ICtx -> Expr -> (Expr, [Expr]) -> EvalST Expr
evalApp :: Knowledge
-> ICtx -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalApp Knowledge
γ ICtx
ctx Expr
_ (EVar Symbol
f, [Expr]
es)
  | Just Equation
eq <- (Equation -> Bool) -> [Equation] -> Maybe Equation
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f) (Symbol -> Bool) -> (Equation -> Symbol) -> Equation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> Symbol
eqName) (Knowledge -> [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 <- SymEnv -> SEnv Sort
seSort (SymEnv -> SEnv Sort)
-> StateT EvalEnv IO SymEnv -> StateT EvalEnv IO (SEnv Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EvalEnv -> SymEnv) -> StateT EvalEnv IO SymEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> SymEnv
evEnv
       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
shortcut (SEnv Sort -> Equation -> [Expr] -> Expr
substEq SEnv Sort
env Equation
eq [Expr]
es1) [Expr]
es2
  where
    shortcut :: Expr -> [Expr] -> StateT EvalEnv IO Expr
shortcut (EIte Expr
i Expr
e1 Expr
e2) [Expr]
es2 = do
      Expr
b   <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx 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 -> 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))
      Expr
r <- if Bool
b' 
        then Expr -> [Expr] -> StateT EvalEnv IO Expr
shortcut Expr
e1 [Expr]
es2
        else if Bool
nb' then Expr -> [Expr] -> StateT EvalEnv IO Expr
shortcut Expr
e2 [Expr]
es2
        else Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> Expr
eApps (Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2) [Expr]
es2
      Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
r
    shortcut Expr
e' [Expr]
es2 = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Expr -> [Expr] -> Expr
eApps Expr
e' [Expr]
es2

evalApp Knowledge
γ ICtx
_ Expr
_ (EVar Symbol
f, Expr
e:[Expr]
es) 
  | (EVar Symbol
dc, [Expr]
as) <- Expr -> (Expr, [Expr])
splitEApp Expr
e
  , 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 Bool -> Bool -> Bool
&& Rewrite -> Symbol
smDC Rewrite
rw Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc) (Knowledge -> [Rewrite]
knSims Knowledge
γ)
  , [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 -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ 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 

evalApp Knowledge
_ ICtx
_ Expr
e (Expr, [Expr])
_
  = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e 
  
--------------------------------------------------------------------------------
-- | '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 -> StateT EvalEnv IO (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 -> StateT EvalEnv IO (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> StateT EvalEnv IO (Maybe Expr))
-> Maybe Expr -> StateT EvalEnv IO (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 -> StateT EvalEnv IO (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Expr -> StateT EvalEnv IO (Maybe Expr))
-> Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall a b. (a -> b) -> a -> b
$ Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
PFalse 
          else Maybe Expr -> StateT EvalEnv IO (Maybe Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Expr
forall a. Maybe a
Nothing
               
fastEvalIte :: Knowledge -> ICtx -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
fastEvalIte :: Knowledge
-> ICtx -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
fastEvalIte Knowledge
γ ICtx
ctx Expr
_ Expr
b0 Expr
e1 Expr
e2 = do 
  Expr
b <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
fastEval Knowledge
γ ICtx
ctx 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 -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Expr
e1 
    else if Bool
nb' then Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Expr
e2 
    else Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2  

evalIte :: Knowledge -> ICtx -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
evalIte :: Knowledge
-> ICtx -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ ICtx
ctx Expr
_ Expr
b0 Expr
e1 Expr
e2 = do 
  Expr
b   <- Knowledge -> ICtx -> Expr -> StateT EvalEnv IO Expr
evalStep Knowledge
γ ICtx
ctx Expr
b0
  if Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
b0 then Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2) else
    do
      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
$ 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
$ Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
b)
      Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$
        if Bool
b'
        then Expr
e1
        else if Bool
nb' then Expr
e2 
        else Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2
        
--------------------------------------------------------------------------------
-- | Knowledge (SMT Interaction)
--------------------------------------------------------------------------------
data Knowledge = KN 
  { Knowledge -> [Rewrite]
knSims              :: ![Rewrite]           -- ^ Rewrite rules came from match and data type definitions 
  , Knowledge -> [Equation]
knAms               :: ![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 :: [Rewrite]
-> [Equation]
-> Context
-> (Context -> [(Symbol, Sort)] -> Expr -> IO Bool)
-> [(Symbol, Sort)]
-> [(Symbol, Int)]
-> HashSet Symbol
-> SelectorMap
-> ConstDCMap
-> HashMap SubcId [AutoRewrite]
-> RWTerminationOpts
-> Knowledge
KN 
  { knSims :: [Rewrite]
knSims                     = [Rewrite]
sims 
  , knAms :: [Equation]
knAms                      = 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)
  , 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 Maybe Int -> RWTerminationOpts
RWTerminationCheckEnabled (Config -> Maybe Int
maxRWOrderingConstraints Config
cfg)
      else RWTerminationOpts
RWTerminationCheckDisabled
  } 
  where 
    sims :: [Rewrite]
sims = AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv [Rewrite] -> [Rewrite] -> [Rewrite]
forall a. [a] -> [a] -> [a]
++ (DataDecl -> [Rewrite]) -> [DataDecl] -> [Rewrite]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [Rewrite]
reWriteDDecl (SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si) 
    aenv :: AxiomEnv
aenv = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
si 

    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 

reWriteDDecl :: DataDecl -> [Rewrite]
reWriteDDecl :: DataDecl -> [Rewrite]
reWriteDDecl DataDecl
ddecl = (DataCtor -> [Rewrite]) -> [DataCtor] -> [Rewrite]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCtor -> [Rewrite]
go (DataDecl -> [DataCtor]
ddCtors DataDecl
ddecl) 
  where 
    go :: DataCtor -> [Rewrite]
go (DCtor LocSymbol
f [DataField]
xs) = (Symbol -> Int -> Rewrite) -> [Symbol] -> Path -> [Rewrite]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
r Int
i -> Symbol -> Symbol -> [Symbol] -> Expr -> Rewrite
SMeasure Symbol
r Symbol
f' [Symbol]
ys (Symbol -> Expr
EVar ([Symbol]
ys[Symbol] -> Int -> Symbol
forall a. [a] -> Int -> a
!!Int
i)) ) [Symbol]
rs [Int
0..]
       where 
        f' :: Symbol
f'  = LocSymbol -> Symbol
forall a. Symbolic a => a -> Symbol
symbol LocSymbol
f 
        rs :: [Symbol]
rs  = (LocSymbol -> Symbol
forall a. Located a -> a
val (LocSymbol -> Symbol)
-> (DataField -> LocSymbol) -> DataField -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataField -> LocSymbol
dfName) (DataField -> Symbol) -> [DataField] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataField]
xs  
        mkArg :: [a] -> [Symbol]
mkArg [a]
ws = (a -> SubcId -> Symbol) -> [a] -> [SubcId] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\a
_ SubcId
i -> Symbol -> SubcId -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String
"darg"::String)) SubcId
i) [a]
ws [SubcId
0..]
        ys :: [Symbol]
ys  = [DataField] -> [Symbol]
forall a. [a] -> [Symbol]
mkArg [DataField]
xs 

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
  | 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]
forall t. Visitable t => t -> [KVar]
Vis.kvars 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 ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms 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
forall t. Visitable t => (Expr -> Expr) -> t -> t
Vis.mapExpr 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 (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  



-------------------------------------------------------------------------------
-- | 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)