Enum 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

pred: Term

LevelMax

Universe level max(a, b)

Fields

a: Term

b: Term

Type

The type of types, indexed by levels.

Fields

level: Term

Var(usize)

A variable.

FuncType

The type of functions. (ie pi types)

Fields

arg_type: Term

res_type: Term

FuncTerm

Functions.

Fields

body: Term

FuncApp

Function application.

Fields

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

head_type: Term

tail_type: Term

PairTerm

A pair term.

Fields

head: Term

tail: Term

PairElim

Dependent pair elimination.

Fields

pair: Term

res: Term

head_type: Term

tail_type: Term

NeverType

The canonical empty type, (ie. bottom).

NeverElim

Never type elimintator

Fields

never: Term

EitherType

Disjoint union, sum type.

Fields

left_type: Term

right_type: Term

EitherLeft

Inject left.

Fields

val: Term

EitherRight

Inject right.

Fields

val: Term

EitherElim

Case match on a sum type.

Fields

arg: Term

arg_type: Term

res_type: Term

on_left: Term

on_right: Term

IdentType

The type of identifications (a == b)

Fields

term_type: Term

a: Term

b: Term

IdentTerm

Reflexivity,

IdentElim

J-elimination for identities.

Fields

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

rec_type: Term

RecTerm

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

Fields

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

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

val: u64

UmSucc

An integer literal equal to 1 + pred

Fields

pred: Term

UmElim

Case match on a Um.

Fields

arg: Term

res_type: Term

on_zero: Term

on_succ: Term

Trait Implementations

impl Clone for TermKind

fn clone(&self) -> TermKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for TermKind

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

Formats the value using the given formatter.

impl PartialEq for TermKind

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for TermKind