lemma/computation/

arithmetic.rs

//! Type-aware arithmetic operations

use crate::computation::operation_result::{OperationResult, VetoType};
use crate::computation::rational::{
    rational_operation, rational_operation_with_fallback, NumericFailure, NumericOperation,
    RationalInteger,
};
use crate::planning::semantics::{
    ArithmeticComputation, BoundValueKind, LemmaType, LiteralValue, TypeFamily, TypedLiteral,
    ValueKind,
};
use indexmap::IndexMap;
use serde::Serialize;
use std::sync::Arc;

/// One resolved unit in a signature: declared name, owning family, exponent.
#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize)]
pub struct SignatureFactor {
    pub name: String,
    pub family: TypeFamily,
    pub exponent: i32,
}

/// Reverse index mapping a resolved unit signature to the unit (by name) and its owning measure type.
pub type SignatureIndex = IndexMap<Vec<SignatureFactor>, (String, Arc<LemmaType>)>;

/// Find the one indexed unit whose factor names and exponents match `names`.
/// Two families with the same names are not one unit.
pub(crate) fn find_by_names<'a>(
    index: &'a SignatureIndex,
    names: &[(String, i32)],
) -> Option<&'a (String, Arc<LemmaType>)> {
    let mut matched = None;
    for (factors, value) in index.iter() {
        if factors.len() != names.len() {
            continue;
        }
        let mut left: Vec<(&str, i32)> = factors
            .iter()
            .map(|factor| (factor.name.as_str(), factor.exponent))
            .collect();
        let mut right: Vec<(&str, i32)> = names
            .iter()
            .map(|(name, exponent)| (name.as_str(), *exponent))
            .collect();
        left.sort();
        right.sort();
        if left != right {
            continue;
        }
        if matched.is_some() {
            return None;
        }
        matched = Some(value);
    }
    matched
}

struct CalendarRangeShiftIndexes<'a> {
    signature_index: &'a SignatureIndex,
    endpoint_type: &'a Arc<LemmaType>,
    calendar_type: &'a Arc<LemmaType>,
}

/// Expand a raw signature (literal unit names) to derived base units, so that signature_index
/// (which is keyed by `derived_measure_factors`) can be searched.
///
/// For each `(unit_name, exp)`:
/// - Look up `unit_name`'s owning type in `unit_index`.
/// - Replace it with its `derived_measure_factors`, scaled by `exp`.
/// - When multiple units from the same family appear, normalize them to the canonical
///   unit name so exponents can cancel (e.g. `hour` and `minute` both become `second`).
/// - Single remaining units keep their declared name (e.g. `minute` stays `minute`).
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
enum SignatureFamily {
    Calendar,
    Measure(crate::planning::semantics::TypeFamily),
}

fn measure_family_key(
    unit_name: &str,
    unit_index: &crate::planning::unit_index::UnitIndex,
    typed_owners: &[&LemmaType],
) -> Option<SignatureFamily> {
    use crate::planning::semantics::calendar_unit_factor;
    if calendar_unit_factor(unit_name).is_some() {
        return Some(SignatureFamily::Calendar);
    }
    unit_index
        .owning_type_for_signature_factor(unit_name, typed_owners)
        .and_then(|t| t.measure_family().cloned())
        .map(SignatureFamily::Measure)
}

/// Factor-1 unit of `family`; `None` when the family declares no such unit.
fn canonical_unit_in_family(
    family: &SignatureFamily,
    unit_index: &crate::planning::unit_index::UnitIndex,
) -> Option<String> {
    use crate::planning::semantics::TypeSpecification;
    let SignatureFamily::Measure(family) = family else {
        return Some("month".to_string());
    };
    let lemma_type = unit_index.family_root(family)?;
    match &lemma_type.specifications {
        TypeSpecification::Measure { units, .. } => units
            .iter()
            .find(|unit| unit.is_canonical_factor())
            .map(|canonical| canonical.name.clone()),
        _ => None,
    }
}

pub(crate) fn expand_signature_to_base_units(
    raw: &[(String, i32)],
    unit_index: &crate::planning::unit_index::UnitIndex,
    typed_owners: &[&LemmaType],
) -> Vec<(String, i32)> {
    use crate::planning::semantics::canonicalize_signature;
    use crate::planning::semantics::TypeSpecification;
    use std::collections::BTreeMap;
    let mut expanded: Vec<(String, i32)> = Vec::new();
    for (unit_name, exp) in raw {
        if let Some(owning_type) =
            unit_index.owning_type_for_signature_factor(unit_name, typed_owners)
        {
            if let TypeSpecification::Measure { units, .. } = &owning_type.specifications {
                if let Ok(unit) = units.get(unit_name) {
                    if !unit.derived_measure_factors.is_empty() {
                        for (base_name, base_exp) in &unit.derived_measure_factors {
                            expanded.push((
                                base_name.clone(),
                                base_exp.checked_mul(*exp).expect(
                                    "BUG: planning bounds declared and signature unit exponents",
                                ),
                            ));
                        }
                        continue;
                    }
                }
            }
        }
        expanded.push((unit_name.clone(), *exp));
    }
    expanded = canonicalize_signature(&expanded);

    let mut by_family: BTreeMap<SignatureFamily, Vec<(String, i32)>> = BTreeMap::new();
    let mut ungrouped: Vec<(String, i32)> = Vec::new();
    for (unit_name, exp) in expanded {
        if let Some(family) = measure_family_key(&unit_name, unit_index, typed_owners) {
            by_family.entry(family).or_default().push((unit_name, exp));
        } else {
            ungrouped.push((unit_name, exp));
        }
    }

    let mut normalized = ungrouped;
    for (family, entries) in by_family {
        let distinct: std::collections::BTreeSet<&str> =
            entries.iter().map(|(name, _)| name.as_str()).collect();
        let canonical = (distinct.len() > 1)
            .then(|| canonical_unit_in_family(&family, unit_index))
            .flatten();
        match canonical {
            Some(canonical) => {
                let net_exp: i32 = entries
                    .iter()
                    .try_fold(0i32, |sum, (_, exp)| sum.checked_add(*exp))
                    .expect("BUG: planning bounds family unit exponents");
                if net_exp != 0 {
                    normalized.push((canonical, net_exp));
                }
            }
            None => normalized.extend(entries),
        }
    }
    canonicalize_signature(&normalized)
}

