logicaffeine_kernel/dag/
name.rs

1//! Hierarchical names, interned: `Nat.succ` is `Str(Str(Anon, "Nat"), "succ")`, and each distinct
2//! name is one [`NameId`], so name equality is an integer compare.
3
4use logicaffeine_base::{Interner, Symbol};
5use rustc_hash::FxHashMap as FxMap;
6
7#[derive(Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord, Debug)]
8pub struct NameId(pub u32);
9
10impl NameId {
11    pub const ANON: NameId = NameId(0);
12}
13
14#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
15pub enum NameNode {
16    Anon,
17    Str(NameId, Symbol),
18    Num(NameId, u64),
19}
20
21#[derive(Clone)]
22pub struct Names {
23    nodes: Vec<NameNode>,
24    index: FxMap<NameNode, NameId>,
25    strings: Interner,
26}
27
28impl Default for Names {
29    fn default() -> Self {
30        Self::new()
31    }
32}
33
34impl Names {
35    pub fn new() -> Names {
36        let mut index = FxMap::default();
37        index.insert(NameNode::Anon, NameId::ANON);
38        Names {
39            nodes: vec![NameNode::Anon],
40            index,
41            strings: Interner::new(),
42        }
43    }
44
45    pub fn intern(&mut self, node: NameNode) -> NameId {
46        if let Some(&id) = self.index.get(&node) {
47            return id;
48        }
49        let id = NameId(self.nodes.len() as u32);
50        self.nodes.push(node);
51        self.index.insert(node, id);
52        id
53    }
54
55    pub fn str(&mut self, prefix: NameId, s: &str) -> NameId {
56        let sym = self.strings.intern(s);
57        self.intern(NameNode::Str(prefix, sym))
58    }
59
60    pub fn component(&self, sym: Symbol) -> &str {
61        self.strings.resolve(sym)
62    }
63
64    pub fn num(&mut self, prefix: NameId, n: u64) -> NameId {
65        self.intern(NameNode::Num(prefix, n))
66    }
67
68    /// Interns a dotted name such as `Nat.succ`. Only for well-known names written in source.
69    pub fn dotted(&mut self, s: &str) -> NameId {
70        s.split('.').fold(NameId::ANON, |p, part| self.str(p, part))
71    }
72
73    pub fn node(&self, id: NameId) -> &NameNode {
74        &self.nodes[id.0 as usize]
75    }
76
77    pub fn prefix(&self, id: NameId) -> NameId {
78        match self.node(id) {
79            NameNode::Anon => NameId::ANON,
80            NameNode::Str(p, _) | NameNode::Num(p, _) => *p,
81        }
82    }
83
84    /// `true` when `p` is a (non-strict) prefix of `n`.
85    pub fn is_prefix_of(&self, p: NameId, mut n: NameId) -> bool {
86        loop {
87            if n == p {
88                return true;
89            }
90            if n == NameId::ANON {
91                return false;
92            }
93            n = self.prefix(n);
94        }
95    }
96
97    /// Replaces prefix `old` of `n` by `new` (`n` unchanged when `old` is not a prefix).
98    pub fn replace_prefix(&mut self, n: NameId, old: NameId, new: NameId) -> NameId {
99        if n == old {
100            return new;
101        }
102        match *self.node(n) {
103            NameNode::Anon => n,
104            NameNode::Str(p, s) => {
105                let p2 = self.replace_prefix(p, old, new);
106                if p2 == p {
107                    n
108                } else {
109                    self.intern(NameNode::Str(p2, s))
110                }
111            }
112            NameNode::Num(p, k) => {
113                let p2 = self.replace_prefix(p, old, new);
114                if p2 == p {
115                    n
116                } else {
117                    self.intern(NameNode::Num(p2, k))
118                }
119            }
120        }
121    }
122
123    /// Lean's `Name.appendIndexAfter`: `u` ↦ `u_1`.
124    pub fn append_index_after(&mut self, n: NameId, i: u64) -> NameId {
125        match *self.node(n) {
126            NameNode::Str(p, s) => {
127                let text = format!("{}_{i}", self.component(s));
128                self.str(p, &text)
129            }
130            _ => self.str(n, &format!("_{i}")),
131        }
132    }
133
134    /// Lean's `Name.append`.
135    pub fn append(&mut self, a: NameId, b: NameId) -> NameId {
136        match *self.node(b) {
137            NameNode::Anon => a,
138            NameNode::Str(p, s) => {
139                let p2 = self.append(a, p);
140                self.intern(NameNode::Str(p2, s))
141            }
142            NameNode::Num(p, k) => {
143                let p2 = self.append(a, p);
144                self.intern(NameNode::Num(p2, k))
145            }
146        }
147    }
148
149    pub fn display(&self, id: NameId) -> String {
150        match self.node(id) {
151            NameNode::Anon => "[anonymous]".to_string(),
152            NameNode::Str(p, s) => {
153                let s = self.component(*s);
154                if *p == NameId::ANON {
155                    s.to_string()
156                } else {
157                    format!("{}.{}", self.display(*p), s)
158                }
159            }
160            NameNode::Num(p, k) => {
161                if *p == NameId::ANON {
162                    k.to_string()
163                } else {
164                    format!("{}.{}", self.display(*p), k)
165                }
166            }
167        }
168    }
169
170    pub fn len(&self) -> usize {
171        self.nodes.len()
172    }
173
174    pub fn is_empty(&self) -> bool {
175        self.nodes.len() <= 1
176    }
177}
178
179/// The kernel spelling of a Lean name given as its hierarchical components: the name the Lean
180/// importer gives a declaration in a kernel context, each component written after `/s:` as a JSON
181/// string, with the kernel's primitive identities applied (`Nat`, `Zero`, `Succ`, the quotient's
182/// four, and every other `Nat` member under `Nat/`).
183///
184/// Every component is a string component; a numeric Lean component cannot be told apart from a
185/// digit string by its dotted spelling, so callers holding an export resolve such names through
186/// the export's own name table (`interface::lean::reference::reference_declaration`).
187pub fn kernel_name_of_components(components: &[&str]) -> String {
188    let mut raw = String::new();
189    for component in components {
190        raw.push_str("/s:");
191        push_json_string(&mut raw, component);
192    }
193    primitive_identity(&raw)
194}
195
196/// `s` as a JSON string literal, byte for byte as `serde_json` writes it: `"` and `\` escaped,
197/// the control characters below U+0020 as `\b`, `\t`, `\n`, `\f`, `\r` or `\u00xx`, and every other
198/// character as itself.
199fn push_json_string(out: &mut String, s: &str) {
200    out.push('"');
201    for c in s.chars() {
202        match c {
203            '"' => out.push_str("\\\""),
204            '\\' => out.push_str("\\\\"),
205            '\u{08}' => out.push_str("\\b"),
206            '\t' => out.push_str("\\t"),
207            '\n' => out.push_str("\\n"),
208            '\u{0c}' => out.push_str("\\f"),
209            '\r' => out.push_str("\\r"),
210            c if (c as u32) < 0x20 => {
211                const HEX: &[u8; 16] = b"0123456789abcdef";
212                out.push_str("\\u00");
213                out.push(HEX[(c as usize) >> 4] as char);
214                out.push(HEX[(c as usize) & 0xf] as char);
215            }
216            c => out.push(c),
217        }
218    }
219    out.push('"');
220}
221
222/// The kernel's primitive identities, applied to a raw hierarchical spelling.
223fn primitive_identity(raw: &str) -> String {
224    const NAT: &str = "/s:\"Nat\"";
225    match raw {
226        "/s:\"Quot\"" => "kernel.quot.type".into(),
227        "/s:\"Quot\"/s:\"mk\"" => "kernel.quot.mk".into(),
228        "/s:\"Quot\"/s:\"lift\"" => "kernel.quot.lift".into(),
229        "/s:\"Quot\"/s:\"ind\"" => "kernel.quot.ind".into(),
230        NAT => "Nat".into(),
231        "/s:\"Nat\"/s:\"zero\"" => "Zero".into(),
232        "/s:\"Nat\"/s:\"succ\"" => "Succ".into(),
233        _ => match raw.strip_prefix("/s:\"Nat\"/") {
234            Some(rest) => format!("Nat/{rest}"),
235            None => raw.to_string(),
236        },
237    }
238}
239
240#[cfg(test)]
241#[path = "../../../logicaffeine_tests/unit/logicaffeine_kernel/dag/name/tests.rs"]
242mod tests;
logicaffeine_kernel/dag/name.rs

logicaffeine_kernel/dag/
name.rs
