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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and