catlog/dbl/modal/
model.rs

1//! Models of modal double theories.
2
3use std::collections::HashMap;
4use std::fmt::Debug;
5use std::rc::Rc;
6use std::sync::LazyLock;
7
8use derive_more::From;
9use itertools::Itertools;
10use ref_cast::RefCast;
11
12use super::theory::*;
13use crate::dbl::theory::DblTheoryKind;
14use crate::dbl::{graph::VDblGraph, model::*, theory::DblTheory};
15use crate::validate::{self, Validate};
16use crate::zero::pretty::*;
17use crate::{one::computad::*, one::*, zero::*};
18
19/// Object in a model of a modal double theory.
20#[derive(Clone, Debug, PartialEq, Eq, From)]
21pub enum ModalOb {
22    /// Generating object.
23    #[from]
24    Generator(QualifiedName),
25
26    /// Application of a generating object operation.
27    App(Box<Self>, QualifiedName),
28
29    /// List of objects in a [list modality](List).
30    List(List, Vec<Self>),
31}
32
33/// Morphism is a model of a modal double theory.
34#[derive(Clone, Debug, PartialEq, Eq, From)]
35pub enum ModalMor {
36    /// Generating morphism.
37    #[from]
38    Generator(QualifiedName),
39
40    /// Composite of morphisms.
41    Composite(Box<Path<ModalOb, Self>>),
42
43    /// Application of a basic morphism operation.
44    App(Box<Path<ModalOb, Self>>, QualifiedName),
45
46    /// Application of the hom operation on a basic object operation.
47    HomApp(Box<Path<ModalOb, Self>>, QualifiedName),
48
49    /// List of morphisms.
50    List(MorListData, Vec<Self>),
51}
52
53/// Extra data associated with a list of morphisms in a [list modality](List).
54#[derive(Clone, Debug, PartialEq, Eq)]
55pub enum MorListData {
56    /// No extra data for a morphism in the [plain list](List::Plain) modality.
57    Plain(),
58
59    /// Data for a morphism in the [symmetric list](List::Symmetric) modality.
60    ///
61    /// A permutation on the indexing set of the list, which acts on the list of
62    /// codomain objects.
63    Symmetric(SkelColumn),
64}
65
66impl MorListData {
67    fn list_type(&self) -> List {
68        match self {
69            MorListData::Plain() => List::Plain,
70            MorListData::Symmetric(..) => List::Symmetric,
71        }
72    }
73}
74
75/// A model of a modal double theory.
76#[derive(Clone)]
77pub struct ModalDblModel<Kind> {
78    theory: Rc<ModalDblTheory<Kind>>,
79    ob_generators: HashFinSet<QualifiedName>,
80    mor_generators: ComputadTop<ModalOb, QualifiedName>,
81    equations: [(); 0], // TODO: Equations not implemented
82    ob_types: HashColumn<QualifiedName, ModalObType>,
83    mor_types: HashColumn<QualifiedName, ModalMorType>,
84}
85
86impl<Kind: DblTheoryKind> ModalDblModel<Kind> {
87    /// Creates an empty model of the given theory.
88    pub fn new(theory: Rc<ModalDblTheory<Kind>>) -> Self {
89        Self {
90            theory,
91            ob_generators: Default::default(),
92            mor_generators: Default::default(),
93            equations: Default::default(),
94            ob_types: Default::default(),
95            mor_types: Default::default(),
96        }
97    }
98
99    /// Gets the computing generating the morphisms of the model.
100    fn computad(&self) -> Computad<'_, ModalOb, ModalDblModelObs<Kind>, QualifiedName> {
101        Computad::new(ModalDblModelObs::ref_cast(self), &self.mor_generators)
102    }
103}
104
105#[derive(RefCast)]
106#[repr(transparent)]
107struct ModalDblModelObs<Kind>(ModalDblModel<Kind>);
108
109impl<Kind: DblTheoryKind> Set for ModalDblModelObs<Kind> {
110    type Elem = ModalOb;
111
112    fn contains(&self, ob: &Self::Elem) -> bool {
113        match ob {
114            ModalOb::Generator(id) => self.0.ob_generators.contains(id),
115            ModalOb::App(x, op_id) => {
116                self.contains(x)
117                    && self.0.ob_has_type(x, &self.0.theory.tight_computad().src(op_id))
118            }
119            ModalOb::List(_, xs) => xs.iter().all(|x| self.contains(x)),
120        }
121    }
122}
123
124impl<Kind: DblTheoryKind> Category for ModalDblModel<Kind> {
125    type Ob = ModalOb;
126    type Mor = ModalMor;
127
128    fn has_ob(&self, ob: &Self::Ob) -> bool {
129        ModalDblModelObs::ref_cast(self).contains(ob)
130    }
131    fn has_mor(&self, mor: &Self::Mor) -> bool {
132        let graph = UnderlyingGraph::ref_cast(self);
133        match mor {
134            ModalMor::Generator(id) => self.computad().has_edge(id),
135            ModalMor::Composite(path) => path.contained_in(graph),
136            // TODO: Check morphism type equals domain of operation.
137            ModalMor::App(path, _) | ModalMor::HomApp(path, _) => path.contained_in(graph),
138            ModalMor::List(MorListData::Plain(), fs) => fs.iter().all(|f| self.has_mor(f)),
139            ModalMor::List(MorListData::Symmetric(sigma), fs) => {
140                sigma.is_permutation(fs.len()) && fs.iter().all(|f| self.has_mor(f))
141            }
142        }
143    }
144
145    fn dom(&self, mor: &Self::Mor) -> Self::Ob {
146        let graph = UnderlyingGraph::ref_cast(self);
147        match mor {
148            ModalMor::Generator(id) => self.computad().src(id),
149            ModalMor::Composite(path) => path.src(graph),
150            ModalMor::App(path, op_id) => {
151                self.ob_act(path.src(graph), &self.theory.dbl_computad().square_src(op_id))
152            }
153            ModalMor::HomApp(path, op_id) => {
154                ModalOp::from(op_id.clone()).ob_act(path.src(graph)).unwrap()
155            }
156            ModalMor::List(data, fs) => {
157                ModalOb::List(data.list_type(), fs.iter().map(|f| self.dom(f)).collect())
158            }
159        }
160    }
161
162    fn cod(&self, mor: &Self::Mor) -> Self::Ob {
163        let graph = UnderlyingGraph::ref_cast(self);
164        match mor {
165            ModalMor::Generator(id) => self.computad().tgt(id),
166            ModalMor::Composite(path) => path.tgt(graph),
167            ModalMor::App(path, op_id) => {
168                self.ob_act(path.tgt(graph), &self.theory.dbl_computad().square_tgt(op_id))
169            }
170            ModalMor::HomApp(path, op_id) => {
171                ModalOp::from(op_id.clone()).ob_act(path.tgt(graph)).unwrap()
172            }
173            ModalMor::List(MorListData::Plain(), fs) => {
174                ModalOb::List(List::Plain, fs.iter().map(|f| self.cod(f)).collect())
175            }
176            ModalMor::List(MorListData::Symmetric(sigma), fs) => {
177                ModalOb::List(List::Symmetric, sigma.values().map(|j| self.cod(&fs[*j])).collect())
178            }
179        }
180    }
181
182    fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor {
183        // TODO: Normalize composites of lists by composing elementwise.
184        ModalMor::Composite(path.into())
185    }
186}
187
188impl<Kind: DblTheoryKind> FgCategory for ModalDblModel<Kind> {
189    type ObGen = QualifiedName;
190    type MorGen = QualifiedName;
191
192    fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen> {
193        self.ob_generators.iter()
194    }
195    fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen> {
196        self.mor_generators.edge_set.iter()
197    }
198    fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob {
199        self.computad().src(f)
200    }
201    fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob {
202        self.computad().tgt(f)
203    }
204}
205
206impl<Kind: DblTheoryKind> DblModel for ModalDblModel<Kind> {
207    type ObType = ModalObType;
208    type MorType = ModalMorType;
209    type ObOp = ModalObOp;
210    type MorOp = ModalMorOp;
211    type Theory = ModalDblTheory<Kind>;
212
213    fn theory(&self) -> Rc<Self::Theory> {
214        self.theory.clone()
215    }
216
217    fn ob_type(&self, ob: &Self::Ob) -> Self::ObType {
218        Option::from(self.infer_ob_type(ob).unwrap()).expect("Object type should be known")
219    }
220
221    fn mor_type(&self, mor: &Self::Mor) -> Self::MorType {
222        Option::from(self.infer_mor_type(mor).unwrap()).expect("Morphism type should be known")
223    }
224
225    fn ob_act(&self, ob: Self::Ob, path: &Self::ObOp) -> Self::Ob {
226        path.clone().ob_act(ob).unwrap()
227    }
228
229    fn mor_act(&self, path: Path<Self::Ob, Self::Mor>, tree: &Self::MorOp) -> Self::Mor {
230        let (Some(mor), Some(node)) = (path.only(), tree.clone().only()) else {
231            panic!("Morphism action only implemented for basic operations");
232        };
233        match node {
234            ModalNode::Basic(op) => op.mor_act(mor, false).unwrap(),
235            ModalNode::Unit(op) => op.mor_act(mor, true).unwrap(),
236            ModalNode::Composite(_) => mor,
237        }
238    }
239}
240
241impl<Kind: DblTheoryKind> FpDblModel for ModalDblModel<Kind> {
242    fn ob_generator_type(&self, id: &Self::ObGen) -> Self::ObType {
243        self.ob_types.apply_to_ref(id).expect("Object should have object type")
244    }
245    fn mor_generator_type(&self, id: &Self::MorGen) -> Self::MorType {
246        self.mor_types.apply_to_ref(id).expect("Morphism should have morphism type")
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    fn equations(&self) -> impl Iterator<Item = (Self::Mor, Self::Mor)> {
255        self.equations.iter().map(|()| unreachable!())
256    }
257}
258
259impl<Kind: DblTheoryKind> MutDblModel for ModalDblModel<Kind> {
260    fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) {
261        self.ob_types.set(x.clone(), ob_type);
262        self.ob_generators.insert(x);
263    }
264    fn add_mor(&mut self, f: Self::MorGen, dom: Self::Ob, cod: Self::Ob, mor_type: Self::MorType) {
265        self.mor_types.set(f.clone(), mor_type);
266        self.mor_generators.add_edge(f, dom, cod);
267    }
268    fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) {
269        self.mor_types.set(f.clone(), mor_type);
270        self.mor_generators.edge_set.insert(f);
271    }
272
273    fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
274        self.mor_generators.src_map.get(f)
275    }
276    fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob> {
277        self.mor_generators.tgt_map.get(f)
278    }
279    fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) {
280        self.mor_generators.src_map.set(f, x);
281    }
282    fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) {
283        self.mor_generators.tgt_map.set(f, x);
284    }
285}
286
287impl<Kind: DblTheoryKind> Validate for ModalDblModel<Kind> {
288    type ValidationError = InvalidDblModel;
289
290    fn validate(&self) -> Result<(), nonempty::NonEmpty<Self::ValidationError>> {
291        let ob_gen_errors = self.ob_generators.iter().filter_map(|x| {
292            if self.ob_types.apply_to_ref(&x).is_none_or(|typ| !self.theory.has_ob_type(&typ)) {
293                Some(InvalidDblModel::ObType(x))
294            } else {
295                None
296            }
297        });
298        validate::wrap_errors(ob_gen_errors)?;
299
300        let computad = self.computad();
301        let mor_gen_errors = computad.edge_set().iter().flat_map(|f| {
302            let mut errors = Vec::new();
303            let mor_type = self.mor_types.apply_to_ref(&f).filter(|m| self.theory.has_mor_type(m));
304            if let Some(ob) = computad.src_map().apply_to_ref(&f)
305                && self.has_ob(&ob)
306            {
307                if mor_type
308                    .as_ref()
309                    .is_some_and(|m| !self.ob_has_type(&ob, &self.theory.src_type(m)))
310                {
311                    errors.push(InvalidDblModel::DomType(f.clone()))
312                }
313            } else {
314                errors.push(InvalidDblModel::Dom(f.clone()))
315            }
316            if let Some(ob) = computad.tgt_map().apply_to_ref(&f)
317                && self.has_ob(&ob)
318            {
319                if mor_type
320                    .as_ref()
321                    .is_some_and(|m| !self.ob_has_type(&ob, &self.theory.tgt_type(m)))
322                {
323                    errors.push(InvalidDblModel::CodType(f.clone()))
324                }
325            } else {
326                errors.push(InvalidDblModel::Cod(f.clone()))
327            }
328            if mor_type.is_none() {
329                errors.push(InvalidDblModel::MorType(f))
330            }
331            errors
332        });
333        validate::wrap_errors(mor_gen_errors)
334    }
335}
336
337#[derive(From)]
338enum InferredType<T> {
339    #[from]
340    Type(T),
341    Unknown,
342}
343
344impl<T> From<InferredType<T>> for Option<T> {
345    fn from(value: InferredType<T>) -> Self {
346        match value {
347            InferredType::Type(value) => Some(value),
348            InferredType::Unknown => None,
349        }
350    }
351}
352
353impl<Kind: DblTheoryKind> ModalDblModel<Kind> {
354    /// Tries to infer the type of an object in the model.
355    fn infer_ob_type(&self, ob: &ModalOb) -> Result<InferredType<ModalObType>, String> {
356        match ob {
357            ModalOb::Generator(id) => Ok(self.ob_generator_type(id).into()),
358            ModalOb::App(_, op_id) => Ok(self.theory.tight_computad().tgt(op_id).into()),
359            ModalOb::List(list_type, vec) => {
360                let inferred_types: Result<Vec<_>, _> =
361                    vec.iter().map(|ob| self.infer_ob_type(ob)).collect();
362                let unique_type = inferred_types?
363                    .into_iter()
364                    .filter_map(Option::<ModalObType>::from)
365                    .all_equal_value();
366                match unique_type {
367                    Ok(ob_type) => Ok(ob_type.apply((*list_type).into()).into()),
368                    Err(Some(_)) => Err("All objects in list should have the same type".into()),
369                    Err(None) => Ok(InferredType::Unknown),
370                }
371            }
372        }
373    }
374
375    /// Tries to infer the type of a morphism in the model.
376    fn infer_mor_type(&self, mor: &ModalMor) -> Result<InferredType<ModalMorType>, String> {
377        match mor {
378            ModalMor::Generator(id) => Ok(self.mor_generator_type(id).into()),
379            ModalMor::Composite(_) => panic!("Composites not implemented"),
380            ModalMor::App(_, op_id) => Ok(self.theory.dbl_computad().square_cod(op_id).into()),
381            ModalMor::HomApp(_, op_id) => {
382                Ok(ShortPath::Zero(self.theory.tight_computad().tgt(op_id)).into())
383            }
384            ModalMor::List(data, vec) => {
385                let inferred_types: Result<Vec<_>, _> =
386                    vec.iter().map(|mor| self.infer_mor_type(mor)).collect();
387                let unique_type = inferred_types?
388                    .into_iter()
389                    .filter_map(Option::<ModalMorType>::from)
390                    .all_equal_value();
391                match unique_type {
392                    Ok(mor_type) => Ok(mor_type.apply(data.list_type().into()).into()),
393                    Err(Some(_)) => Err("All morphisms in list should have the same type".into()),
394                    Err(None) => Ok(InferredType::Unknown),
395                }
396            }
397        }
398    }
399
400    /// Does the object have the given type?
401    fn ob_has_type(&self, ob: &ModalOb, ob_type: &ModalObType) -> bool {
402        if let ModalOb::List(list_type, vec) = ob
403            && vec.is_empty()
404        {
405            // XXX: This is bandaid due to lack of type unification.
406            return ob_type.modalities.last() == Some(&Modality::List(*list_type));
407        }
408        match self.infer_ob_type(ob) {
409            Ok(InferredType::Type(other_type)) => other_type == *ob_type,
410            _ => false,
411        }
412    }
413}
414
415impl ModalObOp {
416    /// Acts on an object in a model of a modal theory.
417    pub fn ob_act(self, ob: ModalOb) -> Result<ModalOb, String> {
418        self.into_iter().try_fold(ob, |ob, op| op.ob_act(ob))
419    }
420}
421
422impl ModeApp<ModalOp> {
423    fn ob_act(mut self, ob: ModalOb) -> Result<ModalOb, String> {
424        match self.modalities.pop() {
425            Some(Modality::List(list_type)) => {
426                if let ModalOb::List(other_type, vec) = ob
427                    && other_type == list_type
428                {
429                    let maybe_vec: Result<Vec<_>, _> =
430                        vec.into_iter().map(|ob| self.clone().ob_act(ob)).collect();
431                    Ok(ModalOb::List(list_type, maybe_vec?))
432                } else {
433                    Err(format!("Object should be a list of type {list_type:?}"))
434                }
435            }
436            Some(Modality::Discrete()) | Some(Modality::Codiscrete()) | None => self.arg.ob_act(ob),
437        }
438    }
439
440    fn mor_act(mut self, mor: ModalMor, is_unit: bool) -> Result<ModalMor, String> {
441        match self.modalities.pop() {
442            Some(Modality::List(list_type)) => {
443                if let ModalMor::List(data, vec) = mor
444                    && data.list_type() == list_type
445                {
446                    let maybe_vec: Result<Vec<_>, _> =
447                        vec.into_iter().map(|mor| self.clone().mor_act(mor, is_unit)).collect();
448                    Ok(ModalMor::List(data, maybe_vec?))
449                } else {
450                    Err(format!("Morphism should be a list of type {list_type:?}"))
451                }
452            }
453            Some(modality) => panic!("Modality {modality:?} is not implemented"),
454            None => self.arg.mor_act(mor, is_unit),
455        }
456    }
457}
458
459impl ModalOp {
460    fn ob_act(self, ob: ModalOb) -> Result<ModalOb, String> {
461        match self {
462            ModalOp::Generator(id) => Ok(ModalOb::App(Box::new(ob), id)),
463            ModalOp::Concat(list_type, n, _) => {
464                Ok(ModalOb::List(list_type, ob.flatten_list(list_type, n)?))
465            }
466        }
467    }
468
469    fn mor_act(self, mor: ModalMor, is_unit: bool) -> Result<ModalMor, String> {
470        match self {
471            ModalOp::Generator(id) => Ok(if is_unit {
472                ModalMor::HomApp(Box::new(mor.into()), id)
473            } else {
474                ModalMor::App(Box::new(mor.into()), id)
475            }),
476            ModalOp::Concat(list_type, n, _) => match list_type {
477                List::Plain => Ok(ModalMor::List(MorListData::Plain(), mor.flatten_list(n)?)),
478                _ => panic!("Flattening of functions is not implemented"),
479            },
480        }
481    }
482}
483
484impl ModalOb {
485    /// Extracts an object generator or nothing.
486    pub fn generator(self) -> Option<QualifiedName> {
487        match self {
488            ModalOb::Generator(id) => Some(id),
489            _ => None,
490        }
491    }
492
493    /// Unwraps an object generator, or panics.
494    pub fn unwrap_generator(self) -> QualifiedName {
495        self.generator().expect("Object should be a generator")
496    }
497
498    /// Collects application of a product operation into a list of objects.
499    ///
500    /// The intended operation has domain equal to the list modality applied to its
501    /// codomain, which usually signifies a product of some kind.
502    pub fn collect_product(self, op_id: Option<QualifiedName>) -> Option<Vec<Self>> {
503        match self {
504            ModalOb::Generator(_) => Some(vec![self]),
505            ModalOb::App(ob, other_id) if op_id.is_none_or(|id| id == other_id) => match *ob {
506                ModalOb::List(_, objects) => Some(objects),
507                _ => None,
508            },
509            _ => None,
510        }
511    }
512
513    /// Recursively flatten a nested list of objects of the given depth.
514    fn flatten_list(self, list_type: List, depth: usize) -> Result<Vec<Self>, String> {
515        if depth == 0 {
516            Ok(vec![self])
517        } else if let ModalOb::List(other_type, vec) = self
518            && other_type == list_type
519        {
520            if depth == 1 {
521                Ok(vec)
522            } else {
523                let maybe_vec: Result<Vec<_>, _> =
524                    vec.into_iter().map(|ob| ob.flatten_list(list_type, depth - 1)).collect();
525                Ok(maybe_vec?.into_iter().flatten().collect())
526            }
527        } else {
528            Err(format!("Object should be a list of type {list_type:?}"))
529        }
530    }
531}
532
533impl ModalMor {
534    /// Recursively flatten a nested list of morphisms of the given depth.
535    fn flatten_list(self, depth: usize) -> Result<Vec<Self>, String> {
536        if depth == 0 {
537            Ok(vec![self])
538        } else if let ModalMor::List(MorListData::Plain(), vec) = self {
539            if depth == 1 {
540                Ok(vec)
541            } else {
542                let maybe_vec: Result<Vec<_>, _> =
543                    vec.into_iter().map(|mor| mor.flatten_list(depth - 1)).collect();
544                Ok(maybe_vec?.into_iter().flatten().collect())
545            }
546        } else {
547            Err(format!("Morphism should be a list of type {:?}", List::Plain))
548        }
549    }
550}
551
552impl<Kind: DblTheoryKind> PrintableDblModel for ModalDblModel<Kind> {
553    fn ob_to_doc<'a>(&self, ob: &Self::Ob, ob_ns: &Namespace, mor_ns: &Namespace) -> D<'a> {
554        match ob {
555            ModalOb::Generator(name) => t(ob_ns.label_string(name)),
556            ModalOb::App(ob, op) => {
557                let op = op.to_string();
558                let op_doc = match UNICODE_OP_LOOKUP.get(op.as_str()) {
559                    Some(uni_op) => t(*uni_op),
560                    None => t(format!("@{op}")),
561                };
562                unop(op_doc, self.ob_to_doc(ob, ob_ns, mor_ns))
563            }
564            ModalOb::List(_, obs) => tuple(obs.iter().map(|ob| self.ob_to_doc(ob, ob_ns, mor_ns))),
565        }
566    }
567
568    fn mor_to_doc<'a>(&self, _mor: &Self::Mor, _ob_ns: &Namespace, _mor_ns: &Namespace) -> D<'a> {
569        todo!("Pretty printing morphisms in models of modal theories")
570    }
571
572    fn ob_type_to_doc<'a>(ob_type: &Self::ObType) -> D<'a> {
573        modal_type_to_doc(ob_type)
574    }
575    fn mor_type_to_doc<'a>(mor_type: &Self::MorType) -> D<'a> {
576        match mor_type {
577            ShortPath::Zero(ob_type) => unop(t("Hom"), Self::ob_type_to_doc(ob_type)),
578            ShortPath::One(app) => modal_type_to_doc(app),
579        }
580    }
581}
582
583fn modal_type_to_doc<'a>(app: &ModalType) -> D<'a> {
584    let mut doc = app.arg.to_doc();
585    for mode in app.modalities.iter() {
586        doc = unop(t(mode.to_string()), doc);
587    }
588    doc
589}
590
591impl<Kind: DblTheoryKind> std::fmt::Display for ModalDblModel<Kind> {
592    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
593        write!(f, "{}", DblModelPrinter::new().doc(self).pretty())
594    }
595}
596
597// XXX: This doesn't really belong here but it makes my pretty print look good.
598static UNICODE_OP_LOOKUP: LazyLock<HashMap<&str, &str>> =
599    LazyLock::new(|| HashMap::from([("tensor", "⨂"), ("cotensor", "⨁")]));
600
601#[cfg(test)]
602mod tests {
603    use expect_test::expect;
604
605    use super::*;
606    use crate::dbl::theory::DblTheory;
607    use crate::stdlib::{models::*, theories::*};
608    use crate::zero::name;
609    use crate::{dbl::tree::DblNode, one::tree::OpenTree};
610
611    #[test]
612    fn monoidal_category() {
613        let th = Rc::new(th_monoidal_category());
614        let ob_type = ModeApp::new(name("Object"));
615
616        // Lists of objects.
617        let mut model = ModalDblModel::new(th.clone());
618        model.add_ob(name("x"), ob_type.clone());
619        model.add_ob(name("y"), ob_type.clone());
620        let [w, x, y, z] = [name("w"), name("x"), name("y"), name("z")].map(ModalOb::from);
621        assert!(model.has_ob(&x));
622        let pair = ModalOb::List(List::Plain, vec![x.clone(), y.clone()]);
623        assert!(model.has_ob(&pair));
624        assert!(!model.has_ob(&ModalOb::List(List::Plain, vec![x.clone(), z.clone()])));
625
626        // Nested lists of objects.
627        model.add_ob(name("w"), ob_type.clone());
628        model.add_ob(name("z"), ob_type.clone());
629        let pairs = ModalOb::List(
630            List::Plain,
631            vec![
632                ModalOb::List(List::Plain, vec![w.clone(), x.clone()]),
633                ModalOb::List(List::Plain, vec![y.clone(), z.clone()]),
634            ],
635        );
636        assert!(model.has_ob(&pairs));
637        assert_eq!(
638            model.ob_act(pairs, &ModalObOp::concat(List::Plain, 2, ob_type.clone())),
639            ModalOb::List(List::Plain, vec![w.clone(), x.clone(), y.clone(), z.clone()])
640        );
641        assert_eq!(
642            model.ob_act(x.clone(), &ModalObOp::concat(List::Plain, 0, ob_type.clone())),
643            ModalOb::List(List::Plain, vec![x.clone()])
644        );
645
646        // Products of objects.
647        assert_eq!(model.ob_type(&pair), ob_type.clone().apply(List::Plain.into()));
648        let mul_op = ModalObOp::generator(name("tensor"));
649        let prod = model.ob_act(pair, &mul_op);
650        assert!(model.has_ob(&prod));
651        assert_eq!(model.ob_type(&prod), ob_type);
652
653        // Model validation.
654        model.add_mor(name("f"), x.clone(), y.clone(), th.hom_type(ob_type.clone()));
655        model.add_mor(name("g"), w.clone(), z.clone(), th.hom_type(ob_type.clone()));
656        let [f, g] = [name("f"), name("g")].map(ModalMor::from);
657        assert!(model.has_mor(&f));
658        assert!(model.validate().is_ok());
659
660        // Lists of morphisms.
661        let pair = ModalMor::List(MorListData::Plain(), vec![f.clone(), g.clone()]);
662        assert!(model.has_mor(&pair));
663        assert_eq!(model.mor_type(&pair), th.hom_type(ob_type.clone().apply(List::Plain.into())));
664        let dom_list = ModalOb::List(List::Plain, vec![x.clone(), w.clone()]);
665        let cod_list = ModalOb::List(List::Plain, vec![y.clone(), z.clone()]);
666        assert_eq!(model.dom(&pair), dom_list);
667        assert_eq!(model.cod(&pair), cod_list);
668
669        // Products of morphisms.
670        let ob_op = ModeApp::new(name("tensor").into());
671        let hom_op = OpenTree::single(DblNode::Cell(ModalNode::Unit(ob_op)), 1).into();
672        let prod = model.mor_act(pair.into(), &hom_op);
673        assert!(model.has_mor(&prod));
674        assert_eq!(model.mor_type(&prod), th.hom_type(ob_type.clone()));
675        assert_eq!(model.dom(&prod), model.ob_act(dom_list, &mul_op));
676        assert_eq!(model.cod(&prod), model.ob_act(cod_list, &mul_op));
677    }
678
679    #[test]
680    fn sym_monoidal_category() {
681        let th = Rc::new(th_sym_monoidal_category());
682        let ob_type = ModeApp::new(name("Object"));
683
684        // Model validation.
685        let mut model = ModalDblModel::new(th.clone());
686        for id in [name("w"), name("x"), name("y"), name("z")] {
687            model.add_ob(id, ob_type.clone());
688        }
689        let [w, x, y, z] = [name("w"), name("x"), name("y"), name("z")].map(ModalOb::from);
690        model.add_mor(name("f"), x.clone(), y.clone(), th.hom_type(ob_type.clone()));
691        model.add_mor(name("g"), w.clone(), z.clone(), th.hom_type(ob_type.clone()));
692        let [f, g] = [name("f"), name("g")].map(ModalMor::from);
693        assert!(model.validate().is_ok());
694
695        // Lists of morphisms, with permutation.
696        let pair = ModalMor::List(
697            MorListData::Symmetric(SkelColumn::new(vec![1, 0])),
698            vec![f.clone(), g.clone()],
699        );
700        assert!(model.has_mor(&pair));
701        assert_eq!(model.dom(&pair), ModalOb::List(List::Symmetric, vec![x.clone(), w.clone()]));
702        assert_eq!(model.cod(&pair), ModalOb::List(List::Symmetric, vec![z.clone(), y.clone()]));
703        // Bad permutation.
704        let pair = ModalMor::List(MorListData::Symmetric(SkelColumn::new(vec![0, 0])), vec![f, g]);
705        assert!(!model.has_mor(&pair));
706    }
707
708    #[test]
709    fn multicategory() {
710        let th = Rc::new(th_multicategory());
711        let ob_type = ModeApp::new(name("Object"));
712        let mor_type: ModalMorType = ModeApp::new(name("Multihom")).into();
713
714        // Model validation.
715        let mut model = ModalDblModel::new(th.clone());
716        model.add_ob(name("x"), ob_type.clone());
717        let x: ModalOb = name("x").into();
718        model.add_mor(
719            name("binary"),
720            ModalOb::List(List::Plain, vec![x.clone(), x.clone()]),
721            x.clone(),
722            mor_type.clone(),
723        );
724        model.add_mor(name("nullary"), ModalOb::List(List::Plain, vec![]), x.clone(), mor_type);
725        assert!(model.validate().is_ok());
726    }
727
728    #[test]
729    fn pretty_print() {
730        let model = sir_petri(Rc::new(th_sym_monoidal_category()));
731        let expected = expect![[r#"
732            model generated by 3 objects and 2 morphisms
733            S : Object
734            I : Object
735            R : Object
736            infect : ⨂ [S, I] -> ⨂ [I, I] : Hom Object
737            recover : I -> R : Hom Object"#]];
738        expected.assert_eq(&format!("{model}"));
739    }
740}
catlog/dbl/modal/model.rs

catlog/dbl/modal/
model.rs
