slotted_egraphs/
slot.rs

1use crate::*;
2use std::cell::RefCell;
3use std::fmt::*;
4
5#[derive(Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)]
6/// Slots represent Variable names.
7///
8/// Internally, they are just a number.
9pub struct Slot(u32);
10
11// %4 = 0 -> numeric
12// %4 = 1 -> fresh
13// %4 = 2 -> named
14// %4 = 3 -> <unused>
15struct SlotTable {
16    fresh_idx: u32,
17    named_vec: Vec<String>,
18    named_map: HashMap<String, u32>,
19}
20
21thread_local! {
22    static SLOT_TABLE: RefCell<SlotTable> = RefCell::new(SlotTable {
23        fresh_idx: 1,
24        named_vec: Vec::default(),
25        named_map: HashMap::default(),
26    });
27}
28
29impl Slot {
30    /// Generates a fresh slot.
31    ///
32    /// Any slot returned from this function has never been constructed before.
33    pub fn fresh() -> Self {
34        SLOT_TABLE.with_borrow_mut(|tab| {
35            let old_val = tab.fresh_idx;
36            tab.fresh_idx += 4;
37            Slot(old_val)
38        })
39    }
40
41    /// Generates a numeric slot like `$42`
42    pub fn numeric(u: u32) -> Slot {
43        Slot(u * 4)
44    }
45
46    /// Generates a named slot like `$xyz`
47    pub fn named(s: &str) -> Slot {
48        if let Ok(x) = s.parse::<u32>() {
49            return Slot(x * 4); // numeric
50        }
51
52        SLOT_TABLE.with_borrow_mut(|tab| {
53            if s.starts_with("f") {
54                if let Ok(x) = s[1..].parse::<u32>() {
55                    let out = x * 4 + 1;
56                    if tab.fresh_idx <= out {
57                        tab.fresh_idx = out + 4;
58                    }
59                    return Slot(out); // fresh
60                }
61            }
62
63            if let Some(x) = tab.named_map.get(s) {
64                return Slot(*x); // cached named
65            }
66
67            let i = tab.named_vec.len() as u32;
68            let i = 4 * i + 2;
69            tab.named_vec.push(s.to_string());
70            tab.named_map.insert(s.to_string(), i);
71            Slot(i) // new named
72        })
73    }
74}
75
76impl Display for Slot {
77    fn fmt(&self, f: &mut Formatter<'_>) -> Result {
78        let u = self.0;
79        match u % 4 {
80            // numeric:
81            0 => write!(f, "${}", u / 4),
82
83            // fresh:
84            1 => write!(f, "$f{}", (u - 1) / 4),
85
86            // named:
87            2 => {
88                let idx = ((u - 2) / 4) as usize;
89                SLOT_TABLE.with_borrow(|tab| write!(f, "${}", tab.named_vec[idx]))
90            }
91
92            // unused:
93            3 => unreachable!(),
94
95            _ => unreachable!(),
96        }
97    }
98}
99
100impl Debug for Slot {
101    // debug falls back to display.
102    fn fmt(&self, f: &mut Formatter<'_>) -> Result {
103        write!(f, "{}", self)
104    }
105}
slotted_egraphs/slot.rs

slotted_egraphs/
slot.rs
