Email Gateway (Aug 22 2022 at 15:50): Email Gateway (Aug 22 2022 at 15:50):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I'm having a lot of troubles with records right now. They're not BNFs,
but luckily there's the "copy_bnf" command. Unfortunately, it seems this
doesn't generate a size function (at least I don't see it). Is it
possible to transfer the size function from the original BNF? Because
without size function, nested recursion through the record becomes tricky.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:51):From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,
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.
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 :-)
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:51):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Lars,
On 11 Aug 2017, at 14:15, Lars Hupel <hupel@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
Email Gateway (Aug 22 2022 at 15:51):From: Lars Hupel <hupel@in.tum.de>
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'm aware of that, but didn't know that the difference is that large.
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.
A good starting point could be to decouple record syntax from record
definitions. There's no reason why
datatype foo = Bar (x: nat) (y: nat)
couldn't be treated as a record, including update functions. I'm already
working on a plugin that produces "*_update" functions (this allows for
record update syntax, albeit not construction syntax). The next step
would be to patch Lem to use this instead of records.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC