--------------------------------------------------------------------------------
-- | 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 #-}

{-# OPTIONS_GHC -Wno-name-shadowing    #-}

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.State
import           Data.Bifunctor (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            (isUpper)
-- import           Debug.Trace          (trace)
-- import           Text.Printf (printf)

mytracepp :: (PPrint a) => String -> a -> a
mytracepp :: forall a. PPrint a => [Char] -> a -> a
mytracepp = 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
fi Maybe [SubcId]
subcIds
  | Bool -> Bool
not (Config -> Bool
oldPLE Config
cfg)
  = forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
PLE.instantiate Config
cfg SInfo a
fi Maybe [SubcId]
subcIds

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

  | Bool
otherwise
  = forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
incrInstantiate' Config
cfg SInfo a
fi 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
fi Maybe [SubcId]
subcIds = do
    let cs :: [(SubcId, SimpC a)]
cs = [ (SubcId
i, SimpC a
c) | (SubcId
i, SimpC a
c) <- forall k v. HashMap k v -> [(k, v)]
M.toList (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi), forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aEnv SubcId
i SimpC a
c
                      ,  forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds ]
    let t :: CTrie
t  = forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
cs                                               -- 1. BUILD the Trie
    InstRes
res   <- forall a. Int -> IO a -> IO a
withProgress (Int
1 forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SubcId, SimpC a)]
cs) forall a b. (a -> b) -> a -> b
$
               forall a. Config -> [Char] -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
sEnv (forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
Loc a =>
Config -> SInfo a -> [(SubcId, SimpC a)] -> Context -> InstEnv a
instEnv Config
cfg SInfo a
fi [(SubcId, SimpC a)]
cs)  -- 2. TRAVERSE Trie to compute InstRes
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo Config
cfg SymEnv
sEnv SInfo a
fi InstRes
res                                 -- 3. STRENGTHEN SInfo using InstRes
  where
    file :: [Char]
file   = Config -> [Char]
srcFile Config
cfg forall a. [a] -> [a] -> [a]
++ [Char]
".evals"
    sEnv :: SymEnv
sEnv   = forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi
    aEnv :: AxiomEnv
aEnv   = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi



