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


-- Existenial hiding and operators on anonymous sums

data Covert t = exists x . Hide (t x)

mapP :: (a -> b) -> (c -> d) -> (a+c) -> (b+d)
mapP f g (L x) = L(f x)
mapP f g (R x) = R(g x)

unP ::  (a+a) -> a
unP (L x) = x
unP (R x) = x

map f [] = []
map f (x:xs) = f x : map f xs

-----------------------------------------
-- singleton Nats and Less-than-equal (LE)

{- Predefined by the compiler
kind Nat = Z | S Nat

data Nat' x
  = Z where x=Z
  | exist m . S (Nat' m) where x=S m
-}


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

g :: LE x y -> LE (S x) (S y)
g LeBase = LeBase
g (LeStep x) = LeStep(g x)

trans :: LE a b -> LE b c -> LE a c
trans LeBase LeBase = LeBase
trans (x@(LeStep z)) LeBase = x
trans LeBase (y@(LeStep z)) = y
trans (a@(LeStep x)) (LeStep y) = LeStep(trans a y)


magnitude :: Nat' a -> LE Z a
magnitude Z = LeBase
magnitude (S x) = LeStep(magnitude x)


-------------------------------------------------
-- Sorted Sequence data

data SSeq n
   = Snil where n = Z
   | ex m . Scons (Nat' n) (LE m n) (SSeq m)

--------------------------------------------------
-- insertion sort

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 g :: LE x y -> LE (S x) (S y)
        g LeBase = LeBase
        g (LeStep x) = LeStep(g x)


insert :: Nat' a -> SSeq b -> ((SSeq a)+(SSeq b))
insert z Snil = L(Scons z (magnitude z) Snil)
insert x (xs@(Scons y p zs)) =
   case compare x y of
     R q -> L(Scons x q xs)
     L q -> case insert x zs of
              L (mm) -> R(Scons y q mm)
              R (mm) -> R(Scons y p mm)

sort :: [Covert Nat'] -> Covert SSeq
sort [] = Hide Snil
sort ((Hide x):xs) =
     case insert x ys of {L w -> Hide w; R w -> Hide w}
   where (Hide ys) = sort xs

toNat :: Int -> Covert Nat'
toNat 0 = Hide Z
toNat n = case toNat (n-1) of Hide b -> Hide(S b)

test :: Nat' x -> Nat' y -> Maybe (Equal x y)
test Z Z = Just Eq
test (S x) (S y) = case (test x y) of { Just Eq -> Just Eq; Nothing -> Nothing}
test _ _ = Nothing

test2 :: [Int] -> Covert SSeq
test2 xs = sort(map toNat xs)

x23 = test2 [0,3,1]

----------------------------------------------------
-- merge sort

merge :: SSeq n -> SSeq m -> (SSeq n + SSeq m)
merge Snil ys = R ys
merge xs Snil = L xs
merge (a@(Scons x px xs)) (b@(Scons y py ys)) =
  case compare x y of
    L p -> case merge a ys of
             L ws -> R(Scons y p ws)
             R ws -> R(Scons y py ws)
    R p -> case merge b xs of
             L ws -> L(Scons x p ws)
             R ws -> L(Scons x px ws)

merge2 :: SSeq u -> SSeq v -> Covert SSeq
merge2 x y = unP (mapP Hide Hide (merge x y))

split [] pair = pair
split [x] (xs,ys) = (x:xs,ys)
split (x:y:zs) (xs,ys) = split zs (x:xs,y:ys)

msort :: [Covert Nat'] -> Covert SSeq
msort [] = Hide Snil
msort [Hide x] = Hide(Scons x (magnitude x) Snil)
msort xs = merge2 ys zs
  where (y,z) = split xs ([],[])
        (Hide ys) = msort y
        (Hide zs) = msort z

--