Skip to main content

conjure_cp_core/ast/
declaration.rs

1use super::categories::{Category, CategoryOf};
2use super::name::Name;
3use super::serde::{DefaultWithId, HasId, IdPtr, ObjId, PtrAsInner};
4use super::{
5    DecisionVariable, DomainPtr, Expression, GroundDomain, HasDomain, Moo, RecordEntry, ReturnType,
6    Typeable,
7};
8use parking_lot::{
9    MappedRwLockReadGuard, MappedRwLockWriteGuard, RwLock, RwLockReadGuard, RwLockWriteGuard,
10};
11use serde::{Deserialize, Serialize};
12use serde_with::serde_as;
13use std::any::TypeId;
14use std::fmt::{Debug, Display};
15use std::mem;
16use std::sync::Arc;
17use std::sync::atomic::{AtomicU32, Ordering};
18use uniplate::{Biplate, Tree, Uniplate};
19
20/// Global counter of declarations.
21/// Note that the counter is shared between all threads
22/// Thus, when running multiple models in parallel, IDs may
23/// be different with every run depending on scheduling order
24static DECLARATION_PTR_ID_COUNTER: AtomicU32 = const { AtomicU32::new(0) };
25
26#[doc(hidden)]
27/// Resets the id counter of `DeclarationPtr` to 0.
28///
29/// This is probably always a bad idea.
30pub fn reset_declaration_id_unchecked() {
31    let _ = DECLARATION_PTR_ID_COUNTER.swap(0, Ordering::Relaxed);
32}
33
34/// A shared pointer to a [`Declaration`].
35///
36/// Two declaration pointers are equal if they point to the same underlying declaration.
37///
38/// # Id
39///
40///  The id of `DeclarationPtr` obeys the following invariants:
41///
42/// 1. Declaration pointers have the same id if they point to the same
43///    underlying declaration.
44///
45/// 2. The id is immutable.
46///
47/// 3. Changing the declaration pointed to by the declaration pointer does not change the id. This
48///    allows declarations to be updated by replacing them with a newer version of themselves.
49///
50/// `Ord`, `Hash`, and `Eq` use id for comparisons.
51/// # Serde
52///
53/// Declaration pointers can be serialised using the following serializers:
54///
55/// + [`DeclarationPtrFull`](serde::DeclarationPtrFull)
56/// + [`DeclarationPtrAsId`](serde::DeclarationPtrAsId)
57///
58/// See their documentation for more information.
59#[derive(Clone, Debug)]
60pub struct DeclarationPtr
61where
62    Self: Send + Sync,
63{
64    // the shared bits of the pointer
65    inner: Arc<DeclarationPtrInner>,
66}
67
68// The bits of a declaration that are shared between all pointers.
69#[derive(Debug)]
70struct DeclarationPtrInner {
71    // We don't want this to be mutable, as `HashMap` and `BTreeMap` rely on the hash or order of
72    // keys to be unchanging.
73    //
74    // See:  https://rust-lang.github.io/rust-clippy/master/index.html#mutable_key_type
75    id: ObjId,
76
77    // The contents of the declaration itself should be mutable.
78    value: RwLock<Declaration>,
79}
80
81impl DeclarationPtrInner {
82    fn new(value: RwLock<Declaration>) -> Arc<DeclarationPtrInner> {
83        Arc::new(DeclarationPtrInner {
84            id: ObjId {
85                type_name: ustr::ustr(DeclarationPtr::TYPE_NAME),
86                object_id: DECLARATION_PTR_ID_COUNTER.fetch_add(1, Ordering::Relaxed),
87            },
88            value,
89        })
90    }
91
92    // SAFETY: only use if you are really really sure you arn't going to break the id invariants of
93    // DeclarationPtr and HasId!
94    fn new_with_id_unchecked(value: RwLock<Declaration>, id: ObjId) -> Arc<DeclarationPtrInner> {
95        Arc::new(DeclarationPtrInner { id, value })
96    }
97}
98
99#[allow(dead_code)]
100impl DeclarationPtr {
101    /******************************/
102    /*        Constructors        */
103    /******************************/
104
105    /// Creates a `DeclarationPtr` for the given `Declaration`.
106    fn from_declaration(declaration: Declaration) -> DeclarationPtr {
107        DeclarationPtr {
108            inner: DeclarationPtrInner::new(RwLock::new(declaration)),
109        }
110    }
111
112    /// Creates a new declaration.
113    ///
114    /// # Examples
115    ///
116    /// ```
117    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
118    ///
119    /// // letting MyDomain be int(1..5)
120    /// let declaration = DeclarationPtr::new(
121    ///     Name::User("MyDomain".into()),
122    ///     DeclarationKind::DomainLetting(Domain::int(vec![
123    ///         Range::Bounded(1,5)])));
124    /// ```
125    pub fn new(name: Name, kind: DeclarationKind) -> DeclarationPtr {
126        DeclarationPtr::from_declaration(Declaration::new(name, kind))
127    }
128
129    /// Creates a new find declaration.
130    ///
131    /// # Examples
132    ///
133    /// ```
134    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
135    ///
136    /// // find x: int(1..5)
137    /// let declaration = DeclarationPtr::new_find(
138    ///     Name::User("x".into()),
139    ///     Domain::int(vec![Range::Bounded(1,5)]));
140    ///
141    /// ```
142    pub fn new_find(name: Name, domain: DomainPtr) -> DeclarationPtr {
143        let kind = DeclarationKind::Find(DecisionVariable::new(domain));
144        DeclarationPtr::new(name, kind)
145    }
146
147    /// Creates a new given declaration.
148    ///
149    /// # Examples
150    ///
151    /// ```
152    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
153    ///
154    /// // given n: int(1..5)
155    /// let declaration = DeclarationPtr::new_given(
156    ///     Name::User("n".into()),
157    ///     Domain::int(vec![Range::Bounded(1,5)]));
158    ///
159    /// ```
160    pub fn new_given(name: Name, domain: DomainPtr) -> DeclarationPtr {
161        let kind = DeclarationKind::Given(domain);
162        DeclarationPtr::new(name, kind)
163    }
164
165    /// Creates a new quantified declaration for local comprehension scopes.
166    ///
167    /// Used when creating the quantified variable in a generator.
168    pub fn new_quantified(name: Name, domain: DomainPtr) -> DeclarationPtr {
169        DeclarationPtr::new(
170            name,
171            DeclarationKind::Quantified(Quantified {
172                domain,
173                generator: None,
174            }),
175        )
176    }
177
178    /// Creates a quantified declaration backed by a generator declaration.
179    ///
180    /// This is used in comprehensions to refer to a quantified variable that is already defined using a generator.
181    pub fn new_quantified_from_generator(decl: &DeclarationPtr) -> Option<DeclarationPtr> {
182        let kind = DeclarationKind::Quantified(Quantified {
183            domain: decl.domain()?,
184            generator: Some(decl.clone()),
185        });
186        Some(DeclarationPtr::new(decl.name().clone(), kind))
187    }
188
189    /// Creates a new value letting declaration.
190    ///
191    /// # Examples
192    ///
193    /// ```
194    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
195    /// Literal,Atom,Moo};
196    /// use conjure_cp_core::{matrix_expr,ast::Metadata};
197    ///
198    /// // letting n be 10 + 10
199    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
200    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
201    /// let declaration = DeclarationPtr::new_value_letting(
202    ///     Name::User("n".into()),
203    ///     expression);
204    ///
205    /// ```
206    pub fn new_value_letting(name: Name, expression: Expression) -> DeclarationPtr {
207        let kind = DeclarationKind::ValueLetting(expression);
208        DeclarationPtr::new(name, kind)
209    }
210
211    /// Creates a new domain letting declaration.
212    ///
213    /// # Examples
214    ///
215    /// ```
216    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
217    ///
218    /// // letting MyDomain be int(1..5)
219    /// let declaration = DeclarationPtr::new_domain_letting(
220    ///     Name::User("MyDomain".into()),
221    ///     Domain::int(vec![Range::Bounded(1,5)]));
222    ///
223    /// ```
224    pub fn new_domain_letting(name: Name, domain: DomainPtr) -> DeclarationPtr {
225        let kind = DeclarationKind::DomainLetting(domain);
226        DeclarationPtr::new(name, kind)
227    }
228
229    /// Creates a new record field declaration.
230    ///
231    /// # Examples
232    ///
233    /// ```
234    /// use conjure_cp_core::ast::{DeclarationPtr,Name,RecordEntry,Domain,Range};
235    ///
236    /// // create declaration for field A in `find rec: record {A: int(0..1), B: int(0..2)}`
237    ///
238    /// let field = RecordEntry {
239    ///     name: Name::User("n".into()),
240    ///     domain: Domain::int(vec![Range::Bounded(1,5)])
241    /// };
242    ///
243    /// let declaration = DeclarationPtr::new_record_field(field);
244    /// ```
245    pub fn new_record_field(entry: RecordEntry) -> DeclarationPtr {
246        let kind = DeclarationKind::RecordField(entry.domain);
247        DeclarationPtr::new(entry.name, kind)
248    }
249
250    /**********************************************/
251    /*        Declaration accessor methods        */
252    /**********************************************/
253
254    /// Gets the domain of the declaration, if it has one.
255    ///
256    /// # Examples
257    ///
258    /// ```
259    /// use conjure_cp_core::ast::{DeclarationPtr, Name, Domain, Range, GroundDomain};
260    ///
261    /// // find a: int(1..5)
262    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
263    ///
264    /// assert!(declaration.domain().is_some_and(|x| x.as_ground().unwrap() == &GroundDomain::Int(vec![Range::Bounded(1,5)])))
265    ///
266    /// ```
267    pub fn domain(&self) -> Option<DomainPtr> {
268        match &self.kind() as &DeclarationKind {
269            DeclarationKind::Find(var) => Some(var.domain_of()),
270            DeclarationKind::ValueLetting(e) => e.domain_of(),
271            DeclarationKind::DomainLetting(domain) => Some(domain.clone()),
272            DeclarationKind::Given(domain) => Some(domain.clone()),
273            DeclarationKind::Quantified(inner) => Some(inner.domain.clone()),
274            DeclarationKind::RecordField(domain) => Some(domain.clone()),
275        }
276    }
277
278    /// Gets the domain of the declaration and fully resolve it
279    pub fn resolved_domain(&self) -> Option<Moo<GroundDomain>> {
280        self.domain()?.resolve()
281    }
282
283    /// Gets the kind of the declaration.
284    ///
285    /// # Examples
286    ///
287    /// ```
288    /// use conjure_cp_core::ast::{DeclarationPtr,DeclarationKind,Name,Domain,Range};
289    ///
290    /// // find a: int(1..5)
291    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
292    /// assert!(matches!(&declaration.kind() as &DeclarationKind, DeclarationKind::Find(_)))
293    /// ```
294    pub fn kind(&self) -> MappedRwLockReadGuard<'_, DeclarationKind> {
295        self.map(|x| &x.kind)
296    }
297
298    /// Gets the name of the declaration.
299    ///
300    /// # Examples
301    ///
302    /// ```
303    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
304    ///
305    /// // find a: int(1..5)
306    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
307    ///
308    /// assert_eq!(&declaration.name() as &Name, &Name::User("a".into()))
309    /// ```
310    pub fn name(&self) -> MappedRwLockReadGuard<'_, Name> {
311        self.map(|x| &x.name)
312    }
313
314    /// This declaration as a decision variable, if it is one.
315    pub fn as_var(&self) -> Option<MappedRwLockReadGuard<'_, DecisionVariable>> {
316        RwLockReadGuard::try_map(self.read(), |x| {
317            if let DeclarationKind::Find(var) = &x.kind {
318                Some(var)
319            } else {
320                None
321            }
322        })
323        .ok()
324    }
325
326    /// This declaration as a mutable decision variable, if it is one.
327    pub fn as_var_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DecisionVariable>> {
328        RwLockWriteGuard::try_map(self.write(), |x| {
329            if let DeclarationKind::Find(var) = &mut x.kind {
330                Some(var)
331            } else {
332                None
333            }
334        })
335        .ok()
336    }
337
338    /// This declaration as a domain letting, if it is one.
339    pub fn as_domain_letting(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
340        RwLockReadGuard::try_map(self.read(), |x| {
341            if let DeclarationKind::DomainLetting(domain) = &x.kind {
342                Some(domain)
343            } else {
344                None
345            }
346        })
347        .ok()
348    }
349
350    /// This declaration as a mutable domain letting, if it is one.
351    pub fn as_domain_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DomainPtr>> {
352        RwLockWriteGuard::try_map(self.write(), |x| {
353            if let DeclarationKind::DomainLetting(domain) = &mut x.kind {
354                Some(domain)
355            } else {
356                None
357            }
358        })
359        .ok()
360    }
361
362    /// This declaration as a value letting, if it is one.
363    pub fn as_value_letting(&self) -> Option<MappedRwLockReadGuard<'_, Expression>> {
364        RwLockReadGuard::try_map(self.read(), |x| {
365            if let DeclarationKind::ValueLetting(expression) = &x.kind {
366                Some(expression)
367            } else {
368                None
369            }
370        })
371        .ok()
372    }
373
374    /// This declaration as a mutable value letting, if it is one.
375    pub fn as_value_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, Expression>> {
376        RwLockWriteGuard::try_map(self.write(), |x| {
377            if let DeclarationKind::ValueLetting(expression) = &mut x.kind {
378                Some(expression)
379            } else {
380                None
381            }
382        })
383        .ok()
384    }
385
386    /// Changes the name in this declaration, returning the old one.
387    ///
388    /// # Examples
389    ///
390    /// ```
391    /// use conjure_cp_core::ast::{DeclarationPtr, Domain, Range, Name};
392    ///
393    /// // find a: int(1..5)
394    /// let mut declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
395    ///
396    /// let old_name = declaration.replace_name(Name::User("b".into()));
397    /// assert_eq!(old_name,Name::User("a".into()));
398    /// assert_eq!(&declaration.name() as &Name,&Name::User("b".into()));
399    /// ```
400    pub fn replace_name(&mut self, name: Name) -> Name {
401        let mut decl = self.write();
402        std::mem::replace(&mut decl.name, name)
403    }
404
405    /// Replaces the underlying declaration kind and returns the previous kind.
406    /// Note: this affects all cloned `DeclarationPtr`s pointing to the same declaration.
407    pub fn replace_kind(&mut self, kind: DeclarationKind) -> DeclarationKind {
408        let mut decl = self.write();
409        std::mem::replace(&mut decl.kind, kind)
410    }
411
412    /*****************************************/
413    /*        Pointer utility methods        */
414    /*****************************************/
415
416    // These are mostly wrappers over RefCell, Ref, and RefMut methods, re-exported here for
417    // convenience.
418
419    /// Read the underlying [Declaration].
420    ///
421    /// Will block the current thread until no other thread has a write lock.
422    /// Attempting to get a read lock if the current thread already has one
423    /// **will** cause it to deadlock.
424    /// The lock is released when the returned guard goes out of scope.
425    fn read(&self) -> RwLockReadGuard<'_, Declaration> {
426        self.inner.value.read()
427    }
428
429    /// Write the underlying [Declaration].
430    ///
431    /// Will block the current thread until no other thread has a read or write lock.
432    /// The lock is released when the returned guard goes out of scope.
433    fn write(&mut self) -> RwLockWriteGuard<'_, Declaration> {
434        self.inner.value.write()
435    }
436
437    /// Creates a new declaration pointer with the same contents as `self` that is not shared with
438    /// anyone else.
439    ///
440    /// As the resulting pointer is unshared, it will have a new id.
441    ///
442    /// # Examples
443    ///
444    /// ```
445    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
446    ///
447    /// // find a: int(1..5)
448    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
449    ///
450    /// let mut declaration2 = declaration.clone();
451    ///
452    /// declaration2.replace_name(Name::User("b".into()));
453    ///
454    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
455    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
456    ///
457    /// declaration2 = declaration2.detach();
458    ///
459    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
460    ///
461    /// declaration2.replace_name(Name::User("c".into()));
462    ///
463    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
464    /// assert_eq!(&declaration2.name() as &Name, &Name::User("c".into()));
465    /// ```
466    pub fn detach(self) -> DeclarationPtr {
467        // despite having the same contents, the new declaration pointer is unshared, so it should
468        // get a new id.
469        let value = self.inner.value.read().clone();
470        DeclarationPtr {
471            inner: DeclarationPtrInner::new(RwLock::new(value)),
472        }
473    }
474
475    /// Applies `f` to the declaration, returning the result as a reference.
476    fn map<U>(&self, f: impl FnOnce(&Declaration) -> &U) -> MappedRwLockReadGuard<'_, U> {
477        RwLockReadGuard::map(self.read(), f)
478    }
479
480    /// Applies mutable function `f` to the declaration, returning the result as a mutable reference.
481    fn map_mut<U>(
482        &mut self,
483        f: impl FnOnce(&mut Declaration) -> &mut U,
484    ) -> MappedRwLockWriteGuard<'_, U> {
485        RwLockWriteGuard::map(self.write(), f)
486    }
487
488    /// Replaces the declaration with a new one, returning the old value, without deinitialising
489    /// either one.
490    fn replace(&mut self, declaration: Declaration) -> Declaration {
491        let mut guard = self.write();
492        let ans = mem::replace(&mut *guard, declaration);
493        drop(guard);
494        ans
495    }
496}
497
498impl CategoryOf for DeclarationPtr {
499    fn category_of(&self) -> Category {
500        match &self.kind() as &DeclarationKind {
501            DeclarationKind::Find(decision_variable) => decision_variable.category_of(),
502            DeclarationKind::ValueLetting(expression) => expression.category_of(),
503            DeclarationKind::DomainLetting(_) => Category::Constant,
504            DeclarationKind::Given(_) => Category::Parameter,
505            DeclarationKind::Quantified(..) => Category::Quantified,
506            DeclarationKind::RecordField(_) => Category::Bottom,
507        }
508    }
509}
510impl HasId for DeclarationPtr {
511    const TYPE_NAME: &'static str = "DeclarationPtrInner";
512    fn id(&self) -> ObjId {
513        self.inner.id.clone()
514    }
515}
516
517impl DefaultWithId for DeclarationPtr {
518    fn default_with_id(id: ObjId) -> Self {
519        DeclarationPtr {
520            inner: DeclarationPtrInner::new_with_id_unchecked(
521                RwLock::new(Declaration {
522                    name: Name::User("_UNKNOWN".into()),
523                    kind: DeclarationKind::ValueLetting(false.into()),
524                }),
525                id,
526            ),
527        }
528    }
529}
530
531impl Typeable for DeclarationPtr {
532    fn return_type(&self) -> ReturnType {
533        match &self.kind() as &DeclarationKind {
534            DeclarationKind::Find(var) => var.return_type(),
535            DeclarationKind::ValueLetting(expression) => expression.return_type(),
536            DeclarationKind::DomainLetting(domain) => domain.return_type(),
537            DeclarationKind::Given(domain) => domain.return_type(),
538            DeclarationKind::Quantified(inner) => inner.domain.return_type(),
539            DeclarationKind::RecordField(domain) => domain.return_type(),
540        }
541    }
542}
543
544impl Uniplate for DeclarationPtr {
545    fn uniplate(&self) -> (Tree<Self>, Box<dyn Fn(Tree<Self>) -> Self>) {
546        let decl = self.read();
547        let (tree, recons) = Biplate::<DeclarationPtr>::biplate(&decl as &Declaration);
548
549        let self2 = self.clone();
550        (
551            tree,
552            Box::new(move |x| {
553                let mut self3 = self2.clone();
554                let inner = recons(x);
555                *(&mut self3.write() as &mut Declaration) = inner;
556                self3
557            }),
558        )
559    }
560}
561
562impl<To> Biplate<To> for DeclarationPtr
563where
564    Declaration: Biplate<To>,
565    To: Uniplate,
566{
567    fn biplate(&self) -> (Tree<To>, Box<dyn Fn(Tree<To>) -> Self>) {
568        if TypeId::of::<To>() == TypeId::of::<Self>() {
569            unsafe {
570                let self_as_to = std::mem::transmute::<&Self, &To>(self).clone();
571                (
572                    Tree::One(self_as_to),
573                    Box::new(move |x| {
574                        let Tree::One(x) = x else { panic!() };
575
576                        let x_as_self = std::mem::transmute::<&To, &Self>(&x);
577                        x_as_self.clone()
578                    }),
579                )
580            }
581        } else {
582            // call biplate on the enclosed declaration
583            let decl = self.read();
584            let (tree, recons) = Biplate::<To>::biplate(&decl as &Declaration);
585
586            let self2 = self.clone();
587            (
588                tree,
589                Box::new(move |x| {
590                    let mut self3 = self2.clone();
591                    let inner = recons(x);
592                    *(&mut self3.write() as &mut Declaration) = inner;
593                    self3
594                }),
595            )
596        }
597    }
598}
599
600impl IdPtr for DeclarationPtr {
601    type Data = Declaration;
602
603    fn get_data(&self) -> Self::Data {
604        self.read().clone()
605    }
606
607    fn with_id_and_data(id: ObjId, data: Self::Data) -> Self {
608        Self {
609            inner: DeclarationPtrInner::new_with_id_unchecked(RwLock::new(data), id),
610        }
611    }
612}
613
614impl Ord for DeclarationPtr {
615    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
616        self.inner.id.cmp(&other.inner.id)
617    }
618}
619
620impl PartialOrd for DeclarationPtr {
621    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
622        Some(self.cmp(other))
623    }
624}
625
626impl PartialEq for DeclarationPtr {
627    fn eq(&self, other: &Self) -> bool {
628        self.inner.id == other.inner.id
629    }
630}
631
632impl Eq for DeclarationPtr {}
633
634impl std::hash::Hash for DeclarationPtr {
635    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
636        // invariant: x == y -> hash(x) == hash(y)
637        self.inner.id.hash(state);
638    }
639}
640
641impl Display for DeclarationPtr {
642    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
643        let value: &Declaration = &self.read();
644        value.fmt(f)
645    }
646}
647
648#[derive(Clone, PartialEq, Debug, Serialize, Deserialize, Eq, Uniplate)]
649#[biplate(to=Expression)]
650#[biplate(to=DeclarationPtr)]
651#[biplate(to=Name)]
652/// The contents of a declaration
653pub(super) struct Declaration {
654    /// The name of the declared symbol.
655    name: Name,
656
657    /// The kind of the declaration.
658    kind: DeclarationKind,
659}
660
661impl Declaration {
662    /// Creates a new declaration.
663    fn new(name: Name, kind: DeclarationKind) -> Declaration {
664        Declaration { name, kind }
665    }
666}
667
668/// A specific kind of declaration.
669#[non_exhaustive]
670#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
671#[biplate(to=Expression)]
672#[biplate(to=DeclarationPtr)]
673#[biplate(to=Declaration)]
674pub enum DeclarationKind {
675    Find(DecisionVariable),
676    Given(DomainPtr),
677    Quantified(Quantified),
678    ValueLetting(Expression),
679    DomainLetting(DomainPtr),
680
681    /// A named field inside a record type.
682    /// e.g. A, B in record{A: int(0..1), B: int(0..2)}
683    RecordField(DomainPtr),
684}
685
686#[serde_as]
687#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
688pub struct Quantified {
689    domain: DomainPtr,
690
691    #[serde_as(as = "Option<PtrAsInner>")]
692    generator: Option<DeclarationPtr>,
693}
694
695impl Quantified {
696    pub fn domain(&self) -> &DomainPtr {
697        &self.domain
698    }
699
700    pub fn generator(&self) -> Option<&DeclarationPtr> {
701        self.generator.as_ref()
702    }
703}