| 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.Core.Data.Class.BitCast
Description
Synopsis
- class BitCast from to where
- bitCast :: from -> to
- class BitCastCanonical from to where
- bitCastCanonicalValue :: proxy from -> to
- class BitCastOr from to where
- bitCastOr :: to -> from -> to
- bitCastOrCanonical :: BitCastOrCanonical from to => from -> to
- type BitCastOrCanonical a b = (BitCastCanonical a b, BitCastOr a b)
Documentation
class BitCast from to where Source #
Type class for bit-casting between types.
Special Considerations for Floating-Point Types:
Typically, bit-casting a value from type a to type b and then back to
type a should result in the original value. However, this is not always
true for floating-point values. In SMT-LIB2, there is only one NaN value with
multiple bit representations.
Given this, we do not provide BitCast for the FP type,
instead, we use the bitCastOrCanonical function to use a canonical
representation for the NaN values.
If your application requires distinguishing between different NaN values, it is recommended to define your own floating-point type using bit-vectors. This allows you to check for NaN values and perform operations by bitcasting back to the provided floating-point types when they are not NaN values.
Instances
class BitCastCanonical from to where Source #
The canonical value when the bitcast cannot be precisely performed.
For example, with SMT-LIB2, there is only one NaN for floating point numbers,
with multiple bit representations. Our underlying FP type
also follows this convention. This means that we cannot precisely bitcast a
FP to other types. So instead, we bitcast the NaN value
to a canonical representation, defined with this type class.
Methods
bitCastCanonicalValue :: proxy from -> to Source #
Instances
class BitCastOr from to where Source #
Bitcasting a value. If the value cannot be precisely bitcast, use the default value.
Instances
| BitCastOr FP16 Int16 Source # | |
| BitCastOr FP16 Word16 Source # | |
| BitCastOr FP32 Int32 Source # | |
| BitCastOr FP32 Word32 Source # | |
| BitCastOr FP32 Float Source # | |
| BitCastOr FP64 Int64 Source # | |
| BitCastOr FP64 Word64 Source # | |
| BitCastOr FP64 Double Source # | |
| (ValidFP eb sb, n ~ (eb + sb)) => BitCastOr (FP eb sb) (IntN n) Source # | |
| (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r) Source # | |
| (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymIntN r) Source # | |
| (ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (SymFP eb sb) (SymWordN r) Source # | |
bitCastOrCanonical :: BitCastOrCanonical from to => from -> to Source #
Bitcasting a value and when the value cannot be precisely bitcast, use the canonical value.
type BitCastOrCanonical a b = (BitCastCanonical a b, BitCastOr a b) Source #
Constraint for bitcasting a value and when the value cannot be precisely bitcast, use the canonical value.