Re: [isabelle-dev] Explicit option "open" for code_reflect
Hi Frédéric, > For a few number of constants it should be possible to write all > constants by hand. For a large number, I will see how feasible it is to > generate this list of constants, or find otherwise a simpler solution... code_reflect is definitely not intended as a watering bin. The typical use case is import one algorithm from HOL into the ML context, with a well-defined and minimal interface (typically, input and output types plus one or two actual calculations). Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Explicit option "open" for code_reflect
Hi Florian, For a few number of constants it should be possible to write all constants by hand. For a large number, I will see how feasible it is to generate this list of constants, or find otherwise a simpler solution... Cheers, Frédéric ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Explicit option "open" for code_reflect
Hi Fréderic, > Between Isabelle 2014 and 2015, the option "open" appeared for the > command export_code, and by default the reflection minimizes the > exported code. > Would it be acceptable for code_reflect to also have a similar option > "open"? what is your use case? If you want to export an operation in the generated code, just add it to the list of constants. It is the very purpose of code_reflect to provide a well-defined interface. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Explicit option "open" for code_reflect
Hi Florian, Between Isabelle 2014 and 2015, the option "open" appeared for the command export_code, and by default the reflection minimizes the exported code. Would it be acceptable for code_reflect to also have a similar option "open"? As a draft example, here is a list of modifications needed for implementing the option "open": afp-devel/thys/Isabelle_Meta_Model/isabelle_home/src/Tools/Code/Isabelle_code_runtime.thy We basically abstract the parameter "false" of Code_Target.produce_code, and propagate this information to the parsing step. Cheers, Frédéric ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
