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

lemma/evaluation/
expression.rs
