lean-rs-host 0.3.1

//! `LeanHost`—entry point for the host-side capability API.
//!
//! A [`LeanHost`] binds a [`lean_rs::LeanRuntime`] borrow to a Lake project
//! on disk. From it, [`LeanHost::load_capabilities`] opens a compiled user
//! capability dylib for its module initializers and imports, while
//! [`LeanHost::load_shims_only`] opens only the bundled host shims for the
//! standard session services. Both paths return a [`LeanCapabilities`] whose
//! sessions resolve checked host-shim bindings once and dispatch subsequent
//! calls without per-call `dlsym`.
//!
//! See `docs/architecture/03-host-stack.md` for the full classification
//! and the host → capabilities → session lifetime cascade.

use core::fmt;
use std::path::Path;

use lean_rs::LeanRuntime;
use lean_rs::error::LeanResult;
use lean_rs::module::LeanLibrary;

use crate::host::capabilities::LeanCapabilities;
use crate::host::lake::LakeProject;

/// Entry point for hosting Lean capabilities from a Lake project.
///
/// Pairs a runtime borrow with a validated Lake project root. Cheap to
/// construct: only the project root's existence is checked; no dylib
/// loading happens until [`LeanHost::load_capabilities`] is called.
///
/// Neither [`Send`] nor [`Sync`]: inherited from the contained
/// `&'lean LeanRuntime`.
pub struct LeanHost<'lean> {
    runtime: &'lean LeanRuntime,
    project: LakeProject,
}

impl fmt::Debug for LeanHost<'_> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        f.debug_struct("LeanHost").finish_non_exhaustive()
    }
}

impl<'lean> LeanHost<'lean> {
    /// Bind a host to the runtime and a Lake project root directory.
    ///
    /// # Errors
    ///
    /// Returns [`lean_rs::LeanError::Host`] with stage
    /// [`lean_rs::HostStage::Load`] if `path` does not exist or is not a
    /// directory.
    pub fn from_lake_project(runtime: &'lean LeanRuntime, path: impl AsRef<Path>) -> LeanResult<Self> {
        let project = LakeProject::new(path)?;
        Ok(Self { runtime, project })
    }

    /// Load the compiled capability dylib for the named
    /// `(package, lib_name)` pair, initialize its root module, and
    /// prepare the checked host-shim capability used by sessions.
    ///
    /// `package` is the Lake package name (e.g. `"lean_rs_fixture"`);
    /// `lib_name` is the Lake `lean_lib` declaration name and, by
    /// convention, also the root Lean module path
    /// (e.g. `"LeanRsFixture"`). For projects where these differ the
    /// `lib_name` argument is also the module that gets initialised.
    ///
    /// # Errors
    ///
    /// Returns [`lean_rs::LeanError::Host`] with stage
    /// [`lean_rs::HostStage::Load`] if the dylib does not exist or fails
    /// to open. Missing or signature-mismatched mandatory host shims fail when
    /// constructing a session; optional host shims degrade to `Unsupported` at
    /// the corresponding call site.
    pub fn load_capabilities<'h>(&'h self, package: &str, lib_name: &str) -> LeanResult<LeanCapabilities<'lean, 'h>> {
        let dylib_path = self.project.capability_dylib(package, lib_name);
        let library = LeanLibrary::open(self.runtime, &dylib_path)?;
        LeanCapabilities::new(self, library, package, lib_name)
    }

    /// Load the bundled host-shim and interop dylibs without opening a user
    /// capability dylib.
    ///
    /// Sessions opened from the returned capabilities can import modules from
    /// this Lake project's `.olean` search path and use the standard
    /// shim-backed Meta, elaboration, kernel, info-tree, declaration, and
    /// source-range services.
    ///
    /// # Errors
    ///
    /// Returns [`lean_rs::LeanError::Host`] with stage
    /// [`lean_rs::HostStage::Load`] / [`lean_rs::LeanDiagnosticCode::ModuleInit`]
    /// if the bundled shim or interop dylibs cannot be built or located.
    /// Returns [`lean_rs::HostStage::Link`] if any mandatory shim symbol is
    /// missing.
    pub fn load_shims_only<'h>(&'h self) -> LeanResult<LeanCapabilities<'lean, 'h>> {
        LeanCapabilities::new_shims_only(self)
    }

    /// The runtime borrow this host was constructed with.
    pub(crate) fn runtime(&self) -> &'lean LeanRuntime {
        self.runtime
    }

    /// The Lake project root, for capability code that needs to pass
    /// the path through to Lean (e.g., setting `Lean.searchPathRef`).
    pub(crate) fn project(&self) -> &LakeProject {
        &self.project
    }
}