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

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

module Language.Fixpoint.Solver.Instantiate (instantiate) where

import           Language.Fixpoint.Types
import           Language.Fixpoint.Types.Config  as FC
import qualified Language.Fixpoint.Types.Visitor as Vis
import qualified Language.Fixpoint.Misc          as Misc -- (mapFst)
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 -- as T 
import           Language.Fixpoint.SortCheck
import           Language.Fixpoint.Graph.Deps             (isTarget) 
import           Language.Fixpoint.Solver.Sanitize        (symbolEnv)
import qualified Language.Fixpoint.Solver.PLE as PLE      (instantiate)
import           Control.Monad.State
import qualified Data.Text            as T
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 -- (isNothing, catMaybes, fromMaybe)
import           Data.Char            (isUpper)
-- import           Debug.Trace          (trace)
-- import           Text.Printf (printf)

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

--------------------------------------------------------------------------------
-- | 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
  | Config -> Bool
rewriteAxioms Config
cfg Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
oldPLE Config
cfg)
  = Config -> SInfo a -> IO (SInfo a)
forall a. Loc a => Config -> SInfo a -> IO (SInfo a)
PLE.instantiate Config
cfg SInfo a
fi

  | Config -> Bool
rewriteAxioms Config
cfg Bool -> Bool -> Bool
&& Config -> Bool
noIncrPle Config
cfg
  = Config -> SInfo a -> IO (SInfo a)
forall a. Loc a => Config -> SInfo a -> IO (SInfo a)
instantiate' Config
cfg SInfo a
fi

  | Config -> Bool
rewriteAxioms Config
cfg -- && incrPle cfg 
  = Config -> SInfo a -> IO (SInfo a)
forall a. Loc a => Config -> SInfo a -> IO (SInfo a)
incrInstantiate' Config
cfg SInfo a
fi

  | Bool
otherwise         
  = SInfo a -> IO (SInfo a)
forall (m :: * -> *) a. Monad m => a -> m a
return SInfo a
fi

------------------------------------------------------------------------------- 
-- | New "Incremental" PLE
------------------------------------------------------------------------------- 
incrInstantiate' :: (Loc a) => Config -> SInfo a -> IO (SInfo a)
------------------------------------------------------------------------------- 
incrInstantiate' :: Config -> SInfo a -> IO (SInfo a)
incrInstantiate' 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 



