Skip to content

Commit b7d31e2

Browse files
KmeakinKmeakin
committed
Fix issue #421 
1 parent 5d4d535 commit b7d31e2

File tree

7 files changed

+111
-69
lines changed

7 files changed

+111
-69
lines changed

‎fathom/src/source.rs‎

Lines changed: 23 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
//! Types related to source files.
22
3-
use std::ops::{Deref, DerefMut};
3+
use std::ops::{Deref, DerefMut, Range};
44

55
// Interned strings.
66
pub type StringId = string_interner::symbol::SymbolU16;
@@ -40,10 +40,29 @@ impl StringInterner {
4040
}
4141
}
4242

43+
/// Allocate and intern all tuple labels upto `max_index` if they are not already present
44+
pub fn reserve_tuple_labels(&mut self, max_index: usize) {
45+
let len = self.tuple_labels.len();
46+
let cap = self.tuple_labels.capacity();
47+
if max_index >= len {
48+
self.tuple_labels.reserve(max_index.saturating_sub(cap));
49+
for index in len..=max_index {
50+
let label = self.get_or_intern(format!("_{}", index));
51+
self.tuple_labels.push(label);
52+
}
53+
}
54+
}
55+
4356
/// Get or intern a string in the form `_{index}`.
4457
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)))
58+
self.reserve_tuple_labels(index);
59+
self.tuple_labels[index]
60+
}
61+
62+
/// Get or intern a slice of strings in the form `_{index}` for each index in `range`.
63+
pub fn get_tuple_labels(&mut self, range: Range<usize>) -> &[StringId] {
64+
self.reserve_tuple_labels(range.end);
65+
&self.tuple_labels[range]
4766
}
4867

4968
/// Returns true if `label` refers to a string in the form `_{index}`.
@@ -53,7 +72,7 @@ impl StringInterner {
5372

5473
/// Returns true if `labels` is a sequence of tuple labels: `_0`, `_1`, ...
5574
pub fn is_tuple_labels(&mut self, labels: &[StringId]) -> bool {
56-
(labels.iter().enumerate()).all(|(index, label)| self.is_tuple_label(index, *label))
75+
labels == self.get_tuple_labels(0..labels.len())
5776
}
5877
}
5978

‎fathom/src/surface/distillation.rs‎

