--------------------------------------------------------------------------------
-- | This module is a preliminary part of the implementation of "Proof by
--   Logical Evaluation" where we unfold function definitions if they *must* be
--   unfolded, to strengthen the environments with function-definition-equalities.
--
--   In this module, we attempt to verify as many of the PLE constaints as
--   possible without invoking the SMT solver or performing any I/O at all.
--   To this end, we use an interpreter in Haskell to attempt to evaluate down
--   expressions and generate equalities.
--------------------------------------------------------------------------------

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

module Language.Fixpoint.Solver.Interpreter
  ( instInterpreter

  -- The following exports are for property testing.
  , ICtx(..)
  , Knowledge(..)
  , Simplifiable(..)
  , interpret
  ) where

import           Language.Fixpoint.Types hiding (simplify)
import           Language.Fixpoint.Types.Config  as FC
import           Language.Fixpoint.Types.Solutions        (CMap)
import qualified Language.Fixpoint.Types.Visitor as Vis
import qualified Language.Fixpoint.Misc          as Misc
import           Language.Fixpoint.Defunctionalize
import qualified Language.Fixpoint.Utils.Trie    as T
import           Language.Fixpoint.Utils.Progress
import           Language.Fixpoint.SortCheck
import           Language.Fixpoint.Graph.Deps             (isTarget)
import           Language.Fixpoint.Solver.Sanitize        (symbolEnv)
import           Language.Fixpoint.Solver.Simplify
import           Control.Monad (foldM)
import           Control.Monad.State
import qualified Data.HashMap.Strict  as M
import qualified Data.HashSet         as S
import qualified Data.List            as L
import qualified Data.Maybe           as Mb
--import           Debug.Trace                              (trace)

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

--mytrace :: String -> a -> a
--mytrace = {-trace-} flip const

--------------------------------------------------------------------------------
-- | Strengthen Constraint Environments via PLE
--------------------------------------------------------------------------------
instInterpreter :: (Loc a) => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instInterpreter :: forall a.
Loc a =>
Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
instInterpreter Config
cfg SInfo a
fi' Maybe [SubcId]
subcIds = do
    let cs :: HashMap SubcId (SimpC a)
cs = (SubcId -> SimpC a -> Bool)
-> HashMap SubcId (SimpC a) -> HashMap SubcId (SimpC a)
forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey
               (\SubcId
i SimpC a
c -> AxiomEnv -> SubcId -> SimpC a -> Bool
forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aEnv SubcId
i SimpC a
c Bool -> Bool -> Bool
&& Bool -> ([SubcId] -> Bool) -> Maybe [SubcId] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i SubcId -> [SubcId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds)
               (SInfo a -> HashMap SubcId (SimpC a)
forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
info)
    let t :: CTrie
t  = [(SubcId, SimpC a)] -> CTrie
forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie (HashMap SubcId (SimpC a) -> [(SubcId, SimpC a)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId (SimpC a)
cs)                      -- 1. BUILD the Trie
    InstRes
res   <- Int -> IO InstRes -> IO InstRes
forall a. Int -> IO a -> IO a
withProgress (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ HashMap SubcId (SimpC a) -> Int
forall k v. HashMap k v -> Int
M.size HashMap SubcId (SimpC a)
cs) (IO InstRes -> IO InstRes) -> IO InstRes -> IO InstRes
forall a b. (a -> b) -> a -> b
$
               CTrie -> InstEnv a -> IO InstRes
forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t (InstEnv a -> IO InstRes) -> InstEnv a -> IO InstRes
forall a b. (a -> b) -> a -> b
$ SInfo a -> HashMap SubcId (SimpC a) -> SymEnv -> InstEnv a
forall a. Loc a => SInfo a -> CMap (SimpC a) -> SymEnv -> InstEnv a
instEnv SInfo a
info HashMap SubcId (SimpC a)
cs SymEnv
sEnv         -- 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
    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
    info :: SInfo a
info   = SInfo a -> SInfo a
forall a. Normalizable a => a -> a
normalize SInfo a
fi'

-------------------------------------------------------------------------------
-- | Step 1a: @instEnv@ sets up the incremental-PLE environment
instEnv :: (Loc a) => SInfo a -> CMap (SimpC a) -> SymEnv -> InstEnv a
instEnv :: forall a. Loc a => SInfo a -> CMap (SimpC a) -> SymEnv -> InstEnv a
instEnv SInfo a
info CMap (SimpC a)
cs SymEnv
sEnv = BindEnv a
-> AxiomEnv -> CMap (SimpC a) -> Knowledge -> EvalEnv -> InstEnv a
forall a.
BindEnv a
-> AxiomEnv -> CMap (SimpC a) -> Knowledge -> EvalEnv -> InstEnv a
InstEnv BindEnv a
bEnv AxiomEnv
aEnv CMap (SimpC a)
cs Knowledge
γ EvalEnv
s0
  where
    csBinds :: IBindEnv
csBinds           = (IBindEnv -> SimpC a -> IBindEnv)
-> IBindEnv -> CMap (SimpC a) -> IBindEnv
forall a v k. (a -> v -> a) -> a -> HashMap k v -> a
M.foldl' (\IBindEnv
acc SimpC a
c -> IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv IBindEnv
acc (SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)) IBindEnv
emptyIBindEnv CMap (SimpC a)
cs
    bEnv :: BindEnv a
bEnv              = (Int -> Symbol -> SortedReft -> Bool) -> BindEnv a -> BindEnv a
forall a.
(Int -> Symbol -> SortedReft -> Bool) -> BindEnv a -> BindEnv a
filterBindEnv (\Int
i Symbol
_ SortedReft
_ -> Int -> IBindEnv -> Bool
memberIBindEnv Int
i IBindEnv
csBinds) (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
γ                 = SInfo a -> Knowledge
forall a. SInfo a -> Knowledge
knowledge SInfo a
info
    s0 :: EvalEnv
s0                = SymEnv -> EvAccum -> EvalEnv
EvalEnv SymEnv
sEnv EvAccum
forall a. Monoid a => a
mempty

----------------------------------------------------------------------------------------------
-- | Step 1b: @mkCTrie@ builds the @Trie@ of constraints indexed by their environments
mkCTrie :: [(SubcId, SimpC a)] -> CTrie
mkCTrie :: forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie [(SubcId, SimpC a)]
ics  = [(Path, SubcId)] -> CTrie
forall a. [(Path, a)] -> Trie a
T.fromList [ (SimpC a -> Path
cBinds SimpC a
c, SubcId
i) | (SubcId
i, SimpC a
c) <- [(SubcId, SimpC a)]
ics ]
  where
    cBinds :: SimpC a -> Path
cBinds   = Path -> Path
forall a. Ord a => [a] -> [a]
L.sort (Path -> Path) -> (SimpC a -> Path) -> SimpC a -> Path
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> Path
elemsIBindEnv (IBindEnv -> Path) -> (SimpC a -> IBindEnv) -> SimpC a -> Path
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimpC a -> IBindEnv
forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv

----------------------------------------------------------------------------------------------
-- | Step 2: @pleTrie@ walks over the @CTrie@ to actually do the incremental-PLE
pleTrie :: CTrie -> InstEnv a -> IO InstRes
pleTrie :: 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         = InstEnv a -> [(ExprV Symbol, ExprV Symbol)] -> ICtx
forall a. InstEnv a -> [(ExprV Symbol, ExprV Symbol)] -> ICtx
initCtx InstEnv a
env ((EquationV Symbol -> (ExprV Symbol, ExprV Symbol)
forall {v}. EquationV v -> (ExprV Symbol, ExprV v)
mkEq (EquationV Symbol -> (ExprV Symbol, ExprV Symbol))
-> [EquationV Symbol] -> [(ExprV Symbol, ExprV Symbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [EquationV Symbol]
es0) [(ExprV Symbol, ExprV Symbol)]
-> [(ExprV Symbol, ExprV Symbol)] -> [(ExprV Symbol, ExprV Symbol)]
forall a. [a] -> [a] -> [a]
++ (Rewrite -> (ExprV Symbol, ExprV Symbol)
mkEq' (Rewrite -> (ExprV Symbol, ExprV Symbol))
-> [Rewrite] -> [(ExprV Symbol, ExprV Symbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
es0'))
    es0 :: [EquationV Symbol]
es0          = (EquationV Symbol -> Bool)
-> [EquationV Symbol] -> [EquationV Symbol]
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)
-> (EquationV Symbol -> [(Symbol, Sort)])
-> EquationV Symbol
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EquationV Symbol -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs) (AxiomEnv -> [EquationV Symbol]
aenvEqs   (AxiomEnv -> [EquationV Symbol])
-> (InstEnv a -> AxiomEnv) -> InstEnv a -> [EquationV Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstEnv a -> AxiomEnv
forall a. InstEnv a -> AxiomEnv
ieAenv (InstEnv a -> [EquationV Symbol])
-> InstEnv a -> [EquationV Symbol]
forall a b. (a -> b) -> a -> b
$ InstEnv a
env)
    es0' :: [Rewrite]
es0'         = (Rewrite -> Bool) -> [Rewrite] -> [Rewrite]
forall a. (a -> Bool) -> [a] -> [a]
L.filter ([Symbol] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Symbol] -> Bool) -> (Rewrite -> [Symbol]) -> Rewrite -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> [Symbol]
smArgs) (AxiomEnv -> [Rewrite]
aenvSimpl (AxiomEnv -> [Rewrite])
-> (InstEnv a -> AxiomEnv) -> InstEnv a -> [Rewrite]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InstEnv a -> AxiomEnv
forall a. InstEnv a -> AxiomEnv
ieAenv (InstEnv a -> [Rewrite]) -> InstEnv a -> [Rewrite]
forall a b. (a -> b) -> a -> b
$ InstEnv a
env)
    mkEq :: EquationV v -> (ExprV Symbol, ExprV v)
mkEq  EquationV v
eq     = (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol) -> Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ EquationV v -> Symbol
forall v. EquationV v -> Symbol
eqName EquationV v
eq, EquationV v -> ExprV v
forall v. EquationV v -> ExprV v
eqBody EquationV v
eq)
    mkEq' :: Rewrite -> (ExprV Symbol, ExprV Symbol)
mkEq' Rewrite
rw     = (ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol) -> Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol) -> Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smDC Rewrite
rw), Rewrite -> ExprV Symbol
smBody Rewrite
rw)

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 -> InstRes -> IO (ICtx, InstRes)
forall a.
InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
i InstRes
res
                  (InstRes -> Branch SubcId -> IO InstRes)
-> InstRes -> [Branch SubcId] -> IO InstRes
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (InstEnv a
-> ICtx
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
forall a.
InstEnv a
-> ICtx
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx'' [] Maybe Int
i) InstRes
res' [Branch SubcId]
bs

loopB :: InstEnv a -> ICtx -> Diff -> Maybe BindId -> InstRes -> CBranch -> IO InstRes
loopB :: 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 -> InstRes -> IO (ICtx, InstRes)
forall a.
InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
iMb InstRes
res

-- Adds to @ctx@ candidate expressions to unfold from the bindings in @delta@
-- and the rhs of @cidMb@.
--
-- Adds to @ctx@ assumptions from @env@ and @delta@ plus rewrites that
-- candidates can use
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{} ICtx
ctx Path
delta Maybe SubcId
cidMb ICtx -> IO b
act = ICtx -> IO b
act (ICtx -> IO b) -> ICtx -> IO b
forall a b. (a -> b) -> a -> b
$
  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

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

evalCandsLoop :: ConstMap -> ICtx -> Knowledge -> EvalEnv -> IO ICtx
evalCandsLoop :: ConstMap -> ICtx -> Knowledge -> EvalEnv -> IO ICtx
evalCandsLoop ConstMap
ie ICtx
ictx0 Knowledge
γ EvalEnv
env = ICtx -> IO ICtx
go ICtx
ictx0
  where
    withRewrites :: EvAccum -> EvAccum
withRewrites EvAccum
exprs =
      let
        rws :: [[(ExprV Symbol, ExprV Symbol)]]
rws = [ExprV Symbol -> Rewrite -> [(ExprV Symbol, ExprV Symbol)]
rewrite ExprV Symbol
e Rewrite
rw | Rewrite
rw <- ((Symbol, Symbol), Rewrite) -> Rewrite
forall a b. (a, b) -> b
snd (((Symbol, Symbol), Rewrite) -> Rewrite)
-> [((Symbol, Symbol), Rewrite)] -> [Rewrite]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (Symbol, Symbol) Rewrite -> [((Symbol, Symbol), Rewrite)]
forall k v. HashMap k v -> [(k, v)]
M.toList (Knowledge -> HashMap (Symbol, Symbol) Rewrite
knSims Knowledge
γ)
                            ,  ExprV Symbol
e <- HashSet (ExprV Symbol) -> [ExprV Symbol]
forall a. HashSet a -> [a]
S.toList ((ExprV Symbol, ExprV Symbol) -> ExprV Symbol
forall a b. (a, b) -> b
snd ((ExprV Symbol, ExprV Symbol) -> ExprV Symbol)
-> EvAccum -> HashSet (ExprV Symbol)
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
exprs)]
      in
        EvAccum
exprs EvAccum -> EvAccum -> EvAccum
forall a. Semigroup a => a -> a -> a
<> [(ExprV Symbol, ExprV Symbol)] -> EvAccum
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([[(ExprV Symbol, ExprV Symbol)]] -> [(ExprV Symbol, ExprV Symbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(ExprV Symbol, ExprV Symbol)]]
rws)
    go :: ICtx -> IO ICtx
go ICtx
ictx | HashSet (ExprV Symbol) -> Bool
forall a. HashSet a -> Bool
S.null (ICtx -> HashSet (ExprV Symbol)
icCands ICtx
ictx) = ICtx -> IO ICtx
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
    go ICtx
ictx =  do let cands :: HashSet (ExprV Symbol)
cands = ICtx -> HashSet (ExprV Symbol)
icCands ICtx
ictx
                  let env' :: EvalEnv
env' = EvalEnv
env { evAccum = icEquals ictx <> evAccum env }
                  (ICtx
ictx', [EvAccum]
evalResults)  <-
                               ((ICtx, [EvAccum]) -> ExprV Symbol -> IO (ICtx, [EvAccum]))
-> (ICtx, [EvAccum]) -> [ExprV Symbol] -> IO (ICtx, [EvAccum])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ConstMap
-> Knowledge
-> EvalEnv
-> (ICtx, [EvAccum])
-> ExprV Symbol
-> IO (ICtx, [EvAccum])
evalOneCandStep ConstMap
ie Knowledge
γ EvalEnv
env') (ICtx
ictx, []) (HashSet (ExprV Symbol) -> [ExprV Symbol]
forall a. HashSet a -> [a]
S.toList HashSet (ExprV Symbol)
cands)
                  let us :: EvAccum
