Skip to content

Commit b4e5f92

Browse files
brendanzabbrendanzab
committed
Improve naming consistency
1 parent 3f37faa commit b4e5f92

File tree

6 files changed

+115
-100
lines changed

6 files changed

+115
-100
lines changed

‎pikelet/src/core/projections/pretty.rs

+34-30
Original file line numberDiff line numberDiff line change
@@ -71,42 +71,46 @@ where
7171
.append(alloc.space())
7272
.append("{")
7373
.group()
74-
.append(alloc.concat(ty_entries.iter().map(|(name, r#type)| {
75-
(alloc.nil())
76-
.append(alloc.hardline())
77-
.append(alloc.text(name))
78-
.append(":")
79-
.append(
80-
(alloc.space())
81-
.append(pretty_term_prec(alloc, r#type, Prec::Term))
82-
.append(",")
83-
.group()
84-
.nest(4),
85-
)
86-
.nest(4)
87-
.group()
88-
})))
74+
.append(
75+
alloc.concat(ty_entries.iter().map(|(entry_name, entry_type)| {
76+
(alloc.nil())
77+
.append(alloc.hardline())
78+
.append(alloc.text(entry_name))
79+
.append(":")
80+
.append(
81+
(alloc.space())
82+
.append(pretty_term_prec(alloc, entry_type, Prec::Term))
83+
.append(",")
84+
.group()
85+
.nest(4),
86+
)
87+
.nest(4)
88+
.group()
89+
})),
90+
)
8991
.append("}"),
9092
Term::RecordTerm(term_entries) => (alloc.nil())
9193
.append("record")
9294
.append(alloc.space())
9395
.append("{")
9496
.group()
95-
.append(alloc.concat(term_entries.iter().map(|(name, term)| {
96-
(alloc.nil())
97-
.append(alloc.hardline())
98-
.append(alloc.text(name))
99-
.append("=")
100-
.append(
101-
(alloc.space())
102-
.append(pretty_term_prec(alloc, term, Prec::Term))
103-
.append(",")
104-
.group()
105-
.nest(4),
106-
)
107-
.nest(4)
108-
.group()
109-
})))
97+
.append(
98+
alloc.concat(term_entries.iter().map(|(entry_name, entry_term)| {
99+
(alloc.nil())
100+
.append(alloc.hardline())
101+
.append(alloc.text(entry_name))
102+
.append("=")
103+
.append(
104+
(alloc.space())
105+
.append(pretty_term_prec(alloc, entry_term, Prec::Term))
106+
.append(",")
107+
.group()
108+
.nest(4),
109+
)
110+
.nest(4)
111+
.group()
112+
})),
113+
)
110114
.append("}"),
111115
Term::RecordElim(head, name) => (alloc.nil())
112116
.append(pretty_term_prec(alloc, head, Prec::Atomic))

‎pikelet/src/core/projections/surface.rs

+6-4
Original file line numberDiff line numberDiff line change
@@ -40,10 +40,10 @@ pub fn delaborate_term(state: &mut State<'_>, term: &Term) -> surface::Term<Stri
4040
Term::RecordType(type_entries) => {
4141
let core_type_entries = type_entries
4242
.iter()
43-
.map(|(name, entry_type)| {
43+
.map(|(entry_name, entry_type)| {
4444
let entry_type = delaborate_term(state, entry_type);
45-
state.names.push(name.clone());
46-
(name.clone(), entry_type)
45+
state.names.push(entry_name.clone());
46+
(entry_name.clone(), entry_type)
4747
})
4848
.collect();
4949

@@ -52,7 +52,9 @@ pub fn delaborate_term(state: &mut State<'_>, term: &Term) -> surface::Term<Stri
5252
Term::RecordTerm(term_entries) => {
5353
let core_term_entries = term_entries
5454
.iter()
55-
.map(|(name, term)| (name.clone(), delaborate_term(state, term)))
55+
.map(|(entry_name, entry_term)| {
56+
(entry_name.clone(), delaborate_term(state, entry_term))
57+
})
5658
.collect();
5759
state.names.pop_many(term_entries.len());
5860

‎pikelet/src/core/semantics.rs

+29-25
Original file line numberDiff line numberDiff line change
@@ -54,31 +54,35 @@ pub fn eval_term(
5454
Term::Ann(term, _) => eval_term(globals, universe_offset, values, term),
5555
Term::RecordType(type_entries) => match type_entries.split_first() {
5656
None => Arc::new(Value::RecordTypeEmpty),
57-
Some(((name, r#type), rest_type)) => {
58-
let r#type = eval_term(globals, universe_offset, values, r#type);
57+
Some(((entry_name, entry_type), rest_type)) => {
58+
let entry_type = eval_term(globals, universe_offset, values, entry_type);
5959
let rest_types = Closure::new(
6060
universe_offset,
6161
values.clone(),
6262
Arc::new(Term::RecordType(rest_type.to_owned())), // FIXME: expensive to_owned?
6363
);
6464

65-
Arc::new(Value::RecordTypeExtend(name.clone(), r#type, rest_types))
65+
Arc::new(Value::RecordTypeExtend(
66+
entry_name.clone(),
67+
entry_type,
68+
rest_types,
69+
))
6670
}
6771
},
6872
Term::RecordTerm(term_entries) => {
6973
let value_entries = term_entries
7074
.iter()
71-
.map(|(name, term)| {
72-
let term = eval_term(globals, universe_offset, values, term);
73-
(name.clone(), term)
75+
.map(|(entry_name, entry_term)| {
76+
let entry_term = eval_term(globals, universe_offset, values, entry_term);
77+
(entry_name.clone(), entry_term)
7478
})
7579
.collect();
7680

7781
Arc::new(Value::RecordTerm(value_entries))
7882
}
79-
Term::RecordElim(head, field_name) => {
83+
Term::RecordElim(head, name) => {
8084
let head = eval_term(globals, universe_offset, values, head);
81-
eval_record_elim(globals, &head, field_name)
85+
eval_record_elim(globals, &head, name)
8286
}
8387
Term::FunctionType(param_type, body_type) => {
8488
let param_type = eval_term(globals, universe_offset, values, param_type);
@@ -131,10 +135,10 @@ pub fn eval_record_elim(globals: &Globals, head_value: &Value, name: &str) -> Ar
131135
Value::Elim(head, elims, r#type) => {
132136
let mut current_type = r#type.clone();
133137

134-
while let Value::RecordTypeExtend(current_name, entry_type, rest_type) =
138+
while let Value::RecordTypeExtend(entry_name, entry_type, rest_type) =
135139
current_type.as_ref()
136140
{
137-
if name == current_name {
141+
if name == entry_name {
138142
let mut elims = elims.clone(); // TODO: Avoid clone?
139143
elims.push(Elim::Record(name.to_owned()));
140144
return Arc::new(Value::Elim(head.clone(), elims, entry_type.clone()));
@@ -220,18 +224,18 @@ pub fn read_back_nf(
220224
_ => Term::Error, // TODO: Report error
221225
}
222226
}
223-
(Value::RecordTerm(_), Value::RecordTypeExtend(name, entry_type, rest_type)) => {
227+
(Value::RecordTerm(_), Value::RecordTypeExtend(entry_name, entry_type, rest_type)) => {
224228
let mut term_entries = BTreeMap::new();
225229

226-
let entry_value = eval_record_elim(globals, value, name);
230+
let entry_value = eval_record_elim(globals, value, entry_name);
227231
let entry_term = read_back_nf(globals, local_size, &entry_value, entry_type);
228-
term_entries.insert(name.clone(), Arc::new(entry_term));
232+
term_entries.insert(entry_name.clone(), Arc::new(entry_term));
229233
let mut r#type = eval_closure_elim(globals, rest_type, entry_value);
230234

231-
while let Value::RecordTypeExtend(name, entry_type, rest_type) = r#type.as_ref() {
232-
let entry_value = eval_record_elim(globals, value, name);
235+
while let Value::RecordTypeExtend(entry_name, entry_type, rest_type) = r#type.as_ref() {
236+
let entry_value = eval_record_elim(globals, value, entry_name);
233237
let entry_term = read_back_nf(globals, local_size, &entry_value, entry_type);
234-
term_entries.insert(name.clone(), Arc::new(entry_term));
238+
term_entries.insert(entry_name.clone(), Arc::new(entry_term));
235239
r#type = eval_closure_elim(globals, rest_type, entry_value);
236240
}
237241

@@ -263,20 +267,20 @@ pub fn read_back_type(globals: &Globals, local_size: LocalSize, r#type: &Value)
263267
match r#type {
264268
Value::Universe(level) => Term::Universe(*level),
265269
Value::Elim(head, spine, _) => read_back_elim(globals, local_size, head, spine),
266-
Value::RecordTypeExtend(name, entry_type, rest_type) => {
270+
Value::RecordTypeExtend(entry_name, entry_type, rest_type) => {
267271
let mut local_size = local_size;
268272
let mut type_entries = Vec::new();
269273

270274
let local = Arc::new(Value::local(local_size.next_level(), entry_type.clone()));
271275
let entry_type = Arc::new(read_back_type(globals, local_size, entry_type));
272-
type_entries.push((name.clone(), entry_type));
276+
type_entries.push((entry_name.clone(), entry_type));
273277
local_size = local_size.increment();
274278
let mut r#type = eval_closure_elim(globals, rest_type, local);
275279

276-
while let Value::RecordTypeExtend(name, entry_type, rest_type) = r#type.as_ref() {
280+
while let Value::RecordTypeExtend(entry_name, entry_type, rest_type) = r#type.as_ref() {
277281
let local = Arc::new(Value::local(local_size.next_level(), entry_type.clone()));
278282
let entry_type = Arc::new(read_back_type(globals, local_size, entry_type));
279-
type_entries.push((name.clone(), entry_type));
283+
type_entries.push((entry_name.clone(), entry_type));
280284
local_size = local_size.increment();
281285
r#type = eval_closure_elim(globals, rest_type, local);
282286
}
@@ -344,14 +348,14 @@ fn compare_types(
344348
is_equal_elim(globals, local_size, (head0, spine0), (head1, spine1))
345349
}
346350
(
347-
Value::RecordTypeExtend(name0, entry_type0, rest_type0),
348-
Value::RecordTypeExtend(name1, entry_type1, rest_type1),
351+
Value::RecordTypeExtend(entry_name0, entry_type0, rest_type0),
352+
Value::RecordTypeExtend(entry_name1, entry_type1, rest_type1),
349353
) => {
350-
name0 == name1
354+
entry_name0 == entry_name1
351355
&& compare_types(globals, local_size, entry_type0, entry_type1, compare)
352356
&& {
353-
let local =
354-
Arc::new(Value::local(local_size.next_level(), entry_type0.clone()));
357+
let level = local_size.next_level();
358+
let local = Arc::new(Value::local(level, entry_type0.clone()));
355359

356360
compare_types(
357361
globals,

‎pikelet/src/core/typing.rs

+4-3
Original file line numberDiff line numberDiff line change
@@ -200,16 +200,17 @@ pub fn check_term(state: &mut State<'_>, term: &Term, expected_type: &Arc<Value>
200200
let mut expected_type = expected_type.clone();
201201
let mut term_entries = term_entries.clone();
202202

203-
while let Value::RecordTypeExtend(name, entry_type, rest_type) = expected_type.as_ref()
203+
while let Value::RecordTypeExtend(entry_name, entry_type, rest_type) =
204+
expected_type.as_ref()
204205
{
205-
expected_type = match term_entries.remove(name) {
206+
expected_type = match term_entries.remove(entry_name) {
206207
Some(entry_term) => {
207208
check_term(state, &entry_term, entry_type);
208209
let entry_value = state.eval_term(&entry_term);
209210
state.eval_closure_elim(rest_type, entry_value)
210211
}
211212
None => {
212-
missing_names.push(name.clone());
213+
missing_names.push(entry_name.clone());
213214
state.eval_closure_elim(rest_type, Arc::new(Value::Error))
214215
}
215216
};

‎pikelet/src/surface/projections/core.rs

+8-8
Original file line numberDiff line numberDiff line change
@@ -312,26 +312,26 @@ pub fn check_term<S: AsRef<str>>(
312312
let mut expected_type = expected_type.clone();
313313
let mut core_term_entries = BTreeMap::new();
314314
let mut term_entries =
315-
(term_entries.iter()).fold(BTreeMap::new(), |mut acc, (name, term)| {
316-
match acc.entry(name.as_ref().to_owned()) {
317-
Entry::Vacant(entry) => drop(entry.insert(term)),
318-
Entry::Occupied(_) => duplicate_names.push(name.as_ref().to_owned()),
315+
(term_entries.iter()).fold(BTreeMap::new(), |mut acc, (entry_name, entry_term)| {
316+
match acc.entry(entry_name.as_ref().to_owned()) {
317+
Entry::Vacant(entry) => drop(entry.insert(entry_term)),
318+
Entry::Occupied(_) => duplicate_names.push(entry_name.as_ref().to_owned()),
319319
}
320320
acc
321321
});
322322

323-
while let core::Value::RecordTypeExtend(name, entry_type, rest_type) =
323+
while let core::Value::RecordTypeExtend(entry_name, entry_type, rest_type) =
324324
expected_type.as_ref()
325325
{
326-
expected_type = match term_entries.remove(name.as_str()) {
326+
expected_type = match term_entries.remove(entry_name.as_str()) {
327327
Some(term) => {
328328
let core_term = Arc::new(check_term(state, term, entry_type));
329329
let core_value = state.eval_term(&core_term);
330-
core_term_entries.insert(name.clone(), core_term);
330+
core_term_entries.insert(entry_name.clone(), core_term);
331331
state.eval_closure_elim(rest_type, core_value)
332332
}
333333
None => {
334-
missing_names.push(name.clone());
334+
missing_names.push(entry_name.clone());
335335
state.eval_closure_elim(rest_type, Arc::new(core::Value::Error))
336336
}
337337
};

‎pikelet/src/surface/projections/pretty.rs

+34-30
Original file line numberDiff line numberDiff line change
@@ -63,42 +63,46 @@ where
6363
.append(alloc.space())
6464
.append("{")
6565
.group()
66-
.append(alloc.concat(ty_entries.iter().map(|(name, r#type)| {
67-
(alloc.nil())
68-
.append(alloc.hardline())
69-
.append(alloc.text(name.as_ref()))
70-
.append(":")
71-
.append(
72-
(alloc.space())
73-
.append(pretty_term_prec(alloc, r#type, Prec::Term))
74-
.append(",")
75-
.group()
76-
.nest(4),
77-
)
78-
.nest(4)
79-
.group()
80-
})))
66+
.append(
67+
alloc.concat(ty_entries.iter().map(|(entry_name, entry_type)| {
68+
(alloc.nil())
69+
.append(alloc.hardline())
70+
.append(alloc.text(entry_name.as_ref()))
71+
.append(":")
72+
.append(
73+
(alloc.space())
74+
.append(pretty_term_prec(alloc, entry_type, Prec::Term))
75+
.append(",")
76+
.group()
77+
.nest(4),
78+
)
79+
.nest(4)
80+
.group()
81+
})),
82+
)
8183
.append("}"),
8284
Term::RecordTerm(_, term_entries) => (alloc.nil())
8385
.append("record")
8486
.append(alloc.space())
8587
.append("{")
8688
.group()
87-
.append(alloc.concat(term_entries.iter().map(|(name, term)| {
88-
(alloc.nil())
89-
.append(alloc.hardline())
90-
.append(alloc.text(name.as_ref()))
91-
.append("=")
92-
.append(
93-
(alloc.space())
94-
.append(pretty_term_prec(alloc, term, Prec::Term))
95-
.append(",")
96-
.group()
97-
.nest(4),
98-
)
99-
.nest(4)
100-
.group()
101-
})))
89+
.append(
90+
alloc.concat(term_entries.iter().map(|(entry_name, entry_term)| {
91+
(alloc.nil())
92+
.append(alloc.hardline())
93+
.append(alloc.text(entry_name.as_ref()))
94+
.append("=")
95+
.append(
96+
(alloc.space())
97+
.append(pretty_term_prec(alloc, entry_term, Prec::Term))
98+
.append(",")
99+
.group()
100+
.nest(4),
101+
)
102+
.nest(4)
103+
.group()
104+
})),
105+
)
102106
.append("}"),
103107
Term::RecordElim(_, head, name) => (alloc.nil())
104108
.append(pretty_term_prec(alloc, head, Prec::Atomic))

0 commit comments

Comments
 (0)