Email Gateway (Aug 22 2022 at 20:35): Email Gateway (Aug 22 2022 at 20:35):From: Moa Johansson <moa.johansson@chalmers.se>
Hi all,
Just updating some of my code to use Isabelle2019. Noticing the interface to the code generation has changed. I managed to get my code to type-check and work, through some qualified guessing, but it would be nice to understand what I was actually doing… ☺.
In Isabelle2019 the function export_code has the following type:
val export_code:
bool -> string list
-> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list
-> local_theory -> local_theory
More specifically, what does the new arguments
{physical: bool} and
Position.T
actually mean? Setting them to “true” and “Position.start” respectively worked fine in my case, when exporting to Haskell.
Also, I am somewhat wondering about to the remark in the Changelog about the “file” argument becoming legacy and being removed. This refers to the export_code command on the Isar-level, but does it affect me when working at the ML level (i.e. what I put in the argument of type Path.T above)?
Best,
Moa
Email Gateway (Aug 22 2022 at 20:35):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Moa,
these changes in the Isabelle/ML interface correspond to the following
NEWS entry:
- Command 'export_code' produces output as logical files within the
theory context, as well as formal session exports that can be
materialized via command-line tools "isabelle export" or "isabelle build
-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
provides a virtual file-system "isabelle-export:" that can be explored
in the regular file-browser. A 'file_prefix' argument allows to specify
an explicit name prefix for the target file (SML, OCaml, Scala) or
directory (Haskell); the default is "export" with a consecutive number
within each theory.
More specifically, what does the new arguments
{physical: bool} and
Position.T
actually mean? Setting them to “true” and “Position.start” respectively worked fine in my case, when exporting to Haskell.
Most idiomatic is to use the \<^here> antiquotation in Isabelle/ML for a
position, if there is no position you can just pass through from
corresponding Isar text.
Also, I am somewhat wondering about to the remark in the Changelog about the “file” argument becoming legacy and being removed. This refers to the export_code command on the Isar-level, but does it affect me when working at the ML level (i.e. what I put in the argument of type Path.T above)?
The possibility to generate files from the exported code
programmatically will always remain (cf. module »Export«).
The idea behind the NEWS entry is to reduce / eliminate the need for
arbitrary dumps to the physical file system over time.
Cheers,
Florian
signature.asc
Last updated: Apr 19 2024 at 04:17 UTC