extend Lambda.subst on bound variables, add Lambda.duplicate #9216

gasche · 2019-12-28T21:06:20Z

It is invalid to reuse a Lambda.t term twice, because bound variables
may be used non-uniquely. If we want to perform a code transformation
may duplicate subterms in some cases, we have to refresh all bound
variables of the copied subterm.

The present PR implements a function

Lambda.duplicate : lambda -> lambda

that does exactly this. It is implemented by making Lambda.subst
parametrized over a transformation on bound variables.

gasche · 2019-12-28T21:07:54Z

(cc @chambart @trefis, who worked on similar questions somewhat recently)

The particular optimization whose study resulted in this PR is TRMC (#181), which generates several copies of a trmc-ed function (typically: one with the normal interface, and one or several in destination-passing style). In absence of such a function, this creates tricky bugs.

gasche · 2020-01-04T10:23:43Z

(Fixed check-typo.)

gasche · 2020-01-20T14:10:50Z

lambda/lambda.ml

        let lev_env =
          Ident.Map.fold (fun id _ env ->
            match Env.find_value (Path.Pident id) evt.lev_env with
            | exception Not_found -> env
            | vd -> update_env id vd env
-          ) s evt.lev_env
+          ) s lev_env


@chambart just asked me why there are two separate environments s (for free variables of the original term) and l (for bound variables traversed so far); the two environments are handled differently here: for free variables substituted by the user, we use the user-provided function update_env; for bound variables substituted in l, I do the correct thing which is to change the binding to the new bound variable name. (Ideally I would also remove the old binding to the substituted-away variable, but there is no API to remove a binding from debug environments.)

lambda/lambda.ml

chambart · 2020-01-20T14:11:12Z

lambda/lambda.ml

    | Lfunction lf ->
-        let s =
-          List.fold_right
-            (fun (id, _) s -> Ident.Map.remove id s)


Why remove that ?

The remove are removing the bound variables from the substitution, so that only free variables remain in the domain of the substitution. My idea was that having two environments of free and bound variables obviates this: I can always tell when something is a bound variable (would, before, have been removed from the map) by looking in l.

In the Tvar case I lookup in the bound-variable environment first, and only then in the free-variable environment. This means that there is no lookup in s for bound variables, so the remove would make no difference.

I'm fine with omitting the removal, but I'm worried that the code was present in the first place. Could you maybe assert that the parameters do not occur in s ? I would consider it an error if subst was called with a substitution for variables that are bound in the term, and also a problem if a variable is both free and bound in the term.

Actually, supporting the odd situations you mention was an explicit addition of #1606, supposedly for the purpose of "a (later) patch about let-rec compilation". I have cold feet about restricting the specification of the function again; I don't need it for my implementation, and I don't want to be responsible for potential breakages that could occur.

(I can see how you could end up in those odd situations if you inline a recursive definition within itself without freshening its bound identifiers. Interesting, the present PR provides an easy way to freshen those bound identifiers. In any case, I think that any such considerations could be left for another PR, possibly by someone else.)

gasche · 2020-03-31T17:27:54Z

I rebased the PR to address @chambart's comments. (If he or others would like to review, please do!)

gasche · 2020-04-29T12:18:21Z

I'm still looking for someone interested in reviewing or discussing this. (cc @chambart, but other people are warmly welcome.)

gasche · 2020-06-08T08:15:59Z

Still looking for a review.

lthls

I'm fine with this PR, which does what it is advertising to do in a generally pleasing way.

I've made some remarks, all of those that start with "Style:" can be completely ignored if you want. For the others I wouldn't mind having some kind of answer, but they do not affect the correctness of the code.

lambda/lambda.ml

lthls · 2020-06-08T15:43:41Z

lambda/lambda.ml

    | Lfunction lf ->
-        let s =
-          List.fold_right
-            (fun (id, _) s -> Ident.Map.remove id s)


I'm fine with omitting the removal, but I'm worried that the code was present in the first place. Could you maybe assert that the parameters do not occur in s ? I would consider it an error if subst was called with a substitution for variables that are bound in the term, and also a problem if a variable is both free and bound in the term.

lambda/lambda.ml

lambda/lambda.mli

lambda/lambda.ml

gasche · 2020-06-08T17:12:18Z

