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;
19
20/// Evaluation context for storing intermediate results
21pub(crate) struct EvaluationContext {
22    fact_values: HashMap<FactPath, LiteralValue>,
23    pub(crate) rule_results: HashMap<RulePath, OperationResult>,
24    rule_proofs: HashMap<RulePath, crate::evaluation::proof::Proof>,
25    operations: Vec<crate::OperationRecord>,
26    pub(crate) sources: HashMap<String, String>,
27    proof_nodes: HashMap<usize, crate::evaluation::proof::ProofNode>,
28    /// The effective datetime (`now` keyword resolves to this).
29    now: LiteralValue,
30}
31
32impl EvaluationContext {
33    fn new(plan: &ExecutionPlan, now: LiteralValue) -> Self {
34        let fact_values: HashMap<FactPath, LiteralValue> = plan
35            .facts
36            .iter()
37            .filter_map(|(path, d)| d.value().map(|v| (path.clone(), v.clone())))
38            .collect();
39        Self {
40            fact_values,
41            rule_results: HashMap::new(),
42            rule_proofs: HashMap::new(),
43            operations: Vec::new(),
44            sources: plan.sources.clone(),
45            proof_nodes: HashMap::new(),
46            now,
47        }
48    }
49
50    pub(crate) fn now(&self) -> &LiteralValue {
51        &self.now
52    }
53
54    fn get_fact(&self, fact_path: &FactPath) -> Option<&LiteralValue> {
55        self.fact_values.get(fact_path)
56    }
57
58    fn push_operation(&mut self, kind: OperationKind) {
59        self.operations.push(OperationRecord { kind });
60    }
61
62    fn set_proof_node(
63        &mut self,
64        expression: &Expression,
65        node: crate::evaluation::proof::ProofNode,
66    ) {
67        self.proof_nodes
68            .insert(expression as *const Expression as usize, node);
69    }
70
71    fn get_proof_node(
72        &self,
73        expression: &Expression,
74    ) -> Option<&crate::evaluation::proof::ProofNode> {
75        self.proof_nodes
76            .get(&(expression as *const Expression as usize))
77    }
78
79    fn get_rule_proof(&self, rule_path: &RulePath) -> Option<&crate::evaluation::proof::Proof> {
80        self.rule_proofs.get(rule_path)
81    }
82
83    fn set_rule_proof(&mut self, rule_path: RulePath, proof: crate::evaluation::proof::Proof) {
84        self.rule_proofs.insert(rule_path, proof);
85    }
86}
87
88/// Evaluates Lemma rules within their spec context
89#[derive(Default)]
90pub(crate) struct Evaluator;
91
92impl Evaluator {
93    /// Evaluate an execution plan.
94    ///
95    /// Executes rules in pre-computed dependency order with all facts pre-loaded.
96    /// Rules are already flattened into executable branches with fact prefixes resolved.
97    ///
98    /// After planning, evaluation is guaranteed to complete. This function never returns
99    /// a Error — runtime issues (division by zero, missing facts, user-defined veto)
100    /// produce Vetoes, which are valid evaluation outcomes.
101    pub(crate) fn evaluate(&self, plan: &ExecutionPlan, now: LiteralValue) -> Response {
102        let mut context = EvaluationContext::new(plan, now);
103
104        let mut response = Response {
105            spec_name: plan.spec_name.clone(),
106            facts: Vec::new(),
107            results: IndexMap::new(),
108        };
109
110        let mut used_facts: HashMap<FactPath, LiteralValue> = HashMap::new();
111
112        // Execute each rule in topological order (already sorted by ExecutionPlan)
113        for exec_rule in &plan.rules {
114            context.operations.clear();
115            context.proof_nodes.clear();
116
117            let (result, proof) = expression::evaluate_rule(exec_rule, &mut context);
118
119            context
120                .rule_results
121                .insert(exec_rule.path.clone(), result.clone());
122            context.set_rule_proof(exec_rule.path.clone(), proof.clone());
123
124            let rule_operations = context.operations.clone();
125
126            for op in &rule_operations {
127                if let OperationKind::FactUsed { fact_ref, value } = &op.kind {
128                    used_facts.entry(fact_ref.clone()).or_insert(value.clone());
129                }
130            }
131
132            if !exec_rule.path.segments.is_empty() {
133                continue;
134            }
135
136            let unless_branches: Vec<(Option<Expression>, Expression)> = exec_rule.branches[1..]
137                .iter()
138                .map(|b| (b.condition.clone(), b.result.clone()))
139                .collect();
140
141            response.add_result(RuleResult {
142                rule: EvaluatedRule {
143                    name: exec_rule.name.clone(),
144                    path: exec_rule.path.clone(),
145                    default_expression: exec_rule.branches[0].result.clone(),
146                    unless_branches,
147                    source_location: exec_rule.source.clone(),
148                    rule_type: exec_rule.rule_type.clone(),
149                },
150                result,
151                facts: vec![],
152                operations: rule_operations,
153                proof: Some(proof),
154                rule_type: exec_rule.rule_type.clone(),
155            });
156        }
157
158        // Build fact list in definition order (plan.facts is an IndexMap)
159        let fact_list: Vec<Fact> = plan
160            .facts
161            .keys()
162            .filter_map(|path| {
163                used_facts.remove(path).map(|value| Fact {
164                    path: path.clone(),
165                    value: FactValue::Literal(value),
166                    source: None,
167                })
168            })
169            .collect();
170
171        if !fact_list.is_empty() {
172            response.facts = vec![Facts {
173                fact_path: String::new(),
174                referencing_fact_name: String::new(),
175                facts: fact_list,
176            }];
177        }
178
179        response
180    }
181}
lemma/evaluation/mod.rs

lemma/evaluation/
mod.rs
