Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: Rob Arthan <rda@win.icl.co.uk>
Date: Tue, 7 Nov 95 09:34:56 GMT
Message-Id: <9511070934.9340.0@win.icl.co.uk>
To: info-hol@leopard.cs.byu.edu, reetz@ira.uka.de
Subject: Re:  better error messages in hol90?

Ralf Reetz would like to see more informative error messages:

> ...  I found it very useful to write error messages,
> which included the term like
> 
> raise HOL_ERROR
> {origin_structure = "bla",
>  origin_function  = "f",
>  message          =
>  "f fails because subterm "^(term_to_string t)^" is blablabla"};

When designing ProofPower, we found that so many of the proof
procedures one wants work by repetition until failure or failure-driven
case selection that using the above approach throughout the system has
a bad effect on performance (because the pretty printer is being
invoked many times to format messages which are never actually seen).
Unfortunately, it is good for usability to make all error messages as
helpful as you can. The ProofPower solution is to defer evaluation of
the slow part, as if HOL_ERROR were defined so you can write:

raise HOL_ERROR
{origin_structure = "bla",
 origin_function  = "f",
 message          = (fn () =>
 "f fails because subterm "^(term_to_string t)^" is blablabla")};

Of course, you then need to arrange things so that if the exception
ever does get to the top level, the user can see the message.
This is fairly easy if you are able to adjust the ML pretty-printer
to print the operand of HOL_ERROR in a custom format.

Rob Arthan.