Thanks for the reviews! I pushed some commits to address most of @lthls points (I will squash them later). I still have to look at some things, and take into account @maranget's point on the environment. (I resolved all comments on which I am confident that no further discussion is useful.)

It is invalid to reuse a Lambda.t term twice, because bound variables may be used non-uniquely. If we want to perform a code transformation may duplicate subterms in some cases, we have to refresh all bound variables of the copied subterm. The present PR implements a function Lambda.duplicate : lambda -> lambda that does exactly this. It is implemented by making Lambda.subst parametrized over a transformation on bound variables.

gasche · 2020-06-10T08:17:17Z

@lthls I don't know if you would like to do another round of feedback on this one, or if I should get in the mindset of merging this eventually.

lthls · 2020-06-10T08:27:22Z

Apart from the Levent code that I haven't followed closely, every change you've made is in the right direction for me, so my approval still stands.

gasche · 2020-06-10T08:40:01Z

Let's talk about Levent just a bit.

Before this PR, the code would traverse the summary, and call update_env for each variable that would be part of the free-variable substitution. (In practice this is used by Lambda.rename which performs variable->variable renaming, and then the binding in the summary would be duplicated for the renamed variable as well (we don't know how to remove the old one, and we don't try to shadow it).)

What the PR does now (it did something less correct before, which I noticed and fixed after the question by @maranget) is to do a merge on the free-variable substitution and the bound-variable map, to decide for each binding in the union how to update the environment:

if the variable is bound, we use the same strategy as in rename (duplicate the binding to the new identifier)
if the variable is part of the free substitution (and not bound), we call update_env
otherwise we change nothing

gasche force-pushed the lambda-duplicate branch from 33cb463 to f573083 Compare January 4, 2020 10:23

gasche commented Jan 20, 2020

View reviewed changes

chambart reviewed Jan 20, 2020

View reviewed changes

gasche force-pushed the lambda-duplicate branch from f573083 to 446f301 Compare March 31, 2020 17:27

lthls approved these changes Jun 8, 2020

View reviewed changes

maranget reviewed Jun 8, 2020

View reviewed changes

lambda/lambda.ml Show resolved Hide resolved

gasche force-pushed the lambda-duplicate branch from 446f301 to 478c930 Compare June 8, 2020 17:09

gasche force-pushed the lambda-duplicate branch from bd81e12 to cc7d557 Compare June 9, 2020 07:38

gasche merged commit 50806ce into ocaml:trunk Jul 2, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

extend Lambda.subst on bound variables, add Lambda.duplicate #9216

extend Lambda.subst on bound variables, add Lambda.duplicate #9216

gasche commented Dec 28, 2019

gasche commented Dec 28, 2019 •

edited

gasche commented Jan 4, 2020

gasche Jan 20, 2020

chambart Jan 20, 2020

gasche Jan 21, 2020

lthls Jun 8, 2020

gasche Jun 8, 2020

gasche Jun 8, 2020

gasche commented Mar 31, 2020

gasche commented Apr 29, 2020

gasche commented Jun 8, 2020

lthls left a comment

lthls Jun 8, 2020

gasche commented Jun 8, 2020

gasche commented Jun 10, 2020

lthls commented Jun 10, 2020

gasche commented Jun 10, 2020

extend Lambda.subst on bound variables, add Lambda.duplicate #9216

extend Lambda.subst on bound variables, add Lambda.duplicate #9216

Conversation

gasche commented Dec 28, 2019

gasche commented Dec 28, 2019 • edited

gasche commented Jan 4, 2020

gasche Jan 20, 2020

Choose a reason for hiding this comment

chambart Jan 20, 2020

Choose a reason for hiding this comment

gasche Jan 21, 2020

Choose a reason for hiding this comment

lthls Jun 8, 2020

Choose a reason for hiding this comment

gasche Jun 8, 2020

Choose a reason for hiding this comment

gasche Jun 8, 2020

Choose a reason for hiding this comment

gasche commented Mar 31, 2020

gasche commented Apr 29, 2020

gasche commented Jun 8, 2020

lthls left a comment

Choose a reason for hiding this comment

lthls Jun 8, 2020

Choose a reason for hiding this comment

gasche commented Jun 8, 2020

gasche commented Jun 10, 2020

lthls commented Jun 10, 2020

gasche commented Jun 10, 2020

gasche commented Dec 28, 2019 •

edited