Enum voile::syntax::surf::Expr

pub enum Expr {
    Var(Ident),
    Cons(Ident),
    Variant(Ident),
    Bot(SyntaxInfo),
    Meta(Ident),
    Lift(SyntaxInfo, u32, Box<Self>),
    Type(SyntaxInfo, Level),
    App(Box<Self>, Vec<Self>),
    Pipe(Box<Self>, Vec<Self>),
    Tup(Box<Self>, Vec<Self>),
    Sum(Box<Self>, Vec<Self>),
    Pi(Vec<Param>, Box<Self>),
    Sig(Vec<Param>, Box<Self>),
    Lam(SyntaxInfo, Vec<Ident>, Box<Self>),
}

Surface syntax tree node: Expression.

Variants

Var(Ident)

Variable reference

Cons(Ident)

Constructor call

Variant(Ident)

Type of a constructor call

Bot(SyntaxInfo)

Empty type

Meta(Ident)

Explicit meta variable

Lift(SyntaxInfo, u32, Box<Self>)

Lift an expression many times

Type(SyntaxInfo, Level)

Type literal, with levels

App(Box<Self>, Vec<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<Self>, Vec<Self>)

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

Tup(Box<Self>, Vec<Self>)

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

Sum(Box<Self>, Vec<Self>)

Type-sum operator.

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.

Lam(SyntaxInfo, 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: SyntaxInfo, params: Vec<Ident>, expr: Self) -> Self

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

pub fn lift(info: SyntaxInfo, count: u32, target: Self) -> Self

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

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

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

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

Trait Implementations

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 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 Debug for Expr

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

Formats the value using the given formatter.