# HG changeset patch # User desharna # Date 1710530630 -3600 # Node ID e6f0a93e2edd7265913fa23a861ab1b64ed3c4f4 # Parent 1f509d01c9e349d6cb5f926c7569a905451376a5# Parent 1cfc913987d95a5760c7711b4b969d390390bca1 merged diff -r 1f509d01c9e3 -r e6f0a93e2edd src/HOL/ex/Sketch_and_Explore.thy --- a/src/HOL/ex/Sketch_and_Explore.thy Fri Mar 15 18:54:15 2024 +0100 +++ b/src/HOL/ex/Sketch_and_Explore.thy Fri Mar 15 20:23:50 2024 +0100 @@ -6,7 +6,7 @@ theory Sketch_and_Explore imports Main \ \TODO: generalize existing sledgehammer functions to Pure\ - keywords "sketch" "nxsketch" "explore" :: diag + keywords "sketch" "explore" :: diag begin ML \ @@ -26,26 +26,20 @@ t |> singleton (Syntax.uncheck_terms ctxt) |> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt - \ \TODO pointless to annotate explicit fixes in term\ |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |> Sledgehammer_Util.simplify_spaces |> ATP_Util.maybe_quote ctxt; -fun eigen_context_for_statement (fixes, assms, concl) ctxt = +fun eigen_context_for_statement (params, assms, concl) ctxt = let - val (fixes', ctxt') = Variable.add_fixes (map fst fixes) ctxt; - val subst_free = AList.lookup (op =) (map fst fixes ~~ fixes') - val subst = map_aterms (fn Free (v, T) => Free (the_default v (subst_free v), T) - | t => t) - val assms' = map subst assms; - val concl' = subst concl; - in ((fixes, assms', concl'), ctxt') end; + val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params + val ctxt' = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd + in ((params, assms, concl), ctxt') end; fun print_isar_skeleton ctxt indent keyword stmt = let val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt; val prefix = replicate_string indent " "; - \ \TODO consider pre-existing indentation -- how?\ val prefix_sep = "\n" ^ prefix ^ " and "; val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl; val if_s = if null assms then NONE @@ -60,17 +54,14 @@ s end; -fun print_nonext_sketch ctxt method_text clauses = - "proof" ^ method_text :: map (print_isar_skeleton ctxt 2 "show") clauses @ ["qed"]; - -fun print_next_skeleton ctxt indent keyword stmt = +fun print_skeleton ctxt indent keyword stmt = let val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt; val prefix = replicate_string indent " "; - val prefix_sep = "\n" ^ prefix ^ " and "; + val prefix_sep = "\n" ^ prefix ^ " and "; val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl; val assumes_s = if null assms then NONE - else SOME (prefix ^ " assume " ^ space_implode prefix_sep + else SOME (prefix ^ "assume " ^ space_implode prefix_sep (map (print_term ctxt') assms)); val fixes_s = if null fixes then NONE else SOME (prefix ^ "fix " ^ space_implode prefix_sep @@ -80,11 +71,8 @@ s end; -fun print_next_sketch ctxt method_text clauses = - "proof" ^ method_text :: separate "next" (map (print_next_skeleton ctxt 2 "show") clauses) @ ["qed"]; - -fun print_sketch ctxt method_text [cl] = print_next_sketch ctxt method_text [cl] - | print_sketch ctxt method_text clauses = print_nonext_sketch ctxt method_text clauses; +fun print_sketch ctxt method_text clauses = + "proof" ^ method_text :: separate "next" (map (print_skeleton ctxt 2 "show") clauses) @ ["qed"]; fun print_exploration ctxt method_text [clause] = ["proof -", print_isar_skeleton ctxt 2 "have" clause, @@ -123,23 +111,18 @@ if is_none some_method_ref then [" .."] else [" by" ^ method_text] else print ctxt_print method_text clauses; - val message = Active.sendback_markup_properties [] (cat_lines lines); + val message = Active.sendback_markup_command (cat_lines lines); in (state |> tap (fn _ => Output.information message)) end val sketch = print_proof_text_from_state print_sketch; -val next_sketch = print_proof_text_from_state print_next_sketch; - fun explore method_ref = print_proof_text_from_state print_exploration (SOME method_ref); fun sketch_cmd some_method_text = Toplevel.keep_proof (K () o sketch some_method_text o Toplevel.proof_of) -fun next_sketch_cmd some_method_text = - Toplevel.keep_proof (K () o next_sketch some_method_text o Toplevel.proof_of) - fun explore_cmd method_text = Toplevel.keep_proof (K () o explore method_text o Toplevel.proof_of) @@ -149,11 +132,6 @@ (Scan.option (Scan.trace Method.parse) >> sketch_cmd); val _ = - Outer_Syntax.command \<^command_keyword>\nxsketch\ - "print sketch of Isar proof text after method application" - (Scan.option (Scan.trace Method.parse) >> next_sketch_cmd); - -val _ = Outer_Syntax.command \<^command_keyword>\explore\ "explore proof obligations after method application as Isar proof text" (Scan.trace Method.parse >> explore_cmd); diff -r 1f509d01c9e3 -r e6f0a93e2edd src/Pure/Build/build_process.scala --- a/src/Pure/Build/build_process.scala Fri Mar 15 18:54:15 2024 +0100 +++ b/src/Pure/Build/build_process.scala Fri Mar 15 20:23:50 2024 +0100 @@ -911,7 +911,7 @@ /* collective operations */ - def pull_database(db: SQL.Database, build_id: Long, worker_uuid: String, state: State): State = { + def pull_state(db: SQL.Database, build_id: Long, worker_uuid: String, state: State): State = { val serial_db = read_serial(db) if (serial_db == state.serial) state else { @@ -928,7 +928,7 @@ } } - def update_database( + def push_state( db: SQL.Database, build_id: Long, worker_uuid: String, @@ -1124,11 +1124,11 @@ case Some(db) => Build_Process.private_data.transaction_lock(db, label = label) { val old_state = - Build_Process.private_data.pull_database(db, build_id, worker_uuid, _state) + Build_Process.private_data.pull_state(db, build_id, worker_uuid, _state) _state = old_state val res = body _state = - Build_Process.private_data.update_database( + Build_Process.private_data.push_state( db, build_id, worker_uuid, _state, old_state) res } diff -r 1f509d01c9e3 -r e6f0a93e2edd src/Pure/Build/build_schedule.scala --- a/src/Pure/Build/build_schedule.scala Fri Mar 15 18:54:15 2024 +0100 +++ b/src/Pure/Build/build_schedule.scala Fri Mar 15 20:23:50 2024 +0100 @@ -879,15 +879,15 @@ case Some(db) => db.transaction_lock(Build_Schedule.private_data.all_tables, label = label) { val old_state = - Build_Process.private_data.pull_database(db, build_id, worker_uuid, _state) + Build_Process.private_data.pull_state(db, build_id, worker_uuid, _state) val old_schedule = Build_Schedule.private_data.pull_schedule(db, _schedule) _state = old_state _schedule = old_schedule val res = body _state = - Build_Process.private_data.update_database( + Build_Process.private_data.push_state( db, build_id, worker_uuid, _state, old_state) - _schedule = Build_Schedule.private_data.update_schedule(db, _schedule, old_schedule) + _schedule = Build_Schedule.private_data.pull_schedule(db, _schedule, old_schedule) res } } @@ -1273,7 +1273,7 @@ } } - def update_schedule(db: SQL.Database, schedule: Schedule, old_schedule: Schedule): Schedule = { + def pull_schedule(db: SQL.Database, schedule: Schedule, old_schedule: Schedule): Schedule = { val changed = schedule.generator != old_schedule.generator || schedule.start != old_schedule.start ||