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