*To*: Dmitriy Traytel <traytel at in.tum.de>*Subject*: Re: [isabelle] Code generation for sorts from locales*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sun, 16 Sep 2012 17:34:06 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <5054E224.9070707@in.tum.de>*Organization*: TU Munich*References*: <5054E224.9070707@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:15.0) Gecko/20120827 Thunderbird/15.0

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 -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Code generation for sorts from locales***From:*Dmitriy Traytel

**Re: [isabelle] Code generation for sorts from locales***From:*Florian Haftmann

**References**:**[isabelle] Code generation for sorts from locales***From:*Dmitriy Traytel

- Previous by Date: Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)
- Next by Date: Re: [isabelle] Code generation for sorts from locales
- Previous by Thread: [isabelle] Code generation for sorts from locales
- Next by Thread: Re: [isabelle] Code generation for sorts from locales
- Cl-isabelle-users September 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list