-------------------------------------------------------------------------------
-- | Step 1a: @instEnv@ sets up the incremental-PLE environment
instEnv :: (Loc a) => Config -> SInfo a -> [(SubcId, SimpC a)] -> SMT.Context -> InstEnv a
instEnv :: forall a.
Loc a =>
Config -> SInfo a -> [(SubcId, SimpC a)] -> Context -> InstEnv a
instEnv Config
cfg SInfo a
fi [(SubcId, SimpC a)]
cs Context
ctx = 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 (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              = forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi
    aEnv :: AxiomEnv
aEnv              = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
    γ :: Knowledge
γ                 = Config -> Context -> AxiomEnv -> Knowledge
knowledge Config
cfg Context
ctx AxiomEnv
aEnv
    s0 :: EvalEnv
s0                = Int -> [(Expr, Expr)] -> AxiomEnv -> SymEnv -> Config -> EvalEnv
EvalEnv Int
0 [] AxiomEnv
aEnv (Context -> SymEnv
SMT.ctxSymEnv Context
ctx) Config
cfg

----------------------------------------------------------------------------------------------
-- | Step 1b: @mkCTrie@ builds the @Trie@ of constraints indexed by their environments
mkCTrie :: [(SubcId, SimpC a)] -> CTrie
mkCTrie :: forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
ics  = forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"TRIE" forall a b. (a -> b) -> a -> b
$ 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   = forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> Path
elemsIBindEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a.
InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx0 forall a. [a]
diff0 forall a. Maybe a
Nothing forall {k} {v}. HashMap k v
res0 CTrie
t
  where
    diff0 :: [a]
diff0        = []
    res0 :: HashMap k v
res0         = forall {k} {v}. HashMap k v
M.empty
    ctx0 :: ICtx
ctx0         = [Expr] -> ICtx
initCtx [Expr]
es0
    es0 :: [Expr]
es0          = Equation -> Expr
eqBody forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
L.filter (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> [(Symbol, Sort)]
eqArgs) (AxiomEnv -> [Equation]
aenvEqs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. InstEnv a -> AxiomEnv
ieAenv 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 []  -> forall (m :: * -> *) a. Monad m => a -> m a
return InstRes
res
  T.Node [Branch SubcId
b] -> 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  -> forall a b.
InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx Path
delta forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do
                  (ICtx
ctx'', InstRes
res') <- forall a.
InstEnv a
-> ICtx
-> Maybe Int
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
i forall a. Maybe a
Nothing InstRes
res
                  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (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 -> forall a.
InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx (Int
iforall a. a -> [a] -> [a]
:Path
delta) (forall a. a -> Maybe a
Just Int
i) InstRes
res CTrie
t
  T.Val SubcId
cid  -> forall a b.
InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx Path
delta (forall a. a -> Maybe a
Just SubcId
cid) forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do
                  IO ()
progressTick
                  forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
InstEnv a
-> ICtx
-> Maybe Int
-> Maybe SubcId
-> InstRes
-> IO (ICtx, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
iMb (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
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: HashMap SubcId (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieSMT :: Context
ieCfg :: Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..} ICtx
ctx Path
delta Maybe SubcId
cidMb ICtx -> IO b
act = do
  let ctx' :: ICtx
ctx'  = forall a. InstEnv a -> ICtx -> Path -> Maybe SubcId -> ICtx
updCtx InstEnv a
env ICtx
ctx Path
delta Maybe SubcId
cidMb
  let assms :: [Expr]
assms = forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"ple1-assms: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Maybe SubcId
cidMb, Path
delta)) (ICtx -> [Expr]
icAssms ICtx
ctx')
  forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ieSMT  [Char]
"PLE.evaluate" forall a b. (a -> b) -> a -> b
$ do
    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
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: HashMap SubcId (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..} ICtx
ctx Maybe Int
i Maybe SubcId
cidMb InstRes
res = do
  let cands :: [Expr]
cands = forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"ple1-cands: "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Maybe SubcId
cidMb) forall a b. (a -> b) -> a -> b
$ 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
  forall (m :: * -> *) a. Monad m => a -> m a
return    forall a b. (a -> b) -> a -> b
$ 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 (forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"ple1-cands-unfolds: " forall a. [a] -> [a] -> [a]
++ 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
_  []    = forall (m :: * -> *) a. Monad m => a -> m a
return []
_evalCands Knowledge
γ EvalEnv
s0 [Expr]
cands = do [[(Expr, Expr)]]
eqs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0) [Expr]
cands
                           forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [(a, [(Expr, Expr)])] -> [(a, [Expr])]
mkUnfolds (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. a -> Maybe a
Just 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 [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Expr] -> Expr
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd

evalCandsLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Expr] -> IO [Unfold]
evalCandsLoop :: Config -> Context -> Knowledge -> EvalEnv -> [Expr] -> IO [Unfold]
evalCandsLoop Config
cfg Context
ctx Knowledge
γ EvalEnv
s0 [Expr]
cands = [Unfold] -> [Expr] -> IO [Unfold]
go [] [Expr]
cands
  where
    go :: [Unfold] -> [Expr] -> IO [Unfold]
go [Unfold]
acc []    = forall (m :: * -> *) a. Monad m => a -> m a
return [Unfold]
acc
    go [Unfold]
acc [Expr]
cands = do [[(Expr, Expr)]]
eqss   <- forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ctx [Char]
"PLE.evaluate" 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)
                                  forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0) [Expr]
cands
                      let us :: [(Maybe Expr, [(Expr, Expr)])]
us  = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
cands) [[(Expr, Expr)]]
eqss
                      case forall a. [(a, [(Expr, Expr)])] -> [(a, [Expr])]
mkUnfolds [(Maybe Expr, [(Expr, Expr)])]
us of
                        []  -> forall (m :: * -> *) a. Monad m => a -> m a
return [Unfold]
acc
                        [Unfold]
us' -> do let acc' :: [Unfold]
acc'   = [Unfold]
acc forall a. [a] -> [a] -> [a]
++ [Unfold]
us'
                                  let oks :: HashSet Expr
oks    = 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 (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
fi InstRes
res = forall a. SInfo a -> InstRes -> SInfo a
strengthenBinds SInfo a
fi InstRes
res'
  where
    res' :: InstRes
res'     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"ELAB-INST:  " forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip Path
is [Expr]
ps''
    ps'' :: [Expr]
ps''     = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i -> forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate (forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan ([Char]
"PLE1 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i)) SymEnv
env) Path
is [Expr]
ps'
    ps' :: [Expr]
ps'      = forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env [Expr]
ps
    (Path
is, [Expr]
ps) = forall a b. [(a, b)] -> ([a], [b])
unzip (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  = forall a. Monoid a => a
mempty
  , icEquals :: [Expr]
icEquals = forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"INITIAL-STUFF-INCR" [Expr]
es
  , icSolved :: HashSet Expr
icSolved = forall a. Monoid a => a
mempty
  }

equalitiesPred :: [(Expr, Expr)] -> [Expr]
equalitiesPred :: [(Expr, Expr)] -> [Expr]
equalitiesPred [(Expr, Expr)]
eqs = [ Expr -> Expr -> Expr
EEq Expr
e1 Expr
e2 | (Expr
e1, Expr
e2) <- [(Expr, Expr)]
eqs, Expr
e1 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 :: HashSet Expr
icSolved = HashSet Expr
solved', icEquals :: [Expr]
icEquals = forall a. Monoid a => a
mempty}
                         , InstRes
res'
                         )
  where
    _msg :: [Char]
_msg               = forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe [Char]
"nuttin\n" (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
pAnd [Expr]
solvedEqs)
    _cands' :: HashSet Expr
_cands'             = (ICtx -> HashSet Expr
icCands ICtx
ctx forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.union` HashSet Expr
newCands) forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` HashSet Expr
solved'
    solved' :: HashSet Expr
solved'            = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union (ICtx -> HashSet Expr
icSolved ICtx
ctx) HashSet Expr
solvedCands
    newCands :: HashSet Expr
newCands           = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
topApps [Expr]
newEqs)
    solvedCands :: HashSet Expr
solvedCands        = 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 forall a. [a] -> [a] -> [a]
++ [Expr]
newEqs
    newEqs :: [Expr]
