Elaborator

catlog_wasm::notation

Struct Elaborator

pub struct Elaborator;

Expand description

An elaborator.

Elaboration is the process of transforming notation (as declared in notebook-types) into syntax and values. This can possibly fail. Eventually, this struct may have some role to play in accumulating errors, but for now it is a singleton.

Trait Implementations§

impl CanElaborate<Mor, ModalMor> for Elaborator

Elaborates into a morphism in a model of a modal theory.

fn elab(&self, mor: &Mor) -> Result<ModalMor, String>

Transform notation into syntax.

impl CanElaborate<Mor, Path<QualifiedName, QualifiedName>> for Elaborator

Elaborates into a morphism in a model of a discrete double theory.

fn elab(&self, mor: &Mor) -> Result<QualifiedPath, String>

Transform notation into syntax.

impl CanElaborate<Mor, Path<TabOb, TabEdge>> for Elaborator

Elaborates into a morphism in a model of a discrete tabulator theory.

fn elab(&self, mor: &Mor) -> Result<TabMor, String>

Transform notation into syntax.

impl CanElaborate<Mor, TabEdge> for Elaborator

fn elab(&self, mor: &Mor) -> Result<TabEdge, String>

Transform notation into syntax.

impl CanElaborate<MorType, Path<QualifiedName, QualifiedName>> for Elaborator

Elaborates into morphism type in a discrete double theory.

fn elab(&self, mor_type: &MorType) -> Result<QualifiedPath, String>

Transform notation into syntax.

impl CanElaborate<MorType, ShortPath<ModeApp<QualifiedName>, ModeApp<QualifiedName>>> for Elaborator

Elaborates into morphism type in a modal double theory.

fn elab(&self, mor_type: &MorType) -> Result<ModalMorType, String>

Transform notation into syntax.

impl CanElaborate<MorType, TabMorType> for Elaborator

Elaborates into morphism type in a discrete tabulator theory.

fn elab(&self, mor_type: &MorType) -> Result<TabMorType, String>

Transform notation into syntax.

impl CanElaborate<Ob, ModalOb> for Elaborator

Elaborates into an object in a model of a modal theory.

fn elab(&self, ob: &Ob) -> Result<ModalOb, String>

Transform notation into syntax.

impl CanElaborate<Ob, QualifiedName> for Elaborator

Elaborates into an object in a model of a discrete double theory.

fn elab(&self, ob: &Ob) -> Result<QualifiedName, String>

Transform notation into syntax.

impl CanElaborate<Ob, TabOb> for Elaborator

Elaborates into an object in a model of a discrete tabulator theory.

fn elab(&self, ob: &Ob) -> Result<TabOb, String>

Transform notation into syntax.

impl CanElaborate<ObOp, Path<ModeApp<QualifiedName>, ModeApp<ModalOp>>> for Elaborator

Elaborates into an object operation in a modal double theory.

fn elab(&self, op: &ObOp) -> Result<ModalObOp, String>

Transform notation into syntax.

impl CanElaborate<ObOp, Path<TabObType, TabObProj>> for Elaborator

Elaborates into object operation in a discrete tabulator theory.

fn elab(&self, op: &ObOp) -> Result<TabObOp, String>

Transform notation into syntax.

impl CanElaborate<ObOp, QualifiedName> for Elaborator

Elaborates into object operation in a discrete double theory.

fn elab(&self, op: &ObOp) -> Result<QualifiedName, String>

Transform notation into syntax.

impl CanElaborate<ObType, ModeApp<QualifiedName>> for Elaborator

Elaborates into object type in a modal double theory.

fn elab(&self, ob_type: &ObType) -> Result<ModalObType, String>

Transform notation into syntax.

impl CanElaborate<ObType, QualifiedName> for Elaborator

Elaborates into object type in a discrete double theory.

fn elab(&self, ob_type: &ObType) -> Result<QualifiedName, String>

Transform notation into syntax.

impl CanElaborate<ObType, TabObType> for Elaborator

Elaborates into object type in a discrete tabulator theory.

fn elab(&self, ob_type: &ObType) -> Result<TabObType, String>

Transform notation into syntax.

Auto Trait Implementations§

impl Freeze for Elaborator

impl RefUnwindSafe for Elaborator

impl Send for Elaborator

impl Sync for Elaborator

impl Unpin for Elaborator

impl UnwindSafe for Elaborator

Blanket Implementations§

impl<T> Any for T
where T: 'static + ?Sized,

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more

impl<T> Borrow<T> for T
where T: ?Sized,

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more

impl<T> BorrowMut<T> for T
where T: ?Sized,

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more

impl<T> From<T> for T

fn from(t: T) -> T

Returns the argument unchanged.

impl<T, U> Into<U> for T
where U: From<T>,

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

impl<T> IntoEither for T

fn into_either(self, into_left: bool) -> Either<Self, Self>

Converts self into a Left variant of Either<Self, Self> if into_left is true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
where F: FnOnce(&Self) -> bool,

Converts self into a Left variant of Either<Self, Self> if into_left(&self) returns true. Converts self into a Right variant of Either<Self, Self> otherwise. Read more

impl<T> Same for T

type Output = T

Should always be Self

impl<SS, SP> SupersetOf<SS> for SP
where SS: SubsetOf<SP>,

fn to_subset(&self) -> Option<SS>

The inverse inclusion map: attempts to construct self from the equivalent element of its superset. Read more

fn is_in_subset(&self) -> bool

Checks if self is actually part of its subset T (and can be converted to it).

fn to_subset_unchecked(&self) -> SS

Use with care! Same as self.to_subset but without any property checks. Always succeeds.

fn from_subset(element: &SS) -> SP

The inclusion map: converts self to the equivalent element of its superset.

impl<T, U> TryFrom<U> for T
where U: Into<T>,

type Error = Infallible

The type returned in the event of a conversion error.

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.

impl<V, T> VZip<V> for T
where V: MultiLane<T>,

fn vzip(self) -> V