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

catlog_wasm/
model_diagram.rs
