Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Function transformers not called on abstract c...

Email Gateway (Aug 22 2022 at 15:34):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear code generator experts,

Pascal, a student of mine, and I are experimenting with the function transformer interface
of the preprocessor for code equations in Isabelle2016-1. After having read the code
generator tutorial, we expected that a function transformer F registered with

Code.add_functrans ("name", F)

would be called with the set of code equations for every HOL function for which code must
be generated. However, we noticed that for constants that have an abstract code equation,
the function transformer is called with an empty list instead of the code equations.

setup ‹
Code_Preproc.add_functrans ("print", (fn _ => fn thms =>
(Output.writeln (@{make_string} thms); NONE)));
›
typedef n = "{x :: nat. x > 0}" by auto
setup_lifting type_definition_n
lift_definition suc :: "n ⇒ n" is Suc by simp
code_thms suc

Are we doing something wrong? Is there a way to have the function transformers called also
for constants with abstract code equations? Or is there a good reason why this is not done?

Thanks,
Andreas

Email Gateway (Aug 22 2022 at 15:34):

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

function transformers are indeed only applied to regular function
equations, and admittedly the documentation is not explicit about that.

The rationale behind this is historic and pragmatic: the typical
application of function transformers is to rewrite whole sets of
equations, particularly patterns on the LHS. For abstract equations,
there is only one equation and no pattern at all.

What application do you have in mind? Maybe there is a different
approach that would work for you.

Personally I would prefer anyway that the whole matter of preprocessing
would take place in situ when function equations are declared, but this
is not possible since function equations can only be treated grouped by
heading constants, and that is architecturally not compatible with Isar
declarations.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 22 2022 at 15:35):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Florian,

Thanks again for the quick reply. Changing the pattern-matching structure is also our
application. But we also have to transform the right-hand sides of code equations. We
might be able to get things done with [code_unfold] declarations, but we are not yet
absolutely sure. Ultimately, our goal is to implement a preprocessor for codatatypes such
that they are implemented lazily in the generated ML code. This means that we have to
replace case-expressions and constructors in the right-hand sides with their lazy
versions. Unfortunately, this may not always enough, e.g., in case the constructor or case
expression is not applied to sufficiently many arguments. So it might be the case that we
want to apply some selective eta expansion in some places.

But we'll try with [code_unfold] first.

Best,
Andreas

Email Gateway (Aug 22 2022 at 15:35):

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

But we'll try with [code_unfold] first.

the preprocessor allows to fully apply the expressive power of the
simplifier; hence sophisticated rewrite procedures can be implemented as
simprocs also.

Cheers,
Florian

Best,
Andreas

On 02/06/17 20:28, Florian Haftmann wrote:

Hi Andreas,

After having read the code generator tutorial, we
expected that a function transformer F registered with

Code.add_functrans ("name", F)

would be called with the set of code equations for every HOL function
for which code must be generated. However, we noticed that for constants
that have an abstract code equation, the function transformer is called
with an empty list instead of the code equations.

setup ‹
Code_Preproc.add_functrans ("print", (fn _ => fn thms =>
(Output.writeln (@{make_string} thms); NONE)));
›
typedef n = "{x :: nat. x > 0}" by auto
setup_lifting type_definition_n
lift_definition suc :: "n ⇒ n" is Suc by simp
code_thms suc

Are we doing something wrong? Is there a way to have the function
transformers called also for constants with abstract code equations? Or
is there a good reason why this is not done?

function transformers are indeed only applied to regular function
equations, and admittedly the documentation is not explicit about that.

The rationale behind this is historic and pragmatic: the typical
application of function transformers is to rewrite whole sets of
equations, particularly patterns on the LHS. For abstract equations,
there is only one equation and no pattern at all.

What application do you have in mind? Maybe there is a different
approach that would work for you.

Personally I would prefer anyway that the whole matter of preprocessing
would take place in situ when function equations are declared, but this
is not possible since function equations can only be treated grouped by
heading constants, and that is architecturally not compatible with Isar
declarations.

Hope this helps,
Florian

signature.asc

Email Gateway (Aug 22 2022 at 15:35):

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

That's an excellent idea. That should work in case we need eta expansion.

Thanks,
Andreas

Last updated: Apr 20 2024 at 12:26 UTC