catlog/dbl/
model_diagram.rs

1/*! Diagrams in models of a double theory.
2
3A **diagram** in a [model](super::model) is simply a
4[morphism](super::model_morphism) into that model. This includes the domain of
5that morphism, which is assumed to be a free model.
6
7Diagrams are currently used primarily to represent instances of models from a
8fibered perspective, generalizing how a diagram in a category can be used to
9represent a copresheaf over that category.
10
11# References
12
13TODO: Document in devs docs and link here.
14 */
15
16use std::hash::Hash;
17
18use derive_more::Into;
19use either::Either;
20use nonempty::NonEmpty;
21
22#[cfg(feature = "serde")]
23use serde::{Deserialize, Serialize};
24#[cfg(feature = "serde-wasm")]
25use tsify_next::{Tsify, declare};
26
27use super::{model::*, model_morphism::*};
28use crate::one::{Category, FgCategory};
29use crate::validate;
30
31/** A diagram in a model of a double theory.
32
33This struct owns its data, namely, the domain of the diagram (a model) and the
34model [mapping](DblModelMapping) itself.
35*/
36#[derive(Clone, Into)]
37#[into(owned, ref, ref_mut)]
38pub struct DblModelDiagram<Map, Dom>(pub Map, pub Dom);
39
40impl<Map, Dom> DblModelDiagram<Map, Dom>
41where
42    Map: DblModelMapping,
43{
44    /// Gets an object indexed by the diagram.
45    pub fn ob(&self, i: &Map::DomOb) -> Map::CodOb {
46        self.0.apply_ob(i).expect("Diagram should be defined at object")
47    }
48
49    /// Gets a morphism indexed by the diagram.
50    pub fn mor(&self, h: &Map::DomMor) -> Map::CodMor {
51        self.0.apply_mor(h).expect("Diagram should be defined at morphism")
52    }
53}
54
55/// A failure of a diagram in a model to be valid.
56#[derive(Clone, Debug, PartialEq, Eq)]
57#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
58#[cfg_attr(feature = "serde", serde(tag = "tag", content = "err"))]
59#[cfg_attr(feature = "serde-wasm", derive(Tsify))]
60#[cfg_attr(feature = "serde-wasm", tsify(into_wasm_abi, from_wasm_abi))]
61pub enum InvalidDblModelDiagram<DomErr, MapErr> {
62    /// Domain of the diagram is invalid.
63    Dom(DomErr),
64
65    /// Mapping underlying the diagram is invalid.
66    Map(MapErr),
67}
68
69/// A diagram in a model of a discrete double theory.
70pub type DiscreteDblModelDiagram<DomId, CodId, Cat> =
71    DblModelDiagram<DiscreteDblModelMapping<DomId, CodId>, DiscreteDblModel<DomId, Cat>>;
72
73/// A failure to be valid in a diagram in a model of a discrete double theory.
74#[cfg_attr(feature = "serde-wasm", declare)]
75pub type InvalidDiscreteDblModelDiagram<DomId> =
76    InvalidDblModelDiagram<InvalidDblModel<DomId>, InvalidDblModelMorphism<DomId, DomId>>;
77
78impl<DomId, CodId, Cat> DiscreteDblModelDiagram<DomId, CodId, Cat>
79where
80    DomId: Eq + Clone + Hash,
81    CodId: Eq + Clone + Hash,
82    Cat: FgCategory,
83    Cat::Ob: Hash,
84    Cat::Mor: Hash,
85{
86    /** Validates that the diagram is well-defined in the given model.
87
88    Assumes that the model is valid. If it is not, this function may panic.
89     */
90    pub fn validate_in(
91        &self,
92        model: &DiscreteDblModel<CodId, Cat>,
93    ) -> Result<(), NonEmpty<InvalidDiscreteDblModelDiagram<DomId>>> {
94        validate::wrap_errors(self.iter_invalid_in(model))
95    }
96
97    /// Iterates over failures of the diagram to be valid in the given model.
98    pub fn iter_invalid_in<'a>(
99        &'a self,
100        model: &'a DiscreteDblModel<CodId, Cat>,
101    ) -> impl Iterator<Item = InvalidDiscreteDblModelDiagram<DomId>> + 'a {
102        let mut dom_errs = self.1.iter_invalid().peekable();
103        if dom_errs.peek().is_some() {
104            Either::Left(dom_errs.map(InvalidDblModelDiagram::Dom))
105        } else {
106            let morphism = DblModelMorphism(&self.0, &self.1, model);
107            Either::Right(morphism.iter_invalid().map(InvalidDblModelDiagram::Map))
108        }
109    }
110
111    /** Infer missing data in the diagram from the model, where possible.
112
113    Assumes that the model is valid.
114     */
115    pub fn infer_missing_from(&mut self, model: &DiscreteDblModel<CodId, Cat>) {
116        let (mapping, domain) = self.into();
117        domain.infer_missing();
118        for e in domain.mor_generators() {
119            let Some(g) = mapping.apply_basic_mor(&e) else {
120                continue;
121            };
122            if !model.has_mor(&g) {
123                continue;
124            }
125            if let Some(x) = domain.get_dom(&e).filter(|x| !mapping.is_ob_assigned(x)) {
126                mapping.assign_ob(x.clone(), model.dom(&g));
127            }
128            if let Some(x) = domain.get_cod(&e).filter(|x| !mapping.is_ob_assigned(x)) {
129                mapping.assign_ob(x.clone(), model.cod(&g));
130            }
131        }
132    }
133}
134
135#[cfg(test)]
136mod tests {
137    use super::*;
138
139    use std::sync::Arc;
140    use ustr::ustr;
141
142    use crate::one::{Path, fin_category::FinMor};
143    use crate::stdlib::*;
144
145    #[test]
146    fn discrete_model_diagram() {
147        let th = Arc::new(th_schema());
148        let mut model = DiscreteDblModel::new(th.clone());
149        let entity = ustr("entity");
150        model.add_ob(entity, ustr("Entity"));
151        model.add_ob(ustr("type"), ustr("AttrType"));
152        model.add_mor(ustr("attr"), entity, ustr("type"), FinMor::Generator(ustr("Attr")));
153
154        let mut f: DiscreteDblModelMapping<_, _> = Default::default();
155        f.assign_ob(entity, 'x');
156        f.assign_ob(ustr("type"), 'y');
157        f.assign_basic_mor(ustr("attr"), Path::pair('p', 'q'));
158
159        let diagram = DblModelDiagram(f, model);
160        assert_eq!(diagram.ob(&entity), 'x');
161        assert_eq!(diagram.mor(&Path::single(ustr("attr"))), Path::pair('p', 'q'));
162    }
163
164    #[test]
165    fn validate_model_diagram() {
166        let th = Arc::new(th_signed_category());
167        let pos_loop = positive_loop(th.clone());
168        let neg_loop = negative_loop(th.clone());
169
170        let mut f: DiscreteDblModelMapping<_, _> = Default::default();
171        f.assign_ob(ustr("x"), ustr("x"));
172        f.assign_basic_mor(ustr("loop"), Path::pair(ustr("loop"), ustr("loop")));
173        let diagram = DblModelDiagram(f, pos_loop);
174        assert!(diagram.validate_in(&neg_loop).is_ok());
175    }
176
177    #[test]
178    fn infer_model_diagram() {
179        let th = Arc::new(th_schema());
180        let mut domain = DiscreteDblModel::new(th.clone());
181        domain.add_mor(0, 0, 1, FinMor::Generator(ustr("Attr")));
182        let mut f: DiscreteDblModelMapping<_, _> = Default::default();
183        f.assign_basic_mor(0, Path::single(ustr("attr")));
184        let mut diagram = DblModelDiagram(f, domain);
185
186        let model = walking_attr(th);
187        diagram.infer_missing_from(&model);
188        assert!(diagram.validate_in(&model).is_ok());
189    }
190}
catlog/dbl/model_diagram.rs

catlog/dbl/
model_diagram.rs
