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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
use crate::normal::*;
use crate::reduce::*;
use crate::syntax::*;
pub fn generate_value<Name: NameTrait>(id: u32) -> Value<Name> {
use crate::syntax::GenericNeutral as Neutral;
Value::Neutral(Neutral::Generated(id))
}
trait ReadBack {
type NormalForm;
fn read_back(self, index: u32) -> Self::NormalForm;
}
impl<Name: DebuggableNameTrait> ReadBack for Value<Name> {
type NormalForm = NormalExpression<Name>;
fn read_back(self, index: u32) -> Self::NormalForm {
match self {
Value::Lambda(closure) => NormalExpression::Lambda(
index,
Box::new(
closure
.instantiate(generate_value(index))
.read_back(index + 1),
),
),
Value::Unit => NormalExpression::Unit,
Value::One => NormalExpression::One,
Value::Type => NormalExpression::Type,
Value::Pi(first, second) => NormalExpression::Pi(
Box::new(first.read_back(index)),
index,
Box::new(
second
.instantiate(generate_value(index))
.read_back(index + 1),
),
),
Value::Sigma(first, second) => NormalExpression::Sigma(
Box::new(first.read_back(index)),
index,
Box::new(
second
.instantiate(generate_value(index))
.read_back(index + 1),
),
),
Value::Pair(first, second) => NormalExpression::Pair(
Box::new(first.read_back(index)),
Box::new(second.read_back(index)),
),
Value::Constructor(name, body) => {
NormalExpression::Constructor(name, Box::new(body.read_back(index)))
}
Value::Function((case_tree, context)) => {
NormalExpression::Function((case_tree, Box::new(context.read_back(index))))
}
Value::Sum((constructors, context)) => {
NormalExpression::Sum((constructors, Box::new(context.read_back(index))))
}
Value::Neutral(neutral) => NormalExpression::Neutral(neutral.read_back(index)),
}
}
}
impl<Name: DebuggableNameTrait> ReadBack for Telescope<Name> {
type NormalForm = NormalTelescope<Name>;
fn read_back(self, index: u32) -> Self::NormalForm {
use crate::syntax::GenericTelescope::*;
match self {
Nil => Nil,
UpDec(context, declaration) => UpDec(Box::new(context.read_back(index)), declaration),
UpVar(context, pattern, val) => UpVar(
Box::new(context.read_back(index)),
pattern,
val.read_back(index),
),
}
}
}
impl<Name: DebuggableNameTrait> ReadBack for Neutral<Name> {
type NormalForm = NormalNeutral<Name>;
fn read_back(self, index: u32) -> Self::NormalForm {
use crate::syntax::GenericNeutral::*;
match self {
Generated(index) => Generated(index),
Application(function, argument) => Application(
Box::new(function.read_back(index)),
Box::new(argument.read_back(index)),
),
First(neutral) => First(Box::new(neutral.read_back(index))),
Second(neutral) => Second(Box::new(neutral.read_back(index))),
Function((case_tree, context), body) => Function(
(case_tree, Box::new(context.read_back(index))),
Box::new(body.read_back(index)),
),
}
}
}