import UInt

import Base

union Int {
  pos(UInt)
  negsuc(UInt)
}

fun abs(x:Int) {
  switch x {
    case pos(n) {
      n
    }
    case negsuc(n) {
      1 + n
    }
  }
}

union Sign {
  positive
  negative
}

fun sign(n:Int) {
  switch n {
    case pos(n') {
      positive
    }
    case negsuc(n') {
      negative
    }
  }
}

fun operator *(s1:Sign, s2:Sign) {
  switch s1 {
    case positive {
      s2
    }
    case negative {
      flip(s2)
    }
  }
}

fun operator -(x:Int) {
  switch x {
    case pos(n) {
      (if n = 0 then +0 else negsuc(n ∸ 1))
    }
    case negsuc(n) {
      pos(1 + n)
    }
  }
}

fun operator -(n:UInt) {
  - pos(n)
}

fun operator *(s:Sign, n:Int) {
  switch s {
    case positive {
      n
    }
    case negative {
      - n
    }
  }
}

fun operator *(s:Sign, n:UInt) {
  s * pos(n)
}

fun operator ⊝(x:UInt, y:UInt) {
  if x < y then
    - (y ∸ x)
  else
    pos(x ∸ y)
}

fun operator +(x:Int, m:Int) {
  switch x {
    case pos(n) {
      switch m { case pos(n') { pos(n + n') } case negsuc(n') { n ⊝ (1 + n') } }
    }
    case negsuc(n) {
      switch m { case pos(n') { n' ⊝ (1 + n) } case negsuc(n') { negsuc((1 + n) + n') } }
    }
  }
}

fun operator +(n:UInt, m:Int) {
  pos(n) + m
}

fun operator +(n:Int, m:UInt) {
  n + pos(m)
}

fun operator -(n:Int, m:Int) {
  n + - m
}

fun operator -(n:UInt, m:Int) {
  pos(n) - m
}

fun operator -(n:Int, m:UInt) {
  n - pos(m)
}

fun operator -(x:UInt, y:UInt) {
  pos(x) - pos(y)
}

fun operator *(x:Int, y:Int) {
  (sign(x) * sign(y)) * (abs(x) * abs(y))
}

fun operator *(n:UInt, m:Int) {
  pos(n) * m
}

fun operator *(n:Int, m:UInt) {
  n * pos(m)
}

fun operator /(n:Int, m:Int) {
  (sign(n) * sign(m)) * (abs(n) / abs(m))
}

fun operator /(n:Int, m:UInt) {
  sign(n) * (abs(n) / m)
}

fun operator ≤(a:Int, y:Int) {
  switch a {
    case pos(x) {
      switch y { case pos(y') { x ≤ y' } case negsuc(y') { false } }
    }
    case negsuc(x) {
      switch y { case pos(y') { true } case negsuc(y') { y' ≤ x } }
    }
  }
}