Armaël Guéneau (Aug 03 2020 at 15:30): 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?
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
Ali Caglayan (Aug 03 2020 at 19:30):Seems to be an open issue https://github.com/coq/coq/issues/4776
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.
Paolo Giarrusso (Aug 03 2020 at 19:44):(which you can specify)
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)
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
Cyril Cohen (Aug 03 2020 at 19:53): 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....
Enrico Tassi (Aug 10 2020 at 12:39):IIRC Ltac2 has a fatal error API. You should try that one.
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.
Enrico Tassi (Aug 10 2020 at 12:40):You'll have to dig yourself ;-)
Last updated: Oct 01 2023 at 18:01 UTC