[isabelle] Code Generation with Locales that Fix Type Parameters



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

Attachment: Codegen_Example.thy
Description: Binary data



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