[isabelle-dev] Method parsing, YXML and term construction.
Thomas.Sewell at nicta.com.au
Mon Feb 8 04:29:34 CET 2010
Hello to isabelle-dev.
Suppose some ML code I wrote has terms f, x and y. I'd like to be able
to produce the function application "f x y" with the catch that f, x and
y may all have type parameters that need to be adapted to each other. Is
there any convenient facility for doing this in Isabelle at the
Specifically, f is a polymorphic constant, x is a simple function
application generated by our ML code, and y is supplied by the user and
must be parsed. So far, our code has simply generated the string
expression "f (x) (y)" and passed it to Syntax.read_term. Using the
parser to get around type problems seems the ugly way through, however.
In upgrading to Isabelle-2009 everything got broken, because the input
for y may be wrapped in YXML code to annotate it with position
information, which results in "f (x) (y)" causing a malformed YXML error
(it's a forest, not a tree). Helpfully, isabelle strips the YXML
annotations from the error message as it is printed, making it difficult
to establish what the cause of the error is.
The simple workaround which I've implemented is to purge the YXML from y
by passing it to YXML.parse and then flattening the XML tree down to
only its Text elements. This gets the job done, but it seems like a good
idea to look for an alternative approach. Assuming I instead construct f
and x as terms in ML, and pass y to Syntax.read_term as intended, is
there a helper API for specialising the resulting types so they apply to
More information about the isabelle-dev