catlog/dbl/discrete/
model_instance.rs

1//! Instances of models of a discrete double theory.
2
3use crate::dbl::model_instance::{DblModelInstance, HasInstanceTerm, InstanceTerm};
4use crate::one::QualifiedPath;
5use crate::zero::QualifiedName;
6
7use super::model::DiscreteDblModel;
8
9/// A term in an instance of a discrete double model: a model morphism
10/// applied to a single instance generator.
11///
12/// Composition of model morphisms is reflected inside [`path`](Self::path)
13/// itself, not by nesting term constructors, so every term has the
14/// flat canonical shape `path(base)`. When `path` is the identity, the
15/// term denotes `base` directly; its `Id` vertex must agree with the
16/// fiber of `base` in the surrounding instance.
17#[derive(Clone, Debug, PartialEq, Eq)]
18pub struct DiscreteInstanceTerm {
19    /// Model morphism applied to `base`.
20    pub path: QualifiedPath,
21    /// The instance generator at the root of the term.
22    pub base: QualifiedName,
23}
24
25impl InstanceTerm for DiscreteInstanceTerm {
26    type Mor = QualifiedPath;
27}
28
29impl HasInstanceTerm for DiscreteDblModel {
30    type Term = DiscreteInstanceTerm;
31}
32
33/// An instance of a model of a discrete double theory.
34pub type DiscreteDblModelInstance = DblModelInstance<DiscreteDblModel>;
catlog/dbl/discrete/model_instance.rs

catlog/dbl/discrete/
model_instance.rs
