*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Code Generation with Locales that Fix Type Parameters*From*: Brandon Bohrer <bbohrer at cs.cmu.edu>*Date*: Thu, 16 Feb 2017 08:55:41 -0500

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

**Attachment:
Codegen_Example.thy**

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

- Previous by Date: Re: [isabelle] [ExternalEmail] Unwanted dependency documents in AFP
- Next by Date: Re: [isabelle] Code Generation with Locales that Fix Type Parameters
- Previous by Thread: Re: [isabelle] [ExternalEmail] Unwanted dependency documents in AFP
- 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