Interfaces.idr

module Prelude.Interfaces

import Builtins
import Prelude.Basics
import Prelude.Bool

%access public export

-- Numerical Operator Precedence
infix 6 ==, /=, <, <=, >, >=
infixl 7 <<, >> -- unused
infixl 8 +, -
infixl 9 *, /

infixl 9 `div`, `mod`

-- ------------------------------------------------------------- [ Boolean Ops ]
intToBool : Int -> Bool
intToBool 0 = False
intToBool x = True

boolOp : (a -> a -> Int) -> a -> a -> Bool
boolOp op x y = intToBool (op x y)

-- ---------------------------------------------------------- [ Equality Interface ]
||| The Eq interface defines inequality and equality.
interface Eq ty where
    (==) : ty -> ty -> Bool
    (/=) : ty -> ty -> Bool

    x /= y = not (x == y)
    x == y = not (x /= y)

Eq () where
  () == () = True

Eq Int where
    (==) = boolOp prim__eqInt

Eq Integer where
    (==) = boolOp prim__eqBigInt

Eq Double where
    (==) = boolOp prim__eqFloat

Eq Char where
    (==) = boolOp prim__eqChar

Eq String where
    (==) = boolOp prim__eqString

Eq Ptr where
    (==) = boolOp prim__eqPtr

Eq ManagedPtr where
    (==) = boolOp prim__eqManagedPtr

Eq Bool where
    True  == True  = True
    True  == False = False
    False == True  = False
    False == False = True

(Eq a, Eq b) => Eq (a, b) where
  (==) (a, c) (b, d) = (a == b) && (c == d)


-- ---------------------------------------------------------- [ Ordering Interface ]
data Ordering = LT | EQ | GT

Eq Ordering where
    LT == LT = True
    EQ == EQ = True
    GT == GT = True
    _  == _  = False

||| Compose two comparisons into the lexicographic product
thenCompare : Ordering -> Lazy Ordering -> Ordering
thenCompare LT y = LT
thenCompare EQ y = y
thenCompare GT y = GT

||| The Ord interface defines comparison operations on ordered data types.
interface Eq ty => Ord ty where
    compare : ty -> ty -> Ordering

    (<) : ty -> ty -> Bool
    (<) x y with (compare x y)
        (<) x y | LT = True
        (<) x y | _  = False

    (>) : ty -> ty -> Bool
    (>) x y with (compare x y)
        (>) x y | GT = True
        (>) x y | _  = False

    (<=) : ty -> ty -> Bool
    (<=) x y = x < y || x == y

    (>=) : ty -> ty -> Bool
    (>=) x y = x > y || x == y

    max : ty -> ty -> ty
    max x y = if x > y then x else y

    min : ty -> ty -> ty
    min x y = if (x < y) then x else y

Ord () where
    compare () () = EQ

Ord Int where
    compare x y = if (x == y) then EQ else
                  if (boolOp prim__sltInt x y) then LT else
                  GT


Ord Integer where
    compare x y = if (x == y) then EQ else
                  if (boolOp prim__sltBigInt x y) then LT else
                  GT


Ord Double where
    compare x y = if (x == y) then EQ else
                  if (boolOp prim__sltFloat x y) then LT else
                  GT


Ord Char where
    compare x y = if (x == y) then EQ else
                  if (boolOp prim__sltChar x y) then LT else
                  GT


Ord String where
    compare x y = if (x == y) then EQ else
                  if (boolOp prim__ltString x y) then LT else
                  GT


Ord Bool where
    compare True True = EQ
    compare False False = EQ
    compare False True = LT
    compare True False = GT


(Ord a, Ord b) => Ord (a, b) where
  compare (xl, xr) (yl, yr) =
    if xl /= yl
      then compare xl yl
      else compare xr yr

-- --------------------------------------------------------- [ Numerical Interface ]
||| The Num interface defines basic numerical arithmetic.
interface Num ty where
    (+) : ty -> ty -> ty
    (*) : ty -> ty -> ty
    ||| Conversion from Integer.
    fromInteger : Integer -> ty

Num Integer where
    (+) = prim__addBigInt
    (*) = prim__mulBigInt

    fromInteger = id

Num Int where
    (+) = prim__addInt
    (*) = prim__mulInt

    fromInteger = prim__truncBigInt_Int


Num Double where
    (+) = prim__addFloat
    (*) = prim__mulFloat

    fromInteger = prim__toFloatBigInt

Num Bits8 where
  (+) = prim__addB8
  (*) = prim__mulB8
  fromInteger = prim__truncBigInt_B8

Num Bits16 where
  (+) = prim__addB16
  (*) = prim__mulB16
  fromInteger = prim__truncBigInt_B16

Num Bits32 where
  (+) = prim__addB32
  (*) = prim__mulB32
  fromInteger = prim__truncBigInt_B32

Num Bits64 where
  (+) = prim__addB64
  (*) = prim__mulB64
  fromInteger = prim__truncBigInt_B64

-- --------------------------------------------------------- [ Negatable Interface ]
||| The `Neg` interface defines operations on numbers which can be negative.
interface Num ty => Neg ty where
    ||| The underlying of unary minus. `-5` desugars to `negate (fromInteger 5)`.
    negate : ty -> ty
    (-) : ty -> ty -> ty


Neg Integer where
    negate x = prim__subBigInt 0 x
    (-) = prim__subBigInt

Neg Int where
    negate x = prim__subInt 0 x
    (-) = prim__subInt

