Code generation from locale interpretations within locale · Beginner Questions

Hi. I've got two locales A and B. Every instance of B yields various instances of A, defined via interpretation within the context of B. Later, I instantiate B using global_interpretation, naming a constant from A inherited in the context of B. However, code extraction fails for that constant. Fiddling a bit, I found a solution using code_unfold, but I don't know what I'm doing. So, my questions are: (a) Why is this not handled by global_interpretation already? (b) Why do I need to use code_unfold rather than code?

Here's a minimal example (with just one interpretation of A within B, for simplicity; I only highlighted this to explain why I'm not using sublocale):

theory Scratch
imports Main
begin

locale A =
  fixes a :: ‹'a::ab_semigroup_add ⇒ 'a›
  assumes a_linear: ‹⋀x y. a (x+y) = a x + a y›
begin
  definition "a_a" where ‹a_a ≡ a ∘ a›
end

thm A.a_a_def

locale B =
  fixes b :: ‹'a::ab_semigroup_add ⇒ 'a›
  assumes b_linear: ‹⋀x y. b (x+y) = b x + b y›

context B
begin
  definition ‹b_a ≡ λx. (b x) + (b x)›
  interpretation B_A : A b_a
    by (simp add: A_def B.b_a_def B.b_linear B_axioms
      ab_semigroup_add_class.add_ac(1) add.left_commute)
  lemmas B_A_axioms = B_A.A_axioms
  definition ‹b_a_a ≡ B_A.a_a›
end

global_interpretation IB : B ‹λ(x::nat). 2*x›
  defines b_a_export = ‹IB.b_a›
      and a_a_export = ‹IB.b_a_a›
  by (simp add: B_def)

―‹No code equations for ▩‹A.a_a››
export_code
  a_a_export
  in SML

―‹▩‹Partially applied constant "Scratch.b_a_export" on left hand side of equation, in theorem:
A.a_a b_a_export ≡ b_a_export ∘ b_a_export››
declare A.a_a_def[OF IB.B_A_axioms, code]

export_code
  a_a_export
  in SML

―‹Finally, this works, but I don't know why. Why ▩‹code_unfold› rather than ▩‹code›?
  Why is this not taken care of by ▩‹global_interpretation›?›
declare A.a_a_def[OF IB.B_A_axioms, code_unfold]

export_code
  a_a_export
  in SML

end

Alexandra Graß (Jan 14 2026 at 14:27):

I just came across this old thread and wanted to ask whether you ever found an answer? I currently struggle with a similar setup (or at least the same warnings and errors :wink:) and would also like to understand what is going on.

Regarding partially applied constants, I found this question on Stack Overflow. I do get the answer by René Thiemann, yet do not know how to get a non-specific code equation when there are assumptions in the locale.

Also, since I'm trying to export code for a recursive function, using code_unfold is not an option – export_code gets stuck in an endless loop.

Hanno Becker (Jan 14 2026 at 15:17):

I think this is a bug in the constant folding in the context of global_interpretation + sublocale/interpretation.

You can manually do the code equation extraction after the global_interpretation, but it is rather cumbersome. In the above example:

(* GOOD: b_a_export ≡ λx. 2 * x + 2 * x *)
thm IB.b_a_def

(* BAD: a_a_export ≡ A.a_a b_a_export *)
(* A.a_a b_a_export has not been unfolded. *)
thm IB.b_a_a_def

(* You need to manually unfold A.a_a, refering to the proof of A in B,
   and then register it as a code equation *)
declare IB.b_a_a_def[simplified A.a_a_def[OF IB.B_A_axioms], code]

(* Hooray! *)
export_code b_a_export in SML

Alexandra Graß (Jan 16 2026 at 09:09):

Thank you for replying so quickly! Still didn't succeed in setting up everything s.t. there is no warnings when declaring the code equations, even with your helpful suggestions above (but again, slightly different setup). I'm currently trying to construct a MWE and will come back to this thread as soon as that exists :)

Stream: Beginner Questions

Topic: Code generation from locale interpretations within locale

Hanno Becker (Aug 28 2023 at 07:51):

Alexandra Graß (Jan 14 2026 at 14:27):

Hanno Becker (Jan 14 2026 at 15:17):

Alexandra Graß (Jan 16 2026 at 09:09):

Hanno Becker (Jan 16 2026 at 09:51):