Enum voile::syntax::core::Neutral

pub enum Neutral {
    Var(DBI),
    Ref(GI),
    Meta(MI),
    Lift(LevelType, Box<Self>),
    Fall(LevelType, Box<Self>),
    Axi(Axiom),
    App(Box<Self>, Vec<Val>),
    Fst(Box<Self>),
    Snd(Box<Self>),
    Proj(Box<Self>, String),
    Row(VarRec, Variants, Box<Self>),
    Rec(Fields, Box<Self>),
    SplitOn(CaseSplit, Box<Self>),
    OrSplit(CaseSplit, Box<Self>),
}

Irreducible because of the presence of generated value.

Variants

Var(DBI)

Local variable, referred by de-bruijn index.

Ref(GI)

Global variable, referred by index. Needed for recursive definitions.

Meta(MI)

Meta variable reference.

Lift(LevelType, Box<Self>)

Lifting self to a higher level.

Fall(LevelType, Box<Self>)

Down-lifting self to a lower level.

Axi(Axiom)

Postulated value, aka axioms.

App(Box<Self>, Vec<Val>)

Function application, with all arguments collected (so we have easy access to application arguments).
This is convenient for meta resolution and termination check.

The "arguments" is supposed to be non-empty.

Fst(Box<Self>)

Projecting the first element of a pair.

Snd(Box<Self>)

Projecting the second element of a pair.

Proj(Box<Self>, String)

Projecting a named element of a record.

Row(VarRec, Variants, Box<Self>)

Row-polymorphic types.

Rec(Fields, Box<Self>)

Record literal, with extension.

SplitOn(CaseSplit, Box<Self>)

Splitting on a neutral term.

OrSplit(CaseSplit, Box<Self>)

Splitting with unknown branches.

Methods

impl Neutral

pub fn map_axiom(self, f: &mut impl FnMut(Axiom) -> Neutral) -> Self

fn map_axiom_split(
    mapper: &mut impl FnMut(Neutral) -> Val,
    split: CaseSplit
) -> CaseSplit

Trait Implementations

impl RedEx<Val> for Neutral

fn reduce_with_dbi(self, arg: Val, dbi: DBI) -> Val

This is primarily a private implementation-related API. Use at your own risk.

fn reduce_with_dbi_borrow(self, arg: &Val, dbi: DBI) -> Val

When the argument is not likely to be used, prefer this over reduce_with_dbi.

impl Clone for Neutral

fn clone(&self) -> Neutral

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Eq for Neutral

fn assert_receiver_is_total_eq(&self)

impl PartialEq<Neutral> for Neutral

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

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

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

This method tests for !=.

impl Display for Neutral

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

Formats the value using the given formatter.

impl Debug for Neutral

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

Formats the value using the given formatter.

impl StructuralPartialEq for Neutral

impl StructuralEq for Neutral

impl LiftEx for Neutral

fn lift(self, levels: LevelType) -> Self

Lift the level of self.

fn fall(self, levels: LevelType) -> Self

Down-lift the level of self. Separated with lift instead of allowing negative numbers to lift because we want the symbol to be explicit.

fn calc_level(&self) -> LevelCalcState

Internal API, for code sharing only.

fn level(&self) -> Level

Calculate the level of self, like a normal value will have level 0, a type expression will have level 1 (or higher).