1(* Title: Pure/Tools/simplifier_trace.ML 2 Author: Lars Hupel 3 4Interactive Simplifier trace. 5*) 6 7signature SIMPLIFIER_TRACE = 8sig 9 val disable: Proof.context -> Proof.context 10 val add_term_breakpoint: term -> Context.generic -> Context.generic 11 val add_thm_breakpoint: thm -> Context.generic -> Context.generic 12end 13 14structure Simplifier_Trace: SIMPLIFIER_TRACE = 15struct 16 17(** context data **) 18 19datatype mode = Disabled | Normal | Full 20 21fun merge_modes Disabled m = m 22 | merge_modes Normal Full = Full 23 | merge_modes Normal _ = Normal 24 | merge_modes Full _ = Full 25 26val empty_breakpoints = 27 (Item_Net.init (op aconv) single, 28 Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm)) 29 30fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) = 31 (Item_Net.merge (term_bs1, term_bs2), 32 Item_Net.merge (thm_bs1, thm_bs2)) 33 34structure Data = Generic_Data 35( 36 type T = 37 {max_depth: int, 38 mode: mode, 39 interactive: bool, 40 memory: bool, 41 parent: int, 42 breakpoints: term Item_Net.T * rrule Item_Net.T} 43 val empty = 44 {max_depth = 10, 45 mode = Disabled, 46 interactive = false, 47 memory = true, 48 parent = 0, 49 breakpoints = empty_breakpoints} 50 val extend = I 51 fun merge 52 ({max_depth = max_depth1, mode = mode1, interactive = interactive1, 53 memory = memory1, breakpoints = breakpoints1, ...}: T, 54 {max_depth = max_depth2, mode = mode2, interactive = interactive2, 55 memory = memory2, breakpoints = breakpoints2, ...}: T) = 56 {max_depth = Int.max (max_depth1, max_depth2), 57 mode = merge_modes mode1 mode2, 58 interactive = interactive1 orelse interactive2, 59 memory = memory1 andalso memory2, 60 parent = 0, 61 breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T 62) 63 64val get_data = Data.get o Context.Proof 65val put_data = Context.proof_map o Data.put 66 67val disable = 68 Config.put simp_trace false #> 69 (Context.proof_map o Data.map) 70 (fn {max_depth, mode = _, interactive, parent, memory, breakpoints} => 71 {max_depth = max_depth, mode = Disabled, interactive = interactive, parent = parent, 72 memory = memory, breakpoints = breakpoints}); 73 74val get_breakpoints = #breakpoints o get_data 75 76fun map_breakpoints f = 77 Data.map 78 (fn {max_depth, mode, interactive, parent, memory, breakpoints} => 79 {max_depth = max_depth, 80 mode = mode, 81 interactive = interactive, 82 memory = memory, 83 parent = parent, 84 breakpoints = f breakpoints}) 85 86fun add_term_breakpoint term = 87 map_breakpoints (apfst (Item_Net.update term)) 88 89fun add_thm_breakpoint thm context = 90 let 91 val rrules = mk_rrules (Context.proof_of context) [thm] 92 in 93 map_breakpoints (apsnd (fold Item_Net.update rrules)) context 94 end 95 96fun check_breakpoint (term, rrule) ctxt = 97 let 98 val thy = Proof_Context.theory_of ctxt 99 val (term_bs, thm_bs) = get_breakpoints ctxt 100 101 val term_matches = 102 filter (fn pat => Pattern.matches thy (pat, term)) 103 (Item_Net.retrieve_matching term_bs term) 104 105 val thm_matches = 106 exists (eq_rrule o pair rrule) 107 (Item_Net.retrieve_matching thm_bs (Thm.full_prop_of (#thm rrule))) 108 in 109 (term_matches, thm_matches) 110 end 111 112 113 114(** config and attributes **) 115 116fun config raw_mode interactive max_depth memory = 117 let 118 val mode = 119 (case raw_mode of 120 "normal" => Normal 121 | "full" => Full 122 | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)) 123 124 val update = Data.map (fn {parent, breakpoints, ...} => 125 {max_depth = max_depth, 126 mode = mode, 127 interactive = interactive, 128 memory = memory, 129 parent = parent, 130 breakpoints = breakpoints}) 131 in Thm.declaration_attribute (K update) end 132 133fun breakpoint terms = 134 Thm.declaration_attribute (fn thm => add_thm_breakpoint thm o fold add_term_breakpoint terms) 135 136 137 138(** tracing state **) 139 140val futures = 141 Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table) 142 143 144 145(** markup **) 146 147fun output_result (id, data) = 148 Output.result (Markup.serial_properties id) [data] 149 150val parentN = "parent" 151val textN = "text" 152val memoryN = "memory" 153val successN = "success" 154 155type payload = 156 {props: Properties.T, 157 pretty: Pretty.T} 158 159fun empty_payload () : payload = 160 {props = [], pretty = Pretty.str ""} 161 162fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt = 163 let 164 val {mode, interactive, memory, parent, ...} = get_data ctxt 165 166 val eligible = 167 (case mode of 168 Disabled => false 169 | Normal => triggered 170 | Full => true) 171 172 val markup' = 173 if markup = Markup.simp_trace_stepN andalso not interactive 174 then Markup.simp_trace_logN 175 else markup 176 in 177 if not eligible then NONE 178 else 179 let 180 val {props = more_props, pretty} = payload () 181 val props = 182 [(textN, text), 183 (memoryN, Value.print_bool memory), 184 (parentN, Value.print_int parent)] 185 val data = 186 Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty]) 187 in 188 SOME (serial (), data) 189 end 190 end 191 192 193 194(** tracing output **) 195 196fun see_panel () = 197 let 198 val ((bg1, bg2), en) = 199 YXML.output_markup_elem 200 (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []}) 201 in "See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en end 202 203 204fun send_request (result_id, content) = 205 let 206 fun break () = 207 (Output.protocol_message (Markup.simp_trace_cancel result_id) []; 208 Synchronized.change futures (Inttab.delete_safe result_id)) 209 val promise = Future.promise break : string future 210 in 211 Synchronized.change futures (Inttab.update_new (result_id, promise)); 212 output_result (result_id, content); 213 promise 214 end 215 216 217type data = {term: term, thm: thm, unconditional: bool, ctxt: Proof.context, rrule: rrule} 218 219fun step ({term, thm, unconditional, ctxt, rrule}: data) = 220 let 221 val (matching_terms, thm_triggered) = check_breakpoint (term, rrule) ctxt 222 223 val {name, ...} = rrule 224 val term_triggered = not (null matching_terms) 225 226 val text = 227 if unconditional then "Apply rewrite rule?" 228 else "Apply conditional rewrite rule?" 229 230 fun payload () = 231 let 232 (* FIXME pretty printing via Proof_Context.pretty_fact *) 233 val pretty_thm = Pretty.block 234 [Pretty.str ("Instance of " ^ name ^ ":"), 235 Pretty.brk 1, 236 Syntax.pretty_term ctxt (Thm.prop_of thm)] 237 238 val pretty_term = Pretty.block 239 [Pretty.str "Trying to rewrite:", 240 Pretty.brk 1, 241 Syntax.pretty_term ctxt term] 242 243 val pretty_matchings = 244 let 245 val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms 246 in 247 if not (null matching_terms) then 248 [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))] 249 else [] 250 end 251 252 val pretty = 253 Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings) 254 in 255 {props = [], pretty = pretty} 256 end 257 258 val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt 259 260 fun mk_promise result = 261 let 262 val result_id = #1 result 263 264 fun put mode' interactive' = put_data 265 {max_depth = max_depth, 266 mode = mode', 267 interactive = interactive', 268 memory = memory, 269 parent = result_id, 270 breakpoints = breakpoints} ctxt 271 272 fun to_response "skip" = NONE 273 | to_response "continue" = SOME (put mode true) 274 | to_response "continue_trace" = SOME (put Full true) 275 | to_response "continue_passive" = SOME (put mode false) 276 | to_response "continue_disable" = SOME (put Disabled false) 277 | to_response _ = raise Fail "Simplifier_Trace.step: invalid message" 278 in 279 if not interactive then 280 (output_result result; Future.value (SOME (put mode false))) 281 else Future.map to_response (send_request result) 282 end 283 284 in 285 (case mk_generic_result Markup.simp_trace_stepN text 286 (thm_triggered orelse term_triggered) payload ctxt of 287 NONE => Future.value (SOME ctxt) 288 | SOME res => mk_promise res) 289 end 290 291fun recurse text depth term ctxt = 292 let 293 fun payload () = 294 {props = [], 295 pretty = Syntax.pretty_term ctxt term} 296 297 val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt 298 299 fun put result_id = put_data 300 {max_depth = max_depth, 301 mode = if depth >= max_depth then Disabled else mode, 302 interactive = interactive, 303 memory = memory, 304 parent = result_id, 305 breakpoints = breakpoints} ctxt 306 in 307 (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of 308 NONE => put 0 309 | SOME res => 310 (if depth = 1 then writeln (see_panel ()) else (); 311 output_result res; 312 put (#1 res))) 313 end 314 315fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' = 316 let 317 fun payload () = 318 let 319 val {name, ...} = rrule 320 val pretty_thm = 321 (* FIXME pretty printing via Proof_Context.pretty_fact *) 322 Pretty.block 323 [Pretty.str ("In an instance of " ^ name ^ ":"), 324 Pretty.brk 1, 325 Syntax.pretty_term ctxt (Thm.prop_of thm)] 326 327 val pretty_term = 328 Pretty.block 329 [Pretty.str "Was trying to rewrite:", 330 Pretty.brk 1, 331 Syntax.pretty_term ctxt term] 332 333 val pretty = 334 Pretty.chunks [pretty_thm, pretty_term] 335 in 336 {props = [(successN, "false")], pretty = pretty} 337 end 338 339 val {interactive, ...} = get_data ctxt 340 341 fun mk_promise result = 342 let 343 fun to_response "exit" = false 344 | to_response "redo" = 345 (Option.app output_result 346 (mk_generic_result Markup.simp_trace_ignoreN "Ignore" true empty_payload ctxt'); 347 true) 348 | to_response _ = raise Fail "Simplifier_Trace.indicate_failure: invalid message" 349 in 350 if not interactive then 351 (output_result result; Future.value false) 352 else Future.map to_response (send_request result) 353 end 354 in 355 (case mk_generic_result Markup.simp_trace_hintN "Step failed" true payload ctxt' of 356 NONE => Future.value false 357 | SOME res => mk_promise res) 358 end 359 360fun indicate_success thm ctxt = 361 let 362 fun payload () = 363 {props = [(successN, "true")], 364 pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)} 365 in 366 Option.app output_result 367 (mk_generic_result Markup.simp_trace_hintN "Successfully rewrote" true payload ctxt) 368 end 369 370 371 372(** setup **) 373 374fun simp_apply args ctxt cont = 375 let 376 val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args 377 val data = 378 {term = term, 379 unconditional = unconditional, 380 ctxt = ctxt, 381 thm = thm, 382 rrule = rrule} 383 in 384 (case Future.join (step data) of 385 NONE => NONE 386 | SOME ctxt' => 387 let val res = cont ctxt' in 388 (case res of 389 NONE => 390 if Future.join (indicate_failure data ctxt') then 391 simp_apply args ctxt cont 392 else NONE 393 | SOME (thm, _) => (indicate_success thm ctxt'; res)) 394 end) 395 end 396 397val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler" 398 399val _ = Theory.setup 400 (Simplifier.set_trace_ops 401 {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" depth term, 402 trace_apply = simp_apply}) 403 404val _ = 405 Isabelle_Process.protocol_command "Simplifier_Trace.reply" 406 (fn [serial_string, reply] => 407 let 408 val serial = Value.parse_int serial_string 409 val result = 410 Synchronized.change_result futures 411 (fn tab => (Inttab.lookup tab serial, Inttab.delete_safe serial tab)) 412 in 413 (case result of 414 SOME promise => Future.fulfill promise reply 415 | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *) 416 end handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn) 417 418 419 420(** attributes **) 421 422val mode_parser = 423 Scan.optional 424 (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full")) 425 "normal" 426 427val interactive_parser = 428 Scan.optional (Args.$$$ "interactive" >> K true) false 429 430val memory_parser = 431 Scan.optional (Args.$$$ "no_memory" >> K false) true 432 433val depth_parser = 434 Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10 435 436val config_parser = 437 (interactive_parser -- mode_parser -- depth_parser -- memory_parser) >> 438 (fn (((interactive, mode), depth), memory) => config mode interactive depth memory) 439 440val _ = Theory.setup 441 (Attrib.setup \<^binding>\<open>simp_break\<close> 442 (Scan.repeat Args.term_pattern >> breakpoint) 443 "declaration of a simplifier breakpoint" #> 444 Attrib.setup \<^binding>\<open>simp_trace_new\<close> (Scan.lift config_parser) 445 "simplifier trace configuration") 446 447end 448