Struct DblModelInstance 

pub struct DblModelInstance<M: HasInstanceTerm> { /* private fields */ }

An instance of a model: a fibered set of generators plus equations between terms in the model’s instance-term language.

Owns the generator-to-fiber assignment and the equations, but does not own the model itself (held behind an Rc, matching how models reference their theories).

Implementations

impl<M: HasInstanceTerm> DblModelInstance<M>

pub fn new(model: Rc<M>) -> Self

Creates an empty instance over the given model.

pub fn model(&self) -> &Rc<M>

The model this is an instance of.

pub fn add_generator(&mut self, name: QualifiedName, fiber: M::Ob)

Adds a generator living over the given object of the model.

pub fn fiber_of(&self, name: &QualifiedName) -> Option<&M::Ob>

The model object that name lives over, if name is a generator of this instance.

pub fn generators(&self) -> impl Iterator<Item = (QualifiedName, &M::Ob)>

Iterates over the instance generators and their fibers.

pub fn add_equation(&mut self, lhs: M::Term, rhs: M::Term)

Adds an equation between two terms.

pub fn equations(&self) -> impl Iterator<Item = &(M::Term, M::Term)>

Iterates over the equations of this instance.