@@ -4,14 +4,14 @@ use scoped_arena::Scope;
44use std:: cell:: RefCell ;
55
66use crate :: alloc:: SliceVec ;
7+ use crate :: core;
78use crate :: core:: { Const , UIntStyle } ;
89use crate :: env:: { self , EnvLen , Index , Level , UniqueEnv } ;
9- use crate :: source:: Span ;
10+ use crate :: source:: { Span , StringId , StringInterner } ;
1011use crate :: surface:: elaboration:: MetaSource ;
1112use crate :: surface:: {
1213 BinOp , ExprField , FormatField , Item , ItemDef , Module , Pattern , Term , TypeField ,
1314} ;
14- use crate :: { core, StringId , StringInterner } ;
1515
1616/// Distillation context.
1717pub struct Context < ' interner , ' arena , ' env > {
@@ -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) ) ;
@@ -517,12 +517,12 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
517517 )
518518 }
519519 } ,
520- core:: Term :: RecordType ( _span , labels, exprs )
521- if is_tuple_type ( labels , exprs , & self . interner . borrow ( ) ) =>
520+ core:: Term :: RecordType ( _ , labels, types )
521+ if is_tuple_type ( & mut self . interner . borrow_mut ( ) , labels , types ) =>
522522 {
523523 let initial_local_len = self . local_len ( ) ;
524524 let types = ( self . scope ) . to_scope_from_iter (
525- Iterator :: zip ( labels. iter ( ) , exprs . iter ( ) ) . map ( |( label, r#type) | {
525+ Iterator :: zip ( labels. iter ( ) , types . iter ( ) ) . map ( |( label, r#type) | {
526526 let r#type = self . check ( r#type) ;
527527 self . push_local ( Some ( * label) ) ;
528528 r#type
@@ -551,8 +551,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
551551
552552 Term :: RecordType ( ( ) , type_fields)
553553 }
554- core:: Term :: RecordLit ( _span , labels, exprs)
555- if is_tuple_expr ( labels , & self . interner . borrow ( ) ) =>
554+ core:: Term :: RecordLit ( _ , labels, exprs)
555+ if self . interner . borrow_mut ( ) . is_tuple_labels ( labels ) =>
556556 {
557557 let scope = self . scope ;
558558 let exprs = exprs. iter ( ) . map ( |expr| self . synth ( expr) ) ;
@@ -592,7 +592,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
592592 Term :: ArrayLiteral ( ( ) , scope. to_scope_from_iter ( elem_exprs) )
593593 }
594594 core:: Term :: FormatRecord ( _span, labels, formats)
595- if is_tuple_type ( labels , formats , & self . interner . borrow ( ) ) =>
595+ if is_tuple_type ( & mut self . interner . borrow_mut ( ) , labels , formats ) =>
596596 {
597597 let scope = self . scope ;
598598 let formats = formats. iter ( ) . map ( |format| self . synth ( format) ) ;
@@ -782,27 +782,19 @@ fn match_if_then_else<'arena>(
782782 }
783783}
784784
785- // Return true if `labels` are all tuple labels
786- fn is_tuple_expr ( labels : & [ StringId ] , interner : & StringInterner ) -> bool {
787- labels
788- . iter ( )
789- . enumerate ( )
790- . all ( |( idx, label) | interner. resolve ( * label) == Some ( & format ! ( "_{}" , idx) ) )
791- }
792-
793- // Return true if `labels` are all tuple labels, and `exprs` do not depend on any of the expressions bound by `labels`
794- fn is_tuple_type ( labels : & [ StringId ] , exprs : & [ core:: Term < ' _ > ] , interner : & StringInterner ) -> bool {
795- let suffixes = ( 1 ..=exprs. len ( ) ) . rev ( ) . map ( move |idx| & exprs[ idx..] ) ;
796- labels
797- . iter ( )
798- . zip ( suffixes)
799- . enumerate ( )
800- . all ( |( idx, ( label, suffix) ) | {
801- interner. resolve ( * label) == Some ( & format ! ( "_{}" , idx) )
802- && suffix
803- . iter ( )
804- . zip ( env:: indices ( ) )
805- . all ( |( expr, idx) | !expr. binds_local ( idx) )
785+ /// Returns true if `labels` is a sequence of tuple labels (`_0`, `_1`, ...),
786+ /// and a telescope of `types` contains independent entries.
787+ fn is_tuple_type (
788+ interner : & mut StringInterner ,
789+ labels : & [ StringId ] ,
790+ types : & [ core:: Term < ' _ > ] ,
791+ ) -> bool {
792+ interner. is_tuple_labels ( labels)
793+ // For each type in the telescope, ensure that the subsequent types in
794+ // the telescope do not depend on the current field.
795+ && ( 1 ..=types. len ( ) ) . all ( |index| {
796+ Iterator :: zip ( types[ index..] . iter ( ) , env:: indices ( ) )
797+ . all ( |( expr, var) | !expr. binds_local ( var) )
806798 } )
807799}
808800
0 commit comments