lemma-engine 0.8.14

//! Iterative expression evaluation
//!
//! Evaluates expressions without recursion using a stack-based approach.
//! All runtime errors (division by zero, etc.) result in Veto instead of errors.

use super::conversion_explanation::build_conversion_steps;
use super::explanation::{ExplanationNode, ValueSource};
use super::operations::{ComputationKind, OperationKind, OperationResult, VetoType};
use crate::computation::{
    arithmetic_operation, comparison_operation, convert_unit, UnitResolutionContext,
};
use crate::planning::semantics::{
    negated_comparison, DataPath, Expression, ExpressionKind, LiteralValue,
    MathematicalComputation, SemanticConversionTarget, Source, ValueKind,
};
use crate::planning::ExecutableRule;
use std::collections::{HashMap, HashSet};
use std::sync::Arc;

/// Get an explanation node for an expression that was already evaluated.
/// Panics if the explanation node is missing — this indicates a bug in the evaluator,
/// since we always set an explanation node immediately after evaluating an expression.
fn get_explanation_node_required(
    context: &crate::evaluation::EvaluationContext,
    expr: &Expression,
    operand_name: &str,
) -> ExplanationNode {
    let loc = expr
        .source_location
        .as_ref()
        .expect("BUG: expression missing source in evaluation");
    context
        .get_explanation_node(expr)
        .cloned()
        .unwrap_or_else(|| {
            unreachable!(
                "BUG: {} was evaluated but has no explanation node ({}:{}:{})",
                operand_name, loc.source_type, loc.span.line, loc.span.col
            )
        })
}

fn expr_ptr(expr: &Expression) -> usize {
    expr as *const Expression as usize
}

/// Convert a value to `target`, record operations, and build a computation explanation node.
pub(crate) fn finish_unit_conversion(
    value: &LiteralValue,
    target: &SemanticConversionTarget,
    operand_explanation: ExplanationNode,
    data_ref: Option<&DataPath>,
    source_location: Option<Source>,
    context: &mut crate::evaluation::EvaluationContext,
) -> (OperationResult, ExplanationNode) {
    let conversion_result = convert_unit(
        value,
        target,
        UnitResolutionContext::WithIndex(&context.unit_index),
    );

    match &conversion_result {
        OperationResult::Value(converted) => {
            let converted = converted.as_ref();
            let kind = ComputationKind::UnitConversion {
                target: target.clone(),
            };
            let conversion_steps = build_conversion_steps(
                value,
                target,
                converted,
                data_ref,
                UnitResolutionContext::WithIndex(&context.unit_index),
            );
            assert!(
                !conversion_steps.is_empty(),
                "BUG: unit conversion succeeded but explanation steps are empty"
            );
            context.push_operation(OperationKind::Computation {
                kind: kind.clone(),
                inputs: vec![value.clone()],
                result: converted.clone(),
            });
            let explanation_node = ExplanationNode::Computation {
                kind,
                conversion_steps,
                original_expression: String::new(),
                expression: String::new(),
                result: converted.clone(),
                source_location: source_location.clone(),
                operands: vec![operand_explanation],
            };
            (conversion_result, explanation_node)
        }
        OperationResult::Veto(_) => (conversion_result, operand_explanation),
    }
}

fn data_ref_for_conversion_operand<'a>(
    value_expr: &'a Expression,
    operand_explanation: &'a ExplanationNode,
) -> Option<&'a DataPath> {
    if let ExpressionKind::DataPath(data_path) = &value_expr.kind {
        return Some(data_path);
    }
    match operand_explanation {
        ExplanationNode::Value {
            source: ValueSource::Data { data_ref },
            ..
        } => Some(data_ref),
        _ => None,
    }
}

/// Get the result of an operand expression that was already evaluated.
fn get_operand_result(
    results: &HashMap<usize, OperationResult>,
    expr: &Expression,
    operand_name: &str,
) -> OperationResult {
    let loc = expr
        .source_location
        .as_ref()
        .expect("BUG: expression missing source in evaluation");
    results.get(&expr_ptr(expr)).cloned().unwrap_or_else(|| {
        unreachable!(
            "BUG: {} operand was marked ready but result is missing ({}:{}:{})",
            operand_name, loc.source_type, loc.span.line, loc.span.col
        )
    })
}

/// Extract the value from an OperationResult that is known to not be Veto.
/// Called only after an explicit Veto check has already returned early.
/// Panics if the result has no value — this is unreachable after the Veto guard.
fn unwrap_value_after_veto_check<'a>(
    result: &'a OperationResult,
    operand_name: &str,
    source_location: &Option<crate::planning::semantics::Source>,
) -> &'a LiteralValue {
    result.value().unwrap_or_else(|| {
        let loc = source_location
            .as_ref()
            .expect("BUG: expression missing source in evaluation");
        unreachable!(
            "BUG: {} passed Veto check but has no value ({}:{}:{})",
            operand_name, loc.source_type, loc.span.line, loc.span.col
        )
    })
}

