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::{discrete, modal, model::PrintableDblModel, theory::DblTheory};
17use crate::one::QualifiedPath;
18use crate::stdlib::theories;
19use crate::zero::{QualifiedName, name};
20
21/// A theory supported by DoubleTT, comprising a name and a definition.
22///
23/// Equality of these theories is nominal; two theories are the same if and only
24/// if they have the same name.
25#[derive(Constructor, Clone, Derivative)]
26#[derivative(PartialEq, Eq)]
27pub struct Theory {
28    /// The name of the theory.
29    pub name: QualifiedName,
30    /// The definition of the theory.
31    #[derivative(PartialEq = "ignore")]
32    pub definition: TheoryDef,
33}
34
35impl fmt::Display for Theory {
36    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
37        write!(f, "{}", self.name)
38    }
39}
40
41/// Definition of a double theory supported by DoubleTT.
42#[derive(Clone, From)]
43pub enum TheoryDef {
44    /// A discrete double theory.
45    Discrete(Rc<discrete::DiscreteDblTheory>),
46    /// A modal double theory.
47    Modal(Rc<modal::ModalDblTheory>),
48}
49
50impl TheoryDef {
51    /// Smart constructor for [`TheoryDef::Discrete`] case.
52    pub fn discrete(theory: discrete::DiscreteDblTheory) -> Self {
53        TheoryDef::Discrete(Rc::new(theory))
54    }
55
56    /// Smart constructor for [`TheoryDef::Modal`] case.
57    pub fn modal(theory: modal::ModalDblTheory) -> Self {
58        TheoryDef::Modal(Rc::new(theory))
59    }
60
61    /// Gets the basic object type with given name, if it exists.
62    pub fn basic_ob_type(&self, name: QualifiedName) -> Option<ObType> {
63        let ob_type = match self {
64            TheoryDef::Discrete(_) => ObType::Discrete(name),
65            TheoryDef::Modal(_) => ObType::Modal(modal::ModeApp::new(name)),
66        };
67        all_the_same!(match self {
68            TheoryDef::[Discrete, Modal](th) => {
69                if th.has_ob_type((&ob_type).try_into().unwrap()) {
70                    Some(ob_type)
71                } else {
72                    None
73                }
74            }
75        })
76    }
77
78    /// Gets the basic morphism type with given name, if it exists.
79    pub fn basic_mor_type(&self, name: QualifiedName) -> Option<MorType> {
80        let mor_type = match self {
81            TheoryDef::Discrete(_) => MorType::Discrete(name.into()),
82            TheoryDef::Modal(_) => MorType::Modal(modal::ModeApp::new(name).into()),
83        };
84        all_the_same!(match self {
85            TheoryDef::[Discrete, Modal](th) => {
86                if th.has_mor_type((&mor_type).try_into().unwrap()) {
87                    Some(mor_type)
88                } else {
89                    None
90                }
91            }
92        })
93    }
94
95    /// Gets the basic object operation with given name, if it exists.
96    pub fn basic_ob_op(&self, name: QualifiedName) -> Option<ObOp> {
97        match self {
98            TheoryDef::Discrete(_) => None,
99            TheoryDef::Modal(th) => {
100                let op = modal::ModalObOp::generator(name);
101                if th.has_ob_op(&op) {
102                    Some(ObOp::Modal(op))
103                } else {
104                    None
105                }
106            }
107        }
108    }
109
110    /// Gets the source type of a morphism type.
111    pub fn src_type(&self, mor_type: &MorType) -> ObType {
112        all_the_same!(match self {
113            TheoryDef::[Discrete, Modal](th) => {
114                th.src_type(mor_type.try_into().unwrap()).into()
115            }
116        })
117    }
118
119    /// Gets the target type of a morphism type.
120    pub fn tgt_type(&self, mor_type: &MorType) -> ObType {
121        all_the_same!(match self {
122            TheoryDef::[Discrete, Modal](th) => {
123                th.tgt_type(mor_type.try_into().unwrap()).into()
124            }
125        })
126    }
127
128    /// Gets the hom (identity) type for an object type.
129    pub fn hom_type(&self, ob_type: ObType) -> MorType {
130        all_the_same!(match self {
131            TheoryDef::[Discrete, Modal](th) => {
132                th.hom_type(ob_type.try_into().unwrap()).into()
133            }
134        })
135    }
136
137    /// Composes a pair of morphism types, if they have a composite.
138    pub fn compose_types2(&self, mt1: MorType, mt2: MorType) -> Option<MorType> {
139        all_the_same!(match self {
140            TheoryDef::[Discrete, Modal](th) => {
141                let path = Path::pair(mt1.try_into().unwrap(), mt2.try_into().unwrap());
142                th.compose_types(path).map(|mt| mt.into())
143            }
144        })
145    }
146
147    /// Gets the domain of an object operation.
148    pub fn ob_op_dom(&self, ob_op: &ObOp) -> ObType {
149        all_the_same!(match self {
150            TheoryDef::[Discrete, Modal](th) => {
151                th.ob_op_dom(ob_op.try_into().unwrap()).into()
152            }
153        })
154    }
155
156    /// Gets the codomain of an object operation.
157    pub fn ob_op_cod(&self, ob_op: &ObOp) -> ObType {
158        all_the_same!(match self {
159            TheoryDef::[Discrete, Modal](th) => {
160                th.ob_op_cod(ob_op.try_into().unwrap()).into()
161            }
162        })
163    }
164}
165
166/// Object type in a double theory supported by DoubleTT.
167#[derive(Clone, Debug, From, TryInto, PartialEq, Eq)]
168#[try_into(owned, ref)]
169pub enum ObType {
170    /// Object type in a discrete theory.
171    Discrete(QualifiedName),
172    /// Object type in a modal theory.
173    Modal(modal::ModalObType),
174}
175
176impl ObType {
177    /// Destructures a modality application, if possible.
178    pub fn mode_app(self) -> Option<(modal::Modality, ObType)> {
179        match self {
180            ObType::Discrete(_) => None,
181            ObType::Modal(ob_type) => {
182                let (maybe_modality, ob_type) = ob_type.pop_app();
183                maybe_modality.map(|modality| (modality, ob_type.into()))
184            }
185        }
186    }
187
188    /// Gets the argument of a list modality application, if the type is one.
189    pub fn list_arg(self) -> Option<ObType> {
190        self.mode_app().and_then(|(modality, ob_type)| match modality {
191            modal::Modality::List(_) => Some(ob_type),
192            _ => None,
193        })
194    }
195}
196
197impl ToDoc for ObType {
198    fn to_doc<'a>(&self) -> D<'a> {
199        match self {
200            ObType::Discrete(name) => discrete::DiscreteDblModel::ob_type_to_doc(name),
201            ObType::Modal(ob_type) => modal::ModalDblModel::ob_type_to_doc(ob_type),
202        }
203    }
204}
205
206impl fmt::Display for ObType {
207    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
208        write!(f, "{}", self.to_doc().group().pretty())
209    }
210}
211
212/// Morphism type in a double theory supported by DoubleTT.
213#[derive(Clone, Debug, From, TryInto, PartialEq, Eq)]
214#[try_into(owned, ref)]
215pub enum MorType {
216    /// Morphism type in a discrete theory.
217    Discrete(QualifiedPath),
218    /// Morphism type in a model theory.
219    Modal(modal::ModalMorType),
220}
221
222impl ToDoc for MorType {
223    fn to_doc<'a>(&self) -> D<'a> {
224        match self {
225            MorType::Discrete(path) => discrete::DiscreteDblModel::mor_type_to_doc(path),
226            MorType::Modal(mor_type) => modal::ModalDblModel::mor_type_to_doc(mor_type),
227        }
228    }
229}
230
231impl fmt::Display for MorType {
232    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
233        write!(f, "{}", self.to_doc().group().pretty())
234    }
235}
236
237/// Object operation in a double theory supported by DoubleTT.
238#[derive(Clone, Debug, TryInto)]
239#[try_into(owned, ref)]
240pub enum ObOp {
241    /// Object operation in a discrete theory: the identity on an object type.
242    Discrete(QualifiedName),
243    /// Object operation in a modal theory.
244    Modal(modal::ModalObOp),
245}
246
247/// Construct a library of standard theories.
248pub fn std_theories() -> HashMap<QualifiedName, Theory> {
249    [
250        (name("ThSchema"), TheoryDef::discrete(theories::th_schema())),
251        (name("ThCategory"), TheoryDef::discrete(theories::th_category())),
252        (name("ThSignedCategory"), TheoryDef::discrete(theories::th_signed_category())),
253        (name("ThMulticategory"), TheoryDef::modal(theories::th_multicategory())),
254        (
255            name("ThSymMonoidalCategory"),
256            TheoryDef::modal(theories::th_sym_monoidal_category()),
257        ),
258    ]
259    .into_iter()
260    .map(|(name, def)| (name.clone(), Theory::new(name, def)))
261    .collect()
262}
catlog/tt/theory.rs

catlog/tt/
theory.rs
