Re: [isabelle] Proof of concept: BNF-based records




On 16 Feb 2018, at 07:56, Makarius <makarius at sketis.net<mailto:makarius at sketis.net>> wrote:

On 14/02/18 22:12, Gerwin.Klein at data61.csiro.au<mailto:Gerwin.Klein at data61.csiro.au> wrote:


I must admit that we have been maintaining a similar (very bare-bones) additional datatype record package on the side for about a decade. We use it in addition to the standard record package to model C structs, because they can contain recursive pointer types, which we couldn’t do with normal records. I.e. it might make sense to have both, as long as it is clear what each is for, what the differences are, and why they can’t/shouldn’t be the same.

Can you point to the sources of this alternative datatype record
package? How does it treat record syntax?

https://github.com/seL4/l4v/tree/master/tools/c-parser/recursive_records

The syntax is a very ad-hoc partial reuse of the standard record translations. Definitely not thought as an example to be followed.

Cheers,
Gerwin


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