Skip to main content

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 conversion_explanation;
8pub mod explanation;
9pub mod expression;
10pub mod operations;
11pub mod request;
12pub mod response;
13
14use crate::computation::units::{convert_unit, UnitResolutionContext};
15use crate::evaluation::explanation::{ExplanationNode, ValueSource};
16use crate::evaluation::operations::VetoType;
17use crate::evaluation::response::EvaluatedRule;
18use crate::planning::execution_plan::validate_value_against_type;
19use crate::planning::semantics::{
20    Data, DataDefinition, DataPath, DataValue, Expression, LemmaType, LiteralValue,
21    ReferenceTarget, RulePath, ValueKind,
22};
23use crate::planning::ExecutionPlan;
24use indexmap::IndexMap;
25pub use operations::{ComputationKind, OperationKind, OperationRecord, OperationResult};
26pub use request::{parse_rule_result_conversion_strings, EvaluationRequest};
27pub use response::{DataGroup, Response, RuleResult};
28use std::collections::{HashMap, HashSet};
29
30pub(crate) const DECIMAL_VALUE_LIMIT_VETO_MESSAGE: &str =
31    "Calculated result exceeds decimal value limit";
32
33fn literal_value_committable_to_decimal_wire(value: &LiteralValue) -> bool {
34    use crate::computation::rational::commit_rational_to_decimal;
35
36    match &value.value {
37        ValueKind::Number(rational)
38        | ValueKind::Ratio(rational, _)
39        | ValueKind::Calendar(rational, _) => commit_rational_to_decimal(rational).is_ok(),
40        ValueKind::Quantity(rational, _, _) => commit_rational_to_decimal(rational).is_ok(),
41        ValueKind::Range(left, right) => {
42            literal_value_committable_to_decimal_wire(left)
43                && literal_value_committable_to_decimal_wire(right)
44        }
45        ValueKind::Text(_) | ValueKind::Date(_) | ValueKind::Time(_) | ValueKind::Boolean(_) => {
46            true
47        }
48    }
49}
50
51fn ensure_rule_result_within_decimal_wire_limit(result: OperationResult) -> OperationResult {
52    match result {
53        OperationResult::Value(value) => {
54            if literal_value_committable_to_decimal_wire(value.as_ref()) {
55                OperationResult::Value(value)
56            } else {
57                OperationResult::Veto(VetoType::computation(DECIMAL_VALUE_LIMIT_VETO_MESSAGE))
58            }
59        }
60        OperationResult::Veto(veto) => OperationResult::Veto(veto),
61    }
62}
63
64/// Evaluation context for storing intermediate results
65pub(crate) struct EvaluationContext {
66    data_values: HashMap<DataPath, LiteralValue>,
67    pub(crate) rule_results: HashMap<RulePath, OperationResult>,
68    rule_explanations: HashMap<RulePath, crate::evaluation::explanation::Explanation>,
69    operations: Option<Vec<crate::evaluation::operations::OperationRecord>>,
70    explanation_nodes: HashMap<usize, crate::evaluation::explanation::ExplanationNode>,
71    now: LiteralValue,
72    /// Map of rule-target reference data paths to their target rule path.
73    /// Used by [`Self::lazy_rule_reference_resolve`] at first read of the
74    /// reference data path: if the target rule produced a `Value`, we copy
75    /// it into `data_values` (memoizing further reads); if it produced a
76    /// `Veto`, we propagate that exact veto reason. The target rule is
77    /// guaranteed to have been evaluated already because planning injected
78    /// a `depends_on_rules` edge from every consumer rule to the target.
79    rule_references: HashMap<DataPath, RulePath>,
80    /// Constraint-violation vetoes on reference data paths discovered at
81    /// run-time. Populated for data-target references when the copied
82    /// value fails validation against the merged `resolved_type`; used by
83    /// the data-path read in [`expression`] so consumers see a precise
84    /// `Computation` veto naming the violated constraint instead of a
85    /// generic missing-data veto.
86    reference_vetoes: HashMap<DataPath, VetoType>,
87    /// Merged `resolved_type` per reference data path, used to validate
88    /// rule-target reference values lazily in
89    /// [`Self::lazy_rule_reference_resolve`].
90    reference_types: HashMap<DataPath, LemmaType>,
91    /// Maps each quantity unit name to its owning `LemmaType` (post-decomp).
92    /// Cloned from [`ExecutionPlan::unit_index`]. Used by the `as <unit>` evaluation path
93    /// to resolve anonymous intermediate quantity values into named typed values.
94    pub(crate) unit_index: HashMap<String, LemmaType>,
95}
96
97impl EvaluationContext {
98    fn new(plan: &ExecutionPlan, now: LiteralValue, record_operations: bool) -> Self {
99        let mut data_values: HashMap<DataPath, LiteralValue> = plan
100            .data
101            .iter()
102            .filter_map(|(path, d)| d.value().map(|v| (path.clone(), v.clone())))
103            .collect();
104
105        let rule_references: HashMap<DataPath, RulePath> =
106            build_transitive_rule_references(&plan.data);
107
108        let reference_types: HashMap<DataPath, LemmaType> = plan
109            .data
110            .iter()
111            .filter_map(|(path, def)| match def {
112                DataDefinition::Reference { resolved_type, .. } => {
113                    Some((path.clone(), resolved_type.clone()))
114                }
115                _ => None,
116            })
117            .collect();
118        let mut reference_vetoes: HashMap<DataPath, VetoType> = HashMap::new();
119
120        // Resolve data-target references: copy the target's value into the
121        // reference path. Must happen in dependency order so reference-of-
122        // reference chains see their target already populated. A reference
123        // whose target value is missing simply stays missing here; any
124        // rule/expression that later reads the reference will produce a
125        // `MissingData` veto, matching the existing missing-data semantics
126        // for type-declaration data with no value.
127        //
128        // A caller-supplied value (via `set_data_values`) replaces the
129        // `DataDefinition::Reference` entry with `DataDefinition::Value`
130        // before evaluation, so any path that is no longer a `Reference` is
131        // skipped here — the user-provided value has already been placed in
132        // `data_values` and wins over the reference copy.
133        //
134        // Rule-target references are intentionally absent from
135        // `reference_evaluation_order` (filtered in planning); they are
136        // resolved lazily at the consumer's read site once the target rule
137        // has been evaluated.
138        for reference_path in &plan.reference_evaluation_order {
139            match plan.data.get(reference_path) {
140                Some(DataDefinition::Reference {
141                    target: ReferenceTarget::Data(target_path),
142                    resolved_type,
143                    local_default,
144                    ..
145                }) => {
146                    let copied_kind: Option<ValueKind> =
147                        data_values.get(target_path).map(|v| v.value.clone());
148                    if let Some(value_kind) = copied_kind {
149                        let value = LiteralValue {
150                            value: value_kind,
151                            lemma_type: resolved_type.clone(),
152                        };
153                        match validate_value_against_type(resolved_type, &value) {
154                            Ok(()) => {
155                                data_values.insert(reference_path.clone(), value);
156                            }
157                            Err(msg) => {
158                                reference_vetoes.insert(
159                                    reference_path.clone(),
160                                    VetoType::computation(format!(
161                                        "Reference '{}' violates declared constraint: {}",
162                                        reference_path, msg
163                                    )),
164                                );
165                            }
166                        }
167                    } else if let Some(dv) = local_default {
168                        let value = LiteralValue {
169                            value: dv.clone(),
170                            lemma_type: resolved_type.clone(),
171                        };
172                        data_values.insert(reference_path.clone(), value);
173                    }
174                }
175                Some(DataDefinition::Reference {
176                    target: ReferenceTarget::Rule(_),
177                    ..
178                }) => {
179                    // Rule-target references are resolved lazily on first
180                    // read. They should never appear in
181                    // `reference_evaluation_order` (planning filters them
182                    // out), but skip defensively.
183                }
184                Some(_) => {
185                    // User-provided value has replaced the reference;
186                    // nothing to copy.
187                }
188                None => unreachable!(
189                    "BUG: reference_evaluation_order references missing data path '{}'",
190                    reference_path
191                ),
192            }
193        }
194
195        let unit_index = plan.unit_index.clone();
196
197        Self {
198            data_values,
199            rule_results: HashMap::new(),
200            rule_explanations: HashMap::new(),
201            operations: if record_operations {
202                Some(Vec::new())
203            } else {
204                None
205            },
206            explanation_nodes: HashMap::new(),
207            now,
208            rule_references,
209            reference_vetoes,
210            reference_types,
211            unit_index,
212        }
213    }
214
215    /// Resolve a rule-target reference data path lazily from the already-
216    /// evaluated target rule's result. Returns:
217    /// - `Some(Ok(value))` — target rule produced a value; memoized into `data_values`.
218    /// - `Some(Err(veto))` — target rule produced a veto, or the rule's
219    ///   value violates the reference's merged `resolved_type` constraints.
220    /// - `None` — the path is not a rule-target reference.
221    pub(crate) fn lazy_rule_reference_resolve(
222        &mut self,
223        data_path: &DataPath,
224    ) -> Option<Result<LiteralValue, crate::evaluation::operations::VetoType>> {
225        let rule_path = self.rule_references.get(data_path)?.clone();
226        let result = self
227            .rule_results
228            .get(&rule_path)
229            .cloned()
230            .unwrap_or_else(|| {
231                unreachable!(
232                    "BUG: rule-target reference '{}' read before target rule '{}' evaluated; \
233                 planning must have injected the dependency edge",
234                    data_path, rule_path
235                );
236            });
237        match result {
238            OperationResult::Value(v) => {
239                let v = *v;
240                let v = match self.reference_types.get(data_path) {
241                    Some(ref_type) => {
242                        let retyped = LiteralValue {
243                            value: v.value,
244                            lemma_type: ref_type.clone(),
245                        };
246                        if let Err(msg) = validate_value_against_type(ref_type, &retyped) {
247                            return Some(Err(VetoType::computation(format!(
248                                "Reference '{}' violates declared constraint: {}",
249                                data_path, msg
250                            ))));
251                        }
252                        retyped
253                    }
254                    None => v,
255                };
256                self.data_values.insert(data_path.clone(), v.clone());
257                Some(Ok(v))
258            }
259            OperationResult::Veto(veto) => Some(Err(veto)),
260        }
261    }
262
263    /// Returns a recorded constraint-violation veto for a reference data
264    /// path, if any. Populated in [`Self::new`] for data-target references
265    /// whose copied value failed `validate_value_against_type`.
266    pub(crate) fn get_reference_veto(&self, data_path: &DataPath) -> Option<&VetoType> {
267        self.reference_vetoes.get(data_path)
268    }
269
270    pub(crate) fn now(&self) -> &LiteralValue {
271        &self.now
272    }
273
274    fn get_data(&self, data_path: &DataPath) -> Option<&LiteralValue> {
275        self.data_values.get(data_path)
276    }
277
278    fn push_operation(&mut self, kind: OperationKind) {
279        if let Some(ref mut ops) = self.operations {
280            ops.push(OperationRecord { kind });
281        }
282    }
283
284    fn set_explanation_node(
285        &mut self,
286        expression: &Expression,
287        node: crate::evaluation::explanation::ExplanationNode,
288    ) {
289        self.explanation_nodes
290            .insert(expression as *const Expression as usize, node);
291    }
292
293    fn get_explanation_node(
294        &self,
295        expression: &Expression,
296    ) -> Option<&crate::evaluation::explanation::ExplanationNode> {
297        self.explanation_nodes
298            .get(&(expression as *const Expression as usize))
299    }
300
301    fn get_rule_explanation(
302        &self,
303        rule_path: &RulePath,
304    ) -> Option<&crate::evaluation::explanation::Explanation> {
305        self.rule_explanations.get(rule_path)
306    }
307
308    fn set_rule_explanation(
309        &mut self,
310        rule_path: RulePath,
311        explanation: crate::evaluation::explanation::Explanation,
312    ) {
313        self.rule_explanations.insert(rule_path, explanation);
314    }
315}
316
317/// For every reference data path in `data`, follow the data-target reference
318/// chain and record the eventual rule-target (if any). Includes direct
319/// rule-target references. A visited set guards against pathological cycles
320/// that planning should already have rejected.
321fn build_transitive_rule_references(
322    data: &IndexMap<DataPath, DataDefinition>,
323) -> HashMap<DataPath, RulePath> {
324    let mut out: HashMap<DataPath, RulePath> = HashMap::new();
325    for (path, def) in data {
326        if !matches!(def, DataDefinition::Reference { .. }) {
327            continue;
328        }
329        let mut visited: HashSet<DataPath> = HashSet::new();
330        let mut cursor: DataPath = path.clone();
331        loop {
332            if !visited.insert(cursor.clone()) {
333                break;
334            }
335            let Some(DataDefinition::Reference { target, .. }) = data.get(&cursor) else {
336                break;
337            };
338            match target {
339                ReferenceTarget::Data(next) => cursor = next.clone(),
340                ReferenceTarget::Rule(rule_path) => {
341                    out.insert(path.clone(), rule_path.clone());
342                    break;
343                }
344            }
345        }
346    }
347    out
348}
349
350fn collect_used_data_from_explanation(
351    node: &ExplanationNode,
352    out: &mut HashMap<DataPath, LiteralValue>,
353) {
354    match node {
355        ExplanationNode::Value {
356            value,
357            source: ValueSource::Data { data_ref },
358            ..
359        } => {
360            out.entry(data_ref.clone()).or_insert_with(|| value.clone());
361        }
362        ExplanationNode::Value { .. } => {}
363        ExplanationNode::RuleReference { expansion, .. } => {
364            collect_used_data_from_explanation(expansion.as_ref(), out);
365        }
366        ExplanationNode::Computation { operands, .. } => {
367            for op in operands {
368                collect_used_data_from_explanation(op, out);
369            }
370        }
371        ExplanationNode::Branches {
372            matched,
373            non_matched,
374            ..
375        } => {
376            if let Some(ref cond) = matched.condition {
377                collect_used_data_from_explanation(cond, out);
378            }
379            collect_used_data_from_explanation(&matched.result, out);
380            for nm in non_matched {
381                collect_used_data_from_explanation(&nm.condition, out);
382                if let Some(ref res) = nm.result {
383                    collect_used_data_from_explanation(res, out);
384                }
385            }
386        }
387        ExplanationNode::Condition { operands, .. } => {
388            for op in operands {
389                collect_used_data_from_explanation(op, out);
390            }
391        }
392        ExplanationNode::Veto { .. } => {}
393    }
394}
395
396#[cfg(test)]
397mod runtime_invariant_tests {
398    use super::*;
399    use crate::parsing::ast::DateTimeValue;
400    use crate::Engine;
401
402    /// At evaluation time the LiteralValue stored under a reference data path
403    /// must carry the reference's own `resolved_type`, not the (possibly looser)
404    /// type embedded in the target's LiteralValue. The merge pass folds in the
405    /// LHS-declared constraints (e.g. a binding's parent-spec type chain) so
406    /// the reference's `resolved_type` is the contract the evaluator promises;
407    /// any consumer that reads `data_values[ref].lemma_type` directly must see
408    /// that contract, not the target's loose shape.
409    #[test]
410    fn reference_runtime_value_carries_resolved_type_not_target_type() {
411        let code = r#"
412spec inner
413data slot: number -> minimum 0 -> maximum 100
414
415spec source_spec
416data v: number -> default 5
417
418spec outer
419uses i: inner
420uses src: source_spec
421fill i.slot: src.v
422rule r: i.slot
423"#;
424        let mut engine = Engine::new();
425        engine
426            .load(
427                code,
428                crate::SourceType::Path(std::sync::Arc::new(std::path::PathBuf::from(
429                    "ref_invariant.lemma",
430                ))),
431            )
432            .expect("must load");
433
434        let now = DateTimeValue::now();
435        let plan_basis = engine
436            .get_plan(None, "outer", Some(&now))
437            .expect("must plan")
438            .clone();
439
440        let reference_path = plan_basis
441            .data
442            .iter()
443            .find_map(|(path, def)| match def {
444                DataDefinition::Reference { .. } => Some(path.clone()),
445                _ => None,
446            })
447            .expect("plan must contain the reference for `i.slot`");
448
449        let resolved_type = match plan_basis.data.get(&reference_path).expect("entry exists") {
450            DataDefinition::Reference { resolved_type, .. } => resolved_type.clone(),
451            _ => unreachable!("filter above kept only Reference entries"),
452        };
453
454        let plan = plan_basis.with_defaults();
455
456        let now_lit = LiteralValue {
457            value: crate::planning::semantics::ValueKind::Date(
458                crate::planning::semantics::date_time_to_semantic(&now),
459            ),
460            lemma_type: crate::planning::semantics::primitive_date().clone(),
461        };
462        let context = EvaluationContext::new(&plan, now_lit, false);
463
464        let stored = context
465            .data_values
466            .get(&reference_path)
467            .expect("EvaluationContext must populate reference path with the copied value");
468
469        assert_eq!(
470            stored.lemma_type, resolved_type,
471            "stored LiteralValue must carry the reference's resolved_type \
472             (LHS-merged), not the target's loose type. \
473             stored = {:?}, resolved = {:?}",
474            stored.lemma_type, resolved_type
475        );
476    }
477}
478
479/// Evaluates Lemma rules within their spec context
480#[derive(Default)]
481pub(crate) struct Evaluator;
482
483impl Evaluator {
484    /// Evaluate an execution plan.
485    ///
486    /// Executes rules in pre-computed dependency order with all data pre-loaded.
487    /// Rules are already flattened into executable branches with data prefixes resolved.
488    ///
489    /// After planning, evaluation completes without `Error`: numeric rules return
490    /// `Value` (stored `Decimal` semantics) or `Veto` for impossible data (e.g. division
491    /// by zero). Panics indicate engine bugs, not user-facing failures.
492    ///
493    /// When `record_operations` is true, each rule's evaluation records a trace of
494    /// operations (data used, rules used, computations, branch evaluations) into
495    /// `RuleResult::operations`. When false, no trace is recorded.
496    pub(crate) fn evaluate(
497        &self,
498        plan: &ExecutionPlan,
499        now: LiteralValue,
500        record_operations: bool,
501        request: &request::EvaluationRequest,
502    ) -> Response {
503        let mut context = EvaluationContext::new(plan, now, record_operations);
504
505        let mut response = Response {
506            spec_name: plan.spec_name.clone(),
507            spec_hash: None,
508            spec_effective_from: None,
509            spec_effective_to: None,
510            data: Vec::new(),
511            results: IndexMap::new(),
512        };
513
514        // Execute each rule in topological order (already sorted by ExecutionPlan)
515        for exec_rule in &plan.rules {
516            if let Some(ref mut ops) = context.operations {
517                ops.clear();
518            }
519            context.explanation_nodes.clear();
520
521            let (mut result, mut explanation) = expression::evaluate_rule(exec_rule, &mut context);
522
523            context
524                .rule_results
525                .insert(exec_rule.path.clone(), result.clone());
526            context.set_rule_explanation(exec_rule.path.clone(), explanation.clone());
527
528            if let Some(target) = request.rule_result_units.get(&exec_rule.name) {
529                if let OperationResult::Value(value) = &result {
530                    let converted = convert_unit(
531                        value.as_ref(),
532                        target,
533                        UnitResolutionContext::WithIndex(&context.unit_index),
534                    );
535                    match converted {
536                        OperationResult::Veto(_) => {
537                            unreachable!(
538                                "BUG: rule '{}' unit conversion to '{}' vetoed after request validation",
539                                exec_rule.name, target
540                            );
541                        }
542                        OperationResult::Value(_) => {
543                            result = converted.clone();
544                            explanation.result = converted;
545                        }
546                    }
547                }
548            }
549
550            let rule_operations = context.operations.clone().unwrap_or_default();
551
552            if !exec_rule.path.segments.is_empty() {
553                continue;
554            }
555
556            result = ensure_rule_result_within_decimal_wire_limit(result);
557            if matches!(result, OperationResult::Veto(_)) {
558                explanation = crate::evaluation::explanation::Explanation {
559                    rule_path: exec_rule.path.clone(),
560                    source: Some(exec_rule.source.clone()),
561                    result: result.clone(),
562                    tree: explanation.tree,
563                };
564            }
565
566            let unless_branches: Vec<(Option<Expression>, Expression)> = exec_rule.branches[1..]
567                .iter()
568                .map(|b| (b.condition.clone(), b.result.clone()))
569                .collect();
570
571            response.add_result(RuleResult {
572                rule: EvaluatedRule {
573                    name: exec_rule.name.clone(),
574                    path: exec_rule.path.clone(),
575                    default_expression: exec_rule.branches[0].result.clone(),
576                    unless_branches,
577                    source_location: exec_rule.source.clone(),
578                    rule_type: exec_rule.rule_type.clone(),
579                },
580                result,
581                data: vec![],
582                operations: rule_operations,
583                explanation: Some(explanation),
584                rule_type: exec_rule.rule_type.clone(),
585            });
586        }
587
588        let mut used_data: HashMap<DataPath, LiteralValue> = HashMap::new();
589        for rule_result in response.results.values() {
590            if let Some(ref explanation) = rule_result.explanation {
591                collect_used_data_from_explanation(explanation.tree.as_ref(), &mut used_data);
592            }
593        }
594
595        // Build data list in definition order (plan.data is an IndexMap)
596        let data_list: Vec<Data> = plan
597            .data
598            .keys()
599            .filter_map(|path| {
600                used_data.remove(path).map(|value| Data {
601                    path: path.clone(),
602                    value: DataValue::from_bound_literal(value),
603                    source: None,
604                })
605            })
606            .collect();
607
608        if !data_list.is_empty() {
609            response.data = vec![DataGroup {
610                data_path: String::new(),
611                referencing_data_name: String::new(),
612                data: data_list,
613            }];
614        }
615
616        response
617    }
618}