Enum voile::syntax::surf::Expr

pub enum Expr {
    Var(Ident),
    Cons(Ident),
    Meta(Ident),
    Lift(Loc, LevelType, Box<Self>),
    Proj(Box<Self>, Vec1<Ident>),
    Type(Loc, Level),
    App(Box<Vec1<Self>>),
    Pipe(Box<Vec1<Self>>),
    Tup(Box<Vec1<Self>>),
    RowPoly(Loc, VarRec, Vec<LabExpr>, Option<Box<Self>>),
    Rec(Loc, Vec<LabExpr>, Option<Box<Self>>),
    RowKind(Loc, VarRec, Vec<Ident>),
    Pi(Vec<Param>, Box<Self>),
    Sig(Vec<Param>, Box<Self>),
    Cases(Ident, Ident, Box<Self>, Box<Self>),
    Whatever(Loc),
    Lam(Loc, Vec<Ident>, Box<Self>),
}

Surface syntax tree node: Expression.

Variants

Var(Ident)

Variable reference.

Cons(Ident)

Constructor call.

Meta(Ident)

Explicit meta variable.

Lift(Loc, LevelType, Box<Self>)

Lift an expression many times.

Proj(Box<Self>, Vec1<Ident>)

Record projections.

Type(Loc, Level)

Type literal, with levels.

App(Box<Vec1<Self>>)

Function application.
Application operator, where f a b c is represented as App(f, vec![a, b, c]) instead of App(App(App(f, a), b), c).

Pipe(Box<Vec1<Self>>)

Function composition.
Pipeline operator, where a |> b |> f is represented as Pipe(vec![a, b, f]) instead of Pipe(Pipe(Pipe(f, a), b), c).

Tup(Box<Vec1<Self>>)

Tuple constructor.
Comma operator, where a, b, c is represented as Tup(a, vec![b, c]) instead of Tup(Tup(a, b), c).

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

Row-polymorphic types, either record types or variant types.

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

Record literals.

RowKind(Loc, VarRec, Vec<Ident>)

Row-polymorphic kinds, either record types or variant kinds.

Pi(Vec<Param>, Box<Self>)

Pi-type expression, where a -> b -> c is represented as Pi(vec![a, b], c) instead of Pi(a, Pi(b, c)). a and b here can introduce telescopes.

Sig(Vec<Param>, Box<Self>)

Sigma-type expression, where a * b * c is represented as Sig(vec![a, b], c) instead of Sig(a, Sig(b, c)). a and b here can introduce telescopes.

Cases(Ident, Ident, Box<Self>, Box<Self>)

Case-chains. Label, binding, body, rest of the clauses

Whatever(Loc)

Termination of a case-chain.

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

Anonymous function, aka lambda expression.

Methods

impl Expr

pub fn pi(params: Vec<Param>, expr: Self) -> Self

pub fn lam(info: Loc, params: Vec<Ident>, expr: Self) -> Self

pub fn app(applied: Self, arguments: Vec<Self>) -> Self

pub fn lift(info: Loc, count: LevelType, target: Self) -> Self

pub fn pipe(first: Self, functions: Vec<Self>) -> Self

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

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

pub fn sum(info: Loc, labels: Vec<LabExpr>, rest: Option<Self>) -> Self

pub fn rec(info: Loc, labels: Vec<LabExpr>, rest: Option<Self>) -> Self

pub fn tup(first: Self, rest: Vec<Self>) -> Self

pub fn sig(params: Vec<Param>, expr: Self) -> Self

pub fn proj(expr: Self, projections: Vec1<Ident>) -> Self

pub fn cases(label: Ident, binding: Ident, body: Self, or: Self) -> Self

Trait Implementations

impl Clone for Expr

fn clone(&self) -> Expr

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Eq for Expr

fn assert_receiver_is_total_eq(&self)

impl PartialEq<Expr> for Expr

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

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

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

This method tests for !=.

impl Debug for Expr

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

Formats the value using the given formatter.

impl StructuralPartialEq for Expr

impl StructuralEq for Expr