-- -- 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)
--