*To*: Brandon Bohrer <bbohrer at cs.cmu.edu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Code Generation with Locales that Fix Type Parameters*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 17 Feb 2017 13:02:29 +0100*In-reply-to*: <CA+cOFsa8cj1FOSY4-SS6UNjtFS3wZ9RXQqq=Ff36j-sQp2NPvQ@mail.gmail.com>*References*: <CA+cOFsa8cj1FOSY4-SS6UNjtFS3wZ9RXQqq=Ff36j-sQp2NPvQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

Dear Brandon,

lemmas [code] = Foo.test1.simps Foo.test2.simps Foo.test3.simps export_code Foo.test3 in SML

definition "bb_test3 = bb.test3" export_code bb_test3 in SML This option works only if your locale does not contain or inherit any "assumes" parts.

global_interpretation bb: Foo Enum.finite_2.aâ1 Enum.finite_2.aâ2 defines bb_test1 = bb.test1 and bb_test2 = bb.test2 and bb_test3 = bb.test3

Hope this helps, Andreas On 16/02/17 14:55, Brandon Bohrer wrote:

Hello All, I've been trying to generate code for functions that are defined inside a locale, but Isabelle is refusing and the error suggests it is related to the type variables fixed by my locale. Here is a toy example of the problem: theory "Codegen_Example" imports Complex_Main begin locale Foo = fixes x::"'type_param::finite" fixes y::"'type_param::finite" context Foo begin fun test1 :: "int \<Rightarrow> int" where "test1 n = n" fun test2 :: "'a \<Rightarrow> 'a" where "test2 n = n" fun test3 :: "int \<Rightarrow> 'type_param \<Rightarrow> int" where "test3 n _= n" end interpretation bb: Foo Enum.finite_2.a\<^sub>1 Enum.finite_2.a\<^sub>2 done (* Works *) export_code "bb.test1" in SML export_code "bb.test2" in SML (* Does Not Work*) export_code "bb.test3" in SML end The last "export_code" line gives the error: Type int â Enum.finite_2 â int of constant "Codegen_Example.Foo.test3" is too specific compared to declared type int â ?'type_param::{} â int I don't understand this error, because generating code for a specific instance 'type_param = Enum.finite_2 seems like something that ought to work (and Enum.finite_2 supports the finite typeclass). Does anyone know a way to convince Isabelle to generate code in such a situation (or fix my confusion as to why this is not supported?). It would actually be more convenient in my case to generate polymorphic code instead of fixing 'type_param = Enum.finite_2, but of course that's cheating in the sense that SML knows nothing about the finite typeclass thus cannot enforce it. Incidentally, in the real code, the reason for fixing the type parameters like this are (1) I use the assumption 'type_param::finite very frequently and it's nicer to only write it down once and (2) I frequently construct values based on x and y (and a number of other arguments) so it would be quite unwieldy if they were not locale parameters. Thanks in advance, Brandon

**Follow-Ups**:**Re: [isabelle] Code Generation with Locales that Fix Type Parameters***From:*Peter Lammich

**Re: [isabelle] Code Generation with Locales that Fix Type Parameters***From:*Florian Haftmann

**Re: [isabelle] Code Generation with Locales that Fix Type Parameters***From:*Brandon Bohrer

**References**:**[isabelle] Code Generation with Locales that Fix Type Parameters***From:*Brandon Bohrer

- Previous by Date: [isabelle] Code Generation with Locales that Fix Type Parameters
- Next by Date: Re: [isabelle] Code Generation with Locales that Fix Type Parameters
- Previous by Thread: [isabelle] Code Generation with Locales that Fix Type Parameters
- Next by Thread: Re: [isabelle] Code Generation with Locales that Fix Type Parameters
- Cl-isabelle-users February 2017 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