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