newEqs             = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [Unfold]
okUnfolds
    okUnfolds :: [Unfold]
okUnfolds          = 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Expr]
ps) ]
    _str :: [Char]
_str               = [Char]
"okUnfolds " forall a. [a] -> [a] -> [a]
++ 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 (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
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: HashMap SubcId (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..} InstRes
res SubcId
i = [Char]
msg
  where
    msg :: [Char]
msg                          = [Char]
"INCR-INSTANTIATE i = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SubcId
i forall a. [a] -> [a] -> [a]
++ [Char]
": " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Expr
cidEqs
    cidEqs :: Expr
cidEqs                       = [Expr] -> Expr
pAnd [ Expr
e | Int
i <- Path
cBinds, Expr
e <- forall a. Maybe a -> [a]
Mb.maybeToList forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
i InstRes
res ]
    cBinds :: Path
cBinds                       = forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> Path
elemsIBindEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr HashMap SubcId (SimpC a)
ieCstrs forall a b. (a -> b) -> a -> b
$ SubcId
i


updRes :: InstRes -> Maybe BindId -> Expr -> InstRes
updRes :: InstRes -> Maybe Int -> Expr -> InstRes
updRes InstRes
res (Just Int
i) Expr
e = 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
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: HashMap SubcId (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieSMT :: Context
ieCfg :: Config
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> HashMap SubcId (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieSMT :: forall a. InstEnv a -> Context
ieCfg :: forall a. InstEnv a -> Config
ieAenv :: forall a. InstEnv a -> AxiomEnv
..} ICtx
ctx Path
delta Maybe SubcId
cidMb
              = ICtx
ctx { icAssms :: [Expr]
icAssms  = [Expr]
ctxEqs
                    , icCands :: HashSet Expr
icCands  = HashSet Expr
cands   forall a. Semigroup a => a -> a -> a
<> ICtx -> HashSet Expr
icCands  ICtx
ctx
                    , icEquals :: [Expr]
icEquals = [Expr]
initEqs forall a. Semigroup a => a -> a -> a
<> ICtx -> [Expr]
icEquals ICtx
ctx }
  where
    initEqs :: [Expr]
initEqs   = [(Expr, Expr)] -> [Expr]
equalitiesPred (Context -> AxiomEnv -> [(Symbol, SortedReft)] -> [(Expr, Expr)]
initEqualities Context
ieSMT AxiomEnv
ieAenv [(Symbol, SortedReft)]
bs)
    cands :: HashSet Expr
cands     = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
topApps [Expr]
es0) 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 [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                  ([Expr]
initEqs forall a. [a] -> [a] -> [a]
++
                  [ forall a. Expression a => a -> Expr
expr (Symbol, SortedReft)
xr
                  | xr :: (Symbol, SortedReft)
xr@(Symbol
_, SortedReft
r) <- [(Symbol, SortedReft)]
bs
                  , forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Expr -> [KVar]
Vis.kvarsExpr forall a b. (a -> b) -> a -> b
$ Reft -> Expr
reftPred forall a b. (a -> b) -> a -> b
$ SortedReft -> Reft
sr_reft SortedReft
r)
                  ])
    ([(Symbol, SortedReft)]
bs, [Expr]
es0) = (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SortedReft -> SortedReft
unElabSortedReft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds, Expr -> Expr
unElab forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
    es :: [Expr]
es        = Expr
eRhs forall a. a -> [a] -> [a]
: (forall a. Expression a => a -> Expr
expr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds)
    eRhs :: Expr
eRhs      = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
PTrue 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
_) = forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv a
ieBEnv ]
    subMb :: Maybe (SimpC a)
subMb     = forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr HashMap SubcId (SimpC a)
ieCstrs 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 = 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
fi Maybe [SubcId]
subcIds = forall a.
Config
-> SymEnv -> SInfo a -> [((SubcId, SrcSpan), Expr)] -> SInfo a
sInfo Config
cfg SymEnv
env SInfo a
fi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Config -> [Char] -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
env Context -> IO [((SubcId, SrcSpan), Expr)]
act
  where
    act :: Context -> IO [((SubcId, SrcSpan), Expr)]
act Context
ctx         = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(SubcId, SimpC a)]
cstrs forall a b. (a -> b) -> a -> b
$ \(SubcId
i, SimpC a
c) ->
                        ((SubcId
i,forall a. Loc a => a -> SrcSpan
srcSpan SimpC a
c),) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"INSTANTIATE i = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show SubcId
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Config
-> Context -> BindEnv a -> AxiomEnv -> SubcId -> SimpC a -> IO Expr
instSimpC Config
cfg Context
ctx (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi) AxiomEnv
aenv SubcId
i SimpC a
c
    cstrs :: [(SubcId, SimpC a)]
cstrs           = [ (SubcId
i, SimpC a
c) | (SubcId
i, SimpC a
c) <- forall k v. HashMap k v -> [(k, v)]
M.toList (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi) , forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
i SimpC a
c
                               ,  forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds ]
    file :: [Char]
file            = Config -> [Char]
srcFile Config
cfg forall a. [a] -> [a] -> [a]
++ [Char]
".evals"
    env :: SymEnv
env             = forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi
    aenv :: AxiomEnv
