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

conjure_cp_core/ast/
declaration.rs
