Detect redundant and exhaustive matches

[julianhyde]

Detect redundant and exhaustive matches in case and fun; optimize case expressions by removing unreachable branches.

In the following case, the user provided a redundant match (the second true) and ML gives an error:

fun f x = case x > 0 of true => "positive" | false => "non-positive" | true => "oops";
stdIn:4.11-4.86 Error: match redundant
          true => ...
          false => ...
    -->   true => ...

In the following case, the user's matches are not exhaustive, and ML gives a warning:

fun f x = case x > 0 of true => "positive";
stdIn:1.12-1.44 Warning: match nonexhaustive
          true => ...

val f = fn : int -> string

Note that if a match is exhaustive, every subsequent branch will be redundant; however, it is possible for a non-exhaustive match to have redundant branches.

The above examples also occur in the fun syntactic sugar:

fun f true = "positive" | f false = "non-positive" | f true = "oops";
stdIn:5.5-5.69 Error: match redundant
          true => ...
          false => ...
    -->   true => ...

fun f true = "positive";
stdIn:1.6-1.25 Warning: match nonexhaustive
          true => ...

val f = fn : bool -> string

Even if the user's program never contains redundant matches, the expressions in the core language (Core.Case) may have redundant matches. Redundant expressions may be safely removed, and we should remove them during optimization.

Notes:

• There is no if in Core. If user code contains if b E1 else E2, we translate it to the Core.Case equivalent of case b of true => E1 | _ => E2;
• Wildcard patterns _ make matches exhaustive;
• Datatypes are the main targets to check for redundancy/exhaustiveness, because they have a small number of possible values. For these purposes, bool is a datatype with values false and true.

[julianhyde]

Another case from sml-nj:

fun f (true, true) = "a" | f (false, _) = "b" | f (_, true) = "c";
stdIn:1.6-1.67 Error: match redundant and nonexhaustive
          (true,true) => ...
          (false,_) => ...
    -->   (_,true) => ...

[julianhyde]

More from sml-nj:

- fun f (1, 2, x) = x
=   | f (_, 1, x) = x
=   | f (1, w, x) = x + w;
stdIn:1.6-3.24 Warning: match nonexhaustive
          (1,2,x) => ...
          (_,1,x) => ...
          (1,w,x) => ...

val f = fn : int * int * int -> int
- fun f (1, 2, x) = x
=   | f (_, 1, x) = x + 1
=   | f (1, 1, x) = x + 2;
stdIn:1.6-7.24 Error: match redundant and nonexhaustive
          (1,2,x) => ...
          (_,1,x) => ...
    -->   (1,1,x) => ...

[julianhyde]

I discovered a classic paper Compiling Pattern Matching (Lennart Augustsson, 1985). It deals nicely with algebraic data types (e.g. NIL | CONS (h, t)) but not so well with specific values (e.g. NIL | CONS (7, t) | CONS (11, t) | CONS (x, CONS (5, t))).

So for specific values I think that a Satisfiability solver is the way to go. We can convert

NIL
 | CONS (7, t)
 | CONS (11, t)
 | CONS (x, CONS (5, t))

into

tag.NIL
 or (tag.CONS and v1.7)
 or (tag.CONS and v1.11)
 or (tag.CONS and tag2.CONS and v2.1.5

where tag.CONS and v1.7 etc. are all boolean variables. tag.CONS and tag.NIL are disjoin (exactly one of them has to be true) so we'll add some extra terms for that.

We can deduce that a pattern is redundant if it doesn't affect satisfiability - i.e. there is no new combination of assignments that is matched when the pattern is added. Something similar for exhaustiveness.

[julianhyde]

Work in progress: https://github.com/julianhyde/morel/tree/0055-exhaustive-patterns