1pub mod discovery;
13pub mod execution_plan;
14pub mod graph;
15pub mod semantics;
16pub mod spec_set;
17use crate::engine::Context;
18use crate::parsing::ast::DateTimeValue;
19use crate::Error;
20pub use execution_plan::ExecutionPlanSet;
21pub use execution_plan::{Branch, ExecutableRule, ExecutionPlan, SpecSchema};
22pub use semantics::{
23 is_same_spec, negated_comparison, ArithmeticComputation, ComparisonComputation, Data,
24 DataDefinition, DataPath, DataValue, Expression, ExpressionKind, LemmaType, LiteralValue,
25 LogicalComputation, MathematicalComputation, NegationType, PathSegment, RulePath, Source, Span,
26 TypeDefiningSpec, TypeExtends, ValueKind, VetoExpression,
27};
28pub use spec_set::LemmaSpecSet;
29use std::collections::BTreeMap;
30
31#[derive(Debug, Clone)]
33pub struct SpecPlanningResult {
34 pub spec: std::sync::Arc<crate::parsing::ast::LemmaSpec>,
35 pub plans: Vec<ExecutionPlan>,
36 pub errors: Vec<Error>,
37}
38
39#[derive(Debug, Clone)]
41pub struct SpecSetPlanningResult {
42 pub name: String,
44 pub lemma_spec_set: LemmaSpecSet,
45 pub specs: Vec<SpecPlanningResult>,
46}
47
48impl SpecSetPlanningResult {
49 pub fn errors(&self) -> impl Iterator<Item = &Error> {
50 self.specs.iter().flat_map(|s| s.errors.iter())
51 }
52
53 pub fn execution_plan_set(&self) -> ExecutionPlanSet {
54 ExecutionPlanSet {
55 spec_name: self.name.clone(),
56 plans: self.specs.iter().flat_map(|s| s.plans.clone()).collect(),
57 }
58 }
59
60 pub fn schema_over(
65 &self,
66 from: &Option<DateTimeValue>,
67 to: &Option<DateTimeValue>,
68 ) -> Option<SpecSchema> {
69 let schemas: Vec<SpecSchema> = self
70 .specs
71 .iter()
72 .filter(|sr| {
73 let (slice_from, slice_to) = self.lemma_spec_set.effective_range(&sr.spec);
74 ranges_overlap(from, to, &slice_from, &slice_to)
75 })
76 .filter_map(|sr| sr.plans.first().map(|p| p.interface_schema()))
77 .collect();
78
79 let first = schemas.first()?;
80 for pair in schemas.windows(2) {
81 if !pair[0].is_type_compatible(&pair[1]) {
82 return None;
83 }
84 }
85 Some(first.clone())
86 }
87}
88
89pub(crate) fn ranges_overlap(
92 a_from: &Option<DateTimeValue>,
93 a_to: &Option<DateTimeValue>,
94 b_from: &Option<DateTimeValue>,
95 b_to: &Option<DateTimeValue>,
96) -> bool {
97 let a_before_b_end = match (a_from, b_to) {
98 (_, None) => true,
99 (None, Some(_)) => true,
100 (Some(a), Some(b)) => a < b,
101 };
102 let b_before_a_end = match (b_from, a_to) {
103 (_, None) => true,
104 (None, Some(_)) => true,
105 (Some(b), Some(a)) => b < a,
106 };
107 a_before_b_end && b_before_a_end
108}
109
110#[derive(Debug, Clone)]
111pub struct PlanningResult {
112 pub results: Vec<SpecSetPlanningResult>,
113}
114
115pub fn plan(context: &Context) -> PlanningResult {
120 let mut results: BTreeMap<String, SpecSetPlanningResult> = BTreeMap::new();
121
122 for spec in context.iter() {
123 let spec_name = &spec.name;
124 let lemma_spec_set = context
125 .spec_sets()
126 .get(spec_name)
127 .expect("spec not found in context");
128
129 let mut spec_result = SpecPlanningResult {
130 spec: std::sync::Arc::clone(&spec),
131 plans: Vec::new(),
132 errors: Vec::new(),
133 };
134
135 for effective in lemma_spec_set.effective_dates(&spec, context) {
136 let dag = match discovery::build_dag_for_spec(context, &spec, &effective) {
137 Ok(dag) => dag,
138 Err(discovery::DagError::Cycle(errors)) => {
139 spec_result.errors.extend(errors);
140 continue;
141 }
142 Err(discovery::DagError::Other(errors)) => {
143 spec_result.errors.extend(errors);
144 continue;
145 }
146 };
147
148 match graph::Graph::build(context, &spec, &dag, &effective) {
149 Ok((graph, slice_types)) => {
150 let execution_plan =
151 execution_plan::build_execution_plan(&graph, &slice_types, &effective);
152 let value_errors =
153 execution_plan::validate_literal_data_against_types(&execution_plan);
154 spec_result.errors.extend(value_errors);
155 spec_result.plans.push(execution_plan);
156 }
157 Err(build_errors) => {
158 spec_result.errors.extend(build_errors);
159 }
160 }
161 }
162
163 if !spec_result.plans.is_empty() || !spec_result.errors.is_empty() {
164 let entry = results
165 .entry(spec_name.clone())
166 .or_insert_with(|| SpecSetPlanningResult {
167 name: spec_name.clone(),
168 lemma_spec_set: lemma_spec_set.clone(),
169 specs: Vec::new(),
170 });
171 entry.specs.push(spec_result);
172 }
173 }
174
175 for (spec_name, err) in discovery::validate_dependency_interfaces(context, &results) {
176 let set_result = results
177 .get_mut(&spec_name)
178 .expect("BUG: validate_dependency_interfaces returned error for absent spec set");
179 let first_spec = set_result
180 .specs
181 .first_mut()
182 .expect("BUG: spec set has no specs to attach error to");
183 first_spec.errors.push(err);
184 }
185
186 PlanningResult {
187 results: results.into_values().collect(),
188 }
189}
190
191#[cfg(test)]
196mod internal_tests {
197 use super::plan;
198 use crate::engine::Context;
199 use crate::parsing::ast::{DataValue, LemmaData, LemmaSpec, ParentType, Reference, Span};
200 use crate::parsing::source::Source;
201 use crate::planning::execution_plan::ExecutionPlan;
202 use crate::planning::semantics::{DataPath, PathSegment, TypeDefiningSpec, TypeExtends};
203 use crate::{parse, Error, ResourceLimits};
204 use std::collections::HashMap;
205 use std::sync::Arc;
206
207 fn plan_single(
209 main_spec: &LemmaSpec,
210 all_specs: &[LemmaSpec],
211 ) -> Result<ExecutionPlan, Vec<Error>> {
212 let mut ctx = Context::new();
213 for spec in all_specs {
214 if let Err(e) = ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry) {
215 return Err(vec![e]);
216 }
217 }
218 let main_spec_arc = ctx
219 .spec_sets()
220 .get(main_spec.name.as_str())
221 .and_then(|ss| ss.get_exact(main_spec.effective_from()).cloned())
222 .expect("main_spec must be in all_specs");
223 let result = plan(&ctx);
224 let all_errors: Vec<Error> = result
225 .results
226 .iter()
227 .flat_map(|r| r.errors().cloned())
228 .collect();
229 if !all_errors.is_empty() {
230 return Err(all_errors);
231 }
232 match result
233 .results
234 .into_iter()
235 .find(|r| r.name == main_spec_arc.name)
236 {
237 Some(spec_result) => {
238 let plan_set = spec_result.execution_plan_set();
239 if plan_set.plans.is_empty() {
240 Err(vec![Error::validation(
241 format!("No execution plan produced for spec '{}'", main_spec.name),
242 Some(crate::planning::semantics::Source::new(
243 "<test>",
244 crate::planning::semantics::Span {
245 start: 0,
246 end: 0,
247 line: 1,
248 col: 0,
249 },
250 )),
251 None::<String>,
252 )])
253 } else {
254 let mut plans = plan_set.plans;
255 Ok(plans.remove(0))
256 }
257 }
258 None => Err(vec![Error::validation(
259 format!("No execution plan produced for spec '{}'", main_spec.name),
260 Some(crate::planning::semantics::Source::new(
261 "<test>",
262 crate::planning::semantics::Span {
263 start: 0,
264 end: 0,
265 line: 1,
266 col: 0,
267 },
268 )),
269 None::<String>,
270 )]),
271 }
272 }
273
274 #[test]
275 fn test_basic_validation() {
276 let input = r#"spec person
277data name: "John"
278data age: 25
279rule is_adult: age >= 18"#;
280
281 let specs = parse(input, "test.lemma", &ResourceLimits::default())
282 .unwrap()
283 .specs;
284
285 let mut sources = HashMap::new();
286 sources.insert("test.lemma".to_string(), input.to_string());
287
288 for spec in &specs {
289 let result = plan_single(spec, &specs);
290 assert!(
291 result.is_ok(),
292 "Basic validation should pass: {:?}",
293 result.err()
294 );
295 }
296 }
297
298 #[test]
299 fn test_duplicate_data() {
300 let input = r#"spec person
301data name: "John"
302data name: "Jane""#;
303
304 let specs = parse(input, "test.lemma", &ResourceLimits::default())
305 .unwrap()
306 .specs;
307
308 let mut sources = HashMap::new();
309 sources.insert("test.lemma".to_string(), input.to_string());
310
311 let result = plan_single(&specs[0], &specs);
312
313 assert!(
314 result.is_err(),
315 "Duplicate data should cause validation error"
316 );
317 let errors = result.unwrap_err();
318 let error_string = errors
319 .iter()
320 .map(|e| e.to_string())
321 .collect::<Vec<_>>()
322 .join(", ");
323 assert!(
324 error_string.contains("Duplicate data"),
325 "Error should mention duplicate data: {}",
326 error_string
327 );
328 assert!(error_string.contains("name"));
329 }
330
331 #[test]
332 fn test_duplicate_rules() {
333 let input = r#"spec person
334data age: 25
335rule is_adult: age >= 18
336rule is_adult: age >= 21"#;
337
338 let specs = parse(input, "test.lemma", &ResourceLimits::default())
339 .unwrap()
340 .specs;
341
342 let mut sources = HashMap::new();
343 sources.insert("test.lemma".to_string(), input.to_string());
344
345 let result = plan_single(&specs[0], &specs);
346
347 assert!(
348 result.is_err(),
349 "Duplicate rules should cause validation error"
350 );
351 let errors = result.unwrap_err();
352 let error_string = errors
353 .iter()
354 .map(|e| e.to_string())
355 .collect::<Vec<_>>()
356 .join(", ");
357 assert!(
358 error_string.contains("Duplicate rule"),
359 "Error should mention duplicate rule: {}",
360 error_string
361 );
362 assert!(error_string.contains("is_adult"));
363 }
364
365 #[test]
366 fn test_circular_dependency() {
367 let input = r#"spec test
368rule a: b
369rule b: a"#;
370
371 let specs = parse(input, "test.lemma", &ResourceLimits::default())
372 .unwrap()
373 .specs;
374
375 let mut sources = HashMap::new();
376 sources.insert("test.lemma".to_string(), input.to_string());
377
378 let result = plan_single(&specs[0], &specs);
379
380 assert!(
381 result.is_err(),
382 "Circular dependency should cause validation error"
383 );
384 let errors = result.unwrap_err();
385 let error_string = errors
386 .iter()
387 .map(|e| e.to_string())
388 .collect::<Vec<_>>()
389 .join(", ");
390 assert!(error_string.contains("Circular dependency") || error_string.contains("circular"));
391 }
392
393 #[test]
394 fn test_multiple_specs() {
395 let input = r#"spec person
396data name: "John"
397data age: 25
398
399spec company
400data name: "Acme Corp"
401with employee: person"#;
402
403 let specs = parse(input, "test.lemma", &ResourceLimits::default())
404 .unwrap()
405 .specs;
406
407 let mut sources = HashMap::new();
408 sources.insert("test.lemma".to_string(), input.to_string());
409
410 let result = plan_single(&specs[0], &specs);
411
412 assert!(
413 result.is_ok(),
414 "Multiple specs should validate successfully: {:?}",
415 result.err()
416 );
417 }
418
419 #[test]
420 fn test_invalid_spec_reference() {
421 let input = r#"spec person
422data name: "John"
423with contract: nonexistent"#;
424
425 let specs = parse(input, "test.lemma", &ResourceLimits::default())
426 .unwrap()
427 .specs;
428
429 let mut sources = HashMap::new();
430 sources.insert("test.lemma".to_string(), input.to_string());
431
432 let result = plan_single(&specs[0], &specs);
433
434 assert!(
435 result.is_err(),
436 "Invalid spec reference should cause validation error"
437 );
438 let errors = result.unwrap_err();
439 let error_string = errors
440 .iter()
441 .map(|e| e.to_string())
442 .collect::<Vec<_>>()
443 .join(", ");
444 assert!(
445 error_string.contains("not found")
446 || error_string.contains("Spec")
447 || (error_string.contains("nonexistent") && error_string.contains("depends")),
448 "Error should mention spec reference issue: {}",
449 error_string
450 );
451 assert!(error_string.contains("nonexistent"));
452 }
453
454 #[test]
455 fn test_type_declaration_empty_base_returns_lemma_error() {
456 let mut spec = LemmaSpec::new("test".to_string());
457 let source = Source::new(
458 "test.lemma",
459 Span {
460 start: 0,
461 end: 10,
462 line: 1,
463 col: 0,
464 },
465 );
466 spec.data.push(LemmaData::new(
467 Reference {
468 segments: vec![],
469 name: "x".to_string(),
470 },
471 DataValue::TypeDeclaration {
472 base: ParentType::Custom {
473 name: String::new(),
474 },
475 constraints: None,
476 from: None,
477 },
478 source,
479 ));
480
481 let specs = vec![spec.clone()];
482 let mut sources = HashMap::new();
483 sources.insert("test.lemma".to_string(), "spec test\ndata x:".to_string());
484
485 let result = plan_single(&spec, &specs);
486 assert!(
487 result.is_err(),
488 "TypeDeclaration with empty base should fail planning"
489 );
490 let errors = result.unwrap_err();
491 let combined = errors
492 .iter()
493 .map(|e| e.to_string())
494 .collect::<Vec<_>>()
495 .join("\n");
496 assert!(
497 combined.contains("Unknown type: ''"),
498 "Error should mention empty/unknown type; got: {}",
499 combined
500 );
501 }
502
503 #[test]
504 fn test_data_binding_with_custom_type_resolves_in_correct_spec_context() {
505 let code = r#"
516spec one
517data money: number
518data x: money
519
520spec two
521with one
522data one.x: 7
523rule getx: one.x
524"#;
525
526 let specs = parse(code, "test.lemma", &ResourceLimits::default())
527 .unwrap()
528 .specs;
529 let spec_two = specs.iter().find(|d| d.name == "two").unwrap();
530
531 let mut sources = HashMap::new();
532 sources.insert("test.lemma".to_string(), code.to_string());
533 let execution_plan = plan_single(spec_two, &specs).expect("planning should succeed");
534
535 let one_x_path = DataPath {
537 segments: vec![PathSegment {
538 data: "one".to_string(),
539 spec: "one".to_string(),
540 }],
541 data: "x".to_string(),
542 };
543
544 let one_x_type = execution_plan
545 .data
546 .get(&one_x_path)
547 .and_then(|d| d.schema_type())
548 .expect("one.x should have a resolved type");
549
550 assert_eq!(
551 one_x_type.name(),
552 "money",
553 "one.x should have type 'money', got: {}",
554 one_x_type.name()
555 );
556 assert!(one_x_type.is_number(), "money should be number-based");
557 }
558
559 #[test]
560 fn test_data_type_declaration_from_spec_has_import_defining_spec() {
561 let code = r#"
562spec examples
563data money: scale
564 -> unit eur 1.00
565
566spec checkout
567data money: scale
568 -> unit eur 1.00
569data local_price: money
570data imported_price: money from examples
571"#;
572
573 let specs = parse(code, "test.lemma", &ResourceLimits::default())
574 .unwrap()
575 .specs;
576
577 let mut ctx = Context::new();
578 for spec in &specs {
579 ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry)
580 .expect("insert spec");
581 }
582
583 let examples_arc = ctx
584 .spec_sets()
585 .get("examples")
586 .and_then(|ss| ss.get_exact(None).cloned())
587 .expect("examples spec should be present");
588 let checkout_arc = ctx
589 .spec_sets()
590 .get("checkout")
591 .and_then(|ss| ss.get_exact(None).cloned())
592 .expect("checkout spec should be present");
593
594 let mut sources = HashMap::new();
595 sources.insert("test.lemma".to_string(), code.to_string());
596
597 let result = plan(&ctx);
598
599 let checkout_result = result
600 .results
601 .iter()
602 .find(|r| r.name == checkout_arc.name)
603 .expect("checkout result should exist");
604 let checkout_errors: Vec<_> = checkout_result.errors().collect();
605 assert!(
606 checkout_errors.is_empty(),
607 "No checkout planning errors expected, got: {:?}",
608 checkout_errors
609 );
610 let checkout_plans = checkout_result.execution_plan_set();
611 assert!(
612 !checkout_plans.plans.is_empty(),
613 "checkout should produce at least one plan"
614 );
615 let execution_plan = &checkout_plans.plans[0];
616
617 let local_type = execution_plan
618 .data
619 .get(&DataPath::new(vec![], "local_price".to_string()))
620 .and_then(|d| d.schema_type())
621 .expect("local_price should have schema type");
622 let imported_type = execution_plan
623 .data
624 .get(&DataPath::new(vec![], "imported_price".to_string()))
625 .and_then(|d| d.schema_type())
626 .expect("imported_price should have schema type");
627
628 match &local_type.extends {
629 TypeExtends::Custom {
630 defining_spec: TypeDefiningSpec::Local,
631 ..
632 } => {}
633 other => panic!(
634 "local_price should resolve as local defining_spec, got {:?}",
635 other
636 ),
637 }
638
639 match &imported_type.extends {
640 TypeExtends::Custom {
641 defining_spec: TypeDefiningSpec::Import { spec, .. },
642 ..
643 } => {
644 assert!(
645 Arc::ptr_eq(spec, &examples_arc),
646 "imported_price should point to resolved 'examples' spec arc"
647 );
648 }
649 other => panic!(
650 "imported_price should resolve as import defining_spec, got {:?}",
651 other
652 ),
653 }
654 }
655
656 #[test]
657 fn test_plan_with_registry_style_spec_names() {
658 let source = r#"spec @user/workspace/somespec
659data quantity: 10
660
661spec user/workspace/example
662with inventory: @user/workspace/somespec
663rule total_quantity: inventory.quantity"#;
664
665 let specs = parse(source, "registry_bundle.lemma", &ResourceLimits::default())
666 .unwrap()
667 .specs;
668 assert_eq!(specs.len(), 2);
669
670 let example_spec = specs
671 .iter()
672 .find(|d| d.name == "user/workspace/example")
673 .expect("should find user/workspace/example");
674
675 let mut sources = HashMap::new();
676 sources.insert("registry_bundle.lemma".to_string(), source.to_string());
677
678 let result = plan_single(example_spec, &specs);
679 assert!(
680 result.is_ok(),
681 "Planning with @... spec names should succeed: {:?}",
682 result.err()
683 );
684 }
685
686 #[test]
687 fn test_multiple_independent_errors_are_all_reported() {
688 let source = r#"spec demo
691data money from nonexistent_type_source
692with helper: nonexistent_spec
693data price: 10
694rule total: helper.value + price"#;
695
696 let specs = parse(source, "test.lemma", &ResourceLimits::default())
697 .unwrap()
698 .specs;
699
700 let mut sources = HashMap::new();
701 sources.insert("test.lemma".to_string(), source.to_string());
702
703 let result = plan_single(&specs[0], &specs);
704 assert!(result.is_err(), "Planning should fail with multiple errors");
705
706 let errors = result.unwrap_err();
707 let all_messages: Vec<String> = errors.iter().map(|e| e.to_string()).collect();
708 let combined = all_messages.join("\n");
709
710 assert!(
711 combined.contains("nonexistent_type_source"),
712 "Should report type import error for 'nonexistent_type_source'. Got:\n{}",
713 combined
714 );
715
716 assert!(
718 combined.contains("nonexistent_spec"),
719 "Should report spec reference error for 'nonexistent_spec'. Got:\n{}",
720 combined
721 );
722
723 assert!(
725 errors.len() >= 2,
726 "Expected at least 2 errors, got {}: {}",
727 errors.len(),
728 combined
729 );
730
731 let type_import_err = errors
732 .iter()
733 .find(|e| e.to_string().contains("nonexistent_type_source"))
734 .expect("type import error");
735 let loc = type_import_err
736 .location()
737 .expect("type import error should carry source location");
738 assert_eq!(loc.attribute, "test.lemma");
739 assert_ne!(
740 (loc.span.start, loc.span.end),
741 (0, 0),
742 "type import error span should not be empty"
743 );
744 }
745
746 #[test]
747 fn test_type_error_does_not_suppress_cross_spec_data_error() {
748 let source = r#"spec demo
752data currency from missing_spec
753with ext: also_missing
754rule val: ext.some_data"#;
755
756 let specs = parse(source, "test.lemma", &ResourceLimits::default())
757 .unwrap()
758 .specs;
759
760 let mut sources = HashMap::new();
761 sources.insert("test.lemma".to_string(), source.to_string());
762
763 let result = plan_single(&specs[0], &specs);
764 assert!(result.is_err());
765
766 let errors = result.unwrap_err();
767 let combined: String = errors
768 .iter()
769 .map(|e| e.to_string())
770 .collect::<Vec<_>>()
771 .join("\n");
772
773 assert!(
774 combined.contains("missing_spec"),
775 "Should report type import error about 'missing_spec'. Got:\n{}",
776 combined
777 );
778
779 assert!(
781 combined.contains("also_missing"),
782 "Should report error about 'also_missing'. Got:\n{}",
783 combined
784 );
785 }
786
787 #[test]
788 fn test_spec_dag_orders_dep_before_consumer() {
789 let source = r#"spec dep 2025-01-01
790data money: number
791data x: money
792
793spec consumer 2025-01-01
794data imported_amount: money from dep
795rule passthrough: imported_amount"#;
796 let specs = parse(source, "test.lemma", &ResourceLimits::default())
797 .unwrap()
798 .specs;
799
800 let mut ctx = Context::new();
801 for spec in &specs {
802 ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry)
803 .expect("insert spec");
804 }
805
806 let dt = crate::DateTimeValue {
807 year: 2025,
808 month: 1,
809 day: 1,
810 hour: 0,
811 minute: 0,
812 second: 0,
813 microsecond: 0,
814 timezone: None,
815 };
816 let effective = crate::parsing::ast::EffectiveDate::DateTimeValue(dt);
817 let consumer_arc = ctx
818 .spec_sets()
819 .get("consumer")
820 .and_then(|ss| ss.spec_at(&effective))
821 .expect("consumer spec");
822 let dag = super::discovery::build_dag_for_spec(&ctx, &consumer_arc, &effective)
823 .expect("DAG should succeed");
824 let ordered_names: Vec<String> = dag.iter().map(|s| s.name.clone()).collect();
825 let dep_idx = ordered_names
826 .iter()
827 .position(|n| n == "dep")
828 .expect("dep must exist");
829 let consumer_idx = ordered_names
830 .iter()
831 .position(|n| n == "consumer")
832 .expect("consumer must exist");
833 assert!(
834 dep_idx < consumer_idx,
835 "dependency must be planned before dependent. order={:?}",
836 ordered_names
837 );
838 }
839
840 #[test]
841 fn test_spec_dependency_cycle_surfaces_as_spec_error_and_populates_results() {
842 let source = r#"spec a 2025-01-01
843with dep_b: b
844
845spec b 2025-01-01
846data imported_value: amount from a
847"#;
848 let specs = parse(source, "test.lemma", &ResourceLimits::default())
849 .unwrap()
850 .specs;
851
852 let mut ctx = Context::new();
853 for spec in &specs {
854 ctx.insert_spec(Arc::new(spec.clone()), spec.from_registry)
855 .expect("insert spec");
856 }
857
858 let result = plan(&ctx);
859
860 let spec_errors: Vec<String> = result
861 .results
862 .iter()
863 .flat_map(|r| r.errors())
864 .map(|e| e.to_string())
865 .collect();
866 assert!(
867 spec_errors
868 .iter()
869 .any(|e| e.contains("Spec dependency cycle")),
870 "expected cycle error on spec, got: {spec_errors:?}",
871 );
872
873 assert!(
874 result.results.iter().any(|r| r.name == "b"),
875 "cyclic spec 'b' must still have an entry in results so downstream invariants hold"
876 );
877 }
878
879 fn has_source_for(plan: &super::execution_plan::ExecutionPlan, name: &str) -> bool {
884 plan.sources.keys().any(|(n, _)| n == name)
885 }
886
887 #[test]
888 fn sources_contain_main_and_dep_for_cross_spec_rule_reference() {
889 let code = r#"
890spec dep
891data x: 10
892rule val: x
893
894spec consumer
895with d: dep
896data d.x: 5
897rule result: d.val
898"#;
899 let specs = parse(code, "test.lemma", &ResourceLimits::default())
900 .unwrap()
901 .specs;
902 let consumer = specs.iter().find(|s| s.name == "consumer").unwrap();
903
904 let mut sources = HashMap::new();
905 sources.insert("test.lemma".to_string(), code.to_string());
906
907 let plan = plan_single(consumer, &specs).expect("planning should succeed");
908
909 assert_eq!(plan.sources.len(), 2, "main + dep, got: {:?}", plan.sources);
910 assert!(
911 has_source_for(&plan, "consumer"),
912 "sources must include main spec"
913 );
914 assert!(
915 has_source_for(&plan, "dep"),
916 "sources must include dep spec"
917 );
918 }
919
920 #[test]
921 fn sources_contain_only_main_for_standalone_spec() {
922 let code = r#"
923spec standalone
924data age: 25
925rule is_adult: age >= 18
926"#;
927 let specs = parse(code, "test.lemma", &ResourceLimits::default())
928 .unwrap()
929 .specs;
930
931 let mut sources = HashMap::new();
932 sources.insert("test.lemma".to_string(), code.to_string());
933
934 let plan = plan_single(&specs[0], &specs).expect("planning should succeed");
935
936 assert_eq!(
937 plan.sources.len(),
938 1,
939 "standalone should have only main spec"
940 );
941 assert!(has_source_for(&plan, "standalone"));
942 }
943
944 #[test]
945 fn sources_contain_all_cross_spec_refs() {
946 let code = r#"
947spec rates
948data base_rate: 0.05
949rule rate: base_rate
950
951spec config
952data threshold: 100
953rule limit: threshold
954
955spec calculator
956with r: rates
957data r.base_rate: 0.03
958with c: config
959data c.threshold: 200
960rule combined: r.rate + c.limit
961"#;
962 let specs = parse(code, "test.lemma", &ResourceLimits::default())
963 .unwrap()
964 .specs;
965 let calc = specs.iter().find(|s| s.name == "calculator").unwrap();
966
967 let mut sources = HashMap::new();
968 sources.insert("test.lemma".to_string(), code.to_string());
969
970 let plan = plan_single(calc, &specs).expect("planning should succeed");
971
972 assert_eq!(
973 plan.sources.len(),
974 3,
975 "calculator + rates + config, got: {:?}",
976 plan.sources
977 );
978 assert!(has_source_for(&plan, "calculator"));
979 assert!(has_source_for(&plan, "rates"));
980 assert!(has_source_for(&plan, "config"));
981 }
982
983 #[test]
984 fn sources_include_spec_ref_even_without_rules() {
985 let code = r#"
986spec dep
987data x: 10
988
989spec consumer
990with d: dep
991data local: 99
992rule result: local
993"#;
994 let specs = parse(code, "test.lemma", &ResourceLimits::default())
995 .unwrap()
996 .specs;
997 let consumer = specs.iter().find(|s| s.name == "consumer").unwrap();
998
999 let mut sources = HashMap::new();
1000 sources.insert("test.lemma".to_string(), code.to_string());
1001
1002 let plan = plan_single(consumer, &specs).expect("planning should succeed");
1003
1004 assert_eq!(
1005 plan.sources.len(),
1006 2,
1007 "consumer + dep, got: {:?}",
1008 plan.sources
1009 );
1010 assert!(
1011 has_source_for(&plan, "dep"),
1012 "spec ref dep must be in sources even without rules"
1013 );
1014 }
1015
1016 #[test]
1017 fn sources_round_trip_to_valid_specs() {
1018 let code = r#"
1019spec dep
1020data x: 42
1021rule val: x
1022
1023spec consumer
1024with d: dep
1025rule result: d.val
1026"#;
1027 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1028 .unwrap()
1029 .specs;
1030 let consumer = specs.iter().find(|s| s.name == "consumer").unwrap();
1031
1032 let mut sources = HashMap::new();
1033 sources.insert("test.lemma".to_string(), code.to_string());
1034
1035 let plan = plan_single(consumer, &specs).expect("planning should succeed");
1036
1037 for ((name, _), source_text) in &plan.sources {
1038 let parsed = parse(source_text, "roundtrip.lemma", &ResourceLimits::default());
1039 assert!(
1040 parsed.is_ok(),
1041 "source for '{}' must re-parse: {:?}\nsource:\n{}",
1042 name,
1043 parsed.err(),
1044 source_text
1045 );
1046 }
1047 }
1048}