Skip to content

Commit f9e0d65

Browse files
brendanzabbrendanzab
committed
Clean up tuple label elaboration and distillation
1 parent e7dc7c7 commit f9e0d65

File tree

3 files changed

+86
-59
lines changed

3 files changed

+86
-59
lines changed

‎fathom/src/source.rs‎

Lines changed: 50 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,56 @@ use std::ops::{Deref, DerefMut};
66
pub type StringId = string_interner::symbol::SymbolU16;
77

88
/// String interner.
9-
pub type StringInterner = string_interner::StringInterner<
10-
string_interner::backend::BucketBackend<StringId>,
11-
std::hash::BuildHasherDefault<fxhash::FxHasher32>,
12-
>;
9+
pub struct StringInterner {
10+
tuple_labels: Vec<StringId>,
11+
strings: string_interner::StringInterner<
12+
string_interner::backend::BucketBackend<StringId>,
13+
std::hash::BuildHasherDefault<fxhash::FxHasher32>,
14+
>,
15+
}
16+
17+
impl Deref for StringInterner {
18+
type Target = string_interner::StringInterner<
19+
string_interner::backend::BucketBackend<StringId>,
20+
std::hash::BuildHasherDefault<fxhash::FxHasher32>,
21+
>;
22+
23+
fn deref(&self) -> &Self::Target {
24+
&self.strings
25+
}
26+
}
27+
28+
impl DerefMut for StringInterner {
29+
fn deref_mut(&mut self) -> &mut Self::Target {
30+
&mut self.strings
31+
}
32+
}
33+
34+
impl StringInterner {
35+
/// Construct an empty string interner.
36+
pub fn new() -> StringInterner {
37+
StringInterner {
38+
tuple_labels: Vec::new(),
39+
strings: string_interner::StringInterner::new(),
40+
}
41+
}
42+
43+
/// Get or intern a string in the form `_{index}`.
44+
pub fn get_tuple_label(&mut self, index: usize) -> StringId {
45+
(self.tuple_labels.get(index).copied())
46+
.unwrap_or_else(|| self.get_or_intern(format!("_{}", index)))
47+
}
48+
49+
/// Returns true if `label` refers to a string in the form `_{index}`.
50+
pub fn is_tuple_label(&mut self, index: usize, label: StringId) -> bool {
51+
label == self.get_tuple_label(index)
52+
}
53+
54+
/// Returns true if `labels` is a sequence of tuple labels: `_0`, `_1`, ...
55+
pub fn is_tuple_labels(&mut self, labels: &[StringId]) -> bool {
56+
(labels.iter().enumerate()).all(|(index, label)| self.is_tuple_label(index, *label))
57+
}
58+
}
1359

1460
/// File id.
1561
pub type FileId = usize; // TODO: use wrapper struct

‎fathom/src/surface/distillation.rs‎

