# HG changeset patch
# User haftmann
# Date 1752298598 -7200
# Node ID 52cf8f3f16525eb395d9cbf510482b81ff2494a0
# Parent  ca4aed6a9eb0a0ea85a91c34e330fe9f765f5941
always use proper context when parsing constants

diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/HOL/Lattices_Big.thy
--- 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)
 
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- 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)
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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'
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/Pure/Isar/code.ML
--- 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
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/Tools/Code/code_haskell.ML
--- 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
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/Tools/Code/code_preproc.ML
--- 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);
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/Tools/Code/code_runtime.ML
--- 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
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/Tools/Code/code_target.ML
--- 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 =
diff -r ca4aed6a9eb0 -r 52cf8f3f1652 src/Tools/Code/code_thingol.ML
--- 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;