lean_rs/module/
loaded.rs

1//! Handle to a Lean module whose initializer has succeeded.
2//!
3//! [`LeanModule`] is the typed proof that
4//! [`crate::module::LeanLibrary::initialize_module`] ran the module's
5//! initializer to `IO.ok(())`. The only constructor is
6//! `pub(super) fn new`, invoked at the end of `initialize_module`;
7//! therefore a value of this type cannot exist unless the corresponding
8//! module is live in the Lean runtime.
9//!
10//! Typed exported-function handles attach to this type via
11//! [`LeanModule::exported`], which returns a
12//! [`crate::module::LeanExported`] parameterised by the argument tuple
13//! and return-type marker.
14
15use super::initializer::InitializerName;
16use super::library::LeanLibrary;
17
18/// A Lean module that has been linked and initialized successfully.
19///
20/// Holds a borrow of its source [`LeanLibrary`]; the `'lib` lifetime
21/// keeps the dylib loaded while any `LeanModule` referring to it is
22/// alive. The `'lean` lifetime is inherited from the library, which
23/// inherits it from the [`crate::LeanRuntime`] borrow that anchored the
24/// whole chain. Neither [`Send`] nor [`Sync`] (inherited from the
25/// `&LeanLibrary` field).
26pub struct LeanModule<'lean, 'lib> {
27    library: &'lib LeanLibrary<'lean>,
28    initializer: InitializerName,
29}
30
31impl<'lean, 'lib> LeanModule<'lean, 'lib> {
32    /// Build the typed handle.
33    ///
34    /// `pub(super)` so only `LeanLibrary::initialize_module` can produce
35    /// one — the construction site is the proof that initialization
36    /// succeeded.
37    pub(super) fn new(library: &'lib LeanLibrary<'lean>, initializer: InitializerName) -> Self {
38        Self { library, initializer }
39    }
40
41    /// Human-readable `package::Module.Path` form for diagnostics.
42    ///
43    /// The format matches what
44    /// [`crate::module::LeanLibrary::initialize_module`] accepted, so
45    /// log messages and test assertions can round-trip the name a
46    /// caller used.
47    #[must_use]
48    pub fn module_name(&self) -> &str {
49        self.initializer.display()
50    }
51
52    /// Borrowed reference to the owning library.
53    ///
54    /// `pub(crate)` so the typed [`crate::module::exported`] machinery
55    /// can resolve exported-function symbols against the same library
56    /// this module was initialized from.
57    pub(crate) fn library(&self) -> &'lib LeanLibrary<'lean> {
58        self.library
59    }
60
61    /// Initializer name in its mangled C form.
62    ///
63    /// `pub(crate)` so internal symbol-derivation code can reach the
64    /// canonical Lake mangling without re-running the validator.
65    #[allow(dead_code, reason = "reserved for symbol-derivation helpers in later prompts")]
66    pub(crate) fn initializer(&self) -> &InitializerName {
67        &self.initializer
68    }
69}
70
71impl std::fmt::Debug for LeanModule<'_, '_> {
72    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
73        f.debug_struct("LeanModule")
74            .field("module", &self.initializer.display())
75            .finish()
76    }
77}
lean_rs/module/loaded.rs

lean_rs/module/
loaded.rs
