[−][src]Trait minitt::check::read_back::ReadBack
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 :(
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.
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)
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.
Implementors
impl ReadBack for Value
[src]
type NormalForm = NormalExpression
fn read_back(self, index: u32) -> Self::NormalForm
[src]
$$
\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
[src]
type NormalForm = NormalCase
fn read_back(self, index: u32) -> Self::NormalForm
[src]
impl ReadBack for Neutral
[src]
type NormalForm = NormalNeutral
fn read_back(self, index: u32) -> Self::NormalForm
[src]
$$
\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>
[src]
type NormalForm = NormalTelescope
fn read_back(self, index: u32) -> Self::NormalForm
[src]
$$
\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.