pub fn respell_names<'t>(
ns: &Namespaces,
env: &Env<'_>,
locals: &mut Vec<String>,
term: &'t Term,
) -> Result<Cow<'t, Term>, ParseError>Expand description
The inverse of resolve_names_in, for a term already in KEY space: every global is re-spelled
so that resolving the result in this same scope reaches exactly the key it holds now.
A key its own spelling still reaches is kept. A key its spelling no longer reaches — a
declaration a shadow hides, or one an enclosing namespace or an open captures — is written
with the _root_ escape, which reaches it and only it. An identity no surface can spell is
kept as it is: resolution leaves it alone too.
A door that must know what a name MEANS while it reads (the literate surface compiles equation
sets and reflects statements at parse time) resolves as it reads and hands its output to the
REPL, which resolves again. Re-spelling the output is what makes that second pass the identity
rather than a second, different reading of _root_.add.