fn number_op_on_stored_rationals(
    left: &RationalInteger,
    operator: &ArithmeticComputation,
    right: &RationalInteger,
) -> OperationResult {
    match number_arithmetic(left, operator, right) {
        Ok(rational) => OperationResult::from_literal(LiteralValue::number(rational)),
        Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
    }
}

fn number_ratio_arithmetic(
    left: &RationalInteger,
    op: &ArithmeticComputation,
    right: &RationalInteger,
) -> Result<RationalInteger, NumberArithmeticFailure> {
    match op {
        ArithmeticComputation::Multiply | ArithmeticComputation::Divide => {
            rational_operation(left, numeric_operation_from_arithmetic(op), right)
                .map_err(map_numeric_failure)
        }
        ArithmeticComputation::Power => {
            rational_operation_with_fallback(left, NumericOperation::Power, right)
                .map_err(map_numeric_failure)
        }
        ArithmeticComputation::Modulo => rational_operation(left, NumericOperation::Modulo, right)
            .map_err(|f| {
                if matches!(f, NumericFailure::DivisionByZero) {
                    NumberArithmeticFailure::ModuloByZero
                } else {
                    map_numeric_failure(f)
                }
            }),
        ArithmeticComputation::Add | ArithmeticComputation::Subtract => {
            unreachable!("BUG: number/ratio add-subtract rejected during planning")
        }
    }
}

fn calendar_from_months_arithmetic(
    left: &RationalInteger,
    operator: &ArithmeticComputation,
    right: &RationalInteger,
) -> OperationResult {
    let result_months = match operator {
        ArithmeticComputation::Add => {
            match rational_operation(left, NumericOperation::Add, right) {
                Ok(r) => r,
                Err(failure) => {
                    return OperationResult::Veto(VetoType::computation(
                        map_numeric_failure(failure).message(),
                    ))
                }
            }
        }
        ArithmeticComputation::Subtract => {
            match rational_operation(left, NumericOperation::Subtract, right) {
                Ok(r) => r,
                Err(failure) => {
                    return OperationResult::Veto(VetoType::computation(
                        map_numeric_failure(failure).message(),
                    ))
                }
            }
        }
        _ => unreachable!(
            "BUG: calendar_from_months_arithmetic called with {:?}; planning rejects this",
            operator
        ),
    };

    OperationResult::from_literal(LiteralValue::measure(result_months))
}

/// Perform type-aware arithmetic operation, returning OperationResult (Veto for runtime errors).
///
/// `expression_units` and `signature_index` come from the plan's resolved types and are
/// used during expression evaluation to resolve combined unit signatures back to a named
/// unit and owning type.
pub fn arithmetic_operation(
    left: &crate::planning::semantics::BoundValueKind,
    left_type: &Arc<LemmaType>,
    op: &ArithmeticComputation,
    right: &crate::planning::semantics::BoundValueKind,
    right_type: &Arc<LemmaType>,
    signature_index: &SignatureIndex,
) -> OperationResult {
    match (&left.value, &right.value) {
        (ValueKind::Range(range_left, range_right), ValueKind::Measure(value))
            if left_type.is_calendar_like_range()
                && right_type.is_calendar_like()
                && matches!(
                    op,
                    ArithmeticComputation::Add | ArithmeticComputation::Subtract
                ) =>
        {
            let endpoint_type = left_type
                .specifications
                .element_from_range()
                .map(|element| Arc::new(LemmaType::primitive(element)))
                .unwrap_or_else(|| Arc::clone(left_type));
            shift_calendar_range_right_endpoint(
                range_left.as_ref(),
                range_right.as_ref(),
                value,
                matches!(op, ArithmeticComputation::Add),
                &CalendarRangeShiftIndexes {
                    signature_index,
                    endpoint_type: &endpoint_type,
                    calendar_type: right_type,
                },
            )
        }

        (ValueKind::Measure(value), ValueKind::Range(range_left, range_right))
            if right_type.is_calendar_like_range()
                && left_type.is_calendar_like()
                && matches!(
                    op,
                    ArithmeticComputation::Add | ArithmeticComputation::Subtract
                ) =>
        {
            let endpoint_type = right_type
                .specifications
                .element_from_range()
                .map(|element| Arc::new(LemmaType::primitive(element)))
                .unwrap_or_else(|| Arc::clone(right_type));
            shift_calendar_range_right_endpoint(
                range_left.as_ref(),
                range_right.as_ref(),
                value,
                matches!(op, ArithmeticComputation::Add),
                &CalendarRangeShiftIndexes {
                    signature_index,
                    endpoint_type: &endpoint_type,
                    calendar_type: left_type,
                },
            )
        }

        (ValueKind::Range(range_left, range_right), ValueKind::Measure(value))
            if left_type.is_date_range()
                && right_type.is_calendar_like()
                && matches!(
                    op,
                    ArithmeticComputation::Add | ArithmeticComputation::Subtract
                ) =>
        {
            shift_date_range_right_endpoint(
                range_left.as_ref(),
                range_right.as_ref(),
                value,
                matches!(op, ArithmeticComputation::Add),
                Arc::clone(right_type),
            )
        }

        (ValueKind::Measure(value), ValueKind::Range(range_left, range_right))
            if right_type.is_date_range()
                && left_type.is_calendar_like()
                && matches!(
                    op,
                    ArithmeticComputation::Add | ArithmeticComputation::Subtract
                ) =>
        {
            shift_date_range_right_endpoint(
                range_left.as_ref(),
                range_right.as_ref(),
                value,
                matches!(op, ArithmeticComputation::Add),
                Arc::clone(left_type),
            )
        }

        (
            ValueKind::Range(left_range_left, left_range_right),
            ValueKind::Range(right_range_left, right_range_right),
        ) if matches!(
            op,
            ArithmeticComputation::Add | ArithmeticComputation::Subtract
        ) =>
        {
            let left_measure =
                super::range::compute_span(left_range_left.as_ref(), left_range_right.as_ref());
            let right_measure =
                super::range::compute_span(right_range_left.as_ref(), right_range_right.as_ref());
            let left_span_ty = super::range::span_result_type(left_type);
            let right_span_ty = super::range::span_result_type(right_type);
            operate_on_operation_results(
                left_measure,
                &left_span_ty,
                op,
                right_measure,
                &right_span_ty,
                signature_index,
            )
        }

        (ValueKind::Range(range_left, range_right), _)
            if matches!(
                op,
                ArithmeticComputation::Add | ArithmeticComputation::Subtract
            ) =>
        {
            let measure = super::range::compute_span(range_left.as_ref(), range_right.as_ref());
            let span_ty = super::range::span_result_type(left_type);
            operate_with_left_result(measure, &span_ty, op, right, right_type, signature_index)
        }

        (_, ValueKind::Range(range_left, range_right))
            if matches!(
                op,
                ArithmeticComputation::Add | ArithmeticComputation::Subtract
            ) =>
        {
            let measure = super::range::compute_span(range_left.as_ref(), range_right.as_ref());
            let span_ty = super::range::span_result_type(right_type);
            operate_with_right_result(left, left_type, op, measure, &span_ty, signature_index)
        }

        _ => scalar_arithmetic(left, left_type, op, right, right_type, signature_index),
    }
}

