388 else (Pretty.fbrk :: Pretty.str ("Evaluated terms:") :: |
388 else (Pretty.fbrk :: Pretty.str ("Evaluated terms:") :: |
389 map (fn (t, u) => |
389 map (fn (t, u) => |
390 Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, |
390 Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1, |
391 Syntax.pretty_term ctxt u]) (rev eval_terms)))); |
391 Syntax.pretty_term ctxt u]) (rev eval_terms)))); |
392 |
392 |
393 fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors, |
|
394 satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) = |
|
395 let |
|
396 fun pretty_stat s i = Pretty.block ([Pretty.str (s ^ ": " ^ string_of_int i)]) |
|
397 in |
|
398 ([pretty_stat "iterations" iterations, |
|
399 pretty_stat "match exceptions" raised_match_errors] |
|
400 @ map_index |
|
401 (fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n) |
|
402 satisfied_assms |
|
403 @ [pretty_stat "positive conclusion tests" positive_concl_tests]) |
|
404 end |
|
405 |
|
406 fun pretty_timings timings = |
|
407 Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" :: |
|
408 maps (fn (label, time) => |
|
409 Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings)) |
|
410 |
|
411 (* Isar commands *) |
393 (* Isar commands *) |
412 |
394 |
413 fun read_nat s = case (Library.read_int o Symbol.explode) s |
395 fun read_nat s = case (Library.read_int o Symbol.explode) s |
414 of (k, []) => if k >= 0 then k |
396 of (k, []) => if k >= 0 then k |
415 else error ("Not a natural number: " ^ s) |
397 else error ("Not a natural number: " ^ s) |