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

{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE TupleSections             #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE 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 qualified Language.Fixpoint.Solver.Common as Common (toSMT)
import           Language.Fixpoint.Solver.Common          (askSMT)
import           Control.Monad ((>=>), foldM, forM, forM_, join)
import           Control.Monad.State
import           Data.Bifunctor (first, second)
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            (isDigit, isUpper)
-- import           Debug.Trace          (trace)
-- import           Text.Printf (printf)

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

--------------------------------------------------------------------------------
-- | Strengthen Constraint Environments via PLE
--------------------------------------------------------------------------------
instantiate :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate :: forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate Config
cfg SInfo a
info Maybe [SubcId]
subcIds
  | Bool -> Bool
not (Config -> Bool
oldPLE Config
cfg)
  = Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
PLE.instantiate Config
cfg SInfo a
info Maybe [SubcId]
subcIds

  | Config -> Bool
noIncrPle Config
cfg
  = Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate' Config
cfg SInfo a
info Maybe [SubcId]
subcIds

  | Bool
otherwise
  = Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
incrInstantiate' Config
cfg SInfo a
info Maybe [SubcId]
subcIds


-------------------------------------------------------------------------------
-- | New "Incremental" PLE -- see [NOTE:TREE-LIKE]

{- | [NOTE:TREE-LIKE] incremental PLE relies crucially on the SInfo satisfying
     a "tree like"   invariant:
       forall constraints c, c'.
         if i in c and i in c' then
           forall 0 <= j < i, j in c and j in c'

 -}

-------------------------------------------------------------------------------
incrInstantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
-------------------------------------------------------------------------------
incrInstantiate' :: forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
incrInstantiate' Config
cfg SInfo a
info Maybe [SubcId]
subcIds = 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
info), AxiomEnv -> SubcId -> SimpC a -> Bool
forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aEnv SubcId
i SimpC a
c
                      ,  Bool -> ([SubcId] -> Bool) -> Maybe [SubcId] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i SubcId -> [SubcId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds ]
    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 a. [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
-> [Char]
-> SymEnv
-> [Equation]
-> (Context -> IO InstRes)
-> IO InstRes
forall a.
Config
-> [Char] -> SymEnv -> [Equation] -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
sEnv (SInfo a -> [Equation]
forall (c :: * -> *) a. GInfo c a -> [Equation]
defns SInfo a
info) (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
info [(SubcId, SimpC a)]
cs)  -- 2. TRAVERSE Trie to compute InstRes
    SInfo a -> IO (SInfo a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SInfo a -> IO (SInfo a)) -> SInfo a -> IO (SInfo a)
forall a b. (a -> b) -> a -> b
$ Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
forall a. Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo Config
cfg SymEnv
sEnv SInfo a
info InstRes
res                                 -- 3. STRENGTHEN SInfo using InstRes
  where
    file :: [Char]
file   = Config -> [Char]
srcFile Config
cfg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
".evals"
    sEnv :: SymEnv
sEnv   = Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
info
    aEnv :: AxiomEnv
aEnv   = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
info



-------------------------------------------------------------------------------
-- | Step 1a: @instEnv@ sets up the incremental-PLE environment
instEnv :: (Loc a) => Config -> SInfo a -> [(SubcId, SimpC a)] -> SMT.Context -> InstEnv a
instEnv :: forall a.
Loc a =>
Config -> SInfo a -> [(SubcId, SimpC a)] -> Context -> InstEnv a
instEnv Config
cfg SInfo a
info [(SubcId, SimpC a)]
cs Context
ctx = Config
-> Context
-> BindEnv a
-> AxiomEnv
-> HashMap SubcId (SimpC a)
-> Knowledge
-> EvalEnv
-> InstEnv a
forall a.
Config
-> Context
-> BindEnv a
-> AxiomEnv
-> HashMap SubcId (SimpC a)
-> Knowledge
-> EvalEnv
-> InstEnv a
InstEnv Config
cfg Context
ctx BindEnv a
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 a
bEnv              = SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
info
    aEnv :: AxiomEnv
aEnv              = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
info
    γ :: 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 :: forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
ics  = [Char] -> CTrie -> CTrie
forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"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 :: forall a. 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
forall v. EquationV v -> ExprV v
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 a. [a] -> 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)]
forall v. EquationV v -> [(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 :: forall a.
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 a. a -> IO a
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 :: forall a.
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 :: forall a b.
InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms env :: InstEnv a
env@InstEnv{HashMap SubcId (SimpC a)
Config
BindEnv a
AxiomEnv
Context
Knowledge
EvalEnv
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieCfg :: Config
ieSMT :: Context
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: HashMap SubcId (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
ieCfg :: forall a. InstEnv a -> Config
ieSMT :: forall a. InstEnv a -> Context
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieKnowl :: forall a. InstEnv a -> Knowledge
ieEvEnv :: forall a. InstEnv a -> EvalEnv
..} 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 = [Char] -> [Expr] -> [Expr]
forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"ple1-assms: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Maybe SubcId, Path) -> [Char]
forall a. Show a => a -> [Char]
show (Maybe SubcId
cidMb, Path
delta)) (ICtx -> [Expr]
icAssms ICtx
ctx')
  Context -> [Char] -> IO b -> IO b
forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ieSMT  [Char]
"PLE.evaluate" (IO b -> IO b) -> IO b -> IO b
forall a b. (a -> b) -> a -> b
$ do
    [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 :: forall a.
InstEnv a
-> ICtx
-> Maybe Int
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
ple1 env :: InstEnv a
env@InstEnv{HashMap SubcId (SimpC a)
Config
BindEnv a
AxiomEnv
Context
Knowledge
EvalEnv
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieCfg :: forall a. InstEnv a -> Config
ieSMT :: forall a. InstEnv a -> Context
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieKnowl :: forall a. InstEnv a -> Knowledge
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieCfg :: Config
ieSMT :: Context
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: HashMap SubcId (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
..} ICtx
ctx Maybe Int
i Maybe SubcId
cidMb InstRes
res = do
  let cands :: [Expr]
cands = [Char] -> [Expr] -> [Expr]
forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"ple1-cands: "  [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe SubcId -> [Char]
forall a. Show a => a -> [Char]
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 a. a -> IO a
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 ([Char] -> [Unfold] -> [Unfold]
forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"ple1-cands-unfolds: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe SubcId -> [Char]
forall a. Show a => a -> [Char]
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 a. a -> IO a
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0) [Expr]
cands
                           [Unfold] -> IO [Unfold]
forall a. a -> IO a
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
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
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 = [Unfold] -> [Expr] -> IO [Unfold]
go []
  where
    go :: [Unfold] -> [Expr] -> IO [Unfold]
go [Unfold]
acc []    = [Unfold] -> IO [Unfold]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Unfold]
acc
    go [Unfold]
acc [Expr]
cands = do [[(Expr, Expr)]]
eqss   <- Context -> [Char] -> IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]]
forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ctx [Char]
"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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> IO a
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 :: forall a. Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo Config
cfg SymEnv
env SInfo a
info InstRes
res = SInfo a -> InstRes -> SInfo a
forall a. SInfo a -> InstRes -> SInfo a
strengthenBinds SInfo a
info 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
$ [Char] -> [(Int, Expr)] -> [(Int, Expr)]
forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"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 -> ElabParam -> Expr -> Expr
forall a. Elaborate a => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver Config
cfg) (SrcSpan -> [Char] -> Located [Char]
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan ([Char]
"PLE1 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) SymEnv
env)) 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
  { forall a. InstEnv a -> Config
ieCfg   :: !Config
  , forall a. InstEnv a -> Context
ieSMT   :: !SMT.Context
  , forall a. InstEnv a -> BindEnv a
ieBEnv  :: !(BindEnv a)
  , forall a. InstEnv a -> AxiomEnv
ieAenv  :: !AxiomEnv
  , forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieCstrs :: !(M.HashMap SubcId (SimpC a))
  , forall a. InstEnv a -> Knowledge
ieKnowl :: !Knowledge
  , forall a. InstEnv a -> EvalEnv
ieEvEnv :: !EvalEnv
  }

-- | @ICtx@ is the local information -- at each trie node -- obtained by incremental PLE
data ICtx    = ICtx
  { ICtx -> [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
  { icAssms :: [Expr]
icAssms  = []
  , icCands :: HashSet Expr
icCands  = HashSet Expr
forall a. Monoid a => a
mempty
  , icEquals :: [Expr]
icEquals = [Char] -> [Expr] -> [Expr]
forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"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
forall v. ExprV v -> ExprV v -> ExprV v
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 :: forall a.
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 = solved', icEquals = mempty}
                         , InstRes
res'
                         )
  where
    _msg :: [Char]
_msg               = [Char] -> (SubcId -> [Char]) -> Maybe SubcId -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe [Char]
"nuttin\n" (InstEnv a -> InstRes -> SubcId -> [Char]
forall a. InstEnv a -> InstRes -> SubcId -> [Char]
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
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd [Expr]
solvedEqs)
    _cands' :: HashSet Expr
_cands'             = (ICtx -> HashSet Expr
icCands ICtx
ctx HashSet Expr -> HashSet Expr -> HashSet Expr
forall a. Eq 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 => 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          = [Char] -> [Unfold] -> [Unfold]
forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
_str [ (Maybe Expr
eMb, [Expr]
ps)  | (Maybe Expr
eMb, [Expr]
ps) <- [Unfold]
us, {- let ps = equalitiesPred eqs, -} Bool -> Bool
not ([Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
ps) ]
    _str :: [Char]
_str               = [Char]
"okUnfolds " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Maybe Int, Maybe SubcId) -> [Char]
forall a. PPrint a => a -> [Char]
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 :: forall a. [(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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
ps)
               ]

debugResult :: InstEnv a -> InstRes -> SubcId -> String
debugResult :: forall a. InstEnv a -> InstRes -> SubcId -> [Char]
debugResult InstEnv{HashMap SubcId (SimpC a)
Config
BindEnv a
AxiomEnv
Context
Knowledge
EvalEnv
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieCfg :: forall a. InstEnv a -> Config
ieSMT :: forall a. InstEnv a -> Context
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieKnowl :: forall a. InstEnv a -> Knowledge
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieCfg :: Config
ieSMT :: Context
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: HashMap SubcId (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
..} InstRes
res SubcId
subId = [Char]
msg
  where
    msg :: [Char]
msg                          = [Char]
"INCR-INSTANTIATE i = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SubcId -> [Char]
forall a. Show a => a -> [Char]
show SubcId
subId [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
showpp Expr
cidEqs
    cidEqs :: Expr
cidEqs                       = [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
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
subId


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 :: forall a. InstEnv a -> ICtx -> Path -> Maybe SubcId -> ICtx
updCtx InstEnv {HashMap SubcId (SimpC a)
Config
BindEnv a
AxiomEnv
Context
Knowledge
EvalEnv
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieCfg :: forall a. InstEnv a -> Config
ieSMT :: forall a. InstEnv a -> Context
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieKnowl :: forall a. InstEnv a -> Knowledge
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieCfg :: Config
ieSMT :: Context
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: HashMap SubcId (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
..} ICtx
ctx Path
delta Maybe SubcId
cidMb
              = ICtx
ctx { icAssms  = ctxEqs
                    , icCands  = cands   <> icCands  ctx
                    , icEquals = initEqs <> icEquals 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]
initEqs [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++
                  [ (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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [KVar]
forall v. ExprV v -> [KVar]
Vis.kvarsExpr (Expr -> [KVar]) -> Expr -> [KVar]
forall a b. (a -> b) -> a -> b
$ ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> Expr) -> ReftV Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft SortedReft
r)
                  ])
    ([(Symbol, SortedReft)]
bs, [Expr]
es0) = ((SortedReft -> SortedReft)
-> (Symbol, SortedReft) -> (Symbol, SortedReft)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SortedReft -> SortedReft
unElabSortedReft ((Symbol, SortedReft) -> (Symbol, SortedReft))
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds, Expr -> Expr
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
forall v. ExprV v
PTrue SimpC a -> Expr
forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs Maybe (SimpC a)
subMb
    binds :: [(Symbol, SortedReft)]
binds     = [ (Symbol
x, SortedReft
y)  | Int
i <- Path
delta, let (Symbol
x, SortedReft
y, a
_) = Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv a
ieBEnv ]
    subMb :: Maybe (SimpC a)
subMb     = 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 :: forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr HashMap SubcId (SimpC a)
env SubcId
cid = [Char] -> SubcId -> HashMap SubcId (SimpC a) -> SimpC a
forall k v.
(HasCallStack, Eq k, Hashable k) =>
[Char] -> k -> HashMap k v -> v
Misc.safeLookup [Char]
"Instantiate.getCstr" SubcId
cid HashMap SubcId (SimpC a)
env

--------------------------------------------------------------------------------
-- | "Old" GLOBAL PLE
--------------------------------------------------------------------------------
instantiate' :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate' :: forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instantiate' Config
cfg SInfo a
info Maybe [SubcId]
subcIds = 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
info ([((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
-> [Char]
-> SymEnv
-> [Equation]
-> (Context -> IO [((SubcId, SrcSpan), Expr)])
-> IO [((SubcId, SrcSpan), Expr)]
forall a.
Config
-> [Char] -> SymEnv -> [Equation] -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
env (SInfo a -> [Equation]
forall (c :: * -> *) a. GInfo c a -> [Equation]
defns SInfo a
info) 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
. [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"INSTANTIATE i = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SubcId -> [Char]
forall a. Show a => a -> [Char]
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 a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
forall a.
Config
-> Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
instSimpC Config
cfg Context
ctx (SInfo a -> BindEnv a
forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
info) 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
info) , AxiomEnv -> SubcId -> SimpC a -> Bool
forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
i SimpC a
c
                               ,  Bool -> ([SubcId] -> Bool) -> Maybe [SubcId] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i SubcId -> [SubcId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds ]
    file :: [Char]
file            = Config -> [Char]
srcFile Config
cfg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
".evals"
    env :: SymEnv
env             = Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
info
    aenv :: AxiomEnv
aenv            = {- mytracepp  "AXIOM-ENV" -} SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
info

sInfo :: Config -> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
sInfo :: forall a.
Config
-> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
sInfo Config
cfg SymEnv
env SInfo a
info [((SubcId, SrcSpan), Expr)]
ips = SInfo a -> [(SubcId, Expr)] -> SInfo a
forall a. SInfo a -> [(SubcId, Expr)] -> SInfo a
strengthenHyp SInfo a
info ([Char] -> [(SubcId, Expr)] -> [(SubcId, Expr)]
forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"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) -> ElabParam -> Expr -> Expr
forall a. Elaborate a => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver Config
cfg) (SrcSpan -> [Char] -> Located [Char]
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
sp ([Char]
"PLE1 " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SubcId -> [Char]
forall a. Show a => a -> [Char]
show SubcId
i)) SymEnv
env)) [(SubcId, SrcSpan)]
is [Expr]
ps'

instSimpC :: Config -> SMT.Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
instSimpC :: forall a.
Config
-> Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
instSimpC Config
cfg Context
ctx BindEnv a
bds AxiomEnv
aenv SubcId
subId SimpC a
sub
  | AxiomEnv -> SubcId -> SimpC a -> Bool
forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
subId SimpC a
sub = do
    let is0 :: [Expr]
is0       = [Char] -> [Expr] -> [Expr]
forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"INITIAL-STUFF" ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Equation -> Expr
forall v. EquationV v -> ExprV v
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 a. [a] -> 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)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs) (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
aenv)
    let ([(Symbol, SortedReft)]
bs, [Expr]
es0) = BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
forall a. BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs BindEnv a
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
subId
    let evalEqs :: [Expr]
evalEqs   = [ Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return        (Expr -> IO Expr) -> Expr -> IO Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([Expr]
is0 [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
evalEqs)
  | Bool
otherwise     = Expr -> IO Expr
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
forall v. ExprV v
PTrue

isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr :: forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
subId 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
subId (AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
aenv)

cstrExprs :: BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs :: forall a. BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs BindEnv a
bds SimpC a
sub = ((SortedReft -> SortedReft)
-> (Symbol, SortedReft) -> (Symbol, SortedReft)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SortedReft -> SortedReft
unElabSortedReft ((Symbol, SortedReft) -> (Symbol, SortedReft))
-> [(Symbol, SortedReft)] -> [(Symbol, SortedReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds, Expr -> Expr
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 a -> IBindEnv -> [(Symbol, SortedReft)]
forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
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
subId = 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    = [Char] -> [Expr] -> [Expr]
forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"evaluate-cands " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SubcId -> [Char]
forall a. PPrint a => a -> [Char]
showpp SubcId
subId) ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
Misc.setNub ((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
forall v. ExprV v -> ExprV v -> ExprV v
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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [KVar]
forall v. ExprV v -> [KVar]
Vis.kvarsExpr (Expr -> [KVar]) -> Expr -> [KVar]
forall a b. (a -> b) -> a -> b
$ ReftV Symbol -> Expr
forall v. ReftV v -> ExprV v
reftPred (ReftV Symbol -> Expr) -> ReftV Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ SortedReft -> ReftV Symbol
sr_reft 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 a. a -> IO a
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 = SubcId -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop SubcId
0 []
  where
    loop :: SubcId -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop SubcId
_ [(Expr, Expr)]
acc []    = [(Expr, Expr)] -> IO [(Expr, Expr)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Expr, Expr)]
acc
    loop SubcId
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
forall v. (Fixpoint v, Ord v) => ListNE (ExprV v) -> ExprV v
pAnd ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ [(Expr, Expr)] -> [Expr]
equalitiesPred [(Expr, Expr)]
acc
                          [[(Expr, Expr)]]
eqss <- Context -> [Char] -> IO [[(Expr, Expr)]] -> IO [[(Expr, Expr)]]
forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ctx [Char]
"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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> IO a
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) ]
                                       SubcId -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop (SubcId
i SubcId -> SubcId -> SubcId
forall a. Num a => a -> a -> a
+ SubcId
1 :: Integer) [(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 ([Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [] else [(Expr, Expr)] -> IO [(Expr, Expr)]
forall a. a -> IO a
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
$c== :: Recur -> Recur -> Bool
== :: Recur -> Recur -> Bool
$c/= :: Recur -> Recur -> Bool
/= :: Recur -> Recur -> Bool
Eq, Int -> Recur -> [Char] -> [Char]
[Recur] -> [Char] -> [Char]
Recur -> [Char]
(Int -> Recur -> [Char] -> [Char])
-> (Recur -> [Char]) -> ([Recur] -> [Char] -> [Char]) -> Show Recur
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> Recur -> [Char] -> [Char]
showsPrec :: Int -> Recur -> [Char] -> [Char]
$cshow :: Recur -> [Char]
show :: Recur -> [Char]
$cshowList :: [Recur] -> [Char] -> [Char]
showList :: [Recur] -> [Char] -> [Char]
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  = Symbol
f Symbol -> [Symbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [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]
forall {v}. ExprV v -> [ExprV v]
go
  where
    go :: ExprV v -> [ExprV v]
go (PAnd [ExprV v]
es)       = (ExprV v -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV v -> [ExprV v]
go [ExprV v]
es
    go (POr [ExprV v]
es)        = (ExprV v -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV v -> [ExprV v]
go [ExprV v]
es
    go (PAtom Brel
_ ExprV v
e1 ExprV v
e2) = ExprV v -> [ExprV v]
go ExprV v
e1  [ExprV v] -> [ExprV v] -> [ExprV v]
forall a. [a] -> [a] -> [a]
++ ExprV v -> [ExprV v]
go ExprV v
e2
    go (PIff ExprV v
e1 ExprV v
e2)    = ExprV v -> [ExprV v]
go ExprV v
e1  [ExprV v] -> [ExprV v] -> [ExprV v]
forall a. [a] -> [a] -> [a]
++ ExprV v -> [ExprV v]
go ExprV v
e2
    go (PImp ExprV v
e1 ExprV v
e2)    = ExprV v -> [ExprV v]
go ExprV v
e1  [ExprV v] -> [ExprV v] -> [ExprV v]
forall a. [a] -> [a] -> [a]
++ ExprV v -> [ExprV v]
go ExprV v
e2
    go (EBin  Bop
_ ExprV v
e1 ExprV v
e2) = ExprV v -> [ExprV v]
go ExprV v
e1  [ExprV v] -> [ExprV v] -> [ExprV v]
forall a. [a] -> [a] -> [a]
++ ExprV v -> [ExprV v]
go ExprV v
e2
    go (PNot ExprV v
e)        = ExprV v -> [ExprV v]
go ExprV v
e
    go (ENeg ExprV v
e)        = ExprV v -> [ExprV v]
go ExprV v
e
    go e :: ExprV v
e@(EApp ExprV v
_ ExprV v
_)    = [ExprV v
e]
    go ExprV v
_               = []

-- 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 b a. (b -> a -> b) -> b -> [a] -> b
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
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
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
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
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 = (x, s) : knLams γ }
    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 a b.
StateT EvalEnv IO a
-> (a -> StateT EvalEnv IO b) -> StateT EvalEnv IO b
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
forall v. Sort -> Sort -> ExprV v -> ExprV v
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 a b.
StateT EvalEnv IO a
-> (a -> StateT EvalEnv IO b) -> StateT EvalEnv IO b
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
forall v. Brel -> ExprV v -> ExprV v -> ExprV v
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 a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
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
forall v. ExprV v -> ExprV v
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
forall v. Bop -> ExprV v -> ExprV v -> ExprV v
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 a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
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
forall v. ExprV v -> Sort -> ExprV v
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
forall v. ExprV v -> Symbol -> ExprV v
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
forall v. ExprV v -> ExprV v
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
forall v. ExprV v -> ExprV v -> ExprV v
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 a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
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
forall v. ExprV v -> ExprV v -> ExprV v
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 a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
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
forall v. [ExprV v] -> ExprV v
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 (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
es)
    go (POr [Expr]
es)         = [Expr] -> Expr
forall v. [ExprV v] -> ExprV v
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 (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
`traverse` [Expr]
es)
    go Expr
e                = Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

-- | `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] -> Expr -> EvalST (Expr, [Expr])
go []
  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 a. a -> StateT EvalEnv IO a
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
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps Expr
e1 [Expr]
es
  Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
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
$ [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalApp:END:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. PPrint a => a -> [Char]
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])
forall v. ExprV v -> (ExprV v, [ExprV v])
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 a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  = do let msg :: [Char]
msg    = [Char]
"evalAppAc:ePop: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Symbol, Symbol, [Expr]) -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Symbol
f, Symbol
dc, [Expr]
es)
       let ePopIf :: Expr
ePopIf = [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
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, [Char]
"Rewrite -" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. PPrint a => a -> [Char]
showpp Symbol
f) (Expr, [Char]) -> 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
forall v. EquationV v -> Symbol
eqName) (Knowledge -> [Equation]
knAms Knowledge
γ)
  , Just Expr
bd <- Equation -> Maybe Expr
getEqBody Equation
eq
  , [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs Equation
eq) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall a. [a] -> 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   <- (EvalEnv -> SEnv Sort) -> StateT EvalEnv IO (SEnv Sort)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort (SymEnv -> SEnv Sort)
-> (EvalEnv -> SymEnv) -> EvalEnv -> SEnv Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalEnv -> SymEnv
evEnv)
       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
forall v. EquationV v -> Symbol
eqName) (Knowledge -> [Equation]
knAms Knowledge
γ)
  , Just Expr
bd <- Equation -> Maybe Expr
getEqBody Equation
eq
  , [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs Equation
eq) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall a. [a] -> 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      <- (EvalEnv -> SEnv Sort) -> StateT EvalEnv IO (SEnv Sort)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort (SymEnv -> SEnv Sort)
-> (EvalEnv -> SymEnv) -> EvalEnv -> SEnv Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalEnv -> SymEnv
evEnv)
       [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"EVAL-REC-APP" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (CStack, Expr) -> [Char]
forall a. PPrint a => a -> [Char]
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
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (Symbol -> Expr
forall v. v -> ExprV v
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 a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> [Expr] -> Expr
forall v. ExprV v -> [ExprV v] -> ExprV v
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)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs Equation
eq
    sp :: SrcSpan
sp    = [Char] -> SrcSpan
panicSpan [Char]
"mkCoSub"
    eTs :: [Sort]
eTs   = SrcSpan -> SEnv Sort -> Expr -> Sort
sortExpr SrcSpan
sp SEnv Sort
env (Expr -> Sort) -> [Expr] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    coSub :: CoSub
coSub = [Char] -> CoSub -> CoSub
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"substEqCoerce" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Symbol, [Expr], [Sort], [Sort]) -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Equation -> Symbol
forall v. EquationV v -> 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    = [Char] -> Sort -> Sort
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"UNITE: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Sort] -> [Char]
forall a. PPrint a => a -> [Char]
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
symToSearch [Sort]
ts)
    symToSearch :: Env
symToSearch = SEnv Sort -> Env
forall a. SEnv a -> Symbol -> SESearch a
mkSearchEnv SEnv Sort
env
    uError :: a -> a
uError a
ts   = [Char] -> a
forall a. [Char] -> a
panic ([Char]
"mkCoSub: cannot build CoSub for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)] -> [Char]
forall a. PPrint a => a -> [Char]
showpp [(Symbol, Sort)]
xys [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" cannot unify " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. PPrint a => a -> [Char]
showpp a
ts)
    xys :: [(Symbol, Sort)]
xys         = [Char] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"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) = [Char] -> ([Sort], [Sort]) -> ([Sort], [Sort])
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"mkCoSub:MATCH" ([Sort]
xTs, [Sort]
eTs)

matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
matchSorts Sort
sort1 Sort
sort2 = [Char] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"matchSorts :" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Sort, Sort) -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Sort
sort1, Sort
sort2)) ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> [(Symbol, Sort)]
go Sort
sort1 Sort
sort2
  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])
forall v. ExprV v -> (ExprV v, [ExprV v])
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
forall v. v -> ExprV v
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)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs

substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
substPopIf [(Symbol, Expr)]
xes Expr
expr' = (Expr -> (Symbol, Expr) -> Expr)
-> Expr -> [(Symbol, Expr)] -> Expr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Expr -> (Symbol, Expr) -> Expr
go Expr
expr' [(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
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
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 a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
forall v. ExprV v
PFalse)
  if Bool
contra
    then Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
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 ([Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"REC-APP-COND" Expr
b) -- <<<<<<<<<<<<<<<<<<<<< MOSSAKA-LOOP?
            Bool
b1 <- IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
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 a b.
StateT EvalEnv IO a -> StateT EvalEnv IO b -> StateT EvalEnv IO b
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 a b.
StateT EvalEnv IO a -> StateT EvalEnv IO b -> StateT EvalEnv IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                   Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk ([Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalREC-1: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CStack -> [Char]
forall a. PPrint a => a -> [Char]
showpp CStack
stk) Expr
e1) StateT EvalEnv IO Expr
-> (Expr -> StateT EvalEnv IO Expr) -> StateT EvalEnv IO Expr
forall a b.
StateT EvalEnv IO a
-> (a -> StateT EvalEnv IO b) -> StateT EvalEnv IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                   ((Expr
e, [Char]
"App1: ") (Expr, [Char]) -> Expr -> StateT EvalEnv IO Expr
~>)
              else do
                   Bool
b2 <- IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
forall v. ExprV v -> ExprV v
PNot Expr
b'))
                   if Bool
b2
                      then Knowledge -> Expr -> Expr -> EvalST ()
addEquality Knowledge
γ Expr
e Expr
e2 EvalST () -> EvalST () -> EvalST ()
forall a b.
StateT EvalEnv IO a -> StateT EvalEnv IO b -> StateT EvalEnv IO b
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 a b.
StateT EvalEnv IO a -> StateT EvalEnv IO b -> StateT EvalEnv IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                           Knowledge -> CStack -> Expr -> StateT EvalEnv IO Expr
eval Knowledge
γ CStack
stk ([Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalREC-2: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CStack -> [Char]
forall a. PPrint a => a -> [Char]
showpp CStack
stk) Expr
e2) StateT EvalEnv IO Expr
-> (Expr -> StateT EvalEnv IO Expr) -> StateT EvalEnv IO Expr
forall a b.
StateT EvalEnv IO a
-> (a -> StateT EvalEnv IO b) -> StateT EvalEnv IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                           ((Expr
e, [Char]
"App2: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ CStack -> [Char]
forall a. PPrint a => a -> [Char]
showpp CStack
stk ) (Expr, [Char]) -> Expr -> StateT EvalEnv IO Expr
~>)
                      else Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
evalRecApplication Knowledge
_ CStack
_ Expr
_ Expr
e
  = Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
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 = (makeLam γ e1, makeLam γ e2):evSequence 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 = [Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"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 ([Char] -> Expr -> Expr
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
msg Expr
e2)
  where
    msg :: [Char]
msg = [Char]
"evalIte:BEGINS: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (CStack, Expr) -> [Char]
forall a. PPrint a => a -> [Char]
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 a. IO a -> StateT EvalEnv IO a
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 a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO Bool -> StateT EvalEnv IO Bool
forall a. IO a -> StateT EvalEnv IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
forall v. ExprV v -> ExprV v
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, [Char]
"If-True of:" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. PPrint a => a -> [Char]
showpp Bool
b)  (Expr, [Char]) -> 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, [Char]
"If-False") (Expr, [Char]) -> 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
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
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 a b.
StateT EvalEnv IO (a -> b)
-> StateT EvalEnv IO a -> StateT EvalEnv IO b
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' = [Char] -> CStack -> CStack
forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"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 = [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"isValid: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
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 :: forall a. (a, SortedReft) -> Bool
isProof (a
_, RR Sort
s ReftV Symbol
_) = Sort -> [Char]
forall a. PPrint a => a -> [Char]
showpp Sort
s [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
"Tuple"

knowledge :: Config -> SMT.Context -> AxiomEnv -> Knowledge
knowledge :: Config -> Context -> AxiomEnv -> Knowledge
knowledge Config
cfg Context
ctx AxiomEnv
aenv = 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 a. Ord a => [a] -> [a]
Misc.setNub ([Maybe (Symbol, [Expr], Expr)] -> [(Symbol, [Expr], Expr)]
forall a. [Maybe a] -> [a]
Mb.catMaybes [SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
getDCEquality SymEnv
symEnv' Expr
e1 Expr
e2 | EEq Expr
e1 Expr
e2 <- [Expr]
atoms])
    atoms :: [Expr]
atoms                  = Expr -> [Expr]
splitPAnd (Expr -> [Expr])
-> ((Symbol, SortedReft) -> Expr) -> (Symbol, SortedReft) -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft) -> Expr
forall a. Expression a => a -> Expr
expr ((Symbol, SortedReft) -> [Expr])
-> [(Symbol, SortedReft)] -> [Expr]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m 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
    symEnv' :: SymEnv
symEnv'                = 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?

toSMT :: Config -> SMT.Context -> [(Symbol, Sort)] -> Expr -> Pred
toSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
toSMT = [Char] -> Config -> Context -> [(Symbol, Sort)] -> Expr -> Expr
Common.toSMT [Char]
"Instantiate.toSMT"

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 a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
     = [(Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
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 [Char] -> Maybe (Symbol, [Expr], Expr)
forall a. HasCallStack => [Char] -> a
error ([Char]
"isDCEquality on" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
showpp Expr
e1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. PPrint a => a -> [Char]
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 b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SymEnv -> Expr -> Maybe Symbol
getDC SymEnv
sEnv) (Expr -> (Expr, [Expr])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp Expr
e1)
    (Maybe Symbol
f2, [Expr]
es2) = (Expr -> Maybe Symbol) -> (Expr, [Expr]) -> (Maybe Symbol, [Expr])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (SymEnv -> Expr -> Maybe Symbol
getDC SymEnv
sEnv) (Expr -> (Expr, [Expr])
forall v. ExprV v -> (ExprV v, [ExprV v])
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 (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. HasCallStack => [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 -> Bool
isTupleSymbol Symbol
s' = Symbol
s'
      | Bool
otherwise        = [Text] -> Symbol
f ([Text] -> Symbol) -> [Text] -> Symbol
forall a b. (a -> b) -> a -> b
$ HasCallStack => Text -> Text -> [Text]
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)

    -- TODO: Remove this code which is LH specific
    isTupleSymbol :: Symbol -> Bool
    isTupleSymbol :: Symbol -> Bool
isTupleSymbol Symbol
s =
      let t :: Text
t = Symbol -> Text
symbolText Symbol
s
       in Text -> Text -> Bool
T.isPrefixOf Text
"Tuple" Text
t Bool -> Bool -> Bool
&&
          (Char -> Bool) -> Text -> Bool
T.all Char -> Bool
isDigit (Int -> Text -> Text
T.drop Int
5 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
expr' = do
    [Rewrite]
sims <- (EvalEnv -> [Rewrite]) -> StateT EvalEnv IO [Rewrite]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (AxiomEnv -> [Rewrite]
aenvSimpl (AxiomEnv -> [Rewrite])
-> (EvalEnv -> AxiomEnv) -> EvalEnv -> [Rewrite]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
expr'
  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])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp Expr
e
      , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc'
      , [Symbol] -> Int
forall a. [a] -> 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
      = do let e1 :: Expr
e1 = Expr -> Expr -> Expr
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> Expr
forall v. v -> ExprV v
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 a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    go Rewrite
_ Expr
e
      = Expr -> StateT EvalEnv IO Expr
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

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

withCtx :: Config -> FilePath -> SymEnv -> [Equation] -> (SMT.Context -> IO a) -> IO a
withCtx :: forall a.
Config
-> [Char] -> SymEnv -> [Equation] -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
env [Equation]
defns Context -> IO a
k = do
  Context
ctx <- Config -> [Char] -> SymEnv -> [Equation] -> IO Context
SMT.makeContextWithSEnv Config
cfg [Char]
file SymEnv
env [Equation]
defns
  ()
_   <- Context -> IO ()
SMT.smtPush Context
ctx
  a
res <- Context -> IO a
k Context
ctx
  Context -> IO ()
SMT.cleanupContext Context
ctx
  a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

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