Email Gateway (Aug 18 2022 at 13:18): Email Gateway (Aug 18 2022 at 13:18):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
Email Gateway (Aug 18 2022 at 13:18):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Last updated: May 03 2024 at 12:27 UTC