aenv            = {- mytracepp  "AXIOM-ENV" -} forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi

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
fi [((SubcId, SrcSpan), Expr)]
ips = forall a. SInfo a -> [(SubcId, Expr)] -> SInfo a
strengthenHyp SInfo a
fi (forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"ELAB-INST:  " forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(SubcId, SrcSpan)]
is) [Expr]
ps'')
  where
    ([(SubcId, SrcSpan)]
is, [Expr]
ps)         = forall a b. [(a, b)] -> ([a], [b])
unzip [((SubcId, SrcSpan), Expr)]
ips
    ps' :: [Expr]
ps'              = forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env [Expr]
ps
    ps'' :: [Expr]
ps''             = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(SubcId
i, SrcSpan
sp) -> forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate (forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
sp ([Char]
"PLE1 " forall a. [a] -> [a] -> [a]
++ 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
sid SimpC a
sub
  | forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
sid SimpC a
sub = do
    let is0 :: [Expr]
is0       = forall a. PPrint a => [Char] -> a -> a
mytracepp  [Char]
"INITIAL-STUFF" forall a b. (a -> b) -> a -> b
$ Equation -> Expr
eqBody forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
L.filter (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> [(Symbol, Sort)]
eqArgs) (AxiomEnv -> [Equation]
aenvEqs AxiomEnv
aenv)
    let ([(Symbol, SortedReft)]
bs, [Expr]
es0) = 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
sid
    let evalEqs :: [Expr]
evalEqs   = [ Expr -> Expr -> Expr
EEq Expr
e1 Expr
e2 | (Expr
e1, Expr
e2) <- [(Expr, Expr)]
equalities, Expr
e1 forall a. Eq a => a -> a -> Bool
/= Expr
e2 ]
    forall (m :: * -> *) a. Monad m => a -> m a
return        forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pAnd ([Expr]
is0 forall a. [a] -> [a] -> [a]
++ [Expr]
evalEqs)
  | Bool
otherwise     = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PTrue

isPleCstr :: AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr :: forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aenv SubcId
sid SimpC a
c = forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c Bool -> Bool -> Bool
&& forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Bool
False SubcId
sid (AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
aenv)

cstrExprs :: BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs :: forall a. BindEnv a -> SimpC a -> ([(Symbol, SortedReft)], [Expr])
cstrExprs BindEnv a
bds SimpC a
sub = (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second SortedReft -> SortedReft
unElabSortedReft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds, Expr -> Expr
unElab forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es)
  where
    es :: [Expr]
es            = forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs SimpC a
sub forall a. a -> [a] -> [a]
: (forall a. Expression a => a -> Expr
expr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SortedReft)]
binds)
    binds :: [(Symbol, SortedReft)]
binds         = forall a. BindEnv a -> IBindEnv -> [(Symbol, SortedReft)]
envCs BindEnv a
bds (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
sub)

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



_evalLoop :: Config -> SMT.Context -> Knowledge -> EvalEnv -> [Pred] -> [Expr] -> IO [(Expr, Expr)]
_evalLoop :: Config
-> Context
-> Knowledge
-> EvalEnv
-> [Expr]
-> [Expr]
-> IO [(Expr, Expr)]
_evalLoop Config
cfg Context
ctx Knowledge
γ EvalEnv
s0 [Expr]
ctxEqs [Expr]
cands = SubcId -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop SubcId
0 [] [Expr]
cands
  where
    loop :: SubcId -> [(Expr, Expr)] -> [Expr] -> IO [(Expr, Expr)]
loop SubcId
_ [(Expr, Expr)]
acc []    = 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 [] forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
pAnd forall a b. (a -> b) -> a -> b
$ [(Expr, Expr)] -> [Expr]
equalitiesPred [(Expr, Expr)]
acc
                          [[(Expr, Expr)]]
eqss <- forall a. Context -> [Char] -> IO a -> IO a
SMT.smtBracket Context
ctx [Char]
"PLE.evaluate" forall a b. (a -> b) -> a -> b
$ do
                                    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Expr
eqp forall a. a -> [a] -> [a]
: [Expr]
ctxEqs) (Context -> Expr -> IO ()
SMT.smtAssert Context
ctx)
                                    forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Knowledge -> EvalEnv -> Expr -> IO [(Expr, Expr)]
evalOne Knowledge
γ EvalEnv
s0) [Expr]
cands
                          case forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Expr, Expr)]]
eqss of
                            []   -> forall (m :: * -> *) a. Monad m => a -> m a
return [(Expr, Expr)]
acc
                            [(Expr, Expr)]
eqs' -> do let acc' :: [(Expr, Expr)]
acc'   = [(Expr, Expr)]
acc forall a. [a] -> [a] -> [a]
++ [(Expr, Expr)]
eqs'
                                       let oks :: HashSet Expr
oks    = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a b. (a, b) -> a
fst 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 (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 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) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
initCS (forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"evalOne: " Expr
e)) EvalEnv
s0
  if Expr
