Skip to main content

lemma/evaluation/
expression.rs

1//! Iterative expression evaluation
2//!
3//! Evaluates expressions without recursion using a stack-based approach.
4//! All runtime errors (division by zero, etc.) result in Veto instead of errors.
5
6use super::operations::{ComputationKind, OperationKind, OperationResult};
7use super::proof::{ProofNode, ValueSource};
8use crate::computation::{arithmetic_operation, comparison_operation};
9use crate::planning::semantics::{
10    negated_comparison, Expression, ExpressionKind, LiteralValue, MathematicalComputation,
11    ValueKind,
12};
13use crate::planning::ExecutableRule;
14use std::collections::HashMap;
15
16/// Get a proof node for an expression that was already evaluated.
17/// Panics if the proof node is missing — this indicates a bug in the evaluator,
18/// since we always set a proof node immediately after evaluating an expression.
19fn get_proof_node_required(
20    context: &crate::evaluation::EvaluationContext,
21    expr: &Expression,
22    operand_name: &str,
23) -> ProofNode {
24    let loc = expr
25        .source_location
26        .as_ref()
27        .expect("BUG: expression missing source in evaluation");
28    context.get_proof_node(expr).cloned().unwrap_or_else(|| {
29        unreachable!(
30            "BUG: {} was evaluated but has no proof node ({}:{}:{} in {})",
31            operand_name, loc.attribute, loc.span.line, loc.span.col, loc.spec_name
32        )
33    })
34}
35
36/// Get the result of an operand expression that was already evaluated.
37/// Panics if the result is missing — this indicates a bug in dependency tracking,
38/// since we only evaluate an expression after all its dependencies are ready.
39fn get_operand_result(
40    results: &HashMap<Expression, OperationResult>,
41    expr: &Expression,
42    operand_name: &str,
43) -> OperationResult {
44    let loc = expr
45        .source_location
46        .as_ref()
47        .expect("BUG: expression missing source in evaluation");
48    results.get(expr).cloned().unwrap_or_else(|| {
49        unreachable!(
50            "BUG: {} operand was marked ready but result is missing ({}:{}:{} in {})",
51            operand_name, loc.attribute, loc.span.line, loc.span.col, loc.spec_name
52        )
53    })
54}
55
56/// Extract the value from an OperationResult that is known to not be Veto.
57/// Called only after an explicit Veto check has already returned early.
58/// Panics if the result has no value — this is unreachable after the Veto guard.
59fn unwrap_value_after_veto_check<'a>(
60    result: &'a OperationResult,
61    operand_name: &str,
62    source_location: &Option<crate::planning::semantics::Source>,
63) -> &'a LiteralValue {
64    result.value().unwrap_or_else(|| {
65        let loc = source_location
66            .as_ref()
67            .expect("BUG: expression missing source in evaluation");
68        unreachable!(
69            "BUG: {} passed Veto check but has no value ({}:{}:{} in {})",
70            operand_name, loc.attribute, loc.span.line, loc.span.col, loc.spec_name
71        )
72    })
73}
74
75/// Propagate veto proof from operand to current expression
76fn propagate_veto_proof(
77    context: &mut crate::evaluation::EvaluationContext,
78    current: &Expression,
79    vetoed_operand: &Expression,
80    veto_result: OperationResult,
81    operand_name: &str,
82) -> OperationResult {
83    let proof = get_proof_node_required(context, vetoed_operand, operand_name);
84    context.set_proof_node(current, proof);
85    veto_result
86}
87
88/// Evaluate a rule to produce its final result and proof.
89/// After planning, evaluation is guaranteed to complete — this function never returns
90/// a Error. It produces an OperationResult (Value or Veto) and a Proof tree.
91pub(crate) fn evaluate_rule(
92    exec_rule: &ExecutableRule,
93    context: &mut crate::evaluation::EvaluationContext,
94) -> (OperationResult, crate::evaluation::proof::Proof) {
95    use crate::evaluation::proof::{Branch, NonMatchedBranch};
96
97    // If rule has no unless clauses, just evaluate the default expression
98    if exec_rule.branches.len() == 1 {
99        return evaluate_rule_without_unless(exec_rule, context);
100    }
101
102    // Rule has unless clauses - collect all branch evaluations for Branches proof node
103    let mut non_matched_branches: Vec<NonMatchedBranch> = Vec::new();
104
105    // Evaluate branches in reverse order (last matching wins)
106    for branch_index in (1..exec_rule.branches.len()).rev() {
107        let branch = &exec_rule.branches[branch_index];
108        if let Some(ref condition) = branch.condition {
109            let condition_expr = condition.get_source_text(&context.sources);
110            let result_expr = branch.result.get_source_text(&context.sources);
111
112            let condition_result = evaluate_expression(condition, context);
113            let condition_proof = get_proof_node_required(context, condition, "condition");
114
115            let matched = match condition_result {
116                OperationResult::Veto(ref msg) => {
117                    // Condition vetoed - this becomes the result
118                    let unless_clause_index = branch_index - 1;
119                    context.push_operation(OperationKind::RuleBranchEvaluated {
120                        index: Some(unless_clause_index),
121                        matched: true,
122                        condition_expr,
123                        result_expr,
124                        result_value: Some(OperationResult::Veto(msg.clone())),
125                    });
126
127                    // Build Branches node with this as the matched branch
128                    let matched_branch = Branch {
129                        condition: Some(Box::new(condition_proof)),
130                        result: Box::new(ProofNode::Veto {
131                            message: msg.clone(),
132                            source_location: branch.result.source_location.clone(),
133                        }),
134                        clause_index: Some(unless_clause_index),
135                        source_location: Some(branch.source.clone()),
136                    };
137
138                    let branches_node = ProofNode::Branches {
139                        matched: Box::new(matched_branch),
140                        non_matched: non_matched_branches,
141                        source_location: Some(exec_rule.source.clone()),
142                    };
143
144                    let proof = crate::evaluation::proof::Proof {
145                        rule_path: exec_rule.path.clone(),
146                        source: Some(exec_rule.source.clone()),
147                        result: OperationResult::Veto(msg.clone()),
148                        tree: branches_node,
149                    };
150                    return (OperationResult::Veto(msg.clone()), proof);
151                }
152                OperationResult::Value(lit) => match &lit.value {
153                    ValueKind::Boolean(b) => *b,
154                    _ => {
155                        let veto = OperationResult::Veto(Some(
156                            "Unless condition must evaluate to boolean".to_string(),
157                        ));
158                        let proof = crate::evaluation::proof::Proof {
159                            rule_path: exec_rule.path.clone(),
160                            source: Some(exec_rule.source.clone()),
161                            result: veto.clone(),
162                            tree: ProofNode::Veto {
163                                message: Some(
164                                    "Unless condition must evaluate to boolean".to_string(),
165                                ),
166                                source_location: Some(exec_rule.source.clone()),
167                            },
168                        };
169                        return (veto, proof);
170                    }
171                },
172            };
173
174            let unless_clause_index = branch_index - 1;
175
176            if matched {
177                // This unless clause matched - evaluate its result
178                let result = evaluate_expression(&branch.result, context);
179
180                context.push_operation(OperationKind::RuleBranchEvaluated {
181                    index: Some(unless_clause_index),
182                    matched: true,
183                    condition_expr,
184                    result_expr,
185                    result_value: Some(result.clone()),
186                });
187
188                let result_proof = get_proof_node_required(context, &branch.result, "result");
189
190                // Build Branches node with this as the matched branch
191                let matched_branch = Branch {
192                    condition: Some(Box::new(condition_proof)),
193                    result: Box::new(result_proof),
194                    clause_index: Some(unless_clause_index),
195                    source_location: Some(branch.source.clone()),
196                };
197
198                let branches_node = ProofNode::Branches {
199                    matched: Box::new(matched_branch),
200                    non_matched: non_matched_branches,
201                    source_location: Some(exec_rule.source.clone()),
202                };
203
204                let proof = crate::evaluation::proof::Proof {
205                    rule_path: exec_rule.path.clone(),
206                    source: Some(exec_rule.source.clone()),
207                    result: result.clone(),
208                    tree: branches_node,
209                };
210                return (result, proof);
211            }
212            // Branch didn't match - record it as non-matched.
213            context.push_operation(OperationKind::RuleBranchEvaluated {
214                index: Some(unless_clause_index),
215                matched: false,
216                condition_expr,
217                result_expr,
218                result_value: None,
219            });
220
221            non_matched_branches.push(NonMatchedBranch {
222                condition: Box::new(condition_proof),
223                result: None,
224                clause_index: Some(unless_clause_index),
225                source_location: Some(branch.source.clone()),
226            });
227        }
228    }
229
230    // No unless clause matched - evaluate default expression (first branch)
231    let default_branch = &exec_rule.branches[0];
232    let default_expr = default_branch.result.get_source_text(&context.sources);
233    let default_result = evaluate_expression(&default_branch.result, context);
234
235    context.push_operation(OperationKind::RuleBranchEvaluated {
236        index: None,
237        matched: true,
238        condition_expr: None,
239        result_expr: default_expr,
240        result_value: Some(default_result.clone()),
241    });
242
243    let default_result_proof =
244        get_proof_node_required(context, &default_branch.result, "default result");
245
246    // Default branch has no condition
247    let matched_branch = Branch {
248        condition: None,
249        result: Box::new(default_result_proof),
250        clause_index: None,
251        source_location: Some(default_branch.source.clone()),
252    };
253
254    let branches_node = ProofNode::Branches {
255        matched: Box::new(matched_branch),
256        non_matched: non_matched_branches,
257        source_location: Some(exec_rule.source.clone()),
258    };
259
260    let proof = crate::evaluation::proof::Proof {
261        rule_path: exec_rule.path.clone(),
262        source: Some(exec_rule.source.clone()),
263        result: default_result.clone(),
264        tree: branches_node,
265    };
266
267    (default_result, proof)
268}
269
270/// Evaluate a rule that has no unless clauses (simple case)
271fn evaluate_rule_without_unless(
272    exec_rule: &ExecutableRule,
273    context: &mut crate::evaluation::EvaluationContext,
274) -> (OperationResult, crate::evaluation::proof::Proof) {
275    let default_branch = &exec_rule.branches[0];
276    let default_expr = default_branch.result.get_source_text(&context.sources);
277    let default_result = evaluate_expression(&default_branch.result, context);
278
279    context.push_operation(OperationKind::RuleBranchEvaluated {
280        index: None,
281        matched: true,
282        condition_expr: None,
283        result_expr: default_expr,
284        result_value: Some(default_result.clone()),
285    });
286
287    let root_proof_node =
288        get_proof_node_required(context, &default_branch.result, "default result");
289
290    let proof = crate::evaluation::proof::Proof {
291        rule_path: exec_rule.path.clone(),
292        source: Some(exec_rule.source.clone()),
293        result: default_result.clone(),
294        tree: root_proof_node,
295    };
296
297    (default_result, proof)
298}
299
300/// Evaluate an expression iteratively without recursion.
301/// Uses a work list approach: collect all expressions first, then evaluate in dependency order.
302/// After planning, expression evaluation is guaranteed to complete — this function never
303/// returns a Error. It produces an OperationResult (Value or Veto).
304fn evaluate_expression(
305    expr: &Expression,
306    context: &mut crate::evaluation::EvaluationContext,
307) -> OperationResult {
308    // First, collect all expressions in the tree
309    let mut all_exprs: HashMap<Expression, ()> = HashMap::new();
310    let mut work_list: Vec<&Expression> = vec![expr];
311
312    while let Some(e) = work_list.pop() {
313        if all_exprs.contains_key(e) {
314            continue;
315        }
316        all_exprs.insert(e.clone(), ());
317
318        // Add dependencies to work list
319        match &e.kind {
320            ExpressionKind::Arithmetic(left, _, right)
321            | ExpressionKind::Comparison(left, _, right)
322            | ExpressionKind::LogicalAnd(left, right) => {
323                work_list.push(left);
324                work_list.push(right);
325            }
326            ExpressionKind::LogicalNegation(operand, _)
327            | ExpressionKind::UnitConversion(operand, _)
328            | ExpressionKind::MathematicalComputation(_, operand)
329            | ExpressionKind::DateCalendar(_, _, operand) => {
330                work_list.push(operand);
331            }
332            ExpressionKind::DateRelative(_, date_expr, tolerance_expr) => {
333                work_list.push(date_expr);
334                if let Some(tol) = tolerance_expr {
335                    work_list.push(tol);
336                }
337            }
338            _ => {}
339        }
340    }
341
342    // Now evaluate expressions in dependency order
343    let mut results: HashMap<Expression, OperationResult> = HashMap::new();
344    let mut remaining: Vec<Expression> = all_exprs.keys().cloned().collect();
345
346    while !remaining.is_empty() {
347        let mut progress = false;
348        let mut to_remove = Vec::new();
349
350        for current in &remaining {
351            // Check if all dependencies are ready
352            let deps_ready = match &current.kind {
353                ExpressionKind::Arithmetic(left, _, right)
354                | ExpressionKind::Comparison(left, _, right)
355                | ExpressionKind::LogicalAnd(left, right) => {
356                    results.contains_key(left.as_ref()) && results.contains_key(right.as_ref())
357                }
358                ExpressionKind::LogicalNegation(operand, _)
359                | ExpressionKind::UnitConversion(operand, _)
360                | ExpressionKind::MathematicalComputation(_, operand)
361                | ExpressionKind::DateCalendar(_, _, operand) => {
362                    results.contains_key(operand.as_ref())
363                }
364                ExpressionKind::DateRelative(_, date_expr, tolerance_expr) => {
365                    results.contains_key(date_expr.as_ref())
366                        && tolerance_expr
367                            .as_ref()
368                            .is_none_or(|t| results.contains_key(t.as_ref()))
369                }
370                _ => true,
371            };
372
373            if deps_ready {
374                to_remove.push(current.clone());
375                progress = true;
376            }
377        }
378
379        if !progress {
380            let loc = expr
381                .source_location
382                .as_ref()
383                .expect("BUG: expression missing source in evaluation");
384            unreachable!(
385                "BUG: circular dependency or missing dependency in expression tree ({}:{}:{} in {})",
386                loc.attribute, loc.span.start, loc.span.end, loc.spec_name
387            );
388        }
389
390        // Evaluate expressions that are ready
391        for current in &to_remove {
392            let result = evaluate_single_expression(current, &results, context);
393            results.insert(current.clone(), result);
394        }
395
396        for key in &to_remove {
397            remaining.retain(|k| k != key);
398        }
399    }
400
401    let loc = expr
402        .source_location
403        .as_ref()
404        .expect("BUG: expression missing source in evaluation");
405    results.get(expr).cloned().unwrap_or_else(|| {
406        unreachable!(
407            "BUG: expression was processed but has no result ({}:{}:{} in {})",
408            loc.attribute, loc.span.start, loc.span.end, loc.spec_name
409        )
410    })
411}
412
413/// Evaluate a single expression given its dependencies are already evaluated.
414/// After planning, this function is guaranteed to complete — it produces an OperationResult
415/// (Value or Veto) without ever returning a Error.
416fn evaluate_single_expression(
417    current: &Expression,
418    results: &HashMap<Expression, OperationResult>,
419    context: &mut crate::evaluation::EvaluationContext,
420) -> OperationResult {
421    match &current.kind {
422        ExpressionKind::Literal(lit) => {
423            let value = lit.as_ref().clone();
424            let proof_node = ProofNode::Value {
425                value: value.clone(),
426                source: ValueSource::Literal,
427                source_location: current.source_location.clone(),
428            };
429            context.set_proof_node(current, proof_node);
430            OperationResult::Value(Box::new(value))
431        }
432
433        ExpressionKind::FactPath(fact_path) => {
434            // Fact lookup: a fact can legitimately be missing (TypeDeclaration without a
435            // provided value at runtime). Returning None → Veto("Missing fact: ...") is
436            // correct domain behavior.
437            let fact_path_clone = fact_path.clone();
438            let value = context.get_fact(fact_path).cloned();
439            match value {
440                Some(v) => {
441                    context.push_operation(OperationKind::FactUsed {
442                        fact_ref: fact_path_clone.clone(),
443                        value: v.clone(),
444                    });
445                    let proof_node = ProofNode::Value {
446                        value: v.clone(),
447                        source: ValueSource::Fact {
448                            fact_ref: fact_path_clone,
449                        },
450                        source_location: current.source_location.clone(),
451                    };
452                    context.set_proof_node(current, proof_node);
453                    OperationResult::Value(Box::new(v))
454                }
455                None => {
456                    let proof_node = ProofNode::Veto {
457                        message: Some(format!("Missing fact: {}", fact_path)),
458                        source_location: current.source_location.clone(),
459                    };
460                    context.set_proof_node(current, proof_node);
461                    OperationResult::Veto(Some(format!("Missing fact: {}", fact_path)))
462                }
463            }
464        }
465
466        ExpressionKind::RulePath(rule_path) => {
467            // Rule lookup: rules are evaluated in topological order. If a referenced rule's
468            // result is not in the map, planning guaranteed no cycles and topological sort
469            // ensured the dependency was evaluated first. Missing result is a bug.
470            let rule_path_clone = rule_path.clone();
471            let loc = current
472                .source_location
473                .as_ref()
474                .expect("BUG: expression missing source in evaluation");
475            let r = context.rule_results.get(rule_path).cloned().unwrap_or_else(|| {
476                unreachable!(
477                    "BUG: Rule '{}' not found in results during topological-order evaluation ({}:{}:{} in {})",
478                    rule_path.rule, loc.attribute, loc.span.line, loc.span.col, loc.spec_name
479                )
480            });
481
482            context.push_operation(OperationKind::RuleUsed {
483                rule_path: rule_path_clone.clone(),
484                result: r.clone(),
485            });
486
487            // Get the full proof tree from the referenced rule
488            let expansion = match context.get_rule_proof(rule_path) {
489                Some(existing_proof) => existing_proof.tree.clone(),
490                None => ProofNode::Value {
491                    value: match &r {
492                        OperationResult::Value(v) => v.as_ref().clone(),
493                        OperationResult::Veto(_) => LiteralValue::from_bool(false),
494                    },
495                    source: ValueSource::Computed,
496                    source_location: current.source_location.clone(),
497                },
498            };
499
500            let proof_node = ProofNode::RuleReference {
501                rule_path: rule_path_clone,
502                result: r.clone(),
503                source_location: current.source_location.clone(),
504                expansion: Box::new(expansion),
505            };
506            context.set_proof_node(current, proof_node);
507            r
508        }
509
510        ExpressionKind::Arithmetic(left, op, right) => {
511            let left_result = get_operand_result(results, left, "left");
512            let right_result = get_operand_result(results, right, "right");
513
514            if let OperationResult::Veto(_) = left_result {
515                return propagate_veto_proof(context, current, left, left_result, "left operand");
516            }
517            if let OperationResult::Veto(_) = right_result {
518                return propagate_veto_proof(
519                    context,
520                    current,
521                    right,
522                    right_result,
523                    "right operand",
524                );
525            }
526
527            let left_val = unwrap_value_after_veto_check(
528                &left_result,
529                "left operand",
530                &current.source_location,
531            );
532            let right_val = unwrap_value_after_veto_check(
533                &right_result,
534                "right operand",
535                &current.source_location,
536            );
537
538            let result = arithmetic_operation(left_val, op, right_val);
539
540            let left_proof = get_proof_node_required(context, left, "left operand");
541            let right_proof = get_proof_node_required(context, right, "right operand");
542
543            if let OperationResult::Value(ref val) = result {
544                let expr_text = current.get_source_text(&context.sources);
545                // Use source text if available, otherwise construct from values for proof display
546                let original_expr = expr_text
547                    .clone()
548                    .unwrap_or_else(|| format!("{} {} {}", left_val, op.symbol(), right_val));
549                let substituted_expr = format!("{} {} {}", left_val, op.symbol(), right_val);
550                context.push_operation(OperationKind::Computation {
551                    kind: ComputationKind::Arithmetic(op.clone()),
552                    inputs: vec![left_val.clone(), right_val.clone()],
553                    result: val.as_ref().clone(),
554                    expr: expr_text,
555                });
556                let proof_node = ProofNode::Computation {
557                    kind: ComputationKind::Arithmetic(op.clone()),
558                    original_expression: original_expr,
559                    expression: substituted_expr,
560                    result: val.as_ref().clone(),
561                    source_location: current.source_location.clone(),
562                    operands: vec![left_proof, right_proof],
563                };
564                context.set_proof_node(current, proof_node);
565            } else if let OperationResult::Veto(_) = result {
566                context.set_proof_node(current, left_proof);
567            }
568            result
569        }
570
571        ExpressionKind::Comparison(left, op, right) => {
572            let left_result = get_operand_result(results, left, "left");
573            let right_result = get_operand_result(results, right, "right");
574
575            if let OperationResult::Veto(_) = left_result {
576                return propagate_veto_proof(context, current, left, left_result, "left operand");
577            }
578            if let OperationResult::Veto(_) = right_result {
579                return propagate_veto_proof(
580                    context,
581                    current,
582                    right,
583                    right_result,
584                    "right operand",
585                );
586            }
587
588            let left_val = unwrap_value_after_veto_check(
589                &left_result,
590                "left operand",
591                &current.source_location,
592            );
593            let right_val = unwrap_value_after_veto_check(
594                &right_result,
595                "right operand",
596                &current.source_location,
597            );
598
599            let result = comparison_operation(left_val, op, right_val);
600
601            let left_proof = get_proof_node_required(context, left, "left operand");
602            let right_proof = get_proof_node_required(context, right, "right operand");
603
604            if let OperationResult::Value(ref val) = result {
605                let is_false = matches!(val.as_ref().value, ValueKind::Boolean(false));
606                let (display_op, original_expr, substituted_expr, display_result) = if is_false {
607                    let negated_op = negated_comparison(op.clone());
608                    let orig = match (
609                        left.get_source_text(&context.sources),
610                        right.get_source_text(&context.sources),
611                    ) {
612                        (Some(l), Some(r)) => {
613                            format!("{} {} {}", l, negated_op.symbol(), r)
614                        }
615                        _ => format!("{} {} {}", left_val, negated_op.symbol(), right_val),
616                    };
617                    let sub = format!("{} {} {}", left_val, negated_op.symbol(), right_val);
618                    (negated_op, orig, sub, LiteralValue::from_bool(true))
619                } else {
620                    let expr_text = current.get_source_text(&context.sources);
621                    let original_expr = expr_text
622                        .clone()
623                        .unwrap_or_else(|| format!("{} {} {}", left_val, op.symbol(), right_val));
624                    let substituted_expr = format!("{} {} {}", left_val, op.symbol(), right_val);
625                    (
626                        op.clone(),
627                        original_expr,
628                        substituted_expr,
629                        val.as_ref().clone(),
630                    )
631                };
632                let expr_text = current.get_source_text(&context.sources);
633                context.push_operation(OperationKind::Computation {
634                    kind: ComputationKind::Comparison(op.clone()),
635                    inputs: vec![left_val.clone(), right_val.clone()],
636                    result: val.as_ref().clone(),
637                    expr: expr_text,
638                });
639                let proof_node = ProofNode::Computation {
640                    kind: ComputationKind::Comparison(display_op),
641                    original_expression: original_expr,
642                    expression: substituted_expr,
643                    result: display_result,
644                    source_location: current.source_location.clone(),
645                    operands: vec![left_proof, right_proof],
646                };
647                context.set_proof_node(current, proof_node);
648            } else if let OperationResult::Veto(_) = result {
649                context.set_proof_node(current, left_proof);
650            }
651            result
652        }
653
654        ExpressionKind::LogicalAnd(left, right) => {
655            let left_result = get_operand_result(results, left, "left");
656            if let OperationResult::Veto(_) = left_result {
657                return propagate_veto_proof(context, current, left, left_result, "left operand");
658            }
659
660            let left_val = unwrap_value_after_veto_check(
661                &left_result,
662                "left operand",
663                &current.source_location,
664            );
665            let left_bool = match &left_val.value {
666                ValueKind::Boolean(b) => b,
667                _ => {
668                    return OperationResult::Veto(Some(
669                        "Logical AND requires boolean operands".to_string(),
670                    ));
671                }
672            };
673
674            if !*left_bool {
675                let left_proof = get_proof_node_required(context, left, "left operand");
676                context.set_proof_node(current, left_proof);
677                OperationResult::Value(Box::new(LiteralValue::from_bool(false)))
678            } else {
679                let right_result = get_operand_result(results, right, "right");
680                let right_proof = get_proof_node_required(context, right, "right operand");
681                context.set_proof_node(current, right_proof);
682                right_result
683            }
684        }
685
686        ExpressionKind::LogicalNegation(operand, _) => {
687            let result = get_operand_result(results, operand, "operand");
688            if let OperationResult::Veto(_) = result {
689                return propagate_veto_proof(context, current, operand, result, "operand");
690            }
691
692            let value = unwrap_value_after_veto_check(&result, "operand", &current.source_location);
693            let operand_proof = get_proof_node_required(context, operand, "operand");
694            match &value.value {
695                ValueKind::Boolean(b) => {
696                    let result_bool = !*b;
697                    context.set_proof_node(current, operand_proof);
698                    OperationResult::Value(Box::new(LiteralValue::from_bool(result_bool)))
699                }
700                _ => {
701                    OperationResult::Veto(Some("Logical NOT requires boolean operand".to_string()))
702                }
703            }
704        }
705
706        ExpressionKind::UnitConversion(value_expr, target) => {
707            let result = get_operand_result(results, value_expr, "operand");
708            if let OperationResult::Veto(_) = result {
709                return propagate_veto_proof(context, current, value_expr, result, "operand");
710            }
711
712            let value = unwrap_value_after_veto_check(&result, "operand", &current.source_location);
713            let operand_proof = get_proof_node_required(context, value_expr, "operand");
714
715            let conversion_result = crate::computation::convert_unit(value, target);
716
717            context.set_proof_node(current, operand_proof);
718            conversion_result
719        }
720
721        ExpressionKind::MathematicalComputation(op, operand) => {
722            let result = get_operand_result(results, operand, "operand");
723            if let OperationResult::Veto(_) = result {
724                return propagate_veto_proof(context, current, operand, result, "operand");
725            }
726
727            let value = unwrap_value_after_veto_check(&result, "operand", &current.source_location);
728            let operand_proof = get_proof_node_required(context, operand, "operand");
729            let math_result = evaluate_mathematical_operator(op, value, context);
730            context.set_proof_node(current, operand_proof);
731            math_result
732        }
733
734        ExpressionKind::Veto(veto_expr) => {
735            let proof_node = ProofNode::Veto {
736                message: veto_expr.message.clone(),
737                source_location: current.source_location.clone(),
738            };
739            context.set_proof_node(current, proof_node);
740            OperationResult::Veto(veto_expr.message.clone())
741        }
742
743        ExpressionKind::Now => {
744            let value = context.now().clone();
745            let proof_node = ProofNode::Value {
746                value: value.clone(),
747                source: ValueSource::Computed,
748                source_location: current.source_location.clone(),
749            };
750            context.set_proof_node(current, proof_node);
751            OperationResult::Value(Box::new(value))
752        }
753
754        ExpressionKind::DateRelative(kind, date_expr, tolerance_expr) => {
755            let date_result = get_operand_result(results, date_expr, "date operand");
756            if let OperationResult::Veto(_) = date_result {
757                return propagate_veto_proof(
758                    context,
759                    current,
760                    date_expr,
761                    date_result,
762                    "date operand",
763                );
764            }
765
766            let date_val = unwrap_value_after_veto_check(
767                &date_result,
768                "date operand",
769                &current.source_location,
770            );
771
772            let date_semantic = match &date_val.value {
773                ValueKind::Date(dt) => dt,
774                _ => {
775                    return OperationResult::Veto(Some(
776                        "Date sugar 'in past/future' requires a date value".to_string(),
777                    ))
778                }
779            };
780
781            let now_val = context.now();
782            let now_semantic = match &now_val.value {
783                ValueKind::Date(dt) => dt,
784                _ => unreachable!("BUG: context.now() must be a Date value"),
785            };
786
787            let tolerance = match tolerance_expr {
788                Some(tol_expr) => {
789                    let tol_result = get_operand_result(results, tol_expr, "tolerance operand");
790                    if let OperationResult::Veto(_) = tol_result {
791                        return propagate_veto_proof(
792                            context,
793                            current,
794                            tol_expr,
795                            tol_result,
796                            "tolerance operand",
797                        );
798                    }
799                    let tol_val = unwrap_value_after_veto_check(
800                        &tol_result,
801                        "tolerance operand",
802                        &current.source_location,
803                    );
804                    match &tol_val.value {
805                        ValueKind::Duration(amount, unit) => Some((*amount, unit.clone())),
806                        _ => {
807                            return OperationResult::Veto(Some(
808                                "Tolerance in date sugar must be a duration value".to_string(),
809                            ))
810                        }
811                    }
812                }
813                None => None,
814            };
815
816            let result = crate::computation::datetime::compute_date_relative(
817                kind,
818                date_semantic,
819                tolerance.as_ref().map(|(a, u)| (a, u)),
820                now_semantic,
821            );
822
823            let date_proof = get_proof_node_required(context, date_expr, "date operand");
824            context.set_proof_node(current, date_proof);
825            result
826        }
827
828        ExpressionKind::DateCalendar(kind, unit, date_expr) => {
829            let date_result = get_operand_result(results, date_expr, "date operand");
830            if let OperationResult::Veto(_) = date_result {
831                return propagate_veto_proof(
832                    context,
833                    current,
834                    date_expr,
835                    date_result,
836                    "date operand",
837                );
838            }
839
840            let date_val = unwrap_value_after_veto_check(
841                &date_result,
842                "date operand",
843                &current.source_location,
844            );
845
846            let date_semantic = match &date_val.value {
847                ValueKind::Date(dt) => dt,
848                _ => {
849                    return OperationResult::Veto(Some(
850                        "Calendar sugar requires a date value".to_string(),
851                    ))
852                }
853            };
854
855            let now_val = context.now();
856            let now_semantic = match &now_val.value {
857                ValueKind::Date(dt) => dt,
858                _ => unreachable!("BUG: context.now() must be a Date value"),
859            };
860
861            let result = crate::computation::datetime::compute_date_calendar(
862                kind,
863                unit,
864                date_semantic,
865                now_semantic,
866            );
867
868            let date_proof = get_proof_node_required(context, date_expr, "date operand");
869            context.set_proof_node(current, date_proof);
870            result
871        }
872    }
873}
874
875fn evaluate_mathematical_operator(
876    op: &MathematicalComputation,
877    value: &LiteralValue,
878    context: &mut crate::evaluation::EvaluationContext,
879) -> OperationResult {
880    match &value.value {
881        ValueKind::Number(n) => {
882            use rust_decimal::prelude::ToPrimitive;
883            let float_val = match n.to_f64() {
884                Some(v) => v,
885                None => {
886                    return OperationResult::Veto(Some(
887                        "Cannot convert to float for mathematical operation".to_string(),
888                    ));
889                }
890            };
891
892            let math_result = match op {
893                MathematicalComputation::Sqrt => float_val.sqrt(),
894                MathematicalComputation::Sin => float_val.sin(),
895                MathematicalComputation::Cos => float_val.cos(),
896                MathematicalComputation::Tan => float_val.tan(),
897                MathematicalComputation::Asin => float_val.asin(),
898                MathematicalComputation::Acos => float_val.acos(),
899                MathematicalComputation::Atan => float_val.atan(),
900                MathematicalComputation::Log => float_val.ln(),
901                MathematicalComputation::Exp => float_val.exp(),
902                MathematicalComputation::Abs => {
903                    return OperationResult::Value(Box::new(LiteralValue::number_with_type(
904                        n.abs(),
905                        value.lemma_type.clone(),
906                    )));
907                }
908                MathematicalComputation::Floor => {
909                    return OperationResult::Value(Box::new(LiteralValue::number_with_type(
910                        n.floor(),
911                        value.lemma_type.clone(),
912                    )));
913                }
914                MathematicalComputation::Ceil => {
915                    return OperationResult::Value(Box::new(LiteralValue::number_with_type(
916                        n.ceil(),
917                        value.lemma_type.clone(),
918                    )));
919                }
920                MathematicalComputation::Round => {
921                    return OperationResult::Value(Box::new(LiteralValue::number_with_type(
922                        n.round(),
923                        value.lemma_type.clone(),
924                    )));
925                }
926            };
927
928            let decimal_result = match rust_decimal::Decimal::from_f64_retain(math_result) {
929                Some(d) => d,
930                None => {
931                    return OperationResult::Veto(Some(
932                        "Mathematical operation result cannot be represented".to_string(),
933                    ));
934                }
935            };
936
937            let result_value =
938                LiteralValue::number_with_type(decimal_result, value.lemma_type.clone());
939            context.push_operation(OperationKind::Computation {
940                kind: ComputationKind::Mathematical(op.clone()),
941                inputs: vec![value.clone()],
942                result: result_value.clone(),
943                expr: None,
944            });
945            OperationResult::Value(Box::new(result_value))
946        }
947        _ => OperationResult::Veto(Some(
948            "Mathematical operators require number operands".to_string(),
949        )),
950    }
951}