Struct ModalDblModel

pub struct ModalDblModel { /* private fields */ }

A model of a modal double theory.

Implementations

impl ModalDblModel

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

Creates an empty model of the given theory.

Trait Implementations

impl Category for ModalDblModel

type Ob = ModalOb

Type of objects in category.

type Mor = ModalMor

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 Clone for ModalDblModel

fn clone(&self) -> ModalDblModel

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl DblModel for ModalDblModel

type ObType = ModeApp<QualifiedName>

Rust type of object types defined in the theory.

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

Rust type of morphism types defined in the theory.

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

Type of operations on objects defined in the theory.

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

Type of operations on morphisms defined in the theory.

type Theory = ModalDblTheory

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 FgCategory for ModalDblModel

type ObGen = QualifiedName

Type of an object generator.

type MorGen = QualifiedName

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 FgDblModel for ModalDblModel

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 MutDblModel for ModalDblModel

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.

impl Validate for ModalDblModel

type ValidationError = InvalidDblModel

The type of a validation error.

fn validate(&self) -> Result<(), NonEmpty<Self::ValidationError>>

Validates the object.