--------------------------------------------------------------------------------
-- | 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 FlexibleInstances         #-}
{-# LANGUAGE PatternGuards             #-}
{-# LANGUAGE RecordWildCards           #-}
{-# LANGUAGE ExistentialQuantification #-}

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

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.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 = 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 = forall k v. (k -> v -> Bool) -> HashMap k v -> HashMap k v
M.filterWithKey
               (\SubcId
i SimpC a
c -> forall a. AxiomEnv -> SubcId -> SimpC a -> Bool
isPleCstr AxiomEnv
aEnv SubcId
i SimpC a
c Bool -> Bool -> Bool
&& forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SubcId
i forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`L.elem`) Maybe [SubcId]
subcIds)
               (forall (c :: * -> *) a. GInfo c a -> HashMap SubcId (c a)
cm SInfo a
fi)
    let t :: CTrie
t  = forall a. [(SubcId, SimpC a)] -> CTrie
mkCTrie (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SubcId (SimpC a)
cs)                      -- 1. BUILD the Trie
    InstRes
res   <- forall a. Int -> IO a -> IO a
withProgress (Int
1 forall a. Num a => a -> a -> a
+ forall k v. HashMap k v -> Int
M.size HashMap SubcId (SimpC a)
cs) forall a b. (a -> b) -> a -> b
$
               forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t forall a b. (a -> b) -> a -> b
$ forall a. Loc a => SInfo a -> CMap (SimpC a) -> SymEnv -> InstEnv a
instEnv SInfo a
fi HashMap SubcId (SimpC a)
cs SymEnv
sEnv           -- 2. TRAVERSE Trie to compute InstRes
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Config -> SymEnv -> SInfo a -> InstRes -> SInfo a
resSInfo Config
cfg SymEnv
sEnv SInfo a
fi InstRes
res                   -- 3. STRENGTHEN SInfo using InstRes
  where
    sEnv :: SymEnv
sEnv   = forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
fi
    aEnv :: AxiomEnv
aEnv   = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
    fi :: SInfo a
fi     = 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
fi CMap (SimpC a)
cs SymEnv
sEnv = 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           = 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 (forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv SimpC a
c)) IBindEnv
emptyIBindEnv CMap (SimpC a)
cs
    bEnv :: BindEnv a
bEnv              = forall a.
(Int -> Symbol -> SortedReft -> Bool) -> BindEnv a -> BindEnv a
filterBindEnv (\Int
i Symbol
_ SortedReft
_ -> Int -> IBindEnv -> Bool
memberIBindEnv Int
i IBindEnv
csBinds) (forall (c :: * -> *) a. GInfo c a -> BindEnv a
bs SInfo a
fi)
    aEnv :: AxiomEnv
aEnv              = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
fi
    γ :: Knowledge
γ                 = forall a. SInfo a -> Knowledge
knowledge SInfo a
fi
    s0 :: EvalEnv
s0                = SymEnv -> EvAccum -> EvalEnv
EvalEnv SymEnv
sEnv 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  = forall a. [(Path, a)] -> Trie a
T.fromList [ (SimpC a -> Path
cBinds SimpC a
c, SubcId
i) | (SubcId
i, SimpC a
c) <- [(SubcId, SimpC a)]
ics ]
  where
    cBinds :: SimpC a -> Path
cBinds   = forall a. Ord a => [a] -> [a]
L.sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. IBindEnv -> Path
elemsIBindEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> IBindEnv
senv

----------------------------------------------------------------------------------------------
-- | Step 2: @pleTrie@ walks over the @CTrie@ to actually do the incremental-PLE
pleTrie :: CTrie -> InstEnv a -> IO InstRes
pleTrie :: forall a. CTrie -> InstEnv a -> IO InstRes
pleTrie CTrie
t InstEnv a
env = forall a.
InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx0 forall {a}. [a]
diff0 forall a. Maybe a
Nothing forall {k} {v}. HashMap k v
res0 CTrie
t
  where
    diff0 :: [a]
diff0        = []
    res0 :: HashMap k v
res0         = forall {k} {v}. HashMap k v
M.empty
    ctx0 :: ICtx
ctx0         = forall a. InstEnv a -> [(Expr, Expr)] -> ICtx
initCtx InstEnv a
env ((Equation -> (Expr, Expr)
mkEq forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Equation]
es0) forall a. [a] -> [a] -> [a]
++ (Rewrite -> (Expr, Expr)
mkEq' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
es0'))
    es0 :: [Equation]
es0          = forall a. (a -> Bool) -> [a] -> [a]
L.filter (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Equation -> [(Symbol, Sort)]
eqArgs) (AxiomEnv -> [Equation]
aenvEqs   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. InstEnv a -> AxiomEnv
ieAenv forall a b. (a -> b) -> a -> b
$ InstEnv a
env)
    es0' :: [Rewrite]
es0'         = forall a. (a -> Bool) -> [a] -> [a]
L.filter (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewrite -> [Symbol]
smArgs) (AxiomEnv -> [Rewrite]
aenvSimpl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. InstEnv a -> AxiomEnv
ieAenv forall a b. (a -> b) -> a -> b
$ InstEnv a
env)
    mkEq :: Equation -> (Expr, Expr)
mkEq  Equation
eq     = (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ Equation -> Symbol
eqName Equation
eq, Equation -> Expr
eqBody Equation
eq)
    mkEq' :: Rewrite -> (Expr, Expr)
mkEq' Rewrite
rw     = (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smDC Rewrite
rw), Rewrite -> Expr
smBody Rewrite
rw)

loopT :: InstEnv a -> ICtx -> Diff -> Maybe BindId -> InstRes -> CTrie -> IO InstRes
loopT :: forall a.
InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx Path
delta Maybe Int
i InstRes
res CTrie
t = case CTrie
t of
  T.Node []  -> forall (m :: * -> *) a. Monad m => a -> m a
return InstRes
res
  T.Node [Branch SubcId
b] -> forall a.
InstEnv a
-> ICtx
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx Path
delta Maybe Int
i InstRes
res Branch SubcId
b
  T.Node [Branch SubcId]
bs  -> forall a b.
InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx Path
delta forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do
                  (ICtx
ctx'', InstRes
res') <- forall a.
InstEnv a -> ICtx -> Maybe Int -> InstRes -> IO (ICtx, InstRes)
ple1 InstEnv a
env ICtx
ctx' Maybe Int
i InstRes
res
                  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (forall a.
InstEnv a
-> ICtx
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx'' [] Maybe Int
i) InstRes
res' [Branch SubcId]
bs

loopB :: InstEnv a -> ICtx -> Diff -> Maybe BindId -> InstRes -> CBranch -> IO InstRes
loopB :: forall a.
InstEnv a
-> ICtx
-> Path
-> Maybe Int
-> InstRes
-> Branch SubcId
-> IO InstRes
loopB InstEnv a
env ICtx
ctx Path
delta Maybe Int
iMb InstRes
res Branch SubcId
b = case Branch SubcId
b of
  T.Bind Int
i CTrie
t -> forall a.
InstEnv a
-> ICtx -> Path -> Maybe Int -> InstRes -> CTrie -> IO InstRes
loopT InstEnv a
env ICtx
ctx (Int
iforall a. a -> [a] -> [a]
:Path
delta) (forall a. a -> Maybe a
Just Int
i) InstRes
res CTrie
t
  T.Val SubcId
cid  -> forall a b.
InstEnv a -> ICtx -> Path -> Maybe SubcId -> (ICtx -> IO b) -> IO b
withAssms InstEnv a
env ICtx
ctx Path
delta (forall a. a -> Maybe a
Just SubcId
cid) forall a b. (a -> b) -> a -> b
$ \ICtx
ctx' -> do
                  IO ()
progressTick
                  forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
InstEnv a -> ICtx -> Maybe Int -> 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 forall a b. (a -> b) -> a -> b
$
  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
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieAenv :: forall a. InstEnv a -> AxiomEnv
..} ICtx
ctx Maybe Int
i InstRes
res =
  InstRes -> Maybe Int -> ICtx -> (ICtx, InstRes)
updCtxRes InstRes
res Maybe Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ConstMap -> ICtx -> Knowledge -> EvalEnv -> IO ICtx
evalCandsLoop {-anfEnv-} 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 :: [[(Expr, Expr)]]
rws = [Expr -> Rewrite -> [(Expr, Expr)]
rewrite Expr
e Rewrite
rw | Rewrite
rw <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. HashMap k v -> [(k, v)]
M.toList (Knowledge -> HashMap (Symbol, Symbol) Rewrite
knSims Knowledge
γ)
                            ,  Expr
e <- forall a. HashSet a -> [a]
S.toList (forall a b. (a, b) -> b
snd forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
exprs)]
      in
        EvAccum
exprs forall a. Semigroup a => a -> a -> a
<> forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Expr, Expr)]]
rws)
    go :: ICtx -> IO ICtx
