{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
module What4.Expr.Simplify
( simplify
, count_subterms
) where
import Control.Lens ((^.))
import Control.Monad (void, when)
import Control.Monad.ST
import Control.Monad.State (MonadState(..), State, execState)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
import qualified Data.Parameterized.HashTable as PH
import Data.Parameterized.Nonce
import Data.Parameterized.TraversableFC
import Data.Word
import What4.Interface
import qualified What4.SemiRing as SR
import What4.Expr.Builder
import qualified What4.Expr.WeightedSum as WSum
data NormCache t st fs
= NormCache { forall t (st :: Type -> Type) fs.
NormCache t st fs -> ExprBuilder t st fs
ncBuilder :: !(ExprBuilder t st fs)
, forall t (st :: Type -> Type) fs.
NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
ncTable :: !(PH.HashTable RealWorld (Expr t) (Expr t))
}
norm :: NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm :: forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
c Expr t tp
e = do
Maybe (Expr t tp)
mr <- forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ forall {k} (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
PH.lookup (forall t (st :: Type -> Type) fs.
NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
ncTable NormCache t st fs
c) Expr t tp
e
case Maybe (Expr t tp)
mr of
Just Expr t tp
r -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
r
Maybe (Expr t tp)
Nothing -> do
Expr t tp
r <- forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm' NormCache t st fs
c Expr t tp
e
forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ forall k (key :: k -> Type) s (val :: k -> Type) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
PH.insert (forall t (st :: Type -> Type) fs.
NormCache t st fs -> HashTable RealWorld (Expr t) (Expr t)
ncTable NormCache t st fs
c) Expr t tp
e Expr t tp
r
forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
r
bvIteDist :: (BoolExpr t -> r -> r -> IO r)
-> Expr t i
-> (Expr t i -> IO r)
-> IO r
bvIteDist :: forall t r (i :: BaseType).
(BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist BoolExpr t -> r -> r -> IO r
muxFn (forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr i
_ Integer
_ BoolExpr t
c Expr t i
t Expr t i
f)) Expr t i -> IO r
atomFn = do
r
t' <- forall t r (i :: BaseType).
(BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist BoolExpr t -> r -> r -> IO r
muxFn Expr t i
t Expr t i -> IO r
atomFn
r
f' <- forall t r (i :: BaseType).
(BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist BoolExpr t -> r -> r -> IO r
muxFn Expr t i
f Expr t i -> IO r
atomFn
BoolExpr t -> r -> r -> IO r
muxFn BoolExpr t
c r
t' r
f'
bvIteDist BoolExpr t -> r -> r -> IO r
_ Expr t i
u Expr t i -> IO r
atomFn = Expr t i -> IO r
atomFn Expr t i
u
newtype Or x = Or {forall {k} (x :: k). Or x -> Bool
unOr :: Bool}
instance Functor Or where
fmap :: forall a b. (a -> b) -> Or a -> Or b
fmap a -> b
_f (Or Bool
b) = (forall {k} (x :: k). Bool -> Or x
Or Bool
b)
instance Applicative Or where
pure :: forall a. a -> Or a
pure a
_ = forall {k} (x :: k). Bool -> Or x
Or Bool
False
(Or Bool
a) <*> :: forall a b. Or (a -> b) -> Or a -> Or b
<*> (Or Bool
b) = forall {k} (x :: k). Bool -> Or x
Or (Bool
a Bool -> Bool -> Bool
|| Bool
b)
norm' :: forall t st fs tp . NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm' :: forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm' NormCache t st fs
nc (AppExpr AppExpr t tp
a0) = do
let sb :: ExprBuilder t st fs
sb = forall t (st :: Type -> Type) fs.
NormCache t st fs -> ExprBuilder t st fs
ncBuilder NormCache t st fs
nc
case forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
a0 of
SemiRingSum WeightedSum (Expr t) sr
s
| let sr :: SemiRingRepr sr
sr = forall (f :: BaseType -> Type) (sr :: SemiRing).
WeightedSum f sr -> SemiRingRepr sr
WSum.sumRepr WeightedSum (Expr t) sr
s
, SR.SemiRingBVRepr BVFlavorRepr fv
SR.BVArithRepr NatRepr w
w <- SemiRingRepr sr
sr
, forall {k} (x :: k). Or x -> Bool
unOr (forall (k :: BaseType -> Type) (j :: BaseType -> Type)
(m :: Type -> Type) (sr :: SemiRing).
(Applicative m, Tm k) =>
(j (SemiRingBase sr) -> m (k (SemiRingBase sr)))
-> WeightedSum j sr -> m (WeightedSum k sr)
WSum.traverseVars @(Expr t) (\Expr t (SemiRingBase sr)
x -> forall {k} (x :: k). Bool -> Or x
Or (forall t (tp :: BaseType). Expr t tp -> Integer
iteSize Expr t (SemiRingBase sr)
x forall a. Ord a => a -> a -> Bool
>= Integer
1)) WeightedSum (Expr t) sr
s)
-> do let tms :: [(BV w, Expr t (BaseBVType w))]
tms = forall r (sr :: SemiRing) (f :: BaseType -> Type).
(r -> r -> r)
-> (Coefficient sr -> f (SemiRingBase sr) -> r)
-> (Coefficient sr -> r)
-> WeightedSum f sr
-> r
WSum.eval forall a. [a] -> [a] -> [a]
(++) (\Coefficient sr
c Expr t (SemiRingBase sr)
x -> [(Coefficient sr
c,Expr t (SemiRingBase sr)
x)]) (forall a b. a -> b -> a
const []) WeightedSum (Expr t) sr
s
let f :: [(BV w, Expr t (BaseBVType w))]
-> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
f [] Expr t tp -> IO (Expr t tp)
k = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
bvLit ExprBuilder t st fs
sb NatRepr w
w (WeightedSum (Expr t) sr
sforall s a. s -> Getting a s a -> a
^.forall (f :: BaseType -> Type) (sr :: SemiRing).
Lens' (WeightedSum f sr) (Coefficient sr)
WSum.sumOffset) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr t tp -> IO (Expr t tp)
k
f ((BV w
c,Expr t (BaseBVType w)
x):[(BV w, Expr t (BaseBVType w))]
xs) Expr t tp -> IO (Expr t tp)
k =
forall t r (i :: BaseType).
(BoolExpr t -> r -> r -> IO r)
-> Expr t i -> (Expr t i -> IO r) -> IO r
bvIteDist (forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvIte ExprBuilder t st fs
sb) Expr t (BaseBVType w)
x forall a b. (a -> b) -> a -> b
$ \Expr t (BaseBVType w)
x' ->
forall t (st :: Type -> Type) fs (sr :: SemiRing).
ExprBuilder t st fs
-> SemiRingRepr sr
-> Coefficient sr
-> Expr t (SemiRingBase sr)
-> IO (Expr t (SemiRingBase sr))
scalarMul ExprBuilder t st fs
sb SemiRingRepr sr
sr BV w
c Expr t (BaseBVType w)
x' forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Expr t (BaseBVType w)
cx' ->
[(BV w, Expr t (BaseBVType w))]
-> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
f [(BV w, Expr t (BaseBVType w))]
xs forall a b. (a -> b) -> a -> b
$ \Expr t tp
xs' ->
forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvAdd ExprBuilder t st fs
sb Expr t (BaseBVType w)
cx' Expr t tp
xs' forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr t tp -> IO (Expr t tp)
k
[(BV w, Expr t (BaseBVType w))]
-> (Expr t tp -> IO (Expr t tp)) -> IO (Expr t tp)
f [(BV w, Expr t (BaseBVType w))]
tms (forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc)
BaseEq (BaseBVRepr NatRepr w
_w) (forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr tp1
_ Integer
_ Expr t BaseBoolType
x_c Expr t tp1
x_t Expr t tp1
x_f)) Expr t tp1
y -> do
Expr t BaseBoolType
z_t <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb Expr t tp1
x_t Expr t tp1
y
Expr t BaseBoolType
z_f <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb Expr t tp1
x_f Expr t tp1
y
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Expr t BaseBoolType
x_c Expr t BaseBoolType
z_t Expr t BaseBoolType
z_f
BaseEq (BaseBVRepr NatRepr w
_w) Expr t tp1
x (forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr tp1
_ Integer
_ Expr t BaseBoolType
y_c Expr t tp1
y_t Expr t tp1
y_f)) -> do
Expr t BaseBoolType
z_t <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb Expr t tp1
x Expr t tp1
y_t
Expr t BaseBoolType
z_f <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvEq ExprBuilder t st fs
sb Expr t tp1
x Expr t tp1
y_f
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Expr t BaseBoolType
y_c Expr t BaseBoolType
z_t Expr t BaseBoolType
z_f
BVSlt (forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr (BaseBVType w)
_ Integer
_ Expr t BaseBoolType
x_c Expr t (BaseBVType w)
x_t Expr t (BaseBVType w)
x_f)) Expr t (BaseBVType w)
y -> do
Expr t BaseBoolType
z_t <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb Expr t (BaseBVType w)
x_t Expr t (BaseBVType w)
y
Expr t BaseBoolType
z_f <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb Expr t (BaseBVType w)
x_f Expr t (BaseBVType w)
y
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Expr t BaseBoolType
x_c Expr t BaseBoolType
z_t Expr t BaseBoolType
z_f
BVSlt Expr t (BaseBVType w)
x (forall t (tp :: BaseType). Expr t tp -> Maybe (App (Expr t) tp)
asApp -> Just (BaseIte BaseTypeRepr (BaseBVType w)
_ Integer
_ Expr t BaseBoolType
y_c Expr t (BaseBVType w)
y_t Expr t (BaseBVType w)
y_f)) -> do
Expr t BaseBoolType
z_t <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb Expr t (BaseBVType w)
x Expr t (BaseBVType w)
y_t
Expr t BaseBoolType
z_f <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
bvSlt ExprBuilder t st fs
sb Expr t (BaseBVType w)
x Expr t (BaseBVType w)
y_f
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> Pred sym -> Pred sym -> IO (Pred sym)
itePred ExprBuilder t st fs
sb Expr t BaseBoolType
y_c Expr t BaseBoolType
z_t Expr t BaseBoolType
z_f
App (Expr t) tp
app -> do
App (Expr t) tp
app' <- forall (m :: Type -> Type) (f :: BaseType -> Type)
(e :: BaseType -> Type) (utp :: BaseType).
(Applicative m, OrdF f, Eq (f BaseBoolType), HashableF f,
HasAbsValue f) =>
(forall (tp :: BaseType). e tp -> m (f tp))
-> App e utp -> m (App f utp)
traverseApp (forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc) App (Expr t) tp
app
if App (Expr t) tp
app' forall a. Eq a => a -> a -> Bool
== App (Expr t) tp
app then
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall t (tp :: BaseType). AppExpr t tp -> Expr t tp
AppExpr AppExpr t tp
a0)
else
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
sbMakeExpr ExprBuilder t st fs
sb App (Expr t) tp
app'
norm' NormCache t st fs
nc (NonceAppExpr NonceAppExpr t tp
p0) = do
let predApp :: NonceApp t (Expr t) tp
predApp = forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
p0
NonceApp t (Expr t) tp
p <- forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
(g :: k -> Type) (m :: Type -> Type).
(TraversableFC t, Applicative m) =>
(forall (x :: k). f x -> m (g x))
-> forall (x :: l). t f x -> m (t g x)
traverseFC (forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc) NonceApp t (Expr t) tp
predApp
if NonceApp t (Expr t) tp
p forall a. Eq a => a -> a -> Bool
== NonceApp t (Expr t) tp
predApp then
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall t (tp :: BaseType). NonceAppExpr t tp -> Expr t tp
NonceAppExpr NonceAppExpr t tp
p0
else
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall t (st :: Type -> Type) fs (tp :: BaseType).
ExprBuilder t st fs -> NonceApp t (Expr t) tp -> IO (Expr t tp)
sbNonceExpr (forall t (st :: Type -> Type) fs.
NormCache t st fs -> ExprBuilder t st fs
ncBuilder NormCache t st fs
nc) NonceApp t (Expr t) tp
p
norm' NormCache t st fs
_ Expr t tp
e = forall (m :: Type -> Type) a. Monad m => a -> m a
return Expr t tp
e
simplify :: ExprBuilder t st fs -> BoolExpr t -> IO (BoolExpr t)
simplify :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> BoolExpr t -> IO (BoolExpr t)
simplify ExprBuilder t st fs
sb BoolExpr t
p = do
HashTable RealWorld (Expr t) (Expr t)
tbl <- forall a. ST RealWorld a -> IO a
stToIO forall a b. (a -> b) -> a -> b
$ forall {k} s (key :: k -> Type) (val :: k -> Type).
ST s (HashTable s key val)
PH.new
let nc :: NormCache t st fs
nc = NormCache { ncBuilder :: ExprBuilder t st fs
ncBuilder = ExprBuilder t st fs
sb
, ncTable :: HashTable RealWorld (Expr t) (Expr t)
ncTable = HashTable RealWorld (Expr t) (Expr t)
tbl
}
forall t (st :: Type -> Type) fs (tp :: BaseType).
NormCache t st fs -> Expr t tp -> IO (Expr t tp)
norm NormCache t st fs
nc BoolExpr t
p
type Counter = State (Map Word64 Int)
recordExpr :: Nonce t (tp::k) -> Counter Bool
recordExpr :: forall t k (tp :: k). Nonce t tp -> Counter Bool
recordExpr Nonce t tp
n = do
Map Word64 Int
m <- forall s (m :: Type -> Type). MonadState s m => m s
get
let (Maybe Int
mr, Map Word64 Int
m') = forall k a.
Ord k =>
(k -> a -> a -> a) -> k -> a -> Map k a -> (Maybe a, Map k a)
Map.insertLookupWithKey (\Word64
_ -> forall a. Num a => a -> a -> a
(+)) (forall k s (tp :: k). Nonce s tp -> Word64
indexValue Nonce t tp
n) Int
1 Map Word64 Int
m
forall s (m :: Type -> Type). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ Map Word64 Int
m'
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall a. Maybe a -> Bool
isNothing Maybe Int
mr
count_subterms' :: Expr t tp -> Counter ()
count_subterms' :: forall t (tp :: BaseType).
Expr t tp -> StateT (Map Word64 Int) Identity ()
count_subterms' Expr t tp
e0 =
case Expr t tp
e0 of
BoolExpr{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
SemiRingLiteral{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
StringExpr{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
FloatExpr{} -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ()
AppExpr AppExpr t tp
ae -> do
Bool
is_new <- forall t k (tp :: k). Nonce t tp -> Counter Bool
recordExpr (forall t (tp :: BaseType). AppExpr t tp -> Nonce t tp
appExprId AppExpr t tp
ae)
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
is_new forall a b. (a -> b) -> a -> b
$ do
forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
(f :: k -> Type) a.
(FoldableFC t, Applicative m) =>
(forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
traverseFC_ forall t (tp :: BaseType).
Expr t tp -> StateT (Map Word64 Int) Identity ()
count_subterms' (forall t (tp :: BaseType). AppExpr t tp -> App (Expr t) tp
appExprApp AppExpr t tp
ae)
NonceAppExpr NonceAppExpr t tp
nae -> do
Bool
is_new <- forall t k (tp :: k). Nonce t tp -> Counter Bool
recordExpr (forall t (tp :: BaseType). NonceAppExpr t tp -> Nonce t tp
nonceExprId NonceAppExpr t tp
nae)
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when Bool
is_new forall a b. (a -> b) -> a -> b
$ do
forall {k} {l} (t :: (k -> Type) -> l -> Type) (m :: Type -> Type)
(f :: k -> Type) a.
(FoldableFC t, Applicative m) =>
(forall (x :: k). f x -> m a) -> forall (x :: l). t f x -> m ()
traverseFC_ forall t (tp :: BaseType).
Expr t tp -> StateT (Map Word64 Int) Identity ()
count_subterms' (forall t (tp :: BaseType).
NonceAppExpr t tp -> NonceApp t (Expr t) tp
nonceExprApp NonceAppExpr t tp
nae)
BoundVarExpr ExprBoundVar t tp
v -> do
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall t k (tp :: k). Nonce t tp -> Counter Bool
recordExpr (forall t (tp :: BaseType). ExprBoundVar t tp -> Nonce t tp
bvarId ExprBoundVar t tp
v)
count_subterms :: Expr t tp -> Map Word64 Int
count_subterms :: forall t (tp :: BaseType). Expr t tp -> Map Word64 Int
count_subterms Expr t tp
e = forall s a. State s a -> s -> s
execState (forall t (tp :: BaseType).
Expr t tp -> StateT (Map Word64 Int) Identity ()
count_subterms' Expr t tp
e) forall k a. Map k a
Map.empty