Re: [isabelle] Parsing a string to a term



On Wed, 21 May 2014, Häuselmann  Rafael wrote:

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.

So what is the purpose of SML/NJ here? It is very slow compared to Poly/ML that underlies Isabelle/ML by default. If you stay within Isabelle/ML the import/export problem goes away, too.


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.

You can invoke the ML compiler and runtime via operations like ML_Context.eval, but I doubt that you really want to do this here. Exchanging data in the notation of the source language is a bit odd for anything other than LISP.

The YXML/XML/ML modules actually imitate the old LISP read/write mode, while avoiding the inclusion of the interpreter/compiler in the pipeline.


	Makarius


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