Cyril Cohen (Oct 19 2023 at 11:42): Cyril Cohen (Oct 19 2023 at 11:42):How do I combine before "name" with x => y ?
Cyril Cohen (Oct 19 2023 at 14:08):FYI, I did not find a one-liner for this, but did something like:
pred graft.
:before "name"
x :- graft, !, c
then replaced the (:before "name" x :- c) => y that I wanted with graft => y this works terribly well...
Cyril Cohen (Oct 19 2023 at 14:08):@Enrico Tassi is there a shorter solution?
Enrico Tassi (Oct 19 2023 at 14:18):Grafting directive are not available to =>, the reason being that I had no example where one would not want p to be the first one to be tried in p => . In your use case too, it seems x :- c is expected to have high precedence.
Note that you don't need the full power of =>, since your clause is static, known a priori. So what you are doing is perfectly legit, although I'd rename graft into enable-whatever.
Cyril Cohen (Oct 19 2023 at 16:32):Enrico Tassi said:
In your use case too, it seems
x :- cis expected to have high precedence.
Actually, it's supposed to substitute for the default case.
Enrico Tassi said:
Note that you don't need the full power of
=>, since your clause is static, known a priori. So what you are doing is perfectly legit, although I'd renamegraftintoenable-whatever.
Of course! Here is my actual use case.
pred do-not-fail.
:before "term->gref:fail"
coq.term->gref _ _ :- do-not-fail, !, false.
(Otherwise coq.term->gref returns a fatal error if the term's head is not a gref)
Last updated: Oct 13 2024 at 01:02 UTC