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 open Uref 89 val infs = Uref.new 0 90 fun read () = !infs 91 in 92 (read, fn n => infs := !infs + n) (* OK *) 93 end; 94 95fun new_meter lim : meter = 96 let val (rdi,log) = new_inference_meter () 97 in {rdt = new_time_meter (), rdi = rdi, log = log, lim = lim} 98 end; 99 100fun sub_meter ({rdt, rdi, log, lim = _} : meter) lim = 101 let 102 val init_time = rdt () and init_infs = rdi () 103 fun sbt time = pos (time - init_time) 104 fun sbi infs = infs - init_infs 105 in 106 {rdt = sbt o rdt, rdi = sbi o rdi, log = log, lim = lim} 107 end; 108 109fun record_infs ({log,...} : meter) = log; 110 111fun read_infs ({rdi,...} : meter) = rdi (); 112 113fun read_meter ({rdt,rdi,...} : meter) = {time = rdt (), infs = rdi ()}; 114 115fun check_meter ({rdt, rdi, lim = {time, infs}, ...} : meter) = 116 (case time of NONE => true | SOME time => rdt () < time) andalso 117 (case infs of NONE => true | SOME infs => rdi () < infs); 118 119val pp_meter = pp_map read_meter pp_meter_reading; 120 121end 122