catlog/dbl/
model.rs

1/*! Models of double theories.
2
3A model of a double theory is a category (or categories) equipped with
4operations specified by the theory, categorifying the familiar idea from logic
5that a model of a theory is a set (or sets) equipped with operations. For
6background on double theories, see the [`theory`](super::theory) module.
7
8In the case of a *simple* double theory, which amounts to a small double
9category, a **model** of the theory is a span-valued *lax* double functor out of
10the theory. Such a model is a "lax copresheaf," categorifying the notion of a
11copresheaf or set-valued functor. Though they are "just" lax double functors,
12models come with extra intuitions. To bring that out we introduce new jargon,
13building on that for double theories.
14
15# Terminology
16
17A model of a double theory consists of elements of two kinds:
18
191. **Objects**, each assigned an object type in the theory;
20
212. **Morphisms**, each having a domain and a codomain object and assigned a
22   morphism type in the theory, compatibly with the domain and codomain types;
23
24In addition, a model has the following operations:
25
26- **Object action**: object operations in the theory act on objects in the model
27  to produce new objects;
28
29- **Morphism action**: morphism operations in the theory act on morphisms in
30  the model to produce new morphisms, compatibly with the object action;
31
32- **Composition**: a path of morphisms in the model has a composite morphism,
33  whose type is the composite of the corresponding morphism types.
34 */
35
36use std::hash::{BuildHasher, BuildHasherDefault, Hash, RandomState};
37use std::iter::Iterator;
38use std::sync::Arc;
39
40use derivative::Derivative;
41use ustr::{IdentityHasher, Ustr};
42
43#[cfg(feature = "serde")]
44use serde::{Deserialize, Serialize};
45#[cfg(feature = "serde-wasm")]
46use tsify_next::Tsify;
47
48use super::category::VDblCategory;
49use super::theory::{DblTheory, DiscreteDblTheory};
50use crate::one::fin_category::{FpCategory, InvalidFpCategory, UstrFinCategory};
51use crate::one::*;
52use crate::validate::{self, Validate};
53use crate::zero::*;
54
55use super::theory::*;
56
57/** A model of a double theory.
58
59As always in logic, a model makes sense only relative to a theory, but a theory
60can have many different models. So, in Rust, a model needs access to its theory
61but should not *own* its theory. Implementors of this trait might use an
62immutable shared reference to the theory.
63
64Objects and morphisms in a model are typed by object types and morphism types in
65the theory. There is a design choice about whether identifiers for objects
66([`Ob`](Category::Ob)) and morphisms ([`Mor`](Category::Mor)) are unique
67relative to their types or globally within the model. If we took the first
68approach (as we do in the Julia package
69[ACSets.jl](https://github.com/AlgebraicJulia/ACSets.jl)), one could only make
70sense of objects and morphisms when their types are known, so the early methods
71in the trait would look like this:
72
73```ignore
74fn has_ob(&self, x: &Self::Ob, t: &Self::ObType) -> bool;
75fn has_mor(&self, m: &Self::Mor, t: &Self::MorType) -> bool;
76fn dom(&self, m: &Self::Mor, t: &Self::MorType) -> Self::Ob;
77fn cod(&self, m: &Self::Mor, t: &Self::MorType) -> Self::Ob;
78```
79
80It will be more convenient for us to take the second approach since in our usage
81object and morphism identifiers will be globally unique in a very strong sense
82(something like UUIDs).
83 */
84pub trait DblModel: Category {
85    /// Rust type of object types defined in the theory.
86    type ObType: Eq;
87
88    /// Rust type of morphism types defined in the theory.
89    type MorType: Eq;
90
91    /// Type of operations on objects defined in the theory.
92    type ObOp: Eq;
93
94    /// Type of operations on morphisms defined in the theory.
95    type MorOp: Eq;
96
97    /// The type of double theory that this is a model of.
98    type Theory: DblTheory<
99            ObType = Self::ObType,
100            MorType = Self::MorType,
101            ObOp = Self::ObOp,
102            MorOp = Self::MorOp,
103        >;
104
105    /// The double theory that this model is a model of.
106    fn theory(&self) -> &Self::Theory;
107
108    /// Type of an object.
109    fn ob_type(&self, x: &Self::Ob) -> Self::ObType;
110
111    /// Type of a morphism.
112    fn mor_type(&self, m: &Self::Mor) -> Self::MorType;
113
114    /// Acts on an object with an object operation.
115    fn ob_act(&self, x: Self::Ob, f: &Self::ObOp) -> Self::Ob;
116
117    /// Acts on a morphism with a morphism operation.
118    fn mor_act(&self, m: Self::Mor, α: &Self::MorOp) -> Self::Mor;
119}
120
121/// A finitely generated model of a double theory.
122pub trait FgDblModel: DblModel + FgCategory {
123    /// Type of an object generator.
124    fn ob_generator_type(&self, ob: &Self::ObGen) -> Self::ObType;
125
126    /// Type of a morphism generator.
127    fn mor_generator_type(&self, mor: &Self::MorGen) -> Self::MorType;
128
129    /// Iterates over object generators with the given object type.
130    fn ob_generators_with_type(&self, obtype: &Self::ObType) -> impl Iterator<Item = Self::ObGen> {
131        self.ob_generators().filter(|ob| self.ob_generator_type(ob) == *obtype)
132    }
133
134    /// Iterates over morphism generators with the given morphism type.
135    fn mor_generators_with_type(
136        &self,
137        mortype: &Self::MorType,
138    ) -> impl Iterator<Item = Self::MorGen> {
139        self.mor_generators().filter(|mor| self.mor_generator_type(mor) == *mortype)
140    }
141
142    /// Iterators over basic objects with the given object type.
143    fn objects_with_type(&self, obtype: &Self::ObType) -> impl Iterator<Item = Self::Ob> {
144        self.ob_generators_with_type(obtype).map(|ob_gen| ob_gen.into())
145    }
146
147    /// Iterates over basic morphisms with the given morphism type.
148    fn morphisms_with_type(&self, mortype: &Self::MorType) -> impl Iterator<Item = Self::Mor> {
149        self.mor_generators_with_type(mortype).map(|mor_gen| mor_gen.into())
150    }
151}
152
153/// A mutable, finitely generated model of a double theory.
154pub trait MutDblModel: FgDblModel {
155    /// Adds a basic object to the model.
156    fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) -> bool;
157
158    /// Adds a basic morphism to the model.
159    fn add_mor(
160        &mut self,
161        f: Self::MorGen,
162        dom: Self::Ob,
163        cod: Self::Ob,
164        mor_type: Self::MorType,
165    ) -> bool {
166        let is_new = self.make_mor(f.clone(), mor_type);
167        self.set_dom(f.clone(), dom);
168        self.set_cod(f, cod);
169        is_new
170    }
171
172    /// Adds a basic morphism to the model without setting its (co)domain.
173    fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) -> bool;
174
175    /// Gets the domain of a basic morphism, if it is set.
176    fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob>;
177
178    /// Gets the codomain of a basic morphism, if it is set.
179    fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob>;
180
181    /// Sets the domain of a basic morphism.
182    fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) -> Option<Self::Ob>;
183
184    /// Sets the codomain of a basic morphism.
185    fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) -> Option<Self::Ob>;
186}
187
188/** A finitely presented model of a discrete double theory.
189
190Since discrete double theory has only identity operations, such a model is a
191finite presentation of a category sliced over the object and morphism types
192comprising the theory. A type theorist would call it a ["displayed
193category"](https://ncatlab.org/nlab/show/displayed+category).
194*/
195#[derive(Clone, Derivative, Debug)]
196#[derivative(PartialEq(bound = "Id: Eq + Hash"))]
197#[derivative(Eq(bound = "Id: Eq + Hash"))]
198pub struct DiscreteDblModel<Id, Cat: FgCategory> {
199    #[derivative(PartialEq(compare_with = "Arc::ptr_eq"))]
200    theory: Arc<DiscreteDblTheory<Cat>>,
201    category: FpCategory<Id, Id, Id>,
202    ob_types: IndexedHashColumn<Id, Cat::Ob>,
203    mor_types: IndexedHashColumn<Id, Cat::Mor>,
204}
205
206/// A model of a discrete double theory where both theoy and model have keys of
207/// type `Ustr`.
208pub type UstrDiscreteDblModel = DiscreteDblModel<Ustr, UstrFinCategory>;
209// NOTE: We are leaving a small optimization on the table by not using the
210// `IdentityHasher` but adding that extra type parameter quickly gets annoying
211// because it has to be propagated everywhere, including into model morphisms.
212
213impl<Id, Cat> DiscreteDblModel<Id, Cat>
214where
215    Id: Eq + Clone + Hash,
216    Cat: FgCategory,
217    Cat::Ob: Hash,
218    Cat::Mor: Hash,
219{
220    /// Creates an empty model of the given theory.
221    pub fn new(theory: Arc<DiscreteDblTheory<Cat>>) -> Self {
222        Self {
223            theory,
224            category: Default::default(),
225            ob_types: Default::default(),
226            mor_types: Default::default(),
227        }
228    }
229
230    /// Returns a reference-counting pointer to the theory for this model.
231    pub fn theory_arc(&self) -> Arc<DiscreteDblTheory<Cat>> {
232        self.theory.clone()
233    }
234
235    /// Returns the underlying graph of the model.
236    pub fn generating_graph(&self) -> &(impl FinGraph<V = Id, E = Id> + use<Id, Cat>) {
237        self.category.generators()
238    }
239
240    /// Is the model freely generated?
241    pub fn is_free(&self) -> bool {
242        self.category.is_free()
243    }
244
245    /// Adds an equation to the model, making it not free.
246    pub fn add_equation(&mut self, key: Id, eq: PathEq<Id, Id>) {
247        self.category.add_equation(key, eq);
248    }
249
250    /// Iterates over failures of model to be well defined.
251    pub fn iter_invalid(&self) -> impl Iterator<Item = InvalidDblModel<Id>> + '_ {
252        type Invalid<Id> = InvalidDblModel<Id>;
253        let category_errors = self.category.iter_invalid().map(|err| match err {
254            InvalidFpCategory::Dom(e) => Invalid::Dom(e),
255            InvalidFpCategory::Cod(e) => Invalid::Cod(e),
256            InvalidFpCategory::EqLhs(eq) => Invalid::EqLhs(eq),
257            InvalidFpCategory::EqRhs(eq) => Invalid::EqRhs(eq),
258            InvalidFpCategory::EqSrc(eq) => Invalid::EqSrc(eq),
259            InvalidFpCategory::EqTgt(eq) => Invalid::EqTgt(eq),
260        });
261        let ob_type_errors = self.category.ob_generators().filter_map(|x| {
262            if self.theory.has_ob_type(&self.ob_type(&x)) {
263                None
264            } else {
265                Some(Invalid::ObType(x))
266            }
267        });
268        let mor_type_errors = self.category.mor_generators().flat_map(|e| {
269            let mut errs = Vec::new();
270            let mor_type = self.mor_generator_type(&e);
271            if self.theory.has_mor_type(&mor_type) {
272                if self.category.get_dom(&e).is_some_and(|x| {
273                    self.has_ob(x) && self.ob_type(x) != self.theory.src(&mor_type)
274                }) {
275                    errs.push(Invalid::DomType(e.clone()));
276                }
277                if self.category.get_cod(&e).is_some_and(|x| {
278                    self.has_ob(x) && self.ob_type(x) != self.theory.tgt(&mor_type)
279                }) {
280                    errs.push(Invalid::CodType(e));
281                }
282            } else {
283                errs.push(Invalid::MorType(e));
284            }
285            errs.into_iter()
286        });
287        category_errors.chain(ob_type_errors).chain(mor_type_errors)
288    }
289
290    /** Infer missing data in the model, where possible.
291
292    Objects used in the domain or codomain of morphisms, but not contained as
293    objects of the model, are added and their types are inferred. It is not
294    always possible to do this consistently, so it is important to `validate`
295    the model even after calling this method.
296    */
297    pub fn infer_missing(&mut self) {
298        let edges: Vec<_> = self.mor_generators().collect();
299        for e in edges {
300            if let Some(x) = self.get_dom(&e).filter(|x| !self.has_ob(x)) {
301                let ob_type = self.theory.src(&self.mor_generator_type(&e));
302                self.add_ob(x.clone(), ob_type);
303            }
304            if let Some(x) = self.get_cod(&e).filter(|x| !self.has_ob(x)) {
305                let ob_type = self.theory.tgt(&self.mor_generator_type(&e));
306                self.add_ob(x.clone(), ob_type);
307            }
308        }
309    }
310}
311
312impl<Id, Cat> Category for DiscreteDblModel<Id, Cat>
313where
314    Id: Eq + Clone + Hash,
315    Cat: FgCategory,
316    Cat::Ob: Hash,
317    Cat::Mor: Hash,
318{
319    type Ob = Id;
320    type Mor = Path<Id, Id>;
321
322    fn has_ob(&self, x: &Self::Ob) -> bool {
323        self.category.has_ob(x)
324    }
325    fn has_mor(&self, m: &Self::Mor) -> bool {
326        self.category.has_mor(m)
327    }
328    fn dom(&self, m: &Self::Mor) -> Self::Ob {
329        self.category.dom(m)
330    }
331    fn cod(&self, m: &Self::Mor) -> Self::Ob {
332        self.category.cod(m)
333    }
334    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
335        self.category.compose(path)
336    }
337}
338
339impl<Id, Cat> FgCategory for DiscreteDblModel<Id, Cat>
340where
341    Id: Eq + Clone + Hash,
342    Cat: FgCategory,
343    Cat::Ob: Hash,
344    Cat::Mor: Hash,
345{
346    type ObGen = Id;
347    type MorGen = Id;
348
349    fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen> {
350        self.category.ob_generators()
351    }
352
353    fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen> {
354        self.category.mor_generators()
355    }
356
357    fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob {
358        self.category.mor_generator_dom(f)
359    }
360
361    fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob {
362        self.category.mor_generator_cod(f)
363    }
364}
365
366impl<Id, Cat> DblModel for DiscreteDblModel<Id, Cat>
367where
368    Id: Eq + Clone + Hash,
369    Cat: FgCategory,
370    Cat::Ob: Hash,
371    Cat::Mor: Hash,
372{
373    type ObType = Cat::Ob;
374    type MorType = Cat::Mor;
375    type ObOp = Cat::Ob;
376    type MorOp = Path<Cat::Ob, Cat::Mor>;
377    type Theory = DiscreteDblTheory<Cat>;
378
379    fn theory(&self) -> &Self::Theory {
380        &self.theory
381    }
382
383    fn ob_act(&self, x: Self::Ob, _: &Self::ObOp) -> Self::Ob {
384        x
385    }
386    fn mor_act(&self, m: Self::Mor, _: &Self::MorOp) -> Self::Mor {
387        m
388    }
389
390    fn ob_type(&self, ob: &Self::Ob) -> Self::ObType {
391        self.ob_generator_type(ob)
392    }
393    fn mor_type(&self, mor: &Self::Mor) -> Self::MorType {
394        let types =
395            mor.clone().map(|x| self.ob_generator_type(&x), |m| self.mor_generator_type(&m));
396        self.theory.compose_types(types).expect("Morphism types should have composite")
397    }
398}
399
400impl<Id, Cat> FgDblModel for DiscreteDblModel<Id, Cat>
401where
402    Id: Eq + Clone + Hash,
403    Cat: FgCategory,
404    Cat::Ob: Hash,
405    Cat::Mor: Hash,
406{
407    fn ob_generator_type(&self, ob: &Self::ObGen) -> Self::ObType {
408        self.ob_types.apply(ob).expect("Object should have type")
409    }
410    fn mor_generator_type(&self, mor: &Self::MorGen) -> Self::MorType {
411        self.mor_types.apply(mor).expect("Morphism should have type")
412    }
413
414    fn ob_generators_with_type(&self, typ: &Self::ObType) -> impl Iterator<Item = Self::ObGen> {
415        self.ob_types.preimage(typ)
416    }
417    fn mor_generators_with_type(&self, typ: &Self::MorType) -> impl Iterator<Item = Self::MorGen> {
418        self.mor_types.preimage(typ)
419    }
420}
421
422impl<Id, Cat> MutDblModel for DiscreteDblModel<Id, Cat>
423where
424    Id: Eq + Clone + Hash,
425    Cat: FgCategory,
426    Cat::Ob: Hash,
427    Cat::Mor: Hash,
428{
429    fn add_ob(&mut self, x: Id, typ: Cat::Ob) -> bool {
430        self.ob_types.set(x.clone(), typ);
431        self.category.add_ob_generator(x)
432    }
433
434    fn add_mor(&mut self, f: Id, dom: Id, cod: Id, typ: Cat::Mor) -> bool {
435        self.mor_types.set(f.clone(), typ);
436        self.category.add_mor_generator(f, dom, cod)
437    }
438
439    fn make_mor(&mut self, f: Id, typ: Cat::Mor) -> bool {
440        self.mor_types.set(f.clone(), typ);
441        self.category.make_mor_generator(f)
442    }
443
444    fn get_dom(&self, f: &Id) -> Option<&Id> {
445        self.category.get_dom(f)
446    }
447    fn get_cod(&self, f: &Id) -> Option<&Id> {
448        self.category.get_cod(f)
449    }
450    fn set_dom(&mut self, f: Id, x: Id) -> Option<Id> {
451        self.category.set_dom(f, x)
452    }
453    fn set_cod(&mut self, f: Id, x: Id) -> Option<Id> {
454        self.category.set_cod(f, x)
455    }
456}
457
458impl<Id, Cat> Validate for DiscreteDblModel<Id, Cat>
459where
460    Id: Eq + Clone + Hash,
461    Cat: FgCategory,
462    Cat::Ob: Hash,
463    Cat::Mor: Hash,
464{
465    type ValidationError = InvalidDblModel<Id>;
466
467    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
468        validate::wrap_errors(self.iter_invalid())
469    }
470}
471
472/** A failure of a model of a double theory to be well defined.
473
474We currently are encompassing error variants for all kinds of double theories in
475a single enum. That will likely become unviable but it's convenient for now.
476
477TODO: We are missing the case that an equation has different composite morphism
478types on left and right hand sides.
479*/
480#[derive(Clone, Debug, PartialEq, Eq)]
481#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
482#[cfg_attr(feature = "serde", serde(tag = "tag", content = "content"))]
483#[cfg_attr(feature = "serde-wasm", derive(Tsify))]
484#[cfg_attr(feature = "serde-wasm", tsify(into_wasm_abi, from_wasm_abi))]
485pub enum InvalidDblModel<Id> {
486    /// Domain of basic morphism is undefined or invalid.
487    Dom(Id),
488
489    /// Codomain of basic morphism is missing or invalid.
490    Cod(Id),
491
492    /// Basic object has invalid object type.
493    ObType(Id),
494
495    /// Basic morphism has invalid morphism type.
496    MorType(Id),
497
498    /// Domain of basic morphism has type incompatible with morphism type.
499    DomType(Id),
500
501    /// Codomain of basic morphism has type incompatible with morphism type.
502    CodType(Id),
503
504    /// Equation has left hand side that is not a well defined path.
505    EqLhs(Id),
506
507    /// Equation has right hand side that is not a well defined path.
508    EqRhs(Id),
509
510    /// Equation has different sources on left and right hand sides.
511    EqSrc(Id),
512
513    /// Equation has different sources on left and right hand sides.
514    EqTgt(Id),
515}
516
517/// Object in a model of a discrete tabulator theory.
518#[derive(Clone, PartialEq, Eq)]
519pub enum TabOb<V, E> {
520    /// Basic or generating object.
521    Basic(V),
522
523    /// A morphism viewed as an object of a tabulator.
524    Tabulated(Box<TabMor<V, E>>),
525}
526
527impl<V, E> From<V> for TabOb<V, E> {
528    fn from(value: V) -> Self {
529        TabOb::Basic(value)
530    }
531}
532
533impl<V, E> TabOb<V, E> {
534    /// Extracts a basic object or nothing.
535    pub fn basic(self) -> Option<V> {
536        match self {
537            TabOb::Basic(v) => Some(v),
538            _ => None,
539        }
540    }
541
542    /// Extracts a tabulated morphism or nothing.
543    pub fn tabulated(self) -> Option<TabMor<V, E>> {
544        match self {
545            TabOb::Tabulated(mor) => Some(*mor),
546            _ => None,
547        }
548    }
549
550    /// Unwraps a basic object, or panics.
551    pub fn unwrap_basic(self) -> V {
552        self.basic().expect("Object should be a basic object")
553    }
554
555    /// Unwraps a tabulated morphism, or panics.
556    pub fn unwrap_tabulated(self) -> TabMor<V, E> {
557        self.tabulated().expect("Object should be a tabulated morphism")
558    }
559}
560
561/** "Edge" in a model of a discrete tabulator theory.
562
563Morphisms of these two forms generate all the morphisms in the model.
564 */
565#[derive(Clone, PartialEq, Eq)]
566pub enum TabEdge<V, E> {
567    /// Basic morphism between any two objects.
568    Basic(E),
569
570    /// Generating morphism between tabulated morphisms, a commutative square.
571    Square {
572        /// The domain, a tabulated morphism.
573        dom: Box<TabMor<V, E>>,
574
575        /// The codomain, a tabulated morphism.
576        cod: Box<TabMor<V, E>>,
577
578        /// Edge that acts by pre-composition onto codomain.
579        pre: Box<TabEdge<V, E>>,
580
581        /// Edge that acts by post-composition onto domain.
582        post: Box<TabEdge<V, E>>,
583    },
584}
585
586impl<V, E> From<E> for TabEdge<V, E> {
587    fn from(value: E) -> Self {
588        TabEdge::Basic(value)
589    }
590}
591
592/// Morphism in a model of a discrete tabulator theory.
593pub type TabMor<V, E> = Path<TabOb<V, E>, TabEdge<V, E>>;
594
595impl<V, E> From<E> for TabMor<V, E> {
596    fn from(value: E) -> Self {
597        Path::single(value.into())
598    }
599}
600
601#[derive(Clone, Derivative)]
602#[derivative(Default(bound = ""))]
603#[derivative(PartialEq(bound = "V: Eq + Hash, E: Eq + Hash"))]
604#[derivative(Eq(bound = "V: Eq + Hash, E: Eq + Hash"))]
605struct DiscreteTabGenerators<V, E> {
606    objects: HashFinSet<V>,
607    morphisms: HashFinSet<E>,
608    dom: HashColumn<E, TabOb<V, E>>,
609    cod: HashColumn<E, TabOb<V, E>>,
610}
611
612impl<V, E> Graph for DiscreteTabGenerators<V, E>
613where
614    V: Eq + Clone + Hash,
615    E: Eq + Clone + Hash,
616{
617    type V = TabOb<V, E>;
618    type E = TabEdge<V, E>;
619
620    fn has_vertex(&self, ob: &Self::V) -> bool {
621        match ob {
622            TabOb::Basic(v) => self.objects.contains(v),
623            TabOb::Tabulated(p) => (*p).contained_in(self),
624        }
625    }
626
627    fn has_edge(&self, edge: &Self::E) -> bool {
628        match edge {
629            TabEdge::Basic(e) => {
630                self.morphisms.contains(e) && self.dom.is_set(e) && self.cod.is_set(e)
631            }
632            TabEdge::Square {
633                dom,
634                cod,
635                pre,
636                post,
637            } => {
638                if !(dom.contained_in(self) && cod.contained_in(self)) {
639                    return false;
640                }
641                let path1 = dom.clone().concat_in(self, Path::single(*post.clone()));
642                let path2 = Path::single(*pre.clone()).concat_in(self, *cod.clone());
643                path1.is_some() && path2.is_some() && path1 == path2
644            }
645        }
646    }
647
648    fn src(&self, edge: &Self::E) -> Self::V {
649        match edge {
650            TabEdge::Basic(e) => self.dom.apply(e).expect("Domain of morphism should be defined"),
651            TabEdge::Square { dom, .. } => TabOb::Tabulated(dom.clone()),
652        }
653    }
654
655    fn tgt(&self, edge: &Self::E) -> Self::V {
656        match edge {
657            TabEdge::Basic(e) => self.cod.apply(e).expect("Codomain of morphism should be defined"),
658            TabEdge::Square { cod, .. } => TabOb::Tabulated(cod.clone()),
659        }
660    }
661}
662
663/** A finitely presented model of a discrete tabulator theory.
664
665A **model** of a [discrete tabulator theory](super::theory::DiscreteTabTheory)
666is a normal lax functor from the theory into the double category of profunctors
667that preserves tabulators. For the definition of "preserving tabulators," see
668the dev docs.
669 */
670#[derive(Clone, Derivative)]
671#[derivative(PartialEq(bound = "Id: Eq + Hash, ThId: Eq + Hash"))]
672#[derivative(Eq(bound = "Id: Eq + Hash, ThId: Eq + Hash"))]
673pub struct DiscreteTabModel<Id, ThId, S = RandomState> {
674    #[derivative(PartialEq(compare_with = "Arc::ptr_eq"))]
675    theory: Arc<DiscreteTabTheory<ThId, ThId, S>>,
676    generators: DiscreteTabGenerators<Id, Id>,
677    // TODO: Equations
678    ob_types: IndexedHashColumn<Id, TabObType<ThId, ThId>>,
679    mor_types: IndexedHashColumn<Id, TabMorType<ThId, ThId>>,
680}
681
682/// A model of a discrete tabulator theory where both theory and model have keys
683/// of type `Ustr`.
684pub type UstrDiscreteTabModel = DiscreteTabModel<Ustr, Ustr, BuildHasherDefault<IdentityHasher>>;
685
686impl<Id, ThId, S> DiscreteTabModel<Id, ThId, S>
687where
688    Id: Eq + Clone + Hash,
689    ThId: Eq + Clone + Hash,
690    S: BuildHasher,
691{
692    /// Creates an empty model of the given theory.
693    pub fn new(theory: Arc<DiscreteTabTheory<ThId, ThId, S>>) -> Self {
694        Self {
695            theory,
696            generators: Default::default(),
697            ob_types: Default::default(),
698            mor_types: Default::default(),
699        }
700    }
701
702    /// Convenience method to turn a morphism into an object.
703    pub fn tabulated(&self, mor: TabMor<Id, Id>) -> TabOb<Id, Id> {
704        TabOb::Tabulated(Box::new(mor))
705    }
706
707    /// Convenience method to turn a morphism generator into an object.
708    pub fn tabulated_gen(&self, f: Id) -> TabOb<Id, Id> {
709        self.tabulated(Path::single(TabEdge::Basic(f)))
710    }
711
712    /// Iterates over failures of model to be well defined.
713    pub fn iter_invalid(&self) -> impl Iterator<Item = InvalidDblModel<Id>> + '_ {
714        type Invalid<Id> = InvalidDblModel<Id>;
715        let ob_errors = self.generators.objects.iter().filter_map(|x| {
716            if self.ob_types.get(&x).is_some_and(|typ| self.theory.has_ob_type(typ)) {
717                None
718            } else {
719                Some(Invalid::ObType(x))
720            }
721        });
722        let mor_errors = self.generators.morphisms.iter().flat_map(|e| {
723            let mut errs = Vec::new();
724            let dom = self.generators.dom.get(&e).filter(|x| self.has_ob(x));
725            let cod = self.generators.cod.get(&e).filter(|x| self.has_ob(x));
726            if dom.is_none() {
727                errs.push(Invalid::Dom(e.clone()));
728            }
729            if cod.is_none() {
730                errs.push(Invalid::Cod(e.clone()));
731            }
732            if let Some(mor_type) =
733                self.mor_types.get(&e).filter(|typ| self.theory.has_mor_type(typ))
734            {
735                if dom.is_some_and(|x| self.ob_type(x) != self.theory.src(mor_type)) {
736                    errs.push(Invalid::DomType(e.clone()));
737                }
738                if cod.is_some_and(|x| self.ob_type(x) != self.theory.tgt(mor_type)) {
739                    errs.push(Invalid::CodType(e.clone()));
740                }
741            } else {
742                errs.push(Invalid::MorType(e));
743            }
744            errs.into_iter()
745        });
746        ob_errors.chain(mor_errors)
747    }
748}
749
750impl<Id, ThId, S> Category for DiscreteTabModel<Id, ThId, S>
751where
752    Id: Eq + Clone + Hash,
753{
754    type Ob = TabOb<Id, Id>;
755    type Mor = TabMor<Id, Id>;
756
757    fn has_ob(&self, x: &Self::Ob) -> bool {
758        self.generators.has_vertex(x)
759    }
760    fn has_mor(&self, path: &Self::Mor) -> bool {
761        path.contained_in(&self.generators)
762    }
763    fn dom(&self, path: &Self::Mor) -> Self::Ob {
764        path.src(&self.generators)
765    }
766    fn cod(&self, path: &Self::Mor) -> Self::Ob {
767        path.tgt(&self.generators)
768    }
769
770    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
771        path.flatten_in(&self.generators).expect("Paths should be composable")
772    }
773}
774
775impl<Id, ThId, S> FgCategory for DiscreteTabModel<Id, ThId, S>
776where
777    Id: Eq + Clone + Hash,
778{
779    type ObGen = Id;
780    type MorGen = Id;
781
782    fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen> {
783        self.generators.objects.iter()
784    }
785    fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen> {
786        self.generators.morphisms.iter()
787    }
788
789    fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob {
790        self.generators.dom.apply(f).expect("Domain should be defined")
791    }
792    fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob {
793        self.generators.cod.apply(f).expect("Codomain should be defined")
794    }
795}
796
797impl<Id, ThId, S> DblModel for DiscreteTabModel<Id, ThId, S>
798where
799    Id: Eq + Clone + Hash,
800    ThId: Eq + Clone + Hash,
801    S: BuildHasher,
802{
803    type ObType = TabObType<ThId, ThId>;
804    type MorType = TabMorType<ThId, ThId>;
805    type ObOp = TabObOp<ThId, ThId>;
806    type MorOp = TabMorOp<ThId, ThId>;
807    type Theory = DiscreteTabTheory<ThId, ThId, S>;
808
809    fn theory(&self) -> &Self::Theory {
810        &self.theory
811    }
812
813    fn ob_type(&self, ob: &Self::Ob) -> Self::ObType {
814        match ob {
815            TabOb::Basic(x) => self.ob_generator_type(x),
816            TabOb::Tabulated(m) => TabObType::Tabulator(Box::new(self.mor_type(m))),
817        }
818    }
819
820    fn mor_type(&self, mor: &Self::Mor) -> Self::MorType {
821        let types = mor.clone().map(
822            |x| self.ob_type(&x),
823            |edge| match edge {
824                TabEdge::Basic(f) => self.mor_generator_type(&f),
825                TabEdge::Square { dom, .. } => {
826                    let typ = self.mor_type(&dom); // == self.mor_type(&cod)
827                    TabMorType::Hom(Box::new(TabObType::Tabulator(Box::new(typ))))
828                }
829            },
830        );
831        self.theory.compose_types(types).expect("Morphism types should have composite")
832    }
833
834    fn ob_act(&self, _ob: Self::Ob, _op: &Self::ObOp) -> Self::Ob {
835        panic!("Action on objects not implemented")
836    }
837
838    fn mor_act(&self, _mor: Self::Mor, _op: &Self::MorOp) -> Self::Mor {
839        panic!("Action on morphisms not implemented")
840    }
841}
842
843impl<Id, ThId, S> FgDblModel for DiscreteTabModel<Id, ThId, S>
844where
845    Id: Eq + Clone + Hash,
846    ThId: Eq + Clone + Hash,
847    S: BuildHasher,
848{
849    fn ob_generator_type(&self, ob: &Self::ObGen) -> Self::ObType {
850        self.ob_types.apply(ob).expect("Object should have type")
851    }
852    fn mor_generator_type(&self, mor: &Self::MorGen) -> Self::MorType {
853        self.mor_types.apply(mor).expect("Morphism should have type")
854    }
855
856    fn ob_generators_with_type(&self, obtype: &Self::ObType) -> impl Iterator<Item = Self::ObGen> {
857        self.ob_types.preimage(obtype)
858    }
859    fn mor_generators_with_type(
860        &self,
861        mortype: &Self::MorType,
862    ) -> impl Iterator<Item = Self::MorGen> {
863        self.mor_types.preimage(mortype)
864    }
865}
866
867impl<Id, ThId, S> MutDblModel for DiscreteTabModel<Id, ThId, S>
868where
869    Id: Eq + Clone + Hash,
870    ThId: Eq + Clone + Hash,
871    S: BuildHasher,
872{
873    fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) -> bool {
874        self.ob_types.set(x.clone(), ob_type);
875        self.generators.objects.insert(x)
876    }
877
878    fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) -> bool {
879        self.mor_types.set(f.clone(), mor_type);
880        self.generators.morphisms.insert(f)
881    }
882
883    fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
884        self.generators.dom.get(f)
885    }
886    fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
887        self.generators.cod.get(f)
888    }
889    fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) -> Option<Self::Ob> {
890        self.generators.dom.set(f, x)
891    }
892    fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) -> Option<Self::Ob> {
893        self.generators.cod.set(f, x)
894    }
895}
896
897impl<Id, ThId, S> Validate for DiscreteTabModel<Id, ThId, S>
898where
899    Id: Eq + Clone + Hash,
900    ThId: Eq + Clone + Hash,
901    S: BuildHasher,
902{
903    type ValidationError = InvalidDblModel<Id>;
904
905    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
906        validate::wrap_errors(self.iter_invalid())
907    }
908}
909
910#[cfg(test)]
911mod tests {
912    use nonempty::nonempty;
913    use ustr::ustr;
914
915    use super::*;
916    use crate::one::fin_category::FinMor;
917    use crate::stdlib::{models::*, theories::*};
918
919    #[test]
920    fn validate_discrete_dbl_model() {
921        let th = Arc::new(th_schema());
922        let mut model = DiscreteDblModel::new(th.clone());
923        let entity = ustr("entity");
924        model.add_ob(entity, ustr("NotObType"));
925        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::ObType(entity)]));
926
927        let mut model = DiscreteDblModel::new(th.clone());
928        model.add_ob(entity, ustr("Entity"));
929        model.add_mor(ustr("map"), entity, entity, FinMor::Generator(ustr("NotMorType")));
930        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::MorType(ustr("map"))]));
931
932        let mut model = DiscreteDblModel::new(th);
933        model.add_ob(entity, ustr("Entity"));
934        model.add_ob(ustr("type"), ustr("AttrType"));
935        model.add_mor(ustr("a"), entity, ustr("type"), FinMor::Generator(ustr("Attr")));
936        assert!(model.validate().is_ok());
937        model.add_mor(ustr("b"), entity, ustr("type"), FinMor::Id(ustr("Entity")));
938        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::CodType(ustr("b"))]));
939    }
940
941    #[test]
942    fn infer_discrete_dbl_model() {
943        let th = Arc::new(th_schema());
944        let mut model = DiscreteDblModel::new(th.clone());
945        model.add_mor(ustr("attr"), ustr("entity"), ustr("type"), FinMor::Generator(ustr("Attr")));
946        model.infer_missing();
947        assert_eq!(model, walking_attr(th));
948    }
949
950    #[test]
951    fn validate_discrete_tab_model() {
952        let th = Arc::new(th_category_links());
953        let mut model = DiscreteTabModel::new(th);
954        let (x, f) = (ustr("x"), ustr("f"));
955        model.add_ob(x, TabObType::Basic(ustr("Object")));
956        model.add_mor(f, TabOb::Basic(x), TabOb::Basic(x), TabMorType::Basic(ustr("Link")));
957        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::CodType(f)]));
958    }
959}
catlog/dbl/model.rs

catlog/dbl/
model.rs
