1(* ========================================================================= *)
2(* METERING TIME AND INFERENCES                                              *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6(*
7app load
8 ["mlibUseful", "Mosml", "mlibTerm", "mlibThm", "mlibCanon", "mlibMatch"];
9*)
10
11(*
12*)
13structure mlibMeter :> mlibMeter =
14struct
15
16open mlibUseful;
17
18(* ------------------------------------------------------------------------- *)
19(* Search limits                                                             *)
20(* ------------------------------------------------------------------------- *)
21
22type limit = {time : real option, infs : int option};
23
24val unlimited = {time = NONE, infs = NONE};
25
26val expired = {time = SOME 0.0, infs = SOME 0};
27
28fun pp_limit {time,infs} =
29  let
30    open PP
31  in
32    block INCONSISTENT 1 [
33      add_string "{",
34      block INCONSISTENT 2 [
35        add_string "time =", add_break (1,0),
36        case time of
37            NONE => add_string "unlimited"
38          | SOME t => add_string (Real.fmt (StringCvt.FIX (SOME 3)) t)
39      ],
40      add_string ",", add_break (1,0),
41      block INCONSISTENT 2 [
42        add_string "infs =", add_break (1,0),
43        case infs of NONE => add_string "unlimited"
44                   | SOME i => add_string (int_to_string i)
45      ],
46      add_string "}"
47    ]
48  end;
49
50fun limit_to_string l = PP.pp_to_string (!LINE_LENGTH) pp_limit l;
51
52(* ------------------------------------------------------------------------- *)
53(* mlibMeter readings.                                                           *)
54(* ------------------------------------------------------------------------- *)
55
56type meter_reading = {time : real, infs : int};
57
58val zero_reading = {time = 0.0, infs = 0};
59
60fun add_readings {time : real, infs} {time = time', infs = infs'} =
61  {time = time + time', infs = infs + infs'};
62
63val pp_meter_reading =
64  pp_map (fn {time,infs} => {time = SOME time, infs = SOME infs}) pp_limit;
65
66fun meter_reading_to_string r =
67  PP.pp_to_string (!LINE_LENGTH) pp_meter_reading r;
68
69(* ------------------------------------------------------------------------- *)
70(* mlibMeters record time and inferences.                                        *)
71(* ------------------------------------------------------------------------- *)
72
73type meter =
74  {rdt : unit -> real, rdi : unit -> int, log : (int -> unit), lim : limit};
75
76fun new_time_meter () =
77  let
78    val tmr = Timer.startCPUTimer ()
79    fun read () =
80      (fn {usr,sys,...} => Time.+ (usr,sys))
81      (Timer.checkCPUTimer tmr)
82  in
83    pos o Time.toReal o read
84  end;
85
86fun new_inference_meter () =
87  let
88    val infs = ref 0
89    fun read () = !infs
90  in
91    (read, fn n => infs := !infs + n) (* OK *)
92  end;
93
94fun new_meter lim : meter =
95  let val (rdi,log) = new_inference_meter ()
96  in {rdt = new_time_meter (), rdi = rdi, log = log, lim = lim}
97  end;
98
99fun sub_meter ({rdt, rdi, log, lim = _} : meter) lim =
100  let
101    val init_time = rdt () and init_infs = rdi ()
102    fun sbt time = pos (time - init_time)
103    fun sbi infs = infs - init_infs
104  in
105    {rdt = sbt o rdt, rdi = sbi o rdi, log = log, lim = lim}
106  end;
107
108fun record_infs ({log,...} : meter) = log;
109
110fun read_infs ({rdi,...} : meter) = rdi ();
111
112fun read_meter ({rdt,rdi,...} : meter) = {time = rdt (), infs = rdi ()};
113
114fun check_meter ({rdt, rdi, lim = {time, infs}, ...} : meter) =
115  (case time of NONE => true | SOME time => rdt () < time) andalso
116  (case infs of NONE => true | SOME infs => rdi () < infs);
117
118val pp_meter = pp_map read_meter pp_meter_reading;
119
120end
121