HOL_ERR to pick up term and type arguments

[mn200]

Change the fundamental exception to give exception-raisers the option of attaching relevant terms and types. For the sake of backwards compatibility, we can redefine helpers like mk_HOL_ERR and friends (creating values with empty lists). My suggestion would be something like

exception HOL_ERR of {origin_structure : string, origin_function : string, message : string,
                                        terms : term list, types : hol_type list}

[barakeel]

Most of the exception won't use these fields. So there might be a negligible amount of a (memory/cpu) waste. Could you provide motivating examples that require these changes?

[konrad-slind]

I agree with Thibault. Some additional ..._ERR exceptions could be perhaps be declared for more demanding situations, but HOL_ERR works OK the majority of the time.

On Mon, Dec 3, 2018 at 4:04 AM Thibault Gauthier [email protected] wrote:

Most of the exception won't use these fields. So there might be a negligible amount of a (memory/cpu) waste. Could you provide motivating examples that require these changes?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/622#issuecomment-443654493, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD8gNEikHwst4BxTF9-ifliRH6yDDks5u1Pc_gaJpZM4Y97cL .

[mn200]

I was actually thinking that it might be worthwhile to further add a location field. The parser could use these additional fields almost everywhere. Tactics that fail because a term has the wrong sort of shape would also use them. Decision procedures likewise.

If we were storing large numbers of exceptions, I might be worried about memory wastage, but almost all exceptions will live only transiently such that I'd be surprised if there were ever more than single digit numbers of them ever allocated at once.

[mn200]

For example, try

   grep -r --include='*.sml' failwith.*term_to_string src

or

   grep -r --include='*.sml' ERR.*term_to_string src

This will return a subset of the occurrences because it requires the term_to_string to appear on the same line as the ERR or failwith, but it still gets a number of hits. These are much worse for efficiency than simply being able to return the term in the proposed list field. Pretty-printing is expensive (i.e., slow) and the generated string is less helpful than actually being able to get your hands on the SML value.

[jeremydaw]

Rather than trying to add additional fields of whatever type anyone will ever find useful, how about something like the following:

exception HOL_ERR of {origin_structure : string, origin_function : string,
  message : string, terms : term list, types : hol_type list,
  further_info : exn list}
  
exception TT of term * hol_type ;

val tt = (``0``, ``:num``) ;

HOL_ERR {origin_structure = "os", origin_function = "of",
  message = "msg", terms = [], types = [], further_info = [TT tt]} ;

[mn200]

This is a good idea, though I'd perhaps prefer to use the slight abstraction provided by our existing UniversalType to get the same effect. I'd keep the common cases of terms and types, and maybe also the location information, but there's little harm in also having the “extra info” field as you describe.

[jeremydaw]

Yes, I hadn't known about UniversalType.

As with the exception constructors in my suggestion, users (ie those who create exceptions using this feature) would need to make sure the destructor function is available (signature-wise) to the end user (ie the one who sees the exception raised)

[mn200]

Absolutely!

[barakeel]

Indeed term_to_string is slow. I understand the reason now.

[talsewell]

Another option is to use lazy strings rather than terms, types, etc, since the most common case is for them to be printed to strings.

I wrote that up in #928 which I now realise is probably just a part of this.

[mn200]

One issue with this is that the HOL_ERR exception declaration has to happen in a context where terms and types are in scope. Currently, it’s declared before the kernel's types are established, which means that kernel operations and even functions in Lib can return it.

Though declaring the exception before term functions were defined, but after the type was set up, would allow term functions to throw it, type functions couldn't. Moreover, my experience elsewhere suggests that the terms put into such an exception wouldn't get pretty-printed well. The UniversalType argument might be a better approach.