[isabelle-dev] Method parsing, YXML and term construction.
Thomas.Sewell at nicta.com.au
Tue Feb 9 01:50:12 CET 2010
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?
> On Mon, 8 Feb 2010, Thomas Sewell wrote:
>> 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.
> Pasting strings together for consumption by the inner syntax engine was
> never robust, and should never be done in production code. (Likewise is
> it a very bad idea to split output by the pretty printing engine, e.g. the
> result of Syntax.string_of_term.)
> In Isabelle2008 we have introduced a clear separation of the raw parsing
> and type-checking phases. The Syntax.parse_term function is your friend
> -- it will parse legal term fragments to produce a certain "preterm"
> format that can be composed with other preterms and then given to
> Syntax.check_term (or Syntax.check_terms for several simulataneous
>> 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).
> When introducing the YXML markup around outer syntax tokens that become
> types/terms later, I was fully aware that any code that manipulates inner
> syntax source will break. This should be taken as an opportunity to
> remove these things from your code.
More information about the isabelle-dev