/// Propagate veto explanation from operand to current expression
fn propagate_veto_explanation(
    context: &mut crate::evaluation::EvaluationContext,
    current: &Expression,
    vetoed_operand: &Expression,
    veto_result: OperationResult,
    operand_name: &str,
) -> OperationResult {
    let node = get_explanation_node_required(context, vetoed_operand, operand_name);
    context.set_explanation_node(current, node);
    veto_result
}

/// Evaluate branch: original expression for explanation trace, normalized for authoritative result.
fn evaluate_branch_dual(
    branch: &crate::planning::execution_plan::Branch,
    context: &mut crate::evaluation::EvaluationContext,
    explanation_operand_name: &str,
) -> (OperationResult, ExplanationNode) {
    let authoritative = evaluate_expression(&branch.normalized_result, context);
    let _ = evaluate_expression(&branch.result, context);
    let explanation_node =
        get_explanation_node_required(context, &branch.result, explanation_operand_name);
    (authoritative, explanation_node)
}

/// Evaluate a rule to produce its final result and explanation.
/// After planning, evaluation is guaranteed to complete — this function never returns
/// a Error. It produces an OperationResult (Value or Veto) and an Explanation tree.
pub(crate) fn evaluate_rule(
    exec_rule: &ExecutableRule,
    context: &mut crate::evaluation::EvaluationContext,
) -> (OperationResult, crate::evaluation::explanation::Explanation) {
    use crate::evaluation::explanation::{Branch, NonMatchedBranch};

    // If rule has no unless clauses, just evaluate the default expression
    if exec_rule.branches.len() == 1 {
        return evaluate_rule_without_unless(exec_rule, context);
    }

    // Rule has unless clauses - collect all branch evaluations for Branches explanation node
    let mut non_matched_branches: Vec<NonMatchedBranch> = Vec::new();

    // Evaluate branches in reverse order (last matching wins)
    for branch_index in (1..exec_rule.branches.len()).rev() {
        let branch = &exec_rule.branches[branch_index];
        if let Some(condition) = branch
            .normalized_condition
            .as_ref()
            .or(branch.condition.as_ref())
        {
            let condition_result = evaluate_expression(condition, context);
            let condition_explanation =
                get_explanation_node_required(context, condition, "condition");

            let matched = match condition_result {
                OperationResult::Veto(ref reason) => {
                    // Condition vetoed - this becomes the result
                    let unless_clause_index = branch_index - 1;
                    context.push_operation(OperationKind::RuleBranchEvaluated {
                        index: Some(unless_clause_index),
                        matched: true,
                        result_value: Some(OperationResult::Veto(reason.clone())),
                    });

                    // Build Branches node with this as the matched branch
                    let matched_branch = Branch {
                        condition: Some(Box::new(condition_explanation)),
                        result: Box::new(ExplanationNode::Veto {
                            message: Some(reason.to_string()),
                            source_location: branch.result.source_location.clone(),
                        }),
                        clause_index: Some(unless_clause_index),
                        source_location: Some(branch.source.clone()),
                    };

                    let branches_node = ExplanationNode::Branches {
                        matched: Box::new(matched_branch),
                        non_matched: non_matched_branches,
                        source_location: Some(exec_rule.source.clone()),
                    };

                    let explanation = crate::evaluation::explanation::Explanation {
                        rule_path: exec_rule.path.clone(),
                        source: Some(exec_rule.source.clone()),
                        result: OperationResult::Veto(reason.clone()),
                        tree: Arc::new(branches_node),
                    };
                    return (OperationResult::Veto(reason.clone()), explanation);
                }
                OperationResult::Value(lit) => match &lit.value {
                    ValueKind::Boolean(b) => *b,
                    _ => {
                        let veto = OperationResult::Veto(VetoType::computation(
                            "Unless condition must evaluate to boolean",
                        ));
                        let explanation = crate::evaluation::explanation::Explanation {
                            rule_path: exec_rule.path.clone(),
                            source: Some(exec_rule.source.clone()),
                            result: veto.clone(),
                            tree: Arc::new(ExplanationNode::Veto {
                                message: Some(
                                    "Unless condition must evaluate to boolean".to_string(),
                                ),
                                source_location: Some(exec_rule.source.clone()),
                            }),
                        };
                        return (veto, explanation);
                    }
                },
            };

            let unless_clause_index = branch_index - 1;

            if matched {
                let (result, result_explanation) = evaluate_branch_dual(branch, context, "result");

                context.push_operation(OperationKind::RuleBranchEvaluated {
                    index: Some(unless_clause_index),
                    matched: true,
                    result_value: Some(result.clone()),
                });

                // Build Branches node with this as the matched branch
                let matched_branch = Branch {
                    condition: Some(Box::new(condition_explanation)),
                    result: Box::new(result_explanation),
                    clause_index: Some(unless_clause_index),
                    source_location: Some(branch.source.clone()),
                };

                let branches_node = ExplanationNode::Branches {
                    matched: Box::new(matched_branch),
                    non_matched: non_matched_branches,
                    source_location: Some(exec_rule.source.clone()),
                };

                let explanation = crate::evaluation::explanation::Explanation {
                    rule_path: exec_rule.path.clone(),
                    source: Some(exec_rule.source.clone()),
                    result: result.clone(),
                    tree: Arc::new(branches_node),
                };
                return (result, explanation);
            }
            // Branch didn't match - record it as non-matched.
            context.push_operation(OperationKind::RuleBranchEvaluated {
                index: Some(unless_clause_index),
                matched: false,
                result_value: None,
            });

            non_matched_branches.push(NonMatchedBranch {
                condition: Box::new(condition_explanation),
                result: None,
                clause_index: Some(unless_clause_index),
                source_location: Some(branch.source.clone()),
            });
        }
    }

    let default_branch = &exec_rule.branches[0];
    let (default_result, default_result_explanation) =
        evaluate_branch_dual(default_branch, context, "default result");

    context.push_operation(OperationKind::RuleBranchEvaluated {
        index: None,
        matched: true,
        result_value: Some(default_result.clone()),
    });

    // Default branch has no condition
    let matched_branch = Branch {
        condition: None,
        result: Box::new(default_result_explanation),
        clause_index: None,
        source_location: Some(default_branch.source.clone()),
    };

    let branches_node = ExplanationNode::Branches {
        matched: Box::new(matched_branch),
        non_matched: non_matched_branches,
        source_location: Some(exec_rule.source.clone()),
    };

    let explanation = crate::evaluation::explanation::Explanation {
        rule_path: exec_rule.path.clone(),
        source: Some(exec_rule.source.clone()),
        result: default_result.clone(),
        tree: Arc::new(branches_node),
    };

    (default_result, explanation)
}

