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