e' forall a. Eq a => a -> a -> Bool
== Expr
e then forall (m :: * -> *) a. Monad m => a -> m a
return [] else forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr
e, Expr
e') 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Recur -> Recur -> Bool
$c/= :: Recur -> Recur -> Bool
== :: Recur -> Recur -> Bool
$c== :: Recur -> Recur -> Bool
Eq, Int -> Recur -> ShowS
[Recur] -> ShowS
Recur -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [Recur] -> ShowS
$cshowList :: [Recur] -> ShowS
show :: Recur -> [Char]
$cshow :: Recur -> [Char]
showsPrec :: Int -> Recur -> ShowS
$cshowsPrec :: Int -> Recur -> ShowS
Show)
type CStack = ([Symbol], Recur)

instance PPrint Recur where
  pprintTidy :: Tidy -> Recur -> Doc
pprintTidy Tidy
_ = 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
fforall 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 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]
go
  where
    go :: Expr -> [Expr]
go (PAnd [Expr]
es)       = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
go [Expr]
es
    go (POr [Expr]
es)        = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [Expr]
go [Expr]
es
    go (PAtom Brel
_ Expr
e1 Expr
e2) = Expr -> [Expr]
go Expr
e1  forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (PIff Expr
e1 Expr
e2)    = Expr -> [Expr]
go Expr
e1  forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (PImp Expr
e1 Expr
e2)    = Expr -> [Expr]
go Expr
e1  forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (EBin  Bop
_ Expr
e1 Expr
e2) = Expr -> [Expr]
go Expr
e1  forall a. [a] -> [a] -> [a]
++ Expr -> [Expr]
go Expr
e2
    go (PNot Expr
e)        = Expr -> [Expr]
go Expr
e
    go (ENeg Expr
e)        = Expr -> [Expr]
go Expr
e
    go e :: Expr
e@(EApp Expr
_ Expr
_)    = [Expr
e]
    go Expr
_               = []

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

eval :: Knowledge -> CStack -> Expr -> EvalST Expr
eval :: Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk = Expr -> EvalST Expr
go
  where
    go :: Expr -> EvalST Expr
go (ELam (Symbol
x,Sort
s) Expr
e)   = (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ' CStack
stk Expr
e where γ' :: Knowledge
γ' = Knowledge
γ { knLams :: [(Symbol, Sort)]
knLams = (Symbol
x, Sort
s) forall a. a -> [a] -> [a]
: Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ }
    go e :: Expr
e@(EIte Expr
b Expr
e1 Expr
e2) = Expr -> EvalST Expr
go Expr
b        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Expr
b' -> Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
evalIte Knowledge
γ CStack
stk Expr
e Expr
b' Expr
e1 Expr
e2
    go (ECoerc Sort
s Sort
t Expr
e)   = Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e
    go e :: Expr
e@(EApp Expr
_ Expr
_)     = Knowledge -> CStack -> Expr -> EvalST (Expr, [Expr])
evalArgs Knowledge
γ CStack
stk Expr
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Knowledge -> CStack -> Expr -> (Expr, [Expr]) -> EvalST Expr
evalApp Knowledge
γ CStack
stk Expr
e
    go e :: Expr
e@(EVar Symbol
_)       = Knowledge -> CStack -> Expr -> (Expr, [Expr]) -> EvalST Expr
evalApp  Knowledge
γ CStack
stk Expr
e (Expr
e, [])
    go (PAtom Brel
r Expr
e1 Expr
e2)  = Brel -> Expr -> Expr -> Expr
PAtom Brel
r      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> EvalST Expr
go Expr
e2
    go (ENeg Expr
e)         = Expr -> Expr
ENeg         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e
    go (EBin Bop
o Expr
e1 Expr
e2)   = Bop -> Expr -> Expr -> Expr
EBin Bop
o       forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> EvalST Expr
go Expr
e2
    go (ETApp Expr
e Sort
t)      = forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Sort -> Expr
ETApp Sort
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e
    go (ETAbs Expr
e Symbol
s)      = forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Symbol -> Expr
ETAbs Symbol
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e
    go (PNot Expr
e)         = Expr -> Expr
PNot         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e
    go (PImp Expr
e1 Expr
e2)     = Expr -> Expr -> Expr
PImp         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> EvalST Expr
go Expr
e2
    go (PIff Expr
e1 Expr
e2)     = Expr -> Expr -> Expr
PIff         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> EvalST Expr
go Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> EvalST Expr
go Expr
e2
    go (PAnd [Expr]
es)        = [Expr] -> Expr
PAnd         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> EvalST Expr
go forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
es)
    go (POr [Expr]
es)         = [Expr] -> Expr
POr          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> EvalST Expr
go forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
`traverse` [Expr]
es)
    go Expr
e                = 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
e = [Expr] -> Expr -> EvalST (Expr, [Expr])
go [] Expr
e
  where
    go :: [Expr] -> Expr -> EvalST (Expr, [Expr])
go [Expr]
acc (EApp Expr
f Expr
e)
      = do Expr
f' <- Knowledge -> CStack -> Expr -> EvalST Expr
evalOk Knowledge
γ CStack
stk Expr
f
           Expr
e' <- Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk Expr
e
           [Expr] -> Expr -> EvalST (Expr, [Expr])
go (Expr
e'forall a. a -> [a] -> [a]
:[Expr]
acc) Expr
f'
    go [Expr]
acc Expr
e
      = (,[Expr]
acc) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> CStack -> Expr -> EvalST 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 -> EvalST Expr
evalOk Knowledge
γ stk :: CStack
stk@([Symbol]
_, Recur
Ok) Expr
e = Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk Expr
e
evalOk Knowledge
_ CStack
_           Expr
e = 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]) -> EvalST Expr
evalApp Knowledge
γ CStack
stk Expr
e (Expr
e1, [Expr]
es) = do
  Expr
