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



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.