[isabelle] Sequential Functions and Code Equations



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






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