Skip to content

Commit 6d8f4c3

Browse files
nicolasstuckinicolasstucki
committed
Add full examples from paper
1 parent 45f1014 commit 6d8f4c3

8 files changed

+693
-0
lines changed

‎tests/run/fully-abstract-nat-1.check‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CaseNums
2+
ok
3+
ok
4+
ok - unchecked error
5+
None
6+
Some((SuccClass(ZeroObj),SuccClass(ZeroObj)))
7+
8+
IntNums
9+
ok
10+
ok
11+
ok - unchecked error
12+
None
13+
Some((1,1))

‎tests/run/fully-abstract-nat-1.scala‎

Lines changed: 142 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,142 @@
1+
2+
object Test {
3+
def main(args: Array[String]): Unit = {
4+
println("CaseNums")
5+
test(CaseNums)
6+
println()
7+
println("IntNums")
8+
test(IntNums)
9+
}
10+
11+
def test(numbers: Numbers) = {
12+
import numbers._
13+
14+
val zero: Nat = Zero()
15+
val one: Nat = Succ(zero)
16+
val two: Nat = Succ(one)
17+
val three: Nat = Succ(two)
18+
19+
zero match {
20+
case Succ(p) => println("error")
21+
case Zero() => println("ok")
22+
}
23+
24+
one match {
25+
case Zero() => println("error")
26+
case Succ(p) => println("ok")
27+
}
28+
29+
zero match {
30+
case s: Succ => println("ok - unchecked error")
31+
case z: Zero => println("ok - unchecked no error")
32+
}
33+
34+
def divOpt(a: Nat, b: Nat): Option[(Nat, Nat)] = b match {
35+
case s @ Succ(_) =>
36+
// s is of type Nat though we know it is a Succ
37+
Some(safeDiv(a, s.asInstanceOf[Succ]))
38+
case _ => None
39+
}
40+
41+
println(divOpt(one, zero))
42+
println(divOpt(three, two))
43+
}
44+
}
45+
46+
trait Numbers {
47+
48+
type Nat
49+
type Zero <: Nat
50+
type Succ <: Nat
51+
52+
val Zero: ZeroExtractor
53+
trait ZeroExtractor {
54+
def apply(): Zero
55+
def unapply(nat: Nat): Boolean
56+
}
57+
58+
val Succ: SuccExtractor
59+
trait SuccExtractor {
60+
def apply(nat: Nat): Succ
61+
def unapply(nat: Nat): Option[Nat]
62+
}
63+
64+
implicit def SuccDeco(succ: Succ): SuccAPI
65+
trait SuccAPI {
66+
def pred: Nat
67+
}
68+
69+
def safeDiv(a: Nat, b: Succ): (Nat, Nat)
70+
}
71+
72+
73+
object CaseNums extends Numbers {
74+
75+
trait NatClass
76+
case object ZeroObj extends NatClass
77+
case class SuccClass(pred: NatClass) extends NatClass
78+
79+
type Nat = NatClass
80+
type Zero = ZeroObj.type
81+
type Succ = SuccClass
82+
83+
object Zero extends ZeroExtractor {
84+
def apply(): Zero = ZeroObj
85+
def unapply(nat: Nat): Boolean = nat == ZeroObj
86+
}
87+
88+
object Succ extends SuccExtractor {
89+
def apply(nat: Nat): Succ = SuccClass(nat)
90+
def unapply(nat: Nat): Option[Nat] = nat match {
91+
case SuccClass(pred) => Some(pred)
92+
case _ => None
93+
}
94+
}
95+
96+
def SuccDeco(succ: Succ): SuccAPI = new SuccAPI {
97+
def pred: Nat = succ.pred
98+
}
99+
100+
def safeDiv(a: Nat, b: Succ): (Nat, Nat) = {
101+
def sdiv(div: Nat, rem: Nat): (Nat, Nat) =
102+
if (lessOrEq(rem, b)) (div, rem)
103+
else sdiv(Succ(div), minus(rem, b))
104+
sdiv(Zero(), a)
105+
}
106+
107+
private def lessOrEq(a: Nat, b: Nat): Boolean = (a, b) match {
108+
case (Succ(a1), Succ(b1)) => lessOrEq(a1, b1)
109+
case (Zero(), _) => true
110+
case _ => false
111+
}
112+
113+
// assumes a >= b
114+
private def minus(a: Nat, b: Nat): Nat = (a, b) match {
115+
case (Succ(a1), Succ(b1)) => minus(a1, b1)
116+
case _ => a
117+
}
118+
119+
}
120+
121+
object IntNums extends Numbers {
122+
type Nat = Int
123+
type Zero = Int // 0
124+
type Succ = Int // n > 0
125+
126+
object Zero extends ZeroExtractor {
127+
def apply(): Int = 0
128+
def unapply(nat: Nat): Boolean = nat == 0
129+
}
130+
131+
object Succ extends SuccExtractor {
132+
def apply(nat: Nat): Int = nat + 1
133+
def unapply(nat: Nat): Option[Int] =
134+
if (nat > 0) Some(nat - 1) else None
135+
}
136+
137+
def SuccDeco(succ: Succ): SuccAPI = new SuccAPI {
138+
def pred: Int = succ - 1
139+
}
140+
141+
def safeDiv(a: Nat, b: Succ): (Nat, Nat) = (a / b, a % b)
142+
}

