Enum TheoryDef 

pub enum TheoryDef {
    Discrete(Rc<DiscreteDblTheory>),
    Modal(Rc<ModalDblTheory>),
}

Definition of a double theory supported by DoubleTT.

Variants

Discrete(Rc<DiscreteDblTheory>)

A discrete double theory.

Modal(Rc<ModalDblTheory>)

A modal double theory.

Implementations

impl TheoryDef

pub fn discrete(theory: DiscreteDblTheory) -> Self

Smart constructor for TheoryDef::Discrete case.

pub fn modal(theory: ModalDblTheory) -> Self

Smart constructor for TheoryDef::Modal case.

pub fn basic_ob_type(&self, name: QualifiedName) -> Option<ObType>

Gets the basic object type with given name, if it exists.

pub fn basic_mor_type(&self, name: QualifiedName) -> Option<MorType>

Gets the basic morphism type with given name, if it exists.

pub fn basic_ob_op(&self, name: QualifiedName) -> Option<ObOp>

Gets the basic object operation with given name, if it exists.

pub fn src_type(&self, mor_type: &MorType) -> ObType

Gets the source type of a morphism type.

pub fn tgt_type(&self, mor_type: &MorType) -> ObType

Gets the target type of a morphism type.

pub fn hom_type(&self, ob_type: ObType) -> MorType

Gets the hom (identity) type for an object type.

pub fn compose_types2(&self, mt1: MorType, mt2: MorType) -> Option<MorType>

Composes a pair of morphism types, if they have a composite.

pub fn ob_op_dom(&self, ob_op: &ObOp) -> ObType

Gets the domain of an object operation.

pub fn ob_op_cod(&self, ob_op: &ObOp) -> ObType

Gets the codomain of an object operation.

Trait Implementations

impl Clone for TheoryDef

fn clone(&self) -> TheoryDef

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl From<Rc<DiscreteDblTheory>> for TheoryDef

fn from(value: Rc<DiscreteDblTheory>) -> Self

Converts to this type from the input type.

impl From<Rc<ModalDblTheory>> for TheoryDef

fn from(value: Rc<ModalDblTheory>) -> Self

Converts to this type from the input type.