catlog/dbl/
model_instance.rs

1//! Instances of models of a double theory.
2//!
3//! An **instance** of a model (see [Carlson-Patterson 2025](https://arxiv.org/abs/2510.08861))
4//! is here presented via
5//! a set of generators living over each object of the model, together with
6//! equations between terms built from morphisms of the model applied to
7//! those generators. Crucially, the
8//! lift targets and lift morphisms forced by the discrete-opfibration
9//! condition may be used in equations but are *not* materialized as explicit generators.
10//!
11//! The term language is left to each doctrine to define, via the
12//! [`InstanceTerm`] trait and the [`HasInstanceTerm`] extension on
13//! [`DblModel`]. Discrete doctrines need only bare generators
14//! and morphism applications; modal doctrines additionally allow list
15//! terms to feed list-shaped morphism domains.
16//!
17//! For the related but distinct notion of a *diagram* in a model — a
18//! morphism into the model from a free model — see
19//! [`model_diagram`](super::model_diagram).
20
21use std::rc::Rc;
22
23use super::model::DblModel;
24use crate::zero::{Column, HashColumn, MutMapping, QualifiedName};
25
26/// A term in the language of an instance of some model.
27///
28/// Each doctrine implements its own concrete term type. The associated
29/// [`Mor`](Self::Mor) type ties the term language to a particular
30/// model's morphism type.
31pub trait InstanceTerm {
32    /// The type of morphisms from the associated model.
33    type Mor;
34}
35
36/// A [`DblModel`] that has an associated term language for instances.
37///
38/// Each doctrine that wants to support [`DblModelInstance`] declares its
39/// term type here.
40pub trait HasInstanceTerm: DblModel {
41    /// The kind of term used to express equations in instances of this
42    /// model.
43    type Term: InstanceTerm<Mor = Self::Mor>;
44}
45
46/// An instance of a model: a fibered set of generators plus equations
47/// between terms in the model's instance-term language.
48///
49/// Owns the generator-to-fiber assignment and the equations, but does
50/// not own the model itself (held behind an [`Rc`], matching how models
51/// reference their theories).
52pub struct DblModelInstance<M: HasInstanceTerm> {
53    model: Rc<M>,
54    /// For each instance generator, the model object it lives over.
55    /// Multiple generators may share a fiber.
56    fibers: HashColumn<QualifiedName, M::Ob>,
57    /// Equations between terms, asserted to hold in this instance.
58    equations: Vec<(M::Term, M::Term)>,
59}
60
61impl<M: HasInstanceTerm> DblModelInstance<M> {
62    /// Creates an empty instance over the given model.
63    pub fn new(model: Rc<M>) -> Self {
64        Self {
65            model,
66            fibers: Default::default(),
67            equations: Vec::new(),
68        }
69    }
70
71    /// The model this is an instance of.
72    pub fn model(&self) -> &Rc<M> {
73        &self.model
74    }
75
76    /// Adds a generator living over the given object of the model.
77    pub fn add_generator(&mut self, name: QualifiedName, fiber: M::Ob) {
78        self.fibers.set(name, fiber);
79    }
80
81    /// The model object that `name` lives over, if `name` is a generator
82    /// of this instance.
83    pub fn fiber_of(&self, name: &QualifiedName) -> Option<&M::Ob> {
84        self.fibers.get(name)
85    }
86
87    /// Iterates over the instance generators and their fibers.
88    pub fn generators(&self) -> impl Iterator<Item = (QualifiedName, &M::Ob)> {
89        self.fibers.iter()
90    }
91
92    /// Adds an equation between two terms.
93    pub fn add_equation(&mut self, lhs: M::Term, rhs: M::Term) {
94        self.equations.push((lhs, rhs));
95    }
96
97    /// Iterates over the equations of this instance.
98    pub fn equations(&self) -> impl Iterator<Item = &(M::Term, M::Term)> {
99        self.equations.iter()
100    }
101}
catlog/dbl/model_instance.rs

catlog/dbl/
model_instance.rs
