minitt 0.0.3

Mini-TT, a dependently-typed lambda calculus, implementated in Rust
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57

use crate::normal::*;
use crate::reduce::*;
use crate::syntax::*;

trait ReadBack {
    type NormalForm;

    /// Interface for `rbV`, `rbN` and `rbRho` in Mini-TT.
    fn read_back(self) -> Self::NormalForm;
}

impl<Name: DebuggableNameTrait> ReadBack for Value<Name> {
    type NormalForm = NormalExpression<Name>;

    /// `rbV` in Mini-TT.
    fn read_back(self) -> Self::NormalForm {
        unimplemented!()
    }
}

impl<Name: DebuggableNameTrait> ReadBack for Telescope<Name> {
    type NormalForm = NormalTelescope<Name>;

    /// `rbRho` in Mini-TT.
    fn read_back(self) -> Self::NormalForm {
        use crate::syntax::GenericTelescope::*;
        match self {
            Nil => Nil,
            UpDec(context, declaration) => UpDec(Box::new(context.read_back()), declaration),
            UpVar(context, pattern, val) => {
                UpVar(Box::new(context.read_back()), pattern, val.read_back())
            }
        }
    }
}

impl<Name: DebuggableNameTrait> ReadBack for Neutral<Name> {
    type NormalForm = NormalNeutral<Name>;

    /// `rbN` in Mini-TT.
    fn read_back(self) -> Self::NormalForm {
        use crate::syntax::GenericNeutral::*;
        match self {
            Generated(index) => Generated(index),
            Application(function, argument) => Application(
                Box::new(function.read_back()),
                Box::new(argument.read_back()),
            ),
            First(neutral) => First(Box::new(neutral.read_back())),
            Second(neutral) => Second(Box::new(neutral.read_back())),
            Function((case_tree, context), body) => Function(
                (case_tree, Box::new(context.read_back())),
                Box::new(body.read_back()),
            ),
        }
    }
}