Re: [isabelle] Parsing a string to a term
On 21/05/14 18:43, Makarius wrote:
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
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
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.
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.
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