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