1(* Title: Pure/Isar/toplevel.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Isabelle/Isar toplevel transactions. 5*) 6 7signature TOPLEVEL = 8sig 9 exception UNDEF 10 type state 11 val theory_toplevel: theory -> state 12 val toplevel: state 13 val is_toplevel: state -> bool 14 val is_theory: state -> bool 15 val is_proof: state -> bool 16 val is_skipped_proof: state -> bool 17 val level: state -> int 18 val previous_theory_of: state -> theory option 19 val context_of: state -> Proof.context 20 val generic_theory_of: state -> generic_theory 21 val theory_of: state -> theory 22 val proof_of: state -> Proof.state 23 val proof_position_of: state -> int 24 val is_end_theory: state -> bool 25 val end_theory: Position.T -> state -> theory 26 val presentation_context: state -> Proof.context 27 val presentation_state: Proof.context -> state 28 val pretty_context: state -> Pretty.T list 29 val pretty_state: state -> Pretty.T list 30 val string_of_state: state -> string 31 val pretty_abstract: state -> Pretty.T 32 type transition 33 val empty: transition 34 val name_of: transition -> string 35 val pos_of: transition -> Position.T 36 val type_error: transition -> string 37 val name: string -> transition -> transition 38 val position: Position.T -> transition -> transition 39 val init_theory: (unit -> theory) -> transition -> transition 40 val is_init: transition -> bool 41 val modify_init: (unit -> theory) -> transition -> transition 42 val exit: transition -> transition 43 val keep: (state -> unit) -> transition -> transition 44 val keep': (bool -> state -> unit) -> transition -> transition 45 val keep_proof: (state -> unit) -> transition -> transition 46 val ignored: Position.T -> transition 47 val is_ignored: transition -> bool 48 val malformed: Position.T -> string -> transition 49 val generic_theory: (generic_theory -> generic_theory) -> transition -> transition 50 val theory': (bool -> theory -> theory) -> transition -> transition 51 val theory: (theory -> theory) -> transition -> transition 52 val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition 53 val end_local_theory: transition -> transition 54 val open_target: (generic_theory -> local_theory) -> transition -> transition 55 val close_target: transition -> transition 56 val local_theory': (bool * Position.T) option -> (xstring * Position.T) option -> 57 (bool -> local_theory -> local_theory) -> transition -> transition 58 val local_theory: (bool * Position.T) option -> (xstring * Position.T) option -> 59 (local_theory -> local_theory) -> transition -> transition 60 val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> 61 transition -> transition 62 val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option -> 63 (bool -> local_theory -> Proof.state) -> transition -> transition 64 val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option -> 65 (local_theory -> Proof.state) -> transition -> transition 66 val theory_to_proof: (theory -> Proof.state) -> transition -> transition 67 val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition 68 val forget_proof: bool -> transition -> transition 69 val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition 70 val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition 71 val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition 72 val proof: (Proof.state -> Proof.state) -> transition -> transition 73 val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition 74 val skip_proof: (unit -> unit) -> transition -> transition 75 val skip_proof_open: transition -> transition 76 val skip_proof_close: transition -> transition 77 val exec_id: Document_ID.exec -> transition -> transition 78 val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b 79 val add_hook: (transition -> state -> state -> unit) -> unit 80 val get_timing: transition -> Time.time 81 val put_timing: Time.time -> transition -> transition 82 val transition: bool -> transition -> state -> state * (exn * string) option 83 val command_errors: bool -> transition -> state -> Runtime.error list * state option 84 val command_exception: bool -> transition -> state -> state 85 val reset_theory: state -> state option 86 val reset_proof: state -> state option 87 type result 88 val join_results: result -> (transition * state) list 89 val element_result: Keyword.keywords -> transition Thy_Syntax.element -> state -> result * state 90end; 91 92structure Toplevel: TOPLEVEL = 93struct 94 95(** toplevel state **) 96 97exception UNDEF = Runtime.UNDEF; 98 99 100(* datatype node *) 101 102datatype node = 103 Theory of generic_theory * Proof.context option 104 (*theory with presentation context*) | 105 Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) 106 (*proof node, finish, original theory*) | 107 Skipped_Proof of int * (generic_theory * generic_theory); 108 (*proof depth, resulting theory, original theory*) 109 110val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE; 111val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; 112val skipped_proof_node = fn Skipped_Proof _ => true | _ => false; 113 114fun cases_node f _ (Theory (gthy, _)) = f gthy 115 | cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) 116 | cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy; 117 118 119(* datatype state *) 120 121datatype state = State of node option * node option; (*current, previous*) 122 123fun theory_toplevel thy = State (SOME (Theory (Context.Theory thy, NONE)), NONE); 124 125val toplevel = State (NONE, NONE); 126 127fun is_toplevel (State (NONE, _)) = true 128 | is_toplevel _ = false; 129 130fun level (State (NONE, _)) = 0 131 | level (State (SOME (Theory _), _)) = 0 132 | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) 133 | level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1; (*different notion of proof depth!*) 134 135fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy, _)))) = 136 "at top level, result theory " ^ quote (Context.theory_name thy) 137 | str_of_state (State (NONE, _)) = "at top level" 138 | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode" 139 | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode" 140 | str_of_state (State (SOME (Proof _), _)) = "in proof mode" 141 | str_of_state (State (SOME (Skipped_Proof _), _)) = "in skipped proof mode"; 142 143 144(* current node *) 145 146fun node_of (State (NONE, _)) = raise UNDEF 147 | node_of (State (SOME node, _)) = node; 148 149fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); 150fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); 151fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); 152 153fun node_case f g state = cases_node f g (node_of state); 154 155fun previous_theory_of (State (_, NONE)) = NONE 156 | previous_theory_of (State (_, SOME prev)) = 157 SOME (cases_node Context.theory_of Proof.theory_of prev); 158 159val context_of = node_case Context.proof_of Proof.context_of; 160val generic_theory_of = node_case I (Context.Proof o Proof.context_of); 161val theory_of = node_case Context.theory_of Proof.theory_of; 162val proof_of = node_case (fn _ => error "No proof state") I; 163 164fun proof_position_of state = 165 (case node_of state of 166 Proof (prf, _) => Proof_Node.position prf 167 | _ => ~1); 168 169fun is_end_theory (State (NONE, SOME (Theory (Context.Theory _, _)))) = true 170 | is_end_theory _ = false; 171 172fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy 173 | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos) 174 | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos); 175 176 177(* presentation context *) 178 179structure Presentation_State = Proof_Data 180( 181 type T = state option; 182 fun init _ = NONE; 183); 184 185fun presentation_context0 state = 186 (case try node_of state of 187 SOME (Theory (_, SOME ctxt)) => ctxt 188 | SOME node => cases_node Context.proof_of Proof.context_of node 189 | NONE => 190 (case try Theory.get_pure () of 191 SOME thy => Proof_Context.init_global thy 192 | NONE => raise UNDEF)); 193 194fun presentation_context (state as State (current, _)) = 195 presentation_context0 state 196 |> Presentation_State.put (SOME (State (current, NONE))); 197 198fun presentation_state ctxt = 199 (case Presentation_State.get ctxt of 200 NONE => State (SOME (Theory (Context.Proof ctxt, SOME ctxt)), NONE) 201 | SOME state => state); 202 203 204(* print state *) 205 206fun pretty_context state = 207 (case try node_of state of 208 NONE => [] 209 | SOME node => 210 let 211 val gthy = 212 (case node of 213 Theory (gthy, _) => gthy 214 | Proof (_, (_, gthy)) => gthy 215 | Skipped_Proof (_, (_, gthy)) => gthy); 216 val lthy = Context.cases (Named_Target.theory_init) I gthy; 217 in Local_Theory.pretty lthy end); 218 219fun pretty_state state = 220 (case try node_of state of 221 NONE => [] 222 | SOME (Theory _) => [] 223 | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf) 224 | SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]); 225 226val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of; 227 228fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); 229 230val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract); 231 232 233 234(** toplevel transitions **) 235 236(* node transactions -- maintaining stable checkpoints *) 237 238exception FAILURE of state * exn; 239 240local 241 242fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) 243 | reset_presentation node = node; 244 245in 246 247fun apply_transaction f g node = 248 let 249 val cont_node = reset_presentation node; 250 val context = cases_node I (Context.Proof o Proof.context_of) cont_node; 251 fun state_error e nd = (State (SOME nd, SOME cont_node), e); 252 253 val (result, err) = 254 cont_node 255 |> Runtime.controlled_execution (SOME context) f 256 |> state_error NONE 257 handle exn => state_error (SOME exn) cont_node; 258 in 259 (case err of 260 NONE => tap g result 261 | SOME exn => raise FAILURE (result, exn)) 262 end; 263 264val exit_transaction = 265 apply_transaction 266 (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE) 267 | node => node) (K ()) 268 #> (fn State (node', _) => State (NONE, node')); 269 270end; 271 272 273(* primitive transitions *) 274 275datatype trans = 276 Init of unit -> theory | (*init theory*) 277 Exit | (*formal exit of theory*) 278 Keep of bool -> state -> unit | (*peek at state*) 279 Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*) 280 281local 282 283fun apply_tr _ (Init f) (State (NONE, _)) = 284 State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE f ()), NONE)), NONE) 285 | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) = 286 exit_transaction state 287 | apply_tr int (Keep f) state = 288 Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state 289 | apply_tr int (Transaction (f, g)) (State (SOME node, _)) = 290 apply_transaction (fn x => f int x) g node 291 | apply_tr _ _ _ = raise UNDEF; 292 293fun apply_union _ [] state = raise FAILURE (state, UNDEF) 294 | apply_union int (tr :: trs) state = 295 apply_union int trs state 296 handle Runtime.UNDEF => apply_tr int tr state 297 | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state 298 | exn as FAILURE _ => raise exn 299 | exn => raise FAILURE (state, exn); 300 301in 302 303fun apply_trans int trs state = (apply_union int trs state, NONE) 304 handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); 305 306end; 307 308 309(* datatype transition *) 310 311datatype transition = Transition of 312 {name: string, (*command name*) 313 pos: Position.T, (*source position*) 314 timing: Time.time, (*prescient timing information*) 315 trans: trans list}; (*primitive transitions (union)*) 316 317fun make_transition (name, pos, timing, trans) = 318 Transition {name = name, pos = pos, timing = timing, trans = trans}; 319 320fun map_transition f (Transition {name, pos, timing, trans}) = 321 make_transition (f (name, pos, timing, trans)); 322 323val empty = make_transition ("", Position.none, Time.zeroTime, []); 324 325 326(* diagnostics *) 327 328fun name_of (Transition {name, ...}) = name; 329fun pos_of (Transition {pos, ...}) = pos; 330 331fun command_msg msg tr = 332 msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^ 333 Position.here (pos_of tr); 334 335fun at_command tr = command_msg "At " tr; 336fun type_error tr = command_msg "Bad context for " tr; 337 338 339(* modify transitions *) 340 341fun name name = map_transition (fn (_, pos, timing, trans) => 342 (name, pos, timing, trans)); 343 344fun position pos = map_transition (fn (name, _, timing, trans) => 345 (name, pos, timing, trans)); 346 347fun add_trans tr = map_transition (fn (name, pos, timing, trans) => 348 (name, pos, timing, tr :: trans)); 349 350val reset_trans = map_transition (fn (name, pos, timing, _) => 351 (name, pos, timing, [])); 352 353 354(* basic transitions *) 355 356fun init_theory f = add_trans (Init f); 357 358fun is_init (Transition {trans = [Init _], ...}) = true 359 | is_init _ = false; 360 361fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; 362 363val exit = add_trans Exit; 364val keep' = add_trans o Keep; 365 366fun present_transaction f g = add_trans (Transaction (f, g)); 367fun transaction f = present_transaction f (K ()); 368 369fun keep f = add_trans (Keep (fn _ => f)); 370 371fun keep_proof f = 372 keep (fn st => 373 if is_proof st then f st 374 else if is_skipped_proof st then () 375 else warning "No proof state"); 376 377fun ignored pos = empty |> name "<ignored>" |> position pos |> keep (fn _ => ()); 378fun is_ignored tr = name_of tr = "<ignored>"; 379 380fun malformed pos msg = 381 empty |> name "<malformed>" |> position pos |> keep (fn _ => error msg); 382 383 384(* theory transitions *) 385 386fun generic_theory f = transaction (fn _ => 387 (fn Theory (gthy, _) => Theory (f gthy, NONE) 388 | _ => raise UNDEF)); 389 390fun theory' f = transaction (fn int => 391 (fn Theory (Context.Theory thy, _) => 392 let val thy' = thy 393 |> Sign.new_group 394 |> f int 395 |> Sign.reset_group; 396 in Theory (Context.Theory thy', NONE) end 397 | _ => raise UNDEF)); 398 399fun theory f = theory' (K f); 400 401fun begin_local_theory begin f = transaction (fn _ => 402 (fn Theory (Context.Theory thy, _) => 403 let 404 val lthy = f thy; 405 val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy); 406 val _ = 407 (case Local_Theory.pretty lthy of 408 [] => () 409 | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); 410 in Theory (gthy, SOME lthy) end 411 | _ => raise UNDEF)); 412 413val end_local_theory = transaction (fn _ => 414 (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (Named_Target.exit lthy), SOME lthy) 415 | _ => raise UNDEF)); 416 417fun open_target f = transaction (fn _ => 418 (fn Theory (gthy, _) => 419 let val lthy = f gthy 420 in Theory (Context.Proof lthy, SOME lthy) end 421 | _ => raise UNDEF)); 422 423val close_target = transaction (fn _ => 424 (fn Theory (Context.Proof lthy, _) => 425 (case try Local_Theory.close_target lthy of 426 SOME ctxt' => 427 let 428 val gthy' = 429 if can Local_Theory.assert ctxt' 430 then Context.Proof ctxt' 431 else Context.Theory (Proof_Context.theory_of ctxt'); 432 in Theory (gthy', SOME lthy) end 433 | NONE => raise UNDEF) 434 | _ => raise UNDEF)); 435 436fun restricted_context (SOME (strict, scope)) = 437 Proof_Context.map_naming (Name_Space.restricted strict scope) 438 | restricted_context NONE = I; 439 440fun local_theory' restricted target f = present_transaction (fn int => 441 (fn Theory (gthy, _) => 442 let 443 val (finish, lthy) = Named_Target.switch target gthy; 444 val lthy' = lthy 445 |> restricted_context restricted 446 |> Local_Theory.new_group 447 |> f int 448 |> Local_Theory.reset_group; 449 in Theory (finish lthy', SOME lthy') end 450 | _ => raise UNDEF)) 451 (K ()); 452 453fun local_theory restricted target f = local_theory' restricted target (K f); 454 455fun present_local_theory target = present_transaction (fn _ => 456 (fn Theory (gthy, _) => 457 let val (finish, lthy) = Named_Target.switch target gthy; 458 in Theory (finish lthy, SOME lthy) end 459 | _ => raise UNDEF)); 460 461 462(* proof transitions *) 463 464fun end_proof f = transaction (fn int => 465 (fn Proof (prf, (finish, _)) => 466 let val state = Proof_Node.current prf in 467 if can (Proof.assert_bottom true) state then 468 let 469 val ctxt' = f int state; 470 val gthy' = finish ctxt'; 471 in Theory (gthy', SOME ctxt') end 472 else raise UNDEF 473 end 474 | Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE) 475 | _ => raise UNDEF)); 476 477local 478 479fun begin_proof init = transaction (fn int => 480 (fn Theory (gthy, _) => 481 let 482 val (finish, prf) = init int gthy; 483 val document = Options.default_string "document"; 484 val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled (); 485 val schematic_goal = try Proof.schematic_goal prf; 486 val _ = 487 if skip andalso schematic_goal = SOME true then 488 warning "Cannot skip proof of schematic goal statement" 489 else (); 490 in 491 if skip andalso schematic_goal = SOME false then 492 Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) 493 else Proof (Proof_Node.init prf, (finish, gthy)) 494 end 495 | _ => raise UNDEF)); 496 497in 498 499fun local_theory_to_proof' restricted target f = begin_proof 500 (fn int => fn gthy => 501 let 502 val (finish, lthy) = Named_Target.switch target gthy; 503 val prf = lthy 504 |> restricted_context restricted 505 |> Local_Theory.new_group 506 |> f int; 507 in (finish o Local_Theory.reset_group, prf) end); 508 509fun local_theory_to_proof restricted target f = 510 local_theory_to_proof' restricted target (K f); 511 512fun theory_to_proof f = begin_proof 513 (fn _ => fn gthy => 514 (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, 515 (case gthy of 516 Context.Theory thy => f (Sign.new_group thy) 517 | _ => raise UNDEF))); 518 519end; 520 521fun forget_proof strict = transaction (fn _ => 522 (fn Proof (prf, (_, orig_gthy)) => 523 if strict andalso not (Proof.has_bottom_goal (Proof_Node.current prf)) 524 then raise UNDEF else Theory (orig_gthy, NONE) 525 | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 526 | _ => raise UNDEF)); 527 528fun proofs' f = transaction (fn int => 529 (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) 530 | skip as Skipped_Proof _ => skip 531 | _ => raise UNDEF)); 532 533fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); 534val proofs = proofs' o K; 535val proof = proof' o K; 536 537 538(* skipped proofs *) 539 540fun actual_proof f = transaction (fn _ => 541 (fn Proof (prf, x) => Proof (f prf, x) 542 | _ => raise UNDEF)); 543 544fun skip_proof f = transaction (fn _ => 545 (fn skip as Skipped_Proof _ => (f (); skip) 546 | _ => raise UNDEF)); 547 548val skip_proof_open = transaction (fn _ => 549 (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x) 550 | _ => raise UNDEF)); 551 552val skip_proof_close = transaction (fn _ => 553 (fn Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE) 554 | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x) 555 | _ => raise UNDEF)); 556 557 558 559(** toplevel transactions **) 560 561(* runtime position *) 562 563fun exec_id id (tr as Transition {pos, ...}) = 564 position (Position.put_id (Document_ID.print id) pos) tr; 565 566fun setmp_thread_position (Transition {pos, ...}) f x = 567 Position.setmp_thread_data pos f x; 568 569 570(* post-transition hooks *) 571 572local 573 val hooks = 574 Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list); 575in 576 577fun add_hook hook = Synchronized.change hooks (cons hook); 578fun get_hooks () = Synchronized.value hooks; 579 580end; 581 582 583(* apply transitions *) 584 585fun get_timing (Transition {timing, ...}) = timing; 586fun put_timing timing = map_transition (fn (name, pos, _, trans) => (name, pos, timing, trans)); 587 588local 589 590fun app int (tr as Transition {trans, ...}) = 591 setmp_thread_position tr 592 (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int trans) 593 ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)); 594 595in 596 597fun transition int tr st = 598 let 599 val (st', opt_err) = 600 Context.setmp_generic_context (try (Context.Proof o presentation_context0) st) 601 (fn () => app int tr st) (); 602 val opt_err' = opt_err |> Option.map 603 (fn Runtime.EXCURSION_FAIL exn_info => exn_info 604 | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); 605 val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ())); 606 in (st', opt_err') end; 607 608end; 609 610 611(* managed commands *) 612 613fun command_errors int tr st = 614 (case transition int tr st of 615 (st', NONE) => ([], SOME st') 616 | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE)); 617 618fun command_exception int tr st = 619 (case transition int tr st of 620 (st', NONE) => st' 621 | (_, SOME (exn, info)) => 622 if Exn.is_interrupt exn then Exn.reraise exn 623 else raise Runtime.EXCURSION_FAIL (exn, info)); 624 625val command = command_exception false; 626 627 628(* reset state *) 629 630local 631 632fun reset_state check trans st = 633 if check st then NONE 634 else #2 (command_errors false (trans empty) st); 635 636in 637 638val reset_theory = reset_state is_theory (forget_proof false); 639 640val reset_proof = 641 reset_state is_proof 642 (transaction (fn _ => 643 (fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy)) 644 | _ => raise UNDEF))); 645 646end; 647 648 649(* scheduled proof result *) 650 651datatype result = 652 Result of transition * state | 653 Result_List of result list | 654 Result_Future of result future; 655 656fun join_results (Result x) = [x] 657 | join_results (Result_List xs) = maps join_results xs 658 | join_results (Result_Future x) = join_results (Future.join x); 659 660local 661 662structure Result = Proof_Data 663( 664 type T = result; 665 fun init _ = Result_List []; 666); 667 668val get_result = Result.get o Proof.context_of; 669val put_result = Proof.map_context o Result.put; 670 671fun timing_estimate elem = 672 let val trs = tl (Thy_Syntax.flat_element elem) 673 in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end; 674 675fun future_proofs_enabled estimate st = 676 (case try proof_of st of 677 NONE => false 678 | SOME state => 679 not (Proof.is_relevant state) andalso 680 (if can (Proof.assert_bottom true) state 681 then Future.proofs_enabled 1 682 else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate)); 683 684fun atom_result keywords tr st = 685 let 686 val st' = 687 if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then 688 (Execution.fork 689 {name = "Toplevel.diag", pos = pos_of tr, pri = ~1} 690 (fn () => command tr st); st) 691 else command tr st; 692 in (Result (tr, st'), st') end; 693 694in 695 696fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st 697 | element_result keywords (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st = 698 let 699 val (head_result, st') = atom_result keywords head_tr st; 700 val (body_elems, end_tr) = element_rest; 701 val estimate = timing_estimate elem; 702 in 703 if not (future_proofs_enabled estimate st') 704 then 705 let 706 val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr]; 707 val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st'; 708 in (Result_List (head_result :: proof_results), st'') end 709 else 710 let 711 val finish = Context.Theory o Proof_Context.theory_of; 712 713 val future_proof = 714 Proof.future_proof (fn state => 715 Execution.fork 716 {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1} 717 (fn () => 718 let 719 val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st'; 720 val prf' = Proof_Node.apply (K state) prf; 721 val (result, result_state) = 722 State (SOME (Proof (prf', (finish, orig_gthy))), prev) 723 |> fold_map (element_result keywords) body_elems ||> command end_tr; 724 in (Result_List result, presentation_context0 result_state) end)) 725 #> (fn (res, state') => state' |> put_result (Result_Future res)); 726 727 val forked_proof = 728 proof (future_proof #> 729 (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o 730 end_proof (fn _ => future_proof #> 731 (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); 732 733 val st'' = st' 734 |> command (head_tr |> reset_trans |> forked_proof); 735 val end_result = Result (end_tr, st''); 736 val result = 737 Result_List [head_result, Result.get (presentation_context0 st''), end_result]; 738 in (result, st'') end 739 end; 740 741end; 742 743end; 744