1(* ===================================================================== *)
2(* FILE          : Feedback.sml                                          *)
3(* DESCRIPTION   : HOL exceptions, messages, warnings, and traces.       *)
4(*                                                                       *)
5(* AUTHOR        : (c) Konrad Slind, University of Cambridge             *)
6(* DATE          : October 1, 2000 Konrad Slind                          *)
7(* HISTORY       : Derived from Exception module, plus generalized       *)
8(*                 tracing stuff from Michael Norrish.                   *)
9(* ===================================================================== *)
10
11structure Feedback :> Feedback =
12struct
13
14type error_record = {origin_structure : string,
15                     origin_function  : string,
16                     message          : string}
17
18exception HOL_ERR of error_record
19
20(*---------------------------------------------------------------------------
21     Curried version of HOL_ERR; can be more comfortable to use.
22 ---------------------------------------------------------------------------*)
23
24fun mk_HOL_ERR s1 s2 s3 =
25   HOL_ERR {origin_structure = s1,
26            origin_function = s2,
27            message = s3}
28
29(* Errors with a known location. *)
30
31fun mk_HOL_ERRloc s1 s2 locn s3 =
32   HOL_ERR {origin_structure = s1,
33            origin_function = s2,
34            message = locn.toString locn ^ ":\n" ^ s3}
35  (* Would like to be much cleverer, adding a field
36     source_location:locn to error_record, but the pain of fixing all
37     occurrences of HOL_ERR would be too great. *)
38
39val ERR = mk_HOL_ERR "Feedback"  (* local to this file *)
40
41(*---------------------------------------------------------------------------
42     Misc. utilities
43 ---------------------------------------------------------------------------*)
44
45fun quote s = String.concat ["\"", s, "\""]
46
47fun assoc1 item =
48   let
49      fun assc ((e as (key, _)) :: rst) =
50            if item = key then SOME e else assc rst
51        | assc [] = NONE
52   in
53      assc
54   end
55
56(*---------------------------------------------------------------------------*
57 * Controlling the display of exceptions, messages, and warnings.            *
58 *---------------------------------------------------------------------------*)
59
60val emit_ERR     = ref true
61val emit_MESG    = ref true
62val emit_WARNING = ref true
63val WARNINGs_as_ERRs = ref false
64
65fun out strm s = (TextIO.output(strm, s); TextIO.flushOut strm)
66
67val ERR_outstream     = ref (out TextIO.stdErr)
68val MESG_outstream    = ref (out TextIO.stdOut)
69val WARNING_outstream = ref (out TextIO.stdOut)
70
71fun quiet_warnings f = Portable.with_flag (emit_WARNING, false) f
72fun quiet_messages f = Portable.with_flag (emit_MESG, false) f
73
74(*---------------------------------------------------------------------------*
75 * Formatting and output for exceptions, messages, and warnings.             *
76 *---------------------------------------------------------------------------*)
77
78fun format_err_rec {message, origin_function, origin_structure} =
79   String.concat
80      ["at ", origin_structure, ".", origin_function, ":\n", message]
81
82fun format_ERR err_rec =
83   String.concat ["\nException raised ", format_err_rec err_rec, "\n"]
84
85fun format_MESG s = String.concat ["<<HOL message: ", s, ">>\n"]
86
87fun format_WARNING structName fnName mesg =
88   String.concat
89      ["<<HOL warning: ", structName, ".", fnName, ": ", mesg, ">>\n"]
90
91val ERR_to_string     = ref format_ERR
92val MESG_to_string    = ref format_MESG
93val WARNING_to_string = ref format_WARNING
94
95fun output_ERR s = if !emit_ERR then !ERR_outstream s else ()
96
97(*---------------------------------------------------------------------------
98    Makes an informative message from an exception. Subtlety: if we see
99    that the exception is an Interrupt, we raise it.
100 ---------------------------------------------------------------------------*)
101
102fun exn_to_string (HOL_ERR sss) = !ERR_to_string sss
103  | exn_to_string Portable.Interrupt = raise Portable.Interrupt
104  | exn_to_string e = General.exnMessage e
105
106fun Raise e = (output_ERR (exn_to_string e); raise e)
107
108local
109   val err1 = mk_HOL_ERR "??" "??" "fail"
110   val err2 = mk_HOL_ERR "??" "failwith"
111in
112   fun fail () = raise err1
113   fun failwith s = raise (err2 s)
114end
115
116(*---------------------------------------------------------------------------
117    Takes an exception, grabs its message as best as possible, then
118    make a HOL exception out of it. Subtlety: if we see that the
119    exception is an Interrupt, we raise it.
120 ---------------------------------------------------------------------------*)
121
122fun wrap_exn s f Portable.Interrupt = raise Portable.Interrupt
123  | wrap_exn s f (HOL_ERR err_rec) = mk_HOL_ERR s f (format_err_rec err_rec)
124  | wrap_exn s f exn = mk_HOL_ERR s f (General.exnMessage exn)
125
126fun wrap_exn_loc s f l Portable.Interrupt = raise Portable.Interrupt
127  | wrap_exn_loc s f l (HOL_ERR err_rec) =
128      mk_HOL_ERRloc s f l (format_err_rec err_rec)
129  | wrap_exn_loc s f l exn = mk_HOL_ERRloc s f l (General.exnMessage exn)
130
131fun HOL_MESG s =
132  if !emit_MESG then !MESG_outstream (!MESG_to_string s) else ()
133
134fun HOL_PROGRESS_MESG (start, finish) f x =
135   if !emit_MESG then
136     let
137     in
138       !MESG_outstream ("<<HOL message: " ^ start);
139       f x before
140       !MESG_outstream (finish ^ ">>\n")
141     end
142   else f x
143
144fun HOL_WARNING s1 s2 s3 =
145    if !WARNINGs_as_ERRs then raise mk_HOL_ERR s1 s2 s3
146    else if !emit_WARNING then
147      !WARNING_outstream (!WARNING_to_string s1 s2 s3)
148    else ()
149
150fun HOL_WARNINGloc s1 s2 locn s3 =
151   HOL_WARNING s1 s2 (locn.toString locn ^ " :\n" ^ s3)
152
153(*---------------------------------------------------------------------------*
154 * Traces, numeric flags; the higher setting, the more verbose the output.   *
155 *---------------------------------------------------------------------------*)
156
157datatype tracefns = TRFP of {get: unit -> int, set: int -> unit}
158fun trfp_set (TRFP {set, ...}) = set
159fun trfp_get (TRFP {get, ...}) = get ()
160
161fun ref2trfp r = TRFP {get = (fn () => !r), set = (fn i => r := i)}
162
163type trace_record = {
164  aliases : string list,
165  value: tracefns,
166  default: int,
167  maximum: int
168}
169
170datatype TI = TR of trace_record | ALIAS of string
171
172val trace_map =
173    ref (Binarymap.mkDict String.compare : (string,TI)Binarymap.dict)
174
175fun find_record n =
176  case Binarymap.peek (!trace_map, n) of
177      NONE => NONE
178    | SOME (TR tr) => SOME tr
179    | SOME (ALIAS a) => find_record a
180
181val WARN = HOL_WARNING "Feedback"
182
183fun register_trace (nm, r, max) =
184   if !r < 0 orelse max < 0
185      then raise ERR "register_trace" "Can't have trace values less than zero."
186   else (case Binarymap.peek (!trace_map, nm) of
187            NONE => ()
188          | SOME _ =>
189             WARN "register_trace" ("Replacing a trace with name " ^ quote nm)
190         ; trace_map := Binarymap.insert
191                          (!trace_map, nm, TR {value = ref2trfp r, default = !r,
192                                               aliases = [], maximum = max}))
193
194fun register_alias_trace {original, alias} =
195  if original = alias then
196    WARN "register_alias_trace" "original and alias are equal; doing nothing"
197  else
198    case find_record original of
199        NONE => raise ERR "register_alias_trace"
200                    ("Original trace: \""^original^"\" doesn't exist")
201      | SOME {aliases,maximum,default,value} =>
202        let
203          val aliases' =
204              if List.exists (fn s => s = alias) aliases then aliases
205              else alias::aliases
206          val rcd = {aliases = aliases', maximum = maximum, default = default,
207                     value = value}
208          val record_alias = Binarymap.insert(!trace_map, original, TR rcd)
209          val mk_alias = Binarymap.insert(record_alias, alias, ALIAS original)
210        in
211          case Binarymap.peek (record_alias, alias) of
212              NONE => ()
213            | SOME (ALIAS a) =>
214                if a = original then ()
215                else WARN "register_alias_trace"
216                          ("Replacing existing alias binding for \""^
217                           alias ^ "\" |-> \"" ^ a ^"\"")
218            | SOME (TR _) =>
219                raise ERR "register_alias_trace"
220                      ("Cannot replace existing genuine trace info for \""^
221                       alias^"\"");
222          trace_map := mk_alias
223        end
224
225fun register_ftrace (nm, (get, set), max) =
226   let
227      val default = get ()
228   in
229      if default < 0 orelse max < 0
230         then raise ERR "register_ftrace"
231                        "Can't have trace values less than zero."
232      else (case Binarymap.peek (!trace_map, nm) of
233               NONE => ()
234             | SOME _ => WARN "register_ftrace"
235                              ("Replacing a trace with name " ^ quote nm)
236            ; trace_map :=
237                  Binarymap.insert
238                     (!trace_map, nm, TR {value = TRFP {get = get, set = set},
239                                          default = default, aliases = [],
240                                          maximum = max}))
241   end
242
243fun register_btrace (nm, bref) =
244   (case Binarymap.peek (!trace_map, nm) of
245       NONE => ()
246     | SOME _ => WARN "register_btrace"
247                      ("Replacing a trace with name "^ quote nm)
248    ; trace_map :=
249        Binarymap.insert
250            (!trace_map, nm,
251             TR {value = TRFP {get = (fn () => if !bref then 1 else 0),
252                               set = (fn i => bref := (i > 0))},
253                 default = if !bref then 1 else 0, aliases = [],
254                 maximum = 1}))
255
256fun traces () =
257   let
258      fun foldthis (n, ti, acc) =
259        case ti of
260            ALIAS _ => acc
261          | TR {value, default = d, maximum, aliases} =>
262            {name = n, aliases = aliases,
263             trace_level = trfp_get value,
264             default = d,
265             max = maximum} :: acc
266   in
267      Binarymap.foldr foldthis [] (!trace_map)
268   end
269
270local
271   fun err f l = raise ERR f (String.concat l)
272in
273   fun registered_err f nm = err f ["No trace ", quote nm, " is registered"]
274
275   fun bound_check f nm maximum value =
276      if value > maximum
277         then err f ["Trace ", quote nm, " can't be set that high."]
278      else if value < 0
279         then err f ["Trace ", quote nm, " can't be set less than 0."]
280      else ()
281end
282
283fun set_trace nm newvalue =
284   case find_record nm of
285      SOME {value, maximum, ...} =>
286        (bound_check "set_trace" nm maximum newvalue; trfp_set value newvalue)
287    | NONE => registered_err "set_trace" nm
288
289fun reset_trace nm =
290   case find_record nm of
291      SOME {value, default, ...} => trfp_set value default
292    | NONE => registered_err "reset_trace" nm
293
294fun reset_traces () =
295  let
296    fun reset (TR{value,default,...}) = trfp_set value default
297      | reset (ALIAS _) = ()
298  in
299    Binarymap.app (reset o #2) (!trace_map)
300  end
301
302fun current_trace nm =
303   case find_record nm of
304      SOME {value, ...} => trfp_get value
305    | NONE => registered_err "current_trace" nm
306
307fun trace (nm, i) f x =
308   case find_record nm of
309      NONE => registered_err "trace" nm
310    | SOME {value, maximum, ...} =>
311        (bound_check "trace" nm maximum i
312         ; let
313              val init = trfp_get value
314              val _ = trfp_set value i
315              val y = f x handle e => (trfp_set value init; raise e)
316              val _ = trfp_set value init
317           in
318              y
319           end)
320
321fun get_tracefn nm =
322   case find_record nm of
323      NONE => registered_err "get_tracefn" nm
324    | SOME {value = TRFP {get, ...}, ...} => get
325
326val () = register_btrace ("assumptions", Globals.show_assums)
327val () = register_btrace ("numeral types", Globals.show_numeral_types)
328
329val () =
330   let
331      val v = Globals.show_types_verbosely
332      val t = Globals.show_types
333      fun get () = if !v then 2 else if !t then 1 else 0
334      fun set i = if i = 0
335                     then (v := false; t := false)
336                  else if i = 1
337                     then (v := false; t := true)
338                  else (v := true; t := true)
339   in
340      register_ftrace ("types", (get, set), 2)
341   end
342
343val () = register_btrace ("PP.catch_withpp_err", OldPP.catch_withpp_err)
344
345end  (* Feedback *)
346