New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
HOL_ERR to pick up term and type arguments #622
Comments
Most of the exception won't use these fields. |
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 ***@***.***> 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
<#622 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ABDgD8gNEikHwst4BxTF9-ifliRH6yDDks5u1Pc_gaJpZM4Y97cL>
.
|
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. |
For example, try
or
This will return a subset of the occurrences because it requires the |
Rather than trying to add additional fields of whatever type anyone will ever find useful, how about something like the following:
|
This is a good idea, though I'd perhaps prefer to use the slight abstraction provided by our existing |
Yes, I hadn't known about 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) |
Absolutely! |
Indeed term_to_string is slow. I understand the reason now. |
This would be better still as a term argument to the HOL_ERR (see #622).
Another option is to use lazy strings rather than terms, types, etc, since the I wrote that up in #928 which I now realise is probably just a part of this. |
One issue with this is that the 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 |
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 likeThe text was updated successfully, but these errors were encountered: