Email Gateway (Aug 18 2022 at 13:20): Email Gateway (Aug 18 2022 at 13:20):From: René Thiemann <rene.thiemann@uibk.ac.at>
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é
Last updated: May 03 2024 at 08:18 UTC