# [isabelle] Question concerning code-generator

Dear all,

`I have some problems using locales in combination with the code-
``generator.
`
Consider the following simple example:
locale loc =
fixes foo :: "'a ⇒ 'a ⇒ 'a"
assumes "foo x y = foo y x"
begin
fun bar where "bar x = foo x x"
end
interpretation interI : loc [ "op + :: nat ⇒ nat ⇒ nat"]
by (unfold_locales, auto)

`fun myplus :: "nat ⇒ nat ⇒ nat" where "myplus x y = 3 * x + y - 2 *
``x"
`
interpretation interII : loc [ "myplus :: nat ⇒ nat ⇒ nat"]
by (unfold_locales, auto)
(* created two different interpretations of loc *)
(* and one can extract and reason about corresponding functions *)
fun doubleI where "doubleI x = interI.bar x"
fun doubleII where "doubleII x = interII.bar x"
fun doubleIII where "doubleIII x = 2 * x"
lemma "doubleI x = doubleII x" by simp
lemma "doubleI x = doubleIII x" by simp
(* however, code generation does not work *)
export_code doubleI in Haskell file "mytest"
*** No defining equations for constant "loc.bar"
*** At command "export_code".
If one defines bar outside of the locale, then there is no problem.
Is there any solution to this problem (beside not using locales)?
Thanks,
René
--
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck

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