feat(tests/playground/qsort): qsort benchmark

tests/playground/Makefile

@@ -1,7 +1,7 @@
 ## CONFIG
 
 BENCH=ulimit -s unlimited && bench
-CROSS_BENCHES = binarytrees deriv expr_const_folding rbmap rbmap_shared
+CROSS_BENCHES = binarytrees deriv expr_const_folding qsort rbmap rbmap_shared
 
 # basic version usable without Nix
 #CROSS_CATS = .lean .perf.lean .hs .gc.hs .perf.hs .llvm.hs .ml .gc.ml .perf.ml
@@ -65,6 +65,8 @@ bench/%.bench: %.out | bench
 
 bench/binarytrees.%.bench: BENCH_PARAMS = 21
 
+bench/qsort.%.bench: BENCH_PARAMS = 250
+
 bench/rbmap.%.bench: BENCH_PARAMS = 7000000
 
 rbmap_shared.%.out: rbmap_checkpoint.%.out; ln -f $< $@

tests/playground/bench.nix

@@ -5,8 +5,8 @@ let
     (pkgs.callPackage ../../default.nix { inherit stdenv; }).overrideAttrs (attrs: {
       inherit cmakeFlags;
       # pin Lean commit to avoid rebuilds
-      # 2019-05-12
-      src = builtins.fetchGit { url = ../../.; rev = "de5b68f1262214eecf3d59d7540ed0e9447edf7b"; };
+      # 2019-05-16
+      src = builtins.fetchGit { url = ../../.; rev = "7a19f246e6fe2aae21b2f336c435f56712926a33"; };
     });
   # for binarytrees.hs
   ghcPackages = p: [ p.parallel ];

tests/playground/qsort.hs

@@ -0,0 +1,82 @@
+import Control.Monad
+import Control.Monad.ST
+import Data.Array.IArray
+import Data.Array.MArray
+import Data.Array.ST
+import Data.Word
+import System.Environment
+
+type Elem = Word32
+
+badRand :: Elem -> Elem
+badRand seed = seed * 1664525 + 1013904223
+
+mkRandomArray :: Elem -> Int -> Array Int Elem
+mkRandomArray seed n = listArray (0, n-1) $ take n $ iterate badRand seed
+
+checkSortedAux :: Array Int Elem -> Int -> IO ()
+checkSortedAux a i =
+  if i < snd (bounds a) - 1 then do
+    unless (a ! i <= a ! (i+1)) $ error "array is not sorted"
+    checkSortedAux a (i+1)
+  else
+    pure ()
+
+swap :: Int -> Int -> STArray s Int Elem -> ST s ()
+swap i j arr = do
+    x <- readArray arr i
+    y <- readArray arr j
+    writeArray arr i y
+    writeArray arr j x
+
+partitionAux as hi pivot i j =
+  if j < hi then do
+    a <- readArray as j
+    if a < pivot then do
+      swap i j as
+      partitionAux as hi pivot (i+1) (j+1)
+    else
+      partitionAux as hi pivot i (j+1)
+  else do
+    swap i hi as
+    pure i
+
+partition :: STArray s Int Elem -> Int -> Int -> ST s Int
+partition as lo hi = do
+  let mid = (lo + hi) `div` 2
+  amid <- readArray as mid
+  alo <- readArray as lo
+  if amid < alo then swap lo mid as else pure ()
+  ahi <- readArray as hi
+  alo <- readArray as lo
+  if ahi < alo then swap lo hi as else pure ()
+  amid <- readArray as mid
+  ahi <- readArray as hi
+  if amid < ahi then swap mid hi as else pure ()
+  pivot <- readArray as hi
+  partitionAux as hi pivot lo lo
+
+qsortAux as low high =
+  if low < high then do
+    mid <- Main.partition as low high
+    qsortAux as low mid
+    qsortAux as (mid+1) high
+  else pure ()
+
+qsort :: STArray s Int Elem -> ST s ()
+qsort as = do
+  (low, high) <- getBounds as
+  qsortAux as low high
+
+main :: IO ()
+main = do
+  [n] <- getArgs >>= mapM readIO
+  forM_ [0..n-1] $ \_ ->
+    forM_ [0..n-1] $ \i -> do
+      let xs = mkRandomArray (toEnum i) i
+      let xs' = runSTArray (do
+          mxs <- thaw xs
+          qsort mxs
+          pure mxs)
+      --print xs'
+      checkSortedAux xs' 0

