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

lemma/evaluation/
expression.rs