Lines changed: 31 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -200,6 +200,23 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
200200
Term::Ann((), self.scope.to_scope(expr), self.scope.to_scope(r#type))
201201
}
202202

203+
fn check_dependent_tuple(
204+
&mut self,
205+
labels: &[StringId],
206+
exprs: &[core::Term<'_>],
207+
) -> Term<'arena, ()> {
208+
let initial_local_len = self.local_len();
209+
let exprs = (self.scope).to_scope_from_iter(
210+
Iterator::zip(labels.iter(), exprs.iter()).map(|(label, expr)| {
211+
let expr = self.check(expr);
212+
self.push_local(Some(*label));
213+
expr
214+
}),
215+
);
216+
self.truncate_local(initial_local_len);
217+
Term::Tuple((), exprs)
218+
}
219+
203220
/// Distill a core term into a surface term, in a 'checkable' context.
204221
pub fn check(&mut self, core_term: &core::Term<'_>) -> Term<'arena, ()> {
205222
match core_term {
@@ -247,9 +264,12 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
247264
core::Term::RecordType(_, labels, types)
248265
if is_tuple_type(&mut self.interner.borrow_mut(), labels, types) =>
249266
{
250-
let scope = self.scope;
251-
let types = types.iter().map(|expr| self.check(expr));
252-
Term::Tuple((), scope.to_scope_from_iter(types))
267+
self.check_dependent_tuple(labels, types)
268+
}
269+
core::Term::FormatRecord(_, labels, formats)
270+
if is_tuple_type(&mut self.interner.borrow_mut(), labels, formats) =>
271+
{
272+
self.check_dependent_tuple(labels, formats)
253273
}
254274
core::Term::RecordLit(_, labels, exprs)
255275
if self.interner.borrow_mut().is_tuple_labels(labels) =>
@@ -274,13 +294,6 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
274294

275295
Term::ArrayLiteral((), scope.to_scope_from_iter(elem_exprs))
276296
}
277-
core::Term::FormatRecord(_, labels, formats)
278-
if is_tuple_type(&mut self.interner.borrow_mut(), labels, formats) =>
279-
{
280-
let scope = self.scope;
281-
let formats = formats.iter().map(|format| self.check(format));
282-
Term::Tuple((), scope.to_scope_from_iter(formats))
283-
}
284297
core::Term::ConstLit(_span, r#const) => match r#const {
285298
core::Const::Bool(boolean) => Term::BooleanLiteral((), *boolean),
286299
core::Const::U8(number, style) => self.check_number_literal_styled(number, *style),
@@ -520,20 +533,13 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
520533
core::Term::RecordType(_, labels, types)
521534
if is_tuple_type(&mut self.interner.borrow_mut(), labels, types) =>
522535
{
523-
let initial_local_len = self.local_len();
524-
let types = (self.scope).to_scope_from_iter(
525-
Iterator::zip(labels.iter(), types.iter()).map(|(label, r#type)| {
526-
let r#type = self.check(r#type);
527-
self.push_local(Some(*label));
528-
r#type
529-
}),
530-
);
531-
self.truncate_local(initial_local_len);
532-
Term::Ann(
533-
(),
534-
self.scope.to_scope(Term::Tuple((), types)),
535-
&Term::Universe(()),
536-
)
536+
let tuple = self.check_dependent_tuple(labels, types);
537+
Term::Ann((), self.scope.to_scope(tuple), &Term::Universe(()))
538+
}
539+
core::Term::FormatRecord(_span, labels, formats)
540+
if is_tuple_type(&mut self.interner.borrow_mut(), labels, formats) =>
541+
{
542+
self.check_dependent_tuple(labels, formats)
537543
}
538544
core::Term::RecordType(_span, labels, types) => {
539545
let initial_local_len = self.local_len();
@@ -591,13 +597,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
591597
// FIXME: Type annotations
592598
Term::ArrayLiteral((), scope.to_scope_from_iter(elem_exprs))
593599
}
594-
core::Term::FormatRecord(_span, labels, formats)
595-
if is_tuple_type(&mut self.interner.borrow_mut(), labels, formats) =>
596-
{
597-
let scope = self.scope;
598-
let formats = formats.iter().map(|format| self.synth(format));
599-
Term::Tuple((), scope.to_scope_from_iter(formats))
600-
}
600+
601601
core::Term::FormatRecord(_span, labels, formats) => {
602602
Term::FormatRecord((), self.synth_format_fields(labels, formats))
603603
}

‎fathom/src/surface/elaboration.rs‎

Lines changed: 34 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -981,25 +981,48 @@ 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())
985-
.map(|index| self.interner.borrow_mut().get_tuple_label(index));
986-
let labels = self.scope.to_scope_from_iter(labels);
984+
let mut interner = self.interner.borrow_mut();
985+
let labels = interner.get_tuple_labels(0..elem_exprs.len());
986+
let labels = self.scope.to_scope_from_iter(labels.iter().copied());
987987

988988
let initial_local_len = self.local_env.len();
989989
let universe = &self.universe.clone();
990-
let types = self
991-
.scope
992-
.to_scope_from_iter(elem_exprs.iter().map(|elem_expr| {
990+
let types = self.scope.to_scope_from_iter(
991+
Iterator::zip(labels.iter(), elem_exprs.iter()).map(|(label, elem_expr)| {
993992
let r#type = self.check(elem_expr, universe);
994993
let type_value = self.eval_env().eval(&r#type);
995-
self.local_env.push_param(None, type_value);
994+
self.local_env.push_param(Some(*label), type_value);
996995
r#type
997-
}));
996+
}),
997+
);
998998

999999
self.local_env.truncate(initial_local_len);
10001000

10011001
core::Term::RecordType(range.into(), labels, types)
10021002
}
1003+
(Term::Tuple(range, elem_exprs), Value::Stuck(Head::Prim(Prim::FormatType), args))
1004+
if args.is_empty() =>
1005+
{
1006+
let mut interner = self.interner.borrow_mut();
1007+
let labels = interner.get_tuple_labels(0..elem_exprs.len());
1008+
let labels = self.scope.to_scope_from_iter(labels.iter().copied());
1009+
1010+
let initial_local_len = self.local_env.len();
1011+
let format_type = self.format_type.clone();
1012+
let formats = self.scope.to_scope_from_iter(
1013+
Iterator::zip(labels.iter(), elem_exprs.iter()).map(|(label, elem_expr)| {
1014+
let format = self.check(elem_expr, &format_type);
1015+
let format_value = self.eval_env().eval(&format);
1016+
let r#type = self.elim_env().format_repr(&format_value);
1017+
self.local_env.push_param(Some(*label), r#type);
1018+
format
1019+
}),
1020+
);
1021+
1022+
self.local_env.truncate(initial_local_len);
1023+
1024+
core::Term::FormatRecord(range.into(), labels, formats)
1025+
}
10031026
(Term::Tuple(range, elem_exprs), Value::RecordType(labels, types)) => {
10041027
if elem_exprs.len() != labels.len() {
10051028
let mut expr_labels = Vec::with_capacity(elem_exprs.len());
@@ -1044,29 +1067,6 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
10441067

10451068
core::Term::RecordLit(range.into(), labels, exprs.into())
10461069
}
1047-
(Term::Tuple(range, elem_exprs), Value::Stuck(Head::Prim(Prim::FormatType), args))
1048-
if args.is_empty() =>
1049-
{
1050-
let initial_local_len = self.local_env.len();
1051-
let format_type = self.format_type.clone();
1052-
1053-
let labels = (0..elem_exprs.len())
1054-
.map(|index| self.interner.borrow_mut().get_tuple_label(index));
1055-
let labels = self.scope.to_scope_from_iter(labels);
1056-
1057-
let mut formats = SliceVec::new(self.scope, elem_exprs.len());
1058-
for elem_expr in elem_exprs.iter() {
1059-
let format = self.check(elem_expr, &format_type);
1060-
let format_value = self.eval_env().eval(&format);
1061-
let r#type = self.elim_env().format_repr(&format_value);
1062-
self.local_env.push_param(None, r#type);
1063-
formats.push(format);
1064-
}
1065-
1066-
self.local_env.truncate(initial_local_len);
1067-
1068-
core::Term::FormatRecord(range.into(), labels, formats.into())
1069-
}
10701070
(Term::ArrayLiteral(range, elem_exprs), _) => {
10711071
use crate::core::semantics::Elim::FunApp as App;
10721072

@@ -1423,9 +1423,9 @@ impl<'interner, 'arena> Context<'interner, 'arena> {
14231423
)
14241424
}
14251425
Term::Tuple(range, elem_exprs) => {
1426-
let labels = (0..elem_exprs.len())
1427-
.map(|index| self.interner.borrow_mut().get_tuple_label(index));
1428-
let labels = self.scope.to_scope_from_iter(labels);
1426+
let mut interner = self.interner.borrow_mut();
1427+
let labels = interner.get_tuple_labels(0..elem_exprs.len());
1428+
let labels = self.scope.to_scope_from_iter(labels.iter().copied());
14291429

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

‎tests/succeed/tuple/generic-pair.fathom‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
let fst = fun (A: Type) (B: Type) (p: {_0: A, _1: B}) => p._0;
2+
let snd = fun (A: Type) (B: Type) (p: (A, B)) => p._1;
3+
{}

‎tests/succeed/tuple/generic-pair.snap‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
stdout = '''
2+
let fst : fun (A : Type) (B : Type) -> (A, B) -> A = fun A B p => p._0;
3+
let snd : fun (A : Type) (B : Type) -> (A, B) -> B = fun A B p => p._1;
4+
() : ()
5+
'''
6+
stderr = ''

‎tests/succeed/tuple/generic-triple.fathom‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
let get1 = fun (A: Type) (B: Type) (C: Type) (p: {_0: A, _1: B, _2: C}) => p._0;
2+
let get2 = fun (A: Type) (B: Type) (C: Type) (p: (A, B, C)) => p._1;
3+
let get3 = fun (A: Type) (B: Type) (C: Type) (p: (A, B, C)) => p._2;
4+
{}

‎tests/succeed/tuple/generic-triple.snap‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
stdout = '''
2+
let get1 : fun (A : Type) (B : Type) (C : Type) -> (A, B, C) -> A =
3+
fun A B C p => p._0;
4+
let get2 : fun (A : Type) (B : Type) (C : Type) -> (A, B, C) -> B =
5+
fun A B C p => p._1;
6+
let get3 : fun (A : Type) (B : Type) (C : Type) -> (A, B, C) -> C =
7+
fun A B C p => p._2;
8+
() : ()
9+
'''
10+
stderr = ''

0 commit comments

Comments
 (0)