Lines changed: 28 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -244,21 +244,21 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
244244
self.scope.to_scope(body_expr),
245245
)
246246
}
247-
core::Term::RecordType(_span, labels, exprs)
248-
if is_tuple_type(labels, exprs, &self.interner.borrow()) =>
247+
core::Term::RecordType(_, labels, types)
248+
if is_tuple_type(&mut self.interner.borrow_mut(), labels, types) =>
249249
{
250250
let scope = self.scope;
251-
let exprs = exprs.iter().map(|expr| self.check(expr));
252-
Term::Tuple((), scope.to_scope_from_iter(exprs))
251+
let types = types.iter().map(|expr| self.check(expr));
252+
Term::Tuple((), scope.to_scope_from_iter(types))
253253
}
254-
core::Term::RecordLit(_span, labels, exprs)
255-
if is_tuple_expr(labels, &self.interner.borrow()) =>
254+
core::Term::RecordLit(_, labels, exprs)
255+
if self.interner.borrow_mut().is_tuple_labels(labels) =>
256256
{
257257
let scope = self.scope;
258258
let exprs = exprs.iter().map(|expr| self.check(expr));
259259
Term::Tuple((), scope.to_scope_from_iter(exprs))
260260
}
261-
core::Term::RecordLit(_span, labels, exprs) => {
261+
core::Term::RecordLit(_, labels, exprs) => {
262262
let scope = self.scope;
263263
let expr_fields =
264264
Iterator::zip(labels.iter(), exprs.iter()).map(|(label, expr)| ExprField {
@@ -274,8 +274,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
274274

275275
Term::ArrayLiteral((), scope.to_scope_from_iter(elem_exprs))
276276
}
277-
core::Term::FormatRecord(_span, labels, formats)
278-
if is_tuple_type(labels, formats, &self.interner.borrow()) =>
277+
core::Term::FormatRecord(_, labels, formats)
278+
if is_tuple_type(&mut self.interner.borrow_mut(), labels, formats) =>
279279
{
280280
let scope = self.scope;
281281
let formats = formats.iter().map(|format| self.check(format));
@@ -516,12 +516,12 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
516516
)
517517
}
518518
},
519-
core::Term::RecordType(_span, labels, exprs)
520-
if is_tuple_type(labels, exprs, &self.interner.borrow()) =>
519+
core::Term::RecordType(_, labels, types)
520+
if is_tuple_type(&mut self.interner.borrow_mut(), labels, types) =>
521521
{
522522
let initial_local_len = self.local_len();
523523
let types = (self.scope).to_scope_from_iter(
524-
Iterator::zip(labels.iter(), exprs.iter()).map(|(label, r#type)| {
524+
Iterator::zip(labels.iter(), types.iter()).map(|(label, r#type)| {
525525
let r#type = self.check(r#type);
526526
self.push_local(Some(*label));
527527
r#type
@@ -550,8 +550,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
550550

551551
Term::RecordType((), type_fields)
552552
}
553-
core::Term::RecordLit(_span, labels, exprs)
554-
if is_tuple_expr(labels, &self.interner.borrow()) =>
553+
core::Term::RecordLit(_, labels, exprs)
554+
if self.interner.borrow_mut().is_tuple_labels(labels) =>
555555
{
556556
let scope = self.scope;
557557
let exprs = exprs.iter().map(|expr| self.synth(expr));
@@ -591,7 +591,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
591591
Term::ArrayLiteral((), scope.to_scope_from_iter(elem_exprs))
592592
}
593593
core::Term::FormatRecord(_span, labels, formats)
594-
if is_tuple_type(labels, formats, &self.interner.borrow()) =>
594+
if is_tuple_type(&mut self.interner.borrow_mut(), labels, formats) =>
595595
{
596596
let scope = self.scope;
597597
let formats = formats.iter().map(|format| self.synth(format));
@@ -781,27 +781,19 @@ fn match_if_then_else<'arena>(
781781
}
782782
}
783783

784-
// Return true if `labels` are all tuple labels
785-
fn is_tuple_expr(labels: &[StringId], interner: &StringInterner) -> bool {
786-
labels
787-
.iter()
788-
.enumerate()
789-
.all(|(idx, label)| interner.resolve(*label) == Some(&format!("_{}", idx)))
790-
}
791-
792-
// Return true if `labels` are all tuple labels, and `exprs` do not depend on any of the expressions bound by `labels`
793-
fn is_tuple_type(labels: &[StringId], exprs: &[core::Term<'_>], interner: &StringInterner) -> bool {
794-
let suffixes = (1..=exprs.len()).rev().map(move |idx| &exprs[idx..]);
795-
labels
796-
.iter()
797-
.zip(suffixes)
798-
.enumerate()
799-
.all(|(idx, (label, suffix))| {
800-
interner.resolve(*label) == Some(&format!("_{}", idx))
801-
&& suffix
802-
.iter()
803-
.zip(env::indices())
804-
.all(|(expr, idx)| !expr.binds_local(idx))
784+
/// Returns true if `labels` is a sequence of tuple labels (`_0`, `_1`, ...),
785+
/// and a telescope of `types` contains independent entries.
786+
fn is_tuple_type(
787+
interner: &mut StringInterner,
788+
labels: &[StringId],
789+
types: &[core::Term<'_>],
790+
) -> bool {
791+
interner.is_tuple_labels(labels)
792+
// For each type in the telescope, ensure that the subsequent types in
793+
// the telescope do not depend on the current field.
794+
&& (1..=types.len()).all(|index| {
795+
Iterator::zip(types[index..].iter(), env::indices())
796+
.all(|(expr, var)| !expr.binds_local(var))
805797
})
806798
}
807799

‎fathom/src/surface/elaboration.rs‎

Lines changed: 8 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -981,11 +981,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
981981
core::Term::RecordLit(range.into(), labels, exprs.into())
982982
}
983983
(Term::Tuple(range, elem_exprs), Value::Universe) => {
984-
let labels = (0..elem_exprs.len()).map(|idx| {
985-
self.interner
986-
.borrow_mut()
987-
.get_or_intern(format!("_{}", idx))
988-
});
984+
let labels = (0..elem_exprs.len())
985+
.map(|index| self.interner.borrow_mut().get_tuple_label(index));
989986
let labels = self.scope.to_scope_from_iter(labels);
990987

991988
let initial_local_len = self.local_env.len();
@@ -1018,12 +1015,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
10181015
}
10191016

10201017
// use numeric labels for excess elems
1021-
for (idx, elem_expr) in elem_exprs {
1018+
for (index, elem_expr) in elem_exprs {
10221019
expr_labels.push((
10231020
elem_expr.range(),
1024-
self.interner
1025-
.borrow_mut()
1026-
.get_or_intern(format!("_{}", idx)),
1021+
self.interner.borrow_mut().get_tuple_label(index),
10271022
));
10281023
}
10291024

@@ -1055,11 +1050,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
10551050
let initial_local_len = self.local_env.len();
10561051
let format_type = self.format_type.clone();
10571052

1058-
let labels = (0..elem_exprs.len()).map(|idx| {
1059-
self.interner
1060-
.borrow_mut()
1061-
.get_or_intern(format!("_{}", idx))
1062-
});
1053+
let labels = (0..elem_exprs.len())
1054+
.map(|index| self.interner.borrow_mut().get_tuple_label(index));
10631055
let labels = self.scope.to_scope_from_iter(labels);
10641056

10651057
let mut formats = SliceVec::new(self.scope, elem_exprs.len());
@@ -1431,11 +1423,8 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14311423
)
14321424
}
14331425
Term::Tuple(range, elem_exprs) => {
1434-
let labels = (0..elem_exprs.len()).map(|idx| {
1435-
self.interner
1436-
.borrow_mut()
1437-
.get_or_intern(format!("_{}", idx))
1438-
});
1426+
let labels = (0..elem_exprs.len())
1427+
.map(|index| self.interner.borrow_mut().get_tuple_label(index));
14391428
let labels = self.scope.to_scope_from_iter(labels);
14401429

14411430
let mut exprs = SliceVec::new(self.scope, labels.len());

0 commit comments

Comments
 (0)