Stream: Elpi users & devs

Topic: Macro tutorial


view this post on Zulip Enzo Crance (May 09 2022 at 15:00):

Is there a tutorial on macros in Elpi? I haven't found it in the repositories.

view this post on Zulip Enrico Tassi (May 09 2022 at 15:25):

No, the only doc is https://github.com/LPCIC/elpi/blob/master/ELPI.md#macros

view this post on Zulip 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

view this post on Zulip Enrico Tassi (May 15 2023 at 15:22):

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: May 19 2024 at 16:02 UTC