# [isabelle] Code generation for functions defined in locales

Hi all,
I have a problem when I try to generate code from constants/functions
defined inside a locale that fixes some parameter of function type.
Consider the following (synthetic) example:
locale test =
fixes a::"nat => nat"
begin
fun test where
"test [] = (0::nat)" |
"test (x#xs) = a(x + test xs)"
definition "c = a (7::nat)"
end
(* Now I interpret this locale with some function: *)
definition "nf x = x"
interpretation t: test nf .
(* And use the resulting instance in some further definitions*)
definition "some_fun l == t.c + t.test l"
(* Now I want to generate code for some_fun: *)
(* First try: *)
export_code some_fun in SML
*** No code equations for test.test, test.c
*** At command "export_code".
(* Second try: *)
lemmas [code] = t.c_def t.test.simps
*** Partially applied constant on left hand side of equation
*** "test.c nf º
*** nf (number_nat_inst.number_of_nat
*** (Int.Bit1 (Int.Bit1 (Int.Bit1 Int.Pls))))"
*** At command "lemmas".
(* Finally I had to manually insert new constants and adjust the lemmas
for the code-generator: *)
definition "t=t.test"
definition "c = t.c"
lemmas [code] = t.test.simps[folded t_def]
lemmas [code] = t.c_def[folded c_def]
lemmas [code unfold] = t_def[symmetric] c_def[symmetric]
export_code some_fun in SML
The final approach worked, but it is somewhat cumbersome to manually
insert constants for each definition and interpretation of the locale.
Is there a simpler (i.e. more automatic) way ?
Regards + Many thanks in advance for any hints
Peter

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