qsort.agda

{-# OPTIONS --no-termination-check #-}

module qsort where

  _o_ : {a : Set} -> {b : Set} -> {c : Set} -> (b -> c) -> (a -> b) -> a -> c
  f o g = \x -> f (g x)

  data Bool : Set where
    true  : Bool
    false : Bool

  not : Bool -> Bool
  not true  = false
  not false = true

  if_then_else_ : {a : Set} -> Bool -> a -> a -> a
  if true  then x else _ = x
  if false then _ else y = y

  data List (a : Set) : Set where
    nil  : List a
    _::_ : a -> List a -> List a

  listrec : {a : Set} -> List a -> (a -> List a -> List a) -> List a -> List a
  listrec e _  nil    = e
  listrec e b (x :: xs) = b x (listrec e b xs)

  filter : {a : Set} -> (a -> Bool) -> List a -> List a
  filter f = listrec nil (\x ih -> if (f x) then (x :: ih) else ih)

  _++_ : {a : Set} -> List a -> List a -> List a
  nil ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

  data Nat : Set where
    zero : Nat
    succ : Nat -> Nat

  _+_ : Nat -> Nat -> Nat
  zero   + m = m
  succ n + m = succ (n + m)

  _*_ : Nat -> Nat -> Nat
  zero   * m = zero
  succ n * m = m + (n * m)

  one : Nat
  one = succ zero

  fact : Nat -> Nat
  fact  zero    = one
  fact (succ n) = succ n * fact n 

  _<_ : Nat -> Nat -> Bool
  zero     < zero     = false
  zero     < n        = true
  n        < zero     = false
  (succ n) < (succ m) = n < m

  --

  qsort : {a : Set} -> (a -> a -> Bool) -> List a -> List a
  qsort f nil       = nil
  qsort f (x :: xs) = (qsort f (filter (not o (f x)) xs)) ++
                    (x :: (qsort f (filter (f x) xs)))