catlog/tt/
theory.rs

1//! Double theories as used by DoubleTT.
2//!
3//! In `catlog`, double theories belonging to different double doctrines
4//! (discrete theories, modal theories, etc) are represented using different
5//! data structures. By contrast, there is just one implementation of DoubleTT,
6//! intended to support all of the features that we need. To provide a uniform
7//! interface to theories of different doctrines, theories are boxed in an enum
8//! ([`TheoryDef`]). This design is similar to that taken in `catlog-wasm`.
9
10use all_the_same::all_the_same;
11use derivative::Derivative;
12use derive_more::{Constructor, From, TryInto};
13use std::{fmt, rc::Rc};
14
15use super::prelude::*;
16use crate::dbl::{
17    discrete, discrete_tabulator, modal,
18    model::PrintableDblModel,
19    theory::{DblTheory, DblTheoryKind, NonUnital, Unital},
20};
21use crate::one::QualifiedPath;
22use crate::stdlib::theories;
23use crate::zero::{QualifiedName, name};
24
25/// A theory supported by DoubleTT, comprising a name and a definition.
26///
27/// Equality of these theories is nominal; two theories are the same if and only
28/// if they have the same name.
29#[derive(Constructor, Clone, Derivative)]
30#[derivative(PartialEq, Eq)]
31pub struct Theory {
32    /// The name of the theory.
33    pub name: QualifiedName,
34    /// The definition of the theory.
35    #[derivative(PartialEq = "ignore")]
36    pub definition: TheoryDef,
37}
38
39impl fmt::Display for Theory {
40    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
41        write!(f, "{}", self.name)
42    }
43}
44
45/// Definition of a double theory supported by DoubleTT.
46#[derive(Clone, From)]
47pub enum TheoryDef {
48    /// A discrete double theory.
49    Discrete(Rc<discrete::DiscreteDblTheory>),
50    /// A discrete tabulator theory.
51    DiscreteTab(Rc<discrete_tabulator::DiscreteTabTheory>),
52    /// A unital modal double theory.
53    ModalUnital(Rc<modal::ModalDblTheory<Unital>>),
54    /// A non-unital modal double theory.
55    ModalNonUnital(Rc<modal::ModalDblTheory<NonUnital>>),
56}
57
58impl TheoryDef {
59    /// Smart constructor for [`TheoryDef::Discrete`] case.
60    pub fn discrete(theory: discrete::DiscreteDblTheory) -> Self {
61        TheoryDef::Discrete(Rc::new(theory))
62    }
63
64    /// Smart constructor for [`TheoryDef::DiscreteTab`] case.
65    pub fn discrete_tab(theory: discrete_tabulator::DiscreteTabTheory) -> Self {
66        TheoryDef::DiscreteTab(Rc::new(theory))
67    }
68
69    /// Smart constructor for [`TheoryDef::ModalUnital`] case.
70    pub fn modal_unital(theory: modal::ModalDblTheory<Unital>) -> Self {
71        TheoryDef::ModalUnital(Rc::new(theory))
72    }
73
74    /// Smart constructor for [`TheoryDef::ModalNonUnital`] case.
75    pub fn modal_non_unital(theory: modal::ModalDblTheory<NonUnital>) -> Self {
76        TheoryDef::ModalNonUnital(Rc::new(theory))
77    }
78
79    /// Gets the basic object type with given name, if it exists.
80    pub fn basic_ob_type(&self, name: QualifiedName) -> Option<ObType> {
81        let ob_type = match self {
82            TheoryDef::Discrete(_) => ObType::Discrete(name),
83            TheoryDef::DiscreteTab(_) => ObType::DiscreteTab(name.into()),
84            TheoryDef::ModalUnital(_) | TheoryDef::ModalNonUnital(_) => {
85                ObType::Modal(modal::ModeApp::new(name))
86            }
87        };
88        all_the_same!(match self {
89            TheoryDef::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](th) => {
90                if th.has_ob_type((&ob_type).try_into().unwrap()) {
91                    Some(ob_type)
92                } else {
93                    None
94                }
95            }
96        })
97    }
98
99    /// Gets the basic morphism type with given name, if it exists.
100    pub fn basic_mor_type(&self, name: QualifiedName) -> Option<MorType> {
101        let mor_type = match self {
102            TheoryDef::Discrete(_) => MorType::Discrete(name.into()),
103            TheoryDef::DiscreteTab(_) => {
104                MorType::DiscreteTab(discrete_tabulator::TabMorType::Basic(name))
105            }
106            TheoryDef::ModalUnital(_) | TheoryDef::ModalNonUnital(_) => {
107                MorType::Modal(modal::ModeApp::new(name).into())
108            }
109        };
110        all_the_same!(match self {
111            TheoryDef::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](th) => {
112                if th.has_mor_type((&mor_type).try_into().unwrap()) {
113                    Some(mor_type)
114                } else {
115                    None
116                }
117            }
118        })
119    }
120
121    /// Gets the basic object operation with given name, if it exists.
122    pub fn basic_ob_op(&self, name: QualifiedName) -> Option<ObOp> {
123        match self {
124            TheoryDef::Discrete(_) | TheoryDef::DiscreteTab(_) => None,
125            TheoryDef::ModalUnital(th) => Self::basic_ob_op_modal(th, name),
126            TheoryDef::ModalNonUnital(th) => Self::basic_ob_op_modal(th, name),
127        }
128    }
129
130    fn basic_ob_op_modal<Kind: DblTheoryKind>(
131        th: &modal::ModalDblTheory<Kind>,
132        name: QualifiedName,
133    ) -> Option<ObOp> {
134        let op = modal::ModalObOp::generator(name);
135        if th.has_ob_op(&op) {
136            Some(ObOp::Modal(op))
137        } else {
138            None
139        }
140    }
141
142    /// Gets the source type of a morphism type.
143    pub fn src_type(&self, mor_type: &MorType) -> ObType {
144        all_the_same!(match self {
145            TheoryDef::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](th) => {
146                th.src_type(mor_type.try_into().unwrap()).into()
147            }
148        })
149    }
150
151    /// Gets the target type of a morphism type.
152    pub fn tgt_type(&self, mor_type: &MorType) -> ObType {
153        all_the_same!(match self {
154            TheoryDef::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](th) => {
155                th.tgt_type(mor_type.try_into().unwrap()).into()
156            }
157        })
158    }
159
160    /// Gets the hom (identity) type for an object type, if it exists.
161    pub fn hom_type(&self, ob_type: ObType) -> Option<MorType> {
162        match self {
163            TheoryDef::Discrete(th) => Some(th.hom_type(ob_type.try_into().unwrap()).into()),
164            TheoryDef::DiscreteTab(th) => Some(th.hom_type(ob_type.try_into().unwrap()).into()),
165            TheoryDef::ModalUnital(th) => Some(th.hom_type(ob_type.try_into().unwrap()).into()),
166            TheoryDef::ModalNonUnital(th) => {
167                th.hom_type(ob_type.try_into().unwrap()).map(|mt| mt.into())
168            }
169        }
170    }
171
172    /// Composes a pair of morphism types, if they have a composite.
173    pub fn compose_types2(&self, mt1: MorType, mt2: MorType) -> Option<MorType> {
174        all_the_same!(match self {
175            TheoryDef::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](th) => {
176                let path = Path::pair(mt1.try_into().unwrap(), mt2.try_into().unwrap());
177                th.compose_types(path).map(|mt| mt.into())
178            }
179        })
180    }
181
182    /// Gets the tabulator of a morphism type, if it exists.
183    pub fn tabulator(&self, mor_type: MorType) -> Option<ObType> {
184        match self {
185            TheoryDef::Discrete(_) => None,
186            TheoryDef::DiscreteTab(th) => Some(th.tabulator(mor_type.try_into().unwrap()).into()),
187            TheoryDef::ModalUnital(_) | TheoryDef::ModalNonUnital(_) => None,
188        }
189    }
190
191    /// Gets the domain of an object operation.
192    pub fn ob_op_dom(&self, ob_op: &ObOp) -> ObType {
193        all_the_same!(match self {
194            TheoryDef::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](th) => {
195                th.ob_op_dom(ob_op.try_into().unwrap()).into()
196            }
197        })
198    }
199
200    /// Gets the codomain of an object operation.
201    pub fn ob_op_cod(&self, ob_op: &ObOp) -> ObType {
202        all_the_same!(match self {
203            TheoryDef::[Discrete, DiscreteTab, ModalUnital, ModalNonUnital](th) => {
204                th.ob_op_cod(ob_op.try_into().unwrap()).into()
205            }
206        })
207    }
208}
209
210/// Object type in a double theory supported by DoubleTT.
211#[derive(Clone, Debug, From, TryInto, PartialEq, Eq)]
212#[try_into(owned, ref)]
213pub enum ObType {
214    /// Object type in a discrete theory.
215    Discrete(QualifiedName),
216    /// Object type in a discrete tabulator theory.
217    DiscreteTab(discrete_tabulator::TabObType),
218    /// Object type in a modal theory.
219    Modal(modal::ModalObType),
220}
221
222impl ObType {
223    /// Destructures a modality application, if possible.
224    pub fn mode_app(self) -> Option<(modal::Modality, ObType)> {
225        match self {
226            ObType::Discrete(_) | ObType::DiscreteTab(_) => None,
227            ObType::Modal(ob_type) => {
228                let (maybe_modality, ob_type) = ob_type.pop_app();
229                maybe_modality.map(|modality| (modality, ob_type.into()))
230            }
231        }
232    }
233
234    /// Gets the argument of a list modality application, if the type is one.
235    pub fn list_arg(self) -> Option<ObType> {
236        self.mode_app().and_then(|(modality, ob_type)| match modality {
237            modal::Modality::List(_) => Some(ob_type),
238            _ => None,
239        })
240    }
241}
242
243impl ToDoc for ObType {
244    fn to_doc<'a>(&self) -> D<'a> {
245        match self {
246            ObType::Discrete(name) => discrete::DiscreteDblModel::ob_type_to_doc(name),
247            ObType::DiscreteTab(name) => discrete_tabulator::DiscreteTabModel::ob_type_to_doc(name),
248            ObType::Modal(ob_type) => modal::ModalDblModel::<Unital>::ob_type_to_doc(ob_type),
249        }
250    }
251}
252
253impl fmt::Display for ObType {
254    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
255        write!(f, "{}", self.to_doc().group().pretty())
256    }
257}
258
259/// Morphism type in a double theory supported by DoubleTT.
260#[derive(Clone, Debug, From, TryInto, PartialEq, Eq)]
261#[try_into(owned, ref)]
262pub enum MorType {
263    /// Morphism type in a discrete theory.
264    Discrete(QualifiedPath),
265    /// Morphism type in a discrete tabulator theory.
266    DiscreteTab(discrete_tabulator::TabMorType),
267    /// Morphism type in a modal theory.
268    Modal(modal::ModalMorType),
269}
270
271impl ToDoc for MorType {
272    fn to_doc<'a>(&self) -> D<'a> {
273        match self {
274            MorType::Discrete(path) => discrete::DiscreteDblModel::mor_type_to_doc(path),
275            MorType::DiscreteTab(mor_type) => {
276                discrete_tabulator::DiscreteTabModel::mor_type_to_doc(mor_type)
277            }
278            MorType::Modal(mor_type) => modal::ModalDblModel::<Unital>::mor_type_to_doc(mor_type),
279        }
280    }
281}
282
283impl fmt::Display for MorType {
284    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
285        write!(f, "{}", self.to_doc().group().pretty())
286    }
287}
288
289/// Object operation in a double theory supported by DoubleTT.
290#[derive(Clone, Debug, TryInto)]
291#[try_into(owned, ref)]
292pub enum ObOp {
293    /// Object operation in a discrete theory: the identity on an object type.
294    Discrete(QualifiedName),
295    /// Object operation in a discrete tabulator theory.
296    DiscreteTab(discrete_tabulator::TabObOp),
297    /// Object operation in a modal theory.
298    Modal(modal::ModalObOp),
299}
300
301/// Construct a library of standard theories.
302pub fn std_theories() -> HashMap<QualifiedName, Theory> {
303    [
304        (name("ThSchema"), TheoryDef::discrete(theories::th_schema())),
305        (name("ThCategory"), TheoryDef::discrete(theories::th_category())),
306        (name("ThSignedCategory"), TheoryDef::discrete(theories::th_signed_category())),
307        (name("ThCategoryLinks"), TheoryDef::discrete_tab(theories::th_category_links())),
308        (name("ThMulticategory"), TheoryDef::modal_unital(theories::th_multicategory())),
309        (
310            name("ThSymMonoidalCategory"),
311            TheoryDef::modal_unital(theories::th_sym_monoidal_category()),
312        ),
313    ]
314    .into_iter()
315    .map(|(name, def)| (name.clone(), Theory::new(name, def)))
316    .collect()
317}
catlog/tt/theory.rs

catlog/tt/
theory.rs
