module Stdlib.Data.Int.Base;

import Stdlib.Data.Fixity open;

import Stdlib.Data.Nat.Base as Nat;
open Nat using {Nat; zero; suc; sub};

import Stdlib.Data.Bool.Base open;

--- Inductive integers. I.e. whole numbers that can be positive, zero, or negative.
builtin int
type Int :=
  | --- ofNat n represents the integer n
    ofNat Nat
  | --- negSuc n represents the integer -(n + 1)
    negSuc Nat
with
  fromNat : Nat -> Int := ofNat;

  --- Converts an ;Int; to a ;Nat;. If the ;Int; is negative, it returns ;zero;.
  toNat (int : Int) : Nat :=
    case int of
      | ofNat n := n
      | negSuc _ := zero;

  --- Subtraction for ;Nat;s.
  builtin int-sub-nat
  subNat (n m : Nat) : Int :=
    case sub n m of
      | zero := ofNat (Nat.sub m n)
      | suc k := negSuc k;

  syntax operator + additive;

  --- Addition for ;Int;s.
  builtin int-plus
  + : Int -> Int -> Int
    | (ofNat m) (ofNat n) := ofNat (m Nat.+ n)
    | (ofNat m) (negSuc n) := subNat m (suc n)
    | (negSuc m) (ofNat n) := subNat n (suc m)
    | (negSuc m) (negSuc n) := negSuc (suc (m Nat.+ n));

  --- Negation for ;Int;s.
  builtin int-neg
  neg : Int -> Int
    | (ofNat n) := negNat n
    | (negSuc n) := ofNat (suc n);

  syntax operator * multiplicative;

  --- Multiplication for ;Int;s.
  builtin int-mul
  * : Int -> Int -> Int
    | (ofNat m) (ofNat n) := ofNat (m Nat.* n)
    | (ofNat m) (negSuc n) := negNat (m Nat.* suc n)
    | (negSuc m) (ofNat n) := negNat (suc m Nat.* n)
    | (negSuc m) (negSuc n) := ofNat (suc m Nat.* suc n);

  syntax operator - additive;

  --- Subtraction for ;Int;s.
  builtin int-sub
  - (n m : Int) : Int := m + neg n;

  --- Division for ;Int;s.
  builtin int-div
  div : Int -> Int -> Int
    | (ofNat m) (ofNat n) := ofNat (Nat.div m n)
    | (ofNat m) (negSuc n) := negNat (Nat.div m (suc n))
    | (negSuc m) (ofNat n) := negNat (Nat.div (suc m) n)
    | (negSuc m) (negSuc n) := ofNat (Nat.div (suc m) (suc n));

  --- Modulo for ;Int;s.
  builtin int-mod
  mod : Int -> Int -> Int
    | (ofNat m) (ofNat n) := ofNat (Nat.mod m n)
    | (ofNat m) (negSuc n) := ofNat (Nat.mod m (suc n))
    | (negSuc m) (ofNat n) := negNat (Nat.mod (suc m) n)
    | (negSuc m) (negSuc n) := negNat (Nat.mod (suc m) (suc n));

  --- Absolute value
  abs (int : Int) : Nat :=
    case int of
      | ofNat n := n
      | negSuc n := suc n;

  --- Non-negative predicate for ;Int;s.
  builtin int-nonneg
  nonNeg : Int -> Bool
    | (ofNat n) := true
    | (negSuc _) := false;

  --- Negation for ;Nat;s.
  builtin int-neg-nat
  negNat : Nat -> Int
    | zero := ofNat zero
    | (suc n) := negSuc n;
end;