catlog_wasm/
model_diagram.rs

1//! Wasm bindings for diagrams in models of a double theory.
2
3use std::rc::Rc;
4
5use all_the_same::all_the_same;
6use derive_more::From;
7use serde::{Deserialize, Serialize};
8use tsify::Tsify;
9use wasm_bindgen::prelude::*;
10
11use catlog::dbl::model::{DblModel as _, DiscreteDblModel, FgDblModel, MutDblModel};
12use catlog::dbl::model_diagram as diagram;
13use catlog::dbl::model_morphism::DiscreteDblModelMapping;
14use catlog::one::FgCategory;
15use catlog::zero::{MutMapping, NameLookup, NameSegment, Namespace, QualifiedLabel, QualifiedName};
16use notebook_types::current::*;
17
18use super::model::DblModel;
19use super::model_diagram_presentation::*;
20use super::notation::*;
21use super::result::JsResult;
22use super::theory::{DblTheory, DblTheoryBox};
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 diagram = match &theory.0 {
45            DblTheoryBox::Discrete(theory) => {
46                let mapping = Default::default();
47                let model = DiscreteDblModel::new(theory.clone());
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 the object type of an object in the diagram's indexing model.
106    #[wasm_bindgen(js_name = "obType")]
107    pub fn ob_type(&self, ob: Ob) -> Result<ObType, String> {
108        all_the_same!(match &self.diagram {
109            DblModelDiagramBox::[Discrete](diagram) => {
110                let (_, model) = diagram.into();
111                Ok(Quoter.quote(&model.ob_type(&Elaborator.elab(&ob)?)))
112            }
113        })
114    }
115
116    /// Gets the morphism type of a morphism in the diagram's indexing model.
117    #[wasm_bindgen(js_name = "morType")]
118    pub fn mor_type(&self, mor: Mor) -> Result<MorType, String> {
119        all_the_same!(match &self.diagram {
120            DblModelDiagramBox::[Discrete](diagram) => {
121                let (_, model) = diagram.into();
122                Ok(Quoter.quote(&model.mor_type(&Elaborator.elab(&mor)?)))
123            }
124        })
125    }
126
127    /// Returns the object generators for the diagram's indexing model.
128    #[wasm_bindgen(js_name = "obGenerators")]
129    pub fn ob_generators(&self) -> Vec<QualifiedName> {
130        all_the_same!(match &self.diagram {
131            DblModelDiagramBox::[Discrete](diagram) => {
132                let (_, model) = diagram.into();
133                model.ob_generators().collect()
134            }
135        })
136    }
137
138    /// Returns the morphism generators for the diagram's indexing model.
139    #[wasm_bindgen(js_name = "morGenerators")]
140    pub fn mor_generators(&self) -> Vec<QualifiedName> {
141        all_the_same!(match &self.diagram {
142            DblModelDiagramBox::[Discrete](diagram) => {
143                let (_, model) = diagram.into();
144                model.mor_generators().collect()
145            }
146        })
147    }
148
149    /// Returns the object generators of the given object type.
150    #[wasm_bindgen(js_name = "obGeneratorsWithType")]
151    pub fn ob_generators_with_type(&self, ob_type: ObType) -> Result<Vec<QualifiedName>, String> {
152        all_the_same!(match &self.diagram {
153            DblModelDiagramBox::[Discrete](diagram) => {
154                let (_, model) = diagram.into();
155                let ob_type = Elaborator.elab(&ob_type)?;
156                Ok(model.ob_generators_with_type(&ob_type).collect())
157            }
158        })
159    }
160
161    /// Returns the morphism generators of the given morphism type.
162    #[wasm_bindgen(js_name = "morGeneratorsWithType")]
163    pub fn mor_generators_with_type(
164        &self,
165        mor_type: MorType,
166    ) -> Result<Vec<QualifiedName>, String> {
167        all_the_same!(match &self.diagram {
168            DblModelDiagramBox::[Discrete](diagram) => {
169                let (_, model) = diagram.into();
170                let mor_type = Elaborator.elab(&mor_type)?;
171                Ok(model.mor_generators_with_type(&mor_type).collect())
172            }
173        })
174    }
175
176    /// Gets the label, if any, for an object generator in the indexing model.
177    #[wasm_bindgen(js_name = "obGeneratorLabel")]
178    pub fn ob_generator_label(&self, id: &QualifiedName) -> Option<QualifiedLabel> {
179        self.ob_namespace.label(id)
180    }
181
182    /// Gets an object generator with the given label in the indexing model.
183    #[wasm_bindgen(js_name = "obGeneratorWithLabel")]
184    pub fn ob_generator_with_label(&self, label: &QualifiedLabel) -> NameLookup {
185        self.ob_namespace.name_with_label(label)
186    }
187
188    /// Gets an object generator as it appears in the diagram's presentation.
189    #[wasm_bindgen(js_name = "obPresentation")]
190    pub fn ob_presentation(&self, id: QualifiedName) -> Option<DiagramObGenerator> {
191        let label = self.ob_generator_label(&id);
192        let (ob_type, over) = all_the_same!(match &self.diagram {
193            DblModelDiagramBox::[Discrete](diagram) => {
194                let (mapping, model) = diagram.into();
195                (Quoter.quote(&model.ob_generator_type(&id)),
196                 Quoter.quote(mapping.0.ob_generator_map.get(&id)?))
197            }
198        });
199        Some(DiagramObGenerator {
200            id,
201            label,
202            ob_type,
203            over,
204        })
205    }
206
207    /// Gets a morphism generator as it appears in the diagram's presentation.
208    #[wasm_bindgen(js_name = "morPresentation")]
209    pub fn mor_presentation(&self, id: QualifiedName) -> Option<DiagramMorGenerator> {
210        let (mor_type, over, dom, cod) = all_the_same!(match &self.diagram {
211            DblModelDiagramBox::[Discrete](diagram) => {
212                let (mapping, model) = diagram.into();
213                (Quoter.quote(&model.mor_generator_type(&id)),
214                 Quoter.quote(mapping.0.mor_generator_map.get(&id)?),
215                 Quoter.quote(model.get_dom(&id)?),
216                 Quoter.quote(model.get_cod(&id)?))
217            }
218        });
219        Some(DiagramMorGenerator {
220            id,
221            mor_type,
222            over,
223            dom,
224            cod,
225        })
226    }
227
228    /// Constructs a serializable presentation of the diagram.
229    #[wasm_bindgen]
230    pub fn presentation(&self) -> ModelDiagramPresentation {
231        all_the_same!(match &self.diagram {
232            DblModelDiagramBox::[Discrete](diagram) => {
233                let (_, model) = diagram.into();
234                ModelDiagramPresentation {
235                    ob_generators: {
236                        model.ob_generators().filter_map(|id| self.ob_presentation(id)).collect()
237                    },
238                    mor_generators: {
239                        model.mor_generators().filter_map(|id| self.mor_presentation(id)).collect()
240                    }
241                }
242            }
243        })
244    }
245
246    /// Infers missing data in the diagram from the model, where possible.
247    #[wasm_bindgen(js_name = "inferMissingFrom")]
248    pub fn infer_missing_from(&mut self, model: &DblModel) -> Result<(), String> {
249        all_the_same!(match &mut self.diagram {
250            DblModelDiagramBox::[Discrete](diagram) => {
251                let model: &Rc<_> = (&model.model).try_into().map_err(
252                    |_| "Type of model should match type of diagram")?;
253                diagram.infer_missing_from(model);
254            }
255        });
256
257        // Assign numbers to anonymous objects added by inference.
258        let mut nanon = 0;
259        for id in self.ob_generators() {
260            if self.ob_namespace.label(&id).is_none() {
261                let Some(NameSegment::Uuid(uuid)) = id.only() else {
262                    todo!("Imputation for diagrams with instantiations");
263                };
264                nanon += 1;
265                self.ob_namespace.set_label(uuid, nanon.into());
266            }
267        }
268
269        Ok(())
270    }
271
272    /// Validates that the diagram is well defined in a model.
273    #[wasm_bindgen(js_name = "validateIn")]
274    pub fn validate_in(&self, model: &DblModel) -> Result<ModelDiagramValidationResult, String> {
275        let result = all_the_same!(match &self.diagram {
276            DblModelDiagramBox::[Discrete](diagram) => {
277                let model: &Rc<_> = (&model.model).try_into().map_err(
278                    |_| "Type of model should match type of diagram")?;
279                diagram.validate_in(model)
280            }
281        });
282        Ok(ModelDiagramValidationResult(result.map_err(|errs| errs.into()).into()))
283    }
284}
285
286/// Result of validating a diagram in a model.
287#[derive(Serialize, Deserialize, Tsify)]
288#[tsify(into_wasm_abi, from_wasm_abi)]
289pub struct ModelDiagramValidationResult(
290    pub JsResult<(), Vec<diagram::InvalidDiscreteDblModelDiagram>>,
291);
292
293/// Elaborates a diagram defined by a notebook into a catlog diagram.
294#[wasm_bindgen(js_name = "elaborateDiagram")]
295pub fn elaborate_diagram(
296    judgments: Vec<DiagramJudgment>,
297    theory: &DblTheory,
298) -> Result<DblModelDiagram, String> {
299    let mut diagram = DblModelDiagram::new(theory);
300    for judgment in judgments {
301        match judgment {
302            DiagramJudgment::Object(decl) => diagram.add_ob(&decl)?,
303            DiagramJudgment::Morphism(decl) => diagram.add_mor(&decl)?,
304        }
305    }
306    Ok(diagram)
307}
308
309#[cfg(test)]
310mod tests {
311    use uuid::Uuid;
312
313    use super::*;
314    use crate::model::tests::sch_walking_attr;
315    use crate::theories::*;
316
317    #[test]
318    fn diagram_schema() {
319        let th = ThSchema::new().theory();
320        let [attr, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
321        let model = sch_walking_attr(&th, [attr, entity, attr_type]);
322
323        let mut diagram = DblModelDiagram::new(&th);
324        let [x, y, var] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
325        assert!(
326            diagram
327                .add_ob(&DiagramObDecl {
328                    name: "var".into(),
329                    id: var,
330                    ob_type: ObType::Basic("AttrType".into()),
331                    over: Some(Ob::Basic(attr_type.to_string()))
332                })
333                .is_ok()
334        );
335        let [a, b] = [Uuid::now_v7(), Uuid::now_v7()];
336        for (name, indiv, f) in [("x", x, a), ("y", y, b)] {
337            assert!(
338                diagram
339                    .add_ob(&DiagramObDecl {
340                        name: name.into(),
341                        id: indiv,
342                        ob_type: ObType::Basic("Entity".into()),
343                        over: Some(Ob::Basic(entity.to_string())),
344                    })
345                    .is_ok()
346            );
347            assert!(
348                diagram
349                    .add_mor(&DiagramMorDecl {
350                        name: "".into(),
351                        id: f,
352                        mor_type: MorType::Basic("Attr".into()),
353                        dom: Some(Ob::Basic(indiv.to_string())),
354                        cod: Some(Ob::Basic(var.to_string())),
355                        over: Some(Mor::Basic(attr.to_string())),
356                    })
357                    .is_ok()
358            );
359        }
360        assert_eq!(diagram.ob_generator_label(&var.into()), Some("var".into()));
361        assert_eq!(diagram.ob_generator_with_label(&"var".into()), NameLookup::Unique(var.into()));
362        assert_eq!(diagram.ob_generators().len(), 3);
363        assert_eq!(diagram.mor_generators().len(), 2);
364        assert_eq!(diagram.validate_in(&model).unwrap().0, JsResult::Ok(()));
365
366        let presentation = diagram.presentation();
367        assert_eq!(presentation.ob_generators.len(), 3);
368        assert_eq!(presentation.mor_generators.len(), 2);
369    }
370}
catlog_wasm/model_diagram.rs

catlog_wasm/
model_diagram.rs