tests/playground/qsort.lean

@@ -1,8 +1,13 @@
-def mkRandomArray (max : Nat) : Nat → Array Nat → IO (Array Nat)
-| 0     as := pure as
-| (i+1) as := do a ← IO.rand 0 max, mkRandomArray i (as.push a)
+abbreviation Elem := UInt32
 
-partial def checkSortedAux (a : Array Nat) : Nat → IO Unit
+def badRand (seed : Elem) : Elem :=
+seed * 1664525 + 1013904223
+
+def mkRandomArray : Nat → Elem → Array Elem → Array Elem
+| 0     seed as := as
+| (i+1) seed as := mkRandomArray i (badRand seed) (as.push seed)
+
+partial def checkSortedAux (a : Array Elem) : Nat → IO Unit
 | i :=
   if i < a.size - 1 then do
     unless (a.get i <= a.get (i+1)) $ throw (IO.userError "array is not sorted"),
@@ -10,22 +15,12 @@ partial def checkSortedAux (a : Array Nat) : Nat → IO Unit
   else
     pure ()
 
-def test1 (xs : Array Nat) : IO Unit :=
-do
-let xs := xs.qsort (λ a b, a < b),
-IO.println ("sorted array of size: " ++ toString (xs.size))
-
 def main (xs : List String) : IO Unit :=
 do
-let n    := xs.head.toNat,
-let seed := xs.tail.head.toNat,
-let m    := xs.tail.tail.head.toNat,
-xs ← mkRandomArray m m Array.empty,
-timeit "qsort" (test1 xs),
-IO.setRandSeed seed,
+let n := xs.head.toNat,
 n.mfor $ λ _,
 n.mfor $ λ i, do
-  xs ← mkRandomArray (i*2) i Array.empty,
+  let xs := mkRandomArray i (UInt32.ofNat i) Array.empty,
   let xs := xs.qsort (λ a b, a < b),
-  IO.println xs,
+  --IO.println xs,
   checkSortedAux xs 0

tests/playground/qsort.ml

@@ -0,0 +1,65 @@
+type elem = int32
+
+let badRand (seed : elem) : elem = Int32.add (Int32.mul seed 1664525l) 1013904223l
+
+let mkRandomArray (seed : elem) n =
+  let s = ref seed in
+  Array.init n (fun _ ->
+    let seed = !s in
+    s := badRand seed;
+    seed)
+
+exception Unsorted of string
+
+let rec checkSortedAux (a : elem array) i =
+  if i < Array.length a - 1 then begin
+    if a.(i) > a.(i+1) then raise (Unsorted "array is not sorted");
+    checkSortedAux a (i+1)
+  end
+
+let swap arr i j =
+  let x = arr.(i) in
+  let y = arr.(j) in
+  arr.(i) <- y;
+  arr.(j) <- x
+
+let rec partitionAux hi pivot arr i j : int =
+  if j < hi then
+    if arr.(j) < pivot then begin
+      swap arr i j;
+      partitionAux hi pivot arr (i+1) (j+1)
+    end else
+      partitionAux hi pivot arr i (j+1)
+  else begin
+    swap arr i hi;
+    i
+  end
+
+let partition arr lo hi =
+  let mid = (lo + hi) / 2 in
+  if arr.(mid) < arr.(lo) then swap arr lo mid;
+  if arr.(hi)  < arr.(lo) then swap arr lo hi ;
+  if arr.(mid) < arr.(hi) then swap arr mid hi;
+  let pivot = arr.(hi) in
+  partitionAux hi pivot arr lo lo
+
+let rec qsortAux arr low high =
+  if low < high then
+    let mid = partition arr low high in
+    qsortAux arr low mid;
+    qsortAux arr (mid+1) high
+  else ()
+
+let qsort arr =
+  qsortAux arr 0 (Array.length arr - 1)
+
+let main n =
+  for _ = 0 to n-1 do
+    for i = 0 to n-1 do
+      let xs = mkRandomArray (Int32.of_int i) i in
+      qsort xs;
+      checkSortedAux xs 0
+    done
+  done;;
+
+main (int_of_string Sys.argv.(1))