[Deprecated] exhaustivity & redundancy check for pattern matching #1261

liufengyun · 2016-05-18T16:10:21Z

This is a work in process, it basically works. The test examples are currently put under tests/patmat/.

Following things need to be done:

A summary is below.

smarter · 2016-05-18T16:11:48Z

Not super important, but if possible it's nice to put the tests in the same commit than the changes that make the tests pass.

smarter · 2016-05-18T16:31:42Z

src/dotty/tools/dotc/transform/Space.scala

+
+// scala implementation of space logic
+class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
+  def debug(s: String): Unit = {


There's ctx.debuglog

But you might want to add a Printer to https://github.com/lampepfl/dotty/blob/master/src/dotty/tools/dotc/config/Printers.scala and use that instead, this way you can take advantage of ctx.traceIndented too.

I'll eventually remove the debug code when everything works. I tried ctx.debuglog, but it seems I can't make it print in the console even if I used the flag -Ydebug -Ylog:patternmatcher.

smarter · 2016-05-18T16:43:59Z

For consistency, we tend to denotes type arguments with tp: Type, not t: Type

smarter · 2016-05-18T16:47:33Z

src/dotty/tools/dotc/transform/Space.scala

+  }
+
+  // widen a type and eliminate anonymous class
+  private def widen(t: Type): Type = t.widen match {


Looks like this method is adapted from PatternMatcher#elimAnonymousClass, instead of copying code it would be better to share it between this and the PatternMatcher, you could for example put elimAnonymousClass in object PatternMatcher

liufengyun · 2016-05-18T19:06:12Z

@smarter thanks a lot for many good points, I'll address them in following commits.

smarter · 2016-05-18T20:37:22Z

src/dotty/tools/dotc/transform/Space.scala

+}
+
+// scala implementation of space logic
+class SpaceEngine(implicit ctx: Context) extends SpaceLogic {


do import tpd._ here so that you can use Tree instead of tpd.Tree below, a lot of phases do this.

smarter · 2016-05-18T20:42:00Z

In https://gist.github.com/liufengyun/66bf0c1bc44cdad12e45dd6db689e9b3 you said:

The space covered by a pattern p is defined as follows:
...
if p is pat guard, space(pat)

I think this is not what we want, unless the guard evaluates to true in all cases, the space covered should just be Empty, you should always have a case without a guard if you want the pattern match to be considered exhaustive. This is not the current scalac behavior but it is the one that it will soon have: scala/scala#4929

smarter · 2016-05-18T20:55:53Z

src/dotty/tools/dotc/transform/Space.scala

+
+
+// space definition
+sealed trait Space


This is pretty cool: you're using the exhaustiveness algorithm to test its own exhaustivity! 💥

liufengyun · 2016-05-18T21:16:24Z

@smarter Guards can be very tricky, generally we can do nothing with them.

However, some ad-hoc heuristics is possible, e.g. the case you mentioned in scalac. But the ad-hoc strategy is very limited and may cause problems:

def foo(l: List[int]): Boolean = l match {
  case x if x.length > 0 => true
  case None => false
}

smarter · 2016-05-18T21:19:29Z

@liufengyun : Yes, you can do tricky things with them, but our response should be: don't do that :)
Your code can easily be rewritten as:

def foo(l: List[int]): Boolean = l match {
  case Nil => false
  case _ => true
}

People should either rewrite their code or add @unchecked

smarter · 2016-05-18T21:31:36Z

I left some comments on https://gist.github.com/liufengyun/66bf0c1bc44cdad12e45dd6db689e9b3

smarter · 2016-05-18T21:39:45Z

src/dotty/tools/dotc/transform/Space.scala

-  def isSubType(t1: Type, t2: Type): Boolean
-  def isEqualType(t1: Type, t2: Type): Boolean
-  def isCaseClass(t: Type): Boolean
+  /** is `tp1` a subtype of `tp2` */


Sorry for being pedantic, but please start comments with a capital letter :). And put ? at the end if it's a question.

That's fine, I'm very grateful to your detailed feedback, thanks a lot :)

liufengyun · 2016-05-18T21:56:46Z

@smarter I just responded to your comments on the algorithm.

smarter · 2016-05-18T21:57:22Z

src/dotty/tools/dotc/transform/Space.scala

