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, Reference,
6    ReturnType, 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::collections::VecDeque;
15use std::fmt::{Debug, Display};
16use std::mem;
17use std::sync::Arc;
18use std::sync::atomic::{AtomicU32, Ordering};
19use uniplate::{Biplate, Tree, Uniplate};
20
21/// Global counter of declarations.
22/// Note that the counter is shared between all threads
23/// Thus, when running multiple models in parallel, IDs may
24/// be different with every run depending on scheduling order
25static DECLARATION_PTR_ID_COUNTER: AtomicU32 = const { AtomicU32::new(0) };
26
27#[doc(hidden)]
28/// Resets the id counter of `DeclarationPtr` to 0.
29///
30/// This is probably always a bad idea.
31pub fn reset_declaration_id_unchecked() {
32    let _ = DECLARATION_PTR_ID_COUNTER.swap(0, Ordering::Relaxed);
33}
34
35/// A shared pointer to a [`Declaration`].
36///
37/// Two declaration pointers are equal if they point to the same underlying declaration.
38///
39/// # Id
40///
41///  The id of `DeclarationPtr` obeys the following invariants:
42///
43/// 1. Declaration pointers have the same id if they point to the same
44///    underlying declaration.
45///
46/// 2. The id is immutable.
47///
48/// 3. Changing the declaration pointed to by the declaration pointer does not change the id. This
49///    allows declarations to be updated by replacing them with a newer version of themselves.
50///
51/// `Ord`, `Hash`, and `Eq` use id for comparisons.
52/// # Serde
53///
54/// Declaration pointers can be serialised using the following serializers:
55///
56/// + [`DeclarationPtrFull`](serde::DeclarationPtrFull)
57/// + [`DeclarationPtrAsId`](serde::DeclarationPtrAsId)
58///
59/// See their documentation for more information.
60#[derive(Clone, Debug)]
61pub struct DeclarationPtr
62where
63    Self: Send + Sync,
64{
65    // the shared bits of the pointer
66    inner: Arc<DeclarationPtrInner>,
67}
68
69// The bits of a declaration that are shared between all pointers.
70#[derive(Debug)]
71struct DeclarationPtrInner {
72    // We don't want this to be mutable, as `HashMap` and `BTreeMap` rely on the hash or order of
73    // keys to be unchanging.
74    //
75    // See:  https://rust-lang.github.io/rust-clippy/master/index.html#mutable_key_type
76    id: ObjId,
77
78    // The contents of the declaration itself should be mutable.
79    value: RwLock<Declaration>,
80}
81
82impl DeclarationPtrInner {
83    fn new(value: RwLock<Declaration>) -> Arc<DeclarationPtrInner> {
84        Arc::new(DeclarationPtrInner {
85            id: ObjId {
86                type_name: ustr::ustr(DeclarationPtr::TYPE_NAME),
87                object_id: DECLARATION_PTR_ID_COUNTER.fetch_add(1, Ordering::Relaxed),
88            },
89            value,
90        })
91    }
92
93    // SAFETY: only use if you are really really sure you arn't going to break the id invariants of
94    // DeclarationPtr and HasId!
95    fn new_with_id_unchecked(value: RwLock<Declaration>, id: ObjId) -> Arc<DeclarationPtrInner> {
96        Arc::new(DeclarationPtrInner { id, value })
97    }
98}
99
100#[allow(dead_code)]
101impl DeclarationPtr {
102    /******************************/
103    /*        Constructors        */
104    /******************************/
105
106    /// Creates a `DeclarationPtr` for the given `Declaration`.
107    fn from_declaration(declaration: Declaration) -> DeclarationPtr {
108        DeclarationPtr {
109            inner: DeclarationPtrInner::new(RwLock::new(declaration)),
110        }
111    }
112
113    /// Creates a new declaration.
114    ///
115    /// # Examples
116    ///
117    /// ```
118    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
119    ///
120    /// // letting MyDomain be int(1..5)
121    /// let declaration = DeclarationPtr::new(
122    ///     Name::User("MyDomain".into()),
123    ///     DeclarationKind::DomainLetting(Domain::int(vec![
124    ///         Range::Bounded(1,5)])));
125    /// ```
126    pub fn new(name: Name, kind: DeclarationKind) -> DeclarationPtr {
127        DeclarationPtr::from_declaration(Declaration::new(name, kind))
128    }
129
130    /// Creates a new find declaration.
131    ///
132    /// # Examples
133    ///
134    /// ```
135    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
136    ///
137    /// // find x: int(1..5)
138    /// let declaration = DeclarationPtr::new_find(
139    ///     Name::User("x".into()),
140    ///     Domain::int(vec![Range::Bounded(1,5)]));
141    ///
142    /// ```
143    pub fn new_find(name: Name, domain: DomainPtr) -> DeclarationPtr {
144        let kind = DeclarationKind::Find(DecisionVariable::new(domain));
145        DeclarationPtr::new(name, kind)
146    }
147
148    /// Creates a new given declaration.
149    ///
150    /// # Examples
151    ///
152    /// ```
153    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
154    ///
155    /// // given n: int(1..5)
156    /// let declaration = DeclarationPtr::new_given(
157    ///     Name::User("n".into()),
158    ///     Domain::int(vec![Range::Bounded(1,5)]));
159    ///
160    /// ```
161    pub fn new_given(name: Name, domain: DomainPtr) -> DeclarationPtr {
162        let kind = DeclarationKind::Given(domain);
163        DeclarationPtr::new(name, kind)
164    }
165
166    /// Creates a new quantified declaration for local comprehension scopes.
167    ///
168    /// Used when creating the quantified variable in a generator.
169    pub fn new_quantified(name: Name, domain: DomainPtr) -> DeclarationPtr {
170        DeclarationPtr::new(
171            name,
172            DeclarationKind::Quantified(Quantified {
173                domain,
174                generator: None,
175            }),
176        )
177    }
178
179    /// Creates a quantified declaration backed by a generator declaration.
180    ///
181    /// This is used in comprehensions to refer to a quantified variable that is already defined using a generator.
182    pub fn new_quantified_from_generator(decl: &DeclarationPtr) -> Option<DeclarationPtr> {
183        let kind = DeclarationKind::Quantified(Quantified {
184            domain: decl.domain()?,
185            generator: Some(decl.clone()),
186        });
187        Some(DeclarationPtr::new(decl.name().clone(), kind))
188    }
189
190    pub fn new_quantified_expr(name: Name, expr: Expression) -> DeclarationPtr {
191        let kind = DeclarationKind::QuantifiedExpr(expr);
192        DeclarationPtr::new(name, kind)
193    }
194
195    /// Creates a new value letting declaration.
196    ///
197    /// # Examples
198    ///
199    /// ```
200    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
201    /// Literal,Atom,Moo};
202    /// use conjure_cp_core::{matrix_expr,ast::Metadata};
203    ///
204    /// // letting n be 10 + 10
205    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
206    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
207    /// let declaration = DeclarationPtr::new_value_letting(
208    ///     Name::User("n".into()),
209    ///     expression);
210    ///
211    /// ```
212    pub fn new_value_letting(name: Name, expression: Expression) -> DeclarationPtr {
213        let kind = DeclarationKind::ValueLetting(expression, None);
214        DeclarationPtr::new(name, kind)
215    }
216
217    /// Creates a new value letting declaration with domain.
218    ///
219    /// # Examples
220    ///
221    /// ```
222    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
223    /// Literal,Atom,Moo,DomainPtr,Metadata};
224    /// use conjure_cp_core::{matrix_expr};
225    ///
226    /// // letting n be 10 + 10
227    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
228    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
229    /// let domain = Domain::bool();
230    /// let declaration = DeclarationPtr::new_value_letting_with_domain(
231    ///     Name::User("n".into()),
232    ///     expression,
233    ///     domain,
234    /// );
235    /// ```
236    pub fn new_value_letting_with_domain(
237        name: Name,
238        expression: Expression,
239        domain: DomainPtr,
240    ) -> DeclarationPtr {
241        let kind = DeclarationKind::ValueLetting(expression, Some(domain));
242        DeclarationPtr::new(name, kind)
243    }
244
245    /// Creates a new domain letting declaration.
246    ///
247    /// # Examples
248    ///
249    /// ```
250    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
251    ///
252    /// // letting MyDomain be int(1..5)
253    /// let declaration = DeclarationPtr::new_domain_letting(
254    ///     Name::User("MyDomain".into()),
255    ///     Domain::int(vec![Range::Bounded(1,5)]));
256    ///
257    /// ```
258    pub fn new_domain_letting(name: Name, domain: DomainPtr) -> DeclarationPtr {
259        let kind = DeclarationKind::DomainLetting(domain);
260        DeclarationPtr::new(name, kind)
261    }
262
263    /// Creates a new record field declaration.
264    ///
265    /// # Examples
266    ///
267    /// ```
268    /// use conjure_cp_core::ast::{DeclarationPtr,Name,RecordEntry,Domain,Range};
269    ///
270    /// // create declaration for field A in `find rec: record {A: int(0..1), B: int(0..2)}`
271    ///
272    /// let field = RecordEntry {
273    ///     name: Name::User("n".into()),
274    ///     domain: Domain::int(vec![Range::Bounded(1,5)])
275    /// };
276    ///
277    /// let declaration = DeclarationPtr::new_record_field(field);
278    /// ```
279    pub fn new_record_field(entry: RecordEntry) -> DeclarationPtr {
280        let kind = DeclarationKind::RecordField(entry.domain);
281        DeclarationPtr::new(entry.name, kind)
282    }
283
284    /**********************************************/
285    /*        Declaration accessor methods        */
286    /**********************************************/
287
288    /// Gets the domain of the declaration, if it has one.
289    ///
290    /// # Examples
291    ///
292    /// ```
293    /// use conjure_cp_core::ast::{DeclarationPtr, Name, Domain, Range, GroundDomain};
294    ///
295    /// // find a: int(1..5)
296    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
297    ///
298    /// assert!(declaration.domain().is_some_and(|x| x.as_ground().unwrap() == &GroundDomain::Int(vec![Range::Bounded(1,5)])))
299    ///
300    /// ```
301    pub fn domain(&self) -> Option<DomainPtr> {
302        match &self.kind() as &DeclarationKind {
303            DeclarationKind::Find(var) => Some(var.domain_of()),
304            DeclarationKind::ValueLetting(e, _) | DeclarationKind::TemporaryValueLetting(e) => {
305                e.domain_of()
306            }
307            DeclarationKind::DomainLetting(domain) => Some(domain.clone()),
308            DeclarationKind::Given(domain) => Some(domain.clone()),
309            DeclarationKind::Quantified(inner) => Some(inner.domain.clone()),
310            DeclarationKind::QuantifiedExpr(expr) => expr.domain_of(),
311            DeclarationKind::RecordField(domain) => Some(domain.clone()),
312        }
313    }
314
315    /// Gets the domain of the declaration and fully resolve it
316    pub fn resolved_domain(&self) -> Option<Moo<GroundDomain>> {
317        self.domain()?.resolve()
318    }
319
320    /// Gets the kind of the declaration.
321    ///
322    /// # Examples
323    ///
324    /// ```
325    /// use conjure_cp_core::ast::{DeclarationPtr,DeclarationKind,Name,Domain,Range};
326    ///
327    /// // find a: int(1..5)
328    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
329    /// assert!(matches!(&declaration.kind() as &DeclarationKind, DeclarationKind::Find(_)))
330    /// ```
331    pub fn kind(&self) -> MappedRwLockReadGuard<'_, DeclarationKind> {
332        self.map(|x| &x.kind)
333    }
334
335    /// Gets the name of the declaration.
336    ///
337    /// # Examples
338    ///
339    /// ```
340    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
341    ///
342    /// // find a: int(1..5)
343    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
344    ///
345    /// assert_eq!(&declaration.name() as &Name, &Name::User("a".into()))
346    /// ```
347    pub fn name(&self) -> MappedRwLockReadGuard<'_, Name> {
348        self.map(|x| &x.name)
349    }
350
351    /// This declaration as a decision variable, if it is one.
352    pub fn as_find(&self) -> Option<MappedRwLockReadGuard<'_, DecisionVariable>> {
353        RwLockReadGuard::try_map(self.read(), |x| {
354            if let DeclarationKind::Find(var) = &x.kind {
355                Some(var)
356            } else {
357                None
358            }
359        })
360        .ok()
361    }
362
363    /// This declaration as a mutable decision variable, if it is one.
364    pub fn as_find_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DecisionVariable>> {
365        RwLockWriteGuard::try_map(self.write(), |x| {
366            if let DeclarationKind::Find(var) = &mut x.kind {
367                Some(var)
368            } else {
369                None
370            }
371        })
372        .ok()
373    }
374
375    /// This declaration as a domain letting, if it is one.
376    pub fn as_domain_letting(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
377        RwLockReadGuard::try_map(self.read(), |x| {
378            if let DeclarationKind::DomainLetting(domain) = &x.kind {
379                Some(domain)
380            } else {
381                None
382            }
383        })
384        .ok()
385    }
386
387    /// This declaration as a mutable domain letting, if it is one.
388    pub fn as_domain_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DomainPtr>> {
389        RwLockWriteGuard::try_map(self.write(), |x| {
390            if let DeclarationKind::DomainLetting(domain) = &mut x.kind {
391                Some(domain)
392            } else {
393                None
394            }
395        })
396        .ok()
397    }
398
399    /// This declaration as a value letting, if it is one.
400    pub fn as_value_letting(&self) -> Option<MappedRwLockReadGuard<'_, Expression>> {
401        RwLockReadGuard::try_map(self.read(), |x| {
402            if let DeclarationKind::ValueLetting(expression, _)
403            | DeclarationKind::TemporaryValueLetting(expression) = &x.kind
404            {
405                Some(expression)
406            } else {
407                None
408            }
409        })
410        .ok()
411    }
412
413    /// This declaration as a mutable value letting, if it is one.
414    pub fn as_value_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, Expression>> {
415        RwLockWriteGuard::try_map(self.write(), |x| {
416            if let DeclarationKind::ValueLetting(expression, _)
417            | DeclarationKind::TemporaryValueLetting(expression) = &mut x.kind
418            {
419                Some(expression)
420            } else {
421                None
422            }
423        })
424        .ok()
425    }
426
427    /// This declaration as a given statement, if it is one.
428    pub fn as_given(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
429        RwLockReadGuard::try_map(self.read(), |x| {
430            if let DeclarationKind::Given(domain) = &x.kind {
431                Some(domain)
432            } else {
433                None
434            }
435        })
436        .ok()
437    }
438
439    /// This declaration as a mutable given statement, if it is one.
440    pub fn as_given_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DomainPtr>> {
441        RwLockWriteGuard::try_map(self.write(), |x| {
442            if let DeclarationKind::Given(domain) = &mut x.kind {
443                Some(domain)
444            } else {
445                None
446            }
447        })
448        .ok()
449    }
450
451    /// This declaration as a quantified expression, if it is one.
452    pub fn as_quantified_expr(&self) -> Option<MappedRwLockReadGuard<'_, Expression>> {
453        RwLockReadGuard::try_map(self.read(), |x| {
454            if let DeclarationKind::QuantifiedExpr(expr) = &x.kind {
455                Some(expr)
456            } else {
457                None
458            }
459        })
460        .ok()
461    }
462
463    /// This declaration as a mutable quantified expression, if it is one.
464    pub fn as_quantified_expr_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, Expression>> {
465        RwLockWriteGuard::try_map(self.write(), |x| {
466            if let DeclarationKind::QuantifiedExpr(expr) = &mut x.kind {
467                Some(expr)
468            } else {
469                None
470            }
471        })
472        .ok()
473    }
474
475    /// Changes the name in this declaration, returning the old one.
476    ///
477    /// # Examples
478    ///
479    /// ```
480    /// use conjure_cp_core::ast::{DeclarationPtr, Domain, Range, Name};
481    ///
482    /// // find a: int(1..5)
483    /// let mut declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
484    ///
485    /// let old_name = declaration.replace_name(Name::User("b".into()));
486    /// assert_eq!(old_name,Name::User("a".into()));
487    /// assert_eq!(&declaration.name() as &Name,&Name::User("b".into()));
488    /// ```
489    pub fn replace_name(&mut self, name: Name) -> Name {
490        let mut decl = self.write();
491        std::mem::replace(&mut decl.name, name)
492    }
493
494    /// Replaces the underlying declaration kind and returns the previous kind.
495    /// Note: this affects all cloned `DeclarationPtr`s pointing to the same declaration.
496    pub fn replace_kind(&mut self, kind: DeclarationKind) -> DeclarationKind {
497        let mut decl = self.write();
498        std::mem::replace(&mut decl.kind, kind)
499    }
500
501    /*****************************************/
502    /*        Pointer utility methods        */
503    /*****************************************/
504
505    // These are mostly wrappers over RefCell, Ref, and RefMut methods, re-exported here for
506    // convenience.
507
508    /// Read the underlying [Declaration].
509    ///
510    /// Will block the current thread until no other thread has a write lock.
511    /// Attempting to get a read lock if the current thread already has one
512    /// **will** cause it to deadlock.
513    /// The lock is released when the returned guard goes out of scope.
514    fn read(&self) -> RwLockReadGuard<'_, Declaration> {
515        self.inner.value.read()
516    }
517
518    /// Write the underlying [Declaration].
519    ///
520    /// Will block the current thread until no other thread has a read or write lock.
521    /// The lock is released when the returned guard goes out of scope.
522    fn write(&mut self) -> RwLockWriteGuard<'_, Declaration> {
523        self.inner.value.write()
524    }
525
526    /// Creates a new declaration pointer with the same contents as `self` that is not shared with
527    /// anyone else.
528    ///
529    /// As the resulting pointer is unshared, it will have a new id.
530    ///
531    /// # Examples
532    ///
533    /// ```
534    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
535    ///
536    /// // find a: int(1..5)
537    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
538    ///
539    /// let mut declaration2 = declaration.clone();
540    ///
541    /// declaration2.replace_name(Name::User("b".into()));
542    ///
543    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
544    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
545    ///
546    /// declaration2 = declaration2.detach();
547    ///
548    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
549    ///
550    /// declaration2.replace_name(Name::User("c".into()));
551    ///
552    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
553    /// assert_eq!(&declaration2.name() as &Name, &Name::User("c".into()));
554    /// ```
555    pub fn detach(self) -> DeclarationPtr {
556        // despite having the same contents, the new declaration pointer is unshared, so it should
557        // get a new id.
558        let value = self.inner.value.read().clone();
559        DeclarationPtr {
560            inner: DeclarationPtrInner::new(RwLock::new(value)),
561        }
562    }
563
564    /// Applies `f` to the declaration, returning the result as a reference.
565    fn map<U>(&self, f: impl FnOnce(&Declaration) -> &U) -> MappedRwLockReadGuard<'_, U> {
566        RwLockReadGuard::map(self.read(), f)
567    }
568
569    /// Applies mutable function `f` to the declaration, returning the result as a mutable reference.
570    fn map_mut<U>(
571        &mut self,
572        f: impl FnOnce(&mut Declaration) -> &mut U,
573    ) -> MappedRwLockWriteGuard<'_, U> {
574        RwLockWriteGuard::map(self.write(), f)
575    }
576
577    /// Replaces the declaration with a new one, returning the old value, without deinitialising
578    /// either one.
579    pub fn replace(&mut self, declaration: Declaration) -> Declaration {
580        let mut guard = self.write();
581        let ans = mem::replace(&mut *guard, declaration);
582        drop(guard);
583        ans
584    }
585}
586
587impl CategoryOf for DeclarationPtr {
588    fn category_of(&self) -> Category {
589        match &self.kind() as &DeclarationKind {
590            DeclarationKind::Find(decision_variable) => decision_variable.category_of(),
591            DeclarationKind::ValueLetting(expression, _)
592            | DeclarationKind::TemporaryValueLetting(expression) => expression.category_of(),
593            DeclarationKind::DomainLetting(_) => Category::Constant,
594            DeclarationKind::Given(_) => Category::Parameter,
595            DeclarationKind::Quantified(..) => Category::Quantified,
596            DeclarationKind::QuantifiedExpr(..) => Category::Quantified,
597            DeclarationKind::RecordField(_) => Category::Bottom,
598        }
599    }
600}
601impl HasId for DeclarationPtr {
602    const TYPE_NAME: &'static str = "DeclarationPtrInner";
603    fn id(&self) -> ObjId {
604        self.inner.id.clone()
605    }
606}
607
608impl DefaultWithId for DeclarationPtr {
609    fn default_with_id(id: ObjId) -> Self {
610        DeclarationPtr {
611            inner: DeclarationPtrInner::new_with_id_unchecked(
612                RwLock::new(Declaration {
613                    name: Name::User("_UNKNOWN".into()),
614                    kind: DeclarationKind::ValueLetting(false.into(), None),
615                }),
616                id,
617            ),
618        }
619    }
620}
621
622impl Typeable for DeclarationPtr {
623    fn return_type(&self) -> ReturnType {
624        match &self.kind() as &DeclarationKind {
625            DeclarationKind::Find(var) => var.return_type(),
626            DeclarationKind::ValueLetting(expression, _)
627            | DeclarationKind::TemporaryValueLetting(expression) => expression.return_type(),
628            DeclarationKind::DomainLetting(domain) => domain.return_type(),
629            DeclarationKind::Given(domain) => domain.return_type(),
630            DeclarationKind::Quantified(inner) => inner.domain.return_type(),
631            DeclarationKind::QuantifiedExpr(expr) => expr.return_type(),
632            DeclarationKind::RecordField(domain) => domain.return_type(),
633        }
634    }
635}
636
637impl Uniplate for DeclarationPtr {
638    fn uniplate(&self) -> (Tree<Self>, Box<dyn Fn(Tree<Self>) -> Self>) {
639        let decl = self.read();
640        let (tree, recons) = Biplate::<DeclarationPtr>::biplate(&decl as &Declaration);
641
642        let self2 = self.clone();
643        (
644            tree,
645            Box::new(move |x| {
646                let mut self3 = self2.clone();
647                let inner = recons(x);
648                *(&mut self3.write() as &mut Declaration) = inner;
649                self3
650            }),
651        )
652    }
653}
654
655impl<To> Biplate<To> for DeclarationPtr
656where
657    Declaration: Biplate<To>,
658    To: Uniplate,
659{
660    fn biplate(&self) -> (Tree<To>, Box<dyn Fn(Tree<To>) -> Self>) {
661        if TypeId::of::<To>() == TypeId::of::<Self>() {
662            unsafe {
663                let self_as_to = std::mem::transmute::<&Self, &To>(self).clone();
664                (
665                    Tree::One(self_as_to),
666                    Box::new(move |x| {
667                        let Tree::One(x) = x else { panic!() };
668
669                        let x_as_self = std::mem::transmute::<&To, &Self>(&x);
670                        x_as_self.clone()
671                    }),
672                )
673            }
674        } else {
675            // call biplate on the enclosed declaration
676            let decl = self.read();
677            let (tree, recons) = Biplate::<To>::biplate(&decl as &Declaration);
678
679            let self2 = self.clone();
680            (
681                tree,
682                Box::new(move |x| {
683                    let mut self3 = self2.clone();
684                    let inner = recons(x);
685                    *(&mut self3.write() as &mut Declaration) = inner;
686                    self3
687                }),
688            )
689        }
690    }
691}
692
693type ReferenceTree = Tree<Reference>;
694type ReferenceReconstructor<T> = Box<dyn Fn(ReferenceTree) -> T>;
695
696impl Biplate<Reference> for DeclarationPtr {
697    fn biplate(&self) -> (ReferenceTree, ReferenceReconstructor<Self>) {
698        let (tree, recons_kind) = biplate_declaration_kind_references(self.kind().clone());
699
700        let self2 = self.clone();
701        (
702            tree,
703            Box::new(move |x| {
704                let mut self3 = self2.clone();
705                let _ = self3.replace_kind(recons_kind(x));
706                self3
707            }),
708        )
709    }
710}
711
712fn biplate_domain_ptr_references(
713    domain: DomainPtr,
714) -> (ReferenceTree, ReferenceReconstructor<DomainPtr>) {
715    let domain_inner = domain.as_ref().clone();
716    let (tree, recons_domain) = Biplate::<Reference>::biplate(&domain_inner);
717    (tree, Box::new(move |x| Moo::new(recons_domain(x))))
718}
719
720fn biplate_declaration_kind_references(
721    kind: DeclarationKind,
722) -> (ReferenceTree, ReferenceReconstructor<DeclarationKind>) {
723    match kind {
724        DeclarationKind::Find(var) => {
725            let (tree, recons_domain) = biplate_domain_ptr_references(var.domain.clone());
726            (
727                tree,
728                Box::new(move |x| {
729                    let mut var2 = var.clone();
730                    var2.domain = recons_domain(x);
731                    DeclarationKind::Find(var2)
732                }),
733            )
734        }
735        DeclarationKind::Given(domain) => {
736            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
737            (
738                tree,
739                Box::new(move |x| DeclarationKind::Given(recons_domain(x))),
740            )
741        }
742        DeclarationKind::DomainLetting(domain) => {
743            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
744            (
745                tree,
746                Box::new(move |x| DeclarationKind::DomainLetting(recons_domain(x))),
747            )
748        }
749        DeclarationKind::RecordField(domain) => {
750            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
751            (
752                tree,
753                Box::new(move |x| DeclarationKind::RecordField(recons_domain(x))),
754            )
755        }
756        DeclarationKind::ValueLetting(expression, domain) => {
757            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expression);
758            (
759                tree,
760                Box::new(move |x| DeclarationKind::ValueLetting(recons_expr(x), domain.clone())),
761            )
762        }
763        DeclarationKind::TemporaryValueLetting(expression) => {
764            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expression);
765            (
766                tree,
767                Box::new(move |x| DeclarationKind::TemporaryValueLetting(recons_expr(x))),
768            )
769        }
770        DeclarationKind::Quantified(quantified) => {
771            let (domain_tree, recons_domain) =
772                biplate_domain_ptr_references(quantified.domain.clone());
773
774            let (generator_tree, recons_generator) = if let Some(generator) = quantified.generator()
775            {
776                let generator = generator.clone();
777                let (tree, recons_declaration) = Biplate::<Reference>::biplate(&generator);
778                (
779                    tree,
780                    Box::new(move |x| Some(recons_declaration(x)))
781                        as ReferenceReconstructor<Option<DeclarationPtr>>,
782                )
783            } else {
784                (
785                    Tree::Zero,
786                    Box::new(|_| None) as ReferenceReconstructor<Option<DeclarationPtr>>,
787                )
788            };
789
790            (
791                Tree::Many(VecDeque::from([domain_tree, generator_tree])),
792                Box::new(move |x| {
793                    let Tree::Many(mut children) = x else {
794                        panic!("unexpected biplate tree shape for quantified declaration")
795                    };
796
797                    let domain = children.pop_front().unwrap_or(Tree::Zero);
798                    let generator = children.pop_front().unwrap_or(Tree::Zero);
799
800                    let mut quantified2 = quantified.clone();
801                    quantified2.domain = recons_domain(domain);
802                    quantified2.generator = recons_generator(generator);
803                    DeclarationKind::Quantified(quantified2)
804                }),
805            )
806        }
807        DeclarationKind::QuantifiedExpr(expr) => {
808            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expr);
809            (
810                tree,
811                Box::new(move |x| DeclarationKind::QuantifiedExpr(recons_expr(x))),
812            )
813        }
814    }
815}
816
817impl IdPtr for DeclarationPtr {
818    type Data = Declaration;
819
820    fn get_data(&self) -> Self::Data {
821        self.read().clone()
822    }
823
824    fn with_id_and_data(id: ObjId, data: Self::Data) -> Self {
825        Self {
826            inner: DeclarationPtrInner::new_with_id_unchecked(RwLock::new(data), id),
827        }
828    }
829}
830
831impl Ord for DeclarationPtr {
832    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
833        self.inner.id.cmp(&other.inner.id)
834    }
835}
836
837impl PartialOrd for DeclarationPtr {
838    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
839        Some(self.cmp(other))
840    }
841}
842
843impl PartialEq for DeclarationPtr {
844    fn eq(&self, other: &Self) -> bool {
845        self.inner.id == other.inner.id
846    }
847}
848
849impl Eq for DeclarationPtr {}
850
851impl std::hash::Hash for DeclarationPtr {
852    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
853        // invariant: x == y -> hash(x) == hash(y)
854        self.inner.id.hash(state);
855    }
856}
857
858impl Display for DeclarationPtr {
859    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
860        let value: &Declaration = &self.read();
861        value.fmt(f)
862    }
863}
864
865#[derive(Clone, PartialEq, Debug, Serialize, Deserialize, Eq, Uniplate)]
866#[biplate(to=Expression)]
867#[biplate(to=DeclarationPtr)]
868#[biplate(to=Name)]
869/// The contents of a declaration
870pub struct Declaration {
871    /// The name of the declared symbol.
872    name: Name,
873
874    /// The kind of the declaration.
875    kind: DeclarationKind,
876}
877
878impl Declaration {
879    /// Creates a new declaration.
880    pub fn new(name: Name, kind: DeclarationKind) -> Declaration {
881        Declaration { name, kind }
882    }
883}
884
885/// A specific kind of declaration.
886#[non_exhaustive]
887#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
888#[biplate(to=Expression)]
889#[biplate(to=DeclarationPtr)]
890#[biplate(to=Declaration)]
891pub enum DeclarationKind {
892    Find(DecisionVariable),
893    Given(DomainPtr),
894    Quantified(Quantified),
895    QuantifiedExpr(Expression),
896
897    /// Carries an optional domain so instantiated `given`s can retain their declared domain.
898    ValueLetting(Expression, Option<DomainPtr>),
899    DomainLetting(DomainPtr),
900
901    /// A short-lived value binding used internally during rewrites (e.g. comprehension unrolling).
902    ///
903    /// Unlike `ValueLetting`, this is not intended to represent a user-visible top-level `letting`.
904    TemporaryValueLetting(Expression),
905
906    /// A named field inside a record type.
907    /// e.g. A, B in record{A: int(0..1), B: int(0..2)}
908    RecordField(DomainPtr),
909}
910
911#[serde_as]
912#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
913pub struct Quantified {
914    domain: DomainPtr,
915
916    #[serde_as(as = "Option<PtrAsInner>")]
917    generator: Option<DeclarationPtr>,
918}
919
920impl Quantified {
921    pub fn domain(&self) -> &DomainPtr {
922        &self.domain
923    }
924
925    pub fn generator(&self) -> Option<&DeclarationPtr> {
926        self.generator.as_ref()
927    }
928}
conjure_cp_core/ast/declaration.rs

conjure_cp_core/ast/
declaration.rs
