[isabelle-dev] Method parsing, YXML and term construction.

[Thomas Sewell]

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 
term-manipulation level?

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 
each other?

Yours,
    Thomas.