Email Gateway (Oct 01 2026 at 10:37): Email Gateway (Oct 01 2026 at 10:37):From: "Becker, Hanno" <cl-isabelle-users@lists.cam.ac.uk>
Hi,
During code generation, Isabelle calls Axclass.unoverload for each code equation, and evaluates:
rewrite_rule ctxt (inst_thms ctxt)
What this does in an example: An equation may use addition on natural numbers through the generic addition operation. Before code generation, Isabelle replaces that operation with the constant registered for natural-number addition. inst_thms collects every equation used for replacements of this kind across the current theory. This preparation does not depend on the individual code equation, yet is repeated for each constant.
One can consider caching the prepared simplification rules in Axclass theory data. I added a tentative patch below (AI generated); probably there are better ways.
I also add a small theory file which illustrates the speedup, using code_timing to report preprocessing time. Locally on a 64-core AArch64 host using eight threads, processing took about 17 seconds with Isabelle2025-2, and about 11 seconds with the proposed change, a reduction of 36 percent.
The change was also evaluated in a larger internal project, leading to a reduction in runtime of a large export_code command from about 29 minutes to under 3 minutes.
I’m not requesting for this to be included in 2026 (I did not check if it applies equally), it’s just an observation that one may take into account for future revisions and that others may find interesting/useful.
Hanno
===== Code-export example ====
Code_Export_Observation.thy:
theory Code_Export_Observation
imports Main
begin
declare [[code_timing]]
export_code _ checking SML
end
==== Patch ====
diff --git a/src/Pure/axclass.ML b/src/Pure/axclass.ML
--- a/src/Pure/axclass.ML
+++ b/src/Pure/axclass.ML
@@ -72,12 +72,16 @@ datatype data = Data of
inst_params:
(string * thm) Symtab.table Symtab.table *
(*constant name ~> type constructor ~> (constant name, equation)*)
- (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*)};
+ (string * string) Symtab.table,
+ (*constant name ~> (constant name, type constructor)*)
+ unoverload_cache:
+ (Context.theory_id * Raw_Simplifier.simpset) option Synchronized.var};
fun rep_data (Data args) = args;
fun make_data (axclasses, params, inst_params) =
- Data {axclasses = axclasses, params = params, inst_params = inst_params};
+ Data {axclasses = axclasses, params = params, inst_params = inst_params,
+ unoverload_cache = Synchronized.var "Axclass.unoverload cache" NONE};
structure Data = Theory_Data'
(
@@ -104,7 +108,7 @@ structure Data = Theory_Data'
);
fun map_data f =
- Data.map (fn Data {axclasses, params, inst_params} =>
+ Data.map (fn Data {axclasses, params, inst_params, ...} =>
make_data (f (axclasses, params, inst_params)));
fun map_axclasses f =
@@ -124,6 +128,7 @@ val rep_theory_data = Data.get #> rep_data;
val axclasses_of = #axclasses o rep_theory_data;
val params_of = #params o rep_theory_data;
val inst_params_of = #inst_params o rep_theory_data;
+val unoverload_cache_of = #unoverload_cache o rep_theory_data;
(* axclasses with parameters *)
@@ -164,12 +169,32 @@ fun inst_thms ctxt =
(Symtab.fold (cons o #2 o #2) o #2) (#1 (inst_params_of (Proof_Context.theory_of ctxt))) []
|> map (Thm.transfer' ctxt);
+fun unoverload_simpset ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val thy_id = Context.theory_id thy;
+ val cache = unoverload_cache_of thy;
+ fun get NONE =
+ let
+ val simpset =
+ Raw_Simplifier.init_simpset (inst_thms ctxt) ctxt
+ |> Raw_Simplifier.simpset_of;
+ in (simpset, SOME (thy_id, simpset)) end
+ | get (SOME (thy_id', simpset)) =
+ if Context.eq_thy_id (thy_id, thy_id')
+ then (simpset, SOME (thy_id', simpset))
+ else get NONE;
+ in Synchronized.change_result cache get end;
+
+fun put_unoverload_simpset ctxt =
+ Raw_Simplifier.put_simpset (unoverload_simpset ctxt) ctxt;
+
fun get_inst_tyco consts = try (dest_Type_name o the_single o Consts.typargs consts);
-fun unoverload ctxt = rewrite_rule ctxt (inst_thms ctxt);
+fun unoverload ctxt = Raw_Simplifier.rewrite0_rule (put_unoverload_simpset ctxt);
fun overload ctxt = rewrite_rule ctxt (map Thm.symmetric (inst_thms ctxt));
-fun unoverload_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true (inst_thms ctxt);
+fun unoverload_conv ctxt = Raw_Simplifier.rewrite0 (put_unoverload_simpset ctxt) true;
fun overload_conv ctxt = Raw_Simplifier.rewrite_wrt ctxt true (map Thm.symmetric (inst_thms ctxt));
fun lookup_inst_param consts params (c, T) =
Last updated: Oct 08 2026 at 21:07 UTC