ComparisonChain.idr

module ComparisonChain

%access public export

infixl 6 |==|, |/=|
infixl 6 |<|, |<=|, |>=|, |>|

namespace Interfaces
  interface ChainEq ty where
    (|==|) : ty -> ty -> Bool

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

  interface ChainEq ty => ChainOrd ty where
      compareC : ty -> ty -> Ordering

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

      (|>|) : ty -> ty -> Bool
      (|>|) x y with (compareC 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

      maxC : ty -> ty -> ty
      maxC x y = if x |>| y then x else y

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

  implementation Eq ty => ChainEq ty where
    (|==|) = (==)
    (|/=|) = (/=)

  implementation Ord ty => ChainOrd ty where
      compareC = compare
      (|<|) = (<)
      (|<=|) = (<=)
      (|>=|) = (>=)
      (|>|) = (>)
      maxC = max
      minC = min


namespace Chain
  data ComparisonChain : (ty : Type) -> Type where
    CmpSuccess : (next : ty) -> ComparisonChain ty
    CmpFailure : ComparisonChain ty

  -- it would be nice if this could be implicit...
  chain : ComparisonChain ty -> Bool
  chain (CmpSuccess _) = True
  chain CmpFailure = False

  implicit
  fromValue : ty -> ComparisonChain ty
  fromValue x = CmpSuccess x

  Cast ty (ComparisonChain ty) where
    cast = fromValue

  chainWith : (op : ty -> ty -> Bool) -> %static ComparisonChain ty -> Lazy ty -> ComparisonChain ty
  chainWith _ CmpFailure _ = CmpFailure
  chainWith op (CmpSuccess x) y with (op x y)
    chainWith op (CmpSuccess x) y | True = CmpSuccess y
    chainWith op (CmpSuccess x) y | False = CmpFailure

  (|==|) : ChainEq ty => ComparisonChain ty -> Lazy ty -> ComparisonChain ty
  (|==|) = chainWith (|==|)

  (|/=|) : ChainEq ty => ComparisonChain ty -> Lazy ty -> ComparisonChain ty
  (|/=|) = chainWith (|/=|)

  (|<|) : ChainOrd ty => ComparisonChain ty -> Lazy ty -> ComparisonChain ty
  (|<|) = chainWith (|<|)

  (|<=|) : ChainOrd ty => ComparisonChain ty -> Lazy ty -> ComparisonChain ty
  (|<=|) = chainWith (|<=|)

  (|>=|) : ChainOrd ty => ComparisonChain ty -> Lazy ty -> ComparisonChain ty
  (|>=|) = chainWith (|>=|)

  (|>|) : ChainOrd ty => ComparisonChain ty -> Lazy ty -> ComparisonChain ty
  (|>|) = chainWith (|>|)


-- a couple tests
test1223 : Bool
test1223 = chain (1.0 |<| 2.0 |==| 2.0 |<=| 3.0)

test252 : Bool
test252 = chain (2.0 |<=| 5.0 |<| 2.0)

test9a7b8 : (a, b : Double) -> Bool
test9a7b8 a b = chain (9.0 |/=| a |>=| 7.0 |<| b |/=| 8.0)