Re: [isabelle] Renaming on code-export



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:

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

2. 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 at 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é







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