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

lemma/evaluation/
expression.rs
