From a given Coq term with holes, I want to synthesize (and then accumulate) an Elpi clause that universally quantifies the holes in the term. For example, `synthesize {{ f _ (g _) }} Clause`

should succeed with `Clause = (pi x y\ clause {{ f lp:x (g lp:y) }} :- !)`

. To do so, I guess I have to define a new type that explicitly quantifies holes in terms (which forms a monad) and then write a translation from a term with holes to that type (which is a monadic variant of the `copy`

predicate, IIUC), as follows.

```
kind w-holes type -> type.
type w-holes.nil A -> w-holes A.
type w-holes.cons (term -> w-holes A) -> w-holes A.
pred w-holes.bind i:(w-holes A), i:(A -> w-holes B -> prop), o:(w-holes B).
w-holes.bind (w-holes.nil X) G Y :- !, G X Y.
w-holes.bind (w-holes.cons F) G (w-holes.cons F') :- !,
pi x\ w-holes.bind (F x) G (F' x).
pred w-holes.of-term i:term, o:(w-holes term).
...
```

Is there any easier way to do this (hopefully without defining such a type)? I also had to define a similar type for let-in bindings for another reason, and found that this is a bit painful. It looks like replacing such data types with `(A -> term) -> term`

(the continuation monad?) would work if I just want to introduce and lift binders during term traversal (as in the above `w-holes.of-term`

), but it makes things incomprehensible for me.

Hum, I think this applies here as well: https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users.20.26.20devs/topic/Renaming.20a.20subterm

The main difference is that you will bind with `pi x\`

rather than `fun ... x\`

. The other caveat is that in order to manipulate holes you have to write a predicate with an input argument, and either use `uvar`

or the `var`

builtin.

```
From elpi Require Import elpi.
Elpi Command generalize.
Elpi Accumulate lp:{{
% we add a new constructor to terms
type abs int -> term.
% gen first argument is in input mode, so we don't risk of assigning holes
% in the input
pred gen i:term, o:term, i:int, o:int.
% the rule we want (uvar is a keyword that matches holes, see ELPI.md in elpi's repo: https://github.com/LPCIC/elpi/blob/master/ELPI.md#modes)
gen (uvar as X) (abs M) N M :- coq.say "grabbing" X, !, M is N + 1.
% alternative: gen X (abs M) N M :- var X, !, M is N + 1.
% boring fold
gen (app L) (app L1) A A1 :- !, gen-list L L1 A A1.
gen T T A A.
gen-list [] [] A A.
gen-list [X|XS] [Y|YS] A A2 :- gen X Y A A1, gen-list XS YS A1 A2.
pred some-pred o:term.
% bind back abstracted subterms
pred bind i:int, i:term, o:prop.
bind 0 T (some-pred T1 :- !) :- copy T T1.
bind M T (pi x\ B x) :-
N is M - 1,
pi x\ copy (abs M) x => bind N T (B x).
main [trm T] :- std.do! [
gen T T1 0 M,
bind M T1 Clause,
coq.say {coq.term->string T} "===>" Clause,
].
}}.
Elpi generalize (3 + _).
```

There are a few occurrences of this in coq-elpi/apps/derive, there I typically have to `pi`

all parameters, and also add some premises after `:-`

(in that case, `:-`

takes on the RHS also a `list prop`

, you don't need to "fold L `,`

`true`

").

I'm not sure I understand the monad thing. Yes, binding forms a monad, but I'm not sure I understand what it brings.

I thought the use of the continuation monad may simplify the implementation since it provides a way to combine two objects involving binders. But my understanding of your answer is that I can do that in a different way (it looks really nice actually) so that I do not have to think about monads. Thanks!

I've recently added fold-map, it may spare you some code https://github.com/LPCIC/coq-elpi/blob/master/elpi/coq-lib.elpi#L152 (it's what I call `gen`

here)

Last updated: May 25 2024 at 20:01 UTC