Re: [isabelle] Code Generation with Locales that Fix Type Parameters



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
>>
>>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.