Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation for sorts from locales

Email Gateway (Aug 19 2022 at 08:36):

From: Dmitriy Traytel <traytel@in.tum.de>
Hi all,

I've stumbled across a problem with the dictionary trick for sorts. I'm
generating code from locales following the guidelines in "Code
generation from Isabelle/HOL theories" (the Haftmann trick, as Lukas
calls it).

Attached is a reduced example where the resulting code contains
non-linear patterns (for the sort arguments) in the generated
ML-functions (same for Isabelle2012 and e.g. ac2e29fc57a5).

Am I doing something wrong?

Best wishes,
Dmitriy
Code.thy

Email Gateway (Aug 19 2022 at 08:37):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dmitriy,

theory Code
imports Main
begin

locale A =
fixes b :: 'b
and ba :: "'b \<Rightarrow> 'a :: linorder"
and baa :: "'b \<Rightarrow> 'a \<Rightarrow> 'a :: linorder"
assumes "baa b a = a"
begin

definition code :: "'a \<Rightarrow> 'a" where
"code a = baa b a"

end

definition my_code where [code del]: "my_code \<equiv> \<lambda>a. A.code a (\<lambda>_. id)"

interpretation A as id "\<lambda>_. id" where "A.code as (\<lambda>_. id) = my_code as" sorry

export_code my_code in SML

end

your experience boils down to the following

definition foo :: "'a ⇒ 'b ⇒ 'b"
where "foo x = id"

lemma [code]:
"foo (x :: 'a) = (id :: 'a ⇒ 'a)"
by (simp add: foo_def)

export_code foo in Haskell

i.e. currently the code generator accepts code equations which violate
the precondition that the type scheme of the constant in the theorem
(here, 'a => 'a => 'a) must match to the type scheme of the constant in
the theory (here, 'a => 'b => 'b). I will have to investigate this and
to repair the corresponding check.

Note that in order for your example to work, you must generalize your
interpretation to let A.my_code have a suitable type scheme for my_code.

Thanks a lot,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 08:37):

From: Dmitriy Traytel <traytel@in.tum.de>
Hi Florian,

On 16.09.2012 17:34, Florian Haftmann wrote:

your experience boils down to the following

definition foo :: "'a ⇒ 'b ⇒ 'b"
where "foo x = id"

lemma [code]:
"foo (x :: 'a) = (id :: 'a ⇒ 'a)"
by (simp add: foo_def)

export_code foo in Haskell
i.e. currently the code generator accepts code equations which violate
the precondition that the type scheme of the constant in the theorem
(here, 'a => 'a => 'a) must match to the type scheme of the constant in
the theory (here, 'a => 'b => 'b). I will have to investigate this and
to repair the corresponding check.
I see. At least one out of three keywords in the title of my email was
appropriate :-)
Note that in order for your example to work, you must generalize your
interpretation to let A.my_code have a suitable type scheme for my_code.
I have restricted the type of my_code instead and it works.

Thanks!

Dmitriy

Email Gateway (Aug 19 2022 at 08:40):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now http://isabelle.in.tum.de/reports/Isabelle/rev/791e6fc53f73

Florian
signature.asc

Last updated: Apr 20 2024 at 08:16 UTC