/// Arithmetic on operands that are not ranges. Never re-enters [`arithmetic_operation`], so
/// the range helpers that call it are not part of a cycle.
pub(crate) fn scalar_arithmetic(
    left: &crate::planning::semantics::BoundValueKind,
    left_type: &Arc<LemmaType>,
    op: &ArithmeticComputation,
    right: &crate::planning::semantics::BoundValueKind,
    right_type: &Arc<LemmaType>,
    signature_index: &SignatureIndex,
) -> OperationResult {
    match (&left.value, &right.value) {
        (ValueKind::Number(l), ValueKind::Number(r)) => number_op_on_stored_rationals(l, op, r),

        (ValueKind::Date(_), _) | (_, ValueKind::Date(_)) => super::datetime::datetime_arithmetic(
            &left.to_literal(),
            left_type,
            op,
            &right.to_literal(),
            right_type,
        ),

        (ValueKind::Time(_), _) | (_, ValueKind::Time(_)) => super::datetime::time_arithmetic(
            &left.to_literal(),
            left_type,
            op,
            &right.to_literal(),
            right_type,
        ),

        // Number op Ratio → Number (multiply is symmetric; divide/power preserve order)
        (ValueKind::Number(n), ValueKind::Ratio(r)) => {
            if matches!(op, ArithmeticComputation::Modulo) {
                unreachable!("BUG: number modulo ratio is rejected during planning");
            }
            match number_ratio_arithmetic(n, op, r) {
                Ok(rational) => OperationResult::from_literal(LiteralValue::number(rational)),
                Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
            }
        }
        // Ratio op Number → result type depends on operator
        (ValueKind::Ratio(r), ValueKind::Number(n)) => match op {
            ArithmeticComputation::Multiply => match number_ratio_arithmetic(r, op, n) {
                Ok(rational) => OperationResult::from_literal(LiteralValue::number(rational)),
                Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
            },
            ArithmeticComputation::Modulo => {
                unreachable!("BUG: ratio modulo number is rejected during planning");
            }
            ArithmeticComputation::Divide | ArithmeticComputation::Power => {
                match number_ratio_arithmetic(r, op, n) {
                    Ok(rational) => OperationResult::from_bound(BoundValueKind {
                        value: ValueKind::Ratio(rational),
                        unit: left.unit.clone(),
                        instance_factors: None,
                    }),
                    Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
                }
            }
            _ => unreachable!(
                "BUG: ratio {:?} number; add/subtract rejected during planning",
                op
            ),
        },

        // Ratio op Ratio → Ratio
        (ValueKind::Ratio(l), ValueKind::Ratio(r)) => {
            if matches!(op, ArithmeticComputation::Modulo) {
                unreachable!("BUG: ratio modulo ratio is rejected during planning");
            }
            match number_arithmetic(l, op, r) {
                Ok(rational) => OperationResult::from_bound(BoundValueKind {
                    value: ValueKind::Ratio(rational),
                    unit: BoundValueKind::agree_or_left_binding(
                        left.unit.as_ref(),
                        right.unit.as_ref(),
                    ),
                    instance_factors: None,
                }),
                Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
            }
        }
        // Measure operations with Measure
        (ValueKind::Measure(l_val), ValueKind::Measure(r_val)) => {
            if left_type.is_calendar_like() != right_type.is_calendar_like() {
                let is_measure_left = left_type.is_measure() && !left_type.is_calendar_like();
                let is_multiply = matches!(op, ArithmeticComputation::Multiply);
                let is_divide = matches!(op, ArithmeticComputation::Divide);
                if !is_multiply && !is_divide {
                    unreachable!("BUG: measure {:?} calendar is rejected during planning", op);
                }
                let (l_val_ref, r_val_ref) = if is_measure_left {
                    (l_val, r_val)
                } else {
                    (r_val, l_val)
                };
                if is_divide && crate::computation::rational::rational_is_zero(r_val_ref) {
                    return OperationResult::Veto(VetoType::computation(
                        "Division by zero is not allowed.",
                    ));
                }
                let raw_result = match rational_operation(
                    l_val_ref,
                    if is_multiply {
                        NumericOperation::Multiply
                    } else {
                        NumericOperation::Divide
                    },
                    r_val_ref,
                ) {
                    Ok(p) => p,
                    Err(failure) => {
                        return OperationResult::Veto(VetoType::computation(
                            map_numeric_failure(failure).message(),
                        ))
                    }
                };
                let q_decomp = if is_measure_left {
                    left_type.measure_type_decomposition()
                } else {
                    right_type.measure_type_decomposition()
                }
                .expect("BUG: decomposition must be resolved after planning");
                let c_decomp = crate::planning::semantics::calendar_decomposition();
                let combined = crate::planning::semantics::combine_decompositions(
                    q_decomp,
                    &c_decomp,
                    is_multiply,
                )
                .expect("BUG: planning bounds combined unit exponents");
                if combined.is_empty() {
                    return OperationResult::from_literal(LiteralValue::number(raw_result));
                }
                return OperationResult::from_bound(BoundValueKind::unbound(ValueKind::Measure(
                    raw_result,
                )));
            }
            if left_type.is_calendar_like() && right_type.is_calendar_like() {
                return match op {
                    ArithmeticComputation::Add | ArithmeticComputation::Subtract => {
                        calendar_from_months_arithmetic(l_val, op, r_val)
                    }
                    ArithmeticComputation::Divide => {
                        number_op_on_stored_rationals(l_val, &ArithmeticComputation::Divide, r_val)
                    }
                    _ => unreachable!(
                        "BUG: calendar * calendar with op {:?}; planning should have rejected this",
                        op
                    ),
                };
            }
            if left_type.is_calendar_like() && !right_type.is_calendar_like() {
                if let ValueKind::Number(n) = &right.value {
                    return match number_arithmetic(l_val, op, n) {
                        Ok(rational) => {
                            OperationResult::from_literal(LiteralValue::measure(rational))
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    };
                }
                if let ValueKind::Ratio(r) = &right.value {
                    return match number_ratio_arithmetic(l_val, op, r) {
                        Ok(rational) => {
                            OperationResult::from_literal(LiteralValue::measure(rational))
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    };
                }
            }
            if right_type.is_calendar_like() && !left_type.is_calendar_like() {
                if let (ValueKind::Number(n), ArithmeticComputation::Multiply) = (&left.value, op) {
                    return match number_arithmetic(n, op, r_val) {
                        Ok(rational) => {
                            OperationResult::from_literal(LiteralValue::measure(rational))
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    };
                }
                if let ValueKind::Number(n) = &left.value {
                    return match number_arithmetic(n, op, r_val) {
                        Ok(rational) => {
                            OperationResult::from_literal(LiteralValue::number(rational))
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    };
                }
                if let ValueKind::Ratio(r) = &left.value {
                    return match number_ratio_arithmetic(r_val, op, r) {
                        Ok(rational) => {
                            OperationResult::from_literal(LiteralValue::measure(rational))
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    };
                }
            }
            match op {
                ArithmeticComputation::Add | ArithmeticComputation::Subtract => {
                    let same_family = left_type.same_measure_family(right_type);
                    let anonymous_compatible =
                        left_type.compatible_with_anonymous_measure(right_type);
                    let identical_measure = left_type.as_ref() == right_type.as_ref()
                        || (left_type
                            .specifications
                            .equal_ignoring_unit(&right_type.specifications)
                            && left_type.name == right_type.name
                            && left_type.extends == right_type.extends);
                    if !identical_measure && !same_family && !anonymous_compatible {
                        unreachable!(
                        "BUG: measure add/subtract with incompatible types ({} vs {}); should be rejected during planning",
                        left_type.name(),
                        right_type.name()
                    );
                    }
                    match measure_add_subtract(l_val, op, r_val) {
                        Ok(rational) => {
                            let instance_factors = BoundValueKind::agree_instance_factors(
                                left.instance_factors.as_ref(),
                                right.instance_factors.as_ref(),
                            );
                            let unit = BoundValueKind::binding_with_agreed_factors(
                                BoundValueKind::agree_or_left_binding(
                                    left.unit.as_ref(),
                                    right.unit.as_ref(),
                                ),
                                &instance_factors,
                            );
                            OperationResult::from_bound(BoundValueKind {
                                value: ValueKind::Measure(rational),
                                unit,
                                instance_factors,
                            })
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    }
                }
                ArithmeticComputation::Multiply | ArithmeticComputation::Divide => {
                    if matches!(op, ArithmeticComputation::Divide)
                        && crate::computation::rational::rational_is_zero(r_val)
                    {
                        return OperationResult::Veto(VetoType::computation(
                            "Division by zero is not allowed.",
                        ));
                    }
                    let numeric_op = match op {
                        ArithmeticComputation::Multiply => NumericOperation::Multiply,
                        ArithmeticComputation::Divide => NumericOperation::Divide,
                        _ => unreachable!("BUG: matched multiply/divide arm with other op"),
                    };
                    let raw_result = match rational_operation(l_val, numeric_op, r_val) {
                        Ok(p) => p,
                        Err(failure) => {
                            return OperationResult::Veto(VetoType::computation(
                                map_numeric_failure(failure).message(),
                            ))
                        }
                    };
                    let l_decomp = left_type
                        .measure_type_decomposition()
                        .expect("BUG: decomposition must be resolved after planning");
                    let r_decomp = right_type
                        .measure_type_decomposition()
                        .expect("BUG: decomposition must be resolved after planning");
                    let combined_decomposition =
                        crate::planning::semantics::combine_decompositions(
                            l_decomp,
                            r_decomp,
                            matches!(op, ArithmeticComputation::Multiply),
                        )
                        .expect("BUG: planning bounds combined unit exponents");
                    if combined_decomposition.is_empty() {
                        OperationResult::from_literal(LiteralValue::number(raw_result))
                    } else if left_type.same_measure_family(right_type) {
                        OperationResult::from_bound(BoundValueKind {
                            value: ValueKind::Measure(raw_result),
                            unit: None,
                            instance_factors: BoundValueKind::agree_instance_factors(
                                left.instance_factors.as_ref(),
                                right.instance_factors.as_ref(),
                            ),
                        })
                    } else {
                        OperationResult::from_bound(BoundValueKind::unbound(ValueKind::Measure(
                            raw_result,
                        )))
                    }
                }
                _ => unreachable!("BUG: measure {:?} measure is rejected during planning", op),
            }
        }
        // Measure op Ratio → Measure (multiply/divide; add/subtract rejected at planning)
        (ValueKind::Measure(q_val), ValueKind::Ratio(r)) => {
            match measure_ratio_arithmetic(q_val.clone(), op, r.clone()) {
                Ok(rational) => OperationResult::from_bound(BoundValueKind {
                    value: ValueKind::Measure(rational),
                    unit: left.unit.clone(),
                    instance_factors: left.instance_factors.clone(),
                }),
                Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
            }
        }
        // Ratio op Measure → Measure only for multiply (commutative); others rejected at planning
        (ValueKind::Ratio(r), ValueKind::Measure(q_val)) => match op {
            ArithmeticComputation::Multiply => {
                match measure_ratio_arithmetic(q_val.clone(), op, r.clone()) {
                    Ok(rational) => OperationResult::from_bound(BoundValueKind {
                        value: ValueKind::Measure(rational),
                        unit: right.unit.clone(),
                        instance_factors: right.instance_factors.clone(),
                    }),
                    Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
                }
            }
            _ => unreachable!(
                "BUG: ratio {:?} measure; planning should have rejected this",
                op
            ),
        },

        // Measure op Number. Multiply and divide keep the operand unit. Power scales
        // the composition, so the magnitude is unbound and the stamped type names the unit.
        // Exponent 0 is the number 1. Modulo of a measure is a planning error.
        (ValueKind::Measure(measure_val), ValueKind::Number(n)) => match op {
            ArithmeticComputation::Multiply
            | ArithmeticComputation::Divide
            | ArithmeticComputation::Add
            | ArithmeticComputation::Subtract => match number_arithmetic(measure_val, op, n) {
                Ok(rational) => OperationResult::from_bound(BoundValueKind {
                    value: ValueKind::Measure(rational),
                    unit: left.unit.clone(),
                    instance_factors: left.instance_factors.clone(),
                }),
                Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
            },
            ArithmeticComputation::Power => {
                if !n.is_integer() {
                    unreachable!(
                        "BUG: measure power with a non-integer exponent is rejected during planning"
                    );
                }
                match number_arithmetic(measure_val, op, n) {
                    Ok(rational) if n.numer_is_zero() => {
                        OperationResult::from_literal(LiteralValue::number(rational))
                    }
                    Ok(rational) => OperationResult::from_bound(BoundValueKind {
                        value: ValueKind::Measure(rational),
                        unit: None,
                        instance_factors: left.instance_factors.clone(),
                    }),
                    Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
                }
            }
            ArithmeticComputation::Modulo => {
                unreachable!("BUG: measure modulo number is rejected during planning")
            }
        },
        // Number op Measure → Measure for multiply; for divide, keep inverse dimensions
        // as an unbound measure until a later cancel or signature hit.
        (ValueKind::Number(n), ValueKind::Measure(measure_val)) => match op {
            ArithmeticComputation::Multiply => match number_arithmetic(n, op, measure_val) {
                Ok(rational) => OperationResult::from_bound(BoundValueKind {
                    value: ValueKind::Measure(rational),
                    unit: right.unit.clone(),
                    instance_factors: right.instance_factors.clone(),
                }),
                Err(failure) => OperationResult::Veto(VetoType::computation(failure.message())),
            },
            ArithmeticComputation::Divide => {
                let measure_decomp = right_type
                    .measure_type_decomposition()
                    .expect("BUG: decomposition must be resolved after planning");
                if measure_decomp.is_empty() {
                    match number_arithmetic(n, op, measure_val) {
                        Ok(rational) => {
                            OperationResult::from_literal(LiteralValue::number(rational))
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    }
                } else {
                    let negated_signature = crate::planning::semantics::negate_signature(
                        &right_type.measure_runtime_signature(),
                    );
                    match number_arithmetic(n, op, measure_val) {
                        Ok(rational) => {
                            if let Some((unit_name, owning_type)) =
                                find_by_names(signature_index, &negated_signature)
                            {
                                let target_factor =
                                    owning_type.measure_unit_factor(unit_name).clone();
                                match crate::computation::rational::checked_div(
                                    &rational,
                                    &target_factor,
                                ) {
                                    Ok(magnitude) => OperationResult::from_bound(
                                        BoundValueKind::unbound(ValueKind::Measure(magnitude)),
                                    ),
                                    Err(failure) => OperationResult::Veto(VetoType::computation(
                                        failure.to_string(),
                                    )),
                                }
                            } else {
                                OperationResult::from_bound(BoundValueKind::unbound(
                                    ValueKind::Measure(rational),
                                ))
                            }
                        }
                        Err(failure) => {
                            OperationResult::Veto(VetoType::computation(failure.message()))
                        }
                    }
                }
            }
            ArithmeticComputation::Modulo
            | ArithmeticComputation::Add
            | ArithmeticComputation::Subtract
            | ArithmeticComputation::Power => {
                unreachable!(
                    "BUG: Number {:?} Measure should be rejected during planning",
                    op
                )
            }
        },
        _ => unreachable!(
            "BUG: arithmetic {:?} for {:?} and {:?}; planning should have rejected this",
            op,
            type_name(left_type),
            type_name(right_type)
        ),
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum NumberArithmeticFailure {
    DivisionByZero,
    ModuloByZero,
    Computation(String),
}

impl NumberArithmeticFailure {
    pub fn message(self) -> String {
        match self {
            Self::DivisionByZero => "Division by zero is not allowed.".to_string(),
            Self::ModuloByZero => "Modulo by zero is not allowed.".to_string(),
            Self::Computation(message) => message,
        }
    }
}

fn numeric_operation_from_arithmetic(operator: &ArithmeticComputation) -> NumericOperation {
    match operator {
        ArithmeticComputation::Add => NumericOperation::Add,
        ArithmeticComputation::Subtract => NumericOperation::Subtract,
        ArithmeticComputation::Multiply => NumericOperation::Multiply,
        ArithmeticComputation::Divide => NumericOperation::Divide,
        ArithmeticComputation::Modulo => NumericOperation::Modulo,
        ArithmeticComputation::Power => NumericOperation::Power,
    }
}

fn map_numeric_failure(failure: NumericFailure) -> NumberArithmeticFailure {
    match failure {
        NumericFailure::DivisionByZero => NumberArithmeticFailure::DivisionByZero,
        other => NumberArithmeticFailure::Computation(other.to_string()),
    }
}

fn map_numeric_failure_modulo(failure: NumericFailure) -> NumberArithmeticFailure {
    match failure {
        NumericFailure::DivisionByZero => NumberArithmeticFailure::ModuloByZero,
        other => map_numeric_failure(other),
    }
}

fn measure_scale_magnitude_by_rational(
    magnitude: RationalInteger,
    factor: &RationalInteger,
) -> Result<RationalInteger, NumberArithmeticFailure> {
    rational_operation(&magnitude, NumericOperation::Multiply, factor).map_err(map_numeric_failure)
}

fn measure_ratio_arithmetic(
    measure_value: RationalInteger,
    operator: &ArithmeticComputation,
    ratio_value: RationalInteger,
) -> Result<RationalInteger, NumberArithmeticFailure> {
    match operator {
        ArithmeticComputation::Multiply => {
            measure_scale_magnitude_by_rational(measure_value, &ratio_value)
        }
        ArithmeticComputation::Divide => {
            rational_operation(&measure_value, NumericOperation::Divide, &ratio_value)
                .map_err(map_numeric_failure)
        }
        _ => unreachable!(
            "BUG: measure {:?} ratio is rejected during planning",
            operator
        ),
    }
}

fn measure_add_subtract(
    left_value: &RationalInteger,
    operator: &ArithmeticComputation,
    right_value: &RationalInteger,
) -> Result<RationalInteger, NumberArithmeticFailure> {
    rational_operation(
        left_value,
        numeric_operation_from_arithmetic(operator),
        right_value,
    )
    .map_err(map_numeric_failure)
}

pub fn number_arithmetic(
    left: &RationalInteger,
    operator: &ArithmeticComputation,
    right: &RationalInteger,
) -> Result<RationalInteger, NumberArithmeticFailure> {
    rational_operation_with_fallback(left, numeric_operation_from_arithmetic(operator), right)
        .map_err(|failure| {
            if matches!(operator, ArithmeticComputation::Modulo) {
                map_numeric_failure_modulo(failure)
            } else {
                map_numeric_failure(failure)
            }
        })
}

fn operate_on_operation_results(
    left_result: OperationResult,
    left_type: &Arc<LemmaType>,
    op: &ArithmeticComputation,
    right_result: OperationResult,
    right_type: &Arc<LemmaType>,
    signature_index: &SignatureIndex,
) -> OperationResult {
    let left_value = match left_result {
        OperationResult::Value(value) => value,
        OperationResult::Veto(reason) => return OperationResult::Veto(reason),
    };
    let right_value = match right_result {
        OperationResult::Value(value) => value,
        OperationResult::Veto(reason) => return OperationResult::Veto(reason),
    };
    scalar_arithmetic(
        &left_value,
        left_type,
        op,
        &right_value,
        right_type,
        signature_index,
    )
}

/// Divide / modulo with OperationResult operands: validate the divisor first so a
/// present definitive Computation factor settles intake even when the dividend is
/// still MissingData (keys that cannot un-veto leave `missing_data`).
pub(crate) fn divisive_operation_results(
    left: &OperationResult,
    left_type: &Arc<LemmaType>,
    op: &ArithmeticComputation,
    right: &OperationResult,
    right_type: &Arc<LemmaType>,
    signature_index: &SignatureIndex,
) -> OperationResult {
    assert!(
        matches!(
            op,
            ArithmeticComputation::Divide | ArithmeticComputation::Modulo
        ),
        "BUG: divisive_operation_results only for Divide/Modulo, got {op:?}"
    );
    let right_value = match right {
        OperationResult::Value(value) => value,
        OperationResult::Veto(_) => return right.clone(),
    };
    if let Some(veto) = computation_if_zero_divisor(&right_value.value, op) {
        return veto;
    }
    match left {
        OperationResult::Value(left_value) => scalar_arithmetic(
            left_value,
            left_type,
            op,
            right_value,
            right_type,
            signature_index,
        ),
        OperationResult::Veto(_) => left.clone(),
    }
}

fn computation_if_zero_divisor(
    right: &ValueKind,
    op: &ArithmeticComputation,
) -> Option<OperationResult> {
    let magnitude = match right {
        ValueKind::Number(n) | ValueKind::Measure(n) | ValueKind::Ratio(n) => n,
        _ => return None,
    };
    if !crate::computation::rational::rational_is_zero(magnitude) {
        return None;
    }
    let failure = match op {
        ArithmeticComputation::Divide => NumberArithmeticFailure::DivisionByZero,
        ArithmeticComputation::Modulo => NumberArithmeticFailure::ModuloByZero,
        _ => return None,
    };
    Some(OperationResult::Veto(VetoType::computation(
        failure.message(),
    )))
}

fn operate_with_left_result(
    left_result: OperationResult,
    left_type: &Arc<LemmaType>,
    op: &ArithmeticComputation,
    right: &BoundValueKind,
    right_type: &Arc<LemmaType>,
    signature_index: &SignatureIndex,
) -> OperationResult {
    let left_value = match left_result {
        OperationResult::Value(value) => value,
        OperationResult::Veto(reason) => return OperationResult::Veto(reason),
    };
    scalar_arithmetic(
        &left_value,
        left_type,
        op,
        right,
        right_type,
        signature_index,
    )
}

fn operate_with_right_result(
    left: &BoundValueKind,
    left_type: &Arc<LemmaType>,
    op: &ArithmeticComputation,
    right_result: OperationResult,
    right_type: &Arc<LemmaType>,
    signature_index: &SignatureIndex,
) -> OperationResult {
    let right_value = match right_result {
        OperationResult::Value(value) => value,
        OperationResult::Veto(reason) => return OperationResult::Veto(reason),
    };
    scalar_arithmetic(
        left,
        left_type,
        op,
        &right_value,
        right_type,
        signature_index,
    )
}

fn shift_date_range_right_endpoint(
    range_left: &TypedLiteral,
    range_right: &TypedLiteral,
    calendar_value: &RationalInteger,
    add: bool,
    calendar_lemma_type: Arc<LemmaType>,
) -> OperationResult {
    let (ValueKind::Date(_), ValueKind::Date(_)) = (&range_left.value, &range_right.value) else {
        unreachable!(
            "BUG: date range calendar arithmetic received non-date endpoints; planning should have rejected this"
        );
    };

    let date_type = crate::planning::semantics::primitive_date_arc();
    let calendar_literal = LiteralValue::measure(calendar_value.clone());
    let op = if add {
        ArithmeticComputation::Add
    } else {
        ArithmeticComputation::Subtract
    };
    let shifted_right = match super::datetime::datetime_arithmetic(
        &range_right.to_literal(),
        date_type,
        &op,
        &calendar_literal,
        &calendar_lemma_type,
    ) {
        OperationResult::Value(value) => value.to_literal(),
        OperationResult::Veto(reason) => return OperationResult::Veto(reason),
    };

    OperationResult::from_literal(LiteralValue::range(
        range_left.clone(),
        TypedLiteral {
            value: shifted_right.value,
            lemma_type: Arc::clone(&range_right.lemma_type),
        },
    ))
}

fn shift_calendar_range_right_endpoint(
    range_left: &TypedLiteral,
    range_right: &TypedLiteral,
    calendar_value: &RationalInteger,
    add: bool,
    indexes: &CalendarRangeShiftIndexes<'_>,
) -> OperationResult {
    let (ValueKind::Measure(_), ValueKind::Measure(_)) = (&range_left.value, &range_right.value)
    else {
        unreachable!(
            "BUG: calendar range calendar arithmetic received non-calendar endpoints; planning should have rejected this"
        );
    };
    let calendar_bound = BoundValueKind::unbound(ValueKind::Measure(calendar_value.clone()));
    let range_right_bound = BoundValueKind::unbound(range_right.value.clone());
    let op = if add {
        ArithmeticComputation::Add
    } else {
        ArithmeticComputation::Subtract
    };
    let shifted_right = match scalar_arithmetic(
        &range_right_bound,
        indexes.endpoint_type,
        &op,
        &calendar_bound,
        indexes.calendar_type,
        indexes.signature_index,
    ) {
        OperationResult::Value(value) => value.to_literal(),
        OperationResult::Veto(reason) => return OperationResult::Veto(reason),
    };

    OperationResult::from_literal(LiteralValue::range(
        range_left.clone(),
        TypedLiteral {
            value: shifted_right.value,
            lemma_type: Arc::clone(&range_right.lemma_type),
        },
    ))
}

fn type_name(lemma_type: &LemmaType) -> String {
    lemma_type.name().to_string()
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::computation::rational::rational_new;
    use crate::planning::semantics::{ArithmeticComputation, LiteralValue, ValueKind};
    use rust_decimal::Decimal;

    #[test]
    fn number_arithmetic_add_on_stored_decimals() {
        let left = rational_new(1, 1);
        let right = rational_new(2, 1);
        let sum = number_arithmetic(&left, &ArithmeticComputation::Add, &right).unwrap();
        assert_eq!(sum, rational_new(3, 1));
    }

    #[test]
    fn number_arithmetic_divide_ten_by_three_returns_value_decimal() {
        let left = rational_new(10, 1);
        let right = rational_new(3, 1);
        let quotient = number_arithmetic(&left, &ArithmeticComputation::Divide, &right).unwrap();
        let decimal = quotient.try_to_decimal().unwrap();
        assert!(decimal > Decimal::from(3));
        assert!(decimal < Decimal::from(4));
    }

    #[test]
    fn number_arithmetic_division_by_zero_returns_failure() {
        let left = rational_new(10, 1);
        let right = rational_new(0, 1);
        let failure = number_arithmetic(&left, &ArithmeticComputation::Divide, &right).unwrap_err();
        assert_eq!(failure, NumberArithmeticFailure::DivisionByZero);
    }

    #[test]
    fn arithmetic_operation_adds_primitive_numbers() {
        use crate::computation::rational::decimal_to_rational;
        use crate::planning::semantics::primitive_number_arc;
        use rust_decimal::Decimal;
        let left = BoundValueKind::unbound(
            LiteralValue::number(decimal_to_rational(Decimal::new(11, 1)).unwrap()).value,
        );
        let right = BoundValueKind::unbound(
            LiteralValue::number(decimal_to_rational(Decimal::new(9, 1)).unwrap()).value,
        );
        let number_ty = primitive_number_arc();
        let signature_index = SignatureIndex::new();
        let OperationResult::Value(lit) = arithmetic_operation(
            &left,
            number_ty,
            &ArithmeticComputation::Add,
            &right,
            number_ty,
            &signature_index,
        ) else {
            panic!("expected value");
        };
        match &lit.value {
            ValueKind::Number(n) => {
                assert_eq!(n, &decimal_to_rational(Decimal::new(2, 0)).unwrap());
            }
            other => panic!("expected number, got {other:?}"),
        }
    }

    #[test]
    fn arithmetic_operation_propagates_veto_from_left() {
        use crate::planning::semantics::primitive_number_arc;
        let left = OperationResult::Veto(VetoType::computation("left failed"));
        let right = LiteralValue::number(rational_new(1, 1));
        let number_ty = primitive_number_arc();
        let signature_index = SignatureIndex::new();
        let result = operate_on_operation_results(
            left,
            number_ty,
            &ArithmeticComputation::Add,
            OperationResult::from_literal(right),
            number_ty,
            &signature_index,
        );
        assert!(matches!(result, OperationResult::Veto(_)));
    }

    // ---------------------------------------------------------------------------
    // Phase 0 — Q*Q signature behaviour for the rewritten arithmetic arm.
    //
    // These tests use ValueKind::Measure with the OLD (RationalInteger, String,
    // BaseMeasureVector) shape today. After rewrite_measure_value_kind_shape lands,
    // they will be updated to (RationalInteger, Vec<(String,i32)>). They will fail today
    // because the Q*Q arm uses canonical magnitudes (not direct multiply), and the result
    // emission paths differ from the rewrite spec.
    // ---------------------------------------------------------------------------

    fn build_engine_and_get_value(code: &str, spec: &str, rule: &str) -> (LiteralValue, String) {
        use crate::engine::Engine;
        use std::path::PathBuf;
        use std::sync::Arc;
        let mut engine = Engine::new();
        engine
            .load([(
                crate::parsing::source::SourceType::Path(Arc::new(PathBuf::from("t.lemma"))),
                code.to_string(),
            )])
            .expect("spec must load");
        let response = engine
            .evaluate(None, spec, None, IndexMap::new(), None, false)
            .expect("spec must evaluate");
        let rule_result = response
            .results
            .get(rule)
            .unwrap_or_else(|| panic!("rule '{}' missing", rule));
        if rule_result.vetoed {
            panic!("rule '{}' vetoed", rule);
        }
        (rule_result.to_literal(), rule_result.rule_type.clone())
    }

    /// Phase 0 — Q*Q producing a signature hit must emit a named lemma_type.
    /// Today the arithmetic arm uses canonical pre-conversion (not direct multiply),
    /// so the magnitude may differ. After the rewrite, the magnitude must equal the
    /// direct product of operand magnitudes.
    #[test]
    fn q_times_q_signature_hit_emits_named_lemma_type() {
        let code = r#"spec t
data money: measure
  -> unit eur: 1
data rate: measure
  -> unit eur_per_hour: eur/hour
data hour: measure
  -> unit hour: 1
data r: 30 eur_per_hour
data h: 2 hour
rule pay: r * h
"#;
        let (value, _) = build_engine_and_get_value(code, "t", "pay");
        // Result must be a Measure. The signature [(eur,1),(hour,-1),(hour,1)] -> [(eur,1)]
        // must hit signature_index and emit lemma_type = money.
        match &value.value {
            ValueKind::Measure(_) => {}
            other => panic!("expected Measure result, got {:?}", other),
        }
        // Type lives on the rule / NormalForm after Change 5, not on LiteralValue.
        assert!(
            matches!(&value.value, ValueKind::Measure(_)),
            "result must be a Measure promoted via signature hit"
        );
    }

    /// Phase 0 — Q*Q producing a signature miss must emit anonymous lemma_type.
    /// e.g., `eur_per_minute * hour` does not cancel; signature is
    /// [(eur,1),(hour,1),(minute,-1)] which has no signature_index entry.
    #[test]
    fn q_times_q_signature_miss_emits_anonymous_lemma_type() {
        let code = r#"spec t
data money: measure
  -> unit eur: 1
data rate: measure
  -> unit eur_per_minute: eur/minute
data hour: measure
  -> unit hour: 1
data r: 40 eur_per_minute
data h: 2 hour
rule weird: r * h
"#;
        // The full evaluation will be rejected today by the rule boundary check (anonymous
        // intermediate). After the rewrite, planning either accepts (no matching named type
        // -> rejected with precise message) or accepts when the signature combines to a known
        // type. For this test, the expectation is that the rule is rejected today.
        use crate::engine::Engine;
        use std::path::PathBuf;
        use std::sync::Arc;
        let mut engine = Engine::new();
        let result = engine.load([(
            crate::parsing::source::SourceType::Path(Arc::new(PathBuf::from("t.lemma"))),
            code.to_string(),
        )]);
        assert!(
            result.is_err(),
            "rule producing anonymous Q*Q with no signature_index match must be rejected"
        );
    }

    /// Phase 0 — Q + Q with identical signatures sums magnitudes directly.
    #[test]
    fn q_plus_q_same_signature() {
        let code = r#"spec t
data money: measure
  -> unit eur: 1
data a: 100 eur
data b: 50 eur
rule total: a + b
"#;
        let (value, _) = build_engine_and_get_value(code, "t", "total");
        match &value.value {
            ValueKind::Measure(n) => {
                let decimal = n.try_to_decimal().unwrap();
                assert_eq!(decimal, Decimal::from(150));
            }
            other => panic!("expected Measure, got {:?}", other),
        }
    }

    /// Phase 0 — Q + Q with different but dimensionally-compatible signatures converts
    /// via signature_factor before summing.
    /// 10 eur_per_second + 20 eur_per_minute = 10 + (20/60) eur_per_second
    #[test]
    fn q_plus_q_different_signature() {
        let code = r#"spec t
uses lemma units
data money: measure
  -> unit eur: 1
data rate: measure
  -> unit eur_per_second: eur/second
  -> unit eur_per_minute: eur/minute
data a: 10 eur_per_second
data b: 20 eur_per_minute
rule total_rate: (a + b) as eur_per_second
"#;
        let (value, _) = build_engine_and_get_value(code, "t", "total_rate");
        match &value.value {
            ValueKind::Measure(n) => {
                let decimal = n.try_to_decimal().unwrap();
                // 10 + 1/3 ≈ 10.333...
                let expected_low = Decimal::new(10_333, 3);
                let expected_high = Decimal::new(10_334, 3);
                assert!(
                    decimal >= expected_low && decimal <= expected_high,
                    "expected ~10.333, got {}",
                    decimal
                );
            }
            other => panic!("expected Measure, got {:?}", other),
        }
    }

    /// Phase 0 — `number / measure` must produce a Measure whose signature is the
    /// negation of the rhs signature, and lemma_type from signature_index lookup or
    /// anonymous marker.
    #[test]
    fn number_divided_by_q_reciprocates_signature() {
        let code = r#"spec t
data duration_t: measure
  -> unit second: 1
data freq: measure
  -> unit per_second: second^-1
data d: 2 second
rule f: 1 / d
"#;
        // 1 / second = 1 per_second; signature_index hit yields named 'freq' type.
        let (value, rule_type) = build_engine_and_get_value(code, "t", "f");
        match &value.value {
            ValueKind::Measure(_) => {}
            other => panic!("expected Measure, got {:?}", other),
        }
        assert_eq!(
            rule_type, "freq",
            "1/second must promote to 'freq' (signature [(second,-1)] -> per_second)"
        );
    }
}