catlog/dbl/discrete/
model_diagram.rs

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

catlog/dbl/discrete/
model_diagram.rs