‎tests/run/fully-abstract-nat-2.check‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CaseNums
2+
ok
3+
ok
4+
ok
5+
None
6+
Some((SuccClass(ZeroObj),SuccClass(ZeroObj)))
7+
8+
IntNums
9+
error
10+
error
11+
error
12+
/ by zero
13+
Some((1,1))

‎tests/run/fully-abstract-nat-2.scala‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
2+
import scala.reflect.ClassTag
3+
4+
object Test {
5+
def main(args: Array[String]): Unit = {
6+
println("CaseNums")
7+
test(CaseNums)
8+
println()
9+
println("IntNums")
10+
test(IntNums)
11+
}
12+
13+
def test(numbers: Numbers) = {
14+
import numbers._
15+
16+
val zero: Nat = Zero()
17+
val one: Nat = Succ(zero)
18+
val two: Nat = Succ(one)
19+
val three: Nat = Succ(two)
20+
21+
zero match {
22+
case Succ(p) => println("error")
23+
case Zero() => println("ok")
24+
}
25+
26+
one match {
27+
case Zero() => println("error")
28+
case Succ(p) => println("ok")
29+
}
30+
31+
zero match {
32+
case s: Succ => println("error") // Will happen with IntNums
33+
case z: Zero => println("ok")
34+
}
35+
36+
def divOpt(a: Nat, b: Nat): Option[(Nat, Nat)] = b match {
37+
case s @ Succ(_) => Some(safeDiv(a, s))
38+
case _ => None
39+
}
40+
41+
try println(divOpt(one, zero))
42+
catch { case ex: java.lang.ArithmeticException => println(ex.getMessage) }
43+
println(divOpt(three, two))
44+
}
45+
}
46+
47+
trait Numbers {
48+
49+
type Nat
50+
type Zero <: Nat
51+
type Succ <: Nat
52+
53+
implicit def natTag: ClassTag[Nat]
54+
implicit def zeroTag: ClassTag[Zero]
55+
implicit def succTag: ClassTag[Succ]
56+
57+
val Zero: ZeroExtractor
58+
trait ZeroExtractor {
59+
def apply(): Zero
60+
def unapply(zero: Zero): Boolean
61+
}
62+
63+
val Succ: SuccExtractor
64+
trait SuccExtractor {
65+
def apply(nat: Nat): Succ
66+
def unapply(succ: Succ): Option[Nat]
67+
}
68+
69+
implicit def SuccDeco(succ: Succ): SuccAPI
70+
trait SuccAPI {
71+
def pred: Nat
72+
}
73+
74+
def safeDiv(a: Nat, b: Succ): (Nat, Nat)
75+
}
76+
77+
78+
object CaseNums extends Numbers {
79+
80+
trait NatClass
81+
object ZeroObj extends NatClass { override def toString: String = "ZeroObj" }
82+
case class SuccClass(pred: NatClass) extends NatClass
83+
84+
type Nat = NatClass
85+
type Zero = ZeroObj.type
86+
type Succ = SuccClass
87+
88+
def natTag: ClassTag[Nat] = implicitly[ClassTag[NatClass]]
89+
def zeroTag: ClassTag[Zero] = implicitly[ClassTag[ZeroObj.type]]
90+
def succTag: ClassTag[Succ] = implicitly[ClassTag[SuccClass]]
91+
92+
object Zero extends ZeroExtractor {
93+
def apply(): Zero = ZeroObj
94+
def unapply(zero: Zero): Boolean = true
95+
}
96+
97+
object Succ extends SuccExtractor {
98+
def apply(nat: Nat): Succ = SuccClass(nat)
99+
def unapply(succ: Succ): Option[Nat] = Some(succ.pred)
100+
}
101+
102+
def SuccDeco(succ: Succ): SuccAPI = new SuccAPI {
103+
def pred: Nat = succ.pred
104+
}
105+
106+
def safeDiv(a: Nat, b: Succ): (Nat, Nat) = {
107+
def sdiv(div: Nat, rem: Nat): (Nat, Nat) =
108+
if (lessOrEq(rem, b)) (div, rem)
109+
else sdiv(Succ(div), minus(rem, b))
110+
sdiv(Zero(), a)
111+
}
112+
113+
private def lessOrEq(a: Nat, b: Nat): Boolean = (a, b) match {
114+
case (Succ(a1), Succ(b1)) => lessOrEq(a1, b1)
115+
case (Zero(), _) => true
116+
case _ => false
117+
}
118+
119+
// assumes a >= b
120+
private def minus(a: Nat, b: Nat): Nat = (a, b) match {
121+
case (Succ(a1), Succ(b1)) => minus(a1, b1)
122+
case _ => a
123+
}
124+
125+
}
126+
127+
object IntNums extends Numbers {
128+
type Nat = Int
129+
type Zero = Int // 0
130+
type Succ = Int // n > 0
131+
132+
// BROKEN
133+
// All class tags are identical: Nat, Zero and Succ cannot be distinguished
134+
def natTag: ClassTag[Int] = ClassTag.Int
135+
def zeroTag: ClassTag[Int] = ClassTag.Int // will also match any Int that is non zero
136+
def succTag: ClassTag[Int] = ClassTag.Int // will also match 0
137+
138+
object Zero extends ZeroExtractor {
139+
def apply(): Int = 0
140+
def unapply(zero: Zero): Boolean = true
141+
}
142+
143+
object Succ extends SuccExtractor {
144+
def apply(nat: Nat): Int = nat + 1
145+
def unapply(succ: Succ): Option[Int] = Some(succ - 1)
146+
}
147+
148+
def SuccDeco(succ: Succ): SuccAPI = new SuccAPI {
149+
def pred: Int = succ - 1
150+
}
151+
152+
def safeDiv(a: Nat, b: Succ): (Nat, Nat) = (a / b, a % b)
153+
}

‎tests/run/fully-abstract-nat-3.check‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CaseNums
2+
ok
3+
ok
4+
ok - unchecked error
5+
None
6+
Some((SuccClass(ZeroObj),SuccClass(ZeroObj)))
7+
8+
IntNums
9+
ok
10+
ok
11+
ok - unchecked error
12+
None
13+
Some((1,1))

0 commit comments

Comments
 (0)