{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( constructUnary,
constructBinary,
constructTernary,
conTerm,
symTerm,
ssymTerm,
isymTerm,
sinfosymTerm,
iinfosymTerm,
notTerm,
orTerm,
andTerm,
eqvTerm,
iteTerm,
addNumTerm,
uminusNumTerm,
timesNumTerm,
absNumTerm,
signumNumTerm,
ltNumTerm,
leNumTerm,
andBitsTerm,
orBitsTerm,
xorBitsTerm,
complementBitsTerm,
shiftLeftTerm,
shiftRightTerm,
rotateLeftTerm,
rotateRightTerm,
toSignedTerm,
toUnsignedTerm,
bvconcatTerm,
bvselectTerm,
bvextendTerm,
bvsignExtendTerm,
bvzeroExtendTerm,
tabularFunApplyTerm,
generalFunApplyTerm,
divIntegralTerm,
modIntegralTerm,
quotIntegralTerm,
remIntegralTerm,
divBoundedIntegralTerm,
modBoundedIntegralTerm,
quotBoundedIntegralTerm,
remBoundedIntegralTerm,
)
where
import Control.DeepSeq (NFData)
import Data.Array ((!))
import Data.Bits (Bits, FiniteBits)
import qualified Data.HashMap.Strict as M
import Data.Hashable (Hashable (hash))
import Data.IORef (atomicModifyIORef')
import Data.Interned
( Interned (Uninterned, cache, cacheWidth, describe, identify),
)
import Data.Interned.Internal
( Cache (getCache),
CacheState (CacheState),
)
import qualified Data.Text as T
import GHC.IO (unsafeDupablePerformIO)
import GHC.TypeNats (KnownNat, type (+), type (<=))
import Grisette.Core.Data.Class.BitVector
( SizedBV,
)
import Grisette.Core.Data.Class.SignConversion (SignConversion)
import Grisette.Core.Data.Class.SymRotate (SymRotate)
import Grisette.Core.Data.Class.SymShift (SymShift)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( BinaryOp,
SupportedPrim,
Term,
TernaryOp,
TypedSymbol (IndexedSymbol, SimpleSymbol, WithInfo),
UTerm
( UAbsNumTerm,
UAddNumTerm,
UAndBitsTerm,
UAndTerm,
UBVConcatTerm,
UBVExtendTerm,
UBVSelectTerm,
UBinaryTerm,
UComplementBitsTerm,
UConTerm,
UDivBoundedIntegralTerm,
UDivIntegralTerm,
UEqvTerm,
UGeneralFunApplyTerm,
UITETerm,
ULENumTerm,
ULTNumTerm,
UModBoundedIntegralTerm,
UModIntegralTerm,
UNotTerm,
UOrBitsTerm,
UOrTerm,
UQuotBoundedIntegralTerm,
UQuotIntegralTerm,
URemBoundedIntegralTerm,
URemIntegralTerm,
URotateLeftTerm,
URotateRightTerm,
UShiftLeftTerm,
UShiftRightTerm,
USignumNumTerm,
USymTerm,
UTabularFunApplyTerm,
UTernaryTerm,
UTimesNumTerm,
UToSignedTerm,
UToUnsignedTerm,
UUMinusNumTerm,
UUnaryTerm,
UXorBitsTerm
),
UnaryOp,
type (-->),
)
import Grisette.IR.SymPrim.Data.TabularFun
( type (=->),
)
import Language.Haskell.TH.Syntax (Lift)
import Type.Reflection (Typeable, typeRep)
internTerm :: forall t. (SupportedPrim t) => Uninterned (Term t) -> Term t
internTerm :: forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm !Uninterned (Term t)
bt = IO (Term t) -> Term t
forall a. IO a -> a
unsafeDupablePerformIO (IO (Term t) -> Term t) -> IO (Term t) -> Term t
forall a b. (a -> b) -> a -> b
$ IORef (CacheState (Term t))
-> (CacheState (Term t) -> (CacheState (Term t), Term t))
-> IO (Term t)
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (CacheState (Term t))
slot CacheState (Term t) -> (CacheState (Term t), Term t)
go
where
slot :: IORef (CacheState (Term t))
slot = Cache (Term t) -> Array Int (IORef (CacheState (Term t)))
forall t. Cache t -> Array Int (IORef (CacheState t))
getCache Cache (Term t)
forall t. Interned t => Cache t
cache Array Int (IORef (CacheState (Term t)))
-> Int -> IORef (CacheState (Term t))
forall i e. Ix i => Array i e -> i -> e
! Int
r
!dt :: Description (Term t)
dt = Uninterned (Term t) -> Description (Term t)
forall t. Interned t => Uninterned t -> Description t
describe Uninterned (Term t)
bt
!hdt :: Int
hdt = Description (Term t) -> Int
forall a. Hashable a => a -> Int
hash Description (Term t)
dt
!wid :: Int
wid = Description (Term t) -> Int
forall t (p :: * -> *). Interned t => p t -> Int
forall (p :: * -> *). p (Term t) -> Int
cacheWidth Description (Term t)
dt
r :: Int
r = Int
hdt Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
wid
go :: CacheState (Term t) -> (CacheState (Term t), Term t)
go (CacheState Int
i HashMap (Description (Term t)) (Term t)
m) = case Description (Term t)
-> HashMap (Description (Term t)) (Term t) -> Maybe (Term t)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Description (Term t)
dt HashMap (Description (Term t)) (Term t)
m of
Maybe (Term t)
Nothing -> let t :: Term t
t = Int -> Uninterned (Term t) -> Term t
forall t. Interned t => Int -> Uninterned t -> t
identify (Int
wid Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r) Uninterned (Term t)
bt in (Int
-> HashMap (Description (Term t)) (Term t) -> CacheState (Term t)
forall t. Int -> HashMap (Description t) t -> CacheState t
CacheState (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Description (Term t)
-> Term t
-> HashMap (Description (Term t)) (Term t)
-> HashMap (Description (Term t)) (Term t)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert Description (Term t)
dt Term t
t HashMap (Description (Term t)) (Term t)
m), Term t
t)
Just Term t
t -> (Int
-> HashMap (Description (Term t)) (Term t) -> CacheState (Term t)
forall t. Int -> HashMap (Description t) t -> CacheState t
CacheState Int
i HashMap (Description (Term t)) (Term t)
m, Term t
t)
constructUnary ::
forall tag arg t.
(SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t, Show tag) =>
tag ->
Term arg ->
Term t
constructUnary :: forall tag arg t.
(SupportedPrim t, UnaryOp tag arg t, Typeable tag, Typeable t,
Show tag) =>
tag -> Term arg -> Term t
constructUnary tag
tag Term arg
tm = let x :: Term t
x = Uninterned (Term t) -> Term t
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term t) -> Term t) -> Uninterned (Term t) -> Term t
forall a b. (a -> b) -> a -> b
$ tag -> Term arg -> UTerm t
forall tag arg t. UnaryOp tag arg t => tag -> Term arg -> UTerm t
UUnaryTerm tag
tag Term arg
tm in Term t
x
{-# INLINE constructUnary #-}
constructBinary ::
forall tag arg1 arg2 t.
(SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t, Show tag) =>
tag ->
Term arg1 ->
Term arg2 ->
Term t
constructBinary :: forall tag arg1 arg2 t.
(SupportedPrim t, BinaryOp tag arg1 arg2 t, Typeable tag,
Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term t
constructBinary tag
tag Term arg1
tm1 Term arg2
tm2 = Uninterned (Term t) -> Term t
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term t) -> Term t) -> Uninterned (Term t) -> Term t
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> UTerm t
forall tag arg1 arg2 t.
BinaryOp tag arg1 arg2 t =>
tag -> Term arg1 -> Term arg2 -> UTerm t
UBinaryTerm tag
tag Term arg1
tm1 Term arg2
tm2
{-# INLINE constructBinary #-}
constructTernary ::
forall tag arg1 arg2 arg3 t.
(SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t, Show tag) =>
tag ->
Term arg1 ->
Term arg2 ->
Term arg3 ->
Term t
constructTernary :: forall tag arg1 arg2 arg3 t.
(SupportedPrim t, TernaryOp tag arg1 arg2 arg3 t, Typeable tag,
Typeable t, Show tag) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
constructTernary tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3 = Uninterned (Term t) -> Term t
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term t) -> Term t) -> Uninterned (Term t) -> Term t
forall a b. (a -> b) -> a -> b
$ tag -> Term arg1 -> Term arg2 -> Term arg3 -> UTerm t
forall tag arg1 arg2 arg3 t.
TernaryOp tag arg1 arg2 arg3 t =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> UTerm t
UTernaryTerm tag
tag Term arg1
tm1 Term arg2
tm2 Term arg3
tm3
{-# INLINE constructTernary #-}
conTerm :: (SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) => t -> Term t
conTerm :: forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm t
t = Uninterned (Term t) -> Term t
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term t) -> Term t) -> Uninterned (Term t) -> Term t
forall a b. (a -> b) -> a -> b
$ t -> UTerm t
forall t. SupportedPrim t => t -> UTerm t
UConTerm t
t
{-# INLINE conTerm #-}
symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm :: forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol t
t = Uninterned (Term t) -> Term t
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term t) -> Term t) -> Uninterned (Term t) -> Term t
forall a b. (a -> b) -> a -> b
$ TypedSymbol t -> UTerm t
forall t. SupportedPrim t => TypedSymbol t -> UTerm t
USymTerm TypedSymbol t
t
{-# INLINE symTerm #-}
ssymTerm :: (SupportedPrim t, Typeable t) => T.Text -> Term t
ssymTerm :: forall t. (SupportedPrim t, Typeable t) => Text -> Term t
ssymTerm = TypedSymbol t -> Term t
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm (TypedSymbol t -> Term t)
-> (Text -> TypedSymbol t) -> Text -> Term t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> TypedSymbol t
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol
{-# INLINE ssymTerm #-}
isymTerm :: (SupportedPrim t, Typeable t) => T.Text -> Int -> Term t
isymTerm :: forall t. (SupportedPrim t, Typeable t) => Text -> Int -> Term t
isymTerm Text
str Int
idx = TypedSymbol t -> Term t
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm (TypedSymbol t -> Term t) -> TypedSymbol t -> Term t
forall a b. (a -> b) -> a -> b
$ Text -> Int -> TypedSymbol t
forall t. SupportedPrim t => Text -> Int -> TypedSymbol t
IndexedSymbol Text
str Int
idx
{-# INLINE isymTerm #-}
sinfosymTerm ::
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
T.Text ->
a ->
Term t
sinfosymTerm :: forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
Show a, Hashable a) =>
Text -> a -> Term t
sinfosymTerm Text
s a
info = TypedSymbol t -> Term t
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm (TypedSymbol t -> Term t) -> TypedSymbol t -> Term t
forall a b. (a -> b) -> a -> b
$ TypedSymbol t -> a -> TypedSymbol t
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (Text -> TypedSymbol t
forall t. SupportedPrim t => Text -> TypedSymbol t
SimpleSymbol Text
s) a
info
{-# INLINE sinfosymTerm #-}
iinfosymTerm ::
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) =>
T.Text ->
Int ->
a ->
Term t
iinfosymTerm :: forall t a.
(SupportedPrim t, Typeable t, Typeable a, Ord a, Lift a, NFData a,
Show a, Hashable a) =>
Text -> Int -> a -> Term t
iinfosymTerm Text
str Int
idx a
info = TypedSymbol t -> Term t
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm (TypedSymbol t -> Term t) -> TypedSymbol t -> Term t
forall a b. (a -> b) -> a -> b
$ TypedSymbol t -> a -> TypedSymbol t
forall t a.
(SupportedPrim t, Typeable a, Ord a, Lift a, NFData a, Show a,
Hashable a) =>
TypedSymbol t -> a -> TypedSymbol t
WithInfo (Text -> Int -> TypedSymbol t
forall t. SupportedPrim t => Text -> Int -> TypedSymbol t
IndexedSymbol Text
str Int
idx) a
info
{-# INLINE iinfosymTerm #-}
notTerm :: Term Bool -> Term Bool
notTerm :: Term Bool -> Term Bool
notTerm = Uninterned (Term Bool) -> Term Bool
UTerm Bool -> Term Bool
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (UTerm Bool -> Term Bool)
-> (Term Bool -> UTerm Bool) -> Term Bool -> Term Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term Bool -> UTerm Bool
UNotTerm
{-# INLINE notTerm #-}
orTerm :: Term Bool -> Term Bool -> Term Bool
orTerm :: Term Bool -> Term Bool -> Term Bool
orTerm Term Bool
l Term Bool
r = Uninterned (Term Bool) -> Term Bool
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term Bool) -> Term Bool)
-> Uninterned (Term Bool) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> UTerm Bool
UOrTerm Term Bool
l Term Bool
r
{-# INLINE orTerm #-}
andTerm :: Term Bool -> Term Bool -> Term Bool
andTerm :: Term Bool -> Term Bool -> Term Bool
andTerm Term Bool
l Term Bool
r = Uninterned (Term Bool) -> Term Bool
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term Bool) -> Term Bool)
-> Uninterned (Term Bool) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool -> UTerm Bool
UAndTerm Term Bool
l Term Bool
r
{-# INLINE andTerm #-}
eqvTerm :: (SupportedPrim a) => Term a -> Term a -> Term Bool
eqvTerm :: forall a. SupportedPrim a => Term a -> Term a -> Term Bool
eqvTerm Term a
l Term a
r = Uninterned (Term Bool) -> Term Bool
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term Bool) -> Term Bool)
-> Uninterned (Term Bool) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm Bool
forall t1. SupportedPrim t1 => Term t1 -> Term t1 -> UTerm Bool
UEqvTerm Term a
l Term a
r
{-# INLINE eqvTerm #-}
iteTerm :: (SupportedPrim a) => Term Bool -> Term a -> Term a -> Term a
iteTerm :: forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
iteTerm Term Bool
c Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term a -> Term a -> UTerm a
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> UTerm t
UITETerm Term Bool
c Term a
l Term a
r
{-# INLINE iteTerm #-}
addNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
addNumTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t. (SupportedPrim t, Num t) => Term t -> Term t -> UTerm t
UAddNumTerm Term a
l Term a
r
{-# INLINE addNumTerm #-}
uminusNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
uminusNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a
uminusNumTerm = Uninterned (Term a) -> Term a
UTerm a -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (UTerm a -> Term a) -> (Term a -> UTerm a) -> Term a -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> UTerm a
forall t. (SupportedPrim t, Num t) => Term t -> UTerm t
UUMinusNumTerm
{-# INLINE uminusNumTerm #-}
timesNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a -> Term a
timesNumTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t. (SupportedPrim t, Num t) => Term t -> Term t -> UTerm t
UTimesNumTerm Term a
l Term a
r
{-# INLINE timesNumTerm #-}
absNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
absNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a
absNumTerm = Uninterned (Term a) -> Term a
UTerm a -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (UTerm a -> Term a) -> (Term a -> UTerm a) -> Term a -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> UTerm a
forall t. (SupportedPrim t, Num t) => Term t -> UTerm t
UAbsNumTerm
{-# INLINE absNumTerm #-}
signumNumTerm :: (SupportedPrim a, Num a) => Term a -> Term a
signumNumTerm :: forall a. (SupportedPrim a, Num a) => Term a -> Term a
signumNumTerm = Uninterned (Term a) -> Term a
UTerm a -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (UTerm a -> Term a) -> (Term a -> UTerm a) -> Term a -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> UTerm a
forall t. (SupportedPrim t, Num t) => Term t -> UTerm t
USignumNumTerm
{-# INLINE signumNumTerm #-}
ltNumTerm :: (SupportedPrim a, Num a, Ord a) => Term a -> Term a -> Term Bool
ltNumTerm :: forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
ltNumTerm Term a
l Term a
r = Uninterned (Term Bool) -> Term Bool
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term Bool) -> Term Bool)
-> Uninterned (Term Bool) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm Bool
forall t1.
(SupportedPrim t1, Num t1, Ord t1) =>
Term t1 -> Term t1 -> UTerm Bool
ULTNumTerm Term a
l Term a
r
{-# INLINE ltNumTerm #-}
leNumTerm :: (SupportedPrim a, Num a, Ord a) => Term a -> Term a -> Term Bool
leNumTerm :: forall a.
(SupportedPrim a, Num a, Ord a) =>
Term a -> Term a -> Term Bool
leNumTerm Term a
l Term a
r = Uninterned (Term Bool) -> Term Bool
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term Bool) -> Term Bool)
-> Uninterned (Term Bool) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm Bool
forall t1.
(SupportedPrim t1, Num t1, Ord t1) =>
Term t1 -> Term t1 -> UTerm Bool
ULENumTerm Term a
l Term a
r
{-# INLINE leNumTerm #-}
andBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
andBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
andBitsTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t. (SupportedPrim t, Bits t) => Term t -> Term t -> UTerm t
UAndBitsTerm Term a
l Term a
r
{-# INLINE andBitsTerm #-}
orBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
orBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
orBitsTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t. (SupportedPrim t, Bits t) => Term t -> Term t -> UTerm t
UOrBitsTerm Term a
l Term a
r
{-# INLINE orBitsTerm #-}
xorBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
xorBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
xorBitsTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t. (SupportedPrim t, Bits t) => Term t -> Term t -> UTerm t
UXorBitsTerm Term a
l Term a
r
{-# INLINE xorBitsTerm #-}
complementBitsTerm :: (SupportedPrim a, Bits a) => Term a -> Term a
complementBitsTerm :: forall a. (SupportedPrim a, Bits a) => Term a -> Term a
complementBitsTerm = Uninterned (Term a) -> Term a
UTerm a -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (UTerm a -> Term a) -> (Term a -> UTerm a) -> Term a -> Term a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term a -> UTerm a
forall t. (SupportedPrim t, Bits t) => Term t -> UTerm t
UComplementBitsTerm
{-# INLINE complementBitsTerm #-}
shiftLeftTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymShift a) => Term a -> Term a -> Term a
shiftLeftTerm :: forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
shiftLeftTerm Term a
t Term a
n = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymShift t) =>
Term t -> Term t -> UTerm t
UShiftLeftTerm Term a
t Term a
n
{-# INLINE shiftLeftTerm #-}
shiftRightTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymShift a) => Term a -> Term a -> Term a
shiftRightTerm :: forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
shiftRightTerm Term a
t Term a
n = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymShift t) =>
Term t -> Term t -> UTerm t
UShiftRightTerm Term a
t Term a
n
{-# INLINE shiftRightTerm #-}
rotateLeftTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymRotate a) => Term a -> Term a -> Term a
rotateLeftTerm :: forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
rotateLeftTerm Term a
t Term a
n = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymRotate t) =>
Term t -> Term t -> UTerm t
URotateLeftTerm Term a
t Term a
n
{-# INLINE rotateLeftTerm #-}
rotateRightTerm :: (SupportedPrim a, Integral a, FiniteBits a, SymRotate a) => Term a -> Term a -> Term a
rotateRightTerm :: forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
rotateRightTerm Term a
t Term a
n = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t, FiniteBits t, SymRotate t) =>
Term t -> Term t -> UTerm t
URotateRightTerm Term a
t Term a
n
{-# INLINE rotateRightTerm #-}
toSignedTerm ::
( SupportedPrim u,
SupportedPrim s,
SignConversion u s
) =>
Term u ->
Term s
toSignedTerm :: forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term u -> Term s
toSignedTerm = Uninterned (Term s) -> Term s
UTerm s -> Term s
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (UTerm s -> Term s) -> (Term u -> UTerm s) -> Term u -> Term s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term u -> UTerm s
forall u t.
(SupportedPrim u, SupportedPrim t, SignConversion u t) =>
Term u -> UTerm t
UToSignedTerm
toUnsignedTerm ::
( SupportedPrim u,
SupportedPrim s,
SignConversion u s
) =>
Term s ->
Term u
toUnsignedTerm :: forall u s.
(SupportedPrim u, SupportedPrim s, SignConversion u s) =>
Term s -> Term u
toUnsignedTerm = Uninterned (Term u) -> Term u
UTerm u -> Term u
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (UTerm u -> Term u) -> (Term s -> UTerm u) -> Term s -> Term u
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term s -> UTerm u
forall t s.
(SupportedPrim t, SupportedPrim s, SignConversion t s) =>
Term s -> UTerm t
UToUnsignedTerm
bvconcatTerm ::
( forall n. (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))
bvconcatTerm :: 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))
bvconcatTerm Term (bv a)
l Term (bv b)
r = Uninterned (Term (bv (a + b))) -> Term (bv (a + b))
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term (bv (a + b))) -> Term (bv (a + b)))
-> Uninterned (Term (bv (a + b))) -> Term (bv (a + b))
forall a b. (a -> b) -> a -> b
$ Term (bv a) -> Term (bv b) -> UTerm (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) -> UTerm (bv (a + b))
UBVConcatTerm Term (bv a)
l Term (bv b)
r
{-# INLINE bvconcatTerm #-}
bvselectTerm ::
forall bv n ix w p q.
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
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)
bvselectTerm :: forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
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)
bvselectTerm p ix
_ q w
_ Term (bv n)
v = Uninterned (Term (bv w)) -> Term (bv w)
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term (bv w)) -> Term (bv w))
-> Uninterned (Term (bv w)) -> Term (bv w)
forall a b. (a -> b) -> a -> b
$ TypeRep ix -> TypeRep w -> Term (bv n) -> UTerm (bv w)
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: 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) =>
TypeRep ix -> TypeRep w -> Term (bv n) -> UTerm (bv w)
UBVSelectTerm (forall (a :: Nat). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @ix) (forall (a :: Nat). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @w) Term (bv n)
v
{-# INLINE bvselectTerm #-}
bvextendTerm ::
forall bv l r proxy.
( forall n. (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)
bvextendTerm :: forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: 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)
bvextendTerm Bool
signed proxy r
_ Term (bv l)
v = Uninterned (Term (bv r)) -> Term (bv r)
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term (bv r)) -> Term (bv r))
-> Uninterned (Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep r -> Term (bv l) -> UTerm (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: 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 -> TypeRep r -> Term (bv l) -> UTerm (bv r)
UBVExtendTerm Bool
signed (forall (a :: Nat). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @r) Term (bv l)
v
{-# INLINE bvextendTerm #-}
bvsignExtendTerm ::
forall bv l r proxy.
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat l,
KnownNat r,
1 <= l,
1 <= r,
l <= r,
SizedBV bv
) =>
proxy r ->
Term (bv l) ->
Term (bv r)
bvsignExtendTerm :: forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: 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) =>
proxy r -> Term (bv l) -> Term (bv r)
bvsignExtendTerm proxy r
_ Term (bv l)
v = Uninterned (Term (bv r)) -> Term (bv r)
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term (bv r)) -> Term (bv r))
-> Uninterned (Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep r -> Term (bv l) -> UTerm (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: 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 -> TypeRep r -> Term (bv l) -> UTerm (bv r)
UBVExtendTerm Bool
True (forall (a :: Nat). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @r) Term (bv l)
v
{-# INLINE bvsignExtendTerm #-}
bvzeroExtendTerm ::
forall bv l r proxy.
( forall n. (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv,
KnownNat l,
KnownNat r,
1 <= l,
1 <= r,
l <= r,
SizedBV bv
) =>
proxy r ->
Term (bv l) ->
Term (bv r)
bvzeroExtendTerm :: forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: 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) =>
proxy r -> Term (bv l) -> Term (bv r)
bvzeroExtendTerm proxy r
_ Term (bv l)
v = Uninterned (Term (bv r)) -> Term (bv r)
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term (bv r)) -> Term (bv r))
-> Uninterned (Term (bv r)) -> Term (bv r)
forall a b. (a -> b) -> a -> b
$ Bool -> TypeRep r -> Term (bv l) -> UTerm (bv r)
forall (bv :: Nat -> *) (l :: Nat) (r :: 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 -> TypeRep r -> Term (bv l) -> UTerm (bv r)
UBVExtendTerm Bool
False (forall (a :: Nat). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @r) Term (bv l)
v
{-# INLINE bvzeroExtendTerm #-}
tabularFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a =-> b) -> Term a -> Term b
tabularFunApplyTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
tabularFunApplyTerm Term (a =-> b)
f Term a
a = Uninterned (Term b) -> Term b
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term b) -> Term b) -> Uninterned (Term b) -> Term b
forall a b. (a -> b) -> a -> b
$ Term (a =-> b) -> Term a -> UTerm b
forall a t.
(SupportedPrim a, SupportedPrim t) =>
Term (a =-> t) -> Term a -> UTerm t
UTabularFunApplyTerm Term (a =-> b)
f Term a
a
{-# INLINE tabularFunApplyTerm #-}
generalFunApplyTerm :: (SupportedPrim a, SupportedPrim b) => Term (a --> b) -> Term a -> Term b
generalFunApplyTerm :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
generalFunApplyTerm Term (a --> b)
f Term a
a = Uninterned (Term b) -> Term b
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term b) -> Term b) -> Uninterned (Term b) -> Term b
forall a b. (a -> b) -> a -> b
$ Term (a --> b) -> Term a -> UTerm b
forall a t.
(SupportedPrim a, SupportedPrim t) =>
Term (a --> t) -> Term a -> UTerm t
UGeneralFunApplyTerm Term (a --> b)
f Term a
a
{-# INLINE generalFunApplyTerm #-}
divIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
divIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
divIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
UDivIntegralTerm Term a
l Term a
r
{-# INLINE divIntegralTerm #-}
modIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
modIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
modIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
UModIntegralTerm Term a
l Term a
r
{-# INLINE modIntegralTerm #-}
quotIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
quotIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
quotIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
UQuotIntegralTerm Term a
l Term a
r
{-# INLINE quotIntegralTerm #-}
remIntegralTerm :: (SupportedPrim a, Integral a) => Term a -> Term a -> Term a
remIntegralTerm :: forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
remIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Integral t) =>
Term t -> Term t -> UTerm t
URemIntegralTerm Term a
l Term a
r
{-# INLINE remIntegralTerm #-}
divBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
divBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
divBoundedIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
UDivBoundedIntegralTerm Term a
l Term a
r
{-# INLINE divBoundedIntegralTerm #-}
modBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
modBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
modBoundedIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
UModBoundedIntegralTerm Term a
l Term a
r
{-# INLINE modBoundedIntegralTerm #-}
quotBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
quotBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
quotBoundedIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
UQuotBoundedIntegralTerm Term a
l Term a
r
{-# INLINE quotBoundedIntegralTerm #-}
remBoundedIntegralTerm :: (SupportedPrim a, Bounded a, Integral a) => Term a -> Term a -> Term a
remBoundedIntegralTerm :: forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
remBoundedIntegralTerm Term a
l Term a
r = Uninterned (Term a) -> Term a
forall t. SupportedPrim t => Uninterned (Term t) -> Term t
internTerm (Uninterned (Term a) -> Term a) -> Uninterned (Term a) -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> UTerm a
forall t.
(SupportedPrim t, Bounded t, Integral t) =>
Term t -> Term t -> UTerm t
URemBoundedIntegralTerm Term a
l Term a
r
{-# INLINE remBoundedIntegralTerm #-}