Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Date: Mon, 13 Jun 94 16:51:15 EDT
From: reetz <reetz@ira.uka.de>
To: hol2000@leopard.cs.byu.edu
Subject: Improved error messages
Message-Id: <"i80fs2.ira.801:13.05.94.14.51.22"@ira.uka.de>

One might consider improved error messages.
Take e.g. mk_cond. It fails with


Exception raised at Dsyntax.mk_cond:

val it = () : unit

That's it. 

[Frankly, this has already caused me
searching and searching around a lot :-( You
might argue, that if such a ``basic'' error
occurs within your own code, your own code
needs more error checking. However, if you
are still developing your own code, these
``basic'' errors are pretty much normal.]

But there are different reasons for failure,
e.g. #cond might not be of type boolean,
#larm and #rarm might not have the same types.
HOL_ERR might report that.
It would be helpful if HOL_ERR would output 
the terms causing the failure, too. Otherwise,
beside #origin_function and #origin_structure in HOL_ERR,
it might still be hard to localize the error,
because the same routine raising this particular
HOL_ERR might be called a dozens of time and
fail only on one of these cases.
Ideally, the user would see e.g. his terms #cond,
#larm and #rarm and the fitting error message and
- jop! - see the error immediately.
Sometimes, the error message might even give a
hint what to correct...