[isabelle] Code generation for functions defined in locales

[Peter Lammich]

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

[Florian Haftmann]

Hi Peter,

the bad news are that there is no direct way to accomplish code
generation from equations stemming from interpretation. The good news
are that you can use the optional "where" part of interpretation to
manually accomplish this:

locale test =
fixes a :: "nat => nat"
begin

primrec test where
"test [] = (0::nat)" |
"test (x#xs) = a(x + test xs)"

definition "c = a (7::nat)"

end

definition "nf x = x"

(* define constants corresponding to the local specifications *)
definition "t = test.test nf"
definition "c = test.c nf"

interpretation t: test nf where
(* give these as equations *)
"test.test nf = t"
and "test.c nf = c"
proof
qed (simp_all add: t_def c_def)

lemmas [code] = t.c_def t.test.simps

definition "some_fun l = t.c + t.test l"

export_code some_fun in SML file -

Hope this helps
Florian