catcolab_document_types/v0/
model.rs

1use serde::{Deserialize, Serialize};
2use tsify::Tsify;
3
4use super::{path::Path, theory::*};
5
6/// An object in a model of a double theory.
7#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
8#[serde(tag = "tag", content = "content")]
9#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
10pub enum Ob {
11    /// Basic or generating object.
12    Basic(String),
13
14    /// Application of an object operation to another object.
15    App { op: ObOp, ob: Box<Ob> },
16
17    /// List of objects, each possibly ill-defined, in a list modality.
18    List {
19        modality: Modality,
20        objects: Vec<Option<Ob>>,
21    },
22
23    /// Morphism viewed as an object of a tabulator.
24    Tabulated(Mor),
25}
26
27/// A morphism in a model of a double theory.
28#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
29#[serde(tag = "tag", content = "content")]
30#[tsify(into_wasm_abi, from_wasm_abi)]
31pub enum Mor {
32    /// Basic or generating morphism.
33    Basic(String),
34
35    /// Composite of morphisms.
36    Composite(Box<Path<Ob, Mor>>),
37
38    /// Morphism between tabulated morphisms, a commutative square.
39    TabulatorSquare {
40        dom: Box<Mor>,
41        cod: Box<Mor>,
42        pre: Box<Mor>,
43        post: Box<Mor>,
44    },
45}
46
47/// Arbitrary instances for property-based testing.
48#[cfg(feature = "property-tests")]
49pub(crate) mod arbitrary {
50    use super::*;
51    use crate::v0::path::arbitrary::arb_path;
52    use proptest::prelude::*;
53
54    /// Strategy for an `Ob` bounded by recursion depth.
55    pub fn arb_ob(depth: u32) -> BoxedStrategy<Ob> {
56        let leaf = any::<String>().prop_map(Ob::Basic);
57        if depth == 0 {
58            return leaf.boxed();
59        }
60        prop_oneof![
61            3 => leaf,
62            1 => (any::<ObOp>(), arb_ob(depth - 1))
63                .prop_map(|(op, ob)| Ob::App { op, ob: Box::new(ob) }),
64            1 => (any::<Modality>(), prop::collection::vec(
65                    proptest::option::of(arb_ob(depth - 1)), 0..3))
66                .prop_map(|(modality, objects)| Ob::List { modality, objects }),
67            1 => arb_mor(depth - 1).prop_map(Ob::Tabulated),
68        ]
69        .boxed()
70    }
71
72    /// Strategy for a `Mor` bounded by recursion depth.
73    pub fn arb_mor(depth: u32) -> BoxedStrategy<Mor> {
74        let leaf = any::<String>().prop_map(Mor::Basic);
75        if depth == 0 {
76            return leaf.boxed();
77        }
78        prop_oneof![
79            3 => leaf,
80            1 => arb_path(arb_ob(depth - 1), arb_mor(depth - 1))
81                .prop_map(|p| Mor::Composite(Box::new(p))),
82            1 => (arb_mor(depth - 1), arb_mor(depth - 1),
83                   arb_mor(depth - 1), arb_mor(depth - 1))
84                .prop_map(|(dom, cod, pre, post)| Mor::TabulatorSquare {
85                    dom: Box::new(dom),
86                    cod: Box::new(cod),
87                    pre: Box::new(pre),
88                    post: Box::new(post),
89                }),
90        ]
91        .boxed()
92    }
93
94    impl Arbitrary for Ob {
95        type Parameters = ();
96        type Strategy = BoxedStrategy<Self>;
97
98        fn arbitrary_with(_: Self::Parameters) -> Self::Strategy {
99            arb_ob(2).boxed()
100        }
101    }
102
103    impl Arbitrary for Mor {
104        type Parameters = ();
105        type Strategy = BoxedStrategy<Self>;
106
107        fn arbitrary_with(_: Self::Parameters) -> Self::Strategy {
108            arb_mor(2).boxed()
109        }
110    }
111}
catcolab_document_types/v0/model.rs

catcolab_document_types/v0/
model.rs
