Enzo Crance (May 09 2022 at 15:00): Enzo Crance (May 09 2022 at 15:00):Is there a tutorial on macros in Elpi? I haven't found it in the repositories.
Enrico Tassi (May 09 2022 at 15:25):No, the only doc is https://github.com/LPCIC/elpi/blob/master/ELPI.md#macros
Enzo Crance (May 15 2023 at 12:48):Is it possible for a macro to take a list of arguments and unpack it to pass it to an arbitrary arity predicate? I am thinking about doing a special macro for logging that would call coq.say internally, passing arguments to it without knowing their number. If I give the list to coq.say it prints a list, not all the arguments one by one.
I am thinking about something like apply in Lisp or the unpack operator * in Python.
Could this hypothetically be implemented in OCaml and added in the builtins?
pred apply i:variadic any prop, i:list any.
macro @log X Args :-
% do something with X like customise a prefix message, etc
apply coq.say Args.
% would work without writing the list at the call point, the last argument of a macro would be a list catching all the remaining arguments ?
@log 2 A B C
One would need to change the implementation of macros as well, which is bad piece of code I'll one day rewrite.
But you can also type coq.say Args and get a few spurious [ , , ], or write a regular predicate and use std.any->string and string.concat, or use the coq.pp facility to get boxes and line splitting.
So I'm not sure hacking the compiler and runtime would pay off
Last updated: Apr 16 2024 at 19:01 UTC