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