lemma/evaluation/
mod.rs

1//! Pure Rust evaluation engine for Lemma
2//!
3//! Executes pre-validated execution plans in dependency order.
4//! The execution plan is self-contained with all rules flattened into branches.
5//! The evaluator executes rules linearly without recursion or tree traversal.
6
7pub mod expression;
8pub mod operations;
9pub mod proof;
10pub mod response;
11
12use crate::evaluation::response::EvaluatedRule;
13use crate::planning::semantics::{Expression, Fact, FactPath, FactValue, LiteralValue, RulePath};
14use crate::planning::ExecutionPlan;
15use indexmap::IndexMap;
16pub use operations::{ComputationKind, OperationKind, OperationRecord, OperationResult};
17pub use response::{Facts, Response, RuleResult};
18use std::collections::{HashMap, HashSet};
19
20/// Evaluation context for storing intermediate results
21pub struct EvaluationContext {
22    fact_values: HashMap<FactPath, LiteralValue>,
23    rule_results: HashMap<RulePath, OperationResult>,
24    rule_proofs: HashMap<RulePath, crate::evaluation::proof::Proof>,
25    operations: Vec<crate::OperationRecord>,
26    sources: HashMap<String, String>,
27    proof_nodes: HashMap<Expression, crate::evaluation::proof::ProofNode>,
28}
29
30impl EvaluationContext {
31    fn new(plan: &ExecutionPlan) -> Self {
32        let fact_values: HashMap<FactPath, LiteralValue> = plan
33            .facts
34            .iter()
35            .filter_map(|(path, d)| d.value().map(|v| (path.clone(), v.clone())))
36            .collect();
37        Self {
38            fact_values,
39            rule_results: HashMap::new(),
40            rule_proofs: HashMap::new(),
41            operations: Vec::new(),
42            sources: plan.sources.clone(),
43            proof_nodes: HashMap::new(),
44        }
45    }
46
47    fn get_fact(&self, fact_path: &FactPath) -> Option<&LiteralValue> {
48        self.fact_values.get(fact_path)
49    }
50
51    fn push_operation(&mut self, kind: OperationKind) {
52        self.operations.push(OperationRecord { kind });
53    }
54
55    fn set_proof_node(
56        &mut self,
57        expression: &Expression,
58        node: crate::evaluation::proof::ProofNode,
59    ) {
60        self.proof_nodes.insert(expression.clone(), node);
61    }
62
63    fn get_proof_node(
64        &self,
65        expression: &Expression,
66    ) -> Option<&crate::evaluation::proof::ProofNode> {
67        self.proof_nodes.get(expression)
68    }
69
70    fn get_rule_proof(&self, rule_path: &RulePath) -> Option<&crate::evaluation::proof::Proof> {
71        self.rule_proofs.get(rule_path)
72    }
73
74    fn set_rule_proof(&mut self, rule_path: RulePath, proof: crate::evaluation::proof::Proof) {
75        self.rule_proofs.insert(rule_path, proof);
76    }
77}
78
79/// Evaluates Lemma rules within their document context
80#[derive(Default)]
81pub struct Evaluator;
82
83impl Evaluator {
84    pub fn new() -> Self {
85        Self
86    }
87
88    /// Evaluate an execution plan.
89    ///
90    /// Executes rules in pre-computed dependency order with all facts pre-loaded.
91    /// Rules are already flattened into executable branches with fact prefixes resolved.
92    ///
93    /// After planning, evaluation is guaranteed to complete. This function never returns
94    /// a LemmaError — runtime issues (division by zero, missing facts, user-defined veto)
95    /// produce Vetoes, which are valid evaluation outcomes.
96    pub fn evaluate(&self, plan: &ExecutionPlan) -> Response {
97        let mut context = EvaluationContext::new(plan);
98
99        let mut response = Response {
100            doc_name: plan.doc_name.clone(),
101            facts: Vec::new(),
102            results: IndexMap::new(),
103        };
104
105        let mut seen_facts = HashSet::new();
106        let mut fact_list = Vec::new();
107
108        // Execute each rule in topological order (already sorted by ExecutionPlan)
109        for exec_rule in &plan.rules {
110            context.operations.clear();
111            context.proof_nodes.clear();
112
113            let (result, proof) = expression::evaluate_rule(exec_rule, &mut context);
114
115            context
116                .rule_results
117                .insert(exec_rule.path.clone(), result.clone());
118            context.set_rule_proof(exec_rule.path.clone(), proof.clone());
119
120            let rule_operations = context.operations.clone();
121
122            // Collect facts from operations (semantics types only; no parsing)
123            for op in &rule_operations {
124                if let OperationKind::FactUsed { fact_ref, value } = &op.kind {
125                    if seen_facts.insert(fact_ref.clone()) {
126                        fact_list.push(Fact {
127                            path: fact_ref.clone(),
128                            value: FactValue::Literal(value.clone()),
129                            source: None,
130                        });
131                    }
132                }
133            }
134
135            let unless_branches: Vec<(Option<Expression>, Expression)> = exec_rule.branches[1..]
136                .iter()
137                .map(|b| (b.condition.clone(), b.result.clone()))
138                .collect();
139
140            response.add_result(RuleResult {
141                rule: EvaluatedRule {
142                    name: exec_rule.name.clone(),
143                    path: exec_rule.path.clone(),
144                    default_expression: exec_rule.branches[0].result.clone(),
145                    unless_branches,
146                    source_location: exec_rule.source.clone(),
147                    rule_type: exec_rule.rule_type.clone(),
148                },
149                result,
150                facts: vec![],
151                operations: rule_operations,
152                proof: Some(proof),
153                rule_type: exec_rule.rule_type.clone(),
154            });
155        }
156
157        if !fact_list.is_empty() {
158            response.facts = vec![Facts {
159                fact_path: String::new(),
160                referencing_fact_name: String::new(),
161                document_reference: None,
162                facts: fact_list,
163                referenced_docs: Vec::new(),
164            }];
165        }
166
167        response
168    }
169}
lemma/evaluation/mod.rs

lemma/evaluation/
mod.rs
