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