Module resolver 

Modules

errors 🔒

refinement_resolver 🔒

Structs

Ambiguity 🔒

A name that two competing glob imports bind to different items:

Binding 🔒

The value stored for each binding in a Rib. Lookups and clash detection are keyed by the name in the Rib’s map, so all a binding carries is where it came from, for diagnostics that point at the previous location of a name.

CrateResolver 🔒

DefinitionMap 🔒

Map to keep track of names defined in a scope

ItemResolver 🔒

Module 🔒

Akin to rustc_resolve::Module but specialized to what we support

NameResolution 🔒

All candidates for a single name in a single namespace, split into the two slots (non_glob_decl/glob_decl). The non-glob slot always wins.

Rib 🔒

Enums

BindingSource 🔒

How a name was brought into a rib. Explicit definitions (items, generics, params, single uses, flux uses) shadow glob imports of the same name in the same namespace, regardless of declaration order; only globs can be ambiguous with each other.

GlobBinding 🔒

The glob-imported candidate(s) for a name, mirroring rustc’s glob_decl slot.

ModuleKind 🔒

Akin to rustc_resolve::ModuleKind but specialized to what we support

ResolveError 🔒

The reason a name lookup (resolve_ident_with_ribs, resolve_ident_in_module, resolve_path_with_ribs) failed.

RibKind 🔒

Traits

Segment 🔒

Abstraction over a “segment” so we can use CrateResolver::resolve_path_with_ribs with paths from different sources (e.g., surface::PathSegment, surface::ExprPathSegment)

Functions

builtin_types_rib 🔒

The Namespace::TypeNS prelude: builtin Rust types (bool, i32, str, …) together with the sort-only primitive sorts (int, real, Set, Map, ptr). Sorts and types share the type namespace; bool/char/str are resolved as fhir::Res::PrimTy and their sort is derived in conv_sort_path (see fhir::PrimSort).

is_prelude_import 🔒

Return true if the item has a #[prelude_import] annotation

mk_crate_mapping 🔒

module_children 🔒

resolve_crate 🔒

theory_funcs_rib 🔒

The Namespace::ReftNS prelude: theory functions and cast.

try_resolve_crate 🔒

visible_module_children 🔒

Iterator over module children visible form curr_mod

Type Aliases

Result 🔒