+        Kon(pat.tpe, pats.map(project _))
+      else if (roundUp) Typ(pat.tpe)
+      else Empty
+    case Typed(pat@UnApply(_, _, _), _) => project(pat)


The style we use is to put spaces around @: pat @ UnApply(_, _, _)

smarter · 2016-05-18T22:33:18Z

src/dotty/tools/dotc/transform/Space.scala

-  // if roundUp, approximate extractors to its type
-  // else approximate extractors to Empty
-  def project(pat: tpd.Tree)(implicit ctx: Context, roundUp: Boolean = true): Space = pat match {
+  /** If roundUp, approximate extractors to its type, else approximate extractors to Empty */


If roundUpis true, approximate an extractor to its type, otherwise approximate it toEmpty``

Also the first line of this comment should explain what this method does, I guess it's something like Return the space that represents the pattern pat``

DarkDimius · 2016-07-01T13:54:24Z

src/dotty/tools/dotc/transform/patmat/Space.scala

+      if (ktor.isInstanceOf[MethodType]) ktor
+      else
+      tp match {
+        case AppliedType(_, params) =>


ping @odersky, this kind-of reimplements asSeenFrom for constructor. I guess there should be a better way to do it but @liufengyun says it does not work.

scala.Nil refines scala.collection.immutable.Nil, this commit follows redefinition of case objects.

milessabin · 2016-07-06T09:32:24Z

It would be good to know where the various open Scala GADT bugs stand wrt this, in particular SI-5195.

liufengyun · 2016-07-06T11:29:21Z

@milessabin SI-5195 is about GADT type checking & inference in patmat, which is not covered by this PR. Exhaustivity & redundancy check happens after typer and only generate warnings.

milessabin · 2016-07-06T11:36:49Z

I obviously read too much into "add GADT test".

DarkDimius · 2016-07-15T11:24:11Z

closing in favor of #1364

smarter reviewed May 18, 2016
View reviewed changes

liufengyun force-pushed the exhaustivity branch from 8b33eb3 to f497865 Compare May 18, 2016 22:30

smarter reviewed May 18, 2016
View reviewed changes

DarkDimius reviewed Jul 1, 2016
View reviewed changes

liufengyun force-pushed the exhaustivity branch 4 times, most recently from 2dc873a to d11b14f Compare July 5, 2016 14:14

liufengyun added 11 commits July 5, 2016 16:23

initial works

5cdd42f

support check java enum from classfile and source file

9a0952c

fix false warning about Nil

fd1b286

scala.Nil refines scala.collection.immutable.Nil, this commit follows redefinition of case objects.

suppress checking of for, try and partial functions

d681a78

add GADT test

da9511d

refine patmat check for type erasure

89e8ff9

add tuple test to patmat check

b25e952

add test t5440 for patmat check

e2db834

better warning for higher-kinded types and alias types

2d6e803

fix SI-9657 about type bounds

f69b305

address counter-example of two unrelated traits

c79181d

liufengyun force-pushed the exhaustivity branch from d11b14f to c79181d Compare July 5, 2016 14:47

liufengyun changed the title ~~[WIP] exhaustivity & redundancy check for pattern matching~~ [Deprecated] exhaustivity & redundancy check for pattern matching Jul 6, 2016

DarkDimius closed this Jul 15, 2016

DarkDimius removed the In progress label Jul 15, 2016

[Deprecated] exhaustivity & redundancy check for pattern matching #1261

[Deprecated] exhaustivity & redundancy check for pattern matching #1261

Uh oh!

Conversation

liufengyun commented May 18, 2016 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smarter commented May 18, 2016

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smarter commented May 18, 2016

Uh oh!

Choose a reason for hiding this comment

Uh oh!

liufengyun commented May 18, 2016

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smarter commented May 18, 2016

Uh oh!

Choose a reason for hiding this comment

Uh oh!

liufengyun commented May 18, 2016 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smarter commented May 18, 2016

Uh oh!

smarter commented May 18, 2016

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

liufengyun commented May 18, 2016

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

milessabin commented Jul 6, 2016

Uh oh!

liufengyun commented Jul 6, 2016

Uh oh!

milessabin commented Jul 6, 2016 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

DarkDimius commented Jul 15, 2016

Uh oh!

Uh oh!

liufengyun commented May 18, 2016 •

edited

Loading

liufengyun commented May 18, 2016 •

edited

Loading

milessabin commented Jul 6, 2016 •

edited

Loading