/// Evaluate a rule that has no unless clauses (simple case)
fn evaluate_rule_without_unless(
    exec_rule: &ExecutableRule,
    context: &mut crate::evaluation::EvaluationContext,
) -> (OperationResult, crate::evaluation::explanation::Explanation) {
    let default_branch = &exec_rule.branches[0];
    let (default_result, root_explanation_node) =
        evaluate_branch_dual(default_branch, context, "default result");

    context.push_operation(OperationKind::RuleBranchEvaluated {
        index: None,
        matched: true,
        result_value: Some(default_result.clone()),
    });

    let explanation = crate::evaluation::explanation::Explanation {
        rule_path: exec_rule.path.clone(),
        source: Some(exec_rule.source.clone()),
        result: default_result.clone(),
        tree: Arc::new(root_explanation_node),
    };

    (default_result, explanation)
}

/// Evaluate an expression iteratively without recursion.
/// Uses a work list approach: collect all expressions first, then evaluate in dependency order.
/// After planning, expression evaluation is guaranteed to complete — this function never
/// returns a Error. It produces an OperationResult (Value or Veto).
/// Iterative post-order traversal: collects expression nodes children-before-parents.
/// Uses pointer identity for dedup (no Hash/Eq on Expression needed).
fn collect_postorder(root: &Expression) -> Vec<&Expression> {
    enum Visit<'a> {
        Enter(&'a Expression),
        Exit(&'a Expression),
    }

    let mut stack: Vec<Visit<'_>> = vec![Visit::Enter(root)];
    let mut seen: HashSet<usize> = HashSet::new();
    let mut nodes: Vec<&Expression> = Vec::new();

    while let Some(visit) = stack.pop() {
        match visit {
            Visit::Enter(e) => {
                if !seen.insert(expr_ptr(e)) {
                    continue;
                }
                stack.push(Visit::Exit(e));
                match &e.kind {
                    ExpressionKind::Arithmetic(left, _, right)
                    | ExpressionKind::Comparison(left, _, right)
                    | ExpressionKind::LogicalAnd(left, right)
                    | ExpressionKind::LogicalOr(left, right)
                    | ExpressionKind::RangeLiteral(left, right)
                    | ExpressionKind::RangeContainment(left, right) => {
                        stack.push(Visit::Enter(right));
                        stack.push(Visit::Enter(left));
                    }
                    ExpressionKind::LogicalNegation(operand, _)
                    | ExpressionKind::UnitConversion(operand, _)
                    | ExpressionKind::MathematicalComputation(_, operand)
                    | ExpressionKind::ResultIsVeto(operand)
                    | ExpressionKind::DateCalendar(_, _, operand)
                    | ExpressionKind::PastFutureRange(_, operand) => {
                        stack.push(Visit::Enter(operand));
                    }
                    ExpressionKind::DateRelative(_, date_expr) => {
                        stack.push(Visit::Enter(date_expr));
                    }
                    _ => {}
                }
            }
            Visit::Exit(e) => {
                nodes.push(e);
            }
        }
    }

    nodes
}

fn evaluate_expression(
    expr: &Expression,
    context: &mut crate::evaluation::EvaluationContext,
) -> OperationResult {
    let nodes = collect_postorder(expr);
    let mut results: HashMap<usize, OperationResult> = HashMap::with_capacity(nodes.len());

    for node in &nodes {
        let result = evaluate_single_expression(node, &results, context);
        results.insert(expr_ptr(node), result);
    }

    results.remove(&expr_ptr(expr)).unwrap_or_else(|| {
        let loc = expr
            .source_location
            .as_ref()
            .expect("BUG: expression missing source in evaluation");
        unreachable!(
            "BUG: expression was processed but has no result ({}:{}:{})",
            loc.source_type, loc.span.start, loc.span.end
        )
    })
}

/// Evaluate a single expression given its dependencies are already evaluated.
/// After planning, this function is guaranteed to complete — it produces an OperationResult
/// (Value or Veto) without ever returning a Error.
fn evaluate_single_expression(
    current: &Expression,
    results: &HashMap<usize, OperationResult>,
    context: &mut crate::evaluation::EvaluationContext,
) -> OperationResult {
    match &current.kind {
        ExpressionKind::Literal(lit) => {
            let value = lit.as_ref().clone();
            let explanation_node = ExplanationNode::Value {
                value: value.clone(),
                source: ValueSource::Literal,
                source_location: current.source_location.clone(),
            };
            context.set_explanation_node(current, explanation_node);
            OperationResult::Value(Box::new(value))
        }

        ExpressionKind::DataPath(data_path) => {
            // Data lookup: a data can legitimately be missing (schema-only declaration without a
            // provided value at runtime). Returning None → Veto("Missing data: ...") is
            // correct domain behavior.
            //
            // Rule-target references are not pre-populated in `data_values`; on
            // first read we lazily resolve them from the (already-evaluated,
            // by topological-sort guarantee) target rule's result. A target
            // rule veto propagates with the exact same reason — copying the
            // veto type without rewrapping in `MissingData`.
            let data_path_clone = data_path.clone();
            let mut value = context.get_data(data_path).cloned();
            if value.is_none() {
                if let Some(resolved) = context.lazy_rule_reference_resolve(data_path) {
                    match resolved {
                        Ok(v) => value = Some(v),
                        Err(veto) => {
                            let explanation_node = ExplanationNode::Veto {
                                message: Some(veto.to_string()),
                                source_location: current.source_location.clone(),
                            };
                            context.set_explanation_node(current, explanation_node);
                            return OperationResult::Veto(veto);
                        }
                    }
                } else if let Some(veto) = context.get_reference_veto(data_path) {
                    let veto = veto.clone();
                    let explanation_node = ExplanationNode::Veto {
                        message: Some(veto.to_string()),
                        source_location: current.source_location.clone(),
                    };
                    context.set_explanation_node(current, explanation_node);
                    return OperationResult::Veto(veto);
                }
            }
            match value {
                Some(v) => {
                    context.push_operation(OperationKind::DataUsed {
                        data_ref: data_path_clone.clone(),
                        value: v.clone(),
                    });
                    let explanation_node = ExplanationNode::Value {
                        value: v.clone(),
                        source: ValueSource::Data {
                            data_ref: data_path_clone,
                        },
                        source_location: current.source_location.clone(),
                    };
                    context.set_explanation_node(current, explanation_node);
                    OperationResult::Value(Box::new(v))
                }
                None => {
                    let reason = VetoType::MissingData {
                        data: data_path_clone.clone(),
                    };
                    let explanation_node = ExplanationNode::Veto {
                        message: Some(reason.to_string()),
                        source_location: current.source_location.clone(),
                    };
                    context.set_explanation_node(current, explanation_node);
                    OperationResult::Veto(reason)
                }
            }
        }

        ExpressionKind::RulePath(rule_path) => {
            // Rule lookup: rules are evaluated in topological order. If a referenced rule's
            // result is not in the map, planning guaranteed no cycles and topological sort
            // ensured the dependency was evaluated first. Missing result is a bug.
            let rule_path_clone = rule_path.clone();
            let loc = current
                .source_location
                .as_ref()
                .expect("BUG: expression missing source in evaluation");
            let r = context.rule_results.get(rule_path).cloned().unwrap_or_else(|| {
                unreachable!(
                    "BUG: Rule '{}' not found in results during topological-order evaluation ({}:{}:{})",
                    rule_path.rule, loc.source_type, loc.span.line, loc.span.col
                )
            });

            context.push_operation(OperationKind::RuleUsed {
                rule_path: rule_path_clone.clone(),
                result: r.clone(),
            });

            // Share expansion via Arc instead of cloning (avoids O(n²) for deep chains)
            let expansion = match context.get_rule_explanation(rule_path) {
                Some(existing_explanation) => Arc::clone(&existing_explanation.tree),
                None => Arc::new(ExplanationNode::Value {
                    value: match &r {
                        OperationResult::Value(v) => v.as_ref().clone(),
                        OperationResult::Veto(_) => LiteralValue::from_bool(false),
                    },
                    source: ValueSource::Computed,
                    source_location: current.source_location.clone(),
                }),
            };

            let explanation_node = ExplanationNode::RuleReference {
                rule_path: rule_path_clone,
                result: r.clone(),
                source_location: current.source_location.clone(),
                expansion,
            };
            context.set_explanation_node(current, explanation_node);
            r
        }

        ExpressionKind::Arithmetic(left, op, right) => {
            let left_result = get_operand_result(results, left, "left");
            let right_result = get_operand_result(results, right, "right");

            if let OperationResult::Veto(_) = left_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    left,
                    left_result,
                    "left operand",
                );
            }
            if let OperationResult::Veto(_) = right_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    right,
                    right_result,
                    "right operand",
                );
            }

            let left_val = unwrap_value_after_veto_check(
                &left_result,
                "left operand",
                &current.source_location,
            );
            let right_val = unwrap_value_after_veto_check(
                &right_result,
                "right operand",
                &current.source_location,
            );

            let result = arithmetic_operation(left_val, op, right_val);

            let left_explanation = get_explanation_node_required(context, left, "left operand");
            let right_explanation = get_explanation_node_required(context, right, "right operand");

            if let OperationResult::Value(ref val) = result {
                let original_expr = format!("{} {} {}", left_val, op, right_val);
                let substituted_expr = format!("{} {} {}", left_val, op, right_val);
                context.push_operation(OperationKind::Computation {
                    kind: ComputationKind::Arithmetic(op.clone()),
                    inputs: vec![left_val.clone(), right_val.clone()],
                    result: val.as_ref().clone(),
                });
                let explanation_node = ExplanationNode::Computation {
                    kind: ComputationKind::Arithmetic(op.clone()),
                    conversion_steps: vec![],
                    original_expression: original_expr,
                    expression: substituted_expr,
                    result: val.as_ref().clone(),
                    source_location: current.source_location.clone(),
                    operands: vec![left_explanation, right_explanation],
                };
                context.set_explanation_node(current, explanation_node);
            } else if let OperationResult::Veto(_) = result {
                context.set_explanation_node(current, left_explanation);
            }
            result
        }

        ExpressionKind::Comparison(left, op, right) => {
            let left_result = get_operand_result(results, left, "left");
            let right_result = get_operand_result(results, right, "right");

            if let OperationResult::Veto(_) = left_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    left,
                    left_result,
                    "left operand",
                );
            }
            if let OperationResult::Veto(_) = right_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    right,
                    right_result,
                    "right operand",
                );
            }

            let left_val = unwrap_value_after_veto_check(
                &left_result,
                "left operand",
                &current.source_location,
            );
            let right_val = unwrap_value_after_veto_check(
                &right_result,
                "right operand",
                &current.source_location,
            );

            let result = comparison_operation(
                left_val,
                op,
                right_val,
                UnitResolutionContext::WithIndex(&context.unit_index),
            );

            let left_explanation = get_explanation_node_required(context, left, "left operand");
            let right_explanation = get_explanation_node_required(context, right, "right operand");

            if let OperationResult::Value(ref val) = result {
                let is_false = matches!(val.as_ref().value, ValueKind::Boolean(false));
                let (display_op, original_expr, substituted_expr, display_result) = if is_false {
                    let negated_op = negated_comparison(op.clone());
                    let orig = format!("{} {} {}", left_val, negated_op, right_val);
                    let sub = format!("{} {} {}", left_val, negated_op, right_val);
                    (negated_op, orig, sub, LiteralValue::from_bool(true))
                } else {
                    let original_expr = format!("{} {} {}", left_val, op, right_val);
                    let substituted_expr = format!("{} {} {}", left_val, op, right_val);
                    (
                        op.clone(),
                        original_expr,
                        substituted_expr,
                        val.as_ref().clone(),
                    )
                };
                context.push_operation(OperationKind::Computation {
                    kind: ComputationKind::Comparison(op.clone()),
                    inputs: vec![left_val.clone(), right_val.clone()],
                    result: val.as_ref().clone(),
                });
                let explanation_node = ExplanationNode::Computation {
                    kind: ComputationKind::Comparison(display_op),
                    conversion_steps: vec![],
                    original_expression: original_expr,
                    expression: substituted_expr,
                    result: display_result,
                    source_location: current.source_location.clone(),
                    operands: vec![left_explanation, right_explanation],
                };
                context.set_explanation_node(current, explanation_node);
            } else if let OperationResult::Veto(_) = result {
                context.set_explanation_node(current, left_explanation);
            }
            result
        }

        ExpressionKind::LogicalAnd(left, right) => {
            let left_result = get_operand_result(results, left, "left");
            if let OperationResult::Veto(_) = left_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    left,
                    left_result,
                    "left operand",
                );
            }

            let left_val = unwrap_value_after_veto_check(
                &left_result,
                "left operand",
                &current.source_location,
            );
            let left_bool = match &left_val.value {
                ValueKind::Boolean(b) => b,
                _ => unreachable!(
                    "BUG: logical AND with non-boolean operand; planning should have rejected this"
                ),
            };

            if !*left_bool {
                let left_explanation = get_explanation_node_required(context, left, "left operand");
                context.set_explanation_node(current, left_explanation);
                OperationResult::Value(Box::new(LiteralValue::from_bool(false)))
            } else {
                let right_result = get_operand_result(results, right, "right");
                let right_explanation =
                    get_explanation_node_required(context, right, "right operand");
                context.set_explanation_node(current, right_explanation);
                right_result
            }
        }

        ExpressionKind::LogicalOr(left, right) => {
            let left_result = get_operand_result(results, left, "left");
            if matches!(&left_result, OperationResult::Veto(_)) {
                let right_result = get_operand_result(results, right, "right");
                let right_explanation =
                    get_explanation_node_required(context, right, "right operand");
                context.set_explanation_node(current, right_explanation);
                return right_result;
            }

            let left_val = unwrap_value_after_veto_check(
                &left_result,
                "left operand",
                &current.source_location,
            );
            if matches!(&left_val.value, ValueKind::Boolean(false)) {
                let right_result = get_operand_result(results, right, "right");
                let right_explanation =
                    get_explanation_node_required(context, right, "right operand");
                context.set_explanation_node(current, right_explanation);
                return right_result;
            }

            let left_explanation = get_explanation_node_required(context, left, "left operand");
            context.set_explanation_node(current, left_explanation);
            left_result
        }

        ExpressionKind::LogicalNegation(operand, _) => {
            let result = get_operand_result(results, operand, "operand");
            if let OperationResult::Veto(_) = result {
                return propagate_veto_explanation(context, current, operand, result, "operand");
            }

            let value = unwrap_value_after_veto_check(&result, "operand", &current.source_location);
            let operand_explanation = get_explanation_node_required(context, operand, "operand");
            match &value.value {
                ValueKind::Boolean(b) => {
                    let result_bool = !*b;
                    context.set_explanation_node(current, operand_explanation);
                    OperationResult::Value(Box::new(LiteralValue::from_bool(result_bool)))
                }
                _ => unreachable!(
                    "BUG: logical NOT with non-boolean operand; planning should have rejected this"
                ),
            }
        }

        ExpressionKind::UnitConversion(value_expr, target) => {
            let result = get_operand_result(results, value_expr, "operand");
            if let OperationResult::Veto(_) = result {
                return propagate_veto_explanation(context, current, value_expr, result, "operand");
            }

            let value = unwrap_value_after_veto_check(&result, "operand", &current.source_location);
            let operand_explanation = get_explanation_node_required(context, value_expr, "operand");
            let data_ref = data_ref_for_conversion_operand(value_expr, &operand_explanation);
            let (conversion_result, explanation_node) = finish_unit_conversion(
                value,
                target,
                operand_explanation.clone(),
                data_ref,
                current.source_location.clone(),
                context,
            );
            context.set_explanation_node(current, explanation_node);
            conversion_result
        }

        ExpressionKind::MathematicalComputation(op, operand) => {
            let result = get_operand_result(results, operand, "operand");
            if let OperationResult::Veto(_) = result {
                return propagate_veto_explanation(context, current, operand, result, "operand");
            }

            let value = unwrap_value_after_veto_check(&result, "operand", &current.source_location);
            let operand_explanation = get_explanation_node_required(context, operand, "operand");
            let math_result = evaluate_mathematical_operator(op, value, context);
            context.set_explanation_node(current, operand_explanation);
            math_result
        }

        ExpressionKind::ResultIsVeto(operand) => {
            let operand_result = get_operand_result(results, operand, "operand");
            let is_vetoed = operand_result.vetoed();
            let result = OperationResult::Value(Box::new(LiteralValue::from_bool(is_vetoed)));

            let operand_explanation = get_explanation_node_required(context, operand, "operand");
            let operand_display = match &operand_result {
                OperationResult::Value(value) => value.to_string(),
                OperationResult::Veto(veto) => veto.to_string(),
            };
            let (original_expression, expression, display_result) = if is_vetoed {
                (
                    format!("{operand_display} is veto"),
                    format!("{operand_display} is veto"),
                    LiteralValue::from_bool(true),
                )
            } else {
                (
                    format!("{operand_display} is veto"),
                    format!("{operand_display} is not veto"),
                    LiteralValue::from_bool(true),
                )
            };
            let computation_result = result
                .value()
                .expect("BUG: ResultIsVeto always produces Value")
                .clone();
            context.push_operation(OperationKind::Computation {
                kind: ComputationKind::ResultIsVeto,
                inputs: vec![],
                result: computation_result,
            });
            let explanation_node = ExplanationNode::Computation {
                kind: ComputationKind::ResultIsVeto,
                conversion_steps: vec![],
                original_expression,
                expression,
                result: display_result,
                source_location: current.source_location.clone(),
                operands: vec![operand_explanation],
            };
            context.set_explanation_node(current, explanation_node);
            result
        }

        ExpressionKind::Veto(veto_expr) => {
            let explanation_node = ExplanationNode::Veto {
                message: veto_expr.message.clone(),
                source_location: current.source_location.clone(),
            };
            context.set_explanation_node(current, explanation_node);
            OperationResult::Veto(VetoType::UserDefined {
                message: veto_expr.message.clone(),
            })
        }

        ExpressionKind::Now => {
            let value = context.now().clone();
            let explanation_node = ExplanationNode::Value {
                value: value.clone(),
                source: ValueSource::Computed,
                source_location: current.source_location.clone(),
            };
            context.set_explanation_node(current, explanation_node);
            OperationResult::Value(Box::new(value))
        }

        ExpressionKind::DateRelative(kind, date_expr) => {
            let date_result = get_operand_result(results, date_expr, "date operand");
            if let OperationResult::Veto(_) = date_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    date_expr,
                    date_result,
                    "date operand",
                );
            }

            let date_val = unwrap_value_after_veto_check(
                &date_result,
                "date operand",
                &current.source_location,
            );

            let date_semantic = match &date_val.value {
                ValueKind::Date(dt) => dt,
                _ => unreachable!(
                    "BUG: date sugar with non-date operand; planning should have rejected this"
                ),
            };

            let now_val = context.now();
            let now_semantic = match &now_val.value {
                ValueKind::Date(dt) => dt,
                _ => unreachable!("BUG: context.now() must be a Date value"),
            };

            let result = crate::computation::datetime::compute_date_relative(
                kind,
                date_semantic,
                now_semantic,
            );

            let date_explanation =
                get_explanation_node_required(context, date_expr, "date operand");
            context.set_explanation_node(current, date_explanation);
            result
        }

        ExpressionKind::DateCalendar(kind, unit, date_expr) => {
            let date_result = get_operand_result(results, date_expr, "date operand");
            if let OperationResult::Veto(_) = date_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    date_expr,
                    date_result,
                    "date operand",
                );
            }

            let date_val = unwrap_value_after_veto_check(
                &date_result,
                "date operand",
                &current.source_location,
            );

            let date_semantic = match &date_val.value {
                ValueKind::Date(dt) => dt,
                _ => unreachable!(
                    "BUG: calendar sugar with non-date operand; planning should have rejected this"
                ),
            };

            let now_val = context.now();
            let now_semantic = match &now_val.value {
                ValueKind::Date(dt) => dt,
                _ => unreachable!("BUG: context.now() must be a Date value"),
            };

            let result = crate::computation::datetime::compute_date_calendar(
                kind,
                unit,
                date_semantic,
                now_semantic,
            );

            let date_explanation =
                get_explanation_node_required(context, date_expr, "date operand");
            context.set_explanation_node(current, date_explanation);
            result
        }

        ExpressionKind::RangeLiteral(left, right) => {
            let left_result = get_operand_result(results, left, "left endpoint");
            let right_result = get_operand_result(results, right, "right endpoint");

            if let OperationResult::Veto(_) = left_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    left,
                    left_result,
                    "left endpoint",
                );
            }
            if let OperationResult::Veto(_) = right_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    right,
                    right_result,
                    "right endpoint",
                );
            }

            let left_value = unwrap_value_after_veto_check(
                &left_result,
                "left endpoint",
                &current.source_location,
            );
            let right_value = unwrap_value_after_veto_check(
                &right_result,
                "right endpoint",
                &current.source_location,
            );

            let range_value = LiteralValue::range(left_value.clone(), right_value.clone());
            let explanation_node = ExplanationNode::Value {
                value: range_value.clone(),
                source: ValueSource::Computed,
                source_location: current.source_location.clone(),
            };
            context.set_explanation_node(current, explanation_node);
            OperationResult::Value(Box::new(range_value))
        }

        ExpressionKind::PastFutureRange(kind, offset_expr) => {
            let offset_result = get_operand_result(results, offset_expr, "offset operand");
            if let OperationResult::Veto(_) = offset_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    offset_expr,
                    offset_result,
                    "offset operand",
                );
            }

            let offset_value = unwrap_value_after_veto_check(
                &offset_result,
                "offset operand",
                &current.source_location,
            );

            let now_value = context.now();
            let now_semantic = match &now_value.value {
                ValueKind::Date(date_time) => date_time,
                _ => unreachable!("BUG: context.now() must be a Date value"),
            };

            let result = crate::computation::datetime::evaluate_past_future_range(
                kind,
                offset_value,
                now_semantic,
            );

            match &result {
                OperationResult::Value(range_value) => {
                    let explanation_node = ExplanationNode::Value {
                        value: range_value.as_ref().clone(),
                        source: ValueSource::Computed,
                        source_location: current.source_location.clone(),
                    };
                    context.set_explanation_node(current, explanation_node);
                }
                OperationResult::Veto(_) => {
                    let offset_explanation =
                        get_explanation_node_required(context, offset_expr, "offset operand");
                    context.set_explanation_node(current, offset_explanation);
                }
            }
            result
        }

        ExpressionKind::RangeContainment(value_expr, range_expr) => {
            let value_result = get_operand_result(results, value_expr, "value operand");
            let range_result = get_operand_result(results, range_expr, "range operand");

            if let OperationResult::Veto(_) = value_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    value_expr,
                    value_result,
                    "value operand",
                );
            }
            if let OperationResult::Veto(_) = range_result {
                return propagate_veto_explanation(
                    context,
                    current,
                    range_expr,
                    range_result,
                    "range operand",
                );
            }

            let value_literal = unwrap_value_after_veto_check(
                &value_result,
                "value operand",
                &current.source_location,
            );
            let range_literal = unwrap_value_after_veto_check(
                &range_result,
                "range operand",
                &current.source_location,
            );

            let contained = match &range_literal.value {
                ValueKind::Range(range_left, range_right) => crate::computation::range::check_containment(
                    value_literal,
                    range_left.as_ref(),
                    range_right.as_ref(),
                ),
                _ => unreachable!(
                    "BUG: range containment reached runtime with non-range operand; planning should have rejected this"
                ),
            };

            let result_value = LiteralValue::from_bool(contained);
            let explanation_node = ExplanationNode::Value {
                value: result_value.clone(),
                source: ValueSource::Computed,
                source_location: current.source_location.clone(),
            };
            context.set_explanation_node(current, explanation_node);
            OperationResult::Value(Box::new(result_value))
        }
    }
}

