Conversion and mixed arithmetic #
Name the destination type when converting a value or combining different formats:
abbrev Binary64 :=
ExecFloat.Binary (exponentBits := 11) (fractionBits := 52)
source.cast (target := Binary64)
ExecFloat.addAs (result := Binary64) left right
Each operation decodes its operands, maps them into the destination's exact domain through
ExactMap, and quantizes the result once. Casts pass infinities and exceptional observations to the
destination's
policy. Mixed arithmetic requires finite inputs and reports the first rejected operand; division
also rejects a denominator satisfying the exact domain's ExactZero predicate.
Binary destinations use SignedRat as their exact domain, so a signed zero survives a cast and
mixed addition, subtraction, and FMA select a cancellation sign from the destination's rounding
context. Posit destinations use Rat, with a single zero.
For longer finite calculations, ExactExpression.operand and roundOnce use the same path with
an ordinary Except-based do expression. Use ExactExpression.addWith and subWith when a
directed cancellation sign is required inside that expression. Conversion.Proof proves that each
entry point satisfies the destination's Quantization.Spec relation. These composition theorems
use the supplied exact-domain operations; numerical preservation of the maps and arithmetic hooks
is a separate family-specific obligation, as described in Conversion.Core.
Decode one source through its canonical exact-domain capability.
Instances For
Decode a source and embed its finite payload into the destination computation domain.
Infinity signs and exceptional observations are preserved structurally by NumericalValue.map.
Instances For
Quantize one complete exact observation with explicit destination context.
Instances For
Convert any exactly decodable source into a named destination under family-specific context.
This function-form API also supports sources outside the ExecFloat carrier when an integration
module supplies their exact decoder. Ordinary ExecFloat values may also use
value.castWith through field notation.
Instances For
Convert any exactly decodable source using the destination's canonical context.
Instances For
Convert an ExecFloat value under explicit destination context, with field notation.
The source type lets Lean resolve value.castWith; the destination can be a local alias such as
Binary64 or Posit32. Use convertWith for source types outside ExecFloat.
Instances For
Convert an ExecFloat value using the destination's canonical context.
Instances For
Extract a finite operand or report its exact non-finite observation and position.
Instances For
Prepare exact finite binary arithmetic, checking the left operand before the right.
Instances For
Prepare exact finite division and reject a zero exact denominator.
ExactZero states and decides which values the exact domain declares to be zero. Domains with
several zero representations justify that choice in their own bridge theorems, not in this
algorithm.
Instances For
Prepare finite fused multiply-add using a supplied exact addition and no intermediate rounding.
Instances For
Prepare exact finite fused multiply-add with the exact domain's ordinary addition.
Instances For
Quantize a prepared exact input, preserving a preparation failure verbatim.
Instances For
Relational contract for preparation followed by one destination quantization.
Instances For
Decode one numbered operand into the exact domain used by an enclosing expression.
Finite inputs are mapped without rounding through ExactMap. The chosen exact domain determines
which representation metadata survives; mapping a SignedRat into Rat forgets its zero sign.
Infinity and exceptional observations become position-indexed failures, so a longer expression
still reports which operand was rejected.
Instances For
Add exact values under the destination context without quantizing.
For signed-rational destinations this selects the sign of exact cancellation before a later
roundOnceWith. Name result when the context alone does not determine the destination type.
Instances For
Subtract exact values using the destination's cancellation-sign rule, without quantizing.
Instances For
Divide two exact finite values, rejecting a denominator declared zero by ExactZero.
Use this inside a do expression. Ordinary exact-domain operations remain available for
calculations without an additional failure case; addWith and subWith also respect the
destination's cancellation-sign rule.
Instances For
Lift a successful exact scalar into the complete finite observation expected by a quantizer.
Instances For
Evaluate an exact scalar expression and quantize its result once under an explicit context.
The expression may contain any executable operation supported by its exact domain. A failed
operand or checked division bypasses the quantizer and is returned unchanged.
For signed-rational binary destinations that support signed zero, quantization preserves the
supplied zero sign; it cannot recover how that zero arose. Ordinary SignedRat addition and
subtraction use their nearest-even cancellation convention. For directed cancellation, use
ExactExpression.addWith and subWith with the intended destination and context.
Instances For
Evaluate an exact scalar expression and quantize its result once using the default context.
Instances For
Add finite values exactly and quantize once into result under explicit context.
Instances For
Add finite values exactly and quantize once using the destination's canonical context.
Instances For
Subtract finite values exactly and quantize once into result under explicit context.
Instances For
Subtract finite values exactly and quantize once using the destination's canonical context.
Instances For
Multiply finite values exactly and quantize once into result under explicit context.
Instances For
Multiply finite values exactly and quantize once using the destination's canonical context.
Instances For
Divide finite values exactly and quantize once into result under explicit context.
Instances For
Divide finite values exactly and quantize once using the destination's canonical context.
Instances For
Compute finite left * right + addend exactly and quantize once into result.
The exact product is added to addend under the context's cancellation-sign rule before the
destination quantizer runs.
Instances For
Fused multiply-add using the destination's canonical quantization context.