Email Gateway (Aug 19 2022 at 14:32): Email Gateway (Aug 19 2022 at 14:32):From: Häuselmann Rafael <rafaelh@student.ethz.ch>
Hi,
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?
Thanks in advance for any help,
Rafael
Email Gateway (Aug 19 2022 at 14:32):From: Makarius <makarius@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
Email Gateway (Aug 19 2022 at 14:32):From: Häuselmann Rafael <rafaelh@student.ethz.ch>
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
Email Gateway (Aug 19 2022 at 14:32):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 14:47):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Last updated: Apr 23 2024 at 20:15 UTC