Struct ModalDblModel

pub struct ModalDblModel<Id, ThId, S = RandomState> { /* private fields */ }

A model of a modal double theory.

Implementations

impl<Id, ThId, S> ModalDblModel<Id, ThId, S>

pub fn new(theory: Rc<ModalDblTheory<ThId, S>>) -> Self

Creates an empty model of the given theory.

Trait Implementations

impl<Id, ThId, S> Category for ModalDblModel<Id, ThId, S>

where Id: Eq + Clone + Hash + Debug, ThId: Eq + Clone + Hash + Debug, S: BuildHasher,

type Ob = ModalOb<Id, ThId>

Type of objects in category.

type Mor = ModalMor<Id, ThId>

Type of morphisms in category.

fn has_ob(&self, ob: &Self::Ob) -> bool

Does the category contain the value as an object?

fn has_mor(&self, mor: &Self::Mor) -> bool

Does the category contain the value as a morphism?

fn dom(&self, mor: &Self::Mor) -> Self::Ob

Gets the domain of a morphism in the category.

fn cod(&self, mor: &Self::Mor) -> Self::Ob

Gets the codomain of a morphism in the category.

fn compose(&self, path: Path<Self::Ob, Self::Mor>) -> Self::Mor

Composes a path of morphisms in the category.

fn compose2(&self, f: Self::Mor, g: Self::Mor) -> Self::Mor

Composes a pair of morphisms with compatible (co)domains.

fn id(&self, x: Self::Ob) -> Self::Mor

Constructs the identity morphism at an object.

fn morphisms_are_equal(&self, f: Self::Mor, g: Self::Mor) -> bool

Are the two morphisms in the category equal?

impl<Id: Clone, ThId: Clone, S: Clone> Clone for ModalDblModel<Id, ThId, S>

fn clone(&self) -> ModalDblModel<Id, ThId, S>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<Id, ThId, S> DblModel for ModalDblModel<Id, ThId, S>

where Id: Eq + Clone + Hash + Debug, ThId: Eq + Clone + Hash + Debug, S: BuildHasher,

type ObType = ModeApp<ThId>

Rust type of object types defined in the theory.

type MorType = ShortPath<ModeApp<ThId>, ModeApp<ThId>>

Rust type of morphism types defined in the theory.

type ObOp = Path<ModeApp<ThId>, ModeApp<ModalOp<ThId>>>

Type of operations on objects defined in the theory.

type MorOp = DblTree<Path<ModeApp<ThId>, ModeApp<ModalOp<ThId>>>, ShortPath<ModeApp<ThId>, ModeApp<ThId>>, ModalNode<ThId>>

Type of operations on morphisms defined in the theory.

type Theory = ModalDblTheory<ThId, S>

The type of double theory that this is a model of.

fn theory(&self) -> &Self::Theory

The double theory that this model is a model of.

fn ob_type(&self, ob: &Self::Ob) -> Self::ObType

Type of an object.

fn mor_type(&self, mor: &Self::Mor) -> Self::MorType

Type of a morphism.

fn ob_act(&self, ob: Self::Ob, path: &Self::ObOp) -> Self::Ob

Acts on an object with an object operation.

fn mor_act( &self, path: Path<Self::Ob, Self::Mor>, tree: &Self::MorOp, ) -> Self::Mor

Acts on a sequence of morphisms with a morphism operation.

impl<Id, ThId, S> FgCategory for ModalDblModel<Id, ThId, S>

where Id: Eq + Clone + Hash + Debug, ThId: Eq + Clone + Hash + Debug, S: BuildHasher,

type ObGen = Id

Type of an object generator.

type MorGen = Id

Type of a morphism generator

fn ob_generators(&self) -> impl Iterator<Item = Self::ObGen>

Iterates over object generators.

fn mor_generators(&self) -> impl Iterator<Item = Self::MorGen>

Iterates over morphism generators.

fn mor_generator_dom(&self, f: &Self::MorGen) -> Self::Ob

The domain of a morphism generator

fn mor_generator_cod(&self, f: &Self::MorGen) -> Self::Ob

The codomain of a morphism generator

fn objects(&self) -> impl Iterator<Item = Self::Ob>

Iterates over basic objects.

fn morphisms(&self) -> impl Iterator<Item = Self::Mor>

Iterates over basic morphisms.

impl<Id, ThId, S> FgDblModel for ModalDblModel<Id, ThId, S>

where Id: Eq + Clone + Hash + Debug, ThId: Eq + Clone + Hash + Debug, S: BuildHasher,

fn ob_generator_type(&self, id: &Self::ObGen) -> Self::ObType

Type of an object generator.

fn mor_generator_type(&self, id: &Self::MorGen) -> Self::MorType

Type of a morphism generator.

fn ob_generators_with_type( &self, typ: &Self::ObType, ) -> impl Iterator<Item = Self::ObGen>

Iterates over object generators with the given object type.

fn mor_generators_with_type( &self, typ: &Self::MorType, ) -> impl Iterator<Item = Self::MorGen>

Iterates over morphism generators with the given morphism type.

fn objects_with_type( &self, obtype: &Self::ObType, ) -> impl Iterator<Item = Self::Ob>

Iterators over basic objects with the given object type.

fn morphisms_with_type( &self, mortype: &Self::MorType, ) -> impl Iterator<Item = Self::Mor>

Iterates over basic morphisms with the given morphism type.

impl<Id, ThId, S> MutDblModel for ModalDblModel<Id, ThId, S>

where Id: Eq + Clone + Hash + Debug, ThId: Eq + Clone + Hash + Debug, S: BuildHasher,

fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType)

Adds an object generator to the model.

fn add_mor( &mut self, f: Self::MorGen, dom: Self::Ob, cod: Self::Ob, mor_type: Self::MorType, )

Adds a morphism generator to the model.

fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType)

Adds a morphism generator to the model without setting its (co)domain.

fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob>

Gets the domain of a morphism generator, if it is set.

fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob>

Gets the codomain of a morphism generator, if it is set.

fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob)

Sets the domain of a morphism generator.

fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob)

Sets the codomain of a morphism generator.