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