fn evaluate_mathematical_operator(
    op: &MathematicalComputation,
    value: &LiteralValue,
    context: &mut crate::evaluation::EvaluationContext,
) -> OperationResult {
    use crate::computation::decimal_math::{decimal_acos, decimal_asin, decimal_atan};
    use rust_decimal::MathematicalOps;

    match &value.value {
        ValueKind::Number(stored_rational) => {
            use crate::computation::rational::{commit_rational_to_decimal, decimal_to_rational};
            let stored_decimal = match commit_rational_to_decimal(stored_rational) {
                Ok(decimal) => decimal,
                Err(_) => {
                    return OperationResult::Veto(VetoType::computation(
                        "Mathematical operation requires a decimal-representable input",
                    ));
                }
            };
            let decimal_result: Option<rust_decimal::Decimal> = match op {
                MathematicalComputation::Abs => Some(stored_decimal.abs()),
                MathematicalComputation::Floor => Some(stored_decimal.floor()),
                MathematicalComputation::Ceil => Some(stored_decimal.ceil()),
                MathematicalComputation::Round => Some(stored_decimal.round()),
                MathematicalComputation::Sqrt => stored_decimal.sqrt(),
                MathematicalComputation::Sin => stored_decimal.checked_sin(),
                MathematicalComputation::Cos => stored_decimal.checked_cos(),
                MathematicalComputation::Tan => stored_decimal.checked_tan(),
                MathematicalComputation::Log => stored_decimal.checked_ln(),
                MathematicalComputation::Exp => stored_decimal.checked_exp(),
                MathematicalComputation::Asin => decimal_asin(stored_decimal),
                MathematicalComputation::Acos => decimal_acos(stored_decimal),
                MathematicalComputation::Atan => decimal_atan(stored_decimal),
            };

            let committed_decimal = match decimal_result {
                Some(committed) => committed,
                None => {
                    return OperationResult::Veto(VetoType::computation(
                        "Mathematical operation result is undefined for this input",
                    ));
                }
            };

            let result_rational = decimal_to_rational(committed_decimal)
                .expect("BUG: transcendental result must lift back to stored rational");
            let result_value =
                LiteralValue::number_with_type(result_rational, value.lemma_type.clone());
            context.push_operation(OperationKind::Computation {
                kind: ComputationKind::Mathematical(op.clone()),
                inputs: vec![value.clone()],
                result: result_value.clone(),
            });
            OperationResult::Value(Box::new(result_value))
        }
        _ => unreachable!(
            "BUG: mathematical operator with non-number operand; planning should have rejected this"
        ),
    }
}