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



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
Description: OpenPGP digital signature



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