1 | package metascala |
---|

2 | |
---|

3 | object 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 | } |
---|