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::planning::ExecutionPlan;
13use crate::{
14    Expression, FactPath, FactReference, FactValue, LemmaFact, LemmaResult, LiteralValue, RulePath,
15};
16use indexmap::IndexMap;
17pub use operations::{ComputationKind, OperationKind, OperationRecord, OperationResult};
18pub use response::{Facts, Response, RuleResult};
19use std::collections::{HashMap, HashSet};
20
21/// Evaluation context for storing intermediate results
22pub struct EvaluationContext {
23    fact_values: HashMap<FactPath, LiteralValue>,
24    rule_results: HashMap<RulePath, OperationResult>,
25    rule_proofs: HashMap<RulePath, crate::evaluation::proof::Proof>,
26    operations: Vec<crate::OperationRecord>,
27    sources: HashMap<String, String>,
28    proof_nodes: HashMap<Expression, crate::evaluation::proof::ProofNode>,
29}
30
31impl EvaluationContext {
32    fn new(plan: &ExecutionPlan) -> Self {
33        Self {
34            fact_values: plan.fact_values.clone(),
35            rule_results: HashMap::new(),
36            rule_proofs: HashMap::new(),
37            operations: Vec::new(),
38            sources: plan.sources.clone(),
39            proof_nodes: HashMap::new(),
40        }
41    }
42
43    fn get_fact(&self, fact_path: &FactPath) -> Option<&LiteralValue> {
44        self.fact_values.get(fact_path)
45    }
46
47    fn push_operation(&mut self, kind: OperationKind) {
48        self.operations.push(OperationRecord { kind });
49    }
50
51    fn set_proof_node(
52        &mut self,
53        expression: &Expression,
54        node: crate::evaluation::proof::ProofNode,
55    ) {
56        self.proof_nodes.insert(expression.clone(), node);
57    }
58
59    fn get_proof_node(
60        &self,
61        expression: &Expression,
62    ) -> Option<&crate::evaluation::proof::ProofNode> {
63        self.proof_nodes.get(expression)
64    }
65
66    fn get_rule_proof(&self, rule_path: &RulePath) -> Option<&crate::evaluation::proof::Proof> {
67        self.rule_proofs.get(rule_path)
68    }
69
70    fn set_rule_proof(&mut self, rule_path: RulePath, proof: crate::evaluation::proof::Proof) {
71        self.rule_proofs.insert(rule_path, proof);
72    }
73}
74
75/// Evaluates Lemma rules within their document context
76#[derive(Default)]
77pub struct Evaluator;
78
79impl Evaluator {
80    pub fn new() -> Self {
81        Self
82    }
83
84    /// Evaluate an execution plan
85    ///
86    /// Executes rules in pre-computed dependency order with all facts pre-loaded.
87    /// Rules are already flattened into executable branches with fact prefixes resolved.
88    /// This evaluation never errors - runtime issues create Vetoes instead.
89    pub fn evaluate(&self, plan: &ExecutionPlan) -> LemmaResult<Response> {
90        let mut context = EvaluationContext::new(plan);
91
92        let mut response = Response {
93            doc_name: plan.doc_name.clone(),
94            facts: Vec::new(),
95            results: IndexMap::new(),
96        };
97
98        let mut seen_facts = HashSet::new();
99        let mut fact_list = Vec::new();
100
101        // Execute each rule in topological order (already sorted by ExecutionPlan)
102        for exec_rule in &plan.rules {
103            context.operations.clear();
104            context.proof_nodes.clear();
105
106            let (result, proof) = expression::evaluate_rule(exec_rule, &mut context)?;
107
108            context
109                .rule_results
110                .insert(exec_rule.path.clone(), result.clone());
111            context.set_rule_proof(exec_rule.path.clone(), proof.clone());
112
113            let rule_operations = context.operations.clone();
114
115            // Collect facts from operations as we go
116            for op in &rule_operations {
117                if let OperationKind::FactUsed { fact_ref, value } = &op.kind {
118                    if seen_facts.insert(fact_ref.clone()) {
119                        let segments: Vec<String> =
120                            fact_ref.segments.iter().map(|s| s.fact.clone()).collect();
121                        fact_list.push(LemmaFact {
122                            reference: FactReference {
123                                segments,
124                                fact: fact_ref.fact.clone(),
125                            },
126                            value: FactValue::Literal(value.clone()),
127                            source_location: None,
128                        });
129                    }
130                }
131            }
132
133            response.add_result(RuleResult {
134                rule: crate::LemmaRule {
135                    name: exec_rule.name.clone(),
136                    expression: exec_rule.branches[0].result.clone(),
137                    unless_clauses: exec_rule.branches[1..]
138                        .iter()
139                        .filter_map(|b| {
140                            b.condition.as_ref().map(|cond| crate::UnlessClause {
141                                condition: cond.clone(),
142                                result: b.result.clone(),
143                                source_location: b.source.clone(),
144                            })
145                        })
146                        .collect(),
147                    source_location: exec_rule.source.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        Ok(response)
168    }
169}
lemma/evaluation/mod.rs

lemma/evaluation/
mod.rs
