132 lines
1.4 KiB
Text
132 lines
1.4 KiB
Text
data List a where
|
|
Nil : List a
|
|
Cons : a -> List a -> List a
|
|
|
|
main = printList (quicksort (mkDescList 1000 0))
|
|
|
|
mkDescList : Int -> Int -> List Int
|
|
mkDescList from to = case from == to of
|
|
True => Nil
|
|
False => Cons from (mkDescList (from - 1) to)
|
|
|
|
quicksort : List Int -> List Int
|
|
quicksort xs = case xs of
|
|
Nil => Nil
|
|
Cons a as => let smaller = quicksort (filter (\y. y < a) xs) in
|
|
let bigger = quicksort (filter (\y. a < y) xs) in
|
|
smaller ++ (Cons a bigger)
|
|
|
|
filter : (a -> Bool) -> List a -> List a
|
|
filter p xs = case xs of
|
|
Nil => Nil
|
|
Cons x xs => case p x of
|
|
True => Cons x (filter p xs)
|
|
False => filter p xs
|
|
|
|
.++ : List a -> List a -> List a
|
|
.++ list1 list2 = case list1 of
|
|
Nil => list2
|
|
Cons x xs => Cons x (xs ++ list2)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
printListH : List Int -> Unit
|
|
printListH xs = case xs of
|
|
Cons a as => flipConst (printInt a) (printListHH as)
|
|
Nil => Unit
|
|
|
|
printListHH : List Int -> Unit
|
|
printListHH xs = case xs of
|
|
Nil => Unit
|
|
Cons a as => flipConst (printChar ',') (flipConst (printInt a) (printListHH as))
|
|
|
|
printList : List Int -> Unit
|
|
printList xs = case Cons (printChar '[') (Cons (printListH xs) (Cons (printChar ']') Nil)) of
|
|
_ => Unit
|
|
|
|
flipConst x y = y
|
|
|
|
|
|
printInt : Int -> Unit
|
|
printInt xs = Unit
|
|
|
|
printChar : Char -> Unit
|
|
printChar = \x. Unit
|
|
|
|
data Unit where
|
|
Unit : Unit
|