Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Code generation of a definition obtained throu...

Email Gateway (Aug 08 2020 at 10:10):

From: isabelle-users@florianmaerkl.de
Hello everyone,

I am currently struggling with the following issue, which I tried to
condense into a minimal example:
I have two locales "FinalThing" and "DetailThing" where FinalThing
defines some useful definition "final_result" and DetailThing is made a
sublocale of FinalThing:

locale FinalThing =
  fixes somefunc :: "nat ⇒ nat"
  assumes "somefunc 42 = 1337"
begin
definition "final_result = somefunc 42"
end

locale DetailThing =
  fixes someval :: "nat"
  assumes "someval = 1336"

context DetailThing
begin
fun thefunc :: "nat ⇒ nat" where
  "thefunc _ = someval + 1"
end
sublocale DetailThing ⊆ DetailSub: FinalThing
  where somefunc = thefunc

(...)

Now I interpret DetailThing and want to execute final_result from this
interpretation:

global_interpretation DetailThing
  where someval = "1334 + 2"
  defines final_result_impl = DetailSub.final_result
  and the_func_impl = thefunc
  by (standard, simp)

export_code the_func_impl in SML ― ‹works because of the "defines
final_result_impl = FinalThing.final_result"›
export_code final_result_impl in SML ― ‹doesn't work despite the
"defines the_func_impl = thefunc"›

Here, I can generate code for thefunc since as it is defined directly in
DetailThing, but for final_result I get the error "No code equations for
final_result_impl".
I found this old thread describing the same problem as far as I
understood:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-October/msg00034.html
However the proposed solution uses permanent_interpretation which
apparently doesn't exist anymore and I am unsure what the equivalent in
Isabelle 2020 would be.

I've attached the full theory.

Cheers

Florian
SublocaleTest.thy

Email Gateway (Aug 17 2020 at 17:50):

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

I did not study your example in full but from

global_interpretation DetailThing
where someval = "1334 + 2"
defines the_func_impl = thefunc
and final_result_impl = DetailSub.final_result
by standard simp

find_theorems final_result_impl

you see that no suitable code equations is provided for
final_result_impl, and looking at the theorems

thm final_result_impl_def DetailSub.final_result_def

I guess this is due to your definitions not forming a confluent system,
maybe due to the construction

fun thefunc :: "nat ⇒ nat" where
"thefunc _ = someval + 1"

which drops an argument. (A rough first guess).

In this case you have to provide your code equation explicitly.

Note that global_interpretation is the offical successor of prototypic
permanent_interpretation.

Cheers,
Florian
signature.asc

Last updated: Jul 15 2022 at 23:21 UTC