Copyright	(c) Galois Inc 2014-2022
License	BSD3
Maintainer	rdockins@galois.com
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

What4.FloatMode

Description

Desired instances for the IsInterpretedFloatExprBuilder class are selected via the different mode values from this module.

Synopsis

data FloatMode
data FloatModeRepr :: FloatMode -> Type where
type FloatIEEE = 'FloatIEEE
type FloatUninterpreted = 'FloatUninterpreted
type FloatReal = 'FloatReal

Documentation

data FloatMode Source #

Mode flag for how floating-point values should be interpreted.

Instances

Instances details

TestEquality FloatModeRepr Source #
Instance details Defined in What4.FloatMode Methods testEquality :: forall (a :: k) (b :: k). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) #
ShowF FloatModeRepr Source #
Instance details Defined in What4.FloatMode Methods withShow :: forall p q (tp :: k) a. p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) => a) -> a # showF :: forall (tp :: k). FloatModeRepr tp -> String # showsPrecF :: forall (tp :: k). Int -> FloatModeRepr tp -> String -> String #
KnownRepr FloatModeRepr FloatIEEE Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatIEEE #
KnownRepr FloatModeRepr FloatReal Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatReal #
KnownRepr FloatModeRepr FloatUninterpreted Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatUninterpreted #

data FloatModeRepr :: FloatMode -> Type where Source #

Constructors

FloatIEEERepr :: FloatModeRepr FloatIEEE
FloatUninterpretedRepr :: FloatModeRepr FloatUninterpreted
FloatRealRepr :: FloatModeRepr FloatReal

Instances

Instances details

TestEquality FloatModeRepr Source #
Instance details Defined in What4.FloatMode Methods testEquality :: forall (a :: k) (b :: k). FloatModeRepr a -> FloatModeRepr b -> Maybe (a :~: b) #
ShowF FloatModeRepr Source #
Instance details Defined in What4.FloatMode Methods withShow :: forall p q (tp :: k) a. p FloatModeRepr -> q tp -> (Show (FloatModeRepr tp) => a) -> a # showF :: forall (tp :: k). FloatModeRepr tp -> String # showsPrecF :: forall (tp :: k). Int -> FloatModeRepr tp -> String -> String #
KnownRepr FloatModeRepr FloatIEEE Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatIEEE #
KnownRepr FloatModeRepr FloatReal Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatReal #
KnownRepr FloatModeRepr FloatUninterpreted Source #
Instance details Defined in What4.FloatMode Methods knownRepr :: FloatModeRepr FloatUninterpreted #
Show (FloatModeRepr fm) Source #
Instance details Defined in What4.FloatMode Methods showsPrec :: Int -> FloatModeRepr fm -> ShowS # show :: FloatModeRepr fm -> String # showList :: [FloatModeRepr fm] -> ShowS #

type FloatIEEE = 'FloatIEEE Source #

In this mode "interpreted" floating-point values are treated as bit-precise IEEE-754 floats.

type FloatUninterpreted = 'FloatUninterpreted Source #

In this mode "interpreted" floating-point values are treated as bitvectors of the appropriate width, and all operations on them are translated as uninterpreted functions.

type FloatReal = 'FloatReal Source #

In this mode "interpreted" floating-point values are treated as real-number values, to the extent possible. Expressions that would result in infinities or NaN will yield unspecified values in this mode, or directly produce runtime errors.