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