catlog_wasm/
theory.rs

1//! Wasm bindings for double theories.
2
3use std::collections::HashMap;
4use std::rc::Rc;
5
6use all_the_same::all_the_same;
7use derive_more::{From, TryInto};
8use ustr::Ustr;
9
10use wasm_bindgen::prelude::*;
11
12use catlog::dbl::theory::{
13    self, DblTheory as _, ModalMorType, ModalObOp, ModalObType, ModalOp, ModeApp, TabMorType,
14    TabObOp, TabObType,
15};
16use catlog::one::{Path, QualifiedPath, ShortPath};
17use catlog::zero::{NameSegment, QualifiedName};
18use notebook_types::current::theory::*;
19
20use super::notation::*;
21
22/// Elaborates into object type in a discrete double theory.
23impl CanElaborate<ObType, QualifiedName> for Elaborator {
24    fn elab(&self, ob_type: &ObType) -> Result<QualifiedName, String> {
25        match ob_type {
26            ObType::Basic(id) => Ok((*id).into()),
27            _ => Err(format!("Cannot use object type in discrete double theory: {ob_type:#?}")),
28        }
29    }
30}
31
32/// Elaborates into morphism type in a discrete double theory.
33impl CanElaborate<MorType, QualifiedPath> for Elaborator {
34    fn elab(&self, mor_type: &MorType) -> Result<QualifiedPath, String> {
35        match mor_type {
36            MorType::Basic(id) => Ok(Path::single((*id).into())),
37            MorType::Composite(fs) => {
38                let fs: Result<Vec<_>, _> = fs.iter().map(|f| self.elab(f)).collect();
39                let path = Path::from_vec(fs?).ok_or("Composite should not be empty")?;
40                Ok(path.flatten())
41            }
42            MorType::Hom(ob_type) => Ok(Path::Id(self.elab(ob_type.as_ref())?)),
43            _ => Err(format!("Cannot use morphsim type in discrete double theory: {mor_type:#?}")),
44        }
45    }
46}
47
48/// Elaborates into object operation in a discrete double theory.
49impl CanElaborate<ObOp, QualifiedName> for Elaborator {
50    fn elab(&self, op: &ObOp) -> Result<QualifiedName, String> {
51        match op {
52            ObOp::Id(ObType::Basic(id)) => Ok((*id).into()),
53            _ => Err(format!("Cannot use operation in discrete double theory: {op:#?}")),
54        }
55    }
56}
57
58/// Elaborates into object type in a discrete tabulator theory.
59impl CanElaborate<ObType, TabObType> for Elaborator {
60    fn elab(&self, ob_type: &ObType) -> Result<TabObType, String> {
61        match ob_type {
62            ObType::Basic(id) => Ok(TabObType::Basic((*id).into())),
63            ObType::Tabulator(mor_type) => {
64                Ok(TabObType::Tabulator(Box::new(self.elab(mor_type.as_ref())?)))
65            }
66            _ => Err(format!("Cannot use object type in discrete tabulator theory: {ob_type:#?}")),
67        }
68    }
69}
70
71/// Elaborates into morphism type in a discrete tabulator theory.
72impl CanElaborate<MorType, TabMorType> for Elaborator {
73    fn elab(&self, mor_type: &MorType) -> Result<TabMorType, String> {
74        match mor_type {
75            MorType::Basic(id) => Ok(TabMorType::Basic((*id).into())),
76            MorType::Composite(_) => {
77                Err("Composites not yet implemented for tabulator theories".into())
78            }
79            MorType::Hom(ob_type) => Ok(TabMorType::Hom(Box::new(self.elab(ob_type.as_ref())?))),
80            _ => {
81                Err(format!("Cannot use morphism type in discrete tabulator theory: {mor_type:#?}"))
82            }
83        }
84    }
85}
86
87/// Elaborates into object operation in a discrete tabulator theory.
88impl CanElaborate<ObOp, TabObOp> for Elaborator {
89    fn elab(&self, op: &ObOp) -> Result<TabObOp, String> {
90        match op {
91            ObOp::Id(ob_type) => Ok(Path::empty(self.elab(ob_type)?)),
92            _ => Err(format!("Cannot use operation in discrete tabulator theory: {op:#?}")),
93        }
94    }
95}
96
97/// Elaborates into object type in a modal double theory.
98impl CanElaborate<ObType, ModalObType> for Elaborator {
99    fn elab(&self, ob_type: &ObType) -> Result<ModalObType, String> {
100        match ob_type {
101            ObType::Basic(id) => Ok(ModeApp::new((*id).into())),
102            ObType::ModeApp { modality, ob_type } => Ok({
103                let ob_type: ModalObType = self.elab(ob_type.as_ref())?;
104                ob_type.apply(promote_modality(*modality))
105            }),
106            _ => Err(format!("Cannot use object type in modal theory: {ob_type:#?}")),
107        }
108    }
109}
110
111/// Elaborates into morphism type in a modal double theory.
112impl CanElaborate<MorType, ModalMorType> for Elaborator {
113    fn elab(&self, mor_type: &MorType) -> Result<ModalMorType, String> {
114        match mor_type {
115            MorType::Basic(id) => Ok(ModeApp::new((*id).into()).into()),
116            MorType::Hom(ob_type) => Ok(ShortPath::Zero(self.elab(ob_type.as_ref())?)),
117            MorType::ModeApp { modality, mor_type } => Ok({
118                let mor_type: ModalMorType = self.elab(mor_type.as_ref())?;
119                mor_type.apply(promote_modality(*modality))
120            }),
121            _ => Err(format!("Cannot use morphism type in modal theory: {mor_type:#?}")),
122        }
123    }
124}
125
126/// Elaborates into an object operation in a modal double theory.
127impl CanElaborate<ObOp, ModalObOp> for Elaborator {
128    fn elab(&self, op: &ObOp) -> Result<ModalObOp, String> {
129        match op {
130            ObOp::Basic(id) => Ok(ModeApp::new(ModalOp::Generator((*id).into())).into()),
131            ObOp::Id(ob_type) => Ok(Path::empty(self.elab(ob_type)?)),
132            ObOp::Composite(ops) => {
133                let ops: Result<Vec<_>, _> = ops.iter().map(|op| self.elab(op)).collect();
134                Ok(Path::from_vec(ops?).ok_or("Composite should be non-empty")?.flatten())
135            }
136            ObOp::ModeApp { modality, op } => Ok({
137                let op: ModalObOp = self.elab(op.as_ref())?;
138                op.apply(promote_modality(*modality))
139            }),
140        }
141    }
142}
143
144pub(crate) fn promote_modality(modality: Modality) -> theory::Modality {
145    match modality {
146        Modality::Discrete => theory::Modality::Discrete(),
147        Modality::Codiscrete => theory::Modality::Codiscrete(),
148        Modality::List => theory::Modality::List(theory::List::Plain),
149        Modality::SymmetricList => theory::Modality::List(theory::List::Symmetric),
150        Modality::ProductList => theory::Modality::List(theory::List::Product),
151        Modality::CoproductList => theory::Modality::List(theory::List::Coproduct),
152        Modality::BiproductList => theory::Modality::List(theory::List::Biproduct),
153    }
154}
155
156pub(crate) fn expect_single_name(name: &QualifiedName) -> Ustr {
157    match name.only() {
158        Some(NameSegment::Text(text)) => text,
159        _ => panic!("Only singleton names are currently supported in notebook types"),
160    }
161}
162
163/// Quotes an object type in a discrete double theory.
164impl CanQuote<QualifiedName, ObType> for Quoter {
165    fn quote(&self, name: &QualifiedName) -> ObType {
166        ObType::Basic(expect_single_name(name))
167    }
168}
169
170/// Quotes a morphism type in a discrete double theory.
171impl CanQuote<QualifiedPath, MorType> for Quoter {
172    fn quote(&self, path: &QualifiedPath) -> MorType {
173        match path {
174            Path::Id(v) => MorType::Hom(Box::new(ObType::Basic(expect_single_name(v)))),
175            Path::Seq(edges) => {
176                if edges.len() == 1 {
177                    MorType::Basic(expect_single_name(&edges.head))
178                } else {
179                    MorType::Composite(
180                        edges.iter().map(|e| MorType::Basic(expect_single_name(e))).collect(),
181                    )
182                }
183            }
184        }
185    }
186}
187
188/// Quotes an object operation in a discrete double theory.
189impl CanQuote<QualifiedName, ObOp> for Quoter {
190    fn quote(&self, name: &QualifiedName) -> ObOp {
191        ObOp::Id(ObType::Basic(expect_single_name(name)))
192    }
193}
194
195/// Quotes an object type in a discrete tabulator theory.
196impl CanQuote<TabObType, ObType> for Quoter {
197    fn quote(&self, ob_type: &TabObType) -> ObType {
198        match ob_type {
199            TabObType::Basic(name) => ObType::Basic(expect_single_name(name)),
200            TabObType::Tabulator(mor_type) => {
201                ObType::Tabulator(Box::new(self.quote(mor_type.as_ref())))
202            }
203        }
204    }
205}
206
207/// Quotes a morphism type in a discrete tabulator theory.
208impl CanQuote<TabMorType, MorType> for Quoter {
209    fn quote(&self, mor_type: &TabMorType) -> MorType {
210        match mor_type {
211            TabMorType::Basic(name) => MorType::Basic(expect_single_name(name)),
212            TabMorType::Hom(ob_type) => MorType::Hom(Box::new(self.quote(ob_type.as_ref()))),
213        }
214    }
215}
216
217/// Quotes an object type in a modal theory.
218impl CanQuote<ModalObType, ObType> for Quoter {
219    fn quote(&self, app: &ModalObType) -> ObType {
220        let mut quoted = ObType::Basic(expect_single_name(&app.arg));
221        for modality in &app.modalities {
222            quoted = ObType::ModeApp {
223                modality: demote_modality(*modality),
224                ob_type: quoted.into(),
225            }
226        }
227        quoted
228    }
229}
230
231/// Quotes a morphism type in a modal theory.
232impl CanQuote<ModalMorType, MorType> for Quoter {
233    fn quote(&self, mor_type: &ModalMorType) -> MorType {
234        match mor_type {
235            ShortPath::Zero(ob_type) => MorType::Hom(Box::new(self.quote(ob_type))),
236            ShortPath::One(app) => {
237                let mut quoted = MorType::Basic(expect_single_name(&app.arg));
238                for modality in &app.modalities {
239                    quoted = MorType::ModeApp {
240                        modality: demote_modality(*modality),
241                        mor_type: quoted.into(),
242                    }
243                }
244                quoted
245            }
246        }
247    }
248}
249
250pub(crate) fn demote_modality(modality: theory::Modality) -> Modality {
251    match modality {
252        theory::Modality::Discrete() => Modality::Discrete,
253        theory::Modality::Codiscrete() => Modality::Codiscrete,
254        theory::Modality::List(list_type) => match list_type {
255            theory::List::Plain => Modality::List,
256            theory::List::Symmetric => Modality::SymmetricList,
257            theory::List::Product => Modality::ProductList,
258            theory::List::Coproduct => Modality::CoproductList,
259            theory::List::Biproduct => Modality::BiproductList,
260        },
261    }
262}
263
264/** A box containing a double theory of any kind.
265
266Ideally the Wasm-bound [`DblTheory`] would just have a type parameter for the
267underlying double theory, but `wasm-bindgen` does not support
268[generics](https://github.com/rustwasm/wasm-bindgen/issues/3309). Instead, we
269explicitly enumerate the supported kinds of double theories in this enum.
270 */
271#[derive(From, TryInto)]
272#[try_into(ref)]
273pub enum DblTheoryBox {
274    /// A discrete double theory.
275    Discrete(Rc<theory::DiscreteDblTheory>),
276    /// A discrete tabulator theory.
277    DiscreteTab(Rc<theory::DiscreteTabTheory>),
278    /// A modal double theory.
279    Modal(Rc<theory::ModalDblTheory>),
280}
281
282/// Wasm binding for a double theory.
283#[wasm_bindgen]
284pub struct DblTheory(#[wasm_bindgen(skip)] pub DblTheoryBox);
285
286impl DblTheory {
287    /// Tries to get a discrete double theory.
288    pub fn discrete(&self) -> Result<&Rc<theory::DiscreteDblTheory>, String> {
289        (&self.0).try_into().map_err(|_| "Theory should be discrete".into())
290    }
291}
292
293#[wasm_bindgen]
294impl DblTheory {
295    /// Gets the source of a morphism type.
296    #[wasm_bindgen]
297    pub fn src(&self, mor_type: MorType) -> Result<ObType, String> {
298        all_the_same!(match &self.0 {
299            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
300                let mor_type = Elaborator.elab(&mor_type)?;
301                Ok(Quoter.quote(&th.src_type(&mor_type)))
302            }
303        })
304    }
305
306    /// Gets the target of a morphism type.
307    #[wasm_bindgen]
308    pub fn tgt(&self, mor_type: MorType) -> Result<ObType, String> {
309        all_the_same!(match &self.0 {
310            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
311                let mor_type = Elaborator.elab(&mor_type)?;
312                Ok(Quoter.quote(&th.tgt_type(&mor_type)))
313            }
314        })
315    }
316
317    /// Gets the domain of an object operation.
318    #[wasm_bindgen]
319    pub fn dom(&self, op: ObOp) -> Result<ObType, String> {
320        all_the_same!(match &self.0 {
321            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
322                let op = Elaborator.elab(&op)?;
323                Ok(Quoter.quote(&th.ob_op_dom(&op)))
324            }
325        })
326    }
327
328    /// Gets the codomain of an object operation.
329    #[wasm_bindgen]
330    pub fn cod(&self, op: ObOp) -> Result<ObType, String> {
331        all_the_same!(match &self.0 {
332            DblTheoryBox::[Discrete, DiscreteTab, Modal](th) => {
333                let op = Elaborator.elab(&op)?;
334                Ok(Quoter.quote(&th.ob_op_cod(&op)))
335            }
336        })
337    }
338}
339
340/** Mapping from object types to numerical indices.
341
342Like [`MorTypeIndex`], this struct just compensates for the lack of hash maps
343with arbitrary keys in JavaScript.
344 */
345#[wasm_bindgen]
346#[derive(Clone, Default)]
347pub struct ObTypeIndex(HashMap<ObType, usize>);
348
349#[wasm_bindgen]
350impl ObTypeIndex {
351    /// Creates a new object type index.
352    #[wasm_bindgen(constructor)]
353    pub fn new() -> Self {
354        Default::default()
355    }
356
357    /// Gets the index of an object type, if set.
358    #[wasm_bindgen]
359    pub fn get(&self, x: &ObType) -> Option<usize> {
360        self.0.get(x).copied()
361    }
362
363    /// Sets the index of an object type.
364    #[wasm_bindgen]
365    pub fn set(&mut self, x: ObType, i: usize) {
366        self.0.insert(x, i);
367    }
368}
369
370/** Mapping from morphism types to numerical indices.
371
372Like [`ObTypeIndex`], this struct just compensates for the lack of hash maps
373with arbitrary keys in JavaScript.
374 */
375#[wasm_bindgen]
376#[derive(Clone, Default)]
377pub struct MorTypeIndex(HashMap<MorType, usize>);
378
379#[wasm_bindgen]
380impl MorTypeIndex {
381    /// Creates a new morphism type index.
382    #[wasm_bindgen(constructor)]
383    pub fn new() -> Self {
384        Default::default()
385    }
386
387    /// Gets the index of a morphism type, if set.
388    #[wasm_bindgen]
389    pub fn get(&self, m: &MorType) -> Option<usize> {
390        self.0.get(m).copied()
391    }
392
393    /// Sets the index of a morphism type.
394    #[wasm_bindgen]
395    pub fn set(&mut self, m: MorType, i: usize) {
396        self.0.insert(m, i);
397    }
398}
catlog_wasm/theory.rs

catlog_wasm/
theory.rs
