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

[Thomas Sewell]

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?

Yours,
     Thomas.

Makarius wrote:
> 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 
> operands).
>
>
>   
>> 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.
>
>
>  	Makarius
>