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 { id, label, ob_type, over })
200    }
201
202    /// Gets a morphism generator as it appears in the diagram's presentation.
203    #[wasm_bindgen(js_name = "morPresentation")]
204    pub fn mor_presentation(&self, id: QualifiedName) -> Option<DiagramMorGenerator> {
205        let (mor_type, over, dom, cod) = all_the_same!(match &self.diagram {
206            DblModelDiagramBox::[Discrete](diagram) => {
207                let (mapping, model) = diagram.into();
208                (Quoter.quote(&model.mor_generator_type(&id)),
209                 Quoter.quote(mapping.0.mor_generator_map.get(&id)?),
210                 Quoter.quote(model.get_dom(&id)?),
211                 Quoter.quote(model.get_cod(&id)?))
212            }
213        });
214        Some(DiagramMorGenerator { id, mor_type, over, dom, cod })
215    }
216
217    /// Constructs a serializable presentation of the diagram.
218    #[wasm_bindgen]
219    pub fn presentation(&self) -> ModelDiagramPresentation {
220        all_the_same!(match &self.diagram {
221            DblModelDiagramBox::[Discrete](diagram) => {
222                let (_, model) = diagram.into();
223                ModelDiagramPresentation {
224                    ob_generators: {
225                        model.ob_generators().filter_map(|id| self.ob_presentation(id)).collect()
226                    },
227                    mor_generators: {
228                        model.mor_generators().filter_map(|id| self.mor_presentation(id)).collect()
229                    }
230                }
231            }
232        })
233    }
234
235    /// Infers missing data in the diagram from the model, where possible.
236    #[wasm_bindgen(js_name = "inferMissingFrom")]
237    pub fn infer_missing_from(&mut self, model: &DblModel) -> Result<(), String> {
238        all_the_same!(match &mut self.diagram {
239            DblModelDiagramBox::[Discrete](diagram) => {
240                let model: &Rc<_> = (&model.model).try_into().map_err(
241                    |_| "Type of model should match type of diagram")?;
242                diagram.infer_missing_from(model);
243            }
244        });
245
246        // Assign numbers to anonymous objects added by inference.
247        let mut nanon = 0;
248        for id in self.ob_generators() {
249            if self.ob_namespace.label(&id).is_none() {
250                let Some(NameSegment::Uuid(uuid)) = id.only() else {
251                    todo!("Imputation for diagrams with instantiations");
252                };
253                nanon += 1;
254                self.ob_namespace.set_label(uuid, nanon.into());
255            }
256        }
257
258        Ok(())
259    }
260
261    /// Validates that the diagram is well defined in a model.
262    #[wasm_bindgen(js_name = "validateIn")]
263    pub fn validate_in(&self, model: &DblModel) -> Result<ModelDiagramValidationResult, String> {
264        let result = all_the_same!(match &self.diagram {
265            DblModelDiagramBox::[Discrete](diagram) => {
266                let model: &Rc<_> = (&model.model).try_into().map_err(
267                    |_| "Type of model should match type of diagram")?;
268                diagram.validate_in(model)
269            }
270        });
271        Ok(ModelDiagramValidationResult(result.map_err(|errs| errs.into()).into()))
272    }
273}
274
275/// Result of validating a diagram in a model.
276#[derive(Serialize, Deserialize, Tsify)]
277#[tsify(into_wasm_abi, from_wasm_abi)]
278pub struct ModelDiagramValidationResult(
279    pub JsResult<(), Vec<diagram::InvalidDiscreteDblModelDiagram>>,
280);
281
282/// Elaborates a diagram defined by a notebook into a catlog diagram.
283#[wasm_bindgen(js_name = "elaborateDiagram")]
284pub fn elaborate_diagram(
285    judgments: Vec<DiagramJudgment>,
286    theory: &DblTheory,
287) -> Result<DblModelDiagram, String> {
288    let mut diagram = DblModelDiagram::new(theory);
289    for judgment in judgments {
290        match judgment {
291            DiagramJudgment::Object(decl) => diagram.add_ob(&decl)?,
292            DiagramJudgment::Morphism(decl) => diagram.add_mor(&decl)?,
293        }
294    }
295    Ok(diagram)
296}
297
298#[cfg(test)]
299mod tests {
300    use uuid::Uuid;
301
302    use super::*;
303    use crate::model::tests::sch_walking_attr;
304    use crate::theories::*;
305
306    #[test]
307    fn diagram_schema() {
308        let th = ThSchema::new().theory();
309        let [attr, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
310        let model = sch_walking_attr(&th, [attr, entity, attr_type]);
311
312        let mut diagram = DblModelDiagram::new(&th);
313        let [x, y, var] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
314        assert!(
315            diagram
316                .add_ob(&DiagramObDecl {
317                    name: "var".into(),
318                    id: var,
319                    ob_type: ObType::Basic("AttrType".into()),
320                    over: Some(Ob::Basic(attr_type.to_string()))
321                })
322                .is_ok()
323        );
324        let [a, b] = [Uuid::now_v7(), Uuid::now_v7()];
325        for (name, indiv, f) in [("x", x, a), ("y", y, b)] {
326            assert!(
327                diagram
328                    .add_ob(&DiagramObDecl {
329                        name: name.into(),
330                        id: indiv,
331                        ob_type: ObType::Basic("Entity".into()),
332                        over: Some(Ob::Basic(entity.to_string())),
333                    })
334                    .is_ok()
335            );
336            assert!(
337                diagram
338                    .add_mor(&DiagramMorDecl {
339                        name: "".into(),
340                        id: f,
341                        mor_type: MorType::Basic("Attr".into()),
342                        dom: Some(Ob::Basic(indiv.to_string())),
343                        cod: Some(Ob::Basic(var.to_string())),
344                        over: Some(Mor::Basic(attr.to_string())),
345                    })
346                    .is_ok()
347            );
348        }
349        assert_eq!(diagram.ob_generator_label(&var.into()), Some("var".into()));
350        assert_eq!(diagram.ob_generator_with_label(&"var".into()), NameLookup::Unique(var.into()));
351        assert_eq!(diagram.ob_generators().len(), 3);
352        assert_eq!(diagram.mor_generators().len(), 2);
353        assert_eq!(diagram.validate_in(&model).unwrap().0, JsResult::Ok(()));
354
355        let presentation = diagram.presentation();
356        assert_eq!(presentation.ob_generators.len(), 3);
357        assert_eq!(presentation.mor_generators.len(), 2);
358    }
359}
catlog_wasm/model_diagram.rs

catlog_wasm/
model_diagram.rs
