Skip to main content

lemma/planning/
mod.rs

1//! Planning module for Lemma specs
2//!
3//! This module performs complete static analysis and builds execution plans:
4//! - Builds Graph with facts and rules (validated, with types computed)
5//! - Builds ExecutionPlan from Graph (topologically sorted, ready for evaluation)
6//! - Validates spec structure and references
7//!
8//! Contract model:
9//! - Interface contract: facts (inputs) + rules (outputs), including full type constraints.
10//!   Cross-spec bindings must satisfy this contract at planning time.
11//! - Behavior lock: plan hash pins full execution semantics (fingerprint), not only IO shape.
12
13pub mod execution_plan;
14pub mod fingerprint;
15pub mod graph;
16pub mod semantics;
17pub mod slice_interface;
18pub mod temporal;
19pub mod types;
20pub mod validation;
21use crate::engine::Context;
22use crate::parsing::ast::{DateTimeValue, FactValue as ParsedFactValue, LemmaSpec, TypeDef};
23use crate::Error;
24pub use execution_plan::{Branch, ExecutableRule, ExecutionPlan, SpecId, SpecSchema};
25pub use semantics::{
26    is_same_spec, negated_comparison, ArithmeticComputation, ComparisonComputation, Expression,
27    ExpressionKind, Fact, FactData, FactPath, FactValue, LemmaType, LiteralValue,
28    LogicalComputation, MathematicalComputation, NegationType, PathSegment, RulePath, Source, Span,
29    TypeDefiningSpec, TypeExtends, ValueKind, VetoExpression,
30};
31use std::collections::{BTreeMap, BTreeSet, HashMap, VecDeque};
32use std::sync::Arc;
33
34/// Slice-keyed registry of plan hashes built during the planning loop.
35/// Filled incrementally as specs are planned in topological order.
36#[derive(Debug, Default, Clone)]
37pub struct PlanHashRegistry {
38    by_slice: BTreeMap<(String, Option<DateTimeValue>), String>,
39    by_pin: BTreeMap<(String, String), Arc<LemmaSpec>>,
40}
41
42impl PlanHashRegistry {
43    pub(crate) fn insert(
44        &mut self,
45        spec: &Arc<LemmaSpec>,
46        slice_from: Option<DateTimeValue>,
47        hash: String,
48    ) {
49        let hash_lower = hash.trim().to_ascii_lowercase();
50        self.by_slice
51            .insert((spec.name.clone(), slice_from), hash_lower.clone());
52        self.by_pin
53            .insert((spec.name.clone(), hash_lower), Arc::clone(spec));
54    }
55
56    /// Lookup plan hash for a dependency at a given slice start.
57    pub(crate) fn get_by_slice(
58        &self,
59        spec_name: &str,
60        slice_from: &Option<DateTimeValue>,
61    ) -> Option<&str> {
62        self.by_slice
63            .get(&(spec_name.to_string(), slice_from.clone()))
64            .map(|s| s.as_str())
65    }
66
67    /// Lookup spec arc by (name, hash) for pin resolution.
68    pub(crate) fn get_by_pin(&self, spec_name: &str, hash: &str) -> Option<&Arc<LemmaSpec>> {
69        let key = (spec_name.to_string(), hash.trim().to_ascii_lowercase());
70        self.by_pin.get(&key)
71    }
72}
73
74#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
75struct SpecName(String);
76
77impl SpecName {
78    fn new(name: impl Into<String>) -> Self {
79        Self(name.into())
80    }
81}
82
83impl std::fmt::Display for SpecName {
84    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
85        write!(f, "{}", self.0)
86    }
87}
88
89fn collect_spec_dependencies(
90    spec: &LemmaSpec,
91    known_names: &BTreeSet<SpecName>,
92) -> BTreeSet<SpecName> {
93    let mut deps = BTreeSet::new();
94    let current = SpecName::new(spec.name.clone());
95
96    for fact in &spec.facts {
97        match &fact.value {
98            ParsedFactValue::SpecReference(r) => {
99                let dep = SpecName::new(r.name.clone());
100                if dep != current && known_names.contains(&dep) {
101                    deps.insert(dep);
102                }
103            }
104            ParsedFactValue::TypeDeclaration {
105                from: Some(from_ref),
106                ..
107            } => {
108                let dep = SpecName::new(from_ref.name.clone());
109                if dep != current && known_names.contains(&dep) {
110                    deps.insert(dep);
111                }
112            }
113            _ => {}
114        }
115    }
116
117    for type_def in &spec.types {
118        if let TypeDef::Import { from, .. } = type_def {
119            let dep = SpecName::new(from.name.clone());
120            if dep != current && known_names.contains(&dep) {
121                deps.insert(dep);
122            }
123        }
124    }
125
126    deps
127}
128
129/// Order specs so dependencies (referenced specs / type-import sources) are planned first.
130/// Needed for `spec dep~hash` resolution: hashes are recorded as each spec's plans are built.
131pub(crate) fn order_specs_for_planning_graph(
132    specs: Vec<Arc<LemmaSpec>>,
133) -> Result<Vec<Arc<LemmaSpec>>, Vec<Error>> {
134    let all_names: BTreeSet<SpecName> = specs
135        .iter()
136        .map(|s| SpecName::new(s.name.clone()))
137        .collect();
138
139    let mut deps_by_name: BTreeMap<SpecName, BTreeSet<SpecName>> = BTreeMap::new();
140    for name in &all_names {
141        deps_by_name.insert(name.clone(), BTreeSet::new());
142    }
143    for spec in &specs {
144        let deps = collect_spec_dependencies(spec, &all_names);
145        deps_by_name.insert(SpecName::new(spec.name.clone()), deps);
146    }
147
148    // Kahn: in_degree[name] = number of prerequisites for that name.
149    let mut in_degree: BTreeMap<SpecName, usize> = BTreeMap::new();
150    for (name, deps) in &deps_by_name {
151        in_degree.insert(name.clone(), deps.len());
152    }
153
154    // Reverse edges: dependency -> dependents
155    let mut dependents: BTreeMap<SpecName, BTreeSet<SpecName>> = BTreeMap::new();
156    for name in &all_names {
157        dependents.insert(name.clone(), BTreeSet::new());
158    }
159    for (name, deps) in &deps_by_name {
160        for dep in deps {
161            if let Some(children) = dependents.get_mut(dep) {
162                children.insert(name.clone());
163            }
164        }
165    }
166
167    let mut queue: VecDeque<SpecName> = VecDeque::new();
168    for (name, degree) in &in_degree {
169        if *degree == 0 {
170            queue.push_back(name.clone());
171        }
172    }
173
174    let mut ordered_names: Vec<SpecName> = Vec::new();
175    while let Some(name) = queue.pop_front() {
176        ordered_names.push(name.clone());
177        if let Some(children) = dependents.get(&name) {
178            for child in children {
179                if let Some(degree) = in_degree.get_mut(child) {
180                    *degree -= 1;
181                    if *degree == 0 {
182                        queue.push_back(child.clone());
183                    }
184                }
185            }
186        }
187    }
188
189    if ordered_names.len() != all_names.len() {
190        let mut cycle_nodes: Vec<SpecName> = in_degree
191            .iter()
192            .filter_map(|(name, degree)| {
193                if *degree > 0 {
194                    Some(name.clone())
195                } else {
196                    None
197                }
198            })
199            .collect();
200        cycle_nodes.sort();
201        let cycle_path = if cycle_nodes.len() > 1 {
202            let mut path = cycle_nodes.clone();
203            path.push(cycle_nodes[0].clone());
204            path.iter()
205                .map(std::string::ToString::to_string)
206                .collect::<Vec<_>>()
207                .join(" -> ")
208        } else {
209            cycle_nodes
210                .iter()
211                .map(std::string::ToString::to_string)
212                .collect::<Vec<_>>()
213                .join(" -> ")
214        };
215        return Err(vec![Error::validation(
216            format!("Spec dependency cycle: {}", cycle_path),
217            None,
218            None::<String>,
219        )]);
220    }
221
222    let mut by_name: HashMap<SpecName, Vec<Arc<LemmaSpec>>> = HashMap::new();
223    for s in specs {
224        by_name
225            .entry(SpecName::new(s.name.clone()))
226            .or_default()
227            .push(s);
228    }
229    for v in by_name.values_mut() {
230        v.sort_by(|a, b| a.effective_from().cmp(&b.effective_from()));
231    }
232
233    let mut out = Vec::new();
234    for name in ordered_names {
235        if let Some(mut vec) = by_name.remove(&name) {
236            out.append(&mut vec);
237        }
238    }
239    Ok(out)
240}
241
242/// Result of planning a single spec: the spec, its execution plans (if any), and errors produced while planning it.
243#[derive(Debug, Clone)]
244pub struct SpecPlanningResult {
245    /// The spec we were planning (the one this result is for).
246    pub spec: Arc<LemmaSpec>,
247    /// Execution plans for that spec (one per temporal interval; empty if planning failed).
248    pub plans: Vec<ExecutionPlan>,
249    /// All planning errors produced while planning this spec.
250    pub errors: Vec<Error>,
251}
252
253/// Result of running plan() across the context: per-spec results and global errors (e.g. temporal coverage).
254#[derive(Debug, Clone)]
255pub struct PlanningResult {
256    /// One result per spec we attempted to plan.
257    pub per_spec: Vec<SpecPlanningResult>,
258    /// Errors not tied to a single spec (e.g. from validate_temporal_coverage).
259    pub global_errors: Vec<Error>,
260    /// Slice- and pin-keyed registry of plan hashes for request-level spec resolution.
261    pub plan_hash_registry: PlanHashRegistry,
262}
263
264/// Build execution plans for one or more Lemma specs.
265///
266/// Context is immutable — types are resolved per (spec, slice) inside Graph::build
267/// and never stored in Context. The flow:
268/// 1. Per-spec, per-slice: Graph::build registers + resolves types using Context + resolve_at
269/// 2. ExecutionPlan is built from the graph (types baked into facts/rules)
270///
271/// Returns a PlanningResult: per-spec results (spec, plans, errors) and global errors.
272/// When displaying errors, iterate per_spec and for each with non-empty errors output "In spec 'X':" then each error.
273pub fn plan(context: &Context, sources: HashMap<String, String>) -> PlanningResult {
274    let mut global_errors: Vec<Error> = Vec::new();
275    global_errors.extend(temporal::validate_temporal_coverage(context));
276
277    let all_specs: Vec<_> = match order_specs_for_planning_graph(context.iter().collect()) {
278        Ok(specs) => specs,
279        Err(mut cycle_errors) => {
280            global_errors.append(&mut cycle_errors);
281            return PlanningResult {
282                per_spec: Vec::new(),
283                global_errors,
284                plan_hash_registry: PlanHashRegistry::default(),
285            };
286        }
287    };
288
289    let mut per_spec: Vec<SpecPlanningResult> = Vec::new();
290    let mut plan_hashes = PlanHashRegistry::default();
291
292    for spec_arc in &all_specs {
293        let slices = temporal::compute_temporal_slices(spec_arc, context);
294        let mut spec_plans: Vec<ExecutionPlan> = Vec::new();
295        let mut spec_errors: Vec<Error> = Vec::new();
296        let mut slice_resolved_types: Vec<HashMap<Arc<LemmaSpec>, types::ResolvedSpecTypes>> =
297            Vec::new();
298
299        for slice in &slices {
300            match graph::Graph::build(
301                spec_arc,
302                context,
303                sources.clone(),
304                slice.from.clone(),
305                &plan_hashes,
306            ) {
307                Ok((graph, slice_types)) => {
308                    let execution_plan = execution_plan::build_execution_plan(
309                        &graph,
310                        &slice_types,
311                        slice.from.clone(),
312                        slice.to.clone(),
313                    );
314                    let value_errors =
315                        execution_plan::validate_literal_facts_against_types(&execution_plan);
316                    if value_errors.is_empty() {
317                        let hash = execution_plan.plan_hash();
318                        plan_hashes.insert(spec_arc, slice.from.clone(), hash);
319                        spec_plans.push(execution_plan);
320                    } else {
321                        spec_errors.extend(value_errors);
322                    }
323                    slice_resolved_types.push(slice_types);
324                }
325                Err(build_errors) => {
326                    spec_errors.extend(build_errors);
327                }
328            }
329        }
330
331        if spec_errors.is_empty() && spec_plans.len() > 1 {
332            spec_errors.extend(slice_interface::validate_slice_interfaces(
333                spec_arc,
334                &spec_plans,
335                &slice_resolved_types,
336            ));
337        }
338
339        per_spec.push(SpecPlanningResult {
340            spec: Arc::clone(spec_arc),
341            plans: spec_plans,
342            errors: spec_errors,
343        });
344    }
345
346    PlanningResult {
347        per_spec,
348        global_errors,
349        plan_hash_registry: plan_hashes,
350    }
351}
352
353// ============================================================================
354// Tests
355// ============================================================================
356
357#[cfg(test)]
358mod internal_tests {
359    use super::{order_specs_for_planning_graph, plan};
360    use crate::engine::Context;
361    use crate::parsing::ast::{FactValue, LemmaFact, LemmaSpec, ParentType, Reference, Span};
362    use crate::parsing::source::Source;
363    use crate::planning::execution_plan::ExecutionPlan;
364    use crate::planning::semantics::{FactPath, PathSegment, TypeDefiningSpec, TypeExtends};
365    use crate::{parse, Error, ResourceLimits};
366    use std::collections::HashMap;
367    use std::sync::Arc;
368
369    /// Test helper: plan a single spec and return its execution plan.
370    fn plan_single(
371        main_spec: &LemmaSpec,
372        all_specs: &[LemmaSpec],
373        sources: HashMap<String, String>,
374    ) -> Result<ExecutionPlan, Vec<Error>> {
375        let mut ctx = Context::new();
376        for spec in all_specs {
377            if let Err(e) = ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry) {
378                return Err(vec![e]);
379            }
380        }
381        let main_spec_arc = ctx
382            .get_spec_effective_from(main_spec.name.as_str(), main_spec.effective_from())
383            .expect("main_spec must be in all_specs");
384        let result = plan(&ctx, sources);
385        let all_errors: Vec<Error> = result
386            .global_errors
387            .into_iter()
388            .chain(
389                result
390                    .per_spec
391                    .iter()
392                    .flat_map(|r| r.errors.clone())
393                    .collect::<Vec<_>>(),
394            )
395            .collect();
396        if !all_errors.is_empty() {
397            return Err(all_errors);
398        }
399        match result
400            .per_spec
401            .into_iter()
402            .find(|r| Arc::ptr_eq(&r.spec, &main_spec_arc))
403        {
404            Some(spec_result) if !spec_result.plans.is_empty() => {
405                let mut plans = spec_result.plans;
406                Ok(plans.remove(0))
407            }
408            _ => Err(vec![Error::validation(
409                format!("No execution plan produced for spec '{}'", main_spec.name),
410                Some(crate::planning::semantics::Source::new(
411                    "<test>",
412                    crate::planning::semantics::Span {
413                        start: 0,
414                        end: 0,
415                        line: 1,
416                        col: 0,
417                    },
418                )),
419                None::<String>,
420            )]),
421        }
422    }
423
424    #[test]
425    fn test_basic_validation() {
426        let input = r#"spec person
427fact name: "John"
428fact age: 25
429rule is_adult: age >= 18"#;
430
431        let specs = parse(input, "test.lemma", &ResourceLimits::default())
432            .unwrap()
433            .specs;
434
435        let mut sources = HashMap::new();
436        sources.insert("test.lemma".to_string(), input.to_string());
437
438        for spec in &specs {
439            let result = plan_single(spec, &specs, sources.clone());
440            assert!(
441                result.is_ok(),
442                "Basic validation should pass: {:?}",
443                result.err()
444            );
445        }
446    }
447
448    #[test]
449    fn test_duplicate_facts() {
450        let input = r#"spec person
451fact name: "John"
452fact name: "Jane""#;
453
454        let specs = parse(input, "test.lemma", &ResourceLimits::default())
455            .unwrap()
456            .specs;
457
458        let mut sources = HashMap::new();
459        sources.insert("test.lemma".to_string(), input.to_string());
460
461        let result = plan_single(&specs[0], &specs, sources);
462
463        assert!(
464            result.is_err(),
465            "Duplicate facts should cause validation error"
466        );
467        let errors = result.unwrap_err();
468        let error_string = errors
469            .iter()
470            .map(|e| e.to_string())
471            .collect::<Vec<_>>()
472            .join(", ");
473        assert!(
474            error_string.contains("Duplicate fact"),
475            "Error should mention duplicate fact: {}",
476            error_string
477        );
478        assert!(error_string.contains("name"));
479    }
480
481    #[test]
482    fn test_duplicate_rules() {
483        let input = r#"spec person
484fact age: 25
485rule is_adult: age >= 18
486rule is_adult: age >= 21"#;
487
488        let specs = parse(input, "test.lemma", &ResourceLimits::default())
489            .unwrap()
490            .specs;
491
492        let mut sources = HashMap::new();
493        sources.insert("test.lemma".to_string(), input.to_string());
494
495        let result = plan_single(&specs[0], &specs, sources);
496
497        assert!(
498            result.is_err(),
499            "Duplicate rules should cause validation error"
500        );
501        let errors = result.unwrap_err();
502        let error_string = errors
503            .iter()
504            .map(|e| e.to_string())
505            .collect::<Vec<_>>()
506            .join(", ");
507        assert!(
508            error_string.contains("Duplicate rule"),
509            "Error should mention duplicate rule: {}",
510            error_string
511        );
512        assert!(error_string.contains("is_adult"));
513    }
514
515    #[test]
516    fn test_circular_dependency() {
517        let input = r#"spec test
518rule a: b
519rule b: a"#;
520
521        let specs = parse(input, "test.lemma", &ResourceLimits::default())
522            .unwrap()
523            .specs;
524
525        let mut sources = HashMap::new();
526        sources.insert("test.lemma".to_string(), input.to_string());
527
528        let result = plan_single(&specs[0], &specs, sources);
529
530        assert!(
531            result.is_err(),
532            "Circular dependency should cause validation error"
533        );
534        let errors = result.unwrap_err();
535        let error_string = errors
536            .iter()
537            .map(|e| e.to_string())
538            .collect::<Vec<_>>()
539            .join(", ");
540        assert!(error_string.contains("Circular dependency") || error_string.contains("circular"));
541    }
542
543    #[test]
544    fn test_unified_references_work() {
545        let input = r#"spec test
546fact age: 25
547rule is_adult: age >= 18
548rule test1: age
549rule test2: is_adult"#;
550
551        let specs = parse(input, "test.lemma", &ResourceLimits::default())
552            .unwrap()
553            .specs;
554
555        let mut sources = HashMap::new();
556        sources.insert("test.lemma".to_string(), input.to_string());
557
558        let result = plan_single(&specs[0], &specs, sources);
559
560        assert!(
561            result.is_ok(),
562            "Unified references should work: {:?}",
563            result.err()
564        );
565    }
566
567    #[test]
568    fn test_multiple_specs() {
569        let input = r#"spec person
570fact name: "John"
571fact age: 25
572
573spec company
574fact name: "Acme Corp"
575fact employee: spec person"#;
576
577        let specs = parse(input, "test.lemma", &ResourceLimits::default())
578            .unwrap()
579            .specs;
580
581        let mut sources = HashMap::new();
582        sources.insert("test.lemma".to_string(), input.to_string());
583
584        let result = plan_single(&specs[0], &specs, sources);
585
586        assert!(
587            result.is_ok(),
588            "Multiple specs should validate successfully: {:?}",
589            result.err()
590        );
591    }
592
593    #[test]
594    fn test_invalid_spec_reference() {
595        let input = r#"spec person
596fact name: "John"
597fact contract: spec nonexistent"#;
598
599        let specs = parse(input, "test.lemma", &ResourceLimits::default())
600            .unwrap()
601            .specs;
602
603        let mut sources = HashMap::new();
604        sources.insert("test.lemma".to_string(), input.to_string());
605
606        let result = plan_single(&specs[0], &specs, sources);
607
608        assert!(
609            result.is_err(),
610            "Invalid spec reference should cause validation error"
611        );
612        let errors = result.unwrap_err();
613        let error_string = errors
614            .iter()
615            .map(|e| e.to_string())
616            .collect::<Vec<_>>()
617            .join(", ");
618        assert!(
619            error_string.contains("not found")
620                || error_string.contains("Spec")
621                || (error_string.contains("nonexistent") && error_string.contains("depends")),
622            "Error should mention spec reference issue: {}",
623            error_string
624        );
625        assert!(error_string.contains("nonexistent"));
626    }
627
628    #[test]
629    fn test_type_declaration_empty_base_returns_lemma_error() {
630        let mut spec = LemmaSpec::new("test".to_string());
631        let source = Source::new(
632            "test.lemma",
633            Span {
634                start: 0,
635                end: 10,
636                line: 1,
637                col: 0,
638            },
639        );
640        spec.facts.push(LemmaFact::new(
641            Reference {
642                segments: vec![],
643                name: "x".to_string(),
644            },
645            FactValue::TypeDeclaration {
646                base: ParentType::Custom {
647                    name: String::new(),
648                },
649                constraints: None,
650                from: None,
651            },
652            source,
653        ));
654
655        let specs = vec![spec.clone()];
656        let mut sources = HashMap::new();
657        sources.insert(
658            "test.lemma".to_string(),
659            "spec test\nfact x: []".to_string(),
660        );
661
662        let result = plan_single(&spec, &specs, sources);
663        assert!(
664            result.is_err(),
665            "TypeDeclaration with empty base should fail planning"
666        );
667        let errors = result.unwrap_err();
668        let combined = errors
669            .iter()
670            .map(|e| e.to_string())
671            .collect::<Vec<_>>()
672            .join("\n");
673        assert!(
674            combined.contains("TypeDeclaration base cannot be empty"),
675            "Error should mention empty base; got: {}",
676            combined
677        );
678    }
679
680    #[test]
681    fn test_fact_binding_with_custom_type_resolves_in_correct_spec_context() {
682        // This is a planning-level test: ensure fact bindings resolve custom types correctly
683        // when the type is defined in a different spec than the binding.
684        //
685        // spec one:
686        //   type money: number
687        //   fact x: [money]
688        // spec two:
689        //   fact one: spec one
690        //   fact one.x: 7
691        //   rule getx: one.x
692        let code = r#"
693spec one
694type money: number
695fact x: [money]
696
697spec two
698fact one: spec one
699fact one.x: 7
700rule getx: one.x
701"#;
702
703        let specs = parse(code, "test.lemma", &ResourceLimits::default())
704            .unwrap()
705            .specs;
706        let spec_two = specs.iter().find(|d| d.name == "two").unwrap();
707
708        let mut sources = HashMap::new();
709        sources.insert("test.lemma".to_string(), code.to_string());
710        let execution_plan =
711            plan_single(spec_two, &specs, sources).expect("planning should succeed");
712
713        // Verify that one.x has type 'money' (resolved from spec one)
714        let one_x_path = FactPath {
715            segments: vec![PathSegment {
716                fact: "one".to_string(),
717                spec: "one".to_string(),
718            }],
719            fact: "x".to_string(),
720        };
721
722        let one_x_type = execution_plan
723            .facts
724            .get(&one_x_path)
725            .and_then(|d| d.schema_type())
726            .expect("one.x should have a resolved type");
727
728        assert_eq!(
729            one_x_type.name(),
730            "money",
731            "one.x should have type 'money', got: {}",
732            one_x_type.name()
733        );
734        assert!(one_x_type.is_number(), "money should be number-based");
735    }
736
737    #[test]
738    fn test_fact_type_declaration_from_spec_has_import_defining_spec() {
739        let code = r#"
740spec examples
741type money: scale
742  -> unit eur 1.00
743
744spec checkout
745type money: scale
746  -> unit eur 1.00
747fact local_price: [money]
748fact imported_price: [money from examples]
749"#;
750
751        let specs = parse(code, "test.lemma", &ResourceLimits::default())
752            .unwrap()
753            .specs;
754
755        let mut ctx = Context::new();
756        for spec in &specs {
757            ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry)
758                .expect("insert spec");
759        }
760
761        let examples_arc = ctx
762            .get_spec_effective_from("examples", None)
763            .expect("examples spec should be present");
764        let checkout_arc = ctx
765            .get_spec_effective_from("checkout", None)
766            .expect("checkout spec should be present");
767
768        let mut sources = HashMap::new();
769        sources.insert("test.lemma".to_string(), code.to_string());
770
771        let result = plan(&ctx, sources);
772        assert!(
773            result.global_errors.is_empty(),
774            "No global errors expected, got: {:?}",
775            result.global_errors
776        );
777
778        let checkout_result = result
779            .per_spec
780            .iter()
781            .find(|r| Arc::ptr_eq(&r.spec, &checkout_arc))
782            .expect("checkout result should exist");
783        assert!(
784            checkout_result.errors.is_empty(),
785            "No checkout planning errors expected, got: {:?}",
786            checkout_result.errors
787        );
788        assert!(
789            !checkout_result.plans.is_empty(),
790            "checkout should produce at least one plan"
791        );
792        let execution_plan = &checkout_result.plans[0];
793
794        let local_type = execution_plan
795            .facts
796            .get(&FactPath::new(vec![], "local_price".to_string()))
797            .and_then(|d| d.schema_type())
798            .expect("local_price should have schema type");
799        let imported_type = execution_plan
800            .facts
801            .get(&FactPath::new(vec![], "imported_price".to_string()))
802            .and_then(|d| d.schema_type())
803            .expect("imported_price should have schema type");
804
805        match &local_type.extends {
806            TypeExtends::Custom {
807                defining_spec: TypeDefiningSpec::Local,
808                ..
809            } => {}
810            other => panic!(
811                "local_price should resolve as local defining_spec, got {:?}",
812                other
813            ),
814        }
815
816        match &imported_type.extends {
817            TypeExtends::Custom {
818                defining_spec: TypeDefiningSpec::Import { spec, .. },
819                ..
820            } => {
821                assert!(
822                    Arc::ptr_eq(spec, &examples_arc),
823                    "imported_price should point to resolved 'examples' spec arc"
824                );
825            }
826            other => panic!(
827                "imported_price should resolve as import defining_spec, got {:?}",
828                other
829            ),
830        }
831    }
832
833    #[test]
834    fn test_plan_with_registry_style_spec_names() {
835        let source = r#"spec @user/workspace/somespec
836fact quantity: 10
837
838spec user/workspace/example
839fact inventory: spec @user/workspace/somespec
840rule total_quantity: inventory.quantity"#;
841
842        let specs = parse(source, "registry_bundle.lemma", &ResourceLimits::default())
843            .unwrap()
844            .specs;
845        assert_eq!(specs.len(), 2);
846
847        let example_spec = specs
848            .iter()
849            .find(|d| d.name == "user/workspace/example")
850            .expect("should find user/workspace/example");
851
852        let mut sources = HashMap::new();
853        sources.insert("registry_bundle.lemma".to_string(), source.to_string());
854
855        let result = plan_single(example_spec, &specs, sources);
856        assert!(
857            result.is_ok(),
858            "Planning with @... spec names should succeed: {:?}",
859            result.err()
860        );
861    }
862
863    #[test]
864    fn test_multiple_independent_errors_are_all_reported() {
865        // A spec referencing a non-existing type import AND a non-existing
866        // spec should report errors for BOTH, not just stop at the first.
867        let source = r#"spec demo
868type money from nonexistent_type_source
869fact helper: spec nonexistent_spec
870fact price: 10
871rule total: helper.value + price"#;
872
873        let specs = parse(source, "test.lemma", &ResourceLimits::default())
874            .unwrap()
875            .specs;
876
877        let mut sources = HashMap::new();
878        sources.insert("test.lemma".to_string(), source.to_string());
879
880        let result = plan_single(&specs[0], &specs, sources);
881        assert!(result.is_err(), "Planning should fail with multiple errors");
882
883        let errors = result.unwrap_err();
884        let all_messages: Vec<String> = errors.iter().map(|e| e.to_string()).collect();
885        let combined = all_messages.join("\n");
886
887        assert!(
888            combined.contains("nonexistent_type_source"),
889            "Should report type import error for 'nonexistent_type_source'. Got:\n{}",
890            combined
891        );
892
893        // Must also report the spec reference error (not just the type error)
894        assert!(
895            combined.contains("nonexistent_spec"),
896            "Should report spec reference error for 'nonexistent_spec'. Got:\n{}",
897            combined
898        );
899
900        // Should have at least 2 distinct kinds of errors (type + spec ref)
901        assert!(
902            errors.len() >= 2,
903            "Expected at least 2 errors, got {}: {}",
904            errors.len(),
905            combined
906        );
907    }
908
909    #[test]
910    fn test_type_error_does_not_suppress_cross_spec_fact_error() {
911        // When a type import fails, errors about cross-spec fact references
912        // (e.g. ext.some_fact where ext is a spec ref to a non-existing spec)
913        // must still be reported.
914        let source = r#"spec demo
915type currency from missing_spec
916fact ext: spec also_missing
917rule val: ext.some_fact"#;
918
919        let specs = parse(source, "test.lemma", &ResourceLimits::default())
920            .unwrap()
921            .specs;
922
923        let mut sources = HashMap::new();
924        sources.insert("test.lemma".to_string(), source.to_string());
925
926        let result = plan_single(&specs[0], &specs, sources);
927        assert!(result.is_err());
928
929        let errors = result.unwrap_err();
930        let combined: String = errors
931            .iter()
932            .map(|e| e.to_string())
933            .collect::<Vec<_>>()
934            .join("\n");
935
936        assert!(
937            combined.contains("missing_spec"),
938            "Should report type import error about 'missing_spec'. Got:\n{}",
939            combined
940        );
941
942        // The spec reference error about 'also_missing' should ALSO be reported
943        assert!(
944            combined.contains("also_missing"),
945            "Should report error about 'also_missing'. Got:\n{}",
946            combined
947        );
948    }
949
950    #[test]
951    fn test_spec_order_includes_fact_type_declaration_from_edges() {
952        let source = r#"spec dep
953type money: number
954fact x: [money]
955
956spec consumer
957fact imported_amount: [money from dep]
958rule passthrough: imported_amount"#;
959        let specs = parse(source, "test.lemma", &ResourceLimits::default())
960            .unwrap()
961            .specs;
962
963        let mut ctx = Context::new();
964        for spec in &specs {
965            ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry)
966                .expect("insert spec");
967        }
968
969        let ordered = order_specs_for_planning_graph(ctx.iter().collect())
970            .expect("spec order should succeed");
971        let ordered_names: Vec<String> = ordered.iter().map(|s| s.name.clone()).collect();
972        let dep_idx = ordered_names
973            .iter()
974            .position(|n| n == "dep")
975            .expect("dep must exist");
976        let consumer_idx = ordered_names
977            .iter()
978            .position(|n| n == "consumer")
979            .expect("consumer must exist");
980        assert!(
981            dep_idx < consumer_idx,
982            "dependency must be planned before dependent. order={:?}",
983            ordered_names
984        );
985    }
986
987    #[test]
988    fn test_spec_dependency_cycle_returns_global_error_and_aborts() {
989        let source = r#"spec a
990fact dep_b: spec b
991
992spec b
993fact imported_value: [amount from a]
994"#;
995        let specs = parse(source, "test.lemma", &ResourceLimits::default())
996            .unwrap()
997            .specs;
998
999        let mut ctx = Context::new();
1000        for spec in &specs {
1001            ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry)
1002                .expect("insert spec");
1003        }
1004
1005        let result = plan(&ctx, HashMap::new());
1006        assert!(
1007            result
1008                .global_errors
1009                .iter()
1010                .any(|e| e.to_string().contains("Spec dependency cycle")),
1011            "expected global cycle error, got {:?}",
1012            result
1013                .global_errors
1014                .iter()
1015                .map(|e| e.to_string())
1016                .collect::<Vec<_>>()
1017        );
1018        assert!(
1019            result.per_spec.is_empty(),
1020            "planning should abort before per-spec planning when cycle exists"
1021        );
1022    }
1023
1024    // ========================================================================
1025    // Dependency tracking
1026    // ========================================================================
1027
1028    #[test]
1029    fn dependencies_populated_for_cross_spec_rule_reference() {
1030        let code = r#"
1031spec dep
1032fact x: 10
1033rule val: x
1034
1035spec consumer
1036fact d: spec dep
1037fact d.x: 5
1038rule result: d.val
1039"#;
1040        let specs = parse(code, "test.lemma", &ResourceLimits::default())
1041            .unwrap()
1042            .specs;
1043        let consumer = specs.iter().find(|s| s.name == "consumer").unwrap();
1044
1045        let mut sources = HashMap::new();
1046        sources.insert("test.lemma".to_string(), code.to_string());
1047
1048        let plan = plan_single(consumer, &specs, sources).expect("planning should succeed");
1049
1050        assert_eq!(
1051            plan.dependencies.len(),
1052            1,
1053            "consumer should depend on exactly one spec, got: {:?}",
1054            plan.dependencies
1055        );
1056        let dep_id = plan.dependencies.iter().next().unwrap();
1057        assert_eq!(dep_id.name, "dep");
1058        assert!(
1059            !dep_id.plan_hash.is_empty(),
1060            "dependency plan hash must be non-empty"
1061        );
1062    }
1063
1064    #[test]
1065    fn dependencies_empty_for_standalone_spec() {
1066        let code = r#"
1067spec standalone
1068fact age: 25
1069rule is_adult: age >= 18
1070"#;
1071        let specs = parse(code, "test.lemma", &ResourceLimits::default())
1072            .unwrap()
1073            .specs;
1074
1075        let mut sources = HashMap::new();
1076        sources.insert("test.lemma".to_string(), code.to_string());
1077
1078        let plan = plan_single(&specs[0], &specs, sources).expect("planning should succeed");
1079
1080        assert!(
1081            plan.dependencies.is_empty(),
1082            "standalone spec should have no dependencies, got: {:?}",
1083            plan.dependencies
1084        );
1085    }
1086
1087    #[test]
1088    fn dependencies_contain_multiple_cross_spec_refs() {
1089        let code = r#"
1090spec rates
1091fact base_rate: 0.05
1092rule rate: base_rate
1093
1094spec config
1095fact threshold: 100
1096rule limit: threshold
1097
1098spec calculator
1099fact r: spec rates
1100fact r.base_rate: 0.03
1101fact c: spec config
1102fact c.threshold: 200
1103rule combined: r.rate + c.limit
1104"#;
1105        let specs = parse(code, "test.lemma", &ResourceLimits::default())
1106            .unwrap()
1107            .specs;
1108        let calc = specs.iter().find(|s| s.name == "calculator").unwrap();
1109
1110        let mut sources = HashMap::new();
1111        sources.insert("test.lemma".to_string(), code.to_string());
1112
1113        let plan = plan_single(calc, &specs, sources).expect("planning should succeed");
1114
1115        assert_eq!(
1116            plan.dependencies.len(),
1117            2,
1118            "calculator should depend on two specs, got: {:?}",
1119            plan.dependencies
1120        );
1121        let dep_names: Vec<&str> = plan.dependencies.iter().map(|d| d.name.as_str()).collect();
1122        assert!(dep_names.contains(&"rates"), "should depend on rates");
1123        assert!(dep_names.contains(&"config"), "should depend on config");
1124    }
1125
1126    #[test]
1127    fn dependency_plan_hash_matches_dep_spec_plan_hash() {
1128        let code = r#"
1129spec dep
1130fact x: 42
1131rule val: x
1132
1133spec consumer
1134fact d: spec dep
1135rule result: d.val
1136"#;
1137        let specs = parse(code, "test.lemma", &ResourceLimits::default())
1138            .unwrap()
1139            .specs;
1140
1141        let mut sources = HashMap::new();
1142        sources.insert("test.lemma".to_string(), code.to_string());
1143
1144        let mut ctx = Context::new();
1145        for spec in &specs {
1146            ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry)
1147                .expect("insert spec");
1148        }
1149        let result = plan(&ctx, sources);
1150        assert!(result.global_errors.is_empty());
1151
1152        let dep_plan = result
1153            .per_spec
1154            .iter()
1155            .find(|r| r.spec.name == "dep")
1156            .expect("dep result")
1157            .plans
1158            .first()
1159            .expect("dep must have a plan");
1160
1161        let consumer_plan = result
1162            .per_spec
1163            .iter()
1164            .find(|r| r.spec.name == "consumer")
1165            .expect("consumer result")
1166            .plans
1167            .first()
1168            .expect("consumer must have a plan");
1169
1170        let recorded_hash = &consumer_plan
1171            .dependencies
1172            .iter()
1173            .find(|d| d.name == "dep")
1174            .expect("consumer should depend on dep")
1175            .plan_hash;
1176
1177        assert_eq!(
1178            recorded_hash,
1179            &dep_plan.plan_hash(),
1180            "dependency hash must match the dep's actual computed plan hash"
1181        );
1182    }
1183
1184    #[test]
1185    fn spec_ref_without_rules_excluded_from_dependencies() {
1186        let code = r#"
1187spec dep
1188fact x: 10
1189
1190spec consumer
1191fact d: spec dep
1192fact local: 99
1193rule result: local
1194"#;
1195        let specs = parse(code, "test.lemma", &ResourceLimits::default())
1196            .unwrap()
1197            .specs;
1198        let consumer = specs.iter().find(|s| s.name == "consumer").unwrap();
1199
1200        let mut sources = HashMap::new();
1201        sources.insert("test.lemma".to_string(), code.to_string());
1202
1203        let plan = plan_single(consumer, &specs, sources).expect("planning should succeed");
1204
1205        assert!(
1206            plan.dependencies.is_empty(),
1207            "spec ref whose facts are not used by any rule should not appear in dependencies, got: {:?}",
1208            plan.dependencies
1209        );
1210    }
1211
1212    #[test]
1213    fn spec_ref_with_rules_always_creates_dependency() {
1214        // Even if the consumer's own rules don't reference dep rules,
1215        // the dep's rules are part of the execution plan and need dep's facts.
1216        let code = r#"
1217spec dep
1218fact x: 10
1219rule val: x
1220
1221spec consumer
1222fact d: spec dep
1223fact local: 99
1224rule result: local
1225"#;
1226        let specs = parse(code, "test.lemma", &ResourceLimits::default())
1227            .unwrap()
1228            .specs;
1229        let consumer = specs.iter().find(|s| s.name == "consumer").unwrap();
1230
1231        let mut sources = HashMap::new();
1232        sources.insert("test.lemma".to_string(), code.to_string());
1233
1234        let plan = plan_single(consumer, &specs, sources).expect("planning should succeed");
1235
1236        assert_eq!(
1237            plan.dependencies.len(),
1238            1,
1239            "dep's rules are in the plan, so dep must be a dependency, got: {:?}",
1240            plan.dependencies
1241        );
1242        assert_eq!(plan.dependencies.iter().next().unwrap().name, "dep");
1243    }
1244}