Re: [isabelle] Sequential Functions and Code Equations



Hi Patrick,

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

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



Attachment: signature.asc
Description: OpenPGP digital signature



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