Skip to main content

lemma/evaluation/
expression.rs

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