src/Tools/Spec_Check/output_style.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 months ago)
changeset 69981 3dced198b9ec
parent 59058 a78612c67ec0
permissions -rw-r--r--
more strict AFP properties;
     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