Stream: Coq users

Topic: Aborting typeclass resolution in an instance


view this post on Zulip Armaël Guéneau (Aug 03 2020 at 15:30):

Is it possible to stop typeclass resolution prematurely from a Hint Extern? As is expected, simply failing in the hint will make the resolution backtrack and try other things; I'm wondering if it's possible to completely abort the resolution?

view this post on Zulip Armaël Guéneau (Aug 03 2020 at 16:05):

Alternatively, if that's not possible, I'm wondering if there's a "well-known" pattern for handling failure and returning error messages for prolog-like programs written using typeclass resolution -- similar to a "result" type

view this post on Zulip Ali Caglayan (Aug 03 2020 at 19:30):

Seems to be an open issue https://github.com/coq/coq/issues/4776

view this post on Zulip Paolo Giarrusso (Aug 03 2020 at 19:44):

I recall that Hint Cut exists and is relevant (it's in the manual), but I also did not understand its semantics or use it (or see anybody using it). IIRC, it performs Prolog-like cuts under some conditions.

view this post on Zulip Paolo Giarrusso (Aug 03 2020 at 19:44):

(which you can specify)

view this post on Zulip Cyril Cohen (Aug 03 2020 at 19:50):

No it does not perform prolog cuts. What does is Hint Extern If but the development is stalled (there is a PR by Matthieu somewhere)

view this post on Zulip Cyril Cohen (Aug 03 2020 at 19:51):

Anyway prolog fail is not implemented either. I strongly recommand any non trivial logic program for Coq to be implemted in coq-elpi for now, which is the only real meta logic programming language available for coq as of today afaik

view this post on Zulip Cyril Cohen (Aug 03 2020 at 19:53):

coq/coq#6285

view this post on Zulip Cyril Cohen (Aug 10 2020 at 12:36):

Armaël Guéneau said:

Alternatively, if that's not possible, I'm wondering if there's a "well-known" pattern for handling failure and returning error messages for prolog-like programs written using typeclass resolution -- similar to a "result" type

FTR I tried anything I could think of, the best result I got is the propagation of an error message with flag parameters for the class, but it does not always work....

view this post on Zulip Enrico Tassi (Aug 10 2020 at 12:39):

IIRC Ltac2 has a fatal error API. You should try that one.

view this post on Zulip Enrico Tassi (Aug 10 2020 at 12:40):

I've seen it in a demo, but I could not point you to the API, sorry.

view this post on Zulip Enrico Tassi (Aug 10 2020 at 12:40):

You'll have to dig yourself ;-)


Last updated: Jan 27 2023 at 00:03 UTC