# HG changeset patch # User haftmann # Date 1748070386 -7200 # Node ID bd951e02d6b9265aee619388f70cda7b1f73f2d3 # Parent c833618d80eb167d25a0ef1caeec7b76c4435ee2 move legacy simplifier interfaces into separate file diff -r c833618d80eb -r bd951e02d6b9 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Thu May 22 19:59:43 2025 +0200 +++ b/src/FOL/IFOL.thy Sat May 24 09:06:26 2025 +0200 @@ -9,6 +9,7 @@ abbrevs "?<" = "\\<^sub>\\<^sub>1" begin +ML_file \~~/src/Tools/simp_legacy.ML\ ML_file \~~/src/Tools/misc_legacy.ML\ ML_file \~~/src/Provers/splitter.ML\ ML_file \~~/src/Provers/hypsubst.ML\ diff -r c833618d80eb -r bd951e02d6b9 src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Thu May 22 19:59:43 2025 +0200 +++ b/src/FOLP/IFOLP.thy Sat May 24 09:06:26 2025 +0200 @@ -9,6 +9,7 @@ imports Pure begin +ML_file \~~/src/Tools/simp_legacy.ML\ ML_file \~~/src/Tools/misc_legacy.ML\ setup Pure_Thy.old_appl_syntax_setup diff -r c833618d80eb -r bd951e02d6b9 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu May 22 19:59:43 2025 +0200 +++ b/src/HOL/HOL.thy Sat May 24 09:06:26 2025 +0200 @@ -13,6 +13,7 @@ abbrevs "?<" = "\\<^sub>\\<^sub>1" begin +ML_file \~~/src/Tools/simp_legacy.ML\ ML_file \~~/src/Tools/misc_legacy.ML\ ML_file \~~/src/Tools/try.ML\ ML_file \~~/src/Tools/quickcheck.ML\ diff -r c833618d80eb -r bd951e02d6b9 src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Thu May 22 19:59:43 2025 +0200 +++ b/src/Pure/raw_simplifier.ML Sat May 24 09:06:26 2025 +0200 @@ -4,11 +4,6 @@ Higher-order Simplification. *) -infix 4 - addsimps delsimps addsimprocs delsimprocs - setloop addloop delloop - setSSolver addSSolver setSolver addSolver; - signature BASIC_RAW_SIMPLIFIER = sig val simp_depth_limit: int Config.T @@ -38,17 +33,6 @@ val map_theory_simpset: (Proof.context -> Proof.context) -> theory -> theory val empty_simpset: Proof.context -> Proof.context val clear_simpset: Proof.context -> Proof.context - val addsimps: Proof.context * thm list -> Proof.context - val delsimps: Proof.context * thm list -> Proof.context - val addsimprocs: Proof.context * simproc list -> Proof.context - val delsimprocs: Proof.context * simproc list -> Proof.context - val setloop: Proof.context * (Proof.context -> int -> tactic) -> Proof.context - val addloop: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context - val delloop: Proof.context * string -> Proof.context - val setSSolver: Proof.context * solver -> Proof.context - val addSSolver: Proof.context * solver -> Proof.context - val setSolver: Proof.context * solver -> Proof.context - val addSolver: Proof.context * solver -> Proof.context val rewrite_rule: Proof.context -> thm list -> thm -> thm val rewrite_goals_rule: Proof.context -> thm list -> thm -> thm @@ -673,8 +657,6 @@ fun add_flipped_simps thms ctxt = comb_simps insert_rrule (mk_rrule ctxt) true thms ctxt; -fun ctxt addsimps thms = ctxt |> add_simps thms; - fun add_simp thm = add_simps [thm]; fun del_simps thms ctxt = @@ -683,8 +665,6 @@ fun del_simps_quiet thms ctxt = comb_simps (del_rrule false) (map mk_rrule2 o mk_rrule ctxt) false thms ctxt; -fun ctxt delsimps thms = ctxt |> del_simps thms; - fun del_simp thm = del_simps [thm]; fun flip_simps thms = del_simps_quiet thms #> add_flipped_simps thms; @@ -828,9 +808,6 @@ val add_proc = fold add_proc1 o split_proc; val del_proc = fold del_proc1 o split_proc; -fun ctxt addsimprocs ps = fold add_proc ps ctxt; -fun ctxt delsimprocs ps = fold del_proc ps ctxt; - end; @@ -888,15 +865,11 @@ map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, _, solvers) => (congs, procs, mk_rews, term_ord, subgoal_tac, [("", tac)], solvers)); -fun ctxt setloop tac = ctxt |> set_loop tac; - fun add_loop (name, tac) = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => (congs, procs, mk_rews, term_ord, subgoal_tac, AList.update (op =) (name, tac) loop_tacs, solvers)); -fun ctxt addloop tac = ctxt |> add_loop tac; - fun del_loop name ctxt = ctxt |> map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, solvers) => (congs, procs, mk_rews, term_ord, subgoal_tac, @@ -904,32 +877,22 @@ else cond_warning ctxt (fn () => "No such looper in simpset: " ^ quote name); AList.delete (op =) name loop_tacs), solvers)); -fun ctxt delloop name = ctxt |> del_loop name; - fun set_safe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, _)) => (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); -fun ctxt setSSolver solver = ctxt |> set_safe_solver solver; - fun add_safe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers))); -fun ctxt addSSolver solver = ctxt |> add_safe_solver solver; - fun set_unsafe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, ([solver], solvers))); -fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver; - fun add_unsafe_solver solver = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers))); -fun ctxt addSolver solver = ctxt |> add_unsafe_solver solver; - fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, term_ord, subgoal_tac, loop_tacs, (solvers, solvers))); diff -r c833618d80eb -r bd951e02d6b9 src/Sequents/Sequents.thy --- a/src/Sequents/Sequents.thy Thu May 22 19:59:43 2025 +0200 +++ b/src/Sequents/Sequents.thy Sat May 24 09:06:26 2025 +0200 @@ -10,6 +10,8 @@ keywords "print_pack" :: diag begin +ML_file \~~/src/Tools/simp_legacy.ML\ + setup Pure_Thy.old_appl_syntax_setup declare [[unify_trace_bound = 20, unify_search_bound = 40]] diff -r c833618d80eb -r bd951e02d6b9 src/Tools/simp_legacy.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/simp_legacy.ML Sat May 24 09:06:26 2025 +0200 @@ -0,0 +1,33 @@ +(* Title: Tools/simp_legacy.ML + +Legacy simplifier configuration interfaces -- to be phased out eventually. +*) + +infix 4 + addsimps delsimps addsimprocs delsimprocs + setloop addloop delloop + setSSolver addSSolver setSolver addSolver; + +local + +open Simplifier + +in + +fun ctxt addsimps thms = ctxt |> add_simps thms; +fun ctxt delsimps thms = ctxt |> del_simps thms; + +fun ctxt addsimprocs procs = ctxt |> fold add_proc procs; +fun ctxt delsimprocs procs = ctxt |> fold del_proc procs; + +fun ctxt setloop looper = ctxt |> set_loop looper; +fun ctxt addloop looper = ctxt |> add_loop looper; +fun ctxt delloop looper = ctxt |> del_loop looper; + +fun ctxt setSSolver solver = ctxt |> set_safe_solver solver; +fun ctxt addSSolver solver = ctxt |> add_safe_solver solver; + +fun ctxt setSolver solver = ctxt |> set_unsafe_solver solver; +fun ctxt addSolver solver = ctxt |> add_unsafe_solver solver; + +end