Email Gateway (Aug 19 2022 at 09:45): Email Gateway (Aug 19 2022 at 09:45):From: René Neumann <rene.neumann@in.tum.de>
Hi,
in my theories I have a fun foo, but I'd like to have it called 'bar' in
my SML code (in usage and definition). Is this possible in general
(without having to add a function bar to Isabelle with the same content
as foo)?
I tried:
definition "bar = foo"
lemma [code_unfold]: "foo = bar" by (simp add: bar_def)
but this did not work out as expected.
Thanks,
René
smime.p7s
Email Gateway (Aug 19 2022 at 09:47):From: andreas.lochbihler@kit.edu
Hi Rene,
the code generator provides no means to specify how a constant be named
in the generated code, so you have to introduce another constant with
the desired name and do the necessary setup yourself. Your attempt
already pursued the right direction, but it was not complete. You must
also transfer foo's code equation to bar:
lemmas [code] = foo.simps[folded bar_def] (* if foo is defined with
primrec or fun *)
foo_def[folded bar_def] (* if foo is defined with definition *)
xxx[folded bar_def] (* if xxx is your custom code equation for foo *)
Here's how this works:
code_unfold on an equation "lhs = rhs" tells the code generator to
replace any lhs instance on the right-hand side of any other code
equation with the appropriate rhs. Thus, it rewrites usages of foo to
usages of bar.
The above addition declares foo's code equation for bar, hence bar
becomes implemented the same way as foo would.
Afterwards, you can even remove foo's code equations from the code
generator setup, if you wished to do so.
Hope this helps,
Andreas
Quoting René Neumann <rene.neumann@in.tum.de>:
Email Gateway (Aug 19 2022 at 09:51):From: René Neumann <rene.neumann@in.tum.de>
Hi Andreas,
thanks for the explanation. I was using this kind of lifting already to
get code generation for locale interpretations work properly. But for
whatever reason I did not see that it is also applicable here. (And this
'lifting from locales' is also just renaming ...)
Last updated: Apr 20 2024 at 12:26 UTC