catlog/dbl/modal/
model_instance.rs

1//! Instances of models of a modal double theory.
2
3use crate::dbl::model_instance::{DblModelInstance, HasInstanceTerm, InstanceTerm};
4use crate::dbl::theory::DblTheoryKind;
5use crate::one::path::Path;
6use crate::zero::QualifiedName;
7
8use super::model::{ModalDblModel, ModalMor, ModalOb};
9use super::theory::List;
10
11/// A term in an instance of a modal double model: a single model morphism
12/// applied to a base built from instance generators.
13///
14/// As in the discrete case, composition of model morphisms is reflected
15/// inside [`mor`](Self::mor) itself — via [`ModalMor::Composite`] for
16/// sequential composition and [`ModalMor::List`] for list-tupling — rather
17/// than by nesting term constructors. A tree-shaped multicategory composite
18/// such as `f([g(x), y])` therefore normalizes to *one* [`ModalMor`] applied
19/// *once* to a base of bare generators; applications never nest. When `mor`
20/// is the identity (`ModalMor::Composite(Path::Id(ob))`), the term denotes
21/// `base` directly, and that `Id` object must agree with the fiber of `base`
22/// in the surrounding instance.
23///
24/// The only recursion that survives lives in [`base`](Self::base), through
25/// [`ModalInstanceBase::List`] (mirroring [`ModalOb::List`]) and
26/// [`ModalInstanceBase::ObApp`] (mirroring [`ModalOb::App`]): this is what
27/// lets a generator over a nested list object be written inline as e.g.
28/// `[x, y]`, or an element of a product object as `@tensor [x, y]`. A base
29/// holds only generators, lists, and object-operation applications — never a
30/// morphism — so the "no application inside an application" invariant is
31/// enforced structurally.
32#[derive(Clone, Debug, PartialEq, Eq)]
33pub struct ModalInstanceTerm {
34    /// Model morphism applied to `base`.
35    pub mor: ModalMor,
36    /// The base of instance generators at the root of the term.
37    pub base: ModalInstanceBase,
38}
39
40/// The base of a [`ModalInstanceTerm`]: instance generators, tupled into
41/// lists to match list-shaped fibers.
42#[derive(Clone, Debug, PartialEq, Eq)]
43pub enum ModalInstanceBase {
44    /// A single instance generator.
45    Generator(QualifiedName),
46    /// A list of bases in a [list modality](List), living over a
47    /// [list object](super::model::ModalOb::List).
48    List(List, Vec<ModalInstanceBase>),
49    /// An object operation applied to a base, e.g. `@tensor [x, y]`, living
50    /// over an [object-operation application](super::model::ModalOb::App).
51    /// Object operations are functorial actions on objects, not morphisms, so
52    /// this stays in the base rather than in the term's morphism.
53    ObApp(QualifiedName, Box<ModalInstanceBase>),
54}
55
56impl InstanceTerm for ModalInstanceTerm {
57    type Mor = ModalMor;
58}
59
60impl<Kind: DblTheoryKind> HasInstanceTerm for ModalDblModel<Kind> {
61    type Term = ModalInstanceTerm;
62}
63
64/// An instance of a model of a modal double theory.
65pub type ModalDblModelInstance<Kind> = DblModelInstance<ModalDblModel<Kind>>;
66
67/// If `mor` is an identity morphism (`Composite(Path::Id(ob))`), returns the
68/// object it is the identity on.
69///
70/// Instance-term normalization uses this to keep terms in their flat normal
71/// form: an identity `mor` means the term denotes its [`base`](ModalInstanceTerm::base)
72/// directly, so a nested application whose argument is a pure base of
73/// generators need not introduce a `Composite`/`List` wrapper.
74pub fn modal_mor_as_identity(mor: &ModalMor) -> Option<&ModalOb> {
75    match mor {
76        ModalMor::Composite(path) => match path.as_ref() {
77            Path::Id(ob) => Some(ob),
78            _ => None,
79        },
80        _ => None,
81    }
82}
catlog/dbl/modal/model_instance.rs

catlog/dbl/modal/
model_instance.rs
