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 ustr::Ustr;
8use uuid::Uuid;
9use wasm_bindgen::prelude::*;
10
11use catlog::dbl::model::{FgDblModel, MutDblModel};
12use catlog::dbl::model_diagram as diagram;
13use catlog::one::FgCategory;
14use catlog::zero::MutMapping;
15use notebook_types::current::*;
16
17use super::model::{CanElaborate, CanQuote, Elaborator, Quoter};
18use super::model::{DblModel, DblModelBox, DiscreteDblModel};
19use super::model_morphism::DiscreteDblModelMapping;
20use super::result::JsResult;
21use super::theory::DblTheory;
22
23/// A box containing a diagram in a model of a double theory.
24#[derive(From)]
25pub enum DblModelDiagramBox {
26    Discrete(diagram::DblModelDiagram<DiscreteDblModelMapping, DiscreteDblModel>),
27    // DiscreteTab(), # TODO: Not implemented.
28}
29
30/// Wasm bindings for a diagram in a model of a double theory.
31#[wasm_bindgen]
32pub struct DblModelDiagram(#[wasm_bindgen(skip)] pub DblModelDiagramBox);
33
34impl DblModelDiagram {
35    /// Creates an empty diagram for the given theory.
36    pub fn new(theory: &DblTheory) -> Self {
37        let model = DblModel::new(theory);
38        Self(match model.0 {
39            DblModelBox::Discrete(model) => {
40                let mapping = Default::default();
41                diagram::DblModelDiagram(mapping, model).into()
42            }
43            DblModelBox::DiscreteTab(_) => {
44                panic!("Diagrams not implemented for tabulator theories")
45            }
46        })
47    }
48
49    /// Adds an object to the diagram.
50    pub fn add_ob(&mut self, decl: &DiagramObDecl) -> Result<(), String> {
51        all_the_same!(match &mut self.0 {
52            DblModelDiagramBox::[Discrete](diagram) => {
53                let (mapping, model) = diagram.into();
54                let ob_type: Ustr = Elaborator.elab(&decl.ob_type)?;
55                if let Some(over) = decl.over.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? {
56                    mapping.assign_ob(decl.id, over);
57                }
58                model.add_ob(decl.id, ob_type);
59                Ok(())
60            }
61        })
62    }
63
64    /// Adds a morphism to the diagram.
65    pub fn add_mor(&mut self, decl: &DiagramMorDecl) -> Result<(), String> {
66        all_the_same!(match &mut self.0 {
67            DblModelDiagramBox::[Discrete](diagram) => {
68                let (mapping, model) = diagram.into();
69                let mor_type = Elaborator.elab(&decl.mor_type)?;
70                model.make_mor(decl.id, mor_type);
71                if let Some(dom) = decl.dom.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? {
72                    model.set_dom(decl.id, dom);
73                }
74                if let Some(cod) = decl.cod.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? {
75                    model.set_cod(decl.id, cod);
76                }
77                if let Some(over) = decl.over.as_ref().map(|mor| Elaborator.elab(mor)).transpose()? {
78                    mapping.assign_mor(decl.id, over);
79                }
80                Ok(())
81            }
82        })
83    }
84}
85
86#[wasm_bindgen]
87impl DblModelDiagram {
88    /// Returns array of all basic objects in the diagram.
89    #[wasm_bindgen]
90    pub fn objects(&self) -> Vec<Ob> {
91        all_the_same!(match &self.0 {
92            DblModelDiagramBox::[Discrete](diagram) => {
93                let (_, model) = diagram.into();
94                model.objects().map(|x| Quoter.quote(&x)).collect()
95            }
96        })
97    }
98
99    /// Returns array of all basic morphisms in the diagram.
100    #[wasm_bindgen]
101    pub fn morphisms(&self) -> Vec<Mor> {
102        all_the_same!(match &self.0 {
103            DblModelDiagramBox::[Discrete](diagram) => {
104                let (_, model) = diagram.into();
105                model.morphisms().map(|f| Quoter.quote(&f)).collect()
106            }
107        })
108    }
109
110    /// Returns array of basic objects with the given type.
111    #[wasm_bindgen(js_name = "objectsWithType")]
112    pub fn objects_with_type(&self, ob_type: ObType) -> Result<Vec<Ob>, String> {
113        all_the_same!(match &self.0 {
114            DblModelDiagramBox::[Discrete](diagram) => {
115                let (_, model) = diagram.into();
116                let ob_type = Elaborator.elab(&ob_type)?;
117                Ok(model.objects_with_type(&ob_type).map(|x| Quoter.quote(&x)).collect())
118            }
119        })
120    }
121
122    /// Returns array of basic morphisms with the given type.
123    #[wasm_bindgen(js_name = "morphismsWithType")]
124    pub fn morphisms_with_type(&self, mor_type: MorType) -> Result<Vec<Mor>, String> {
125        all_the_same!(match &self.0 {
126            DblModelDiagramBox::[Discrete](diagram) => {
127                let (_, model) = diagram.into();
128                let mor_type = Elaborator.elab(&mor_type)?;
129                Ok(model.morphisms_with_type(&mor_type).map(|f| Quoter.quote(&f)).collect())
130            }
131        })
132    }
133
134    /// Returns array of declarations of basic objects.
135    #[wasm_bindgen(js_name = "objectDeclarations")]
136    pub fn object_declarations(&self) -> Vec<DiagramObDecl> {
137        all_the_same!(match &self.0 {
138            DblModelDiagramBox::[Discrete](diagram) => {
139                let (mapping, model) = diagram.into();
140                let decls = model.ob_generators().map(|x| {
141                    DiagramObDecl {
142                        name: "".into(),
143                        id: x,
144                        ob_type: Quoter.quote(&model.ob_generator_type(&x)),
145                        over: mapping.0.ob_generator_map.get(&x).map(|ob| Quoter.quote(ob))
146                    }
147                });
148                decls.collect()
149            }
150        })
151    }
152
153    /// Returns array of declarations of basic morphisms.
154    #[wasm_bindgen(js_name = "morphismDeclarations")]
155    pub fn morphism_declarations(&self) -> Vec<DiagramMorDecl> {
156        all_the_same!(match &self.0 {
157            DblModelDiagramBox::[Discrete](diagram) => {
158                let (mapping, model) = diagram.into();
159                let decls = model.mor_generators().map(|f| {
160                    DiagramMorDecl {
161                        name: "".into(),
162                        id: f,
163                        mor_type: Quoter.quote(&model.mor_generator_type(&f)),
164                        over: mapping.0.mor_generator_map.get(&f).map(|mor| Quoter.quote(mor)),
165                        dom: model.get_dom(&f).cloned().map(|ob| Quoter.quote(&ob)),
166                        cod: model.get_cod(&f).cloned().map(|ob| Quoter.quote(&ob)),
167                    }
168                });
169                decls.collect()
170            }
171        })
172    }
173
174    /// Infers missing data in the diagram from the model, where possible.
175    #[wasm_bindgen(js_name = "inferMissingFrom")]
176    pub fn infer_missing_from(&mut self, model: &DblModel) -> Result<(), String> {
177        all_the_same!(match &mut self.0 {
178            DblModelDiagramBox::[Discrete](diagram) => {
179                let model = (&model.0).try_into().map_err(
180                    |_| "Type of model should match type of diagram")?;
181                diagram.infer_missing_from(model);
182                Ok(())
183            }
184        })
185    }
186
187    /// Validates that the diagram is well defined in a model.
188    #[wasm_bindgen(js_name = "validateIn")]
189    pub fn validate_in(&self, model: &DblModel) -> Result<ModelDiagramValidationResult, String> {
190        all_the_same!(match &self.0 {
191            DblModelDiagramBox::[Discrete](diagram) => {
192                let model = (&model.0).try_into().map_err(
193                    |_| "Type of model should match type of diagram")?;
194                let res = diagram.validate_in(model);
195                Ok(ModelDiagramValidationResult(res.map_err(|errs| errs.into()).into()))
196            }
197        })
198    }
199}
200
201/// Result of validating a diagram in a model.
202#[derive(Serialize, Deserialize, Tsify)]
203#[tsify(into_wasm_abi, from_wasm_abi)]
204pub struct ModelDiagramValidationResult(
205    pub JsResult<(), Vec<diagram::InvalidDiscreteDblModelDiagram<Uuid>>>,
206);
207
208#[wasm_bindgen(js_name = "elaborateDiagram")]
209pub fn elaborate_diagram(doc: &DiagramDocumentContent, theory: &DblTheory) -> DblModelDiagram {
210    let mut diagram = DblModelDiagram::new(theory);
211    for cell in doc.notebook.cells.iter() {
212        if let Cell::Formal { id: _, content } = cell {
213            match content {
214                DiagramJudgment::Object(decl) => diagram.add_ob(decl).unwrap(),
215                DiagramJudgment::Morphism(decl) => diagram.add_mor(decl).unwrap(),
216            }
217        }
218    }
219    diagram
220}
221
222#[cfg(test)]
223mod tests {
224    use super::*;
225    use crate::model::tests::sch_walking_attr;
226    use crate::theories::*;
227
228    #[test]
229    fn diagram_schema() {
230        let th = ThSchema::new().theory();
231        let [attr, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
232        let model = sch_walking_attr(&th, [attr, entity, attr_type]);
233
234        let mut diagram = DblModelDiagram::new(&th);
235        let [x, y, var] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
236        assert!(
237            diagram
238                .add_ob(&DiagramObDecl {
239                    name: "var".into(),
240                    id: var,
241                    ob_type: ObType::Basic("AttrType".into()),
242                    over: Some(Ob::Basic(attr_type))
243                })
244                .is_ok()
245        );
246        for (name, indiv) in [("x", x), ("y", y)] {
247            assert!(
248                diagram
249                    .add_ob(&DiagramObDecl {
250                        name: name.into(),
251                        id: indiv,
252                        ob_type: ObType::Basic("Entity".into()),
253                        over: Some(Ob::Basic(entity)),
254                    })
255                    .is_ok()
256            );
257            assert!(
258                diagram
259                    .add_mor(&DiagramMorDecl {
260                        name: "".into(),
261                        id: Uuid::now_v7(),
262                        mor_type: MorType::Basic("Attr".into()),
263                        dom: Some(Ob::Basic(indiv)),
264                        cod: Some(Ob::Basic(var)),
265                        over: Some(Mor::Basic(attr)),
266                    })
267                    .is_ok()
268            );
269        }
270        assert_eq!(diagram.objects().len(), 3);
271        assert_eq!(diagram.object_declarations().len(), 3);
272        assert_eq!(diagram.morphisms().len(), 2);
273        assert_eq!(diagram.morphism_declarations().len(), 2);
274        assert_eq!(diagram.validate_in(&model).unwrap().0, JsResult::Ok(()));
275    }
276}
catlog_wasm/model_diagram.rs

catlog_wasm/
model_diagram.rs
