Enum ExprKind

pub enum ExprKind {
    Var {
        name: Ident,
    },
    Constr {
        name: QualifiedIdent,
        args: Spine,
    },
    All {
        param: Option<Ident>,
        typ: Box<Expr>,
        body: Box<Expr>,
        erased: bool,
    },
    Sigma {
        param: Option<Ident>,
        fst: Box<Expr>,
        snd: Box<Expr>,
    },
    Lambda {
        param: Ident,
        typ: Option<Box<Expr>>,
        body: Box<Expr>,
        erased: bool,
    },
    App {
        fun: Box<Expr>,
        args: Vec<AppBinding>,
    },
    Let {
        name: Destruct,
        val: Box<Expr>,
        next: Box<Expr>,
    },
    Ann {
        val: Box<Expr>,
        typ: Box<Expr>,
    },
    Lit {
        lit: Literal,
    },
    Binary {
        op: Operator,
        fst: Box<Expr>,
        snd: Box<Expr>,
    },
    Hole,
    Do {
        typ: QualifiedIdent,
        sttm: Box<Sttm>,
    },
    If {
        cond: Box<Expr>,
        then_: Box<Expr>,
        else_: Box<Expr>,
    },
    Pair {
        fst: Box<Expr>,
        snd: Box<Expr>,
    },
    List {
        args: Vec<Expr>,
    },
    Subst(Substitution),
    Match(Box<Match>),
    Open {
        type_name: QualifiedIdent,
        var_name: Ident,
        motive: Option<Box<Expr>>,
        next: Box<Expr>,
    },
    SeqRecord(SeqRecord),
}

Variants

Var

Name of a variable

Fields

name: Ident

Constr

Name of a function/constructor

Fields

name: QualifiedIdent

args: Spine

All

The dependent function space (e.g. (x : Int) -> y)

Fields

param: Option<Ident>

typ: Box<Expr>

body: Box<Expr>

erased: bool

Sigma

The dependent product space (e.g. [x : Int] -> y)

Fields

param: Option<Ident>

fst: Box<Expr>

snd: Box<Expr>

Lambda

A anonymous function that receives one argument

Fields

param: Ident

typ: Option<Box<Expr>>

body: Box<Expr>

erased: bool

App

Application of a expression to a spine of expressions

Fields

fun: Box<Expr>

args: Vec<AppBinding>

Let

Declaration of a local variable

Fields

name: Destruct

val: Box<Expr>

next: Box<Expr>

Ann

Type ascription (x : y)

Fields

val: Box<Expr>

typ: Box<Expr>

Lit

Literal

Fields

lit: Literal

Binary

Binary operation (e.g. 2 + 3)

Fields

op: Operator

fst: Box<Expr>

snd: Box<Expr>

Hole

A expression open to unification (e.g. _)

Do

Do notation

Fields

typ: QualifiedIdent

sttm: Box<Sttm>

If

If else statement

Fields

cond: Box<Expr>

then_: Box<Expr>

else_: Box<Expr>

Pair

If else statement

Fields

fst: Box<Expr>

snd: Box<Expr>

List

Array

Fields

args: Vec<Expr>

Subst(Substitution)

Substituion

Match(Box<Match>)

A match block that will be translated into an eliminator of a datatype.

Open

Adds all of the variables inside the context

Fields

type_name: QualifiedIdent

var_name: Ident

motive: Option<Box<Expr>>

next: Box<Expr>

SeqRecord(SeqRecord)

Trait Implementations

impl Clone for ExprKind

fn clone(&self) -> ExprKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ExprKind

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

Formats the value using the given formatter.