import UInt

import Base

import Nat

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

abs_neg: (all n:Int. abs(- n) = abs(n))

neg_zero: - +0 = +0

neg_involutive: (all n:Int. - (- n) = n)

int_zero_add: (all n:Int. +0 + n = n)

int_add_zero: (all n:Int. n + +0 = n)

int_add_commute: (all x:Int, y:Int. x + y = y + x)

add_commute_uint_int: (all x:UInt, y:Int. x + y = y + x)

int_add_assoc: (all x:Int, y:Int, z:Int. (x + y) + z = x + (y + z))

int_add_inverse: (all x:Int. x + - x = +0)

neg_distr_add: (all x:Int, y:Int. - (x + y) = - x + - y)

int_sub_cancel: (all x:Int. x - x = +0)

int_one_mult: (all x:Int. +1 * x = x)

int_zero_mult: (all x:Int. +0 * x = +0)

dist_neg_mult: (all x:Int, y:Int. - (x * y) = - x * y)

int_mult_commute: (all x:Int, y:Int. x * y = y * x)

int_mult_one: (all x:Int. x * +1 = x)

int_mult_zero: (all x:Int. x * +0 = +0)

int_mult_assoc: (all x:Int, y:Int, z:Int. (x * y) * z = x * (y * z))

int_less_equal_refl: (all n:Int. n ≤ n)

int_less_equal_trans: (all m:Int, n:Int, o:Int. (if (m ≤ n and n ≤ o) then m ≤ o))

int_less_equal_antisymmetric: (all x:Int, y:Int. (if (x ≤ y and y ≤ x) then x = y))