logicaffeine_kernel/interface/lean/
emit_names.rs

1//! Names: the Lean name behind an importer key, and the deterministic, reversible allocation of a
2//! LOGOS name for every declaration a document writes.
3//!
4//! The importer keys a Lean constant structurally (`/s:"LE_Emit"/s:"Color"`), with four fixed
5//! identities (`Nat`, `Zero`, `Succ`, the kernel quotient primitives). A LOGOS name is a
6//! hierarchical name the term door can spell and whose flat key reads back as itself.
7//!
8//! Allocation walks the TRIE of Lean names, so a Lean namespace becomes exactly one LOGOS
9//! namespace: siblings get distinct components, so two Lean namespaces never merge, and a Lean
10//! root the LOGOS prelude already uses (`Eq`, `Nat`, …) moves whole — with everything inside it —
11//! under one fresh root (`Lean.Eq`, `Lean.Eq.mpr`), so no Lean name can collide with or merge
12//! into a prelude name. The mapping is recorded pair by pair in the correspondence, which is what
13//! makes it reversible.
14
15use super::terms::{is_plain_identifier, is_reserved_word};
16use std::collections::{BTreeMap, BTreeSet, HashSet};
17
18/// One component of a Lean name.
19#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
20pub enum LeanPart {
21    Str(String),
22    Num(u64),
23}
24
25/// The Lean name an importer key stands for, or `None` for a constant the importer made itself.
26pub(super) fn lean_name(key: &str) -> Option<Vec<LeanPart>> {
27    let s = |x: &str| LeanPart::Str(x.to_string());
28    match key {
29        "Nat" => return Some(vec![s("Nat")]),
30        "Zero" => return Some(vec![s("Nat"), s("zero")]),
31        "Succ" => return Some(vec![s("Nat"), s("succ")]),
32        _ => {}
33    }
34    for kind in [
35        crate::quotient::Kind::Type,
36        crate::quotient::Kind::Constructor,
37        crate::quotient::Kind::Lift,
38        crate::quotient::Kind::Induction,
39    ] {
40        if key == kind.name() {
41            let mut parts = vec![s("Quot")];
42            match kind {
43                crate::quotient::Kind::Type => {}
44                crate::quotient::Kind::Constructor => parts.push(s("mk")),
45                crate::quotient::Kind::Lift => parts.push(s("lift")),
46                crate::quotient::Kind::Induction => parts.push(s("ind")),
47            }
48            return Some(parts);
49        }
50    }
51    if let Some(rest) = key.strip_prefix("Nat/") {
52        let mut parts = vec![s("Nat")];
53        parts.extend(decode_structural(&format!("/{rest}"))?);
54        return Some(parts);
55    }
56    decode_structural(key)
57}
58
59/// `/s:"A"/n:3/s:"b"` → `[A, 3, b]`. `None` for anything else.
60fn decode_structural(key: &str) -> Option<Vec<LeanPart>> {
61    let mut parts = Vec::new();
62    let mut rest = key;
63    while !rest.is_empty() {
64        rest = rest.strip_prefix('/')?;
65        if let Some(after) = rest.strip_prefix("s:") {
66            let mut stream = serde_json::Deserializer::from_str(after).into_iter::<String>();
67            let text = stream.next()?.ok()?;
68            let used = stream.byte_offset();
69            parts.push(LeanPart::Str(text));
70            rest = &after[used..];
71        } else if let Some(after) = rest.strip_prefix("n:") {
72            let digits = after.len() - after.trim_start_matches(|c: char| c.is_ascii_digit()).len();
73            if digits == 0 {
74                return None;
75            }
76            parts.push(LeanPart::Num(after[..digits].parse().ok()?));
77            rest = &after[digits..];
78        } else {
79            return None;
80        }
81    }
82    (!parts.is_empty()).then_some(parts)
83}
84
85/// The Lean spelling of a name: components joined by `.`, a component Lean cannot read bare
86/// written `«…»`.
87pub(super) fn lean_display(parts: &[LeanPart]) -> String {
88    parts
89        .iter()
90        .map(|p| match p {
91            LeanPart::Num(n) => n.to_string(),
92            LeanPart::Str(s) if lean_bare(s) => s.clone(),
93            LeanPart::Str(s) => format!("\u{ab}{s}\u{bb}"),
94        })
95        .collect::<Vec<_>>()
96        .join(".")
97}
98
99fn lean_bare(s: &str) -> bool {
100    let mut chars = s.chars();
101    matches!(chars.next(), Some(c) if c.is_alphabetic() || c == '_')
102        && chars.all(|c| c.is_alphanumeric() || matches!(c, '_' | '\'' | '!' | '?'))
103}
104
105/// The LOGOS component a Lean component asks for, before sibling collisions are settled, and
106/// whether it had to be changed to be a LOGOS identifier at all.
107fn preferred_component(part: &LeanPart) -> (String, bool) {
108    match part {
109        LeanPart::Str(s) if is_plain_identifier(s) => (s.clone(), false),
110        LeanPart::Str(s) => {
111            let mut out: String = s
112                .chars()
113                .map(|c| {
114                    if c.is_alphanumeric() || c == '_' || c == '\'' {
115                        c
116                    } else {
117                        '_'
118                    }
119                })
120                .collect();
121            if !out
122                .chars()
123                .next()
124                .is_some_and(|c| c.is_alphabetic() || c == '_')
125            {
126                out.insert(0, '_');
127            }
128            if is_reserved_word(&out) || !is_plain_identifier(&out) {
129                out.push('_');
130            }
131            (out, true)
132        }
133        LeanPart::Num(n) => (format!("_{n}"), true),
134    }
135}
136
137/// The names the LOGOS prelude already declares, as the allocator needs them.
138pub(super) struct Taken {
139    /// Every first component of a prelude key.
140    pub roots: HashSet<String>,
141    /// Every full prelude key.
142    pub keys: HashSet<String>,
143}
144
145/// One allocation: a LOGOS key for every importer key given.
146#[derive(Debug)]
147pub(super) struct Allocation {
148    pub logos: BTreeMap<String, String>,
149    /// The root under which Lean roots the prelude already uses were placed, if any was needed.
150    pub relocated_under: Option<String>,
151}
152
153/// Allocate a LOGOS key for every Lean-named importer key in `keys`.
154///
155/// `fixed` are keys whose LOGOS name is decided already (a prelude identity: Lean `Nat` IS the
156/// prelude's `Nat`); `reserved` are full LOGOS keys the fresh context will derive on its own (an
157/// inductive's recursor family, a definition's equation lemmas) and so must stay free.
158pub(super) fn allocate(
159    keys: &BTreeSet<String>,
160    fixed: &BTreeMap<String, String>,
161    taken: &Taken,
162    reserved: &dyn Fn(&BTreeMap<String, String>) -> BTreeSet<String>,
163) -> Result<Allocation, String> {
164    let mut named: BTreeMap<Vec<LeanPart>, String> = BTreeMap::new();
165    for key in keys {
166        if fixed.contains_key(key) {
167            continue;
168        }
169        let parts = lean_name(key).ok_or_else(|| format!("`{key}` has no Lean name"))?;
170        if named.insert(parts.clone(), key.clone()).is_some() {
171            return Err(format!(
172                "two importer keys denote the Lean name `{}`",
173                lean_display(&parts)
174            ));
175        }
176    }
177
178    // A component the fresh context will derive beside an inductive or a definition is refused to
179    // the sibling that would take it, and allocation runs again until nothing new is refused.
180    let mut refused: BTreeMap<Vec<String>, BTreeSet<String>> = BTreeMap::new();
181    for _ in 0..=keys.len() {
182        let allocation = allocate_once(&named, fixed, taken, &refused)?;
183        let derived = reserved(&allocation.logos);
184        let mut changed = false;
185        for (key, logos) in &allocation.logos {
186            if fixed.contains_key(key) || !derived.contains(logos) {
187                continue;
188            }
189            let mut parts: Vec<String> = logos.split('.').map(str::to_string).collect();
190            let last = parts.pop().expect("a LOGOS key has a component");
191            changed |= refused.entry(parts).or_default().insert(last);
192        }
193        if !changed {
194            return Ok(allocation);
195        }
196    }
197    Err("LOGOS name allocation did not settle beside the names the context derives".to_string())
198}
199
200fn allocate_once(
201    named: &BTreeMap<Vec<LeanPart>, String>,
202    fixed: &BTreeMap<String, String>,
203    taken: &Taken,
204    refused: &BTreeMap<Vec<String>, BTreeSet<String>>,
205) -> Result<Allocation, String> {
206    // The trie of every Lean name, including the namespaces that only prefix others.
207    let mut nodes: BTreeSet<Vec<LeanPart>> = BTreeSet::new();
208    for parts in named.keys() {
209        for len in 1..=parts.len() {
210            nodes.insert(parts[..len].to_vec());
211        }
212    }
213    let lean_roots: BTreeSet<String> = nodes
214        .iter()
215        .filter(|n| n.len() == 1)
216        .map(|n| preferred_component(&n[0]).0)
217        .collect();
218    // A fixed identity is not a trie node (only the names it prefixes are), so a Lean root spelled like
219    // a prelude name is never that identity: Lean's class `Zero` is not the prelude's `Zero`, which is
220    // Lean's `Nat.zero`.
221    let collides_with_prelude =
222        |component: &str| taken.roots.contains(component) || taken.keys.contains(component);
223    let needs_relocation = |root: &LeanPart| {
224        let (c, _) = preferred_component(root);
225        collides_with_prelude(&c) || fixed_root_collides(root, named, fixed)
226    };
227    let relocated_under = if nodes
228        .iter()
229        .any(|n| n.len() == 1 && needs_relocation(&n[0]))
230    {
231        let base = "Lean";
232        let chosen = std::iter::successors(Some(base.to_string()), |s| Some(format!("{s}'")))
233            .find(|c| {
234                !taken.roots.contains(c) && !taken.keys.contains(c) && !lean_roots.contains(c)
235            })
236            .expect("an unbounded sequence of candidates has a free one");
237        Some(chosen)
238    } else {
239        None
240    };
241
242    // Children of each LOGOS prefix, settled in a fixed order: names that needed no change first
243    // (so a Lean `a_b` keeps its name when a Lean `«a b»` also wants it), then by Lean name.
244    let mut logos_of: BTreeMap<Vec<LeanPart>, Vec<String>> = BTreeMap::new();
245    let mut used: BTreeMap<Vec<String>, BTreeSet<String>> = BTreeMap::new();
246    let mut by_depth: Vec<&Vec<LeanPart>> = nodes.iter().collect();
247    by_depth.sort_by(|a, b| {
248        let (pa, sa) = preferred_component(a.last().unwrap());
249        let (pb, sb) = preferred_component(b.last().unwrap());
250        (a.len(), a[..a.len() - 1].to_vec(), sa, pa, *a).cmp(&(
251            b.len(),
252            b[..b.len() - 1].to_vec(),
253            sb,
254            pb,
255            *b,
256        ))
257    });
258    for node in by_depth {
259        let parent: Vec<String> = if node.len() == 1 {
260            match &relocated_under {
261                Some(root) if needs_relocation(&node[0]) => vec![root.clone()],
262                _ => Vec::new(),
263            }
264        } else {
265            logos_of[&node[..node.len() - 1].to_vec()].clone()
266        };
267        let (preferred, _) = preferred_component(node.last().unwrap());
268        let siblings = used.entry(parent.clone()).or_default();
269        let refused_here = refused.get(&parent);
270        let free = |c: &str| {
271            !siblings.contains(c)
272                && !refused_here.is_some_and(|r| r.contains(c))
273                && (!parent.is_empty()
274                    || (!collides_with_prelude(c) && !lean_root_is_relocation(c, &relocated_under)))
275        };
276        let component = std::iter::successors(Some(preferred.clone()), |s| Some(format!("{s}'")))
277            .find(|c| free(c))
278            .expect("an unbounded sequence of candidates has a free one");
279        siblings.insert(component.clone());
280        let mut path = parent;
281        path.push(component);
282        logos_of.insert(node.clone(), path);
283    }
284
285    let mut logos = BTreeMap::new();
286    for (key, name) in fixed {
287        logos.insert(key.clone(), name.clone());
288    }
289    for (parts, key) in named {
290        logos.insert(key.clone(), logos_of[parts].join("."));
291    }
292    Ok(Allocation {
293        logos,
294        relocated_under,
295    })
296}
297
298fn lean_root_is_relocation(component: &str, relocated_under: &Option<String>) -> bool {
299    relocated_under.as_deref() == Some(component)
300}
301
302/// A Lean root whose own name is fixed to a prelude identity (`Nat`) while other Lean names live
303/// under it (`Nat.add`): those others must not land inside the prelude's namespace.
304fn fixed_root_collides(
305    root: &LeanPart,
306    named: &BTreeMap<Vec<LeanPart>, String>,
307    fixed: &BTreeMap<String, String>,
308) -> bool {
309    let root_key_fixed = fixed
310        .keys()
311        .any(|k| lean_name(k).is_some_and(|p| p.len() == 1 && &p[0] == root));
312    root_key_fixed && named.keys().any(|p| p.len() > 1 && &p[0] == root)
313}
logicaffeine_kernel/interface/lean/emit_names.rs

logicaffeine_kernel/interface/lean/
emit_names.rs