------------------------------------------------------------------------------- 
-- | 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
-> HashMap SubcId (SimpC a)
-> Knowledge
-> EvalEnv
-> InstEnv a
forall a.
Config
-> Context
-> BindEnv
-> AxiomEnv
-> HashMap SubcId (SimpC a)
-> Knowledge
-> EvalEnv
-> InstEnv a
InstEnv Config
cfg Context
ctx BindEnv
bEnv AxiomEnv
aEnv ([(SubcId, SimpC a)] -> HashMap SubcId (SimpC a)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(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 -> AxiomEnv -> Knowledge
knowledge Config
cfg Context
ctx AxiomEnv
aEnv 
    s0 :: EvalEnv
s0                = Int -> [(Expr, Expr)] -> AxiomEnv -> SymEnv -> Config -> EvalEnv
EvalEnv Int
0 [] AxiomEnv
aEnv (Context -> SymEnv
SMT.ctxSymEnv Context
ctx) Config
cfg 

---------------------------------------------------------------------------------------------- 
-- | 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  = String -> CTrie -> CTrie
forall a. PPrint a => String -> a -> a
mytracepp  String
"TRIE" (CTrie -> CTrie) -> CTrie -> CTrie
forall a b. (a -> b) -> a -> b
$ [(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] -> ICtx
initCtx [Expr]
es0
    es0 :: [Expr]
es0          = Equation -> Expr
eqBody (Equation -> Expr) -> [Equation] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (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)

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
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
forall a.
InstEnv a
-> ICtx
-> Maybe Int
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
i Maybe SubcId
forall a. Maybe a
Nothing 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
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
forall a.
InstEnv a
-> ICtx
-> Maybe Int
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
iMb (SubcId -> Maybe SubcId
forall a. a -> Maybe a
Just SubcId
cid) 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 {HashMap 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 -> HashMap 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 :: HashMap 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 :: [Expr]
assms = String -> [Expr] -> [Expr]
forall a. PPrint a => String -> a -> a
mytracepp  (String
"ple1-assms: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe SubcId, Path) -> String
forall a. Show a => a -> String
show (Maybe SubcId
cidMb, Path
delta)) (ICtx -> [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
    [Expr] -> (Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [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 -> Maybe SubcId -> InstRes -> IO (ICtx, InstRes)
ple1 :: InstEnv a
-> ICtx
-> Maybe Int
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
ple1 env :: InstEnv a
env@(InstEnv {HashMap SubcId (SimpC a)
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: HashMap 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 -> HashMap 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 Maybe SubcId
cidMb InstRes
res = do 
  let cands :: [Expr]
cands = String -> [Expr] -> [Expr]
forall a. PPrint a => String -> a -> a
mytracepp  (String
"ple1-cands: "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe SubcId -> String
forall a. Show a => a -> String
show Maybe SubcId
cidMb) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ HashSet Expr -> [Expr]
forall a. HashSet a -> [a]
S.toList (ICtx -> HashSet Expr
icCands ICtx
ctx) 
  -- unfolds  <- evalCands ieKnowl ieEvEnv cands   
  [Unfold]
unfolds  <- Config -> Context -> Knowledge -> EvalEnv -> [Expr] -> IO [Unfold]
evalCandsLoop Config
ieCfg Context
ieSMT Knowledge
ieKnowl EvalEnv
ieEvEnv [Expr]
cands   
  (ICtx, InstRes) -> IO (ICtx, InstRes)
forall (m :: * -> *) a. Monad m => a -> m a
return    ((ICtx, InstRes) -> IO (ICtx, InstRes))
-> (ICtx, InstRes) -> IO (ICtx, InstRes)
forall a b. (a -> b) -> a -> b
$ InstEnv a
-> ICtx
-> InstRes
-> Maybe Int
-> Maybe SubcId
-> [Unfold]
-> (ICtx, InstRes)
forall a.
InstEnv a
-> ICtx
-> InstRes
-> Maybe Int
-> Maybe SubcId
-> [Unfold]
-> (ICtx, InstRes)
updCtxRes InstEnv a
env ICtx
ctx InstRes
res Maybe Int
i Maybe SubcId
cidMb (String -> [Unfold] -> [Unfold]
forall a. PPrint a => String -> a -> a
mytracepp  (String
"ple1-cands-unfolds: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe SubcId -> String
forall a. Show a => a -> String
show Maybe SubcId
cidMb) [Unfold]
unfolds)

_evalCands :: Knowledge -> EvalEnv -> [Expr] -> IO [Unfold] 
_evalCands :: Knowledge -> EvalEnv -> [Expr] -> IO [Unfold]
_evalCands Knowledge
_ EvalEnv
_  []    = [Unfold] -> IO [Unfold]
forall (m :: * -> *) a. Monad m => a -> m a
return []
_evalCands Knowledge
γ EvalEnv
s0 [Expr]
cands = do [[(Expr, Expr)]]
eqs <- (Expr -> IO [(Expr, Expr)]) -> [Expr] -> IO [[(Expr, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0) [Expr]
cands
                           [Unfold] -> IO [Unfold]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Unfold] -> IO [Unfold]) -> [Unfold] -> IO [Unfold]
forall a b. (a -> b) -> a -> b
$ [(Maybe Expr, [(Expr, Expr)])] -> [Unfold]
forall a. [(a, [(Expr, Expr)])] -> [(a, [Expr])]
mkUnfolds ([Maybe Expr] -> [[(Expr, Expr)]] -> [(Maybe Expr, [(Expr, Expr)])]
forall a b. [a] -> [b] -> [(a, b)]
zip (Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> [Expr] -> [Maybe Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
cands) [[(Expr, Expr)]]
eqs)

unfoldPred :: Config -> SMT.Context -> [Unfold] -> Pred 
unfoldPred :: Config -> Context -> [Unfold] -> Expr
unfoldPred Config
cfg Context
ctx = Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT Config
cfg Context
ctx [] (Expr -> Expr) -> ([Unfold] -> Expr) -> [Unfold] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
pAnd ([Expr] -> Expr) -> ([Unfold] -> [Expr]) -> [Unfold] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Unfold -> [Expr]) -> [Unfold] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Unfold -> [Expr]
forall a b. (a, b) -> b
snd  

evalCandsLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Expr] -> IO [Unfold] 
evalCandsLoop :: Config -> Context -> Knowledge -> EvalEnv -> [Expr] -> IO [Unfold]
evalCandsLoop Config
cfg Context
ctx Knowledge
γ EvalEnv
s0 [Expr]
cands = [Unfold] -> [Expr] -> IO [Unfold]
go [] [Expr]
cands 
  where 
    go :: [Unfold] -> [Expr] -> IO [Unfold]
go [Unfold]
acc []    = [Unfold] -> IO [Unfold]
forall (m :: * -> *) a. Monad m => a -> m a
return [Unfold]
acc 
    go [Unfold]
acc [Expr]
cands = do [[(Expr, Expr)]]
eqss   <- Context -> String -> IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]]
forall a. Context -> String -> IO a -> IO a
SMT.smtBracket Context
ctx String
"PLE.evaluate" (IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]])
-> IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]]
forall a b. (a -> b) -> a -> b
$ do
                                  Context -> Expr -> IO ()
SMT.smtAssert Context
ctx (Config -> Context -> [Unfold] -> Expr
unfoldPred Config
cfg Context
ctx [Unfold]
acc) 
                                  (Expr -> IO [(Expr, Expr)]) -> [Expr] -> IO [[(Expr, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0) [Expr]
cands
                      let us :: [(Maybe Expr, [(Expr, Expr)])]
us  = [Maybe Expr] -> [[(Expr, Expr)]] -> [(Maybe Expr, [(Expr, Expr)])]
forall a b. [a] -> [b] -> [(a, b)]
zip (Expr -> Maybe Expr
forall a. a -> Maybe a
Just (Expr -> Maybe Expr) -> [Expr] -> [Maybe Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
cands) [[(Expr, Expr)]]
eqss 
                      case [(Maybe Expr, [(Expr, Expr)])] -> [Unfold]
forall a. [(a, [(Expr, Expr)])] -> [(a, [Expr])]
mkUnfolds [(Maybe Expr, [(Expr, Expr)])]
us of 
                        []  -> [Unfold] -> IO [Unfold]
forall (m :: * -> *) a. Monad m => a -> m a
return [Unfold]
acc 
                        [Unfold]
us' -> do let acc' :: [Unfold]
acc'   = [Unfold]
acc [Unfold] -> [Unfold] -> [Unfold]
forall a. [a] -> [a] -> [a]
++ [Unfold]
us' 
                                  let oks :: HashSet Expr
oks    = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ Expr
e | (Just Expr
e, [Expr]
_) <- [Unfold]
us' ]
                                  let cands' :: [Expr]
cands' = [ Expr
e | Expr
e <- [Expr]
cands, Bool -> Bool
not (Expr -> HashSet Expr -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Expr
e HashSet Expr
oks) ] 
                                  [Unfold] -> [Expr] -> IO [Unfold]
go [Unfold]
acc' [Expr]
cands' 


---------------------------------------------------------------------------------------------- 
-- | 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
$ String -> [(Int, Expr)] -> [(Int, Expr)]
forall a. PPrint a => String -> a -> a
mytracepp  String
"ELAB-INST:  " ([(Int, Expr)] -> [(Int, Expr)]) -> [(Int, Expr)] -> [(Int, Expr)]
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 -> HashMap SubcId (SimpC a)
ieCstrs :: !(M.HashMap 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 -> [Expr]
icAssms  :: ![Pred]          -- ^ Hypotheses, already converted to SMT format 
  , ICtx -> HashSet Expr
icCands  :: S.HashSet Expr   -- ^ "Candidates" for unfolding
  , ICtx -> [Expr]
icEquals :: ![Expr]          -- ^ "Known" equalities
  , ICtx -> HashSet Expr
icSolved :: S.HashSet Expr   -- ^ Terms that we have already expanded
  } 

-- | @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 Unfold  = (Maybe Expr, [(Expr, Expr)])
type Unfold  = (Maybe Expr, [Expr])
type CTrie   = T.Trie   SubcId
type CBranch = T.Branch SubcId
type Diff    = [BindId]    -- ^ in "reverse" order

initCtx :: [Expr] -> ICtx
initCtx :: [Expr] -> ICtx
initCtx [Expr]
es = ICtx :: [Expr] -> HashSet Expr -> [Expr] -> HashSet Expr -> ICtx
ICtx 
  { icAssms :: [Expr]
icAssms  = [] 
  , icCands :: HashSet Expr
icCands  = HashSet Expr
forall a. Monoid a => a
mempty 
  , icEquals :: [Expr]
icEquals = String -> [Expr] -> [Expr]
forall a. PPrint a => String -> a -> a
mytracepp  String
"INITIAL-STUFF-INCR" [Expr]
es 
  , icSolved :: HashSet Expr
icSolved = HashSet Expr
forall a. Monoid a => a
mempty
  }

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

updCtxRes :: InstEnv a -> ICtx -> InstRes -> Maybe BindId -> Maybe SubcId -> [Unfold] -> (ICtx, InstRes) 
updCtxRes :: InstEnv a
-> ICtx
-> InstRes
-> Maybe Int
-> Maybe SubcId
-> [Unfold]
-> (ICtx, InstRes)
updCtxRes InstEnv a
env ICtx
ctx InstRes
res Maybe Int
iMb Maybe SubcId
cidMb [Unfold]
us 
                       = -- trace _msg 
                         ( ICtx
ctx { {- icCands  = cands', -} icSolved :: HashSet Expr
icSolved = HashSet Expr
solved', icEquals :: [Expr]
icEquals = [Expr]
forall a. Monoid a => a
mempty}
                         , InstRes
res'
                         ) 
  where 
    _msg :: String
_msg               = String -> (SubcId -> String) -> Maybe SubcId -> String
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe String
"nuttin\n" (InstEnv a -> InstRes -> SubcId -> String
forall a. InstEnv a -> InstRes -> SubcId -> String
debugResult InstEnv a
env InstRes
res') Maybe SubcId
cidMb
    res' :: InstRes
res'               = InstRes -> Maybe Int -> Expr -> InstRes
updRes InstRes
res Maybe Int
iMb ([Expr] -> Expr
pAnd [Expr]
solvedEqs) 
    _cands' :: HashSet Expr
_cands'             = ((ICtx -> HashSet Expr
icCands ICtx
ctx) HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet Expr
newCands) HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` HashSet Expr
solved' 
    solved' :: HashSet Expr
solved'            = HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union (ICtx -> HashSet Expr
icSolved ICtx
ctx) HashSet Expr
solvedCands 
    newCands :: HashSet Expr
newCands           = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
topApps [Expr]
newEqs) 
    solvedCands :: HashSet Expr
solvedCands        = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ Expr
e | (Just Expr
e, [Expr]
_) <- [Unfold]
okUnfolds ] 
    solvedEqs :: [Expr]
solvedEqs          = ICtx -> [Expr]
icEquals ICtx
ctx [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
newEqs 
    newEqs :: [Expr]
newEqs             = (Unfold -> [Expr]) -> [Unfold] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Unfold -> [Expr]
forall a b. (a, b) -> b
snd [Unfold]
okUnfolds
    okUnfolds :: [Unfold]
okUnfolds          = String -> [Unfold] -> [Unfold]
forall a. PPrint a => String -> a -> a
mytracepp  String
_str [ (Maybe Expr
eMb, [Expr]
ps)  | (Maybe Expr
eMb, [Expr]
ps) <- [Unfold]
us, {- let ps = equalitiesPred eqs, -} Bool -> Bool
not ([Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
ps) ] 
    _str :: String
_str               = String
"okUnfolds " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Maybe Int, Maybe SubcId) -> String
forall a. PPrint a => a -> String
showpp (Maybe Int
iMb, Maybe SubcId
cidMb)
    -- cands'             = S.difference (icCands ctx) (S.fromList solvedCands)
    -- solvedEqs          = icEquals ctx ++ concatMap snd us
    -- solvedCands        = [ e          | (Just e, _) <- us]

mkUnfolds :: [(a, [(Expr, Expr)])] -> [(a, [Expr])]
mkUnfolds :: [(a, [(Expr, Expr)])] -> [(a, [Expr])]
mkUnfolds [(a, [(Expr, Expr)])]
us = [ (a
eMb, [Expr]
ps)  | (a
eMb, [(Expr, Expr)]
eqs) <- [(a, [(Expr, Expr)])]
us
                            , let ps :: [Expr]
ps = [(Expr, Expr)] -> [Expr]
equalitiesPred [(Expr, Expr)]
eqs
                            , Bool -> Bool
not ([Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
ps) 
               ] 

debugResult :: InstEnv a -> InstRes -> SubcId -> String 
debugResult :: InstEnv a -> InstRes -> SubcId -> String
debugResult (InstEnv {HashMap SubcId (SimpC a)
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: HashMap 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 -> HashMap 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
..}) InstRes
res SubcId
i = String
msg 
  where 
    msg :: String
msg                          = String
"INCR-INSTANTIATE i = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SubcId -> String
forall a. Show a => a -> String
show SubcId
i 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
cidEqs 
    cidEqs :: Expr
cidEqs                       = [Expr] -> Expr
pAnd [ Expr
e | Int
i <- Path
cBinds, Expr
e <- Maybe Expr -> [Expr]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe Expr -> [Expr]) -> Maybe Expr -> [Expr]
forall a b. (a -> b) -> a -> b
$ Int -> InstRes -> Maybe Expr
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i InstRes
res ] 
    cBinds :: Path
cBinds                       = Path -> Path
forall a. Ord a => [a] -> [a]
L.sort (Path -> Path) -> (SubcId -> Path) -> SubcId -> Path
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> Path
elemsIBindEnv (IBindEnv -> Path) -> (SubcId -> IBindEnv) -> SubcId -> Path
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv (SimpC a -> IBindEnv) -> (SubcId -> SimpC a) -> SubcId -> IBindEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr HashMap SubcId (SimpC a)
ieCstrs (SubcId -> Path) -> SubcId -> Path
forall a b. (a -> b) -> a -> b
$ SubcId
i


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 {HashMap SubcId (SimpC a)
Config
BindEnv
AxiomEnv
Context
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: HashMap 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 -> HashMap 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 :: [Expr]
icAssms  = [Expr]
ctxEqs  
                    , icCands :: HashSet Expr
icCands  = HashSet Expr
cands   HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Semigroup a => a -> a -> a
<> ICtx -> HashSet Expr
icCands  ICtx
ctx
                    , icEquals :: [Expr]
icEquals = [Expr]
initEqs [Expr] -> [Expr] -> [Expr]
forall a. Semigroup a => a -> a -> a
<> ICtx -> [Expr]
icEquals ICtx
ctx }
  where         
    initEqs :: [Expr]
initEqs   = [(Expr, Expr)] -> [Expr]
equalitiesPred (Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)]
initEqualities Context
ieSMT AxiomEnv
ieAenv [(Symbol, SortedReft)]
bs)
    cands :: HashSet Expr
cands     = ([Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
topApps [Expr]
es0)) HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` (ICtx -> HashSet Expr
icSolved ICtx
ctx)
    ctxEqs :: [Expr]
ctxEqs    = Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT Config
ieCfg Context
ieSMT [] (Expr -> Expr) -> [Expr] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat 
                  [ [Expr]
initEqs 
                  , [ (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) ] 
                  ]
    ([(Symbol, SortedReft)]
bs, [Expr]
es0) = ((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 -> 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]
es)
    es :: [Expr]
es        = 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 HashMap 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

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

--------------------------------------------------------------------------------
-- | "Old" GLOBAL PLE 
--------------------------------------------------------------------------------
instantiate' :: (Loc a) => Config -> SInfo a -> IO (SInfo a)
instantiate' :: Config -> SInfo a -> IO (SInfo a)
instantiate' Config
cfg SInfo a
fi = Config
-> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
forall a.
Config
-> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
sInfo Config
cfg SymEnv
env SInfo a
fi ([((SubcId, SrcSpan), Expr)] -> SInfo a)
-> IO [((SubcId, SrcSpan), Expr)] -> IO (SInfo a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config
-> String
-> SymEnv
-> (Context -> IO [((SubcId, SrcSpan), Expr)])
-> IO [((SubcId, SrcSpan), Expr)]
forall a. Config -> String -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg String
file SymEnv
env Context -> IO [((SubcId, SrcSpan), Expr)]
act
  where
    act :: Context -> IO [((SubcId, SrcSpan), Expr)]
act Context
ctx         = [(SubcId, SimpC a)]
-> ((SubcId, SimpC a) -> IO ((SubcId, SrcSpan), Expr))
-> IO [((SubcId, SrcSpan), Expr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(SubcId, SimpC a)]
cstrs (((SubcId, SimpC a) -> IO ((SubcId, SrcSpan), Expr))
 -> IO [((SubcId, SrcSpan), Expr)])
-> ((SubcId, SimpC a) -> IO ((SubcId, SrcSpan), Expr))
-> IO [((SubcId, SrcSpan), Expr)]
forall a b. (a -> b) -> a -> b
$ \(SubcId
i, SimpC a
c) ->
                        ((SubcId
i,SimpC a -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan SimpC a
c),) (Expr -> ((SubcId, SrcSpan), Expr))
-> (Expr -> Expr) -> Expr -> ((SubcId, SrcSpan), Expr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp  (String
"INSTANTIATE i = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SubcId -> String
forall a. Show a => a -> String
show SubcId
i) (Expr -> ((SubcId, SrcSpan), Expr))
-> IO Expr -> IO ((SubcId, SrcSpan), Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Config
-> Context -> BindEnv -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
forall a.
Config
-> Context -> BindEnv -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
instSimpC Config
cfg Context
ctx (SInfo a -> BindEnv
forall (c :: * -> *) a. GInfo c a -> BindEnv
bs SInfo a
fi) AxiomEnv
aenv SubcId
i SimpC a
c
    cstrs :: [(SubcId, SimpC a)]
cstrs           = [ (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] 
    file :: String
file            = Config -> String
srcFile Config
cfg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".evals"
    env :: SymEnv
env             = Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi
    aenv :: AxiomEnv
aenv            = {- mytracepp  "AXIOM-ENV" -} (SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi)

sInfo :: Config -> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
sInfo :: Config
-> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
sInfo Config
cfg SymEnv
env SInfo a
fi [((SubcId, SrcSpan), Expr)]
ips = SInfo a -> [(SubcId, Expr)] -> SInfo a
forall a. SInfo a -> [(SubcId, Expr)] -> SInfo a
strengthenHyp SInfo a
fi (String -> [(SubcId, Expr)] -> [(SubcId, Expr)]
forall a. PPrint a => String -> a -> a
mytracepp  String
"ELAB-INST:  " ([(SubcId, Expr)] -> [(SubcId, Expr)])
-> [(SubcId, Expr)] -> [(SubcId, Expr)]
forall a b. (a -> b) -> a -> b
$ [SubcId] -> [Expr] -> [(SubcId, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((SubcId, SrcSpan) -> SubcId
forall a b. (a, b) -> a
fst ((SubcId, SrcSpan) -> SubcId) -> [(SubcId, SrcSpan)] -> [SubcId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubcId, SrcSpan)]
is) [Expr]
ps'')
  where
    ([(SubcId, SrcSpan)]
is, [Expr]
ps)         = [((SubcId, SrcSpan), Expr)] -> ([(SubcId, SrcSpan)], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip [((SubcId, SrcSpan), Expr)]
ips
    ps' :: [Expr]
ps'              = Config -> SymEnv -> [Expr] -> [Expr]
forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env [Expr]
ps
    ps'' :: [Expr]
ps''             = ((SubcId, SrcSpan) -> Expr -> Expr)
-> [(SubcId, SrcSpan)] -> [Expr] -> [Expr]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(SubcId
i, SrcSpan
sp) -> 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
sp (String
"PLE1 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SubcId -> String
forall a. Show a => a -> String
show SubcId
i)) SymEnv
env) [(SubcId, SrcSpan)]
is [Expr]
ps' 

instSimpC :: Config -> SMT.Context -> BindEnv -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
instSimpC :: Config
-> Context -> BindEnv -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
instSimpC Config
cfg Context
ctx BindEnv
bds AxiomEnv
aenv SubcId
sid SimpC a
sub 
  | AxiomEnv -> SubcId -> SimpC a -> Bool
forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
sid SimpC a
sub = do
    let is0 :: [Expr]
is0       = String -> [Expr] -> [Expr]
forall a. PPrint a => String -> a -> a
mytracepp  String
"INITIAL-STUFF" ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Equation -> Expr
eqBody (Equation -> Expr) -> [Equation] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (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
aenv) 
    let ([(Symbol, SortedReft)]
bs, [Expr]
es0) = BindEnv -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
forall a. BindEnv -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs BindEnv
bds SimpC a
sub
    [(Expr, Expr)]
equalities   <- Config
-> Context
-> AxiomEnv
-> [(Symbol, SortedReft)]
-> [Expr]
-> SubcId
-> IO [(Expr, Expr)]
evaluate Config
cfg Context
ctx AxiomEnv
aenv [(Symbol, SortedReft)]
bs [Expr]
es0 SubcId
sid 
    let evalEqs :: [Expr]
evalEqs   = [ Expr -> Expr -> Expr
EEq Expr
e1 Expr
e2 | (Expr
e1, Expr
e2) <- [(Expr, Expr)]
equalities, Expr
e1 Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= Expr
e2 ] 
    Expr -> IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return        (Expr -> IO Expr) -> Expr -> IO Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pAnd ([Expr]
is0 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
evalEqs)  
  | Bool
otherwise     = Expr -> IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PTrue

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) 

cstrExprs :: BindEnv -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs :: BindEnv -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs BindEnv
bds SimpC a
sub = ((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 -> 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]
es)
  where
    es :: [Expr]
es            = (SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
sub) 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)
    binds :: [(Symbol, SortedReft)]
binds         = BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv
bds (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
sub)

--------------------------------------------------------------------------------
-- | Symbolic Evaluation with SMT
--------------------------------------------------------------------------------
evaluate :: Config -> SMT.Context -> AxiomEnv -- ^ Definitions
         -> [(Symbol, SortedReft)]            -- ^ Environment of "true" facts 
         -> [Expr]                            -- ^ Candidates for unfolding 
         -> SubcId                            -- ^ Constraint Id
         -> IO [(Expr, Expr)]                 -- ^ Newly unfolded equalities
--------------------------------------------------------------------------------
evaluate :: Config
-> Context
-> AxiomEnv
-> [(Symbol, SortedReft)]
-> [Expr]
-> SubcId
-> IO [(Expr, Expr)]
evaluate Config
cfg Context
ctx AxiomEnv
aenv [(Symbol, SortedReft)]
facts [Expr]
es SubcId
sid = do 
  let eqs :: [(Expr, Expr)]
eqs      = Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)]
initEqualities Context
ctx AxiomEnv
aenv [(Symbol, SortedReft)]
facts  
  let γ :: Knowledge
γ        = Config -> Context -> AxiomEnv -> Knowledge
knowledge Config
cfg Context
ctx AxiomEnv
aenv 
  let cands :: [Expr]
cands    = String -> [Expr] -> [Expr]
forall a. PPrint a => String -> a -> a
mytracepp  (String
"evaluate-cands " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SubcId -> String
forall a. PPrint a => a -> String
showpp SubcId
sid) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [Expr]
forall k. (Eq k, Hashable k) => [k] -> [k]
Misc.hashNub ((Expr -> [Expr]) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
topApps [Expr]
es)
  let s0 :: EvalEnv
s0       = Int -> [(Expr, Expr)] -> AxiomEnv -> SymEnv -> Config -> EvalEnv
EvalEnv Int
0 [] AxiomEnv
aenv (Context -> SymEnv
SMT.ctxSymEnv Context
ctx) Config
cfg
  let ctxEqs :: [Expr]
ctxEqs   = [ Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT Config
cfg Context
ctx [] (Expr -> Expr -> Expr
EEq Expr
e1 Expr
e2) | (Expr
e1, Expr
e2)  <- [(Expr, Expr)]
eqs ]
              [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [ Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT Config
cfg Context
ctx [] ((Symbol, SortedReft) -> Expr
forall a. Expression a => a -> Expr
expr (Symbol, SortedReft)
xr)   | xr :: (Symbol, SortedReft)
xr@(Symbol
_, SortedReft
r) <- [(Symbol, SortedReft)]
facts, [KVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (SortedReft -> [KVar]
forall t. Visitable t => t -> [KVar]
Vis.kvars SortedReft
r) ] 
  [(Expr, Expr)]
eqss        <- Config
-> Context
-> Knowledge
-> EvalEnv
-> [Expr]
-> [Expr]
-> IO [(Expr, Expr)]
_evalLoop Config
cfg Context
ctx Knowledge
γ EvalEnv
s0 [Expr]
ctxEqs [Expr]
cands 
  [(Expr, Expr)] -> IO [(Expr, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return       ([(Expr, Expr)] -> IO [(Expr, Expr)])
-> [(Expr, Expr)] -> IO [(Expr, Expr)]
forall a b. (a -> b) -> a -> b
$ [(Expr, Expr)]
eqs [(Expr, Expr)] -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ [(Expr, Expr)]
eqss


 
_evalLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Pred] -> [Expr] -> IO [(Expr, Expr)]
_evalLoop :: Config
-> Context
-> Knowledge
-> EvalEnv
-> [Expr]
-> [Expr]
-> IO [(Expr, Expr)]
_evalLoop Config
cfg Context
ctx Knowledge
γ EvalEnv
s0 [Expr]
ctxEqs [Expr]
cands = SubcId -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
forall t.
Num t =>
t -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop SubcId
0 [] [Expr]
cands 
  where 
    loop :: t -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop t
_ [(Expr, Expr)]
acc []    = [(Expr, Expr)] -> IO [(Expr, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Expr, Expr)]
acc
    loop t
i [(Expr, Expr)]
acc [Expr]
cands = do let eqp :: Expr
eqp = Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT Config
cfg Context
ctx [] (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pAnd ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ [(Expr, Expr)] -> [Expr]
equalitiesPred [(Expr, Expr)]
acc
                          [[(Expr, Expr)]]
eqss <- Context -> String -> IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]]
forall a. Context -> String -> IO a -> IO a
SMT.smtBracket Context
ctx String
"PLE.evaluate" (IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]])
-> IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]]
forall a b. (a -> b) -> a -> b
$ do
                                    [Expr] -> (Expr -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Expr
eqp Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
ctxEqs) (Context -> Expr -> IO ()
SMT.smtAssert Context
ctx) 
                                    (Expr -> IO [(Expr, Expr)]) -> [Expr] -> IO [[(Expr, Expr)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0) [Expr]
cands
                          case [[(Expr, Expr)]] -> [(Expr, Expr)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Expr, Expr)]]
eqss of 
                            []   -> [(Expr, Expr)] -> IO [(Expr, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Expr, Expr)]
acc 
                            [(Expr, Expr)]
eqs' -> do let acc' :: [(Expr, Expr)]
acc'   = [(Expr, Expr)]
acc [(Expr, Expr)] -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. [a] -> [a] -> [a]
++ [(Expr, Expr)]
eqs' 
                                       let oks :: HashSet Expr
oks    = [Expr] -> HashSet Expr
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ((Expr, Expr) -> Expr
forall a b. (a, b) -> a
fst ((Expr, Expr) -> Expr) -> [(Expr, Expr)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Expr, Expr)]
eqs')
                                       let cands' :: [Expr]
cands' = [ Expr
e | Expr
e <- [Expr]
cands, Bool -> Bool
not (Expr -> HashSet Expr -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Expr
e HashSet Expr
oks) ] 
                                       t -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) [(Expr, Expr)]
acc' [Expr]
cands'



--------------------------------------------------------------------------------
data EvalEnv = EvalEnv
  { EvalEnv -> Int
evId        :: !Int
  , EvalEnv -> [(Expr, Expr)]
evSequence  :: [(Expr,Expr)]
  , EvalEnv -> AxiomEnv
_evAEnv     :: !AxiomEnv
  , EvalEnv -> SymEnv
evEnv       :: !SymEnv
  , EvalEnv -> Config
_evCfg      :: !Config
  }

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

evalOne :: Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne :: Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0 Expr
e = 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 -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
initCS (String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp String
"evalOne: " Expr
e)) EvalEnv
s0 
  if Expr
e' Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
e then [(Expr, Expr)] -> IO [(Expr, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else [(Expr, Expr)] -> IO [(Expr, Expr)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr
e, Expr
e') (Expr, Expr) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. a -> [a] -> [a]
: EvalEnv -> [(Expr, Expr)]
evSequence EvalEnv
st)

{- | [NOTE: Eval-Ite]  We should not be doing any PLE/eval under if-then-else where 
     the guard condition does not provably hold. For example, see issue #387.
     However, its ok and desirable to `eval` in this case, as long as one is not 
     unfolding recursive functions. To permit this, we track the "call-stack" and 
     whether or not, `eval` is occurring under an unresolved guard: if so, we do not 
     expand under any function that is already on the call-stack.
  -}

data Recur  = Ok | Stop deriving (Recur -> Recur -> Bool
(Recur -> Recur -> Bool) -> (Recur -> Recur -> Bool) -> Eq Recur
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Recur -> Recur -> Bool
$c/= :: Recur -> Recur -> Bool
== :: Recur -> Recur -> Bool
$c== :: Recur -> Recur -> Bool
Eq, Int -> Recur -> String -> String
[Recur] -> String -> String
Recur -> String
(Int -> Recur -> String -> String)
-> (Recur -> String) -> ([Recur] -> String -> String) -> Show Recur
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Recur] -> String -> String
$cshowList :: [Recur] -> String -> String
show :: Recur -> String
$cshow :: Recur -> String
showsPrec :: Int -> Recur -> String -> String
$cshowsPrec :: Int -> Recur -> String -> String
Show)
type CStack = ([Symbol], Recur)

instance PPrint Recur where 
  pprintTidy :: Tidy -> Recur -> Doc
pprintTidy Tidy
_ = Recur -> Doc
forall a. Show a => a -> Doc
Misc.tshow 

initCS :: CStack 
initCS :: CStack
initCS = ([], Recur
Ok)

pushCS :: CStack -> Symbol -> CStack 
pushCS :: CStack -> Symbol -> CStack
pushCS ([Symbol]
fs, Recur
r) Symbol
f = (Symbol
fSymbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
:[Symbol]
fs, Recur
r)

recurCS :: CStack -> Symbol -> Bool 
recurCS :: CStack -> Symbol -> Bool
recurCS ([Symbol]
_,  Recur
Ok) Symbol
_ = Bool
True 
-- recurCS (_,  _ ) _ = False -- not (f `elem` fs) 
recurCS ([Symbol]
fs, Recur
_) Symbol
f  = Bool -> Bool
not (Symbol
f Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
fs) 

noRecurCS :: CStack -> CStack 
noRecurCS :: CStack -> CStack
noRecurCS ([Symbol]
fs, Recur
_) = ([Symbol]
fs, Recur
Stop)

-- Don't evaluate under Lam, App, Ite, or Constants
topApps :: Expr -> [Expr]
topApps :: Expr -> [Expr]
topApps = Expr -> [Expr]
go 
  where 
    go :: Expr -> [Expr]
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@(EApp Expr
_ Expr
_)    = [Expr
e]
    go Expr
_               = []

-- makeLam is the adjoint of splitEApp
makeLam :: Knowledge -> Expr -> Expr
makeLam :: Knowledge -> Expr -> Expr
makeLam Knowledge
γ Expr
e = (Expr -> (Symbol, Sort) -> Expr)
-> Expr -> [(Symbol, Sort)] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (((Symbol, Sort) -> Expr -> Expr) -> Expr -> (Symbol, Sort) -> Expr
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Symbol, Sort) -> Expr -> Expr
ELam) Expr
e (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ)

