axiolid_exact/
certify.rs

1//! The two-tier driver: interval filter first, exact fallback second.
2
3use axiolid_guarantees::{Certified, Precision, Sign};
4
5use crate::arith::Arith;
6use crate::dyadic::Dyadic;
7use crate::interval::Interval;
8
9/// Why an exact computation was refused.
10#[non_exhaustive]
11#[derive(Debug, Clone, Copy, PartialEq, Eq)]
12pub enum ExactError {
13    /// An input was NaN or infinite. Exact values exist only for finite
14    /// numbers.
15    NonFinite,
16    /// A line's two defining points coincide, so it has no direction.
17    DegenerateLine,
18    /// A circle's radius was negative.
19    NegativeRadius,
20    /// Two parameters were compared along different lines, where
21    /// parameters mean different things.
22    DifferentLines,
23    /// The expression has no real value in exact arithmetic (for example a
24    /// square root of a negative number). A construction that validated its
25    /// inputs never reports this.
26    Undefined,
27    /// More nested square roots than [`crate::tower::MAX_DEPTH`]: cost
28    /// grows exponentially with depth, so the tower refuses rather than
29    /// run unboundedly.
30    TooDeep,
31    /// A conic whose quadratic part is identically zero (it is a line), or
32    /// a conic pair no admissible shear could separate.
33    DegenerateConic,
34}
35
36/// Refuse NaN and infinities before any arithmetic runs.
37pub fn require_finite(values: &[f64]) -> Result<(), ExactError> {
38    if values.iter().all(|value| value.is_finite()) {
39        Ok(())
40    } else {
41        Err(ExactError::NonFinite)
42    }
43}
44
45/// A sign question, written once and evaluable in any [`Arith`].
46///
47/// Implementors build their polynomial from `T::from_f64` of the inputs and
48/// return `None` only when `T` cannot decide. The same code then runs as
49/// the interval filter and as the exact fallback.
50pub trait SignExpr {
51    /// The sign in arithmetic `T`, or `None` when `T` cannot decide.
52    fn sign_in<T: Arith>(&self) -> Option<Sign>;
53}
54
55/// The interval filter alone, so escalation can be observed and measured.
56///
57/// [`Certified::Uncertain`] means the exact tier is needed.
58pub fn filter<E: SignExpr>(expr: &E) -> Certified {
59    match expr.sign_in::<Interval>() {
60        Some(sign) => Certified::Certain {
61            sign,
62            precision: Precision::F64,
63        },
64        None => Certified::Uncertain {
65            attempted: Precision::F64,
66        },
67    }
68}
69
70/// The proven sign: filter, then exact arithmetic if the filter was
71/// undecided.
72///
73/// Callers must have checked their inputs are finite
74/// ([`require_finite`]); the exact tier has no value for NaN or infinity.
75pub fn certify<E: SignExpr>(expr: &E) -> Result<Sign, ExactError> {
76    if let Some(sign) = expr.sign_in::<Interval>() {
77        return Ok(sign);
78    }
79    expr.sign_in::<Dyadic>().ok_or(ExactError::Undefined)
80}
axiolid_exact/certify.rs

axiolid_exact/
certify.rs
