catlog/dbl/discrete/
model.rs

1//! Models of discrete double theories.
2
3use std::rc::Rc;
4
5use derivative::Derivative;
6
7use super::theory::DiscreteDblTheory;
8use crate::dbl::{category::*, model::*, theory::DblTheory};
9use crate::one::{fp_category::QualifiedFpCategory, *};
10use crate::validate::{self, Validate};
11use crate::zero::pretty::*;
12use crate::zero::*;
13
14/// A finitely presented model of a discrete double theory.
15///
16/// Since discrete double theory has only identity operations, such a model is a
17/// finite presentation of a category sliced over the object and morphism types
18/// comprising the theory. A type theorist would call it a ["displayed
19/// category"](https://ncatlab.org/nlab/show/displayed+category).
20#[derive(Clone, Debug, Derivative)]
21#[derivative(PartialEq, Eq)]
22pub struct DiscreteDblModel {
23    #[derivative(PartialEq(compare_with = "Rc::ptr_eq"))]
24    theory: Rc<DiscreteDblTheory>,
25    pub(crate) category: QualifiedFpCategory,
26    ob_types: IndexedHashColumn<QualifiedName, QualifiedName>,
27    mor_types: IndexedHashColumn<QualifiedName, QualifiedPath>,
28}
29
30impl DiscreteDblModel {
31    /// Creates an empty model of the given theory.
32    pub fn new(theory: Rc<DiscreteDblTheory>) -> Self {
33        Self {
34            theory,
35            category: Default::default(),
36            ob_types: Default::default(),
37            mor_types: Default::default(),
38        }
39    }
40
41    /// Returns the underlying graph of the model.
42    pub fn generating_graph(&self) -> &impl FinGraph<V = QualifiedName, E = QualifiedName> {
43        self.category.generators()
44    }
45
46    /// Is the model freely generated?
47    pub fn is_free(&self) -> bool {
48        self.category.is_free()
49    }
50
51    /// Adds a path equation to the model.
52    pub fn add_equation(&mut self, eq: PathEq<QualifiedName, QualifiedName>) {
53        self.category.add_equation(eq);
54    }
55
56    /// Iterates over failures of model to be well defined.
57    pub fn iter_invalid(&self) -> impl Iterator<Item = InvalidDblModel> + '_ {
58        type Invalid = InvalidDblModel;
59        let category_errors = self.category.iter_invalid().map(|err| match err {
60            InvalidFpCategory::Dom(e) => Invalid::Dom(e),
61            InvalidFpCategory::Cod(e) => Invalid::Cod(e),
62            InvalidFpCategory::Eqn(eq, errs) => Invalid::Eqn(Some(eq), errs.map(|e| e.into())),
63        });
64        let ob_type_errors = self.category.ob_generators().filter_map(|x| {
65            if self.theory.has_ob_type(&self.ob_type(&x)) {
66                None
67            } else {
68                Some(Invalid::ObType(x))
69            }
70        });
71        let mor_type_errors = self.category.mor_generators().flat_map(|e| {
72            let mut errs = Vec::new();
73            let mor_type = self.mor_generator_type(&e);
74            if self.theory.has_mor_type(&mor_type) {
75                if self.category.get_dom(&e).is_some_and(|x| {
76                    self.has_ob(x) && self.ob_type(x) != self.theory.src(&mor_type)
77                }) {
78                    errs.push(Invalid::DomType(e.clone()));
79                }
80                if self.category.get_cod(&e).is_some_and(|x| {
81                    self.has_ob(x) && self.ob_type(x) != self.theory.tgt(&mor_type)
82                }) {
83                    errs.push(Invalid::CodType(e));
84                }
85            } else {
86                errs.push(Invalid::MorType(e));
87            }
88            errs.into_iter()
89        });
90        category_errors.chain(ob_type_errors).chain(mor_type_errors)
91    }
92
93    /// Infer missing data in the model, where possible.
94    ///
95    /// Objects used in the domain or codomain of morphisms, but not contained as
96    /// objects of the model, are added and their types are inferred. It is not
97    /// always possible to do this consistently, so it is important to `validate`
98    /// the model even after calling this method.
99    pub fn infer_missing(&mut self) {
100        let edges: Vec<_> = self.mor_generators().collect();
101        for e in edges {
102            if let Some(x) = self.get_dom(&e).filter(|x| !self.has_ob(x)) {
103                let ob_type = self.theory.src(&self.mor_generator_type(&e));
104                self.add_ob(x.clone(), ob_type);
105            }
106            if let Some(x) = self.get_cod(&e).filter(|x| !self.has_ob(x)) {
107                let ob_type = self.theory.tgt(&self.mor_generator_type(&e));
108                self.add_ob(x.clone(), ob_type);
109            }
110        }
111    }
112
113    /// Migrate model forward along a map between discrete double theories.
114    pub fn push_forward<F>(&mut self, f: &F, new_theory: Rc<DiscreteDblTheory>)
115    where
116        F: CategoryMap<
117                DomOb = QualifiedName,
118                DomMor = QualifiedPath,
119                CodOb = QualifiedName,
120                CodMor = QualifiedPath,
121            >,
122    {
123        self.ob_types = std::mem::take(&mut self.ob_types).postcompose(f.ob_map());
124        self.mor_types = std::mem::take(&mut self.mor_types).postcompose(f.mor_map());
125        self.theory = new_theory;
126    }
127}
128
129impl Category for DiscreteDblModel {
130    type Ob = QualifiedName;
131    type Mor = QualifiedPath;
132
133    fn has_ob(&self, x: &Self::Ob) -> bool {
134        self.category.has_ob(x)
135    }
136    fn has_mor(&self, m: &Self::Mor) -> bool {
137        self.category.has_mor(m)
138    }
139    fn dom(&self, m: &Self::Mor) -> Self::Ob {
140        self.category.dom(m)
141    }
142    fn cod(&self, m: &Self::Mor) -> Self::Ob {
143        self.category.cod(m)
144    }
145    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
146        self.category.compose(path)
147    }
148}
149
150impl FgCategory for DiscreteDblModel {
151    type ObGen = QualifiedName;
152    type MorGen = QualifiedName;
153
154    fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen> {
155        self.category.ob_generators()
156    }
157    fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen> {
158        self.category.mor_generators()
159    }
160    fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob {
161        self.category.mor_generator_dom(f)
162    }
163    fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob {
164        self.category.mor_generator_cod(f)
165    }
166}
167
168impl DblModel for DiscreteDblModel {
169    type ObType = QualifiedName;
170    type MorType = QualifiedPath;
171    type ObOp = QualifiedName;
172    type MorOp = Path<QualifiedName, QualifiedPath>;
173    type Theory = DiscreteDblTheory;
174
175    fn theory(&self) -> Rc<Self::Theory> {
176        self.theory.clone()
177    }
178
179    fn ob_act(&self, x: Self::Ob, _: &Self::ObOp) -> Self::Ob {
180        x
181    }
182    fn mor_act(&self, path: Path<Self::Ob, Self::Mor>, _: &Self::MorOp) -> Self::Mor {
183        path.flatten()
184    }
185
186    fn ob_type(&self, ob: &Self::Ob) -> Self::ObType {
187        self.ob_generator_type(ob)
188    }
189    fn mor_type(&self, mor: &Self::Mor) -> Self::MorType {
190        let types =
191            mor.clone().map(|x| self.ob_generator_type(&x), |m| self.mor_generator_type(&m));
192        self.theory.compose_types(types).expect("Morphism types should have composite")
193    }
194}
195
196impl FpDblModel for DiscreteDblModel {
197    fn ob_generator_type(&self, ob: &Self::ObGen) -> Self::ObType {
198        self.ob_types.apply_to_ref(ob).expect("Object should have type")
199    }
200    fn mor_generator_type(&self, mor: &Self::MorGen) -> Self::MorType {
201        self.mor_types.apply_to_ref(mor).expect("Morphism should have type")
202    }
203
204    fn ob_generators_with_type(&self, typ: &Self::ObType) -> impl Iterator<Item = Self::ObGen> {
205        self.ob_types.preimage(typ)
206    }
207    fn mor_generators_with_type(&self, typ: &Self::MorType) -> impl Iterator<Item = Self::MorGen> {
208        self.mor_types.preimage(typ)
209    }
210
211    fn equations(&self) -> impl Iterator<Item = (Self::Mor, Self::Mor)> {
212        self.category.equations().map(|PathEq { lhs, rhs }| (lhs.clone(), rhs.clone()))
213    }
214}
215
216impl MutDblModel for DiscreteDblModel {
217    fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) {
218        self.ob_types.set(x.clone(), ob_type);
219        self.category.add_ob_generator(x);
220    }
221
222    fn add_mor(&mut self, f: Self::MorGen, dom: Self::Ob, cod: Self::Ob, mor_type: Self::MorType) {
223        self.mor_types.set(f.clone(), mor_type);
224        self.category.add_mor_generator(f, dom, cod);
225    }
226
227    fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) {
228        self.mor_types.set(f.clone(), mor_type);
229        self.category.make_mor_generator(f);
230    }
231
232    fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
233        self.category.get_dom(f)
234    }
235    fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
236        self.category.get_cod(f)
237    }
238    fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) {
239        self.category.set_dom(f, x);
240    }
241    fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) {
242        self.category.set_cod(f, x);
243    }
244}
245
246impl PrintableDblModel for DiscreteDblModel {
247    fn ob_to_doc<'a>(&self, ob: &Self::Ob, ob_ns: &Namespace, _mor_ns: &Namespace) -> D<'a> {
248        t(ob_ns.label_string(ob))
249    }
250
251    fn mor_to_doc<'a>(&self, mor: &Self::Mor, ob_ns: &Namespace, mor_ns: &Namespace) -> D<'a> {
252        match mor {
253            Path::Id(ob) => unop(t("Id"), self.ob_to_doc(ob, ob_ns, mor_ns)),
254            Path::Seq(seq) => intersperse(seq.iter().map(|f| t(mor_ns.label_string(f))), t(" ⋅ ")),
255        }
256    }
257
258    fn ob_type_to_doc<'a>(ob_type: &Self::ObType) -> D<'a> {
259        ob_type.to_doc()
260    }
261
262    fn mor_type_to_doc<'a>(mor_type: &Self::MorType) -> D<'a> {
263        match mor_type {
264            Path::Id(ob_type) => unop(t("Hom"), Self::ob_type_to_doc(ob_type)),
265            Path::Seq(seq) => intersperse(seq.iter().map(|m| m.to_doc()), t(" ⊙ ")),
266        }
267    }
268}
269
270impl std::fmt::Display for DiscreteDblModel {
271    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
272        write!(f, "{}", DblModelPrinter::new().doc(self).pretty())
273    }
274}
275
276impl Validate for DiscreteDblModel {
277    type ValidationError = InvalidDblModel;
278
279    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
280        validate::wrap_errors(self.iter_invalid())
281    }
282}
283
284#[cfg(test)]
285mod tests {
286    use expect_test::expect;
287    use nonempty::nonempty;
288
289    use super::*;
290    use crate::stdlib::{models::*, theories::*, theory_morphisms::*};
291    use crate::{one::Path, zero::name};
292
293    #[test]
294    fn validate() {
295        let th = Rc::new(th_schema());
296        let mut model = DiscreteDblModel::new(th.clone());
297        model.add_ob(name("entity"), name("NotObType"));
298        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::ObType(name("entity"))]));
299
300        let mut model = DiscreteDblModel::new(th.clone());
301        model.add_ob(name("entity"), name("Entity"));
302        model.add_mor(name("map"), name("entity"), name("entity"), name("NotMorType").into());
303        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::MorType(name("map"))]));
304
305        let mut model = DiscreteDblModel::new(th);
306        model.add_ob(name("entity"), name("Entity"));
307        model.add_ob(name("type"), name("AttrType"));
308        model.add_mor(name("a"), name("entity"), name("type"), name("Attr").into());
309        assert!(model.validate().is_ok());
310        model.add_mor(name("b"), name("entity"), name("type"), Path::Id(name("Entity")));
311        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::CodType(name("b"))]));
312    }
313
314    #[test]
315    fn pretty_print() {
316        let model = walking_attr(Rc::new(th_schema()));
317        let expected = expect![[r#"
318            model generated by 2 objects and 1 morphism
319            entity : Entity
320            type : AttrType
321            attr : entity -> type : Attr"#]];
322        expected.assert_eq(&format!("{model}"));
323    }
324
325    #[test]
326    fn infer_missing() {
327        let th = Rc::new(th_schema());
328        let mut model = DiscreteDblModel::new(th.clone());
329        model.add_mor(name("attr"), name("entity"), name("type"), name("Attr").into());
330        model.infer_missing();
331        assert_eq!(model, walking_attr(th));
332    }
333
334    #[test]
335    fn pushforward_migrate() {
336        let th = Rc::new(th_category());
337        let mut model = DiscreteDblModel::new(th);
338        model.add_ob(name("x"), name("Object"));
339        model.add_mor(name("f"), name("x"), name("x"), Path::Id(name("Object")));
340
341        let functor_data = th_category_to_schema();
342        let new_th = Rc::new(th_schema());
343        model.push_forward(&functor_data.functor_into(&new_th.0), new_th.clone());
344        assert_eq!(model.ob_generator_type(&name("x")), name("Entity"));
345        assert_eq!(model.mor_generator_type(&name("f")), Path::Id(name("Entity")));
346    }
347}
catlog/dbl/discrete/model.rs

catlog/dbl/discrete/
model.rs