eval :: Knowledge -> CStack -> Expr -> EvalST Expr
eval :: Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk = Expr -> StateT EvalEnv IO Expr
go 
  where 
    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 -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ' CStack
stk 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) = Expr -> StateT EvalEnv IO Expr
go Expr
b        StateT EvalEnv IO Expr
-> (Expr -> StateT EvalEnv IO Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Expr
b' -> Knowledge
-> CStack -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ CStack
stk 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
_)     = Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])
evalArgs Knowledge
γ CStack
stk Expr
e EvalST (Expr, [Expr])
-> ((Expr, [Expr]) -> StateT EvalEnv IO Expr)
-> StateT EvalEnv IO Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Knowledge
-> CStack -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalApp Knowledge
γ CStack
stk Expr
e 
    go e :: Expr
e@(EVar Symbol
_)       = Knowledge
-> CStack -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalApp  Knowledge
γ CStack
stk Expr
e (Expr
e, [])
    go (PAtom Brel
r Expr
e1 Expr
e2)  = 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
    go (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
<$> Expr -> StateT EvalEnv IO Expr
go Expr
e
    go (EBin Bop
o Expr
e1 Expr
e2)   = Bop -> Expr -> Expr -> Expr
EBin Bop
o       (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
    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 (PNot Expr
e)         = 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
    go (PImp Expr
e1 Expr
e2)     = 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
    go (PIff Expr
e1 Expr
e2)     = 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
    go (PAnd [Expr]
es)        = [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)
    go (POr [Expr]
es)         = [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)
    go Expr
e                = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

(<$$>) :: (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

-- | `evalArgs` also evaluates all the partial applications for hacky reasons,
--   suppose `foo g = id` then we want `foo g 10 = 10` and for that we need 
--   to `eval` the term `foo g` into `id` to tickle the `eval` on `id 10`.
--   This seems a bit of a hack. At any rate, this can lead to divergence. 
--   TODO: distill a .fq test from the MOSSAKA-hw3 example.

evalArgs :: Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])
evalArgs :: Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])
evalArgs Knowledge
γ CStack
stk Expr
e = [Expr] -> Expr -> EvalST (Expr, [Expr])
go [] Expr
e 
  where
    go :: [Expr] -> Expr -> EvalST (Expr, [Expr])
