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