Struct Namespaces 

pub struct Namespaces { /* private fields */ }

The namespace scope: what is CURRENT, and what is OPEN.

Empty is the state every existing session is in, and in that state Namespaces::resolve is the identity on every name that resolves and on every name that does not — the resolver costs one map lookup and changes nothing. That is deliberate: a subsystem that is free when unused is one nobody has to opt out of.

Implementations

impl Namespaces

pub fn new() -> Namespaces

A scope with nothing open and nothing current.

pub fn is_trivial(&self) -> bool

Is the scope empty? In that state resolve is provably the identity — every name that resolves resolves to itself and every name that does not keeps its spelling — which is what makes this subsystem free for every session that never writes Namespace, Open or Export. All three must be absent for the claim to hold, which is why all three are checked.

Protected is deliberately NOT a fourth: it can only refuse a candidate reached through lookup_qualified, which is the enclosing-namespace walk and a wholesale open — both of which require a non-empty scope to exist at all. The root reading goes through lookup and consults it not at all, exactly as Lean’s line 177 does not (ResolveName.lean:177), so the identity claim survives a Protected written at the root.

pub fn current(&self) -> &[String]

The components of the current namespace, outermost first.

pub fn opens(&self) -> &[OpenClause]

The openings in force, earliest first, each with its namespace already resolved.

pub fn depth(&self) -> usize

How many Namespace \u{2026} frames are entered.

pub fn frame_names(&self) -> Vec<String>

The entered namespaces, outermost first \u{2014} what a document must close before it ends.

pub fn mark(&self) -> ScopeMark

Where the scope stands now.

pub fn rewind(&mut self, mark: ScopeMark)

Wind the scope back to mark. Used for Open … in <command>, which scopes its opens to exactly one command, and for a declaration whose own name names a namespace.

pub fn enter_declaration( &mut self, declared: &Name, section_depth: usize, ) -> (String, ScopeMark)

Enter the scope a DECLARATION elaborates in, and give back the absolute key it declares.

def Foo.Bar.baz elaborates with Foo.Bar current — a declaration name that NAMES a namespace opens it for its own body, which is where a short sibling name is found. That is Lean’s rule and it is the whole of T02-011’s third assertion. _root_.baz declares the top-level name and elaborates at the root, which is what the escape is for.

pub fn enter(&mut self, name: &Name, section_depth: usize)

Namespace Foo.Bar. — push one frame. Foo.Bar is ONE frame of two components, so End Foo.Bar. closes it and End Bar. does not.

pub fn record_declaration(&mut self, key: &str)

Note that the absolute key key has been declared, so every namespace its prefixes name now EXISTS and can be opened. Called on SUCCESS only — a refused declaration creates nothing.

pub fn record_protected(&mut self, key: &str)

Mark the absolute key key as protected: it stops answering to its SHORT name, here and under any open, and keeps answering to its full one. Called on SUCCESS only, like record_declaration — a refused declaration protects nothing.

pub fn resolve_namespace(&self, written: &Name) -> Option<Name>

Which namespace written names, read relative to the current one: the longest enclosing prefix that exists, else the bare name if that exists. None if no such namespace has ever been declared — which is what makes Open Typo. an error rather than a silent no-op.

pub fn leave(&mut self, name: &Name) -> bool

End Foo.Bar. — pop the innermost frame if it is the one named, restoring the open state it was entered with. false if the innermost open scope is not that namespace, which is how the same End keyword serves both namespaces and sections without either guessing.

pub fn innermost_scope(&self, section_depth: usize) -> Option<&Name>

The namespace that is the INNERMOST open scope, if a namespace is — i.e. if no section has been opened since it was entered. End consults this so one keyword can serve both stacks without either of them guessing.

pub fn open(&mut self, name: Name) -> Result<(), ParseError>

Open Foo. — bring a namespace’s short names into scope, reading Foo relative to the current namespace. A namespace nothing has ever declared into is REFUSED, as Lean refuses it: an open that brings in nothing looks exactly like an open that worked, and every short name under it then quietly means the root’s constant instead.

pub fn open_clause( &mut self, clause: OpenClause, known: &dyn Fn(&str) -> bool, ) -> Result<(), ParseError>

open for a clause that NARROWS the opening — Open Alpha (a b). and Open Alpha hiding (a).

known is the environment predicate, and it is needed here for the reason export needs one: a clause that names something the namespace does not declare narrows the opening to nothing and is indistinguishable from one that worked. The wholesale form names nothing, so open can still be called without an environment.

pub fn declaration_key(&self, declared: &Name) -> String

The absolute key a DECLARATION written here gets: the current namespace, then the name as written. _root_.x declares the absolute x.

pub fn export( &mut self, namespace: &Name, names: &[Name], known: &dyn Fn(&str) -> bool, ) -> Result<(), ParseError>

Export Alpha (token other). — make each Alpha.<name> answer to <name> in the CURRENT namespace, PERMANENTLY — an alias is an environment fact, not scope state, so unlike an open it survives the End of the namespace it was written in. That is Lean’s own staging (addAlias is a persistent env extension, OpenDecl is elaborator Scope state) and it is what export is for: publishing a name from inside the namespace that is to answer to it.

Every failure mode is LOUD, because a silent one is an alias nobody can see: an unknown source namespace, a name that namespace does not declare, and a name the current namespace already declares (which would leave two readings of one key and no way to say which was meant).

pub fn resolve( &self, written: &Name, known: &dyn Fn(&str) -> bool, ) -> Resolution

Resolve a written name to the absolute key it denotes, in Lean’s order.

1. _root_.x is absolute and consults nothing.
2. The enclosing namespace, LONGEST prefix first. An inner namespace SHADOWS an outer one — Lean’s resolveUsingNamespace returns at the first prefix that resolves, so this is a shadow and never an ambiguity.
3. Every open namespace AND the root, at ONE priority. Lean combines them (resolveOpenDecls seeded from the root lookup), so a short name that answers to two different constants is AMBIGUOUS. This is the case the audit called the dangerous one: with 50 prelude names already in the root, a short name written under an open used to resolve to the PRELUDE’s constant and report nothing. It is now reported.

known is the environment predicate — “is this absolute key declared?”. Passing it in rather than a Context is what keeps the kernel out of the surface.

Trait Implementations

impl Clone for Namespaces

fn clone(&self) -> Namespaces

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Namespaces

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Default for Namespaces

fn default() -> Namespaces

Returns the “default value” for a type.