From 41e33530c06aa0ab97ebb3bda455ad7f9da21b22 Mon Sep 17 00:00:00 2001
From: Georg Schmid <georg.schmid@epfl.ch>
Date: Wed, 24 Jan 2018 12:14:47 +0100
Subject: [PATCH] Added tests for AppliedTermRefs.

---
 tests/neg/appliedTerm.scala | 25 +++++++++++
 tests/pos/appliedTerm.scala | 88 +++++++++++++++++++++++++++++++++++++
 2 files changed, 113 insertions(+)
 create mode 100644 tests/neg/appliedTerm.scala
 create mode 100644 tests/pos/appliedTerm.scala

diff --git a/tests/neg/appliedTerm.scala b/tests/neg/appliedTerm.scala
new file mode 100644
index 000000000000..e4fe9900d628
--- /dev/null
+++ b/tests/neg/appliedTerm.scala
@@ -0,0 +1,25 @@
+object SimpleEqs {
+  val x = 1
+  val y: {x} = x
+  implicitly[{x + 1} =:= {y}]  // error
+  implicitly[{x + 1} =:= {y + 2}]  // error
+  implicitly[{x + 1} =:= {1 + y}]  // error: TypeComparer doesn't know about commutativity
+
+  val b = true
+  implicitly[{b} =:= {b}]
+  implicitly[{!b} =:= {!b}]
+  implicitly[{!b} =:= {b}]  // error
+}
+
+
+object Stability {
+  def f1(x: Int): Int = x
+  def f2(x: Int): {x} = x
+
+  val x = 1
+  implicitly[{f1(x)} =:= {x}]  // error: f1 is not considered stable  // error: f1's result type is not precise enough
+  implicitly[{f1(x)} =:= {f1(x)}]  // error: f1 is not considered stable  // error: f1 is not considered stable
+  implicitly[{f2(x)} =:= {x}]
+  implicitly[{f2(x)} =:= {f2(x)}]
+  implicitly[{f1(x)} =:= {f2(x)}]  // error: f1 is not considered stable  // error: f1's result type is not precise enough
+}
\ No newline at end of file
diff --git a/tests/pos/appliedTerm.scala b/tests/pos/appliedTerm.scala
new file mode 100644
index 000000000000..da876db93915
--- /dev/null
+++ b/tests/pos/appliedTerm.scala
@@ -0,0 +1,88 @@
+object SimpleEqs {
+  val x = 1
+  val y: {x} = x
+  implicitly[{x + 1} =:= {y + 1}]
+}
+
+
+object AvoidLocalRefs {
+  type Id[T] = T
+
+  val x = 1
+  def y = { val a: {x} = x; val t: Id[{a + 1}] = a + 1; t }
+  def z: {x + 1} = { val a: {x} = x; val t: Id[{a + 1}] = a + 1; t }
+
+  { val a = 0; a + 1 }
+  { val a = 0; 1 + a }
+}
+
+
+object Bounds {
+  @annotation.implicitNotFound(msg = "Cannot prove that ${B} holds.")
+  sealed abstract class P[B <: Boolean](val b: B)
+  private[this] val prop_singleton = new P[true](true) {}
+  object P {
+    def assume(b: Boolean): P[b.type] = prop_singleton.asInstanceOf[P[b.type]]
+  }
+
+  def if_(cond: Boolean): (implicit (ev: P[cond.type]) => Unit) => Unit =
+    thn => if (cond) thn(P.assume(cond))
+
+
+  // Bounds-checked
+
+  def index(k: Int)(implicit ev: P[{k >= 0}]): Int = k
+
+  def run(i: Int) =
+    if_(i >= 0) {
+      index(i)
+    }
+
+
+  // Boxed value with a predicate
+
+  class PredBox[T, B <: Boolean](val v: T)(val p: P[B])
+  object PredBox {
+    def apply[T, B <: Boolean](v: T)(implicit ev: P[B]) = new PredBox[T, B](v)(ev)
+  }
+
+  def run2(i: Int) =
+    if_(i != 0) {
+      PredBox[Int, {i != 0}](i)
+    }
+}
+
+
+object ArithmeticIdentities {
+  type SInt = Int & Singleton
+
+  class DecomposeHelper[V <: SInt](val v: V) {
+    import DecomposeHelper._
+    def asSumOf[X <: SInt, Y <: SInt](x: X, y: Y)(implicit ev: {v} =:= {x + y}): SumOf[{x}, {y}] = SumOf(x, y)(ev(v))
+  }
+
+  object DecomposeHelper {
+    /* Axioms */
+    sealed trait Decomposition[V <: SInt]
+    case class SumOf[X <: SInt, Y <: SInt](x: X, y: Y)(val v: {x + y}) extends Decomposition[{v}] {
+      def commuted: SumOf[Y, X] = SumOf(y, x)(v.asInstanceOf[{y + x}])
+    }
+  }
+
+  implicit def toDecomposeHelper[V <: Int](v: V): DecomposeHelper[v.type] = new DecomposeHelper(v)
+
+
+  // Let's "show" that x + 1 == 1 + x
+
+  val x = 123
+  (x + 1).asSumOf(x, 1).v: {x + 1}
+  (x + 1).asSumOf(x, 1).commuted.v: {1 + x}
+}
+
+
+//object ArithmeticIdentities2 {
+//  // FIXME: Crashes during the computation of `add`'s signature (when typing the ident `add`):
+//  def add[X<:Int, Y<:Int, Z<:Int](x: X, y: Y, z: {x + y}): z.type = z
+//  val x = 1
+//  add(x, x, x + x)
+//}
\ No newline at end of file