1open HolKernel boolLib Parse wordsLib testutils 2 3val _ = new_theory "test_wordpp"; 4 5 6(********** Helper functions **********) 7 8fun test (expected, s) = tpp_expected { 9 input = s, output = expected, testf = standard_tpp_message }; 10 11fun concat_type s ty = s ^ " :" ^ ty; 12 13(* Allow specification of word length, without expecting it in output *) 14fun test_with_type (ty, (expected, s)) = test (expected, concat_type s ty); 15 16fun remove l ls = filter (fn a => a <> l) ls; 17 18(* Test multiple input formats against a single expected output format *) 19fun run_tests tys expected inputs = let 20 val inputs' = remove expected inputs 21 val tests = List.concat (map (zip tys) (map (zip expected) inputs')) in 22 map test_with_type tests end; 23 24 25(********** Specify tests **********) 26 27val tys = ["word3", "word2", "word10", "word24"]; 28 29val default = ["0w", "1w", "42w", "0x10000w"]; 30 31val dec = ["0w", "1w", "42w", "65536w"]; 32 33val bin = ["0b0w", "0b1w", "0b101010w", "0b10000000000000000w"]; 34 35val padded_bin = ["0b000w", "0b01w", "0b0000101010w", 36 "0b000000010000000000000000w"]; 37 38val oct = ["00w", "01w", "052w", "0200000w"]; 39 40val hex = ["0x0w", "0x1w", "0x2Aw", "0x10000w"]; 41 42val padded_hex = ["0x0w", "0x1w", "0x2Aw", "0x010000w"]; 43 44val tests = [default, dec, bin, padded_bin, oct, hex, padded_hex]; 45 46 47val tys_neg = ["word8", "word1", "word6", "17 word"]; 48 49val default_neg = ["0w", "-1w", "-22w", "-0x10000w"]; 50 51val dec_neg = ["0w", "-1w", "-22w", "-65536w"]; 52 53val bin_neg = ["0b0w", "-0b1w", "-0b10110w", "-0b10000000000000000w"]; 54 55val padded_bin_neg = ["0b00000000w", "-0b1w", "-0b010110w", 56 "-0b10000000000000000w"]; 57 58val oct_neg = ["00w", "-01w", "-026w", "-0200000w"]; 59 60val hex_neg = ["0x0w", "-0x1w", "-0x16w", "-0x10000w"]; 61 62val padded_hex_neg = ["0x00w", "-0x1w", "-0x16w", "-0x10000w"]; 63 64(* 65val neg_tests = [default_neg, dec_neg, bin_neg, padded_bin_neg, oct_neg, 66 hex_neg, padded_hex_neg]; 67*) 68 69(********** Execute tests **********) 70(* interactive only: 71val _ = diemode := FailException 72*) 73val _ = base_tokens.allow_octal_input := true; 74 75(* Test default printing *) 76val _ = tprint "Testing default words output"; 77val _ = run_tests tys default tests; 78 79(* Test decimal printing *) 80val _ = tprint "Testing output_words_as_dec"; 81val _ = output_words_as_dec(); 82val _ = run_tests tys dec tests; 83 84(* Test binary printing *) 85val _ = tprint "Testing output_words_as_bin"; 86val _ = output_words_as_bin(); 87val _ = run_tests tys bin tests; 88 89(* Test padded binary printing *) 90val _ = tprint "Testing output_words_as_padded_bin"; 91val _ = output_words_as_padded_bin(); 92val _ = run_tests tys padded_bin tests; 93 94(* Test octal printing *) 95val _ = tprint "Testing output_words_as_oct"; 96val _ = output_words_as_oct(); 97val _ = run_tests tys oct tests; 98 99(* Test hexadecimal printing *) 100val _ = tprint "Testing output_words_as_hex"; 101val _ = output_words_as_hex(); 102val _ = run_tests tys hex tests; 103 104(* Test padded hexadecimal printing *) 105val _ = tprint "Testing output_words_as_padded_hex"; 106val _ = output_words_as_padded_hex(); 107val _ = run_tests tys padded_hex tests; 108 109(* Test resetting to default printing *) 110val _ = tprint "Testing remove_word_printer"; 111val _ = remove_word_printer(); 112val _ = run_tests tys default tests; 113 114(* Test two's complement printing printer *) 115val _ = tprint "Testing two's complement printing"; 116val _ = set_trace "word pp as 2's comp" 1; 117val _ = run_tests tys_neg default_neg tests; 118 119val _ = output_words_as_dec(); 120val _ = run_tests tys_neg dec_neg tests; 121 122val _ = output_words_as_bin(); 123val _ = run_tests tys_neg bin_neg tests; 124 125val _ = output_words_as_padded_bin(); 126val _ = run_tests tys_neg padded_bin_neg tests; 127 128val _ = output_words_as_oct(); 129val _ = run_tests tys_neg oct_neg tests; 130 131val _ = output_words_as_hex(); 132val _ = run_tests tys_neg hex_neg tests; 133 134val _ = output_words_as_padded_hex(); 135val _ = run_tests tys_neg padded_hex_neg tests; 136 137val _ = export_theory(); 138 139