Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sequential Functions and Code Equations

Email Gateway (Aug 19 2022 at 07:51):

From: Patrick Michel <uni@pbmichel.de>
Hi!

I am currently using the code generation facility (Haskell backend) and can't seem to figure out how to get rid of redundant code equations.
Function definitions with deep patterns and/or patterns on multiple arguments are currently unfolded to an abysmal amount of redundant equations.

I understand why Isabelle is doing this; all these specialized equations can be directly used for reasoning, as they do not need any guards.
It's a price I can pay for using sequential mode while reasoning about functions in Isabelle.

In the target language, however, the semantics is also sequential, i.e. the original equation given in the function definition would have the correct semantics.
I have read through the refinement section of the code generation documentation, but it doesn't seem to talk about these situations.

Thanks,

Patrick Michel
Software Technology Group
University of Kaiserslautern

Email Gateway (Aug 19 2022 at 08:03):

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

the code generator does not attempt to minimize patterns, for two reasons:

a) This would be an extra-logical optimisation.
b) The task is far from being trivial.

CU,
Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC