Re: [isabelle] size for records



Hi Lars,

> On 11 Aug 2017, at 14:15, Lars Hupel <hupel at in.tum.de> wrote:
> 
>> To quote from the docs: "For each datatype t, the size plugin generates a generic size function t.size_t as well as a specific instance size :: t â nat belonging to the size type class."
>> 
>> The key word is "datatype". In general, a BNF is not a datatype.
> 
> yeah, right. I guess the general problem is that records are
> insufficiently like datatypes. But rebasing their construction on top of
> new datatypes would be a significant effort.

not only that: the record construction is much more efficient than the datatype one. So, basing record on datatype would make the seL4 people with their huge records quite unhappy.

>> I would presume that this should be an easy task for the Lifting package. Otherwise, you should be able to define the size function manually without too much effort.
> 
> Sure, and I just went down that route (manually). But I thought I might
> ask if someone has done anything similar :-)

Ideally, there should be a plugin infrastructure and a size plugin for records. (Oh, and record should be localized. :) ) But since the workaround of a manual definition is so easy, it is hard to find a volunteer to do this.

Dmitriy







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