Enum voile::syntax::abs::ast::Abs

pub enum Abs {
    Type(Loc, Level),
    Var(Ident, UID, DBI),
    Ref(Ident, GI),
    Meta(Ident, MI),
    Lift(Loc, LevelType, Box<Self>),
    Cons(Ident),
    Proj(Loc, Box<Self>, Ident),
    App(Loc, Box<Self>, Plicit, Box<Self>),
    Dt(Loc, PiSig, UID, Plicit, Box<Self>, Box<Self>),
    Lam(Loc, Ident, UID, Box<Self>),
    Pair(Loc, Box<Self>, Box<Self>),
    Fst(Loc, Box<Self>),
    Snd(Loc, Box<Self>),
    RowPoly(Loc, VarRec, Vec<LabAbs>, Option<Box<Self>>),
    Rec(Loc, Vec<LabAbs>, Option<Box<Self>>),
    Whatever(Loc),
    CaseOr(Ident, Ident, UID, Box<Self>, Box<Self>),
    RowKind(Loc, VarRec, Vec<Ident>),
}

Variants

Type(Loc, Level)

Var(Ident, UID, DBI)

Local variable

Ref(Ident, GI)

Global variable

Meta(Ident, MI)

Meta variable

Lift(Loc, LevelType, Box<Self>)

Lift an expression many times

Cons(Ident)

Constructor call

Proj(Loc, Box<Self>, Ident)

Record projection

App(Loc, Box<Self>, Plicit, Box<Self>)

Apply or Pipeline in surface

Dt(Loc, PiSig, UID, Plicit, Box<Self>, Box<Self>)

Dependent Type, (a -> b -> c) as Dt(_, DtKind::Pi, _, _, a, Dt(_, DtKind::Pi, _, _, b, c))

Lam(Loc, Ident, UID, Box<Self>)

The first Loc is the syntax info of this whole lambda, while the second is about its parameter

Pair(Loc, Box<Self>, Box<Self>)

Fst(Loc, Box<Self>)

Snd(Loc, Box<Self>)

RowPoly(Loc, VarRec, Vec<LabAbs>, Option<Box<Self>>)

Row-polymorphic types, corresponds to RowPoly

Rec(Loc, Vec<LabAbs>, Option<Box<Self>>)

Record literals

Whatever(Loc)

Empty type eliminator,

CaseOr(Ident, Ident, UID, Box<Self>, Box<Self>)

Case-split expressions.

RowKind(Loc, VarRec, Vec<Ident>)

Row-polymorphic kinds, corresponds to RowKind

Methods

impl Abs

pub fn dependent_type(
    info: Loc,
    kind: PiSig,
    name: UID,
    plicit: Plicit,
    a: Self,
    b: Self
) -> Self

pub fn row_polymorphic_type(
    info: Loc,
    kind: VarRec,
    labels: Vec<LabAbs>,
    rest: Option<Self>
) -> Self

pub fn record(info: Loc, fields: Vec<LabAbs>, rest: Option<Self>) -> Self

pub fn app(info: Loc, function: Self, plicit: Plicit, argument: Self) -> Self

pub fn proj(info: Loc, record: Self, field: Ident) -> Self

pub fn fst(info: Loc, of: Self) -> Self

pub fn snd(info: Loc, of: Self) -> Self

pub fn lam(whole_info: Loc, param: Ident, name: UID, body: Self) -> Self

pub fn pair(info: Loc, first: Self, second: Self) -> Self

pub fn case_or(
    label: Ident,
    binding: Ident,
    uid: UID,
    clause: Self,
    or: Self
) -> Self

pub fn lift(info: Loc, lift_count: LevelType, expr: Self) -> Self

pub fn pi(
    info: Loc,
    name: UID,
    plicit: Plicit,
    input: Self,
    output: Self
) -> Self

pub fn sig(
    info: Loc,
    name: UID,
    plicit: Plicit,
    first: Self,
    second: Self
) -> Self

Trait Implementations

impl Eq for Abs

fn assert_receiver_is_total_eq(&self)

impl Clone for Abs

fn clone(&self) -> Abs

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq<Abs> for Abs

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

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

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

This method tests for !=.

impl Debug for Abs

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

Formats the value using the given formatter.

impl Display for Abs

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

Formats the value using the given formatter.

impl ToLoc for Abs

fn loc(&self) -> Loc

Access the location information.