catlog/tt/
notebook_elab.rs

1//! Elaboration for frontend notebooks.
2use notebook_types::v1::{ModelJudgment, MorDecl, Ob, ObDecl, ObType};
3use uuid::Uuid;
4
5use crate::dbl::{
6    VDblCategory,
7    theory::{DblTheory, DiscreteDblTheory},
8};
9use std::str::FromStr;
10
11use crate::{
12    tt::{context::*, eval::*, prelude::*, stx::*, toplevel::*, val::*},
13    zero::QualifiedName,
14};
15
16// There is some infrastructure that needs to be put into place before
17// notebook elaboration can be fully successful.
18//
19// First of all, we need an error reporting strategy adapted for the
20// notebook interface.
21//
22// As a first pass, we will associate the cell uuid with errors. I think
23// that it makes sense to have an entirely separate file for notebook
24// elaboration, mainly because the error reporting is going to be so
25// different.
26//
27// Another reason for a separate file is that we can handle the caching
28// there. Ideally, actually, the existing `Toplevel` struct should work
29// just fine.
30//
31// It is also desirable to extract a "partial model" from a notebook.
32// I think that this is possible if we simply ignore any cells that have
33// errors, including cells that depend on cells that have errors.
34
35/// An elaboration error
36#[derive(Debug)]
37pub enum Error {
38    /// The theory does not contain this object type
39    NoSuchObjectType(QualifiedName),
40    /// There is no such variable in scope
41    NoSuchVariable(VarName),
42    /// Tried to elaborate a notebook that uses tabulator features
43    TabulatorUnsupported,
44    /// Tried to elaborate a notebook that uses modal features
45    ModalUnsupported,
46    /// Tried to elaborate a notebook that uses a non-discrete double theory
47    NonDiscreteUnsupported,
48    /// Expected a variable to refer to an object
49    ExpectedObject,
50    /// The variable in the domain slot of an arrow doesn't have the right object type
51    MismatchedDomTypes {
52        /// The expected object type
53        expected: ObjectType,
54        /// The object type of the variable given
55        synthesized: ObjectType,
56    },
57    /// The variable in the codomain slot of an arrow doesn't have the right object type
58    MismatchedCodTypes {
59        /// The expected object type
60        expected: ObjectType,
61        /// The object type of the variable given
62        synthesized: ObjectType,
63    },
64}
65
66/// An error along with its location (a cell in a notebook)
67pub struct LocatedError {
68    /// The location of the error.
69    pub cell: Option<Uuid>,
70    /// The content of the error.
71    pub content: Error,
72}
73
74/// The current state of a notebook elaboration session.
75///
76/// We feed a notebook into this cell-by-cell.
77pub struct Elaborator<'a> {
78    theory: Theory,
79    toplevel: &'a Toplevel,
80    current_cell: Option<Uuid>,
81    ctx: Context,
82    errors: Vec<LocatedError>,
83}
84
85struct ElaboratorCheckpoint {
86    ctx: ContextCheckpoint,
87}
88
89impl<'a> Elaborator<'a> {
90    /// Create a new notebook elaborator
91    pub fn new(theory: Theory, toplevel: &'a Toplevel) -> Self {
92        Self {
93            theory,
94            toplevel,
95            current_cell: None,
96            ctx: Context::new(),
97            errors: Vec::new(),
98        }
99    }
100
101    fn dbl_theory(&self) -> &DiscreteDblTheory {
102        &self.theory.definition
103    }
104
105    /// Get all of the errors from elaboration
106    pub fn errors(&self) -> &[LocatedError] {
107        &self.errors
108    }
109
110    fn checkpoint(&self) -> ElaboratorCheckpoint {
111        ElaboratorCheckpoint {
112            ctx: self.ctx.checkpoint(),
113        }
114    }
115
116    fn reset_to(&mut self, c: ElaboratorCheckpoint) {
117        self.ctx.reset_to(c.ctx);
118    }
119
120    fn evaluator(&self) -> Evaluator<'a> {
121        Evaluator::new(self.toplevel, self.ctx.env.clone(), self.ctx.scope.len())
122    }
123
124    fn intro(&mut self, name: VarName, label: LabelSegment, ty: Option<TyV>) -> TmV {
125        let v = TmV::Neu(
126            TmN::var(self.ctx.scope.len().into(), name, label),
127            ty.clone().unwrap_or(TyV::unit()),
128        );
129        let v = if let Some(ty) = &ty {
130            self.evaluator().eta(&v, ty)
131        } else {
132            v
133        };
134        self.ctx.env = self.ctx.env.snoc(v.clone());
135        self.ctx.scope.push(VarInContext::new(name, label, ty));
136        v
137    }
138
139    fn error<T>(&mut self, error: Error) -> Option<T> {
140        self.errors.push(LocatedError {
141            cell: self.current_cell,
142            content: error,
143        });
144        None
145    }
146
147    fn ob_type(&mut self, ob_type: &ObType) -> Option<QualifiedName> {
148        match &ob_type {
149            ObType::Basic(name) => Some(QualifiedName::single(name_seg(*name))),
150            ObType::Tabulator(_) => self.error(Error::TabulatorUnsupported),
151            ObType::ModeApp { .. } => self.error(Error::ModalUnsupported),
152        }
153    }
154
155    fn object_cell(&mut self, ob_decl: &ObDecl) -> Option<(NameSegment, LabelSegment, TyS, TyV)> {
156        let ob_type = self.ob_type(&ob_decl.ob_type)?;
157        if !self.dbl_theory().has_ob(&ob_type) {
158            return self.error(Error::NoSuchObjectType(ob_type.clone()));
159        }
160        let name = NameSegment::Uuid(ob_decl.id);
161        let label = LabelSegment::Text(ustr(&ob_decl.name));
162        Some((name, label, TyS::object(ob_type.clone()), TyV::object(ob_type)))
163    }
164
165    fn lookup_tm(&mut self, name: VarName) -> Option<(TmS, TmV, TyV)> {
166        let Some((i, label, ty)) = self.ctx.lookup(name) else {
167            return self.error(Error::NoSuchVariable(name));
168        };
169        let v = self.ctx.env.get(*i).unwrap().clone();
170        Some((TmS::var(i, name, label), v, ty.clone().unwrap()))
171    }
172
173    fn ob(&mut self, n: &Ob) -> Option<(TmS, TmV, ObjectType)> {
174        match n {
175            Ob::Basic(name) => {
176                let (tm, val, ty) =
177                    self.lookup_tm(NameSegment::Uuid(Uuid::from_str(name).unwrap()))?;
178                let ob_type = match &*ty {
179                    TyV_::Object(ob_type) => ob_type.clone(),
180                    _ => return self.error(Error::ExpectedObject),
181                };
182                Some((tm, val, ob_type))
183            }
184            Ob::App { .. } => self.error(Error::NonDiscreteUnsupported),
185            Ob::List { .. } => self.error(Error::ModalUnsupported),
186            Ob::Tabulated(_) => self.error(Error::TabulatorUnsupported),
187        }
188    }
189
190    fn morphism_cell(
191        &mut self,
192        mor_decl: &MorDecl,
193    ) -> Option<(NameSegment, LabelSegment, TyS, TyV)> {
194        let (mor_type, dom_ty, cod_ty) = match &mor_decl.mor_type {
195            notebook_types::v1::MorType::Basic(name) => {
196                let name = QualifiedName::single(name_seg(*name));
197                let mor_type = Path::single(name);
198                let dom_ty = self.dbl_theory().src_type(&mor_type);
199                let cod_ty = self.dbl_theory().tgt_type(&mor_type);
200                (MorphismType(mor_type), dom_ty, cod_ty)
201            }
202            notebook_types::v1::MorType::Hom(ob_type) => {
203                let ob_type = self.ob_type(ob_type)?;
204                (MorphismType(Path::Id(ob_type.clone())), ob_type.clone(), ob_type)
205            }
206            notebook_types::v1::MorType::Composite(_) => {
207                todo!()
208            }
209            notebook_types::v1::MorType::ModeApp { .. } => {
210                return self.error(Error::ModalUnsupported);
211            }
212        };
213        let name = NameSegment::Uuid(mor_decl.id);
214        let label = LabelSegment::Text(ustr(&mor_decl.name));
215        let dom = mor_decl.dom.as_ref().and_then(|ob| self.ob(ob));
216        let cod = mor_decl.cod.as_ref().and_then(|ob| self.ob(ob));
217        let ((dom_s, dom_v, synthed_dom_ty), (cod_s, cod_v, synthed_cod_ty)) = (dom?, cod?);
218        let correct_dom = if synthed_dom_ty != dom_ty {
219            self.error(Error::MismatchedDomTypes {
220                expected: dom_ty,
221                synthesized: synthed_dom_ty,
222            })
223        } else {
224            Some(())
225        };
226        let correct_cod = if synthed_cod_ty != cod_ty {
227            self.error(Error::MismatchedCodTypes {
228                expected: cod_ty,
229                synthesized: synthed_cod_ty,
230            })
231        } else {
232            Some(())
233        };
234        let _ = (correct_dom?, correct_cod?);
235        Some((
236            name,
237            label,
238            TyS::morphism(mor_type.clone(), dom_s, cod_s),
239            TyV::morphism(mor_type, dom_v, cod_v),
240        ))
241    }
242
243    /// Elaborate a notebook into a type.
244    pub fn notebook(&mut self, cells: &[(Uuid, &ModelJudgment)]) -> Option<(TyS, TyV)> {
245        let mut field_ty0s = Vec::new();
246        let mut field_ty_vs = Vec::new();
247        let self_var = self.intro(name_seg("self"), label_seg("self"), None).as_neu();
248        let c = self.checkpoint();
249        for (id, cell) in cells.iter() {
250            self.current_cell = Some(*id);
251            let (name, label, _, ty_v) = match cell {
252                ModelJudgment::Object(ob_decl) => self.object_cell(ob_decl),
253                ModelJudgment::Morphism(mor_decl) => self.morphism_cell(mor_decl),
254            }?;
255            field_ty0s.push((name, (label, ty_v.ty0())));
256            field_ty_vs.push((name, (label, ty_v.clone())));
257            self.ctx.scope.push(VarInContext::new(name, label, Some(ty_v.clone())));
258            self.ctx.env =
259                self.ctx.env.snoc(TmV::Neu(TmN::proj(self_var.clone(), name, label), ty_v));
260        }
261        self.reset_to(c);
262        let field_tys: Row<_> = field_ty_vs
263            .iter()
264            .map(|(name, (label, ty_v))| (*name, (*label, self.evaluator().quote_ty(ty_v))))
265            .collect();
266        let field_ty0s: Row<_> = field_ty0s.into_iter().collect();
267        let r_s = RecordS::new(field_ty0s.clone(), field_tys.clone());
268        let r_v = RecordV::new(field_ty0s, self.ctx.env.clone(), field_tys, Dtry::empty());
269        Some((TyS::record(r_s), TyV::record(r_v)))
270    }
271}
272
273#[cfg(test)]
274mod test {
275    use notebook_types::v1::ModelDocumentContent;
276    use serde_json;
277    use std::fmt::Write;
278    use std::{fs, rc::Rc};
279
280    use expect_test::{Expect, expect};
281
282    use crate::stdlib::th_schema;
283    use crate::tt::toplevel::{Theory, std_theories};
284    use crate::tt::{
285        modelgen::{generate, model_output},
286        notebook_elab::Elaborator,
287        toplevel::Toplevel,
288    };
289    use crate::zero::name;
290
291    fn elab_example(theory: &Theory, name: &str, expected: Expect) {
292        let src = fs::read_to_string(format!("examples/{name}.json")).unwrap();
293        let doc: ModelDocumentContent = serde_json::from_str(&src).unwrap();
294        let cells = doc
295            .notebook
296            .cells()
297            .filter_map(|c| match c {
298                notebook_types::v1::NotebookCell::Formal { id, content } => Some((*id, content)),
299                _ => None,
300            })
301            .collect::<Vec<_>>();
302        let toplevel = Toplevel::new(std_theories());
303        let mut elab = Elaborator::new(theory.clone(), &toplevel);
304        let mut out = String::new();
305        if let Some((_, ty_v)) = elab.notebook(&cells) {
306            let (model, name_translation) = generate(&toplevel, &theory, &ty_v);
307            model_output("", &mut out, &model, &name_translation).unwrap();
308        } else {
309            assert!(
310                !elab.errors().is_empty(),
311                "did not produce a model, but no errors were reported"
312            );
313            for error in elab.errors() {
314                writeln!(&mut out, "error at cell {:?} : {:?}", error.cell.unwrap(), error.content)
315                    .unwrap()
316            }
317        }
318        expected.assert_eq(&out);
319    }
320
321    #[test]
322    fn examples() {
323        let th_schema = Theory::new(name("ThSchema"), Rc::new(th_schema()));
324        elab_example(
325            &th_schema,
326            "weighted_graph",
327            expect![[r#"
328                object generators:
329                  E : Entity
330                  V : Entity
331                  Weight : AttrType
332                morphism generators:
333                  weight : E -> Weight (Attr)
334                  src : E -> V (Id Entity)
335                  tgt : E -> V (Id Entity)
336            "#]],
337        );
338    }
339}
catlog/tt/notebook_elab.rs

catlog/tt/
notebook_elab.rs