go [Expr]
acc (EApp Expr
f Expr
e)
      = do Expr
f' <- Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
evalOk Knowledge
γ CStack
stk Expr
f
           Expr
e' <- Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk Expr
e
           [Expr] -> Expr -> EvalST (Expr, [Expr])
go (Expr
e'Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
acc) Expr
f'
    go [Expr]
acc Expr
e
      = (,[Expr]
acc) (Expr -> (Expr, [Expr]))
-> StateT EvalEnv IO Expr -> EvalST (Expr, [Expr])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk Expr
e

-- | Minimal test case illustrating this `evalOk` hack is LH#tests/ple/pos/MossakaBug.hs
--   too tired & baffled to generate simple .fq version. TODO:nuke and rewrite PLE!
evalOk :: Knowledge -> CStack -> Expr -> EvalST Expr
evalOk :: Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
evalOk Knowledge
γ stk :: CStack
stk@([Symbol]
_, Recur
Ok) Expr
e = Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk Expr
e 
evalOk Knowledge
_ CStack
_           Expr
e = Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr
e 

{- 
evalArgs :: Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])
evalArgs 
  | True  = evalArgsOLD 
  | False = evalArgsNEW 

evalArgsNEW :: Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])
evalArgsNEW γ stk e = do 
    let (e1, es) = splitEApp e 
    e1' <- eval γ stk e1 
    es' <- mapM (eval γ stk) es 
    return (e1', es')

-}
    
evalApp :: Knowledge -> CStack -> Expr -> (Expr, [Expr]) -> EvalST Expr
-- evalApp γ stk e (e1, es) = tracepp ("evalApp:END" ++ showpp (e1,es)) <$> (evalAppAc γ stk e (e1, es))
evalApp :: Knowledge
-> CStack -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalApp Knowledge
γ CStack
stk Expr
e (Expr
e1, [Expr]
es) = do 
  Expr
res     <- Knowledge
-> CStack -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalAppAc Knowledge
γ CStack
stk Expr
e (Expr
e1, [Expr]
es)
  let diff :: Bool
diff = (Expr
res Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
/= (Expr -> [Expr] -> Expr
eApps Expr
e1 [Expr]
es))
  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
$ String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalApp:END:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. PPrint a => a -> String
showpp Bool
diff) Expr
res 

evalAppAc :: Knowledge -> CStack -> Expr -> (Expr, [Expr]) -> EvalST Expr

{- MOSSAKA-} 
evalAppAc :: Knowledge
-> CStack -> Expr -> (Expr, [Expr]) -> StateT EvalEnv IO Expr
evalAppAc Knowledge
γ CStack
stk Expr
e (EVar Symbol
f, [Expr
ex])
  | (EVar Symbol
dc, [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
ex
  , Just Rewrite
simp <- (Rewrite -> Bool) -> [Rewrite] -> Maybe Rewrite
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\Rewrite
simp -> (Rewrite -> Symbol
smName Rewrite
simp Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f) Bool -> Bool -> Bool
&& (Rewrite -> Symbol
smDC Rewrite
simp Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc)) (Knowledge -> [Rewrite]
knSims Knowledge
γ)
  , [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
simp) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  = do let msg :: String
msg    = String
"evalAppAc:ePop: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, Symbol, [Expr]) -> String
forall a. PPrint a => a -> String
showpp (Symbol
f, Symbol
dc, [Expr]
es)
       let ePopIf :: Expr
ePopIf = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp String
msg (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Expr -> Expr
substPopIf ([Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
simp) [Expr]
es) (Rewrite -> Expr
smBody Rewrite
simp)
       Expr
e'    <- Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk Expr
ePopIf 
       (Expr
e, String
"Rewrite -" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. PPrint a => a -> String
showpp Symbol
f) (Expr, String) -> Expr -> StateT EvalEnv IO Expr
~> Expr
e'

evalAppAc Knowledge
γ CStack
stk Expr
_ (EVar Symbol
f, [Expr]
es)
  -- we should move the lookupKnowledge stuff here into kmAms γ
  | 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
γ)
  , Just Expr
bd <- Equation -> Maybe Expr
getEqBody Equation
eq
  , [(Symbol, Sort)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  , Symbol
f Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Expr -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms Expr
bd               -- non-recursive equations << HACK! misses MUTUALLY RECURSIVE definitions! 
  , CStack -> Symbol -> Bool
recurCS CStack
stk Symbol
f 
  = 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 ee :: Expr
ee = SEnv Sort -> SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEq SEnv Sort
env SubstOp
PopIf Equation
eq [Expr]
es Expr
bd
       Knowledge -> Expr -> EvalST ()
assertSelectors Knowledge
γ Expr
ee 
       Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ (CStack -> Symbol -> CStack
pushCS CStack
stk Symbol
f) Expr
ee 

evalAppAc Knowledge
γ CStack
stk Expr
_e (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
γ)
  , Just Expr
bd <- Equation -> Maybe Expr
getEqBody Equation
eq
  , [(Symbol, Sort)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es   -- recursive equations
  , CStack -> Symbol -> Bool
recurCS CStack
stk Symbol
f 
  = 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
       String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"EVAL-REC-APP" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CStack, Expr) -> String
forall a. PPrint a => a -> String
showpp (CStack
stk, Expr
_e)) 
         (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> CStack -> Expr -> Expr -> StateT EvalEnv IO Expr
evalRecApplication Knowledge
γ (CStack -> Symbol -> CStack
pushCS CStack
stk Symbol
f) (Expr -> [Expr] -> Expr
eApps (Symbol -> Expr
EVar Symbol
f) [Expr]
es) (SEnv Sort -> SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEq SEnv Sort
env SubstOp
Normal Equation
eq [Expr]
es Expr
bd)

evalAppAc Knowledge
_ CStack
_ Expr
_ (Expr
f, [Expr]
es)
  = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Expr] -> Expr
eApps Expr
f [Expr]
es)

