module MiniLibrary.Integer where

open import MiniLibrary.Base
open import MiniLibrary.Nat
open import MiniLibrary.Natplus

data  : Set where
  +_     :  ℕ+         
  zero   :   
  -_     :  ℕ+        


_<ℤb_ :     Bool
(- n) <ℤb (- m) = m <ℕ+b n
(- n) <ℤb z     = true
zero  <ℤb (+ m) = true
zero  <ℤb z     = false
(+ n) <ℤb (+ m) = n <ℕ+b m
(+ n) <ℤb z     = false

_<ℤ_ :     Set
n <ℤ m = True (n <ℤb m)

_≤ℤb_ :     Bool
(- n) ≤ℤb (- m) = m ≤ℕ+b n
(- n) ≤ℤb z     = true
zero  ≤ℤb (- m) = false
zero  ≤ℤb z     = true
(+ n) ≤ℤb (+ m) = n ≤ℕ+b m
(+ n) ≤ℤb z     = false

_≤ℤ_ :     Set
z ≤ℤ z' = True (z ≤ℤb z')

_≥ℤb_ :   ->     Bool
z ≥ℤb z' = z' ≤ℤb z


_≥ℤ_ :   ->   -> Set
z ≥ℤ z' = z' ≤ℤ z




_==ℤb_ :     Bool
(- n) ==ℤb (- m) = m ==ℕ+b n
(- n) ==ℤb z     = false
zero  ==ℤb zero  = true
zero  ==ℤb z     = false
(+ n) ==ℤb (+ m) = n ==ℕ+b m
(+ n) ==ℤb z     = false

_==ℤ_ :     Set
n ==ℤ m = True (n ==ℤb m)

decideℤ : (z z' : )  z <ℤ   z'  z ==ℤ z'  z' <ℤ z
decideℤ (- n) (- m) = decideℕ+ m n 
decideℤ (- n) (+ _) = in0 triv
decideℤ (- n) zero  = in0 triv
decideℤ zero (+ _)  = in0 triv
decideℤ zero zero   = in1 triv
decideℤ zero (- _)  = in2 triv
decideℤ (+ n) (+ m) = decideℕ+ n m
decideℤ (+ n) zero  = in2 triv
decideℤ (+ n) (- _) = in2 triv


decideℤ≤ : (z z' : )  z ≤ℤ   z'  z' ≤ℤ z
decideℤ≤ (- n) (- m) = decideℕ+≤ m n 
decideℤ≤ (- n) (+ _) = inl triv
decideℤ≤ (- n) zero  = inl triv
decideℤ≤ zero (+ _) = inl triv
decideℤ≤ zero zero = inl triv
decideℤ≤ zero (- _) = inr triv
decideℤ≤ (+ n) (+ m) = decideℕ+≤ n m
decideℤ≤ (+ n) zero = inr triv
decideℤ≤ (+ n) (- _) = inr triv


_-ℕ2ℤ_ :     
zero    -ℕ2ℤ zero  = zero
zero    -ℕ2ℤ suc n = - (suc n)
suc n   -ℕ2ℤ zero  = + (suc n)
suc n   -ℕ2ℤ suc m = n  -ℕ2ℤ m 


minusℤ  :    
minusℤ (+ n)  = - n
minusℤ zero   = zero
minusℤ (- n)  = + n

_+ℤ_ :      
z           +ℤ zero        = z
zero        +ℤ z           = z
(+ n)       +ℤ (+ m)       = + (n +ℕ+ m)
(+ (suc n)) +ℤ (- (suc m)) = n -ℕ2ℤ m
(- n)       +ℤ (- m)       = - (n +ℕ+ m)
(- (suc n)) +ℤ (+ (suc m)) = m -ℕ2ℤ n

_*ℤ_ :      
z           *ℤ zero               = zero
zero        *ℤ z                  = zero
(+ (suc n)) *ℤ (+ (suc m)) = + suc (n * m + n + m)
(+ (suc n)) *ℤ (- (suc m)) = - suc (n * m + n + m)
(- (suc n)) *ℤ (+ (suc m)) = - suc (n * m + n + m)
(- (suc n)) *ℤ (- (suc m)) = + suc (n * m + n + m)

_-ℤ_ :      
z -ℤ z' = z +ℤ (minusℤ z')


_*ℤℕ+_ :   ℕ+   
z *ℤℕ+ n = z *ℤ (+ n)

-- temporiliy only for easy

_*m_ :   ℕ+   
z *m z' = z *ℤℕ+ z'

0ℤ  :  
0ℤ  = zero

1ℤ  :  
1ℤ  = + 1ℕ+

2ℤ  :  
2ℤ  = + 2ℕ+

-1ℤ  :  
-1ℤ  = - 1ℕ+

-2ℤ  :  
-2ℤ  = - 2ℕ+