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