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

lemma/evaluation/
expression.rs
