1use crate::ast::enumerated::{EnumVariant, EnumeratedType};
2use crate::ast::{DeclarationKind, Literal, eval_constant};
3use std::fmt::{Display, Formatter};
4use std::iter::zip;
5use std::ops::Deref;
6
7use crate::ast::domains::attrs::MSetAttr;
8use crate::ast::domains::attrs::PartitionAttr;
9use crate::ast::domains::attrs::PermutationAttr;
10use crate::ast::domains::attrs::SetAttr;
11use crate::ast::domains::ground::{
12 FieldGround, int_type_string, representation_attribute, write_int_domain,
13};
14use crate::ast::records::Field;
15use crate::ast::{
16 DomainOpError, Expression, FuncAttr, Moo, Reference, RelAttr, ReturnType, SequenceAttr,
17 Typeable,
18 domains::{DomainPtr, GroundDomain, int_val::IntVal, range::Range},
19 pretty::pretty_vec,
20};
21use crate::bug;
22
23use funcmap::{FuncMap, TryFuncMap};
24use itertools::Itertools;
25use polyquine::Quine;
26use serde::{Deserialize, Serialize};
27use uniplate::Uniplate;
28
29fn eval_expr_to_enum_variant(expr: &Expression, expected: &Moo<EnumeratedType>) -> Option<u32> {
30 let Literal::EnumVariant(EnumVariant { ty, variant }) = eval_constant(expr)? else {
31 bug!("Expected enum variant expression, got: {expr}");
32 };
33
34 if ty != *expected {
35 bug!("Expected variant of enum {expected}, got {ty}:");
36 }
37
38 Some(variant)
39}
40
41#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Uniplate)]
42#[biplate(to=Expression)]
43#[biplate(to=Reference)]
44pub struct EnumVariantVal(pub Reference);
45
46impl EnumVariantVal {
47 fn resolve(&self, expected: &Moo<EnumeratedType>) -> Option<u32> {
48 let re = &self.0;
49 match re.ptr.kind().deref() {
50 DeclarationKind::ValueLetting(expr, _)
51 | DeclarationKind::TemporaryValueLetting(expr)
52 | DeclarationKind::QuantifiedExpr(expr) => eval_expr_to_enum_variant(expr, expected),
53 DeclarationKind::Given(_) => None,
55 DeclarationKind::Quantified(inner) => {
56 if let Some(generator) = inner.generator()
57 && let Some(expr) = generator.as_value_letting()
58 {
59 eval_expr_to_enum_variant(&expr, expected)
60 } else {
61 None
62 }
63 }
64 DeclarationKind::Find(_) | DeclarationKind::FindAuxiliary(_) => None,
66 DeclarationKind::DomainLetting(_)
67 | DeclarationKind::EnumeratedType(_)
68 | DeclarationKind::UnnamedType(_) => {
69 bug!("Expected integer expression, given, or letting inside enum domain; Got: {re}")
70 }
71 }
72 }
73}
74
75impl Range<EnumVariantVal> {
76 pub fn resolve(&self, expected: &Moo<EnumeratedType>) -> Option<Range<u32>> {
77 match self {
78 Range::Single(x) => Some(Range::Single(x.resolve(expected)?)),
79 Range::Bounded(l, r) => {
80 Some(Range::Bounded(l.resolve(expected)?, r.resolve(expected)?))
81 }
82 Range::UnboundedL(r) => Some(Range::UnboundedL(r.resolve(expected)?)),
83 Range::UnboundedR(l) => Some(Range::UnboundedR(l.resolve(expected)?)),
84 Range::Unbounded => Some(Range::Unbounded),
85 }
86 }
87}
88
89impl Display for EnumVariantVal {
90 fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
91 write!(f, "{}", self.0)
92 }
95}
96
97pub(super) type FieldUnresolved = Field<DomainPtr>;
98
99impl From<FieldGround> for FieldUnresolved {
100 fn from(v: FieldGround) -> Self {
101 v.func_map(DomainPtr::from)
102 }
103}
104
105impl TryFrom<FieldUnresolved> for FieldGround {
106 type Error = DomainOpError;
107 fn try_from(v: FieldUnresolved) -> Result<Self, Self::Error> {
108 v.try_func_map(DomainPtr::try_into)
109 }
110}
111
112#[derive(Clone, Debug, PartialEq, Eq, Hash, Serialize, Deserialize, Quine, Uniplate)]
113#[path_prefix(conjure_cp::ast)]
114#[biplate(to=Expression)]
115#[biplate(to=Reference)]
116#[biplate(to=IntVal)]
117#[biplate(to=DomainPtr)]
118pub enum UnresolvedDomain {
120 Int(Vec<Range<IntVal>>, Option<String>),
122 IntFromValues(Moo<Expression>),
127 Tuple(Vec<DomainPtr>, Option<String>),
129 Record(Vec<FieldUnresolved>, Option<String>),
131 Variant(Vec<FieldUnresolved>, Option<String>),
134 Matrix(DomainPtr, Vec<DomainPtr>, Option<String>),
137 Sequence(SequenceAttr<IntVal>, DomainPtr),
138 Set(SetAttr<IntVal>, DomainPtr),
140 MSet(MSetAttr<IntVal>, DomainPtr),
141 Function(FuncAttr<IntVal>, DomainPtr, DomainPtr),
143 Relation(RelAttr<IntVal>, Vec<DomainPtr>),
145 Partition(PartitionAttr<IntVal>, DomainPtr),
146 #[polyquine_skip]
148 EnumeratedType(Moo<EnumeratedType>, Vec<Range<EnumVariantVal>>),
149 #[polyquine_skip]
151 UnnamedType(Reference),
152 Permutation(PermutationAttr<IntVal>, DomainPtr),
153 #[polyquine_skip]
155 Reference(Reference),
156}
157
158impl UnresolvedDomain {
159 pub(super) fn from_ground(domain: &GroundDomain) -> Option<UnresolvedDomain> {
160 let unresolved = match domain {
161 GroundDomain::Empty(_)
162 | GroundDomain::Bool
163 | GroundDomain::EnumeratedType(_, _)
164 | GroundDomain::UnnamedType(_) => return None,
165 GroundDomain::Int(ranges, representation) => UnresolvedDomain::Int(
166 ranges.iter().cloned().map(Into::into).collect(),
167 representation.clone(),
168 ),
169 GroundDomain::Tuple(inners, representation) => UnresolvedDomain::Tuple(
170 inners.iter().map(DomainPtr::from).collect(),
171 representation.clone(),
172 ),
173 GroundDomain::Record(fields, representation) => UnresolvedDomain::Record(
174 fields.iter().cloned().map(Into::into).collect(),
175 representation.clone(),
176 ),
177 GroundDomain::Variant(fields, representation) => UnresolvedDomain::Variant(
178 fields.iter().cloned().map(Into::into).collect(),
179 representation.clone(),
180 ),
181 GroundDomain::Matrix(inner, indices, representation) => UnresolvedDomain::Matrix(
182 DomainPtr::from(inner),
183 indices.iter().map(DomainPtr::from).collect(),
184 representation.clone(),
185 ),
186 GroundDomain::Sequence(attributes, inner) => {
187 UnresolvedDomain::Sequence(attributes.clone().into(), DomainPtr::from(inner))
188 }
189 GroundDomain::Set(attributes, inner) => {
190 UnresolvedDomain::Set(attributes.clone().into(), DomainPtr::from(inner))
191 }
192 GroundDomain::MSet(attributes, inner) => {
193 UnresolvedDomain::MSet(attributes.clone().into(), DomainPtr::from(inner))
194 }
195 GroundDomain::Function(attributes, domain, codomain) => UnresolvedDomain::Function(
196 attributes.clone().into(),
197 DomainPtr::from(domain),
198 DomainPtr::from(codomain),
199 ),
200 GroundDomain::Relation(attributes, inners) => UnresolvedDomain::Relation(
201 attributes.clone().into(),
202 inners.iter().map(DomainPtr::from).collect(),
203 ),
204 GroundDomain::Partition(attributes, inner) => {
205 UnresolvedDomain::Partition(attributes.clone().into(), DomainPtr::from(inner))
206 }
207 GroundDomain::Permutation(attributes, inner) => {
208 UnresolvedDomain::Permutation(attributes.clone().into(), DomainPtr::from(inner))
209 }
210 };
211
212 Some(unresolved)
213 }
214
215 pub fn has_int_from_values(&self) -> bool {
220 match self {
221 UnresolvedDomain::IntFromValues(_) => true,
222 UnresolvedDomain::Int(_, _) => false,
223 UnresolvedDomain::Tuple(inners, _) | UnresolvedDomain::Relation(_, inners) => {
224 inners.iter().any(domain_has_int_from_values)
225 }
226 UnresolvedDomain::Record(entries, _) | UnresolvedDomain::Variant(entries, _) => entries
227 .iter()
228 .any(|entry| domain_has_int_from_values(&entry.value)),
229 UnresolvedDomain::Matrix(value, indices, _) => {
230 domain_has_int_from_values(value) || indices.iter().any(domain_has_int_from_values)
231 }
232 UnresolvedDomain::Sequence(_, inner)
233 | UnresolvedDomain::Set(_, inner)
234 | UnresolvedDomain::MSet(_, inner)
235 | UnresolvedDomain::Partition(_, inner)
236 | UnresolvedDomain::Permutation(_, inner) => domain_has_int_from_values(inner),
237 UnresolvedDomain::Function(_, from, to) => {
238 domain_has_int_from_values(from) || domain_has_int_from_values(to)
239 }
240 UnresolvedDomain::Reference(_)
241 | UnresolvedDomain::EnumeratedType(_, _)
242 | UnresolvedDomain::UnnamedType(_) => false,
243 }
244 }
245
246 pub fn resolve(&self) -> Result<GroundDomain, DomainOpError> {
247 match self {
248 UnresolvedDomain::IntFromValues(expr) => {
249 let values = crate::ast::eval::generator_values_from_expr(expr)
250 .ok_or(DomainOpError::NotGround)?;
251 let mut ranges = Vec::with_capacity(values.len());
252 for value in values {
253 let crate::ast::Literal::Int(value) = value else {
254 return Err(DomainOpError::WrongType);
255 };
256 ranges.push(Range::Single(value));
257 }
258 Ok(GroundDomain::Int(Range::squeeze(&ranges), None))
259 }
260 UnresolvedDomain::Int(rngs, representation) => rngs
261 .iter()
262 .map(Range::<IntVal>::resolve)
263 .collect::<Result<Vec<_>, _>>()
264 .map(|ranges| {
265 let ranges = ranges
266 .into_iter()
267 .filter(
268 |range| !matches!(range, Range::Bounded(lower, upper) if lower > upper),
269 )
270 .collect::<Vec<_>>();
271 GroundDomain::Int(Range::squeeze(&ranges), representation.clone())
272 }),
273 UnresolvedDomain::Tuple(inners, representation) => inners
274 .iter()
275 .map(DomainPtr::resolve)
276 .collect::<Result<_, _>>()
277 .map(|inners| GroundDomain::Tuple(inners, representation.clone())),
278 UnresolvedDomain::Record(entries, representation) => entries
279 .iter()
280 .map(|f| {
281 f.value.resolve().map(|gd| FieldGround {
282 name: f.name.clone(),
283 value: gd,
284 })
285 })
286 .collect::<Result<_, _>>()
287 .map(|entries| GroundDomain::Record(entries, representation.clone())),
288 UnresolvedDomain::Variant(entries, representation) => entries
289 .iter()
290 .map(|f| {
291 f.value.resolve().map(|gd| FieldGround {
292 name: f.name.clone(),
293 value: gd,
294 })
295 })
296 .collect::<Result<_, _>>()
297 .map(|entries| GroundDomain::Variant(entries, representation.clone())),
298 UnresolvedDomain::Matrix(inner, idx_doms, representation) => {
299 let inner_gd = inner.resolve()?;
300 idx_doms
301 .iter()
302 .map(DomainPtr::resolve)
303 .collect::<Result<_, _>>()
304 .map(|idx| GroundDomain::Matrix(inner_gd, idx, representation.clone()))
305 }
306 UnresolvedDomain::Sequence(attr, inner) => {
307 Ok(GroundDomain::Sequence(attr.resolve()?, inner.resolve()?))
308 }
309 UnresolvedDomain::Set(attr, inner) => {
310 Ok(GroundDomain::Set(attr.resolve()?, inner.resolve()?))
311 }
312 UnresolvedDomain::MSet(attr, inner) => {
313 Ok(GroundDomain::MSet(attr.resolve()?, inner.resolve()?))
314 }
315 UnresolvedDomain::Function(attr, dom, cdom) => Ok(GroundDomain::Function(
316 attr.resolve()?,
317 dom.resolve()?,
318 cdom.resolve()?,
319 )),
320 UnresolvedDomain::Relation(attr, inners) => {
321 let resolved_attr = attr.resolve()?;
322 inners
323 .iter()
324 .map(DomainPtr::resolve)
325 .collect::<Result<_, _>>()
326 .map(|items| GroundDomain::Relation(resolved_attr, items))
327 }
328 UnresolvedDomain::Partition(attr, inner) => {
329 Ok(GroundDomain::Partition(attr.resolve()?, inner.resolve()?))
330 }
331 UnresolvedDomain::Permutation(attr, inner) => {
332 Ok(GroundDomain::Permutation(attr.resolve()?, inner.resolve()?))
333 }
334 UnresolvedDomain::Reference(re) => re
335 .ptr
336 .as_domain_letting()
337 .unwrap_or_else(|| {
338 bug!("Reference domain should point to domain letting, but got {re}")
339 })
340 .resolve()
341 .map(Moo::unwrap_or_clone),
342 UnresolvedDomain::EnumeratedType(et, ranges) => {
343 let ranges: Vec<_> = ranges
344 .clone()
345 .into_iter()
346 .map(|r| r.resolve(et))
347 .collect::<Option<Vec<_>>>()
348 .ok_or(DomainOpError::NotGround)?;
349 Ok(GroundDomain::EnumeratedType(et.clone(), ranges))
350 }
351 UnresolvedDomain::UnnamedType(decl) => {
352 let ut = *decl
353 .ptr
354 .as_unnamed_type()
355 .unwrap_or_else(|| {
356 bug!("Unnamed type domain should point to an unnamed type declaration, but got {decl}")
357 });
358
359 Ok(GroundDomain::UnnamedType(Moo::new(
360 crate::ast::unnamed::UnnamedType {
361 name: decl.ptr.name().clone(),
362 size: ut,
363 },
364 )))
365 }
366 }
367 }
368
369 pub(super) fn union_unresolved(
370 &self,
371 other: &UnresolvedDomain,
372 ) -> Result<UnresolvedDomain, DomainOpError> {
373 match (self, other) {
376 (UnresolvedDomain::Int(lhs, _), UnresolvedDomain::Int(rhs, _)) => {
377 let merged = lhs.iter().chain(rhs.iter()).cloned().collect_vec();
378 Ok(UnresolvedDomain::Int(merged, None))
379 }
380 (UnresolvedDomain::IntFromValues(_), _) | (_, UnresolvedDomain::IntFromValues(_)) => {
381 Err(DomainOpError::NotGround)
382 }
383 (UnresolvedDomain::Int(_, _), _) | (_, UnresolvedDomain::Int(_, _)) => {
384 Err(DomainOpError::WrongType)
385 }
386 (UnresolvedDomain::Tuple(lhs, _), UnresolvedDomain::Tuple(rhs, _))
387 if lhs.len() == rhs.len() =>
388 {
389 let mut merged = Vec::new();
390 for (l, r) in zip(lhs, rhs) {
391 merged.push(l.union(r)?)
392 }
393 Ok(UnresolvedDomain::Tuple(merged, None))
394 }
395 (UnresolvedDomain::Tuple(_, _), _) | (_, UnresolvedDomain::Tuple(_, _)) => {
396 Err(DomainOpError::WrongType)
397 }
398 (UnresolvedDomain::Matrix(in1, idx1, _), UnresolvedDomain::Matrix(in2, idx2, _))
399 if idx1 == idx2 =>
400 {
401 Ok(UnresolvedDomain::Matrix(
402 in1.union(in2)?,
403 idx1.clone(),
404 None,
405 ))
406 }
407 (UnresolvedDomain::Matrix(_, _, _), _) | (_, UnresolvedDomain::Matrix(_, _, _)) => {
408 Err(DomainOpError::WrongType)
409 }
410 (UnresolvedDomain::Set(_, in1), UnresolvedDomain::Set(_, in2)) => {
411 Ok(UnresolvedDomain::Set(SetAttr::default(), in1.union(in2)?))
412 }
413 (UnresolvedDomain::Set(_, _), _) | (_, UnresolvedDomain::Set(_, _)) => {
414 Err(DomainOpError::WrongType)
415 }
416 (UnresolvedDomain::MSet(_, in1), UnresolvedDomain::MSet(_, in2)) => {
417 Ok(UnresolvedDomain::MSet(MSetAttr::default(), in1.union(in2)?))
418 }
419 (UnresolvedDomain::MSet(_, _), _) | (_, UnresolvedDomain::MSet(_, _)) => {
420 Err(DomainOpError::WrongType)
421 }
422 (UnresolvedDomain::Relation(_, in1s), UnresolvedDomain::Relation(_, in2s)) => {
423 let mut inners = Vec::new();
424 for (in1, in2) in in1s.iter().zip(in2s.iter()) {
425 inners.push(in1.union(in2)?)
426 }
427 Ok(UnresolvedDomain::Relation(RelAttr::default(), inners))
428 }
429 (UnresolvedDomain::Relation(_, _), _) | (_, UnresolvedDomain::Relation(_, _)) => {
430 Err(DomainOpError::WrongType)
431 }
432 #[allow(unreachable_patterns)]
434 (UnresolvedDomain::Record(_, _), _) | (_, UnresolvedDomain::Record(_, _)) => {
435 Err(DomainOpError::WrongType)
436 }
437 #[allow(unreachable_patterns)]
438 (UnresolvedDomain::Variant(_, _), _) | (_, UnresolvedDomain::Variant(_, _)) => {
439 Err(DomainOpError::WrongType)
440 }
441 #[allow(unreachable_patterns)]
442 (UnresolvedDomain::Sequence(_, _), _) | (_, UnresolvedDomain::Sequence(_, _)) => {
443 Err(DomainOpError::WrongType)
444 }
445 #[allow(unreachable_patterns)]
446 (UnresolvedDomain::EnumeratedType(_, _), _)
447 | (_, UnresolvedDomain::EnumeratedType(_, _)) => Err(DomainOpError::WrongType),
448 #[allow(unreachable_patterns)]
449 (UnresolvedDomain::UnnamedType(_), _) | (_, UnresolvedDomain::UnnamedType(_)) => {
450 Err(DomainOpError::WrongType)
451 }
452 (UnresolvedDomain::Function(_, _, _), _) | (_, UnresolvedDomain::Function(_, _, _)) => {
453 Err(DomainOpError::WrongType)
454 }
455 #[allow(unreachable_patterns)]
456 (UnresolvedDomain::Partition(_, _), _) | (_, UnresolvedDomain::Partition(_, _)) => {
457 Err(DomainOpError::WrongType)
458 }
459 #[allow(unreachable_patterns)]
460 (UnresolvedDomain::Permutation(_, _), _) | (_, UnresolvedDomain::Permutation(_, _)) => {
461 Err(DomainOpError::WrongType)
462 }
463 #[allow(unreachable_patterns)]
465 (UnresolvedDomain::Reference(_), _) | (_, UnresolvedDomain::Reference(_)) => {
466 Err(DomainOpError::NotGround)
467 }
468 }
469 }
470
471 pub fn element_domain(&self) -> Option<DomainPtr> {
472 match self {
473 UnresolvedDomain::Matrix(inner, _, _) => Some(inner.clone()),
474 UnresolvedDomain::Sequence(attr, inner_dom) => {
478 let max = match &attr.size {
479 Range::Single(max) | Range::UnboundedL(max) | Range::Bounded(_, max) => {
480 max.clone()
481 }
482 Range::UnboundedR(_) | Range::Unbounded => return None,
483 };
484 let positions = Moo::new(crate::ast::Domain::Unresolved(Moo::new(
485 UnresolvedDomain::Int(vec![Range::Bounded(IntVal::new_const(1), max)], None),
486 )));
487 Some(Moo::new(crate::ast::Domain::Unresolved(Moo::new(
488 UnresolvedDomain::Tuple(vec![positions, inner_dom.clone()], None),
489 ))))
490 }
491 UnresolvedDomain::Set(_, inner_dom) => Some(inner_dom.clone()),
492 _ => None,
493 }
494 }
495
496 pub fn has_representation_preference(&self) -> bool {
498 match self {
499 UnresolvedDomain::Int(_, representation) => representation.is_some(),
500 UnresolvedDomain::IntFromValues(_)
501 | UnresolvedDomain::EnumeratedType(_, _)
502 | UnresolvedDomain::UnnamedType(_) => false,
503 UnresolvedDomain::Tuple(inners, representation) => {
504 representation.is_some() || inners.iter().any(|d| d.has_representation_preference())
505 }
506 UnresolvedDomain::Record(entries, representation) => {
507 representation.is_some()
508 || entries
509 .iter()
510 .any(|f| f.value.has_representation_preference())
511 }
512 UnresolvedDomain::Variant(entries, representation) => {
513 representation.is_some()
514 || entries
515 .iter()
516 .any(|f| f.value.has_representation_preference())
517 }
518 UnresolvedDomain::Matrix(inner, idxs, representation) => {
519 representation.is_some()
520 || inner.has_representation_preference()
521 || idxs.iter().any(|d| d.has_representation_preference())
522 }
523 UnresolvedDomain::Sequence(attr, inner) => {
524 attr.representation.is_some() || inner.has_representation_preference()
525 }
526 UnresolvedDomain::Set(attr, inner) => {
527 attr.representation.is_some() || inner.has_representation_preference()
528 }
529 UnresolvedDomain::MSet(attr, inner) => {
530 attr.representation.is_some() || inner.has_representation_preference()
531 }
532 UnresolvedDomain::Function(attr, dom, cdom) => {
533 attr.representation.is_some()
534 || dom.has_representation_preference()
535 || cdom.has_representation_preference()
536 }
537 UnresolvedDomain::Relation(attr, inners) => {
538 attr.representation.is_some()
539 || inners.iter().any(|d| d.has_representation_preference())
540 }
541 UnresolvedDomain::Partition(attr, inner) => {
542 attr.representation.is_some() || inner.has_representation_preference()
543 }
544 UnresolvedDomain::Permutation(attr, inner) => {
545 attr.representation.is_some() || inner.has_representation_preference()
546 }
547 UnresolvedDomain::Reference(re) => re
548 .domain()
549 .is_some_and(|d| d.has_representation_preference()),
550 }
551 }
552
553 pub fn as_type_string(&self) -> String {
555 match self {
556 UnresolvedDomain::Int(_, representation) => int_type_string(representation.as_deref()),
557 UnresolvedDomain::IntFromValues(_) => "int".to_string(),
558 UnresolvedDomain::EnumeratedType(ty, _) => ty.to_string(),
559 UnresolvedDomain::UnnamedType(_) => "unnamed type".to_string(),
560 UnresolvedDomain::Tuple(inners, representation) => {
561 let args = representation
562 .iter()
563 .map(|r| format!("representation {r}"))
564 .chain(inners.iter().map(|d| d.as_type_string()))
565 .join(", ");
566 format!("tuple ({args})")
567 }
568 UnresolvedDomain::Record(entries, representation) => {
569 let inners = entries
570 .iter()
571 .map(|f| format!("{}: {}", f.name, f.value.as_type_string()))
572 .join(", ");
573 format!(
574 "record{} {{{inners}}}",
575 representation_attribute(representation)
576 )
577 }
578 UnresolvedDomain::Variant(entries, representation) => {
579 let inners = entries
580 .iter()
581 .map(|f| format!("{}: {}", f.name, f.value.as_type_string()))
582 .join(", ");
583 format!(
584 "variant{} {{{inners}}}",
585 representation_attribute(representation)
586 )
587 }
588 UnresolvedDomain::Matrix(inner, idxs, representation) => {
589 let idxs = idxs.iter().map(|d| d.as_type_string()).join(", ");
590 format!(
591 "matrix{} indexed by [{idxs}] of {}",
592 representation_attribute(representation),
593 inner.as_type_string()
594 )
595 }
596 UnresolvedDomain::Sequence(attrs, inner) => format!(
597 "sequence{} of {}",
598 representation_attribute(&attrs.representation),
599 inner.as_type_string()
600 ),
601 UnresolvedDomain::Set(attrs, inner) => {
602 let mut out = String::from("set");
603 if let Some(repr) = &attrs.representation {
604 out.push_str(" (representation ");
605 out.push_str(repr);
606 out.push(')');
607 }
608 out.push_str(" of ");
609 out.push_str(&inner.as_type_string());
610 out
611 }
612 UnresolvedDomain::MSet(attrs, inner) => {
613 let mut out = String::from("mset");
614 if let Some(repr) = &attrs.representation {
615 out.push_str(" (representation ");
616 out.push_str(repr);
617 out.push(')');
618 }
619 out.push_str(" of ");
620 out.push_str(&inner.as_type_string());
621 out
622 }
623 UnresolvedDomain::Function(attr, dom, cdom) => {
624 format!(
625 "function{} {} --> {}",
626 representation_attribute(&attr.representation),
627 dom.as_type_string(),
628 cdom.as_type_string()
629 )
630 }
631 UnresolvedDomain::Relation(attr, inners) => {
632 format!(
633 "relation{} of ({})",
634 representation_attribute(&attr.representation),
635 inners.iter().map(|d| d.as_type_string()).join(" * ")
636 )
637 }
638 UnresolvedDomain::Partition(attr, inner) => {
639 format!(
640 "partition{} from {}",
641 representation_attribute(&attr.representation),
642 inner.as_type_string()
643 )
644 }
645 UnresolvedDomain::Permutation(attr, inner) => {
646 format!(
647 "permutation{} of {}",
648 representation_attribute(&attr.representation),
649 inner.as_type_string()
650 )
651 }
652 UnresolvedDomain::Reference(re) => re.to_string(),
653 }
654 }
655}
656
657impl Typeable for UnresolvedDomain {
658 fn return_type(&self) -> ReturnType {
659 match self {
660 UnresolvedDomain::Int(_, _) | UnresolvedDomain::IntFromValues(_) => ReturnType::Int,
661 UnresolvedDomain::Tuple(inners, _) => {
662 let mut inner_types = Vec::new();
663 for inner in inners {
664 inner_types.push(inner.return_type());
665 }
666 ReturnType::Tuple(inner_types)
667 }
668 UnresolvedDomain::Record(entries, _) => {
669 let mut entry_types = Vec::new();
670 for entry in entries {
671 entry_types.push(entry.clone().func_map(|x| x.return_type()));
672 }
673 entry_types.sort();
674 ReturnType::Record(entry_types)
675 }
676 UnresolvedDomain::Variant(entries, _) => {
677 let mut entry_types = Vec::new();
678 for entry in entries {
679 entry_types.push(entry.clone().func_map(|x| x.return_type()));
680 }
681 ReturnType::Variant(entry_types)
682 }
683 UnresolvedDomain::Matrix(inner, _idx, _) => {
684 ReturnType::Matrix(Box::new(inner.return_type()))
685 }
686 UnresolvedDomain::Sequence(_attr, inner) => {
687 ReturnType::Sequence(Box::new(inner.return_type()))
688 }
689 UnresolvedDomain::Set(_attr, inner) => ReturnType::Set(Box::new(inner.return_type())),
690 UnresolvedDomain::MSet(_attr, inner) => ReturnType::MSet(Box::new(inner.return_type())),
691 UnresolvedDomain::Function(_, dom, cdom) => {
692 ReturnType::Function(Box::new(dom.return_type()), Box::new(cdom.return_type()))
693 }
694 UnresolvedDomain::Relation(_, inners) => {
695 let mut inner_types = Vec::new();
696 for inner in inners {
697 inner_types.push(inner.return_type());
698 }
699 ReturnType::Relation(inner_types)
700 }
701 UnresolvedDomain::EnumeratedType(et, _) => ReturnType::EnumeratedType(et.clone()),
702 UnresolvedDomain::UnnamedType(reference) => reference.ptr.return_type(),
703 UnresolvedDomain::Partition(_, inner) => {
704 ReturnType::Partition(Box::new(inner.return_type()))
705 }
706 UnresolvedDomain::Permutation(_, inner) => {
707 ReturnType::Permutation(Box::new(inner.return_type()))
708 }
709 UnresolvedDomain::Reference(re) => re.return_type(),
710 }
711 }
712}
713
714impl Display for FieldUnresolved {
715 fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
716 write!(f, "{}: {}", self.name, self.value)
717 }
718}
719
720impl Display for UnresolvedDomain {
721 fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
722 match &self {
723 UnresolvedDomain::Int(ranges, representation) => {
724 write_int_domain(f, ranges, representation.as_deref())
725 }
726 UnresolvedDomain::IntFromValues(expr) => write!(f, "int({expr})"),
727 UnresolvedDomain::Tuple(domains, representation) => {
728 let members = domains.iter().join(",");
730 match representation {
731 Some(representation) if members.is_empty() => {
732 write!(f, "tuple (representation {representation})")
733 }
734 Some(representation) => {
735 write!(f, "tuple (representation {representation}, {members})")
736 }
737 None => write!(f, "tuple ({members})"),
738 }
739 }
740 UnresolvedDomain::Record(entries, representation) => {
741 let inners = entries.iter().map(|t| format!("{}", t)).join(", ");
742 let attrs = representation_attribute(representation);
743 write!(f, "record{attrs} {{{inners}}}",)
744 }
745 UnresolvedDomain::Variant(entries, representation) => {
746 let inners = entries.iter().map(|t| format!("{}", t)).join(", ");
747 let attrs = representation_attribute(representation);
748 write!(f, "variant{attrs} {{{inners}}}",)
749 }
750 UnresolvedDomain::Matrix(value_domain, index_domains, representation) => {
751 write!(
752 f,
753 "matrix{} indexed by {} of {value_domain}",
754 representation_attribute(representation),
755 pretty_vec(&index_domains.iter().collect_vec())
756 )
757 }
758 UnresolvedDomain::Sequence(attrs, inner_dom) => {
759 write!(f, "sequence {attrs} of {inner_dom}")
760 }
761 UnresolvedDomain::Set(attrs, inner_dom) => {
762 write!(f, "set")?;
763 let attrs = attrs.to_string();
764 if attrs.is_empty() {
765 write!(f, " of {inner_dom}")
766 } else {
767 write!(f, " {attrs} of {inner_dom}")
768 }
769 }
770 UnresolvedDomain::MSet(attrs, inner_dom) => {
771 write!(f, "mset")?;
772 let attrs = attrs.to_string();
773 if attrs.is_empty() {
774 write!(f, " of {inner_dom}")
775 } else {
776 write!(f, " {attrs} of {inner_dom}")
777 }
778 }
779 UnresolvedDomain::Function(attribute, domain, codomain) => {
780 write!(f, "function {} {} --> {} ", attribute, domain, codomain)
781 }
782 UnresolvedDomain::Relation(attrs, domains) => {
783 write!(f, "relation {} of ({})", attrs, domains.iter().join(" * "))
784 }
785 UnresolvedDomain::EnumeratedType(ty, ranges) => {
786 if !ranges.is_empty() && ranges.iter().all(Range::is_lower_or_upper_bounded) {
787 let rngs: String = ranges.iter().map(|r| format!("{r}")).join(", ");
788 write!(f, "{}({})", ty.name, rngs)
789 } else {
790 write!(f, "{}", ty.name)
791 }
792 }
793 UnresolvedDomain::UnnamedType(reference) => {
794 write!(f, "{reference}")
795 }
796 UnresolvedDomain::Partition(attrs, inner_dom) => {
797 write!(f, "partition {attrs} from {inner_dom}")
798 }
799 UnresolvedDomain::Permutation(attrs, inner_dom) => {
800 write!(f, "permutation {attrs} of {inner_dom}")
801 }
802 UnresolvedDomain::Reference(re) => write!(f, "{re}"),
803 }
804 }
805}
806
807pub fn domain_has_int_from_values(domain: &DomainPtr) -> bool {
809 match &**domain {
810 crate::ast::Domain::Ground(_) => false,
811 crate::ast::Domain::Unresolved(unresolved) => unresolved.has_int_from_values(),
812 }
813}