--------------------------------------------------------------------------------
-- | '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 -> SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEq :: SEnv Sort -> SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEq SEnv Sort
env SubstOp
o Equation
eq [Expr]
es Expr
bd = SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEqVal SubstOp
o Equation
eq [Expr]
es (SEnv Sort -> Equation -> [Expr] -> Expr -> Expr
substEqCoerce SEnv Sort
env Equation
eq [Expr]
es Expr
bd)

data SubstOp = PopIf | Normal

substEqVal :: SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEqVal :: SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEqVal SubstOp
o Equation
eq [Expr]
es Expr
bd = case SubstOp
o of
    SubstOp
PopIf  -> [(Symbol, Expr)] -> Expr -> Expr
substPopIf     [(Symbol, Expr)]
xes  Expr
bd
    SubstOp
Normal -> Subst -> Expr -> Expr
forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol, Expr)]
xes) Expr
bd
  where
    xes :: [(Symbol, Expr)]
xes    =  [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [Expr]
es
    xs :: [Symbol]
xs     =  Equation -> [Symbol]
eqArgNames Equation
eq

substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr -> Expr
substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr -> Expr
substEqCoerce SEnv Sort
env Equation
eq [Expr]
es Expr
bd = CoSub -> Expr -> Expr
Vis.applyCoSub CoSub
coSub Expr
bd
  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 = String -> CoSub -> CoSub
forall a. PPrint a => String -> a -> a
mytracepp  (String
"substEqCoerce" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Symbol, [Expr], [Sort], [Sort]) -> String
forall a. PPrint a => a -> String
showpp (Equation -> Symbol
eqName Equation
eq, [Expr]
es, [Sort]
eTs, [Sort]
ts)) (CoSub -> CoSub) -> CoSub -> CoSub
forall a b. (a -> b) -> a -> b
$ 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    = String -> Sort -> Sort
forall a. PPrint a => String -> a -> a
mytracepp (String
"UNITE: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Sort] -> String
forall a. PPrint a => a -> String
showpp [Sort]
ts) (Sort -> Sort) -> Sort -> Sort
forall a b. (a -> b) -> a -> b
$ 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         = String -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. PPrint a => String -> a -> a
mytracepp String
"mkCoSubXXX" ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ [(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) = String -> ([Sort], [Sort]) -> ([Sort], [Sort])
forall a. PPrint a => String -> a -> a
mytracepp String
"mkCoSub:MATCH" (([Sort], [Sort]) -> ([Sort], [Sort]))
-> ([Sort], [Sort]) -> ([Sort], [Sort])
forall a b. (a -> b) -> a -> b
$ ([Sort]
xTs, [Sort]
eTs)

matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
matchSorts Sort
s1 Sort
s2 = String -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. PPrint a => String -> a -> a
mytracepp  (String
"matchSorts :" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Sort, Sort) -> String
forall a. PPrint a => a -> String
showpp (Sort
s1, Sort
s2)) ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ 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
_             = []

--------------------------------------------------------------------------------
getEqBody :: Equation -> Maybe Expr
getEqBody :: Equation -> Maybe Expr
getEqBody (Equ Symbol
x [(Symbol, Sort)]
xts Expr
b Sort
_ Bool
_)
  | Just (Expr
fxs, Expr
e) <- Expr -> Maybe (Expr, Expr)
getEqBodyPred Expr
b
  , (EVar Symbol
f, [Expr]
es)  <- Expr -> (Expr, [Expr])
splitEApp Expr
fxs
  , Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
x
  , [Expr]
es [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
== (Symbol -> Expr
EVar (Symbol -> Expr)
-> ((Symbol, Sort) -> Symbol) -> (Symbol, Sort) -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, Sort) -> Expr) -> [(Symbol, Sort)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
xts)
  = Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
e
getEqBody Equation
_
  = Maybe Expr
forall a. Maybe a
Nothing

getEqBodyPred :: Expr -> Maybe (Expr, Expr)
getEqBodyPred :: Expr -> Maybe (Expr, Expr)
getEqBodyPred (PAtom Brel
Eq Expr
fxs Expr
e)
  = (Expr, Expr) -> Maybe (Expr, Expr)
forall a. a -> Maybe a
Just (Expr
fxs, Expr
e)
getEqBodyPred (PAnd ((PAtom Brel
Eq Expr
fxs Expr
e):[Expr]
_))
  = (Expr, Expr) -> Maybe (Expr, Expr)
forall a. a -> Maybe a
Just (Expr
fxs, Expr
e)
getEqBodyPred Expr
_
  = Maybe (Expr, Expr)
forall a. Maybe a
Nothing

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

substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
substPopIf [(Symbol, Expr)]
xes Expr
e = (Expr -> (Symbol, Expr) -> Expr)
-> Expr -> [(Symbol, Expr)] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Expr -> (Symbol, Expr) -> Expr
go Expr
e [(Symbol, Expr)]
xes
  where
    go :: Expr -> (Symbol, Expr) -> Expr
go Expr
e (Symbol
x, EIte Expr
b Expr
e1 Expr
e2) = Expr -> Expr -> Expr -> Expr
EIte Expr
b (Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
e (Symbol
x, Expr
e1)) (Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
e (Symbol
x, Expr
e2))
    go Expr
e (Symbol
x, Expr
ex)           = Expr -> (Symbol, Expr) -> Expr
forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
e (Symbol
x, Expr
ex)

-- see [NOTE:Eval-Ite] the below is wrong; we need to guard other branches too. sigh.

evalRecApplication :: Knowledge -> CStack -> Expr -> Expr -> EvalST Expr
evalRecApplication :: Knowledge -> CStack -> Expr -> Expr -> StateT EvalEnv IO Expr
evalRecApplication Knowledge
γ CStack
stk Expr
e (EIte Expr
b Expr
e1 Expr
e2) = do
  Bool
contra <- {- mytracepp  ("CONTRA? " ++ showpp e) <$> -} IO Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
PFalse)
  if Bool
contra
    then Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    else do Expr
b' <- Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk (String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp String
"REC-APP-COND" Expr
b) -- <<<<<<<<<<<<<<<<<<<<< MOSSAKA-LOOP?
            Bool
b1 <- IO Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
b')
            if Bool
b1
              then Knowledge -> Expr -> Expr -> EvalST ()
