catlog/stdlib/
theory_morphisms.rs

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

catlog/stdlib/
theory_morphisms.rs
