grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell2010

Grisette.Core.Data.BV

Description

 
Synopsis

Documentation

data BitwidthMismatch Source #

Constructors

BitwidthMismatch 

Instances

Instances details
Exception BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.BV

Generic BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.BV

Associated Types

type Rep BitwidthMismatch :: Type -> Type #

Show BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.BV

Eq BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.BV

Ord BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.BV

Mergeable BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

type Rep BitwidthMismatch Source # 
Instance details

Defined in Grisette.Core.Data.BV

type Rep BitwidthMismatch = D1 ('MetaData "BitwidthMismatch" "Grisette.Core.Data.BV" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'False) (C1 ('MetaCons "BitwidthMismatch" 'PrefixI 'False) (U1 :: Type -> Type))

newtype IntN (n :: Nat) Source #

Symbolic signed bit vectors.

Constructors

IntN 

Fields

Instances

Instances details
SizedBV IntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r) Source #

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source #

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source #

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r Source #

sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> IntN n -> IntN w Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n, IntN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> uf (IntN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => IntN n -> IntN n -> uf (IntN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> uf (IntN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> IntN n -> IntN n -> uf (IntN n) Source #

(KnownNat n, 1 <= n) => Bits (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

(.&.) :: IntN n -> IntN n -> IntN n #

(.|.) :: IntN n -> IntN n -> IntN n #

xor :: IntN n -> IntN n -> IntN n #

complement :: IntN n -> IntN n #

shift :: IntN n -> Int -> IntN n #

rotate :: IntN n -> Int -> IntN n #

zeroBits :: IntN n #

bit :: Int -> IntN n #

setBit :: IntN n -> Int -> IntN n #

clearBit :: IntN n -> Int -> IntN n #

complementBit :: IntN n -> Int -> IntN n #

testBit :: IntN n -> Int -> Bool #

bitSizeMaybe :: IntN n -> Maybe Int #

bitSize :: IntN n -> Int #

isSigned :: IntN n -> Bool #

shiftL :: IntN n -> Int -> IntN n #

unsafeShiftL :: IntN n -> Int -> IntN n #

shiftR :: IntN n -> Int -> IntN n #

unsafeShiftR :: IntN n -> Int -> IntN n #

rotateL :: IntN n -> Int -> IntN n #

rotateR :: IntN n -> Int -> IntN n #

popCount :: IntN n -> Int #

(KnownNat n, 1 <= n) => FiniteBits (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

(KnownNat n, 1 <= n) => Bounded (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

minBound :: IntN n #

maxBound :: IntN n #

(KnownNat n, 1 <= n) => Enum (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

succ :: IntN n -> IntN n #

pred :: IntN n -> IntN n #

toEnum :: Int -> IntN n #

fromEnum :: IntN n -> Int #

enumFrom :: IntN n -> [IntN n] #

enumFromThen :: IntN n -> IntN n -> [IntN n] #

enumFromTo :: IntN n -> IntN n -> [IntN n] #

enumFromThenTo :: IntN n -> IntN n -> IntN n -> [IntN n] #

Generic (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Associated Types

type Rep (IntN n) :: Type -> Type #

Methods

from :: IntN n -> Rep (IntN n) x #

to :: Rep (IntN n) x -> IntN n #

(KnownNat n, 1 <= n) => Num (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

(+) :: IntN n -> IntN n -> IntN n #

(-) :: IntN n -> IntN n -> IntN n #

(*) :: IntN n -> IntN n -> IntN n #

negate :: IntN n -> IntN n #

abs :: IntN n -> IntN n #

signum :: IntN n -> IntN n #

fromInteger :: Integer -> IntN n #

(KnownNat n, 1 <= n) => Read (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

(KnownNat n, 1 <= n) => Integral (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

quot :: IntN n -> IntN n -> IntN n #

rem :: IntN n -> IntN n -> IntN n #

div :: IntN n -> IntN n -> IntN n #

mod :: IntN n -> IntN n -> IntN n #

quotRem :: IntN n -> IntN n -> (IntN n, IntN n) #

divMod :: IntN n -> IntN n -> (IntN n, IntN n) #

toInteger :: IntN n -> Integer #

(KnownNat n, 1 <= n) => Real (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

toRational :: IntN n -> Rational #

(KnownNat n, 1 <= n) => Show (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

showsPrec :: Int -> IntN n -> ShowS #

show :: IntN n -> String #

showList :: [IntN n] -> ShowS #

NFData (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

rnf :: IntN n -> () #

Eq (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

(==) :: IntN n -> IntN n -> Bool #

(/=) :: IntN n -> IntN n -> Bool #

(KnownNat n, 1 <= n) => Ord (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

compare :: IntN n -> IntN n -> Ordering #

(<) :: IntN n -> IntN n -> Bool #

(<=) :: IntN n -> IntN n -> Bool #

(>) :: IntN n -> IntN n -> Bool #

(>=) :: IntN n -> IntN n -> Bool #

max :: IntN n -> IntN n -> IntN n #

min :: IntN n -> IntN n -> IntN n #

(KnownNat n, 1 <= n) => SEq (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

Methods

(==~) :: IntN n -> IntN n -> SymBool Source #

(/=~) :: IntN n -> IntN n -> SymBool Source #

(KnownNat n, 1 <= n) => EvaluateSym (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> IntN n -> IntN n Source #

(KnownNat n, 1 <= n) => ExtractSymbolics (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

(KnownNat n, 1 <= n) => Mergeable (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(KnownNat n, 1 <= n) => SOrd (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

Methods

(<~) :: IntN n -> IntN n -> SymBool Source #

(<=~) :: IntN n -> IntN n -> SymBool Source #

(>~) :: IntN n -> IntN n -> SymBool Source #

(>=~) :: IntN n -> IntN n -> SymBool Source #

symCompare :: IntN n -> IntN n -> UnionM Ordering Source #

(KnownNat n, 1 <= n) => SubstituteSym (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n Source #

(KnownNat w, 1 <= w) => SupportedPrim (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (IntN w) Source #

(KnownNat n, 1 <= n) => SymRep (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (IntN n) Source #

Hashable (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

hashWithSalt :: Int -> IntN n -> Int #

hash :: IntN n -> Int #

(KnownNat n, 1 <= n) => ToSym (IntN n) SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: IntN n -> SomeSymIntN Source #

(KnownNat n, 1 <= n) => GenSym (IntN n) (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => IntN n -> m (UnionM (IntN n)) Source #

(KnownNat n, 1 <= n) => GenSymSimple (IntN n) (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => IntN n -> m (IntN n) Source #

(KnownNat n, 1 <= n) => Solvable (IntN n) (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: IntN n -> SymIntN n Source #

conView :: SymIntN n -> Maybe (IntN n) Source #

ssym :: String -> SymIntN n Source #

isym :: String -> Int -> SymIntN n Source #

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymIntN n Source #

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymIntN n Source #

(KnownNat n, 1 <= n) => ToCon (IntN n) (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: IntN n -> Maybe (IntN n) Source #

(KnownNat n, 1 <= n) => ToCon (SymIntN n) (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN n -> Maybe (IntN n) Source #

(KnownNat n, 1 <= n) => ToSym (UnionM (IntN n)) (SymIntN n) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM (IntN n) -> SymIntN n Source #

(KnownNat n, 1 <= n) => ToSym (IntN n) (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: IntN n -> IntN n Source #

(KnownNat n, 1 <= n) => ToSym (IntN n) (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: IntN n -> SymIntN n Source #

(KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Lift (IntN n :: TYPE LiftedRep) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

lift :: Quote m => IntN n -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => IntN n -> Code m (IntN n) #

type Rep (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

type Rep (IntN n) = D1 ('MetaData "IntN" "Grisette.Core.Data.BV" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'True) (C1 ('MetaCons "IntN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unIntN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type PrimConstraint (IntN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type PrimConstraint (IntN w) = (KnownNat w, 1 <= w)
type SymType (IntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type SymType (IntN n) = SymIntN n

newtype WordN (n :: Nat) Source #

Symbolic unsigned bit vectors.

Constructors

WordN 

Fields

Instances

Instances details
SizedBV WordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

sizedBVConcat :: forall (l :: Nat) (r :: Nat). (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r) Source #

sizedBVZext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source #

sizedBVSext :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source #

sizedBVExt :: forall (l :: Nat) (r :: Nat) proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r Source #

sizedBVSelect :: forall (n :: Nat) (ix :: Nat) (w :: Nat) proxy. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, (ix + w) <= n) => proxy ix -> proxy w -> WordN n -> WordN w Source #

(KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeDivMod :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeQuot :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeQuotRem :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n, WordN n) Source #

(KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeAdd :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeNeg :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> uf (WordN n) Source #

safeMinus :: (MonadError ArithException uf, MonadUnion uf) => WordN n -> WordN n -> uf (WordN n) Source #

safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> uf (WordN n) Source #

safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (ArithException -> e') -> WordN n -> WordN n -> uf (WordN n) Source #

(KnownNat n, 1 <= n) => Bits (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

(.&.) :: WordN n -> WordN n -> WordN n #

(.|.) :: WordN n -> WordN n -> WordN n #

xor :: WordN n -> WordN n -> WordN n #

complement :: WordN n -> WordN n #

shift :: WordN n -> Int -> WordN n #

rotate :: WordN n -> Int -> WordN n #

zeroBits :: WordN n #

bit :: Int -> WordN n #

setBit :: WordN n -> Int -> WordN n #

clearBit :: WordN n -> Int -> WordN n #

complementBit :: WordN n -> Int -> WordN n #

testBit :: WordN n -> Int -> Bool #

bitSizeMaybe :: WordN n -> Maybe Int #

bitSize :: WordN n -> Int #

isSigned :: WordN n -> Bool #

shiftL :: WordN n -> Int -> WordN n #

unsafeShiftL :: WordN n -> Int -> WordN n #

shiftR :: WordN n -> Int -> WordN n #

unsafeShiftR :: WordN n -> Int -> WordN n #

rotateL :: WordN n -> Int -> WordN n #

rotateR :: WordN n -> Int -> WordN n #

popCount :: WordN n -> Int #

(KnownNat n, 1 <= n) => FiniteBits (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

(KnownNat n, 1 <= n) => Bounded (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

minBound :: WordN n #

maxBound :: WordN n #

(KnownNat n, 1 <= n) => Enum (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

succ :: WordN n -> WordN n #

pred :: WordN n -> WordN n #

toEnum :: Int -> WordN n #

fromEnum :: WordN n -> Int #

enumFrom :: WordN n -> [WordN n] #

enumFromThen :: WordN n -> WordN n -> [WordN n] #

enumFromTo :: WordN n -> WordN n -> [WordN n] #

enumFromThenTo :: WordN n -> WordN n -> WordN n -> [WordN n] #

Generic (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Associated Types

type Rep (WordN n) :: Type -> Type #

Methods

from :: WordN n -> Rep (WordN n) x #

to :: Rep (WordN n) x -> WordN n #

(KnownNat n, 1 <= n) => Num (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

(+) :: WordN n -> WordN n -> WordN n #

(-) :: WordN n -> WordN n -> WordN n #

(*) :: WordN n -> WordN n -> WordN n #

negate :: WordN n -> WordN n #

abs :: WordN n -> WordN n #

signum :: WordN n -> WordN n #

fromInteger :: Integer -> WordN n #

(KnownNat n, 1 <= n) => Read (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

(KnownNat n, 1 <= n) => Integral (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

quot :: WordN n -> WordN n -> WordN n #

rem :: WordN n -> WordN n -> WordN n #

div :: WordN n -> WordN n -> WordN n #

mod :: WordN n -> WordN n -> WordN n #

quotRem :: WordN n -> WordN n -> (WordN n, WordN n) #

divMod :: WordN n -> WordN n -> (WordN n, WordN n) #

toInteger :: WordN n -> Integer #

(KnownNat n, 1 <= n) => Real (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

toRational :: WordN n -> Rational #

(KnownNat n, 1 <= n) => Show (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

showsPrec :: Int -> WordN n -> ShowS #

show :: WordN n -> String #

showList :: [WordN n] -> ShowS #

NFData (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

rnf :: WordN n -> () #

Eq (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

(==) :: WordN n -> WordN n -> Bool #

(/=) :: WordN n -> WordN n -> Bool #

Ord (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

compare :: WordN n -> WordN n -> Ordering #

(<) :: WordN n -> WordN n -> Bool #

(<=) :: WordN n -> WordN n -> Bool #

(>) :: WordN n -> WordN n -> Bool #

(>=) :: WordN n -> WordN n -> Bool #

max :: WordN n -> WordN n -> WordN n #

min :: WordN n -> WordN n -> WordN n #

(KnownNat n, 1 <= n) => SEq (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

Methods

(==~) :: WordN n -> WordN n -> SymBool Source #

(/=~) :: WordN n -> WordN n -> SymBool Source #

(KnownNat n, 1 <= n) => EvaluateSym (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

Methods

evaluateSym :: Bool -> Model -> WordN n -> WordN n Source #

(KnownNat n, 1 <= n) => ExtractSymbolics (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

(KnownNat n, 1 <= n) => Mergeable (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

(KnownNat n, 1 <= n) => SOrd (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

(KnownNat n, 1 <= n) => SubstituteSym (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n Source #

(KnownNat w, 1 <= w) => SupportedPrim (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

Associated Types

type PrimConstraint (WordN w) Source #

(KnownNat n, 1 <= n) => SymRep (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Associated Types

type SymType (WordN n) Source #

Hashable (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

hashWithSalt :: Int -> WordN n -> Int #

hash :: WordN n -> Int #

(KnownNat n, 1 <= n) => ToSym (WordN n) SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

(KnownNat n, 1 <= n) => GenSym (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => WordN n -> m (UnionM (WordN n)) Source #

(KnownNat n, 1 <= n) => GenSymSimple (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => WordN n -> m (WordN n) Source #

(KnownNat n, 1 <= n) => Solvable (WordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

con :: WordN n -> SymWordN n Source #

conView :: SymWordN n -> Maybe (WordN n) Source #

ssym :: String -> SymWordN n Source #

isym :: String -> Int -> SymWordN n Source #

sinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> SymWordN n Source #

iinfosym :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> Int -> a -> SymWordN n Source #

(KnownNat n, 1 <= n) => ToCon (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: WordN n -> Maybe (WordN n) Source #

(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN n -> Maybe (WordN n) Source #

(KnownNat n, 1 <= n) => ToSym (UnionM (WordN n)) (SymWordN n) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM (WordN n) -> SymWordN n Source #

(KnownNat n, 1 <= n) => ToSym (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: WordN n -> WordN n Source #

(KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: WordN n -> SymWordN n Source #

(KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Lift (WordN n :: TYPE LiftedRep) Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

lift :: Quote m => WordN n -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => WordN n -> Code m (WordN n) #

type Rep (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.BV

type Rep (WordN n) = D1 ('MetaData "WordN" "Grisette.Core.Data.BV" "grisette-0.2.0.0-CYZZ7WjRTnw1wxrPITB8ce" 'True) (C1 ('MetaCons "WordN" 'PrefixI 'True) (S1 ('MetaSel ('Just "unWordN") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))
type PrimConstraint (WordN w) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

type PrimConstraint (WordN w) = (KnownNat w, 1 <= w)
type SymType (WordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

type SymType (WordN n) = SymWordN n

data SomeIntN where Source #

A non-indexed version of IntN.

Constructors

SomeIntN :: (KnownNat n, 1 <= n) => IntN n -> SomeIntN 

Instances

Instances details
Bits SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

FiniteBits SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Enum SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Num SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Integral SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Real SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Show SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

NFData SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

rnf :: SomeIntN -> () #

Eq SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Ord SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

SomeBV SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

someBVConcat :: SomeIntN -> SomeIntN -> SomeIntN Source #

someBVZext :: forall p (l :: Nat). KnownNat l => p l -> SomeIntN -> SomeIntN Source #

someBVSext :: forall p (l :: Nat). KnownNat l => p l -> SomeIntN -> SomeIntN Source #

someBVExt :: forall p (l :: Nat). KnownNat l => p l -> SomeIntN -> SomeIntN Source #

someBVSelect :: forall p (ix :: Nat) q (w :: Nat). (KnownNat ix, KnownNat w) => p ix -> q w -> SomeIntN -> SomeIntN Source #

SEq SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

EvaluateSym SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

ExtractSymbolics SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

Mergeable SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

SOrd SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SubstituteSym SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeIntN -> SomeIntN Source #

Hashable SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

hashWithSalt :: Int -> SomeIntN -> Int #

hash :: SomeIntN -> Int #

GenSym SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

ToCon SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon SomeSymIntN SomeIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym SomeIntN SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Lift SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

lift :: Quote m => SomeIntN -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => SomeIntN -> Code m SomeIntN #

ToSym (UnionM SomeIntN) SomeSymIntN Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

SafeDivision (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf SomeIntN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeIntN -> SomeIntN -> uf (SomeIntN, SomeIntN) Source #

SafeLinearArith (Either BitwidthMismatch ArithException) SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

data SomeWordN where Source #

A non-indexed version of WordN.

Constructors

SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN 

Instances

Instances details
Bits SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

FiniteBits SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Enum SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Num SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Integral SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Real SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Show SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

NFData SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

rnf :: SomeWordN -> () #

Eq SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Ord SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

SomeBV SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

someBVConcat :: SomeWordN -> SomeWordN -> SomeWordN Source #

someBVZext :: forall p (l :: Nat). KnownNat l => p l -> SomeWordN -> SomeWordN Source #

someBVSext :: forall p (l :: Nat). KnownNat l => p l -> SomeWordN -> SomeWordN Source #

someBVExt :: forall p (l :: Nat). KnownNat l => p l -> SomeWordN -> SomeWordN Source #

someBVSelect :: forall p (ix :: Nat) q (w :: Nat). (KnownNat ix, KnownNat w) => p ix -> q w -> SomeWordN -> SomeWordN Source #

SEq SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Bool

EvaluateSym SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Evaluate

ExtractSymbolics SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ExtractSymbolics

Mergeable SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Mergeable

SOrd SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SOrd

SubstituteSym SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeWordN -> SomeWordN Source #

Hashable SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

GenSym SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

GenSymSimple SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.GenSym

ToCon SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon SomeSymWordN SomeWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym SomeWordN SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Lift SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.BV

Methods

lift :: Quote m => SomeWordN -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => SomeWordN -> Code m SomeWordN #

ToSym (UnionM SomeWordN) SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

SafeDivision (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

Methods

safeDiv :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem :: (MonadError (Either BitwidthMismatch ArithException) uf, MonadUnion uf) => SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf SomeWordN Source #

safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (Either BitwidthMismatch ArithException -> e') -> SomeWordN -> SomeWordN -> uf (SomeWordN, SomeWordN) Source #

SafeLinearArith (Either BitwidthMismatch ArithException) SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.SafeArith

unarySomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> r) -> SomeIntN -> r Source #

unarySomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n) -> SomeIntN -> SomeIntN Source #

binSomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> r) -> SomeIntN -> SomeIntN -> r Source #

binSomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> IntN n) -> SomeIntN -> SomeIntN -> SomeIntN Source #

binSomeIntNR2 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> (IntN n, IntN n)) -> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN) Source #

unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r Source #

unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN Source #

binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r Source #

binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN Source #

binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN) Source #