[isabelle-dev] Method parsing, YXML and term construction.
makarius at sketis.net
Tue Feb 9 11:56:43 CET 2010
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
More information about the isabelle-dev