Re: [isabelle] lexical matters



on 17/1/11 11:34 PM, Michael Norrish <Michael.Norrish at nicta.com.au> wrote:

> On 18/01/11 09:34, mark at proof-technologies.com wrote:
>> It puzzles me how little has been done about these things until now.  Are
>> not people concerned that what is being displayed could be misleading?
>
> No.
>
> If one has reason to suspect that something funny might be going on, the
> terms in question can be examined using the primitive ML API.

This relies on having a sharp-sighted user who can spot subtle strange
behaviour (in addition to all the other demands on the attention of the poor
theorem prover user).  And in any case, it will sometimes not be possible to
spot that something funny has happened, because it may appear to be behaving
precisely as expected (even though it actually isn't).  Isn't it better to
have tools that we can solidly rely on?

But yes, I suppose terms can be examined in terms of their primitive syntax,
but surely this is completely impractical for large industrial formal
methods projects involving large formal specifications.  In practice, anyone
reviewing a large industrial proof will be using the normal pretty printer.
That is, if anyone is actually bothering to do a reviewing exercise in the
first place...

> Alternatively, one can print the term out using a primitive pretty-printer
> that doesn't attempt to do anything "fancy".
>
> For example, in HOL4 one can use
>
> Parse.print_term_by_grammar min_grammars

I don't think this particular command solves the irregular names problem, or
the overloaded variables problem.  But I suppose if used in conjunction with
HOL4's optional type annotated output and the new facility for coloured
printing of variables then it could help.

Mark.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.