-- Define the integers as a HIT by identifying +0 and -0
{-# OPTIONS --safe #-}
module Cubical.Data.Int.MoreInts.QuoInt.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Univalence

open import Cubical.Relation.Nullary

open import Cubical.Data.Int using ()
  renaming (ℤ to Int ; discreteℤ to discreteInt ; isSetℤ to isSetInt ; 0≢1-ℤ to 0≢1-Int)
open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
open import Cubical.Data.Bool as Bool using (Bool; not; notnot)

variable
  l : Level


Sign : Type₀
Sign = Bool

pattern spos = Bool.false
pattern sneg = Bool.true

_·S_ : Sign → Sign → Sign
_·S_ = Bool._⊕_


data ℤ : Type₀ where
  signed : (s : Sign) (n : ℕ) → ℤ
  posneg : signed spos  ≡ signed sneg 

pattern pos n = signed spos n
pattern neg n = signed sneg n


sign : ℤ → Sign
sign (signed _ zero) = spos
sign (signed s (suc _)) = s
sign (posneg i) = spos

sign-pos : ∀ n → sign (pos n) ≡ spos
sign-pos zero = refl
sign-pos (suc n) = refl

abs : ℤ → ℕ
abs (signed _ n) = n
abs (posneg i) = zero

signed-inv : ∀ n → signed (sign n) (abs n) ≡ n
signed-inv (pos zero) = refl
signed-inv (neg zero) = posneg
signed-inv (signed s (suc n)) = refl
signed-inv (posneg i) j = posneg (i ∧ j)

signed-zero : ∀ s₁ s₂ → signed s₁ zero ≡ signed s₂ zero
signed-zero spos spos = refl
signed-zero sneg sneg = refl
signed-zero spos sneg = posneg
signed-zero sneg spos = sym posneg


rec : ∀ {A : Type l} → (pos' neg' : ℕ → A) → pos'  ≡ neg'  → ℤ → A
rec pos' neg' eq (pos m)    = pos' m
rec pos' neg' eq (neg m)    = neg' m
rec pos' neg' eq (posneg i) = eq i

elim : ∀ (P : ℤ → Type l)
       → (pos' : ∀ n → P (pos n))
       → (negsuc' : ∀ n → P (neg (suc n)))
       → ∀ z → P z
elim P pos' negsuc' (pos n) = pos' n
elim P pos' negsuc' (neg zero) = subst P posneg (pos' zero)
elim P pos' negsuc' (neg (suc n)) = negsuc' n
elim P pos' negsuc' (posneg i) = subst-filler P posneg (pos' zero) i


Int→ℤ : Int → ℤ
Int→ℤ (Int.pos n) = pos n
Int→ℤ (Int.negsuc n) = neg (suc n)

ℤ→Int : ℤ → Int
ℤ→Int (pos n) = Int.pos n
ℤ→Int (neg zero) = Int.pos 
ℤ→Int (neg (suc n)) = Int.negsuc n
ℤ→Int (posneg _) = Int.pos 

ℤ→Int→ℤ : ∀ (n : ℤ) → Int→ℤ (ℤ→Int n) ≡ n
ℤ→Int→ℤ (pos n) _       = pos n
ℤ→Int→ℤ (neg zero) i    = posneg i
ℤ→Int→ℤ (neg (suc n)) _ = neg (suc n)
ℤ→Int→ℤ (posneg j) i    = posneg (j ∧ i)

Int→ℤ→Int : ∀ (n : Int) → ℤ→Int (Int→ℤ n) ≡ n
Int→ℤ→Int (Int.pos n) _ = Int.pos n
Int→ℤ→Int (Int.negsuc n) _ = Int.negsuc n

isoIntℤ : Iso Int ℤ
isoIntℤ = iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int

Int≡ℤ : Int ≡ ℤ
Int≡ℤ = isoToPath isoIntℤ

discreteℤ : Discrete ℤ
discreteℤ = subst Discrete Int≡ℤ discreteInt

isSetℤ : isSet ℤ
isSetℤ = subst isSet Int≡ℤ isSetInt


-_ : ℤ → ℤ
- signed s n = signed (not s) n
- posneg i   = posneg (~ i)

negate-invol : ∀ n → - - n ≡ n
negate-invol (signed s n) i = signed (notnot s i) n
negate-invol (posneg i)   _ = posneg i

negateEquiv : ℤ ≃ ℤ
negateEquiv = isoToEquiv (iso -_ -_ negate-invol negate-invol)

negateEq : ℤ ≡ ℤ
negateEq = ua negateEquiv


infixl  _+_
infixl  _·_

sucℤ : ℤ → ℤ
sucℤ (pos n)       = pos (suc n)
sucℤ (neg zero)    = pos 
sucℤ (neg (suc n)) = neg n
sucℤ (posneg _)    = pos 

predℤ : ℤ → ℤ
predℤ = subst (λ Z → (Z → Z)) negateEq sucℤ
  -- definitionally equal to λ n → - (sucℤ (- n))
  -- strictly more useful than the direct pattern matching version,
  --  see negateSuc and negatePred

sucPredℤ : ∀ n → sucℤ (predℤ n) ≡ n
sucPredℤ (pos zero)    = sym posneg
sucPredℤ (pos (suc _)) = refl
sucPredℤ (neg _)       = refl
sucPredℤ (posneg i) j  = posneg (i ∨ ~ j)

predSucℤ : ∀ n → predℤ (sucℤ n) ≡ n
predSucℤ (pos _)       = refl
predSucℤ (neg zero)    = posneg
predSucℤ (neg (suc _)) = refl
predSucℤ (posneg i) j  = posneg (i ∧ j)

_+_ : ℤ → ℤ → ℤ
(signed _ zero) + n = n
(posneg _)      + n = n
(pos (suc m))   + n = sucℤ  (pos m + n)
(neg (suc m))   + n = predℤ (neg m + n)


sucPathℤ : ℤ ≡ ℤ
sucPathℤ  = isoToPath (iso sucℤ predℤ sucPredℤ predSucℤ)

-- We do the same trick as in Cubical.Data.Int to prove that addition
-- is an equivalence
addEqℤ : ℕ → ℤ ≡ ℤ
addEqℤ zero    = refl
addEqℤ (suc n) = addEqℤ n ∙ sucPathℤ

predPathℤ : ℤ ≡ ℤ
predPathℤ = isoToPath (iso predℤ sucℤ predSucℤ sucPredℤ)

subEqℤ : ℕ → ℤ ≡ ℤ
subEqℤ zero    = refl
subEqℤ (suc n) = subEqℤ n ∙ predPathℤ

addℤ : ℤ → ℤ → ℤ
addℤ (pos m) n    = transport (addEqℤ m) n
addℤ (neg m) n    = transport (subEqℤ m) n
addℤ (posneg _) n = n

isEquivAddℤ : (m : ℤ) → isEquiv (addℤ m)
isEquivAddℤ (pos n)    = isEquivTransport (addEqℤ n)
isEquivAddℤ (neg n)    = isEquivTransport (subEqℤ n)
isEquivAddℤ (posneg _) = isEquivTransport refl

addℤ≡+ℤ : addℤ ≡ _+_
addℤ≡+ℤ i  (pos (suc m)) n = sucℤ   (addℤ≡+ℤ i (pos m) n)
addℤ≡+ℤ i  (neg (suc m)) n = predℤ  (addℤ≡+ℤ i (neg m) n)
addℤ≡+ℤ i  (pos zero) n    = n
addℤ≡+ℤ i  (neg zero) n    = n
addℤ≡+ℤ _  (posneg _) n    = n

isEquiv+ℤ : (m : ℤ) → isEquiv (m +_)
isEquiv+ℤ = subst (λ _+_ → (m : ℤ) → isEquiv (m +_)) addℤ≡+ℤ isEquivAddℤ


_·_ : ℤ → ℤ → ℤ
m · n = signed (sign m ·S sign n) (abs m ℕ.· abs n)

private
  ·-abs : ∀ m n → abs (m · n) ≡ abs m ℕ.· abs n
  ·-abs m n = refl


-- Natural number and negative integer literals for ℤ

open import Cubical.Data.Nat.Literals public

instance
  fromNatℤ : HasFromNat ℤ
  fromNatℤ = record { Constraint = λ _ → Unit ; fromNat = λ n → pos n }

instance
  fromNegℤ : HasFromNeg ℤ
  fromNegℤ = record { Constraint = λ _ → Unit ; fromNeg = λ n → neg n }


-- ℤ is non-trivial

0≢1-ℤ : ¬  ≡ 
0≢1-ℤ p = 0≢1-Int (cong ℤ→Int p)