catlog/dbl/discrete_tabulator/
model.rs

1//! Models of discrete tabulator theories.
2
3use std::rc::Rc;
4
5use derivative::Derivative;
6use derive_more::From;
7
8use super::theory::*;
9use crate::dbl::{category::*, model::*, theory::DblTheory};
10use crate::validate::{self, Validate};
11use crate::zero::pretty::*;
12use crate::{one::*, zero::*};
13
14/// Object in a model of a discrete tabulator theory.
15#[derive(Clone, PartialEq, Debug, Eq, From)]
16pub enum TabOb {
17    /// Basic or generating object.
18    #[from]
19    Basic(QualifiedName),
20
21    /// A morphism viewed as an object of a tabulator.
22    Tabulated(Box<TabMor>),
23}
24
25impl TabOb {
26    /// Extracts a basic object or nothing.
27    pub fn basic(self) -> Option<QualifiedName> {
28        match self {
29            TabOb::Basic(id) => Some(id),
30            _ => None,
31        }
32    }
33
34    /// Extracts a tabulated morphism or nothing.
35    pub fn tabulated(self) -> Option<TabMor> {
36        match self {
37            TabOb::Tabulated(mor) => Some(*mor),
38            _ => None,
39        }
40    }
41
42    /// Unwraps a basic object, or panics.
43    pub fn unwrap_basic(self) -> QualifiedName {
44        self.basic().expect("Object should be a basic object")
45    }
46
47    /// Unwraps a tabulated morphism, or panics.
48    pub fn unwrap_tabulated(self) -> TabMor {
49        self.tabulated().expect("Object should be a tabulated morphism")
50    }
51}
52
53/// "Edge" in a model of a discrete tabulator theory.
54///
55/// Morphisms of these two forms generate all the morphisms in the model.
56#[derive(Clone, PartialEq, Debug, Eq, From)]
57pub enum TabEdge {
58    /// Basic morphism between any two objects.
59    #[from]
60    Basic(QualifiedName),
61
62    /// Generating morphism between tabulated morphisms, a commutative square.
63    Square {
64        /// The domain, a tabulated morphism.
65        dom: Box<TabMor>,
66
67        /// The codomain, a tabulated morphism.
68        cod: Box<TabMor>,
69
70        /// Edge that acts by pre-composition onto codomain.
71        pre: Box<TabEdge>,
72
73        /// Edge that acts by post-composition onto domain.
74        post: Box<TabEdge>,
75    },
76}
77
78/// Morphism in a model of a discrete tabulator theory.
79pub type TabMor = Path<TabOb, TabEdge>;
80
81impl From<QualifiedName> for TabMor {
82    fn from(value: QualifiedName) -> Self {
83        Path::single(value.into())
84    }
85}
86
87#[derive(Clone, Default, PartialEq, Eq)]
88struct DiscreteTabGenerators {
89    objects: HashFinSet<QualifiedName>,
90    morphisms: HashFinSet<QualifiedName>,
91    dom: HashColumn<QualifiedName, TabOb>,
92    cod: HashColumn<QualifiedName, TabOb>,
93}
94
95impl Graph for DiscreteTabGenerators {
96    type V = TabOb;
97    type E = TabEdge;
98
99    fn has_vertex(&self, ob: &Self::V) -> bool {
100        match ob {
101            TabOb::Basic(v) => self.objects.contains(v),
102            TabOb::Tabulated(p) => (*p).contained_in(self),
103        }
104    }
105
106    fn has_edge(&self, edge: &Self::E) -> bool {
107        match edge {
108            TabEdge::Basic(e) => {
109                self.morphisms.contains(e) && self.dom.is_set(e) && self.cod.is_set(e)
110            }
111            TabEdge::Square { dom, cod, pre, post } => {
112                if !(dom.contained_in(self) && cod.contained_in(self)) {
113                    return false;
114                }
115                let path1 = dom.clone().concat_in(self, Path::single(*post.clone()));
116                let path2 = Path::single(*pre.clone()).concat_in(self, *cod.clone());
117                path1.is_some() && path2.is_some() && path1 == path2
118            }
119        }
120    }
121
122    fn src(&self, edge: &Self::E) -> Self::V {
123        match edge {
124            TabEdge::Basic(e) => {
125                self.dom.apply_to_ref(e).expect("Domain of morphism should be defined")
126            }
127            TabEdge::Square { dom, .. } => TabOb::Tabulated(dom.clone()),
128        }
129    }
130
131    fn tgt(&self, edge: &Self::E) -> Self::V {
132        match edge {
133            TabEdge::Basic(e) => {
134                self.cod.apply_to_ref(e).expect("Codomain of morphism should be defined")
135            }
136            TabEdge::Square { cod, .. } => TabOb::Tabulated(cod.clone()),
137        }
138    }
139}
140
141/// A finitely presented model of a discrete tabulator theory.
142///
143/// A **model** of a [discrete tabulator theory](super::theory::DiscreteTabTheory)
144/// is a normal lax functor from the theory into the double category of profunctors
145/// that preserves tabulators. For the definition of "preserving tabulators," see
146/// the dev docs.
147#[derive(Clone, Derivative)]
148#[derivative(PartialEq, Eq)]
149pub struct DiscreteTabModel {
150    #[derivative(PartialEq(compare_with = "Rc::ptr_eq"))]
151    theory: Rc<DiscreteTabTheory>,
152    generators: DiscreteTabGenerators,
153    equations: [(); 0], // TODO: Equations yet implemented
154    ob_types: IndexedHashColumn<QualifiedName, TabObType>,
155    mor_types: IndexedHashColumn<QualifiedName, TabMorType>,
156}
157
158impl DiscreteTabModel {
159    /// Creates an empty model of the given theory.
160    pub fn new(theory: Rc<DiscreteTabTheory>) -> Self {
161        Self {
162            theory,
163            generators: Default::default(),
164            equations: Default::default(),
165            ob_types: Default::default(),
166            mor_types: Default::default(),
167        }
168    }
169
170    /// Convenience method to turn a morphism into an object.
171    pub fn tabulated(&self, mor: TabMor) -> TabOb {
172        TabOb::Tabulated(Box::new(mor))
173    }
174
175    /// Convenience method to turn a morphism generator into an object.
176    pub fn tabulated_gen(&self, f: QualifiedName) -> TabOb {
177        self.tabulated(Path::single(TabEdge::Basic(f)))
178    }
179
180    /// Iterates over failures of model to be well defined.
181    pub fn iter_invalid(&self) -> impl Iterator<Item = InvalidDblModel> + '_ {
182        type Invalid = InvalidDblModel;
183        let ob_errors = self.generators.objects.iter().filter_map(|x| {
184            if self.ob_types.get(&x).is_some_and(|typ| self.theory.has_ob_type(typ)) {
185                None
186            } else {
187                Some(Invalid::ObType(x))
188            }
189        });
190        let mor_errors = self.generators.morphisms.iter().flat_map(|e| {
191            let mut errs = Vec::new();
192            let dom = self.generators.dom.get(&e).filter(|x| self.has_ob(x));
193            let cod = self.generators.cod.get(&e).filter(|x| self.has_ob(x));
194            if dom.is_none() {
195                errs.push(Invalid::Dom(e.clone()));
196            }
197            if cod.is_none() {
198                errs.push(Invalid::Cod(e.clone()));
199            }
200            if let Some(mor_type) =
201                self.mor_types.get(&e).filter(|typ| self.theory.has_mor_type(typ))
202            {
203                if dom.is_some_and(|x| self.ob_type(x) != self.theory.src(mor_type)) {
204                    errs.push(Invalid::DomType(e.clone()));
205                }
206                if cod.is_some_and(|x| self.ob_type(x) != self.theory.tgt(mor_type)) {
207                    errs.push(Invalid::CodType(e.clone()));
208                }
209            } else {
210                errs.push(Invalid::MorType(e));
211            }
212            errs.into_iter()
213        });
214        ob_errors.chain(mor_errors)
215    }
216}
217
218impl Category for DiscreteTabModel {
219    type Ob = TabOb;
220    type Mor = TabMor;
221
222    fn has_ob(&self, x: &Self::Ob) -> bool {
223        self.generators.has_vertex(x)
224    }
225    fn has_mor(&self, path: &Self::Mor) -> bool {
226        path.contained_in(&self.generators)
227    }
228    fn dom(&self, path: &Self::Mor) -> Self::Ob {
229        path.src(&self.generators)
230    }
231    fn cod(&self, path: &Self::Mor) -> Self::Ob {
232        path.tgt(&self.generators)
233    }
234
235    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
236        path.flatten_in(&self.generators).expect("Paths should be composable")
237    }
238}
239
240impl FgCategory for DiscreteTabModel {
241    type ObGen = QualifiedName;
242    type MorGen = QualifiedName;
243
244    fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen> {
245        self.generators.objects.iter()
246    }
247    fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen> {
248        self.generators.morphisms.iter()
249    }
250
251    fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob {
252        self.generators.dom.apply_to_ref(f).expect("Domain should be defined")
253    }
254    fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob {
255        self.generators.cod.apply_to_ref(f).expect("Codomain should be defined")
256    }
257}
258
259impl DblModel for DiscreteTabModel {
260    type ObType = TabObType;
261    type MorType = TabMorType;
262    type ObOp = TabObOp;
263    type MorOp = TabMorOp;
264    type Theory = DiscreteTabTheory;
265
266    fn theory(&self) -> Rc<Self::Theory> {
267        self.theory.clone()
268    }
269
270    fn ob_type(&self, ob: &Self::Ob) -> Self::ObType {
271        match ob {
272            TabOb::Basic(x) => self.ob_generator_type(x),
273            TabOb::Tabulated(m) => TabObType::Tabulator(Box::new(self.mor_type(m))),
274        }
275    }
276
277    fn mor_type(&self, mor: &Self::Mor) -> Self::MorType {
278        let types = mor.clone().map(
279            |x| self.ob_type(&x),
280            |edge| match edge {
281                TabEdge::Basic(f) => self.mor_generator_type(&f),
282                TabEdge::Square { dom, .. } => {
283                    let typ = self.mor_type(&dom); // == self.mor_type(&cod)
284                    TabMorType::Hom(Box::new(TabObType::Tabulator(Box::new(typ))))
285                }
286            },
287        );
288        self.theory.compose_types(types).expect("Morphism types should have composite")
289    }
290
291    fn ob_act(&self, _ob: Self::Ob, _op: &Self::ObOp) -> Self::Ob {
292        panic!("Action on objects not implemented")
293    }
294
295    fn mor_act(&self, _path: Path<Self::Ob, Self::Mor>, _op: &Self::MorOp) -> Self::Mor {
296        panic!("Action on morphisms not implemented")
297    }
298}
299
300impl FpDblModel for DiscreteTabModel {
301    fn ob_generator_type(&self, ob: &Self::ObGen) -> Self::ObType {
302        self.ob_types.apply_to_ref(ob).expect("Object should have type")
303    }
304    fn mor_generator_type(&self, mor: &Self::MorGen) -> Self::MorType {
305        self.mor_types.apply_to_ref(mor).expect("Morphism should have type")
306    }
307
308    fn ob_generators_with_type(&self, obtype: &Self::ObType) -> impl Iterator<Item = Self::ObGen> {
309        self.ob_types.preimage(obtype)
310    }
311    fn mor_generators_with_type(
312        &self,
313        mortype: &Self::MorType,
314    ) -> impl Iterator<Item = Self::MorGen> {
315        self.mor_types.preimage(mortype)
316    }
317
318    fn equations(&self) -> impl Iterator<Item = (Self::Mor, Self::Mor)> {
319        self.equations.iter().map(|()| unreachable!())
320    }
321}
322
323impl MutDblModel for DiscreteTabModel {
324    fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) {
325        self.ob_types.set(x.clone(), ob_type);
326        self.generators.objects.insert(x);
327    }
328
329    fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) {
330        self.mor_types.set(f.clone(), mor_type);
331        self.generators.morphisms.insert(f);
332    }
333
334    fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
335        self.generators.dom.get(f)
336    }
337    fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
338        self.generators.cod.get(f)
339    }
340    fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) {
341        self.generators.dom.set(f, x);
342    }
343    fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) {
344        self.generators.cod.set(f, x);
345    }
346}
347
348impl PrintableDblModel for DiscreteTabModel {
349    fn ob_to_doc<'a>(&self, ob: &Self::Ob, ob_ns: &Namespace, mor_ns: &Namespace) -> D<'a> {
350        match ob {
351            TabOb::Basic(name) => t(ob_ns.label_string(name)),
352            // TODO: This makes printing a bit ambiguous, should wrap in a tab(...)
353            TabOb::Tabulated(mor) => self.mor_to_doc(mor, ob_ns, mor_ns),
354        }
355    }
356
357    fn mor_to_doc<'a>(&self, mor: &Self::Mor, ob_ns: &Namespace, mor_ns: &Namespace) -> D<'a> {
358        match mor {
359            Path::Id(ob) => unop(t("Id"), self.ob_to_doc(ob, ob_ns, mor_ns)),
360            Path::Seq(edges) => intersperse(edges.iter().map(|e| edge_to_doc(e, mor_ns)), t(" ⋅ ")),
361        }
362    }
363
364    fn ob_type_to_doc<'a>(ob_type: &Self::ObType) -> D<'a> {
365        ob_type.to_doc()
366    }
367
368    fn mor_type_to_doc<'a>(mor_type: &Self::MorType) -> D<'a> {
369        mor_type.to_doc()
370    }
371}
372
373fn edge_to_doc<'a>(edge: &TabEdge, mor_ns: &Namespace) -> D<'a> {
374    match edge {
375        TabEdge::Basic(name) => t(mor_ns.label_string(name)),
376        TabEdge::Square { dom: _, cod: _, pre, post } => {
377            tuple([edge_to_doc(pre, mor_ns), edge_to_doc(post, mor_ns)])
378        }
379    }
380}
381
382impl std::fmt::Display for DiscreteTabModel {
383    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
384        write!(f, "{}", DblModelPrinter::new().doc(self).pretty())
385    }
386}
387
388impl Validate for DiscreteTabModel {
389    type ValidationError = InvalidDblModel;
390
391    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
392        validate::wrap_errors(self.iter_invalid())
393    }
394}
395
396#[cfg(test)]
397mod tests {
398    use expect_test::expect;
399    use nonempty::nonempty;
400
401    use super::*;
402    use crate::{
403        stdlib::{models::*, theories::*},
404        zero::name,
405    };
406
407    #[test]
408    fn validate() {
409        let th = Rc::new(th_category_links());
410        let mut model = DiscreteTabModel::new(th);
411        model.add_ob(name("x"), name("Object").into());
412        model.add_mor(name("f"), name("x").into(), name("x").into(), name("Link").into());
413        assert_eq!(model.validate(), Err(nonempty![InvalidDblModel::CodType(name("f"))]));
414    }
415
416    #[test]
417    fn pretty_print() {
418        let model = backward_link(Rc::new(th_category_links()));
419        let expected = expect![[r#"
420            model generated by 2 objects and 2 morphisms
421            x : Object
422            y : Object
423            f : x -> y : Hom Object
424            link : y -> f : Link"#]];
425        expected.assert_eq(&format!("{model}"));
426    }
427}
catlog/dbl/discrete_tabulator/model.rs

catlog/dbl/discrete_tabulator/
model.rs
