[isabelle-dev] Method parsing, YXML and term construction.
On Tue, 9 Feb 2010, Thomas Sewell wrote: Thanks Makarius, Syntax.parse_term and Syntax.check_term do indeed seem to be my friends. In fact, I sort of wish I'd known about them earlier. I remember in one of the record package proofs it was annoying me that I had to construct the types explicitly when it felt like I should be able to construct the term skeleton and appeal to the type resolver. Now I know how. BTW, should I have known this already? Is there some part of the documentation that I should have read, but have overlooked? I've checked again: you would have had to be a very keen reader of NEWS, where it says for Isabelle2007 (not Isabelle2008 as I claimed): * Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.) and type checking (Syntax.check_term etc.), with common combinations (Syntax.read_term etc.). These supersede former Sign.read_term etc. which are considered legacy and await removal. * Pure/Syntax: generic interfaces for type unchecking (Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.), with common combinations (Syntax.pretty_term, Syntax.string_of_term etc.). Former Sign.pretty_term, Sign.string_of_term etc. are still available for convenience, but refer to the very same operations using a mere theory instead of a full context. The corresponding section in the Isar Implementation manual is this a dummy -- I've been close to touching it during my vacation last week. These issues of parse/check and uncheck/unparse were once very hot in the discussion -- a discussion that was somehow too much localized, though. Both those asking questions and those giving answers should develop a habit of making this a bit more public, i.e. on the isabelle-dev mailing list. Makarius
[isabelle-dev] Method parsing, YXML and term construction.
Hi Thomas, Isabelle internalizes expressions in two steps: (1) parse :: raw string (type string) - raw term (type term) (2) check :: raw term (type term) - internalized term with types inferred etc. (type term) It seems to me that most things you want to do can be done using (2) only: a) read your y using Syntax.read_term b) assemble your f and x using datatype term, placing type inference parameters wherever suitable using Type_Infer.param c) put the term together d) check it using Syntax.check_term. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de -- next part -- A non-text attachment was scrubbed... Name: signature.asc Type: application/pgp-signature Size: 260 bytes Desc: OpenPGP digital signature URL: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20100208/118a11b1/attachment.pgp
[isabelle-dev] Method parsing, YXML and term construction.
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.
