[isabelle-dev] copy_bnf

[Dmitriy Traytel]

Hi Lars,

this was exactly the vision for copy_bnf, modulo that I thought of using a plugin (“src/Pure/Tools/plugin.ML”) instead of an option. But since I am not the author of record, I went for the less invasive option of a separate command (in the spirit of setup_lifting for typedef). So if the authors of record agree, I can add the plugin.

I guess the general question is, whether it is fine to add the plugin infrastructure for (most of the) existing commands (e.g., definition, typedef, record, fun), thus enabling us writing tools that extend the command’s functionality (be them enabled by default or not).

Dmitriy


> On 29 Oct 2015, at 13:41, Lars Hupel <hupel at in.tum.de> wrote:
> 
> Dear Dmitriy,
> 
> I like the new "copy_bnf" command a lot, especially to allow records to
> be used in nested recursion. However, after a record definition, I have
> to invoke the command manually*. I would like to propose that "record"
> gains an option to call it directly. So, instead of writing:
> 
>  record 'a foo = bla :: 'a
> 
>  copy_bnf ('a, 'b) foo_ext
> 
> ... I could write
> 
>  record (copy_bnf) 'a foo = bla :: 'a
> 
> Depending on the efficiency of the internal constructions "copy_bnf"
> could also be the default.
> 
> I do have a use case for this: Lem** is able to generate Isar sources
> containing records, and in CakeML, these records are then used for
> nested recursion. Lem could be changed to emit an additional "copy_bnf",
> but that would make it dependent on the internal construction ("_ext").
> Hence, I would much prefer a flag or to run it by default.
> 
> Cheers
> Lars
> 
> 
> * and to remember that I need to use "foo_ext" because otherwise I get
> an ML exception
> 
> ** <https://bitbucket.org/Peter_Sewell/lem/>