@@ -38,12 +38,7 @@ trait Peano {
3838 val Succ : SuccExtractor
3939 trait SuccExtractor {
4040 def apply (nat : Nat ): Succ
41- def unapply (nat : Nat ): SuccOpt { def refinedScrutinee : Succ & nat.type }
42- }
43- trait SuccOpt {
44- def isEmpty : Boolean
45- def refinedScrutinee : Succ
46- def get : Nat
41+ def unapply (nat : Nat ): RefinedScrutinee [nat.type & Succ , Nat ]
4742 }
4843}
4944
@@ -58,13 +53,10 @@ object IntNums extends Peano {
5853
5954 object Succ extends SuccExtractor {
6055 def apply (nat : Nat ): Succ = nat + 1
61- def unapply (nat : Nat ) = new SuccOpt {
62- def isEmpty : Boolean = nat == 0
63- def refinedScrutinee : Succ & nat.type = nat
64- def get : Int = nat - 1
65- }
56+ def unapply (nat : Nat ) =
57+ if (nat == 0 ) RefinedScrutinee .noMatch
58+ else RefinedScrutinee .matchOf(nat)(nat - 1 )
6659 }
67-
6860 def succDeco (succ : Succ ): SuccAPI = new SuccAPI {
6961 def pred : Nat = succ - 1
7062 }
@@ -75,17 +67,7 @@ object ClassNums extends Peano {
7567 object ZeroObject extends NatTrait {
7668 override def toString : String = " ZeroObject"
7769 }
78- case class SuccClass (predecessor : NatTrait ) extends NatTrait with SuccOpt {
79- def isEmpty : Boolean = false
80- def refinedScrutinee : this .type = this
81- def get : NatTrait = this
82- }
83-
84- object SuccNoMatch extends SuccOpt {
85- def isEmpty : Boolean = true
86- def refinedScrutinee : Nothing = throw new NoSuchElementException
87- def get : NatTrait = throw new NoSuchElementException
88- }
70+ case class SuccClass (predecessor : NatTrait ) extends NatTrait
8971
9072 type Nat = NatTrait
9173 type Zero = ZeroObject .type
@@ -109,8 +91,8 @@ object ClassNums extends Peano {
10991 object Succ extends SuccExtractor {
11092 def apply (nat : Nat ): Succ = new SuccClass (nat)
11193 def unapply (nat : Nat ) = nat match {
112- case nat : (SuccClass & nat.type ) => nat
113- case _ => SuccNoMatch
94+ case nat : (SuccClass & nat.type ) => RefinedScrutinee .matchOf( nat)(nat.predecessor)
95+ case _ => RefinedScrutinee .noMatch
11496 }
11597 }
11698
0 commit comments