source: src/metascala/Nats.scala @ 26

Revision 21, 2.1 KB checked in by mayhem, 5 years ago (diff)

.

Line 
1package metascala
2
3object Nats {
4  import Utils._
5  import Booleans._
6  import Addables._
7  import Comparables._
8  import Visitables._
9
10  trait NatVisitor extends TypeVisitor {
11    type Visit0 <: ResultType
12    type VisitSucc[Pre <: Nat] <: ResultType
13  }
14 
15  sealed trait Nat extends Addable with Comparable {
16    type CompareType = Nat
17   
18    type Pre
19    type Is0 <: Bool
20    type Add[T <: Nat] <: Nat
21    type AddType = Nat
22    type Accept[N <: NatVisitor] <: N#ResultType
23    type Equals[N <: Nat] <: Bool
24    type LessThan[N <: Nat] <: Bool
25
26    def toInt : Int
27  }
28 
29  final class _0 extends Nat {
30    type Pre = Invalid
31    type Is0 = True
32    type Add[N <: Nat] = N
33    type Accept[N <: NatVisitor] = N#Visit0
34
35    type Equals[N <: Nat] = N#Is0
36    type LessThan[N <: Nat] = N#Is0#Not
37
38    def toInt = 0
39  }
40 
41  final case class Succ[P <: Nat](toInt : Int) extends Nat {
42    type Pre = P
43    type Is0 = False
44    type Add[N <: Nat] = Succ[P#Add[N]]
45    type Accept[N <: NatVisitor] = N#VisitSucc[P]
46
47    trait EqualsVisitor extends NatVisitor {
48      type ResultType = Bool
49      type Visit0 = False
50      type VisitSucc[Pre <: Nat] = P#Equals[Pre]
51    }
52
53    type Equals[N <: Nat] = N#Accept[EqualsVisitor]
54
55    trait LessThanVisitor extends NatVisitor {
56      type ResultType = Bool
57      type Visit0 = False
58      type VisitSucc[Pre <: Nat] = P#LessThan[Pre]
59    }
60
61    type LessThan[N <: Nat] = N#Accept[LessThanVisitor]
62
63    def +[N <: Nat](n : N) : Add[N] = Succ[P#Add[N]](toInt + n.toInt)
64  }
65 
66  type _1 = Succ[_0]
67  type _2 = Succ[_1]
68  type _3 = Succ[_2]
69  type _4 = Succ[_3]
70  type _5 = Succ[_4]
71  type _6 = Succ[_5]
72  type _7 = Succ[_6]
73  type _8 = Succ[_7]
74  type _9 = Succ[_8]
75  type _10 = Succ[_9]
76 
77  val _0 = new _0
78  val _1 = new _1(1)
79  val _2 = new _2(2)
80  val _3 = new _3(3)
81  val _4 = new _4(4)
82  val _5 = new _5(5)
83  val _6 = new _6(6)
84  val _7 = new _7(7)
85  val _8 = new _8(8)
86  val _9 = new _9(9)
87  val _10 = new _10(10)
88
89  implicit val _0ToInt = TypeToValue[_0, Int](0)
90  implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) = TypeToValue[Succ[P], Int](1 + v.value)
91
92  def toInt[T <: Nat](v : T)(implicit fn : TypeToValue[T, Int]) = fn()
93}
Note: See TracBrowser for help on using the repository browser.