1structure Trace :> Trace = 2struct 3open Feedback boolSyntax Rsyntax Abbrev; 4 5val print_term = Lib.say o Parse.term_to_string 6val print_thm = Parse.print_thm 7val concl = Thm.concl 8val say = Lib.say 9 10 (* --------------------------------------------------------------------- 11 * Tracing utilities 12 * ---------------------------------------------------------------------*) 13 14 datatype action = 15 LZ_TEXT of unit -> string 16 | TEXT of string 17 | REDUCE of (string * Term.term) 18 | REWRITING of (Term.term * Thm.thm) 19 | SIDECOND_ATTEMPT of Term.term 20 | SIDECOND_SOLVED of Thm.thm 21 | SIDECOND_NOT_SOLVED of Term.term 22 | OPENING of (Term.term * Thm.thm) 23 | PRODUCE of (Term.term * string * Thm.thm) 24 | IGNORE of (string * Thm.thm) 25 | MORE_CONTEXT of Thm.thm; 26 27 val trace_hook : ((int * action) -> unit) ref = ref (fn (n,s) => ()); 28 fun trace x = (!trace_hook) x 29 30val trace_level = ref 0; 31val _ = Feedback.register_trace("simplifier", trace_level, 7); 32 33fun tty_trace (LZ_TEXT fs) = (say " "; say (fs ()); say "\n") 34 | tty_trace (TEXT s) = (say " "; say s; say "\n") 35 | tty_trace (REDUCE (s,tm)) = (say " "; say s; say " "; print_term tm; say "\n") 36 | tty_trace (REWRITING (tm,thm)) = 37 (say " rewriting "; print_term tm; say " with "; print_thm thm; say "\n") 38 | tty_trace (SIDECOND_ATTEMPT tm) = 39 (say " trying to solve: "; print_term tm; say "\n") 40 | tty_trace (SIDECOND_SOLVED thm) = 41 (say " solved! "; print_thm thm; say "\n") 42 | tty_trace (SIDECOND_NOT_SOLVED tm) = 43 (say " couldn't solve: "; print_term tm; say "\n") 44 | tty_trace (OPENING (tm,thm)) = 45 (say " "; print_term tm; say " matches congruence rule "; print_thm thm; say "\n") 46 | tty_trace (PRODUCE (tm,s,thm)) = 47 (say " "; print_term tm; say " via "; say s; say " simplifies to: "; 48 print_term (rhs (concl thm)) handle HOL_ERR _ => print_thm thm; say "\n") 49 | tty_trace (IGNORE (s,thm)) = 50 (say " Ignoring "; say s; say " rewrite\n "; print_thm thm; say "\n") 51 | tty_trace (MORE_CONTEXT thm) = 52 (say " more context: "; print_thm thm; say "\n"); 53 54(* hol_clock is sometimes a small amount of time in the future under Poly/ML, 55 presumably a consequence of being stored in a heap. 56*) 57fun fudge t = Time.+(t, Time.fromSeconds 10) 58 59val _ = trace_hook := 60 (fn (n,a) => if (n <= !trace_level) then 61 (say "["; 62 say ((Arbnum.toString o #usec o Portable.dest_time o 63 fudge) 64 (#usr (Timer.checkCPUTimer Globals.hol_clock))); 65 say "]: "; 66 tty_trace a) 67 else ()) 68 69end (* struct *) 70