-- <PRE>
-- This code written by James Hook
-- This file should work with Omega version 1.1
-- released May 23, 2005
-- See http://www.cs.pdx.edu/~sheard/Omega/index.html

{-- These are predefined by the compiler
kind Nat = Z | S Nat

data Nat' n
  = Z where n = Z
  | forall m . S (Nat' m) where n = S m
-}


data LE a b
  = LeBase where a = b
  | ex c . LeStep (LE a c) where b = S c

reflLE :: LE a a
reflLE = LeBase

transLE :: (LE a b) -> (LE b c) -> (LE a c)
transLE p LeBase = p
transLE p (LeStep q) = LeStep (transLE p q)

compare :: Nat' a -> Nat' b -> ((LE a b)+(LE b a))
compare Z Z = L LeBase
compare Z (S x) =
  case compare Z x of L w -> L (LeStep w)
compare (S x) Z =
  case compare Z x of L w -> R (LeStep w)
compare (S x) (S y) = mapP g g (compare x y )
  where mapP f g (L x) = L(f x)
        mapP f g (R x) = R(g x)
        g :: LE x y -> LE (S x) (S y)
        g LeBase = LeBase
        g (LeStep x) = LeStep (g x)

data MonoList min max
  = MonoNil (LE min max)
  | forall n a . MonoCons (Nat' n) (LE a n) (LE n max) (MonoList min a)

appMonoList :: MonoList b c -> MonoList a b -> MonoList a c
appMonoList (MonoNil bc) (MonoNil ab) =
      MonoNil (transLE ab bc)
appMonoList (MonoNil bc) (MonoCons n an nb xs) =
      MonoCons n an (transLE nb bc) xs
appMonoList (MonoCons m dm mc ys) xs =
      MonoCons m dm mc (appMonoList ys xs)

singletonMonoList :: Nat' n -> MonoList n n
singletonMonoList n = MonoCons n reflLE reflLE (MonoNil reflLE)

data IntervalList min max
  = ILNil (LE min max)
  | forall x . ILCons (Nat' x) (LE min x) (LE x max) (IntervalList min max)

partition :: Nat' n -> LE a n -> LE n b -> IntervalList a b ->
                     (IntervalList a n, IntervalList n b)
partition x an nb xs = partitionAcc (ILNil an) (ILNil nb) xs
  where partitionAcc ls gs (ILNil ab) = (ls,gs)
        partitionAcc ls gs (ILCons y ay yb ys) =
            case compare y x of
              L yx -> partitionAcc (ILCons y ay yx ls) gs ys
              R xy -> partitionAcc ls (ILCons y xy yb gs) ys

qsort :: IntervalList a b -> MonoList a b
qsort (ILNil ab) = MonoNil ab
qsort (ILCons x ax xb (ILNil ab)) = MonoCons x ax xb (MonoNil reflLE)
qsort (ILCons x ax xb xs) =
     let (less,greater) = partition x ax xb xs
         sortedLess = qsort less
	 sortedGreater = qsort greater
     in appMonoList sortedGreater (appMonoList (singletonMonoList x) sortedLess)

-- </PRE>