# HG changeset patch # User wenzelm # Date 1369943821 -7200 # Node ID 490860e0fbe243a4d893de3ddf876b80bfe99e76 # Parent 9e97fd77a879c25c31b02f2cc0481a699b7fd976 tuned; diff -r 9e97fd77a879 -r 490860e0fbe2 src/HOL/Spec_Check/output_style.ML --- a/src/HOL/Spec_Check/output_style.ML Thu May 30 21:50:09 2013 +0200 +++ b/src/HOL/Spec_Check/output_style.ML Thu May 30 21:57:01 2013 +0200 @@ -7,117 +7,108 @@ signature OUTPUT_STYLE = sig - val setup: theory -> theory + val setup : theory -> theory end -structure Output_Style: OUTPUT_STYLE = +structure Output_Style : OUTPUT_STYLE = struct (* perl style *) -local +val perl_style = + Spec_Check.register_style "Perl" + (fn ctxt => fn tag => + let + val target = Config.get ctxt Spec_Check.gen_target + val namew = Config.get ctxt Spec_Check.column_width + val sort_examples = Config.get ctxt Spec_Check.sort_examples + val show_stats = Config.get ctxt Spec_Check.show_stats + val limit = Config.get ctxt Spec_Check.examples -fun new ctxt tag = - let - val target = Config.get ctxt Spec_Check.gen_target - val namew = Config.get ctxt Spec_Check.column_width - val sort_examples = Config.get ctxt Spec_Check.sort_examples - val show_stats = Config.get ctxt Spec_Check.show_stats - val limit = Config.get ctxt Spec_Check.examples + val resultw = 8 + val countw = 20 + val allw = namew + resultw + countw + 2 - val resultw = 8 - val countw = 20 - val allw = namew + resultw + countw + 2 - - val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I + val maybe_sort = if sort_examples then sort (int_ord o pairself size) else I - fun result ({count=0,...}, _) _ = "dubious" - | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" - | result ({count,tags,...}, badobjs) true = - if not (null badobjs) then "FAILED" - else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" - else "ok" + fun result ({count=0,...}, _) _ = "dubious" + | result (_ : Property.stats, badobjs) false = if null badobjs then "ok" else "FAILED" + | result ({count,tags,...}, badobjs) true = + if not (null badobjs) then "FAILED" + else if AList.defined (op =) tags "__GEN" andalso count < target then "dubious" + else "ok" - fun ratio (0, _) = "(0/0 passed)" - | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)" - | ratio (count, n) = "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)" + fun ratio (0, _) = "(0/0 passed)" + | ratio (count, 0) = "(" ^ string_of_int count ^ " passed)" + | ratio (count, n) = "(" ^ string_of_int (count - n) ^ "/" ^ string_of_int count ^ " passed)" - fun update (stats, badobjs) donep = - "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^ - StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^ - StringCvt.padRight #" " countw (ratio (#count stats, length badobjs)) - - fun status (_, result, (stats, badobjs)) = - if Property.failure result then writeln (update (stats, badobjs) false) else () + fun update (stats, badobjs) donep = + "\r" ^ StringCvt.padRight #"." namew tag ^ "." ^ + StringCvt.padRight #" " resultw (result (stats, badobjs) donep) ^ + StringCvt.padRight #" " countw (ratio (#count stats, length badobjs)) - fun prtag count (tag, n) first = - if String.isPrefix "__" tag then ("", first) - else - let - val ratio = round ((real n / real count) * 100.0) - in - (((if first then "" else StringCvt.padRight #" " allw "\n") ^ - StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag), - false) - end + fun status (_, result, (stats, badobjs)) = + if Property.failure result then writeln (update (stats, badobjs) false) else () - fun prtags ({count, tags, ...} : Property.stats) = - if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else "" + fun prtag count (tag, n) first = + if String.isPrefix "__" tag then ("", first) + else + let + val ratio = round ((real n / real count) * 100.0) + in + (((if first then "" else StringCvt.padRight #" " allw "\n") ^ + StringCvt.padLeft #" " 3 (string_of_int ratio) ^ "% " ^ tag), + false) + end + + fun prtags ({count, tags, ...} : Property.stats) = + if show_stats then cat_lines (fst (fold_map (prtag count) tags true)) else "" - fun err badobjs = - let - fun iter [] _ = () - | iter (e :: es) k = - (writeln (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^ - StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e); - iter es (k + 1)) - in - iter (maybe_sort (take limit (map_filter I badobjs))) 0 - end + fun err badobjs = + let + fun iter [] _ = () + | iter (e :: es) k = + (writeln (StringCvt.padLeft #" " namew (if k > 0 then "" else "counter-examples") ^ + StringCvt.padRight #" " resultw (if k > 0 then "" else ":") ^ e); + iter es (k + 1)) + in + iter (maybe_sort (take limit (map_filter I badobjs))) 0 + end - fun finish (stats, badobjs) = - if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats) - else (writeln (update (stats, badobjs) true); err badobjs) - in - {status = status, finish = finish} - end - -in - val perl_style = Spec_Check.register_style ("Perl", new) -end + fun finish (stats, badobjs) = + if null badobjs then writeln (update (stats, badobjs) true ^ prtags stats) + else (writeln (update (stats, badobjs) true); err badobjs) + in + {status = status, finish = finish} + end) (* CM style: meshes with CM output; highlighted in sml-mode *) -local - -fun pad wd = StringCvt.padLeft #"0" wd o Int.toString - -fun new ctxt tag = - let - val gen_target = Config.get ctxt Spec_Check.gen_target - val _ = writeln ("[testing " ^ tag ^ "... ") - fun finish ({count, ...}, badobjs) = - (case (count, badobjs) of - (0, []) => writeln ("no valid cases generated]") - | (n, []) => writeln ( - if n >= gen_target then "ok]" - else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]") - | (_, es) => - let - val wd = size (string_of_int (length es)) - fun each (NONE, _) = () - | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e) - in - (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ()) - end) - in - {status = K (), finish = finish} - end - -in - val cm_style = Spec_Check.register_style ("CM", new) -end +val cm_style = + Spec_Check.register_style "CM" + (fn ctxt => fn tag => + let + fun pad wd = StringCvt.padLeft #"0" wd o Int.toString + val gen_target = Config.get ctxt Spec_Check.gen_target + val _ = writeln ("[testing " ^ tag ^ "... ") + fun finish ({count, ...}, badobjs) = + (case (count, badobjs) of + (0, []) => writeln ("no valid cases generated]") + | (n, []) => writeln ( + if n >= gen_target then "ok]" + else "ok on " ^ string_of_int n ^ "; " ^ string_of_int gen_target ^ " required]") + | (_, es) => + let + val wd = size (string_of_int (length es)) + fun each (NONE, _) = () + | each (SOME e, i) = writeln (tag ^ ":" ^ pad wd i ^ ".0 Error: " ^ e) + in + (writeln "FAILED]"; map each (es ~~ (1 upto (length es))); ()) + end) + in + {status = K (), finish = finish} + end) (* setup *) diff -r 9e97fd77a879 -r 490860e0fbe2 src/HOL/Spec_Check/spec_check.ML --- a/src/HOL/Spec_Check/spec_check.ML Thu May 30 21:50:09 2013 +0200 +++ b/src/HOL/Spec_Check/spec_check.ML Thu May 30 21:57:01 2013 +0200 @@ -19,7 +19,7 @@ {status : string option * Property.result * (Property.stats * string option list) -> unit, finish: Property.stats * string option list -> unit} - val register_style : (string * output_style) -> theory -> theory + val register_style : string -> output_style -> theory -> theory val checkGen : Proof.context -> 'a Generator.gen * ('a -> string) option -> string * 'a Property.prop -> unit @@ -65,7 +65,7 @@ | NONE => error ("No style called " ^ quote name ^ " found")) end -fun register_style (name, style) = Style.map (Symtab.update (name, style)) +fun register_style name style = Style.map (Symtab.update (name, style)) (* testing functions *)