Stream: Elpi users & devs

Topic: Renaming a subterm


view this post on Zulip Enzo Crance (Feb 08 2021 at 17:02):

Now suppose that I have f : A -> B and I need to rename a subterm f x into a variable y : B. The following predicate fails and I think that I know why:

rename (app [E, X]) Y :-
    target-typ E Ty,
    pi y\
      decl y _ Ty =>
      Y = y.

It fails because Y = y makes the newly created y "leak" outside of the pi rule, whereas the predicate you gave me was using recursion under a binder, never "going out". What would be the idiomatic solution for renaming?

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

You got it right, the problem is the scope of y. The slogan is "there is not such a thing as a free variable".

Here you need y to exist before rename is called, otherwise Y cannot see it. In some sense you need to allocate y in advance. It is hard to suggest any other solution without seeing more code.

view this post on Zulip Enrico Tassi (Feb 08 2021 at 17:12):

I think I can imagine what you are trying to do, see for example the reification example https://github.com/LPCIC/coq-elpi/blob/master/examples/example_reflexive_tactic.v . There the y are not real bound variable, but rather numbers. You could also go this way.

view this post on Zulip Enzo Crance (Feb 08 2021 at 17:15):

I am exploring the AST of a Coq term and I want to hide some subtrees behind names, so I need to introduce new variables. I'm checking your link right now.

view this post on Zulip Enrico Tassi (Feb 08 2021 at 17:20):

So, either you do it in 2 passes, first you see how many you need, then you create binders for all of them and rename... but it depends what you really have to do, without knowing more I can't be more precise. Well, I've to go now.

view this post on Zulip Enzo Crance (Feb 08 2021 at 17:21):

Thank you very much for all the help!

view this post on Zulip Enrico Tassi (Feb 09 2021 at 11:03):

I wrote a silly example of another way to skin the cat, hope it helps.

From elpi Require Import elpi.
Elpi Command generalize.
Elpi Accumulate lp:{{
% we add a new constructor to terms
type abs int -> term.
% the rule we want
gen {{ 1 }} (abs M) N M :- !, 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.
% bind back abstracted subterms
bind 0 T T1 :- copy T T1.
bind M T {{ fun x => lp:(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 T2,
  coq.say {coq.term->string T} "===>" {coq.term->string T2},
].
}}.

Elpi generalize (3 + 7).

It prints

(3 + 7) ===> (fun (x : ?e) (x0 : ?e0) => S (S x0) + S (S (S (S (S (S x))))))

view this post on Zulip Enzo Crance (Feb 09 2021 at 11:16):

So every 1 encountered in the term is changed to an abstraction abs with a counter, then after the first run, another predicate runs replacing every abstraction with the correct variable according to the number encoded in this abs constructor. I think I understand the idea; I'll give it a try on my problem and see if it fits. Thank you for the additional idea.


Last updated: Mar 29 2024 at 15:02 UTC