[isabelle-dev] Method parsing, YXML and term construction.
makarius at sketis.net
Mon Feb 8 14:42:18 CET 2010
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