1open HolKernel boolLib bossLib BasicProvers; 2open pred_setTheory arithmeticTheory listTheory rich_listTheory optionTheory 3 pairTheory relationTheory sortingTheory; 4open permLib; 5 6val _ = new_theory "mergesort"; 7 8val _ = temp_tight_equality (); 9 10val every_case_tac = BasicProvers.EVERY_CASE_TAC; 11 12val last_reverse = Q.prove ( 13`!l. l <> [] ==> LAST (REVERSE l) = HD l`, 14 Induct_on `l` >> 15 srw_tac[][]); 16 17val mem_sorted_append = Q.prove ( 18`!R l1 l2 x y. 19 transitive R /\ 20 SORTED R (l1 ++ l2) /\ 21 MEM x l1 /\ 22 MEM y l2 23 ==> 24 R x y`, 25 Induct_on `l1` >> 26 srw_tac[][] >> 27 REV_FULL_SIMP_TAC (srw_ss()) [SORTED_EQ] >> 28 metis_tac []); 29 30val stable_def = Define ` 31stable R l1 l2 = 32 !p. (!x y. p x /\ p y ==> R x y) ==> FILTER p l1 = FILTER p l2`; 33 34val sort2_def = Define ` 35sort2 R x y = 36 if R x y then 37 [x;y] 38 else 39 [y;x]`; 40 41val sort3_def = Define ` 42sort3 R x y z = 43 if R x y then 44 if R y z then 45 [x;y;z] 46 else if R x z then 47 [x;z;y] 48 else 49 [z;x;y] 50 else if R y z then 51 if R x z then 52 [y;x;z] 53 else 54 [y;z;x] 55 else 56 [z;y;x]`; 57 58Definition merge_def: 59 (merge R [] [] = []) /\ 60 (merge R l [] = l) /\ 61 (merge R [] l = l) /\ 62 (merge R (x::l1) (y::l2) = 63 if R x y then 64 x::merge R l1 (y::l2) 65 else 66 y::merge R (x::l1) l2) 67End 68 69Definition mergesortN_def: 70 (mergesortN R 0 l = []) /\ 71 (mergesortN R 1 (x::l) = [x]) /\ 72 (mergesortN R 1 [] = []) /\ 73 (mergesortN R 2 (x::y::l) = sort2 R x y) /\ 74 (mergesortN R 2 [x] = [x]) /\ 75 (mergesortN R 2 [] = []) /\ 76 (mergesortN R 3 (x::y::z::l) = sort3 R x y z) /\ 77 (mergesortN R 3 [x;y] = sort2 R x y) /\ 78 (mergesortN R 3 [x] = [x]) /\ 79 (mergesortN R 3 [] = []) /\ 80 (mergesortN R n l = 81 let len1 = DIV2 n in 82 merge R 83 (mergesortN R (DIV2 n) l) 84 (mergesortN R (n - len1) (DROP len1 l))) 85Termination 86 WF_REL_TAC `measure (��(R,n,l). n)` >> 87 srw_tac[][DIV2_def, X_LT_DIV] 88 >- (match_mp_tac DIV_LESS >> 89 decide_tac) >> 90 decide_tac 91End 92 93val mergesort_def = Define ` 94mergesort R l = mergesortN R (LENGTH l) l`; 95 96(* A mergesort using tail recursive merging. This is what OCaml's standard 97 * library does, but instead of parameterizing with negate, it just copies the 98 * code for merge_rev sort. *) 99 100val sort2_tail_def = Define ` 101sort2_tail (neg:bool) R x y = 102 if R x y <> neg then 103 [x;y] 104 else 105 [y;x]`; 106 107val sort3_tail_def = Define ` 108sort3_tail (neg:bool) R x y z = 109 if R x y <> neg then 110 if R y z <> neg then 111 [x;y;z] 112 else if R x z <> neg then 113 [x;z;y] 114 else 115 [z;x;y] 116 else if R y z <> neg then 117 if R x z <> neg then 118 [y;x;z] 119 else 120 [y;z;x] 121 else 122 [z;y;x]`; 123 124Definition merge_tail_def: 125 (merge_tail (negate:bool) R [] [] acc = acc) /\ 126 (merge_tail negate R l [] acc = REV l acc) /\ 127 (merge_tail negate R [] l acc = REV l acc) /\ 128 (merge_tail negate R (x::l1) (y::l2) acc = 129 if R x y <> negate then 130 merge_tail negate R l1 (y::l2) (x::acc) 131 else 132 merge_tail negate R (x::l1) l2 (y::acc)) 133End 134 135Definition mergesortN_tail_def: 136 (mergesortN_tail (negate :bool) R 0 l = []) /\ 137 (mergesortN_tail negate R 1 (x::l) = [x]) /\ 138 (mergesortN_tail negate R 1 [] = []) /\ 139 (mergesortN_tail negate R 2 (x::y::l) = sort2_tail negate R x y) /\ 140 (mergesortN_tail negate R 2 [x] = [x]) /\ 141 (mergesortN_tail negate R 2 [] = []) /\ 142 (mergesortN_tail negate R 3 (x::y::z::l) = sort3_tail negate R x y z) /\ 143 (mergesortN_tail negate R 3 [x;y] = sort2_tail negate R x y) /\ 144 (mergesortN_tail negate R 3 [x] = [x]) /\ 145 (mergesortN_tail negate R 3 [] = []) /\ 146 (mergesortN_tail negate R n l = 147 let len1 = DIV2 n in 148 let neg = ~negate in 149 merge_tail neg R (mergesortN_tail neg R (DIV2 n) l) 150 (mergesortN_tail neg R (n - len1) (DROP len1 l)) 151 []) 152Termination 153 WF_REL_TAC `measure (��(neg,R,n,l). n)` >> 154 srw_tac[][DIV2_def] >> 155 srw_tac[][DIV2_def, X_LT_DIV] 156 >- (match_mp_tac DIV_LESS >> decide_tac) >> 157 decide_tac 158End 159 160val mergesort_tail_def = Define ` 161mergesort_tail R l = mergesortN_tail F R (LENGTH l) l`; 162 163 164(* ------------------------- proofs ----------------------- *) 165 166(* mergesort permutes its input *) 167 168val sort2_perm = Q.store_thm ("sort2_perm", 169`!R x y. PERM [x;y] (sort2 R x y)`, 170 srw_tac [PERM_ss] [sort2_def]); 171 172val sort3_perm = Q.store_thm ("sort3_perm", 173`!R x y z. PERM [x;y;z] (sort3 R x y z)`, 174 srw_tac [PERM_ss] [sort3_def]); 175 176val merge_perm = Q.store_thm ("merge_perm", 177`!R l1 l2. PERM (l1++l2) (merge R l1 l2)`, 178 ho_match_mp_tac merge_ind >> 179 srw_tac[][merge_def] >> 180 full_simp_tac (srw_ss()++PERM_ss) []); 181 182val mergesortN_perm = Q.store_thm ("mergesortN_perm", 183`!R n l. PERM (TAKE n l) (mergesortN R n l)`, 184 ho_match_mp_tac mergesortN_ind >> 185 srw_tac[][] >> 186 ONCE_REWRITE_TAC [mergesortN_def] >> 187 srw_tac[][sort2_perm, sort3_perm] 188 >- (every_case_tac >> 189 fs []) 190 >- (every_case_tac >> 191 fs [sort2_perm] >> 192 metis_tac []) 193 >- (every_case_tac >> 194 fs [sort2_perm, sort3_perm] >> 195 metis_tac []) >> 196 `len1 <= n` 197 by (UNABBREV_ALL_TAC >> 198 fs [DIV2_def, DIV_LESS_EQ]) >> 199 metis_tac [take_drop_partition, PERM_TRANS, PERM_CONG, merge_perm]); 200 201val mergesort_perm = Q.store_thm ("mergesort_perm", 202`!R l. PERM l (mergesort R l)`, 203 srw_tac[][mergesort_def] >> 204 metis_tac [TAKE_LENGTH_ID, mergesortN_perm]); 205 206(* mergesort's output is sorted *) 207 208val sort2_sorted = Q.store_thm ("sort2_sorted", 209`!R x y. 210 total R 211 ==> 212 SORTED R (sort2 R x y)`, 213 srw_tac[][sort2_def, SORTED_DEF, total_def] >> 214 metis_tac []); 215 216val sort3_sorted = Q.store_thm ("sort3_sorted", 217`!R x y z. 218 total R 219 ==> 220 SORTED R (sort3 R x y z)`, 221 srw_tac[][sort3_def, SORTED_DEF, total_def] >> 222 metis_tac []); 223 224val merge_sorted = Q.store_thm ("merge_sorted", 225`!R l1 l2. 226 transitive R /\ total R /\ SORTED R l1 /\ SORTED R l2 227 ==> 228 SORTED R (merge R l1 l2)`, 229 ho_match_mp_tac merge_ind >> 230 srw_tac[][merge_def] >> 231 REV_FULL_SIMP_TAC (srw_ss()) [SORTED_EQ] >> 232 srw_tac[][] >> 233 fs [transitive_def, total_def] 234 >- (`PERM (l1++(y::l2)) (merge R l1 (y::l2))` by metis_tac [merge_perm] >> 235 imp_res_tac MEM_PERM >> 236 fs [] >> 237 metis_tac []) 238 >- (`PERM ((x::l1)++l2) (merge R (x::l1) l2)` by metis_tac [merge_perm] >> 239 imp_res_tac MEM_PERM >> 240 fs [] >> 241 metis_tac [])); 242 243val mergesortN_sorted = Q.store_thm ("mergesortN_sorted", 244`!R n l. 245 total R /\ transitive R 246 ==> 247 SORTED R (mergesortN R n l)`, 248 ho_match_mp_tac mergesortN_ind >> 249 srw_tac[][] >> 250 ONCE_REWRITE_TAC [mergesortN_def] >> 251 srw_tac[][SORTED_EQ, SORTED_DEF, sort2_sorted, sort3_sorted] 252 >- (Cases_on `l` >> 253 srw_tac[][]) 254 >- (Cases_on `l` >> 255 srw_tac[][] >> 256 Cases_on `t` >> 257 srw_tac[][sort2_sorted]) 258 >- (Cases_on `l` >> 259 srw_tac[][] >> 260 Cases_on `t` >> 261 srw_tac[][sort2_sorted] >> 262 Cases_on `t'` >> 263 srw_tac[][sort2_sorted, sort3_sorted]) 264 >- metis_tac [merge_sorted]); 265 266val mergesort_sorted = Q.store_thm ("mergesort_sorted", 267`!R l. transitive R /\ total R ==> SORTED R (mergesort R l)`, 268 metis_tac [mergesort_def, mergesortN_sorted]); 269 270(* mergesort is stable *) 271 272val stable_cong = Q.store_thm ("stable_cong", 273`!R l1 l2 l3 l4. 274 stable R l1 l2 /\ stable R l3 l4 275 ==> 276 stable R (l1++l3) (l2++l4)`, 277 srw_tac[][stable_def, FILTER_APPEND]); 278 279val stable_trans = Q.store_thm ("stable_trans", 280`!R l1 l2 l3. 281 stable R l1 l2 /\ stable R l2 l3 282 ==> 283 stable R l1 l3`, 284 srw_tac[][stable_def]); 285 286val sort2_stable = Q.store_thm ("sort2_stable", 287`!R x y. stable R [x;y] (sort2 R x y)`, 288 srw_tac[][stable_def, sort2_def] >> 289 every_case_tac >> 290 srw_tac[][] >> 291 metis_tac []); 292 293val sort3_stable = Q.store_thm ("sort3_stable", 294`!R x y z. 295 total R /\ transitive R 296 ==> 297 stable R [x;y;z] (sort3 R x y z)`, 298 srw_tac[][sort3_def, stable_def] >> 299 every_case_tac >> 300 srw_tac[][] >> 301 metis_tac [total_def, transitive_def]); 302 303val filter_merge = Q.store_thm ("filter_merge", 304`!P R l1 l2. 305 transitive R /\ 306 (!x y. P x /\ P y ==> R x y) /\ 307 SORTED R l1 308 ==> 309 FILTER P (merge R l1 l2) = FILTER P (l1 ++ l2)`, 310 gen_tac >> 311 ho_match_mp_tac merge_ind >> 312 srw_tac[][merge_def, SORTED_EQ] >> 313 srw_tac[][merge_def, FILTER_APPEND] >> 314 REV_FULL_SIMP_TAC (srw_ss()) [SORTED_EQ, FILTER_APPEND] 315 >- metis_tac [] 316 >- metis_tac [] 317 >- (`FILTER P l1 = []` 318 by (srw_tac[][FILTER_EQ_NIL] >> 319 CCONTR_TAC >> 320 fs [EXISTS_MEM] >> 321 metis_tac [transitive_def]) >> 322 srw_tac[][])); 323 324val merge_stable = Q.store_thm ("merge_stable", 325`!R l1 l2. 326 transitive R /\ 327 SORTED R l1 328 ==> 329 stable R (l1 ++ l2) (merge R l1 l2)`, 330 srw_tac[][stable_def, filter_merge]); 331 332val mergesortN_stable = Q.store_thm ("mergesortN_stable", 333`!R n l. 334 total R /\ transitive R 335 ==> 336 stable R (TAKE n l) (mergesortN R n l)`, 337 ho_match_mp_tac mergesortN_ind >> 338 srw_tac[][] >> 339 ONCE_REWRITE_TAC [mergesortN_def] >> 340 srw_tac[][sort2_stable, sort3_stable] >> 341 TRY (srw_tac[][stable_def] >> NO_TAC) 342 >- (Cases_on `l` >> 343 srw_tac[][stable_def]) 344 >- (Cases_on `l` >> 345 srw_tac[][] >> 346 TRY (srw_tac[][stable_def] >> NO_TAC) >> 347 Cases_on `t` >> 348 srw_tac[][sort2_stable] >> 349 srw_tac[][stable_def]) 350 >- (Cases_on `l` >> 351 srw_tac[][] >> 352 TRY (srw_tac[][stable_def] >> NO_TAC) >> 353 Cases_on `t` >> 354 srw_tac[][sort2_stable] >> 355 TRY (srw_tac[][stable_def] >> NO_TAC) >> 356 Cases_on `t'` >> 357 srw_tac[][sort2_stable, sort3_stable]) 358 >- (`len1 <= n` 359 by (UNABBREV_ALL_TAC >> 360 fs [DIV2_def, DIV_LESS_EQ]) >> 361 metis_tac [stable_cong, merge_stable, take_drop_partition, stable_trans, mergesortN_sorted])); 362 363val mergesort_stable = Q.store_thm ("mergesort_stable", 364`!R l. transitive R /\ total R ==> stable R l (mergesort R l)`, 365 metis_tac [mergesortN_stable, mergesort_def, TAKE_LENGTH_ID]); 366 367(* packaging things up *) 368 369val mergesort_STABLE_SORT = Q.store_thm ("mergesort_STABLE_SORT", 370`!R. transitive R /\ total R ==> STABLE mergesort R`, 371 srw_tac[][STABLE_DEF, SORTS_DEF] >> 372 metis_tac [mergesort_perm, mergesort_sorted, mergesort_stable, stable_def]); 373 374val mergesort_mem = Q.store_thm ("mergesort_mem", 375`!R L x. MEM x (mergesort R L) <=> MEM x L`, 376 metis_tac [mergesort_perm, MEM_PERM]); 377 378(* On to mergesort_tail *) 379 380val sort2_tail_correct = Q.store_thm ("sort2_tail_correct", 381`!neg R x y. 382 sort2_tail neg R x y = if neg then REVERSE (sort2 R x y) else sort2 R x y`, 383 srw_tac[][sort2_def, sort2_tail_def] >> 384 fs []); 385 386val sort3_tail_correct = Q.store_thm ("sort3_tail_correct", 387`!neg R x y z. 388 sort3_tail neg R x y z = if neg then REVERSE (sort3 R x y z) else sort3 R x y z`, 389 srw_tac[][sort3_def, sort3_tail_def] >> 390 fs []); 391 392val merge_tail_correct1 = Q.store_thm ("merge_tail_correct1", 393`!neg R l1 l2 acc. 394 (neg = F) 395 ==> 396 merge_tail neg R l1 l2 acc = REVERSE (merge R l1 l2) ++ acc`, 397 ho_match_mp_tac merge_tail_ind >> 398 srw_tac[][merge_tail_def, merge_def, REV_REVERSE_LEM]); 399 400val merge_empty = Q.store_thm ("merge_empty", 401`!R l acc. 402 merge R l [] = l /\ 403 merge R [] l = l`, 404 Cases_on `l` >> 405 srw_tac[][merge_def]); 406 407val merge_last_lem1 = Q.prove ( 408`!R l1 l2 x. 409 (!y. MEM y l2 ==> ~R x y) 410 ==> 411 merge R (l1 ++ [x]) l2 = merge R l1 l2 ++ [x]`, 412 ho_match_mp_tac merge_ind >> 413 srw_tac[][merge_def, merge_empty] >> 414 Induct_on `v5` >> 415 srw_tac[][merge_empty, merge_def] >> 416 metis_tac []); 417 418val merge_last_lem2 = Q.prove ( 419`!R l1 l2 y. 420 (!x. MEM x l1 ==> R x y) 421 ==> 422 merge R l1 (l2 ++ [y]) = merge R l1 l2 ++ [y]`, 423 ho_match_mp_tac merge_ind >> 424 srw_tac[][merge_def, merge_empty] >> 425 Induct_on `v9` >> 426 srw_tac[][merge_empty, merge_def] >> 427 metis_tac []); 428 429val merge_tail_correct2 = Q.store_thm ("merge_tail_correct2", 430`!neg R l1 l2 acc. 431 (neg = T) /\ 432 transitive R /\ 433 SORTED R (REVERSE l1) /\ 434 SORTED R (REVERSE l2) 435 ==> 436 merge_tail neg R l1 l2 acc = (merge R (REVERSE l1) (REVERSE l2)) ++ acc`, 437 ho_match_mp_tac merge_tail_ind >> 438 srw_tac[][merge_tail_def, merge_def, REV_REVERSE_LEM, merge_empty] >> 439 fs [] >> 440 `SORTED R (REVERSE l1) /\ SORTED R (REVERSE l2)` 441 by metis_tac [SORTED_APPEND_GEN] >> 442 fs [] 443 >- (match_mp_tac (GSYM merge_last_lem1) >> 444 srw_tac[][] >> 445 srw_tac[][] >> 446 CCONTR_TAC >> 447 fs [] >> 448 `R y' y` by metis_tac [mem_sorted_append, MEM_REVERSE, MEM] >> 449 metis_tac [transitive_def]) 450 >- (match_mp_tac (GSYM merge_last_lem2) >> 451 srw_tac[][] >> 452 srw_tac[][] >> 453 `R x' x` by metis_tac [mem_sorted_append, MEM_REVERSE, MEM] >> 454 metis_tac [transitive_def])); 455 456val mergesortN_correct = Q.store_thm ("mergesortN_correct", 457`!negate R n l. 458 total R /\ 459 transitive R 460 ==> 461 mergesortN_tail negate R n l = 462 (if negate then REVERSE (mergesortN R n l) else mergesortN R n l)`, 463 ho_match_mp_tac mergesortN_tail_ind >> 464 srw_tac[][] >> 465 ONCE_REWRITE_TAC [mergesortN_tail_def, mergesortN_def] >> 466 srw_tac[][sort2_tail_correct, sort3_tail_correct] >> 467 fs [] >> 468 every_case_tac >> 469 fs [] >> 470 UNABBREV_ALL_TAC >> 471 srw_tac[][merge_tail_correct1] >> 472 metis_tac [merge_tail_correct2, mergesortN_sorted, REVERSE_REVERSE, APPEND_NIL]); 473 474val mergesort_tail_correct = Q.store_thm ("mergesort_tail_correct", 475`!R l. 476 total R /\ 477 transitive R 478 ==> 479 mergesort_tail R l = mergesort R l`, 480 srw_tac[][mergesort_tail_def, mergesort_def, mergesortN_correct]); 481 482 483 (* 484(* Timings *) 485 486load "intLib"; 487 488val mergesortN'_def = tDefine "mergesortN'" ` 489(mergesortN' R 0 l = []) /\ 490(mergesortN' R 1 (x::l) = [x]) /\ 491(mergesortN' R 1 [] = []) /\ 492(mergesortN' R 2 (x::y::l) = sort2 R x y) /\ 493(mergesortN' R 2 [x] = [x]) /\ 494(mergesortN' R 2 [] = []) /\ 495(mergesortN' R n l = 496 let len1 = DIV2 n in 497 merge R (mergesortN' R (DIV2 n) l) (mergesortN' R (n - len1) (DROP len1 l)))` 498 (WF_REL_TAC `measure (��(R,n,l). n)` >> 499 srw_tac[][DIV2_def] >> 500 COOPER_TAC); 501 502val mergesortN''_def = tDefine "mergesortN''" ` 503(mergesortN'' R 0 l = []) /\ 504(mergesortN'' R 1 (x::l) = [x]) /\ 505(mergesortN'' R 1 [] = []) /\ 506(mergesortN'' R n l = 507 let len1 = DIV2 n in 508 merge R (mergesortN'' R (DIV2 n) l) (mergesortN'' R (n - len1) (DROP len1 l)))` 509 (WF_REL_TAC `measure (��(R,n,l). n)` >> 510 srw_tac[][DIV2_def] >> 511 COOPER_TAC); 512 513val rand_list_def = Define ` 514(rand_list 0 seed = []) /\ 515(rand_list (SUC n) seed = 516 let v = (1664525 * seed + 1013904223) MOD 4294967296 in 517 v::rand_list n v)`; 518 519val l = (time EVAL ``rand_list 10000 353``) |> concl |> rand; 520val len_l = ``10000:num``; 521 522val l' = (time EVAL ``MAP (\x. x MOD 65536) ^l``) |> concl |> rand; 523 524 525time (fn x => (EVAL x; ())) ``LENGTH (COUNT_LIST 10000)``; 526time (fn x => (EVAL x; ())) ``COUNT_LIST 10000``; 527 528time (fn x => (EVAL x; ())) ``mergesortN $<= 10000 (COUNT_LIST 10000)``; 529>runtime: 10.905s, gctime: 0.29495s, systime: 0.06740s. 530time (fn x => (EVAL x; ())) ``mergesortN $<= ^len_l ^l``; 531> runtime: 27.618s, gctime: 1.106s, systime: 0.24801s. 532time (fn x => (EVAL x; ())) ``mergesortN $<= ^len_l ^l'``; 533> runtime: 18.192s, gctime: 0.76859s, systime: 0.16917s. 534 535time (fn x => (EVAL x; ())) ``mergesortN' $<= 10000 (COUNT_LIST 10000)``; 536> runtime: 11.322s, gctime: 0.33336s, systime: 0.07988s 537time (fn x => (EVAL x; ())) ``mergesortN' $<= ^len_l ^l``; 538> runtime: 28.974s, gctime: 1.162s, systime: 0.31028s. 539time (fn x => (EVAL x; ())) ``mergesortN' $<= ^len_l ^l'``; 540> runtime: 18.985s, gctime: 0.94506s, systime: 0.22901s. 541 542time (fn x => (EVAL x; ())) ``mergesortN'' $<= 10000 (COUNT_LIST 10000)``; 543> runtime: 11.977s, gctime: 0.34678s, systime: 0.08751s. 544time (fn => (EVAL x; ())) ``mergesortN'' $<= ^len_l ^l``; 545> runtime: 29.934s, gctime: 1.386s, systime: 0.38797s. 546time (fn x => (EVAL x; ())) ``mergesortN'' $<= ^len_l ^l'``; 547> runtime: 20.251s, gctime: 1.180s, systime: 0.26435s. 548 549time (fn x => (EVAL x; ())) ``mergesort_tail $<= (COUNT_LIST 10000)``; 550> runtime: 13.388s, gctime: 0.59262s, systime: 0.15220s. 551time (fn x => (EVAL x; ())) ``mergesort_tail $<= ^l``; 552> runtime: 30.701s, gctime: 1.878s, systime: 0.68566s. 553time (fn x => (EVAL x; ())) ``mergesort_tail $<= ^l'``; 554> runtime: 20.488s, gctime: 0.64356s, systime: 0.59357s. 555 556time (fn x => (EVAL x; ())) ``QSORT3 $<= (COUNT_LIST 500)``; 557> runtime: 31.436s, gctime: 0.97548s, systime: 0.23698s. 558time (fn x => (EVAL x; ())) ``QSORT3 $<= ^l``; 559> runtime: 1m23s, gctime: 6.614s, systime: 2.108s. 560time (fn x => (EVAL x; ())) ``QSORT3 $<= ^l'``; 561> runtime: 55.361s, gctime: 5.010s, systime: 2.373s. 562 563time (fn x => (EVAL x; ())) ``QSORT $<= (COUNT_LIST 500)``; 564> runtime: 10.795s, gctime: 0.80040s, systime: 0.11975s. 565time (fn x => (EVAL x; ())) ``QSORT $<= ^l``; 566> runtime: 33.837s, gctime: 1.495s, systime: 0.33714s. 567time (fn x => (EVAL x; ())) ``QSORT $<= ^l'``; 568> runtime: 21.398s, gctime: 1.040s, systime: 0.22661s. 569 570*) 571 572val _ = export_theory (); 573