Philip Kaludercic (May 12 2024 at 21:31): Philip Kaludercic (May 12 2024 at 21:31):Is there an easy way to fix the synterp issues and do whatever Coq/Coq-ELPI did before the last update? I have don't understand what it is doing and don't have to time to read into the technical details, so I'd really appreciate a simple hack to fix the issue.
Philip Kaludercic (May 12 2024 at 21:38):I am specifically referring to the
The command did perform no (more) actions during the parsing phase (aka
synterp), while during the execution phase (aka interp) it tried to perform a
begin-module "eval" action. Interp actions must match synterp actions. For
example if a module was imported during the synterp phase, then it must also
be imported during the interp one.
Since adding #[synterp] appears to break our code that used to work just fine.
Enrico Tassi (May 13 2024 at 05:35):No hack. I can help porting your code if you give me a pointer. Or at least tell you if it is easy or hard.
Philip Kaludercic (May 13 2024 at 05:38):I'd would appreciate that very much! These should be the relevant files:
Philip Kaludercic (May 13 2024 at 05:38): Philip Kaludercic (May 13 2024 at 05:41):Without #[synterp] added in line 9 of Abella2Coq.v I get the above error message, with #[synterp] the main predicate fails to match. I tried using the main-synterp and main-interp predicates, but they didn't help either.
Philip Kaludercic (May 13 2024 at 05:58):I understand that this is related to begin-module in this file: https://git8.cs.fau.de/software/abellatocoq/-/blob/main/src/elpi/translation.elpi#L509, but I don't know what Elpi wants me to do? Should I declare another predicate, that will just announce the module during the interp/synterp phase?
Philip Kaludercic (May 13 2024 at 06:49):(the last point allowed me to temporarily hack around the issue, so the problem has become less urgent, yet it would still be nice to figure out how to update the code appropriately)
Enrico Tassi (May 13 2024 at 14:51):Here it is. I could not test it, but it compiles.
diff --git a/src/elpi/translation.elpi b/src/elpi/translation.elpi
index 7863ac8..067015e 100644
--- a/src/elpi/translation.elpi
+++ b/src/elpi/translation.elpi
@@ -505,8 +505,9 @@ generate-mod! Ps :-
% == Wrapper predicate ===============================================
pred translate i:string i:list ast-term i:ast-tyctx.
-translate Name Mods Sigs :-
- coq.env.begin-module {coq.env.fresh-global-id Name} none,
+translate _ Mods Sigs :-
+ coq.next-synterp-action (begin-module ID),
+ coq.env.begin-module ID none,
generate-sig! Sigs,
generate-mod! Mods,
coq.env.end-module _.
diff --git a/src/theories/Abella2Coq.v b/src/theories/Abella2Coq.v
index 6bfd2ac..9d76b51 100644
--- a/src/theories/Abella2Coq.v
+++ b/src/theories/Abella2Coq.v
@@ -7,6 +7,18 @@ From Abella2Coq.elpi Extra Dependency "translation.elpi" as translation.
Elpi Accumulate File translation.
From Abella2Coq.elpi Extra Dependency "abella2coq.elpi" as abella2coq.
Elpi Accumulate File abella2coq.
+#[synterp] Elpi Accumulate lp:{{
+main [str _, str "as", str Name] :-
+ coq.env.begin-module Name none, coq.env.end-module _.
+
+main [str ExtraDep] :-
+ std.last {rex.split "\\." ExtraDep} Name,
+ coq.env.begin-module Name none, coq.env.end-module _.
+
+main _ :-
+ coq.error "Usage: Abella2Coq FILE [as MODULE NAME]?".
+
+}}.
Elpi Typecheck.
Elpi Export Abella2Coq.
The only thing is that it does not check anymore for a global id, but the test was anyway wrong IMO, since you create a module and not a definition.
Enrico Tassi (May 13 2024 at 14:52):The program running in synterp phase just announces the creation of the module.
The real program stays the same, and has to create the same module.
Enrico Tassi (May 13 2024 at 14:53):of course you could factor some code, etc, but the patch should help you anyway.
Enrico Tassi (May 13 2024 at 14:56):And good luck with your submission!
Last updated: Oct 13 2024 at 01:02 UTC