[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.