You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: