Re: [isabelle] Code equations for "power"



Hi Manuel,

On 08/01/16 17:26, Manuel Eberl wrote:
The code_unfold works if the call to power in the code equations is types with something
of sort mult_monoid. So if the code equation uses power on one of the standard numeric
types, everything is fine. But if you use power polymorphically for some 'a, then this
does not work if mult_monoid is not a supersort of 'a's sort. For example, if you have
something like

I guess that's a pretty good compromise, isn't it? Most of the time, exported code using
the "power" operation will probably be dealing with types that fulfil at least
monoid_mult, and then this fast variant could be used.
I think that this can work for power, but it can also lead to surprises because the rewrite does not trigger always and users then have to understand the whole setup to find out. I had experimented with such rewrites for subset tests (end of theory Library/Cardinality), but this never worked as well as I had hoped, because the rewrite needed the sort card_UNIV, which was hardly present in any code equation.

Renà Thiemann and Christian Sternagel faced the same problem for linorders and comparators. They have implemented a custom function in ML that transforms the code equations, but users have to call this manually (see their ITP2015 paper). This approach is less convenient, but more robust.

Best,
Andreas




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