conjure_cp_core/ast/
declaration.rs

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

conjure_cp_core/ast/
declaration.rs