go ICtx
ictx | forall a. HashSet a -> Bool
S.null (ICtx -> HashSet Expr
icCands ICtx
ictx) = forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
    go ICtx
ictx =  do let cands :: HashSet Expr
cands = ICtx -> HashSet Expr
icCands ICtx
ictx
                  let env' :: EvalEnv
env' = EvalEnv
env { evAccum :: EvAccum
evAccum = ICtx -> EvAccum
icEquals ICtx
ictx forall a. Semigroup a => a -> a -> a
<> EvalEnv -> EvAccum
evAccum EvalEnv
env }
                  (ICtx
ictx', [EvAccum]
evalResults)  <-
                               forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (ConstMap
-> Knowledge
-> EvalEnv
-> (ICtx, [EvAccum])
-> Expr
-> IO (ICtx, [EvAccum])
evalOneCandStep ConstMap
ie Knowledge
γ EvalEnv
env') (ICtx
ictx, []) (forall a. HashSet a -> [a]
S.toList HashSet Expr
cands)
                  let us :: EvAccum
us = forall a. Monoid a => [a] -> a
mconcat [EvAccum]
evalResults
                  if forall a. HashSet a -> Bool
S.null (EvAccum
us forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.difference` ICtx -> EvAccum
icEquals ICtx
ictx)
                        then forall (m :: * -> *) a. Monad m => a -> m a
return ICtx
ictx
                        else do  let oks :: HashSet Expr
oks      = forall a b. (a, b) -> a
fst 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 :: HashSet Expr
icSolved = ICtx -> HashSet Expr
icSolved ICtx
ictx forall a. Semigroup a => a -> a -> a
<> HashSet Expr
oks
                                                      , icEquals :: EvAccum
icEquals = ICtx -> EvAccum
icEquals ICtx
ictx forall a. Semigroup a => a -> a -> a
<> EvAccum
us' }
                                 let newcands :: [Expr]
newcands = forall a. Monoid a => [a] -> a
mconcat (Knowledge -> ICtx -> Expr -> [Expr]
makeCandidates Knowledge
γ ICtx
ictx'' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList (HashSet Expr
cands forall a. Semigroup a => a -> a -> a
<> (forall a b. (a, b) -> b
snd forall b a.
(Hashable b, Eq b) =>
(a -> b) -> HashSet a -> HashSet b
`S.map` EvAccum
us)))
                                 ICtx -> IO ICtx
go (ICtx
ictx'' { icCands :: HashSet Expr
icCands = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Expr]
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])
-> Expr
-> IO (ICtx, [EvAccum])
evalOneCandStep ConstMap
env Knowledge
γ EvalEnv
env' (ICtx
ictx, [EvAccum]
acc) Expr
e = do
  EvAccum
res <- ConstMap -> Knowledge -> EvalEnv -> ICtx -> Expr -> IO EvAccum
evalOne ConstMap
env Knowledge
γ EvalEnv
env' ICtx
ictx Expr
e
  forall (m :: * -> *) a. Monad m => a -> m a
return (ICtx
ictx, EvAccum
res forall a. a -> [a] -> [a]
: [EvAccum]
acc)

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

rewriteTop :: Expr -> Rewrite -> Maybe (Expr,Expr)
rewriteTop :: Expr -> Rewrite -> Maybe (Expr, Expr)
rewriteTop Expr
e Rewrite
rw
  | (EVar Symbol
f, [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
e
  , Symbol
f forall a. Eq a => a -> a -> Bool
== Rewrite -> Symbol
smDC Rewrite
rw
  , forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (Rewrite -> [Symbol]
smArgs Rewrite
rw)
  = forall a. a -> Maybe a
Just (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar forall a b. (a -> b) -> a -> b
$ Rewrite -> Symbol
smName Rewrite
rw) Expr
e, forall a. Subable a => Subst -> a -> a
subst ([(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (Rewrite -> [Symbol]
smArgs Rewrite
rw) [Expr]
es) (Rewrite -> Expr
smBody Rewrite
rw))
  | Bool
otherwise
  = 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
fi InstRes
res = forall a. SInfo a -> InstRes -> SInfo a
strengthenBinds SInfo a
fi InstRes
res'
  where
    res' :: InstRes
res'     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip Path
is [Expr]
ps''
    ps'' :: [Expr]
ps''     = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Int
i -> forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate (forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan ([Char]
"PLE1 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i)) SymEnv
env) Path
is [Expr]
ps'
    ps' :: [Expr]
ps'      = forall a. Defunc a => Config -> SymEnv -> a -> a
defuncAny Config
cfg SymEnv
env [Expr]
ps
    (Path
is, [Expr]
ps) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall k v. HashMap k v -> [(k, v)]
M.toList InstRes
res)

----------------------------------------------------------------------------------------------
-- | @InstEnv@ has the global information needed to do PLE
----------------------------------------------------------------------------------------------

data InstEnv a = InstEnv
  { forall a. InstEnv a -> 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 Expr
icCands    :: S.HashSet Expr            -- ^ "Candidates" for unfolding
  , ICtx -> EvAccum
icEquals   :: EvAccum                   -- ^ Accumulated equalities
  , ICtx -> HashSet Expr
icSolved   :: S.HashSet Expr            -- ^ Terms that we have already expanded
  , ICtx -> ConstMap
icSimpl    :: !ConstMap                 -- ^ Map of expressions to constants
  , ICtx -> Maybe SubcId
icSubcId   :: Maybe SubcId              -- ^ Current subconstraint ID
  }

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

type InstRes = M.HashMap BindId Expr

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

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

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

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

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


updRes :: InstRes -> Maybe BindId -> Expr -> InstRes
updRes :: InstRes -> Maybe Int -> Expr -> InstRes
updRes InstRes
res (Just Int
i) Expr
e = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith (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 Expr
e InstRes
res
updRes InstRes
res  Maybe Int
Nothing Expr
_ = InstRes
res


----------------------------------------------------------------------------------------------
-- | @updCtx env ctx delta cidMb@ adds the assumptions and candidates from @delta@ and @cidMb@
--   to the context.
----------------------------------------------------------------------------------------------

updCtx :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> ICtx
updCtx :: forall a. InstEnv a -> ICtx -> Path -> Maybe SubcId -> ICtx
updCtx InstEnv{CMap (SimpC a)
BindEnv a
AxiomEnv
Knowledge
EvalEnv
ieEvEnv :: EvalEnv
ieKnowl :: Knowledge
ieCstrs :: CMap (SimpC a)
ieAenv :: AxiomEnv
ieBEnv :: BindEnv a
ieEvEnv :: forall a. InstEnv a -> EvalEnv
ieKnowl :: forall a. InstEnv a -> Knowledge
ieCstrs :: forall a. InstEnv a -> CMap (SimpC a)
ieBEnv :: forall a. InstEnv a -> BindEnv a
ieAenv :: forall a. InstEnv a -> AxiomEnv
..} ICtx
ctx Path
delta Maybe SubcId
cidMb
    = ICtx
ctx { icCands :: HashSet Expr
icCands  = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Expr]
cands           forall a. Semigroup a => a -> a -> a
<> ICtx -> HashSet Expr
icCands  ICtx
ctx
          , icEquals :: EvAccum
icEquals = EvAccum
initEqs                    forall a. Semigroup a => a -> a -> a
<> ICtx -> EvAccum
icEquals ICtx
ctx
          , icSimpl :: ConstMap
icSimpl  = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (forall a. HashSet a -> [a]
S.toList EvAccum
sims) forall a. Semigroup a => a -> a -> a
<> ICtx -> ConstMap
icSimpl ICtx
ctx forall a. Semigroup a => a -> a -> a
<> ConstMap
econsts
          , icSubcId :: Maybe SubcId
icSubcId = Maybe SubcId
cidMb -- fst <$> L.find (\(_, b) -> (head delta) `memberIBindEnv` (_cenv b)) ieCstrs
          }                  -- eliminate above if nothing broken
  where
    initEqs :: EvAccum
initEqs   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Expr -> Rewrite -> [(Expr, Expr)]
rewrite Expr
e Rewrite
rw | Expr
e  <- [Expr]
cands forall a. [a] -> [a] -> [a]
++ (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList (ICtx -> EvAccum
icEquals ICtx
ctx))
                                                  , Rewrite
rw <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. HashMap k v -> [(k, v)]
M.toList (Knowledge -> HashMap (Symbol, Symbol) Rewrite
knSims Knowledge
ieKnowl)]
    cands :: [Expr]
cands     = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Knowledge -> ICtx -> Expr -> [Expr]
makeCandidates Knowledge
ieKnowl ICtx
ctx) (Expr
rhsforall a. a -> [a] -> [a]
:[Expr]
es)
    sims :: EvAccum
sims      = forall a. (a -> Bool) -> HashSet a -> HashSet a
S.filter (HashSet Symbol -> (Expr, Expr) -> Bool
isSimplification (Knowledge -> HashSet Symbol
knDCs Knowledge
ieKnowl)) (EvAccum
initEqs forall a. Semigroup a => a -> a -> a
<> ICtx -> EvAccum
icEquals ICtx
ctx)
    econsts :: ConstMap
econsts   = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ Knowledge -> [Expr] -> [(Expr, Expr)]
findConstants Knowledge
ieKnowl [Expr]
es
    rhs :: Expr
rhs       = Expr -> Expr
unElab Expr
eRhs
    es :: [Expr]
es        = Expr -> Expr
unElab forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Expression a => a -> Expr
expr 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 :: Expr
eRhs      = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expr
PTrue forall (c :: * -> *) a. TaggedC c a => c a -> Expr
crhs Maybe (SimpC a)
subMb
    binds :: [(Symbol, SortedReft, a)]
binds     = [ forall a. Int -> BindEnv a -> (Symbol, SortedReft, a)
lookupBindEnv Int
i BindEnv a
ieBEnv | Int
i <- Path
delta ]
    subMb :: Maybe (SimpC a)
subMb     = forall a. HashMap SubcId (SimpC a) -> SubcId -> SimpC a
getCstr CMap (SimpC a)
ieCstrs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SubcId
cidMb


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

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

    -- 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 -> Expr -> Bool
hasConstructors Knowledge
γ Expr
e =  Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall a. HashSet a -> Bool
S.null forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.intersection (Expr -> HashSet Symbol
exprSymbolsSet Expr
e) (Knowledge -> HashSet Symbol
knDCs Knowledge
γ)

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


isGoodApp :: Knowledge -> Expr -> Bool
isGoodApp :: Knowledge -> Expr -> Bool
isGoodApp Knowledge
γ Expr
e
  | (EVar Symbol
f, [Expr]
es) <- Expr -> (Expr, [Expr])
splitEApp Expr
e
  , Just Int
i       <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
L.lookup Symbol
f (Knowledge -> [(Symbol, Int)]
knSummary Knowledge
γ)
  = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
es 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 = 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
sid SimpC a
c = forall (c :: * -> *) a. TaggedC c a => c a -> Bool
isTarget SimpC a
c Bool -> Bool -> Bool
&& forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Bool
False SubcId
sid (AxiomEnv -> HashMap SubcId Bool
aenvExpand AxiomEnv
aenv)

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

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

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

fastEval :: ConstMap -> Knowledge -> ICtx -> Expr -> EvalST Expr
fastEval :: ConstMap -> Knowledge -> ICtx -> Expr -> EvalST Expr
fastEval ConstMap
ienv Knowledge
γ ICtx
ctx Expr
e
    = do SEnv Sort
env  <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SymEnv -> SEnv Sort
seSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalEnv -> SymEnv
evEnv)
         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => [Char] -> a -> a
mytracepp ([Char]
"evaluating" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Expr
e) forall a b. (a -> b) -> a -> b
$ ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret ConstMap
ienv Knowledge
γ ICtx
ctx SEnv Sort
env forall a b. (a -> b) -> a -> b
$ forall a. Simplifiable a => Knowledge -> ICtx -> a -> a
simplify Knowledge
γ ICtx
ctx Expr
e

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

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

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

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

mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub
mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> CoSub
mkCoSub SEnv Sort
env [Sort]
eTs [Sort]
xTs = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x, [Sort] -> Sort
unite [Sort]
ys) | (Symbol
x, [Sort]
ys) <- forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, Sort)]
xys ]
  where
    unite :: [Sort] -> Sort
unite [Sort]
ts    = forall a. a -> Maybe a -> a
Mb.fromMaybe (forall {a} {a}. PPrint a => a -> a
uError [Sort]
ts) (Env -> [Sort] -> Maybe Sort
unifyTo1 Env
senv [Sort]
ts)
    senv :: Env
senv        = forall a. SEnv a -> Symbol -> SESearch a
mkSearchEnv SEnv Sort
env
    uError :: a -> a
uError a
ts   = forall a. [Char] -> a
panic ([Char]
"mkCoSub: cannot build CoSub for " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp [(Symbol, Sort)]
xys forall a. [a] -> [a] -> [a]
++ [Char]
" cannot unify " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp a
ts)
    xys :: [(Symbol, Sort)]
xys         = forall a. Ord a => [a] -> [a]
Misc.sortNub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Sort -> Sort -> [(Symbol, Sort)]
matchSorts [Sort]
_xTs [Sort]
_eTs
    ([Sort]
_xTs,[Sort]
_eTs) = ([Sort]
xTs, [Sort]
eTs)

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

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

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

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

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

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

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

      interpretApp ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   Expr
f        [Expr]
es     = {-simplify γ ctx $-} Expr -> [Expr] -> Expr
eApps Expr
f [Expr]
es
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ENeg Expr
e1)      = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1 in
                                            Bop -> Expr -> Expr -> Expr
applyConstantFolding Bop
Minus (Constant -> Expr
ECon (SubcId -> Constant
I SubcId
0)) Expr
e1'
--                                          simplify γ ctx (ENeg e1')
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (EBin Bop
o Expr
e1 Expr
e2) = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1
                                              e2' :: Expr
e2' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e2 in
                                            Bop -> Expr -> Expr -> Expr
applyConstantFolding Bop
o Expr
e1' Expr
e2'
--                                          simplify γ ctx (EBin o e1' e2')
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (EIte Expr
g Expr
e1 Expr
e2) = let b :: Expr
b = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
g in
                                            if Expr
b forall a. Eq a => a -> a -> Bool
== Expr
PTrue then ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1 else
                                              if Expr
b forall a. Eq a => a -> a -> Bool
== Expr
PFalse then ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e2 else
                                                forall a. Simplifiable a => Knowledge -> ICtx -> a -> a
simplify Knowledge
γ ICtx
ctx forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr -> Expr
EIte Expr
b Expr
e1 Expr
e2
--                                          EIte b (interpret' γ ctx env e1) (interpret' γ ctx env e2)
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ECst Expr
e1 Sort
s)    = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1 in
                                            Expr -> Sort -> Expr
simplifyCasts Expr
e1' Sort
s -- ECst e1' s
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (ELam (Symbol
x,Sort
s) Expr
e)   = let γ' :: Knowledge
γ' = Knowledge
γ { knLams :: [(Symbol, Sort)]
knLams = (Symbol
x, Sort
s) forall a. a -> [a] -> [a]
: Knowledge -> [(Symbol, Sort)]
knLams Knowledge
γ }
                                              e' :: Expr
e' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ' ICtx
ctx SEnv Sort
env Expr
e in
                                            (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
s) Expr
e'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ETApp Expr
e1 Sort
t)   = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1 in Expr -> Sort -> Expr
ETApp Expr
e1' Sort
t
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (ETAbs Expr
e1 Symbol
sy)  = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1 in Expr -> Symbol -> Expr
ETAbs Expr
e1' Symbol
sy
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env   (PAnd [Expr]
es)      = let es' :: [Expr]
es' = forall a b. (a -> b) -> [a] -> [b]
map (ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env) [Expr]
es in [Expr] -> [Expr] -> Expr
go [] (forall a. [a] -> [a]
reverse [Expr]
es')
  where
    go :: [Expr] -> [Expr] -> Expr
go []  []         = Expr
PTrue
    go [Expr
p] []         = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
p
    go [Expr]
acc []         = [Expr] -> Expr
PAnd [Expr]
acc
    go [Expr]
acc (Expr
PTrue:[Expr]
es) = [Expr] -> [Expr] -> Expr
go [Expr]
acc [Expr]
es
    go [Expr]
_   (Expr
PFalse:[Expr]
_) = Expr
PFalse
    go [Expr]
acc (Expr
e:[Expr]
es)     = [Expr] -> [Expr] -> Expr
go (Expr
eforall a. a -> [a] -> [a]
:[Expr]
acc) [Expr]
es
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (POr [Expr]
es)         = let es' :: [Expr]
es' = forall a b. (a -> b) -> [a] -> [b]
map (ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env) [Expr]
es in [Expr] -> [Expr] -> Expr
go [] (forall a. [a] -> [a]
reverse [Expr]
es')
  where
    go :: [Expr] -> [Expr] -> Expr
go []  []          = Expr
PFalse
    go [Expr
p] []          = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
p
    go [Expr]
acc []          = [Expr] -> Expr
POr [Expr]
acc
    go [Expr]
_   (Expr
PTrue:[Expr]
_)   = Expr
PTrue
    go [Expr]
acc (Expr
PFalse:[Expr]
es) = [Expr] -> [Expr] -> Expr
go [Expr]
acc [Expr]
es
    go [Expr]
acc (Expr
e:[Expr]
es)      = [Expr] -> [Expr] -> Expr
go (Expr
eforall a. a -> [a] -> [a]
:[Expr]
acc) [Expr]
es
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PNot Expr
e)         = let e' :: Expr
e' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e in case Expr
e' of
    (PNot Expr
e'')    -> Expr
e''
    Expr
PTrue         -> Expr
PFalse
    Expr
PFalse        -> Expr
PTrue
    Expr
_             -> Expr -> Expr
PNot Expr
e'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PImp Expr
e1 Expr
e2)     = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1
                                              e2' :: Expr
e2' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e2 in
                                            if Expr
e1' forall a. Eq a => a -> a -> Bool
== Expr
PFalse Bool -> Bool -> Bool
|| Expr
e2' forall a. Eq a => a -> a -> Bool
== Expr
PTrue then Expr
PTrue else
                                              if Expr
e1' forall a. Eq a => a -> a -> Bool
== Expr
PTrue then Expr
e2' else
                                                if Expr
e2' forall a. Eq a => a -> a -> Bool
== Expr
PFalse then ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (Expr -> Expr
PNot Expr
e1') else
                                                  Expr -> Expr -> Expr
PImp Expr
e1' Expr
e2'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PIff Expr
e1 Expr
e2)     = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1
                                              e2' :: Expr
e2' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e2 in
                                            if Expr
e1' forall a. Eq a => a -> a -> Bool
== Expr
PTrue then Expr
e2' else
                                              if Expr
e2' forall a. Eq a => a -> a -> Bool
== Expr
PTrue then Expr
e1' else
                                                if Expr
e1' forall a. Eq a => a -> a -> Bool
== Expr
PFalse then ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (Expr -> Expr
PNot Expr
e2') else
                                                  if Expr
e2' forall a. Eq a => a -> a -> Bool
== Expr
PFalse then ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (Expr -> Expr
PNot Expr
e1') else
                                                    Expr -> Expr -> Expr
PIff Expr
e1' Expr
e2'
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (PAtom Brel
o Expr
e1 Expr
e2)  = let e1' :: Expr
e1' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1
                                              e2' :: Expr
e2' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e2 in
                                            Brel -> Expr -> Expr -> Expr
applyBooleanFolding Brel
o Expr
e1' Expr
e2'
interpret ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   e :: Expr
e@(PKVar KVar
_ Subst
_)    = Expr
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env e :: Expr
e@(PAll [(Symbol, Sort)]
xss Expr
e1)  = case [(Symbol, Sort)]
xss of
  [] -> ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1
  [(Symbol, Sort)]
_  -> Expr
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env e :: Expr
e@(PExist [(Symbol, Sort)]
xss Expr
e1) = case [(Symbol, Sort)]
xss of
  [] -> ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e1
  [(Symbol, Sort)]
_  -> Expr
e
interpret ConstMap
_  Knowledge
_ ICtx
_   SEnv Sort
_   e :: Expr
e@PGrad{}         = Expr
e
interpret ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env (ECoerc Sort
s Sort
t Expr
e)    = let e' :: Expr
e' = ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr
interpret' ConstMap
ie Knowledge
γ ICtx
ctx SEnv Sort
env Expr
e in
                                             if Sort
s forall a. Eq a => a -> a -> Bool
== Sort
t then Expr
e' else Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t Expr
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 Equation
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
si = KN
  { knSims :: HashMap (Symbol, Symbol) Rewrite
knSims                     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ (\Rewrite
r -> ((Rewrite -> Symbol
smName Rewrite
r, Rewrite -> Symbol
smDC Rewrite
r), Rewrite
r)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims
  , knAms :: HashMap Symbol Equation
knAms                      = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ (\Equation
a -> (Equation -> Symbol
eqName Equation
a, Equation
a)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Equation]
aenvEqs AxiomEnv
aenv
  , knLams :: [(Symbol, Sort)]
knLams                     = []
  , knSummary :: [(Symbol, Int)]
knSummary                  =    ((\Rewrite
s -> (Rewrite -> Symbol
smName Rewrite
s, Int
1)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)
                                 forall a. [a] -> [a] -> [a]
++ ((\Equation
s -> (Equation -> Symbol
eqName Equation
s, forall (t :: * -> *) a. Foldable t => t a -> Int
length (Equation -> [(Symbol, Sort)]
eqArgs Equation
s))) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Equation]
aenvEqs AxiomEnv
aenv)
  , knDCs :: HashSet Symbol
knDCs                      = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (Rewrite -> Symbol
smDC forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Rewrite]
sims)  forall a. Semigroup a => a -> a -> a
<> forall {c :: * -> *} {a}. GInfo c a -> HashSet Symbol
constNames SInfo a
si
  , knAllDCs :: HashSet Symbol
knAllDCs                   = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> LocSymbol
dcName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataDecl -> [DataCtor]
ddCtors (forall (c :: * -> *) a. GInfo c a -> [DataDecl]
ddecls SInfo a
si)
  , knSels :: SelectorMap
knSels                     = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Rewrite -> Maybe (Symbol, (Symbol, Int))
makeSel  [Rewrite]
sims
  , knConsts :: ConstDCMap
knConsts                   = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Rewrite -> Maybe (Symbol, (Symbol, Expr))
makeCons [Rewrite]
sims
  }
  where
    sims :: [Rewrite]
sims = AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv
    aenv :: AxiomEnv
aenv = forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae SInfo a
si

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

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

    constNames :: GInfo c a -> HashSet Symbol
constNames GInfo c a
si = (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits forall a b. (a -> b) -> a -> b
$ GInfo c a
si) forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.union`
                      (forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SEnv a -> [(Symbol, a)]
toListSEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits 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 -> (Expr, Expr) -> Bool
isSimplification HashSet Symbol
dcs (Expr
_,Expr
c) = HashSet Symbol -> Expr -> Bool
isConstant HashSet Symbol
dcs Expr
c

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

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


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

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

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

simplifyCasts :: Expr -> Sort -> Expr
simplifyCasts :: Expr -> Sort -> Expr
simplifyCasts (ECon (I SubcId
n)) Sort
FInt  = Constant -> Expr
ECon (SubcId -> Constant
I SubcId
n)
simplifyCasts (ECon (R Double
x)) Sort
FReal = Constant -> Expr
ECon (Double -> Constant
R Double
x)
simplifyCasts Expr
e            Sort
s     = Expr -> Sort -> Expr
ECst Expr
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 :: AxiomEnv
ae = forall a. Normalizable a => a -> a
normalize forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a. GInfo c a -> AxiomEnv
ae GInfo c a
si}

instance Normalizable AxiomEnv where
  normalize :: AxiomEnv -> AxiomEnv
normalize AxiomEnv
aenv = AxiomEnv
aenv { aenvEqs :: [Equation]
aenvEqs   = {-notracepp-} forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"aenvEqs"   (forall a. Normalizable a => a -> a
normalize forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Equation]
aenvEqs   AxiomEnv
aenv)
                        , aenvSimpl :: [Rewrite]
aenvSimpl = {-notracepp-} forall a. PPrint a => [Char] -> a -> a
mytracepp [Char]
"aenvSimpl" (forall a. Normalizable a => a -> a
normalize forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AxiomEnv -> [Rewrite]
aenvSimpl AxiomEnv
aenv) }

