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

Stream: Beginner Questions

Topic: Code generation from locale interpretations within locale

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