catlog/dbl/discrete_tabulator/
model.rs

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

catlog/dbl/discrete_tabulator/
model.rs