res     <- Knowledge -> CStack -> Expr -> (Expr, [Expr]) -> EvalST Expr
evalAppAc Knowledge
γ CStack
stk Expr
e (Expr
e1, [Expr]
es)
  let diff :: Bool
diff = Expr
res forall a. Eq a => a -> a -> Bool
/= Expr -> [Expr] -> Expr
eApps Expr
e1 [Expr]
es
  forall (m :: * -> *) a. Monad m => a -> m a
return   forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalApp:END:" forall a. [a] -> [a] -> [a]
++ 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]) -> EvalST Expr
evalAppAc Knowledge
γ CStack
stk Expr
e (EVar Symbol
f, [Expr
ex])
  | (EVar Symbol
dc, [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
ex
  , Just Rewrite
simp <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (\Rewrite
simp -> (Rewrite -> Symbol
smName Rewrite
simp forall a. Eq a => a -> a -> Bool
== Symbol
f) Bool -> Bool -> Bool
&& (Rewrite -> Symbol
smDC Rewrite
simp forall a. Eq a => a -> a -> Bool
== Symbol
dc)) (Knowledge -> [Rewrite]
knSims Knowledge
γ)
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
simp) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  = do let msg :: [Char]
msg    = [Char]
"evalAppAc:ePop: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (Symbol
f, Symbol
dc, [Expr]
es)
       let ePopIf :: Expr
