1(* 2load "bossLib"; 3load "computeLib"; 4*) 5open bossLib computeLib; 6 7 8val thms = ref ([] : thm list); 9fun add_thm thm = thms := thm :: (!thms); 10 11fun Define_rw q = 12 let val thm = bossLib.Define q 13 in add_thm thm; thm end 14; 15 16val le_nat_def = Define_rw 17 ` (le_nat 0 n = T) 18/\ (le_nat (SUC k) 0 = F) 19/\ (le_nat (SUC k) (SUC l) = le_nat k l) ` 20; 21 22val append_def = Define_rw 23 ` (append [] l2 = l2) 24/\ (append (x :: l1) l2 = x :: (append l1 l2)) ` 25; 26 27val double_def = Define_rw ` double l = append l l ` 28; 29 30val triple_def = Define_rw ` triple l = append l (append l l) ` 31; 32 33(* merge sort *) 34 35val merge_def = Define_rw 36 ` (merge (h1 :: t1) (h2 :: t2) = 37 if le_nat h1 h2 then h1 :: merge t1 (h2 :: t2) 38 else h2 :: merge (h1 :: t1) t2) 39/\ (merge [] l2 = l2) 40/\ (merge l1 [] = l1) ` 41; 42 43 44val _ = Hol_datatype ` arbin = 45 Lf 46 | Nd of num => arbin => arbin ` 47; 48 49val Tree2List_def = Define_rw 50 ` (Tree2List Lf = []) 51/\ (Tree2List (Nd n a1 a2) = n :: merge (Tree2List a1) (Tree2List a2)) ` 52; 53 54val insTree_def = Define_rw 55 ` (insTree Lf n = Nd n Lf Lf) 56/\ (insTree (Nd m a1 a2) n = 57 if (le_nat n m) then Nd n a2 (insTree a1 m) 58 else Nd m a2 (insTree a1 n)) ` 59; 60 61val List2Tree_def = Define_rw 62` (List2Tree [] = Lf) 63/\ (List2Tree (n :: ns) = insTree (List2Tree ns) n) ` 64; 65 66val merge_sort_def = Define_rw 67 ` merge_sort l = Tree2List (List2Tree l) ` 68; 69 70 71 72(* Example *) 73val n1 = --`SUC 0 `--; 74val n2 = --`SUC ^n1 `--; 75val n3 = --`SUC ^n2 `--; 76val n4 = --`SUC ^n3 `--; 77 78val l0 = --`[] : num list`--; 79 80fun app_l4 l = --` ^n2 :: 0 :: ^n1 :: 0 :: ^l `--; 81 82fun app_l20 l = 83 --` ^n2 :: 0 :: ^n1 :: 0 :: ^n1 :: ^n3 :: ^n4 :: 84 ^n1 :: 0 :: ^n1 :: ^n3 :: 0 :: ^n1 :: ^n3 :: 85 ^n4 :: ^n2 :: 0 :: ^n1 :: 0 :: ^n1 :: ^l `-- 86; 87 88 89val L2_def = Define_rw ` L2 = [ ^n2; 0] `; 90val L4_def = Define_rw ` L4 = ^(app_l4 l0) `; 91val L8_def = Define_rw ` L8 = ^(funpow 2 app_l4 l0) `; 92val L12_def = Define_rw ` L12 = ^(funpow 3 app_l4 l0) `; 93val L16_def = Define_rw ` L16 = ^(funpow 4 app_l4 l0) `; 94val L20'_def = Define_rw ` L20' = ^(funpow 5 app_l4 l0) `; 95val L40'_def = Define_rw ` L40' = double L20' `; 96val L80'_def = Define_rw ` L80' = double L40'`; 97 98 99val L20_def = Define_rw ` L20 = ^(app_l20 l0) `; 100val L40_def = Define_rw ` L40 = double L20`; 101val L100_def = Define_rw ` L100 = ^(funpow 5 app_l20 l0) `; 102val L200_def = Define_rw ` L200 = double L100 `; 103val L400_def = Define_rw ` L400 = double L200 `; 104val L1200_def = Define_rw ` L1200 = triple L400 `; 105val L2400_def = Define_rw ` L2400 = double L1200 `; 106val L4800_def = Define_rw ` L4800 = double L2400 `; 107val L9600_def = Define_rw ` L9600 = double L4800 `; 108val L19200_def = Define_rw ` L19200 = double L9600 `; 109val L38400_def = Define_rw ` L38400 = double L19200 `; 110 111 112(* Save the useful thms *) 113val sort_thms = rev (!thms); 114 115val rws = reduceLib.reduce_rws(); 116val _ = add_thms sort_thms rws; 117 118fun norm q = time (CBV_CONV rws) (--q--); 119(* 120fun norm q = timing.with_stats (timing.tickt "total" (CBV_CONV rws)) (--q--); 121*) 122 123(* rules.sml implemented witout expl. subst.: quadratic 124 * Ln | time on sprat 125 * --------+----------------- 126 * L4 | ~ 0.03s 127 * L12 | ~ 0.11s 128 * L20 | ~ 0.30s 129 * L40 | ~ 0.89s 130 * L100 | ~ 3.5s 131 * L200 | ~ 11.7s = 3300 times slower than Moscow ML 132 * L1200 | ~ 377s 133 *) 134 135(* with expl. subst.: N.log N *) 136norm ` merge_sort L12 `; (* ~ 0.09s *) 137norm ` merge_sort L20 `; (* ~ 0.24s *) 138norm ` merge_sort L100 `; (* ~ 2.04s *) 139norm ` merge_sort L200 `; (* ~ 4.9s *) 140norm ` merge_sort L400 `; (* ~ 11.4s *) 141val _ = norm ` merge_sort L1200 `; (* ~ 41.6s / MosML: 0.043s --> 990 *) 142val _ = norm ` merge_sort L19200 `; (* ~ 996s / --> 634 *) 143val _ = norm ` merge_sort L38400 `; (* ~ 2090s, 66Mo / MosML: 4.3s --> 490 *) 144 145 146(* Comparison with REWRITE_CONV: exponential *) 147 148fun rw_norm q = time (REWRITE_CONV sort_thms) (--q--); 149 150rw_norm `merge_sort L4`; (* ~ 0.06s *) 151rw_norm `merge_sort L12`; (* ~ 3.4s *) 152rw_norm `merge_sort L20`; (* ~ 15mn *) 153 154(* And SIMP_CONV *) 155open simpLib; 156 157val srws = flatten (map BODY_CONJUNCTS (COND_CLAUSES :: sort_thms)); 158 159fun simp_norm q = time (SIMP_CONV empty_ss srws) (--q--); 160 161simp_norm `merge_sort L12`; (* ~ 5s *) 162