Use value for Zero in the abstract interface

Author: nicolasstucki

tests/run/fully-abstract-nat-7.check

@@ -0,0 +1,17 @@
+CaseNums
+ok
+ok
+ok - unchecked error
+None
+Some((SuccClass(ZeroObj),SuccClass(ZeroObj)))
+None
+Some((SuccClass(ZeroObj),SuccClass(ZeroObj)))
+
+IntNums
+ok
+ok
+ok - unchecked error
+None
+Some((1,1))
+None
+Some((1,1))

tests/run/fully-abstract-nat-7.scala

@@ -0,0 +1,160 @@
+
+object Test {
+  def main(args: Array[String]): Unit = {
+      println("CaseNums")
+      test(CaseNums)
+      println()
+      println("IntNums")
+      test(IntNums)
+  }
+
+  def test(numbers: Numbers) = {
+    import numbers._
+
+    val zero: Nat = Zero
+    val one: Nat = Succ(zero)
+    val two: Nat = Succ(one)
+    val three: Nat = Succ(two)
+
+    zero match {
+      case Succ(p) => println("error")
+      case Zero => println("ok") // extra argument removed by language extension
+    }
+
+    one match {
+      case Zero => println("error") // extra argument removed by language extension
+      case Succ(p) => println("ok")
+    }
+
+    zero match {
+      case s: Succ => println("ok - unchecked error")
+      case z: Zero => println("ok - unchecked no error")
+    }
+
+    def divOpt(a: Nat, b: Nat): Option[(Nat, Nat)] = b match {
+      case s @ Succ(p) =>
+        Some(safeDiv(a, s.asInstanceOf[Succ])) // this case will not be needed
+      case _ => None
+    }
+    println(divOpt(one, zero))
+    println(divOpt(three, two))
+
+    def divOptExpanded(a: Nat, b: Nat): Option[(Nat, Nat)] = {
+      val x0 = Succ.unapply(b)
+      if (!x0.isEmpty) {
+        val s = b.asInstanceOf[x0.Refined] // safe unchecked cast inserted by the language extension
+        val p = x0.get
+        Some(safeDiv(a, s))
+      } else {
+        None
+      }
+    }
+    println(divOptExpanded(one, zero))
+    println(divOptExpanded(three, two))
+  }
+}
+
+trait Numbers {
+
+  type Nat
+  type Zero <: Nat
+  type Succ <: Nat
+
+  val Zero: Zero
+
+  val Succ: SuccExtractor
+  trait SuccExtractor {
+    def apply(nat: Nat): Succ
+    def unapply(nat: Nat): SuccOpt { type Refined <: nat.type } // check that SuccOpt#Refined <: nat.type. Could be forced by the compiler?
+  }
+  trait SuccOpt {
+    type Refined <: Succ // optionally added by language extension
+    def get: Nat
+    def isEmpty: Boolean
+  }
+
+  implicit def SuccDeco(succ: Succ): SuccAPI
+  trait SuccAPI {
+    def pred: Nat
+  }
+
+  def safeDiv(a: Nat, b: Succ): (Nat, Nat)
+}
+
+object CaseNums extends Numbers {
+
+  trait NatClass
+  case object ZeroObj extends NatClass
+  case class SuccClass(pred: NatClass) extends NatClass with SuccOpt {
+    type Refined = this.type
+    def get: NatClass = pred
+    def isEmpty: Boolean = false
+  }
+
+  class EmptySuccOpt extends SuccOpt {
+    type Refined = Nothing
+    def isEmpty: Boolean = true
+    def get: NatClass = throw new Exception("empty")
+  }
+
+  type Nat = NatClass
+  type Zero = ZeroObj.type
+  type Succ = SuccClass
+
+  val Zero: Zero = ZeroObj
+
+  object Succ extends SuccExtractor {
+    def apply(nat: Nat): Succ = SuccClass(nat)
+    def unapply(nat: Nat) = nat match {
+      case succ: SuccClass => succ.asInstanceOf[nat.type & SuccClass]
+      case _ => new EmptySuccOpt
+    }
+  }
+
+  def SuccDeco(succ: Succ): SuccAPI = new SuccAPI {
+    def pred: Nat = succ.pred
+  }
+
+  def safeDiv(a: Nat, b: Succ): (Nat, Nat) = {
+    def sdiv(div: Nat, rem: Nat): (Nat, Nat) =
+      if (lessOrEq(rem, b)) (div, rem)
+      else sdiv(Succ(div), minus(rem, b))
+    sdiv(Zero, a)
+  }
+
+  private def lessOrEq(a: Nat, b: Nat): Boolean = (a, b) match {
+    case (Succ(a1), Succ(b1)) => lessOrEq(a1, b1)
+    case (Zero, _) => true // extra argument removed by language extension
+    case _ => false
+  }
+
+  // assumes a >= b
+  private def minus(a: Nat, b: Nat): Nat = (a, b) match {
+    case (Succ(a1), Succ(b1)) => minus(a1, b1)
+    case _ => a
+  }
+
+}
+
+object IntNums extends Numbers {
+  type Nat = Int
+  type Zero = Int // 0
+  type Succ = Int // n > 0
+
+  val Zero = 0
+
+  object Succ extends SuccExtractor {
+    def apply(nat: Nat): Int = nat + 1
+    def unapply(nat: Nat) = new SuccOpt {
+      type Refined = nat.type
+      def isEmpty: Boolean = nat <= 0
+      def get: Int = nat - 1
+    }
+  }
+
+  def SuccDeco(succ: Succ): SuccAPI = new SuccAPI {
+    def pred: Int = succ - 1
+  }
+
+  def safeDiv(a: Nat, b: Succ): (Nat, Nat) = (a / b, a % b)
+}