Enum minitt::ast::Value

pub enum Value {
    Lambda(Closure),
    Unit,
    One,
    Type(Level),
    Pi(Box<Self>, Closure),
    Sigma(Box<Self>, Closure),
    Pair(Box<Self>, Box<Self>),
    Constructor(String, Box<Self>),
    Split(CaseTree),
    Sum(CaseTree),
    Neutral(Neutral),
}

Val in Mini-TT, value term.
Terms are either of canonical form or neutral form.

$u,v,t ::=$

Variants

Lambda(Closure)

$\lambda\ f$. Canonical form: lambda abstraction.

Unit

$0$. Canonical form: unit instance.

One

$\textbf{1}$. Canonical form: unit type.

Type(Level)

$\textsf{U}$. Canonical form: type universe.

Pi(Box<Self>, Closure)

$\Pi \ t\ g$. Canonical form: pi type (type for dependent functions).

Sigma(Box<Self>, Closure)

$\Sigma \ t\ g$. Canonical form: sigma type (type for dependent pair).

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

$u,v$. Canonical form: Pair value (value for sigma).

Constructor(String, Box<Self>)

$c \ t$. Canonical form: call to a constructor.

Split(CaseTree)

$\textsf{fun}\ s$. Canonical form: case-split.

Sum(CaseTree)

$\textsf{Sum}\ s$. Canonical form: sum type.

Neutral(Neutral)

$[k]$. Neutral form.

Implementations

impl Value

pub fn level_safe(&self) -> Option<Level>

This is not present in Mini-TT.
Calculate the level of self, return None if it's not a type value.

pub fn level(&self) -> u32

This is not present in Mini-TT.
This is called levelView in Agda.

pub fn first(self) -> Self

$$ \begin{alignedat}{2} & (u,v).1 &&= u \\ & [k].1 &&= [k.1] \\ \end{alignedat} $$ vfst in Mini-TT.
Run .1 on a Pair.

pub fn second(self) -> Self

$$ \begin{alignedat}{2} & (u,v).2 &&= v \\ & [k].2 &&= [k.2] \\ \end{alignedat} $$ vsnd in Mini-TT.
Run .2 on a Pair.

pub fn destruct(self) -> (Self, Self)

Combination of vsnd and vfst in Mini-TT.
Run .2 on a Pair.

pub fn apply(self, argument: Self) -> Self

$$ \begin{alignedat}{2} & \textsf{app} (\lambda \ f) v &&= \textsf{inst} \ f \ v \\ & \textsf{app} (\textsf{fun}\lang S,\rho \rang (c_i \ v)) &&= \textsf{app}(⟦ M_i ⟧ \rho)v \\ & && \ \ \ \ \ \ \textnormal{where} \ S=(c_1 \rightarrow M_1 | ... | c_n \rightarrow M_n) \\ & \textsf{app} (\textsf{fun} \ s) [k] &&= [s \ k] \\ & \textsf{app} [k] \ v &&= [k \ v] \end{alignedat} $$ app in Mini-TT.

Trait Implementations

impl Clone for Value

fn clone(&self) -> Value

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Value

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

Formats the value using the given formatter.

impl Display for Value

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

Formats the value using the given formatter.

impl ReadBack for Value

type NormalForm = NormalExpression

Corresponding normal form type for the read-backable structures.
This is needed because Rust does not support Higher-Kinded Types :(

fn read_back(self, index: u32) -> Self::NormalForm

$$ \begin{alignedat}{2} & \textsf{R}_i (\lambda \ f) &&= \lambda \ \textsf{x}_i \ . \ \textsf{R}_{i+1} (\textsf{inst}\ f [ \textsf{x}_i ]) \\ & \textsf{R}_i (u,v) &&= (\textsf{R}_i u,\textsf{R}_i v) \\ & \textsf{R}_i 0 &&= 0 \\ & \textsf{R}_i (c\ v) &&= c \ (\textsf{R}_i v) \\ & \textsf{R}_i (\textsf{fun}\lang S,\rho\rang) &&= \textsf{fun}\lang S, \textsf{R}_i \rho\rang \\ & \textsf{R}_i (\textsf{Sum}\lang S,\rho\rang) &&= \textsf{Sum}\lang S, \textsf{R}_i \rho\rang \\ & \textsf{R}_i \textsf{U} &&= \textsf{U} \\ & \textsf{R}_i \textbf{1} &&= \textbf{1} \\ & \textsf{R}_i (\Pi\ t\ g) &&= \Pi \textsf{x}_i : \textsf{R}_i \ t \ . \ \textsf{R}_{i+1} (\textsf{inst}\ g [ \textsf{x}_i ]) \\ & \textsf{R}_i (\Sigma\ t\ g) &&= \Sigma \textsf{x}_i : \textsf{R}_i \ t \ . \ \textsf{R}_{i+1} (\textsf{inst}\ g [ \textsf{x}_i ]) \\ & \textsf{R}_i [k] &&= [\textsf{R}_i\ k] \end{alignedat} $$ rbV in Mini-TT.

fn read_back_please(self) -> Self::NormalForm

Sometimes you don't want to pass an argument, and let me do this for you :)

fn normal(
    index: u32,
    me: Self,
    other: Self
) -> (Self::NormalForm, Self::NormalForm)

eqNf in Mini-TT, but returning normal forms for error reporting.
Whether two structures are equivalent up to normal form.