public open import Arith::Nat
public open import Arith::Bool
open import Paths
open import Algebra::Formula

open data Int
| signed Bool Nat
| posneg : neg 0 = pos 0

def pos ⇒ signed true
def neg ⇒ signed false

def negate Int : Int
| signed b n ⇒ signed (not b) n
| posneg i ⇒ posneg (~ i)

def succInt Int : Int
| signed true n ⇒ pos (suc n)
| signed false (suc n) ⇒ neg n
| signed false zero ⇒ pos 1
| posneg i ⇒ pos 1

def abs Int : Nat
| signed _ n ⇒ n
| posneg i ⇒ 0

// TODO: reimplement using univalence
def predInt (x : Int) : Int ⇒ negate (succInt (negate x))

def subI (x y : Int) : Int ⇒ addI x (negate y)

def addI : BinOp Int
| signed _ 0, n ⇒ n
| posneg _, n ⇒ n
| signed true (suc m), n ⇒ succInt (addI (pos m) n)
| signed false (suc m), n ⇒ predInt (addI (neg m) n)

/*
def addI-comm (a b : Int) : addI a b = addI b a
| pos n, pos m => pmap pos (+-comm n m)
| neg n, neg m => pmap neg (+-comm n m)
| pos n, neg m => idp
| neg n, pos m => idp
*/