Rodolphe Lepigre (Feb 29 2024 at 10:13): Rodolphe Lepigre (Feb 29 2024 at 10:13):Question for @Enrico Tassi: while debugging, we ended up adding the following code:
--- a/apps/NES/elpi/nes_synterp.elpi
+++ b/apps/NES/elpi/nes_synterp.elpi
@@ -16,6 +16,7 @@ begin-ns NS Path In Out :-
Clause = open-ns NS CP,
Out = [Clause | In],
@local! =>
+ coq.say "synterp.begin-ns" (clause _ (after "open-ns:begin") Clause),
coq.elpi.accumulate current "NES.db"
(clause _ (after "open-ns:begin") Clause).
and this seems to have the effect of accumulating the Clause twice. Is it obvious why?
Rodolphe Lepigre (Feb 29 2024 at 10:13):CC @Janno.
Enrico Tassi (Feb 29 2024 at 10:44):Hem, it is a bad choice in the syntax of Prolog that was inherited by Elpi. I should have signaled it in the tutorials.
The point is that A => B, C really reads (A => B), C hence the @local! attribute only operates on coq.say and not coq.elpi.accumulate.
Rodolphe Lepigre (Feb 29 2024 at 10:46):Makes sense, thanks!
Enrico Tassi (Feb 29 2024 at 10:46):and local is what makes the clause being dropped at the end of the module...
Notification Bot (Feb 29 2024 at 10:46):Enrico Tassi has marked this topic as resolved.
Pierre Roux (Feb 29 2024 at 10:49):Enrico Tassi said:
Hem, it is a bad choice in the syntax of Prolog that was inherited by Elpi. I should have signaled it in the tutorials.
I think you did a very good job pointing it in the tutorials. But well, it's so bad that we probably all have to be caught by it at least once before we remember it :sad:
Pierre Roux (Feb 29 2024 at 10:51):The only improvement I could see would be a warning in presence of A => B, C that would be silenced by both (A => B), C and A => (B, C)
Enrico Tassi (Feb 29 2024 at 11:57):Not a bad idea, but the current backend (where the warnings are generated) does not have enough info... the parser could do it, I guess, but right now it only emits errors
Pierre Roux (Feb 29 2024 at 12:46):Sure, I understand this can be tricky to actually implement.
Last updated: Oct 13 2024 at 01:02 UTC