Struct ModalDblModel 

pub struct ModalDblModel<Kind> { /* private fields */ }

A model of a modal double theory.

Implementations

impl<Kind: DblTheoryKind> ModalDblModel<Kind>

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

Creates an empty model of the given theory.

Trait Implementations

impl<Kind: DblTheoryKind> Category for ModalDblModel<Kind>

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

fn clone(&self) -> ModalDblModel<Kind>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<Kind: DblTheoryKind> DblModel for ModalDblModel<Kind>

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<Kind>

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

fn theory(&self) -> Rc<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<Kind: DblTheoryKind> Display for ModalDblModel<Kind>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<Kind: DblTheoryKind> FgCategory for ModalDblModel<Kind>

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<Kind: DblTheoryKind> FpDblModel for ModalDblModel<Kind>

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 equations(&self) -> impl Iterator<Item = (Self::Mor, Self::Mor)>

Iterates over equations between morphisms.

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<Kind: DblTheoryKind> MutDblModel for ModalDblModel<Kind>

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<Kind: DblTheoryKind> PrintableDblModel for ModalDblModel<Kind>

fn ob_to_doc<'a>( &self, ob: &Self::Ob, ob_ns: &Namespace, mor_ns: &Namespace, ) -> D<'a>

Pretty prints an object in the model.

fn mor_to_doc<'a>( &self, _mor: &Self::Mor, _ob_ns: &Namespace, _mor_ns: &Namespace, ) -> D<'a>

Pretty prints a morphism in the model.

fn ob_type_to_doc<'a>(ob_type: &Self::ObType) -> D<'a>

Pretty prints an object type in the model’s theory.

fn mor_type_to_doc<'a>(mor_type: &Self::MorType) -> D<'a>

Pretty prints a morphism type in the model’s theory.

impl<Kind: DblTheoryKind> Validate for ModalDblModel<Kind>

type ValidationError = InvalidDblModel

The type of a validation error.

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

Validates the object.