Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.SymPrim.SymFP

Contents

Orphan instances

Description

Synopsis

newtype SymFP (eb :: Nat) (sb :: Nat) = SymFP (Term (FP eb sb))
type SymFP16 = SymFP 5 11
type SymFP32 = SymFP 8 24
type SymFP64 = SymFP 11 53
type SymFPKey (eb :: Nat) (sb :: Nat) = AsKey (SymFP eb sb)
type SymFP16Key = SymFPKey 5 11
type SymFP32Key = SymFPKey 8 24
type SymFP64Key = SymFPKey 11 53
newtype SymFPRoundingMode = SymFPRoundingMode (Term FPRoundingMode)
type SymFPRoundingModeKey = AsKey SymFPRoundingMode

Documentation

newtype SymFP (eb :: Nat) (sb :: Nat) Source #

Symbolic IEEE 754 floating-point number with eb exponent bits and sb significand bits.

>>> "a" + 2.0 :: SymFP 11 53
(+ a 2.0)
>>> fpAdd rne "a" 2.0 :: SymFP 11 53
(fp.add rne a 2.0)

More operations are available. Please refer to Grisette.Core for more information.

Constructors

SymFP (Term (FP eb sb))

Instances

Instances details

ToCon SymFP32 Float Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP32 -> Maybe Float Source #

ToCon SymFP64 Double Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP64 -> Maybe Double Source #

ToSym Double SymFP64 Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: Double -> SymFP64 Source #

ToSym Float SymFP32 Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: Float -> SymFP32 Source #

ValidFP eb sb => UnifiedFPImpl 'S SymFP eb sb (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP

Associated Types

type GetFP 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFP 'S = SymFP
type GetFPRoundingMode 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFPRoundingMode 'S = SymFPRoundingMode

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

ValidFP eb sb => UnifiedFromIntegral 'S SymInteger (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral SymInteger, Num (SymFP eb sb)) (SymFromIntegral SymInteger (SymFP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymAlgReal Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymInteger Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN n) m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN n) m => r) -> r Source #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymIntN n') (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymIntN n'), Num (SymFP eb sb)) (SymFromIntegral (SymIntN n') (SymFP eb sb)) => r) -> r Source #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'S (SymWordN n') (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'S) (Integral (SymWordN n'), Num (SymFP eb sb)) (SymFromIntegral (SymWordN n') (SymFP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymIntN n) Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymWordN n) Source #

