Simplify replace_subtree interface

[acl33]

This attempts to address #784 with two changes:

• Don't pass the payload (expression to avoid capturing) to the applicator (function). Since the payload will not be changed by alpha-renaming (instead it causes changes to the Expr nodes that will contain it), any caller passing a payload can use the same Expr in the applicator if it wants to.
• Allow passing payload = None (if there is an applicator function instead).

It might be better to rename "payload" to something like "dont_capture", although the case with a payload and no applicator function, where the payload is inserted directly into the new expression (as used for inline_var), is still supported.

[awf]

Can you provide some examples?

replace_subtree(expr, location, new_subexpr, bindings_to_avoid_capturing)

An example of an example:

expr:   (let (x (FOO y)) (let (y 7) (add x y)))
loc:                                     ^
new:    (exp y)
avoid:  {y} # Just freeVars(new)?
result: (let (x (FOO y)) (let (y_0 7) (add (FOO y) y_0)))
                                           ^^^^^^^

An example where we need to use the lambda would be helpful, as it's clearly simpler to understand if we simply pass new_expr. An example where avoid should not be freevars(new_expr) would also help.

[acl33]

So for a ParsedRule that commutes adds:

expr: (let (x FOO) (let (y BAR) (add x y)))
loc:                            ^^^^^^^^^
new subtree: (add y x)
avoid: {} # do not rename binders of x or y
result: (let (x FOO) (let (y BAR) (add y x)))
                                  ^^^^^^^^^

As an example of a lambda, the current form of delete_let:

expr: (let (x FOO) (let (y BAR) (add x x)))
loc:               ^^^^^^^^^^^^^^^^^^^^^^
lambda: let_node => let_node.body # maybe assert first
avoid: {} # do not rename any binders
result: (let (x FOO) (add x x))

The lambda can be avoided in many cases if we store in the Match not just the location of the subtree to replace, but the subtree itself (or if we are willing to traverse the expression twice - first to retrieve the current subtree, then again to place the new one). For example, the previous example of delete_let then looks like:

expr: (let (x FOO) (let (y BAR) (add x x)))
loc:               ^^^^^^^^^^^^^^^^^^^^^^
subtree stored in Match object: (let (y BAR) (add x x))
new subtree: (add x x)
avoid: {} # do not rename binders of x
result: (let (x FOO) (add x x))

However, inlining a lam into a call, the lambda is necessary (?), because if there are renames to avoid capturing the lam-body, we need to perform these on the call-arguments before we put these in the result:

expr: (let (myfunc (lam (arg : Float) ....x....)) # note the x here - some outer x
            (let (x FOO)   # (re)bind x
               (Call myfunc x y))))    # x in arguments = the x bound to FOO
loc:           ^^^^^^^^^^^^^^^^^       # on last line
avoid: free_vars((lam (arg : Float) ...x...)) == {x}
lambda: (renamed_call) => (let (arg (renamed_call.args)) ....x....)
result: (let (myfunc (lam (arg : Float) ....x....)) # As before
              (let (x_1 FOO) # binder renamed to avoid capture
                 (let (arg (tuple x_1 y))  # the call arguments, after renaming
                     ....x....))  # the body of the lam, without renaming

So that's actually a bit more complicated than I suggested: it's not even that we apply renaming-to-avoid-capture only for some variables, rather, we need to apply renaming-to-avoid-capture to the existing subtree (before we build the new subtree from that) as well as the containing Expr nodes - (or, we apply renaming to some parts (but not all) of the new subtree)

This is in the test: https://github.com/microsoft/knossos-ksc/blob/45423d4371bf9c2e5889860538c82c63dbfcb18a/test/python/test_subst.py#L115-L135

[awf]

please edit above to include the carets showing the loc, as in the template I gave (I've done the first one)

[awf]

Why not this for delete_let?

expr: (let (x FOO) (let (y BAR) (add x x)))
loc:               ^^^^^^^^^^^^^^^^^^^^^^^
new_subtree: (add x x) # Just a pointer to the subtree
avoid: {}
result: (let (x FOO) (add x x))
                     ^^^^^^^^^

[awf]

expr: (let (myfunc (lam (arg : Float) ....x....)) # note the x here - some outer x
            (let (x FOO)   # (re)bind x
               (Call myfunc x y))))    # x in arguments = the x bound to FOO
loc: (1,1,) # body of "let myfunc", body of "let x"
avoid: free_vars((lam (arg : Float) ...x...)) == {x}
lambda: (renamed_call) => (let (arg (renamed_call.args)) ....x....)
result: (let (myfunc (lam (arg : Float) ....x....)) # As before
              (let (x_1 FOO) # binder renamed to avoid capture
                 (let (arg (tuple x_1 y))  # the call arguments, after renaming
                     ....x....))  # the body of the lam, without renaming

Oh my word. #807

[acl33]

expr: (let (myfunc (lam (arg : Float) ....x....)) # note the x here - some outer x
            (let (x FOO)   # (re)bind x
               (Call myfunc x y))))    # x in arguments = the x bound to FOO
loc: (1,1,) # body of "let myfunc", body of "let x"
avoid: free_vars((lam (arg : Float) ...x...)) == {x}
lambda: (renamed_call) => (let (arg (renamed_call.args)) ....x....)
result: (let (myfunc (lam (arg : Float) ....x....)) # As before
              (let (x_1 FOO) # binder renamed to avoid capture
                 (let (arg (tuple x_1 y))  # the call arguments, after renaming
                     ....x....))  # the body of the lam, without renaming

Oh my word. #807

I believe you've just realized the horror of lambda calculus ;-). Perhaps @simonpj might comment.

Given the case causing your horror, is the inlining of calls to lambdas that we don't have in the ks language yet, we should consider whether #807 is required for the first release (in which I do not believe calls will be able to name let-bound lambdas?), and then whether we could benefit in the meantime from simplifying the interface to replace_subtree if we don't need to support such case until a later release with ABU and language enhancements?

[awf]

I understand the lambda calculus, thank you. So why not ABU?

[awf]

Given the case causing your horror, is the inlining of calls to lambdas that we don't have in the ks language yet,

So why did we have the peculiar API for replace_subtree then?

[awf]

Or let me put it another way. You have shown a hairy case. ABU makes it go away. Is there another hairy case?

Answers at #807.

[acl33]

I understand the lambda calculus, thank you. So why not ABU?

Well, I did not say, welcome to the lambda calculus - but, welcome to the horrors. I don't mean to be sarcastic, rather, surely this must be a fairly standard situation, resulting from the standard application of standard rules? Perhaps it's actually less likely in lambda calculus compilers, as they are more likely to use other techniques, discussion of which should be in #807; but in other compilers? (Ah, hmm - SSA form is kind of ABU ?) Refactoring tools? (Maybe not something we want to copy!)

So why did we have the peculiar API for replace_subtree then?

This was my fault, in that at the time of writing #654 I was (wrongly) thinking that we would need to deal with that case, hence the test that replace_subtree allowed it. However #779 demonstrates that we do not need to deal with case, and so in #784 I commented that we could simplify by removing the ability to inline calls to lams, and you replied that you wanted to keep that ability. That then leads to wanting ABU.

My question is - given that ABU is a much larger change than #784 - whether we want to do any cleanups in the meantime, such as this PR?

[awf]

I would say wait until ABU to see how this might look