us = [EvAccum] -> EvAccum
forall a. Monoid a => [a] -> a
mconcat [EvAccum]
evalResults
                  if EvAccum -> Bool
forall a. HashSet a -> Bool
S.null (EvAccum
us EvAccum -> EvAccum -> EvAccum
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` ICtx -> EvAccum
icEquals ICtx
ictx)
                        then ICtx -> IO ICtx
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
                        else do  let oks :: HashSet (ExprV Symbol)
oks      = (ExprV Symbol, ExprV Symbol) -> ExprV Symbol
forall a b. (a, b) -> a
fst ((ExprV Symbol, ExprV Symbol) -> ExprV Symbol)
-> EvAccum -> HashSet (ExprV Symbol)
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
us
                                 let us' :: EvAccum
us'      = EvAccum -> EvAccum
withRewrites EvAccum
us
                                 let ictx'' :: ICtx
ictx''   = ICtx
ictx' { icSolved = icSolved ictx <> oks
                                                      , icEquals = icEquals ictx <> us' }
                                 let newcands :: [ExprV Symbol]
newcands = [[ExprV Symbol]] -> [ExprV Symbol]
forall a. Monoid a => [a] -> a
mconcat (Knowledge -> ICtx -> ExprV Symbol -> [ExprV Symbol]
makeCandidates Knowledge
γ ICtx
ictx'' (ExprV Symbol -> [ExprV Symbol])
-> [ExprV Symbol] -> [[ExprV Symbol]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet (ExprV Symbol) -> [ExprV Symbol]
forall a. HashSet a -> [a]
S.toList (HashSet (ExprV Symbol)
cands HashSet (ExprV Symbol)
-> HashSet (ExprV Symbol) -> HashSet (ExprV Symbol)
forall a. Semigroup a => a -> a -> a
<> ((ExprV Symbol, ExprV Symbol) -> ExprV Symbol
forall a b. (a, b) -> b
snd ((ExprV Symbol, ExprV Symbol) -> ExprV Symbol)
-> EvAccum -> HashSet (ExprV Symbol)
forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
us)))
                                 ICtx -> IO ICtx
go (ICtx
ictx'' { icCands = S.fromList newcands})

-- evalOneCands :: Knowledge -> EvalEnv -> ICtx -> [Expr] -> IO (ICtx, [EvAccum])
-- evalOneCands γ env' ictx = foldM step (ictx, [])
evalOneCandStep :: ConstMap -> Knowledge -> EvalEnv -> (ICtx, [EvAccum]) -> Expr -> IO (ICtx, [EvAccum])
evalOneCandStep :: ConstMap
-> Knowledge
-> EvalEnv
-> (ICtx, [EvAccum])
-> ExprV Symbol
-> IO (ICtx, [EvAccum])
evalOneCandStep ConstMap
env Knowledge
γ EvalEnv
env' (ICtx
ictx, [EvAccum]
acc) ExprV Symbol
e = do
  EvAccum
res <- ConstMap
-> Knowledge -> EvalEnv -> ICtx -> ExprV Symbol -> IO EvAccum
evalOne ConstMap
env Knowledge
γ EvalEnv
env' ICtx
ictx ExprV Symbol
e
  (ICtx, [EvAccum]) -> IO (ICtx, [EvAccum])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ICtx
ictx, EvAccum
res EvAccum -> [EvAccum] -> [EvAccum]
forall a. a -> [a] -> [a]
: [EvAccum]
acc)

rewrite :: Expr -> Rewrite -> [(Expr,Expr)]
rewrite :: ExprV Symbol -> Rewrite -> [(ExprV Symbol, ExprV Symbol)]
rewrite ExprV Symbol
e Rewrite
rw = (ExprV Symbol -> Maybe (ExprV Symbol, ExprV Symbol))
-> [ExprV Symbol] -> [(ExprV Symbol, ExprV Symbol)]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (ExprV Symbol -> Rewrite -> Maybe (ExprV Symbol, ExprV Symbol)
`rewriteTop` Rewrite
rw) (ExprV Symbol -> [ExprV Symbol]
notGuardedApps ExprV Symbol
e)

rewriteTop :: Expr -> Rewrite -> Maybe (Expr,Expr)
rewriteTop :: ExprV Symbol -> Rewrite -> Maybe (ExprV Symbol, ExprV Symbol)
rewriteTop ExprV Symbol
e Rewrite
rw
  | (EVar Symbol
f, [ExprV Symbol]
es) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp ExprV Symbol
e
  , Symbol
f Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Rewrite -> Symbol
smDC Rewrite
rw
  , [ExprV Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExprV Symbol]
es Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
  = (ExprV Symbol, ExprV Symbol) -> Maybe (ExprV Symbol, ExprV Symbol)
forall a. a -> Maybe a
Just (ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
EApp (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar (Symbol -> ExprV Symbol) -> Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) ExprV Symbol
e, Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst ([(Symbol, ExprV Symbol)] -> Subst
mkSubst ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
rw) [ExprV Symbol]
es) (Rewrite -> ExprV Symbol
smBody Rewrite
rw))
  | Bool
otherwise
  = Maybe (ExprV Symbol, ExprV Symbol)
forall a. Maybe a
Nothing

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

resSInfo :: Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo :: 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, ExprV Symbol)] -> InstRes
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Int, ExprV Symbol)] -> InstRes)
-> [(Int, ExprV Symbol)] -> InstRes
forall a b. (a -> b) -> a -> b
$ Path -> [ExprV Symbol] -> [(Int, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip Path
is [ExprV Symbol]
ps''
    ps'' :: [ExprV Symbol]
ps''     = (Int -> ExprV Symbol -> ExprV Symbol)
-> Path -> [ExprV Symbol] -> [ExprV Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i -> ElabParam -> ExprV Symbol -> ExprV Symbol
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 [ExprV Symbol]
ps'
    ps' :: [ExprV Symbol]
ps'      = Config -> SymEnv -> [ExprV Symbol] -> [ExprV Symbol]
forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env [ExprV Symbol]
ps
    (Path
is, [ExprV Symbol]
ps) = [(Int, ExprV Symbol)] -> (Path, [ExprV Symbol])
forall a b. [(a, b)] -> ([a], [b])
unzip (InstRes -> [(Int, ExprV Symbol)]
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 -> BindEnv a
ieBEnv  :: !(BindEnv a)
  , forall a. InstEnv a -> AxiomEnv
ieAenv  :: !AxiomEnv
  , forall a. InstEnv a -> CMap (SimpC a)
ieCstrs :: !(CMap (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 -> HashSet (ExprV Symbol)
icCands    :: S.HashSet Expr            -- ^ "Candidates" for unfolding
  , ICtx -> EvAccum
icEquals   :: EvAccum                   -- ^ Accumulated equalities
  , ICtx -> HashSet (ExprV Symbol)
icSolved   :: S.HashSet Expr            -- ^ Terms that we have already expanded
  , ICtx -> ConstMap
icSimpl    :: !ConstMap                 -- ^ Map of expressions to constants
  , ICtx -> Maybe SubcId
icSubcId   :: Maybe SubcId              -- ^ Current subconstraint ID
  }

----------------------------------------------------------------------------------------------
-- | @InstRes@ is the final result of PLE; a map from @BindId@ to the equations "known" at that BindId
----------------------------------------------------------------------------------------------

type InstRes = M.HashMap BindId Expr

----------------------------------------------------------------------------------------------
-- | @Unfold is the result of running PLE at a single equality;
--     (e, [(e1, e1')...]) is the source @e@ and the (possible empty)
--   list of PLE-generated equalities (e1, e1') ...
----------------------------------------------------------------------------------------------

type CTrie   = T.Trie   SubcId
type CBranch = T.Branch SubcId
type Diff    = [BindId]    -- ^ in "reverse" order

initCtx :: InstEnv a -> [(Expr,Expr)] -> ICtx
initCtx :: forall a. InstEnv a -> [(ExprV Symbol, ExprV Symbol)] -> ICtx
initCtx InstEnv a
_   [(ExprV Symbol, ExprV Symbol)]
es   = ICtx
  { icCands :: HashSet (ExprV Symbol)
icCands  = HashSet (ExprV Symbol)
forall a. Monoid a => a
mempty
  , icEquals :: EvAccum
icEquals = [(ExprV Symbol, ExprV Symbol)] -> EvAccum
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [(ExprV Symbol, ExprV Symbol)]
es
  , icSolved :: HashSet (ExprV Symbol)
icSolved = HashSet (ExprV Symbol)
forall a. Monoid a => a
mempty
  , icSimpl :: ConstMap
icSimpl  = ConstMap
forall a. Monoid a => a
mempty
  , icSubcId :: Maybe SubcId
icSubcId = Maybe SubcId
forall a. Maybe a
Nothing
  }

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

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


updRes :: InstRes -> Maybe BindId -> Expr -> InstRes
updRes :: InstRes -> Maybe Int -> ExprV Symbol -> InstRes
updRes InstRes
res (Just Int
i) ExprV Symbol
e = (ExprV Symbol -> ExprV Symbol -> ExprV Symbol)
-> Int -> ExprV Symbol -> InstRes -> InstRes
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith ([Char] -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall a. HasCallStack => [Char] -> a
error [Char]
"tree-like invariant broken in ple. See https://github.com/ucsd-progsys/liquid-fixpoint/issues/496") Int
i ExprV Symbol
e InstRes
res
updRes InstRes
res  Maybe Int
Nothing ExprV Symbol
_ = 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{CMap (SimpC a)
BindEnv a
AxiomEnv
Knowledge
EvalEnv
ieAenv :: forall a. InstEnv a -> AxiomEnv
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieKnowl :: forall a. InstEnv a -> Knowledge
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieBEnv :: BindEnv a
ieAenv :: AxiomEnv
ieCstrs :: CMap (SimpC a)
ieKnowl :: Knowledge
ieEvEnv :: EvalEnv
..} ICtx
ctx Path
delta Maybe SubcId
cidMb
    = ICtx
ctx { icCands  = S.fromList cands           <> icCands  ctx
          , icEquals = initEqs                    <> icEquals ctx
          , icSimpl  = M.fromList (S.toList sims) <> icSimpl ctx <> econsts
          , icSubcId = cidMb -- fst <$> L.find (\(_, b) -> (head delta) `memberIBindEnv` (_cenv b)) ieCstrs
          }                  -- eliminate above if nothing broken
  where
    initEqs :: EvAccum
initEqs   = [(ExprV Symbol, ExprV Symbol)] -> EvAccum
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([(ExprV Symbol, ExprV Symbol)] -> EvAccum)
-> [(ExprV Symbol, ExprV Symbol)] -> EvAccum
forall a b. (a -> b) -> a -> b
$ [[(ExprV Symbol, ExprV Symbol)]] -> [(ExprV Symbol, ExprV Symbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ExprV Symbol -> Rewrite -> [(ExprV Symbol, ExprV Symbol)]
rewrite ExprV Symbol
e Rewrite
rw | ExprV Symbol
e  <- [ExprV Symbol]
cands [ExprV Symbol] -> [ExprV Symbol] -> [ExprV Symbol]
forall a. [a] -> [a] -> [a]
++ ((ExprV Symbol, ExprV Symbol) -> ExprV Symbol
forall a b. (a, b) -> b
snd ((ExprV Symbol, ExprV Symbol) -> ExprV Symbol)
-> [(ExprV Symbol, ExprV Symbol)] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EvAccum -> [(ExprV Symbol, ExprV Symbol)]
forall a. HashSet a -> [a]
S.toList (ICtx -> EvAccum
icEquals ICtx
ctx))
                                                  , Rewrite
rw <- ((Symbol, Symbol), Rewrite) -> Rewrite
forall a b. (a, b) -> b
snd (((Symbol, Symbol), Rewrite) -> Rewrite)
-> [((Symbol, Symbol), Rewrite)] -> [Rewrite]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap (Symbol, Symbol) Rewrite -> [((Symbol, Symbol), Rewrite)]
forall k v. HashMap k v -> [(k, v)]
M.toList (Knowledge -> HashMap (Symbol, Symbol) Rewrite
knSims Knowledge
ieKnowl)]
    cands :: [ExprV Symbol]
cands     = (ExprV Symbol -> [ExprV Symbol])
-> [ExprV Symbol] -> [ExprV Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Knowledge -> ICtx -> ExprV Symbol -> [ExprV Symbol]
makeCandidates Knowledge
ieKnowl ICtx
ctx) (ExprV Symbol
rhsExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> [a] -> [a]
:[ExprV Symbol]
es)
    sims :: EvAccum
sims      = ((ExprV Symbol, ExprV Symbol) -> Bool) -> EvAccum -> EvAccum
forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter (HashSet Symbol -> (ExprV Symbol, ExprV Symbol) -> Bool
isSimplification (Knowledge -> HashSet Symbol
knDCs Knowledge
ieKnowl)) (EvAccum
initEqs EvAccum -> EvAccum -> EvAccum
forall a. Semigroup a => a -> a -> a
<> ICtx -> EvAccum
icEquals ICtx
ctx)
    econsts :: ConstMap
econsts   = [(ExprV Symbol, ExprV Symbol)] -> ConstMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(ExprV Symbol, ExprV Symbol)] -> ConstMap)
-> [(ExprV Symbol, ExprV Symbol)] -> ConstMap
forall a b. (a -> b) -> a -> b
$ Knowledge -> [ExprV Symbol] -> [(ExprV Symbol, ExprV Symbol)]
findConstants Knowledge
ieKnowl [ExprV Symbol]
es
    rhs :: ExprV Symbol
rhs       = ExprV Symbol -> ExprV Symbol
unElab ExprV Symbol
eRhs
    es :: [ExprV Symbol]
es        = ExprV Symbol -> ExprV Symbol
unElab (ExprV Symbol -> ExprV Symbol)
-> ((Symbol, SortedReft) -> ExprV Symbol)
-> (Symbol, SortedReft)
-> ExprV Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SortedReft) -> ExprV Symbol
forall a. Expression a => a -> ExprV Symbol
expr ((Symbol, SortedReft) -> ExprV Symbol)
-> [(Symbol, SortedReft)] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ (Symbol
x, SortedReft
y) | (Symbol
x, SortedReft
y,a
_ ) <- [(Symbol, SortedReft, a)]
binds ]
    eRhs :: ExprV Symbol
eRhs      = ExprV Symbol
-> (SimpC a -> ExprV Symbol) -> Maybe (SimpC a) -> ExprV Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ExprV Symbol
forall v. ExprV v
PTrue SimpC a -> ExprV Symbol
forall (c :: * -> *) a. TaggedC c a => c a -> ExprV Symbol
crhs Maybe (SimpC a)
subMb
    binds :: [(Symbol, SortedReft, a)]
binds     = [ Int -> BindEnv a -> (Symbol, SortedReft, a)
forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv a
ieBEnv | Int
i <- Path
delta ]
    subMb :: Maybe (SimpC a)
subMb     = CMap (SimpC a) -> SubcId -> SimpC a
forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr CMap (SimpC a)
ieCstrs (SubcId -> SimpC a) -> Maybe SubcId -> Maybe (SimpC a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SubcId
cidMb


findConstants :: Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants :: Knowledge -> [ExprV Symbol] -> [(ExprV Symbol, ExprV Symbol)]
findConstants Knowledge
γ [ExprV Symbol]
es = [(Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
x, ExprV Symbol
c) | (Symbol
x,ExprV Symbol
c) <- [(Symbol, ExprV Symbol)]
-> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
go [] ((ExprV Symbol -> [ExprV Symbol])
-> [ExprV Symbol] -> [ExprV Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ExprV Symbol -> [ExprV Symbol]
splitPAnd [ExprV Symbol]
es)]
  where
    go :: [(Symbol, ExprV Symbol)]
-> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
go [(Symbol, ExprV Symbol)]
su [ExprV Symbol]
ess = if [ExprV Symbol]
ess [ExprV Symbol] -> [ExprV Symbol] -> Bool
forall a. Eq a => a -> a -> Bool
== [ExprV Symbol]
ess'
                  then [(Symbol, ExprV Symbol)]
su
                  else [(Symbol, ExprV Symbol)]
-> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
go ([(Symbol, ExprV Symbol)]
su [(Symbol, ExprV Symbol)]
-> [(Symbol, ExprV Symbol)] -> [(Symbol, ExprV Symbol)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, ExprV Symbol)]
su') [ExprV Symbol]
ess'
       where ess' :: [ExprV Symbol]
ess' = Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst ([(Symbol, ExprV Symbol)] -> Subst
mkSubst [(Symbol, ExprV Symbol)]
su') (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
ess
             su' :: [(Symbol, ExprV Symbol)]
su'  = [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
makeSu [ExprV Symbol]
ess
    makeSu :: [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
makeSu [ExprV Symbol]
exprs  = [(Symbol
x,ExprV Symbol
c) | (EEq (EVar Symbol
x) ExprV Symbol
c) <- [ExprV Symbol]
exprs
                           , HashSet Symbol -> ExprV Symbol -> Bool
isConstant (Knowledge -> HashSet Symbol
knDCs Knowledge
γ) ExprV Symbol
c
                           , Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
x ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= ExprV Symbol
c ]

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

    -- Constructor occurrences need to be considered as candidadates since
    -- they identify relevant measure equations. The function 'rewrite'
    -- introduces these equations.
    hasConstructors :: Knowledge -> Expr -> Bool
    hasConstructors :: Knowledge -> ExprV Symbol -> Bool
hasConstructors Knowledge
γ ExprV Symbol
e =  Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null (HashSet Symbol -> Bool) -> HashSet Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.intersection (ExprV Symbol -> HashSet Symbol
exprSymbolsSet ExprV Symbol
e) (Knowledge -> HashSet Symbol
knDCs Knowledge
γ)

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


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




getCstr :: M.HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr :: 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

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)

type EvAccum = S.HashSet (Expr, Expr)

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

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


evalOne :: ConstMap -> Knowledge -> EvalEnv -> ICtx -> Expr -> IO EvAccum
evalOne :: ConstMap
-> Knowledge -> EvalEnv -> ICtx -> ExprV Symbol -> IO EvAccum
evalOne ConstMap
ienv Knowledge
γ EvalEnv
env ICtx
ctx ExprV Symbol
e {- null (getAutoRws γ ctx) -} = do
    (ExprV Symbol
e', EvalEnv
st) <- StateT EvalEnv IO (ExprV Symbol)
-> EvalEnv -> IO (ExprV Symbol, EvalEnv)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ConstMap
-> Knowledge
-> ICtx
-> ExprV Symbol
-> StateT EvalEnv IO (ExprV Symbol)
fastEval ConstMap
ienv Knowledge
γ ICtx
ctx ExprV Symbol
e) EvalEnv
env
    let evAcc' :: EvAccum
evAcc' = if [Char] -> ExprV Symbol -> ExprV Symbol
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evalOne: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ExprV Symbol -> [Char]
forall a. PPrint a => a -> [Char]
showpp ExprV Symbol
e) ExprV Symbol
e' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
e then EvalEnv -> EvAccum
evAccum EvalEnv
st else (ExprV Symbol, ExprV Symbol) -> EvAccum -> EvAccum
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (ExprV Symbol
e, ExprV Symbol
e') (EvalEnv -> EvAccum
evAccum EvalEnv
st)
    EvAccum -> IO EvAccum
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return EvAccum
evAcc'

notGuardedApps :: Expr -> [Expr]
notGuardedApps :: ExprV Symbol -> [ExprV Symbol]
notGuardedApps = (ExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol])
-> [ExprV Symbol] -> ExprV Symbol -> [ExprV Symbol]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall {v}. ExprV v -> [ExprV v] -> [ExprV v]
go []
  where
    go :: ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e0 [ExprV v]
acc = case ExprV v
e0 of
      EApp ExprV v
e1 ExprV v
e2 -> ExprV v
e0 ExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
: ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 (ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc)
      PAnd [ExprV v]
es    -> (ExprV v -> [ExprV v] -> [ExprV v])
-> [ExprV v] -> [ExprV v] -> [ExprV v]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ExprV v -> [ExprV v] -> [ExprV v]
go [ExprV v]
acc [ExprV v]
es
      POr [ExprV v]
es     -> (ExprV v -> [ExprV v] -> [ExprV v])
-> [ExprV v] -> [ExprV v] -> [ExprV v]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ExprV v -> [ExprV v] -> [ExprV v]
go [ExprV v]
acc [ExprV v]
es
      PAtom Brel
_ ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      PIff ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      PImp ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      EBin  Bop
_ ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      PNot ExprV v
e -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      ENeg ExprV v
e -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      EIte ExprV v
b ExprV v
_ ExprV v
_ -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
b ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v
e0 ExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
: [ExprV v]
acc
      ECoerc Sort
_ Sort
_ ExprV v
e -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      ECst ExprV v
e Sort
_ -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      ESym SymConst
_ -> [ExprV v]
acc
      ECon Constant
_ -> [ExprV v]
acc
      EVar v
_ -> [ExprV v]
acc
      ELam (Symbol, Sort)
_ ExprV v
_ -> [ExprV v]
acc
      ETApp ExprV v
_ Sort
_ -> [ExprV v]
acc
      ETAbs ExprV v
_ Symbol
_ -> [ExprV v]
acc
      PKVar KVar
_ SubstV v
_ -> [ExprV v]
acc
      PAll [(Symbol, Sort)]
_ ExprV v
_ -> [ExprV v]
acc
      PExist [(Symbol, Sort)]
_ ExprV v
_ -> [ExprV v]
acc
      PGrad{} -> [ExprV v]
acc

largestApps :: Expr -> [Expr]
largestApps :: ExprV Symbol -> [ExprV Symbol]
largestApps = (ExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol])
-> [ExprV Symbol] -> ExprV Symbol -> [ExprV Symbol]
forall a b c. (a -> b -> c) -> b -> a -> c
flip ExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall {v}. ExprV v -> [ExprV v] -> [ExprV v]
go []
  where
    go :: ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e0 [ExprV v]
acc = case ExprV v
e0 of
      EApp ExprV v
_ ExprV v
_ -> ExprV v
e0 ExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
: [ExprV v]
acc
      PAnd [ExprV v]
es -> (ExprV v -> [ExprV v] -> [ExprV v])
-> [ExprV v] -> [ExprV v] -> [ExprV v]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ExprV v -> [ExprV v] -> [ExprV v]
go [ExprV v]
acc [ExprV v]
es
      POr [ExprV v]
es -> (ExprV v -> [ExprV v] -> [ExprV v])
-> [ExprV v] -> [ExprV v] -> [ExprV v]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ExprV v -> [ExprV v] -> [ExprV v]
go [ExprV v]
acc [ExprV v]
es
      PAtom Brel
_ ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      PIff ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      PImp ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      EBin  Bop
_ ExprV v
e1 ExprV v
e2 -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e1 ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e2 [ExprV v]
acc
      PNot ExprV v
e -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      ENeg ExprV v
e -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      EIte ExprV v
b ExprV v
_ ExprV v
_ -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
b ([ExprV v] -> [ExprV v]) -> [ExprV v] -> [ExprV v]
forall a b. (a -> b) -> a -> b
$ ExprV v
e0 ExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
: [ExprV v]
acc
      ECoerc Sort
_ Sort
_ ExprV v
e -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      ECst ExprV v
e Sort
_ -> ExprV v -> [ExprV v] -> [ExprV v]
go ExprV v
e [ExprV v]
acc
      ESym SymConst
_ -> [ExprV v]
acc
      ECon Constant
_ -> [ExprV v]
acc
      EVar v
_ -> ExprV v
e0 ExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
: [ExprV v]
acc
      ELam (Symbol, Sort)
_ ExprV v
_ -> [ExprV v]
acc
      ETApp ExprV v
_ Sort
_ -> [ExprV v]
acc
      ETAbs ExprV v
_ Symbol
_ -> [ExprV v]
acc
      PKVar KVar
_ SubstV v
_ -> [ExprV v]
acc
      PAll [(Symbol, Sort)]
_ ExprV v
_ -> [ExprV v]
acc
      PExist [(Symbol, Sort)]
_ ExprV v
_ -> [ExprV v]
acc
      PGrad{} -> [ExprV v]
acc

fastEval :: ConstMap -> Knowledge -> ICtx -> Expr -> EvalST Expr
fastEval :: ConstMap
-> Knowledge
-> ICtx
-> ExprV Symbol
-> StateT EvalEnv IO (ExprV Symbol)
fastEval ConstMap
ienv Knowledge
γ ICtx
ctx ExprV Symbol
e
    = 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)
         ExprV Symbol -> StateT EvalEnv IO (ExprV Symbol)
forall a. a -> StateT EvalEnv IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExprV Symbol -> StateT EvalEnv IO (ExprV Symbol))
-> ExprV Symbol -> StateT EvalEnv IO (ExprV Symbol)
forall a b. (a -> b) -> a -> b
$ [Char] -> ExprV Symbol -> ExprV Symbol
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evaluating" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ExprV Symbol -> [Char]
forall a. Show a => a -> [Char]
show ExprV Symbol
e) (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret ConstMap
ienv Knowledge
γ ICtx
ctx SEnv Sort
env (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ Knowledge -> ICtx -> ExprV Symbol -> ExprV Symbol
forall a. Simplifiable a => Knowledge -> ICtx -> a -> a
simplify Knowledge
γ ICtx
ctx ExprV Symbol
e

--------------------------------------------------------------------------------
-- | 'substEq' unfolds or instantiates an equation at a particular list of
--   argument values. We must also substitute the sort-variables that appear
--   as coercions. See tests/proof/ple1.fq
--------------------------------------------------------------------------------

unfoldExpr :: ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> {-EvalST-} Expr
unfoldExpr :: ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
unfoldExpr ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (EIte ExprV Symbol
e0 ExprV Symbol
e1 ExprV Symbol
e2) = let g' :: ExprV Symbol
g' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e0 in
                                             if ExprV Symbol
g' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PTrue
                                                then ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
unfoldExpr ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1
                                                else if ExprV Symbol
g' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PFalse
                                                        then ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
unfoldExpr ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e2
                                                        else ExprV Symbol -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte ExprV Symbol
g' ExprV Symbol
e1 ExprV Symbol
e2
unfoldExpr ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   ExprV Symbol
e               = ExprV Symbol
e

substEq :: SEnv Sort -> Equation -> [Expr] -> Expr
substEq :: SEnv Sort -> EquationV Symbol -> [ExprV Symbol] -> ExprV Symbol
substEq SEnv Sort
env EquationV Symbol
eq [ExprV Symbol]
es = Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst Subst
su (SEnv Sort -> EquationV Symbol -> [ExprV Symbol] -> ExprV Symbol
substEqCoerce SEnv Sort
env EquationV Symbol
eq [ExprV Symbol]
es)
  where su :: Subst
su = [(Symbol, ExprV Symbol)] -> Subst
mkSubst ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (EquationV Symbol -> [Symbol]
eqArgNames EquationV Symbol
eq) [ExprV Symbol]
es

substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
substEqCoerce :: SEnv Sort -> EquationV Symbol -> [ExprV Symbol] -> ExprV Symbol
substEqCoerce SEnv Sort
env EquationV Symbol
eq [ExprV Symbol]
es = CoSub -> ExprV Symbol -> ExprV Symbol
Vis.applyCoSub CoSub
coSub (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ EquationV Symbol -> ExprV Symbol
forall v. EquationV v -> ExprV v
eqBody EquationV Symbol
eq
  where
    ts :: [Sort]
ts    = (Symbol, Sort) -> Sort
forall a b. (a, b) -> b
snd    ((Symbol, Sort) -> Sort) -> [(Symbol, Sort)] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EquationV Symbol -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs EquationV Symbol
eq
    sp :: SrcSpan
sp    = [Char] -> SrcSpan
panicSpan [Char]
"mkCoSub"
    eTs :: [Sort]
eTs   = SrcSpan -> SEnv Sort -> ExprV Symbol -> Sort
sortExpr SrcSpan
sp SEnv Sort
env (ExprV Symbol -> Sort) -> [ExprV Symbol] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExprV Symbol]
es
    coSub :: CoSub
coSub = SEnv Sort -> [Sort] -> [Sort] -> CoSub
mkCoSub SEnv Sort
env [Sort]
eTs [Sort]
ts

mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub
mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> CoSub
mkCoSub SEnv Sort
env [Sort]
eTs [Sort]
xTs = [(Symbol, Sort)] -> CoSub
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x, [Sort] -> Sort
unite [Sort]
ys) | (Symbol
x, [Sort]
ys) <- [(Symbol, Sort)] -> [(Symbol, [Sort])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, Sort)]
xys ]
  where
    unite :: [Sort] -> Sort
unite [Sort]
ts    = Sort -> Maybe Sort -> Sort
forall a. a -> Maybe a -> a
Mb.fromMaybe ([Sort] -> Sort
forall {a} {a}. PPrint a => a -> a
uError [Sort]
ts) (Env -> [Sort] -> Maybe Sort
unifyTo1 Env
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         = [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. Ord a => [a] -> [a]
Misc.sortNub ([(Symbol, Sort)] -> [(Symbol, Sort)])
-> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ [[(Symbol, Sort)]] -> [(Symbol, Sort)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(Symbol, Sort)]] -> [(Symbol, Sort)])
-> [[(Symbol, Sort)]] -> [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ (Sort -> Sort -> [(Symbol, Sort)])
-> [Sort] -> [Sort] -> [[(Symbol, Sort)]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Sort -> Sort -> [(Symbol, Sort)]
matchSorts [Sort]
_xTs [Sort]
_eTs
    ([Sort]
_xTs,[Sort]
_eTs) = ([Sort]
xTs, [Sort]
eTs)

matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
matchSorts = Sort -> Sort -> [(Symbol, Sort)]
go
  where
    go :: Sort -> Sort -> [(Symbol, Sort)]
go (FObj Symbol
x)      {-FObj-} Sort
y    = [(Symbol
x, Sort
y)]
    go (FAbs Int
_ Sort
t1)   (FAbs Int
_ Sort
t2)   = Sort -> Sort -> [(Symbol, Sort)]
go Sort
t1 Sort
t2
    go (FFunc Sort
s1 Sort
t1) (FFunc Sort
s2 Sort
t2) = Sort -> Sort -> [(Symbol, Sort)]
go Sort
s1 Sort
s2 [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ Sort -> Sort -> [(Symbol, Sort)]
go Sort
t1 Sort
t2
    go (FApp Sort
s1 Sort
t1)  (FApp Sort
s2 Sort
t2)  = Sort -> Sort -> [(Symbol, Sort)]
go Sort
s1 Sort
s2 [(Symbol, Sort)] -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. [a] -> [a] -> [a]
++ Sort -> Sort -> [(Symbol, Sort)]
go Sort
t1 Sort
t2
    go Sort
_             Sort
_             = []

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

eqArgNames :: Equation -> [Symbol]
eqArgNames :: EquationV Symbol -> [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])
-> (EquationV Symbol -> [(Symbol, Sort)])
-> EquationV Symbol
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EquationV Symbol -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs

interpret' :: ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' :: ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e = [Char] -> ExprV Symbol -> ExprV Symbol
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"Interpreting " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ExprV Symbol -> [Char]
forall a. Show a => a -> [Char]
show ExprV Symbol
e) (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e

interpret :: ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret :: ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   e :: ExprV Symbol
e@(ESym SymConst
_)       = ExprV Symbol
e
interpret ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   e :: ExprV Symbol
e@(ECon Constant
_)       = ExprV Symbol
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (EVar Symbol
sym)
    | Just ExprV Symbol
e' <- ExprV Symbol -> ConstMap -> Maybe (ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
sym) (ICtx -> ConstMap
icSimpl ICtx
ctx)
    = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e'
interpret ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   e :: ExprV Symbol
e@(EVar Symbol
_)       = ExprV Symbol
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (EApp ExprV Symbol
e1 ExprV Symbol
e2)
  | ExprV Symbol -> Bool
isSetPred ExprV Symbol
e1                        = let e2' :: ExprV Symbol
e2' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e2 in
                                             ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applySetFolding ExprV Symbol
e1 ExprV Symbol
e2'
interpret ConstMap
cmap Knowledge
know ICtx
ictx SEnv Sort
ssenv e :: ExprV Symbol
e@(EApp ExprV Symbol
_ ExprV Symbol
_)     = case ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp ExprV Symbol
e of
  (ExprV Symbol
exprs, [ExprV Symbol]
exprses) -> let g :: ExprV Symbol -> ExprV Symbol
g = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
cmap Knowledge
know ICtx
ictx SEnv Sort
ssenv in
    ConstMap
-> Knowledge
-> ICtx
-> SEnv Sort
-> ExprV Symbol
-> [ExprV Symbol]
-> ExprV Symbol
interpretApp ConstMap
cmap Knowledge
know ICtx
ictx SEnv Sort
ssenv (ExprV Symbol -> ExprV Symbol
g ExprV Symbol
exprs) ((ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ExprV Symbol -> ExprV Symbol
g [ExprV Symbol]
exprses)
    where
      interpretApp :: ConstMap
-> Knowledge
-> ICtx
-> SEnv Sort
-> ExprV Symbol
-> [ExprV Symbol]
-> ExprV Symbol
interpretApp ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (EVar Symbol
f) [ExprV Symbol]
es
        | Just EquationV Symbol
eq <- Symbol
-> HashMap Symbol (EquationV Symbol) -> Maybe (EquationV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f (Knowledge -> HashMap Symbol (EquationV Symbol)
knAms Knowledge
γ)
        , [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EquationV Symbol -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs EquationV Symbol
eq) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [ExprV Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExprV Symbol]
es
        = let ([ExprV Symbol]
es1,[ExprV Symbol]
es2) = Int -> [ExprV Symbol] -> ([ExprV Symbol], [ExprV Symbol])
forall a. Int -> [a] -> ([a], [a])
splitAt ([(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EquationV Symbol -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs EquationV Symbol
eq)) [ExprV Symbol]
es
              ges :: ExprV Symbol
ges       = SEnv Sort -> EquationV Symbol -> [ExprV Symbol] -> ExprV Symbol
substEq SEnv Sort
env EquationV Symbol
eq [ExprV Symbol]
es1
              exp1 :: ExprV Symbol
exp1      = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
unfoldExpr ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
ges
              exp2 :: ExprV Symbol
exp2      = ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps ExprV Symbol
exp1 [ExprV Symbol]
es2 in  --exp' -- TODO undo
            if ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
f) [ExprV Symbol]
es ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
exp2 then ExprV Symbol
exp2 else ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
exp2

      interpretApp ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (EVar Symbol
f) (ExprV Symbol
e1:[ExprV Symbol]
es)
        | (EVar Symbol
dc, [ExprV Symbol]
as) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp ExprV Symbol
e1
        , Just Rewrite
rw <- (Symbol, Symbol)
-> HashMap (Symbol, Symbol) Rewrite -> Maybe Rewrite
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (Symbol
f, Symbol
dc) (Knowledge -> HashMap (Symbol, Symbol) Rewrite
knSims Knowledge
γ)
        , [ExprV Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ExprV Symbol]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
        = let e' :: ExprV Symbol
e' = ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (Subst -> ExprV Symbol -> ExprV Symbol
forall a. Subable a => Subst -> a -> a
subst ([(Symbol, ExprV Symbol)] -> Subst
mkSubst ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [ExprV Symbol] -> [(Symbol, ExprV Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
rw) [ExprV Symbol]
as) (Rewrite -> ExprV Symbol
smBody Rewrite
rw)) [ExprV Symbol]
es in --e' -- TODO undo
            if ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
f) [ExprV Symbol]
es ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
e' then ExprV Symbol
e' else ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e'

      interpretApp ConstMap
_  Knowledge
γ ICtx
_   SEnv Sort
_   (EVar Symbol
f) [ExprV Symbol
e0]
        | (EVar Symbol
dc, [ExprV Symbol]
_as) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp ExprV Symbol
e0
        , Symbol -> Bool
isTestSymbol Symbol
f
        = if Symbol -> Symbol
testSymbol Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
f then ExprV Symbol
forall v. ExprV v
PTrue else
            if Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
dc (Knowledge -> HashSet Symbol
knAllDCs Knowledge
γ) then ExprV Symbol
forall v. ExprV v
PFalse else {-simplify γ ctx $-} ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps (Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
f) [ExprV Symbol
e0]

      interpretApp ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   ExprV Symbol
f        [ExprV Symbol]
es     = {-simplify γ ctx $-} ExprV Symbol -> [ExprV Symbol] -> ExprV Symbol
forall v. ExprV v -> [ExprV v] -> ExprV v
eApps ExprV Symbol
f [ExprV Symbol]
es
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ENeg ExprV Symbol
e1)      = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1 in
                                            Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applyConstantFolding Bop
Minus (Constant -> ExprV Symbol
forall v. Constant -> ExprV v
ECon (SubcId -> Constant
I SubcId
0)) ExprV Symbol
e1'
--                                          simplify γ ctx (ENeg e1')
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (EBin Bop
o ExprV Symbol
e1 ExprV Symbol
e2) = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1
                                              e2' :: ExprV Symbol
e2' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e2 in
                                            Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applyConstantFolding Bop
o ExprV Symbol
e1' ExprV Symbol
e2'
--                                          simplify γ ctx (EBin o e1' e2')
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (EIte ExprV Symbol
g ExprV Symbol
e1 ExprV Symbol
e2) = let b :: ExprV Symbol
b = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
g in
                                            if ExprV Symbol
b ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PTrue then ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1 else
                                              if ExprV Symbol
b ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PFalse then ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e2 else
                                                Knowledge -> ICtx -> ExprV Symbol -> ExprV Symbol
forall a. Simplifiable a => Knowledge -> ICtx -> a -> a
simplify Knowledge
γ ICtx
ctx (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte ExprV Symbol
b ExprV Symbol
e1 ExprV Symbol
e2
--                                          EIte b (interpret' γ ctx env e1) (interpret' γ ctx env e2)
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ECst ExprV Symbol
e1 Sort
s)    = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1 in
                                            ExprV Symbol -> Sort -> ExprV Symbol
simplifyCasts ExprV Symbol
e1' Sort
s -- ECst e1' s
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (ELam (Symbol
x,Sort
s) ExprV Symbol
e)   = let γ' :: Knowledge
γ' = Knowledge
γ { knLams = (x, s) : knLams γ }
                                              e' :: ExprV Symbol
e' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ' ICtx
ctx SEnv Sort
env ExprV Symbol
e in
                                            (Symbol, Sort) -> ExprV Symbol -> ExprV Symbol
forall v. (Symbol, Sort) -> ExprV v -> ExprV v
ELam (Symbol
x, Sort
s) ExprV Symbol
e'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ETApp ExprV Symbol
e1 Sort
t)   = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1 in ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ETApp ExprV Symbol
e1' Sort
t
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ETAbs ExprV Symbol
e1 Symbol
sy)  = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1 in ExprV Symbol -> Symbol -> ExprV Symbol
forall v. ExprV v -> Symbol -> ExprV v
ETAbs ExprV Symbol
e1' Symbol
sy
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (PAnd [ExprV Symbol]
exprses) = let es' :: [ExprV Symbol]
es' = (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env) [ExprV Symbol]
exprses in [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go [] ([ExprV Symbol] -> [ExprV Symbol]
forall a. [a] -> [a]
reverse [ExprV Symbol]
es')
  where
    go :: [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go []  []         = ExprV Symbol
forall v. ExprV v
PTrue
    go [ExprV Symbol
p] []         = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
p
    go [ExprV Symbol]
acc []         = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd [ExprV Symbol]
acc
    go [ExprV Symbol]
acc (ExprV Symbol
PTrue:[ExprV Symbol]
es) = [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go [ExprV Symbol]
acc [ExprV Symbol]
es
    go [ExprV Symbol]
_   (ExprV Symbol
PFalse:[ExprV Symbol]
_) = ExprV Symbol
forall v. ExprV v
PFalse
    go [ExprV Symbol]
acc (ExprV Symbol
e:[ExprV Symbol]
es)     = [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go (ExprV Symbol
eExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> [a] -> [a]
:[ExprV Symbol]
acc) [ExprV Symbol]
es
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (POr [ExprV Symbol]
exprses)      = let es' :: [ExprV Symbol]
es' = (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env) [ExprV Symbol]
exprses in [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go [] ([ExprV Symbol] -> [ExprV Symbol]
forall a. [a] -> [a]
reverse [ExprV Symbol]
es')
  where
    go :: [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go []  []          = ExprV Symbol
forall v. ExprV v
PFalse
    go [ExprV Symbol
p] []          = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
p
    go [ExprV Symbol]
acc []          = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
POr [ExprV Symbol]
acc
    go [ExprV Symbol]
_   (ExprV Symbol
PTrue:[ExprV Symbol]
_)   = ExprV Symbol
forall v. ExprV v
PTrue
    go [ExprV Symbol]
acc (ExprV Symbol
PFalse:[ExprV Symbol]
es) = [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go [ExprV Symbol]
acc [ExprV Symbol]
es
    go [ExprV Symbol]
acc (ExprV Symbol
e:[ExprV Symbol]
es)      = [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
go (ExprV Symbol
eExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> [a] -> [a]
:[ExprV Symbol]
acc) [ExprV Symbol]
es
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PNot ExprV Symbol
e)         = let e' :: ExprV Symbol
e' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e in case ExprV Symbol
e' of
    (PNot ExprV Symbol
e'')    -> ExprV Symbol
e''
    ExprV Symbol
PTrue         -> ExprV Symbol
forall v. ExprV v
PFalse
    ExprV Symbol
PFalse        -> ExprV Symbol
forall v. ExprV v
PTrue
    ExprV Symbol
_             -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot ExprV Symbol
e'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PImp ExprV Symbol
e1 ExprV Symbol
e2)     = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1
                                              e2' :: ExprV Symbol
e2' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e2 in
                                            if ExprV Symbol
e1' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PFalse Bool -> Bool -> Bool
|| ExprV Symbol
e2' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PTrue then ExprV Symbol
forall v. ExprV v
PTrue else
                                              if ExprV Symbol
e1' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PTrue then ExprV Symbol
e2' else
                                                if ExprV Symbol
e2' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PFalse then ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot ExprV Symbol
e1') else
                                                  ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PImp ExprV Symbol
e1' ExprV Symbol
e2'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PIff ExprV Symbol
e1 ExprV Symbol
e2)     = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1
                                              e2' :: ExprV Symbol
e2' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e2 in
                                            if ExprV Symbol
e1' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PTrue then ExprV Symbol
e2' else
                                              if ExprV Symbol
e2' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PTrue then ExprV Symbol
e1' else
                                                if ExprV Symbol
e1' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PFalse then ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot ExprV Symbol
e2') else
                                                  if ExprV Symbol
e2' ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PFalse then ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot ExprV Symbol
e1') else
                                                    ExprV Symbol -> ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v -> ExprV v
PIff ExprV Symbol
e1' ExprV Symbol
e2'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PAtom Brel
o ExprV Symbol
e1 ExprV Symbol
e2)  = let e1' :: ExprV Symbol
e1' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1
                                              e2' :: ExprV Symbol
e2' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e2 in
                                            Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applyBooleanFolding Brel
o ExprV Symbol
e1' ExprV Symbol
e2'
interpret ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   e :: ExprV Symbol
e@(PKVar KVar
_ Subst
_)    = ExprV Symbol
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env e :: ExprV Symbol
e@(PAll [(Symbol, Sort)]
xss ExprV Symbol
e1)  = case [(Symbol, Sort)]
xss of
  [] -> ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1
  [(Symbol, Sort)]
_  -> ExprV Symbol
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env e :: ExprV Symbol
e@(PExist [(Symbol, Sort)]
xss ExprV Symbol
e1) = case [(Symbol, Sort)]
xss of
  [] -> ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e1
  [(Symbol, Sort)]
_  -> ExprV Symbol
e
interpret ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   e :: ExprV Symbol
e@PGrad{}         = ExprV Symbol
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (ECoerc Sort
s Sort
t ExprV Symbol
e)    = let e' :: ExprV Symbol
e' = ConstMap
-> Knowledge -> ICtx -> SEnv Sort -> ExprV Symbol -> ExprV Symbol
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env ExprV Symbol
e in
                                             if Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t then ExprV Symbol
e' else Sort -> Sort -> ExprV Symbol -> ExprV Symbol
forall v. Sort -> Sort -> ExprV v -> ExprV v
ECoerc Sort
s Sort
t ExprV Symbol
e'


--------------------------------------------------------------------------------
-- | Knowledge (SMT Interaction)
--------------------------------------------------------------------------------
data Knowledge = KN
  { Knowledge -> HashMap (Symbol, Symbol) Rewrite
knSims              :: M.HashMap (Symbol, Symbol) Rewrite  -- ^ Rewrite rules came from match and data type definitions
  , Knowledge -> HashMap Symbol (EquationV Symbol)
knAms               :: M.HashMap Symbol Equation  -- ^ All function definitions -- restore ! here?
  , Knowledge -> [(Symbol, Sort)]
knLams              :: ![(Symbol, Sort)]
  , Knowledge -> [(Symbol, Int)]
knSummary           :: ![(Symbol, Int)]     -- ^ summary of functions to be evaluates (knSims and knAsms) with their arity
  , Knowledge -> HashSet Symbol
knDCs               :: !(S.HashSet Symbol)  -- ^ data constructors drawn from Rewrite
  , Knowledge -> HashSet Symbol
knAllDCs            :: !(S.HashSet Symbol)  -- ^
  , Knowledge -> SelectorMap
knSels              :: !SelectorMap
  , Knowledge -> ConstDCMap
knConsts            :: !ConstDCMap
  }

knowledge :: SInfo a -> Knowledge
knowledge :: forall a. SInfo a -> Knowledge
knowledge SInfo a
info = KN
  { knSims :: HashMap (Symbol, Symbol) Rewrite
knSims                     = [((Symbol, Symbol), Rewrite)] -> HashMap (Symbol, Symbol) Rewrite
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([((Symbol, Symbol), Rewrite)] -> HashMap (Symbol, Symbol) Rewrite)
-> [((Symbol, Symbol), Rewrite)]
-> HashMap (Symbol, Symbol) Rewrite
forall a b. (a -> b) -> a -> b
$ (\Rewrite
r -> ((Rewrite -> Symbol
smName Rewrite
r, Rewrite -> Symbol
smDC Rewrite
r), Rewrite
r)) (Rewrite -> ((Symbol, Symbol), Rewrite))
-> [Rewrite] -> [((Symbol, Symbol), Rewrite)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims
  , knAms :: HashMap Symbol (EquationV Symbol)
knAms                      = [(Symbol, EquationV Symbol)] -> HashMap Symbol (EquationV Symbol)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, EquationV Symbol)] -> HashMap Symbol (EquationV Symbol))
-> [(Symbol, EquationV Symbol)]
-> HashMap Symbol (EquationV Symbol)
forall a b. (a -> b) -> a -> b
$ (\EquationV Symbol
a -> (EquationV Symbol -> Symbol
forall v. EquationV v -> Symbol
eqName EquationV Symbol
a, EquationV Symbol
a)) (EquationV Symbol -> (Symbol, EquationV Symbol))
-> [EquationV Symbol] -> [(Symbol, EquationV Symbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [EquationV Symbol]
aenvEqs AxiomEnv
aenv
  , knLams :: [(Symbol, Sort)]
knLams                     = []
  , knSummary :: [(Symbol, Int)]
knSummary                  =    ((\Rewrite
s -> (Rewrite -> Symbol
smName Rewrite
s, Int
1)) (Rewrite -> (Symbol, Int)) -> [Rewrite] -> [(Symbol, Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)
                                 [(Symbol, Int)] -> [(Symbol, Int)] -> [(Symbol, Int)]
forall a. [a] -> [a] -> [a]
++ ((\EquationV Symbol
s -> (EquationV Symbol -> Symbol
forall v. EquationV v -> Symbol
eqName EquationV Symbol
s, [(Symbol, Sort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (EquationV Symbol -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs EquationV Symbol
s))) (EquationV Symbol -> (Symbol, Int))
-> [EquationV Symbol] -> [(Symbol, Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [EquationV Symbol]
aenvEqs AxiomEnv
aenv)
  , knDCs :: HashSet Symbol
knDCs                      = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (Rewrite -> Symbol
smDC (Rewrite -> Symbol) -> [Rewrite] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)  HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Semigroup a => a -> a -> a
<> SInfo a -> HashSet Symbol
forall {c :: * -> *} {a}. GInfo c a -> HashSet Symbol
constNames SInfo a
info
  , knAllDCs :: HashSet Symbol
knAllDCs                   = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol) -> [Symbol] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ Located Symbol -> Symbol
forall a. Located a -> a
val (Located Symbol -> Symbol)
-> (DataCtor -> Located Symbol) -> DataCtor -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> Located Symbol
dcName (DataCtor -> Symbol) -> [DataCtor] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DataDecl -> [DataCtor]) -> [DataDecl] -> [DataCtor]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [DataCtor]
ddCtors (SInfo a -> [DataDecl]
forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
info)
  , knSels :: SelectorMap
knSels                     = [(Symbol, (Symbol, Int))] -> SelectorMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, (Symbol, Int))] -> SelectorMap)
-> [(Symbol, (Symbol, Int))] -> SelectorMap
forall a b. (a -> b) -> a -> b
$ (Rewrite -> Maybe (Symbol, (Symbol, Int)))
-> [Rewrite] -> [(Symbol, (Symbol, Int))]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel  [Rewrite]
sims
  , knConsts :: ConstDCMap
knConsts                   = [(Symbol, (Symbol, ExprV Symbol))] -> ConstDCMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(Symbol, (Symbol, ExprV Symbol))] -> ConstDCMap)
-> [(Symbol, (Symbol, ExprV Symbol))] -> ConstDCMap
forall a b. (a -> b) -> a -> b
$ (Rewrite -> Maybe (Symbol, (Symbol, ExprV Symbol)))
-> [Rewrite] -> [(Symbol, (Symbol, ExprV Symbol))]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Rewrite -> Maybe (Symbol, (Symbol, ExprV Symbol))
makeCons [Rewrite]
sims
  }
  where
    sims :: [Rewrite]
sims = AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv
    aenv :: AxiomEnv
aenv = SInfo a -> AxiomEnv
forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
info

    makeCons :: Rewrite -> Maybe (Symbol, (Symbol, ExprV Symbol))
makeCons Rewrite
rw
      | [Symbol] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (ExprV Symbol -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms (ExprV Symbol -> [Symbol]) -> ExprV Symbol -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Rewrite -> ExprV Symbol
smBody Rewrite
rw)
      = (Symbol, (Symbol, ExprV Symbol))
-> Maybe (Symbol, (Symbol, ExprV Symbol))
forall a. a -> Maybe a
Just (Rewrite -> Symbol
smName Rewrite
rw, (Rewrite -> Symbol
smDC Rewrite
rw, Rewrite -> ExprV Symbol
smBody Rewrite
rw))
      | Bool
otherwise
      = Maybe (Symbol, (Symbol, ExprV Symbol))
forall a. Maybe a
Nothing

    makeSel :: Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel Rewrite
rw
      | EVar Symbol
x <- Rewrite -> ExprV Symbol
smBody Rewrite
rw
      = (Rewrite -> Symbol
smName Rewrite
rw,) ((Symbol, Int) -> (Symbol, (Symbol, Int)))
-> (Int -> (Symbol, Int)) -> Int -> (Symbol, (Symbol, Int))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Rewrite -> Symbol
smDC Rewrite
rw,) (Int -> (Symbol, (Symbol, Int)))
-> Maybe Int -> Maybe (Symbol, (Symbol, Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Symbol -> [Symbol] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
L.elemIndex Symbol
x (Rewrite -> [Symbol]
smArgs Rewrite
rw)
      | Bool
otherwise
      = Maybe (Symbol, (Symbol, Int))
forall a. Maybe a
Nothing

    constNames :: GInfo c a -> HashSet Symbol
constNames GInfo c a
si = ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> (GInfo c a -> [Symbol]) -> GInfo c a -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((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])
-> (GInfo c a -> [(Symbol, Sort)]) -> GInfo c a -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (GInfo c a -> SEnv Sort) -> GInfo c a -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits (GInfo c a -> HashSet Symbol) -> GInfo c a -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ GInfo c a
si) HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
`S.union`
                      ([Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> (GInfo c a -> [Symbol]) -> GInfo c a -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((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])
-> (GInfo c a -> [(Symbol, Sort)]) -> GInfo c a -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEnv Sort -> [(Symbol, Sort)]
forall a. SEnv a -> [(Symbol, a)]
toListSEnv (SEnv Sort -> [(Symbol, Sort)])
-> (GInfo c a -> SEnv Sort) -> GInfo c a -> [(Symbol, Sort)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GInfo c a -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits (GInfo c a -> HashSet Symbol) -> GInfo c a -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ GInfo c a
si)
-- testSymbol (from names)


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

-- (sel_i, D, i), meaning sel_i (D x1 .. xn) = xi,
-- i.e., sel_i selects the ith value for the data constructor D
type SelectorMap = M.HashMap Symbol (Symbol, Int)
type ConstDCMap  = M.HashMap Symbol (Symbol, Expr)

-- ValueMap maps expressions to constants (including data constructors)
type ConstMap = M.HashMap Expr Expr
type LDataCon = Symbol              -- Data Constructors

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

isConstant :: S.HashSet LDataCon -> Expr -> Bool
isConstant :: HashSet Symbol -> ExprV Symbol -> Bool
isConstant HashSet Symbol
dcs ExprV Symbol
e = HashSet Symbol -> Bool
forall a. HashSet a -> Bool
S.null (HashSet Symbol -> HashSet Symbol -> HashSet Symbol
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference (ExprV Symbol -> HashSet Symbol
exprSymbolsSet ExprV Symbol
e) HashSet Symbol
dcs)

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


instance Simplifiable Expr where
  simplify :: Knowledge -> ICtx -> ExprV Symbol -> ExprV Symbol
simplify Knowledge
γ ICtx
ictx ExprV Symbol
exprs = [Char] -> ExprV Symbol -> ExprV Symbol
forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"simplification of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ExprV Symbol -> [Char]
forall a. Show a => a -> [Char]
show ExprV Symbol
exprs) (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall {t}. Eq t => (t -> t) -> t -> t
fix' ((ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall t. Visitable t => (ExprV Symbol -> ExprV Symbol) -> t -> t
Vis.mapExpr ExprV Symbol -> ExprV Symbol
tx) ExprV Symbol
exprs
    where
      fix' :: (t -> t) -> t -> t
fix' t -> t
f t
e = if t
e t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
e' then t
e else (t -> t) -> t -> t
fix' t -> t
f t
e' where e' :: t
e' = t -> t
f t
e
      tx :: ExprV Symbol -> ExprV Symbol
tx ExprV Symbol
e
        | Just ExprV Symbol
e' <- ExprV Symbol -> ConstMap -> Maybe (ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup ExprV Symbol
e (ICtx -> ConstMap
icSimpl ICtx
ictx)
        = ExprV Symbol
e'

      tx (PAtom Brel
rel ExprV Symbol
e1 ExprV Symbol
e2) = Brel -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applyBooleanFolding Brel
rel ExprV Symbol
e1 ExprV Symbol
e2
      tx (EBin Bop
bop ExprV Symbol
e1 ExprV Symbol
e2) = Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applyConstantFolding Bop
bop ExprV Symbol
e1 ExprV Symbol
e2
      tx (ENeg ExprV Symbol
e)         = Bop -> ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applyConstantFolding Bop
Minus (Constant -> ExprV Symbol
forall v. Constant -> ExprV v
ECon (SubcId -> Constant
I SubcId
0)) ExprV Symbol
e
      tx (EApp ExprV Symbol
e1 ExprV Symbol
e2)
        | ExprV Symbol -> Bool
isSetPred ExprV Symbol
e1    = ExprV Symbol -> ExprV Symbol -> ExprV Symbol
applySetFolding ExprV Symbol
e1 ExprV Symbol
e2

      tx (EApp (EVar Symbol
f) ExprV Symbol
a)
        | Just (Symbol
dc, ExprV Symbol
c)  <- Symbol -> ConstDCMap -> Maybe (Symbol, ExprV Symbol)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f (Knowledge -> ConstDCMap
knConsts Knowledge
γ)
        , (EVar Symbol
dc', [ExprV Symbol]
_) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp ExprV Symbol
a
        , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc'
        = ExprV Symbol
c
      tx (EIte ExprV Symbol
b ExprV Symbol
e1 ExprV Symbol
e2)
        | ExprV Symbol -> Bool
forall v. Eq v => ExprV v -> Bool
isTautoPred ExprV Symbol
b  = ExprV Symbol
e1
        | ExprV Symbol -> Bool
forall v. Eq v => ExprV v -> Bool
isContraPred ExprV Symbol
b = ExprV Symbol
e2
      tx (ECst ExprV Symbol
e Sort
s)       = ExprV Symbol -> Sort -> ExprV Symbol
simplifyCasts ExprV Symbol
e Sort
s
      tx (ECoerc Sort
s Sort
t ExprV Symbol
e)
        | Sort
s Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
t = ExprV Symbol
e
      tx (EApp (EVar Symbol
f) ExprV Symbol
a)
        | Just (Symbol
dc, Int
i)  <- Symbol -> SelectorMap -> Maybe (Symbol, Int)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Symbol
f (Knowledge -> SelectorMap
knSels Knowledge
γ)
        , (EVar Symbol
dc', [ExprV Symbol]
es) <- ExprV Symbol -> (ExprV Symbol, [ExprV Symbol])
forall v. ExprV v -> (ExprV v, [ExprV v])
splitEApp ExprV Symbol
a
        , Symbol
dc Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
dc'
        = [ExprV Symbol]
es[ExprV Symbol] -> Int -> ExprV Symbol
forall a. HasCallStack => [a] -> Int -> a
!!Int
i
      tx (PAnd [ExprV Symbol]
exprses)         = [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
forall {v}. Eq v => [ExprV v] -> [ExprV v] -> ExprV v
go [] ([ExprV Symbol] -> [ExprV Symbol]
forall a. [a] -> [a]
reverse [ExprV Symbol]
exprses)
        where
          go :: [ExprV v] -> [ExprV v] -> ExprV v
go []  []     = ExprV v
forall v. ExprV v
PTrue
          go [ExprV v
p] []     = ExprV v
p
          go [ExprV v]
acc []     = [ExprV v] -> ExprV v
forall v. [ExprV v] -> ExprV v
PAnd [ExprV v]
acc
          go [ExprV v]
acc (ExprV v
e:[ExprV v]
es)
            | ExprV v
e ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PTrue = [ExprV v] -> [ExprV v] -> ExprV v
go [ExprV v]
acc [ExprV v]
es
            | ExprV v
e ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PFalse = ExprV v
forall v. ExprV v
PFalse
            | Bool
otherwise = [ExprV v] -> [ExprV v] -> ExprV v
go (ExprV v
eExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
:[ExprV v]
acc) [ExprV v]
es
      tx (POr [ExprV Symbol]
exprses)          = [ExprV Symbol] -> [ExprV Symbol] -> ExprV Symbol
forall {v}. Eq v => [ExprV v] -> [ExprV v] -> ExprV v
go [] ([ExprV Symbol] -> [ExprV Symbol]
forall a. [a] -> [a]
reverse [ExprV Symbol]
exprses)
        where
          go :: [ExprV v] -> [ExprV v] -> ExprV v
go []  []     = ExprV v
forall v. ExprV v
PFalse
          go [ExprV v
p] []     = ExprV v
p
          go [ExprV v]
acc []     = [ExprV v] -> ExprV v
forall v. [ExprV v] -> ExprV v
POr [ExprV v]
acc
          go [ExprV v]
acc (ExprV v
e:[ExprV v]
es)
            | ExprV v
e ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PTrue = ExprV v
forall v. ExprV v
PTrue
            | ExprV v
e ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
forall v. ExprV v
PFalse = [ExprV v] -> [ExprV v] -> ExprV v
go [ExprV v]
acc [ExprV v]
es
            | Bool
otherwise = [ExprV v] -> [ExprV v] -> ExprV v
go (ExprV v
eExprV v -> [ExprV v] -> [ExprV v]
forall a. a -> [a] -> [a]
:[ExprV v]
acc) [ExprV v]
es
      tx (PNot ExprV Symbol
e)
        | ExprV Symbol
e ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PTrue = ExprV Symbol
forall v. ExprV v
PFalse
        | ExprV Symbol
e ExprV Symbol -> ExprV Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV Symbol
forall v. ExprV v
PFalse = ExprV Symbol
forall v. ExprV v
PTrue
        | Bool
otherwise = ExprV Symbol -> ExprV Symbol
forall v. ExprV v -> ExprV v
PNot ExprV Symbol
e
      tx ExprV Symbol
e = ExprV Symbol
e

simplifyCasts :: Expr -> Sort -> Expr
simplifyCasts :: ExprV Symbol -> Sort -> ExprV Symbol
simplifyCasts (ECon (I SubcId
n)) Sort
FInt  = Constant -> ExprV Symbol
forall v. Constant -> ExprV v
ECon (SubcId -> Constant
I SubcId
n)
simplifyCasts (ECon (R Double
x)) Sort
FReal = Constant -> ExprV Symbol
forall v. Constant -> ExprV v
ECon (Double -> Constant
R Double
x)
simplifyCasts ExprV Symbol
e            Sort
s     = ExprV Symbol -> Sort -> ExprV Symbol
forall v. ExprV v -> Sort -> ExprV v
ECst ExprV Symbol
e Sort
s

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

class Normalizable a where
  normalize :: a -> a

instance Normalizable (GInfo c a) where
  normalize :: GInfo c a -> GInfo c a
normalize GInfo c a
si = GInfo c a
si {ae = normalize $ ae si}

instance Normalizable AxiomEnv where
  normalize :: AxiomEnv -> AxiomEnv
normalize AxiomEnv
aenv = AxiomEnv
aenv { aenvEqs   = {-notracepp-} mytracepp "aenvEqs"   (normalize <$> aenvEqs   aenv)
                        , aenvSimpl = {-notracepp-} mytracepp "aenvSimpl" (normalize <$> aenvSimpl aenv) }

instance Normalizable Rewrite where
  normalize :: Rewrite -> Rewrite
normalize Rewrite
rw = Rewrite
rw { smArgs = xs', smBody = normalizeBody (smName rw) $ subst su $ smBody rw }
    where
      su :: Subst
su  = [(Symbol, ExprV Symbol)] -> Subst
mkSubst ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> (Symbol, ExprV Symbol))
-> [Symbol] -> [Symbol] -> [(Symbol, ExprV Symbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      xs :: [Symbol]
xs  = Rewrite -> [Symbol]
smArgs Rewrite
rw
      xs' :: [Symbol]
xs' = (Symbol -> SubcId -> Symbol) -> [Symbol] -> [SubcId] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> SubcId -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
mkSymbol [Symbol]
xs [SubcId
0 :: Integer ..]
      mkSymbol :: Symbol -> a -> Symbol
mkSymbol Symbol
x a
i = Symbol
x Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol -> a -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (Rewrite -> Symbol
smName Rewrite
rw) a
i

instance Normalizable Equation where
  normalize :: EquationV Symbol -> EquationV Symbol
normalize EquationV Symbol
eq = EquationV Symbol
eq {eqArgs = zip xs' ss,
                     eqBody = normalizeBody (eqName eq) $ subst su $ eqBody eq }
    where
      su :: Subst
su           = [(Symbol, ExprV Symbol)] -> Subst
mkSubst ([(Symbol, ExprV Symbol)] -> Subst)
-> [(Symbol, ExprV Symbol)] -> Subst
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> (Symbol, ExprV Symbol))
-> [Symbol] -> [Symbol] -> [(Symbol, ExprV Symbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> ExprV Symbol
forall v. v -> ExprV v
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      ([Symbol]
xs,[Sort]
ss)      = [(Symbol, Sort)] -> ([Symbol], [Sort])
forall a b. [(a, b)] -> ([a], [b])
unzip (EquationV Symbol -> [(Symbol, Sort)]
forall v. EquationV v -> [(Symbol, Sort)]
eqArgs EquationV Symbol
eq)
      xs' :: [Symbol]
xs'          = (Symbol -> SubcId -> Symbol) -> [Symbol] -> [SubcId] -> [Symbol]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Symbol -> SubcId -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
mkSymbol [Symbol]
xs [SubcId
0 :: Integer ..]
      mkSymbol :: Symbol -> a -> Symbol
mkSymbol Symbol
x a
i = Symbol
x Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol -> a -> Symbol
forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (EquationV Symbol -> Symbol
forall v. EquationV v -> Symbol
eqName EquationV Symbol
eq) a
i

normalizeBody :: Symbol -> Expr -> Expr
normalizeBody :: Symbol -> ExprV Symbol -> ExprV Symbol
normalizeBody Symbol
f = ExprV Symbol -> ExprV Symbol
forall {v}. (Subable (ExprV v), Eq v) => ExprV v -> ExprV v
go
  where
    go :: ExprV v -> ExprV v
go ExprV v
e
      | Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Symbol
f (ExprV v -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms ExprV v
e)
      = ExprV v -> ExprV v
forall {v}. Eq v => ExprV v -> ExprV v
go' ExprV v
e
    go ExprV v
e
      = ExprV v
e

    go' :: ExprV v -> ExprV v
go' (PAnd [PImp ExprV v
c ExprV v
e1,PImp (PNot ExprV v
c') ExprV v
e2])
      | ExprV v
c ExprV v -> ExprV v -> Bool
forall a. Eq a => a -> a -> Bool
== ExprV v
c' = ExprV v -> ExprV v -> ExprV v -> ExprV v
forall v. ExprV v -> ExprV v -> ExprV v -> ExprV v
EIte ExprV v
c ExprV v
e1 (ExprV v -> ExprV v
go' ExprV v
e2)
    go' ExprV v
e = ExprV v
e