*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Code Generation with Locales that Fix Type Parameters*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Fri, 17 Feb 2017 20:06:17 +0100*In-reply-to*: <39a14b92-ec57-5ac0-0a2f-c1ce9e1d092d@inf.ethz.ch>*Organization*: TU Munich*References*: <CA+cOFsa8cj1FOSY4-SS6UNjtFS3wZ9RXQqq=Ff36j-sQp2NPvQ@mail.gmail.com> <39a14b92-ec57-5ac0-0a2f-c1ce9e1d092d@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

Hi Brandon, > 2. You define at the time of interpretation new constants for all the > terms you ever want to execute. You must use global_interpretation > instead of interpretation. > > 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 this approach is indeed canonical. CU, Florian > > > 3. You use one of Peter Lammich's tools from Autoref or Monadic > Refinement Framework that automates step 2. He can tell you more about > this. > > 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 >> > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

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

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

- Previous by Date: [isabelle] VSTTE 2017 - First Call for Papers
- Next by Date: [isabelle] Standardized notation <# -> \<subset>#
- Previous by Thread: Re: [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