1load "acl2encodeLib"; 2load "testTypesTheory"; 3load "testFunctionsTheory"; 4load "intLib"; 5 6open Parse 7open polytypicLib encodeLib functionEncodeLib 8open acl2encodeLib testTypesTheory testFunctionsTheory; 9open listTheory rich_listTheory optionTheory combinTheory; 10 11(*****************************************************************************) 12(* Testing ... *) 13(*****************************************************************************) 14 15fun mappartition f [] = ([],[]) 16 | mappartition f (x::xs) = 17 (cons (f x) ## I) (mappartition f xs) 18 handle e => (print (exn_to_string e) ; (I ## cons x) (mappartition f xs)); 19 20val type_tests = (ref 0,ref ([]:(string * hol_type list) list)); 21 22fun Test s f t = 23let val (count,results) = type_tests 24 val (passed,failed) = mappartition f t 25in 26 (count := (!count) + 1 ; 27 results := ("Test " ^ s ^ " : " ^ 28 int_to_string (!count),failed) :: (!results)) 29end 30 31val types = ref (rev (map (type_of o lhs) (strip_conj (concl LIST)))); 32 33(* Initialisation *) 34 35val num = ``:num``; 36val int = ``:int``; 37val rat = ``:rat``; 38val com = ``:complex_rational``; 39val bool = ``:bool``; 40val char = ``:char``; 41val string = ``:string``; 42val pair = ``:'a # 'b``; 43val list = ``:'a list``; 44val sexp = ``:sexp``; 45 46local 47in 48fun generate_functions target = 49let val _ = Test "" (map (add_translation target o fst) o 50 split_nested_recursive_set) (rev (!types)); 51 val _ = Test "map" (generate_source_function "map" o base_type) 52 (rev (!types)); 53 val _ = Test "all" (generate_source_function "all" o base_type) 54 (rev (!types)); 55 val _ = Test "encode" (generate_coding_function target "encode" o base_type) 56 (rev (!types)); 57 val _ = Test "detect" (generate_coding_function target "detect" o base_type) 58 (rev (!types)); 59 val _ = Test "decode" (generate_coding_function target "decode" o base_type) 60 (rev (!types)); 61 val _ = Test "fix" (generate_coding_function target "fix" o base_type) 62 (rev (!types)); 63in 64 () 65end 66end 67 68fun generate_theorems target = 69let val every_type = 70 filter (fn x => not (can (match_type x) pair) andalso 71 not (can (match_type x) list) andalso 72 not (x = num) andalso not (x = bool) andalso 73 not (x = rat) andalso not (x = int)) 74 (mk_set (flatten (map (fn t => 75 t::map snd (reachable_graph uncurried_subtypes t)) (rev (!types))))) 76 77 fun cremove_all string = 78 mapfilter (fn t => remove_coding_theorem_precise sexp t string) 79 every_type 80 fun sremove_all string = 81 mapfilter (fn t => remove_source_theorem_precise t string) 82 every_type 83 84 val remove_all = cremove_all "encode_detect_all"; 85 val remove_all = sremove_all "map_compose"; 86 val remove_all = cremove_all "encode_decode_map"; 87 val remove_all = cremove_all "encode_map_encode"; 88 val remove_all = cremove_all "general_detect"; 89 val remove_all = cremove_all "general_detect"; 90 val remove_all = cremove_all "decode_encode_fix"; 91 val remove_all = cremove_all "fix_id"; 92 93 val _ = time (Test "encode_detect_all" 94 (generate_coding_theorem sexp "encode_detect_all")) 95 (rev (!types)); 96 val _ = time (Test "all_id" 97 (generate_source_theorem "all_id")) 98 (rev (!types)); 99 val _ = time (Test "map_id" 100 (generate_source_theorem "map_id")) 101 (rev (!types)); 102 val _ = time (Test "map_compose" 103 (generate_source_theorem "map_compose")) 104 (rev (!types)); 105 val _ = time (Test "encode_decode_map" 106 (generate_coding_theorem sexp "encode_decode_map")) 107 (rev (!types)); 108 val _ = time (Test "encode_map_encode" 109 (generate_coding_theorem sexp "encode_map_encode")) 110 (rev (!types)); 111 val _ = time (Test "general_detect" 112 (generate_coding_theorem sexp "general_detect")) 113 (rev (!types)); 114 val _ = time (Test "decode_encode_fix" 115 (generate_coding_theorem sexp "decode_encode_fix")) 116 (rev (!types)); 117 val _ = time (Test "fix_id" 118 (generate_coding_theorem sexp "fix_id")) 119 (rev (!types)); 120in 121() 122end 123 124 125(*****************************************************************************) 126(* Function testing: *) 127(* add_test adds a test as a string, function, data pair *) 128(* *) 129(*****************************************************************************) 130 131val tests = ref ([] : (string * (thm -> unit) * thm) list); 132fun add_test (name,func,arg) = 133 tests := !tests @ [(name,(fn y => (func y ; ())),arg)]; 134fun run_test (s,func,thm) = 135 (print ("Test: " ^ s ^ "\n") ; 136 (func thm) before (print "passed!\n")) 137 handle e => Raise e; 138val last_test = ref (NONE : (string * (thm -> unit) * thm) option); 139fun run_function_tests () = 140 case (total (first (not o can run_test)) (!tests)) 141 of NONE => print "Success!!!!!!\n" 142 | SOME last => (last_test := SOME last ; print "Failed.\n"); 143fun run_last_function_test () = run_test (Option.valOf (!last_test)) 144 145(*****************************************************************************) 146(* Initialisation: *) 147(* Add theorems for natural numbers and the conditional *) 148(* Add theorems for booleans and polymorphic equality *) 149(* Add simple theorems for lists *) 150(* Add simple pair theorems *) 151(* *) 152(*****************************************************************************) 153 154fun initialise_function_tests () = 155let val _ = add_standard_coding_rewrites ``:sexp`` ``:'a option`` 156 handle e => Raise e; 157 val _ = add_standard_coding_rewrites ``:sexp`` ``:'a Tree`` 158 handle e => Raise e; 159in 160 () 161end; 162 163(*****************************************************************************) 164(* Flattening: 'a list, 'a + num, (num + 'a) list, ('a + num) list *) 165(*****************************************************************************) 166 167val _ = add_test ("flatten list", 168 flatten_recognizers (mk_fullname ``:sexp``) o 169 type_of o lhs o concl, 170 (REFL o curry mk_var "a") ``:'a list``); 171 172val _ = add_test ("flatten sum", 173 flatten_recognizers (mk_fullname ``:sexp``) o 174 type_of o lhs o concl, 175 (REFL o curry mk_var "a") ``:'a + num``); 176 177val _ = add_test ("flatten sum list A", 178 flatten_recognizers (mk_fullname ``:sexp``) o 179 type_of o lhs o concl, 180 (REFL o curry mk_var "a") ``:(num + 'a) list``); 181 182val _ = add_test ("flatten sum list B", 183 flatten_recognizers (mk_fullname ``:sexp``) o 184 type_of o lhs o concl, 185 (REFL o curry mk_var "a") ``:('a + num) list``); 186 187(*****************************************************************************) 188(* Simple functions: *) 189(* EXP : Clause form & natural number case *) 190(* LENGTH (num) : Clause form & list case *) 191(* APPEND (num) : Clause form & list case *) 192(* REVERSE (num) : Clause form & list case *) 193(* FLAT (num) : Clause form & list case (hard) *) 194(* LAST (num) : Missing cases *) 195(* SEG (num) : Missing cases (hard) *) 196(* SPLIT (num) : Mutually Recursive Definition *) 197(* EVEN_EXTEND : Extended case on SUC *) 198(* ODD_EVEN : Mutually Recursive Definition *) 199(* ECASE (num) : Extended case (num) & Missing case (hard) *) 200(* LCASE (num) : Extended case (list) & Missing case (hard) *) 201(* *) 202(* Datatype functions: *) 203(* OPTION_JOIN (num) : Simple option case *) 204(* OLIST (num) : Option cases in a list *) 205(* FLATTEN_TREE (num) : Flatten a binary tree using append *) 206(* FT_FAST (num) : Flatten a binary tree using an accumulator *) 207(* *) 208(* Functions from the thesis: *) 209(* merge : Combintation *) 210(* merge_sort : LET construct *) 211(* *) 212(*****************************************************************************) 213 214open testFunctionsTheory; 215 216val _ = add_test ("EXP", 217 translate_simple_function [(``($**):num -> num -> num``,"exp")], 218 arithmeticTheory.EXP); 219val _ = add_test ("LENGTH (num)", 220 translate_simple_function [(``LENGTH``,"length")], 221 INST_TYPE [alpha |-> num] LENGTH); 222val _ = add_test ("APPEND (num)", 223 translate_simple_function [(``$++``,"append")], 224 INST_TYPE [alpha |-> num] APPEND); 225val _ = add_test ("REVERSE (num)", 226 translate_simple_function [(``REVERSE``,"reverse")], 227 INST_TYPE [alpha |-> num] REVERSE_DEF); 228val _ = add_test ("FLAT (num)", 229 translate_simple_function [(``testFunctions$FLAT``,"flat")], 230 INST_TYPE [alpha |-> num] FLAT_def); 231val _ = add_test ("LAST (num)", 232 translate_simple_function [(``LAST``,"last")], 233 INST_TYPE [alpha |-> num] LAST_DEF); 234 235val limit_correct = 236 prove(``a + b <= LENGTH c ==> ~((?n. a = SUC n) /\ (c = []))``, 237 Cases_on `c` THEN RW_TAC arith_ss [listTheory.LENGTH]); 238val limit_recursive1 = 239 prove(``(?d. a = SUC d) /\ (b = 0) /\ 240 (?x y. c = x :: y) /\ a + b <= LENGTH c ==> 241 PRE a + 0 <= LENGTH (TL c)``, 242 Cases_on `c` THEN RW_TAC arith_ss [LENGTH,TL,NULL]); 243val limit_recursive2 = 244 prove(``(?d. a = SUC d) /\ (?d. b = SUC d) /\ 245 (?x y. c = x :: y) /\ a + b <= LENGTH c ==> 246 SUC (PRE a) + PRE b <= LENGTH (TL c)``, 247 Cases_on `c` THEN RW_TAC arith_ss [LENGTH,TL,NULL]); 248 249val _ = add_test ("SEG (num)", 250 translate_limit_function 251 [(``SEG``,"seg")] 252 [(``SEG``,[``\a b c. a + b <= LENGTH c``])] 253 [limit_correct,limit_recursive1,limit_recursive2], 254 INST_TYPE [alpha |-> num] SEG); 255 256val _ = add_test ("SPLIT (num)", 257 translate_simple_function 258 [(``split1``,"splitn1"),(``split2``,"splitn2")], 259 INST_TYPE [alpha |-> num] SPLIT_def); 260val _ = add_test ("EVEN_EXTEND", 261 translate_simple_function [(``EVEN``,"even_extend")], 262 EVEN_EXTEND_def); 263val _ = add_test ("ODD_EVEN", 264 translate_simple_function [(``ODD``,"odd"),(``EVEN``,"even")], 265 ODD_EVEN_def); 266val _ = add_test ("ECASE (num)", 267 translate_simple_function [(``ECASE``,"ecase")], 268 INST_TYPE [alpha |-> num] ECASE_def); 269val _ = add_test ("LCASE (num)", 270 translate_simple_function [(``LCASE``,"lcase")], 271 INST_TYPE [alpha |-> num] LCASE_def); 272 273val _ = add_test ("OPTION_JOIN (num)", 274 translate_simple_function [(``OPTION_JOIN``,"option_join")], 275 INST_TYPE [alpha |-> num] OPTION_JOIN_DEF); 276val _ = add_test ("OLIST (num)", 277 translate_simple_function [(``OLIST``,"olist")], 278 INST_TYPE [alpha |-> num] OLIST_def); 279 280val _ = add_test ("merge", 281 translate_simple_function [(``merge``,"mergen")], 282 merge_def); 283val _ = add_test ("merge_sort", 284 translate_simple_function [(``merge_sort``,"merge_sortn")], 285 merge_sort_def); 286 287val _ = add_test ("FLATTEN_TREE (num)", 288 translate_simple_function [(``FLATTEN_TREE``,"flatten_tree")], 289 INST_TYPE [alpha |-> num] FLATTEN_TREE_def); 290 291val _ = add_test ("FT_FAST (num)", 292 translate_simple_function [(``FT_FAST``,"ft_fast")], 293 INST_TYPE [alpha |-> num] FT_FAST_def); 294 295val LENGTH_MAP = prove(``!x f. LENGTH (MAP f x) = LENGTH x``, 296 Induct THEN 297 FULL_SIMP_TAC std_ss [LENGTH,MAP,o_THM]); 298 299val _ = add_test ("LENGTH (polymorphic)", 300 translate_simple_polymorphic_function 301 [(``LENGTH``,"length_poly")] 302 [(``LENGTH``,LENGTH_MAP)], 303 LENGTH); 304 305val APPEND_MAP = prove(``!x y f. MAP f x ++ MAP f y = MAP f (x ++ y)``, 306 Induct THEN RW_TAC std_ss [MAP,APPEND]); 307 308val _ = add_test ("APPEND (polymorphic)", 309 translate_simple_polymorphic_function 310 [(``$++``,"append")] 311 [(``$++``,APPEND_MAP)], 312 APPEND); 313 314val REVERSE_APP_MAP = prove( 315 ``!x y f. REVERSE (MAP f x) ++ MAP f y = MAP f (REVERSE x ++ y)``, 316 Induct THEN RW_TAC std_ss [MAP,REVERSE_DEF,APPEND,GSYM APPEND_ASSOC] THEN 317 RW_TAC std_ss [GSYM MAP]); 318 319val REVERSE_MAP = REWRITE_RULE [APPEND_NIL,MAP] 320 (Q.SPECL [`x`,`[]`] REVERSE_APP_MAP); 321 322val _ = add_test ("REVERSE (polymorphic)", 323 translate_simple_polymorphic_function 324 [(``REVERSE``,"reverse")] 325 [(``REVERSE``,REVERSE_MAP)], 326 REVERSE_DEF); 327 328val FLAT_MAP = prove(``!x. FLAT (MAP (MAP f) x) = MAP f (FLAT x)``, 329 Induct THEN TRY Induct THEN RW_TAC std_ss [FLAT_def,MAP] THEN 330 ASM_REWRITE_TAC [GSYM MAP]); 331 332val _ = add_test ("FLAT (polymorphic)", 333 translate_simple_polymorphic_function 334 [(``testFunctions$FLAT``,"flat")] 335 [(``testFunctions$FLAT``,FLAT_MAP)], 336 FLAT_def); 337 338val LAST_MAP = prove( 339 ``!x. (?a b. x = a :: b) ==> (LAST (MAP f x) = f (LAST x))``, 340 Induct THEN TRY (Cases_on `x`) THEN RW_TAC std_ss [MAP,LAST_DEF] THEN 341 FULL_SIMP_TAC std_ss [MAP] THEN METIS_TAC []); 342 343val MAP_CONS = prove( 344 ``!x. (?a b. x = a :: b) ==> (?a b. MAP f x = a :: b)``, 345 Induct THEN RW_TAC std_ss [MAP]); 346 347val last_limit = prove(``!a. (?x y. a = x :: y) ==> ~(a = [])``, 348 Cases THEN RW_TAC std_ss []); 349 350val _ = add_test ("LAST (polymorphic)", 351 translate_limit_polymorphic_function 352 [(``LAST``,"last")] 353 [(``LAST``,LAST_MAP)] 354 [(``LAST``,[``\a. (?x y. a = x :: y)``])] 355 [MAP_CONS,SPEC_ALL last_limit], 356 LAST_DEF); 357 358val limit_correct = 359 prove(``a + b <= LENGTH c ==> ~((?n. a = SUC n) /\ (c = []))``, 360 Cases_on `c` THEN RW_TAC arith_ss [listTheory.LENGTH]); 361val limit_recursive1 = 362 prove(``(?d. a = SUC d) /\ (b = 0) /\ 363 (?x y. c = x :: y) /\ a + b <= LENGTH c ==> 364 PRE a + 0 <= LENGTH (TL c)``, 365 Cases_on `c` THEN RW_TAC arith_ss [LENGTH,TL,NULL]); 366val limit_recursive2 = 367 prove(``(?d. a = SUC d) /\ (?d. b = SUC d) /\ 368 (?x y. c = x :: y) /\ a + b <= LENGTH c ==> 369 SUC (PRE a) + PRE b <= LENGTH (TL c)``, 370 Cases_on `c` THEN RW_TAC arith_ss [LENGTH,TL,NULL]); 371 372val SEG_MAP = prove( 373 ``!c a b. a + b <= LENGTH c ==> (SEG a b (MAP f c) = MAP f (SEG a b c))``, 374 Induct THEN1 RW_TAC std_ss [LENGTH,MAP,SEG] THEN 375 Induct_on `a` THEN Induct_on `b` THEN RW_TAC std_ss [SEG,LENGTH,MAP] THEN 376 FIRST_ASSUM MATCH_MP_TAC THEN DECIDE_TAC); 377 378val LIMIT_MAP = prove( 379 ``!c a b f. a + b <= LENGTH c ==> a + b <= LENGTH (MAP f c)``, 380 Induct THEN RW_TAC std_ss [LENGTH,MAP,LENGTH_MAP]); 381 382val _ = add_test ("SEG (polymorphic)", 383 translate_limit_polymorphic_function 384 [(``SEG``,"seg")] 385 [(``SEG``,SEG_MAP)] 386 [(``SEG``,[``\a b c. a + b <= LENGTH c``])] 387 [LIMIT_MAP,limit_correct,limit_recursive1,limit_recursive2], 388 SEG); 389 390(*****************************************************************************) 391(* Word and FCP testing: *) 392(* i2n : Convert integers to natural numbers (mod p) *) 393(* extend : Convert a signed int to a signed int (mod p) *) 394(* *) 395(*****************************************************************************) 396 397local 398open intLib integerTheory 399val i2n_lemma = prove(``0 <= (i + 1) rem 2 ** l - 1 + 2 ** l``, 400 REWRITE_TAC [ARITH_PROVE ``0i <= a - 1 + b = ~a < b``] THEN 401 MATCH_MP_TAC (ARITH_PROVE ``!a b c. a <= b /\ b < c ==> a < c:int``) THEN 402 Q.EXISTS_TAC `ABS ((i + 1) rem 2 ** l)` THEN 403 METIS_TAC [INT_REMQUOT,INT_ABS_NUM,INT_EXP,INT_EXP_EQ0, 404 ARITH_PROVE ``~(2 = 0i)``,INT_ABS,INT_NOT_LT,INT_NEGNEG,INT_LE_REFL, 405 INT_LE_NEGL]); 406in 407val thms = [INT_EXP_EQ0,ARITH_PROVE ``~(2 = 0i)``, 408 REWRITE_CONV [integerTheory.INT_POS,integerTheory.INT_EXP] 409 ``0 <= 2 ** a``, 410 prove(``~(b = 0) /\ 0i <= b ==> 0 <= a % b``, 411 METIS_TAC [INT_MOD_BOUNDS,INT_NOT_LT]),i2n_lemma] 412end; 413 414val _ = add_test("i2n", 415 translate_conditional_function [(``i2n``,"I2N")] thms, 416 signedintTheory.i2n_def); 417 418val _ = add_test("extend", 419 translate_simple_function [(``extend``,"EXTEND")], 420 signedintTheory.extend_def); 421 422val _ = add_test("word_div", 423 translate_limit_fcp_function 424 "WORDDIV" 425 [``\a b. ~(b = 0w)``] [wordsTheory.w2n_eq_0], 426 wordsTheory.word_div_def); 427 428(*****************************************************************************) 429(* Functions with limits and recursion proofs (ie. LOG) *) 430(*****************************************************************************) 431 432val log_compute = prove(``1 < a /\ 1 <= x ==> 433 (LOG a x = if x < a then 0 else 1 + LOG a (x DIV a))``, 434 RW_TAC std_ss [] THEN 435 FULL_SIMP_TAC std_ss [arithmeticTheory.NOT_LESS,logrootTheory.LOG_DIV] THEN 436 MATCH_MP_TAC logrootTheory.LOG_UNIQUE THEN 437 RW_TAC arith_ss [arithmeticTheory.EXP]); 438 439val log_rec = prove(``1 < a /\ 1 <= x ==> x DIV a < x``, 440 REPEAT (Induct_on `a` THEN 441 RW_TAC arith_ss [arithmeticTheory.DIV_LT_X,arithmeticTheory.ADD1, 442 arithmeticTheory.LEFT_ADD_DISTRIB])); 443 444val log_rec_ok = prove(``~(a = 0) /\ ~(x < a) ==> (1 <= x DIV a)``, 445 RW_TAC arith_ss [arithmeticTheory.NOT_LESS,arithmeticTheory.X_LE_DIV]); 446 447val _ = add_test("LOG", 448 translate_limit_function 449 [(``LOG``,"log")] 450 [(``LOG``,[``\a b. 1n < a /\ 1n <= b ``, 451 ``\a b. 1 < a /\ 1 <= b ==> b DIV a < b``])] 452 [GEN_ALL log_rec,DECIDE ``1 < a ==> ~(a = 0n)``,log_rec_ok], 453 log_compute); 454 455(*****************************************************************************) 456(* Testing HO functions *) 457(*****************************************************************************) 458 459val _ = add_test("EVERY", 460 translate_simple_function 461 [(``EVERY``,"everyless")], 462 (CONJ (ISPEC ``\a. 0n < a`` (CONJUNCT1 EVERY_DEF)) 463 (ISPEC ``\a. 0n < a`` (CONJUNCT2 EVERY_DEF)))); 464 465val _ = add_test("ADDLIST", 466 translate_simple_function 467 [(``ADDLIST``,"addlist")], 468 ADDLIST_def); 469 470val _ = add_test("SNOC", 471 translate_simple_function 472 [(``SNOC``,"snoc")], 473 (INST_TYPE [alpha |-> num] rich_listTheory.SNOC)); 474 475val _ = add_test("GENLIST", 476 translate_simple_function 477 [(``GENLIST``,"genlist")], 478 (REWRITE_RULE [combinTheory.I_THM] 479 ((LIST_CONJ (map (ISPEC ``I:num -> num``) 480 (CONJUNCTS rich_listTheory.GENLIST)))))); 481 482val _ = add_test("GENL",translate_simple_function 483 [(``GENL``,"genl")],GENL_def); 484 485val _ = add_test("ADDN",translate_simple_function 486 [(``ADDN``,"addn")],ADDN_def); 487 488(*****************************************************************************) 489(* Perform the testing... *) 490(*****************************************************************************) 491 492(* 493val _ = Hol_datatype `wordlist = WNil | WCons of 'a word => wordlist`; 494 495val _ = types := ``:'a wordlist``::(!types); 496*) 497 498val _ = generate_functions ``:sexp``; 499val _ = generate_theorems ``:sexp``; 500 501val _ = print "Testing flattening...."; 502val _ = set_trace "functionEncodeLib.Trace" 1; 503val (passed,failed) = 504 mappartition (flatten_recognizers (mk_fullname ``:sexp``)) 505 (!types); 506val _ = if length failed > 1 then raise Empty else (); 507 508 509val _ = print "Testing abstract flattening..."; 510 511val gen = Random.newgen(); 512 513fun mk_word t = type_subst [alpha |-> t] ``:'a word``; 514 515fun tsubst t = 516let val tvs = type_vars t 517 val tvs' = map (fn x => 518 if (Random.range(0,2) gen = 1) then mk_word x else x) tvs 519 val r = type_subst (map2 (curry op|->) tvs tvs') t 520in 521 (print_type r ; print "\n" ; r) 522end; 523 524val _ = set_trace "functionEncodeLib.Trace" 1; 525val f = can (match_term ``dimindex (:'a)``); 526val target = ``:sexp``; 527val word_gen = flatten_abstract_recognizers (K "wordp") 528 f ``:sexp`` ``:'a word``; 529val cstypes = mapfilter Type [`:'a CS3`, `:'a CS2`, `:'a CS1`, `:'a CS4`]; 530val sane_types = filter (fn x => not (exists (can (C match_type x)) cstypes)) 531 (!types) 532val (passed,failed) = 533 mappartition (flatten_abstract_recognizers (mk_fullname ``:sexp``) 534 f ``:sexp`` o tsubst) sane_types; 535val _ = if length failed > 1 then raise Empty else (); 536 537val _ = print "Testing rewrite-initialisation..."; 538val (passed,failed) = 539 mappartition (add_standard_coding_rewrites ``:sexp``) 540 (filter (not o C mem [``:register``,``:Steve0``]) (!types)); 541val _ = if length failed > 1 then raise Empty else (); 542 543val _ = print "Testing predicate equivalence..."; 544val (passed,failed) = 545 mappartition (predicate_equivalence ``:sexp``) 546 (filter (not o C mem [``:register``,``:Steve0``]) (!types)); 547val _ = if length failed > 1 then raise Empty else (); 548 549val _ = initialise_function_tests (); 550val _ = set_trace "functionEncodeLib.Trace" 4; 551 552(*****************************************************************************) 553(* Polymorphic tests for datatypes... *) 554(*****************************************************************************) 555 556val OPTION_JOIN_MAP = prove( 557 ``!x. OPTION_JOIN (map (map f) x) = map f (OPTION_JOIN x)``, 558 Cases THEN RW_TAC std_ss [get_source_function_def ``:'a option`` "map"]); 559 560val _ = add_test ("OPTION_JOIN (polymorphic)", 561 translate_simple_polymorphic_function 562 [(``OPTION_JOIN``,"option_join")] 563 [(``OPTION_JOIN``,OPTION_JOIN_MAP)], 564 OPTION_JOIN_DEF); 565 566val FLATTEN_TREE_MAP = prove( 567 ``!x. FLATTEN_TREE (map f x) = MAP f (FLATTEN_TREE x)``, 568 Induct THEN 569 RW_TAC std_ss [FLATTEN_TREE_def,get_source_function_def ``:'a Tree`` "map", 570 MAP,MAP_APPEND]); 571 572val _ = add_test ("FLATTEN_TREE (polymorphic)", 573 translate_simple_polymorphic_function 574 [(``FLATTEN_TREE``,"flatten_tree")] 575 [(``FLATTEN_TREE``,FLATTEN_TREE_MAP)], 576 FLATTEN_TREE_def); 577 578val FT_FAST_MAP = prove( 579 ``!x y f. FT_FAST (map f x) (MAP f y) = MAP f (FT_FAST x y)``, 580 Induct THEN 581 RW_TAC std_ss [FT_FAST_def,get_source_function_def ``:'a Tree`` "map",MAP]); 582 583val _ = add_test ("FT_FAST (polymorphic)", 584 translate_simple_polymorphic_function 585 [(``FT_FAST``,"ft_fast")] 586 [(``FT_FAST``,FT_FAST_MAP)], 587 FT_FAST_def); 588 589val _ = run_function_tests(); 590 591