addEquality Knowledge
γ Expr
e Expr
e1 EvalST () -> EvalST () -> EvalST ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                   ({-# SCC "assertSelectors-1" #-} Knowledge -> Expr -> EvalST ()
assertSelectors Knowledge
γ Expr
e1) EvalST () -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                   Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk (String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalREC-1: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CStack -> String
forall a. PPrint a => a -> String
showpp CStack
stk) Expr
e1) StateT EvalEnv IO Expr
-> (Expr -> StateT EvalEnv IO Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                   ((Expr
e, String
"App1: ") (Expr, String) -> Expr -> StateT EvalEnv IO Expr
~>)
              else do
                   Bool
b2 <- IO Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
b'))
                   if Bool
b2
                      then Knowledge -> Expr -> Expr -> EvalST ()
addEquality Knowledge
γ Expr
e Expr
e2 EvalST () -> EvalST () -> EvalST ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                           ({-# SCC "assertSelectors-2" #-} Knowledge -> Expr -> EvalST ()
assertSelectors Knowledge
γ Expr
e2) EvalST () -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                           Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk (String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp (String
"evalREC-2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CStack -> String
forall a. PPrint a => a -> String
showpp CStack
stk) Expr
e2) StateT EvalEnv IO Expr
-> (Expr -> StateT EvalEnv IO Expr) -> StateT EvalEnv IO Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                           ((Expr
e, (String
"App2: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CStack -> String
forall a. PPrint a => a -> String
showpp CStack
stk ) ) (Expr, String) -> Expr -> StateT EvalEnv IO Expr
~>)
                      else Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
evalRecApplication Knowledge
_ CStack
_ Expr
_ Expr
e
  = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

addEquality :: Knowledge -> Expr -> Expr -> EvalST ()
addEquality :: Knowledge -> Expr -> Expr -> EvalST ()
addEquality Knowledge
γ Expr
e1 Expr
e2 =
  (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st{evSequence :: [(Expr, Expr)]
evSequence = (Knowledge -> Expr -> Expr
makeLam Knowledge
γ Expr
e1, Knowledge -> Expr -> Expr
makeLam Knowledge
γ Expr
e2)(Expr, Expr) -> [(Expr, Expr)] -> [(Expr, Expr)]
forall a. a -> [a] -> [a]
:EvalEnv -> [(Expr, Expr)]
evSequence EvalEnv
st})

evalIte :: Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
evalIte :: Knowledge
-> CStack -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
evalIte Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 Expr
e2 = String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp String
"evalIte:END: " (Expr -> Expr) -> StateT EvalEnv IO Expr -> StateT EvalEnv IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 
                            Knowledge
-> CStack -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
evalIteAc Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 (String -> Expr -> Expr
forall a. PPrint a => String -> a -> a
mytracepp String
msg Expr
e2) 
  where 
    msg :: String
msg = String
"evalIte:BEGINS: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (CStack, Expr) -> String
forall a. PPrint a => a -> String
showpp (CStack
stk, Expr
e) 


evalIteAc :: Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
evalIteAc :: Knowledge
-> CStack -> Expr -> Expr -> Expr -> Expr -> StateT EvalEnv IO Expr
evalIteAc Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 Expr
e2 
  = StateT EvalEnv IO (StateT EvalEnv IO Expr)
-> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (StateT EvalEnv IO (StateT EvalEnv IO Expr)
 -> StateT EvalEnv IO Expr)
-> StateT EvalEnv IO (StateT EvalEnv IO Expr)
-> StateT EvalEnv IO Expr
forall a b. (a -> b) -> a -> b
$ Knowledge
-> CStack
-> Expr
-> Expr
-> Expr
-> Expr
-> Bool
-> Bool
-> StateT EvalEnv IO Expr
evalIte' Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 Expr
e2 (Bool -> Bool -> StateT EvalEnv IO Expr)
-> StateT EvalEnv IO Bool
-> StateT EvalEnv IO (Bool -> StateT EvalEnv IO Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
b) StateT EvalEnv IO (Bool -> StateT EvalEnv IO Expr)
-> StateT EvalEnv IO Bool
-> StateT EvalEnv IO (StateT EvalEnv IO Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO Bool -> StateT EvalEnv IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
b))

evalIte' :: Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> Bool -> Bool -> EvalST Expr
evalIte' :: Knowledge
-> CStack
-> Expr
-> Expr
-> Expr
-> Expr
-> Bool
-> Bool
-> StateT EvalEnv IO Expr
evalIte' Knowledge
γ CStack
stk Expr
e Expr
_ Expr
e1 Expr
_ Bool
b Bool
_
  | Bool
b
  = do Expr
e' <- Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk Expr
e1
       (Expr
e, String
"If-True of:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. PPrint a => a -> String
showpp Bool
b)  (Expr, String) -> Expr -> StateT EvalEnv IO Expr
~> Expr
e'
evalIte' Knowledge
γ CStack
stk Expr
e Expr
_ Expr
_ Expr
e2 Bool
_ Bool
b'
  | Bool
b'
  = do Expr
e' <- Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk Expr
e2
       (Expr
e, String
"If-False") (Expr, String) -> Expr -> StateT EvalEnv IO Expr
~> Expr
e'
evalIte' Knowledge
γ CStack
stk Expr
_ Expr
b Expr
e1 Expr
e2 Bool
_ Bool
_
  -- see [NOTE:Eval-Ite] #387 
  = Expr -> Expr -> Expr -> Expr
EIte Expr
b (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 -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk' 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 -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk' Expr
e2 
    where stk' :: CStack
stk' = String -> CStack -> CStack
forall a. PPrint a => String -> a -> a
mytracepp String
"evalIte'" (CStack -> CStack) -> CStack -> CStack
forall a b. (a -> b) -> a -> b
$ CStack -> CStack
noRecurCS CStack
stk 

--------------------------------------------------------------------------------
-- | Knowledge (SMT Interaction)
--------------------------------------------------------------------------------
data Knowledge = KN 
  { Knowledge -> [Rewrite]
knSims    :: ![Rewrite]           -- ^ Measure info, asserted for each new Ctor ('assertSelectors')
  , Knowledge -> [Equation]
knAms     :: ![Equation]          -- ^ (Recursive) function definitions, used for PLE
  , 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)]
  }

isValid :: Knowledge -> Expr -> IO Bool
isValid :: Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
e = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
mytracepp (String
"isValid: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e) (Bool -> Bool) -> IO Bool -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 
                Knowledge -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knPreds Knowledge
γ (Knowledge -> Context
knContext Knowledge
γ) (Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ) Expr
e

isProof :: (a, SortedReft) -> Bool 
isProof :: (a, SortedReft) -> Bool
isProof (a
_, RR Sort
s Reft
_) = Sort -> String
forall a. PPrint a => a -> String
showpp Sort
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"Tuple"

knowledge :: Config -> SMT.Context -> AxiomEnv -> Knowledge
knowledge :: Config -> Context -> AxiomEnv -> Knowledge
knowledge Config
cfg Context
ctx AxiomEnv
aenv = KN :: [Rewrite]
-> [Equation]
-> Context
-> (Context -> [(Symbol, Sort)] -> Expr -> IO Bool)
-> [(Symbol, Sort)]
-> Knowledge
KN 
  { knSims :: [Rewrite]
knSims    = AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv
  , 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    = [] 
  } 

-- | This creates the rewrite rule e1 -> e2, applied when:
-- 1. when e2 is a DataCon and can lead to further reductions
-- 2. when size e2 < size e1
initEqualities :: SMT.Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)]
initEqualities :: Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)]
initEqualities Context
ctx AxiomEnv
aenv [(Symbol, SortedReft)]
es = ((Symbol, [Expr], Expr) -> [(Expr, Expr)])
-> [(Symbol, [Expr], Expr)] -> [(Expr, Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)]
makeSimplifications (AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv)) [(Symbol, [Expr], Expr)]
dcEqs
  where
    dcEqs :: [(Symbol, [Expr], Expr)]
dcEqs                  = [(Symbol, [Expr], Expr)] -> [(Symbol, [Expr], Expr)]
forall k. (Eq k, Hashable k) => [k] -> [k]
Misc.hashNub ([Maybe (Symbol, [Expr], Expr)] -> [(Symbol, [Expr], Expr)]
forall a. [Maybe a] -> [a]
Mb.catMaybes [SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
getDCEquality SymEnv
senv Expr
e1 Expr
e2 | EEq Expr
e1 Expr
e2 <- [Expr]
atoms])
    atoms :: [Expr]
atoms                  = Expr -> [Expr]
splitPAnd (Expr -> [Expr]) -> [Expr] -> [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ((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) -> Bool)
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Symbol, SortedReft) -> Bool
forall a. (a, SortedReft) -> Bool
isProof [(Symbol, SortedReft)]
es)
    senv :: SymEnv
senv                   = Context -> SymEnv
SMT.ctxSymEnv Context
ctx

-- AT: Non-obvious needed invariant: askSMT True is always the 
-- totality-effecting one.
-- RJ: What does "totality effecting" mean? 

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'                 = Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT Config
cfg Context
ctx [(Symbol, Sort)]
bs Expr
e 

toSMT :: Config -> SMT.Context -> [(Symbol, Sort)] -> Expr -> Pred
toSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT Config
cfg Context
ctx [(Symbol, Sort)]
bs = 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)
  where
    elabEnv :: [(Symbol, Sort)] -> SymEnv
elabEnv      = SymEnv -> [(Symbol, Sort)] -> SymEnv
insertsSymEnv SymEnv
senv
    senv :: SymEnv
senv         = Context -> SymEnv
SMT.ctxSymEnv Context
ctx

