Re: [isabelle] Parsing a string to a term



Hi Makarius,

On 21/05/14 18:43, Makarius wrote:
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.
We want to run test cases for the code generator in different implementations of the target languages. That is, for SML, we are working on test drivers for SML/NJ, PolyML and mlton.

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.
We have now mimicked a stripped-down version of these modules in Isabelle/HOL's term language that suffices to convert Typerep.typerep and Code_Evaluation.term into YXML such that Isabelle's decode function can reconstruct the terms again. That is indeed easier than invoking the ML compiler.

Andreas




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