Re: [isabelle] Parsing a string to a term

On Tue, 20 May 2014, Häuselmann  Rafael wrote:

I have a function that returns (from the bash-output) a string containing the Isabelle representation of a term. Now I'm trying to find a way to transform such a string into the actual term. I have for example the string "Const (\"Num.num.One\", Type (\"Num.num\", []))", how do I get from this string to the according term? There must be an already existing parser functionality for this, right?

"The Isabelle representation of a term" is a certain ML datatype, but that does not have a canonical string representation a priori. The above is what the ML compiler would use for it, but parsing that within the running program would mean to invoke the compiler at runtime (which is possible, but a bit indirect) or imitate the parser of ML.

From where is the bash output coming and where is it going? If you
produce the output yourself, you could do that more directly, e.g. by emitting an XML or YXML encoding of the format defined in $ISABELLE_HOME/src/Pure/term_xml.ML

See also to get some idea how this works, independently of the huge Isabelle code base.

The Isabelle inner syntax parser, i.e. what you write in source text as lemma "prop" also happens to understand YXML directly, which is occasionally useful for program-generated sources that are not shown to the user.


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