formal_lp/old/hypermap/list_conversions.hl

   1 needs "../formal_lp/hypermap/list_hypermap_defs.hl";;
   2
   3 #load "unix.cma";;
   4 (*
   5 itlist_conv_univ;;
   6 el_conv;;
   7 *)
   8
   9 let test n f x =
  10   let start = Unix.gettimeofday() in
  11     for i = 1 to n do
  12       let _ = f x in ()
  13     done;
  14     Unix.time() -. start;;
  15
  16
  17
  18 let t_const = `T` and
  19     f_const = `F`;;
  20
  21 let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;
  22
  23
  24
  25 (******************************)
  26
  27 (* HD conversions *)
  28
  29 let HD_A_CONS = prove(`HD (CONS (h:A) t) = h`, REWRITE_TAC[HD]);;
  30
  31 let hd_conv tm =
  32   let h_tm', t_tm = dest_comb(rand tm) in
  33   let h_tm = rand h_tm' in
  34   let list_ty = type_of t_tm in
  35   let ty = type_of h_tm in
  36   let h_var = mk_var("h", ty) in
  37   let t_var = mk_var("t", list_ty) in
  38     INST[h_tm, h_var; t_tm, t_var] (INST_TYPE[ty, aty] HD_A_CONS);;
  39
  40 (*
  41 let tm = `HD [1;2;3;4]`;;
  42 (* 0.072 *)
  43 test 1000 (REWRITE_CONV[HD]) tm;;
  44 (* 0.016 *)
  45 test 1000 hd_conv tm;;
  46 *)
  47
  48
  49
  50
  51
  52
  53
  54
  55 (*******************************)
  56
  57 (* FST, SND conversions *)
  58
  59
  60 let FST' = ISPECL[`x:A`; `y:B`] FST;;
  61 let SND' = ISPECL[`x:A`; `y:B`] SND;;
  62
  63
  64 let fst_conv tm =
  65   let x_tm, y_tm = dest_pair (rand tm) in
  66   let x_ty, y_ty = type_of x_tm, type_of y_tm in
  67   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
  68     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) FST';;
  69
  70 let snd_conv tm =
  71   let x_tm, y_tm = dest_pair (rand tm) in
  72   let x_ty, y_ty = type_of x_tm, type_of y_tm in
  73   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
  74     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) SND';;
  75
  76
  77 (*
  78 let tm = `FST (1,2)`;;
  79 fst_conv tm;;
  80
  81 (* 0.688 *)
  82 test 10000 (REWRITE_CONV[]) tm;;
  83 (* 0.100 *)
  84 test 10000 fst_conv tm;;
  85 *)
  86
  87
  88 (******************************)
  89
  90 (* LENGTH conversions *)
  91
  92 let LENGTH_A_EMPTY = prove(`LENGTH ([]:(A)list) = 0`, REWRITE_TAC[LENGTH]) and
  93     LENGTH_A_CONS = prove(`LENGTH (CONS (h:A) t) = SUC (LENGTH t)`, REWRITE_TAC[LENGTH]);;
  94
  95 let suc_const = `SUC`;;
  96
  97
  98 let length_conv_univ suc_conv tm =
  99   let list_tm = rand tm in
 100   let list_ty = type_of list_tm in
 101   let ty = (hd o snd o dest_type) list_ty in
 102   let inst_t = INST_TYPE[ty, aty] in
 103   let length_empty, length_cons = inst_t LENGTH_A_EMPTY, inst_t LENGTH_A_CONS in
 104   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
 105
 106   let rec length_conv_raw = fun list_tm ->
 107     if (is_comb list_tm) then
 108       let ltm, t_tm = dest_comb list_tm in
 109       let h_tm = rand ltm in
 110       let th0 = INST[h_tm, h_var; t_tm, t_var] length_cons in
 111       let th1' = length_conv_raw t_tm in
 112       let th1 = AP_TERM suc_const th1' in
 113       let th2 = suc_conv (rand(concl th1)) in
 114         TRANS (TRANS th0 th1) th2
 115     else
 116       length_empty in
 117
 118     length_conv_raw list_tm;;
 119
 120
 121 (*
 122 let tm = `LENGTH [&1;&4;&4;&6;&7 * &8]`;;
 123
 124 test 1000 (REWRITE_CONV[LENGTH; ARITH_SUC]) tm;; (* 0.792 *)
 125 test 1000 (length_conv_univ NUM_SUC_CONV) tm;; (* 0.104 *)
 126 *)
 127
 128
 129 (******************************)
 130
 131 (* MEM conversions *)
 132
 133 let MEM_A_EMPTY = prove(`MEM (x:A) [] <=> F`, REWRITE_TAC[MEM]) and
 134     MEM_A_HD = UNDISCH_ALL (prove(`(x = h <=> T) ==> (MEM (x:A) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
 135     MEM_A_TL = UNDISCH_ALL (prove(`(x = h <=> F) ==> (MEM (x:A) (CONS h t) <=> MEM x t)`, SIMP_TAC[MEM]));;
 136
 137
 138
 139
 140 let rec mem_conv_univ eq_conv tm =
 141   let ltm, list_tm = dest_comb tm in
 142   let x_tm = rand ltm in
 143   let ty = type_of x_tm in
 144   let inst_t = INST_TYPE[ty, aty] in
 145   let mem_empty, mem_hd, mem_tl = inst_t MEM_A_EMPTY, inst_t MEM_A_HD, inst_t MEM_A_TL in
 146   let x_var, h_var = mk_var("x", ty), mk_var("h", ty) in
 147   let t_var = mk_var("t", mk_type("list", [ty])) in
 148
 149   let rec mem_conv_raw list_tm =
 150     if (is_comb list_tm) then
 151       let h_tm', t_tm = dest_comb list_tm in
 152       let h_tm = rand h_tm' in
 153       let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
 154         if (rand(concl eq_th) = t_const) then
 155           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_hd in
 156             MY_PROVE_HYP eq_th th0'
 157         else
 158           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_tl in
 159           let th0 = MY_PROVE_HYP eq_th th0' in
 160           let th1 = mem_conv_raw t_tm in
 161             TRANS th0 th1
 162     else
 163       INST[x_tm, x_var] mem_empty in
 164
 165     mem_conv_raw list_tm;;
 166
 167
 168 (*
 169 let tm = `MEM 11 [1;2;3;4;5;6;4;5;6;7;3;4;4;6;8;9;10]`;;
 170 mem_conv_univ (PURE_REWRITE_CONV[ARITH_EQ]) tm;;
 171
 172 test 100 (mem_conv_univ (REWRITE_CONV[ARITH_EQ])) tm;; (* 0.176 *)
 173 test 100 (REWRITE_CONV[MEM; ARITH_EQ]) tm;; (* 0.352 *)
 174 *)
 175
 176
 177 (**********************************)
 178
 179 (* FILTER conversions *)
 180
 181 let FILTER_A_EMPTY = prove(`FILTER (P:A->bool) [] = []`, REWRITE_TAC[FILTER]) and
 182     FILTER_A_HD = UNDISCH_ALL (prove(`(P h <=> T) ==> FILTER (P:A->bool) (CONS h t) = CONS h (FILTER P t)`, SIMP_TAC[FILTER])) and
 183     FILTER_A_TL = UNDISCH_ALL (prove(`(P h <=> F) ==> FILTER (P:A->bool) (CONS h t) = FILTER P t`, SIMP_TAC[FILTER]));;
 184
 185
 186
 187 let filter_conv_univ p_conv tm =
 188   let ltm, list_tm = dest_comb tm in
 189   let p_tm = rand ltm in
 190   let p_ty = type_of p_tm in
 191   let ty = (hd o snd o dest_type) p_ty in
 192   let inst_t = INST_TYPE[ty, aty] in
 193   let filter_empty, filter_hd, filter_tl =
 194     inst_t FILTER_A_EMPTY, inst_t FILTER_A_HD, inst_t FILTER_A_TL in
 195   let p_var = mk_var("P", p_ty) in
 196   let h_var = mk_var("h", ty) in
 197   let t_var = mk_var("t", mk_type("list",[ty])) in
 198
 199   let rec filter_conv_raw = fun list_tm ->
 200     if (is_comb list_tm) then
 201       let ltm, t_tm = dest_comb list_tm in
 202       let h_tm = rand ltm in
 203       let p_th = p_conv (mk_comb(p_tm, h_tm)) in
 204         if (rand(concl p_th) = t_const) then
 205           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_hd in
 206           let th0 = MY_PROVE_HYP p_th th0' in
 207           let ltm = rator(rand(concl th0)) in
 208           let th1 = filter_conv_raw t_tm in
 209             TRANS th0 (AP_TERM ltm th1)
 210         else
 211           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_tl in
 212           let th0 = MY_PROVE_HYP p_th th0' in
 213           let th1 = filter_conv_raw t_tm in
 214             TRANS th0 th1
 215     else
 216       INST[p_tm, p_var] filter_empty in
 217
 218     filter_conv_raw list_tm;;
 219
 220
 221
 222
 223 (*
 224 let tm = `FILTER (\n. n = 2 \/ n = 3) [1;2;3;4;2;3;1]`;;
 225
 226 REWRITE_CONV[FILTER; ARITH_EQ] tm;;
 227 filter_conv_univ (REWRITE_CONV[ARITH_EQ]) tm;;
 228
 229 test 100 (REWRITE_CONV[FILTER; ARITH_EQ]) tm;; (* 7.596 *)
 230 test 100 (filter_conv_univ (REWRITE_CONV[ARITH_EQ])) tm;; (* 0.236 *)
 231 *)
 232
 233 (***************************)
 234
 235 (* FLATTEN conversions *)
 236
 237 let FLATTEN_A_EMPTY = prove(`FLATTEN ([]:((A)list)list) = []`, REWRITE_TAC[FLATTEN; ITLIST; APPEND]) and
 238     FLATTEN_A_CONS_EMPTY = prove(`FLATTEN (CONS ([]:(A)list) tt) = FLATTEN tt`, REWRITE_TAC[FLATTEN; ITLIST; APPEND]) and
 239     FLATTEN_A_CONS_CONS = prove(`FLATTEN (CONS (CONS (h:A) t) tt) = CONS h (FLATTEN (CONS t tt))`, REWRITE_TAC[FLATTEN; ITLIST; APPEND]);;
 240
 241
 242
 243 (* Works for any list of lists *)
 244 let flatten_conv_univ tm =
 245   let list_list_tm = rand tm in
 246   let list_list_ty = type_of list_list_tm in
 247   let list_ty = (hd o snd o dest_type) list_list_ty in
 248   let ty = (hd o snd o dest_type) list_ty in
 249   let inst_t = INST_TYPE[ty, aty] in
 250   let flatten_empty, flatten_cons_empty, flatten_cons_cons =
 251     inst_t FLATTEN_A_EMPTY, inst_t FLATTEN_A_CONS_EMPTY, inst_t FLATTEN_A_CONS_CONS in
 252   let tt_var = mk_var("tt", list_list_ty) in
 253   let t_var = mk_var("t", list_ty) in
 254   let h_var = mk_var("h", ty) in
 255
 256   let rec flatten_conv_raw list_list_tm =
 257     if (is_comb list_list_tm) then
 258       let hh_tm', tt_tm = dest_comb list_list_tm in
 259       let hh_tm = rand hh_tm' in
 260         if (is_comb hh_tm) then
 261           let h_tm', t_tm = dest_comb hh_tm in
 262           let h_tm = rand h_tm' in
 263           let th0 = INST[h_tm, h_var; t_tm, t_var; tt_tm, tt_var] flatten_cons_cons in
 264           let ltm, rtm = dest_comb(rand(concl th0)) in
 265           let th1 = AP_TERM ltm (flatten_conv_raw (rand rtm)) in
 266             TRANS th0 th1
 267         else
 268           let th0 = INST[tt_tm, tt_var] flatten_cons_empty in
 269           let th1 = flatten_conv_raw tt_tm in
 270             TRANS th0 th1
 271     else
 272       flatten_empty in
 273
 274     flatten_conv_raw list_list_tm;;
 275
 276
 277 (*
 278 let tm = `FLATTEN [[1;2;3];[3];[4;5;2;1;6;7]]`;;
 279 flatten_conv_univ tm;;
 280 REWRITE_CONV[FLATTEN; ITLIST; APPEND] tm;;
 281
 282 test 100 (REWRITE_CONV[FLATTEN; ITLIST; APPEND]) tm;; (* 0.348 *)
 283 test 100 (flatten_conv_univ) tm;; (* 0.028 *)
 284 *)
 285
 286
 287 (***************************)
 288
 289 (* MAP conversions *)
 290
 291
 292 let MAP_AB_EMPTY = prove(`MAP (f:A->B) [] = []`, REWRITE_TAC[MAP]) and
 293     MAP_AB_CONS = prove(`MAP (f:A->B) (CONS h t) = CONS (f h) (MAP f t)`, REWRITE_TAC[MAP]);;
 294
 295
 296 let map_conv_univ f_conv tm =
 297   let ltm, list_tm = dest_comb tm in
 298   let ftm = rand ltm in
 299   let ftm_ty = type_of ftm in
 300   let f_var = mk_var("f", ftm_ty) in
 301   let [a_type; b_type] = snd(dest_type ftm_ty) in
 302   let h_var = mk_var("h", a_type) in
 303   let t_var = mk_var("t", mk_type("list", [a_type])) in
 304   let inst_t = INST[ftm, f_var] o INST_TYPE[a_type, aty; b_type, bty] in
 305   let map_empty, map_cons =
 306     inst_t MAP_AB_EMPTY, inst_t MAP_AB_CONS in
 307
 308   let rec map_conv_raw list_tm =
 309     if (is_comb list_tm) then
 310       let h_tm', t_tm = dest_comb list_tm in
 311       let h_tm = rand h_tm' in
 312       let th0 = INST[h_tm, h_var; t_tm, t_var] map_cons in
 313       let ltm, rtm = dest_comb (rand(concl th0)) in
 314       let cons_tm, f_h_tm = dest_comb ltm in
 315       let f_h_th = f_conv f_h_tm in
 316       let map_t_th = map_conv_raw t_tm in
 317         TRANS th0 (MK_COMB (AP_TERM cons_tm f_h_th, map_t_th))
 318     else
 319       map_empty in
 320
 321     map_conv_raw list_tm;;
 322
 323
 324 (*
 325 let tm = `MAP (\x. x + 1) [1;2;3;4;5;6;7;8;9;10;11]`;;
 326
 327 REWRITE_CONV[MAP] tm;;
 328 map_conv_univ BETA_CONV tm;;
 329
 330 test 100 (REWRITE_CONV[MAP]) tm;; (* 0.464 *)
 331 test 100 (map_conv_univ BETA_CONV) tm;; (* 0.04 *)
 332
 333 test 100 (map_conv_univ (BETA_CONV THENC NUM_ADD_CONV)) tm;; (* 0.096 *)
 334 *)
 335
 336
 337 (*****************************************)
 338
 339 (* ALL rules *)
 340
 341
 342 let ALL_A_HD = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> P h`, SIMP_TAC[ALL])) and
 343     ALL_A_TL = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> ALL P t`, SIMP_TAC[ALL]));;
 344
 345
 346 (* Given a theorem `ALL P list` returns the list of theorems (P x1),...,(P xn) *)
 347 let get_all th =
 348   let ltm, list_tm = dest_comb (concl th) in
 349   let p_tm = rand ltm in
 350   let list_ty = type_of list_tm in
 351   let p_ty = type_of p_tm in
 352   let ty = (hd o snd o dest_type) list_ty in
 353   let p_var = mk_var("P", p_ty) in
 354   let h_var = mk_var("h", ty) in
 355   let t_var = mk_var("t", list_ty) in
 356
 357   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 358   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 359
 360   let rec get_all_raw all_th list_tm =
 361     if (is_comb list_tm) then
 362       let h_tm', t_tm = dest_comb list_tm in
 363       let h_tm = rand h_tm' in
 364       let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 365       let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 366       let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 367         th_hd :: get_all_raw th_tl t_tm
 368     else
 369       [] in
 370
 371     get_all_raw th list_tm;;
 372
 373
 374
 375 (* Given a theorem `ALL P list`, returns (P x_i1),..., (P x_in)
 376    where i1,...,in are given indices.
 377    The list of indices should be sorted *)
 378 let select_all th indices =
 379   let ltm, list_tm = dest_comb (concl th) in
 380   let p_tm = rand ltm in
 381   let list_ty = type_of list_tm in
 382   let p_ty = type_of p_tm in
 383   let ty = (hd o snd o dest_type) list_ty in
 384   let p_var = mk_var("P", p_ty) in
 385   let h_var = mk_var("h", ty) in
 386   let t_var = mk_var("t", list_ty) in
 387
 388   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 389   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 390
 391   let rec get_all_raw all_th list_tm indices n =
 392     match indices with
 393         [] -> []
 394       | i::is ->
 395           let h_tm', t_tm = dest_comb list_tm in
 396           let h_tm = rand h_tm' in
 397           let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 398           let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 399
 400           if (i - n = 0) then
 401             let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 402               th_hd :: get_all_raw th_tl t_tm is (n + 1)
 403           else
 404             get_all_raw th_tl t_tm (i::is) (n + 1) in
 405
 406     get_all_raw th list_tm indices 0;;
 407
 408
 409 (*
 410 let tm = `ALL (\x. x > 3) [4; 5; 8; 10; 5; 4]`;;
 411 let th = (EQT_ELIM o REWRITE_CONV[ALL; ARITH]) tm;;
 412
 413 (* 0.192 *)
 414 test 100 (CONJUNCTS o REWRITE_RULE[ALL]) th;;
 415 (* 0.016 *)
 416 test 100 (get_all) th;;
 417 (* 0.012 *)
 418 test 100 (select_all th) [2;3;4];;
 419 *)
 420
 421
 422
 423 (*************************************)
 424
 425 (* list_sum conversions *)
 426
 427
 428 let LIST_SUM_A_EMPTY = prove(`list_sum [] (f:A->real) = &0`, REWRITE_TAC[list_sum; ITLIST]) and
 429     LIST_SUM_A_H = prove(`list_sum [h:A] f = f h`, REWRITE_TAC[list_sum; ITLIST; REAL_ADD_RID]) and
 430     LIST_SUM_A_CONS = prove(`list_sum (CONS (h:A) t) f = f h + list_sum t f`, REWRITE_TAC[list_sum; ITLIST]);;
 431
 432
 433 let list_sum_conv f_conv tm =
 434   let ltm, f_tm = dest_comb tm in
 435   let list_tm = rand ltm in
 436   let list_ty = type_of list_tm in
 437   let f_ty = type_of f_tm in
 438   let ty = (hd o snd o dest_type) list_ty in
 439   let f_var = mk_var("f", f_ty) and
 440       h_var = mk_var("h", ty) and
 441       t_var = mk_var("t", list_ty) in
 442   let inst_t = INST[f_tm, f_var] o INST_TYPE[ty, aty] in
 443   let list_sum_h = inst_t LIST_SUM_A_H and
 444       list_sum_cons = inst_t LIST_SUM_A_CONS in
 445
 446   let rec list_sum_conv_raw = fun h_tm t_tm ->
 447     if (is_comb t_tm) then
 448       let h_tm', t_tm' = dest_comb t_tm in
 449       let th0 = INST[h_tm, h_var; t_tm, t_var] list_sum_cons in
 450       let ltm, rtm = dest_comb(rand(concl th0)) in
 451       let plus_op, fh_tm = dest_comb ltm in
 452       let f_th = f_conv fh_tm in
 453       let th1 = list_sum_conv_raw (rand h_tm') t_tm' in
 454       let th2 = MK_COMB(AP_TERM plus_op f_th, th1) in
 455         TRANS th0 th2
 456     else
 457       let th0 = INST[h_tm, h_var] list_sum_h in
 458       let f_th = f_conv (rand(concl th0)) in
 459         TRANS th0 f_th in
 460
 461     if (is_comb list_tm) then
 462       let h_tm, t_tm = dest_comb list_tm in
 463         list_sum_conv_raw (rand h_tm) t_tm
 464     else
 465       inst_t LIST_SUM_A_EMPTY;;
 466
 467
 468
 469
 470 (*
 471 let tm = `list_sum [&1; &3; &4; pi; #0.1] cos`;;
 472
 473 list_sum_conv ALL_CONV tm;;
 474
 475 (* 2.812 *)
 476 test 1000 (REWRITE_CONV[list_sum; ITLIST; REAL_ADD_RID]) tm;;
 477 (* 0.076 *)
 478 test 1000 (list_sum_conv ALL_CONV) tm;;
 479
 480
 481 let tm = `list_sum [&1; &3; &4; pi; #0.1] (\x. cos x)`;;
 482 (* 0.104 *)
 483 test 1000 (list_sum_conv BETA_CONV) tm;;
 484 *)
 485
 486
 487
 488 (*****************************************)
 489
 490 (* set_of_list conversions *)
 491
 492 let SET_OF_LIST_A_EMPTY = prove(`set_of_list ([]:(A)list) = {}`, REWRITE_TAC[set_of_list]) and
 493     SET_OF_LIST_A_H = prove(`set_of_list [h:A] = {h}`, REWRITE_TAC[set_of_list]) and
 494     SET_OF_LIST_A_CONS = prove(`set_of_list (CONS (h:A) t) = h INSERT set_of_list t`, REWRITE_TAC[set_of_list]);;
 495
 496
 497
 498 let set_of_list_conv tm =
 499   let list_tm = rand tm in
 500   let list_ty = type_of list_tm in
 501   let ty = (hd o snd o dest_type) list_ty in
 502   let h_var = mk_var("h", ty) in
 503   let t_var = mk_var("t", list_ty) in
 504   let inst_t = INST_TYPE[ty, aty] in
 505   let set_of_list_h, set_of_list_cons = inst_t SET_OF_LIST_A_H, inst_t SET_OF_LIST_A_CONS in
 506
 507   let rec set_of_list_conv_raw = fun h_tm t_tm ->
 508     if (is_comb t_tm) then
 509       let h_tm', t_tm' = dest_comb t_tm in
 510       let th0 = INST[h_tm, h_var; t_tm, t_var] set_of_list_cons in
 511       let ltm, rtm = dest_comb(rand(concl th0)) in
 512         TRANS th0 (AP_TERM ltm (set_of_list_conv_raw (rand h_tm') t_tm'))
 513     else
 514       INST[h_tm, h_var] set_of_list_h in
 515
 516     if (is_comb list_tm) then
 517       let h_tm, t_tm = dest_comb list_tm in
 518         set_of_list_conv_raw (rand h_tm) t_tm
 519     else
 520       inst_t SET_OF_LIST_A_EMPTY;;
 521
 522
 523
 524 (*
 525 let tm = `set_of_list [&1; &5; &6; &3; &5; &8; &9]`;;
 526
 527 (* 0.872 *)
 528 test 1000 (REWRITE_CONV[set_of_list]) tm;;
 529 (* 0.076 *)
 530 test 1000 set_of_list_conv tm;;
 531 *)