package hstar.utils

/**
 * Developed with pleasure :)<br>
 * User: HoD<br>
 * Date: 14.02.11<br>
 * Time: 21:56<br>
 */

object ChurchNumerals {
  trait CInt {
    type Succ <: CInt
    type Add[N <: CInt] <: CInt
    type Pred <: CInt
    type Sub[N <: CInt] <: CInt
    type Neg <: CInt
  }

  trait CPos extends CInt

  trait CNeg extends CInt

  class CSucc[P <: CPos] extends CPos {
    type Succ = CSucc[CSucc[P]]
    type Add[N <: CInt] = P#Add[N]#Succ
    type Pred = P
    type Sub[N <: CInt] = P#Sub[N]#Succ
    type Neg = P#Neg#Pred
  }

  class CPred[S <: CNeg] extends CNeg {
    type Succ = S
    type Add[N <: CInt] = S#Add[N]#Pred
    type Pred = CPred[CPred[S]]
    type Sub[N <: CInt] = S#Sub[N]#Pred
    type Neg = S#Neg#Succ
  }

  final class _0 extends CPos with CNeg {
    type Succ = CSucc[_0]
    type Add[N <: CInt] = N
    type Pred = CPred[_0]
    type Sub[N <: CInt] = N#Neg
    type Neg = _0
  }

  type +[N1 <: CInt, N2 <: CInt] = N1#Add[N2]
  type -[N1 <: CInt, N2 <: CInt] = N1#Sub[N2]
}