module Stdlib.Data.Int;

import Stdlib.Data.Int.Base open hiding {+; -; *; div; mod} public;
-- should be re-exported qualified
import Stdlib.Data.Int.Base as Int;

import Stdlib.Data.String open;
import Stdlib.Data.Bool open;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Natural open;
import Stdlib.Trait.FromNatural open;
import Stdlib.Trait.Integral open;
import Stdlib.Trait.DivMod open;

-- should be re-exported qualified
import Stdlib.Data.Int.Ord as Int;

--- Converts an ;Int; into ;String;.
builtin int-to-string
axiom intToString : Int -> String;

{-# specialize: true, inline: case #-}
instance
eqIntI : Eq Int := mkEq (Int.==);

{-# specialize: true, inline: case #-}
instance
ordIntI : Ord Int := mkOrd Int.compare;

instance
showIntI : Show Int := mkShow intToString;

{-# specialize: true, inline: case #-}
instance
fromNaturalIntI : FromNatural Int :=
  mkFromNatural@{
    fromNat := ofNat;
  };

{-# specialize: true, inline: case #-}
instance
naturalIntI : Natural Int :=
  mkNatural@{
    + := (Int.+);
    * := (Int.*);
  };

{-# specialize: true, inline: case #-}
instance
integralIntI : Integral Int :=
  mkIntegral@{
    naturalI := naturalIntI;
    - := (Int.-);
    fromInt (x : Int) : Int := x;
  };

{-# specialize: true, inline: case #-}
instance
divModIntI : DivMod Int :=
  mkDivMod@{
    div := Int.div;
    mod := Int.mod;
  };