Skip to main content

logicaffeine_compile/codegen_ana/
mod.rs

1//! LOGOS → **analog spatial fabric** (FPAA-style mixed-signal coprocessor) — the analog lane.
2//!
3//! Analog computing is inherently spatial: there is no program counter to run through continuous
4//! physics, so a computation is laid out as a topology and signals flow through it. This module
5//! lowers the float-dataflow region of a LOGOS program onto an analog execution plane (Kirchhoff
6//! current-summing adds, transconductance multiplies, OTA-C integrators) framed by a digital
7//! control plane (DAC/ADC strobes, sample-and-hold ticks).
8//!
9//! ## The trust model
10//! Everything except one arrow stays **exact**: the digital control plane, the gain-schedule
11//! rationals, calibration fixed-point, and the DAC/ADC quantizer functions. The single
12//! analog-uncertain arrow — DAC-out to ADC-in — is *bounded* (an `ErrorBudget` the compiler
13//! emits), *certified non-clipping* (a range certificate replayed by an independent checker),
14//! and *sampled/simulated* (fixed-seed Monte-Carlo, SPICE). ε is a compiler output derived from
15//! the artifact, never a hand-tuned test tolerance; `logos_approx_eq` is the ideal-tier floor
16//! and is never widened.
17//!
18//! ## Proof-regime firewall
19//! [`crate::codegen_sva`]'s value is exact ≡VM (SAT bitblast, byte-identical eval, iverilog
20//! diff). The analog lane is tolerance-≡ by physics, so it lives in its OWN ADL
21//! ([`target::AnalogTarget`]) and imports the digital fabric's extraction IR read-only —
22//! `codegen_sva` itself is untouched.
23//!
24//! ## Totality discipline (mirrors the Tenstorrent / RISC-V tiers)
25//! Every program gets a correct artifact or a NAMED refusal, never a silent miscompile:
26//! concurrency/networking → [`AnaLowerError::Unsupported`]; no float dataflow →
27//! [`AnaLowerError::NoAnalogRegion`]; float dataflow without declared input ranges →
28//! [`AnaLowerError::UnboundedInput`] (gain scaling without bounds would be a guess, and this
29//! lane does not guess). The `analog_op_coverage_lock` ratchet classifies all VM ops four ways
30//! (OnPlane / Boundary / ControlPlane / OffPlane) so nothing is silently dropped.
31
32pub mod calibrate;
33pub mod cell;
34pub mod control;
35pub mod dims;
36pub mod dynamics;
37pub mod effects;
38pub mod error_budget;
39pub mod eval;
40pub mod gain;
41pub mod int_lane;
42pub mod integrator;
43pub mod lower;
44pub mod nonideal;
45pub mod ontology;
46pub mod place;
47pub mod reduction;
48pub mod spice_emit;
49pub mod stack;
50pub mod stack_place;
51pub mod target;
52pub mod thermal;
53pub mod wta;
54pub mod xbar;
55
56pub use calibrate::{
57    apply_calibration, calibrate, error_budget_calibrated, v1_trim, CalibrationTable, TrimSpec,
58};
59pub use cell::{ASrc, AnalogCell, AnalogNetlist};
60pub use control::{ControlProgram, CtrlStep};
61pub use error_budget::{
62    error_budget, error_budget_chopped, error_budget_nonideal, ErrorSource, ErrorTerm, OutputBudget,
63};
64pub use eval::{eval_analog_dc, eval_analog_quantized, ConverterGrid};
65pub use gain::{scale_pass, to_range_claim, GainSchedule, MathBound, NetBound, RangeCertificate};
66pub use int_lane::analog_int_netlist_from_source;
67pub use integrator::{
68    analog_integrator_from_source, eval_analog_integrated, eval_analog_integrated_quantized,
69    integrator_error_budget, integrator_scale_pass, AnalogIntegrator, InitSrc,
70};
71pub use lower::analog_netlist_from_source;
72pub use nonideal::{
73    eval_analog_instance, eval_analog_instance_chopped, sample_instance, sky130_nonideal,
74    InstanceSample, NonIdealityModel, KSIGMA,
75};
76pub use place::{place_analog, place_blind, AnalogPlacement};
77pub use reduction::{
78    analog_int_reduction_from_source, analog_reduction_from_source, eval_analog_sampled,
79    eval_analog_sampled_quantized, reduction_error_budget, reduction_scale_pass, AnalogReduction,
80};
81pub use spice_emit::{emit_spice_dc, SPICE_ABSTOL, SPICE_RELTOL, SPICE_VNTOL};
82pub use target::{
83    AnaUnplaceable, AnalogCapability, AnalogCellKind, AnalogTarget, ALL_ANALOG_CELL_KINDS,
84};
85pub use xbar::{fold_crossbar, fold_crossbar_for};
86
87use crate::ast::stmt::{BinaryOpKind, Expr, Literal, Stmt};
88use crate::intern::Interner;
89use crate::vm::{CompiledProgram, Constant};
90
91/// The mixed-signal compilation artifact: the lowered region, its physical schedule and
92/// placement, the certificates and the budget, and the behavioral SPICE netlist (emitted at the
93/// declared input box's midpoint).
94#[derive(Debug, Clone, PartialEq)]
95pub struct AnalogArtifact {
96    pub fn_name: String,
97    pub netlist: AnalogNetlist,
98    pub schedule: GainSchedule,
99    pub cert: RangeCertificate,
100    pub budget: OutputBudget,
101    pub placement: AnalogPlacement,
102    pub spice: String,
103}
104
105/// The contract-free twin of a source: the `Assume` range-check lines stripped. The checks
106/// belong to the CONTROL PLANE (the digital side validates each word before the DAC fires, and
107/// runs them as ordinary bytecode in the digital fallback), so the region DATAFLOW both lanes
108/// lower is this twin — exposed for the mixed-signal composition to build its fallback configs
109/// from the same text the analog lane extracts.
110pub fn contract_free_twin(src: &str) -> String {
111    lower::source_without_range_contracts(src)
112}
113
114/// Which certified lane a region compiled through.
115#[derive(Clone, Copy, Debug, PartialEq, Eq)]
116pub enum RegionLane {
117    /// ε-certified float dataflow.
118    Float,
119    /// ½-grid-certified EXACT integer dataflow (calibrated budget).
120    Int,
121}
122
123/// Try to compile ONE region function on `target`, deciding the lane from its parameter
124/// family: float params → the ε-certified pipeline; else the certified-exact integer pipeline.
125/// PANIC-SAFE: extraction shapes outside the supported family become a typed refusal, never a
126/// crash — this is the entry the mixed-signal partition (and `compile_to_analog`) dispatches
127/// through for arbitrary programs.
128pub fn try_region(
129    src: &str,
130    fn_name: &str,
131    target: &AnalogTarget,
132) -> Result<(RegionLane, AnalogArtifact), AnaLowerError> {
133    let guard = |f: &dyn Fn() -> Result<AnalogArtifact, AnaLowerError>| {
134        std::panic::catch_unwind(std::panic::AssertUnwindSafe(f)).unwrap_or_else(|_| {
135            Err(AnaLowerError::UnloweredOp(
136                "region outside the supported extraction family".to_string(),
137            ))
138        })
139    };
140    match guard(&|| analog_artifact_from_source(src, fn_name, target)) {
141        Ok(art) => Ok((RegionLane::Float, art)),
142        // Not a float region — the integer lane decides (its own gates refuse non-int shapes).
143        Err(AnaLowerError::NoAnalogRegion) => {
144            guard(&|| analog_int_artifact_from_source(src, fn_name, target))
145                .map(|a| (RegionLane::Int, a))
146        }
147        Err(e) => Err(e),
148    }
149}
150
151/// The INTEGER pipeline for one region function: lower through the int lane, schedule, place,
152/// take the CALIBRATED physical budget (the product configuration — trims burned at final
153/// test), and PROVE exactness through the ½-grid gate before any artifact exists. An integer
154/// artifact is therefore certified-exact by construction: its budget is the proof.
155pub fn analog_int_artifact_from_source(
156    src: &str,
157    fn_name: &str,
158    target: &AnalogTarget,
159) -> Result<AnalogArtifact, AnaLowerError> {
160    let netlist = int_lane::analog_int_netlist_from_source(src, fn_name, target)?;
161    let ranges = int_lane::int_region_param_ranges(src, fn_name)?;
162    let (schedule, cert) = scale_pass(&netlist, &ranges, target)?;
163    let placement = place_analog(&schedule.quantized, target)?;
164    let model = sky130_nonideal();
165    let spec = calibrate::v1_trim(target);
166    let budget = error_budget_calibrated(
167        &netlist, &cert, &schedule, target, &model, &placement, &spec,
168    );
169    exactness_gate(&budget)?;
170    let mid: Vec<f64> = ranges
171        .iter()
172        .map(|r| ((r.lo + r.hi) / 2.0).round())
173        .collect();
174    let spice = spice_emit::emit_spice_dc(&schedule, target, &mid, "out.txt");
175    Ok(AnalogArtifact {
176        fn_name: fn_name.to_string(),
177        netlist,
178        schedule,
179        cert,
180        budget,
181        placement,
182        spice,
183    })
184}
185
186/// The full DAG-lane pipeline for one region function on one target: lower → schedule/certify →
187/// place → budget (physical, with the sourced non-ideality model) → behavioral SPICE.
188pub fn analog_artifact_from_source(
189    src: &str,
190    fn_name: &str,
191    target: &AnalogTarget,
192) -> Result<AnalogArtifact, AnaLowerError> {
193    let netlist = analog_netlist_from_source(src, fn_name, target)?;
194    let ranges = lower::region_param_ranges(src, fn_name)?;
195    let (schedule, cert) = scale_pass(&netlist, &ranges, target)?;
196    let placement = place_analog(&schedule.quantized, target)?;
197    let model = sky130_nonideal();
198    let budget = error_budget_nonideal(&netlist, &cert, &schedule, target, &model, &placement);
199    let mid: Vec<f64> = ranges.iter().map(|r| (r.lo + r.hi) / 2.0).collect();
200    let spice = spice_emit::emit_spice_dc(&schedule, target, &mid, "out.txt");
201    Ok(AnalogArtifact {
202        fn_name: fn_name.to_string(),
203        netlist,
204        schedule,
205        cert,
206        budget,
207        placement,
208        spice,
209    })
210}
211
212/// Why the analog tier declines a program — a SOUND refusal, never wrong silicon.
213#[derive(Debug, Clone, PartialEq)]
214pub enum AnaLowerError {
215    /// The program uses an op outside the mixed-signal SoC model (concurrency / networking).
216    Unsupported(&'static str),
217    /// The program has no float dataflow to map onto the analog plane.
218    NoAnalogRegion,
219    /// Float dataflow is present but an input has no declared range — refused, because gain
220    /// scaling without bounds would be a guess.
221    UnboundedInput(String),
222    /// An op inside the region has no witnessed analog tile — a named lowering gap, never a
223    /// silent drop.
224    UnloweredOp(String),
225    /// The integer lane's exactness proof failed: the error budget reaches or exceeds half an
226    /// integer grid step, so the rounded readout cannot be guaranteed to be the VM's integer.
227    /// Shrink the ranges/depth, use more converter bits, or calibrate.
228    ExactnessUnprovable { eps_math: f64 },
229    /// A declared range is empty (`lo > hi`) — no value can satisfy it, so no scaling or
230    /// certificate built on it can mean anything. Refused for bare and dimensioned contracts
231    /// alike (the runtime twin simply fires the impossible assert when reached).
232    ContradictoryContract { var: String, lo: f64, hi: f64 },
233    /// The relaxation lane's admission gate: no cited convergence theorem covers this system
234    /// (asymmetric, indefinite, malformed) — refused, never settled into a wrong answer.
235    ConvergenceUnprovable { reason: String },
236    /// The stack's thermal network has heat with nowhere to go (a floating island / no
237    /// cooling boundary) — no steady state exists, so no temperature map is emitted.
238    ThermalModelDisconnected,
239    /// The CERTIFIED temperature map's hottest junction exceeds the stack's declared cooling
240    /// budget — the same program may compile under a stronger cooling class; under this one
241    /// it refuses. "Meets its budget under forced-air cooling, proven" is the checker's
242    /// verdict, not the producer's word.
243    ThermalBudgetExceeded {
244        node: usize,
245        tier: usize,
246        t_junction_c: f64,
247        t_max_c: f64,
248        cooling: &'static str,
249    },
250    /// The settled answer's EXACT residual exceeds the demanded certificate budget — the run
251    /// is under-settled (or the demand unrealistic); no certificate is emitted.
252    ResidualExceedsBudget { linf: f64, required: f64 },
253    /// The netlist cannot be realized on the requested target.
254    Unplaceable(AnaUnplaceable),
255}
256
257impl std::fmt::Display for AnaLowerError {
258    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
259        match self {
260            AnaLowerError::Unsupported(what) => write!(f, "unsupported {what}"),
261            AnaLowerError::NoAnalogRegion => {
262                write!(f, "no analog region: the program has no float dataflow to map onto the analog plane")
263            }
264            AnaLowerError::UnboundedInput(msg) => write!(f, "unbounded input: {msg}"),
265            AnaLowerError::UnloweredOp(what) => write!(f, "unlowered op: {what}"),
266            AnaLowerError::ExactnessUnprovable { eps_math } => write!(
267                f,
268                "exactness unprovable: the error budget ε = {eps_math} reaches half an integer \
269                 grid step — shrink ranges/depth, add converter bits, or calibrate"
270            ),
271            AnaLowerError::ContradictoryContract { var, lo, hi } => write!(
272                f,
273                "contradictory contract: `{var}` is bounded to [{lo}, {hi}], an empty range — \
274                 no value can satisfy it"
275            ),
276            AnaLowerError::ConvergenceUnprovable { reason } => {
277                write!(f, "convergence unprovable: {reason}")
278            }
279            AnaLowerError::ThermalModelDisconnected => write!(
280                f,
281                "thermal model disconnected: heat has nowhere to go (floating island or no \
282                 cooling boundary) — no steady state exists"
283            ),
284            AnaLowerError::ThermalBudgetExceeded {
285                node,
286                tier,
287                t_junction_c,
288                t_max_c,
289                cooling,
290            } => write!(
291                f,
292                "thermal budget exceeded: node {node} (tier {tier}) reaches {t_junction_c} degC \
293                 against the declared {t_max_c} degC junction ceiling under {cooling} cooling — \
294                 use a stronger cooling class or a cooler layout"
295            ),
296            AnaLowerError::ResidualExceedsBudget { linf, required } => write!(
297                f,
298                "residual exceeds budget: ‖A·x̂ − b‖∞ = {linf} > required {required} — \
299                 under-settled or the demand is unrealistic; no certificate emitted"
300            ),
301            AnaLowerError::Unplaceable(u) => write!(f, "{u}"),
302        }
303    }
304}
305
306impl std::error::Error for AnaLowerError {}
307
308/// Returns `Some(reason)` if `program` uses an op with no home anywhere in the mixed-signal SoC
309/// model — concurrency (the analog control plane is a frame sequencer, not a thread pool) and
310/// networking (host-only IO). Everything else either maps to the plane, frames its boundary, or
311/// runs digitally VM-identical on the control side.
312pub fn unsupported_reason(program: &CompiledProgram) -> Option<&'static str> {
313    use crate::aot_unsupported::Offload;
314    crate::aot_unsupported::first(program).map(|o| match o {
315        Offload::Channel => "channel op (no channels in the mixed-signal SoC model)",
316        Offload::Task => {
317            "task spawn/await (the analog control plane is a frame sequencer, not a thread pool)"
318        }
319        Offload::VirtualTime => "virtual-time / select (needs a cooperative scheduler)",
320        Offload::Net => "networking op (host-only IO)",
321        Offload::Dom => "DOM / browser op (no document in the mixed-signal SoC model)",
322    })
323}
324
325/// Whether the program carries any float dataflow at all — the analog-region existence probe.
326/// A float constant in the pool is the witness; the region extractor sharpens this to the real
327/// dataflow graph when the lowering lands.
328fn has_float_dataflow(program: &CompiledProgram) -> bool {
329    program
330        .constants
331        .iter()
332        .any(|c| matches!(c, Constant::Float(_)))
333}
334
335/// The fail-closed refusal gate every analog compilation runs FIRST. `None` means the program
336/// clears the gate (an analog region exists, with declared ranges, inside the SoC model).
337pub fn analog_refusal(program: &CompiledProgram, ranges: &[AssumedRange]) -> Option<AnaLowerError> {
338    if let Some(reason) = unsupported_reason(program) {
339        return Some(AnaLowerError::Unsupported(reason));
340    }
341    if !has_float_dataflow(program) {
342        return Some(AnaLowerError::NoAnalogRegion);
343    }
344    if ranges.is_empty() {
345        return Some(AnaLowerError::UnboundedInput(
346            "float dataflow is present but no input has a declared range (`Assume x is between A and B.`)"
347                .to_string(),
348        ));
349    }
350    if let Some(r) = ranges.iter().find(|r| r.lo > r.hi) {
351        return Some(AnaLowerError::ContradictoryContract {
352            var: r.var.clone(),
353            lo: r.lo,
354            hi: r.hi,
355        });
356    }
357    None
358}
359
360/// The integer lane's ½-grid exactness proof: integer inputs on a grid-preserving region read
361/// back EXACTLY through the rounding ADC iff the compiler's own error budget stays under half
362/// a grid step. `Ok(())` is the exactness CERTIFICATE'S admission condition; the refusal
363/// carries the budget that broke so the diagnostic names the cost.
364pub fn exactness_gate(budget: &OutputBudget) -> Result<(), AnaLowerError> {
365    if budget.eps_math < 0.5 {
366        Ok(())
367    } else {
368        Err(AnaLowerError::ExactnessUnprovable {
369            eps_math: budget.eps_math,
370        })
371    }
372}
373
374/// A declared input range: `Assume x is between lo and hi.` (or the `Require that` spelling —
375/// the range IS the enforced `RuntimeAssert` shape, not the head keyword). The gain-scaling
376/// pass's input: a variable whose runtime value is CONTRACT-bounded to `[lo, hi]` on every tier.
377#[derive(Debug, Clone, PartialEq)]
378pub struct AssumedRange {
379    pub var: String,
380    pub lo: f64,
381    pub hi: f64,
382    /// The contract's physical dimension — recovered from the parser's quantity-bound fold
383    /// (`Assume v is between 0.2 volts and 0.7 volts.`). Bare numeric contracts carry
384    /// `Dimension::DIMENSIONLESS`. Metadata + coherence in this phase: the artifact bits are
385    /// identical to the bare twin's; netlist dimension propagation is a later phase.
386    pub dim: logicaffeine_base::dimension::Dimension,
387}
388
389/// Recover every declared range from a program's source — the source-level surface of
390/// [`assumed_ranges_in`], for callers outside the compile pipeline.
391pub fn assumed_ranges(source: &str) -> Vec<AssumedRange> {
392    crate::ui_bridge::with_parsed_program(source, |parsed, interner| match parsed {
393        Ok((stmts, _types, _pol)) => assumed_ranges_in(stmts, interner),
394        Err(_) => Vec::new(),
395    })
396}
397
398/// Recover every declared range from parsed statements: each enforced (`hard`) `RuntimeAssert`
399/// whose condition is the `between` desugar shape `lo <= x and x <= hi` with literal bounds.
400/// Walks function bodies and nested blocks — a contract is a contract wherever it is stated.
401pub fn assumed_ranges_in(stmts: &[Stmt<'_>], interner: &Interner) -> Vec<AssumedRange> {
402    let mut out = Vec::new();
403    collect_ranges(stmts, interner, &mut out);
404    out
405}
406
407fn collect_ranges(stmts: &[Stmt<'_>], interner: &Interner, out: &mut Vec<AssumedRange>) {
408    for stmt in stmts {
409        match stmt {
410            Stmt::RuntimeAssert {
411                condition,
412                hard: true,
413                dim,
414                reason: _,
415            } => {
416                if let Some((var, lo, hi)) = match_between(condition) {
417                    out.push(AssumedRange {
418                        var: interner.resolve(var).to_string(),
419                        lo,
420                        hi,
421                        dim: dim.unwrap_or(logicaffeine_base::dimension::Dimension::DIMENSIONLESS),
422                    });
423                }
424            }
425            Stmt::FunctionDef { body, .. } => collect_ranges(body, interner, out),
426            Stmt::If {
427                then_block,
428                else_block,
429                ..
430            } => {
431                collect_ranges(then_block, interner, out);
432                if let Some(e) = else_block {
433                    collect_ranges(e, interner, out);
434                }
435            }
436            Stmt::While { body, .. } | Stmt::Repeat { body, .. } => {
437                collect_ranges(body, interner, out)
438            }
439            _ => {}
440        }
441    }
442}
443
444/// A declared COLLECTION-LENGTH range: `Assume length of xs is between A and B.` — the streamed
445/// lane's frame bound (the control plane schedules `hi` frames; the runtime check enforces the
446/// contract on every tier, so a longer sequence fails loudly before the DAC ever fires).
447#[derive(Debug, Clone, PartialEq)]
448pub struct AssumedLenRange {
449    pub var: String,
450    pub lo: i64,
451    pub hi: i64,
452}
453
454/// Recover every declared length range from parsed statements (the `between` desugar over a
455/// `length of <ident>` operand, in an enforced `RuntimeAssert`).
456pub fn assumed_len_ranges_in(stmts: &[Stmt<'_>], interner: &Interner) -> Vec<AssumedLenRange> {
457    let mut out = Vec::new();
458    collect_len_ranges(stmts, interner, &mut out);
459    out
460}
461
462fn collect_len_ranges(stmts: &[Stmt<'_>], interner: &Interner, out: &mut Vec<AssumedLenRange>) {
463    for stmt in stmts {
464        match stmt {
465            Stmt::RuntimeAssert {
466                condition,
467                hard: true,
468                dim: _,
469                reason: _,
470            } => {
471                if let Some((var, lo, hi)) = match_len_between(condition) {
472                    out.push(AssumedLenRange {
473                        var: interner.resolve(var).to_string(),
474                        lo,
475                        hi,
476                    });
477                }
478            }
479            Stmt::FunctionDef { body, .. } => collect_len_ranges(body, interner, out),
480            Stmt::If {
481                then_block,
482                else_block,
483                ..
484            } => {
485                collect_len_ranges(then_block, interner, out);
486                if let Some(e) = else_block {
487                    collect_len_ranges(e, interner, out);
488                }
489            }
490            Stmt::While { body, .. } | Stmt::Repeat { body, .. } => {
491                collect_len_ranges(body, interner, out)
492            }
493            _ => {}
494        }
495    }
496}
497
498/// Match `lo <= length of xs and length of xs <= hi` with integer literal bounds.
499fn match_len_between(e: &Expr<'_>) -> Option<(crate::intern::Symbol, i64, i64)> {
500    let Expr::BinaryOp {
501        op: BinaryOpKind::And,
502        left,
503        right,
504    } = e
505    else {
506        return None;
507    };
508    let Expr::BinaryOp {
509        op: BinaryOpKind::LtEq,
510        left: lo,
511        right: lv,
512    } = left
513    else {
514        return None;
515    };
516    let Expr::BinaryOp {
517        op: BinaryOpKind::LtEq,
518        left: rv,
519        right: hi,
520    } = right
521    else {
522        return None;
523    };
524    let (Expr::Length { collection: ca }, Expr::Length { collection: cb }) = (lv, rv) else {
525        return None;
526    };
527    let (Expr::Identifier(a), Expr::Identifier(b)) = (ca, cb) else {
528        return None;
529    };
530    if a != b {
531        return None;
532    }
533    let int_lit = |e: &Expr<'_>| -> Option<i64> {
534        match e {
535            Expr::Literal(Literal::Number(n)) => Some(*n),
536            _ => None,
537        }
538    };
539    Some((*a, int_lit(lo)?, int_lit(hi)?))
540}
541
542/// Match the parser's `is between` desugar: `(lo <= x) and (x <= hi)` with literal numeric bounds.
543fn match_between(e: &Expr<'_>) -> Option<(crate::intern::Symbol, f64, f64)> {
544    let Expr::BinaryOp {
545        op: BinaryOpKind::And,
546        left,
547        right,
548    } = e
549    else {
550        return None;
551    };
552    let Expr::BinaryOp {
553        op: BinaryOpKind::LtEq,
554        left: lo,
555        right: lv,
556    } = left
557    else {
558        return None;
559    };
560    let Expr::BinaryOp {
561        op: BinaryOpKind::LtEq,
562        left: rv,
563        right: hi,
564    } = right
565    else {
566        return None;
567    };
568    let (Expr::Identifier(a), Expr::Identifier(b)) = (lv, rv) else {
569        return None;
570    };
571    if a != b {
572        return None;
573    }
574    Some((*a, numeric_literal(lo)?, numeric_literal(hi)?))
575}
576
577/// A literal numeric bound, including the negated spelling.
578fn numeric_literal(e: &Expr<'_>) -> Option<f64> {
579    match e {
580        Expr::Literal(Literal::Float(f)) => Some(*f),
581        Expr::Literal(Literal::Number(n)) => Some(*n as f64),
582        Expr::BinaryOp {
583            op: BinaryOpKind::Subtract,
584            left,
585            right,
586        } => {
587            // `-1.0` may parse as `0 - 1.0`; accept the zero-minus-literal spelling.
588            match (numeric_literal(left), numeric_literal(right)) {
589                (Some(l), Some(r)) if l == 0.0 => Some(-r),
590                _ => None,
591            }
592        }
593        _ => None,
594    }
595}