1open HolKernel Parse boolLib testutils
2
3local
4val sorteval = let
5  val cs = listLib.list_compset()
6  val _ = pairLib.add_pair_compset cs;
7  val _ = sortingLib.add_sorting_compset cs;
8in
9  computeLib.CBV_CONV cs
10end
11val sort = ``QSORT $<``
12
13fun sorttest ns =
14    let
15      fun mk xs =
16          listSyntax.mk_list(map (numSyntax.mk_numeral o Arbnum.fromInt) xs,
17                             numSyntax.num)
18    in
19      convtest("QSORT $< [" ^ String.concatWith "," (map Int.toString ns) ^ "]",
20               sorteval, mk_comb(sort, mk ns),
21               mk (Listsort.sort Int.compare ns))
22    end
23in
24
25val _ = List.app sorttest [
26      [], [1], [10,2,101,4,5],
27      List.tabulate(20, fn n => n),
28      List.rev (List.tabulate(20, fn n => n)),
29      Random.rangelist (0,100) (20, Random.newgen())
30    ]
31end
32