makeSimplifications :: [Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)]
makeSimplifications :: [Rewrite] -> (Symbol, [Expr], Expr) -> [(Expr, Expr)]
makeSimplifications [Rewrite]
sis (Symbol
dc, [Expr]
es, Expr
e)
     = Rewrite -> [(Expr, Expr)]
go (Rewrite -> [(Expr, Expr)]) -> [Rewrite] -> [(Expr, Expr)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Rewrite]
sis
 where
   go :: Rewrite -> [(Expr, Expr)]
go (SMeasure Symbol
f Symbol
dc' [Symbol]
xs Expr
bd)
     | Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc', [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
     = [(Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar Symbol
f) 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 [Symbol]
xs [Expr]
es) Expr
bd)]
   go Rewrite
_
     = []

getDCEquality :: SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
getDCEquality :: SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
getDCEquality SymEnv
senv Expr
e1 Expr
e2
  | Just Symbol
dc1 <- Maybe Symbol
f1
  , Just Symbol
dc2 <- Maybe Symbol
f2
  = if Symbol
dc1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc2
      then Maybe (Symbol, [Expr], Expr)
forall a. Maybe a
Nothing
      else String -> Maybe (Symbol, [Expr], Expr)
forall a. (?callStack::CallStack) => String -> a
error (String
"isDCEquality on" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. PPrint a => a -> String
showpp Expr
e2)
  | Just Symbol
dc1 <- Maybe Symbol
f1
  = (Symbol, [Expr], Expr) -> Maybe (Symbol, [Expr], Expr)
forall a. a -> Maybe a
Just (Symbol
dc1, [Expr]
es1, Expr
e2)
  | Just Symbol
dc2 <- Maybe Symbol
f2
  = (Symbol, [Expr], Expr) -> Maybe (Symbol, [Expr], Expr)
forall a. a -> Maybe a
Just (Symbol
dc2, [Expr]
es2, Expr
e1)
  | Bool
otherwise
  = Maybe (Symbol, [Expr], Expr)
forall a. Maybe a
Nothing
  where
    (Maybe Symbol
f1, [Expr]
es1) = (Expr -> Maybe Symbol) -> (Expr, [Expr]) -> (Maybe Symbol, [Expr])
forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst (SymEnv -> Expr -> Maybe Symbol
getDC SymEnv
senv) (Expr -> (Expr, [Expr])
splitEApp Expr
e1)
    (Maybe Symbol
f2, [Expr]
es2) = (Expr -> Maybe Symbol) -> (Expr, [Expr]) -> (Maybe Symbol, [Expr])
forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst (SymEnv -> Expr -> Maybe Symbol
getDC SymEnv
senv) (Expr -> (Expr, [Expr])
splitEApp Expr
e2)

-- TODO: Stringy hacks
getDC :: SymEnv -> Expr -> Maybe Symbol
getDC :: SymEnv -> Expr -> Maybe Symbol
getDC SymEnv
senv (EVar Symbol
x)
  | Symbol -> Bool
isUpperSymbol Symbol
x Bool -> Bool -> Bool
&& Maybe TheorySymbol -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (Symbol -> SymEnv -> Maybe TheorySymbol
symEnvTheory Symbol
x SymEnv
senv)
  = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
x
getDC SymEnv
_ Expr
_
  = Maybe Symbol
forall a. Maybe a
Nothing

isUpperSymbol :: Symbol -> Bool
isUpperSymbol :: Symbol -> Bool
isUpperSymbol Symbol
x = (Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Symbol -> Int
lengthSym Symbol
x') Bool -> Bool -> Bool
&& (Char -> Bool
isUpper (Char -> Bool) -> Char -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> Char
headSym Symbol
x')
  where 
    x' :: Symbol
x' = Symbol -> Symbol
dropModuleNames Symbol
x 

dropModuleNames :: Symbol -> Symbol
dropModuleNames :: Symbol -> Symbol
dropModuleNames = ([Text] -> Symbol) -> Text -> Symbol -> Symbol
mungeNames (Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> ([Text] -> Text) -> [Text] -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> Text
forall a. [a] -> a
last) Text
"."
  where
    mungeNames :: ([Text] -> Symbol) -> Text -> Symbol -> Symbol
mungeNames [Text] -> Symbol
_ Text
_ Symbol
""  = Symbol
""
    mungeNames [Text] -> Symbol
f Text
d s' :: Symbol
s'@(Symbol -> Text
symbolText -> Text
s)
      | Symbol
s' Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
tupConName = Symbol
tupConName
      | Bool
otherwise        = [Text] -> Symbol
f ([Text] -> Symbol) -> [Text] -> Symbol
forall a b. (a -> b) -> a -> b
$ Text -> Text -> [Text]
T.splitOn Text
d (Text -> [Text]) -> Text -> [Text]
forall a b. (a -> b) -> a -> b
$ Text -> Text
stripParens Text
s
    stripParens :: Text -> Text
stripParens Text
t = Text -> Maybe Text -> Text
forall a. a -> Maybe a -> a
Mb.fromMaybe Text
t ((Text -> Text -> Maybe Text
T.stripPrefix Text
"(" (Text -> Maybe Text) -> (Text -> Maybe Text) -> Text -> Maybe Text
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Text -> Text -> Maybe Text
T.stripSuffix Text
")") Text
t)

--------------------------------------------------------------------------------
-- | Creating Measure Info
--------------------------------------------------------------------------------
-- AT@TODO do this for all reflected functions, not just DataCons

{- [NOTE:Datacon-Selectors] The 'assertSelectors' function
   insert measure information for every constructor that appears
   in the expression e.

   In theory, this is not required as the SMT ADT encoding takes
   care of it. However, in practice, some constructors, e.g. from
   GADTs cannot be directly encoded in SMT due to the lack of SMTLIB
   support for GADT. Hence, we still need to hang onto this code.

   See tests/proof/ple2.fq for a concrete example.
 -}

assertSelectors :: Knowledge -> Expr -> EvalST ()
assertSelectors :: Knowledge -> Expr -> EvalST ()
assertSelectors Knowledge
γ Expr
e = do
    [Rewrite]
sims <- AxiomEnv -> [Rewrite]
aenvSimpl (AxiomEnv -> [Rewrite])
-> StateT EvalEnv IO AxiomEnv -> StateT EvalEnv IO [Rewrite]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EvalEnv -> AxiomEnv) -> StateT EvalEnv IO AxiomEnv
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets EvalEnv -> AxiomEnv
_evAEnv
    -- cfg  <- gets evCfg
    -- _    <- foldlM (\_ s -> Vis.mapMExpr (go s) e) (mytracepp  "assertSelector" e) sims
    [Rewrite] -> (Rewrite -> StateT EvalEnv IO Expr) -> EvalST ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Rewrite]
sims ((Rewrite -> StateT EvalEnv IO Expr) -> EvalST ())
-> (Rewrite -> StateT EvalEnv IO Expr) -> EvalST ()
forall a b. (a -> b) -> a -> b
$ \Rewrite
s -> (Expr -> StateT EvalEnv IO Expr) -> Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
Vis.mapMExpr (Rewrite -> Expr -> StateT EvalEnv IO Expr
go Rewrite
s) Expr
e
    () -> EvalST ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    go :: Rewrite -> Expr -> EvalST Expr
    go :: Rewrite -> Expr -> StateT EvalEnv IO Expr
go (SMeasure Symbol
f Symbol
dc [Symbol]
xs Expr
bd) e :: Expr
e@(EApp Expr
_ Expr
_)
      | (EVar Symbol
dc', [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
e
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc'
      , [Symbol] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
      = do let e1 :: Expr
e1 = Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar Symbol
f) Expr
e
           let e2 :: Expr
e2 = 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 [Symbol]
xs [Expr]
es) Expr
bd
           Knowledge -> Expr -> Expr -> EvalST ()
addEquality Knowledge
γ Expr
e1 Expr
e2
           Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    go Rewrite
_ Expr
e
      = Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

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

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

(~>) :: (Expr, String) -> Expr -> EvalST Expr
(Expr
e, String
_str) ~> :: (Expr, String) -> Expr -> StateT EvalEnv IO Expr
~> Expr
e' = do
  let msg :: String
msg = String
"PLE: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
_str String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Expr, Expr) -> String
forall a. PPrint a => a -> String
showpp (Expr
e, Expr
e') 
  (EvalEnv -> EvalEnv) -> EvalST ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st {evId :: Int
evId = (String -> Int -> Int
forall a. PPrint a => String -> a -> a
mytracepp String
msg (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ EvalEnv -> Int
evId EvalEnv
st) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1})
  Expr -> StateT EvalEnv IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'