conjure_cp_core/representation/
uniform.rs

1//! Model-scoped representation choices for `--channelling uniform`.
2//!
3//! Choices concern the outer type family, ignoring domain bounds and element types. Integer
4//! encoding is separate from matrix layout. State is scoped to a rewrite, including nested
5//! rewrites, so enumerated models and subsequent solves never inherit another model's choices.
6use super::{ReprInitError, ReprRulePtr};
7use crate::ast::{DomainPtr, ReturnType, Typeable};
8use crate::settings::{Channelling, channelling};
9use std::cell::RefCell;
10use std::collections::HashMap;
11use std::mem::{Discriminant, discriminant};
12
13pub(crate) type Choices = HashMap<Discriminant<ReturnType>, ReprRulePtr>;
14thread_local! {
15    static CHOICES: RefCell<Choices> = RefCell::new(HashMap::new());
16}
17
18fn family(dom: &DomainPtr, rule: ReprRulePtr) -> Discriminant<ReturnType> {
19    discriminant(&if rule.is_integer_encoding() {
20        ReturnType::Int
21    } else {
22        dom.return_type()
23    })
24}
25
26/// Return the uniform representation selected for this type in the current model.
27pub fn selected(dom: &DomainPtr, integer_encoding: bool) -> Option<ReprRulePtr> {
28    if channelling() != Channelling::Uniform {
29        return None;
30    }
31    let key = discriminant(&if integer_encoding {
32        ReturnType::Int
33    } else {
34        dom.return_type()
35    });
36    CHOICES.with(|choices| choices.borrow().get(&key).copied())
37}
38
39pub(crate) fn check_choice(dom: &DomainPtr, rule: ReprRulePtr) -> Result<(), ReprInitError> {
40    if channelling() == Channelling::Uniform
41        && let Some(existing) =
42            CHOICES.with(|choices| choices.borrow().get(&family(dom, rule)).copied())
43        && existing.id() != rule.id()
44    {
45        return Err(ReprInitError::UniformConflict {
46            domain: dom.clone(),
47            existing: existing.name(),
48            requested: rule.name(),
49        });
50    }
51    Ok(())
52}
53
54pub(crate) fn reset() {
55    CHOICES.with(|choices| choices.borrow_mut().clear());
56}
57
58pub(crate) fn record_choice(dom: &DomainPtr, rule: ReprRulePtr) {
59    if channelling() == Channelling::Uniform {
60        CHOICES.with(|choices| {
61            choices.borrow_mut().insert(family(dom, rule), rule);
62        });
63    }
64}
65
66/// Restore the enclosing rewrite's choices even on early return or panic.
67pub(crate) struct Scope(Choices);
68impl Scope {
69    pub(crate) fn new() -> Self {
70        Self(CHOICES.with(|choices| std::mem::take(&mut *choices.borrow_mut())))
71    }
72}
73impl Drop for Scope {
74    fn drop(&mut self) {
75        CHOICES.with(|choices| *choices.borrow_mut() = std::mem::take(&mut self.0));
76    }
77}
78
79/// Representation probes instantiate a detached declaration. They must not select a family.
80pub(crate) fn probe<T>(f: impl FnOnce() -> T) -> T {
81    if channelling() != Channelling::Uniform {
82        return f();
83    }
84    let _restore = Scope(CHOICES.with(|choices| choices.borrow().clone()));
85    f()
86}
87
88/// Rule applicability is speculative. Commit choices only for the selected effect.
89pub(crate) fn attempt(
90    f: impl FnOnce() -> crate::rule_engine::ApplicationResult,
91) -> crate::rule_engine::ApplicationResult {
92    if channelling() != Channelling::Uniform {
93        return f();
94    }
95    let previous = CHOICES.with(|choices| choices.borrow().clone());
96    let restore = Scope(previous.clone());
97    let result = f().map(|mut effect| {
98        effect.uniform_choices = CHOICES.with(|choices| {
99            choices
100                .borrow()
101                .iter()
102                .filter(|(key, _)| !previous.contains_key(*key))
103                .map(|(key, rule)| (*key, *rule))
104                .collect()
105        });
106        effect
107    });
108    drop(restore);
109    result
110}
111
112pub(crate) fn commit(choices: Choices) {
113    if channelling() == Channelling::Uniform {
114        CHOICES.with(|current| current.borrow_mut().extend(choices));
115    }
116}
conjure_cp_core/representation/uniform.rs

conjure_cp_core/representation/
uniform.rs
