author | wenzelm |
Fri, 31 May 2013 11:56:48 +0200 | |
changeset 52277 | 2bbeab01c0ea |
parent 52264 | cdba0c3cb4c2 |
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 |
|
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
8 |
signature OUTPUT_STYLE = |
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
9 |
sig |
52258 | 10 |
val setup : theory -> theory |
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
11 |
end |
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
12 |
|
52258 | 13 |
structure Output_Style : OUTPUT_STYLE = |
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
14 |
struct |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
15 |
|
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
16 |
(* perl style *) |
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
17 |
|
52258 | 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 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
27 |
|
52258 | 28 |
val resultw = 8 |
29 |
val countw = 20 |
|
30 |
val allw = namew + resultw + countw + 2 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
31 |
|
52258 | 32 |
val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I |
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
33 |
|
52277 | 34 |
fun result ({count = 0, ...}, _) _ = "dubious" |
52258 | 35 |
| result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" |
52277 | 36 |
| result ({count, tags}, badobjs) true = |
52258 | 37 |
if not (null badobjs) then "FAILED" |
38 |
else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" |
|
39 |
else "ok" |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
40 |
|
52258 | 41 |
fun ratio (0, _) = "(0/0 passed)" |
42 |
| ratio (count, 0) = "(" ^ string_of_int count ^ " passed)" |
|
52261 | 43 |
| ratio (count, n) = |
44 |
"(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)" |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
45 |
|
52258 | 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)) |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
50 |
|
52258 | 51 |
fun status (_, result, (stats, badobjs)) = |
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
52 |
if Property.failure result then warning (update (stats, badobjs) false) else () |
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
53 |
|
52258 | 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 |
||
52277 | 65 |
fun prtags ({count, tags} : Property.stats) = |
52258 | 66 |
if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else "" |
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
67 |
|
52258 | 68 |
fun err badobjs = |
69 |
let |
|
70 |
fun iter [] _ = () |
|
71 |
| iter (e :: es) k = |
|
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
72 |
(warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^ |
52258 | 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 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
78 |
|
52258 | 79 |
fun finish (stats, badobjs) = |
80 |
if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats) |
|
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
81 |
else (warning (update (stats, badobjs) true); err badobjs) |
52258 | 82 |
in |
83 |
{status = status, finish = finish} |
|
84 |
end) |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
85 |
|
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
86 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
87 |
(* 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
|
88 |
|
52258 | 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 ^ "... ") |
|
52277 | 96 |
fun finish ({count, ...} : Property.stats, badobjs) = |
52258 | 97 |
(case (count, badobjs) of |
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
98 |
(0, []) => warning ("no valid cases generated]") |
52258 | 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, _) = () |
|
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
106 |
| each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e) |
52258 | 107 |
in |
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
108 |
(warning "FAILED]"; map each (es ~~ (1 upto (length es))); ()) |
52258 | 109 |
end) |
110 |
in |
|
111 |
{status = K (), finish = finish} |
|
112 |
end) |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
113 |
|
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
114 |
|
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
115 |
(* setup *) |
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
116 |
|
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
117 |
val setup = perl_style #> cm_style |
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
118 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
119 |
end |