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