author | wenzelm |
Mon, 25 Mar 2019 17:21:26 +0100 | |
changeset 69981 | 3dced198b9ec |
parent 59058 | a78612c67ec0 |
permissions | -rw-r--r-- |
53164
beb4ee344c22
clarified position of Spec_Check for Isabelle/ML -- it is unrelated to Isabelle/HOL;
wenzelm
parents:
52277
diff
changeset
|
1 |
(* Title: Tools/Spec_Check/output_style.ML |
52248
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 |
|
53165 | 8 |
structure Output_Style : sig end = |
52248
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 |
|
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
11 |
(* perl style *) |
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
12 |
|
52258 | 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 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
22 |
|
52258 | 23 |
val resultw = 8 |
24 |
val countw = 20 |
|
25 |
val allw = namew + resultw + countw + 2 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
26 |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
53171
diff
changeset
|
27 |
val maybe_sort = if sort_examples then sort (int_ord o apply2 size) else I |
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
28 |
|
52277 | 29 |
fun result ({count = 0, ...}, _) _ = "dubious" |
52258 | 30 |
| result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" |
52277 | 31 |
| result ({count, tags}, badobjs) true = |
52258 | 32 |
if not (null badobjs) then "FAILED" |
33 |
else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" |
|
34 |
else "ok" |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
35 |
|
52258 | 36 |
fun ratio (0, _) = "(0/0 passed)" |
37 |
| ratio (count, 0) = "(" ^ string_of_int count ^ " passed)" |
|
52261 | 38 |
| ratio (count, n) = |
39 |
"(" ^ 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
|
40 |
|
52258 | 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)) |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
45 |
|
52258 | 46 |
fun status (_, result, (stats, badobjs)) = |
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
47 |
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
|
48 |
|
52258 | 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 |
||
52277 | 60 |
fun prtags ({count, tags} : Property.stats) = |
52258 | 61 |
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
|
62 |
|
52258 | 63 |
fun err badobjs = |
64 |
let |
|
65 |
fun iter [] _ = () |
|
66 |
| iter (e :: es) k = |
|
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
67 |
(warning (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^ |
52258 | 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 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
73 |
|
52258 | 74 |
fun finish (stats, badobjs) = |
75 |
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
|
76 |
else (warning (update (stats, badobjs) true); err badobjs) |
52258 | 77 |
in |
78 |
{status = status, finish = finish} |
|
79 |
end) |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
80 |
|
53171 | 81 |
val _ = Theory.setup perl_style; |
82 |
||
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
83 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
84 |
(* 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
|
85 |
|
52258 | 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 ^ "... ") |
|
52277 | 93 |
fun finish ({count, ...} : Property.stats, badobjs) = |
52258 | 94 |
(case (count, badobjs) of |
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
95 |
(0, []) => warning ("no valid cases generated]") |
52258 | 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, _) = () |
|
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
103 |
| each (SOME e, i) = warning (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e) |
52258 | 104 |
in |
52264
cdba0c3cb4c2
tuned messages -- some attempts to observe Isabelle output channel semantics;
wenzelm
parents:
52261
diff
changeset
|
105 |
(warning "FAILED]"; map each (es ~~ (1 upto (length es))); ()) |
52258 | 106 |
end) |
107 |
in |
|
108 |
{status = K (), finish = finish} |
|
109 |
end) |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
110 |
|
53171 | 111 |
val _ = Theory.setup cm_style; |
52254
994055f7db80
simplified context and data management -- plain ctxt: Proof.context is default for most operations;
wenzelm
parents:
52253
diff
changeset
|
112 |
|
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
113 |
end |