Integer destination ranges

A range check follows exact rational-to-integer rounding. The caller supplies the integer rounder and the policy for failure, allowing IEEE invalid results and Posit integer sentinels to share the same numerical range calculation. Signed and unsigned words are instances of an inclusive integer interval.

structure FloatLib.Numerics.IntegerRange : Type

An inclusive integer interval. Empty intervals are permitted and reject every result.

• lower : ℤ

  Inclusive lower endpoint of the accepted integer interval.

• upper : ℤ

  Inclusive upper endpoint; an endpoint below lower gives an empty interval.

def FloatLib.Numerics.instDecidableEqIntegerRange.decEq (x✝ x✝¹ : IntegerRange) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqIntegerRange : DecidableEq IntegerRange

def FloatLib.Numerics.instReprIntegerRange.repr : IntegerRange → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.instReprIntegerRange : Repr IntegerRange

def FloatLib.Numerics.IntegerRange.Contains (range : IntegerRange) (value : ℤ) : Prop

Membership in the inclusive destination interval.

@[instance_reducible]

instance FloatLib.Numerics.instDecidableContains (range : IntegerRange) (value : ℤ) : Decidable (range.Contains value)

def FloatLib.Numerics.IntegerRange.round? (range : IntegerRange) (round : ℚ → ℤ) (value : ℚ) : Option ℤ

Round first, then test the resulting integer against the destination interval.

inductive FloatLib.Numerics.IntegerFormat : Type

Signedness and width specify the ordinary numerical range of a word. Reserved bit patterns are a separate format-specific conversion policy.

• signed (width : ℕ) : IntegerFormat

  Two's-complement numerical range, with width zero containing only zero.

• unsigned (width : ℕ) : IntegerFormat

  Unsigned numerical range from zero through 2 ^ width - 1.

def FloatLib.Numerics.instDecidableEqIntegerFormat.decEq (x✝ x✝¹ : IntegerFormat) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Numerics.instDecidableEqIntegerFormat : DecidableEq IntegerFormat

def FloatLib.Numerics.instReprIntegerFormat.repr : IntegerFormat → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Numerics.instReprIntegerFormat : Repr IntegerFormat

def FloatLib.Numerics.IntegerFormat.minValue : IntegerFormat → ℤ

Smallest integer accepted by the word format.

def FloatLib.Numerics.IntegerFormat.maxValue : IntegerFormat → ℤ

Largest integer accepted by the word format.

def FloatLib.Numerics.IntegerFormat.range (destination : IntegerFormat) : IntegerRange

Inclusive numerical range; width zero denotes only zero for either signedness.

@[reducible, inline]

abbrev FloatLib.Numerics.IntegerFormat.InRange (destination : IntegerFormat) (value : ℤ) : Prop

Numerical representability, independently of any reserved bit pattern.