Enum Term

pub enum Term<'a> {
    Wildcard,
    Type,
    StaticType,
    Constraint,
    Var(LocalRef<'a>),
    Apply {
        global: GlobalRef<'a>,
        args: &'a [TermId],
    },
    ApplyFull {
        global: GlobalRef<'a>,
        args: &'a [TermId],
    },
    Quote {
        type: TermId,
    },
    List {
        items: &'a [TermId],
        tail: Option<TermId>,
    },
    ListType {
        item_type: TermId,
    },
    Str(&'a str),
    StrType,
    Nat(u64),
    NatType,
    ExtSet {
        extensions: &'a [&'a str],
        rest: Option<TermId>,
    },
    ExtSetType,
    Adt {
        variants: TermId,
    },
    FuncType {
        inputs: TermId,
        outputs: TermId,
        extensions: TermId,
    },
    Control {
        values: TermId,
    },
    ControlType,
}

A term in the compile time meta language.

Variants

Wildcard

Standin for any term.

Type

The type of runtime types.

type : static

StaticType

The type of static types.

static : static

Constraint

The type of constraints.

constraint : static

Var(LocalRef<'a>)

A local variable.

Apply

A symbolic function application.

The arguments of this application cover only the explicit parameters of the referenced declaration, leaving out the implicit parameters. Once the type of the declaration is known, the implicit parameters can be inferred and the term replaced with Term::ApplyFull.

(GLOBAL ARG-0 ... ARG-n)

Fields

global: GlobalRef<'a>

Reference to the global declaration to apply.

args: &'a [TermId]

Arguments to the function, covering only the explicit parameters.

ApplyFull

A symbolic function application with all arguments applied.

The arguments to this application cover both the implicit and explicit parameters of the referenced declaration. Since this can be tedious to write out, only the explicit parameters can be provided via Term::Apply.

(@GLOBAL ARG-0 ... ARG-n)

Fields

global: GlobalRef<'a>

Reference to the global declaration to apply.

args: &'a [TermId]

Arguments to the function, covering both implicit and explicit parameters.

Quote

Quote a runtime type as a static type.

(quote T) : static where T : type.

Fields

type: TermId

The runtime type to be quoted.

Type: type

List

A list, with an optional tail.

• [ITEM-0 ... ITEM-n] : (list T) where T : static, ITEM-i : T.
• [ITEM-0 ... ITEM-n . TAIL] : (list item-type) where T : static, ITEM-i : T, TAIL : (list T).

Fields

items: &'a [TermId]

The items in the list.

item-i : item-type

tail: Option<TermId>

The tail of the list.

tail : (list item-type)

ListType

The type of lists, given a type for the items.

(list T) : static where T : static.

Fields

item_type: TermId

The type of the items in the list.

item_type : static

Str(&'a str)

A literal string.

"STRING" : str

StrType

The type of literal strings.

str : static

Nat(u64)

A literal natural number.

N : nat

NatType

The type of literal natural numbers.

nat : static

ExtSet

Extension set.

• (ext EXT-0 ... EXT-n) : ext-set
• (ext EXT-0 ... EXT-n . REST) : ext-set where REST : ext-set.

Fields

extensions: &'a [&'a str]

The items in the extension set.

rest: Option<TermId>

The rest of the extension set.

ExtSetType

The type of extension sets.

ext-set : static

Adt

An algebraic data type.

(adt VARIANTS) : type where VARIANTS : (list (list type)).

Fields

variants: TermId

List of variants in the algrebaic data type. Each of the variants is itself a list of runtime types.

FuncType

The type of functions, given lists of input and output types and an extension set.

Fields

inputs: TermId

The input types of the function, given as a list of runtime types.

inputs : (list type)

outputs: TermId

The output types of the function, given as a list of runtime types.

outputs : (list type)

extensions: TermId

The set of extensions that the function requires to be present in order to be called.

extensions : ext-set

Control

Control flow.

(ctrl VALUES) : ctrl where VALUES : (list type).

Fields

values: TermId

List of values.

ControlType

Type of control flow edges.

ctrl : static

Trait Implementations

impl<'a> Clone for Term<'a>

fn clone(&self) -> Term<'a>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'a> Debug for Term<'a>

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

Formats the value using the given formatter.

impl<'a> Default for Term<'a>

fn default() -> Self

Returns the “default value” for a type.

impl<'a> Hash for Term<'a>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<'a> PartialEq for Term<'a>

fn eq(&self, other: &Term<'a>) -> 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<'a> Eq for Term<'a>

impl<'a> StructuralPartialEq for Term<'a>