--- a/src/HOL/Lattices_Big.thy Sun Jul 13 13:41:24 2025 +0200
+++ b/src/HOL/Lattices_Big.thy Sat Jul 12 07:36:38 2025 +0200
@@ -938,9 +938,7 @@
qualified definition Least_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
where \<open>Least_abort = Least\<close>
-declare [[code abort: Least_abort]]
-
-qualified lemma Least_code [code]:
+qualified lemma Least_code [code abort: Lattices_Big.Least_abort, code]:
\<open>Least A = (if finite A \<longrightarrow> Set.is_empty A then Least_abort A else Min A)\<close>
using Least_Min [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Least_abort_def)
@@ -954,9 +952,7 @@
qualified definition Greatest_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
where \<open>Greatest_abort = Greatest\<close>
-declare [[code abort: Greatest_abort]]
-
-qualified lemma Greatest_code [code]:
+qualified lemma Greatest_code [code abort: Lattices_Big.Greatest_abort, code]:
\<open>Greatest A = (if finite A \<longrightarrow> Set.is_empty A then Greatest_abort A else Max A)\<close>
using Greatest_Max [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Greatest_abort_def)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Jul 12 07:36:38 2025 +0200
@@ -158,7 +158,7 @@
(case proposed_modes of
Single_Pred proposed_modes => [(const, proposed_modes)]
| Multiple_Preds proposed_modes =>
- map (apfst (Code.read_const (Proof_Context.theory_of lthy))) proposed_modes)
+ map (apfst (Code.read_const lthy)) proposed_modes)
in
Options {
expected_modes = Option.map (pair const) expected_modes,
@@ -191,7 +191,7 @@
fun code_pred_cmd (((expected_modes, proposed_modes), raw_options), raw_const) lthy =
let
val thy = Proof_Context.theory_of lthy
- val const = Code.read_const thy raw_const
+ val const = Code.read_const lthy raw_const
val T = Sign.the_const_type thy const
val t = Const (const, T)
val options = extract_options lthy (((expected_modes, proposed_modes), raw_options), const)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Jul 12 07:36:38 2025 +0200
@@ -1623,8 +1623,7 @@
(* FIXME ... this is important to avoid changing the background theory below *)
fun generic_code_pred prep_const options raw_const lthy =
let
- val thy = Proof_Context.theory_of lthy
- val const = prep_const thy raw_const
+ val const = prep_const lthy raw_const
val lthy' = Local_Theory.background_theory (Core_Data.extend_intro_graph [const]) lthy
val thy' = Proof_Context.theory_of lthy'
val ctxt' = Proof_Context.init_global thy'
--- a/src/Pure/Isar/code.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/Pure/Isar/code.ML Sat Jul 12 07:36:38 2025 +0200
@@ -10,7 +10,7 @@
sig
(*constants*)
val check_const: theory -> term -> string
- val read_const: theory -> string -> string
+ val read_const: Proof.context -> string -> string
val string_of_const: theory -> string -> string
val args_number: theory -> string -> int
@@ -138,6 +138,8 @@
fun typscheme_equiv (ty1, ty2) =
Type.raw_instance (devarify ty1, ty2) andalso Type.raw_instance (devarify ty2, ty1);
+local
+
fun check_bare_const thy t = case try dest_Const t
of SOME c_ty => c_ty
| NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
@@ -156,11 +158,38 @@
string_of_typ thy ty_decl)
end;
-fun check_const thy = check_unoverload thy o check_bare_const thy;
+fun export_global ctxt thy =
+ Variable.export_terms ctxt (Proof_Context.init_global thy);
+
+in
+
+fun check_const thy =
+ check_bare_const thy #> check_unoverload thy;
+
+fun read_bare_const thy =
+ Syntax.read_term (Proof_Context.init_global thy) #> check_bare_const thy;
-fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy;
+fun read_const ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ in
+ Syntax.read_term ctxt
+ #> singleton (export_global ctxt thy)
+ #> Logic.unvarify_types_global
+ #> check_bare_const thy
+ #> check_unoverload thy
+ end;
-fun read_const thy = check_unoverload thy o read_bare_const thy;
+fun prospective_check_consts ctxt ts thy =
+ ts
+ |> export_global ctxt thy
+ |> map Logic.unvarify_types_global
+ |> map (check_const thy);
+
+val prospective_const_args = Args.context :|--
+ (fn ctxt => Scan.repeat1 Args.term >> prospective_check_consts ctxt);
+
+end;
(** executable specifications **)
@@ -1552,15 +1581,15 @@
(* attributes *)
-fun code_attribute f = Thm.declaration_attribute
- (fn thm => Context.mapping (f thm) I);
+fun code_attribute decl = Thm.declaration_attribute
+ (fn thm => Context.mapping (decl thm) I);
-fun code_thm_attribute g f =
- Scan.lift (g |-- Scan.succeed (code_attribute f));
+fun code_thm_attribute qualifier decl =
+ Scan.lift (qualifier |-- Scan.succeed (code_attribute decl));
-fun code_const_attribute g f =
- Scan.lift (g -- Args.colon) |-- Scan.repeat1 Args.term
- >> (fn ts => code_attribute (K (fold (fn t => fn thy => f ((check_const thy o Logic.unvarify_types_global) t) thy) ts)));
+fun code_const_attribute qualifier decl =
+ Scan.lift (qualifier -- Args.colon) |-- prospective_const_args
+ >> (fn prospective_cs => code_attribute (fn _ => fn thy => fold decl (prospective_cs thy) thy));
val _ = Theory.setup
(let
--- a/src/Tools/Code/code_haskell.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/Tools/Code/code_haskell.ML Sat Jul 12 07:36:38 2025 +0200
@@ -475,7 +475,7 @@
fun add_monad target' raw_c_bind thy =
let
- val c_bind = Code.read_const thy raw_c_bind;
+ val c_bind = Code.read_const (Proof_Context.init_global thy) raw_c_bind;
in
if target = target' then
thy
--- a/src/Tools/Code/code_preproc.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/Tools/Code/code_preproc.ML Sat Jul 12 07:36:38 2025 +0200
@@ -329,7 +329,7 @@
fun gen_trace_only prep_const raw_cs context =
let
- val cs = map (prep_const (Context.theory_of context)) raw_cs;
+ val cs = map (prep_const (Context.proof_of context)) raw_cs;
in Trace_Switch.put (SOME cs) context end;
val trace_only = gen_trace_only (K I);
--- a/src/Tools/Code/code_runtime.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/Tools/Code/code_runtime.ML Sat Jul 12 07:36:38 2025 +0200
@@ -727,10 +727,10 @@
let
val ctxt = Proof_Context.init_global thy;
val datatypes = map (fn (raw_tyco, raw_cos) =>
- (prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes;
+ (prep_type ctxt raw_tyco, (Option.map o map) (prep_const ctxt) raw_cos)) raw_datatypes;
val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes
|> apsnd flat;
- val functions = map (prep_const thy) raw_functions;
+ val functions = map (prep_const ctxt) raw_functions;
val consts = constrs @ functions;
val program = Code_Thingol.consts_program ctxt consts;
val result = runtime_code'' ctxt module_name program tycos consts
--- a/src/Tools/Code/code_target.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/Tools/Code/code_target.ML Sat Jul 12 07:36:38 2025 +0200
@@ -89,8 +89,6 @@
else error ("No such constant: " ^ quote const);
in const end;
-fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt);
-
fun cert_tyco ctxt tyco =
let
val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then ()
@@ -120,7 +118,7 @@
(cert_class ctxt) (apply2 (cert_class ctxt)) (cert_inst ctxt) I;
fun read_syms ctxt =
- Code_Symbol.map_attr (read_const ctxt) (read_tyco ctxt)
+ Code_Symbol.map_attr (Code.read_const ctxt) (read_tyco ctxt)
(Proof_Context.read_class ctxt) (apply2 (Proof_Context.read_class ctxt)) (read_inst ctxt) I;
fun cert_syms' ctxt =
@@ -128,7 +126,7 @@
(apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
fun read_syms' ctxt =
- Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
+ Code_Symbol.map_attr (apfst (Code.read_const ctxt)) (apfst (read_tyco ctxt))
(apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
fun check_name is_module s =
--- a/src/Tools/Code/code_thingol.ML Sun Jul 13 13:41:24 2025 +0200
+++ b/src/Tools/Code/code_thingol.ML Sat Jul 12 07:36:38 2025 +0200
@@ -995,8 +995,8 @@
| SOME s =>
(case try (unsuffix "._") s of
SOME name => ([], consts_of_select (this_theory name))
- | NONE => ([Code.read_const thy str], []))
- | NONE => ([Code.read_const thy str], []));
+ | NONE => ([Code.read_const ctxt str], []))
+ | NONE => ([Code.read_const ctxt str], []));
in apply2 flat o split_list o map read_const_expr end;
fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;