{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Grisette.Internal.SymPrim.Prim.TermUtils
( extractTerm,
castTerm,
someTermsSize,
someTermSize,
termSize,
termsSize,
)
where
import Control.Monad.State
( State,
execState,
gets,
modify',
)
import Data.Data (cast)
import Data.Foldable (Foldable (toList), traverse_)
import qualified Data.HashSet as HS
import Grisette.Internal.Core.Data.MemoUtils (htmemo2)
import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))
import Grisette.Internal.SymPrim.Prim.Internal.Term
( IsSymbolKind (SymbolKindConstraint),
SomeTypedConstantSymbol,
SomeTypedSymbol (SomeTypedSymbol),
SupportedPrim (castTypedSymbol),
Term
( AbsNumTerm,
AddNumTerm,
AndBitsTerm,
AndTerm,
ApplyTerm,
BVConcatTerm,
BVExtendTerm,
BVSelectTerm,
BinaryTerm,
BitCastOrTerm,
BitCastTerm,
ComplementBitsTerm,
ConTerm,
DistinctTerm,
DivIntegralTerm,
EqTerm,
ExistsTerm,
FPBinaryTerm,
FPFMATerm,
FPRoundingBinaryTerm,
FPRoundingUnaryTerm,
FPTraitTerm,
FPUnaryTerm,
FdivTerm,
FloatingUnaryTerm,
ForallTerm,
FromFPOrTerm,
FromIntegralTerm,
ITETerm,
LeOrdTerm,
LtOrdTerm,
ModIntegralTerm,
MulNumTerm,
NegNumTerm,
NotTerm,
OrBitsTerm,
OrTerm,
PowerTerm,
QuotIntegralTerm,
RecipTerm,
RemIntegralTerm,
RotateLeftTerm,
RotateRightTerm,
ShiftLeftTerm,
ShiftRightTerm,
SignumNumTerm,
SymTerm,
TernaryTerm,
ToFPTerm,
UnaryTerm,
XorBitsTerm
),
TypedAnySymbol,
introSupportedPrimConstraint,
someTypedSymbol,
)
import Grisette.Internal.SymPrim.Prim.SomeTerm
( SomeTerm (SomeTerm),
)
import Type.Reflection
( TypeRep,
Typeable,
eqTypeRep,
typeRep,
pattern App,
type (:~~:) (HRefl),
)
import qualified Type.Reflection as R
extractSymSomeTerm ::
forall knd.
(IsSymbolKind knd) =>
HS.HashSet (SomeTypedConstantSymbol) ->
SomeTerm ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
= (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo
where
gotyped ::
(SupportedPrim a) =>
( HS.HashSet (SomeTypedConstantSymbol) ->
SomeTerm ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
) ->
HS.HashSet (SomeTypedConstantSymbol) ->
Term a ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
gotyped :: forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
boundedSymbols Term a
a = HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
boundedSymbols (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
a)
initialMemo ::
HS.HashSet (SomeTypedConstantSymbol) ->
SomeTerm ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
initialMemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
initialMemo)
{-# NOINLINE initialMemo #-}
go ::
( HS.HashSet (SomeTypedConstantSymbol) ->
SomeTerm ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
) ->
HS.HashSet (SomeTypedConstantSymbol) ->
SomeTerm ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
go :: (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (SymTerm Id
_ (TypedAnySymbol a
sym :: TypedAnySymbol a))) =
case (TypedAnySymbol a -> Maybe (TypedSymbol 'ConstantKind a)
forall t (knd' :: SymbolKind) (knd :: SymbolKind).
(SupportedPrim t, IsSymbolKind knd') =>
TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
forall (knd' :: SymbolKind) (knd :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd a -> Maybe (TypedSymbol knd' a)
castTypedSymbol TypedAnySymbol a
sym, TypedAnySymbol a -> Maybe (TypedSymbol knd a)
forall t (knd' :: SymbolKind) (knd :: SymbolKind).
(SupportedPrim t, IsSymbolKind knd') =>
TypedSymbol knd t -> Maybe (TypedSymbol knd' t)
forall (knd' :: SymbolKind) (knd :: SymbolKind).
IsSymbolKind knd' =>
TypedSymbol knd a -> Maybe (TypedSymbol knd' a)
castTypedSymbol TypedAnySymbol a
sym) of
(Just TypedSymbol 'ConstantKind a
sym', Maybe (TypedSymbol knd a)
_) | SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member (TypedSymbol 'ConstantKind a -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind a
sym') HashSet SomeTypedConstantSymbol
bs -> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet (SomeTypedSymbol knd)
forall a. HashSet a
HS.empty
(Maybe (TypedSymbol 'ConstantKind a)
_, Just TypedSymbol knd a
sym') ->
HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd)
forall a. Hashable a => a -> HashSet a
HS.singleton (SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd))
-> SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd)
forall a b. (a -> b) -> a -> b
$ TypeRep a -> TypedSymbol knd a -> SomeTypedSymbol knd
forall (knd :: SymbolKind) t.
TypeRep t -> TypedSymbol knd t -> SomeTypedSymbol knd
SomeTypedSymbol (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep @a) TypedSymbol knd a
sym'
(Maybe (TypedSymbol 'ConstantKind a), Maybe (TypedSymbol knd a))
_ -> Maybe (HashSet (SomeTypedSymbol knd))
forall a. Maybe a
Nothing
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ConTerm Id
_ a
cv :: Term v)) =
case (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep v) of
App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
case TypeRep (-->) -> TypeRep a -> Maybe ((-->) :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> *). Typeable a => TypeRep a
typeRep @(-->)) TypeRep a
gf of
Just (-->) :~~: a
HRefl -> case a
cv of
GeneralFun TypedConstantSymbol b
sym (Term b
tm :: Term r) ->
let newmemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo)
{-# NOINLINE newmemo #-}
in (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped
HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo
(HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HS.union (SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol
forall a. Hashable a => a -> HashSet a
HS.singleton (TypedConstantSymbol b -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedConstantSymbol b
sym)) HashSet SomeTypedConstantSymbol
bs)
Term b
tm
Maybe ((-->) :~~: a)
Nothing -> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet (SomeTypedSymbol knd)
forall a. HashSet a
HS.empty
TypeRep a
_ -> HashSet (SomeTypedSymbol knd)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return HashSet (SomeTypedSymbol knd)
forall a. HashSet a
HS.empty
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ForallTerm Id
_ TypedSymbol 'ConstantKind t1
sym Term Bool
arg)) =
let newmemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo)
{-# NOINLINE newmemo #-}
in (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo (SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'ConstantKind t1 -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t1
sym) HashSet SomeTypedConstantSymbol
bs) Term Bool
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ExistsTerm Id
_ TypedSymbol 'ConstantKind t1
sym Term Bool
arg)) =
let newmemo :: HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
forall k1 k2 a.
(Eq k1, Hashable k1, Eq k2, Hashable k2) =>
(k1 -> k2 -> a) -> k1 -> k2 -> a
htmemo2 ((HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> SomeTerm
-> Maybe (HashSet (SomeTypedSymbol knd))
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo)
{-# NOINLINE newmemo #-}
in (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
newmemo (SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
-> HashSet SomeTypedConstantSymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (TypedSymbol 'ConstantKind t1 -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'ConstantKind t1
sym) HashSet SomeTypedConstantSymbol
bs) Term Bool
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (UnaryTerm Id
_ tag
_ Term arg
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term arg
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term arg
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term arg1
-> Term arg2
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term arg1
arg1 Term arg2
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (TernaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2 Term arg3
arg3)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term arg1
-> Term arg2
-> Term arg3
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (NotTerm Id
_ Term Bool
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (OrTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
arg1 Term Bool
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AndTerm Id
_ Term Bool
arg1 Term Bool
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term Bool
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
arg1 Term Bool
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (EqTerm Id
_ Term t1
arg1 Term t1
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term t1
arg1 Term t1
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (DistinctTerm Id
_ NonEmpty (Term t1)
args)) =
[Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets ([Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd)))
-> [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b. (a -> b) -> a -> b
$ (Term t1 -> Maybe (HashSet (SomeTypedSymbol knd)))
-> [Term t1] -> [Maybe (HashSet (SomeTypedSymbol knd))]
forall a b. (a -> b) -> [a] -> [b]
map ((HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs) ([Term t1] -> [Maybe (HashSet (SomeTypedSymbol knd))])
-> [Term t1] -> [Maybe (HashSet (SomeTypedSymbol knd))]
forall a b. (a -> b) -> a -> b
$ NonEmpty (Term t1) -> [Term t1]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (Term t1)
args
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ITETerm Id
_ Term Bool
cond Term a
arg1 Term a
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term Bool
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term Bool
cond Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AddNumTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (NegNumTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (MulNumTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AbsNumTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (SignumNumTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (LtOrdTerm Id
_ Term t1
arg1 Term t1
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term t1
arg1 Term t1
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (LeOrdTerm Id
_ Term t1
arg1 Term t1
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term t1
-> Term t1
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term t1
arg1 Term t1
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (AndBitsTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (OrBitsTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (XorBitsTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ComplementBitsTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ShiftLeftTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ShiftRightTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RotateLeftTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RotateRightTerm Id
_ Term a
arg Term a
n1)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg Term a
n1
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BitCastTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BitCastOrTerm Id
_ Term a
d Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
d Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BVConcatTerm Id
_ Term (bv l)
arg1 Term (bv r)
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (bv l)
-> Term (bv r)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (bv l)
arg1 Term (bv r)
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv n)
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (bv n)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (bv n)
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (bv l)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (bv l)
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ApplyTerm Id
_ Term f
func Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term f
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term f
func Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (DivIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ModIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (QuotIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RemIntegralTerm Id
_ Term a
arg1 Term a
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPTraitTerm Id
_ FPTrait
_ Term (FP eb sb)
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FdivTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (RecipTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FloatingUnaryTerm Id
_ FloatingUnaryOp
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (PowerTerm Id
_ Term a
arg1 Term a
arg2)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term a
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPUnaryTerm Id
_ FPUnaryOp
_ Term (FP eb sb)
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPBinaryTerm Id
_ FPBinaryOp
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPRoundingUnaryTerm Id
_ FPRoundingUnaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPRoundingBinaryTerm Id
_ FPRoundingBinaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FPFMATerm Id
_ Term FPRoundingMode
mode Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3)) =
[Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets
[ (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term FPRoundingMode
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term FPRoundingMode
mode,
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg1,
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg2,
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term (FP eb sb)
arg3
]
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FromIntegralTerm Id
_ Term a
arg)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (FromFPOrTerm Id
_ Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg)) =
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg
go HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs (SomeTerm (ToFPTerm Id
_ Term FPRoundingMode
mode Term a
arg Proxy eb
_ Proxy sb
_)) = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term FPRoundingMode
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term FPRoundingMode
mode Term a
arg
goUnary ::
(SupportedPrim a) =>
(HS.HashSet (SomeTypedConstantSymbol) -> SomeTerm -> Maybe (HS.HashSet (SomeTypedSymbol knd))) ->
HS.HashSet (SomeTypedConstantSymbol) ->
Term a ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
goUnary :: forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
goUnary = (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped
goBinary ::
(SupportedPrim a, SupportedPrim b) =>
(HS.HashSet (SomeTypedConstantSymbol) -> SomeTerm -> Maybe (HS.HashSet (SomeTypedSymbol knd))) ->
HS.HashSet (SomeTypedConstantSymbol) ->
Term a ->
Term b ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
goBinary :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
goBinary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term b
arg2 =
Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
forall {a}.
Eq a =>
Maybe (HashSet a) -> Maybe (HashSet a) -> Maybe (HashSet a)
combineSet ((HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1) ((HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term b
arg2)
goTernary ::
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HS.HashSet (SomeTypedConstantSymbol) -> SomeTerm -> Maybe (HS.HashSet (SomeTypedSymbol knd))) ->
HS.HashSet (SomeTypedConstantSymbol) ->
Term a ->
Term b ->
Term c ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
goTernary :: forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Term b
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
goTernary HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1 Term b
arg2 Term c
arg3 =
[Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets
[ (HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term a
arg1,
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term b
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term b
arg2,
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term c
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a.
SupportedPrim a =>
(HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd)))
-> HashSet SomeTypedConstantSymbol
-> Term a
-> Maybe (HashSet (SomeTypedSymbol knd))
gotyped HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
memo HashSet SomeTypedConstantSymbol
bs Term c
arg3
]
combineSet :: Maybe (HashSet a) -> Maybe (HashSet a) -> Maybe (HashSet a)
combineSet (Just HashSet a
a) (Just HashSet a
b) = HashSet a -> Maybe (HashSet a)
forall a. a -> Maybe a
Just (HashSet a -> Maybe (HashSet a)) -> HashSet a -> Maybe (HashSet a)
forall a b. (a -> b) -> a -> b
$ HashSet a -> HashSet a -> HashSet a
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
HS.union HashSet a
a HashSet a
b
combineSet Maybe (HashSet a)
_ Maybe (HashSet a)
_ = Maybe (HashSet a)
forall a. Maybe a
Nothing
combineAllSets :: [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
combineAllSets = (Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd)))
-> [Maybe (HashSet (SomeTypedSymbol knd))]
-> Maybe (HashSet (SomeTypedSymbol knd))
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
-> Maybe (HashSet (SomeTypedSymbol knd))
forall {a}.
Eq a =>
Maybe (HashSet a) -> Maybe (HashSet a) -> Maybe (HashSet a)
combineSet
{-# INLINEABLE extractSymSomeTerm #-}
extractTerm ::
(IsSymbolKind knd, SymbolKindConstraint knd a, SupportedPrim a) =>
HS.HashSet (SomeTypedConstantSymbol) ->
Term a ->
Maybe (HS.HashSet (SomeTypedSymbol knd))
HashSet SomeTypedConstantSymbol
initialBoundedSymbols Term a
t =
HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
forall (knd :: SymbolKind).
IsSymbolKind knd =>
HashSet SomeTypedConstantSymbol
-> SomeTerm -> Maybe (HashSet (SomeTypedSymbol knd))
extractSymSomeTerm HashSet SomeTypedConstantSymbol
initialBoundedSymbols (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t)
{-# INLINE extractTerm #-}
castTerm :: forall a b. (Typeable b) => Term a -> Maybe (Term b)
castTerm :: forall a b. Typeable b => Term a -> Maybe (Term b)
castTerm Term a
t = Term a -> (SupportedPrim a => Maybe (Term b)) -> Maybe (Term b)
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
t ((SupportedPrim a => Maybe (Term b)) -> Maybe (Term b))
-> (SupportedPrim a => Maybe (Term b)) -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ Term a -> Maybe (Term b)
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term a
t
{-# INLINE castTerm #-}
someTermsSize :: [SomeTerm] -> Int
someTermsSize :: [SomeTerm] -> Id
someTermsSize [SomeTerm]
terms = HashSet SomeTerm -> Id
forall a. HashSet a -> Id
HS.size (HashSet SomeTerm -> Id) -> HashSet SomeTerm -> Id
forall a b. (a -> b) -> a -> b
$ State (HashSet SomeTerm) [()]
-> HashSet SomeTerm -> HashSet SomeTerm
forall s a. State s a -> s -> s
execState ((SomeTerm -> StateT (HashSet SomeTerm) Identity ())
-> [SomeTerm] -> State (HashSet SomeTerm) [()]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse SomeTerm -> StateT (HashSet SomeTerm) Identity ()
goSome [SomeTerm]
terms) HashSet SomeTerm
forall a. HashSet a
HS.empty
where
exists :: Term a -> m Bool
exists Term a
t = (HashSet SomeTerm -> Bool) -> m Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (SomeTerm -> HashSet SomeTerm -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
HS.member (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
add :: Term a -> m ()
add Term a
t = (HashSet SomeTerm -> HashSet SomeTerm) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' (SomeTerm -> HashSet SomeTerm -> HashSet SomeTerm
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HS.insert (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t))
goSome :: SomeTerm -> State (HS.HashSet SomeTerm) ()
goSome :: SomeTerm -> StateT (HashSet SomeTerm) Identity ()
goSome (SomeTerm Term a
b) = Term a -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term a
b
go :: forall b. Term b -> State (HS.HashSet SomeTerm) ()
go :: forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go t :: Term b
t@ConTerm {} = Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
go t :: Term b
t@SymTerm {} = Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
go t :: Term b
t@(ForallTerm Id
_ TypedSymbol 'ConstantKind t1
_ Term Bool
arg) = Term b -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term Bool
arg
go t :: Term b
t@(ExistsTerm Id
_ TypedSymbol 'ConstantKind t1
_ Term Bool
arg) = Term b -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term Bool
arg
go t :: Term b
t@(UnaryTerm Id
_ tag
_ Term arg
arg) = Term b -> Term arg -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term arg
arg
go t :: Term b
t@(BinaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2) = Term b
-> Term arg1 -> Term arg2 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term arg1
arg1 Term arg2
arg2
go t :: Term b
t@(TernaryTerm Id
_ tag
_ Term arg1
arg1 Term arg2
arg2 Term arg3
arg3) = Term b
-> Term arg1
-> Term arg2
-> Term arg3
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
go t :: Term b
t@(NotTerm Id
_ Term Bool
arg) = Term b -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term Bool
arg
go t :: Term b
t@(OrTerm Id
_ Term Bool
arg1 Term Bool
arg2) = Term b
-> Term Bool -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
go t :: Term b
t@(AndTerm Id
_ Term Bool
arg1 Term Bool
arg2) = Term b
-> Term Bool -> Term Bool -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term Bool
arg1 Term Bool
arg2
go t :: Term b
t@(EqTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
go t :: Term b
t@(DistinctTerm Id
_ NonEmpty (Term t1)
args) = do
Bool
b <- Term b -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term b
t
if Bool
b
then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else do
Term b -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term b
t
(Term t1 -> StateT (HashSet SomeTerm) Identity ())
-> NonEmpty (Term t1) -> StateT (HashSet SomeTerm) Identity ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go NonEmpty (Term t1)
args
go t :: Term b
t@(ITETerm Id
_ Term Bool
cond Term b
arg1 Term b
arg2) = Term b
-> Term Bool
-> Term b
-> Term b
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term Bool
cond Term b
arg1 Term b
arg2
go t :: Term b
t@(AddNumTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(NegNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
go t :: Term b
t@(MulNumTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(AbsNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
go t :: Term b
t@(SignumNumTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
go t :: Term b
t@(LtOrdTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
go t :: Term b
t@(LeOrdTerm Id
_ Term t1
arg1 Term t1
arg2) = Term b
-> Term t1 -> Term t1 -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term t1
arg1 Term t1
arg2
go t :: Term b
t@(AndBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(OrBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(XorBitsTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(ComplementBitsTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
go t :: Term b
t@(ShiftLeftTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
go t :: Term b
t@(ShiftRightTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
go t :: Term b
t@(RotateLeftTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
go t :: Term b
t@(RotateRightTerm Id
_ Term b
arg Term b
n) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg Term b
n
go t :: Term b
t@(BitCastTerm Id
_ Term a
arg) = Term b -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term a
arg
go t :: Term b
t@(BitCastOrTerm Id
_ Term b
d Term a
arg) = Term b -> Term b -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
d Term a
arg
go t :: Term b
t@(BVConcatTerm Id
_ Term (bv l)
arg1 Term (bv r)
arg2) = Term b
-> Term (bv l)
-> Term (bv r)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term (bv l)
arg1 Term (bv r)
arg2
go t :: Term b
t@(BVSelectTerm Id
_ TypeRep ix
_ TypeRep w
_ Term (bv n)
arg) = Term b -> Term (bv n) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv n)
arg
go t :: Term b
t@(BVExtendTerm Id
_ Bool
_ TypeRep r
_ Term (bv l)
arg) = Term b -> Term (bv l) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (bv l)
arg
go t :: Term b
t@(ApplyTerm Id
_ Term f
func Term a
arg) = Term b -> Term f -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term f
func Term a
arg
go t :: Term b
t@(DivIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(ModIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(QuotIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(RemIntegralTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(FPTraitTerm Id
_ FPTrait
_ Term (FP eb sb)
arg) = Term b -> Term (FP eb sb) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (FP eb sb)
arg
go t :: Term b
t@(FdivTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(RecipTerm Id
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
go t :: Term b
t@(FloatingUnaryTerm Id
_ FloatingUnaryOp
_ Term b
arg) = Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term b
arg
go t :: Term b
t@(PowerTerm Id
_ Term b
arg1 Term b
arg2) = Term b -> Term b -> Term b -> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term b
arg1 Term b
arg2
go t :: Term b
t@(FPUnaryTerm Id
_ FPUnaryOp
_ Term (FP eb sb)
arg) = Term b -> Term (FP eb sb) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (FP eb sb)
arg
go t :: Term b
t@(FPBinaryTerm Id
_ FPBinaryOp
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2) = Term b
-> Term (FP eb sb)
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
go t :: Term b
t@(FPRoundingUnaryTerm Id
_ FPRoundingUnaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg) = Term b -> Term (FP eb sb) -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term (FP eb sb)
arg
go t :: Term b
t@(FPRoundingBinaryTerm Id
_ FPRoundingBinaryOp
_ Term FPRoundingMode
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2) = Term b
-> Term (FP eb sb)
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
go t :: Term b
t@(FPFMATerm Id
_ Term FPRoundingMode
_ Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3) = Term b
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3
go t :: Term b
t@(FromIntegralTerm Id
_ Term a
arg) = Term b -> Term a -> StateT (HashSet SomeTerm) Identity ()
forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term b
t Term a
arg
go t :: Term b
t@(FromFPOrTerm Id
_ Term b
d Term FPRoundingMode
mode Term (FP eb sb)
arg) =
Term b
-> Term b
-> Term FPRoundingMode
-> Term (FP eb sb)
-> StateT (HashSet SomeTerm) Identity ()
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term b
t Term b
d Term FPRoundingMode
mode Term (FP eb sb)
arg
go t :: Term b
t@(ToFPTerm Id
_ Term FPRoundingMode
mode Term a
arg Proxy eb
_ Proxy sb
_) = Term b
-> Term FPRoundingMode
-> Term a
-> StateT (HashSet SomeTerm) Identity ()
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term b
t Term FPRoundingMode
mode Term a
arg
goUnary :: forall a b. (SupportedPrim a) => Term a -> Term b -> State (HS.HashSet SomeTerm) ()
goUnary :: forall a b.
SupportedPrim a =>
Term a -> Term b -> StateT (HashSet SomeTerm) Identity ()
goUnary Term a
t Term b
arg = do
Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
if Bool
b
then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else do
Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg
goBinary ::
forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a ->
Term b ->
Term c ->
State (HS.HashSet SomeTerm) ()
goBinary :: forall a b c.
(SupportedPrim a, SupportedPrim b) =>
Term a -> Term b -> Term c -> StateT (HashSet SomeTerm) Identity ()
goBinary Term a
t Term b
arg1 Term c
arg2 = do
Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
if Bool
b
then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else do
Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg1
Term c -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term c
arg2
goTernary ::
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a ->
Term b ->
Term c ->
Term d ->
State (HS.HashSet SomeTerm) ()
goTernary :: forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
Term a
-> Term b
-> Term c
-> Term d
-> StateT (HashSet SomeTerm) Identity ()
goTernary Term a
t Term b
arg1 Term c
arg2 Term d
arg3 = do
Bool
b <- Term a -> StateT (HashSet SomeTerm) Identity Bool
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m Bool
exists Term a
t
if Bool
b
then () -> StateT (HashSet SomeTerm) Identity ()
forall a. a -> StateT (HashSet SomeTerm) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
else do
Term a -> StateT (HashSet SomeTerm) Identity ()
forall {m :: * -> *} {a}.
(MonadState (HashSet SomeTerm) m, SupportedPrim a) =>
Term a -> m ()
add Term a
t
Term b -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term b
arg1
Term c -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term c
arg2
Term d -> StateT (HashSet SomeTerm) Identity ()
forall b. Term b -> StateT (HashSet SomeTerm) Identity ()
go Term d
arg3
{-# INLINEABLE someTermsSize #-}
someTermSize :: SomeTerm -> Int
someTermSize :: SomeTerm -> Id
someTermSize SomeTerm
term = [SomeTerm] -> Id
someTermsSize [SomeTerm
term]
{-# INLINE someTermSize #-}
termsSize :: [Term a] -> Int
termsSize :: forall a. [Term a] -> Id
termsSize [Term a]
terms =
[SomeTerm] -> Id
someTermsSize ([SomeTerm] -> Id) -> [SomeTerm] -> Id
forall a b. (a -> b) -> a -> b
$
(\Term a
x -> Term a -> (SupportedPrim a => SomeTerm) -> SomeTerm
forall t a. Term t -> (SupportedPrim t => a) -> a
introSupportedPrimConstraint Term a
x ((SupportedPrim a => SomeTerm) -> SomeTerm)
-> (SupportedPrim a => SomeTerm) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
x) (Term a -> SomeTerm) -> [Term a] -> [SomeTerm]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term a]
terms
{-# INLINEABLE termsSize #-}
termSize :: Term a -> Int
termSize :: forall a. Term a -> Id
termSize Term a
term = [Term a] -> Id
forall a. [Term a] -> Id
termsSize [Term a
term]
{-# INLINE termSize #-}