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



Thanks to everybody who contributed to this thread.

Here is a summary of important points that are relevant for the next
round of renovation of the Isabelle/HOL record package.

* Scalability and extensibility are both used in applications and very
relevant. 100-1000 record fields and max. 5 record extensions occur
routinely -- e.g. in the seL4 project by Data61 (usually generated from
programs / specifications).

* Some connection of records with datatypes is occasionally useful, e.g.
for recursion through record types or convenient notation for datatype
constructors (with updates), but it works against scalability demands
for records, because datatypes are very heavy.

Some partial solutions (for small records) are:

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


http://isabelle.in.tum.de/repos/isabelle/file/3107dcea3493/src/HOL/Library/Datatype_Records.thy

* Instead of providing a separate datatype_record or record_datatype
package, it might be better to have a plugin for the existing BNF
datatype package to provide certain notational conveniences of records.

* There are existing techniques to connect records and datatypes
manually, e.g. with 'copy_bnf'.

* The record package is still awaiting localization, in order to make it
work in local contexts (locale, class, context, experiment etc.). Some
key challenges:

  - The package is very large and complex, with many cumulative
additions over time, by several authors.

  - Record syntax needs to be somehow localized; conceptually it should
work, because the syntax is "constant", only the record field names,
types, and extensions depend on the context.

* Update syntax is actually generic, there is no direct connection to
records.

* There are some open questions concerning code-generation for records.

* Instead of using records (with predicates over them) it is often more
convenient to use locales (with individual parameters and assumptions)
and let the locale + interpretation infrastructure handle merges,
instantiation etc.

* The Isabelle mailing lists have accumulated various non-conclusive
threads about records vs. datatypes over the past few years, e.g. see
here
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-August/msg00016.html


	Makarius




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