Enum GenericTelescope

pub enum GenericTelescope<Value: Clone> {
    Nil,
    UpDec(Rc<Self>, Declaration),
    UpVar(Rc<Self>, Pattern, Value),
}

Generic definition for two kinds of telescopes.
Value can be specialized with Value or NormalExpression.

Implementing Eq because of NormalExpression

Variants

Nil

$()$, Empty telescope.

UpDec(Rc<Self>, Declaration)

$\rho, p=D$, In Mini-TT, checked declarations are put here. However, it’s not possible to store a recursive declaration as an Expression (which is a member of Declaration) here.

The problem is quite complicated and can be reproduced by checking out 0.1.5 revision and type-check this code (Type was U and Sum was sum at that time):

rec nat : U = sum { Zero 1 | Suc nat };
-- Inductive definition of nat

let one : nat = Zero 0;
let two : nat = Suc one;
-- Unresolved reference

UpVar(Rc<Self>, Pattern, Value)

$\rho, p=v$, Usually a local variable, introduced in your telescope

Implementations

impl GenericTelescope<Value>

pub fn resolve(&self, name: &str) -> Result<Value, String>

$$ \textnormal{If} \ x \ \textnormal{is\ in}\ p, \\ \begin{alignedat}{2} & (\rho, p=v)(x) &&= \textsf{proj}^p_x(v) \\ & (\rho, p:A=M)(x) &&= \textsf{proj}^p_x(⟦ M ⟧ \rho) \\ & (\rho, \textsf{rec}\ p:A=M)(x) &&= \textsf{proj}^p_x(⟦ M ⟧ (\rho, \textsf{rec}\ p:A=M)) \end{alignedat} \\ \textnormal{If} \ x \ \textnormal{is\ not\ in}\ p, \\ \begin{alignedat}{2} & (\rho, p=v)(x) &&= \rho(x) \\ & (\rho, D)(x) &&= \rho(x) \\ \end{alignedat} $$ getRho in Mini-TT.

Trait Implementations

impl<Value: Clone + Clone> Clone for GenericTelescope<Value>

fn clone(&self) -> GenericTelescope<Value>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<Value: Debug + Clone> Debug for GenericTelescope<Value>

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

Formats the value using the given formatter.

impl<Value: Clone + Display> Display for GenericTelescope<Value>

Actually it’s for NeutralTelescope

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

Formats the value using the given formatter.

impl<Value: PartialEq + Clone> PartialEq for GenericTelescope<Value>

fn eq(&self, other: &GenericTelescope<Value>) -> 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 ReadBack for &GenericTelescope<Value>

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.

type NormalForm = Rc<GenericTelescope<NormalExpression>>

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

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.

impl<Value: Eq + Clone> Eq for GenericTelescope<Value>

impl<Value: Clone> StructuralPartialEq for GenericTelescope<Value>