1 (* Title: HOL/Spec_Check/output_style.ML |
|
2 Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen |
|
3 Author: Christopher League |
|
4 |
|
5 Output styles for presenting Spec_Check's results. |
|
6 *) |
|
7 |
|
8 signature OUTPUT_STYLE = |
|
9 sig |
|
10 val setup : theory -> theory |
|
11 end |
|
12 |
|
13 structure Output_Style : OUTPUT_STYLE = |
|
14 struct |
|
15 |
|
16 (* perl style *) |
|
17 |
|
18 val perl_style = |
|
19 Spec_Check.register_style "Perl" |
|
20 (fn ctxt => fn tag => |
|
21 let |
|
22 val target = Config.get ctxt Spec_Check.gen_target |
|
23 val namew = Config.get ctxt Spec_Check.column_width |
|
24 val sort_examples = Config.get ctxt Spec_Check.sort_examples |
|
25 val show_stats = Config.get ctxt Spec_Check.show_stats |
|
26 val limit = Config.get ctxt Spec_Check.examples |
|
27 |
|
28 val resultw = 8 |
|
29 val countw = 20 |
|
30 val allw = namew + resultw + countw + 2 |
|
31 |
|
32 val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I |
|
33 |
|
34 fun result ({count = 0, ...}, _) _ = "dubious" |
|
35 | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" |
|
36 | result ({count, tags}, badobjs) true = |
|
37 if not (null badobjs) then "FAILED" |
|
38 else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" |
|
39 else "ok" |
|
40 |
|
41 fun ratio (0, _) = "(0/0 passed)" |
|
42 | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)" |
|
43 | ratio (count, n) = |
|
44 "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)" |
|
45 |
|
46 fun update (stats, badobjs) donep = |
|
47 "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^ |
|
48 StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^ |
|
49 StringCvt.padRight #" " countw (ratio (#count stats, length badobjs)) |
|
50 |
|
51 fun status (_, result, (stats, badobjs)) = |
|
52 if Property.failure result then warning (update (stats, badobjs) false) else () |
|
53 |
|
54 fun prtag count (tag, n) first = |
|
55 if String.isPrefix "__" tag then ("", first) |
|
56 else |
|
57 let |
|
58 val ratio = round ((real n / real count) * 100.0) |
|
59 in |
|
60 (((if first then "" else StringCvt.padRight #" " allw "\n") ^ |
|
61 StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag), |
|
62 false) |
|
63 end |
|
64 |
|
65 fun prtags ({count, tags} : Property.stats) = |
|
66 if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else "" |
|
67 |
|
68 fun err badobjs = |
|
69 let |
|
70 fun iter [] _ = () |
|
71 | iter (e :: es) k = |
|
72 (warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^ |
|
73 StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e); |
|
74 iter es (k + 1)) |
|
75 in |
|
76 iter (maybe_sort (take limit (map_filter I badobjs))) 0 |
|
77 end |
|
78 |
|
79 fun finish (stats, badobjs) = |
|
80 if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats) |
|
81 else (warning (update (stats, badobjs) true); err badobjs) |
|
82 in |
|
83 {status = status, finish = finish} |
|
84 end) |
|
85 |
|
86 |
|
87 (* CM style: meshes with CM output; highlighted in sml-mode *) |
|
88 |
|
89 val cm_style = |
|
90 Spec_Check.register_style "CM" |
|
91 (fn ctxt => fn tag => |
|
92 let |
|
93 fun pad wd = StringCvt.padLeft #"0" wd o Int.toString |
|
94 val gen_target = Config.get ctxt Spec_Check.gen_target |
|
95 val _ = writeln ("[testing " ^ tag ^ "... ") |
|
96 fun finish ({count, ...} : Property.stats, badobjs) = |
|
97 (case (count, badobjs) of |
|
98 (0, []) => warning ("no valid cases generated]") |
|
99 | (n, []) => writeln ( |
|
100 if n >= gen_target then "ok]" |
|
101 else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]") |
|
102 | (_, es) => |
|
103 let |
|
104 val wd = size (string_of_int (length es)) |
|
105 fun each (NONE, _) = () |
|
106 | each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e) |
|
107 in |
|
108 (warning "FAILED]"; map each (es ~~ (1 upto (length es))); ()) |
|
109 end) |
|
110 in |
|
111 {status = K (), finish = finish} |
|
112 end) |
|
113 |
|
114 |
|
115 (* setup *) |
|
116 |
|
117 val setup = perl_style #> cm_style |
|
118 |
|
119 end |
|