{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Grisette.Internal.SymPrim.GeneralFun
( type (-->) (..),
buildGeneralFun,
generalSubstSomeTerm,
substTerm,
)
where
import Control.DeepSeq (NFData (rnf))
import Data.Bifunctor (Bifunctor (second))
import Data.Foldable (Foldable (foldl'))
import qualified Data.HashSet as HS
import Data.Hashable (Hashable (hashWithSalt))
import qualified Data.SBV as SBV
import qualified Data.SBV.Dynamic as SBVD
import GHC.Generics (Generic)
import Grisette.Internal.Core.Data.Class.Function (Function ((#)))
import Grisette.Internal.Core.Data.MemoUtils (htmemo)
import Grisette.Internal.Core.Data.Symbol
( Symbol (IndexedSymbol, SimpleSymbol),
withInfo,
)
import Grisette.Internal.SymPrim.FunInstanceGen (supportedPrimFunUpTo)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP
( pevalFPBinaryTerm,
pevalFPFMATerm,
pevalFPRoundingBinaryTerm,
pevalFPRoundingUnaryTerm,
pevalFPTraitTerm,
pevalFPUnaryTerm,
)
import Grisette.Internal.SymPrim.Prim.Internal.PartialEval (totalize2)
import Grisette.Internal.SymPrim.Prim.Internal.Term
( BinaryOp (pevalBinary),
IsSymbolKind,
LinkedRep (underlyingTerm, wrapTerm),
NonFuncPrimConstraint,
NonFuncSBVBaseType,
PEvalApplyTerm (pevalApplyTerm, sbvApplyTerm),
PEvalBVTerm (pevalBVConcatTerm, pevalBVExtendTerm, pevalBVSelectTerm),
PEvalBitCastOrTerm (pevalBitCastOrTerm),
PEvalBitCastTerm (pevalBitCastTerm),
PEvalBitwiseTerm
( pevalAndBitsTerm,
pevalComplementBitsTerm,
pevalOrBitsTerm,
pevalXorBitsTerm
),
PEvalDivModIntegralTerm
( pevalDivIntegralTerm,
pevalModIntegralTerm
),
PEvalFloatingTerm (pevalFloatingUnaryTerm, pevalPowerTerm),
PEvalFractionalTerm (pevalFdivTerm, pevalRecipTerm),
PEvalFromIntegralTerm (pevalFromIntegralTerm),
PEvalIEEEFPConvertibleTerm (pevalFromFPOrTerm, pevalToFPTerm),
PEvalNumTerm
( pevalAbsNumTerm,
pevalAddNumTerm,
pevalMulNumTerm,
pevalNegNumTerm,
pevalSignumNumTerm
),
PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm),
PEvalRotateTerm (pevalRotateRightTerm),
PEvalShiftTerm (pevalShiftLeftTerm, pevalShiftRightTerm),
SBVRep (SBVType),
SomeTypedConstantSymbol,
SupportedNonFuncPrim (withNonFuncPrim),
SupportedPrim
( castTypedSymbol,
defaultValue,
parseSMTModelResult,
pevalDistinctTerm,
pevalITETerm,
withPrim
),
SupportedPrimConstraint (PrimConstraint),
SymbolKind (AnyKind),
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
),
TernaryOp (pevalTernary),
TypedConstantSymbol,
TypedSymbol (TypedSymbol, unTypedSymbol),
UnaryOp (pevalUnary),
applyTerm,
conTerm,
eqHeteroSymbol,
existsTerm,
forallTerm,
partitionCVArg,
pevalAndTerm,
pevalEqTerm,
pevalNotTerm,
pevalOrTerm,
pevalQuotIntegralTerm,
pevalRemIntegralTerm,
pevalRotateLeftTerm,
pformatTerm,
someTypedSymbol,
symTerm,
translateTypeError,
)
import Grisette.Internal.SymPrim.Prim.SomeTerm (SomeTerm (SomeTerm), someTerm)
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Type.Reflection
( TypeRep,
eqTypeRep,
typeRep,
pattern App,
type (:~~:) (HRefl),
)
import Unsafe.Coerce (unsafeCoerce)
data (-->) a b where
GeneralFun ::
(SupportedPrim a, SupportedPrim b) =>
TypedConstantSymbol a ->
Term b ->
a --> b
instance (LinkedRep a sa, LinkedRep b sb) => Function (a --> b) sa sb where
(GeneralFun TypedConstantSymbol a
s Term b
t) # :: (a --> b) -> sa -> sb
# sa
x = Term b -> sb
forall con sym. LinkedRep con sym => Term con -> sym
wrapTerm (Term b -> sb) -> Term b -> sb
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol a -> Term a -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol a
s (sa -> Term a
forall con sym. LinkedRep con sym => sym -> Term con
underlyingTerm sa
x) Term b
t
infixr 0 -->
buildGeneralFun ::
(SupportedNonFuncPrim a, SupportedPrim b) =>
TypedConstantSymbol a ->
Term b ->
a --> b
buildGeneralFun :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
buildGeneralFun TypedConstantSymbol a
arg Term b
v =
TypedConstantSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
GeneralFun
(Symbol -> TypedConstantSymbol a
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
newarg)
(TypedConstantSymbol a -> Term a -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol a
arg (Symbol -> Term a
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
newarg) Term b
v)
where
newarg :: Symbol
newarg = case TypedConstantSymbol a -> Symbol
forall t (knd :: SymbolKind). TypedSymbol knd t -> Symbol
unTypedSymbol TypedConstantSymbol a
arg of
SimpleSymbol Identifier
s -> Identifier -> Symbol
SimpleSymbol (Identifier -> ARG -> Identifier
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Identifier -> a -> Identifier
withInfo Identifier
s ARG
ARG)
IndexedSymbol Identifier
s Int
i -> Identifier -> Int -> Symbol
IndexedSymbol (Identifier -> ARG -> Identifier
forall a.
(Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
Identifier -> a -> Identifier
withInfo Identifier
s ARG
ARG) Int
i
data ARG = ARG
deriving (ARG -> ARG -> Bool
(ARG -> ARG -> Bool) -> (ARG -> ARG -> Bool) -> Eq ARG
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ARG -> ARG -> Bool
== :: ARG -> ARG -> Bool
$c/= :: ARG -> ARG -> Bool
/= :: ARG -> ARG -> Bool
Eq, Eq ARG
Eq ARG =>
(ARG -> ARG -> Ordering)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> Bool)
-> (ARG -> ARG -> ARG)
-> (ARG -> ARG -> ARG)
-> Ord ARG
ARG -> ARG -> Bool
ARG -> ARG -> Ordering
ARG -> ARG -> ARG
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ARG -> ARG -> Ordering
compare :: ARG -> ARG -> Ordering
$c< :: ARG -> ARG -> Bool
< :: ARG -> ARG -> Bool
$c<= :: ARG -> ARG -> Bool
<= :: ARG -> ARG -> Bool
$c> :: ARG -> ARG -> Bool
> :: ARG -> ARG -> Bool
$c>= :: ARG -> ARG -> Bool
>= :: ARG -> ARG -> Bool
$cmax :: ARG -> ARG -> ARG
max :: ARG -> ARG -> ARG
$cmin :: ARG -> ARG -> ARG
min :: ARG -> ARG -> ARG
Ord, (forall (m :: * -> *). Quote m => ARG -> m Exp)
-> (forall (m :: * -> *). Quote m => ARG -> Code m ARG) -> Lift ARG
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => ARG -> m Exp
forall (m :: * -> *). Quote m => ARG -> Code m ARG
$clift :: forall (m :: * -> *). Quote m => ARG -> m Exp
lift :: forall (m :: * -> *). Quote m => ARG -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
liftTyped :: forall (m :: * -> *). Quote m => ARG -> Code m ARG
Lift, Int -> ARG -> ShowS
[ARG] -> ShowS
ARG -> String
(Int -> ARG -> ShowS)
-> (ARG -> String) -> ([ARG] -> ShowS) -> Show ARG
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ARG -> ShowS
showsPrec :: Int -> ARG -> ShowS
$cshow :: ARG -> String
show :: ARG -> String
$cshowList :: [ARG] -> ShowS
showList :: [ARG] -> ShowS
Show, (forall x. ARG -> Rep ARG x)
-> (forall x. Rep ARG x -> ARG) -> Generic ARG
forall x. Rep ARG x -> ARG
forall x. ARG -> Rep ARG x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ARG -> Rep ARG x
from :: forall x. ARG -> Rep ARG x
$cto :: forall x. Rep ARG x -> ARG
to :: forall x. Rep ARG x -> ARG
Generic)
instance NFData ARG where
rnf :: ARG -> ()
rnf ARG
ARG = ()
instance Hashable ARG where
hashWithSalt :: Int -> ARG -> Int
hashWithSalt Int
s ARG
ARG = Int
s Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int)
instance Eq (a --> b) where
GeneralFun TypedConstantSymbol a
sym1 Term b
tm1 == :: (a --> b) -> (a --> b) -> Bool
== GeneralFun TypedConstantSymbol a
sym2 Term b
tm2 = TypedConstantSymbol a
sym1 TypedConstantSymbol a -> TypedConstantSymbol a -> Bool
forall a. Eq a => a -> a -> Bool
== TypedConstantSymbol a
sym2 Bool -> Bool -> Bool
&& Term b
tm1 Term b -> Term b -> Bool
forall a. Eq a => a -> a -> Bool
== Term b
tm2
instance Show (a --> b) where
show :: (a --> b) -> String
show (GeneralFun TypedConstantSymbol a
sym Term b
tm) = String
"\\(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypedConstantSymbol a -> String
forall a. Show a => a -> String
show TypedConstantSymbol a
sym String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Term b -> String
forall t. SupportedPrim t => Term t -> String
pformatTerm Term b
tm
instance Lift (a --> b) where
liftTyped :: forall (m :: * -> *). Quote m => (a --> b) -> Code m (a --> b)
liftTyped (GeneralFun TypedConstantSymbol a
sym Term b
tm) = [||TypedConstantSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
GeneralFun TypedConstantSymbol a
sym Term b
tm||]
instance Hashable (a --> b) where
Int
s hashWithSalt :: Int -> (a --> b) -> Int
`hashWithSalt` (GeneralFun TypedConstantSymbol a
sym Term b
tm) = Int
s Int -> TypedConstantSymbol a -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypedConstantSymbol a
sym Int -> Term b -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Term b
tm
instance NFData (a --> b) where
rnf :: (a --> b) -> ()
rnf (GeneralFun TypedConstantSymbol a
sym Term b
tm) = TypedConstantSymbol a -> ()
forall a. NFData a => a -> ()
rnf TypedConstantSymbol a
sym () -> () -> ()
forall a b. a -> b -> b
`seq` Term b -> ()
forall a. NFData a => a -> ()
rnf Term b
tm
instance
(SupportedNonFuncPrim a, SupportedPrim b) =>
SupportedPrimConstraint (a --> b)
where
type
PrimConstraint (a --> b) =
( SupportedNonFuncPrim a,
SupportedPrim b,
NonFuncPrimConstraint a,
PrimConstraint b,
SBVType (a --> b) ~ (SBV.SBV (NonFuncSBVBaseType a) -> SBVType b)
)
instance
(SupportedNonFuncPrim a, SupportedPrim b) =>
SBVRep (a --> b)
where
type
SBVType (a --> b) =
SBV.SBV (NonFuncSBVBaseType a) ->
SBVType b
pevalGeneralFunApplyTerm ::
( SupportedNonFuncPrim a,
SupportedPrim b,
SupportedPrim (a --> b)
) =>
Term (a --> b) ->
Term a ->
Term b
pevalGeneralFunApplyTerm :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b,
SupportedPrim (a --> b)) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm = (Term (a --> b) -> PartialFun (Term a) (Term b))
-> (Term (a --> b) -> Term a -> Term b)
-> Term (a --> b)
-> Term a
-> Term b
forall a b c. (a -> PartialFun b c) -> (a -> b -> c) -> a -> b -> c
totalize2 Term (a --> b) -> PartialFun (Term a) (Term b)
forall {a} {b}.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Maybe (Term b)
doPevalApplyTerm Term (a --> b) -> Term a -> Term b
forall a b f.
(SupportedPrim a, SupportedPrim b, SupportedPrim f,
PEvalApplyTerm f a b) =>
Term f -> Term a -> Term b
applyTerm
where
doPevalApplyTerm :: Term (a --> b) -> Term a -> Maybe (Term b)
doPevalApplyTerm (ConTerm Int
_ (GeneralFun TypedConstantSymbol a
arg Term b
tm)) Term a
v =
Term b -> Maybe (Term b)
forall a. a -> Maybe a
Just (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol a -> Term a -> Term b -> Term b
forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedConstantSymbol a
arg Term a
v Term b
tm
doPevalApplyTerm (ITETerm Int
_ Term Bool
c Term (a --> b)
l Term (a --> b)
r) Term a
v =
Term b -> Maybe (Term b)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term b -> Maybe (Term b)) -> Term b -> Maybe (Term b)
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term b -> Term b -> Term b
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm Term Bool
c (Term (a --> b) -> Term a -> Term b
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term (a --> b)
l Term a
v) (Term (a --> b) -> Term a -> Term b
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term (a --> b)
r Term a
v)
doPevalApplyTerm Term (a --> b)
_ Term a
_ = Maybe (Term b)
forall a. Maybe a
Nothing
instance
( SupportedPrim (a --> b),
SupportedNonFuncPrim a,
SupportedPrim b
) =>
PEvalApplyTerm (a --> b) a b
where
pevalApplyTerm :: Term (a --> b) -> Term a -> Term b
pevalApplyTerm = Term (a --> b) -> Term a -> Term b
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b,
SupportedPrim (a --> b)) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm
sbvApplyTerm :: SBVType (a --> b) -> SBVType a -> SBVType b
sbvApplyTerm SBVType (a --> b)
f SBVType a
a =
forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
Mergeable (SBVType t), Typeable (SBVType t)) =>
a)
-> a
withPrim @(a --> b) (((PrimConstraint (a --> b), SMTDefinable (SBVType (a --> b)),
Mergeable (SBVType (a --> b)), Typeable (SBVType (a --> b))) =>
SBVType b)
-> SBVType b)
-> ((PrimConstraint (a --> b), SMTDefinable (SBVType (a --> b)),
Mergeable (SBVType (a --> b)), Typeable (SBVType (a --> b))) =>
SBVType b)
-> SBVType b
forall a b. (a -> b) -> a -> b
$ forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @a (((SymVal (NonFuncSBVBaseType a), EqSymbolic (SBVType a),
Mergeable (SBVType a), SMTDefinable (SBVType a),
Mergeable (SBVType a), SBVType a ~ SBV (NonFuncSBVBaseType a),
PrimConstraint a) =>
SBVType b)
-> SBVType b)
-> ((SymVal (NonFuncSBVBaseType a), EqSymbolic (SBVType a),
Mergeable (SBVType a), SMTDefinable (SBVType a),
Mergeable (SBVType a), SBVType a ~ SBV (NonFuncSBVBaseType a),
PrimConstraint a) =>
SBVType b)
-> SBVType b
forall a b. (a -> b) -> a -> b
$ SBVType (a --> b)
SBV (NonFuncSBVBaseType a) -> SBVType b
f SBV (NonFuncSBVBaseType a)
SBVType a
a
parseGeneralFunSMTModelResult ::
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int ->
([([SBVD.CV], SBVD.CV)], SBVD.CV) ->
a --> b
parseGeneralFunSMTModelResult :: forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
Int -> ([([CV], CV)], CV) -> a --> b
parseGeneralFunSMTModelResult Int
level ([([CV], CV)]
l, CV
s) =
let sym :: Symbol
sym = Identifier -> Int -> Symbol
IndexedSymbol Identifier
"arg" Int
level
funs :: [(a, b)]
funs =
([([CV], CV)] -> b) -> (a, [([CV], CV)]) -> (a, b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second
( \[([CV], CV)]
r ->
case [([CV], CV)]
r of
[([], CV
v)] -> Int -> ([([CV], CV)], CV) -> b
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([], CV
v)
[([CV], CV)]
_ -> Int -> ([([CV], CV)], CV) -> b
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([([CV], CV)]
r, CV
s)
)
((a, [([CV], CV)]) -> (a, b)) -> [(a, [([CV], CV)])] -> [(a, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
SupportedNonFuncPrim a =>
[([CV], CV)] -> [(a, [([CV], CV)])]
partitionCVArg @a [([CV], CV)]
l
def :: b
def = Int -> ([([CV], CV)], CV) -> b
forall t. SupportedPrim t => Int -> ([([CV], CV)], CV) -> t
parseSMTModelResult (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([], CV
s)
body :: Term b
body =
(Term b -> (a, b) -> Term b) -> Term b -> [(a, b)] -> Term b
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
( \Term b
acc (a
v, b
f) ->
Term Bool -> Term b -> Term b -> Term b
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
(Term a -> Term a -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm (Symbol -> Term a
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
sym) (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v))
(b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
f)
Term b
acc
)
(b -> Term b
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm b
def)
[(a, b)]
funs
in TypedConstantSymbol a -> Term b -> a --> b
forall a b.
(SupportedNonFuncPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
buildGeneralFun (Symbol -> TypedConstantSymbol a
forall t (knd :: SymbolKind).
(SupportedPrim t, SymbolKindConstraint knd t, IsSymbolKind knd) =>
Symbol -> TypedSymbol knd t
TypedSymbol Symbol
sym) Term b
body
{-# NOINLINE generalSubstSomeTerm #-}
generalSubstSomeTerm ::
forall v.
(forall a. TypedSymbol 'AnyKind a -> Term a) ->
HS.HashSet SomeTypedConstantSymbol ->
Term v ->
Term v
generalSubstSomeTerm :: forall v.
(forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term v -> Term v
generalSubstSomeTerm forall a. TypedSymbol 'AnyKind a -> Term a
subst HashSet SomeTypedConstantSymbol
initialBoundedSymbols = (SomeTerm -> SomeTerm) -> Term v -> Term v
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
initialMemo
where
go :: forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go :: forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a = case SomeTerm -> SomeTerm
memo (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
forall a. Term a -> SomeTerm
someTerm Term a
a of
SomeTerm Term a
v -> Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
v
initialMemo :: SomeTerm -> SomeTerm
initialMemo :: SomeTerm -> SomeTerm
initialMemo = (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
initialMemo HashSet SomeTypedConstantSymbol
initialBoundedSymbols)
{-# NOINLINE initialMemo #-}
goSome ::
(SomeTerm -> SomeTerm) ->
HS.HashSet SomeTypedConstantSymbol ->
SomeTerm ->
SomeTerm
goSome :: (SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs c :: SomeTerm
c@(SomeTerm (ConTerm Int
_ a
cv :: Term x)) =
case (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep x) 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 TypedConstantSymbol b
sym (Term b
tm :: Term r) ->
let newmemo :: SomeTerm -> SomeTerm
newmemo =
(SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo
( (SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome
SomeTerm -> SomeTerm
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)
)
{-# NOINLINE newmemo #-}
in 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
$ TypedConstantSymbol b -> Term b -> b --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
GeneralFun TypedConstantSymbol b
sym ((SomeTerm -> SomeTerm) -> Term b -> Term b
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
newmemo Term b
tm)
Maybe (a :~~: (-->))
Nothing -> SomeTerm
c
TypeRep a
_ -> SomeTerm
c
goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs c :: SomeTerm
c@(SomeTerm ((SymTerm Int
_ TypedSymbol 'AnyKind a
sym) :: Term a)) =
case TypedSymbol 'AnyKind 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 TypedSymbol 'AnyKind a
sym of
Just TypedSymbol 'ConstantKind a
sym' | 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 -> SomeTerm
c
Maybe (TypedSymbol 'ConstantKind a)
_ -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ TypedSymbol 'AnyKind a -> Term a
forall a. TypedSymbol 'AnyKind a -> Term a
subst TypedSymbol 'AnyKind a
sym
goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ForallTerm Int
_ TypedSymbol 'ConstantKind t1
tsym Term Bool
b)) =
let newmemo :: SomeTerm -> SomeTerm
newmemo =
(SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
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
tsym) HashSet SomeTypedConstantSymbol
bs))
{-# NOINLINE newmemo #-}
in (SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool) -> Term Bool -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
newmemo (TypedSymbol 'ConstantKind t1 -> Term Bool -> Term Bool
forall t.
(SupportedNonFuncPrim t, Typeable t) =>
TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
forallTerm TypedSymbol 'ConstantKind t1
tsym) Term Bool
b
goSome SomeTerm -> SomeTerm
_ HashSet SomeTypedConstantSymbol
bs (SomeTerm (ExistsTerm Int
_ TypedSymbol 'ConstantKind t1
tsym Term Bool
b)) =
let newmemo :: SomeTerm -> SomeTerm
newmemo =
(SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo ((SomeTerm -> SomeTerm)
-> HashSet SomeTypedConstantSymbol -> SomeTerm -> SomeTerm
goSome SomeTerm -> SomeTerm
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
tsym) HashSet SomeTypedConstantSymbol
bs))
{-# NOINLINE newmemo #-}
in (SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool) -> Term Bool -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
newmemo (TypedSymbol 'ConstantKind t1 -> Term Bool -> Term Bool
forall t.
(SupportedNonFuncPrim t, Typeable t) =>
TypedSymbol 'ConstantKind t -> Term Bool -> Term Bool
existsTerm TypedSymbol 'ConstantKind t1
tsym) Term Bool
b
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (UnaryTerm Int
_ tag
tag (Term arg
arg :: Term a))) =
(SomeTerm -> SomeTerm)
-> (Term arg -> Term a) -> Term arg -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (tag -> Term arg -> Term a
forall tag arg t.
(UnaryOp tag arg t, Typeable tag, Typeable t) =>
tag -> Term arg -> Term t
pevalUnary tag
tag) Term arg
arg
goSome
SomeTerm -> SomeTerm
memo
HashSet SomeTypedConstantSymbol
_
(SomeTerm (BinaryTerm Int
_ tag
tag (Term arg1
arg1 :: Term a1) (Term arg2
arg2 :: Term a2))) =
(SomeTerm -> SomeTerm)
-> (Term arg1 -> Term arg2 -> Term a)
-> Term arg1
-> Term arg2
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (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
pevalBinary tag
tag) Term arg1
arg1 Term arg2
arg2
goSome
SomeTerm -> SomeTerm
memo
HashSet SomeTypedConstantSymbol
_
( SomeTerm
( TernaryTerm
Int
_
tag
tag
(Term arg1
arg1 :: Term a1)
(Term arg2
arg2 :: Term a2)
(Term arg3
arg3 :: Term a3)
)
) = do
(SomeTerm -> SomeTerm)
-> (Term arg1 -> Term arg2 -> Term arg3 -> Term a)
-> Term arg1
-> Term arg2
-> Term arg3
-> SomeTerm
forall {a} {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo (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
pevalTernary tag
tag) Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (NotTerm Int
_ Term Bool
arg)) =
(SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool) -> Term Bool -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term Bool -> Term Bool
pevalNotTerm Term Bool
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool -> Term Bool)
-> Term Bool
-> Term Bool
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
arg1 Term Bool
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term Bool -> Term Bool -> Term Bool)
-> Term Bool
-> Term Bool
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
arg1 Term Bool
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (EqTerm Int
_ Term t1
arg1 Term t1
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term t1 -> Term t1 -> Term Bool)
-> Term t1
-> Term t1
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term t1 -> Term t1 -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term t1
arg1 Term t1
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (DistinctTerm Int
_ NonEmpty (Term t1)
args)) =
Term Bool -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term Bool -> SomeTerm) -> Term Bool -> SomeTerm
forall a b. (a -> b) -> a -> b
$ NonEmpty (Term t1) -> Term Bool
forall t. SupportedPrim t => NonEmpty (Term t) -> Term Bool
pevalDistinctTerm ((Term t1 -> Term t1) -> NonEmpty (Term t1) -> NonEmpty (Term t1)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SomeTerm -> SomeTerm) -> Term t1 -> Term t1
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo) NonEmpty (Term t1)
args)
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ITETerm Int
_ Term Bool
cond Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term Bool -> Term a -> Term a -> Term a)
-> Term Bool
-> Term a
-> Term a
-> SomeTerm
forall {a} {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo Term Bool -> Term a -> Term a -> Term a
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm Term Bool
cond Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AddNumTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (NegNumTerm Int
_ Term a
arg)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (MulNumTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AbsNumTerm Int
_ Term a
arg)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (SignumNumTerm Int
_ Term a
arg)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (LtOrdTerm Int
_ Term t1
arg1 Term t1
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term t1 -> Term t1 -> Term Bool)
-> Term t1
-> Term t1
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLtOrdTerm Term t1
arg1 Term t1
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (LeOrdTerm Int
_ Term t1
arg1 Term t1
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term t1 -> Term t1 -> Term Bool)
-> Term t1
-> Term t1
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm Term t1
arg1 Term t1
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (AndBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalAndBitsTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (OrBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalOrBitsTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (XorBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalXorBitsTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ComplementBitsTerm Int
_ Term a
arg)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ShiftLeftTerm Int
_ Term a
arg Term a
n)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term a
arg Term a
n
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RotateLeftTerm Int
_ Term a
arg Term a
n)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm Term a
arg Term a
n
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ShiftRightTerm Int
_ Term a
arg Term a
n)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term a
arg Term a
n
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RotateRightTerm Int
_ Term a
arg Term a
n)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateRightTerm Term a
arg Term a
n
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BitCastTerm Int
_ (Term a
arg :: Term a) :: Term r)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (forall a b. PEvalBitCastTerm a b => Term a -> Term b
pevalBitCastTerm @a @r) Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BitCastOrTerm Int
_ (Term a
d :: term r) (Term a
arg :: Term a) :: Term r)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (forall a b. PEvalBitCastOrTerm a b => Term b -> Term a -> Term b
pevalBitCastOrTerm @a @r) Term a
d Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BVConcatTerm Int
_ Term (bv l)
arg1 Term (bv r)
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term (bv l) -> Term (bv r) -> Term (bv (l + r)))
-> Term (bv l)
-> Term (bv r)
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm Term (bv l)
arg1 Term (bv r)
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BVSelectTerm Int
_ TypeRep ix
ix TypeRep w
w Term (bv n)
arg)) =
(SomeTerm -> SomeTerm)
-> (Term (bv n) -> Term (bv w)) -> Term (bv n) -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
forall (n :: Natural) (ix :: Natural) (w :: Natural)
(p :: Natural -> *) (q :: Natural -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
(w :: Natural) (p :: Natural -> *) (q :: Natural -> *).
(PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n,
1 <= w, (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm TypeRep ix
ix TypeRep w
w) Term (bv n)
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (BVExtendTerm Int
_ Bool
n TypeRep r
signed Term (bv l)
arg)) =
(SomeTerm -> SomeTerm)
-> (Term (bv l) -> Term (bv r)) -> Term (bv l) -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
(proxy :: Natural -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
n TypeRep r
signed) Term (bv l)
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ApplyTerm Int
_ Term f
f Term a
arg)) =
(SomeTerm -> SomeTerm)
-> (Term f -> Term a -> Term a) -> Term f -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term f -> Term a -> Term a
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term f
f Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (DivIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalDivIntegralTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (ModIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalModIntegralTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (QuotIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalQuotIntegralTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RemIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalRemIntegralTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPTraitTerm Int
_ FPTrait
trait Term (FP eb sb)
arg)) =
(SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term Bool) -> Term (FP eb sb) -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FPTrait -> Term (FP eb sb) -> Term Bool
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPTrait -> Term (FP eb sb) -> Term Bool
pevalFPTraitTerm FPTrait
trait) Term (FP eb sb)
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FdivTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalFractionalTerm t => Term t -> Term t -> Term t
pevalFdivTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (RecipTerm Int
_ Term a
arg)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
forall t. PEvalFractionalTerm t => Term t -> Term t
pevalRecipTerm Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FloatingUnaryTerm Int
_ FloatingUnaryOp
op Term a
arg)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FloatingUnaryOp -> Term a -> Term a
forall t.
PEvalFloatingTerm t =>
FloatingUnaryOp -> Term t -> Term t
pevalFloatingUnaryTerm FloatingUnaryOp
op) Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (PowerTerm Int
_ Term a
arg1 Term a
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
forall t. PEvalFloatingTerm t => Term t -> Term t -> Term t
pevalPowerTerm Term a
arg1 Term a
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPUnaryTerm Int
_ FPUnaryOp
op Term (FP eb sb)
arg)) =
(SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPUnaryTerm FPUnaryOp
op) Term (FP eb sb)
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPBinaryTerm Int
_ FPBinaryOp
op Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb)) =>
FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPBinaryTerm FPBinaryOp
op) Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPRoundingUnaryTerm Int
_ FPRoundingUnaryOp
op Term FPRoundingMode
mode Term (FP eb sb)
arg)) =
(SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb),
SupportedPrim FPRoundingMode) =>
FPRoundingUnaryOp
-> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb)
pevalFPRoundingUnaryTerm FPRoundingUnaryOp
op Term FPRoundingMode
mode) Term (FP eb sb)
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPRoundingBinaryTerm Int
_ FPRoundingBinaryOp
op Term FPRoundingMode
mode Term (FP eb sb)
arg1 Term (FP eb sb)
arg2)) =
(SomeTerm -> SomeTerm)
-> (Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb))
-> Term (FP eb sb)
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb),
SupportedPrim FPRoundingMode) =>
FPRoundingBinaryOp
-> Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPRoundingBinaryTerm FPRoundingBinaryOp
op Term FPRoundingMode
mode) Term (FP eb sb)
arg1 Term (FP eb sb)
arg2
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FPFMATerm Int
_ Term FPRoundingMode
mode Term (FP eb sb)
arg1 Term (FP eb sb)
arg2 Term (FP eb sb)
arg3)) =
Term (FP eb sb) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (FP eb sb) -> SomeTerm) -> Term (FP eb sb) -> SomeTerm
forall a b. (a -> b) -> a -> b
$
Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
forall (eb :: Natural) (sb :: Natural).
(ValidFP eb sb, SupportedPrim (FP eb sb),
SupportedPrim FPRoundingMode) =>
Term FPRoundingMode
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
-> Term (FP eb sb)
pevalFPFMATerm
((SomeTerm -> SomeTerm)
-> Term FPRoundingMode -> Term FPRoundingMode
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term FPRoundingMode
mode)
((SomeTerm -> SomeTerm) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term (FP eb sb)
arg1)
((SomeTerm -> SomeTerm) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term (FP eb sb)
arg2)
((SomeTerm -> SomeTerm) -> Term (FP eb sb) -> Term (FP eb sb)
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term (FP eb sb)
arg3)
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FromIntegralTerm Int
_ (Term a
arg :: Term a) :: Term b)) =
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
forall {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo (forall a b. PEvalFromIntegralTerm a b => Term a -> Term b
pevalFromIntegralTerm @a @b) Term a
arg
goSome SomeTerm -> SomeTerm
memo HashSet SomeTypedConstantSymbol
_ (SomeTerm (FromFPOrTerm Int
_ Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg)) =
(SomeTerm -> SomeTerm)
-> (Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a)
-> Term a
-> Term FPRoundingMode
-> Term (FP eb sb)
-> SomeTerm
forall {a} {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
forall (eb :: Natural) (sb :: Natural).
ValidFP eb sb =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
forall a (eb :: Natural) (sb :: Natural).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term a -> Term FPRoundingMode -> Term (FP eb sb) -> Term a
pevalFromFPOrTerm Term a
d Term FPRoundingMode
mode Term (FP eb sb)
arg
goSome
SomeTerm -> SomeTerm
memo
HashSet SomeTypedConstantSymbol
_
(SomeTerm (ToFPTerm Int
_ Term FPRoundingMode
mode (Term a
arg :: Term a) (Proxy eb
_ :: p eb) (Proxy sb
_ :: q sb))) =
(SomeTerm -> SomeTerm)
-> (Term FPRoundingMode -> Term a -> Term (FP eb sb))
-> Term FPRoundingMode
-> Term a
-> SomeTerm
forall {a} {a} {a}.
SupportedPrim a =>
(SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo (forall a (eb :: Natural) (sb :: Natural).
(PEvalIEEEFPConvertibleTerm a, ValidFP eb sb) =>
Term FPRoundingMode -> Term a -> Term (FP eb sb)
pevalToFPTerm @a @eb @sb) Term FPRoundingMode
mode Term a
arg
goUnary :: (SomeTerm -> SomeTerm) -> (Term a -> Term a) -> Term a -> SomeTerm
goUnary SomeTerm -> SomeTerm
memo Term a -> Term a
f Term a
a = 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
f ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a)
goBinary :: (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
goBinary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a
f Term a
a Term a
b = 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
f ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a) ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
b)
goTernary :: (SomeTerm -> SomeTerm)
-> (Term a -> Term a -> Term a -> Term a)
-> Term a
-> Term a
-> Term a
-> SomeTerm
goTernary SomeTerm -> SomeTerm
memo Term a -> Term a -> Term a -> Term a
f Term a
a Term a
b Term a
c =
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 -> Term a
f ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
a) ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
b) ((SomeTerm -> SomeTerm) -> Term a -> Term a
forall a. (SomeTerm -> SomeTerm) -> Term a -> Term a
go SomeTerm -> SomeTerm
memo Term a
c)
substTerm ::
forall knd a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a ->
Term a ->
Term b ->
Term b
substTerm :: forall (knd :: SymbolKind) a b.
(SupportedPrim a, SupportedPrim b, IsSymbolKind knd) =>
TypedSymbol knd a -> Term a -> Term b -> Term b
substTerm TypedSymbol knd a
sym Term a
a =
(forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term b -> Term b
forall v.
(forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term v -> Term v
generalSubstSomeTerm
( \t :: TypedSymbol 'AnyKind a
t@(TypedSymbol Symbol
t') ->
if TypedSymbol knd a -> TypedSymbol 'AnyKind a -> Bool
forall (ta :: SymbolKind) a (tb :: SymbolKind) b.
TypedSymbol ta a -> TypedSymbol tb b -> Bool
eqHeteroSymbol TypedSymbol knd a
sym TypedSymbol 'AnyKind a
t then Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
a else Symbol -> Term a
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm Symbol
t'
)
HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty
supportedPrimFunUpTo
[|buildGeneralFun (TypedSymbol "a") (conTerm defaultValue)|]
[|parseGeneralFunSMTModelResult|]
( \tyVars ->
[|
translateTypeError
(Just "x")
( typeRep ::
TypeRep
$( foldl1 (\fty ty -> [t|$ty --> $fty|])
. reverse
$ tyVars
)
)
|]
)
"GeneralFun"
"gfunc"
''(-->)
8