1structure dbgTools = struct
2
3local
4
5open Globals HolKernel Parse PrimitiveBddRules DerivedBddRules Binaryset
6
7val dbg = ref 0
8
9val _ = Feedback.register_trace("HolCheckDBG",dbg,3)
10
11val vis = ref (empty String.compare)
12val visp = ref (empty String.compare)
13val visee = ref (empty String.compare)
14val saee = ref false
15val tmcb = ref (Binarymap.mkDict String.compare)
16val tmlcb = ref (Binarymap.mkDict String.compare)
17val thcb = ref (Binarymap.mkDict String.compare)
18val thlcb = ref (Binarymap.mkDict String.compare)
19val sbdd = ref false
20
21fun set_pfx s k = foldr (fn (v,av) => if String.isPrefix v k then true else av) false s
22
23fun show s = (member(!vis,s) orelse set_pfx (!visp) s)
24
25fun showe s f = (!saee orelse member(!visee,s) orelse member(!visee,s^f))
26
27fun printer s p = (print ("["^s^"]\n"); with_flag (show_types,(!dbg)>1) with_flag (show_assums,(!dbg)>2) p (); print "\n")
28
29in
30
31fun DEN s f = if (!dbg)>0 andalso showe s f then print ("\n> > > > > > > > ["^s^"."^f^"]\n") else ()
32fun DEX s f = if (!dbg)>0 andalso showe s f then print ("\n< < < < < < < < ["^s^"."^f^"]\n") else ()
33fun DTM s t = if (!dbg)>0 andalso show s then (printer (s^":TM") (fn _ => print_term t)) else ()
34fun DTH s t = if (!dbg)>0 andalso show s then (printer (s^":TH") (fn _ => print_thm t)) else ()
35fun DTY s t = if (!dbg)>0 andalso show s then (printer (s^":TY") (fn _ => print_type t)) else ()
36fun DST s =   if (!dbg)>0 andalso show s then printer s (fn _ => ()) else ()
37fun DBD s b = if (!dbg)>0 andalso (!sbdd) andalso show s then (printer (s^":BD") (fn _ => bdd.printset b)) else ()
38fun DNM s i = if (!dbg)>0 andalso show s then (printer (s^":NM") (fn _ => print (int_to_string i))) else ()
39fun DTB s t = if (!dbg)>0 andalso show s then (printer (s^":TB") (fn _ => print_term  (getTerm t))) else ()
40
41(* default behaviour is to not show any messages. Use sm/sp to enable single/groups of messages *)
42fun sm s = if (!dbg)>0 then (vis:= add(!vis,s)) else ()  (* unhide messages from s *)
43
44fun sp s = if (!dbg)>0 then (visp := add(!visp,s)) else () (* show all with prefix s *)
45fun hp s = if (!dbg)>0 then (visp := delete(!visp,s)) else () (* hide all with prefix s *)
46
47fun se s = if(!dbg)>0 then (visee := add(!visee,s)) else () (* show entry/exit for these *)
48
49fun he s = if(!dbg)>0 then (visee := delete(!visee,s)) else () (* hide entry/exit for these  *)
50
51fun sae() = if (!dbg)>0 then saee := true else () (* show all entry/exit *)
52
53fun hae() = if (!dbg)>0 then saee := false else () (* show no entry/exit *)
54
55fun sb t = if (!dbg)>0 then sbdd := t else () (* enable/disable DBD calls *)
56
57(* however, after a run, may need to reset to default if rerun is done within same session *)
58fun reset() = if (!dbg)>0 then (vis := (empty String.compare); visp := (empty String.compare);
59                                tmcb := (Binarymap.mkDict String.compare);
60                                thcb := (Binarymap.mkDict String.compare);
61                                thlcb := (Binarymap.mkDict String.compare)
62                                ) else ()
63
64(* allow code to register call backs that I can use after a run to recover run-time values*)
65fun CBTM s tm = if (!dbg)>0  then (tmcb:= (Binarymap.insert(!tmcb,s,Susp.delay (fn _ => (tm:term))))) else ()
66fun cbtm s = if (!dbg)>0 then Susp.force(Binarymap.find(!tmcb,s)) else failwith "No debug info"
67
68fun CBTH s th = if (!dbg)>0  then (thcb:= (Binarymap.insert(!thcb,s,Susp.delay (fn _ => (th:thm))))) else ()
69fun cbth s = if (!dbg)>0 then Susp.force(Binarymap.find(!thcb,s)) else failwith "No debug info"
70
71fun CBTHL s thl = if (!dbg)>0  then (thlcb:= (Binarymap.insert(!thlcb,s,Susp.delay (fn _ => (thl:thm list))))) else ()
72fun cbthl s = if (!dbg)>0 then Susp.force(Binarymap.find(!thlcb,s)) else failwith "No debug info"
73
74fun CBTML s tml = if (!dbg)>0  then (tmlcb:= (Binarymap.insert(!tmlcb,s,Susp.delay (fn _ => (tml:term list))))) else ()
75fun cbtml s = if (!dbg)>0 then Susp.force(Binarymap.find(!tmlcb,s)) else failwith "No debug info"
76
77end
78end
79