lemma-engine 0.10.2

use std::sync::Arc;

use crate::computation::arithmetic::SignatureIndex;
use crate::computation::operation_result::{OperationResult, VetoType};
use crate::computation::rational::{rational_abs, rational_zero, RationalInteger};
use crate::planning::semantics::{
    primitive_time_arc, semantic_date_as_time, ArithmeticComputation, ComparisonComputation,
    LemmaType, LiteralValue, TypedLiteral, ValueKind,
};

pub fn compute_span(left: &TypedLiteral, right: &TypedLiteral) -> OperationResult {
    absolute_span(compute_signed_span(left, right))
}

/// Result type of a range span derived from the range's LemmaType.
pub fn span_result_type(range_type: &LemmaType) -> Arc<LemmaType> {
    if range_type.is_date_range() || range_type.is_time_range() {
        return Arc::new(LemmaType::anonymous_for_decomposition(
            crate::planning::semantics::duration_decomposition(),
        ));
    }
    range_type
        .specifications
        .element_from_range()
        .map(|element| Arc::new(LemmaType::primitive(element)))
        .unwrap_or_else(|| Arc::new(range_type.clone()))
}

fn compute_signed_span(left: &TypedLiteral, right: &TypedLiteral) -> OperationResult {
    let left_type = &left.lemma_type;
    let right_type = &right.lemma_type;
    match (&left.value, &right.value) {
        (ValueKind::Date(left_date), ValueKind::Date(right_date)) => {
            let left_chrono = match super::datetime::semantic_datetime_to_chrono(left_date) {
                Ok(d) => d,
                Err(msg) => return OperationResult::Veto(VetoType::computation(msg)),
            };
            let right_chrono = match super::datetime::semantic_datetime_to_chrono(right_date) {
                Ok(d) => d,
                Err(msg) => return OperationResult::Veto(VetoType::computation(msg)),
            };
            compute_elapsed_duration_span(left_chrono, right_chrono)
        }
        (ValueKind::Time(left_time), ValueKind::Time(right_time)) => {
            let left_chrono = match super::datetime::semantic_time_to_chrono_datetime(left_time) {
                Ok(d) => d,
                Err(msg) => return OperationResult::Veto(VetoType::computation(msg)),
            };
            let right_chrono = match super::datetime::semantic_time_to_chrono_datetime(right_time) {
                Ok(d) => d,
                Err(msg) => return OperationResult::Veto(VetoType::computation(msg)),
            };
            compute_elapsed_duration_span(left_chrono, right_chrono)
        }
        _ => {
            // Span computation only performs Subtract, which never resolves a signature_index
            // entry (the result type matches the operand family).
            let empty_signature_index = SignatureIndex::new();
            super::arithmetic::scalar_arithmetic(
                &crate::planning::semantics::BoundValueKind::unbound(right.value.clone()),
                right_type,
                &ArithmeticComputation::Subtract,
                &crate::planning::semantics::BoundValueKind::unbound(left.value.clone()),
                left_type,
                &empty_signature_index,
            )
        }
    }
}

fn absolute_span(span: OperationResult) -> OperationResult {
    let OperationResult::Value(bound) = span else {
        return span;
    };
    let literal = bound.to_literal();
    let magnitude = stored_magnitude(&literal);
    match magnitude.try_cmp(&rational_zero()) {
        Ok(std::cmp::Ordering::Less) => {}
        Ok(_) => return OperationResult::from_bound(bound),
        Err(e) => return OperationResult::Veto(VetoType::computation(e.to_string())),
    }
    let negated = match negate_stored_magnitude(&literal) {
        Ok(magnitude) => magnitude,
        Err(failure) => return OperationResult::Veto(VetoType::computation(failure.message())),
    };
    OperationResult::from_literal(rebuild_literal_with_magnitude(&literal, negated))
}

fn stored_magnitude(literal: &LiteralValue) -> RationalInteger {
    match &literal.value {
        ValueKind::Number(n) | ValueKind::Measure(n) | ValueKind::Ratio(n) => n.clone(),
        other => unreachable!(
            "BUG: range span must be number, measure, ratio, or calendar measure, got {other:?}"
        ),
    }
}

fn negate_stored_magnitude(
    literal: &LiteralValue,
) -> Result<RationalInteger, super::arithmetic::NumberArithmeticFailure> {
    let zero = rational_zero();
    let magnitude = stored_magnitude(literal);
    super::arithmetic::number_arithmetic(&zero, &ArithmeticComputation::Subtract, &magnitude)
}

fn rebuild_literal_with_magnitude(
    literal: &LiteralValue,
    magnitude: RationalInteger,
) -> LiteralValue {
    match &literal.value {
        ValueKind::Number(_) => LiteralValue::number(magnitude),
        ValueKind::Measure(_) => LiteralValue::measure(magnitude),
        ValueKind::Ratio(_) => LiteralValue::ratio(magnitude),
        other => unreachable!(
            "BUG: range span must be number, measure, ratio, or calendar measure, got {other:?}"
        ),
    }
}

fn compute_elapsed_duration_span(
    left_chrono: chrono::DateTime<chrono::FixedOffset>,
    right_chrono: chrono::DateTime<chrono::FixedOffset>,
) -> OperationResult {
    let duration = right_chrono - left_chrono;
    let second = match super::datetime::chrono_duration_to_rational_seconds(duration) {
        Ok(s) => s,
        Err(msg) => return OperationResult::Veto(VetoType::computation(msg)),
    };
    let second = match rational_abs(&second) {
        Ok(s) => s,
        Err(failure) => return OperationResult::Veto(VetoType::computation(failure.to_string())),
    };
    OperationResult::from_literal(LiteralValue::measure(second))
}

