Re: [isabelle] Parsing a string to a term



Am 21.05.2014 um 13:44 schrieb Makarius <makarius at sketis.net>:

> 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 https://bitbucket.org/makarius/yxml 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.
> 
> 
> 	Makarius

Yeah, my function produces the string itself by exporting a term from Isabelle and evaluating that term in SML/NJ, wich then produces the string I was talking about, and then I want to interprete this string as the term it represents.
I will have a look at your suggestion and see if it helps me, but basically I was searching for a way to invoke the compiler at runtime for this string.

thanks
Rafael



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