Neg Double where
    negate x = prim__negFloat x
    (-) = prim__subFloat

-- ---------------------------------------------------- [ Absolute Value Interface ]
||| Numbers for which the absolute value is defined should implement `Abs`.
interface Num ty => Abs ty where
    ||| Absolute value
    abs : ty -> ty

Abs Integer where
    abs x = if x < 0 then -x else x

Abs Int where
    abs x = if x < (prim__truncBigInt_Int 0) then -x else x

Abs Double where
    abs x = if x < (prim__toFloatBigInt 0) then -x else x

-- ------------------------------------------------------------
Eq Bits8 where
  x == y = intToBool (prim__eqB8 x y)

Eq Bits16 where
  x == y = intToBool (prim__eqB16 x y)

Eq Bits32 where
  x == y = intToBool (prim__eqB32 x y)

Eq Bits64 where
  x == y = intToBool (prim__eqB64 x y)

Ord Bits8 where
  (<) = boolOp prim__ltB8
  (>) = boolOp prim__gtB8
  (<=) = boolOp prim__lteB8
  (>=) = boolOp prim__gteB8
  compare l r = if l < r then LT
                else if l > r then GT
                     else EQ

Ord Bits16 where
  (<) = boolOp prim__ltB16
  (>) = boolOp prim__gtB16
  (<=) = boolOp prim__lteB16
  (>=) = boolOp prim__gteB16
  compare l r = if l < r then LT
                else if l > r then GT
                     else EQ

Ord Bits32 where
  (<) = boolOp prim__ltB32
  (>) = boolOp prim__gtB32
  (<=) = boolOp prim__lteB32
  (>=) = boolOp prim__gteB32
  compare l r = if l < r then LT
                else if l > r then GT
                     else EQ

Ord Bits64 where
  (<) = boolOp prim__ltB64
  (>) = boolOp prim__gtB64
  (<=) = boolOp prim__lteB64
  (>=) = boolOp prim__gteB64
  compare l r = if l < r then LT
                else if l > r then GT
                     else EQ

-- ------------------------------------------------------------- [ Bounded ]

interface Ord b => MinBound b where
  ||| The lower bound for the type
  minBound : b

interface Ord b => MaxBound b where
  ||| The upper bound for the type
  maxBound : b

MinBound Bits8 where
  minBound = 0x0

MaxBound Bits8 where
  maxBound = 0xff

MinBound Bits16 where
  minBound = 0x0

MaxBound Bits16 where
  maxBound = 0xffff

MinBound Bits32 where
  minBound = 0x0

MaxBound Bits32 where
  maxBound = 0xffffffff

MinBound Bits64 where
  minBound = 0x0

MaxBound Bits64 where
  maxBound = 0xffffffffffffffff


-- ------------------------------------------------------------- [ Fractionals ]

interface Num ty => Fractional ty where
  (/) : ty -> ty -> ty
  recip : ty -> ty

  recip x = 1 / x

Fractional Double where
  (/) = prim__divFloat

-- --------------------------------------------------------------- [ Integrals ]
%default partial

interface Num ty => Integral ty where
   div : ty -> ty -> ty
   mod : ty -> ty -> ty

-- ---------------------------------------------------------------- [ Integers ]
divBigInt : Integer -> Integer -> Integer
divBigInt x y = case y == 0 of
  False => prim__sdivBigInt x y

modBigInt : Integer -> Integer -> Integer
modBigInt x y = case y == 0 of
  False => prim__sremBigInt x y

Integral Integer where
  div = divBigInt
  mod = modBigInt

-- --------------------------------------------------------------------- [ Int ]

divInt : Int -> Int -> Int
divInt x y = case y == 0 of
  False => prim__sdivInt x y

modInt : Int -> Int -> Int
modInt x y = case y == 0 of
  False => prim__sremInt x y

Integral Int where
  div = divInt
  mod = modInt

-- ------------------------------------------------------------------- [ Bits8 ]
divB8 : Bits8 -> Bits8 -> Bits8
divB8 x y = case y == 0 of
  False => prim__udivB8 x y

modB8 : Bits8 -> Bits8 -> Bits8
modB8 x y = case y == 0 of
  False => prim__uremB8 x y

Integral Bits8 where
  div = divB8
  mod = modB8

-- ------------------------------------------------------------------ [ Bits16 ]
divB16 : Bits16 -> Bits16 -> Bits16
divB16 x y = case y == 0 of
  False => prim__udivB16 x y

modB16 : Bits16 -> Bits16 -> Bits16
modB16 x y = case y == 0 of
  False => prim__uremB16 x y

Integral Bits16 where
  div = divB16
  mod = modB16

-- ------------------------------------------------------------------ [ Bits32 ]
divB32 : Bits32 -> Bits32 -> Bits32
divB32 x y = case y == 0 of
  False => prim__udivB32 x y

modB32 : Bits32 -> Bits32 -> Bits32
modB32 x y = case y == 0 of
  False => prim__uremB32 x y

Integral Bits32 where
  div = divB32
  mod = modB32

-- ------------------------------------------------------------------ [ Bits64 ]
divB64 : Bits64 -> Bits64 -> Bits64
divB64 x y = case y == 0 of
  False => prim__udivB64 x y

modB64 : Bits64 -> Bits64 -> Bits64
modB64 x y = case y == 0 of
  False => prim__uremB64 x y

Integral Bits64 where
  div = divB64
  mod = modB64