Stream: Elpi users & devs

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


view this post on Zulip Kazuhiko Sakaguchi (Feb 27 2021 at 08:43):

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.

view this post on Zulip Enrico Tassi (Feb 27 2021 at 13:21):

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

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

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

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

view this post on Zulip Enrico Tassi (Feb 28 2021 at 17:30):

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: Feb 05 2023 at 13:02 UTC