Decimal sign operations

IEEE 754-2019 §5.5.1 specifies bit operations, including on noncanonical representations. Bits.copy, negate, abs, and copySign preserve every bit below the sign. They neither quiet signaling NaNs nor report exceptions. The corresponding datum operations retain the quantum and NaN metadata.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.isSignMinus : Datum → Bool

Read the sign, including the sign of a zero or NaN.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.withSign (negative : Bool) : Datum → Datum

Replace just the sign, without quieting a signaling NaN.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.copy (d : Datum) : Datum

Copy a complete datum. Stored-word copying is Bits.copy.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.abs (d : Datum) : Datum

Clear the sign, including on zeros and NaNs.

def FloatLib.Floats.Formats.DecimalInterchange.Datum.copySign (x y : Datum) : Datum

Preserve the first datum except for the sign supplied by the second.

def FloatLib.Floats.Formats.DecimalInterchange.Bits.copy (f : Format) (word : BitVec f.bitWidth) : BitVec f.bitWidth

Copy every bit, including noncanonical coefficient and special-value bits.

def FloatLib.Floats.Formats.DecimalInterchange.Bits.withSign (f : Format) (negative : Bool) (word : BitVec f.bitWidth) : BitVec f.bitWidth

Replace the stored sign while retaining all lower bits.

def FloatLib.Floats.Formats.DecimalInterchange.Bits.negate (f : Format) (word : BitVec f.bitWidth) : BitVec f.bitWidth

Reverse the stored sign, preserving signaling NaNs and noncanonical encodings.

def FloatLib.Floats.Formats.DecimalInterchange.Bits.abs (f : Format) (word : BitVec f.bitWidth) : BitVec f.bitWidth

Clear the stored sign without canonicalizing the representation.

def FloatLib.Floats.Formats.DecimalInterchange.Bits.copySign (f : Format) (x y : BitVec f.bitWidth) : BitVec f.bitWidth

Copy the second word's sign onto the otherwise unchanged first word.