minitt/check/read_back.rs
1use std::collections::BTreeMap;
2use std::fmt::Display;
3use std::rc::Rc;
4
5use either::Either;
6
7use crate::ast::*;
8
9/// `NRho` in Mini-TT, normal form telescopes (contexts).
10pub type NormalTelescope = Rc<GenericTelescope<NormalExpression>>;
11
12pub type NormalCase = GenericCase<Either<NormalExpression, Expression>, NormalExpression>;
13
14/// `NSClos` in Mini-TT, normal form closures.
15pub type NormalCaseTree = GenericBranch<NormalCase>;
16
17/// `NNeut` in Mini-TT, normal form neutral values.
18pub type NormalNeutral = GenericNeutral<NormalExpression>;
19
20/// `NExp` in Mini-TT, normal form expressions.<br/>
21/// Deriving `Eq` so we can do comparison.
22///
23/// $E ::=$
24#[derive(Debug, Clone, Eq, PartialEq)]
25pub enum NormalExpression {
26 /// $\lambda \textsf{x}_i\ .\ E$
27 Lambda(u32, Box<Self>),
28 /// $E_1, E_2$
29 Pair(Box<Self>, Box<Self>),
30 /// $0$
31 Unit,
32 /// $\textbf{1}$
33 One,
34 /// $\textsf{U}$
35 Type(Level),
36 /// $\Pi \textsf{x}_i:E_1.E_2$
37 Pi(Box<Self>, u32, Box<Self>),
38 /// $\Sigma \textsf{x}_i:E_1.E_2$
39 Sigma(Box<Self>, u32, Box<Self>),
40 /// $c\ E$
41 Constructor(String, Box<Self>),
42 /// $\textsf{fun}\lang S,\alpha \rang$
43 Split(NormalCaseTree),
44 /// $\textsf{Sum}\lang S,\alpha \rang$
45 Sum(NormalCaseTree),
46 /// $[K]$
47 Neutral(NormalNeutral),
48}
49
50/// `genV` in Mini-TT.
51pub fn generate_value(id: u32) -> Value {
52 use crate::ast::GenericNeutral as Neutral;
53 Value::Neutral(Neutral::Generated(id))
54}
55
56/// Since all of `Value`, `Neutral` and `Telescope` have a read back function,
57/// I extracted this common interface for them.
58///
59/// Implementing `Sized` to make the compiler happy.
60pub trait ReadBack: Sized {
61 /// Corresponding normal form type for the read-backable structures.<br/>
62 /// This is needed because Rust does not support Higher-Kinded Types :(
63 type NormalForm: Eq + Display;
64
65 /// $$
66 /// \begin{alignedat}{2}
67 /// & \textsf{R}_i (\lambda \ f) &&= \lambda \ \textsf{x}_i
68 /// \ . \ \textsf{R}\_{i+1} (\textsf{inst}\ f [ \textsf{x}\_i ]) \\\\
69 /// & \textsf{R}_i (u,v) &&= (\textsf{R}_i u,\textsf{R}_i v) \\\\
70 /// & \textsf{R}_i 0 &&= 0 \\\\
71 /// & \textsf{R}_i (c\ v) &&= c \ (\textsf{R}_i v) \\\\
72 /// & \textsf{R}_i (\textsf{fun}\lang S,\rho\rang) &&= \textsf{fun}\lang S,
73 /// \textsf{R}_i \rho\rang \\\\
74 /// & \textsf{R}_i (\textsf{Sum}\lang S,\rho\rang) &&= \textsf{Sum}\lang S,
75 /// \textsf{R}_i \rho\rang \\\\
76 /// & \textsf{R}_i \textsf{U} &&= \textsf{U} \\\\
77 /// & \textsf{R}_i \textbf{1} &&= \textbf{1} \\\\
78 /// & \textsf{R}_i (\Pi\ t\ g) &&= \Pi \textsf{x}_i : \textsf{R}\_i \ t
79 /// \ . \ \textsf{R}\_{i+1} (\textsf{inst}\ g [ \textsf{x}\_i ]) \\\\
80 /// & \textsf{R}_i (\Sigma\ t\ g) &&= \Sigma \textsf{x}_i : \textsf{R}\_i \ t
81 /// \ . \ \textsf{R}\_{i+1} (\textsf{inst}\ g [ \textsf{x}\_i ]) \\\\
82 /// & \textsf{R}_i [k] &&= [\textsf{R}\_i\ k] \\\\
83 /// & && \\\\
84 /// & \textsf{R}_i \textsf{x}\_j &&= \textsf{x}\_j \\\\
85 /// & \textsf{R}_i (k\ v) &&= (\textsf{R}_i\ k) (\textsf{R}_i\ v) \\\\
86 /// & \textsf{R}_i (k.1) &&= (\textsf{R}_i\ k) .1 \\\\
87 /// & \textsf{R}_i (k.2) &&= (\textsf{R}_i\ k) .2 \\\\
88 /// & \textsf{R}_i (\lang S,\rho \rang\ k) &&=
89 /// \lang S,\textsf{R}\_i \rho \rang (\textsf{R}_i\ k) \\\\
90 /// & && \\\\
91 /// & \textsf{R}_i (\rho,p=v) &&= \textsf{R}_i\ \rho,p=\textsf{R}\_i\ v \\\\
92 /// & \textsf{R}_i (\rho,D) &&= \textsf{R}_i\ \rho,D \\\\
93 /// & \textsf{R}_i () &&= ()
94 /// \end{alignedat}
95 /// $$
96 /// Interface for `rbV`, `rbN` and `rbRho` in Mini-TT.
97 fn read_back(self, index: u32) -> Self::NormalForm;
98
99 /// Sometimes you don't want to pass an argument, and let me do this for you :)
100 fn read_back_please(self) -> Self::NormalForm {
101 self.read_back(0)
102 }
103
104 /// `eqNf` in Mini-TT, but returning normal forms for error reporting.<br/>
105 /// Whether two structures are equivalent up to normal form.
106 fn normal(index: u32, me: Self, other: Self) -> (Self::NormalForm, Self::NormalForm) {
107 let me_read_back = me.read_back(index);
108 let other_read_back = other.read_back(index);
109 (me_read_back, other_read_back)
110 }
111}
112
113impl ReadBack for Value {
114 type NormalForm = NormalExpression;
115
116 /// $$
117 /// \begin{alignedat}{2}
118 /// & \textsf{R}_i (\lambda \ f) &&= \lambda \ \textsf{x}_i
119 /// \ . \ \textsf{R}\_{i+1} (\textsf{inst}\ f [ \textsf{x}\_i ]) \\\\
120 /// & \textsf{R}_i (u,v) &&= (\textsf{R}_i u,\textsf{R}_i v) \\\\
121 /// & \textsf{R}_i 0 &&= 0 \\\\
122 /// & \textsf{R}_i (c\ v) &&= c \ (\textsf{R}_i v) \\\\
123 /// & \textsf{R}_i (\textsf{fun}\lang S,\rho\rang) &&= \textsf{fun}\lang S,
124 /// \textsf{R}_i \rho\rang \\\\
125 /// & \textsf{R}_i (\textsf{Sum}\lang S,\rho\rang) &&= \textsf{Sum}\lang S,
126 /// \textsf{R}_i \rho\rang \\\\
127 /// & \textsf{R}_i \textsf{U} &&= \textsf{U} \\\\
128 /// & \textsf{R}_i \textbf{1} &&= \textbf{1} \\\\
129 /// & \textsf{R}_i (\Pi\ t\ g) &&= \Pi \textsf{x}_i : \textsf{R}\_i \ t
130 /// \ . \ \textsf{R}\_{i+1} (\textsf{inst}\ g [ \textsf{x}\_i ]) \\\\
131 /// & \textsf{R}_i (\Sigma\ t\ g) &&= \Sigma \textsf{x}_i : \textsf{R}\_i \ t
132 /// \ . \ \textsf{R}\_{i+1} (\textsf{inst}\ g [ \textsf{x}\_i ]) \\\\
133 /// & \textsf{R}_i [k] &&= [\textsf{R}\_i\ k]
134 /// \end{alignedat}
135 /// $$
136 /// `rbV` in Mini-TT.
137 fn read_back(self, index: u32) -> Self::NormalForm {
138 use crate::check::read_back::NormalExpression::*;
139 match self {
140 Value::Lambda(closure) => {
141 let closure = closure
142 .instantiate(generate_value(index))
143 .read_back(index + 1);
144 Lambda(index, Box::new(closure))
145 }
146 Value::Unit => Unit,
147 Value::One => One,
148 Value::Type(level) => Type(level),
149 Value::Pi(input, output) => {
150 let output = output
151 .instantiate(generate_value(index))
152 .read_back(index + 1);
153 Pi(Box::new(input.read_back(index)), index, Box::new(output))
154 }
155 Value::Sigma(first, second) => {
156 let second = second
157 .instantiate(generate_value(index))
158 .read_back(index + 1);
159 Sigma(Box::new(first.read_back(index)), index, Box::new(second))
160 }
161 Value::Pair(first, second) => Pair(
162 Box::new(first.read_back(index)),
163 Box::new(second.read_back(index)),
164 ),
165 Value::Constructor(name, body) => Constructor(name, Box::new(body.read_back(index))),
166 Value::Split(case_tree) => Split(read_back_branches(index, case_tree)),
167 Value::Sum(constructors) => Sum(read_back_branches(index, constructors)),
168 Value::Neutral(neutral) => Neutral(neutral.read_back(index)),
169 }
170 }
171}
172
173fn read_back_branches(index: u32, branches: CaseTree) -> NormalCaseTree {
174 let mut read_back_constructors = BTreeMap::new();
175 for (name, case) in branches.into_iter() {
176 read_back_constructors.insert(name, Box::new(case.read_back(index)));
177 }
178 read_back_constructors
179}
180
181impl ReadBack for Case {
182 type NormalForm = NormalCase;
183
184 fn read_back(self, index: u32) -> Self::NormalForm {
185 Self::NormalForm::new(
186 self.expression.map_left(|l| l.read_back(index)),
187 self.context.read_back(index),
188 )
189 }
190}
191
192impl ReadBack for &GenericTelescope<Value> {
193 type NormalForm = NormalTelescope;
194
195 /// $$
196 /// \begin{alignedat}{2}
197 /// & \textsf{R}_i (\rho,p=v) &&= \textsf{R}_i\ \rho,p=\textsf{R}\_i\ v \\\\
198 /// & \textsf{R}_i (\rho,D) &&= \textsf{R}_i\ \rho,D \\\\
199 /// & \textsf{R}_i () &&= ()
200 /// \end{alignedat}
201 /// $$
202 /// `rbRho` in Mini-TT.
203 fn read_back(self, index: u32) -> Self::NormalForm {
204 use crate::ast::GenericTelescope::*;
205 match self {
206 Nil => Rc::new(Nil),
207 UpDec(context, declaration) => {
208 Rc::new(UpDec(context.read_back(index), declaration.clone()))
209 }
210 UpVar(context, pattern, val) => Rc::new(UpVar(
211 context.read_back(index),
212 pattern.clone(),
213 val.clone().read_back(index),
214 )),
215 }
216 }
217}
218
219impl ReadBack for Neutral {
220 type NormalForm = NormalNeutral;
221
222 /// $$
223 /// \begin{alignedat}{2}
224 /// & \textsf{R}_i \textsf{x}\_j &&= \textsf{x}\_j \\\\
225 /// & \textsf{R}_i (k\ v) &&= (\textsf{R}_i\ k) (\textsf{R}_i\ v) \\\\
226 /// & \textsf{R}_i (k.1) &&= (\textsf{R}_i\ k) .1 \\\\
227 /// & \textsf{R}_i (k.2) &&= (\textsf{R}_i\ k) .2 \\\\
228 /// & \textsf{R}_i (\lang S,\rho \rang\ k) &&=
229 /// \lang S,\textsf{R}\_i \rho \rang (\textsf{R}_i\ k)
230 /// \end{alignedat}
231 /// $$
232 /// `rbN` in Mini-TT.
233 fn read_back(self, index: u32) -> Self::NormalForm {
234 use crate::ast::GenericNeutral::*;
235 match self {
236 Generated(index) => Generated(index),
237 Application(function, argument) => Application(
238 Box::new(function.read_back(index)),
239 Box::new(argument.read_back(index)),
240 ),
241 First(neutral) => First(Box::new(neutral.read_back(index))),
242 Second(neutral) => Second(Box::new(neutral.read_back(index))),
243 Split(case_tree, body) => Split(
244 read_back_branches(index, case_tree),
245 Box::new(body.read_back(index)),
246 ),
247 }
248 }
249}