Re: [isabelle] export .thy files as xml



On Fri, 24 Oct 2008, Christian Maeder wrote:

> 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.

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.


	Makarius
theory A
imports Main
begin

definition foo where "foo x = x"

lemma a: "foo (foo x) = x" unfolding foo_def ..
 
end
<command_span line="1" column="1" offset="1" end_line="3" end_column="6" end_offset="28" file="/home/makarius/tmp/A.thy" name="theory"></command_span>
<ignored_span line="3" column="6" offset="28" end_line="5" end_column="1" end_offset="30" file="/home/makarius/tmp/A.thy"></ignored_span>
<command_span line="5" column="1" offset="30" end_line="5" end_column="33" end_offset="62" file="/home/makarius/tmp/A.thy" name="definition"></command_span>
<ignored_span line="5" column="33" offset="62" end_line="7" end_column="1" end_offset="64" file="/home/makarius/tmp/A.thy"></ignored_span>
<command_span line="7" column="1" offset="64" end_line="7" end_column="27" end_offset="90" file="/home/makarius/tmp/A.thy" name="lemma"></command_span>
<ignored_span line="7" column="27" offset="90" end_line="7" end_column="28" end_offset="91" file="/home/makarius/tmp/A.thy"></ignored_span>
<command_span line="7" column="28" offset="91" end_line="7" end_column="45" end_offset="108" file="/home/makarius/tmp/A.thy" name="unfolding"></command_span>
<ignored_span line="7" column="45" offset="108" end_line="7" end_column="46" end_offset="109" file="/home/makarius/tmp/A.thy"></ignored_span>
<command_span line="7" column="46" offset="109" end_line="7" end_column="48" end_offset="111" file="/home/makarius/tmp/A.thy" name=".."></command_span>
<ignored_span line="7" column="48" offset="111" end_line="9" end_column="1" end_offset="114" file="/home/makarius/tmp/A.thy"></ignored_span>
<command_span line="9" column="1" offset="114" end_line="9" end_column="4" end_offset="117" file="/home/makarius/tmp/A.thy" name="end"></command_span>
<ignored_span line="9" column="4" offset="117" end_line="10" end_column="1" end_offset="118" file="/home/makarius/tmp/A.thy"></ignored_span>
<command line="1" column="1" offset="1" end_line="1" end_column="7" end_offset="7" file="/home/makarius/tmp/A.thy"></command>
<ident line="1" column="8" offset="8" end_line="1" end_column="9" end_offset="9" file="/home/makarius/tmp/A.thy"></ident>
<keyword line="2" column="1" offset="10" end_line="2" end_column="8" end_offset="17" file="/home/makarius/tmp/A.thy"></keyword>
<ident line="2" column="9" offset="18" end_line="2" end_column="13" end_offset="22" file="/home/makarius/tmp/A.thy"></ident>
<keyword line="3" column="1" offset="23" end_line="3" end_column="6" end_offset="28" file="/home/makarius/tmp/A.thy"></keyword>
<command line="5" column="1" offset="30" end_line="5" end_column="11" end_offset="40" file="/home/makarius/tmp/A.thy"></command>
<ident line="5" column="12" offset="41" end_line="5" end_column="15" end_offset="44" file="/home/makarius/tmp/A.thy"></ident>
<keyword line="5" column="16" offset="45" end_line="5" end_column="21" end_offset="50" file="/home/makarius/tmp/A.thy"></keyword>
<string line="5" column="22" offset="51" end_line="5" end_column="33" end_offset="62" file="/home/makarius/tmp/A.thy"></string>
<command line="7" column="1" offset="64" end_line="7" end_column="6" end_offset="69" file="/home/makarius/tmp/A.thy"></command>
<ident line="7" column="7" offset="70" end_line="7" end_column="8" end_offset="71" file="/home/makarius/tmp/A.thy"></ident>
<keyword line="7" column="8" offset="71" end_line="7" end_column="9" end_offset="72" file="/home/makarius/tmp/A.thy"></keyword>
<string line="7" column="10" offset="73" end_line="7" end_column="27" end_offset="90" file="/home/makarius/tmp/A.thy"></string>
<command line="7" column="28" offset="91" end_line="7" end_column="37" end_offset="100" file="/home/makarius/tmp/A.thy"></command>
<ident line="7" column="38" offset="101" end_line="7" end_column="45" end_offset="108" file="/home/makarius/tmp/A.thy"></ident>
<command line="7" column="46" offset="109" end_line="7" end_column="48" end_offset="111" file="/home/makarius/tmp/A.thy"></command>
<command line="9" column="1" offset="114" end_line="9" end_column="4" end_offset="117" file="/home/makarius/tmp/A.thy"></command>
<fixed_decl line="5" column="12" offset="41" end_line="5" end_column="15" end_offset="44" file="/home/makarius/tmp/A.thy" name="foo"></fixed_decl>
<prop line="5" column="22" offset="51" end_line="5" end_column="33" end_offset="62" file="/home/makarius/tmp/A.thy"></prop>
<ident line="5" column="23" offset="52" end_line="5" end_column="26" end_offset="55" file="/home/makarius/tmp/A.thy"></ident>
<ident line="5" column="27" offset="56" end_line="5" end_column="28" end_offset="57" file="/home/makarius/tmp/A.thy"></ident>
<literal line="5" column="29" offset="58" end_line="5" end_column="30" end_offset="59" file="/home/makarius/tmp/A.thy"></literal>
<ident line="5" column="31" offset="60" end_line="5" end_column="32" end_offset="61" file="/home/makarius/tmp/A.thy"></ident>
<const_decl line="5" column="12" offset="41" end_line="5" end_column="15" end_offset="44" file="/home/makarius/tmp/A.thy" name="A.foo"></const_decl>
<fixed_decl line="5" column="12" offset="41" end_line="5" end_column="15" end_offset="44" file="/home/makarius/tmp/A.thy" name="foo"></fixed_decl>
<prop line="7" column="10" offset="73" end_line="7" end_column="27" end_offset="90" file="/home/makarius/tmp/A.thy"></prop>
<ident line="7" column="11" offset="74" end_line="7" end_column="14" end_offset="77" file="/home/makarius/tmp/A.thy"></ident>
<literal line="7" column="15" offset="78" end_line="7" end_column="16" end_offset="79" file="/home/makarius/tmp/A.thy"></literal>
<ident line="7" column="16" offset="79" end_line="7" end_column="19" end_offset="82" file="/home/makarius/tmp/A.thy"></ident>
<ident line="7" column="20" offset="83" end_line="7" end_column="21" end_offset="84" file="/home/makarius/tmp/A.thy"></ident>
<literal line="7" column="21" offset="84" end_line="7" end_column="22" end_offset="85" file="/home/makarius/tmp/A.thy"></literal>
<literal line="7" column="23" offset="86" end_line="7" end_column="24" end_offset="87" file="/home/makarius/tmp/A.thy"></literal>
<ident line="7" column="25" offset="88" end_line="7" end_column="26" end_offset="89" file="/home/makarius/tmp/A.thy"></ident>
<fact line="7" column="38" offset="101" end_line="7" end_column="45" end_offset="108" file="/home/makarius/tmp/A.thy" name="A.foo_def"></fact>
<fact_decl line="7" column="7" offset="70" end_line="7" end_column="8" end_offset="71" file="/home/makarius/tmp/A.thy" name="A.a"></fact_decl>
<local_fact_decl line="7" column="7" offset="70" end_line="7" end_column="8" end_offset="71" file="/home/makarius/tmp/A.thy" name="local.a"></local_fact_decl>


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.