From 1d124e9455ecb56d8fcfa42c4523f70c5cb0a952 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 27 Feb 2017 11:26:17 +0100
Subject: New test

The HLists test brought out the unsoundness of alias
rewriting in glbs which is tackled in the last commit.
---
 tests/run/HLists.check |  8 ++++++
 tests/run/HLists.scala | 78 ++++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 86 insertions(+)
 create mode 100644 tests/run/HLists.check
 create mode 100644 tests/run/HLists.scala

(limited to 'tests/run')

diff --git a/tests/run/HLists.check b/tests/run/HLists.check
new file mode 100644
index 000000000..53efe30d7
--- /dev/null
+++ b/tests/run/HLists.check
@@ -0,0 +1,8 @@
+1
+A
+true
+true
+HCons(1,HCons(A,HCons(true,HNil)))
+1
+A
+true
diff --git a/tests/run/HLists.scala b/tests/run/HLists.scala
new file mode 100644
index 000000000..eebbcb4cd
--- /dev/null
+++ b/tests/run/HLists.scala
@@ -0,0 +1,78 @@
+sealed trait HList
+case class HCons[+HD, +TL](hd: HD, tl: TL) extends HList
+case object HNil extends HList
+
+sealed trait Num
+case object Zero extends Num
+case class Succ[N <: Num](pred: N) extends Num
+
+object Test {
+
+  type HNil = HNil.type
+  type Zero = Zero.type
+
+  trait Concat[Xs <: HList, Ys <: HList, Zs <: HList] {
+    def concat(xs: Xs, ys: Ys): Zs
+  }
+
+  implicit def concatNil[Xs <: HList]: Concat[HNil, Xs, Xs] =
+    new Concat[HNil, Xs, Xs] {
+      def concat(fst: HNil, snd: Xs) = snd
+    }
+
+  implicit def concatCons[X, Xs <: HList, Ys <: HList, Zs <: HList](
+    implicit ev: Concat[Xs, Ys, Zs]
+  ): Concat[HCons[X, Xs], Ys, HCons[X, Zs]] =
+    new Concat[HCons[X, Xs], Ys, HCons[X, Zs]] {
+      def concat(xs: HCons[X, Xs], ys: Ys): HCons[X, Zs] =
+        HCons(xs.hd, ev.concat(xs.tl, ys))
+    }
+
+  def concat[Xs <: HList, Ys <: HList, Zs <: HList](xs: Xs, ys: Ys)(implicit ev: Concat[Xs, Ys, Zs]): Zs =
+    ev.concat(xs, ys)
+
+  val xs = HCons(1, HCons("A", HNil))
+  val ys = HCons(true, HNil)
+  val zs = concat(xs, ys)
+  val zs1: HCons[Int, HCons[String, HCons[Boolean, HNil]]] = zs
+
+  trait At[Xs <: HList, N <: Num] {
+    type Out
+    def at(xs: Xs, n: N): Out
+  }
+
+  implicit def atZero[XZ, Xs <: HList]: At[HCons[XZ, Xs], Zero] { type Out = XZ } =
+    new At[HCons[XZ, Xs], Zero] {
+      type Out = XZ
+      def at(xs: HCons[XZ, Xs], n: Zero) = xs.hd
+    }
+
+  implicit def atSucc[XX, Xs <: HList, N <: Num](
+    implicit ev: At[Xs, N]
+  ): At[HCons[XX, Xs], Succ[N]] { type Out = ev.Out } = new At[HCons[XX, Xs], Succ[N]] {
+    type Out = ev.Out
+    def at(xs: HCons[XX, Xs], n: Succ[N]): Out = ev.at(xs.tl, n.pred)
+  }
+
+  def at[Xs <: HList, N <: Num](xs: Xs, n: N)(
+    implicit ev: At[Xs, N]
+  ): ev.Out = ev.at(xs, n)
+
+  def main(args: Array[String]) = {
+    val ys1 = HCons(1, HNil)
+    println(at(ys1, Zero))
+
+    val ys2 = HCons(1, HCons("A", HNil))
+    val y2 = at(ys2, Succ(Zero))
+    println(at(ys2, Succ(Zero)))
+    val ys3 = HCons(1, HCons("A", HCons(true, HNil)))
+    println(at(ys3, Succ(Succ(Zero))))
+    val ys4 = HCons(1, HCons("A", HCons(true, HCons(1.0, HNil))))
+    println(at(ys4, Succ(Succ(Zero))))
+
+    println(zs1)
+    println(at(zs1, Zero))
+    println(at(zs1, Succ(Zero)))
+    println(at(zs1, Succ(Succ(Zero))))
+  }
+}
-- 
cgit v1.2.3