module Haskell.Prim.Ord where

open import Haskell.Prim
open import Haskell.Prim.Eq
open import Haskell.Prim.Bool
open import Haskell.Prim.Int
open import Haskell.Prim.Word
open import Haskell.Prim.Integer
open import Haskell.Prim.Double
open import Haskell.Prim.Tuple
open import Haskell.Prim.Monoid
open import Haskell.Prim.List
open import Haskell.Prim.Maybe
open import Haskell.Prim.Either

--------------------------------------------------
-- Ordering

data Ordering : Set where
  LT EQ GT : Ordering

instance
  iEqOrdering : Eq Ordering
  iEqOrdering ._==_ LT LT = True
  iEqOrdering ._==_ EQ EQ = True
  iEqOrdering ._==_ GT GT = True
  iEqOrdering ._==_ _  _  = False

  iSemigroupOrdering : Semigroup Ordering
  iSemigroupOrdering ._<>_ LT _ = LT
  iSemigroupOrdering ._<>_ EQ o = o
  iSemigroupOrdering ._<>_ GT _ = GT

  iMonoidOrdering : Monoid Ordering
  iMonoidOrdering = record {DefaultMonoid (record {mempty = EQ})}

--------------------------------------------------
-- Ord

record Ord (a : Set) : Set where
  field
    compare : a → a → Ordering
    _<_  : a → a → Bool
    _>_  : a → a → Bool
    _>=_ : a → a → Bool
    _<=_ : a → a → Bool
    max  : a → a → a
    min  : a → a → a
    overlap ⦃ super ⦄ : Eq a

  infix  _<_ _>_ _<=_ _>=_

open Ord ⦃...⦄ public

{-# COMPILE AGDA2HS Ord existing-class #-}

ordFromCompare : ⦃ Eq a ⦄ → (a → a → Ordering) → Ord a
ordFromCompare cmp .compare = cmp
ordFromCompare cmp ._<_  x y = cmp x y == LT
ordFromCompare cmp ._>_  x y = cmp x y == GT
ordFromCompare cmp ._<=_ x y = cmp x y /= GT
ordFromCompare cmp ._>=_ x y = cmp x y /= LT
ordFromCompare cmp .max  x y = if cmp x y == LT then y else x
ordFromCompare cmp .min  x y = if cmp x y == GT then y else x

ordFromLessThan : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a
ordFromLessThan _<_ .compare x y = if x < y then LT else if x == y then EQ else GT
ordFromLessThan _<_ ._<_  x y = x < y
ordFromLessThan _<_ ._>_  x y = y < x
ordFromLessThan _<_ ._<=_ x y = x < y || x == y
ordFromLessThan _<_ ._>=_ x y = y < x || x == y
ordFromLessThan _<_ .max  x y = if x < y then y else x
ordFromLessThan _<_ .min  x y = if y < x then y else x

ordFromLessEq : ⦃ Eq a ⦄ → (a → a → Bool) → Ord a
ordFromLessEq _<=_ .compare x y = if x == y then EQ else if x <= y then LT else GT
ordFromLessEq _<=_ ._<_  x y = x <= y && not (x == y)
ordFromLessEq _<=_ ._>_  x y = y <= x && not (x == y)
ordFromLessEq _<=_ ._<=_ x y = x <= y
ordFromLessEq _<=_ ._>=_ x y = y <= x
ordFromLessEq _<=_ .max  x y = if y <= x then x else y
ordFromLessEq _<=_ .min  x y = if x <= y then x else y

private
  compareFromLt : ⦃ Eq a ⦄ → (a → a → Bool) → a → a → Ordering
  compareFromLt _<_ x y = if x < y then LT else if x == y then EQ else GT

private
  maxNat : Nat → Nat → Nat
  maxNat zero    y       = y
  maxNat (suc x) zero    = suc x
  maxNat (suc x) (suc y) = suc (maxNat x y)

  minNat : Nat → Nat → Nat
  minNat zero    y       = zero
  minNat (suc x) zero    = zero
  minNat (suc x) (suc y) = suc (minNat x y)

instance
  iOrdNat : Ord Nat
  iOrdNat = record (ordFromLessThan ltNat)
    { max = maxNat
    ; min = minNat
    }

  iOrdInteger : Ord Integer
  iOrdInteger = ordFromLessThan ltInteger

  iOrdInt : Ord Int
  iOrdInt = ordFromLessThan ltInt

  iOrdWord : Ord Word
  iOrdWord = ordFromLessThan ltWord

  iOrdDouble : Ord Double
  iOrdDouble = ordFromLessThan primFloatLess

  iOrdChar : Ord Char
  iOrdChar = ordFromLessThan λ x y → c2n x < c2n y

  iOrdBool : Ord Bool
  iOrdBool = ordFromCompare λ where
    False True  → LT
    True  False → GT
    _     _     → EQ

  iOrdUnit : Ord ⊤
  iOrdUnit = ordFromCompare λ _ _ → EQ

  iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b)
  iOrdTuple₂ = ordFromCompare λ where
    (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂

  iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c)
  iOrdTuple₃ = ordFromCompare λ where
    (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂

compareList : ⦃ Ord a ⦄ → List a → List a → Ordering
compareList []       []       = EQ
compareList []       (_ ∷ _)  = LT
compareList (_ ∷ _)  []       = GT
compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys

instance
  iOrdList : ⦃ Ord a ⦄ → Ord (List a)
  iOrdList = ordFromCompare compareList

  iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a)
  iOrdMaybe = ordFromCompare λ where
    Nothing  Nothing  → EQ
    Nothing  (Just _) → LT
    (Just _) Nothing  → GT
    (Just x) (Just y) → compare x y

  iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b)
  iOrdEither = ordFromCompare λ where
    (Left  x) (Left  y) → compare x y
    (Left  _) (Right _) → LT
    (Right _) (Left  _) → GT
    (Right x) (Right y) → compare x y

  iOrdOrdering : Ord Ordering
  iOrdOrdering = ordFromCompare λ where
    LT LT → EQ
    LT _  → LT
    _  LT → GT
    EQ EQ → EQ
    EQ GT → LT
    GT EQ → GT
    GT GT → EQ