14
14
//! * `vars` contains the current "in-scope" destructured variables
15
15
16
16
use super :: * ;
17
- use elaborate:: Context ;
17
+ use elaborate:: { Context , ElabError , ErrorKind } ;
18
18
use std:: collections:: { HashMap , HashSet , VecDeque } ;
19
19
20
20
pub type Var < ' a > = ( Symbol , & ' a Type < ' a > ) ;
21
21
22
22
pub fn case < ' a > (
23
- ctx : & Context < ' a > ,
23
+ ctx : & mut Context < ' a > ,
24
24
scrutinee : Expr < ' a > ,
25
25
ret_ty : & ' a Type < ' a > ,
26
26
rules : Vec < Rule < ' a > > ,
27
27
span : Span ,
28
28
) -> Expr < ' a > {
29
29
let test = ctx. fresh_var ( ) ;
30
30
let pats = rules. iter ( ) . map ( |r| vec ! [ r. pat] ) . collect ( ) ;
31
- let ( mut decls, rules) = preflight ( ctx, rules) ;
31
+
32
+ let mut diags = MatchDiags :: with_capacity ( span, rules. len ( ) ) ;
33
+ let ( mut decls, rules) = preflight ( ctx, rules, & mut diags) ;
32
34
33
35
decls. push ( Decl :: Val ( Rule {
34
36
pat : ctx. arena . pat_var ( test, scrutinee. ty ) ,
@@ -45,7 +47,8 @@ pub fn case<'a>(
45
47
} ;
46
48
47
49
let mut facts = Facts :: default ( ) ;
48
- let expr = mat. compile ( & mut facts) ;
50
+ let expr = mat. compile ( & mut facts, & mut diags) ;
51
+ diags. emit_diagnostics ( ctx) ;
49
52
Expr :: new (
50
53
ctx. arena . exprs . alloc ( ExprKind :: Let ( decls, expr) ) ,
51
54
expr. ty ,
@@ -54,15 +57,16 @@ pub fn case<'a>(
54
57
}
55
58
56
59
pub fn fun < ' a > (
57
- ctx : & Context < ' a > ,
60
+ ctx : & mut Context < ' a > ,
58
61
ret_ty : & ' a Type < ' a > ,
59
62
vars : Vec < Var < ' a > > ,
60
63
pats : Vec < Vec < Pat < ' a > > > ,
61
64
rules : Vec < Rule < ' a > > ,
62
65
span : Span ,
63
66
) -> Expr < ' a > {
64
67
let test = ctx. fresh_var ( ) ;
65
- let ( decls, rules) = preflight ( ctx, rules) ;
68
+ let mut diags = MatchDiags :: with_capacity ( span, rules. len ( ) ) ;
69
+ let ( decls, rules) = preflight ( ctx, rules, & mut diags) ;
66
70
67
71
let rec = SortedRecord :: new_unchecked (
68
72
vars. iter ( )
@@ -88,7 +92,8 @@ pub fn fun<'a>(
88
92
vars,
89
93
} ;
90
94
91
- let expr = mat. compile ( & mut facts) ;
95
+ let expr = mat. compile ( & mut facts, & mut diags) ;
96
+ diags. emit_diagnostics ( ctx) ;
92
97
Expr :: new (
93
98
ctx. arena . exprs . alloc ( ExprKind :: Let ( decls, expr) ) ,
94
99
expr. ty ,
@@ -117,7 +122,11 @@ pub fn fun<'a>(
117
122
/// case x of
118
123
/// ...
119
124
/// ```
120
- fn preflight < ' a > ( ctx : & Context < ' a > , rules : Vec < Rule < ' a > > ) -> ( Vec < Decl < ' a > > , Vec < Rule < ' a > > ) {
125
+ fn preflight < ' a > (
126
+ ctx : & Context < ' a > ,
127
+ rules : Vec < Rule < ' a > > ,
128
+ diags : & mut MatchDiags ,
129
+ ) -> ( Vec < Decl < ' a > > , Vec < Rule < ' a > > ) {
121
130
let mut finished = Vec :: new ( ) ;
122
131
let mut decls = Vec :: new ( ) ;
123
132
for Rule { pat, expr } in rules {
@@ -158,7 +167,9 @@ fn preflight<'a>(ctx: &Context<'a>, rules: Vec<Rule<'a>>) -> (Vec<Decl<'a>>, Vec
158
167
finished. push ( Rule {
159
168
pat,
160
169
expr : ctx. arena . expr_var ( name, ty) ,
161
- } )
170
+ } ) ;
171
+
172
+ diags. renamed . push ( ( expr. span , name) ) ;
162
173
}
163
174
( decls, finished)
164
175
}
@@ -218,6 +229,42 @@ impl Facts {
218
229
}
219
230
}
220
231
232
+ pub struct MatchDiags {
233
+ span : Span ,
234
+ // mapping from match arm index to renamed/abstracted arms
235
+ renamed : Vec < ( Span , Symbol ) > ,
236
+ // Which arms were reached
237
+ reached : HashSet < Symbol > ,
238
+ // Did we emit a `raise Match`?
239
+ inexhaustive : bool ,
240
+ }
241
+
242
+ impl MatchDiags {
243
+ pub fn with_capacity ( span : Span , capacity : usize ) -> MatchDiags {
244
+ MatchDiags {
245
+ span,
246
+ renamed : Vec :: with_capacity ( capacity) ,
247
+ reached : HashSet :: with_capacity ( capacity) ,
248
+ inexhaustive : false ,
249
+ }
250
+ }
251
+
252
+ pub fn emit_diagnostics ( self , ctx : & mut Context < ' _ > ) {
253
+ for ( sp, sym) in self . renamed {
254
+ if !self . reached . contains ( & sym) {
255
+ ctx. elab_errors
256
+ . push ( ElabError :: new ( sp, "unreachable match arm" ) . kind ( ErrorKind :: Redundant ) ) ;
257
+ }
258
+ }
259
+ if self . inexhaustive {
260
+ ctx. elab_errors . push (
261
+ ElabError :: new ( self . span , "inexhaustive `case` expression" )
262
+ . kind ( ErrorKind :: Redundant ) ,
263
+ ) ;
264
+ }
265
+ }
266
+ }
267
+
221
268
pub struct Matrix < ' a , ' ctx > {
222
269
// ref to the context so we can allocate stuff in arenas
223
270
ctx : & ' ctx Context < ' a > ,
@@ -264,7 +311,12 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
264
311
/// Deconstruct a record or tuple pattern, binding each field to a fresh
265
312
/// variable, and flattening all of the record patterns in the first column
266
313
/// [{a, b, c}, ...] --> [a, b, c, ...]
267
- fn record_rule ( & self , facts : & mut Facts , fields : & SortedRecord < Pat < ' a > > ) -> Expr < ' a > {
314
+ fn record_rule (
315
+ & self ,
316
+ facts : & mut Facts ,
317
+ diags : & mut MatchDiags ,
318
+ fields : & SortedRecord < Pat < ' a > > ,
319
+ ) -> Expr < ' a > {
268
320
// This part is a little tricky. We need to generate a fresh variable
269
321
// for every field in the pattern
270
322
let mut vars = self . vars . clone ( ) ;
@@ -310,7 +362,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
310
362
mat. vars = vars;
311
363
self . ctx
312
364
. arena
313
- . let_derecord ( record, base. 0 , mat. compile ( facts) )
365
+ . let_derecord ( record, base. 0 , mat. compile ( facts, diags ) )
314
366
}
315
367
316
368
/// This is basically the same thing as the record rule, but for data
@@ -320,6 +372,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
320
372
fn specialize (
321
373
& self ,
322
374
facts : & mut Facts ,
375
+ diags : & mut MatchDiags ,
323
376
head : & Constructor ,
324
377
arity : Option < Var < ' a > > ,
325
378
) -> Expr < ' a > {
@@ -352,11 +405,11 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
352
405
}
353
406
}
354
407
// mat.test = mat.vars[0].0;
355
- mat. compile ( facts)
408
+ mat. compile ( facts, diags )
356
409
}
357
410
358
411
/// Generate a case expression for the data constructors in the first column
359
- fn sum_rule ( & self , facts : & mut Facts ) -> Expr < ' a > {
412
+ fn sum_rule ( & self , facts : & mut Facts , diags : & mut MatchDiags ) -> Expr < ' a > {
360
413
// Generate the set of constructors appearing in the column
361
414
let mut set = HashMap :: new ( ) ;
362
415
let mut type_arity = 0 ;
@@ -374,7 +427,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
374
427
for ( con, arg_ty) in set {
375
428
let fresh = self . ctx . fresh_var ( ) ;
376
429
let mut f = facts. clone ( ) ;
377
- let expr = self . specialize ( & mut f, con, arg_ty. map ( |ty| ( fresh, ty) ) ) ;
430
+ let expr = self . specialize ( & mut f, diags , con, arg_ty. map ( |ty| ( fresh, ty) ) ) ;
378
431
379
432
let arg = match arg_ty {
380
433
Some ( ty) => Some ( self . ctx . arena . pat_var ( fresh, ty) ) ,
@@ -391,7 +444,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
391
444
// If we don't have an exhaustive match, generate a default matrix
392
445
if !exhaustive {
393
446
let pat = self . mk_wild ( self . pats [ 0 ] [ 0 ] . ty ) ;
394
- let expr = self . default_matrix ( facts) ;
447
+ let expr = self . default_matrix ( facts, diags ) ;
395
448
rules. push ( Rule { pat, expr } ) ;
396
449
}
397
450
@@ -409,7 +462,12 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
409
462
/// constructors. We want to select all of the rows in the first column
410
463
/// that will match the constructor `head` (e.g. `head` itself, and
411
464
/// wildcard)
412
- fn specialize_const ( & self , facts : & mut Facts , head : & Const ) -> Expr < ' a > {
465
+ fn specialize_const (
466
+ & self ,
467
+ facts : & mut Facts ,
468
+ diags : & mut MatchDiags ,
469
+ head : & Const ,
470
+ ) -> Expr < ' a > {
413
471
let mut mat = self . shallow ( ) ;
414
472
for ( idx, row) in self . pats . iter ( ) . enumerate ( ) {
415
473
match & row[ 0 ] . pat {
@@ -422,11 +480,11 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
422
480
mat. pats . push ( new_row) ;
423
481
}
424
482
mat. vars . remove ( 0 ) ;
425
- mat. compile ( facts)
483
+ mat. compile ( facts, diags )
426
484
}
427
485
428
486
/// Generate a case expression for the data constructors in the first column
429
- fn const_rule ( & self , facts : & mut Facts ) -> Expr < ' a > {
487
+ fn const_rule ( & self , facts : & mut Facts , diags : & mut MatchDiags ) -> Expr < ' a > {
430
488
// Generate the set of constructors appearing in the column
431
489
let mut set = HashSet :: new ( ) ;
432
490
for row in & self . pats {
@@ -444,7 +502,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
444
502
for con in set {
445
503
// Clone facts so we don't polute other branches with identical bound
446
504
let mut f = facts. clone ( ) ;
447
- let expr = self . specialize_const ( & mut f, con) ;
505
+ let expr = self . specialize_const ( & mut f, diags , con) ;
448
506
449
507
let pat = Pat :: new (
450
508
self . ctx . arena . pats . alloc ( PatKind :: Const ( * con) ) ,
@@ -455,7 +513,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
455
513
}
456
514
457
515
let pat = self . mk_wild ( self . pats [ 0 ] [ 0 ] . ty ) ;
458
- let expr = self . default_matrix ( facts) ;
516
+ let expr = self . default_matrix ( facts, diags ) ;
459
517
rules. push ( Rule { pat, expr } ) ;
460
518
461
519
Expr :: new (
@@ -469,7 +527,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
469
527
}
470
528
471
529
/// Compute the "default" matrix
472
- fn default_matrix ( & self , facts : & mut Facts ) -> Expr < ' a > {
530
+ fn default_matrix ( & self , facts : & mut Facts , diags : & mut MatchDiags ) -> Expr < ' a > {
473
531
let mut mat = self . shallow ( ) ;
474
532
mat. vars . remove ( 0 ) ;
475
533
@@ -480,11 +538,11 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
480
538
}
481
539
}
482
540
// mat.test = mat.vars[0].0;
483
- mat. compile ( facts)
541
+ mat. compile ( facts, diags )
484
542
}
485
543
486
544
/// Compile a [`Matrix`] into a source-level expression
487
- fn compile ( & mut self , facts : & mut Facts ) -> Expr < ' a > {
545
+ fn compile ( & mut self , facts : & mut Facts , diags : & mut MatchDiags ) -> Expr < ' a > {
488
546
if self . pats . is_empty ( ) {
489
547
// We have an in-exhaustive case expression
490
548
// TODO: Emit better diagnostics
@@ -499,6 +557,8 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
499
557
Span :: zero ( ) ,
500
558
) ;
501
559
560
+ diags. inexhaustive = true ;
561
+
502
562
Expr :: new (
503
563
self . ctx . arena . exprs . alloc ( ExprKind :: Raise ( matchh) ) ,
504
564
self . ret_ty ,
@@ -530,6 +590,8 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
530
590
} ) ) ,
531
591
} ;
532
592
593
+ diags. reached . insert ( self . rules [ 0 ] . expr . as_symbol ( ) ) ;
594
+
533
595
// TODO: Check types just in case
534
596
Expr :: new (
535
597
self . ctx
@@ -543,9 +605,9 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
543
605
// There is at least one non-wild pattern in the matrix somewhere
544
606
for row in & self . pats {
545
607
match & row[ 0 ] . pat {
546
- PatKind :: Record ( fields) => return self . record_rule ( facts, fields) ,
547
- PatKind :: App ( _, _) => return self . sum_rule ( facts) ,
548
- PatKind :: Const ( _) => return self . const_rule ( facts) ,
608
+ PatKind :: Record ( fields) => return self . record_rule ( facts, diags , fields) ,
609
+ PatKind :: App ( _, _) => return self . sum_rule ( facts, diags ) ,
610
+ PatKind :: Const ( _) => return self . const_rule ( facts, diags ) ,
549
611
PatKind :: Wild | PatKind :: Var ( _) => continue ,
550
612
}
551
613
}
@@ -571,9 +633,9 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
571
633
}
572
634
// Swap variables as well
573
635
self . vars . swap ( 0 , col) ;
574
- self . compile ( facts)
636
+ self . compile ( facts, diags )
575
637
} else {
576
- self . default_matrix ( facts)
638
+ self . default_matrix ( facts, diags )
577
639
}
578
640
}
579
641
}
0 commit comments