Stream: Elpi users & devs

Topic: Abstract function application

Enzo Crance (Apr 14 2021 at 18:36):

Hello. I am trying to transform a pair of elpi values (a Coq term and a list of elpi functions) into a Coq function whose body applies the term to the elpi functions called on the bound variables. Starting from this:

G : term
[F1, ..., Fn] : list (term -> term)

I would like to make this:

fun x1 ... xn => lp:{{ app [G, F1 x1, ..., Fn xn] }}

I have been struggling for a while with the pi operator once again, but have not managed to program it properly. Is there a standard way to do this? Thanks.

Enrico Tassi (Apr 14 2021 at 20:51):

From elpi Require Import elpi.

Elpi Command test.
Elpi Accumulate lp:{{

pred loop i:list (term -> term), i:list term, i:term, o:term.
loop [] ArgsRev Head T :- std.rev ArgsRev Args, coq.mk-app Head Args T.
loop [F|Fs] ArgsRev Head (fun Label {{nat}} x\ Bo x) :-
  coq.name-suffix `a` {std.length ArgsRev} Label, % not really needed
  pi a\ % we need to move under x to build Bo, so we postulate a symbol a
    loop Fs [F a|ArgsRev] % and we pass a to F
      Head (Bo a). % and plays the role of x inside Bo

main _ :-
  loop
    [ (x\app[{{S}},x]) , (x\app[{{plus}},{{2}},x]) ] % These are the F1 ... Fn
    [] % initial value of the accumulator ArgsRev
    {{mult}}   % this is G
    T,
  coq.say T.

}}.
Elpi test.

prints

fun `a0` (global (indt «nat»)) c0 \
 fun `a1` (global (indt «nat»)) c1 \
  app
   [global (const «Nat.mul»), app [global (indc «S»), c0],
    app [global (const «Nat.add»), ... , c1]]

Enrico Tassi (Apr 14 2021 at 20:51):

This is a quite recurrent pattern, while you recurse, you apply the variable introduced by pi to some argument.
Sorry, I don't have much time to explain further.

Enzo Crance (Apr 15 2021 at 08:14):

Enrico Tassi said:

This is a quite recurrent pattern, while you recurse, you apply the variable introduced by pi to some argument.
Sorry, I don't have much time to explain further.

Great. There is no elpi notion in your code that I do have never encountered before, so I will read it in detail and I think I will understand it. Thank you very much!

Enrico Tassi (Apr 15 2021 at 10:32):

This one also works, but is less efficient, since coq.mk-app has to append [F a] at the end of T, but if it is not a bottleneck, then this code is simpler.

pred loop i:list (term -> term), i:term, o:term.
loop [] T T.
loop [F|Fs] T (fun `a` {{nat}} x\ Bo x) :-
  pi a\
    loop Fs {coq.mk-app T [F a]} (Bo a).

Last updated: Oct 13 2024 at 01:02 UTC