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