1structure profTools = 2struct 3 4local 5 6open Binarymap Binaryset 7 8val find = Binarymap.find 9val app = Binarymap.app 10val foldr = Binarymap.foldr 11 12val cnt = ref (mkDict String.compare) (* counters *) 13val tim = ref (mkDict String.compare) (* timers *) 14val hid = ref (empty String.compare) (* hidden *) 15 16val prf = ref false 17 18(* set profile tracing on/off; turn off debugging infrastructure if profiling is switched on *) 19fun set_prf n = 20 let val _ = (prf:= not (n=0)) 21 in if (!prf) then (Feedback.set_trace "HolCheckDBG" 0;Feedback.set_trace "HolCheckDBGLZ" 0) else () end 22 handle _ => ()(* handle is for when dbgTools is unloaded *) 23 24fun get_prf () = if !prf then 1 else 0 25 26val _ = Feedback.register_ftrace("HolCheckPRF",(get_prf,set_prf),1) 27 28(* counters *) 29 30fun incc s = if !prf then let val _ = (cnt:=insert(!cnt,s,1+find(!cnt,s))) handle ex => (cnt:=insert(!cnt,s,1)) in () end else () 31 32fun prc s = if !prf then print (s^".count = "^(Int.toString(find(!cnt,s)))^"\n") else () 33 34fun prlc l = if !prf then List.app prc l else () 35 36fun prac() = if !prf then app (fn (s,c) => prc s) (!cnt) else () 37 38fun resc s = if !prf then (cnt := (insert(!cnt,s,0))) else () 39 40fun reslc l = if !prf then List.app resc l else () 41 42fun resac() = if !prf then (cnt := (mkDict String.compare)) else () 43 44in 45 46(* timers (also have their own call count and inference count) *) 47 48local open Timer Real Count in 49 50local open Int in fun addI x y = x + y end (*FIXME: stupid hack to access Int.+ *) 51 52(* start timer s, if already present, do not reset the aggregates *) 53fun bgt s = if !prf then let val (t,mtr,(utot,stot,gtot),ptot) = find(!tim,s) 54 in ((tim := insert(!tim,s,(startCPUTimer(),Count.mk_meter(),(utot,stot,gtot),ptot))); incc s) end 55 handle ex => ((tim := insert(!tim,s,(startCPUTimer(),Count.mk_meter(),(0.0,0.0,0.0),0))); incc s) 56 else () 57 58(* update aggregates for timer s *) 59fun ent s = 60 if !prf then let val (t,mtr,(utot,stot,gtot),ptot) = find(!tim,s) handle ex => Feedback.failwith("profTools.ent: Not Found") 61 val {usr=ut,sys=st} = checkCPUTimer t 62 val gt = checkGCTime t 63 val {prims=p,...} = read mtr 64 in (tim := insert(!tim,s,(t,mtr,(utot+(Time.toReal ut),stot+(Time.toReal st),gtot+(Time.toReal gt)),addI ptot p))) end 65 else () 66 67fun prt s = (* print info for timer s if not hidden*) 68 if !prf 69 then if not (member(!hid,s)) 70 then let val (_,_,(utot,stot,gtot),ptot) = find(!tim,s) 71 val _ = print (StringCvt.padRight #" " 25 s) 72 val _ = print ("count = "^(Int.toString(find(!cnt,s)))^"\t") 73 val _ = print ("time=("^(fmt (StringCvt.FIX (SOME 3)) utot)^","^(fmt (StringCvt.FIX (SOME 3)) stot)^","^ 74 (fmt (StringCvt.FIX (SOME 3)) gtot)^")\t\t") 75 val _ = print ("total="^(fmt (StringCvt.FIX (SOME 3)) (utot+stot))^"\t") 76 val avg = (fmt (StringCvt.FIX (SOME 4)) ((utot+stot)/(fromInt(find(!cnt,s))))) handle Div => "NA" 77 val _ = print ("avg = "^avg^"\t") 78 val _ = print ("inf = "^Int.toString(ptot)^"\n") 79 in () end 80 else () 81 else () 82 83fun prlt l = if !prf then List.app prt l else () (* print list of visible timers *) 84 85fun prat() = if !prf then app (fn (s,c) => prt s) (!tim) else () (* print all visible timers *) 86 87(* print all visible timers, sorting on nth column (skipping the times triple column) *) 88fun sprat n = 89 if (!prf) then 90 let val comp_fun = fn ((s1,(_,_,(utot1,stot1,gtot1),ptot1,avg1)),(s2,(_,_,(utot2,stot2,gtot2),ptot2,avg2))) => 91 case n of 92 0 => String.compare (s1,s2) 93 | 1 => Int.compare (find(!cnt,s1),find(!cnt,s2)) 94 | 2 => Real.compare(utot1+stot1,utot2+stot2) 95 | 3 => Real.compare(avg1,avg2) 96 | 4 => Int.compare(ptot1,ptot2) 97 | _ => String.compare (s1,s2) 98 val l = List.map (fn (s,(t,mt,(utot,stot,gtot),ptot)) => 99 (s,(t,mt,(utot,stot,gtot),ptot,(utot+stot)/(fromInt(find(!cnt,s)))))) 100 (Binarymap.listItems (!tim)) 101 val sl = Listsort.sort comp_fun l 102 in List.app (fn (s,c) => prt s) sl end 103 else () 104 105fun rest s = if !prf then ((tim := insert(!tim,s,(startCPUTimer(),Count.mk_meter(),(0.0,0.0,0.0),0))); resc s) else () (* reset *) 106 107fun reslt l = if !prf then List.app rest l else () (* reset list *) 108 109fun resat() = if !prf then ((tim := (mkDict String.compare)); resac()) else () (* reset all*) 110 111fun ht s =if !prf then (hid := add(!hid,s)) else () (* hide timer s *) 112 113fun uht s = if !prf then (hid := delete(!hid,s)) else () handle NotFound => () (* unhide timer *) 114 115fun hp s = if !prf (*hide prefix*) 116 then (hid := (foldr (fn (k,_,st) => if String.isPrefix s k then add(st,k) else st) (!hid) (!tim))) 117 else () 118 119fun uhp s = if !prf (*unhide prefix*) 120 then (hid := (foldl (fn (k,st) => if String.isPrefix s k then delete(st,k) else st) (!hid) (!hid))) 121 else () 122 123fun ha() = if !prf then (hid := (foldr (fn (k,_,st) => add(st,k)) (!hid) (!tim))) else () (* hide all *) 124 125fun uha() = if !prf then (hid := (empty String.compare)) else () (* unhide all *) 126 127fun sp s = if !prf then (ha(); uhp s) else () (*hide all but those with prefix s *) 128 129fun prap s = if !prf then (sp s;prat()) else () (* print only the ones with prefix s *) 130 131fun prapl l = if !prf then (List.app sp l;prat()) else () (* print only the ones with prefixes in l *) 132 133end 134 135end 136end 137