1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Apply_Debug 8 imports 9 Apply_Trace 10 "HOL-Eisbach.Eisbach_Tools" 11 keywords 12 "apply_debug" :: "prf_script" % "proof" and 13 "continue" :: prf_script % "proof" and "finish" :: prf_script % "proof" 14begin 15 16(* Small hack to keep enough available threads around to support ongoing apply_debug sessions *) 17ML \<open> 18val start_max_threads = Multithreading.max_threads (); 19\<close> 20 21(*FIXME: Add proper interface to match *) 22context 23begin 24 25private method put_prems = 26 (match premises in H:"PROP _" (multi) \<Rightarrow> \<open>insert H\<close>) 27 28ML \<open> 29fun get_match_prems ctxt = 30 let 31 32 val st = Goal.init @{cterm "PROP P"} 33 34 fun get_wrapped () = 35 let 36 val ((_,st'),_) = 37 Method_Closure.apply_method ctxt @{method put_prems} [] [] [] ctxt [] (ctxt, st) 38 |> Seq.first_result "prems"; 39 40 val prems = 41 Thm.prems_of st' |> hd |> Logic.strip_imp_prems; 42 43 in prems end 44 45 val match_prems = the_default [] (try get_wrapped ()); 46 47 val all_prems = Assumption.all_prems_of ctxt; 48 49 in map_filter (fn t => find_first (fn thm => t aconv (Thm.prop_of thm)) all_prems) match_prems end 50 51\<close> 52end 53 54ML \<open> 55signature APPLY_DEBUG = 56sig 57type break_opts = { tags : string list, trace : (string * Position.T) option, show_running : bool } 58 59val break : Proof.context -> string option -> tactic; 60val apply_debug : break_opts -> Method.text_range -> Proof.state -> Proof.state; 61val continue : int option -> (context_state -> context_state option) option -> Proof.state -> Proof.state; 62val finish : Proof.state -> Proof.state; 63 64val pretty_state: Toplevel.state -> Pretty.T option; 65 66end 67 68structure Apply_Debug : APPLY_DEBUG = 69struct 70type break_opts = { tags : string list, trace : (string * Position.T) option, show_running : bool } 71 72fun do_markup range m = Output.report [Markup.markup (Markup.properties (Position.properties_of_range range) m) ""]; 73fun do_markup_pos pos m = Output.report [Markup.markup (Markup.properties (Position.properties_of pos) m) ""]; 74 75type markup_queue = { cur : Position.range option, next : Position.range option, clear_cur : bool } 76 77fun map_cur f ({cur, next, clear_cur} : markup_queue) = 78 ({cur = f cur, next = next, clear_cur = clear_cur} : markup_queue) 79 80fun map_next f ({cur, next, clear_cur} : markup_queue) = 81 ({cur = cur, next = f next, clear_cur = clear_cur} : markup_queue) 82 83fun map_clear_cur f ({cur, next, clear_cur} : markup_queue) = 84 ({cur = cur, next = next, clear_cur = f clear_cur} : markup_queue) 85 86type markup_state = 87 { running : markup_queue 88 } 89 90fun map_running f ({running} : markup_state) = 91 {running = f running} 92 93 94structure Markup_Data = Proof_Data 95( 96 type T = markup_state Synchronized.var option * 97 Position.range option (* latest method location *) * 98 Position.range option (* latest breakpoint location *) 99 fun init _ : T = (NONE, NONE, NONE) 100); 101 102val init_queue = ({cur = NONE, next = NONE, clear_cur = false}: markup_queue) 103val init_markup_state = ({running = init_queue} : markup_state) 104 105fun set_markup_state id = Markup_Data.map (@{apply 3 (1)} (K id)); 106fun get_markup_id ctxt = #1 (Markup_Data.get ctxt); 107 108fun set_latest_range range = Markup_Data.map (@{apply 3 (2)} (K (SOME range))); 109fun get_latest_range ctxt = #2 (Markup_Data.get ctxt); 110 111fun set_breakpoint_range range = Markup_Data.map (@{apply 3 (3)} (K (SOME range))); 112fun get_breakpoint_range ctxt = #3 (Markup_Data.get ctxt); 113 114val clear_ranges = Markup_Data.map (@{apply 3 (3)} (K NONE) o @{apply 3 (2)} (K NONE)); 115 116fun swap_markup queue startm endm = 117if is_some (#next queue) andalso #next queue = #cur queue then SOME (map_next (K NONE) queue) else 118let 119 fun clear_cur () = 120 (case #cur queue of SOME crng => 121 do_markup crng endm 122 | NONE => ()) 123in 124 case #next queue of SOME rng => 125 (clear_cur (); do_markup rng startm; SOME ((map_cur (K (SOME rng)) o map_next (K NONE)) queue)) 126 | NONE => if #clear_cur queue then (clear_cur (); SOME ((map_cur (K NONE) o map_clear_cur (K false)) queue)) 127 else NONE 128end 129 130fun markup_worker (SOME (id : markup_state Synchronized.var)) = 131let 132 fun main_loop () = 133 let val _ = Synchronized.guarded_access id (fn e => 134 case swap_markup (#running e) Markup.running Markup.finished of 135 SOME queue' => SOME ((),map_running (fn _ => queue') e) 136 | NONE => NONE) 137 in main_loop () end 138in main_loop () end 139 | markup_worker NONE = (fn () => ()) 140 141fun set_gen get set (SOME id) rng = 142 let 143 val _ = 144 Synchronized.guarded_access id (fn e => 145 if is_some (#next (get e)) orelse (#clear_cur (get e)) then NONE else 146 if (#cur (get e)) = SOME rng then SOME ((), e) 147 else (SOME ((),(set (map_next (fn _ => SOME rng)) e)))) 148 149 val _ = Synchronized.guarded_access id (fn e => if is_some (#next (get e)) then NONE else SOME ((),e)) 150 in () end 151 | set_gen _ _ NONE _ = () 152 153 154fun clear_gen get set (SOME id) = 155 Synchronized.guarded_access id (fn e => 156 if (#clear_cur (get e)) then NONE 157 else (SOME ((),(set (map_clear_cur (fn _ => true)) e)))) 158 | clear_gen _ _ NONE = () 159 160val set_running = set_gen #running map_running 161val clear_running = clear_gen #running map_running 162 163 164fun traceify_method static_ctxt src = 165let 166 val range = Token.range_of src; 167 val head_range = Token.range_of [hd src]; 168 val m = Method.method_cmd static_ctxt src; 169 170in (fn eval_ctxt => fn facts => 171 let 172 val eval_ctxt = set_latest_range head_range eval_ctxt; 173 val markup_id = get_markup_id eval_ctxt; 174 175 fun traceify seq = Seq.make (fn () => 176 let 177 val _ = set_running markup_id range; 178 val r = Seq.pull seq; 179 val _ = clear_running markup_id; 180 in Option.map (apsnd traceify) r end) 181 182 fun tac (runtime_ctxt,thm) = 183 let 184 val runtime_ctxt' = set_latest_range head_range runtime_ctxt; 185 val _ = set_running markup_id range; 186 in traceify (m eval_ctxt facts (runtime_ctxt', thm)) end 187 188 in tac end) 189end 190 191fun add_debug ctxt (Method.Source src) = (Method.Basic (traceify_method ctxt src)) 192 | add_debug ctxt (Method.Combinator (x,y,txts)) = (Method.Combinator (x,y, map (add_debug ctxt) txts)) 193 | add_debug _ x = x 194 195fun st_eq (ctxt : Proof.context,st) (ctxt',st') = 196 pointer_eq (ctxt,ctxt') andalso Thm.eq_thm (st,st') 197 198type result = 199 { pre_state : thm, 200 post_state : thm, 201 context: Proof.context} 202 203datatype final_state = RESULT of (Proof.context * thm) | ERR of (unit -> string) 204 205type debug_state = 206 {results : result list, (* this execution, in order of appearance *) 207 prev_results : thm list, (* continuations needed to get thread back to some state*) 208 next_state : thm option, (* proof thread blocks waiting for this *) 209 break_state : (Proof.context * thm) option, (* state of proof thread just before blocking *) 210 restart : (unit -> unit) * int, (* restart function (how many previous results to keep), restart requested if non-zero *) 211 final : final_state option, (* final result, maybe error *) 212 trans_id : int, (* increment on every restart *) 213 ignore_breaks: bool} 214 215val init_state = 216 ({results = [], 217 prev_results = [], 218 next_state = NONE, break_state = NONE, 219 final = NONE, ignore_breaks = false, restart = (K (), ~1), trans_id = 0} : debug_state) 220 221fun map_next_state f ({results, next_state, break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 222 ({results = results, next_state = f next_state, break_state = break_state, final = final, prev_results = prev_results, 223 restart = restart, ignore_breaks = ignore_breaks, trans_id = trans_id} : debug_state) 224 225fun map_results f ({results, next_state, break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 226 ({results = f results, next_state = next_state, break_state = break_state, final = final, prev_results = prev_results, 227 restart = restart, ignore_breaks = ignore_breaks, trans_id = trans_id} : debug_state) 228 229fun map_prev_results f ({results, next_state, break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 230 ({results = results, next_state = next_state, break_state = break_state, final = final, prev_results = f prev_results, 231 restart = restart, ignore_breaks = ignore_breaks, trans_id = trans_id} : debug_state) 232 233fun map_ignore_breaks f ({results, next_state, break_state = break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 234 ({results = results, next_state = next_state, break_state = break_state,final = final, prev_results = prev_results, 235 restart = restart, ignore_breaks = f ignore_breaks, trans_id = trans_id} : debug_state) 236 237fun map_final f ({results, next_state, break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 238 ({results = results, next_state = next_state, break_state =break_state ,final = f final, prev_results = prev_results, 239 restart = restart, ignore_breaks = ignore_breaks, trans_id = trans_id} : debug_state) 240 241fun map_restart f ({results, next_state, break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 242 ({results = results, next_state = next_state, break_state = break_state, final = final, prev_results = prev_results, 243 restart = f restart, ignore_breaks = ignore_breaks, trans_id = trans_id} : debug_state) 244 245fun map_break_state f ({results, next_state, break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 246 ({results = results, next_state = next_state, break_state = f break_state, final = final, prev_results = prev_results, 247 restart = restart, ignore_breaks = ignore_breaks, trans_id = trans_id} : debug_state) 248 249fun map_trans_id f ({results, next_state, break_state, final, ignore_breaks, prev_results, restart, trans_id} : debug_state) = 250 ({results = results, next_state = next_state, break_state = break_state, final = final, prev_results = prev_results, 251 restart = restart, ignore_breaks = ignore_breaks, trans_id = f trans_id} : debug_state) 252 253fun is_restarting ({restart,...} : debug_state) = snd restart > ~1; 254fun is_finished ({final,...} : debug_state) = is_some final; 255 256val drop_states = map_break_state (K NONE) o map_next_state (K NONE); 257 258fun add_result ctxt pre post = map_results (cons {pre_state = pre, post_state = post, context = ctxt}) o drop_states; 259 260fun get_trans_id (id : debug_state Synchronized.var) = #trans_id (Synchronized.value id); 261 262fun stale_transaction_err trans_id trans_id' = 263 error ("Stale transaction. Expected " ^ Int.toString trans_id ^ " but found " ^ Int.toString trans_id') 264 265fun assert_trans_id trans_id (e : debug_state) = 266 if trans_id = (#trans_id e) then () 267 else stale_transaction_err trans_id (#trans_id e) 268 269fun guarded_access id f = 270 let 271 val trans_id = get_trans_id id; 272 in 273 Synchronized.guarded_access id 274 (fn (e : debug_state) => 275 (assert_trans_id trans_id e; 276 (case f e of 277 NONE => NONE 278 | SOME (e', g) => SOME (e', g e)))) 279 end 280 281fun guarded_read id f = 282 let 283 val trans_id = get_trans_id id; 284 in 285 Synchronized.guarded_access id 286 (fn (e : debug_state) => 287 (assert_trans_id trans_id e; 288 (case f e of 289 NONE => NONE 290 | SOME e' => SOME (e', e)))) 291 end 292 293 294 295(* Immediate return if there are previous results available or we are ignoring breakpoints *) 296 297fun pop_state_no_block id ctxt pre = guarded_access id (fn e => 298 if is_finished e then error "Attempted to pop state from finished proof" else 299 if (#ignore_breaks e) then SOME (SOME pre, add_result ctxt pre pre) else 300 case #prev_results e of 301 [] => SOME (NONE, I) 302 | (st :: sts) => SOME (SOME st, add_result ctxt pre st o map_prev_results (fn _ => sts))) 303 304fun pop_next_state id ctxt pre = guarded_access id (fn e => 305 if is_finished e then error "Attempted to pop state from finished proof" else 306 if not (null (#prev_results e)) then error "Attempted to pop state when previous results exist" else 307 if (#ignore_breaks e) then SOME (pre, add_result ctxt pre pre) else 308 (case #next_state e of 309 NONE => NONE 310 | SOME st => SOME (st, add_result ctxt pre st))) 311 312fun set_next_state id trans_id st = guarded_access id (fn e => 313 (assert_trans_id trans_id e; 314 (if is_none (#next_state e) andalso is_some (#break_state e) then 315 SOME ((), map_next_state (fn _ => SOME st) o map_break_state (fn _ => NONE)) 316 else error ("Attempted to set next state in inconsistent state" ^ (@{make_string} e))))) 317 318fun set_break_state id st = guarded_access id (fn e => 319 if is_none (#next_state e) andalso is_none (#break_state e) then 320 SOME ((), map_break_state (fn _ => SOME st)) 321 else error ("Attempted to set break state in inconsistent state" ^ (@{make_string} e))) 322 323fun pop_state id ctxt pre = 324 case pop_state_no_block id ctxt pre of SOME st => st 325 | NONE => 326 let 327 val _ = set_break_state id (ctxt, pre); (* wait for continue *) 328 in pop_next_state id ctxt pre end 329 330(* block until a breakpoint is hit or method finishes *) 331fun wait_break_state id trans_id = guarded_read id 332 (fn e => 333 (assert_trans_id trans_id e; 334 (case (#final e) of SOME st => SOME (st, true) | NONE => 335 case (#break_state e) of SOME st => SOME (RESULT st, false) 336 | NONE => NONE))); 337 338fun debug_print (id : debug_state Synchronized.var) = 339 (@{print} (Synchronized.value id)); 340 341(* Trigger a restart if an existing nth entry differs from the given one *) 342fun maybe_restart id n st = 343let 344 val gen = guarded_read id (fn e => SOME (#trans_id e)); 345 346 val did_restart = guarded_access id (fn e => 347 if is_some (#next_state e) then NONE else 348 if not (null (#prev_results e)) then NONE else 349 if is_restarting e then NONE (* TODO, what to do if we're already restarting? *) 350 else if length (#results e) > n then 351 (SOME (true, map_restart (apsnd (fn _ => n)))) 352 else SOME (false, I)) 353 354 355 val trans_id = Synchronized.guarded_access id 356 (fn e => if is_restarting e then NONE else 357 if not did_restart orelse gen + 1 = #trans_id e then SOME (#trans_id e,e) else 358 stale_transaction_err (gen + 1) (#trans_id e)); 359in trans_id end; 360 361 362fun peek_all_results id = guarded_read id (fn e => SOME (#results e)); 363 364fun peek_final_result id = 365 guarded_read id (fn e => #final e) 366 367fun poke_error (RESULT st) = st 368 | poke_error (ERR e) = error (e ()) 369 370fun context_state e = (#context e, #pre_state e); 371 372fun nth_pre_result id i = guarded_read id 373 (fn e => 374 if length (#results e) > i then SOME (RESULT (context_state (nth (rev (#results e)) i)), false) else 375 if not (null (#prev_results e)) then NONE else 376 (if length (#results e) = i then 377 (case #break_state e of SOME st => SOME (RESULT st, false) | NONE => NONE) else 378 (case #final e of SOME st => SOME (st, true) | NONE => NONE))) 379 380fun set_finished_result id trans_id st = 381 guarded_access id (fn e => 382 (assert_trans_id trans_id e; 383 SOME ((), map_final (K (SOME st))))); 384 385fun is_finished_result id = guarded_read id (fn e => SOME (is_finished e)); 386 387fun get_finish id = 388if is_finished_result id then peek_final_result id else 389 let 390 val _ = guarded_access id 391 (fn _ => SOME ((), (map_ignore_breaks (fn _ => true)))) 392 393 in peek_final_result id end 394 395 396val no_break_opts = ({tags = [], trace = NONE, show_running = false} : break_opts) 397 398structure Debug_Data = Proof_Data 399( 400 type T = debug_state Synchronized.var option (* handle on active proof thread *) * 401 int * (* continuation counter *) 402 bool * (* currently interactive context *) 403 break_opts * (* global break arguments *) 404 string option (* latest breakpoint tag *) 405 fun init _ : T = (NONE,~1, false, no_break_opts, NONE) 406); 407 408fun set_debug_ident ident = Debug_Data.map (@{apply 5 (1)} (fn _ => SOME ident)) 409val get_debug_ident = #1 o Debug_Data.get; 410val get_the_debug_ident = the o get_debug_ident; 411 412fun set_break_opts opts = Debug_Data.map (@{apply 5 (4)} (fn _ => opts)) 413val get_break_opts = #4 o Debug_Data.get; 414 415fun set_last_tag tags = Debug_Data.map (@{apply 5 (5)} (fn _ => tags)) 416val get_last_tag = #5 o Debug_Data.get; 417 418val is_debug_ctxt = is_some o #1 o Debug_Data.get; 419 420fun clear_debug ctxt = ctxt 421 |> Debug_Data.map (fn _ => (NONE,~1,false, no_break_opts, NONE)) 422 |> clear_ranges 423 424 425val get_continuation = #2 o Debug_Data.get; 426val get_can_break = #3 o Debug_Data.get; 427 428(* Maintain pointer equality if possible *) 429fun set_continuation i ctxt = if get_continuation ctxt = i then ctxt else 430 Debug_Data.map (@{apply 5 (2)} (fn _ => i)) ctxt; 431 432fun set_can_break b ctxt = if get_can_break ctxt = b then ctxt else 433 Debug_Data.map (@{apply 5 (3)} (fn _ => b)) ctxt; 434 435fun has_break_tag (SOME tag) tags = member (=) tags tag 436 | has_break_tag NONE _ = true; 437 438fun break ctxt tag = (fn thm => 439if not (get_can_break ctxt) 440 orelse Method.detect_closure_state thm 441 orelse not (has_break_tag tag (#tags (get_break_opts ctxt))) 442 then Seq.single thm else 443 let 444 val id = get_the_debug_ident ctxt; 445 val ctxt' = set_last_tag tag ctxt; 446 447 val st' = Seq.make (fn () => 448 SOME (pop_state id ctxt' thm,Seq.empty)) 449 450 in st' end) 451 452fun init_interactive ctxt = ctxt 453 |> set_can_break false 454 |> Config.put Method.closure true; 455 456type static_info = 457 {private_dyn_facts : string list, local_facts : (string * thm list) list} 458 459structure Data = Generic_Data 460( 461 type T = (morphism * Proof.context * static_info) option; 462 val empty: T = NONE; 463 val extend = K NONE; 464 fun merge data : T = NONE; 465); 466 467(* Present Eisbach/Match variable binding context as normal context elements. 468 Potentially shadows existing facts/binds *) 469 470fun dest_local s = 471 let 472 val ["local",s'] = Long_Name.explode s; 473 in SOME s' end handle Bind => NONE 474 475fun maybe_bind st (_,[tok]) ctxt = 476 if Method.detect_closure_state st then 477 let 478 val target = Local_Theory.target_of ctxt 479 val local_facts = Proof_Context.facts_of ctxt; 480 val global_facts = map (Global_Theory.facts_of) (Context.parents_of (Proof_Context.theory_of ctxt)); 481 val raw_facts = Facts.dest_all (Context.Proof ctxt) true global_facts local_facts |> map fst; 482 483 fun can_retrieve s = can (Facts.retrieve (Context.Proof ctxt) local_facts) (s, Position.none) 484 485 val private_dyns = raw_facts |> 486 (filter (fn s => Facts.is_concealed local_facts s andalso Facts.is_dynamic local_facts s 487 andalso can_retrieve (Long_Name.base_name s) 488 andalso Facts.intern local_facts (Long_Name.base_name s) = s 489 andalso not (can_retrieve s)) ) 490 491 val local_facts = Facts.dest_static true [(Proof_Context.facts_of target)] local_facts; 492 493 val _ = Token.assign (SOME (Token.Declaration (fn phi => 494 Data.put (SOME (phi,ctxt, {private_dyn_facts = private_dyns, local_facts = local_facts}))))) tok; 495 496 in ctxt end 497 else 498 let 499 val SOME (Token.Declaration decl) = Token.get_value tok; 500 val dummy_ctxt = decl Morphism.identity (Context.Proof ctxt); 501 val SOME (phi,static_ctxt,{private_dyn_facts, local_facts}) = Data.get dummy_ctxt; 502 503 val old_facts = Proof_Context.facts_of static_ctxt; 504 val cur_priv_facts = map (fn s => 505 Facts.retrieve (Context.Proof ctxt) old_facts (Long_Name.base_name s,Position.none)) private_dyn_facts; 506 507 val cur_local_facts = 508 map (fn (s,fact) => (dest_local s, Morphism.fact phi fact)) local_facts 509 |> map_filter (fn (s,fact) => case s of SOME s => SOME (s,fact) | _ => NONE) 510 511 val old_fixes = (Variable.dest_fixes static_ctxt) 512 513 val local_fixes = 514 filter (fn (_,f) => 515 Variable.is_newly_fixed static_ctxt (Local_Theory.target_of static_ctxt) f) old_fixes 516 |> map_filter (fn (n,f) => case Variable.default_type static_ctxt f of SOME typ => 517 if typ = dummyT then NONE else SOME (n, Free (f, typ)) 518 | NONE => NONE) 519 520 val local_binds = (map (apsnd (Morphism.term phi)) local_fixes) 521 522 val ctxt' = ctxt 523 |> fold (fn (s,t) => 524 Variable.bind_term ((s,0),t) 525 #> Variable.declare_constraints (Var ((s,0),Term.fastype_of t))) local_binds 526 |> fold (fn e => 527 Proof_Context.put_thms true (Long_Name.base_name (#name e), SOME (#thms e))) cur_priv_facts 528 |> fold (fn (nm,fact) => 529 Proof_Context.put_thms true (nm, SOME fact)) cur_local_facts 530 |> Proof_Context.put_thms true ("match_prems", SOME (get_match_prems ctxt)); 531 532 in ctxt' end 533 | maybe_bind _ _ ctxt = ctxt 534 535val _ = Context.>> (Context.map_theory (Method.setup @{binding #} 536 (Scan.lift (Scan.trace (Scan.trace (Args.$$$ "break") -- (Scan.option Parse.string))) >> 537 (fn ((b,tag),toks) => fn _ => fn _ => 538 fn (ctxt,thm) => 539 (let 540 541 val range = Token.range_of toks; 542 val ctxt' = ctxt 543 |> maybe_bind thm b 544 |> set_breakpoint_range range; 545 546 in Seq.make_results (Seq.map (fn thm' => (ctxt',thm')) (break ctxt' tag thm)) end))) "")) 547 548fun map_state f state = 549 let 550 val (r,_) = Seq.first_result "map_state" (Proof.apply 551 (Method.Basic (fn _ => fn _ => fn st => 552 Seq.make_results (Seq.single (f st))), 553 Position.no_range) state) 554 in r end; 555 556fun get_state state = 557let 558 val {context,goal} = Proof.simple_goal state; 559in (context,goal) end 560 561 562fun maybe_trace (SOME (tr, pos)) (ctxt, st) = 563let 564 val deps = Apply_Trace.used_facts ctxt st; 565 val query = if tr = "" then NONE else SOME (tr, pos); 566 val pr = Apply_Trace.pretty_deps false query ctxt st deps; 567in Pretty.writeln pr end 568 | maybe_trace NONE (ctxt, st) = () 569 570val active_debug_threads = Synchronized.var "active_debug_threads" ([] : unit future list); 571 572fun update_max_threads extra = 573let 574 val n_active = Synchronized.change_result active_debug_threads (fn ts => 575 let 576 val ts' = List.filter (not o Future.is_finished) ts; 577 in (length ts',ts') end) 578 val _ = Multithreading.max_threads_update (start_max_threads + ((n_active + extra) * 3)); 579in () end 580 581 582fun continue i_opt m_opt = 583(map_state (fn (ctxt,thm) => 584 let 585 586 val ctxt = set_can_break true ctxt 587 588 val thm = Apply_Trace.clear_deps thm; 589 590 val _ = if is_none (get_debug_ident ctxt) then error "Cannot continue in a non-debug state" else (); 591 592 val id = get_the_debug_ident ctxt; 593 594 val start_cont = get_continuation ctxt; (* how many breakpoints so far *) 595 596 val trans_id = maybe_restart id start_cont (ctxt,thm); 597 (* possibly restart if the thread has made too much progress. 598 trans_id is the current number of restarts, used to avoid manipulating 599 stale states *) 600 601 val _ = nth_pre_result id start_cont; (* block until we've hit the start of this continuation *) 602 603 fun get_final n (st as (ctxt,_)) = 604 case (i_opt,m_opt) of 605 (SOME i,NONE) => if i < 1 then error "Can only continue a positive number of breakpoints" else 606 if n = start_cont + i then SOME st else NONE 607 | (NONE, SOME m) => (m (apfst init_interactive st)) 608 | (_, _) => error "Invalid continue arguments" 609 610 val ex_results = peek_all_results id |> rev; 611 612 fun tick_up n (_,thm) = 613 if n < length ex_results then error "Unexpected number of existing results" 614 (*case get_final n (#pre_state (nth ex_results n)) of SOME st' => (st', false, n) 615 | NONE => tick_up (n + 1) st *) 616 else 617 let 618 val _ = if n > length ex_results then set_next_state id trans_id thm else (); 619 val (n_r, b) = wait_break_state id trans_id; 620 val st' = poke_error n_r; 621 in if b then (st',b, n) else 622 case get_final n st' of SOME st'' => (st'', false, n) 623 | NONE => tick_up (n + 1) st' end 624 625 val _ = if length ex_results < start_cont then 626 (debug_print id; @{print} ("start_cont",start_cont); @{print} ("trans_id",trans_id); 627 error "Unexpected number of existing results") 628 else () 629 630 631 val (st',b, cont) = tick_up (start_cont + 1) (ctxt, thm) 632 633 val st'' = if b then (Output.writeln "Final Result."; st' |> apfst clear_debug) 634 else st' |> apfst (set_continuation cont) |> apfst (init_interactive); 635 636 (* markup for matching breakpoints to continues *) 637 638 val sr = serial (); 639 640 fun markup_def rng = 641 (Output.report 642 [Markup.markup (Markup.entity "breakpoint" "" 643 |> Markup.properties (Position.entity_properties_of true sr 644 (Position.range_position rng))) ""]); 645 646 val _ = Option.map markup_def (get_latest_range (fst st'')); 647 val _ = Option.map markup_def (get_breakpoint_range (fst st'')); 648 649 val _ = 650 (Context_Position.report ctxt (Position.thread_data ()) 651 (Markup.entity "breakpoint" "" 652 |> Markup.properties (Position.entity_properties_of false sr Position.none))) 653 654 val _ = maybe_trace (#trace (get_break_opts ctxt)) st''; 655 656 in st'' end)) 657 658fun do_apply pos rng opts m = 659let 660 val {tags, trace, show_running} = opts; 661 val batch_mode = is_some (Position.line_of (fst rng)); 662 val show_running = if batch_mode then false else show_running; 663 664 val _ = if batch_mode then () else update_max_threads 1; 665 666in 667 (fn st => map_state (fn (ctxt,thm) => 668 let 669 val ident = Synchronized.var "debug_state" init_state; 670 val markup_id = if show_running then SOME (Synchronized.var "markup_state" init_markup_state) 671 else NONE; 672 fun maybe_markup m = if show_running then do_markup rng m else (); 673 674 val _ = if is_debug_ctxt ctxt then 675 error "Cannot use apply_debug while debugging" else (); 676 677 val m = apfst (fn f => f ctxt) m; 678 679 val st = Proof.map_context 680 (set_can_break true 681 #> set_break_opts opts 682 #> set_markup_state markup_id 683 #> set_debug_ident ident 684 #> set_continuation ~1) st 685 |> map_state (apsnd Apply_Trace.clear_deps); 686 687 fun do_cancel thread = (Future.cancel thread; Future.join_result thread; ()); 688 689 fun do_fork trans_id = Future.fork (fn () => 690 let 691 val (ctxt,thm) = get_state st; 692 693 val r = case Exn.interruptible_capture (fn st => 694 let val _ = Seq.pull (break ctxt NONE thm) in 695 (case (Seq.pull o Proof.apply m) st 696 of (SOME (Seq.Result st', _)) => RESULT (get_state st') 697 | (SOME (Seq.Error e, _)) => ERR e 698 | _ => ERR (fn _ => "No results")) end) st 699 of Exn.Res (RESULT r) => RESULT r 700 | Exn.Res (ERR e) => ERR e 701 | Exn.Exn e => ERR (fn _ => Runtime.exn_message e) 702 val _ = set_finished_result ident trans_id r; 703 704 val _ = clear_running markup_id; 705 706 in () end) 707 708 709 val thread = do_fork 0; 710 val _ = Synchronized.change ident (map_restart (fn _ => (fn () => do_cancel thread, ~1))); 711 712 val _ = maybe_markup Markup.finished; 713 714 val _ = Future.fork (fn () => markup_worker markup_id ()); 715 716 val st' = get_state (continue (SOME 1) NONE (Proof.map_context (set_continuation 0) st)) 717 718 val _ = maybe_markup Markup.joined; 719 720 721 val main_thread = if batch_mode then Future.fork (fn () => ()) else Future.fork (fn () => 722 let 723 724 fun restart_state gls e = e 725 |> map_prev_results (fn _ => map #post_state (take gls (rev (#results e)))) 726 |> map_results (fn _ => []) 727 |> map_final (fn _ => NONE) 728 |> map_ignore_breaks (fn _ => false) 729 |> map_restart (fn _ => (K (), gls)) 730 |> map_break_state (fn _ => NONE) 731 |> map_next_state (fn _ => NONE) 732 |> map_trans_id (fn i => i + 1); 733 734 fun main_loop () = 735 let 736 val r = Synchronized.timed_access ident (fn _ => SOME (seconds 0.1)) (fn e as {restart,next_state,...} => 737 if is_restarting e andalso is_none next_state then 738 SOME ((fst restart, #trans_id e), restart_state (snd restart) e) else NONE); 739 val _ = OS.Process.sleep (seconds 0.1); 740 in case r of NONE => main_loop () 741 | SOME (f,trans_id) => 742 let 743 val _ = f (); 744 val _ = clear_running markup_id; 745 val thread = do_fork (trans_id + 1); 746 val _ = Synchronized.change ident (map_restart (fn _ => (fn () => do_cancel thread, ~1))) 747 in main_loop () end 748 end; 749 in main_loop () end); 750 751 val _ = maybe_markup Markup.running; 752 val _ = maybe_markup Markup.forked; 753 754 val _ = Synchronized.change active_debug_threads (cons main_thread); 755 756 in st' end) st) 757end 758 759fun apply_debug opts (m', rng) = 760 let 761 val _ = Method.report (m', rng); 762 763 val m'' = (fn ctxt => add_debug ctxt m') 764 val m = (m'',rng) 765 val pos = Position.thread_data (); 766 767 in do_apply pos rng opts m end; 768 769fun quasi_keyword x = Scan.trace (Args.$$$ x) >> 770 (fn (s,[tok]) => (Position.reports [(Token.pos_of tok, Markup.quasi_keyword)]; s)) 771 772val parse_tags = (Args.parens (quasi_keyword "tags" |-- Parse.enum1 "," Parse.string)); 773val parse_trace = Scan.option (Args.parens (quasi_keyword "trace" |-- Scan.option (Parse.position Parse.cartouche))) >> 774 (fn SOME NONE => SOME ("", Position.none) | SOME (SOME x) => SOME x | _ => NONE); 775 776val parse_opts1 = (parse_tags -- parse_trace) >> 777 (fn (tags,trace) => {tags = tags, trace = trace}); 778 779val parse_opts2 = (parse_trace -- (Scan.optional parse_tags [])) >> 780 (fn (trace,tags) => {tags = tags, trace = trace}); 781 782fun mode s = Scan.optional (Args.parens (quasi_keyword s) >> (K true)) false 783 784val parse_opts = ((parse_opts1 || parse_opts2) -- mode "show_running") >> 785 (fn ({tags, trace}, show_running) => {tags = tags, trace = trace, show_running = show_running} : break_opts) ; 786 787val _ = 788 Outer_Syntax.command @{command_keyword apply_debug} "initial goal refinement step (unstructured)" 789 (Scan.trace 790 (parse_opts -- Method.parse) >> 791 (fn ((opts, (m,_)),toks) => Toplevel.proof (apply_debug opts (m,Token.range_of toks)))); 792 793val finish = map_state (fn (ctxt,_) => 794 let 795 val _ = if is_none (get_debug_ident ctxt) then error "Cannot finish in a non-debug state" else (); 796 val f = get_finish (get_the_debug_ident ctxt); 797 in f |> poke_error |> apfst clear_debug end) 798 799 800 801 802fun continue_cmd i_opt m_opt state = 803let 804 val {context,...} = Proof.simple_goal state; 805 val check = Method.map_source (Method.method_closure (init_interactive context)) 806 807 val m_opt' = Option.map (check o Method.check_text context o fst) m_opt; 808 809 fun eval_method txt = 810 (fn (ctxt,thm) => try (fst o Seq.first_result "method") (Method.evaluate txt ctxt [] (ctxt,thm))) 811 812 val i_opt' = case (i_opt,m_opt) of (NONE,NONE) => SOME 1 | _ => i_opt; 813 814in continue i_opt' (Option.map eval_method m_opt') state end 815 816val _ = 817 Outer_Syntax.command @{command_keyword continue} "step to next breakpoint" 818 (Scan.option Parse.int -- Scan.option Method.parse >> (fn (i_opt,m_opt) => 819 (Toplevel.proof (continue_cmd i_opt m_opt)))) 820 821val _ = 822 Outer_Syntax.command @{command_keyword finish} "finish debugging" 823 (Scan.succeed (Toplevel.proof (continue NONE (SOME (fn _ => NONE))))) 824 825fun pretty_hidden_goals ctxt0 thm = 826 let 827 val ctxt = ctxt0 828 |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts) 829 |> Config.put show_sorts false; 830 831 val prt_term = 832 singleton (Syntax.uncheck_terms ctxt) #> 833 Type_Annotation.ignore_free_types #> 834 Syntax.unparse_term ctxt; 835 val prt_subgoal = prt_term 836 837 fun pretty_subgoal s A = 838 Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_subgoal A]; 839 fun pretty_subgoals n = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + n)) A); 840 841 fun collect_extras prop = 842 case try Logic.unprotect prop of 843 SOME prop' => 844 (if Logic.count_prems prop' > 0 then 845 (case try Logic.strip_horn prop' 846 of SOME (As, B) => As :: collect_extras B 847 | NONE => []) 848 else []) 849 | NONE => [] 850 851 val (As,B) = Logic.strip_horn (Thm.prop_of thm); 852 val extras' = collect_extras B; 853 val extra_goals_limit = Int.max (Config.get ctxt0 Goal_Display.goals_limit - length As, 0); 854 val all_extras = flat (take (length extras' - 1) extras'); 855 val extras = take extra_goals_limit all_extras; 856 857 val pretty = pretty_subgoals (length As + 1) extras @ 858 (if extra_goals_limit < length all_extras then 859 [Pretty.str ("A total of " ^ (string_of_int (length all_extras)) ^ " hidden subgoals...")] 860 else []) 861 in pretty end 862 863fun pretty_state state = 864 if Toplevel.is_proof state 865 then 866 let 867 val st = Toplevel.proof_of state; 868 val {goal, context, ...} = Proof.raw_goal st; 869 val pretty = Toplevel.pretty_state state; 870 val hidden = pretty_hidden_goals context goal; 871 val out = pretty @ 872 (if length hidden > 0 then [Pretty.keyword1 "hidden goals"] @ hidden else []); 873 in SOME (Pretty.chunks out) end 874 else NONE 875 876end 877\<close> 878 879ML \<open>val _ = 880 Query_Operation.register {name = "print_state", pri = Task_Queue.urgent_pri} 881 (fn {state = st, output_result, ...} => 882 case Apply_Debug.pretty_state st of 883 SOME prt => output_result (Markup.markup Markup.state (Pretty.string_of prt)) 884 | NONE => ());\<close> 885 886end 887