Re: [isabelle] Code generation & type classes - inefficient code



Hi Dominique,

Am 21.05.19 um 12:08 schrieb Dominique Unruh:
> Generation of ML code from Isabelle mimics type classes by passing
> around explicit records containing the functions specific to the type
> class.
> 
> This works well, however, I noticed that the resulting code can be very
> inefficient because the same records are constructed over and over.

[...]

> My questions:
> 
>  * Is there a way to tell the code generator to do things more
>    efficiently? (E.g., the way I described.)

one approach is to provide explicit local definitions in code equations,
e. g.

lemma [code]:
  ‹f x = let e = (enum :: …) in …›

Another possibility is to provide monomorphic abbreviations, e. g.

definition min_int :: ‹int => int => int›
  [code_abbrev]: "min_int = min"

lemma [code]:
  "min_int k l = …"

Or a combination of both.  It depends on the context what is actually
applicable.

>  * Perhaps future versions of the code generator could do this? (I
>    don't know if the code generator is still being developed.)

Ocassionally there are still things happening.  But not with a big
agenda in mind.

Hope this helps,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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