ePopIf = forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
msg forall a b. (a -> b) -> a -> b
$ [(Symbol, Expr)] -> Expr -> Expr
substPopIf (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 -> EvalST Expr
eval Knowledge
γ CStack
stk Expr
ePopIf
       (Expr
e, [Char]
"Rewrite -" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Symbol
f) (Expr, [Char]) -> Expr -> EvalST 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 <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (( forall a. Eq a => a -> a -> Bool
== Symbol
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> Symbol
eqName) (Knowledge -> [Equation]
knAms Knowledge
γ)
  , Just Expr
bd <- Equation -> Maybe Expr
getEqBody Equation
eq
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq) forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
  , Symbol
f forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` 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   <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort 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 -> EvalST 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 <- forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find ((forall a. Eq a => a -> a -> Bool
== Symbol
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> Symbol
eqName) (Knowledge -> [Equation]
knAms Knowledge
γ)
  , Just Expr
bd <- Equation -> Maybe Expr
getEqBody Equation
eq
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq) forall a. Eq a => a -> a -> Bool
== 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      <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalEnv -> SymEnv
evEnv)
       forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"EVAL-REC-APP" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (CStack
stk, Expr
_e))
         forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> CStack -> Expr -> Expr -> EvalST Expr
evalRecApplication Knowledge
γ (CStack -> Symbol -> CStack
pushCS CStack
stk Symbol
f) (Expr -> [Expr] -> Expr
eApps (Symbol -> Expr
EVar Symbol
f) [Expr]
es) (SEnv Sort -> SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEq SEnv Sort
env SubstOp
Normal Equation
eq [Expr]
es Expr
bd)

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

--------------------------------------------------------------------------------
-- | 'substEq' unfolds or instantiates an equation at a particular list of
--   argument values. We must also substitute the sort-variables that appear
--   as coercions. See tests/proof/ple1.fq
--------------------------------------------------------------------------------
substEq :: SEnv Sort -> SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEq :: SEnv Sort -> SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEq SEnv Sort
env SubstOp
o Equation
eq [Expr]
es Expr
bd = SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEqVal SubstOp
o Equation
eq [Expr]
es (SEnv Sort -> Equation -> [Expr] -> Expr -> Expr
substEqCoerce SEnv Sort
env Equation
eq [Expr]
es Expr
bd)

data SubstOp = PopIf | Normal

substEqVal :: SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEqVal :: SubstOp -> Equation -> [Expr] -> Expr -> Expr
substEqVal SubstOp
o Equation
eq [Expr]
es Expr
bd = case SubstOp
o of
    SubstOp
PopIf  -> [(Symbol, Expr)] -> Expr -> Expr
substPopIf     [(Symbol, Expr)]
xes  Expr
bd
    SubstOp
Normal -> forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst [(Symbol, Expr)]
xes) Expr
bd
  where
    xes :: [(Symbol, Expr)]
xes    =  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    = forall a b. (a, b) -> b
snd    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Equation -> [(Symbol, Sort)]
eqArgs Equation
eq
    sp :: SrcSpan
sp    = [Char] -> SrcSpan
panicSpan [Char]
"mkCoSub"
    eTs :: [Sort]
eTs   = SrcSpan -> SEnv Sort -> Expr -> Sort
sortExpr SrcSpan
sp SEnv Sort
env forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Expr]
es
    coSub :: CoSub
coSub = forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"substEqCoerce" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (Equation -> Symbol
eqName Equation
eq, [Expr]
es, [Sort]
eTs, [Sort]
ts)) 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 = 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) <- forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, Sort)]
xys ]
  where
    unite :: [Sort] -> Sort
unite [Sort]
ts    = forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"UNITE: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp [Sort]
ts) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
Mb.fromMaybe (forall {a} {a}. PPrint a => a -> a
uError [Sort]
ts) (Env -> [Sort] -> Maybe Sort
unifyTo1 Env
senv [Sort]
ts)
    senv :: Env
senv        = forall a. SEnv a -> Symbol -> SESearch a
mkSearchEnv SEnv Sort
env
    uError :: a -> a
uError a
ts   = forall a. [Char] -> a
panic ([Char]
"mkCoSub: cannot build CoSub for " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp [(Symbol, Sort)]
xys forall a. [a] -> [a] -> [a]
++ [Char]
" cannot unify " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp a
ts)
    xys :: [(Symbol, Sort)]
xys         = forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"mkCoSubXXX" forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Sort -> Sort -> [(Symbol, Sort)]
matchSorts [Sort]
_xTs [Sort]
_eTs
    ([Sort]
_xTs,[Sort]
_eTs) = 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
s1 Sort
s2 = forall a. PPrint a => [Char] -> a -> a
mytracepp  ([Char]
"matchSorts :" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (Sort
s1, Sort
s2)) forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> [(Symbol, Sort)]
go Sort
s1 Sort
s2
  where
    go :: Sort -> Sort -> [(Symbol, Sort)]
go (FObj Symbol
x)      {-FObj-} Sort
y    = [(Symbol
x, Sort
y)]
    go (FAbs Int
_ Sort
t1)   (FAbs Int
_ Sort
t2)   = Sort -> Sort -> [(Symbol, Sort)]
go Sort
t1 Sort
t2
    go (FFunc Sort
s1 Sort
t1) (FFunc Sort
s2 Sort
t2) = Sort -> Sort -> [(Symbol, Sort)]
go Sort
s1 Sort
s2 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 forall a. [a] -> [a] -> [a]
++ Sort -> Sort -> [(Symbol, Sort)]
go Sort
t1 Sort
t2
    go Sort
_             Sort
_             = []

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

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

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

substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
substPopIf :: [(Symbol, Expr)] -> Expr -> Expr
substPopIf [(Symbol, Expr)]
xes Expr
e = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' Expr -> (Symbol, Expr) -> Expr
go Expr
e [(Symbol, Expr)]
xes
  where
    go :: Expr -> (Symbol, Expr) -> Expr
go Expr
e (Symbol
x, EIte Expr
b Expr
e1 Expr
e2) = Expr -> Expr -> Expr -> Expr
EIte Expr
b (forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
e (Symbol
x, Expr
e1)) (forall a. Subable a => a -> (Symbol, Expr) -> a
subst1 Expr
e (Symbol
x, Expr
e2))
    go Expr
e (Symbol
x, Expr
ex)           = 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 -> EvalST Expr
evalRecApplication Knowledge
γ CStack
stk Expr
e (EIte Expr
b Expr
e1 Expr
e2) = do
  Bool
contra <- {- mytracepp  ("CONTRA? " ++ showpp e) <$> -} forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
PFalse)
  if Bool
contra
    then forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    else do Expr
b' <- Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk (forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"REC-APP-COND" Expr
b) -- <<<<<<<<<<<<<<<<<<<<< MOSSAKA-LOOP?
            Bool
b1 <- 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                   {- SCC "assertSelectors-1" -} Knowledge -> Expr -> EvalST ()
assertSelectors Knowledge
γ Expr
e1 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                   Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk (forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalREC-1: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp CStack
stk) Expr
e1) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                   ((Expr
e, [Char]
"App1: ") (Expr, [Char]) -> Expr -> EvalST Expr
~>)
              else do
                   Bool
b2 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
b'))
                   if Bool
b2
                      then Knowledge -> Expr -> Expr -> EvalST ()
addEquality Knowledge
γ Expr
e Expr
e2 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                           {- SCC "assertSelectors-2" -} Knowledge -> Expr -> EvalST ()
assertSelectors Knowledge
γ Expr
e2 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                           Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk (forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalREC-2: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp CStack
stk) Expr
e2) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                           ((Expr
e, [Char]
"App2: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp CStack
stk ) (Expr, [Char]) -> Expr -> EvalST Expr
~>)
                      else forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
evalRecApplication Knowledge
_ CStack
_ Expr
_ Expr
e
  = 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 =
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st{evSequence :: [(Expr, Expr)]
evSequence = (Knowledge -> Expr -> Expr
makeLam Knowledge
γ Expr
e1, Knowledge -> Expr -> Expr
makeLam Knowledge
γ Expr
e2)forall a. a -> [a] -> [a]
:EvalEnv -> [(Expr, Expr)]
evSequence EvalEnv
st})

evalIte :: Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
evalIte :: Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
evalIte Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 Expr
e2 = forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"evalIte:END: " forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                            Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> EvalST Expr
evalIteAc Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 (forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
msg Expr
e2)
  where
    msg :: [Char]
msg = [Char]
"evalIte:BEGINS: " forall a. [a] -> [a] -> [a]
++ 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 -> EvalST Expr
evalIteAc Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 Expr
e2
  = forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ Knowledge
-> CStack
-> Expr
-> Expr
-> Expr
-> Expr
-> Bool
-> Bool
-> EvalST Expr
evalIte' Knowledge
γ CStack
stk Expr
e Expr
b Expr
e1 Expr
e2 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ Expr
b) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (Knowledge -> Expr -> IO Bool
isValid Knowledge
γ (Expr -> Expr
PNot Expr
b))

evalIte' :: Knowledge -> CStack -> Expr -> Expr -> Expr -> Expr -> Bool -> Bool -> EvalST Expr
evalIte' :: Knowledge
-> CStack
-> Expr
-> Expr
-> Expr
-> Expr
-> Bool
-> Bool
-> EvalST Expr
evalIte' Knowledge
γ CStack
stk Expr
e Expr
_ Expr
e1 Expr
_ Bool
b Bool
_
  | Bool
b
  = do Expr
e' <- Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk Expr
e1
       (Expr
e, [Char]
"If-True of:" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Bool
b)  (Expr, [Char]) -> Expr -> EvalST Expr
~> Expr
e'
evalIte' Knowledge
γ CStack
stk Expr
e Expr
_ Expr
_ Expr
e2 Bool
_ Bool
b'
  | Bool
b'
  = do Expr
e' <- Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk Expr
e2
       (Expr
e, [Char]
"If-False") (Expr, [Char]) -> Expr -> EvalST Expr
~> Expr
e'
evalIte' Knowledge
γ CStack
stk Expr
_ Expr
b Expr
e1 Expr
e2 Bool
_ Bool
_
  -- see [NOTE:Eval-Ite] #387
  = Expr -> Expr -> Expr -> Expr
EIte Expr
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk' Expr
e1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Knowledge -> CStack -> Expr -> EvalST Expr
eval Knowledge
γ CStack
stk' Expr
e2
    where stk' :: CStack
stk' = forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"evalIte'" 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 = forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"isValid: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Expr
e) 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 Reft
_) = forall a. PPrint a => a -> [Char]
showpp Sort
s 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 = 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                  = forall a. Ord a => [a] -> [a]
Misc.setNub (forall a. [Maybe a] -> [a]
Mb.catMaybes [SymEnv -> Expr -> Expr -> Maybe (Symbol, [Expr], Expr)
getDCEquality SymEnv
senv Expr
e1 Expr
e2 | EEq Expr
e1 Expr
e2 <- [Expr]
atoms])
    atoms :: [Expr]
atoms                  = Expr -> [Expr]
splitPAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Expression a => a -> Expr
expr forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (a -> Bool) -> [a] -> [a]
filter forall a. (a, SortedReft) -> Bool
isProof [(Symbol, SortedReft)]
es
    senv :: SymEnv
senv                   = Context -> SymEnv
SMT.ctxSymEnv Context
ctx

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

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 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 forall a. Eq a => a -> a -> Bool
== Symbol
dc', forall (t :: * -> *) a. Foldable t => t a -> Int
length [Symbol]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es
     = [(Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar Symbol
f) Expr
e, forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== Symbol
dc2
      then forall a. Maybe a
Nothing
      else forall a. HasCallStack => [Char] -> a
error ([Char]
"isDCEquality on" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Expr
e1 forall a. [a] -> [a] -> [a]
++ [Char]
"\n" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Expr
e2)
  | Just Symbol
dc1 <- Maybe Symbol
f1
  = forall a. a -> Maybe a
Just (Symbol
dc1, [Expr]
es1, Expr
e2)
  | Just Symbol
dc2 <- Maybe Symbol
f2
  = forall a. a -> Maybe a
Just (Symbol
dc2, [Expr]
es2, Expr
e1)
  | Bool
otherwise
  = forall a. Maybe a
Nothing
  where
    (Maybe Symbol
f1, [Expr]
es1) = forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst (SymEnv -> Expr -> Maybe Symbol
getDC SymEnv
senv) (Expr -> (Expr, [Expr])
splitEApp Expr
e1)
    (Maybe Symbol
f2, [Expr]
es2) = forall a c b. (a -> c) -> (a, b) -> (c, b)
Misc.mapFst (SymEnv -> Expr -> Maybe Symbol
getDC SymEnv
senv) (Expr -> (Expr, [Expr])
splitEApp Expr
e2)

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

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

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

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

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

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

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

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

withCtx :: Config -> FilePath -> SymEnv -> (SMT.Context -> IO a) -> IO a
withCtx :: forall a. Config -> [Char] -> SymEnv -> (Context -> IO a) -> IO a
withCtx Config
cfg [Char]
file SymEnv
env Context -> IO a
k = do
  Context
ctx <- Config -> [Char] -> SymEnv -> IO Context
SMT.makeContextWithSEnv Config
cfg [Char]
file SymEnv
env
  ()
_   <- Context -> IO ()
SMT.smtPush Context
ctx
  a
res <- Context -> IO a
k Context
ctx
  Context -> IO ()
SMT.cleanupContext Context
ctx
  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 -> EvalST Expr
~> Expr
e' = do
  let msg :: [Char]
msg = [Char]
"PLE: " forall a. [a] -> [a] -> [a]
++ [Char]
_str forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp (Expr
e, Expr
e')
  forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\EvalEnv
st -> EvalEnv
st {evId :: Int
evId = forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
msg (EvalEnv -> Int
evId EvalEnv
st) forall a. Num a => a -> a -> a
+ Int
1})
  forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e'