Re: [isabelle] make_string





On 06/22/2018 11:46 PM, Makarius wrote:
On 21/06/18 16:05, Jeremy Dawson wrote:

Right at the moment, I'm working on using the content of a goal in an
Isabelle/ZF session to calculate, and print, a term which can be used as
a goal when read into an Isabelle/HOL session

If this is only for machine writable/readable data, you can use XML/YXML
encoding for actual term values, without getting notation and
type-inference in between. E.g. like this:

ML ‹
   val t = @{term ‹λx. x›};
   val path = Path.explode "/tmp/a";
   File.write path (YXML.string_of_body (Term_XML.Encode.term t));
   val t' = Term_XML.Decode.term (YXML.parse_body (File.read path));
   @{assert} (t = t');
›

Hi Makarius,

Well, as you suggest, this gives only machine writable/readable data; I want to get an ML value of type term (or, as in my case, a related datatype, or more generally any ML value), as a string, that is, an ML value of type string, which is readable, and could be used to construct a theory file, by reading it in by
 ML {* val t = ... *}
Just like PolyML.makestring, which I assume has been deliberately made unavailable (why is this?) And just like @{make_string} combined with |> YXML.parse_body |> XML.content_of seems to do, but you seem to be saying that I shouldn't use this for production-quality output (why is this the case?)

Regards,

Jeremy





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