catlog/dbl/discrete/
model.rs

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

catlog/dbl/discrete/
model.rs
