Maybe HOL_ERR should have lazy strings, (unit -> string) list

[talsewell]

Something I thought of a while ago.

HOL4 error messages tend to be very terse, for instance, if MATCH_MP fails, you might get an error message like "different constructors" with no further details. The Isabelle equivalent would be a TERM exception with the un-matcheable terms attached (TERM has type (string * term list -> exn)). To add that info in HOL4's HOL_ERR, however, the terms would have to be formatted into strings, which is an upfront cost for an exception that will probably be handled and dropped rather than displayed to a user.

I'm not recommending a move to the Isabelle style, there are plenty of advantages to having a single exception, but I'm noting one of the key disadvantages.

However, suppose that HOL_ERR also took a list of additional diagnostic values whose formatting is deferred lazily, i.e. (unit -> string) list. This would allow various failure points to add diagnostic details, with very little upfront cost.

The existing mk_HOL_ERR interface would be left unchanged for compatibility, I assume, and a standard helper for using the pretty-printer to add in terms would be added as another interface.