Enum malk_core::TermKind

pub enum TermKind {
    Omega,
    Level,
    LevelZero,
    LevelSucc {
        pred: Term,
    },
    LevelMax {
        a: Term,
        b: Term,
    },
    Type {
        level: Term,
    },
    Var(usize),
    FuncType {
        arg_type: Term,
        res_type: Term,
    },
    FuncTerm {
        body: Term,
    },
    FuncApp {
        func: Term,
        arg: Term,
        arg_type: Term,
        res_type: Term,
    },
    UnitType,
    UnitTerm,
    PairType {
        head_type: Term,
        tail_type: Term,
    },
    PairTerm {
        head: Term,
        tail: Term,
    },
    PairElim {
        pair: Term,
        res: Term,
        head_type: Term,
        tail_type: Term,
    },
    NeverType,
    NeverElim {
        never: Term,
    },
    EitherType {
        left_type: Term,
        right_type: Term,
    },
    EitherLeft {
        val: Term,
    },
    EitherRight {
        val: Term,
    },
    EitherElim {
        arg: Term,
        arg_type: Term,
        res_type: Term,
        on_left: Term,
        on_right: Term,
    },
    IdentType {
        term_type: Term,
        a: Term,
        b: Term,
    },
    IdentTerm,
    IdentElim {
        term_type: Term,
        a: Term,
        b: Term,
        path: Term,
        context: Term,
        proof: Term,
    },
    RecType {
        rec_type: Term,
    },
    RecTerm {
        rec_term: Term,
    },
    WorldType,
    WorldTerm,
    WorldElim {
        intrinsic: &'static str,
        world_in: Term,
        arg: Term,
        expr: Term,
    },
    UmType,
    UmTerm {
        val: u64,
    },
    UmSucc {
        pred: Term,
    },
    UmElim {
        arg: Term,
        res_type: Term,
        on_zero: Term,
        on_succ: Term,
    },
}

The different kinds of term that can appear in the AST.

Variants

Omega

The type of all types, and levels, which does not itself have a type.

Level

The type of universe levels.

LevelZero

Universe level zero.

LevelSucc

Universe level (pred + 1).

Fields of LevelSucc

pred: Term

LevelMax

Universe level max(a, b)

Fields of LevelMax

a: Term
b: Term

Type

The type of types, indexed by levels.

Fields of Type

level: Term

Var(usize)

A variable.

FuncType

The type of functions. (ie pi types)

Fields of FuncType

arg_type: Term
res_type: Term

FuncTerm

Functions.

Fields of FuncTerm

body: Term

FuncApp

Function application.

Fields of FuncApp

func: Term
arg: Term
arg_type: Term
res_type: Term

UnitType

The unit type.

UnitTerm

The unit term.

PairType

A dependent pair type (ie. sigma type)

Fields of PairType

head_type: Term
tail_type: Term

PairTerm

A pair term.

Fields of PairTerm

head: Term
tail: Term

PairElim

Dependent pair elimination.

Fields of PairElim

pair: Term
res: Term
head_type: Term
tail_type: Term

NeverType

The canonical empty type, (ie. bottom).

NeverElim

Never type elimintator

Fields of NeverElim

never: Term

EitherType

Disjoint union, sum type.

Fields of EitherType

left_type: Term
right_type: Term

EitherLeft

Inject left.

Fields of EitherLeft

val: Term

EitherRight

Inject right.

Fields of EitherRight

val: Term

EitherElim

Case match on a sum type.

Fields of EitherElim

arg: Term
arg_type: Term
res_type: Term
on_left: Term
on_right: Term

IdentType

The type of identifications (a == b)

Fields of IdentType

term_type: Term
a: Term
b: Term

IdentTerm

Reflexivity,

IdentElim

J-elimination for identities.

Fields of IdentElim

term_type: Term
a: Term
b: Term
path: Term
context: Term
proof: Term

RecType

A recursive type. rec_type is under a context where Var(0) refers back to the type.

Fields of RecType

rec_type: Term

RecTerm

A recursive term. Used to mark rec_term as a member of a recursive type.

Fields of RecTerm

rec_term: Term

WorldType

The type for interacting with the outside world through intrinsics.

WorldTerm

The term used to represent a fully-normalised world ready to perform IO on.

WorldElim

Performs an intrinsic call.

Fields of WorldElim

intrinsic: &'static str	The name of the intrinsic
world_in: Term	The world argument.
arg: Term	The argument type that the intrinsic expects.
expr: Term	The result of the expression. Evaluated with the intrinsic result at Var(1) and another World at Var(0).

UmType

Unsigned, memory-sized integers.

UmTerm

An intger literal.

Fields of UmTerm

val: u64

UmSucc

An integer literal equal to 1 + pred

Fields of UmSucc

pred: Term

UmElim

Case match on a Um.

Fields of UmElim

arg: Term
res_type: Term
on_zero: Term
on_succ: Term

Trait Implementations

impl Debug for TermKind

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

Formats the value using the given formatter.

impl Clone for TermKind

fn clone(&self) -> TermKind

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq for TermKind

fn eq(&self, __arg_0: &TermKind) -> bool

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

fn ne(&self, __arg_0: &TermKind) -> bool

This method tests for !=.