fn comparison_boolean_result(result: OperationResult, context: &str) -> Result<bool, VetoType> {
    match result {
        OperationResult::Value(literal) => match &literal.value {
            ValueKind::Boolean(value) => Ok(*value),
            other => {
                unreachable!("BUG: {context} expected boolean comparison result, got {other:?}")
            }
        },
        OperationResult::Veto(v) => Err(v),
    }
}

/// Smaller endpoint first. Written order is not normalized, so `10...5` orders as `(5, 10)`.
/// Equal endpoints come back swapped; the two values are equal.
pub fn ordered_endpoints<'a>(
    range_left: &'a ValueKind,
    range_right: &'a ValueKind,
    endpoint_type: &Arc<LemmaType>,
) -> Result<(&'a ValueKind, &'a ValueKind), VetoType> {
    match comparison_boolean_result(
        super::comparison_operation(
            range_left,
            endpoint_type,
            &ComparisonComputation::LessThan,
            range_right,
            endpoint_type,
        ),
        "range endpoint ordering",
    ) {
        Ok(true) => Ok((range_left, range_right)),
        Ok(false) => Ok((range_right, range_left)),
        Err(veto) => Err(veto),
    }
}

/// Half-open interval `[lo, hi)` where `lo` and `hi` are the ordered range endpoints.
/// Returns `OperationResult::from_literal(Boolean)` or propagates a Veto from inner comparisons.
///
/// `date in time range` projects the date's clock via [`semantic_date_as_time`] (same as `as time`).
pub fn check_containment(
    value: &ValueKind,
    value_type: &Arc<LemmaType>,
    range_left: &ValueKind,
    range_right: &ValueKind,
    endpoint_type: &Arc<LemmaType>,
) -> OperationResult {
    let (lo, hi) = match ordered_endpoints(range_left, range_right, endpoint_type) {
        Ok(pair) => pair,
        Err(veto) => return OperationResult::Veto(veto),
    };

    let projected_time;
    let (value, value_type) = match value {
        ValueKind::Date(date) if endpoint_type.is_time() => {
            projected_time = ValueKind::Time(semantic_date_as_time(date));
            (&projected_time, primitive_time_arc())
        }
        _ => (value, value_type),
    };

    let lower_ok = match comparison_boolean_result(
        super::comparison_operation(
            value,
            value_type,
            &ComparisonComputation::GreaterThanOrEqual,
            lo,
            endpoint_type,
        ),
        "range containment lower bound",
    ) {
        Ok(b) => b,
        Err(v) => return OperationResult::Veto(v),
    };
    let upper_ok = match comparison_boolean_result(
        super::comparison_operation(
            value,
            value_type,
            &ComparisonComputation::LessThan,
            hi,
            endpoint_type,
        ),
        "range containment upper bound",
    ) {
        Ok(b) => b,
        Err(v) => return OperationResult::Veto(v),
    };

    OperationResult::from_literal(LiteralValue::from_bool(lower_ok && upper_ok))
}

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

    #[test]
    fn compute_span_is_absolute_for_reversed_number_range() {
        let number_ty = primitive_number_arc().clone();
        let five = TypedLiteral {
            value: ValueKind::Number(rational_new(5, 1)),
            lemma_type: Arc::clone(&number_ty),
        };
        let three = TypedLiteral {
            value: ValueKind::Number(rational_new(3, 1)),
            lemma_type: Arc::clone(&number_ty),
        };
        let OperationResult::Value(span) = compute_span(&five, &three) else {
            panic!("expected span value");
        };
        match &span.value {
            ValueKind::Number(n) => assert_eq!(n, &rational_new(2, 1)),
            other => panic!("expected number span, got {other:?}"),
        }
    }

    fn assert_contained(value: &LiteralValue, left: &LiteralValue, right: &LiteralValue) -> bool {
        let number_ty = primitive_number_arc();
        match check_containment(
            &value.value,
            number_ty,
            &left.value,
            &right.value,
            number_ty,
        ) {
            OperationResult::Value(lit) => match &lit.value {
                ValueKind::Boolean(b) => *b,
                other => panic!("expected Boolean, got {other:?}"),
            },
            OperationResult::Veto(v) => panic!("unexpected veto: {v:?}"),
        }
    }

    #[test]
    fn check_containment_half_open_and_reversed_number_range() {
        let three = LiteralValue::number(rational_new(3, 1));
        let four = LiteralValue::number(rational_new(4, 1));
        let five = LiteralValue::number(rational_new(5, 1));
        let two = LiteralValue::number(rational_new(2, 1));

        assert!(assert_contained(&three, &three, &five));
        assert!(!assert_contained(&five, &three, &five));
        assert!(!assert_contained(&two, &three, &five));
        assert!(!assert_contained(&five, &five, &five));
        assert!(assert_contained(&four, &five, &three));
    }

    #[test]
    fn rebuild_literal_with_magnitude_preserves_measure_kind() {
        let original = LiteralValue::measure(rational_new(10, 1));
        let rebuilt = rebuild_literal_with_magnitude(&original, rational_new(99, 1));
        match &rebuilt.value {
            ValueKind::Measure(n) => assert_eq!(n, &rational_new(99, 1)),
            other => panic!("expected Measure, got {:?}", other),
        }
    }
}