Re: [isabelle] Parsing a string to a term
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and