*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Code Generation with Locales that Fix Type Parameters*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 17 Feb 2017 14:30:54 +0100*In-reply-to*: <39a14b92-ec57-5ac0-0a2f-c1ce9e1d092d@inf.ethz.ch>*References*: <CA+cOFsa8cj1FOSY4-SS6UNjtFS3wZ9RXQqq=Ff36j-sQp2NPvQ@mail.gmail.com> <39a14b92-ec57-5ac0-0a2f-c1ce9e1d092d@inf.ethz.ch>

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. Unfortunately, the Locale_Code tool Andreas probably refers to does not work for this particular case.Â This tool was specifically developed for the needs of the Isabelle Collection Framework. It's a workaround, and after being told that this hack is of no general interest as it should be done properly, I did not invest more work to make it usable in more general cases. Anyway, 5 years later, the problem of generating code from locale interpretations *without* writing tons of boilerplate seems still not solved. So again, here the idea of my hack: Before and after interpreting a locale, record the existing Spec_Rules. After interpreting the locale, make a diff to find the new spec rules, and process them to automatically set up new code equations. However, as far as I can remember, the current implementation only declares new code equations, without defining new constants.Â SeeÂ"$AFP/Collections/ICF/tools/Locale_Code_Ex" and the Isabelle Collection Framework for examples where it actually works and the three linesÂ setup Locale_Code.open_block interpretation ... setup Locale_Code.close_block declare dozens of code theorems, thus saving dozens of boilerplate declarations as would be required for method 1 or 2. -- Â Peter > > 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 > >

**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: Re: [isabelle] Code Generation with Locales that Fix Type Parameters
- Next by Date: [isabelle] VSTTE 2017 - First Call for Papers
- 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