1use crate::error::Error;
10use crate::parsing::ast::{self as ast, CommandArg, LemmaSpec, Reference, TypeDef};
11use crate::planning::semantics::{self, LemmaType, TypeExtends, TypeSpecification};
12use crate::planning::validation::validate_type_specifications;
13
14use std::collections::{HashMap, HashSet};
15use std::sync::Arc;
16
17#[derive(Debug, Clone)]
20pub struct ResolvedSpecTypes {
21 pub named_types: HashMap<String, LemmaType>,
23
24 pub inline_type_definitions: HashMap<Reference, LemmaType>,
26
27 pub unit_index: HashMap<String, (LemmaType, Option<TypeDef>)>,
32}
33
34#[derive(Debug, Clone)]
40pub struct TypeResolver {
41 named_types: HashMap<Arc<LemmaSpec>, HashMap<String, TypeDef>>,
42 inline_type_definitions: HashMap<Arc<LemmaSpec>, HashMap<Reference, TypeDef>>,
43 name_to_arc: HashMap<String, Arc<LemmaSpec>>,
45}
46
47impl TypeResolver {
48 pub fn new() -> Self {
49 TypeResolver {
50 named_types: HashMap::new(),
51 inline_type_definitions: HashMap::new(),
52 name_to_arc: HashMap::new(),
53 }
54 }
55
56 pub fn register_all(&mut self, spec: &Arc<LemmaSpec>) -> Vec<Error> {
58 let mut errors = Vec::new();
59 for type_def in &spec.types {
60 let type_name = match type_def {
61 ast::TypeDef::Regular { name, .. } | ast::TypeDef::Import { name, .. } => {
62 Some(name.as_str())
63 }
64 ast::TypeDef::Inline { .. } => None,
65 };
66 if let Some(name) = type_name {
67 if let Err(e) = crate::limits::check_max_length(
68 name,
69 crate::limits::MAX_TYPE_NAME_LENGTH,
70 "type",
71 Some(type_def.source_location().clone()),
72 ) {
73 errors.push(e);
74 continue;
75 }
76 }
77 if let Err(e) = self.register_type(spec, type_def.clone()) {
78 errors.push(e);
79 }
80 }
81 errors
82 }
83
84 pub fn resolve(
88 &self,
89 all_specs: impl IntoIterator<Item = Arc<LemmaSpec>>,
90 ) -> (HashMap<Arc<LemmaSpec>, ResolvedSpecTypes>, Vec<Error>) {
91 let mut result = HashMap::new();
92 let mut errors = Vec::new();
93
94 for spec_arc in all_specs {
95 let spec_arc = &spec_arc;
96 match self.resolve_named_types(spec_arc) {
97 Ok(resolved_types) => {
98 for (type_name, lemma_type) in &resolved_types.named_types {
99 let source = spec_arc
100 .types
101 .iter()
102 .find(|td| match td {
103 ast::TypeDef::Regular { name, .. }
104 | ast::TypeDef::Import { name, .. } => name == type_name,
105 ast::TypeDef::Inline { .. } => false,
106 })
107 .map(|td| td.source_location().clone())
108 .unwrap_or_else(|| {
109 unreachable!(
110 "BUG: resolved named type '{}' has no corresponding TypeDef in spec '{}'",
111 type_name, spec_arc.name
112 )
113 });
114 let mut spec_errors = validate_type_specifications(
115 &lemma_type.specifications,
116 type_name,
117 &source,
118 );
119 errors.append(&mut spec_errors);
120 }
121 result.insert(Arc::clone(spec_arc), resolved_types);
122 }
123 Err(es) => errors.extend(es),
124 }
125 }
126
127 (result, errors)
128 }
129
130 pub fn register_type(&mut self, spec: &Arc<LemmaSpec>, def: TypeDef) -> Result<(), Error> {
133 self.name_to_arc
134 .entry(spec.name.clone())
135 .and_modify(|existing| {
136 if spec.effective_from() < existing.effective_from() {
137 *existing = Arc::clone(spec);
138 }
139 })
140 .or_insert_with(|| Arc::clone(spec));
141
142 let def_loc = def.source_location().clone();
143 let spec_name = &spec.name;
144 match &def {
145 TypeDef::Regular { name, .. } | TypeDef::Import { name, .. } => {
146 let spec_types = self.named_types.entry(Arc::clone(spec)).or_default();
147 if spec_types.contains_key(name) {
148 return Err(Error::validation(
149 format!("Type '{}' is already defined in spec '{}'", name, spec_name),
150 Some(def_loc.clone()),
151 None::<String>,
152 ));
153 }
154 spec_types.insert(name.clone(), def);
155 }
156 TypeDef::Inline { fact_ref, .. } => {
157 let spec_inline_types = self
158 .inline_type_definitions
159 .entry(Arc::clone(spec))
160 .or_default();
161 if spec_inline_types.contains_key(fact_ref) {
162 return Err(Error::validation(
163 format!(
164 "Inline type definition for fact '{}' is already defined in spec '{}'",
165 fact_ref.name, spec_name
166 ),
167 Some(def_loc.clone()),
168 None::<String>,
169 ));
170 }
171 spec_inline_types.insert(fact_ref.clone(), def);
172 }
173 }
174 Ok(())
175 }
176
177 pub fn resolve_types(&self, spec: &Arc<LemmaSpec>) -> Result<ResolvedSpecTypes, Vec<Error>> {
179 self.resolve_types_internal(spec, true)
180 }
181
182 pub fn resolve_named_types(
184 &self,
185 spec: &Arc<LemmaSpec>,
186 ) -> Result<ResolvedSpecTypes, Vec<Error>> {
187 self.resolve_types_internal(spec, false)
188 }
189
190 pub fn resolve_inline_types(
193 &self,
194 spec: &Arc<LemmaSpec>,
195 mut existing: ResolvedSpecTypes,
196 ) -> Result<ResolvedSpecTypes, Vec<Error>> {
197 let mut errors = Vec::new();
198
199 if let Some(spec_inline_types) = self.inline_type_definitions.get(spec) {
200 for (fact_ref, type_def) in spec_inline_types {
201 let mut visited = HashSet::new();
202 match self.resolve_inline_type_definition(spec, type_def, &mut visited) {
203 Ok(Some(resolved_type)) => {
204 existing
205 .inline_type_definitions
206 .insert(fact_ref.clone(), resolved_type);
207 }
208 Ok(None) => {
209 unreachable!(
210 "BUG: registered inline type definition for fact '{}' could not be resolved (spec='{}')",
211 fact_ref, spec.name
212 );
213 }
214 Err(es) => return Err(es),
215 }
216 }
217 }
218
219 if let Some(spec_inline_defs) = self.inline_type_definitions.get(spec) {
220 for (fact_ref, type_def) in spec_inline_defs {
221 let Some(resolved_type) = existing.inline_type_definitions.get(fact_ref) else {
222 continue;
223 };
224 let e: Result<(), Error> = if resolved_type.is_scale() {
225 Self::add_scale_units_to_index(
226 &mut existing.unit_index,
227 resolved_type,
228 type_def,
229 )
230 } else if resolved_type.is_ratio() {
231 Self::add_ratio_units_to_index(
232 &mut existing.unit_index,
233 resolved_type,
234 type_def,
235 )
236 } else {
237 Ok(())
238 };
239 if let Err(e) = e {
240 errors.push(e);
241 }
242 }
243 }
244
245 if !errors.is_empty() {
246 return Err(errors);
247 }
248
249 Ok(existing)
250 }
251
252 fn resolve_types_internal(
253 &self,
254 spec: &Arc<LemmaSpec>,
255 include_anonymous: bool,
256 ) -> Result<ResolvedSpecTypes, Vec<Error>> {
257 let mut named_types = HashMap::new();
258 let mut inline_type_definitions = HashMap::new();
259 let mut visited = HashSet::new();
260
261 if let Some(spec_types) = self.named_types.get(spec) {
262 for type_name in spec_types.keys() {
263 match self.resolve_type_internal(spec, type_name, &mut visited) {
264 Ok(Some(resolved_type)) => {
265 named_types.insert(type_name.clone(), resolved_type);
266 }
267 Ok(None) => {
268 unreachable!(
269 "BUG: registered named type '{}' could not be resolved (spec='{}')",
270 type_name, spec.name
271 );
272 }
273 Err(es) => return Err(es),
274 }
275 visited.clear();
276 }
277 }
278
279 if include_anonymous {
280 if let Some(spec_inline_types) = self.inline_type_definitions.get(spec) {
281 for (fact_ref, type_def) in spec_inline_types {
282 let mut visited = HashSet::new();
283 match self.resolve_inline_type_definition(spec, type_def, &mut visited) {
284 Ok(Some(resolved_type)) => {
285 inline_type_definitions.insert(fact_ref.clone(), resolved_type);
286 }
287 Ok(None) => {
288 unreachable!(
289 "BUG: registered inline type definition for fact '{}' could not be resolved (spec='{}')",
290 fact_ref, spec.name
291 );
292 }
293 Err(es) => return Err(es),
294 }
295 }
296 }
297 }
298
299 let mut unit_index: HashMap<String, (LemmaType, Option<TypeDef>)> = HashMap::new();
300 let mut errors = Vec::new();
301
302 let prim_ratio = semantics::primitive_ratio();
303 for unit in Self::extract_units_from_type(&prim_ratio.specifications) {
304 unit_index.insert(unit, (prim_ratio.clone(), None));
305 }
306
307 for (type_name, resolved_type) in &named_types {
308 let type_def = self
309 .named_types
310 .get(spec)
311 .and_then(|defs| defs.get(type_name.as_str()))
312 .expect("BUG: named type was resolved but not in registry");
313 let e: Result<(), Error> = if resolved_type.is_scale() {
314 Self::add_scale_units_to_index(&mut unit_index, resolved_type, type_def)
315 } else if resolved_type.is_ratio() {
316 Self::add_ratio_units_to_index(&mut unit_index, resolved_type, type_def)
317 } else {
318 Ok(())
319 };
320 if let Err(e) = e {
321 errors.push(e);
322 }
323 }
324
325 for (fact_ref, resolved_type) in &inline_type_definitions {
326 let type_def = self
327 .inline_type_definitions
328 .get(spec)
329 .and_then(|defs| defs.get(fact_ref))
330 .expect("BUG: inline type was resolved but not in registry");
331 let e: Result<(), Error> = if resolved_type.is_scale() {
332 Self::add_scale_units_to_index(&mut unit_index, resolved_type, type_def)
333 } else if resolved_type.is_ratio() {
334 Self::add_ratio_units_to_index(&mut unit_index, resolved_type, type_def)
335 } else {
336 Ok(())
337 };
338 if let Err(e) = e {
339 errors.push(e);
340 }
341 }
342
343 if !errors.is_empty() {
344 return Err(errors);
345 }
346
347 Ok(ResolvedSpecTypes {
348 named_types,
349 inline_type_definitions,
350 unit_index,
351 })
352 }
353
354 fn resolve_type_internal(
355 &self,
356 spec: &Arc<LemmaSpec>,
357 name: &str,
358 visited: &mut HashSet<String>,
359 ) -> Result<Option<LemmaType>, Vec<Error>> {
360 let key = format!("{}::{}", spec.name, name);
361 if visited.contains(&key) {
362 let source_location = self
363 .named_types
364 .get(spec)
365 .and_then(|dt| dt.get(name))
366 .map(|td| td.source_location().clone())
367 .unwrap_or_else(|| {
368 unreachable!(
369 "BUG: circular dependency detected for type '{}::{}' but type definition not found in registry",
370 spec.name, name
371 )
372 });
373 return Err(vec![Error::validation(
374 format!("Circular dependency detected in type resolution: {}", key),
375 Some(source_location),
376 None::<String>,
377 )]);
378 }
379 visited.insert(key.clone());
380
381 let type_def = match self.named_types.get(spec).and_then(|dt| dt.get(name)) {
382 Some(def) => def.clone(),
383 None => {
384 visited.remove(&key);
385 return Ok(None);
386 }
387 };
388
389 let (parent, from, constraints, type_name) = match &type_def {
391 TypeDef::Regular {
392 name,
393 parent,
394 constraints,
395 ..
396 } => (parent.clone(), None, constraints.clone(), name.clone()),
397 TypeDef::Import {
398 name,
399 source_type,
400 from,
401 constraints,
402 ..
403 } => (
404 source_type.clone(),
405 Some(from.clone()),
406 constraints.clone(),
407 name.clone(),
408 ),
409 TypeDef::Inline { .. } => {
410 visited.remove(&key);
412 return Ok(None);
413 }
414 };
415
416 let parent_specs = match self.resolve_parent(
417 spec,
418 &parent,
419 &from,
420 visited,
421 type_def.source_location(),
422 ) {
423 Ok(Some(specs)) => specs,
424 Ok(None) => {
425 visited.remove(&key);
428 let source = type_def.source_location().clone();
429 return Err(vec![Error::validation(
430 format!("Unknown type: '{}'. Type must be defined before use. Valid primitive types are: boolean, scale, number, ratio, text, date, time, duration, percent", parent),
431 Some(source.clone()),
432 None::<String>,
433 )]);
434 }
435 Err(es) => {
436 visited.remove(&key);
437 return Err(es);
438 }
439 };
440
441 let final_specs = if let Some(constraints) = &constraints {
442 match self.apply_constraints(parent_specs, constraints, type_def.source_location()) {
443 Ok(specs) => specs,
444 Err(errors) => {
445 visited.remove(&key);
446 return Err(errors);
447 }
448 }
449 } else {
450 parent_specs
451 };
452
453 visited.remove(&key);
454
455 let extends = if self.resolve_primitive_type(&parent).is_some() {
456 TypeExtends::Primitive
457 } else {
458 let parent_spec_name = from
459 .as_ref()
460 .map(|r| r.name.as_str())
461 .unwrap_or(spec.name.as_str());
462 let parent_arc = self.name_to_arc.get(parent_spec_name);
463 let family = match parent_arc {
464 Some(arc) => match self.resolve_type_internal(arc, &parent, visited) {
465 Ok(Some(parent_type)) => parent_type
466 .scale_family_name()
467 .map(String::from)
468 .unwrap_or_else(|| parent.clone()),
469 Ok(None) => parent.clone(),
470 Err(es) => return Err(es),
471 },
472 None => parent.clone(),
473 };
474 TypeExtends::Custom {
475 parent: parent.clone(),
476 family,
477 }
478 };
479
480 Ok(Some(LemmaType {
481 name: Some(type_name),
482 specifications: final_specs,
483 extends,
484 }))
485 }
486
487 fn resolve_parent(
488 &self,
489 spec: &Arc<LemmaSpec>,
490 parent: &str,
491 from: &Option<crate::parsing::ast::SpecRef>,
492 visited: &mut HashSet<String>,
493 source: &crate::Source,
494 ) -> Result<Option<TypeSpecification>, Vec<Error>> {
495 if let Some(specs) = self.resolve_primitive_type(parent) {
496 return Ok(Some(specs));
497 }
498
499 let parent_spec_name = from
500 .as_ref()
501 .map(|r| r.name.as_str())
502 .unwrap_or(spec.name.as_str());
503 let parent_arc = self.name_to_arc.get(parent_spec_name);
504 let result = match parent_arc {
505 Some(arc) => self.resolve_type_internal(arc, parent, visited),
506 None => Ok(None),
507 };
508 match result {
509 Ok(Some(t)) => Ok(Some(t.specifications)),
510 Ok(None) => {
511 let type_exists = parent_arc
512 .and_then(|arc| self.named_types.get(arc))
513 .map(|spec_types| spec_types.contains_key(parent))
514 .unwrap_or(false);
515
516 if !type_exists {
517 let suggestion = from.as_ref().filter(|r| r.is_registry).map(|r| {
518 format!(
519 "Run `lemma get` or `lemma get {}` to fetch this dependency.",
520 r.name
521 )
522 });
523 Err(vec![Error::validation(
524 format!("Unknown type: '{}'. Type must be defined before use. Valid primitive types are: boolean, scale, number, ratio, text, date, time, duration, percent", parent),
525 Some(source.clone()),
526 suggestion,
527 )])
528 } else {
529 Ok(None)
530 }
531 }
532 Err(es) => Err(es),
533 }
534 }
535
536 pub fn resolve_primitive_type(&self, name: &str) -> Option<TypeSpecification> {
538 match name {
539 "boolean" => Some(TypeSpecification::boolean()),
540 "scale" => Some(TypeSpecification::scale()),
541 "number" => Some(TypeSpecification::number()),
542 "ratio" => Some(TypeSpecification::ratio()),
543 "text" => Some(TypeSpecification::text()),
544 "date" => Some(TypeSpecification::date()),
545 "time" => Some(TypeSpecification::time()),
546 "duration" => Some(TypeSpecification::duration()),
547 "percent" => Some(TypeSpecification::ratio()),
548 _ => None,
549 }
550 }
551
552 fn apply_constraints(
555 &self,
556 mut specs: TypeSpecification,
557 constraints: &[(String, Vec<CommandArg>)],
558 source: &crate::Source,
559 ) -> Result<TypeSpecification, Vec<Error>> {
560 let mut errors = Vec::new();
561 for (command, args) in constraints {
562 let specs_clone = specs.clone();
563 match specs.apply_constraint(command, args) {
564 Ok(updated_specs) => specs = updated_specs,
565 Err(e) => {
566 errors.push(Error::validation(
567 format!("Failed to apply constraint '{}': {}", command, e),
568 Some(source.clone()),
569 None::<String>,
570 ));
571 specs = specs_clone;
572 }
573 }
574 }
575 if !errors.is_empty() {
576 return Err(errors);
577 }
578 Ok(specs)
579 }
580
581 fn resolve_inline_type_definition(
582 &self,
583 spec: &Arc<LemmaSpec>,
584 type_def: &TypeDef,
585 visited: &mut HashSet<String>,
586 ) -> Result<Option<LemmaType>, Vec<Error>> {
587 let def_loc = type_def.source_location().clone();
588 let TypeDef::Inline {
589 parent,
590 constraints,
591 fact_ref: _,
592 from,
593 ..
594 } = type_def
595 else {
596 return Ok(None);
597 };
598
599 let parent_specs = match self.resolve_parent(spec, parent, from, visited, &def_loc) {
600 Ok(Some(specs)) => specs,
601 Ok(None) => {
602 return Err(vec![Error::validation(
603 format!("Unknown type: '{}'. Type must be defined before use. Valid primitive types are: boolean, scale, number, ratio, text, date, time, duration, percent", parent),
604 Some(def_loc.clone()),
605 None::<String>,
606 )]);
607 }
608 Err(es) => return Err(es),
609 };
610
611 let final_specs = if let Some(constraints) = constraints {
612 self.apply_constraints(parent_specs, constraints, &def_loc)?
613 } else {
614 parent_specs
615 };
616
617 let extends = if self.resolve_primitive_type(parent).is_some() {
618 TypeExtends::Primitive
619 } else {
620 let parent_spec_name = from
621 .as_ref()
622 .map(|r| r.name.as_str())
623 .unwrap_or(spec.name.as_str());
624 let family = match self.name_to_arc.get(parent_spec_name) {
625 Some(arc) => match self.resolve_type_internal(arc, parent, visited) {
626 Ok(Some(parent_type)) => parent_type
627 .scale_family_name()
628 .map(String::from)
629 .unwrap_or_else(|| parent.to_string()),
630 Ok(None) => parent.to_string(),
631 Err(es) => return Err(es),
632 },
633 None => parent.to_string(),
634 };
635 TypeExtends::Custom {
636 parent: parent.to_string(),
637 family,
638 }
639 };
640
641 Ok(Some(LemmaType::without_name(final_specs, extends)))
642 }
643
644 fn add_scale_units_to_index(
645 unit_index: &mut HashMap<String, (LemmaType, Option<TypeDef>)>,
646 resolved_type: &LemmaType,
647 defined_by: &TypeDef,
648 ) -> Result<(), Error> {
649 let units = Self::extract_units_from_type(&resolved_type.specifications);
650 for unit in units {
651 if let Some((existing_type, existing_def)) = unit_index.get(&unit) {
652 let same_type = existing_def.as_ref() == Some(defined_by);
653
654 if same_type {
655 return Err(Error::validation(
656 format!(
657 "Unit '{}' is defined more than once in type '{}'",
658 unit,
659 defined_by.name()
660 ),
661 Some(defined_by.source_location().clone()),
662 None::<String>,
663 ));
664 }
665
666 let existing_name: String = existing_def
667 .as_ref()
668 .map(|d| d.name().to_owned())
669 .unwrap_or_else(|| existing_type.name());
670 let current_extends_existing = resolved_type
671 .extends
672 .parent_name()
673 .map(|p| p == existing_name.as_str())
674 .unwrap_or(false);
675 let existing_extends_current = existing_type
676 .extends
677 .parent_name()
678 .map(|p| p == defined_by.name())
679 .unwrap_or(false);
680
681 if existing_type.is_scale()
682 && (current_extends_existing || existing_extends_current)
683 {
684 if current_extends_existing {
685 unit_index.insert(unit, (resolved_type.clone(), Some(defined_by.clone())));
686 }
687 continue;
688 }
689
690 if existing_type.same_scale_family(resolved_type) {
691 continue;
692 }
693
694 return Err(Error::validation(
695 format!(
696 "Ambiguous unit '{}'. Defined in multiple types: '{}' and '{}'",
697 unit,
698 existing_name,
699 defined_by.name()
700 ),
701 Some(defined_by.source_location().clone()),
702 None::<String>,
703 ));
704 }
705 unit_index.insert(unit, (resolved_type.clone(), Some(defined_by.clone())));
706 }
707 Ok(())
708 }
709
710 fn add_ratio_units_to_index(
711 unit_index: &mut HashMap<String, (LemmaType, Option<TypeDef>)>,
712 resolved_type: &LemmaType,
713 defined_by: &TypeDef,
714 ) -> Result<(), Error> {
715 let units = Self::extract_units_from_type(&resolved_type.specifications);
716 for unit in units {
717 if let Some((existing_type, existing_def)) = unit_index.get(&unit) {
718 if existing_type.is_ratio() {
719 continue;
720 }
721 let existing_name: String = existing_def
722 .as_ref()
723 .map(|d| d.name().to_owned())
724 .unwrap_or_else(|| existing_type.name());
725 return Err(Error::validation(
726 format!(
727 "Ambiguous unit '{}'. Defined in multiple types: '{}' and '{}'",
728 unit,
729 existing_name,
730 defined_by.name()
731 ),
732 Some(defined_by.source_location().clone()),
733 None::<String>,
734 ));
735 }
736 unit_index.insert(unit, (resolved_type.clone(), Some(defined_by.clone())));
737 }
738 Ok(())
739 }
740
741 fn extract_units_from_type(specs: &TypeSpecification) -> Vec<String> {
742 match specs {
743 TypeSpecification::Scale { units, .. } => {
744 units.iter().map(|unit| unit.name.clone()).collect()
745 }
746 TypeSpecification::Ratio { units, .. } => {
747 units.iter().map(|unit| unit.name.clone()).collect()
748 }
749 _ => Vec::new(),
750 }
751 }
752}
753
754impl Default for TypeResolver {
755 fn default() -> Self {
756 Self::new()
757 }
758}
759
760#[cfg(test)]
761mod tests {
762 use super::*;
763 use crate::parse;
764 use crate::parsing::ast::LemmaSpec;
765 use crate::ResourceLimits;
766 use rust_decimal::Decimal;
767 use std::sync::Arc;
768
769 fn test_registry() -> TypeResolver {
770 TypeResolver::new()
771 }
772
773 fn test_spec_arc() -> Arc<LemmaSpec> {
774 Arc::new(LemmaSpec::new("test_spec".to_string()))
775 }
776
777 #[test]
778 fn test_registry_creation() {
779 let registry = test_registry();
780 let spec_arc = test_spec_arc();
781 let resolved = registry.resolve_types(&spec_arc).unwrap();
782 assert!(resolved.named_types.is_empty());
783 assert!(resolved.inline_type_definitions.is_empty());
784 }
785
786 #[test]
787 fn test_resolve_primitive_types() {
788 let registry = test_registry();
789
790 assert!(registry.resolve_primitive_type("boolean").is_some());
791 assert!(registry.resolve_primitive_type("scale").is_some());
792 assert!(registry.resolve_primitive_type("number").is_some());
793 assert!(registry.resolve_primitive_type("ratio").is_some());
794 assert!(registry.resolve_primitive_type("text").is_some());
795 assert!(registry.resolve_primitive_type("date").is_some());
796 assert!(registry.resolve_primitive_type("time").is_some());
797 assert!(registry.resolve_primitive_type("duration").is_some());
798 assert!(registry.resolve_primitive_type("unknown").is_none());
799 }
800
801 #[test]
802 fn test_register_named_type() {
803 let mut registry = test_registry();
804 let type_def = TypeDef::Regular {
805 source_location: crate::Source::new(
806 "<test>",
807 crate::parsing::ast::Span {
808 start: 0,
809 end: 0,
810 line: 1,
811 col: 0,
812 },
813 Arc::from("spec test\nfact x: 1"),
814 ),
815 name: "money".to_string(),
816 parent: "number".to_string(),
817 constraints: None,
818 };
819
820 let result = registry.register_type(&test_spec_arc(), type_def);
821 assert!(result.is_ok());
822 }
823
824 #[test]
825 fn test_register_inline_type_definition() {
826 use crate::parsing::ast::Reference;
827 let mut registry = test_registry();
828 let fact_ref = Reference::local("age".to_string());
829 let type_def = TypeDef::Inline {
830 source_location: crate::Source::new(
831 "<test>",
832 crate::parsing::ast::Span {
833 start: 0,
834 end: 0,
835 line: 1,
836 col: 0,
837 },
838 Arc::from("spec test\nfact x: 1"),
839 ),
840 parent: "number".to_string(),
841 constraints: Some(vec![
842 (
843 "minimum".to_string(),
844 vec![CommandArg::Number("0".to_string())],
845 ),
846 (
847 "maximum".to_string(),
848 vec![CommandArg::Number("150".to_string())],
849 ),
850 ]),
851 fact_ref: fact_ref.clone(),
852 from: None,
853 };
854
855 let spec_arc = test_spec_arc();
856 let result = registry.register_type(&spec_arc, type_def);
857 assert!(result.is_ok());
858 let resolved = registry.resolve_types(&spec_arc).unwrap();
859 assert!(resolved.inline_type_definitions.contains_key(&fact_ref));
860 }
861
862 #[test]
863 fn test_register_duplicate_type_fails() {
864 let mut registry = test_registry();
865 let type_def = TypeDef::Regular {
866 source_location: crate::Source::new(
867 "<test>",
868 crate::parsing::ast::Span {
869 start: 0,
870 end: 0,
871 line: 1,
872 col: 0,
873 },
874 Arc::from("spec test\nfact x: 1"),
875 ),
876 name: "money".to_string(),
877 parent: "number".to_string(),
878 constraints: None,
879 };
880
881 let spec_arc = test_spec_arc();
882 registry.register_type(&spec_arc, type_def.clone()).unwrap();
883 let result = registry.register_type(&spec_arc, type_def);
884 assert!(result.is_err());
885 }
886
887 #[test]
888 fn test_resolve_custom_type_from_primitive() {
889 let mut registry = test_registry();
890 let type_def = TypeDef::Regular {
891 source_location: crate::Source::new(
892 "<test>",
893 crate::parsing::ast::Span {
894 start: 0,
895 end: 0,
896 line: 1,
897 col: 0,
898 },
899 Arc::from("spec test\nfact x: 1"),
900 ),
901 name: "money".to_string(),
902 parent: "number".to_string(),
903 constraints: None,
904 };
905
906 let spec_arc = test_spec_arc();
907 registry.register_type(&spec_arc, type_def).unwrap();
908 let resolved = registry.resolve_types(&spec_arc).unwrap();
909
910 assert!(resolved.named_types.contains_key("money"));
911 let money_type = resolved.named_types.get("money").unwrap();
912 assert_eq!(money_type.name, Some("money".to_string()));
913 }
914
915 #[test]
916 fn test_type_definition_resolution() {
917 let code = r#"spec test
918type dice: number -> minimum 0 -> maximum 6"#;
919
920 let specs = parse(code, "test.lemma", &ResourceLimits::default())
921 .unwrap()
922 .specs;
923 let spec = &specs[0];
924
925 let mut registry = test_registry();
927 registry
928 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
929 .unwrap();
930
931 let resolved_types = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
932 let dice_type = resolved_types.named_types.get("dice").unwrap();
933
934 match &dice_type.specifications {
936 TypeSpecification::Number {
937 minimum, maximum, ..
938 } => {
939 assert_eq!(*minimum, Some(Decimal::from(0)));
940 assert_eq!(*maximum, Some(Decimal::from(6)));
941 }
942 _ => panic!("Expected Number type specifications"),
943 }
944 }
945
946 #[test]
947 fn test_type_definition_with_multiple_commands() {
948 let code = r#"spec test
949type money: scale -> decimals 2 -> unit eur 1.0 -> unit usd 1.18"#;
950
951 let specs = parse(code, "test.lemma", &ResourceLimits::default())
952 .unwrap()
953 .specs;
954 let spec = &specs[0];
955 let type_def = &spec.types[0];
956
957 let mut registry = test_registry();
959 registry
960 .register_type(&Arc::new(spec.clone()), type_def.clone())
961 .unwrap();
962
963 let resolved_types = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
964 let money_type = resolved_types.named_types.get("money").unwrap();
965
966 match &money_type.specifications {
967 TypeSpecification::Scale {
968 decimals, units, ..
969 } => {
970 assert_eq!(*decimals, Some(2));
971 assert_eq!(units.len(), 2);
972 assert!(units.iter().any(|u| u.name == "eur"));
973 assert!(units.iter().any(|u| u.name == "usd"));
974 }
975 _ => panic!("Expected Scale type specifications"),
976 }
977 }
978
979 #[test]
980 fn test_number_type_with_decimals() {
981 let code = r#"spec test
982type price: number -> decimals 2 -> minimum 0"#;
983
984 let specs = parse(code, "test.lemma", &ResourceLimits::default())
985 .unwrap()
986 .specs;
987 let spec = &specs[0];
988
989 let mut registry = test_registry();
991 registry
992 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
993 .unwrap();
994
995 let resolved_types = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
996 let price_type = resolved_types.named_types.get("price").unwrap();
997
998 match &price_type.specifications {
1000 TypeSpecification::Number {
1001 decimals, minimum, ..
1002 } => {
1003 assert_eq!(*decimals, Some(2));
1004 assert_eq!(*minimum, Some(Decimal::from(0)));
1005 }
1006 _ => panic!("Expected Number type specifications with decimals"),
1007 }
1008 }
1009
1010 #[test]
1011 fn test_number_type_decimals_only() {
1012 let code = r#"spec test
1013type precise_number: number -> decimals 4"#;
1014
1015 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1016 .unwrap()
1017 .specs;
1018 let spec = &specs[0];
1019
1020 let mut registry = test_registry();
1021 registry
1022 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1023 .unwrap();
1024
1025 let resolved_types = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
1026 let precise_type = resolved_types.named_types.get("precise_number").unwrap();
1027
1028 match &precise_type.specifications {
1029 TypeSpecification::Number { decimals, .. } => {
1030 assert_eq!(*decimals, Some(4));
1031 }
1032 _ => panic!("Expected Number type with decimals 4"),
1033 }
1034 }
1035
1036 #[test]
1037 fn test_scale_type_decimals_only() {
1038 let code = r#"spec test
1039type weight: scale -> unit kg 1 -> decimals 3"#;
1040
1041 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1042 .unwrap()
1043 .specs;
1044 let spec = &specs[0];
1045
1046 let mut registry = test_registry();
1047 registry
1048 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1049 .unwrap();
1050
1051 let resolved_types = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
1052 let weight_type = resolved_types.named_types.get("weight").unwrap();
1053
1054 match &weight_type.specifications {
1055 TypeSpecification::Scale { decimals, .. } => {
1056 assert_eq!(*decimals, Some(3));
1057 }
1058 _ => panic!("Expected Scale type with decimals 3"),
1059 }
1060 }
1061
1062 #[test]
1063 fn test_ratio_type_accepts_optional_decimals_command() {
1064 let code = r#"spec test
1065type ratio_type: ratio -> decimals 2"#;
1066
1067 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1068 .unwrap()
1069 .specs;
1070 let spec = &specs[0];
1071
1072 let mut registry = test_registry();
1073 registry
1074 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1075 .unwrap();
1076
1077 let resolved_types = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
1078 let ratio_type = resolved_types.named_types.get("ratio_type").unwrap();
1079
1080 match &ratio_type.specifications {
1081 TypeSpecification::Ratio { decimals, .. } => {
1082 assert_eq!(
1083 *decimals,
1084 Some(2),
1085 "ratio type should accept decimals command"
1086 );
1087 }
1088 _ => panic!("Expected Ratio type with decimals 2"),
1089 }
1090 }
1091
1092 #[test]
1093 fn test_ratio_type_with_default_command() {
1094 let code = r#"spec test
1095type percentage: ratio -> minimum 0 -> maximum 1 -> default 0.5"#;
1096
1097 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1098 .unwrap()
1099 .specs;
1100 let spec = &specs[0];
1101
1102 let mut registry = test_registry();
1103 registry
1104 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1105 .unwrap();
1106
1107 let resolved_types = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
1108 let percentage_type = resolved_types.named_types.get("percentage").unwrap();
1109
1110 match &percentage_type.specifications {
1111 TypeSpecification::Ratio {
1112 minimum,
1113 maximum,
1114 default,
1115 ..
1116 } => {
1117 assert_eq!(
1118 *minimum,
1119 Some(Decimal::from(0)),
1120 "ratio type should have minimum 0"
1121 );
1122 assert_eq!(
1123 *maximum,
1124 Some(Decimal::from(1)),
1125 "ratio type should have maximum 1"
1126 );
1127 assert_eq!(
1128 *default,
1129 Some(Decimal::from_i128_with_scale(5, 1)),
1130 "ratio type with default command must work"
1131 );
1132 }
1133 _ => panic!("Expected Ratio type with minimum, maximum, and default"),
1134 }
1135 }
1136
1137 #[test]
1138 fn test_scale_extension_chain_same_family_units_allowed() {
1139 let code = r#"spec test
1140type money: scale -> unit eur 1
1141type money2: money -> unit usd 1.24"#;
1142
1143 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1144 .unwrap()
1145 .specs;
1146 let spec = &specs[0];
1147
1148 let mut registry = test_registry();
1149 for type_def in &spec.types {
1150 registry
1151 .register_type(&Arc::new(spec.clone()), type_def.clone())
1152 .unwrap();
1153 }
1154
1155 let result = registry.resolve_types(&Arc::new(spec.clone()));
1156 assert!(
1157 result.is_ok(),
1158 "Scale extension chain should resolve: {:?}",
1159 result.err()
1160 );
1161
1162 let resolved = result.unwrap();
1163 assert!(
1164 resolved.unit_index.contains_key("eur"),
1165 "eur should be in unit_index"
1166 );
1167 assert!(
1168 resolved.unit_index.contains_key("usd"),
1169 "usd should be in unit_index"
1170 );
1171 let (eur_type, _) = resolved.unit_index.get("eur").unwrap();
1172 let (usd_type, _) = resolved.unit_index.get("usd").unwrap();
1173 assert_eq!(
1174 eur_type.name.as_deref(),
1175 Some("money2"),
1176 "more derived type (money2) should own eur for conversion"
1177 );
1178 assert_eq!(usd_type.name.as_deref(), Some("money2"));
1179 }
1180
1181 #[test]
1182 fn test_invalid_parent_type_in_named_type_should_error() {
1183 let code = r#"spec test
1184type invalid: nonexistent_type -> minimum 0"#;
1185
1186 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1187 .unwrap()
1188 .specs;
1189 let spec = &specs[0];
1190
1191 let mut registry = test_registry();
1192 registry
1193 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1194 .unwrap();
1195
1196 let result = registry.resolve_types(&Arc::new(spec.clone()));
1197 assert!(result.is_err(), "Should reject invalid parent type");
1198
1199 let errs = result.unwrap_err();
1200 assert!(!errs.is_empty(), "expected at least one error");
1201 let error_msg = errs[0].to_string();
1202 assert!(
1203 error_msg.contains("Unknown type") && error_msg.contains("nonexistent_type"),
1204 "Error should mention unknown type. Got: {}",
1205 error_msg
1206 );
1207 }
1208
1209 #[test]
1210 fn test_invalid_primitive_type_name_should_error() {
1211 let code = r#"spec test
1213type invalid: choice -> option "a""#;
1214
1215 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1216 .unwrap()
1217 .specs;
1218 let spec = &specs[0];
1219
1220 let mut registry = test_registry();
1221 registry
1222 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1223 .unwrap();
1224
1225 let result = registry.resolve_types(&Arc::new(spec.clone()));
1226 assert!(result.is_err(), "Should reject invalid type base 'choice'");
1227
1228 let errs = result.unwrap_err();
1229 assert!(!errs.is_empty(), "expected at least one error");
1230 let error_msg = errs[0].to_string();
1231 assert!(
1232 error_msg.contains("Unknown type") && error_msg.contains("choice"),
1233 "Error should mention unknown type 'choice'. Got: {}",
1234 error_msg
1235 );
1236 }
1237
1238 #[test]
1239 fn test_unit_constraint_validation_errors_are_reported() {
1240 let code = r#"spec test
1242type money: scale
1243 -> unit eur 1.00
1244 -> unit usd 1.19
1245
1246type money2: money
1247 -> unit eur 1.20
1248 -> unit usd 1.21
1249 -> unit gbp 1.30"#;
1250
1251 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1252 .unwrap()
1253 .specs;
1254 let spec = &specs[0];
1255
1256 let mut registry = test_registry();
1257 for type_def in &spec.types {
1258 registry
1259 .register_type(&Arc::new(spec.clone()), type_def.clone())
1260 .unwrap();
1261 }
1262
1263 let result = registry.resolve_types(&Arc::new(spec.clone()));
1264 assert!(
1265 result.is_err(),
1266 "Expected unit constraint conflicts to error"
1267 );
1268
1269 let errs = result.unwrap_err();
1270 assert!(!errs.is_empty(), "expected at least one error");
1271 let error_msg = errs
1272 .iter()
1273 .map(ToString::to_string)
1274 .collect::<Vec<_>>()
1275 .join("; ");
1276 assert!(
1277 error_msg.contains("eur") || error_msg.contains("usd"),
1278 "Error should mention the conflicting units. Got: {}",
1279 error_msg
1280 );
1281 }
1282
1283 #[test]
1284 fn test_spec_level_unit_ambiguity_errors_are_reported() {
1285 let code = r#"spec test
1287type money_a: scale
1288 -> unit eur 1.00
1289 -> unit usd 1.19
1290
1291type money_b: scale
1292 -> unit eur 1.00
1293 -> unit usd 1.20
1294
1295type length_a: scale
1296 -> unit meter 1.0
1297
1298type length_b: scale
1299 -> unit meter 1.0"#;
1300
1301 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1302 .unwrap()
1303 .specs;
1304 let spec = &specs[0];
1305
1306 let mut registry = test_registry();
1307 for type_def in &spec.types {
1308 registry
1309 .register_type(&Arc::new(spec.clone()), type_def.clone())
1310 .unwrap();
1311 }
1312
1313 let result = registry.resolve_types(&Arc::new(spec.clone()));
1314 assert!(
1315 result.is_err(),
1316 "Expected ambiguous unit definitions to error"
1317 );
1318
1319 let errs = result.unwrap_err();
1320 assert!(!errs.is_empty(), "expected at least one error");
1321 let error_msg = errs
1322 .iter()
1323 .map(ToString::to_string)
1324 .collect::<Vec<_>>()
1325 .join("; ");
1326 assert!(
1327 error_msg.contains("eur") || error_msg.contains("usd") || error_msg.contains("meter"),
1328 "Error should mention at least one ambiguous unit. Got: {}",
1329 error_msg
1330 );
1331 }
1332
1333 #[test]
1334 fn test_number_type_cannot_have_units() {
1335 let code = r#"spec test
1336type price: number
1337 -> unit eur 1.00"#;
1338
1339 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1340 .unwrap()
1341 .specs;
1342 let spec = &specs[0];
1343
1344 let mut registry = test_registry();
1345 registry
1346 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1347 .unwrap();
1348
1349 let result = registry.resolve_types(&Arc::new(spec.clone()));
1350 assert!(result.is_err(), "Number types must reject unit commands");
1351
1352 let errs = result.unwrap_err();
1353 assert!(!errs.is_empty(), "expected at least one error");
1354 let error_msg = errs[0].to_string();
1355 assert!(
1356 error_msg.contains("unit") && error_msg.contains("number"),
1357 "Error should mention units are invalid on number. Got: {}",
1358 error_msg
1359 );
1360 }
1361
1362 #[test]
1363 fn test_scale_type_can_have_units() {
1364 let code = r#"spec test
1365type money: scale
1366 -> unit eur 1.00
1367 -> unit usd 1.19"#;
1368
1369 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1370 .unwrap()
1371 .specs;
1372 let spec = &specs[0];
1373
1374 let mut registry = test_registry();
1375 registry
1376 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1377 .unwrap();
1378
1379 let resolved = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
1380 let money_type = resolved.named_types.get("money").unwrap();
1381
1382 match &money_type.specifications {
1383 TypeSpecification::Scale { units, .. } => {
1384 assert_eq!(units.len(), 2);
1385 assert!(units.iter().any(|u| u.name == "eur"));
1386 assert!(units.iter().any(|u| u.name == "usd"));
1387 }
1388 other => panic!("Expected Scale type specifications, got {:?}", other),
1389 }
1390 }
1391
1392 #[test]
1393 fn test_extending_type_inherits_units() {
1394 let code = r#"spec test
1395type money: scale
1396 -> unit eur 1.00
1397 -> unit usd 1.19
1398
1399type my_money: money
1400 -> unit gbp 1.30"#;
1401
1402 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1403 .unwrap()
1404 .specs;
1405 let spec = &specs[0];
1406
1407 let mut registry = test_registry();
1408 for type_def in &spec.types {
1409 registry
1410 .register_type(&Arc::new(spec.clone()), type_def.clone())
1411 .unwrap();
1412 }
1413
1414 let resolved = registry.resolve_types(&Arc::new(spec.clone())).unwrap();
1415 let my_money_type = resolved.named_types.get("my_money").unwrap();
1416
1417 match &my_money_type.specifications {
1418 TypeSpecification::Scale { units, .. } => {
1419 assert_eq!(units.len(), 3);
1420 assert!(units.iter().any(|u| u.name == "eur"));
1421 assert!(units.iter().any(|u| u.name == "usd"));
1422 assert!(units.iter().any(|u| u.name == "gbp"));
1423 }
1424 other => panic!("Expected Scale type specifications, got {:?}", other),
1425 }
1426 }
1427
1428 #[test]
1429 fn test_duplicate_unit_in_same_type_is_rejected() {
1430 let code = r#"spec test
1431type money: scale
1432 -> unit eur 1.00
1433 -> unit eur 1.19"#;
1434
1435 let specs = parse(code, "test.lemma", &ResourceLimits::default())
1436 .unwrap()
1437 .specs;
1438 let spec = &specs[0];
1439
1440 let mut registry = test_registry();
1441 registry
1442 .register_type(&Arc::new(spec.clone()), spec.types[0].clone())
1443 .unwrap();
1444
1445 let result = registry.resolve_types(&Arc::new(spec.clone()));
1446 assert!(
1447 result.is_err(),
1448 "Duplicate units within a type should error"
1449 );
1450
1451 let errs = result.unwrap_err();
1452 assert!(!errs.is_empty(), "expected at least one error");
1453 let error_msg = errs[0].to_string();
1454 assert!(
1455 error_msg.contains("Duplicate unit")
1456 || error_msg.contains("duplicate")
1457 || error_msg.contains("already exists")
1458 || error_msg.contains("eur"),
1459 "Error should mention duplicate unit issue. Got: {}",
1460 error_msg
1461 );
1462 }
1463
1464 #[test]
1465 fn repro_named_type_source_location_panic() {
1466 use crate::parsing::ast::CommandArg;
1467 let code = r#"spec nettoloon
1468type geld: scale
1469 -> decimals 2
1470 -> unit eur 1.00
1471 -> minimum 0 eur
1472fact bruto_salaris: 0 eur"#;
1473 let specs = parse(code, "nettoloon.lemma", &ResourceLimits::default())
1474 .unwrap()
1475 .specs;
1476 let spec_arc = Arc::new(specs[0].clone());
1477 let mut registry = test_registry();
1478 for td in &spec_arc.types {
1479 registry.register_type(&spec_arc, td.clone()).unwrap();
1480 }
1481 let fact_ref = Reference::local("bruto_salaris".to_string());
1482 let inline_def = TypeDef::Inline {
1483 source_location: spec_arc.types[0].source_location().clone(),
1484 parent: "scale".to_string(),
1485 constraints: Some(vec![(
1486 "unit".to_string(),
1487 vec![
1488 CommandArg::Label("eur".to_string()),
1489 CommandArg::Number("1.00".to_string()),
1490 ],
1491 )]),
1492 fact_ref: fact_ref.clone(),
1493 from: None,
1494 };
1495 registry.register_type(&spec_arc, inline_def).unwrap();
1496 let _ = registry.resolve_types(&spec_arc);
1497 }
1498}