ValidFP eb sb => GenSym () (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (Union (SymFP eb sb)) Source #

ValidFP eb sb => GenSymSimple () (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m (SymFP eb sb) Source #

ValidFP eb sb => SymFromIntegral SymInteger (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral

Methods

symFromIntegral :: SymInteger -> SymFP eb sb Source #

Lift (SymFP eb sb :: Type) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

lift :: Quote m => SymFP eb sb -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => SymFP eb sb -> Code m (SymFP eb sb) #

ValidFP eb sb => IEEEFPConvertible SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymAlgReal -> SymFPRoundingMode -> SymFP eb sb -> SymAlgReal Source #

toFP :: SymFPRoundingMode -> SymAlgReal -> SymFP eb sb Source #

ValidFP eb sb => IEEEFPConvertible SymInteger (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymInteger -> SymFPRoundingMode -> SymFP eb sb -> SymInteger Source #

toFP :: SymFPRoundingMode -> SymInteger -> SymFP eb sb Source #

ValidFP eb sb => IEEEFPToAlgReal SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpToAlgReal :: SymAlgReal -> SymFP eb sb -> SymAlgReal Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: SymFP eb sb -> m (SymIntN r) Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: SymFP eb sb -> m (SymWordN r) Source #

ValidFP eb sb => UnifiedSolvable 'S (SymFP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'S) (SymFP eb sb ~ FP eb sb) (Solvable (FP eb sb) (SymFP eb sb)) => r) -> r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (SymIntN r) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCast :: SymIntN r -> SymFP eb sb Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (SymWordN r) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCast :: SymWordN r -> SymFP eb sb Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => SymFromIntegral (SymIntN n) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral

Methods

symFromIntegral :: SymIntN n -> SymFP eb sb Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => SymFromIntegral (SymWordN n) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SymFromIntegral

Methods

symFromIntegral :: SymWordN n -> SymFP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymIntN n) (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymIntN n -> SymFPRoundingMode -> SymFP eb sb -> SymIntN n Source #

toFP :: SymFPRoundingMode -> SymIntN n -> SymFP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymWordN n) (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n Source #

toFP :: SymFPRoundingMode -> SymWordN n -> SymFP eb sb Source #

ValidFP eb sb => Binary (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

put :: SymFP eb sb -> Put #

get :: Get (SymFP eb sb) #

putList :: [SymFP eb sb] -> Put #

ValidFP eb sb => Serial (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

serialize :: MonadPut m => SymFP eb sb -> m () #

deserialize :: MonadGet m => m (SymFP eb sb) #

ValidFP eb sb => Serialize (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

put :: Putter (SymFP eb sb) #

get :: Get (SymFP eb sb) #

NFData (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

rnf :: SymFP eb sb -> () #

ValidFP eb sb => IsString (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromString :: String -> SymFP eb sb #

ValidFP eb sb => Floating (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

pi :: SymFP eb sb #

exp :: SymFP eb sb -> SymFP eb sb #

log :: SymFP eb sb -> SymFP eb sb #

sqrt :: SymFP eb sb -> SymFP eb sb #

(**) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

logBase :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

sin :: SymFP eb sb -> SymFP eb sb #

cos :: SymFP eb sb -> SymFP eb sb #

tan :: SymFP eb sb -> SymFP eb sb #

asin :: SymFP eb sb -> SymFP eb sb #

acos :: SymFP eb sb -> SymFP eb sb #

atan :: SymFP eb sb -> SymFP eb sb #

sinh :: SymFP eb sb -> SymFP eb sb #

cosh :: SymFP eb sb -> SymFP eb sb #

tanh :: SymFP eb sb -> SymFP eb sb #

asinh :: SymFP eb sb -> SymFP eb sb #

acosh :: SymFP eb sb -> SymFP eb sb #

atanh :: SymFP eb sb -> SymFP eb sb #

log1p :: SymFP eb sb -> SymFP eb sb #

expm1 :: SymFP eb sb -> SymFP eb sb #

log1pexp :: SymFP eb sb -> SymFP eb sb #

log1mexp :: SymFP eb sb -> SymFP eb sb #

Generic (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type Rep (SymFP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type Rep (SymFP eb sb) = D1 ('MetaData "SymFP" "Grisette.Internal.SymPrim.SymFP" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymFP" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingFPTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (FP eb sb)))))

Methods

from :: SymFP eb sb -> Rep (SymFP eb sb) x #

to :: Rep (SymFP eb sb) x -> SymFP eb sb #

ValidFP eb sb => Num (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(+) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

(-) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

(*) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

negate :: SymFP eb sb -> SymFP eb sb #

abs :: SymFP eb sb -> SymFP eb sb #

signum :: SymFP eb sb -> SymFP eb sb #

fromInteger :: Integer -> SymFP eb sb #

ValidFP eb sb => Fractional (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(/) :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb #

recip :: SymFP eb sb -> SymFP eb sb #

fromRational :: Rational -> SymFP eb sb #

ValidFP eb sb => Show (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

showsPrec :: Int -> SymFP eb sb -> ShowS #

show :: SymFP eb sb -> String #

showList :: [SymFP eb sb] -> ShowS #

ValidFP eb sb => Eq (SymFP eb sb) Source #

This will crash the program.

SymFP cannot be compared concretely.

If you want to use the type as keys in hash maps based on term equality, say memo table, you should use AsKey SymFP instead.

If you want symbolic version of the equality operator, use SymEq instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(==) :: SymFP eb sb -> SymFP eb sb -> Bool #

(/=) :: SymFP eb sb -> SymFP eb sb -> Bool #

ValidFP eb sb => KeyEq (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

keyEq :: SymFP eb sb -> SymFP eb sb -> Bool Source #

ValidFP eb sb => KeyHashable (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

keyHashWithSalt :: Int -> SymFP eb sb -> Int Source #

ValidFP eb sb => Apply (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type FunType (SymFP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type FunType (SymFP eb sb) = SymFP eb sb

Methods

apply :: SymFP eb sb -> FunType (SymFP eb sb) Source #

ValidFP eb sb => IEEEFPConstants (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpPositiveInfinite :: SymFP eb sb Source #

fpNegativeInfinite :: SymFP eb sb Source #

fpNaN :: SymFP eb sb Source #

fpNegativeZero :: SymFP eb sb Source #

fpPositiveZero :: SymFP eb sb Source #

fpMinNormalized :: SymFP eb sb Source #

fpMinSubnormal :: SymFP eb sb Source #

fpMaxNormalized :: SymFP eb sb Source #

fpMaxSubnormal :: SymFP eb sb Source #

ValidFP eb sb => IEEEFPOp (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpAbs :: SymFP eb sb -> SymFP eb sb Source #

fpNeg :: SymFP eb sb -> SymFP eb sb Source #

fpRem :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMinimum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMinimumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMaximum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMaximumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => ITEOp (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => SymIEEEFPTraits (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

symFpIsNaN :: SymFP eb sb -> SymBool Source #

symFpIsPositive :: SymFP eb sb -> SymBool Source #

symFpIsNegative :: SymFP eb sb -> SymBool Source #

symFpIsPositiveInfinite :: SymFP eb sb -> SymBool Source #

symFpIsNegativeInfinite :: SymFP eb sb -> SymBool Source #

symFpIsInfinite :: SymFP eb sb -> SymBool Source #

symFpIsPositiveZero :: SymFP eb sb -> SymBool Source #

symFpIsNegativeZero :: SymFP eb sb -> SymBool Source #

symFpIsZero :: SymFP eb sb -> SymBool Source #

symFpIsNormal :: SymFP eb sb -> SymBool Source #

symFpIsSubnormal :: SymFP eb sb -> SymBool Source #

symFpIsPoint :: SymFP eb sb -> SymBool Source #

ValidFP eb sb => EvalSym (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb fb => ExtractSym (SymFP eb fb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: SymFP eb fb -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymFP eb fb -> Maybe (SymbolSet knd) Source #

ValidFP eb sb => Mergeable (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (SymFP eb sb) Source #

sortIndices :: SymFP eb sb -> [DynamicSortedIdx] Source #

ValidFP eb sb => PPrint (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: SymFP eb sb -> Doc ann Source #

pformatPrec :: Int -> SymFP eb sb -> Doc ann Source #

pformatList :: [SymFP eb sb] -> Doc ann Source #

ValidFP eb sb => SimpleMergeable (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => SubstSym (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => SymEq (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(./=) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

symDistinct :: [SymFP eb sb] -> SymBool Source #

ValidFP eb sb => SymOrd (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(.<=) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(.>) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

(.>=) :: SymFP eb sb -> SymFP eb sb -> SymBool Source #

symCompare :: SymFP eb sb -> SymFP eb sb -> Union Ordering Source #

ValidFP eb sb => AllSyms (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

allSymsS :: SymFP eb sb -> [SomeSym] -> [SomeSym] Source #

allSyms :: SymFP eb sb -> [SomeSym] Source #

ConRep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type ConType (SymFP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type ConType (SymFP eb sb) = FP eb sb

ValidFP eb sb => UnifiedConRep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType (SymFP eb sb)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType (SymFP eb sb) = FP eb sb

ValidFP eb sb => UnifiedSymRep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType (SymFP eb sb)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType (SymFP eb sb) = SymFP eb sb

ValidFP eb sb => Hashable (SymFP eb sb) Source #

This will crash the program.

SymFP cannot be hashed concretely.

If you want to use the type as keys in hash maps based on term equality, say memo table, you should use AsKey SymFP instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

hashWithSalt :: Int -> SymFP eb sb -> Int #

hash :: SymFP eb sb -> Int #

ValidFP eb sb => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpAdd :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpSub :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMul :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpDiv :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpFMA :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpSqrt :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source #

fpRoundToIntegral :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastCanonical (SymFP eb sb) (SymIntN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastCanonicalValue :: proxy (SymFP eb sb) -> SymIntN r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastCanonical (SymFP eb sb) (SymWordN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastCanonicalValue :: proxy (SymFP eb sb) -> SymWordN r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymIntN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastOr :: SymIntN r -> SymFP eb sb -> SymIntN r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymWordN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

bitCastOr :: SymWordN r -> SymFP eb sb -> SymWordN r Source #

ValidFP eb sb => GenSym (SymFP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => SymFP eb sb -> m (Union (SymFP eb sb)) Source #

ValidFP eb sb => GenSymSimple (SymFP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => SymFP eb sb -> m (SymFP eb sb) Source #

ValidFP eb sb => Solvable (FP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

con :: FP eb sb -> SymFP eb sb Source #

conView :: SymFP eb sb -> Maybe (FP eb sb) Source #

sym :: Symbol -> SymFP eb sb Source #

ssym :: Identifier -> SymFP eb sb Source #

isym :: Identifier -> Int -> SymFP eb sb Source #

ValidFP eb sb => ToCon (SymFP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP eb sb -> Maybe (FP eb sb) Source #

ValidFP eb sb => ToCon (SymFP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP eb sb -> Maybe (SymFP eb sb) Source #

ValidFP eb sb => ToSym (FP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: FP eb sb -> SymFP eb sb Source #

ValidFP eb sb => ToSym (SymFP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: SymFP eb sb -> SymFP eb sb Source #

ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

underlyingTerm :: SymFP eb sb -> Term (FP eb sb) Source #

wrapTerm :: Term (FP eb sb) -> SymFP eb sb Source #

(ValidFP eb sb, ValidFP eb' sb') => IEEEFPConvertible (SymFP eb' sb') (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymFP eb' sb' -> SymFPRoundingMode -> SymFP eb sb -> SymFP eb' sb' Source #

toFP :: SymFPRoundingMode -> SymFP eb' sb' -> SymFP eb sb Source #

type Rep (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type Rep (SymFP eb sb) = D1 ('MetaData "SymFP" "Grisette.Internal.SymPrim.SymFP" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymFP" 'PrefixI 'True) (S1 ('MetaSel ('Just "underlyingFPTerm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term (FP eb sb)))))

type FunType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type FunType (SymFP eb sb) = SymFP eb sb

type ConType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type ConType (SymFP eb sb) = FP eb sb

type ConType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (SymFP eb sb) = FP eb sb

type SymType (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (SymFP eb sb) = SymFP eb sb

type SymFP16 = SymFP 5 11 Source #

Symbolic IEEE 754 half-precision floating-point number.

type SymFP32 = SymFP 8 24 Source #

Symbolic IEEE 754 single-precision floating-point number.

type SymFP64 = SymFP 11 53 Source #

Symbolic IEEE 754 double-precision floating-point number.

type SymFPKey (eb :: Nat) (sb :: Nat) = AsKey (SymFP eb sb) Source #

SymFP type with identity equality.

type SymFP16Key = SymFPKey 5 11 Source #

SymFP 16 type with identity equality.

type SymFP32Key = SymFPKey 8 24 Source #

SymFP 32 type with identity equality.

type SymFP64Key = SymFPKey 11 53 Source #

SymFP 64 type with identity equality.

newtype SymFPRoundingMode Source #

Symbolic floating-point rounding mode.

Constructors

SymFPRoundingMode (Term FPRoundingMode)

Instances

Instances details

NFData SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

rnf :: SymFPRoundingMode -> () #

IsString SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromString :: String -> SymFPRoundingMode #

Generic SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type Rep SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type Rep SymFPRoundingMode = D1 ('MetaData "SymFPRoundingMode" "Grisette.Internal.SymPrim.SymFP" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymFPRoundingMode" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term FPRoundingMode))))

Methods

from :: SymFPRoundingMode -> Rep SymFPRoundingMode x #

to :: Rep SymFPRoundingMode x -> SymFPRoundingMode #

Show SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

showsPrec :: Int -> SymFPRoundingMode -> ShowS #

show :: SymFPRoundingMode -> String #

showList :: [SymFPRoundingMode] -> ShowS #

Eq SymFPRoundingMode Source #

This will crash the program.

SymFPRoundingMode cannot be compared concretely.

If you want to use the type as keys in hash maps based on term equality, say memo table, you should use AsKey SymFPRoundingMode instead.

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

(==) :: SymFPRoundingMode -> SymFPRoundingMode -> Bool #

(/=) :: SymFPRoundingMode -> SymFPRoundingMode -> Bool #

KeyEq SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

keyEq :: SymFPRoundingMode -> SymFPRoundingMode -> Bool Source #

KeyHashable SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

keyHashWithSalt :: Int -> SymFPRoundingMode -> Int Source #

Apply SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type FunType SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type FunType SymFPRoundingMode = SymFPRoundingMode

Methods

apply :: SymFPRoundingMode -> FunType SymFPRoundingMode Source #

IEEEFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

rne :: SymFPRoundingMode Source #

rna :: SymFPRoundingMode Source #

rtp :: SymFPRoundingMode Source #

rtn :: SymFPRoundingMode Source #

rtz :: SymFPRoundingMode Source #

ITEOp SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.ITEOp

Methods

symIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode Source #

EvalSym SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymFPRoundingMode -> SymFPRoundingMode Source #

ExtractSym SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: SymFPRoundingMode -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => SymFPRoundingMode -> Maybe (SymbolSet knd) Source #

Mergeable SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy SymFPRoundingMode Source #

sortIndices :: SymFPRoundingMode -> [DynamicSortedIdx] Source #

PPrint SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: SymFPRoundingMode -> Doc ann Source #

pformatPrec :: Int -> SymFPRoundingMode -> Doc ann Source #

pformatList :: [SymFPRoundingMode] -> Doc ann Source #

SimpleMergeable SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SimpleMergeable

Methods

mrgIte :: SymBool -> SymFPRoundingMode -> SymFPRoundingMode -> SymFPRoundingMode Source #

SubstSym SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> SymFPRoundingMode -> SymFPRoundingMode Source #

SymEq SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(./=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

symDistinct :: [SymFPRoundingMode] -> SymBool Source #

SymOrd SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(.<=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(.>) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

(.>=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source #

symCompare :: SymFPRoundingMode -> SymFPRoundingMode -> Union Ordering Source #

AllSyms SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

allSymsS :: SymFPRoundingMode -> [SomeSym] -> [SomeSym] Source #

allSyms :: SymFPRoundingMode -> [SomeSym] Source #

ConRep SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type ConType SymFPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type ConType SymFPRoundingMode = FPRoundingMode

GenSym SymFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => SymFPRoundingMode -> m (Union SymFPRoundingMode) Source #

GenSym () SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => () -> m (Union SymFPRoundingMode) Source #

GenSymSimple SymFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => SymFPRoundingMode -> m SymFPRoundingMode Source #

GenSymSimple () SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => () -> m SymFPRoundingMode Source #

Solvable FPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

con :: FPRoundingMode -> SymFPRoundingMode Source #

conView :: SymFPRoundingMode -> Maybe FPRoundingMode Source #

sym :: Symbol -> SymFPRoundingMode Source #

ssym :: Identifier -> SymFPRoundingMode Source #

isym :: Identifier -> Int -> SymFPRoundingMode Source #

ToCon SymFPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFPRoundingMode -> Maybe FPRoundingMode Source #

ToCon SymFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFPRoundingMode -> Maybe SymFPRoundingMode Source #

ToSym FPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: FPRoundingMode -> SymFPRoundingMode Source #

ToSym SymFPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: SymFPRoundingMode -> SymFPRoundingMode Source #

LinkedRep FPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode Source #

wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode Source #

Lift SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

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

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

ValidFP eb sb => UnifiedFPImpl 'S SymFP eb sb (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP

Associated Types

type GetFP 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFP 'S = SymFP
type GetFPRoundingMode 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFPRoundingMode 'S = SymFPRoundingMode

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymAlgReal Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymInteger Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymIntN n) Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymWordN n) Source #

ValidFP eb sb => IEEEFPConvertible SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymAlgReal -> SymFPRoundingMode -> SymFP eb sb -> SymAlgReal Source #

toFP :: SymFPRoundingMode -> SymAlgReal -> SymFP eb sb Source #

ValidFP eb sb => IEEEFPConvertible SymInteger (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymInteger -> SymFPRoundingMode -> SymFP eb sb -> SymInteger Source #

toFP :: SymFPRoundingMode -> SymInteger -> SymFP eb sb Source #

ValidFP eb sb => IEEEFPToAlgReal SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpToAlgReal :: SymAlgReal -> SymFP eb sb -> SymAlgReal Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymIntN n) (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymIntN n -> SymFPRoundingMode -> SymFP eb sb -> SymIntN n Source #

toFP :: SymFPRoundingMode -> SymIntN n -> SymFP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymWordN n) (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n Source #

toFP :: SymFPRoundingMode -> SymWordN n -> SymFP eb sb Source #

ValidFP eb sb => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fpAdd :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpSub :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpMul :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpDiv :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpFMA :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

fpSqrt :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source #

fpRoundToIntegral :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source #

(ValidFP eb sb, ValidFP eb' sb') => IEEEFPConvertible (SymFP eb' sb') (SymFP eb sb) SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

fromFPOr :: SymFP eb' sb' -> SymFPRoundingMode -> SymFP eb sb -> SymFP eb' sb' Source #

toFP :: SymFPRoundingMode -> SymFP eb' sb' -> SymFP eb sb Source #

type Rep SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type Rep SymFPRoundingMode = D1 ('MetaData "SymFPRoundingMode" "Grisette.Internal.SymPrim.SymFP" "grisette-0.12.0.0-2G8wsM3ZzbCKYYnSn6PeBx" 'True) (C1 ('MetaCons "SymFPRoundingMode" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term FPRoundingMode))))

type FunType SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type FunType SymFPRoundingMode = SymFPRoundingMode

type ConType SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type ConType SymFPRoundingMode = FPRoundingMode

type SymFPRoundingModeKey = AsKey SymFPRoundingMode Source #

SymFPRoundingMode type with identity equality.

Orphan instances

SymRep FPRoundingMode Source #

Instance details

Associated Types

type SymType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType FPRoundingMode = SymFPRoundingMode

LinkedRep FPRoundingMode SymFPRoundingMode Source #

Instance details

Methods

underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode Source #

wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode Source #

ValidFP eb sb => SymRep (FP eb sb) Source #

Instance details

Associated Types

type SymType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType (FP eb sb) = SymFP eb sb

ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb) Source #

Instance details

Methods

underlyingTerm :: SymFP eb sb -> Term (FP eb sb) Source #

wrapTerm :: Term (FP eb sb) -> SymFP eb sb Source #