formal_ineqs/verifier/interval_m/report.ml

   1 (* =========================================================== *)
   2 (* Report functions                                            *)
   3 (* Author: Thomas C. Hales                                     *)
   4 (* Date: 2011-08-21                                            *)
   5 (* =========================================================== *)
   6
   7 (* port of error.cc
   8     basic procedures to print messages to the standard output
   9    and to count errors.
  10
  11 *)
  12
  13 needs "verifier/interval_m/types.ml";;
  14
  15 module Report = struct
  16
  17 open Interval_types;;
  18
  19 let time_string () =   Printf.sprintf "time(%.0f)" (Sys.time());;
  20
  21 let (get_error_count,reset_error_count,inc_error_count) =
  22   let error_count = ref 0 in
  23     ((fun _ -> !error_count),(fun _ -> error_count := 0),
  24    (fun _ -> error_count:= !error_count + 1));;
  25
  26 let (get_corner_count,reset_corner_count,inc_corner_count) =
  27   let corner_count = ref 0 in
  28     ((fun _ -> !corner_count),(fun _ -> corner_count := 0),
  29    (fun _ -> corner_count:= !corner_count + 1));;
  30
  31 let diagnostic_string () =
  32   let d = get_error_count() in
  33   if (d>0) then Printf.sprintf "(errors %d)" (get_error_count())  else "(no errors)";;
  34
  35 let report s =
  36   Format.print_string s; Format.print_newline(); Format.print_flush();;
  37
  38 let report_timed s = report (s^" "^(time_string()));;
  39
  40 let report_error =
  41   let error_max = 25 in  (* was 200, recurse.cc had a separate counter limit at 25 *)
  42     fun s ->
  43       let ec = get_error_count() in
  44       (inc_error_count(); report_timed (Printf.sprintf "error(%d) --\n%s" ec s);
  45        Pervasives.ignore(get_error_count() < error_max or raise Fatal));;
  46
  47 let report_fatal s =
  48   ( inc_error_count(); report_timed ("error --\n"^s); raise Fatal);;
  49
  50 end;;