Re: [isabelle] export and import term



On Wed, 15 May 2013, Yuhui Lin wrote:

I've got a an exception "exception XML_ATOM term raised" when I use Syntax.parse_term to parse a string which is exported by Syntax.string_of_term, e.g.

Syntax.string_of_term @{context} @{term" a + b"} |> Syntax.parse_term @{context};

Conceptually, functions like Syntax.string_of_term from Isabelle inner syntax produce a pretty tree with additional markup. Its main purpose is to be output via one of the standard Isabelle channels (writeln, warning etc.), e.g. like this:

ML {*
  val s = Syntax.string_of_term @{context} @{term" a + b"};
  writeln s;
*}

The front-end on the Isabelle/Scala side then renders the pretty tree as best as it can -- Isabelle/jEdit presently uses a lot of this information for hilighting, hyperlinks, tooltips etc.

You can peek at that raw XML tree representation in Isabelle/ML using YXML.parse_body on the string s above. This is mainly for information, normally you don't work with these internal representations directly.


There are some tricks to avoid producing extra markup, and get back to nostalgic raw text output, but one should try first to stay within the regular mode of operation. Note that Syntax.parse_term cannot recover exactly the same term in general, even when printed without YXML markup.


The reason for me to do this is that the system, which I am developing, need to communicate with Isabelle. So I want to export and import terms in Isabelle as string to my system in the json format in ML. But I get the above exception.

There are various ways to do that, depending what you actually need.


For example, you can use encode/decode functions from the XML and Term_XML module (both in Isabelle/ML and Isabelle/Scala) to get structured values back and forth, without concrete syntax getting in between.

The Isabelle term parser also accepts low-level YXML terms directly like this:

ML {*
  val t = @{term "a + b"};
  val yxml = YXML.string_of_body (Term_XML.Encode.term t);

  writeln (YXML.embed_controls yxml);
*}

Now the Output panel in Isabelle/jEdit shows some funny string with bold X and Y characters. This is you externalized term, it can be sent around between process, over the Net etc.

It can be re-internalized in Isabelle/Isar, e.g. like this:

  term "XY5XXY:..."


The same in Isabelle/ML:

ML {*
  val t' = Term_XML.Decode.term (YXML.parse_body yxml);
  @{assert} (t = t');
*}


Thus you can bypass traditional troubles with official "XML", even json.

Note that Isabelle/Scala hardly provides any operations on logical Term language.


	Makarius




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