Email Gateway (Aug 18 2022 at 12:33): Email Gateway (Aug 18 2022 at 12:33):From: Christian Maeder <Christian.Maeder@dfki.de>
Hi,
is there a way to export a parsed, type-checked and possibly proven
theory file as an xml file (or another format.)
I've found the yxml (xml to yxml converter) in the documentation, but no
way to create xml in the first place.
Thanks Christian
Email Gateway (Aug 18 2022 at 12:34):From: Makarius <makarius@sketis.net>
XML is merely a complex way to represent simple trees, while YXML is a
much simpler version that also achieves better performance (about an order
of magnitude compared to the best XML parser).
Being able to import and export simple trees efficiently does not give
access to internal Isabelle theory content yet. In fact it is impossible
to externalize the actual theory, because it may contain arbitary abstract
data defined by the user somewhere.
What you can do is to turn some aspects of the theory content into an
external format and try to make sense out of it. For example the tables
of types, consts, theorems etc. similar to the output of print_theory.
See also src/Pure/Tools/xml_syntax.ML for an example of how some concrete
ML datatypes of Isabelle can be represented as XML trees.
Instead of peeking at low-level details of internal theory values there is
another way of getting information about how the system interprets the
original sources. This is an emerging concept only present in recent
development versions: the system issues detailed status messages for the
bits and pieces of text it has encountered and parsed in a certain way
(information about type-checking will follow later).
You can try this with Proof General with option -m test_markup enabled.
See the attached theory and log of status messages produced as a side
effect of loading it.
At the moment this is merely a trace of some aspects of the internal
processing of theory sources. Later we will use it more systematically
for the next generation of Isabelle user interfaces and document
preparation systems, with "semantic" information attached to the sources.
Last updated: Nov 21 2024 at 12:39 UTC