1pub 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#[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 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 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
129pub(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 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 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#[derive(Debug, Clone)]
244pub struct SpecPlanningResult {
245 pub spec: Arc<LemmaSpec>,
247 pub plans: Vec<ExecutionPlan>,
249 pub errors: Vec<Error>,
251}
252
253#[derive(Debug, Clone)]
255pub struct PlanningResult {
256 pub per_spec: Vec<SpecPlanningResult>,
258 pub global_errors: Vec<Error>,
260 pub plan_hash_registry: PlanHashRegistry,
262}
263
264pub 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#[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 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 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 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 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 assert!(
895 combined.contains("nonexistent_spec"),
896 "Should report spec reference error for 'nonexistent_spec'. Got:\n{}",
897 combined
898 );
899
900 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 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 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 #[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 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}