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 <hu...@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/>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
