catlog/dbl/discrete/
model_diagram.rs

1//! Diagrams in models of a discrete double theory.
2
3use itertools::Either;
4use nonempty::NonEmpty;
5
6#[cfg(feature = "serde-wasm")]
7use tsify::declare;
8
9use crate::dbl::{model::*, model_diagram::*, model_morphism::*};
10use crate::one::{Category, FgCategory, GraphMapping};
11use crate::validate;
12use crate::zero::{Mapping, QualifiedName};
13
14/// A diagram in a model of a discrete double theory.
15pub type DiscreteDblModelDiagram = DblModelDiagram<DiscreteDblModelMapping, DiscreteDblModel>;
16
17/// A failure to be valid in a diagram in a model of a discrete double theory.
18#[cfg_attr(feature = "serde-wasm", declare)]
19pub type InvalidDiscreteDblModelDiagram =
20    InvalidDblModelDiagram<InvalidDblModel, InvalidDblModelMorphism<QualifiedName, QualifiedName>>;
21
22impl DiscreteDblModelDiagram {
23    /// Validates that the diagram is well-defined in the given model.
24    ///
25    /// Assumes that the model is valid. If it is not, this function may panic.
26    pub fn validate_in(
27        &self,
28        model: &DiscreteDblModel,
29    ) -> Result<(), NonEmpty<InvalidDiscreteDblModelDiagram>> {
30        validate::wrap_errors(self.iter_invalid_in(model))
31    }
32
33    /// Iterates over failures of the diagram to be valid in the given model.
34    pub fn iter_invalid_in<'a>(
35        &'a self,
36        model: &'a DiscreteDblModel,
37    ) -> impl Iterator<Item = InvalidDiscreteDblModelDiagram> + 'a {
38        let mut dom_errs = self.1.iter_invalid().peekable();
39        if dom_errs.peek().is_some() {
40            Either::Left(dom_errs.map(InvalidDblModelDiagram::Dom))
41        } else {
42            let morphism = DblModelMorphism(&self.0, &self.1, model);
43            Either::Right(morphism.iter_invalid().map(InvalidDblModelDiagram::Map))
44        }
45    }
46
47    /// Infer missing data in the diagram from the model, where possible.
48    ///
49    /// Assumes that the model is valid.
50    pub fn infer_missing_from(&mut self, model: &DiscreteDblModel) {
51        let (mapping, domain) = self.into();
52        domain.infer_missing();
53        for e in domain.mor_generators() {
54            let Some(g) = mapping.0.edge_map().apply_to_ref(&e) else {
55                continue;
56            };
57            if !model.has_mor(&g) {
58                continue;
59            }
60            if let Some(x) = domain.get_dom(&e).filter(|x| !mapping.0.is_vertex_assigned(x)) {
61                mapping.assign_ob(x.clone(), model.dom(&g));
62            }
63            if let Some(x) = domain.get_cod(&e).filter(|x| !mapping.0.is_vertex_assigned(x)) {
64                mapping.assign_ob(x.clone(), model.cod(&g));
65            }
66        }
67    }
68}
69
70#[cfg(test)]
71mod tests {
72    use std::rc::Rc;
73
74    use super::*;
75    use crate::stdlib::*;
76    use crate::{one::Path, zero::name};
77
78    #[test]
79    fn validate_model_diagram() {
80        let th = Rc::new(th_signed_category());
81        let pos_loop = positive_loop(th.clone());
82        let neg_loop = negative_loop(th.clone());
83
84        let mut f: DiscreteDblModelMapping = Default::default();
85        f.assign_ob(name("x"), name("x"));
86        f.assign_mor(name("loop"), Path::pair(name("loop"), name("loop")));
87        let diagram = DblModelDiagram(f, pos_loop);
88        assert!(diagram.validate_in(&neg_loop).is_ok());
89    }
90
91    #[test]
92    fn infer_model_diagram() {
93        let th = Rc::new(th_schema());
94        let mut domain = DiscreteDblModel::new(th.clone());
95        domain.add_mor(name("f"), name("x"), name("y"), name("Attr").into());
96        let mut f: DiscreteDblModelMapping = Default::default();
97        f.assign_mor(name("f"), Path::single(name("attr")));
98        let mut diagram = DblModelDiagram(f, domain);
99
100        let model = walking_attr(th);
101        diagram.infer_missing_from(&model);
102        assert!(diagram.validate_in(&model).is_ok());
103    }
104}
catlog/dbl/discrete/model_diagram.rs

catlog/dbl/discrete/
model_diagram.rs
