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.