load "nat.quox"

namespace int {

def0 Sign : ★ = {pos, neg-succ}
def0 ℤ : ★ = Sign × ℕ

def from-ℕ : ℕ → ℤ = λ n ⇒ ('pos, n)

def neg-ℕ : ℕ → ℤ =
  λ n ⇒ case n return ℤ of { 0 ⇒ ('pos, 0); succ n ⇒ ('neg-succ, n) }

def zeroℤ : ℤ = ('pos, 0)


def match : 0.(A : ★) → ω.(pos neg : ℕ → A) → ℤ → A =
  λ A pos neg x ⇒
    case x return A of { (s, x) ⇒
      case s return A of { 'pos ⇒ pos x; 'neg-succ ⇒ neg x }
    }

def negate : ℤ → ℤ =
  match ℤ neg-ℕ (λ x ⇒ from-ℕ (succ x))

def minus-ℕ-ℕ : ℕ → ℕ → ℤ =
  λ m n ⇒
    letω f : ω.ℕ → ω.ℕ → ℤ = λ m n ⇒
      bool.if ℤ (nat.ge m n) (from-ℕ (nat.minus m n))
                             (neg-ℕ (nat.minus n m)) in
    getω ℤ (app2ω ℕ ℕ ℤ f (nat.dup m) (nat.dup n))

def plus-ℕ : ℤ → ℕ → ℤ =
  match (ℕ → ℤ) (λ x n ⇒ from-ℕ (nat.plus x n))
                (λ x n ⇒ minus-ℕ-ℕ n (succ x))

def minus-ℕ : ℤ → ℕ → ℤ =
  match (ℕ → ℤ) minus-ℕ-ℕ (λ x n ⇒ ('neg-succ, nat.plus x n))


def plus : ℤ → ℤ → ℤ =
  match (ℤ → ℤ) (λ x y ⇒ plus-ℕ y x) (λ x y ⇒ minus-ℕ y (succ x))

def minus : ℤ → ℤ → ℤ = λ x y ⇒ plus x (negate y)


def dup-sign : Sign → [ω. Sign] =
  λ s ⇒ case s return [ω. Sign] of {
    'pos      ⇒ ['pos];
    'neg-succ ⇒ ['neg-succ]
  }

def0 dup-sign-ok : (s : Sign) → dup-sign s ≡ [s] : [ω. Sign] =
  λ s ⇒ case s return s' ⇒ dup-sign s' ≡ [s'] : [ω. Sign] of {
    'pos      ⇒ δ 𝑖 ⇒ ['pos];
    'neg-succ ⇒ δ 𝑖 ⇒ ['neg-succ]
  }

def dup : ℤ → [ω.ℤ] =
  λ x ⇒ case x return [ω.ℤ] of { (s, n) ⇒
    app2ω Sign ℕ ℤ (λ s n ⇒ (s, n)) (dup-sign s) (nat.dup n)
  }

def0 dup-ok : (x : ℤ) → dup x ≡ [x] : [ω.ℤ] =
  λ x ⇒
  case x return x' ⇒ dup x' ≡ [x'] : [ω.ℤ] of { (s, n) ⇒ δ 𝑖 ⇒
    app2ω Sign ℕ ℤ (λ s n ⇒ (s, n)) (dup-sign-ok s @𝑖) (nat.dup-ok n @𝑖)
  }


def times-ℕ : ℤ → ℕ → ℤ =
  match (ℕ → ℤ)
    (λ m  n ⇒ from-ℕ (nat.times m n))
    (λ m' n ⇒ neg-ℕ (nat.times (succ m') n))

def times : ℤ → ℤ → ℤ =
  match (ℤ → ℤ) (λ p x ⇒ times-ℕ x p) (λ n x ⇒ negate (times-ℕ x (succ n)))


def abs : ℤ → ℕ = match ℕ (λ p ⇒ p) (λ n ⇒ succ n)


def pair-eq? : 0.(A B : ★) → ω.(DecEq A) → ω.(DecEq B) → DecEq (A × B) =
  λ A B eqA? eqB? x y ⇒
    let0 Ret : ★ = x ≡ y : (A × B) in
    letω a0 = fst x; a1 = fst y;
         b0 = snd x; b1 = snd y in
    dec.elim (a0 ≡ a1 : A) (λ _ ⇒ Dec Ret)
      (λ ya ⇒
        dec.elim (b0 ≡ b1 : B) (λ _ ⇒ Dec Ret)
          (λ yb ⇒ Yes Ret (δ 𝑖 ⇒ (ya @𝑖, yb @𝑖)))
          (λ nb ⇒ No  Ret (λ eq ⇒ nb (δ 𝑖 ⇒ snd (eq @𝑖))))
          (eqB? b0 b1))
      (λ na ⇒ No Ret (λ eq ⇒ na (δ 𝑖 ⇒ fst (eq @𝑖))))
      (eqA? a0 a1)


def sign-eq? : DecEq Sign =
  λ x y ⇒
    let0 disc : Sign → ★ =
      λ s ⇒ case s return ★ of { 'pos ⇒ True; 'neg-succ ⇒ False } in
  case x return x' ⇒ Dec (x' ≡ y : Sign) of {
    'pos ⇒
      case y return y' ⇒ Dec ('pos ≡ y' : Sign) of {
        'pos ⇒ dec.yes-refl Sign 'pos;
        'neg-succ ⇒
          No ('pos ≡ 'neg-succ : Sign)
             (λ eq ⇒ coe (𝑖 ⇒ disc (eq @𝑖)) 'true)
      };
    'neg-succ ⇒
      case y return y' ⇒ Dec ('neg-succ ≡ y' : Sign) of {
        'neg-succ ⇒ dec.yes-refl Sign 'neg-succ;
        'pos ⇒
          No ('neg-succ ≡ 'pos : Sign)
             (λ eq ⇒ coe (𝑖 ⇒ disc (eq @𝑖)) @1 @0 'true)
      }
  }

#[compile-scheme "(lambda% (x y) (if (equal? x y) Yes No))"]
def eq? : DecEq ℤ = pair-eq? Sign ℕ sign-eq? nat.eq?

def eq : ω.ℤ → ω.ℤ → Bool =
  λ x y ⇒ dec.bool (x ≡ y : ℤ) (eq? x y)

}

def0 ℤ = int.ℤ


namespace scheme-int {
  postulate0 Int : ★

  #[compile-scheme "(lambda (x) x)"]
  postulate from-ℕ : ℕ → Int

  #[compile-scheme "(lambda% (x y) (+ x y))"]
  postulate plus : Int → Int → Int

  #[compile-scheme "(lambda% (x y) (- x y))"]
  postulate minus : Int → Int → Int

  #[compile-scheme "(lambda% (x y) (* x y))"]
  postulate times : Int → Int → Int

  #[compile-scheme "(lambda% (x y) (if (= x y) 'true 'false))"]
  postulate eq : Int → Int → Bool

  #[compile-scheme "abs"]
  postulate abs : Int → ℕ
}