*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Code Generation with Locales that Fix Type Parameters*From*: Brandon Bohrer <bbohrer at cs.cmu.edu>*Date*: Tue, 21 Feb 2017 09:31:12 -0500*Cc*: cl-isabelle-users at lists.cam.ac.uk*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>

Hi Andreas, Thank you for such a detailed response! Solution #2 got export_code to work (my locale has assumptions, so #1 was not an option). I don't mind the boilerplate code so long as it works. My locale also has some inductive predicates for which I would like to generate code. Am I correct that the predicate compiler doesn't work inside locales that have assumptions? The following thread seems to suggest so: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-January/msg00063.html If that's the case, it shouldn't be too hard to turn all my predicates into functions. It just looks cleaner when they're written as inductive predicates, so it would be nice if code generation for predicates happens to work. On Fri, Feb 17, 2017 at 7:02 AM, Andreas Lochbihler < andreas.lochbihler at inf.ethz.ch> wrote: > Dear Brandon, > > The underlying reason is not related to type classes. It is simply that > you must do some work to get the code generator work on interpretations of > locales. You have three options: > > 1. Export the code for the general constant Foo.test3 after having > re-declared the code equations on the theory level: > > lemmas [code] = Foo.test1.simps Foo.test2.simps Foo.test3.simps > > export_code Foo.test3 in SML > > In addition, if you want to get the specialisation for the interpretation, > you must define a constant instead of the abbreviation: > > 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. > > > 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 > > > 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 >> >>

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

**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] Overlapping patterns in code export
- Next by Date: Re: [isabelle] Code Generation with Locales that Fix Type Parameters
- 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