catlog/tt/
notebook_elab.rs

1//! Elaboration for frontend notebooks.
2//!
3//! The notebook elaborator is disjoint from the [text
4//! elaborator](super::text_elab). One reason for this is that error reporting
5//! must be completely different to be well adapted to the notebook interface.
6//! As a first pass, we are associating cell UUIDs with errors.
7
8use catcolab_document_types::current as nb;
9use nonempty::NonEmpty;
10use std::str::FromStr;
11use uuid::Uuid;
12
13use super::fiber_elab::{CODOMAIN_BINDER, FiberElab, FiberError};
14use super::{context::*, eval::*, prelude::*, stx::*, theory::*, toplevel::*, val::*};
15use crate::dbl::{
16    modal,
17    model::{Feature, InvalidDblModel, InvalidModelEqn},
18};
19use crate::zero::QualifiedName;
20
21/// The current state of a notebook elaboration session.
22///
23/// We feed a notebook into this cell-by-cell.
24pub struct Elaborator<'a> {
25    theory: Theory,
26    toplevel: &'a Toplevel,
27    ctx: Context,
28    errors: Vec<InvalidDblModel>,
29    ref_id: Ustr,
30    next_meta: usize,
31    /// The cell currently being elaborated, for error attribution.
32    current_cell: Option<QualifiedName>,
33}
34
35struct ElaboratorCheckpoint {
36    ctx: ContextCheckpoint,
37}
38
39impl<'a> Elaborator<'a> {
40    /// Create a new notebook elaborator.
41    pub fn new(theory: Theory, toplevel: &'a Toplevel, ref_id: Ustr) -> Self {
42        Self {
43            theory,
44            toplevel,
45            ctx: Context::new(),
46            errors: Vec::new(),
47            ref_id,
48            next_meta: 0,
49            current_cell: None,
50        }
51    }
52
53    fn theory(&self) -> &TheoryDef {
54        &self.theory.definition
55    }
56
57    /// Get all of the errors from elaboration.
58    pub fn errors(&self) -> &[InvalidDblModel] {
59        &self.errors
60    }
61
62    fn checkpoint(&self) -> ElaboratorCheckpoint {
63        ElaboratorCheckpoint { ctx: self.ctx.checkpoint() }
64    }
65
66    fn reset_to(&mut self, c: ElaboratorCheckpoint) {
67        self.ctx.reset_to(c.ctx);
68    }
69
70    fn evaluator(&self) -> Evaluator<'a> {
71        Evaluator::new(self.toplevel, self.ctx.env.clone(), self.ctx.scope.len())
72    }
73
74    fn intro(&mut self, name: VarName, label: LabelSegment, ty: Option<BaseTyV>) -> BaseTmV {
75        let v = BaseTmV::neu(
76            TmN::var(self.ctx.scope.len().into(), name, label),
77            ty.clone().unwrap_or(BaseTyV::empty_record()),
78        );
79        let v = if ty.is_some() {
80            self.evaluator().eta(&v, ty.as_ref())
81        } else {
82            v
83        };
84        self.ctx.env = self.ctx.env.snoc(v.clone());
85        self.ctx.scope.push(VarInContext::new(name, label, ty));
86        v
87    }
88
89    fn fresh_meta(&mut self) -> MetaVar {
90        let i = self.next_meta;
91        self.next_meta += 1;
92        MetaVar::new(Some(self.ref_id), i)
93    }
94
95    fn ty_error(&mut self, error: InvalidDblModel) -> (BaseTyS, BaseTyV) {
96        self.errors.push(error);
97        let ty_m = self.fresh_meta();
98        (BaseTyS::meta(ty_m), BaseTyV::meta(ty_m))
99    }
100
101    fn ob_type(&mut self, ob_type: &nb::ObType) -> Option<ObType> {
102        match &ob_type {
103            nb::ObType::Basic(name) => self.theory().basic_ob_type((*name).into()),
104            nb::ObType::Tabulator(_) => None,
105            nb::ObType::ModeApp { .. } => None,
106        }
107    }
108
109    fn object_cell(
110        &mut self,
111        ob_decl: &nb::ObDecl,
112    ) -> (NameSegment, LabelSegment, BaseTyS, BaseTyV) {
113        let name = NameSegment::Uuid(ob_decl.id);
114        let label = LabelSegment::Text(ustr(&ob_decl.name));
115        let (ty_s, ty_v) = match self.ob_type(&ob_decl.ob_type) {
116            Some(ob_type) => (BaseTyS::object(ob_type.clone()), BaseTyV::object(ob_type)),
117            None => self.ty_error(InvalidDblModel::ObType(QualifiedName::single(name))),
118        };
119        (name, label, ty_s, ty_v)
120    }
121
122    fn lookup_tm(&self, name: VarName) -> Option<(BaseTmS, BaseTmV, BaseTyV)> {
123        let (i, label, ty) = self.ctx.lookup(name)?;
124        let v = self.ctx.env.get(*i).unwrap().clone();
125        Some((BaseTmS::var(i, name, label), v, ty.clone().unwrap()))
126    }
127
128    fn resolve_name(&self, segments: &[VarName]) -> Option<(BaseTmS, BaseTmV, BaseTyV)> {
129        let (&last, rest) = segments.split_last()?;
130        if rest.is_empty() {
131            self.lookup_tm(last)
132        } else {
133            let (tm_s, tm_v, ty_v) = self.resolve_name(rest)?;
134            let BaseTyV_::Record(r) = &*ty_v else {
135                return None;
136            };
137            let &(label, _) = r.fields.get_with_label(last)?;
138            Some((
139                BaseTmS::proj(tm_s, last, label),
140                self.evaluator().proj(&tm_v, last, label),
141                self.evaluator().field_ty(&ty_v, &tm_v, last),
142            ))
143        }
144    }
145
146    fn ob_syn(&self, n: &nb::Ob) -> Option<(BaseTmS, BaseTmV, ObType)> {
147        match n {
148            nb::Ob::Basic(name) => {
149                let name = QualifiedName::deserialize_str(name).unwrap();
150                let (stx, val, ty) = self.resolve_name(name.as_slice())?;
151                let BaseTyV_::Object(ob_type) = &*ty else {
152                    return None;
153                };
154                Some((stx, val, ob_type.clone()))
155            }
156            nb::Ob::App { op: nb::ObOp::Basic(name), ob } => {
157                let name = name_seg(*name);
158                let ob_op = self.theory().basic_ob_op([name].into())?;
159                let arg_type = self.theory().ob_op_dom(&ob_op);
160                let (arg_stx, arg_val) = self.ob_chk(ob, &arg_type)?;
161                let stx = BaseTmS::ob_app(name, arg_stx);
162                let val = BaseTmV::app(name, arg_val);
163                Some((stx, val, self.theory().ob_op_cod(&ob_op)))
164            }
165            nb::Ob::Tabulated(mor) => {
166                let (mor_stx, mor_val, mor_ty) = self.mor_syn(mor)?;
167                let BaseTyV_::Morphism(mt, _, _) = &*mor_ty else {
168                    return None;
169                };
170                let ob_type = self.theory().tabulator(mt.clone())?;
171                Some((BaseTmS::tab(mor_stx), BaseTmV::tab(mor_val), ob_type))
172            }
173            _ => None,
174        }
175    }
176
177    fn mor_syn(&self, n: &nb::Mor) -> Option<(BaseTmS, BaseTmV, BaseTyV)> {
178        match n {
179            nb::Mor::Basic(name) => {
180                let name = QualifiedName::deserialize_str(name).unwrap();
181                let (stx, val, ty) = self.resolve_name(name.as_slice())?;
182                let BaseTyV_::Morphism(..) = &*ty else {
183                    return None;
184                };
185                Some((stx, val, ty))
186            }
187            nb::Mor::Composite(path) => match path.as_ref() {
188                nb::path::Path::Id(ob) => {
189                    let (stx, val, ob_type) = self.ob_syn(ob)?;
190                    let mor_type = self.theory().hom_type(ob_type)?;
191                    Some((stx, val.clone(), BaseTyV::morphism(mor_type, val.clone(), val.clone())))
192                }
193                nb::path::Path::Seq(ms) => match ms.as_slice() {
194                    [] => None,
195                    [only] => self.mor_syn(only),
196                    [first, rest @ ..] => {
197                        let (stx_first, val_first, type_first) = self.mor_syn(first)?;
198                        let rest = nb::Mor::Composite(Box::new(nb::path::Path::Seq(rest.to_vec())));
199                        let (stx_rest, val_rest, type_rest) = self.mor_syn(&rest)?;
200                        let BaseTyV_::Morphism(mt_first, dom_first, cod_first) = &*type_first
201                        else {
202                            unreachable!()
203                        };
204                        let BaseTyV_::Morphism(mt_rest, dom_rest, cod_rest) = &*type_rest else {
205                            unreachable!()
206                        };
207                        if mt_first != mt_rest {
208                            return None;
209                        }
210                        if self.evaluator().equal_tm(cod_first, dom_rest).is_err() {
211                            return None;
212                        }
213                        let stx = BaseTmS::compose(stx_first, stx_rest);
214                        let val = BaseTmV::compose(val_first, val_rest);
215                        Some((
216                            stx,
217                            val,
218                            BaseTyV::morphism(
219                                mt_first.clone(),
220                                dom_first.clone(),
221                                cod_rest.clone(),
222                            ),
223                        ))
224                    }
225                },
226            },
227            _ => None, // tabulator morphisms tbd
228        }
229    }
230
231    fn ob_chk(&self, n: &nb::Ob, ob_type: &ObType) -> Option<(BaseTmS, BaseTmV)> {
232        match n {
233            nb::Ob::List { modality: nb_modality, objects: elems } => {
234                let (modality, ob_type) = ob_type.clone().mode_app()?;
235                if promote_modality(*nb_modality) != modality {
236                    return None;
237                }
238                let mut elem_stxs = Vec::new();
239                let mut elem_vals = Vec::new();
240                for elem in elems {
241                    let (tm_s, tm_v) = self.ob_chk(elem.as_ref()?, &ob_type)?;
242                    elem_stxs.push(tm_s);
243                    elem_vals.push(tm_v);
244                }
245                Some((BaseTmS::list(elem_stxs), BaseTmV::list(elem_vals)))
246            }
247            _ => {
248                let (tm_s, tm_v, synthed) = self.ob_syn(n)?;
249                if synthed == *ob_type {
250                    Some((tm_s, tm_v))
251                } else {
252                    None
253                }
254            }
255        }
256    }
257
258    fn morphism_cell_ty(&mut self, mor_decl: &nb::MorDecl) -> (BaseTyS, BaseTyV) {
259        let id = QualifiedName::from(mor_decl.id);
260        let (mor_type, dom_ty, cod_ty) = match &mor_decl.mor_type {
261            nb::MorType::Basic(name) => {
262                if let Some(mor_type) = self.theory().basic_mor_type((*name).into()) {
263                    let dom_ty = self.theory().src_type(&mor_type);
264                    let cod_ty = self.theory().tgt_type(&mor_type);
265                    (mor_type, dom_ty, cod_ty)
266                } else {
267                    return self.ty_error(InvalidDblModel::MorType(id));
268                }
269            }
270            nb::MorType::Hom(ob_type) => match self.ob_type(ob_type.as_ref()) {
271                Some(ot) => match self.theory().hom_type(ot.clone()) {
272                    Some(mt) => (mt, ot.clone(), ot),
273                    None => return self.ty_error(InvalidDblModel::MorType(id)),
274                },
275                None => return self.ty_error(InvalidDblModel::MorType(id)),
276            },
277            _ => {
278                return self.ty_error(InvalidDblModel::UnsupportedFeature(Feature::ComplexMorType));
279            }
280        };
281        let Some((dom_s, dom_v)) = mor_decl.dom.as_ref().and_then(|ob| self.ob_chk(ob, &dom_ty))
282        else {
283            return self.ty_error(InvalidDblModel::DomType(id));
284        };
285        let Some((cod_s, cod_v)) = mor_decl.cod.as_ref().and_then(|ob| self.ob_chk(ob, &cod_ty))
286        else {
287            return self.ty_error(InvalidDblModel::CodType(id));
288        };
289        (
290            BaseTyS::morphism(mor_type.clone(), dom_s, cod_s),
291            BaseTyV::morphism(mor_type, dom_v, cod_v),
292        )
293    }
294
295    fn morphism_cell(
296        &mut self,
297        mor_decl: &nb::MorDecl,
298    ) -> (NameSegment, LabelSegment, BaseTyS, BaseTyV) {
299        let name = NameSegment::Uuid(mor_decl.id);
300        let label = LabelSegment::Text(ustr(&mor_decl.name));
301        let (ty_s, ty_v) = self.morphism_cell_ty(mor_decl);
302        (name, label, ty_s, ty_v)
303    }
304
305    fn equation_cell_ty(&mut self, eqn_decl: &nb::EqnDecl) -> (BaseTyS, BaseTyV) {
306        let (lhs_m, rhs_m) = match (&eqn_decl.lhs, &eqn_decl.rhs) {
307            (Some(lhs), Some(rhs)) => (lhs, rhs),
308            _ => {
309                return self
310                    .ty_error(InvalidDblModel::UnsupportedFeature(Feature::PartialEquation));
311            }
312        };
313        let mut errors = Vec::new();
314        let lhs = match self.mor_syn(lhs_m) {
315            Some(synthed) => Some(synthed),
316            None => {
317                errors.push(InvalidModelEqn::Lhs);
318                None
319            }
320        };
321        let rhs = match self.mor_syn(rhs_m) {
322            Some(synthed) => Some(synthed),
323            None => {
324                errors.push(InvalidModelEqn::Rhs);
325                None
326            }
327        };
328
329        if let (Some((_, _, lhs_ty)), Some((_, _, rhs_ty))) = (&lhs, &rhs) {
330            let BaseTyV_::Morphism(mt_lhs, dom_lhs, cod_lhs) = &**lhs_ty else {
331                unreachable!()
332            };
333            let BaseTyV_::Morphism(mt_rhs, dom_rhs, cod_rhs) = &**rhs_ty else {
334                unreachable!()
335            };
336            if mt_lhs != mt_rhs {
337                errors.push(InvalidModelEqn::MorType);
338            } else {
339                if self.evaluator().equal_tm(dom_lhs, dom_rhs).is_err() {
340                    errors.push(InvalidModelEqn::Src);
341                }
342                if self.evaluator().equal_tm(cod_lhs, cod_rhs).is_err() {
343                    errors.push(InvalidModelEqn::Tgt);
344                }
345            }
346        }
347        match (NonEmpty::from_vec(errors), lhs, rhs) {
348            (None, Some((lhs_s, lhs_v, lhs_ty)), Some((rhs_s, rhs_v, _))) => {
349                let ty_s = BaseTyS::id(self.evaluator().quote_ty(&lhs_ty), lhs_s, rhs_s);
350                let ty_v = BaseTyV::id(lhs_ty, lhs_v, rhs_v);
351                (ty_s, ty_v)
352            }
353            (Some(errors), _, _) => {
354                // FIXME: The assumption in InvalidDblModel that we should already have the vector of equations
355                // built up, so as to give the index in the first argument here, doesn't hold in this case.
356                // It would be best not to use InvalidDblModel here before we've begun
357                // to build a DblModel.
358                self.ty_error(InvalidDblModel::Eqn(None, errors))
359            }
360            _ => unreachable!(),
361        }
362    }
363
364    fn equation_cell(
365        &mut self,
366        eqn_decl: &nb::EqnDecl,
367    ) -> (NameSegment, LabelSegment, BaseTyS, BaseTyV) {
368        // Kind of funny that the decl's id produces the cell's name
369        // but the decl's name produces the cell's label.
370        let name = NameSegment::Uuid(eqn_decl.id);
371        let label = LabelSegment::Text(ustr(&eqn_decl.name));
372        let (ty_s, ty_v) = self.equation_cell_ty(eqn_decl);
373        (name, label, ty_s, ty_v)
374    }
375
376    fn instantiation_cell_ty(&mut self, i_decl: &nb::InstantiatedModel) -> (BaseTyS, BaseTyV) {
377        let name = QualifiedName::single(NameSegment::Uuid(i_decl.id));
378        let link = match &i_decl.model {
379            Some(l) => l,
380            None => return self.ty_error(InvalidDblModel::InvalidLink(name)),
381        };
382        let catcolab_document_types::current::LinkType::Instantiation = link.r#type else {
383            return self.ty_error(InvalidDblModel::InvalidLink(name));
384        };
385        let ref_id = ustr(&link.stable_ref.id);
386        let topname = NameSegment::Text(ref_id);
387        let Some(TopDecl::Type(type_def)) = self.toplevel.declarations.get(&topname) else {
388            return self.ty_error(InvalidDblModel::InvalidLink(name));
389        };
390        if type_def.theory != self.theory {
391            return self.ty_error(InvalidDblModel::InvalidLink(name));
392        }
393        let mut specializations = Vec::new();
394        let BaseTyV_::Record(r) = &*type_def.val else {
395            return self.ty_error(InvalidDblModel::InvalidLink(name));
396        };
397        let mut r = r.clone();
398        for specialization in i_decl.specializations.iter() {
399            if let (Some(field_id), Some(ob)) = (&specialization.id, &specialization.ob) {
400                let field_name = NameSegment::Uuid(Uuid::from_str(field_id).unwrap());
401                let Some((ob_s, ob_v, ob_type)) = self.ob_syn(ob) else {
402                    continue;
403                };
404                let Some((field_label, field_ty)) = r.fields.get_with_label(field_name) else {
405                    continue;
406                };
407                match &**field_ty {
408                    BaseTyS_::Object(expected_ob_ty) => {
409                        if &ob_type != expected_ob_ty {
410                            continue;
411                        }
412                    }
413                    _ => {
414                        continue;
415                    }
416                }
417                specializations.push((
418                    vec![(field_name, *field_label)],
419                    BaseTyS::sing(BaseTyS::object(ob_type.clone()), ob_s),
420                ));
421                r = r.add_specialization(
422                    &[(field_name, *field_label)],
423                    BaseTyV::sing(BaseTyV::object(ob_type), ob_v),
424                )
425            }
426        }
427        let ty_s = if specializations.is_empty() {
428            BaseTyS::topvar(topname)
429        } else {
430            BaseTyS::specialize(BaseTyS::topvar(topname), specializations)
431        };
432        (ty_s, BaseTyV::record(r))
433    }
434
435    fn instantiation_cell(
436        &mut self,
437        i_decl: &nb::InstantiatedModel,
438    ) -> (NameSegment, LabelSegment, BaseTyS, BaseTyV) {
439        let name = NameSegment::Uuid(i_decl.id);
440        let label = LabelSegment::Text(ustr(&i_decl.name));
441        let (ty_s, ty_v) = self.instantiation_cell_ty(i_decl);
442        (name, label, ty_s, ty_v)
443    }
444
445    /// Elaborate a notebook into a type.
446    pub fn notebook<'b>(
447        &mut self,
448        cells: impl Iterator<Item = &'b nb::ModelJudgment>,
449    ) -> (BaseTyS, BaseTyV) {
450        // Process the cells in dependency order. This is important because the
451        // UI allows users to reorder cells freely and that shouldn't affect the
452        // result of elaboration.
453        let mut cells: Vec<_> = cells.collect();
454        cells.sort_by_key(|judgment| match judgment {
455            nb::ModelJudgment::Object(_) => 0,
456            nb::ModelJudgment::Instantiation(_) => 1,
457            nb::ModelJudgment::Morphism(_) => 2,
458            nb::ModelJudgment::Equation(_) => 3,
459        });
460
461        let mut field_ty_vs = Vec::new();
462        let self_var = self.intro(name_seg("self"), label_seg("self"), None).unwrap_neu();
463        let c = self.checkpoint();
464
465        for cell in cells {
466            let (name, label, _, ty_v) = match &cell {
467                nb::ModelJudgment::Object(ob_decl) => self.object_cell(ob_decl),
468                nb::ModelJudgment::Morphism(mor_decl) => self.morphism_cell(mor_decl),
469                nb::ModelJudgment::Instantiation(i_decl) => self.instantiation_cell(i_decl),
470                nb::ModelJudgment::Equation(eqn_decl) => self.equation_cell(eqn_decl),
471            };
472            field_ty_vs.push((name, (label, ty_v.clone())));
473            self.ctx.scope.push(VarInContext::new(name, label, Some(ty_v.clone())));
474            self.ctx.env =
475                self.ctx.env.snoc(BaseTmV::neu(TmN::proj(self_var.clone(), name, label), ty_v));
476        }
477
478        self.reset_to(c);
479        let field_tys: Row<_> = field_ty_vs
480            .iter()
481            .map(|(name, (label, ty_v))| (*name, (*label, self.evaluator().quote_ty(ty_v))))
482            .collect();
483        let r_v = RecordV::new(self.ctx.env.clone(), field_tys.clone(), Dtry::empty());
484        (BaseTyS::record(field_tys), BaseTyV::record(r_v))
485    }
486}
487
488/// Instance-notebook elaboration: cells presenting an instance of a model,
489/// elaborated to a fiber record packaged as an [`Instance`] — the
490/// same target as the text elaborator's `instance NAME : X := [...]` path,
491/// whose `instance_body_inner` is the blueprint for everything here. The
492/// fiber helpers are deliberate near-duplicates of their text-side namesakes
493/// with typed errors; extracting a shared core is planned once the error
494/// channels unify.
495impl<'a> Elaborator<'a> {
496    /// Resolve a qualified name to a codomain morphism: the path (with
497    /// labels, for [`FiberTmS::over_app`]) and the morphism's type. The
498    /// codomain's fields are in the base scope (see
499    /// [`Self::instance_notebook`]), so the first segment is a context
500    /// variable and later segments project through records (a morphism of a
501    /// model instantiated into the codomain).
502    fn resolve_codomain_mor(
503        &self,
504        name: &QualifiedName,
505    ) -> Option<(Vec<(FieldName, LabelSegment)>, BaseTyV)> {
506        let (&first, rest) = name.as_slice().split_first()?;
507        let (i, label, ty) = self.ctx.lookup(first)?;
508        let mut tm_v = self.ctx.env.get(*i).unwrap().clone();
509        let mut ty_v = ty?;
510        let mut path = vec![(first, label)];
511        for &seg in rest {
512            let BaseTyV_::Record(r) = &*ty_v else {
513                return None;
514            };
515            let (seg_label, _) = r.fields.get_with_label(seg)?;
516            path.push((seg, *seg_label));
517            let next_ty = self.evaluator().field_ty(&ty_v, &tm_v, seg);
518            tm_v = self.evaluator().proj(&tm_v, seg, *seg_label);
519            ty_v = next_ty;
520        }
521        Some((path, ty_v))
522    }
523
524    /// Resolve a qualified fiber reference: a generator, or a projection
525    /// path through imports (`hydro.n`). The fiber-scope analogue of
526    /// [`Self::resolve_name`].
527    fn resolve_fiber(&self, segments: &[VarName]) -> Option<(FiberTmS, FiberTmV, FiberTyV)> {
528        let (&first, rest) = segments.split_first()?;
529        let (mut tm_s, mut tm_v, mut ty_v) = self.lookup_fiber_tm(first)?;
530        for &seg in rest {
531            let FiberTyV_::Record(r) = &*ty_v else {
532                return None;
533            };
534            let (label, field_ty) = r.get_with_label(seg)?;
535            tm_s = FiberTmS::proj(tm_s, seg, *label);
536            tm_v = FiberTmV::proj(tm_v, seg, *label);
537            ty_v = field_ty.clone();
538        }
539        Some((tm_s, tm_v, ty_v))
540    }
541
542    /// Apply a codomain morphism to an already-elaborated fiber argument:
543    /// resolve the morphism against the codomain fields in scope, then
544    /// delegate the checks and construction to the shared
545    /// [`FiberElab::fiber_mor_app`].
546    fn apply_codomain_morphism(
547        &mut self,
548        mor_name: &QualifiedName,
549        arg_s: FiberTmS,
550        arg_v: FiberTmV,
551        arg_ty: FiberTyV,
552    ) -> (FiberTmS, FiberTmV, FiberTyV) {
553        let Some((path, mor_ty)) = self.resolve_codomain_mor(mor_name) else {
554            return self.fiber_syn_error(FiberError::UnknownElement(mor_name.to_string()));
555        };
556        let FiberTyV_::Over(arg_obj) = &*arg_ty else {
557            return self.fiber_syn_error(FiberError::ArgNotElement(None));
558        };
559        let arg_obj = arg_obj.clone();
560        self.fiber_mor_app(&path, &mor_ty, arg_s, arg_v, &arg_obj)
561    }
562
563    /// Synthesize a fiber term from a notebook instance term. Mirrors the
564    /// text elaborator's `fiber_syn`, dispatching on [`nb::InstanceTm`]
565    /// instead of surface notation; errors are attributed to the cell in
566    /// [`Self::current_cell`].
567    fn fiber_syn_nb(&mut self, tm: &nb::InstanceTm) -> (FiberTmS, FiberTmV, FiberTyV) {
568        match tm {
569            nb::InstanceTm::Generator(name) => {
570                let Ok(qname) = QualifiedName::deserialize_str(name) else {
571                    return self.fiber_syn_error(FiberError::UnknownElement(name.clone()));
572                };
573                match self.resolve_fiber(qname.as_slice()) {
574                    Some(r) => r,
575                    None => self.fiber_syn_error(FiberError::UnknownElement(name.clone())),
576                }
577            }
578            nb::InstanceTm::App { mor, arg } => {
579                let nb::Mor::Basic(mor_name) = mor else {
580                    self.errors
581                        .push(InvalidDblModel::UnsupportedFeature(Feature::CompositeApplication));
582                    return self.fiber_syn_hole();
583                };
584                let Ok(mor_qname) = QualifiedName::deserialize_str(mor_name) else {
585                    return self.fiber_syn_error(FiberError::UnknownElement(mor_name.clone()));
586                };
587                let (arg_s, arg_v, arg_ty) = self.fiber_syn_nb(arg);
588                self.apply_codomain_morphism(&mor_qname, arg_s, arg_v, arg_ty)
589            }
590            nb::InstanceTm::List { terms, .. } => {
591                let mut ss = Vec::with_capacity(terms.len());
592                let mut vs = Vec::with_capacity(terms.len());
593                let mut objs = Vec::with_capacity(terms.len());
594                for term in terms {
595                    let Some(term) = term else {
596                        return self.fiber_syn_error(FiberError::MissingTerm);
597                    };
598                    let (s, v, ty) = self.fiber_syn_nb(term);
599                    let FiberTyV_::Over(o) = &*ty else {
600                        return self.fiber_syn_error(FiberError::ListElementNotOver);
601                    };
602                    objs.push(o.clone());
603                    ss.push(s);
604                    vs.push(v);
605                }
606                (FiberTmS::list(ss), FiberTmV::list(vs), FiberTyV::over(BaseTmV::list(objs)))
607            }
608            nb::InstanceTm::ObApp { op, tm } => {
609                let nb::ObOp::Basic(op_name) = op;
610                let op_seg = name_seg(*op_name);
611                if !self.check_ob_op(op_seg) {
612                    return self.fiber_syn_hole();
613                }
614                let (arg_s, arg_v, arg_ty) = self.fiber_syn_nb(tm);
615                self.fiber_ob_app(op_seg, arg_s, arg_v, &arg_ty)
616            }
617        }
618    }
619
620    /// Check a notebook instance term against an expected fiber type. Fiber
621    /// terms are all synthesizing, so this synthesizes and checks
622    /// convertibility.
623    fn fiber_chk_nb(&mut self, expected: &FiberTyV, tm: &nb::InstanceTm) -> (FiberTmS, FiberTmV) {
624        let syn = self.fiber_syn_nb(tm);
625        self.check_fiber(syn, expected)
626    }
627
628    /// Elaborate the cells of an instance notebook against the codomain
629    /// model, producing the instance as a fiber record — the notebook
630    /// analogue of the text elaborator's `instance_body`.
631    ///
632    /// The codomain is bound under `CODOMAIN_BINDER` and each of its
633    /// fields is pushed into the base scope as a variable projecting out of
634    /// that binding, so cell references to codomain objects and morphisms
635    /// (UUID-qualified names) resolve through the ordinary
636    /// `Self::resolve_name` machinery — including modal objects in `over`
637    /// and paths through model instantiations. Generators and imports go to
638    /// the separate fiber scope, exactly as in the text pipeline. Unlike the
639    /// text pipeline, a bad cell does not abort the instance: the error is
640    /// recorded against the cell and elaboration continues.
641    pub fn instance_notebook<'b>(
642        &mut self,
643        codomain: &RecordV,
644        cells: impl Iterator<Item = &'b nb::InstanceJudgment>,
645    ) -> (FiberTyS, FiberTyV) {
646        let toplevel = self.toplevel;
647        // Like model notebooks, cells are elaborated in dependency order so
648        // that UI reordering cannot change the result.
649        let mut cells: Vec<_> = cells.collect();
650        cells.sort_by_key(|judgment| match judgment {
651            nb::InstanceJudgment::Generator(_) => 0,
652            nb::InstanceJudgment::Import(_) => 1,
653            nb::InstanceJudgment::Equation(_) => 2,
654        });
655
656        let c = self.checkpoint();
657        let codomain_ty = BaseTyV::record(codomain.clone());
658        let self_v = self.intro(
659            name_seg(CODOMAIN_BINDER),
660            label_seg(CODOMAIN_BINDER),
661            Some(codomain_ty.clone()),
662        );
663        for (name, (label, _)) in codomain.fields.iter() {
664            let field_ty = self.evaluator().field_ty(&codomain_ty, &self_v, *name);
665            let field_v = self.evaluator().proj(&self_v, *name, *label);
666            self.ctx.push_scope(*name, *label, Some(field_ty));
667            self.ctx.env = self.ctx.env.snoc(field_v);
668        }
669
670        let mut fields_s: Row<FiberTyS> = Row::empty();
671        let mut fields_v: Row<FiberTyV> = Row::empty();
672
673        for cell in cells {
674            match cell {
675                // A generator lying over a codomain object.
676                nb::InstanceJudgment::Generator(gen_decl) => {
677                    let name = NameSegment::Uuid(gen_decl.id);
678                    let label = LabelSegment::Text(ustr(&gen_decl.name));
679                    self.current_cell = Some(QualifiedName::single(name));
680                    let over = gen_decl.over.as_ref().and_then(|ob| self.ob_syn(ob));
681                    let (ty_s, ty_v) = match over {
682                        Some((obj_s, obj_v, _)) => (FiberTyS::over(obj_s), FiberTyV::over(obj_v)),
683                        None => {
684                            self.errors.push(InvalidDblModel::ObType(QualifiedName::single(name)));
685                            let m = self.fresh_meta();
686                            (FiberTyS::over(BaseTmS::meta(m)), FiberTyV::over(BaseTmV::meta(m)))
687                        }
688                    };
689                    self.intro_fiber(name, label, ty_v.clone());
690                    fields_s.insert(name, label, ty_s);
691                    fields_v.insert(name, label, ty_v);
692                }
693                // An import of another instance of the same codomain.
694                nb::InstanceJudgment::Import(import) => {
695                    let name = NameSegment::Uuid(import.id);
696                    let label = LabelSegment::Text(ustr(&import.name));
697                    let qname = QualifiedName::single(name);
698                    self.current_cell = Some(qname.clone());
699                    let resolved = import.instance.as_ref().and_then(|link| {
700                        let nb::LinkType::Instantiation = link.r#type else {
701                            return None;
702                        };
703                        let topname = NameSegment::Text(ustr(&link.stable_ref.id));
704                        match toplevel.declarations.get(&topname) {
705                            Some(TopDecl::Instance(inst)) if inst.theory == self.theory => {
706                                Some((topname, inst))
707                            }
708                            _ => None,
709                        }
710                    });
711                    let Some((topname, inst)) = resolved else {
712                        self.errors.push(InvalidDblModel::InvalidLink(qname));
713                        continue;
714                    };
715                    if !self.codomains_match(&codomain_ty, &inst.codomain) {
716                        self.errors.push(InvalidDblModel::ImportCodomain(qname));
717                        continue;
718                    }
719                    let val = inst.val.clone();
720                    self.intro_fiber(name, label, val.clone());
721                    fields_s.insert(name, label, FiberTyS::topvar(topname));
722                    fields_v.insert(name, label, val);
723                }
724                // An equation between fiber elements.
725                nb::InstanceJudgment::Equation(eqn_decl) => {
726                    let name = NameSegment::Uuid(eqn_decl.id);
727                    let label = LabelSegment::Text(ustr(&eqn_decl.name));
728                    self.current_cell = Some(QualifiedName::single(name));
729                    let (Some(lhs), Some(rhs)) = (&eqn_decl.lhs, &eqn_decl.rhs) else {
730                        self.errors
731                            .push(InvalidDblModel::UnsupportedFeature(Feature::PartialEquation));
732                        continue;
733                    };
734                    let (lhs_s, lhs_v, lhs_ty) = self.fiber_syn_nb(lhs);
735                    let FiberTyV_::Over(obj) = &*lhs_ty else {
736                        // Only fiber-element equations live in an instance;
737                        // morphism equations constrain the model.
738                        self.report_fiber(FiberError::EquationNotOver);
739                        continue;
740                    };
741                    let obj = obj.clone();
742                    let (rhs_s, rhs_v) = self.fiber_chk_nb(&lhs_ty, rhs);
743                    let (id_s, id_v) =
744                        self.fiber_id_field(&lhs_ty, &obj, lhs_s, lhs_v, rhs_s, rhs_v);
745                    fields_s.insert(name, label, id_s);
746                    fields_v.insert(name, label, id_v);
747                }
748            }
749        }
750        self.reset_to(c);
751        (FiberTyS::record(fields_s), FiberTyV::record(fields_v))
752    }
753
754    /// Elaborate an instance document into a top-level instance declaration.
755    ///
756    /// Resolves the document's `instanceOf` link to a model previously
757    /// declared in the toplevel (mirroring how instantiation cells resolve
758    /// their links), elaborates the cells against it, and packages the
759    /// result exactly as the text pipeline does — ready for
760    /// [`instance_from_def`](super::modelgen::instance_from_def).
761    ///
762    /// Returns `None` (with an error recorded) if the codomain link cannot
763    /// be resolved at all; cell-level problems are recorded per-cell in
764    /// [`Self::errors`] and still produce an instance.
765    pub fn instance_document(&mut self, doc: &nb::InstanceDocumentContent) -> Option<Instance> {
766        let toplevel = self.toplevel;
767        let link = &doc.instance_of;
768        let link_name = QualifiedName::single(NameSegment::Text(ustr(&link.stable_ref.id)));
769        let nb::LinkType::InstanceOf = link.r#type else {
770            self.errors.push(InvalidDblModel::InvalidLink(link_name));
771            return None;
772        };
773        let topname = NameSegment::Text(ustr(&link.stable_ref.id));
774        let Some(TopDecl::Type(type_def)) = toplevel.declarations.get(&topname) else {
775            self.errors.push(InvalidDblModel::InvalidLink(link_name));
776            return None;
777        };
778        if type_def.theory != self.theory {
779            self.errors.push(InvalidDblModel::InvalidLink(link_name));
780            return None;
781        }
782        let BaseTyV_::Record(codomain) = &*type_def.val else {
783            self.errors.push(InvalidDblModel::InvalidLink(link_name));
784            return None;
785        };
786        let codomain = codomain.clone();
787        let codomain_ty = type_def.val.clone();
788        let (stx, val) = self.instance_notebook(&codomain, doc.notebook.formal_content());
789        Some(Instance::new(self.theory.clone(), stx, val, codomain_ty))
790    }
791}
792
793impl<'a> FiberElab for Elaborator<'a> {
794    fn ctx(&self) -> &Context {
795        &self.ctx
796    }
797
798    fn ctx_mut(&mut self) -> &mut Context {
799        &mut self.ctx
800    }
801
802    fn elab_theory(&self) -> &Theory {
803        &self.theory
804    }
805
806    fn evaluator(&self) -> Evaluator<'_> {
807        Elaborator::evaluator(self)
808    }
809
810    fn fresh_meta(&mut self) -> MetaVar {
811        Elaborator::fresh_meta(self)
812    }
813
814    /// Attribute fiber errors to the cell currently being elaborated, as
815    /// typed [`InvalidDblModel`] values for the notebook interface.
816    fn report_fiber(&mut self, err: FiberError) {
817        let cell = self
818            .current_cell
819            .clone()
820            .unwrap_or_else(|| QualifiedName::single(name_seg("unknown cell")));
821        let error = match err {
822            FiberError::UnknownElement(_)
823            | FiberError::ProjNonRecord
824            | FiberError::UnknownProj(_)
825            | FiberError::MissingTerm => InvalidDblModel::FiberElement(cell),
826            FiberError::ImportCodomainMismatch(_) => InvalidDblModel::ImportCodomain(cell),
827            _ => InvalidDblModel::FiberType(cell),
828        };
829        self.errors.push(error);
830    }
831}
832
833/// Promotes a modality from notebook type to modality for modal theory.
834pub fn promote_modality(modality: nb::Modality) -> modal::Modality {
835    match modality {
836        nb::Modality::Discrete => modal::Modality::Discrete(),
837        nb::Modality::Codiscrete => modal::Modality::Codiscrete(),
838        nb::Modality::List => modal::Modality::List(modal::List::Plain),
839        nb::Modality::SymmetricList => modal::Modality::List(modal::List::Symmetric),
840        nb::Modality::CartesianList => modal::Modality::List(modal::List::Cartesian),
841        nb::Modality::CocartesianList => modal::Modality::List(modal::List::Cocartesian),
842        nb::Modality::AdditiveList => modal::Modality::List(modal::List::Additive),
843    }
844}
845
846/// Demotes a modality to notebook type.
847pub fn demote_modality(modality: modal::Modality) -> nb::Modality {
848    match modality {
849        modal::Modality::Discrete() => nb::Modality::Discrete,
850        modal::Modality::Codiscrete() => nb::Modality::Codiscrete,
851        modal::Modality::List(list_type) => match list_type {
852            modal::List::Plain => nb::Modality::List,
853            modal::List::Symmetric => nb::Modality::SymmetricList,
854            modal::List::Cartesian => nb::Modality::CartesianList,
855            modal::List::Cocartesian => nb::Modality::CocartesianList,
856            modal::List::Additive => nb::Modality::AdditiveList,
857        },
858    }
859}
860
861#[cfg(test)]
862mod test {
863    use expect_test::{Expect, expect};
864    use serde_json;
865    use std::{fmt::Write, fs};
866    use ustr::ustr;
867
868    use crate::dbl::model::DblModelPrinter;
869    use crate::stdlib::{th_schema, th_sym_monoidal_category, th_sym_multicategory};
870    use crate::tt::{
871        batch::{format_modal_instance_term, format_modal_ob, write_instance_summary},
872        modelgen::{Model, ModelInstance, instance_from_def},
873        notebook_elab::Elaborator,
874        prelude::*,
875        theory::{Theory, TheoryDef},
876        toplevel::{Instance, TopDecl, Toplevel, Type},
877    };
878    use crate::zero::name;
879    use catcolab_document_types::current::{InstanceDocumentContent, ModelDocumentContent};
880
881    fn elab_example(theory: &Theory, name: &str, expected: Expect) -> Model {
882        let src = fs::read_to_string(format!("examples/tt/notebook/{name}.json")).unwrap();
883        let doc: ModelDocumentContent = serde_json::from_str(&src).unwrap();
884        let toplevel = Toplevel::new(Default::default());
885        let mut elab = Elaborator::new(theory.clone(), &toplevel, ustr(""));
886        let (_, ty_v) = elab.notebook(doc.notebook.formal_content());
887        let (model, ns) = Model::from_ty(&toplevel, &theory.definition, &ty_v);
888        let mut out = model.to_doc(&DblModelPrinter::new(), &ns).pretty().to_string();
889        for error in elab.errors() {
890            writeln!(&mut out, "error {:?}", error).unwrap()
891        }
892        expected.assert_eq(&out);
893        model
894    }
895
896    #[test]
897    fn discrete_theories() {
898        let th_schema = Theory::new(name("ThSchema"), TheoryDef::discrete(th_schema()));
899        elab_example(
900            &th_schema,
901            "sch_weighted_graph",
902            expect![[r#"
903                model generated by 3 objects and 3 morphisms
904                E : Entity
905                V : Entity
906                Weight : AttrType
907                weight : E -> Weight : Attr
908                src : E -> V : Hom Entity
909                tgt : E -> V : Hom Entity"#]],
910        );
911    }
912
913    #[test]
914    fn modal_theories() {
915        let th_smc =
916            Theory::new(name("ThSMC"), TheoryDef::modal_unital(th_sym_monoidal_category()));
917        elab_example(
918            &th_smc,
919            "sir_petri",
920            expect![[r#"
921                model generated by 3 objects and 2 morphisms
922                S : Object
923                I : Object
924                R : Object
925                infect : ⨂ [S, I] -> ⨂ [I, I] : Hom Object
926                recover : ⨂ [I] -> ⨂ [R] : Hom Object"#]],
927        );
928    }
929
930    /// Test that morphisms can reference objects that appear later in the notebook.
931    #[test]
932    fn morphism_before_codomain() {
933        let th_schema = Theory::new(name("ThSchema"), TheoryDef::discrete(th_schema()));
934        // In this example, the cell order is: A (object), f (morphism A->B), B (object)
935        elab_example(
936            &th_schema,
937            "morphism_before_codomain",
938            expect![[r#"
939                model generated by 2 objects and 1 morphism
940                A : Entity
941                B : Entity
942                f : A -> B : Hom Entity"#]],
943        );
944    }
945
946    /// Every notebook fixture under `examples/tt/notebook` deserializes
947    /// against the document schema for its declared `type`. Elaboration
948    /// coverage is per-file opt-in (each fixture needs a theory and, for
949    /// instances, a populated toplevel), but this sweep catches schema
950    /// drift and orphaned fixtures that no named test reads.
951    #[test]
952    fn notebook_fixtures_deserialize() {
953        fn walk(dir: &std::path::Path, checked: &mut usize) {
954            for entry in fs::read_dir(dir).unwrap().flatten() {
955                let path = entry.path();
956                if path.is_dir() {
957                    walk(&path, checked);
958                    continue;
959                }
960                if path.extension().is_none_or(|e| e != "json") {
961                    continue;
962                }
963                let src = fs::read_to_string(&path).unwrap();
964                let value: serde_json::Value = serde_json::from_str(&src).unwrap();
965                let display = path.display();
966                match value.get("type").and_then(|t| t.as_str()) {
967                    Some("model") => {
968                        serde_json::from_str::<ModelDocumentContent>(&src)
969                            .unwrap_or_else(|e| panic!("{display}: {e}"));
970                    }
971                    Some("instance") => {
972                        serde_json::from_str::<InstanceDocumentContent>(&src)
973                            .unwrap_or_else(|e| panic!("{display}: {e}"));
974                    }
975                    other => panic!("{display}: unexpected document type {other:?}"),
976                }
977                *checked += 1;
978            }
979        }
980        let mut checked = 0;
981        walk(std::path::Path::new("examples/tt/notebook"), &mut checked);
982        assert!(checked >= 8, "expected at least 8 fixtures, found {checked}");
983    }
984
985    /// Elaborate a model document and install it in the toplevel under the
986    /// given ref id, so instance documents can link to it.
987    fn install_model(toplevel: &mut Toplevel, theory: &Theory, ref_id: &str, src: &str) {
988        let doc: ModelDocumentContent = serde_json::from_str(src).unwrap();
989        let (ty_s, ty_v) = {
990            let mut elab = Elaborator::new(theory.clone(), toplevel, ustr(ref_id));
991            let r = elab.notebook(doc.notebook.formal_content());
992            assert!(elab.errors().is_empty(), "{ref_id}: {:?}", elab.errors());
993            r
994        };
995        toplevel.declarations.insert(
996            NameSegment::Text(ustr(ref_id)),
997            TopDecl::Type(Type::new(theory.clone(), ty_s, ty_v)),
998        );
999    }
1000
1001    /// Elaborate an instance document, asserting no errors.
1002    fn elab_instance(toplevel: &Toplevel, theory: &Theory, ref_id: &str, src: &str) -> Instance {
1003        let doc: InstanceDocumentContent = serde_json::from_str(src).unwrap();
1004        let mut elab = Elaborator::new(theory.clone(), toplevel, ustr(ref_id));
1005        let inst = elab.instance_document(&doc).expect("codomain should resolve");
1006        assert!(elab.errors().is_empty(), "{ref_id}: {:?}", elab.errors());
1007        inst
1008    }
1009
1010    /// The Klausmeier fixtures: DEC model + hydro/phyto instances installed
1011    /// in a toplevel, ready for tests to elaborate against.
1012    fn klausmeier_setup() -> (Theory, Toplevel) {
1013        let th =
1014            Theory::new(name("ThMulticategory"), TheoryDef::modal_unital(th_sym_multicategory()));
1015        let mut toplevel = Toplevel::new(Default::default());
1016        let src = fs::read_to_string("examples/tt/notebook/klausmeier/dec_model.json").unwrap();
1017        install_model(&mut toplevel, &th, "dec_model", &src);
1018        for ref_id in ["hydrodynamics", "phytodynamics"] {
1019            let src = fs::read_to_string(format!("examples/tt/notebook/klausmeier/{ref_id}.json"))
1020                .unwrap();
1021            let inst = elab_instance(&toplevel, &th, ref_id, &src);
1022            toplevel
1023                .declarations
1024                .insert(NameSegment::Text(ustr(ref_id)), TopDecl::Instance(inst));
1025        }
1026        (th, toplevel)
1027    }
1028
1029    /// Render an elaborated instance through `instance_from_def` in the
1030    /// batch snapshot format.
1031    fn instance_summary(toplevel: &Toplevel, theory: &Theory, inst: &Instance) -> String {
1032        let (instance, ns) = instance_from_def(toplevel, &theory.definition, inst).unwrap();
1033        let ModelInstance::ModalUnital(instance) = &instance else {
1034            panic!("expected a modal instance");
1035        };
1036        let mut out = String::new();
1037        write_instance_summary(
1038            &mut out,
1039            instance,
1040            &ns,
1041            |ob| format_modal_ob(ob, &ns),
1042            |tm| format_modal_instance_term(tm, &ns),
1043        );
1044        out
1045    }
1046
1047    /// End-to-end: the Klausmeier instance notebooks elaborate to
1048    /// `DblModelInstance`s through the same pipeline as the text examples
1049    /// (compare `examples/tt/text/test_klausmeier.dbltt.snapshot`).
1050    #[test]
1051    fn klausmeier_instance_notebooks() {
1052        let (th, toplevel) = klausmeier_setup();
1053
1054        let Some(TopDecl::Instance(hydro)) =
1055            toplevel.declarations.get(&NameSegment::Text(ustr("hydrodynamics")))
1056        else {
1057            unreachable!()
1058        };
1059        expect![[r#"
1060            #/ instance generators:
1061            #/   a : Form0
1062            #/   k : Form0
1063            #/   dX : Form1
1064            #/   w : DualForm0
1065            #/   n : DualForm0
1066            #/   x0 : DualForm0
1067            #/   x1 : DualForm0
1068            #/   x2 : DualForm0
1069            #/   x3 : DualForm0
1070            #/   x4 : DualForm0
1071            #/   x5 : DualForm0
1072            #/ instance equations:
1073            #/   x0 == sub_d01([w, a])
1074            #/   x1 == square_d0([n])
1075            #/   x2 == mult_d0d0([w, x1])
1076            #/   x3 == sub_d0d0([x0, x2])
1077            #/   x4 == lie_1d0([dX, w])
1078            #/   x5 == mult_0d0([k, x4])
1079            #/   partial_d0([w]) == add_d0d0([x3, x5])
1080        "#]]
1081        .assert_eq(&instance_summary(&toplevel, &th, hydro));
1082
1083        let src = fs::read_to_string("examples/tt/notebook/klausmeier/klausmeier.json").unwrap();
1084        let klausmeier = elab_instance(&toplevel, &th, "klausmeier", &src);
1085        expect![[r#"
1086            #/ instance generators:
1087            #/   hydro.a : Form0
1088            #/   hydro.k : Form0
1089            #/   hydro.dX : Form1
1090            #/   hydro.w : DualForm0
1091            #/   hydro.n : DualForm0
1092            #/   hydro.x0 : DualForm0
1093            #/   hydro.x1 : DualForm0
1094            #/   hydro.x2 : DualForm0
1095            #/   hydro.x3 : DualForm0
1096            #/   hydro.x4 : DualForm0
1097            #/   hydro.x5 : DualForm0
1098            #/   phyto.m : Form0
1099            #/   phyto.n : DualForm0
1100            #/   phyto.w : DualForm0
1101            #/   phyto.y0 : DualForm0
1102            #/   phyto.y1 : DualForm0
1103            #/   phyto.y2 : DualForm0
1104            #/   phyto.y3 : DualForm0
1105            #/   phyto.y4 : DualForm0
1106            #/ instance equations:
1107            #/   hydro.x0 == sub_d01([hydro.w, hydro.a])
1108            #/   hydro.x1 == square_d0([hydro.n])
1109            #/   hydro.x2 == mult_d0d0([hydro.w, hydro.x1])
1110            #/   hydro.x3 == sub_d0d0([hydro.x0, hydro.x2])
1111            #/   hydro.x4 == lie_1d0([hydro.dX, hydro.w])
1112            #/   hydro.x5 == mult_0d0([hydro.k, hydro.x4])
1113            #/   partial_d0([hydro.w]) == add_d0d0([hydro.x3, hydro.x5])
1114            #/   phyto.y0 == square_d0([phyto.n])
1115            #/   phyto.y1 == mult_d0d0([phyto.w, phyto.y0])
1116            #/   phyto.y2 == mult_0d0([phyto.m, phyto.n])
1117            #/   phyto.y3 == sub_d0d0([phyto.y1, phyto.y2])
1118            #/   phyto.y4 == lapl_d0([phyto.n])
1119            #/   partial_d0([phyto.w]) == add_d0d0([phyto.y3, phyto.y4])
1120            #/   hydro.n == phyto.n
1121            #/   hydro.w == phyto.w
1122        "#]]
1123        .assert_eq(&instance_summary(&toplevel, &th, &klausmeier));
1124    }
1125
1126    /// Importing an instance of a different model into an instance notebook
1127    /// is an error (notebook twin of the text suite's MismatchedImport).
1128    #[test]
1129    fn instance_import_codomain_mismatch() {
1130        use crate::dbl::model::InvalidDblModel;
1131        let (th, mut toplevel) = klausmeier_setup();
1132        let other_model = r##"{"type":"model","name":"Other","theory":"multicategory","version":"2",
1133            "notebook":{"cellContents":{"11111111-1111-1111-1111-111111111111":{
1134                "tag":"formal","id":"11111111-1111-1111-1111-111111111111",
1135                "content":{"tag":"object","name":"X","id":"22222222-2222-2222-2222-222222222222",
1136                    "obType":{"tag":"Basic","content":"Object"}}}},
1137                "cellOrder":["11111111-1111-1111-1111-111111111111"]}}"##;
1138        install_model(&mut toplevel, &th, "other_model", other_model);
1139        let bad_import = r##"{"type":"instance","name":"Bad","version":"2",
1140            "instanceOf":{"_id":"other_model","_version":null,"_server":"catcolab.org","type":"instance-of"},
1141            "notebook":{"cellContents":{"33333333-3333-3333-3333-333333333333":{
1142                "tag":"formal","id":"33333333-3333-3333-3333-333333333333",
1143                "content":{"tag":"import","name":"h","id":"44444444-4444-4444-4444-444444444444",
1144                    "instance":{"_id":"hydrodynamics","_version":null,"_server":"catcolab.org","type":"instantiation"}}}},
1145                "cellOrder":["33333333-3333-3333-3333-333333333333"]}}"##;
1146        let doc: InstanceDocumentContent = serde_json::from_str(bad_import).unwrap();
1147        let mut elab = Elaborator::new(th.clone(), &toplevel, ustr("bad_import"));
1148        let inst = elab.instance_document(&doc);
1149        assert!(inst.is_some());
1150        assert!(
1151            elab.errors().iter().any(|e| matches!(e, InvalidDblModel::ImportCodomain(_))),
1152            "expected an ImportCodomain error, got {:?}",
1153            elab.errors()
1154        );
1155    }
1156
1157    /// Test a notebook with an equation.
1158    #[test]
1159    fn commutative_square() {
1160        let th_schema = Theory::new(name("ThSchema"), TheoryDef::discrete(th_schema()));
1161        let model = elab_example(
1162            &th_schema,
1163            "commutative_square",
1164            expect![[r#"
1165                model generated by 4 objects and 4 morphisms
1166                NW : Entity
1167                NE : Entity
1168                SW : Entity
1169                SE : Entity
1170                t : NW -> NE : Hom Entity
1171                l : NW -> SW : Hom Entity
1172                r : NE -> SE : Hom Entity
1173                b : SW -> SE : Hom Entity
1174                t ⋅ r = l ⋅ b : (Hom Entity)[NW, SE]"#]],
1175        );
1176        let model = model.as_discrete().unwrap();
1177        let eqns: Vec<_> = model.category.equations().collect();
1178        assert_eq!(eqns.len(), 1);
1179    }
1180}
catlog/tt/notebook_elab.rs

catlog/tt/
notebook_elab.rs
