catlog_wasm/
model_diagram.rs

1//! Wasm bindings for diagrams in models of a double theory.
2
3use all_the_same::all_the_same;
4use derive_more::From;
5use serde::{Deserialize, Serialize};
6use tsify::Tsify;
7use uuid::Uuid;
8use wasm_bindgen::prelude::*;
9
10use catlog::dbl::model::{DblModel as _, DiscreteDblModel, FgDblModel, MutDblModel};
11use catlog::dbl::model_diagram as diagram;
12use catlog::dbl::model_morphism::DiscreteDblModelMapping;
13use catlog::one::FgCategory;
14use catlog::zero::{
15    Mapping, MutMapping, NameLookup, NameSegment, Namespace, QualifiedLabel, QualifiedName,
16};
17use notebook_types::current::*;
18
19use super::model::{DblModel, DblModelBox};
20use super::notation::*;
21use super::result::JsResult;
22use super::theory::DblTheory;
23
24/// A box containing a diagram in a model of a double theory.
25#[derive(From)]
26pub enum DblModelDiagramBox {
27    /// A diagram in a model of a discrete double theory.
28    Discrete(diagram::DblModelDiagram<DiscreteDblModelMapping, DiscreteDblModel>),
29    // Modal(), # TODO: Not implemented.
30}
31
32/// Wasm binding for a diagram in a model of a double theory.
33#[wasm_bindgen]
34pub struct DblModelDiagram {
35    /// The boxed underlying diagram.
36    #[wasm_bindgen(skip)]
37    pub diagram: DblModelDiagramBox,
38    ob_namespace: Namespace,
39}
40
41impl DblModelDiagram {
42    /// Creates an empty diagram for the given theory.
43    pub fn new(theory: &DblTheory) -> Self {
44        let model = DblModel::new(theory);
45        let diagram = match model.model {
46            DblModelBox::Discrete(model) => {
47                let mapping = Default::default();
48                diagram::DblModelDiagram(mapping, model).into()
49            }
50            _ => panic!("Diagrams only implemented for discrete double theories"),
51        };
52        Self {
53            diagram,
54            ob_namespace: Namespace::new_for_uuid(),
55        }
56    }
57
58    /// Adds an object to the diagram.
59    pub fn add_ob(&mut self, decl: &DiagramObDecl) -> Result<(), String> {
60        all_the_same!(match &mut self.diagram {
61            DblModelDiagramBox::[Discrete](diagram) => {
62                let (mapping, model) = diagram.into();
63                let ob_type: QualifiedName = Elaborator.elab(&decl.ob_type)?;
64                if let Some(over) = decl.over.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? {
65                    mapping.assign_ob(decl.id.into(), over);
66                }
67                model.add_ob(decl.id.into(), ob_type);
68            }
69        });
70        if !decl.name.is_empty() {
71            self.ob_namespace.set_label(decl.id, decl.name.as_str().into());
72        }
73        Ok(())
74    }
75
76    /// Adds a morphism to the diagram.
77    pub fn add_mor(&mut self, decl: &DiagramMorDecl) -> Result<(), String> {
78        all_the_same!(match &mut self.diagram {
79            DblModelDiagramBox::[Discrete](diagram) => {
80                let (mapping, model) = diagram.into();
81                let mor_type = Elaborator.elab(&decl.mor_type)?;
82                model.make_mor(decl.id.into(), mor_type);
83                if let Some(dom) = decl.dom.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? {
84                    model.set_dom(decl.id.into(), dom);
85                }
86                if let Some(cod) = decl.cod.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? {
87                    model.set_cod(decl.id.into(), cod);
88                }
89                if let Some(over) = decl.over.as_ref().map(|mor| Elaborator.elab(mor)).transpose()? {
90                    mapping.assign_mor(decl.id.into(), over);
91                }
92            }
93        });
94        if decl.name.is_empty() {
95            Ok(())
96        } else {
97            // There's no reason for this, but it's what we're currently doing.
98            Err("Indexing morphisms in diagrams cannot be labeled".into())
99        }
100    }
101}
102
103#[wasm_bindgen]
104impl DblModelDiagram {
105    /// Gets domain of a morphism generator for the diagram's indexing model.
106    #[wasm_bindgen(js_name = "getDom")]
107    pub fn get_dom(&self, id: &QualifiedName) -> Option<Ob> {
108        all_the_same!(match &self.diagram {
109            DblModelDiagramBox::[Discrete](diagram) => {
110                let (_, model) = diagram.into();
111                model.get_dom(id).map(|ob| Quoter.quote(ob))
112            }
113        })
114    }
115
116    /// Gets codomain of a morphism generator for the diagram's indexing model.
117    #[wasm_bindgen(js_name = "getCod")]
118    pub fn get_cod(&self, id: &QualifiedName) -> Option<Ob> {
119        all_the_same!(match &self.diagram {
120            DblModelDiagramBox::[Discrete](diagram) => {
121                let (_, model) = diagram.into();
122                model.get_cod(id).map(|ob| Quoter.quote(ob))
123            }
124        })
125    }
126
127    /// Gets the object that the given object generator is over.
128    #[wasm_bindgen(js_name = "getObOver")]
129    pub fn get_ob_over(&self, id: &QualifiedName) -> Option<Ob> {
130        all_the_same!(match &self.diagram {
131            DblModelDiagramBox::[Discrete](diagram) => {
132                let (mapping, _) = diagram.into();
133                mapping.0.ob_generator_map.apply_to_ref(id).map(|ob| Quoter.quote(&ob))
134            }
135        })
136    }
137
138    /// Gets the morphism that the given morphism generator is over.
139    #[wasm_bindgen(js_name = "getMorOver")]
140    pub fn get_mor_over(&self, id: &QualifiedName) -> Option<Mor> {
141        all_the_same!(match &self.diagram {
142            DblModelDiagramBox::[Discrete](diagram) => {
143                let (mapping, _) = diagram.into();
144                mapping.0.mor_generator_map.apply_to_ref(id).map(|mor| Quoter.quote(&mor))
145            }
146        })
147    }
148
149    /// Gets the object type of an object in the diagram's indexing model.
150    #[wasm_bindgen(js_name = "obType")]
151    pub fn ob_type(&self, ob: Ob) -> Result<ObType, String> {
152        all_the_same!(match &self.diagram {
153            DblModelDiagramBox::[Discrete](diagram) => {
154                let (_, model) = diagram.into();
155                Ok(Quoter.quote(&model.ob_type(&Elaborator.elab(&ob)?)))
156            }
157        })
158    }
159
160    /// Gets the morphism type of a morphism in the diagram's indexing model.
161    #[wasm_bindgen(js_name = "morType")]
162    pub fn mor_type(&self, mor: Mor) -> Result<MorType, String> {
163        all_the_same!(match &self.diagram {
164            DblModelDiagramBox::[Discrete](diagram) => {
165                let (_, model) = diagram.into();
166                Ok(Quoter.quote(&model.mor_type(&Elaborator.elab(&mor)?)))
167            }
168        })
169    }
170
171    /// Returns the object generators for the diagram's indexing model.
172    #[wasm_bindgen(js_name = "obGenerators")]
173    pub fn ob_generators(&self) -> Vec<QualifiedName> {
174        all_the_same!(match &self.diagram {
175            DblModelDiagramBox::[Discrete](diagram) => {
176                let (_, model) = diagram.into();
177                model.ob_generators().collect()
178            }
179        })
180    }
181
182    /// Returns the morphism generators for the diagram's indexing model.
183    #[wasm_bindgen(js_name = "morGenerators")]
184    pub fn mor_generators(&self) -> Vec<QualifiedName> {
185        all_the_same!(match &self.diagram {
186            DblModelDiagramBox::[Discrete](diagram) => {
187                let (_, model) = diagram.into();
188                model.mor_generators().collect()
189            }
190        })
191    }
192
193    /// Returns the object generators of the given object type.
194    #[wasm_bindgen(js_name = "obGeneratorsWithType")]
195    pub fn ob_generators_with_type(&self, ob_type: ObType) -> Result<Vec<QualifiedName>, String> {
196        all_the_same!(match &self.diagram {
197            DblModelDiagramBox::[Discrete](diagram) => {
198                let (_, model) = diagram.into();
199                let ob_type = Elaborator.elab(&ob_type)?;
200                Ok(model.ob_generators_with_type(&ob_type).collect())
201            }
202        })
203    }
204
205    /// Returns the morphism generators of the given morphism type.
206    #[wasm_bindgen(js_name = "morGeneratorsWithType")]
207    pub fn mor_generators_with_type(
208        &self,
209        mor_type: MorType,
210    ) -> Result<Vec<QualifiedName>, String> {
211        all_the_same!(match &self.diagram {
212            DblModelDiagramBox::[Discrete](diagram) => {
213                let (_, model) = diagram.into();
214                let mor_type = Elaborator.elab(&mor_type)?;
215                Ok(model.mor_generators_with_type(&mor_type).collect())
216            }
217        })
218    }
219
220    /// Gets the label, if any, for an object generator in the indexing model.
221    #[wasm_bindgen(js_name = "obGeneratorLabel")]
222    pub fn ob_generator_label(&self, id: &QualifiedName) -> Option<QualifiedLabel> {
223        self.ob_namespace.label(id)
224    }
225
226    /// Gets an object generator with the given label in the indexing model.
227    #[wasm_bindgen(js_name = "obGeneratorWithLabel")]
228    pub fn ob_generator_with_label(&self, label: &QualifiedLabel) -> NameLookup {
229        self.ob_namespace.name_with_label(label)
230    }
231
232    /// Returns array of diagram judgments that would define the diagram.
233    #[wasm_bindgen]
234    pub fn judgments(&self) -> Vec<DiagramJudgment> {
235        let ob_decls = self.ob_declarations().into_iter().map(DiagramJudgment::Object);
236        let mor_decls = self.mor_declarations().into_iter().map(DiagramJudgment::Morphism);
237        ob_decls.chain(mor_decls).collect()
238    }
239
240    /// Returns array of declarations of basic objects.
241    fn ob_declarations(&self) -> Vec<DiagramObDecl> {
242        all_the_same!(match &self.diagram {
243            DblModelDiagramBox::[Discrete](diagram) => {
244                let (mapping, model) = diagram.into();
245                let decls = model.ob_generators().map(|x| {
246                    let maybe_label = self.ob_namespace.label(&x);
247                    DiagramObDecl {
248                        name: maybe_label.map(|label| label.to_string()).unwrap_or_default(),
249                        id: expect_single_uuid(&x),
250                        ob_type: Quoter.quote(&model.ob_generator_type(&x)),
251                        over: mapping.0.ob_generator_map.get(&x).map(|ob| Quoter.quote(ob))
252                    }
253                });
254                decls.collect()
255            }
256        })
257    }
258
259    /// Returns array of declarations of basic morphisms.
260    fn mor_declarations(&self) -> Vec<DiagramMorDecl> {
261        all_the_same!(match &self.diagram {
262            DblModelDiagramBox::[Discrete](diagram) => {
263                let (mapping, model) = diagram.into();
264                let decls = model.mor_generators().map(|f| {
265                    DiagramMorDecl {
266                        name: "".into(),
267                        id: expect_single_uuid(&f),
268                        mor_type: Quoter.quote(&model.mor_generator_type(&f)),
269                        over: mapping.0.mor_generator_map.get(&f).map(|mor| Quoter.quote(mor)),
270                        dom: model.get_dom(&f).map(|ob| Quoter.quote(ob)),
271                        cod: model.get_cod(&f).map(|ob| Quoter.quote(ob)),
272                    }
273                });
274                decls.collect()
275            }
276        })
277    }
278
279    /// Infers missing data in the diagram from the model, where possible.
280    #[wasm_bindgen(js_name = "inferMissingFrom")]
281    pub fn infer_missing_from(&mut self, model: &DblModel) -> Result<(), String> {
282        all_the_same!(match &mut self.diagram {
283            DblModelDiagramBox::[Discrete](diagram) => {
284                let model = (&model.model).try_into().map_err(
285                    |_| "Type of model should match type of diagram")?;
286                diagram.infer_missing_from(model);
287            }
288        });
289
290        // Assign numbers to anonymous objects added by inference.
291        let mut nanon = 0;
292        for id in self.ob_generators() {
293            if self.ob_namespace.label(&id).is_none() {
294                nanon += 1;
295                self.ob_namespace.set_label(expect_single_uuid(&id), nanon.into());
296            }
297        }
298
299        Ok(())
300    }
301
302    /// Validates that the diagram is well defined in a model.
303    #[wasm_bindgen(js_name = "validateIn")]
304    pub fn validate_in(&self, model: &DblModel) -> Result<ModelDiagramValidationResult, String> {
305        let result = all_the_same!(match &self.diagram {
306            DblModelDiagramBox::[Discrete](diagram) => {
307                let model = (&model.model).try_into().map_err(
308                    |_| "Type of model should match type of diagram")?;
309                diagram.validate_in(model)
310            }
311        });
312        Ok(ModelDiagramValidationResult(result.map_err(|errs| errs.into()).into()))
313    }
314}
315
316/// XXX: We only use this in `DblModelDiagram.judgments`, which probably
317/// shouldn't need anyway but is currently used in the Decapodes interop.
318fn expect_single_uuid(name: &QualifiedName) -> Uuid {
319    match name.only() {
320        Some(NameSegment::Uuid(uuid)) => uuid,
321        _ => panic!("Only names that are single UUIDs are currently supported in notebook types"),
322    }
323}
324
325/// Result of validating a diagram in a model.
326#[derive(Serialize, Deserialize, Tsify)]
327#[tsify(into_wasm_abi, from_wasm_abi)]
328pub struct ModelDiagramValidationResult(
329    pub JsResult<(), Vec<diagram::InvalidDiscreteDblModelDiagram>>,
330);
331
332/// Elaborates a diagram defined by a notebook into a catlog diagram.
333#[wasm_bindgen(js_name = "elaborateDiagram")]
334pub fn elaborate_diagram(
335    judgments: Vec<DiagramJudgment>,
336    theory: &DblTheory,
337) -> Result<DblModelDiagram, String> {
338    let mut diagram = DblModelDiagram::new(theory);
339    for judgment in judgments {
340        match judgment {
341            DiagramJudgment::Object(decl) => diagram.add_ob(&decl)?,
342            DiagramJudgment::Morphism(decl) => diagram.add_mor(&decl)?,
343        }
344    }
345    Ok(diagram)
346}
347
348#[cfg(test)]
349mod tests {
350    use uuid::Uuid;
351
352    use super::*;
353    use crate::model::tests::sch_walking_attr;
354    use crate::theories::*;
355
356    #[test]
357    fn diagram_schema() {
358        let th = ThSchema::new().theory();
359        let [attr, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
360        let model = sch_walking_attr(&th, [attr, entity, attr_type]);
361
362        let mut diagram = DblModelDiagram::new(&th);
363        let [x, y, var] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
364        assert!(
365            diagram
366                .add_ob(&DiagramObDecl {
367                    name: "var".into(),
368                    id: var,
369                    ob_type: ObType::Basic("AttrType".into()),
370                    over: Some(Ob::Basic(attr_type.to_string()))
371                })
372                .is_ok()
373        );
374        let [a, b] = [Uuid::now_v7(), Uuid::now_v7()];
375        for (name, indiv, f) in [("x", x, a), ("y", y, b)] {
376            assert!(
377                diagram
378                    .add_ob(&DiagramObDecl {
379                        name: name.into(),
380                        id: indiv,
381                        ob_type: ObType::Basic("Entity".into()),
382                        over: Some(Ob::Basic(entity.to_string())),
383                    })
384                    .is_ok()
385            );
386            assert!(
387                diagram
388                    .add_mor(&DiagramMorDecl {
389                        name: "".into(),
390                        id: f,
391                        mor_type: MorType::Basic("Attr".into()),
392                        dom: Some(Ob::Basic(indiv.to_string())),
393                        cod: Some(Ob::Basic(var.to_string())),
394                        over: Some(Mor::Basic(attr.to_string())),
395                    })
396                    .is_ok()
397            );
398        }
399        assert_eq!(diagram.get_dom(&a.into()), Some(Ob::Basic(x.into())));
400        assert_eq!(diagram.get_cod(&a.into()), Some(Ob::Basic(var.into())));
401        assert_eq!(diagram.get_ob_over(&x.into()), Some(Ob::Basic(entity.into())));
402        assert_eq!(diagram.get_mor_over(&a.into()), Some(Mor::Basic(attr.into())));
403        assert_eq!(diagram.ob_generator_label(&var.into()), Some("var".into()));
404        assert_eq!(diagram.ob_generator_with_label(&"var".into()), NameLookup::Unique(var.into()));
405        assert_eq!(diagram.ob_generators().len(), 3);
406        assert_eq!(diagram.mor_generators().len(), 2);
407        assert_eq!(diagram.judgments().len(), 5);
408        assert_eq!(diagram.validate_in(&model).unwrap().0, JsResult::Ok(()));
409    }
410}
catlog_wasm/model_diagram.rs

catlog_wasm/
model_diagram.rs
