catlog/stdlib/
theory_morphisms.rs

1//! Standard library of morphisms between double theories.
2//!
3//! These can be used to migrate models from one theory to another.
4
5use crate::one::{FpFunctorData, Path, QualifiedPath};
6use crate::zero::{HashColumn, QualifiedName, name};
7
8type DiscreteDblTheoryMap = FpFunctorData<
9    HashColumn<QualifiedName, QualifiedName>,
10    HashColumn<QualifiedName, QualifiedPath>,
11>;
12
13/// Map from theory of categories to the theories of schemas.
14///
15/// Sigma migration along this map sends objects in a category to entity types in a
16/// schema, yielding a schema with no attributes or attribute types.
17pub fn th_category_to_schema() -> DiscreteDblTheoryMap {
18    FpFunctorData::new(
19        HashColumn::from_iter([(name("Object"), name("Entity"))]),
20        HashColumn::default(),
21    )
22}
23
24/// Map from theory of schemas to theory of categories.
25///
26/// Sigma migration along this map erases the distinction between entity types and
27/// attribute types, turning both into objects in a category.
28pub fn th_schema_to_category() -> DiscreteDblTheoryMap {
29    FpFunctorData::new(
30        HashColumn::from_iter([
31            (name("Entity"), name("Object")),
32            (name("AttrType"), name("Object")),
33        ]),
34        HashColumn::from_iter([(name("Attr"), Path::Id(name("Object")))]),
35    )
36}
37
38/// Projection from theory of delayable signed categories.
39///
40/// Sigma migration along this map forgets about the delays.
41pub fn th_delayable_signed_category_to_signed_category() -> DiscreteDblTheoryMap {
42    FpFunctorData::new(
43        HashColumn::from_iter([(name("Object"), name("Object"))]),
44        HashColumn::from_iter([
45            (name("Negative"), name("Negative").into()),
46            (name("Slow"), Path::Id(name("Object"))),
47            // TODO: Shouldn't have to define on these superfluous generators.
48            (name("PositiveSlow"), Path::Id(name("Object"))),
49            (name("NegativeSlow"), name("Negative").into()),
50        ]),
51    )
52}
53
54#[cfg(test)]
55mod tests {
56    use super::super::theories::*;
57    use super::*;
58
59    #[test]
60    fn discrete_theory_morphisms() {
61        let (th_cat, th_sch) = (th_category().0, th_schema().0);
62        assert!(th_category_to_schema().functor_into(&th_sch).validate_on(&th_cat).is_ok());
63        assert!(th_schema_to_category().functor_into(&th_cat).validate_on(&th_sch).is_ok());
64
65        assert!(
66            th_delayable_signed_category_to_signed_category()
67                .functor_into(&th_signed_category().0)
68                .validate_on(&th_delayable_signed_category().0)
69                .is_ok()
70        );
71    }
72}
catlog/stdlib/theory_morphisms.rs

catlog/stdlib/
theory_morphisms.rs
