Synthesizing an Elpi clause from a Coq term with holes · Elpi users & devs

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.

Enrico Tassi (Feb 27 2021 at 13:21):

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 + _).

Enrico Tassi (Feb 27 2021 at 13:23):

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").

Enrico Tassi (Feb 27 2021 at 13:24):

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

Kazuhiko Sakaguchi (Feb 28 2021 at 10:27):

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!

Stream: Elpi users & devs

Topic: Synthesizing an Elpi clause from a Coq term with holes

Kazuhiko Sakaguchi (Feb 27 2021 at 08:43):

Enrico Tassi (Feb 27 2021 at 13:21):

Enrico Tassi (Feb 27 2021 at 13:23):

Enrico Tassi (Feb 27 2021 at 13:24):

Kazuhiko Sakaguchi (Feb 28 2021 at 10:27):

Enrico Tassi (Feb 28 2021 at 17:30):