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    /// Creates a new value letting declaration.
191    ///
192    /// # Examples
193    ///
194    /// ```
195    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
196    /// Literal,Atom,Moo};
197    /// use conjure_cp_core::{matrix_expr,ast::Metadata};
198    ///
199    /// // letting n be 10 + 10
200    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
201    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
202    /// let declaration = DeclarationPtr::new_value_letting(
203    ///     Name::User("n".into()),
204    ///     expression);
205    ///
206    /// ```
207    pub fn new_value_letting(name: Name, expression: Expression) -> DeclarationPtr {
208        let kind = DeclarationKind::ValueLetting(expression, None);
209        DeclarationPtr::new(name, kind)
210    }
211
212    /// Creates a new value letting declaration with domain.
213    ///
214    /// # Examples
215    ///
216    /// ```
217    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range, Expression,
218    /// Literal,Atom,Moo,DomainPtr,Metadata};
219    /// use conjure_cp_core::{matrix_expr};
220    ///
221    /// // letting n be 10 + 10
222    /// let ten = Expression::Atomic(Metadata::new(),Atom::Literal(Literal::Int(10)));
223    /// let expression = Expression::Sum(Metadata::new(),Moo::new(matrix_expr![ten.clone(),ten]));
224    /// let domain = Domain::bool();
225    /// let declaration = DeclarationPtr::new_value_letting_with_domain(
226    ///     Name::User("n".into()),
227    ///     expression,
228    ///     domain,
229    /// );
230    /// ```
231    pub fn new_value_letting_with_domain(
232        name: Name,
233        expression: Expression,
234        domain: DomainPtr,
235    ) -> DeclarationPtr {
236        let kind = DeclarationKind::ValueLetting(expression, Some(domain));
237        DeclarationPtr::new(name, kind)
238    }
239
240    /// Creates a new domain letting declaration.
241    ///
242    /// # Examples
243    ///
244    /// ```
245    /// use conjure_cp_core::ast::{DeclarationPtr,Name,DeclarationKind,Domain,Range};
246    ///
247    /// // letting MyDomain be int(1..5)
248    /// let declaration = DeclarationPtr::new_domain_letting(
249    ///     Name::User("MyDomain".into()),
250    ///     Domain::int(vec![Range::Bounded(1,5)]));
251    ///
252    /// ```
253    pub fn new_domain_letting(name: Name, domain: DomainPtr) -> DeclarationPtr {
254        let kind = DeclarationKind::DomainLetting(domain);
255        DeclarationPtr::new(name, kind)
256    }
257
258    /// Creates a new record field declaration.
259    ///
260    /// # Examples
261    ///
262    /// ```
263    /// use conjure_cp_core::ast::{DeclarationPtr,Name,RecordEntry,Domain,Range};
264    ///
265    /// // create declaration for field A in `find rec: record {A: int(0..1), B: int(0..2)}`
266    ///
267    /// let field = RecordEntry {
268    ///     name: Name::User("n".into()),
269    ///     domain: Domain::int(vec![Range::Bounded(1,5)])
270    /// };
271    ///
272    /// let declaration = DeclarationPtr::new_record_field(field);
273    /// ```
274    pub fn new_record_field(entry: RecordEntry) -> DeclarationPtr {
275        let kind = DeclarationKind::RecordField(entry.domain);
276        DeclarationPtr::new(entry.name, kind)
277    }
278
279    /**********************************************/
280    /*        Declaration accessor methods        */
281    /**********************************************/
282
283    /// Gets the domain of the declaration, if it has one.
284    ///
285    /// # Examples
286    ///
287    /// ```
288    /// use conjure_cp_core::ast::{DeclarationPtr, Name, Domain, Range, GroundDomain};
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    ///
293    /// assert!(declaration.domain().is_some_and(|x| x.as_ground().unwrap() == &GroundDomain::Int(vec![Range::Bounded(1,5)])))
294    ///
295    /// ```
296    pub fn domain(&self) -> Option<DomainPtr> {
297        match &self.kind() as &DeclarationKind {
298            DeclarationKind::Find(var) => Some(var.domain_of()),
299            DeclarationKind::ValueLetting(e, _) | DeclarationKind::TemporaryValueLetting(e) => {
300                e.domain_of()
301            }
302            DeclarationKind::DomainLetting(domain) => Some(domain.clone()),
303            DeclarationKind::Given(domain) => Some(domain.clone()),
304            DeclarationKind::Quantified(inner) => Some(inner.domain.clone()),
305            DeclarationKind::RecordField(domain) => Some(domain.clone()),
306        }
307    }
308
309    /// Gets the domain of the declaration and fully resolve it
310    pub fn resolved_domain(&self) -> Option<Moo<GroundDomain>> {
311        self.domain()?.resolve()
312    }
313
314    /// Gets the kind of the declaration.
315    ///
316    /// # Examples
317    ///
318    /// ```
319    /// use conjure_cp_core::ast::{DeclarationPtr,DeclarationKind,Name,Domain,Range};
320    ///
321    /// // find a: int(1..5)
322    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
323    /// assert!(matches!(&declaration.kind() as &DeclarationKind, DeclarationKind::Find(_)))
324    /// ```
325    pub fn kind(&self) -> MappedRwLockReadGuard<'_, DeclarationKind> {
326        self.map(|x| &x.kind)
327    }
328
329    /// Gets the name of the declaration.
330    ///
331    /// # Examples
332    ///
333    /// ```
334    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
335    ///
336    /// // find a: int(1..5)
337    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
338    ///
339    /// assert_eq!(&declaration.name() as &Name, &Name::User("a".into()))
340    /// ```
341    pub fn name(&self) -> MappedRwLockReadGuard<'_, Name> {
342        self.map(|x| &x.name)
343    }
344
345    /// This declaration as a decision variable, if it is one.
346    pub fn as_find(&self) -> Option<MappedRwLockReadGuard<'_, DecisionVariable>> {
347        RwLockReadGuard::try_map(self.read(), |x| {
348            if let DeclarationKind::Find(var) = &x.kind {
349                Some(var)
350            } else {
351                None
352            }
353        })
354        .ok()
355    }
356
357    /// This declaration as a mutable decision variable, if it is one.
358    pub fn as_find_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DecisionVariable>> {
359        RwLockWriteGuard::try_map(self.write(), |x| {
360            if let DeclarationKind::Find(var) = &mut x.kind {
361                Some(var)
362            } else {
363                None
364            }
365        })
366        .ok()
367    }
368
369    /// This declaration as a domain letting, if it is one.
370    pub fn as_domain_letting(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
371        RwLockReadGuard::try_map(self.read(), |x| {
372            if let DeclarationKind::DomainLetting(domain) = &x.kind {
373                Some(domain)
374            } else {
375                None
376            }
377        })
378        .ok()
379    }
380
381    /// This declaration as a mutable domain letting, if it is one.
382    pub fn as_domain_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DomainPtr>> {
383        RwLockWriteGuard::try_map(self.write(), |x| {
384            if let DeclarationKind::DomainLetting(domain) = &mut x.kind {
385                Some(domain)
386            } else {
387                None
388            }
389        })
390        .ok()
391    }
392
393    /// This declaration as a value letting, if it is one.
394    pub fn as_value_letting(&self) -> Option<MappedRwLockReadGuard<'_, Expression>> {
395        RwLockReadGuard::try_map(self.read(), |x| {
396            if let DeclarationKind::ValueLetting(expression, _)
397            | DeclarationKind::TemporaryValueLetting(expression) = &x.kind
398            {
399                Some(expression)
400            } else {
401                None
402            }
403        })
404        .ok()
405    }
406
407    /// This declaration as a mutable value letting, if it is one.
408    pub fn as_value_letting_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, Expression>> {
409        RwLockWriteGuard::try_map(self.write(), |x| {
410            if let DeclarationKind::ValueLetting(expression, _)
411            | DeclarationKind::TemporaryValueLetting(expression) = &mut x.kind
412            {
413                Some(expression)
414            } else {
415                None
416            }
417        })
418        .ok()
419    }
420
421    /// This declaration as a given statement, if it is one.
422    pub fn as_given(&self) -> Option<MappedRwLockReadGuard<'_, DomainPtr>> {
423        RwLockReadGuard::try_map(self.read(), |x| {
424            if let DeclarationKind::Given(domain) = &x.kind {
425                Some(domain)
426            } else {
427                None
428            }
429        })
430        .ok()
431    }
432
433    /// This declaration as a mutable given statement, if it is one.
434    pub fn as_given_mut(&mut self) -> Option<MappedRwLockWriteGuard<'_, DomainPtr>> {
435        RwLockWriteGuard::try_map(self.write(), |x| {
436            if let DeclarationKind::Given(domain) = &mut x.kind {
437                Some(domain)
438            } else {
439                None
440            }
441        })
442        .ok()
443    }
444
445    /// Changes the name in this declaration, returning the old one.
446    ///
447    /// # Examples
448    ///
449    /// ```
450    /// use conjure_cp_core::ast::{DeclarationPtr, Domain, Range, Name};
451    ///
452    /// // find a: int(1..5)
453    /// let mut declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
454    ///
455    /// let old_name = declaration.replace_name(Name::User("b".into()));
456    /// assert_eq!(old_name,Name::User("a".into()));
457    /// assert_eq!(&declaration.name() as &Name,&Name::User("b".into()));
458    /// ```
459    pub fn replace_name(&mut self, name: Name) -> Name {
460        let mut decl = self.write();
461        std::mem::replace(&mut decl.name, name)
462    }
463
464    /// Replaces the underlying declaration kind and returns the previous kind.
465    /// Note: this affects all cloned `DeclarationPtr`s pointing to the same declaration.
466    pub fn replace_kind(&mut self, kind: DeclarationKind) -> DeclarationKind {
467        let mut decl = self.write();
468        std::mem::replace(&mut decl.kind, kind)
469    }
470
471    /*****************************************/
472    /*        Pointer utility methods        */
473    /*****************************************/
474
475    // These are mostly wrappers over RefCell, Ref, and RefMut methods, re-exported here for
476    // convenience.
477
478    /// Read the underlying [Declaration].
479    ///
480    /// Will block the current thread until no other thread has a write lock.
481    /// Attempting to get a read lock if the current thread already has one
482    /// **will** cause it to deadlock.
483    /// The lock is released when the returned guard goes out of scope.
484    fn read(&self) -> RwLockReadGuard<'_, Declaration> {
485        self.inner.value.read()
486    }
487
488    /// Write the underlying [Declaration].
489    ///
490    /// Will block the current thread until no other thread has a read or write lock.
491    /// The lock is released when the returned guard goes out of scope.
492    fn write(&mut self) -> RwLockWriteGuard<'_, Declaration> {
493        self.inner.value.write()
494    }
495
496    /// Creates a new declaration pointer with the same contents as `self` that is not shared with
497    /// anyone else.
498    ///
499    /// As the resulting pointer is unshared, it will have a new id.
500    ///
501    /// # Examples
502    ///
503    /// ```
504    /// use conjure_cp_core::ast::{DeclarationPtr,Name,Domain,Range};
505    ///
506    /// // find a: int(1..5)
507    /// let declaration = DeclarationPtr::new_find(Name::User("a".into()),Domain::int(vec![Range::Bounded(1,5)]));
508    ///
509    /// let mut declaration2 = declaration.clone();
510    ///
511    /// declaration2.replace_name(Name::User("b".into()));
512    ///
513    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
514    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
515    ///
516    /// declaration2 = declaration2.detach();
517    ///
518    /// assert_eq!(&declaration2.name() as &Name, &Name::User("b".into()));
519    ///
520    /// declaration2.replace_name(Name::User("c".into()));
521    ///
522    /// assert_eq!(&declaration.name() as &Name, &Name::User("b".into()));
523    /// assert_eq!(&declaration2.name() as &Name, &Name::User("c".into()));
524    /// ```
525    pub fn detach(self) -> DeclarationPtr {
526        // despite having the same contents, the new declaration pointer is unshared, so it should
527        // get a new id.
528        let value = self.inner.value.read().clone();
529        DeclarationPtr {
530            inner: DeclarationPtrInner::new(RwLock::new(value)),
531        }
532    }
533
534    /// Applies `f` to the declaration, returning the result as a reference.
535    fn map<U>(&self, f: impl FnOnce(&Declaration) -> &U) -> MappedRwLockReadGuard<'_, U> {
536        RwLockReadGuard::map(self.read(), f)
537    }
538
539    /// Applies mutable function `f` to the declaration, returning the result as a mutable reference.
540    fn map_mut<U>(
541        &mut self,
542        f: impl FnOnce(&mut Declaration) -> &mut U,
543    ) -> MappedRwLockWriteGuard<'_, U> {
544        RwLockWriteGuard::map(self.write(), f)
545    }
546
547    /// Replaces the declaration with a new one, returning the old value, without deinitialising
548    /// either one.
549    pub fn replace(&mut self, declaration: Declaration) -> Declaration {
550        let mut guard = self.write();
551        let ans = mem::replace(&mut *guard, declaration);
552        drop(guard);
553        ans
554    }
555}
556
557impl CategoryOf for DeclarationPtr {
558    fn category_of(&self) -> Category {
559        match &self.kind() as &DeclarationKind {
560            DeclarationKind::Find(decision_variable) => decision_variable.category_of(),
561            DeclarationKind::ValueLetting(expression, _)
562            | DeclarationKind::TemporaryValueLetting(expression) => expression.category_of(),
563            DeclarationKind::DomainLetting(_) => Category::Constant,
564            DeclarationKind::Given(_) => Category::Parameter,
565            DeclarationKind::Quantified(..) => Category::Quantified,
566            DeclarationKind::RecordField(_) => Category::Bottom,
567        }
568    }
569}
570impl HasId for DeclarationPtr {
571    const TYPE_NAME: &'static str = "DeclarationPtrInner";
572    fn id(&self) -> ObjId {
573        self.inner.id.clone()
574    }
575}
576
577impl DefaultWithId for DeclarationPtr {
578    fn default_with_id(id: ObjId) -> Self {
579        DeclarationPtr {
580            inner: DeclarationPtrInner::new_with_id_unchecked(
581                RwLock::new(Declaration {
582                    name: Name::User("_UNKNOWN".into()),
583                    kind: DeclarationKind::ValueLetting(false.into(), None),
584                }),
585                id,
586            ),
587        }
588    }
589}
590
591impl Typeable for DeclarationPtr {
592    fn return_type(&self) -> ReturnType {
593        match &self.kind() as &DeclarationKind {
594            DeclarationKind::Find(var) => var.return_type(),
595            DeclarationKind::ValueLetting(expression, _)
596            | DeclarationKind::TemporaryValueLetting(expression) => expression.return_type(),
597            DeclarationKind::DomainLetting(domain) => domain.return_type(),
598            DeclarationKind::Given(domain) => domain.return_type(),
599            DeclarationKind::Quantified(inner) => inner.domain.return_type(),
600            DeclarationKind::RecordField(domain) => domain.return_type(),
601        }
602    }
603}
604
605impl Uniplate for DeclarationPtr {
606    fn uniplate(&self) -> (Tree<Self>, Box<dyn Fn(Tree<Self>) -> Self>) {
607        let decl = self.read();
608        let (tree, recons) = Biplate::<DeclarationPtr>::biplate(&decl as &Declaration);
609
610        let self2 = self.clone();
611        (
612            tree,
613            Box::new(move |x| {
614                let mut self3 = self2.clone();
615                let inner = recons(x);
616                *(&mut self3.write() as &mut Declaration) = inner;
617                self3
618            }),
619        )
620    }
621}
622
623impl<To> Biplate<To> for DeclarationPtr
624where
625    Declaration: Biplate<To>,
626    To: Uniplate,
627{
628    fn biplate(&self) -> (Tree<To>, Box<dyn Fn(Tree<To>) -> Self>) {
629        if TypeId::of::<To>() == TypeId::of::<Self>() {
630            unsafe {
631                let self_as_to = std::mem::transmute::<&Self, &To>(self).clone();
632                (
633                    Tree::One(self_as_to),
634                    Box::new(move |x| {
635                        let Tree::One(x) = x else { panic!() };
636
637                        let x_as_self = std::mem::transmute::<&To, &Self>(&x);
638                        x_as_self.clone()
639                    }),
640                )
641            }
642        } else {
643            // call biplate on the enclosed declaration
644            let decl = self.read();
645            let (tree, recons) = Biplate::<To>::biplate(&decl as &Declaration);
646
647            let self2 = self.clone();
648            (
649                tree,
650                Box::new(move |x| {
651                    let mut self3 = self2.clone();
652                    let inner = recons(x);
653                    *(&mut self3.write() as &mut Declaration) = inner;
654                    self3
655                }),
656            )
657        }
658    }
659}
660
661type ReferenceTree = Tree<Reference>;
662type ReferenceReconstructor<T> = Box<dyn Fn(ReferenceTree) -> T>;
663
664impl Biplate<Reference> for DeclarationPtr {
665    fn biplate(&self) -> (ReferenceTree, ReferenceReconstructor<Self>) {
666        let (tree, recons_kind) = biplate_declaration_kind_references(self.kind().clone());
667
668        let self2 = self.clone();
669        (
670            tree,
671            Box::new(move |x| {
672                let mut self3 = self2.clone();
673                let _ = self3.replace_kind(recons_kind(x));
674                self3
675            }),
676        )
677    }
678}
679
680fn biplate_domain_ptr_references(
681    domain: DomainPtr,
682) -> (ReferenceTree, ReferenceReconstructor<DomainPtr>) {
683    let domain_inner = domain.as_ref().clone();
684    let (tree, recons_domain) = Biplate::<Reference>::biplate(&domain_inner);
685    (tree, Box::new(move |x| Moo::new(recons_domain(x))))
686}
687
688fn biplate_declaration_kind_references(
689    kind: DeclarationKind,
690) -> (ReferenceTree, ReferenceReconstructor<DeclarationKind>) {
691    match kind {
692        DeclarationKind::Find(var) => {
693            let (tree, recons_domain) = biplate_domain_ptr_references(var.domain.clone());
694            (
695                tree,
696                Box::new(move |x| {
697                    let mut var2 = var.clone();
698                    var2.domain = recons_domain(x);
699                    DeclarationKind::Find(var2)
700                }),
701            )
702        }
703        DeclarationKind::Given(domain) => {
704            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
705            (
706                tree,
707                Box::new(move |x| DeclarationKind::Given(recons_domain(x))),
708            )
709        }
710        DeclarationKind::DomainLetting(domain) => {
711            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
712            (
713                tree,
714                Box::new(move |x| DeclarationKind::DomainLetting(recons_domain(x))),
715            )
716        }
717        DeclarationKind::RecordField(domain) => {
718            let (tree, recons_domain) = biplate_domain_ptr_references(domain);
719            (
720                tree,
721                Box::new(move |x| DeclarationKind::RecordField(recons_domain(x))),
722            )
723        }
724        DeclarationKind::ValueLetting(expression, domain) => {
725            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expression);
726            (
727                tree,
728                Box::new(move |x| DeclarationKind::ValueLetting(recons_expr(x), domain.clone())),
729            )
730        }
731        DeclarationKind::TemporaryValueLetting(expression) => {
732            let (tree, recons_expr) = Biplate::<Reference>::biplate(&expression);
733            (
734                tree,
735                Box::new(move |x| DeclarationKind::TemporaryValueLetting(recons_expr(x))),
736            )
737        }
738        DeclarationKind::Quantified(quantified) => {
739            let (domain_tree, recons_domain) =
740                biplate_domain_ptr_references(quantified.domain.clone());
741
742            let (generator_tree, recons_generator) = if let Some(generator) = quantified.generator()
743            {
744                let generator = generator.clone();
745                let (tree, recons_declaration) = Biplate::<Reference>::biplate(&generator);
746                (
747                    tree,
748                    Box::new(move |x| Some(recons_declaration(x)))
749                        as ReferenceReconstructor<Option<DeclarationPtr>>,
750                )
751            } else {
752                (
753                    Tree::Zero,
754                    Box::new(|_| None) as ReferenceReconstructor<Option<DeclarationPtr>>,
755                )
756            };
757
758            (
759                Tree::Many(VecDeque::from([domain_tree, generator_tree])),
760                Box::new(move |x| {
761                    let Tree::Many(mut children) = x else {
762                        panic!("unexpected biplate tree shape for quantified declaration")
763                    };
764
765                    let domain = children.pop_front().unwrap_or(Tree::Zero);
766                    let generator = children.pop_front().unwrap_or(Tree::Zero);
767
768                    let mut quantified2 = quantified.clone();
769                    quantified2.domain = recons_domain(domain);
770                    quantified2.generator = recons_generator(generator);
771                    DeclarationKind::Quantified(quantified2)
772                }),
773            )
774        }
775    }
776}
777
778impl IdPtr for DeclarationPtr {
779    type Data = Declaration;
780
781    fn get_data(&self) -> Self::Data {
782        self.read().clone()
783    }
784
785    fn with_id_and_data(id: ObjId, data: Self::Data) -> Self {
786        Self {
787            inner: DeclarationPtrInner::new_with_id_unchecked(RwLock::new(data), id),
788        }
789    }
790}
791
792impl Ord for DeclarationPtr {
793    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
794        self.inner.id.cmp(&other.inner.id)
795    }
796}
797
798impl PartialOrd for DeclarationPtr {
799    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
800        Some(self.cmp(other))
801    }
802}
803
804impl PartialEq for DeclarationPtr {
805    fn eq(&self, other: &Self) -> bool {
806        self.inner.id == other.inner.id
807    }
808}
809
810impl Eq for DeclarationPtr {}
811
812impl std::hash::Hash for DeclarationPtr {
813    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
814        // invariant: x == y -> hash(x) == hash(y)
815        self.inner.id.hash(state);
816    }
817}
818
819impl Display for DeclarationPtr {
820    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
821        let value: &Declaration = &self.read();
822        value.fmt(f)
823    }
824}
825
826#[derive(Clone, PartialEq, Debug, Serialize, Deserialize, Eq, Uniplate)]
827#[biplate(to=Expression)]
828#[biplate(to=DeclarationPtr)]
829#[biplate(to=Name)]
830/// The contents of a declaration
831pub struct Declaration {
832    /// The name of the declared symbol.
833    name: Name,
834
835    /// The kind of the declaration.
836    kind: DeclarationKind,
837}
838
839impl Declaration {
840    /// Creates a new declaration.
841    pub fn new(name: Name, kind: DeclarationKind) -> Declaration {
842        Declaration { name, kind }
843    }
844}
845
846/// A specific kind of declaration.
847#[non_exhaustive]
848#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
849#[biplate(to=Expression)]
850#[biplate(to=DeclarationPtr)]
851#[biplate(to=Declaration)]
852pub enum DeclarationKind {
853    Find(DecisionVariable),
854    Given(DomainPtr),
855    Quantified(Quantified),
856
857    /// Carries an optional domain so instantiated `given`s can retain their declared domain.
858    ValueLetting(Expression, Option<DomainPtr>),
859    DomainLetting(DomainPtr),
860
861    /// A short-lived value binding used internally during rewrites (e.g. comprehension unrolling).
862    ///
863    /// Unlike `ValueLetting`, this is not intended to represent a user-visible top-level `letting`.
864    TemporaryValueLetting(Expression),
865
866    /// A named field inside a record type.
867    /// e.g. A, B in record{A: int(0..1), B: int(0..2)}
868    RecordField(DomainPtr),
869}
870
871#[serde_as]
872#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Uniplate)]
873pub struct Quantified {
874    domain: DomainPtr,
875
876    #[serde_as(as = "Option<PtrAsInner>")]
877    generator: Option<DeclarationPtr>,
878}
879
880impl Quantified {
881    pub fn domain(&self) -> &DomainPtr {
882        &self.domain
883    }
884
885    pub fn generator(&self) -> Option<&DeclarationPtr> {
886        self.generator.as_ref()
887    }
888}
conjure_cp_core/ast/declaration.rs

conjure_cp_core/ast/
declaration.rs
