@@ -13,6 +13,8 @@ use crate::surface::{
1313 BinOp , ExprField , FormatField , Item , ItemDef , Module , Pattern , Term , TypeField ,
1414} ;
1515
16+ use super :: { AppArg , FunParam , Plicity } ;
17+
1618/// Distillation context.
1719pub struct Context < ' interner , ' arena , ' env > {
1820 interner : & ' interner RefCell < StringInterner > ,
@@ -129,7 +131,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
129131 Item :: Def ( ItemDef {
130132 range : ( ) ,
131133 label : ( ( ) , * label) ,
132- patterns : & [ ] ,
134+ params : & [ ] ,
133135 r#type : Some ( r#type) ,
134136 expr,
135137 } )
@@ -273,13 +275,15 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
273275 let body_expr = self . check ( body_expr) ;
274276 self . truncate_local ( initial_local_len) ;
275277
276- let patterns = param_names
277- . into_iter ( )
278- . map ( |name| ( Pattern :: Name ( ( ) , name) , None ) ) ;
278+ let params = param_names. into_iter ( ) . map ( |name| FunParam {
279+ plicity : Plicity :: Explicit ,
280+ pattern : Pattern :: Name ( ( ) , name) ,
281+ r#type : None ,
282+ } ) ;
279283
280284 Term :: FunLiteral (
281285 ( ) ,
282- self . scope . to_scope_from_iter ( patterns ) ,
286+ self . scope . to_scope_from_iter ( params ) ,
283287 self . scope . to_scope ( body_expr) ,
284288 )
285289 }
@@ -416,19 +420,22 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
416420 head_expr
417421 } else {
418422 let head_expr = self . scope . to_scope ( head_expr) ;
419- let mut arg_exprs = SliceVec :: new ( self . scope , num_params) ;
423+ let mut args = SliceVec :: new ( self . scope , num_params) ;
420424
421425 for ( var, info) in Iterator :: zip ( env:: levels ( ) , local_infos. iter ( ) ) {
422426 match info {
423427 core:: LocalInfo :: Def => { }
424428 core:: LocalInfo :: Param => {
425429 let var = self . local_len ( ) . level_to_index ( var) . unwrap ( ) ;
426- arg_exprs. push ( self . check ( & core:: Term :: LocalVar ( Span :: Empty , var) ) ) ;
430+ args. push ( AppArg {
431+ plicity : Plicity :: Explicit ,
432+ term : self . check ( & core:: Term :: LocalVar ( Span :: Empty , var) ) ,
433+ } ) ;
427434 }
428435 }
429436 }
430437
431- Term :: App ( ( ) , head_expr, arg_exprs . into ( ) )
438+ Term :: App ( ( ) , head_expr, args . into ( ) )
432439 }
433440 }
434441 core:: Term :: Ann ( _span, expr, r#type) => {
@@ -459,7 +466,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
459466 core:: Term :: FunType ( ..) => {
460467 let initial_local_len = self . local_len ( ) ;
461468
462- let mut patterns = Vec :: new ( ) ;
469+ let mut params = Vec :: new ( ) ;
463470 let mut body_type = core_term;
464471
465472 let body_type = loop {
@@ -471,10 +478,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
471478 let param_type = self . check ( param_type) ;
472479 let param_name = self . freshen_name ( * param_name, next_body_type) ;
473480 let param_name = self . push_local ( param_name) ;
474- patterns. push ( (
475- Pattern :: Name ( ( ) , param_name) ,
476- Some ( self . scope . to_scope ( param_type) as & _ ) ,
477- ) ) ;
481+ params. push ( FunParam {
482+ plicity : Plicity :: Explicit ,
483+ pattern : Pattern :: Name ( ( ) , param_name) ,
484+ r#type : Some ( param_type) ,
485+ } ) ;
478486 body_type = next_body_type;
479487 }
480488 // Use arrow sugar if the parameter is not referenced in the body type.
@@ -487,6 +495,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
487495
488496 break Term :: Arrow (
489497 ( ) ,
498+ Plicity :: Explicit ,
490499 self . scope . to_scope ( param_type) ,
491500 self . scope . to_scope ( body_type) ,
492501 ) ;
@@ -497,12 +506,12 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
497506
498507 self . truncate_local ( initial_local_len) ;
499508
500- if patterns . is_empty ( ) {
509+ if params . is_empty ( ) {
501510 body_type
502511 } else {
503512 Term :: FunType (
504513 ( ) ,
505- self . scope . to_scope_from_iter ( patterns ) ,
514+ self . scope . to_scope_from_iter ( params ) ,
506515 self . scope . to_scope ( body_type) ,
507516 )
508517 }
@@ -522,40 +531,46 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> {
522531 let body_expr = self . synth ( body_expr) ;
523532 self . truncate_local ( initial_local_len) ;
524533
525- let patterns = param_names
526- . into_iter ( )
527- . map ( |name| ( Pattern :: Name ( ( ) , name) , None ) ) ;
534+ let params = param_names. into_iter ( ) . map ( |name| FunParam {
535+ plicity : Plicity :: Explicit ,
536+ pattern : Pattern :: Name ( ( ) , name) ,
537+ r#type : None ,
538+ } ) ;
528539
529540 Term :: FunLiteral (
530541 ( ) ,
531- self . scope . to_scope_from_iter ( patterns ) ,
542+ self . scope . to_scope_from_iter ( params ) ,
532543 self . scope . to_scope ( body_expr) ,
533544 )
534545 }
535- core:: Term :: FunApp ( _, mut head_expr, arg_expr) => match head_expr {
536- core:: Term :: FunApp ( _, core:: Term :: Prim ( _, prim) , lhs)
537- if prim_to_bin_op ( prim) . is_some ( ) =>
538- {
539- // unwrap is safe due to is_some check above
540- self . synth_bin_op ( lhs, arg_expr, prim_to_bin_op ( prim) . unwrap ( ) )
541- }
542- _ => {
543- let mut arg_exprs = vec ! [ self . check( arg_expr) ] ;
544-
545- while let core:: Term :: FunApp ( _, next_head_expr, arg_expr) = head_expr {
546- head_expr = next_head_expr;
547- arg_exprs. push ( self . check ( arg_expr) ) ;
548- }
546+ core:: Term :: FunApp (
547+ _,
548+ core:: Term :: FunApp ( _, core:: Term :: Prim ( _, prim) , lhs) ,
549+ arg_expr,
550+ ) if prim_to_bin_op ( prim) . is_some ( ) => {
551+ self . synth_bin_op ( lhs, arg_expr, prim_to_bin_op ( prim) . unwrap ( ) )
552+ }
549553
550- let head_expr = self . synth ( head_expr) ;
554+ core:: Term :: FunApp ( ..) => {
555+ let mut head_expr = core_term;
556+ let mut args = Vec :: new ( ) ;
551557
552- Term :: App (
553- ( ) ,
554- self . scope . to_scope ( head_expr) ,
555- self . scope . to_scope_from_iter ( arg_exprs. into_iter ( ) . rev ( ) ) ,
556- )
558+ while let core:: Term :: FunApp ( _, next_head_expr, arg_expr) = head_expr {
559+ head_expr = next_head_expr;
560+ args. push ( AppArg {
561+ plicity : Plicity :: Explicit ,
562+ term : self . check ( arg_expr) ,
563+ } ) ;
557564 }
558- } ,
565+
566+ let head_expr = self . synth ( head_expr) ;
567+
568+ Term :: App (
569+ ( ) ,
570+ self . scope . to_scope ( head_expr) ,
571+ self . scope . to_scope_from_iter ( args. into_iter ( ) . rev ( ) ) ,
572+ )
573+ }
559574 core:: Term :: RecordType ( _, labels, types)
560575 if is_tuple_type ( & mut self . interner . borrow_mut ( ) , labels, types) =>
561576 {
0 commit comments