Enum minitt::ast::Expression

pub enum Expression {
    Unit,
    One,
    Type(Level),
    Void,
    Var(String),
    Sum(Branch),
    Split(Branch),
    Merge(Box<Self>, Box<Self>),
    Pi(Typed, Box<Self>),
    Sigma(Typed, Box<Self>),
    Lambda(Pattern, Option<AnonymousValue>, Box<Self>),
    First(Box<Self>),
    Second(Box<Self>),
    Application(Box<Self>, Box<Self>),
    Pair(Box<Self>, Box<Self>),
    Constructor(String, Box<Self>),
    Constant(Pattern, Box<Self>, Box<Self>),
    Declaration(Box<Declaration>, Box<Self>),
}

Exp in Mini-TT. Expression language for Mini-TT.

$M,\ N,\ A,\ B ::=$

Variants

Unit

$0$

One

$\textbf{1}$

Type(Level)

$\textsf{U}$, Type. Extended with levels.

Void

Empty file

Var(String)

$x$, bla

Sum(Branch)

$\textsf{Sum} \ S$, Sum { Bla x }

Split(Branch)

$\textsf{fun} \ S$, split { Bla x => y }

Merge(Box<Self>, Box<Self>)

This is an extension to Mini-TT, A ++ B.

Pi(Typed, Box<Self>)

$\Pi p : A. B$ or $A \rightarrow B$, \Pi a: b. c or A -> B

Sigma(Typed, Box<Self>)

$\Sigma p : A. B$ or $A \times B$, \Sigma a: b. c or A * B

Lambda(Pattern, Option<AnonymousValue>, Box<Self>)

$\lambda p. M$, \lambda a. c, the optional value is the type of the argument.
This cannot be specified during parsing because it's used for generated intermediate values during type-checking.

First(Box<Self>)

$M.1$, bla.1

Second(Box<Self>)

$M.2$, bla.2

Application(Box<Self>, Box<Self>)

$M \ N$, f a

Pair(Box<Self>, Box<Self>)

$M, N$, a, b

Constructor(String, Box<Self>)

$\textsf{c}\ M$, Cons a

Constant(Pattern, Box<Self>, Box<Self>)

const a = b, this is an extension: a declaration whose type-signature is inferred. This is very similar to a Declaration.

Declaration(Box<Declaration>, Box<Self>)

$D; M$, let bla or rec bla

Methods

impl Expression

pub fn eval_to_sum(self, context: Telescope) -> Option<Vec<String>>

This is not present in Mini-TT.
Return true if self is a Sum or Merge. This is quite expensive! Can we optimize it a little bit?

pub fn eval(self, context: Telescope) -> Value

$$ \begin{alignedat}{2} & ⟦ \lambda p.M ⟧ \rho &&= \lang \lambda p.M,\rho \rang \\ & ⟦ x ⟧ \rho &&= \rho(x) \\ & ⟦ M \ N ⟧ \rho &&= \textsf{app} (⟦ M ⟧ \rho, ⟦ N ⟧ \rho) \\ & ⟦ \Pi \ p:A.B ⟧ \rho &&= \Pi (⟦ A ⟧ \rho) \lang \lambda p.B,\rho \rang \\ & ⟦ \textsf{U} ⟧ \rho &&= \textsf{U} \\ & ⟦ D; M ⟧ \rho &&= ⟦ M ⟧ (\rho(x); D) \\ & && \\ & ⟦ M,N ⟧ \rho &&= (⟦ M ⟧ \rho, ⟦ N ⟧ \rho) \\ & ⟦ 0 ⟧ \rho &&= 0 \\ & ⟦ M.1 ⟧ \rho &&= (⟦ M\rho ⟧).1 \\ & ⟦ M.2 ⟧ \rho &&= (⟦ M\rho ⟧).2 \\ & ⟦ \Sigma \ p:A.B ⟧ \rho &&= \Sigma (⟦ A ⟧ \rho) \lang \lambda p.B,\rho \rang \\ & ⟦ \textbf{1} ⟧ \rho &&= \textbf{1} \\ & && \\ & ⟦ c \ M ⟧ \rho &&= c(⟦ M ⟧ \rho) \\ & ⟦ \textsf{fun} \ S ⟧ \rho &&= \textsf{fun} \lang S,\rho \rang \\ & ⟦ \textsf{Sum} \ S ⟧ \rho &&= \textsf{Sum} \lang S,\rho \rang \end{alignedat} $$ eval in Mini-TT.
Evaluate an Expression to a Value under a Telescope, panic if not well-typed.

Trait Implementations

impl Eq for Expression

fn assert_receiver_is_total_eq(&self)

impl Clone for Expression

fn clone(&self) -> Expression

Returns a copy of the value.

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

Performs copy-assignment from source.

impl PartialEq<Expression> for Expression

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

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

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

This method tests for !=.

impl Debug for Expression

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

Formats the value using the given formatter.

impl Display for Expression

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

Formats the value using the given formatter.