Enum libunseemly::beta::Beta

pub enum Beta {
    Basic(Name, Name),
    SameAs(Name, Box<Ast>),
    BoundButNotUsable(Name),
    Underspecified(Name),
    Protected(Name),
    Shadow(Box<Beta>, Box<Beta>),
    ShadowAll(Box<Beta>, Vec<Name>),
    Nothing,
}

Betas are always tied to a particular Form, and they have names that refer to the parts of that Form. They are generally used to talk about environmental operations, and they are most useful for typechecking (the evaluation process ignores them, because it needs to do more complex operations to calculate extended environments).

Betas are trees that determine how variables shadow each other, if multiple variables are being handled at once. The leaf nodes, Basic and SameAs, indicate (a) where the name comes from (b) where to get the type annotation (Basic) or an expression producing the type (SameAs) for that name. The more exotic leaf nodes, Underspecified, Protected, and BoundButNotUsable do various weird things.

I have no idea where the name “β” came from, and whether it has any connection to α-equivalence.

There’s probably a very elegant way to make Beta just another kind of Ast. Finding it might require some time in the math mines, though.

Variants

Basic(Name, Name)

Tuple Fields

0: Name

1: Name

Both of these Names refer to named terms in the current Scope (or ResEnv, for Asts). The first is the identifier to import, and the second the syntax for its type.

SameAs(Name, Box<Ast>)

Tuple Fields

0: Name

1: Box<Ast>

Like Basic, but here the second part is another expression which should be typechecked, and whose type the new name gets. (This can be used write to let without requiring a type annotation.)

BoundButNotUsable(Name)

Tuple Fields

0: Name

Names are introduced here, but bound to Trivial. Needed to avoid an infinite regress where the syntax for Scope does a self-import to expose the names it introduces to the (syntax for) betas that need them.

Underspecified(Name)

Tuple Fields

0: Name

Name is introduced here (must be a single Atom), and its meaning is figured out from usage.

Protected(Name)

Tuple Fields

0: Name

Name is left alone (must be a single VarRef, and already bound)

Shadow(Box<Beta>, Box<Beta>)

Tuple Fields

0: Box<Beta>

1: Box<Beta>

Shadow the names from two Betas.

ShadowAll(Box<Beta>, Vec<Name>)

Tuple Fields

0: Box<Beta>

1: Vec<Name>

Shadow the names from a Beta, repeated. The Vec should always be equal to names_mentioned(...) of the Beta.

Nothing

No names

Implementations

impl Beta

pub fn names_mentioned(&self) -> Vec<Name>

pub fn names_mentioned_and_bound(&self) -> Vec<Name>

pub fn extract_from_mbe<T: Clone + Debug>(
    &self,
    parts: &EnvMBE<T>,
    f: &dyn Fn(&T) -> &Ren
) -> Ren

Trait Implementations

impl Clone for Beta

fn clone(&self) -> Beta

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Beta

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

Formats the value using the given formatter.

impl PartialEq<Beta> for Beta

fn eq(&self, other: &Beta) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Beta) -> bool

This method tests for !=.

impl<'t> Reifiable for Beta

fn ty() -> Ast

The Unseemly type that corresponds to to the Reifiable type. This leaves abstract the type parameters of Self; invoke like Self::<Irr,Irr>::ty(). e.g. ∀ A. Pair<A int> TODO: rename to generic_ty

fn ty_name() -> Name

A name for that type, so that recursive types are okay. Ignore the type parameters of Self; invoke like Self::<Irr,Irr>::ty_name(). e.g. WithInteger

fn concrete_arguments() -> Option<Vec<Ast>>

fn reify(&self) -> Value

The Unseemly value that corresponds to a value.

fn reflect(v: &Value) -> Self

Get a value from an Unseemly value

fn ty_invocation() -> Ast

How to refer to this type, given an environment in which ty_name() is defined to be ty(). Parameters will be concrete. e.g. WithInteger<Float> (Types using this type will use this, rather than ty) Don’t override this.

impl StructuralPartialEq for Beta