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        let mut ob_gens: Vec<_> = all_the_same!(match &self.diagram {
175            DblModelDiagramBox::[Discrete](diagram) => {
176                let (_, model) = diagram.into();
177                model.ob_generators().collect()
178            }
179        });
180        ob_gens.sort();
181        ob_gens
182    }
183
184    /// Returns the morphism generators for the diagram's indexing model.
185    #[wasm_bindgen(js_name = "morGenerators")]
186    pub fn mor_generators(&self) -> Vec<QualifiedName> {
187        let mut mor_gens: Vec<_> = all_the_same!(match &self.diagram {
188            DblModelDiagramBox::[Discrete](diagram) => {
189                let (_, model) = diagram.into();
190                model.mor_generators().collect()
191            }
192        });
193        mor_gens.sort();
194        mor_gens
195    }
196
197    /// Returns the object generators of the given object type.
198    #[wasm_bindgen(js_name = "obGeneratorsWithType")]
199    pub fn ob_generators_with_type(&self, ob_type: ObType) -> Result<Vec<QualifiedName>, String> {
200        all_the_same!(match &self.diagram {
201            DblModelDiagramBox::[Discrete](diagram) => {
202                let (_, model) = diagram.into();
203                let ob_type = Elaborator.elab(&ob_type)?;
204                Ok(model.ob_generators_with_type(&ob_type).collect())
205            }
206        })
207    }
208
209    /// Returns the morphism generators of the given morphism type.
210    #[wasm_bindgen(js_name = "morGeneratorsWithType")]
211    pub fn mor_generators_with_type(
212        &self,
213        mor_type: MorType,
214    ) -> Result<Vec<QualifiedName>, String> {
215        all_the_same!(match &self.diagram {
216            DblModelDiagramBox::[Discrete](diagram) => {
217                let (_, model) = diagram.into();
218                let mor_type = Elaborator.elab(&mor_type)?;
219                Ok(model.mor_generators_with_type(&mor_type).collect())
220            }
221        })
222    }
223
224    /// Gets the label, if any, for an object generator in the indexing model.
225    #[wasm_bindgen(js_name = "obGeneratorLabel")]
226    pub fn ob_generator_label(&self, id: &QualifiedName) -> Option<QualifiedLabel> {
227        self.ob_namespace.label(id)
228    }
229
230    /// Gets an object generator with the given label in the indexing model.
231    #[wasm_bindgen(js_name = "obGeneratorWithLabel")]
232    pub fn ob_generator_with_label(&self, label: &QualifiedLabel) -> NameLookup {
233        self.ob_namespace.name_with_label(label)
234    }
235
236    /// Returns array of diagram judgments that would define the diagram.
237    #[wasm_bindgen]
238    pub fn judgments(&self) -> Vec<DiagramJudgment> {
239        let ob_decls = self.ob_declarations().into_iter().map(DiagramJudgment::Object);
240        let mor_decls = self.mor_declarations().into_iter().map(DiagramJudgment::Morphism);
241        ob_decls.chain(mor_decls).collect()
242    }
243
244    /// Returns array of declarations of basic objects.
245    fn ob_declarations(&self) -> Vec<DiagramObDecl> {
246        all_the_same!(match &self.diagram {
247            DblModelDiagramBox::[Discrete](diagram) => {
248                let (mapping, model) = diagram.into();
249                let decls = model.ob_generators().map(|x| {
250                    let maybe_label = self.ob_namespace.label(&x);
251                    DiagramObDecl {
252                        name: maybe_label.map(|label| label.to_string()).unwrap_or_default(),
253                        id: expect_single_uuid(&x),
254                        ob_type: Quoter.quote(&model.ob_generator_type(&x)),
255                        over: mapping.0.ob_generator_map.get(&x).map(|ob| Quoter.quote(ob))
256                    }
257                });
258                decls.collect()
259            }
260        })
261    }
262
263    /// Returns array of declarations of basic morphisms.
264    fn mor_declarations(&self) -> Vec<DiagramMorDecl> {
265        all_the_same!(match &self.diagram {
266            DblModelDiagramBox::[Discrete](diagram) => {
267                let (mapping, model) = diagram.into();
268                let decls = model.mor_generators().map(|f| {
269                    DiagramMorDecl {
270                        name: "".into(),
271                        id: expect_single_uuid(&f),
272                        mor_type: Quoter.quote(&model.mor_generator_type(&f)),
273                        over: mapping.0.mor_generator_map.get(&f).map(|mor| Quoter.quote(mor)),
274                        dom: model.get_dom(&f).map(|ob| Quoter.quote(ob)),
275                        cod: model.get_cod(&f).map(|ob| Quoter.quote(ob)),
276                    }
277                });
278                decls.collect()
279            }
280        })
281    }
282
283    /// Infers missing data in the diagram from the model, where possible.
284    #[wasm_bindgen(js_name = "inferMissingFrom")]
285    pub fn infer_missing_from(&mut self, model: &DblModel) -> Result<(), String> {
286        all_the_same!(match &mut self.diagram {
287            DblModelDiagramBox::[Discrete](diagram) => {
288                let model = (&model.model).try_into().map_err(
289                    |_| "Type of model should match type of diagram")?;
290                diagram.infer_missing_from(model);
291            }
292        });
293
294        // Assign numbers to anonymous objects added by inference.
295        let mut nanon = 0;
296        for id in self.ob_generators() {
297            if self.ob_namespace.label(&id).is_none() {
298                nanon += 1;
299                self.ob_namespace.set_label(expect_single_uuid(&id), nanon.into());
300            }
301        }
302
303        Ok(())
304    }
305
306    /// Validates that the diagram is well defined in a model.
307    #[wasm_bindgen(js_name = "validateIn")]
308    pub fn validate_in(&self, model: &DblModel) -> Result<ModelDiagramValidationResult, String> {
309        let result = all_the_same!(match &self.diagram {
310            DblModelDiagramBox::[Discrete](diagram) => {
311                let model = (&model.model).try_into().map_err(
312                    |_| "Type of model should match type of diagram")?;
313                diagram.validate_in(model)
314            }
315        });
316        Ok(ModelDiagramValidationResult(result.map_err(|errs| errs.into()).into()))
317    }
318}
319
320/// XXX: We only use this in `DblModelDiagram.judgments`, which probably
321/// shouldn't need anyway but is currently used in the Decapodes interop.
322fn expect_single_uuid(name: &QualifiedName) -> Uuid {
323    match name.only() {
324        Some(NameSegment::Uuid(uuid)) => uuid,
325        _ => panic!("Only names that are single UUIDs are currently supported in notebook types"),
326    }
327}
328
329/// Result of validating a diagram in a model.
330#[derive(Serialize, Deserialize, Tsify)]
331#[tsify(into_wasm_abi, from_wasm_abi)]
332pub struct ModelDiagramValidationResult(
333    pub JsResult<(), Vec<diagram::InvalidDiscreteDblModelDiagram>>,
334);
335
336/// Elaborates a diagram defined by a notebook into a catlog diagram.
337#[wasm_bindgen(js_name = "elaborateDiagram")]
338pub fn elaborate_diagram(
339    judgments: Vec<DiagramJudgment>,
340    theory: &DblTheory,
341) -> Result<DblModelDiagram, String> {
342    let mut diagram = DblModelDiagram::new(theory);
343    for judgment in judgments {
344        match judgment {
345            DiagramJudgment::Object(decl) => diagram.add_ob(&decl)?,
346            DiagramJudgment::Morphism(decl) => diagram.add_mor(&decl)?,
347        }
348    }
349    Ok(diagram)
350}
351
352#[cfg(test)]
353mod tests {
354    use uuid::Uuid;
355
356    use super::*;
357    use crate::model::tests::sch_walking_attr;
358    use crate::theories::*;
359
360    #[test]
361    fn diagram_schema() {
362        let th = ThSchema::new().theory();
363        let [attr, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
364        let model = sch_walking_attr(&th, [attr, entity, attr_type]);
365
366        let mut diagram = DblModelDiagram::new(&th);
367        let [x, y, var] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
368        assert!(
369            diagram
370                .add_ob(&DiagramObDecl {
371                    name: "var".into(),
372                    id: var,
373                    ob_type: ObType::Basic("AttrType".into()),
374                    over: Some(Ob::Basic(attr_type.to_string()))
375                })
376                .is_ok()
377        );
378        let [a, b] = [Uuid::now_v7(), Uuid::now_v7()];
379        for (name, indiv, f) in [("x", x, a), ("y", y, b)] {
380            assert!(
381                diagram
382                    .add_ob(&DiagramObDecl {
383                        name: name.into(),
384                        id: indiv,
385                        ob_type: ObType::Basic("Entity".into()),
386                        over: Some(Ob::Basic(entity.to_string())),
387                    })
388                    .is_ok()
389            );
390            assert!(
391                diagram
392                    .add_mor(&DiagramMorDecl {
393                        name: "".into(),
394                        id: f,
395                        mor_type: MorType::Basic("Attr".into()),
396                        dom: Some(Ob::Basic(indiv.to_string())),
397                        cod: Some(Ob::Basic(var.to_string())),
398                        over: Some(Mor::Basic(attr.to_string())),
399                    })
400                    .is_ok()
401            );
402        }
403        assert_eq!(diagram.get_dom(&a.into()), Some(Ob::Basic(x.into())));
404        assert_eq!(diagram.get_cod(&a.into()), Some(Ob::Basic(var.into())));
405        assert_eq!(diagram.get_ob_over(&x.into()), Some(Ob::Basic(entity.into())));
406        assert_eq!(diagram.get_mor_over(&a.into()), Some(Mor::Basic(attr.into())));
407        assert_eq!(diagram.ob_generator_label(&var.into()), Some("var".into()));
408        assert_eq!(diagram.ob_generator_with_label(&"var".into()), NameLookup::Unique(var.into()));
409        assert_eq!(diagram.ob_generators().len(), 3);
410        assert_eq!(diagram.mor_generators().len(), 2);
411        assert_eq!(diagram.judgments().len(), 5);
412        assert_eq!(diagram.validate_in(&model).unwrap().0, JsResult::Ok(()));
413    }
414}
catlog_wasm/model_diagram.rs

catlog_wasm/
model_diagram.rs
