Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code Generation with Locales that Fix Type Par...

view this post on Zulip Email Gateway (Aug 22 2022 at 15:05):

From: Brandon Bohrer <bbohrer@cs.cmu.edu>
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
Codegen_Example.thy

view this post on Zulip Email Gateway (Aug 22 2022 at 15:05):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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.

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

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

view this post on Zulip Email Gateway (Aug 22 2022 at 15:06):

From: Peter Lammich <lammich@in.tum.de>

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

Unfortunately, the Locale_Code tool Andreas probably refers to does not
work for this particular case. 

This tool was specifically developed for the needs of the Isabelle
Collection Framework. It's a workaround, and after being told that this
hack is of no general interest as it should be done properly, I did not
invest more work to make it usable in more general cases.

Anyway, 5 years later, the problem of generating code from locale
interpretations without writing tons of boilerplate seems still not
solved.

So again, here the idea of my hack:

Before and after interpreting a locale, record the existing Spec_Rules.
After interpreting the locale, make a diff to find the new spec rules,
and process them to automatically set up new code equations.

However, as far as I can remember, the current implementation only
declares new code equations, without defining new constants. 

See "$AFP/Collections/ICF/tools/Locale_Code_Ex" and the Isabelle
Collection Framework for examples where it actually works and the three
lines 

setup Locale_Code.open_block
interpretation ...
setup Locale_Code.close_block

declare dozens of code theorems, thus saving dozens of boilerplate declarations as would be required for method 1 or 2.

view this post on Zulip Email Gateway (Aug 22 2022 at 15:06):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Brandon,

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

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

signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 15:06):

From: Brandon Bohrer <bbohrer@cs.cmu.edu>
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.

view this post on Zulip Email Gateway (Aug 22 2022 at 15:06):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Brandon,

code_pred does not work inside the locale, but you can use it with global_interpretation.
Here's an example:

locale l = fixes x :: 'a assumes "x = x"
inductive (in l) is_x where "is_x x"
global_interpretation i: l "0 :: nat" defines i_is_x = "i.is_x" by unfold_locales simp

declare i.is_x.intros[code_pred_intro]
code_pred i_is_x by(rule i.is_x.cases)
thm i_is_x.equation

The crucial line is the re-declaration of the intro rules.

Hope this helps,
Andreas

Last updated: Nov 21 2024 at 12:39 UTC