Struct spacetimedb_sats::typespace::Typespace

pub struct Typespace {
    pub types: Vec<AlgebraicType>,
}

A Typespace represents the typing context in SATS.

That is, this is the Δ or Γ you’ll see in type theory litterature.

We use (sort of) deBrujin indices to represent our type variables. Notably however, these are given for the entire module and there are no universal quantifiers (i.e., Δ, α ⊢ τ | Δ ⊢ ∀ α. τ) nor are there type lambdas (i.e., Λτ. v). See System F, the second-order lambda calculus, for more on ∀ and Λ.

There are however recursive types in SATs, e.g., &0 = { Cons({ v: U8, t: &0 }), Nil } represents a basic cons list where &0 is the type reference at index 0.

Fields

types: Vec<AlgebraicType>

The types in our typing context that can be referred to with AlgebraicTypeRefs.

Implementations

impl Typespace

pub const EMPTY: &'static Typespace = _

pub const fn new(types: Vec<AlgebraicType>) -> Self

Returns a context (Typespace) with the given types.

pub fn get(&self, r: AlgebraicTypeRef) -> Option<&AlgebraicType>

Returns the AlgebraicType referred to by r within this context.

pub fn get_mut(&mut self, r: AlgebraicTypeRef) -> Option<&mut AlgebraicType>

Returns a mutable reference to the AlgebraicType referred to by r within this context.

pub fn add(&mut self, ty: AlgebraicType) -> AlgebraicTypeRef

Inserts an AlgebraicType into the typespace and returns an AlgebraicTypeRef that refers to the inserted AlgebraicType.

This allows for self referential, recursive or other complex types to be declared in the typespace.

You can also use this to later change the meaning of the returned AlgebraicTypeRef when you cannot provide the full definition of the type yet.

Panics if the number of type references exceeds an u32.

pub const fn with_type<'a, T: ?Sized>( &'a self, ty: &'a T ) -> WithTypespace<'a, T>

Returns ty combined with the context self.

pub fn inline_typerefs_in_type( &mut self, ty: &mut AlgebraicType ) -> Result<(), TypeRefError>

Inlines all type references in ty recursively using the current typeset.

pub fn inline_all_typerefs(&mut self) -> Result<(), TypeRefError>

Inlines all type references in the typespace recursively.

Errors out if any type reference is invalid or self-referential.

Trait Implementations

impl Clone for Typespace

fn clone(&self) -> Typespace

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Typespace

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

Formats the value using the given formatter.

impl Default for Typespace

fn default() -> Self

Returns the “default value” for a type.

impl<'de> Deserialize<'de> for Typespace

fn deserialize<D: Deserializer<'de>>(deserializer: D) -> Result<Self, D::Error>

Deserialize this value from the given deserializer.

impl Index<AlgebraicTypeRef> for Typespace

type Output = AlgebraicType

The returned type after indexing.

fn index(&self, index: AlgebraicTypeRef) -> &Self::Output

Performs the indexing (container[index]) operation.

impl IndexMut<AlgebraicTypeRef> for Typespace

fn index_mut(&mut self, index: AlgebraicTypeRef) -> &mut Self::Output

Performs the mutable indexing (container[index]) operation.

impl Serialize for Typespace

fn serialize<S: Serializer>(&self, __serializer: S) -> Result<S::Ok, S::Error>

Serialize self in the data format of S using the provided serializer.