# [isabelle] global_interpretation and code generation

Hi.
Suppose I have the following locale hierachy:
A definition f = ...
A' = A + ...
B = A + ... definition h = ... f ...
I (globally) interpret i10: A', and then B (using the i10-
interpretation for the A part). The proof obligations are as expected,
however, it will not generate code equations for functions in B that
use functions from A.
If I build i10 stepwise, by first interpreting A and then A',
everything works fine. Is there a canonical way to obtain code
equations with global_interpretation? Does it include manually
providing interpretations for every super-locale, as worked in my case?
Is it documented somewhere?
--
Peter
locale A =
fixes n :: nat
assumes "n<42"
begin
definition "f x ≡ n+x"
end
locale A' = A + assumes "n<20"
locale B = A +
fixes m :: nat
assumes "m>42"
begin
definition "h x = f (x+m)"
end
global_interpretation i10: A' where n="10"
defines f_impl = i10.f
by
standard auto
global_interpretation B where n="10" and m="100"
defines h_impl = h
by standard auto
export_code h_impl checking SML
*** No code equations for A.f
************ This works:
global_interpretation i10: A where n="10"
defines f_impl = i10.f
by standard auto
global_interpretation i10: A' where n="10"
by standard auto
global_interpretation B where n="10" and m="100"
defines h_impl = h
by standard auto
export_code h_impl checking SML

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*