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



On 15/02/18 00:46, Gerwin.Klein at data61.csiro.au wrote:
> 
>> Can you point to the sources of a few such big record definitions?
> 
> They get produced by the C parser, e.g. at this call:
> 
> https://github.com/seL4/l4v/blob/3d225cde694ba60a/spec/cspec/X64/Kernel_C.thy#L78
> 
> The record becomes large, because Norbert's SIMPL framework expects one record field per local variable in the union of all functions of the program. The final state record is an extension of a default state record + these local variables.
> 

I now recall that Norbert Schirmer made the first major scalability
changes for the record package.

Earlier it was actually based on datatypes, since I did not want to
fiddle with typedefs manually, but that was very slow (as expected).


> We could synthesise a manual definition that simulates this situation if it helps.

For the moment it is sufficient to get an idea about:

  (1) typical number of record fields
  (2) typical number of record extensions (i.e. the depth of the hierarchy)


	Makarius




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