Skip to main content

omena_abstract_value/
guarded_token_map.rs

1use std::collections::{BTreeMap, BTreeSet};
2
3use omena_cascade::{
4    FALSE_NODE_ID_V0, FirstWitnessErrorV0, FirstWitnessManagerConfigV0, FirstWitnessManagerV0,
5    NodeId, TRUE_NODE_ID_V0, VariableOrderRegistrationV0,
6};
7use omena_syntax::ident::{CanonicalClassKeyV0, ClassNameV0};
8use serde::{Serialize, Serializer};
9
10#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
11pub enum GuardedTokenLanguageV0 {
12    Concrete(CanonicalClassKeyV0),
13    Symbolic { raw_language: String },
14}
15
16impl GuardedTokenLanguageV0 {
17    pub fn concrete(authored: impl Into<String>) -> Self {
18        Self::Concrete(ClassNameV0::new(authored).canonical_key())
19    }
20
21    pub fn symbolic(raw_language: impl Into<String>) -> Self {
22        Self::Symbolic {
23            raw_language: raw_language.into(),
24        }
25    }
26
27    pub fn label(&self) -> &str {
28        match self {
29            Self::Concrete(token) => token.as_str(),
30            Self::Symbolic { raw_language } => raw_language,
31        }
32    }
33}
34
35impl Serialize for GuardedTokenLanguageV0 {
36    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
37    where
38        S: Serializer,
39    {
40        serializer.serialize_str(self.label())
41    }
42}
43
44#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Serialize)]
45#[serde(rename_all = "camelCase")]
46pub struct GuardAtomV0 {
47    pub atom: String,
48    pub polarity: bool,
49}
50
51#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
52#[serde(rename_all = "camelCase")]
53pub struct TokenObserverProjectionV0 {
54    pub raw_string: String,
55    pub ordered_word: Vec<String>,
56    pub support_set: BTreeSet<String>,
57}
58
59impl TokenObserverProjectionV0 {
60    pub fn exact(token: &GuardedTokenLanguageV0) -> Self {
61        let token = token.label().to_string();
62        Self {
63            raw_string: token.clone(),
64            ordered_word: vec![token.clone()],
65            support_set: BTreeSet::from([token]),
66        }
67    }
68}
69
70#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
71#[serde(rename_all = "camelCase")]
72pub struct GuardedTokenInputV0 {
73    pub token: GuardedTokenLanguageV0,
74    pub guards: Vec<GuardAtomV0>,
75    pub observers: TokenObserverProjectionV0,
76}
77
78#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
79#[serde(rename_all = "camelCase")]
80pub struct GuardedTokenMapInputV0 {
81    pub tokens: Vec<GuardedTokenInputV0>,
82    pub site_usage_guards: Vec<GuardAtomV0>,
83}
84
85#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
86#[serde(rename_all = "camelCase")]
87pub enum GuardedTokenObserverV0 {
88    RawString,
89    OrderedWord,
90    SupportSet,
91}
92
93#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
94#[serde(rename_all = "camelCase")]
95pub struct PresenceConditionV0 {
96    pub root: NodeId,
97}
98
99#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
100#[serde(rename_all = "camelCase")]
101pub struct GuardedTokenMapEntryV0 {
102    pub token: GuardedTokenLanguageV0,
103    pub condition: PresenceConditionV0,
104    pub observers: TokenObserverProjectionV0,
105}
106
107#[derive(Debug, Clone)]
108pub struct GuardedTokenMapV0 {
109    manager: FirstWitnessManagerV0,
110    entries: Vec<GuardedTokenMapEntryV0>,
111    site_usage: PresenceConditionV0,
112}
113
114impl GuardedTokenMapV0 {
115    /// Builds a free-boolean condition map.
116    ///
117    /// Treating predicates as independent atoms enlarges the assignment space,
118    /// so an unsatisfiable or tautological result remains sound under later
119    /// refinement. Precision may be lost. Numeric predicate relationships are
120    /// deliberately not inferred here.
121    pub fn build(input: GuardedTokenMapInputV0) -> Result<Self, FirstWitnessErrorV0> {
122        Self::build_with_config(input, FirstWitnessManagerConfigV0::default())
123    }
124
125    pub fn build_with_config(
126        input: GuardedTokenMapInputV0,
127        config: FirstWitnessManagerConfigV0,
128    ) -> Result<Self, FirstWitnessErrorV0> {
129        let first_appearance = input
130            .tokens
131            .iter()
132            .flat_map(|token| token.guards.iter())
133            .chain(input.site_usage_guards.iter())
134            .map(|guard| guard.atom.clone())
135            .collect::<Vec<_>>();
136        let order = VariableOrderRegistrationV0::site_first_appearance(first_appearance)?;
137        let mut manager = FirstWitnessManagerV0::new(order, config);
138        let site_usage = condition_from_guards(&mut manager, &input.site_usage_guards)?;
139        let mut entries = BTreeMap::<GuardedTokenLanguageV0, GuardedTokenMapEntryV0>::new();
140        for token in input.tokens {
141            let condition = condition_from_guards(&mut manager, &token.guards)?;
142            if let Some(existing) = entries.get_mut(&token.token) {
143                existing.condition.root = manager.or(existing.condition.root, condition)?;
144            } else {
145                entries.insert(
146                    token.token.clone(),
147                    GuardedTokenMapEntryV0 {
148                        token: token.token,
149                        condition: PresenceConditionV0 { root: condition },
150                        observers: token.observers,
151                    },
152                );
153            }
154        }
155        Ok(Self {
156            manager,
157            entries: entries.into_values().collect(),
158            site_usage: PresenceConditionV0 { root: site_usage },
159        })
160    }
161
162    pub fn entries(&self) -> &[GuardedTokenMapEntryV0] {
163        &self.entries
164    }
165
166    pub fn manager(&self) -> &FirstWitnessManagerV0 {
167        &self.manager
168    }
169
170    pub fn condition(&self, token: &GuardedTokenLanguageV0) -> Option<PresenceConditionV0> {
171        self.entry(token).map(|entry| entry.condition.clone())
172    }
173
174    pub fn is_must(&self, token: &GuardedTokenLanguageV0) -> bool {
175        self.entry(token)
176            .is_some_and(|entry| self.manager.is_tautology(entry.condition.root))
177    }
178
179    pub fn is_may(&self, token: &GuardedTokenLanguageV0) -> bool {
180        self.entry(token)
181            .is_some_and(|entry| self.manager.is_satisfiable(entry.condition.root))
182    }
183
184    pub fn is_dead_css(
185        &mut self,
186        token: &GuardedTokenLanguageV0,
187    ) -> Result<bool, FirstWitnessErrorV0> {
188        let condition = self
189            .entry(token)
190            .map(|entry| entry.condition.root)
191            .unwrap_or(FALSE_NODE_ID_V0);
192        let conjunction = self.manager.and(condition, self.site_usage.root)?;
193        Ok(!self.manager.is_satisfiable(conjunction))
194    }
195
196    pub fn rename_is_safe(
197        &self,
198        from: &GuardedTokenLanguageV0,
199        to: &GuardedTokenLanguageV0,
200        observer: GuardedTokenObserverV0,
201    ) -> bool {
202        let Some(from) = self.entry(from) else {
203            return false;
204        };
205        let Some(to) = self.entry(to) else {
206            return false;
207        };
208        if from.condition.root != to.condition.root {
209            return false;
210        }
211        match observer {
212            GuardedTokenObserverV0::RawString => {
213                from.observers.raw_string == to.observers.raw_string
214            }
215            GuardedTokenObserverV0::OrderedWord => {
216                from.observers.ordered_word == to.observers.ordered_word
217            }
218            GuardedTokenObserverV0::SupportSet => {
219                from.observers.support_set == to.observers.support_set
220            }
221        }
222    }
223
224    pub fn reclaim_if_due(
225        &mut self,
226    ) -> Result<Option<omena_cascade::FirstWitnessRebuildReportV0>, FirstWitnessErrorV0> {
227        let mut roots = self
228            .entries
229            .iter()
230            .map(|entry| entry.condition.root)
231            .chain(std::iter::once(self.site_usage.root))
232            .collect::<Vec<_>>();
233        let report = self.manager.reclaim_if_due(&mut roots)?;
234        if report.is_some() {
235            for (entry, root) in self.entries.iter_mut().zip(roots.iter().copied()) {
236                entry.condition.root = root;
237            }
238            self.site_usage.root = roots.last().copied().unwrap_or(TRUE_NODE_ID_V0);
239        }
240        Ok(report)
241    }
242
243    fn entry(&self, token: &GuardedTokenLanguageV0) -> Option<&GuardedTokenMapEntryV0> {
244        self.entries.iter().find(|entry| &entry.token == token)
245    }
246}
247
248fn condition_from_guards(
249    manager: &mut FirstWitnessManagerV0,
250    guards: &[GuardAtomV0],
251) -> Result<NodeId, FirstWitnessErrorV0> {
252    let mut root = TRUE_NODE_ID_V0;
253    for guard in guards {
254        let variable = manager.variable(&guard.atom)?;
255        let literal = if guard.polarity {
256            variable
257        } else {
258            manager.not(variable)?
259        };
260        root = manager.and(root, literal)?;
261    }
262    Ok(root)
263}
264
265#[cfg(test)]
266mod tests {
267    use super::*;
268
269    fn guarded(token: &str, guards: Vec<GuardAtomV0>) -> GuardedTokenInputV0 {
270        let token = GuardedTokenLanguageV0::concrete(token);
271        GuardedTokenInputV0 {
272            observers: TokenObserverProjectionV0::exact(&token),
273            token,
274            guards,
275        }
276    }
277
278    fn atom(atom: &str, polarity: bool) -> GuardAtomV0 {
279        GuardAtomV0 {
280            atom: atom.to_string(),
281            polarity,
282        }
283    }
284
285    #[test]
286    fn diagram_answers_must_may_dead_css_and_observer_rename() -> Result<(), FirstWitnessErrorV0> {
287        let always = GuardedTokenLanguageV0::concrete("always");
288        let maybe = GuardedTokenLanguageV0::concrete("maybe");
289        let impossible = GuardedTokenLanguageV0::concrete("impossible");
290        let raw_alias = GuardedTokenLanguageV0::symbolic("alias-raw");
291        let ordered_alias = GuardedTokenLanguageV0::symbolic("alias-ordered");
292        let shared_observers = TokenObserverProjectionV0 {
293            raw_string: "different-raw-a".to_string(),
294            ordered_word: vec!["same".to_string()],
295            support_set: BTreeSet::from(["same".to_string()]),
296        };
297        let mut map = GuardedTokenMapV0::build(GuardedTokenMapInputV0 {
298            tokens: vec![
299                guarded("always", vec![atom("c", true)]),
300                guarded("always", vec![atom("c", false)]),
301                guarded("maybe", vec![atom("c", true)]),
302                guarded("impossible", vec![atom("c", true), atom("c", false)]),
303                GuardedTokenInputV0 {
304                    token: raw_alias.clone(),
305                    guards: vec![atom("c", true)],
306                    observers: shared_observers.clone(),
307                },
308                GuardedTokenInputV0 {
309                    token: ordered_alias.clone(),
310                    guards: vec![atom("c", true)],
311                    observers: TokenObserverProjectionV0 {
312                        raw_string: "different-raw-b".to_string(),
313                        ..shared_observers
314                    },
315                },
316            ],
317            site_usage_guards: Vec::new(),
318        })?;
319        assert!(map.is_must(&always));
320        assert!(map.is_may(&maybe));
321        assert!(map.is_dead_css(&impossible)?);
322        assert!(!map.is_dead_css(&maybe)?);
323        assert!(!map.rename_is_safe(
324            &raw_alias,
325            &ordered_alias,
326            GuardedTokenObserverV0::RawString
327        ));
328        assert!(map.rename_is_safe(
329            &raw_alias,
330            &ordered_alias,
331            GuardedTokenObserverV0::OrderedWord
332        ));
333        assert!(map.rename_is_safe(
334            &raw_alias,
335            &ordered_alias,
336            GuardedTokenObserverV0::SupportSet
337        ));
338        Ok(())
339    }
340
341    #[test]
342    fn dead_css_changes_when_the_site_guard_becomes_satisfiable() -> Result<(), FirstWitnessErrorV0>
343    {
344        let token = GuardedTokenLanguageV0::concrete("conditional");
345        let build = |usage| {
346            GuardedTokenMapV0::build(GuardedTokenMapInputV0 {
347                tokens: vec![guarded("conditional", vec![atom("c", true)])],
348                site_usage_guards: usage,
349            })
350        };
351        let mut dead = build(vec![atom("c", false)])?;
352        let mut alive = build(Vec::new())?;
353        assert!(dead.is_dead_css(&token)?);
354        assert!(!alive.is_dead_css(&token)?);
355        Ok(())
356    }
357}