Trait minitt::check::read_back::ReadBack

pub trait ReadBack: Sized {
    type NormalForm: Eq + Display;
    fn read_back(self, index: u32) -> Self::NormalForm;

    fn read_back_please(self) -> Self::NormalForm { ... }
    fn normal(
        index: u32, 
        me: Self, 
        other: Self
    ) -> (Self::NormalForm, Self::NormalForm) { ... }
}

Since all of Value, Neutral and Telescope have a read back function, I extracted this common interface for them.

Implementing Sized to make the compiler happy.

Associated Types

type NormalForm: Eq + Display

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

Loading content...

Required methods

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] \\ & && \\ & \textsf{R}_i \textsf{x}_j &&= \textsf{x}_j \\ & \textsf{R}_i (k\ v) &&= (\textsf{R}_i\ k) (\textsf{R}_i\ v) \\ & \textsf{R}_i (k.1) &&= (\textsf{R}_i\ k) .1 \\ & \textsf{R}_i (k.2) &&= (\textsf{R}_i\ k) .2 \\ & \textsf{R}_i (\lang S,\rho \rang\ k) &&= \lang S,\textsf{R}_i \rho \rang (\textsf{R}_i\ k) \\ & && \\ & \textsf{R}_i (\rho,p=v) &&= \textsf{R}_i\ \rho,p=\textsf{R}_i\ v \\ & \textsf{R}_i (\rho,D) &&= \textsf{R}_i\ \rho,D \\ & \textsf{R}_i () &&= () \end{alignedat} $$ Interface for rbV, rbN and rbRho in Mini-TT.

Loading content...

Provided methods

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.

Loading content...

Implementors

impl ReadBack for Value

type NormalForm = NormalExpression

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.

impl ReadBack for Case

type NormalForm = NormalCase

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

impl ReadBack for Neutral

type NormalForm = NormalNeutral

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

$$ \begin{alignedat}{2} & \textsf{R}_i \textsf{x}_j &&= \textsf{x}_j \\ & \textsf{R}_i (k\ v) &&= (\textsf{R}_i\ k) (\textsf{R}_i\ v) \\ & \textsf{R}_i (k.1) &&= (\textsf{R}_i\ k) .1 \\ & \textsf{R}_i (k.2) &&= (\textsf{R}_i\ k) .2 \\ & \textsf{R}_i (\lang S,\rho \rang\ k) &&= \lang S,\textsf{R}_i \rho \rang (\textsf{R}_i\ k) \end{alignedat} $$ rbN in Mini-TT.

impl<'_> ReadBack for &'_ GenericTelescope<Value>

type NormalForm = NormalTelescope

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

$$ \begin{alignedat}{2} & \textsf{R}_i (\rho,p=v) &&= \textsf{R}_i\ \rho,p=\textsf{R}_i\ v \\ & \textsf{R}_i (\rho,D) &&= \textsf{R}_i\ \rho,D \\ & \textsf{R}_i () &&= () \end{alignedat} $$ rbRho in Mini-TT.

Loading content...