Struct Elaborator 

pub struct Elaborator<'a> { /* private fields */ }

The current state of a notebook elaboration session.

We feed a notebook into this cell-by-cell.

Implementations

impl<'a> Elaborator<'a>

pub fn new(theory: Theory, toplevel: &'a Toplevel, ref_id: Ustr) -> Self

Create a new notebook elaborator.

pub fn errors(&self) -> &[InvalidDblModel]

Get all of the errors from elaboration.

pub fn notebook<'b>( &mut self, cells: impl Iterator<Item = &'b ModelJudgment>, ) -> (BaseTyS, BaseTyV)

Elaborate a notebook into a type.

impl<'a> Elaborator<'a>

Instance-notebook elaboration: cells presenting an instance of a model, elaborated to a fiber record packaged as an Instance — the same target as the text elaborator’s instance NAME : X := [...] path, whose instance_body_inner is the blueprint for everything here. The fiber helpers are deliberate near-duplicates of their text-side namesakes with typed errors; extracting a shared core is planned once the error channels unify.

pub fn instance_notebook<'b>( &mut self, codomain: &RecordV, cells: impl Iterator<Item = &'b InstanceJudgment>, ) -> (FiberTyS, FiberTyV)

Elaborate the cells of an instance notebook against the codomain model, producing the instance as a fiber record — the notebook analogue of the text elaborator’s instance_body.

The codomain is bound under CODOMAIN_BINDER and each of its fields is pushed into the base scope as a variable projecting out of that binding, so cell references to codomain objects and morphisms (UUID-qualified names) resolve through the ordinary Self::resolve_name machinery — including modal objects in over and paths through model instantiations. Generators and imports go to the separate fiber scope, exactly as in the text pipeline. Unlike the text pipeline, a bad cell does not abort the instance: the error is recorded against the cell and elaboration continues.

pub fn instance_document( &mut self, doc: &InstanceDocumentContent, ) -> Option<Instance>

Elaborate an instance document into a top-level instance declaration.

Resolves the document’s instanceOf link to a model previously declared in the toplevel (mirroring how instantiation cells resolve their links), elaborates the cells against it, and packages the result exactly as the text pipeline does — ready for instance_from_def.

Returns None (with an error recorded) if the codomain link cannot be resolved at all; cell-level problems are recorded per-cell in Self::errors and still produce an instance.