@@ -17,6 +17,7 @@ use crate::builtin::constructors::{C_BIND, C_MATCH};
17
17
use crate :: elaborate:: { Context , ElabError , ErrorKind } ;
18
18
use crate :: types:: { Constructor , Type } ;
19
19
use crate :: { Decl , Expr , ExprKind , Lambda , Pat , PatKind , Row , Rule , SortedRecord } ;
20
+ use sml_util:: diagnostics:: Level ;
20
21
use sml_util:: interner:: Symbol ;
21
22
use sml_util:: span:: Span ;
22
23
use sml_util:: Const ;
@@ -117,12 +118,7 @@ pub fn val<'a>(
117
118
let test = ctx. fresh_var ( ) ;
118
119
119
120
let ( ret_ty, rpat, rexpr) = match bindings. len ( ) {
120
- 0 => {
121
- return Rule {
122
- pat,
123
- expr : scrutinee,
124
- }
125
- }
121
+ 0 => ( pat. ty , pat, scrutinee) ,
126
122
1 => {
127
123
let ( sym, ty) = bindings[ 0 ] ;
128
124
let p = Pat :: new ( ctx. arena . pats . alloc ( PatKind :: Var ( sym) ) , ty, Span :: dummy ( ) ) ;
@@ -134,6 +130,8 @@ pub fn val<'a>(
134
130
( ty, p, e)
135
131
}
136
132
_ => {
133
+ // This is incredibly ugly, maybe clean it up at cost of performance?
134
+
137
135
let mut vt = Vec :: new ( ) ;
138
136
let mut vp = Vec :: new ( ) ;
139
137
let mut ve = Vec :: new ( ) ;
@@ -176,8 +174,6 @@ pub fn val<'a>(
176
174
}
177
175
} ;
178
176
179
- // let expr = crate::match_compile::case(ctx, expr, rw_ty, vec![Rule { pat, expr: rw_expr}], pat.span + expr.span);
180
-
181
177
let pats = vec ! [ vec![ pat] ] ;
182
178
let mut diags = MatchDiags :: with_capacity ( span, 1 , C_BIND ) ;
183
179
let ( mut decls, rules) = preflight ( ctx, vec ! [ Rule { pat, expr: rexpr } ] , & mut diags) ;
@@ -367,10 +363,25 @@ impl MatchDiags {
367
363
}
368
364
}
369
365
if self . inexhaustive {
370
- ctx. elab_errors . push (
371
- ElabError :: new ( self . span , "inexhaustive `case` expression" )
372
- . kind ( ErrorKind :: Redundant ) ,
373
- ) ;
366
+ match self . constr {
367
+ C_BIND => {
368
+ let level = match ctx. scope_depth ( ) {
369
+ 0 => Level :: Warn ,
370
+ _ => Level :: Error ,
371
+ } ;
372
+ ctx. elab_errors . push (
373
+ ElabError :: new ( self . span , "inexhaustive `val` binding" )
374
+ . kind ( ErrorKind :: Inexhaustive )
375
+ . level ( level) ,
376
+ ) ;
377
+ }
378
+ _ => {
379
+ ctx. elab_errors . push (
380
+ ElabError :: new ( self . span , "inexhaustive `case` expression" )
381
+ . kind ( ErrorKind :: Inexhaustive ) ,
382
+ ) ;
383
+ }
384
+ }
374
385
}
375
386
}
376
387
}
@@ -609,7 +620,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
609
620
set. sort_by ( |a, b| a. cmp ( & b) ) ;
610
621
611
622
let mut rules = Vec :: new ( ) ;
612
- for con in set {
623
+ for & con in & set {
613
624
// Clone facts so we don't polute other branches with identical bound
614
625
let mut f = facts. clone ( ) ;
615
626
let expr = self . specialize_const ( & mut f, diags, con) ;
@@ -622,9 +633,13 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
622
633
rules. push ( Rule { pat, expr } ) ;
623
634
}
624
635
625
- let pat = self . mk_wild ( self . pats [ 0 ] [ 0 ] . ty ) ;
626
- let expr = self . default_matrix ( facts, diags) ;
627
- rules. push ( Rule { pat, expr } ) ;
636
+ if set. len ( ) == 1 && set[ 0 ] == & Const :: Unit {
637
+ // Unit is exhaustive
638
+ } else {
639
+ let pat = self . mk_wild ( self . pats [ 0 ] [ 0 ] . ty ) ;
640
+ let expr = self . default_matrix ( facts, diags) ;
641
+ rules. push ( Rule { pat, expr } ) ;
642
+ }
628
643
629
644
Expr :: new (
630
645
self . ctx . arena . exprs . alloc ( ExprKind :: Case (
@@ -658,7 +673,7 @@ impl<'a, 'ctx> Matrix<'a, 'ctx> {
658
673
self . ctx
659
674
. arena
660
675
. exprs
661
- . alloc ( ExprKind :: Con ( crate :: builtin :: constructors :: C_MATCH , vec ! [ ] ) ) ,
676
+ . alloc ( ExprKind :: Con ( diags . constr , vec ! [ ] ) ) ,
662
677
self . ret_ty ,
663
678
Span :: zero ( ) ,
664
679
) ;
0 commit comments