instance Normalizable Rewrite where
  normalize :: Rewrite -> Rewrite
normalize Rewrite
rw = Rewrite
rw { smArgs :: [Symbol]
smArgs = [Symbol]
xs', smBody :: Expr
smBody = Symbol -> Expr -> Expr
normalizeBody (Rewrite -> Symbol
smName Rewrite
rw) forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su forall a b. (a -> b) -> a -> b
$ Rewrite -> Expr
smBody Rewrite
rw }
    where
      su :: Subst
su  = [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> Expr
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      xs :: [Symbol]
xs  = Rewrite -> [Symbol]
smArgs Rewrite
rw
      xs' :: [Symbol]
xs' = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith 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` forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (Rewrite -> Symbol
smName Rewrite
rw) a
i

instance Normalizable Equation where
  normalize :: Equation -> Equation
normalize Equation
eq = Equation
eq {eqArgs :: [(Symbol, Sort)]
eqArgs = forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs' [Sort]
ss,
                     eqBody :: Expr
eqBody = Symbol -> Expr -> Expr
normalizeBody (Equation -> Symbol
eqName Equation
eq) forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
subst Subst
su forall a b. (a -> b) -> a -> b
$ Equation -> Expr
eqBody Equation
eq }
    where
      su :: Subst
su           = [(Symbol, Expr)] -> Subst
mkSubst forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
x Symbol
y -> (Symbol
x,Symbol -> Expr
EVar Symbol
y)) [Symbol]
xs [Symbol]
xs'
      ([Symbol]
xs,[Sort]
ss)      = forall a b. [(a, b)] -> ([a], [b])
unzip (Equation -> [(Symbol, Sort)]
eqArgs Equation
eq)
      xs' :: [Symbol]
xs'          = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith 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` forall {a}. Show a => Symbol -> a -> Symbol
intSymbol (Equation -> Symbol
eqName Equation
eq) a
i

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

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