module Stdlib.Data.Int.Ord;

import Stdlib.Data.Fixity open;

import Stdlib.Data.Int.Base open;
import Stdlib.Data.Bool.Base open;
import Stdlib.Trait.Ord open using {Equal; LessThan; GreaterThan; Ordering};

import Stdlib.Data.Nat.Base as Nat;
import Stdlib.Data.Nat.Ord as Nat;

syntax operator == comparison;

--- Tests for equality.
builtin int-eq
== : Int -> Int -> Bool
  | (ofNat m) (ofNat n) := m Nat.== n
  | (negSuc m) (negSuc n) := m Nat.== n
  | _ _ := false;

syntax operator /= comparison;

--- Tests for inequality.
/= (m n : Int) : Bool := not (m == n);

syntax operator <= comparison;

--- Returns ;true; iff the first element is less than or equal to the second.
builtin int-le
<= (m n : Int) : Bool := nonNeg (n - m);

syntax operator < comparison;

--- Returns ;true; iff the first element is less than the second.
builtin int-lt
< (m n : Int) : Bool := m + ofNat (Nat.suc Nat.zero) <= n;

syntax operator > comparison;

--- Returns ;true; iff the first element is greater than the second.
> (m n : Int) : Bool := n < m;

syntax operator >= comparison;

--- Returns ;true; iff the first element is greater than or equal to the second.
>= (m n : Int) : Bool := n <= m;

--- Tests for ;Ordering;.
{-# inline: true #-}
compare (m n : Int) : Ordering :=
  if 
    | m == n := Equal
    | m < n := LessThan
    | else := GreaterThan;

--- Returns the smallest ;Int;.
min (x y : Int) : Int := ite (x < y) x y;

--- Returns the biggest ;Int;.
max (x y : Int) : Int := ite (x > y) x y;