{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermSubstitution
( substTerm,
)
where
import Grisette.Core.Data.MemoUtils (htmemo)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( conTerm,
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
( SomeTerm (SomeTerm),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( BinaryOp (partialEvalBinary),
SupportedPrim,
Term
( AbsNumTerm,
AddNumTerm,
AndBitsTerm,
AndTerm,
BVConcatTerm,
BVExtendTerm,
BVSelectTerm,
BinaryTerm,
ComplementBitsTerm,
ConTerm,
DivBoundedIntegralTerm,
DivIntegralTerm,
EqvTerm,
GeneralFunApplyTerm,
ITETerm,
LENumTerm,
LTNumTerm,
ModBoundedIntegralTerm,
ModIntegralTerm,
NotTerm,
OrBitsTerm,
OrTerm,
QuotBoundedIntegralTerm,
QuotIntegralTerm,
RemBoundedIntegralTerm,
RemIntegralTerm,
RotateLeftTerm,
RotateRightTerm,
ShiftLeftTerm,
ShiftRightTerm,
SignumNumTerm,
SymTerm,
TabularFunApplyTerm,
TernaryTerm,
TimesNumTerm,
ToSignedTerm,
ToUnsignedTerm,
UMinusNumTerm,
UnaryTerm,
XorBitsTerm
),
TernaryOp (partialEvalTernary),
TypedSymbol,
UnaryOp (partialEvalUnary),
someTypedSymbol,
type (-->) (GeneralFun),
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
( pevalBVConcatTerm,
pevalBVExtendTerm,
pevalBVSelectTerm,
pevalToSignedTerm,
pevalToUnsignedTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
( pevalAndBitsTerm,
pevalComplementBitsTerm,
pevalOrBitsTerm,
pevalRotateLeftTerm,
pevalRotateRightTerm,
pevalShiftLeftTerm,
pevalShiftRightTerm,
pevalXorBitsTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
( pevalAndTerm,
pevalEqvTerm,
pevalITETerm,
pevalNotTerm,
pevalOrTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
( pevalGeneralFunApplyTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
( pevalDivBoundedIntegralTerm,
pevalDivIntegralTerm,
pevalModBoundedIntegralTerm,
pevalModIntegralTerm,
pevalQuotBoundedIntegralTerm,
pevalQuotIntegralTerm,
pevalRemBoundedIntegralTerm,
pevalRemIntegralTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
( pevalAbsNumTerm,
pevalAddNumTerm,
pevalLeNumTerm,
pevalLtNumTerm,
pevalSignumNumTerm,
pevalTimesNumTerm,
pevalUMinusNumTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
( pevalTabularFunApplyTerm,
)
import Type.Reflection
( TypeRep,
eqTypeRep,
typeRep,
pattern App,
type (:~~:) (HRefl),
)
import Unsafe.Coerce (unsafeCoerce)
substTerm :: forall a b. (SupportedPrim a, SupportedPrim b) => TypedSymbol a -> Term a -> Term b -> Term b
substTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term a -> Term b -> Term b
substTerm TypedSymbol a
sym Term a
term = Term b -> Term b
forall x. SupportedPrim x => Term x -> Term x
gov
where
gov :: (SupportedPrim x) => Term x -> Term x
gov :: forall x. SupportedPrim x => Term x -> Term x
gov Term x
b = case SomeTerm -> SomeTerm
go (Term x -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term x
b) of
SomeTerm Term a
v -> Term a -> Term x
forall a b. a -> b
unsafeCoerce Term a
v
go :: SomeTerm -> SomeTerm
go :: SomeTerm -> SomeTerm
go = (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm)
-> (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall a b. (a -> b) -> a -> b
$ \stm :: SomeTerm
stm@(SomeTerm (Term a
tm :: Term v)) ->
case Term a
tm of
ConTerm Id
_ a
cv -> 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 a -> TypeRep (-->) -> Maybe (a :~~: (-->))
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
gf (forall {k} (a :: k). Typeable a => TypeRep a
forall (a :: * -> * -> *). Typeable a => TypeRep a
typeRep @(-->)) of
Just a :~~: (-->)
HRefl -> case a
cv of
GeneralFun TypedSymbol b
sym1 Term b
tm1 ->
if TypedSymbol b -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol b
sym1 SomeTypedSymbol -> SomeTypedSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym
then SomeTerm
stm
else Term (b --> b) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (b --> b) -> SomeTerm) -> Term (b --> b) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ (b --> b) -> Term (b --> b)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm ((b --> b) -> Term (b --> b)) -> (b --> b) -> Term (b --> b)
forall a b. (a -> b) -> a -> b
$ TypedSymbol b -> Term b -> b --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym1 (Term b -> Term b
forall x. SupportedPrim x => Term x -> Term x
gov Term b
tm1)
Maybe (a :~~: (-->))
Nothing -> SomeTerm
stm
TypeRep a
_ -> SomeTerm
stm
SymTerm Id
_ TypedSymbol a
ts -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ if TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
ts SomeTypedSymbol -> SomeTypedSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym then Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
term else Term a
tm
UnaryTerm Id
_ tag
tag Term arg
te -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg -> Term a
forall tag arg t.
(UnaryOp tag arg t, Typeable tag, Typeable t) =>
tag -> Term arg -> Term t
partialEvalUnary tag
tag (Term arg -> Term arg
forall x. SupportedPrim x => Term x -> Term x
gov Term arg
te)
BinaryTerm Id
_ tag
tag Term arg1
te Term arg2
te' -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> Term a
forall tag arg1 arg2 t.
(BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term t
partialEvalBinary tag
tag (Term arg1 -> Term arg1
forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
te) (Term arg2 -> Term arg2
forall x. SupportedPrim x => Term x -> Term x
gov Term arg2
te')
TernaryTerm Id
_ tag
tag Term arg1
op1 Term arg2
op2 Term arg3
op3 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term a
forall tag arg1 arg2 arg3 t.
(TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
partialEvalTernary tag
tag (Term arg1 -> Term arg1
forall x. SupportedPrim x => Term x -> Term x
gov Term arg1
op1) (Term arg2 -> Term arg2
forall x. SupportedPrim x => Term x -> Term x
gov Term arg2
op2) (Term arg3 -> Term arg3
forall x. SupportedPrim x => Term x -> Term x
gov Term arg3
op3)
NotTerm Id
_ Term Bool
op -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
pevalNotTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op)
OrTerm Id
_ Term Bool
op1 Term Bool
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalOrTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
AndTerm Id
_ Term Bool
op1 Term Bool
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> Term Bool
pevalAndTerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op1) (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
op2)
EqvTerm Id
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
ITETerm Id
_ Term Bool
c Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term a -> Term a -> Term a
forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm (Term Bool -> Term Bool
forall x. SupportedPrim x => Term x -> Term x
gov Term Bool
c) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
AddNumTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
UMinusNumTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
TimesNumTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
AbsNumTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
SignumNumTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
LTNumTerm Id
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
LENumTerm Id
_ Term t1
op1 Term t1
op2 -> Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term t1 -> Term t1 -> Term Bool
forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op1) (Term t1 -> Term t1
forall x. SupportedPrim x => Term x -> Term x
gov Term t1
op2)
AndBitsTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
OrBitsTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
XorBitsTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
ComplementBitsTerm Id
_ Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
ShiftLeftTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftLeftTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
RotateLeftTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateLeftTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
ShiftRightTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftRightTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
RotateRightTerm Id
_ Term a
op Term a
n -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateRightTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
n)
ToSignedTerm Id
_ Term u
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term u -> Term a
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
pevalToSignedTerm Term u
op
ToUnsignedTerm Id
_ Term s
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term s -> Term a
forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
pevalToUnsignedTerm Term s
op
BVConcatTerm Id
_ Term (bv a)
op1 Term (bv b)
op2 -> Term (bv (a + b)) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv (a + b)) -> SomeTerm) -> Term (bv (a + b)) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (bv a) -> Term (bv b) -> Term (bv (a + b))
forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
pevalBVConcatTerm (Term (bv a) -> Term (bv a)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv a)
op1) (Term (bv b) -> Term (bv b)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv b)
op2)
BVSelectTerm Id
_ TypeRep ix
ix TypeRep w
w Term (bv n)
op -> Term (bv w) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv w) -> SomeTerm) -> Term (bv w) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(forall (n1 :: Nat).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (bv n1),
Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm TypeRep ix
ix TypeRep w
w (Term (bv n) -> Term (bv n)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv n)
op)
BVExtendTerm Id
_ Bool
n TypeRep r
signed Term (bv l)
op -> Term (bv r) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (bv r) -> SomeTerm) -> Term (bv r) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
n TypeRep r
signed (Term (bv l) -> Term (bv l)
forall x. SupportedPrim x => Term x -> Term x
gov Term (bv l)
op)
TabularFunApplyTerm Id
_ Term (a =-> a)
f Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (a =-> a) -> Term a -> Term a
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm (Term (a =-> a) -> Term (a =-> a)
forall x. SupportedPrim x => Term x -> Term x
gov Term (a =-> a)
f) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
GeneralFunApplyTerm Id
_ Term (a --> a)
f Term a
op -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term (a --> a) -> Term a -> Term a
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm (Term (a --> a) -> Term (a --> a)
forall x. SupportedPrim x => Term x -> Term x
gov Term (a --> a)
f) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op)
DivIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalDivIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
ModIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
QuotIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
RemIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalRemIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
DivBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDivBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
ModBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
QuotBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)
RemBoundedIntegralTerm Id
_ Term a
op1 Term a
op2 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalRemBoundedIntegralTerm (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op1) (Term a -> Term a
forall x. SupportedPrim x => Term x -> Term x
gov Term a
op2)