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<Expression, 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.insert(expression.clone(), node);
68    }
69
70    fn get_proof_node(
71        &self,
72        expression: &Expression,
73    ) -> Option<&crate::evaluation::proof::ProofNode> {
74        self.proof_nodes.get(expression)
75    }
76
77    fn get_rule_proof(&self, rule_path: &RulePath) -> Option<&crate::evaluation::proof::Proof> {
78        self.rule_proofs.get(rule_path)
79    }
80
81    fn set_rule_proof(&mut self, rule_path: RulePath, proof: crate::evaluation::proof::Proof) {
82        self.rule_proofs.insert(rule_path, proof);
83    }
84}
85
86/// Evaluates Lemma rules within their spec context
87#[derive(Default)]
88pub(crate) struct Evaluator;
89
90impl Evaluator {
91    /// Evaluate an execution plan.
92    ///
93    /// Executes rules in pre-computed dependency order with all facts pre-loaded.
94    /// Rules are already flattened into executable branches with fact prefixes resolved.
95    ///
96    /// After planning, evaluation is guaranteed to complete. This function never returns
97    /// a Error — runtime issues (division by zero, missing facts, user-defined veto)
98    /// produce Vetoes, which are valid evaluation outcomes.
99    pub(crate) fn evaluate(&self, plan: &ExecutionPlan, now: LiteralValue) -> Response {
100        let mut context = EvaluationContext::new(plan, now);
101
102        let mut response = Response {
103            spec_name: plan.spec_name.clone(),
104            facts: Vec::new(),
105            results: IndexMap::new(),
106        };
107
108        let mut used_facts: HashMap<FactPath, LiteralValue> = HashMap::new();
109
110        // Execute each rule in topological order (already sorted by ExecutionPlan)
111        for exec_rule in &plan.rules {
112            context.operations.clear();
113            context.proof_nodes.clear();
114
115            let (result, proof) = expression::evaluate_rule(exec_rule, &mut context);
116
117            context
118                .rule_results
119                .insert(exec_rule.path.clone(), result.clone());
120            context.set_rule_proof(exec_rule.path.clone(), proof.clone());
121
122            let rule_operations = context.operations.clone();
123
124            for op in &rule_operations {
125                if let OperationKind::FactUsed { fact_ref, value } = &op.kind {
126                    used_facts.entry(fact_ref.clone()).or_insert(value.clone());
127                }
128            }
129
130            if !exec_rule.path.segments.is_empty() {
131                continue;
132            }
133
134            let unless_branches: Vec<(Option<Expression>, Expression)> = exec_rule.branches[1..]
135                .iter()
136                .map(|b| (b.condition.clone(), b.result.clone()))
137                .collect();
138
139            response.add_result(RuleResult {
140                rule: EvaluatedRule {
141                    name: exec_rule.name.clone(),
142                    path: exec_rule.path.clone(),
143                    default_expression: exec_rule.branches[0].result.clone(),
144                    unless_branches,
145                    source_location: exec_rule.source.clone(),
146                    rule_type: exec_rule.rule_type.clone(),
147                },
148                result,
149                facts: vec![],
150                operations: rule_operations,
151                proof: Some(proof),
152                rule_type: exec_rule.rule_type.clone(),
153            });
154        }
155
156        // Build fact list in definition order (plan.facts is an IndexMap)
157        let fact_list: Vec<Fact> = plan
158            .facts
159            .keys()
160            .filter_map(|path| {
161                used_facts.remove(path).map(|value| Fact {
162                    path: path.clone(),
163                    value: FactValue::Literal(value),
164                    source: None,
165                })
166            })
167            .collect();
168
169        if !fact_list.is_empty() {
170            response.facts = vec![Facts {
171                fact_path: String::new(),
172                referencing_fact_name: String::new(),
173                facts: fact_list,
174            }];
175        }
176
177        response
178    }
179}
lemma/evaluation/mod.rs

lemma/evaluation/
mod.rs
