Re: [isabelle] Code generation for functions defined in locales



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

-- 

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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