add @slots macro to improve readability of rules

[willow-ahrens]

My proposed, backwards-compatible, tilde-avoiding, rule syntax extension discussed in #344. This PR allows users to write, e.g., a chain of rules like:

@slots x y z a b c Chain([
    (@rule x^2 + 2x*y + y^2 => (x + y)^2),
    (@rule x^a * y^b => (x*y)^a * y^(b-a)),
    (@rule +(x...) => sum(x)),
])

We could write a single rule as

@rule a b a + b => add(a, b)

or

@slots a b @rule a + b => add(a, b)

This is accomplished by making 4 changes:

1. @capture and @rule take an optional (prefixed) list of symbols to turn into slots, e.g. @rule a b a + b => add(a, b)
2. @slots syms... expr adds the list of symbols syms to the beginning of each macrocall @rule @capture or @slots in the expression expr.
3. If a slot in a pattern would be the argument to a ... expression, it is interpreted as a segment.
4. Matched variables are injected directly as variables into the environment of the rhs of an @rule.

This change is backwards-compatible, as it still recognizes the ~a and ~~a syntax. The only instance where this would be breaking is if the user expected to be able to use the variable a in the rhs when a is also a slot or segment in the lhs. We could avoid this by only injecting variables declared with the new syntax, but I think it's a rare case anyway.

This PR is missing docs and tests, but I am happy to add those if there is interest.

[willow-ahrens]

For comparison, I believe the first example in the current syntax looks like

Chain([
    (@rule (~x)^2 + 2(~x)*~y + (~y)^2 => (~x + ~y)^2),
    (@rule (~x)^~a * (~y)^~b => ((~x)*~y)^(~a) * (~y)^(~b - ~a)),
    (@rule +(~~x) => sum(~~x)),
])

[shashi]

Let's get some docs and merge this!

[willow-ahrens]

I would also like to move forward with this PR.

@0x0f0f0f has expressed in the SymbolicManipulation slack that https://github.com/JuliaSymbolics/Metatheory.jl/pull/77 introduces a different ~-less syntax into MetaTheory.jl. If I understand correctly, the new syntax referred to is described in the file named NewSyntax.jl. The new syntax assumes any symbol that isn't the function name in a function call to be a slot variable. As an example, for the expression a + f(b), @0x0f0f0f's new syntax would turn a and b into slots, but read + and f from the local scope.

Unfortunately, @0x0f0f0f's new syntax would be a breaking change. It is not backwards-compatible with the current SymbolicUtils syntax, which expects symbols to default to their values in the local scope. If @0x0f0f0f is alright with instead using this PR (~, ~~, ... and the @slots syntax) to specify slot variables, then I think these changes can integrate with the other syntax changes in https://github.com/JuliaSymbolics/Metatheory.jl/pull/77, which are mostly different meanings for different kinds of arrows (e.g. =>, |> or -->).

[MasonProtter]

I'm pretty against using that new MetaTheory syntax in SymbolicUtils. I played around with it earlier and found it very frustrating and unpleasant to use

[willow-ahrens]

I have hidden this comment since it's out of date. The new metatheory syntax will be this PR and some new arrow types, so It's backwards-compatible with SU.

Please feel free to correct me if I'm wrong: After reading https://github.com/JuliaSymbolics/SymbolicUtils.jl/pull/368, I now see that this syntax doesn't need to play nice with MetaTheory's new syntax. This change is an extension to SU syntax, therefore corresponding changes would belong in MetaTheory's SUSyntax module. This change is orthogonal to the alternative, breaking, NewSyntax module being considered for MetaTheory.

[codecov-commenter]

Codecov Report

Merging #374 (4d07540) into master (48cc5ff) will increase coverage by 0.42%. The diff coverage is 97.67%.

@@            Coverage Diff             @@
##           master     #374      +/-   ##
==========================================
+ Coverage   83.70%   84.13%   +0.42%     
==========================================
  Files          12       12              
  Lines        1479     1506      +27     
==========================================
+ Hits         1238     1267      +29     
+ Misses        241      239       -2     

Impacted Files	Coverage Δ
src/rule.jl	91.35% <97.67%> (+6.91%)	:arrow_up:
src/polyform.jl	92.76% <0.00%> (-1.36%)	:arrow_down:
src/ordering.jl	89.53% <0.00%> (-1.17%)	:arrow_down:
src/code.jl	80.55% <0.00%> (-0.56%)	:arrow_down:

---

Continue to review full report at Codecov.

Legend - Click here to learn more Δ = absolute <relative> (impact), ø = not affected, ? = missing data Powered by Codecov. Last update 48cc5ff...4d07540. Read the comment docs.

[0x0f0f0f]

Please feel free to correct me if I'm wrong: After reading #368, I now see that this syntax doesn't need to play nice with MetaTheory's new syntax. This change is an extension to SU syntax, therefore corresponding changes would belong in MetaTheory's SUSyntax module. This change is orthogonal to the alternative, breaking, NewSyntax module being considered for MetaTheory.

Peter could you move this PR to Metatheory.jl/pull/77 please? It would avoid merging conflicts when #368 is done :)

[willow-ahrens]

If merging PRs into SymbolicUtils is not an option at this time, perhaps I should wait for things to settle a bit before merging into Metatheory.jl instead?

On the other hand, if you were planning to unify the Metatheory and SymbolicUtils syntaxes in Metatheory.jl/pull/77, then of course I can merge this into that PR.

[0x0f0f0f]

Yes, exactly, plan is to unify syntaxes and add more features to rules like the @theory macro! There is also the addition of the <:AbstractPat type to build rules programmatically!

[willow-ahrens]

It would help me if you could clarify what you mean by "unify the syntaxes." Are you referring to the solution that currently lives in MT/77 (separate submodules for two different syntaxes)?

If you're envisioning a solution with a single syntax for both SU and MT, would this unified syntax be backwards-compatible with current SU syntax or with the current MT syntax?

[0x0f0f0f]

It would help me if you could clarify what you mean by "unify the syntaxes." Are you referring to the solution that currently lives in MT/77 (separate submodules for two different syntaxes)? If you're envisioning a solution with a single syntax for both SU and MT, would this unified syntax be backwards-compatible with current SU syntax or with the current MT syntax?

it must be backwards compatible with SU syntax. MT NewSyntax currently does not have any dependent packages deployed to registry (and shouldn't). So my plan is to delete the NewSyntax module and idea altogether. Then, to merge your introduced features (@slots and ...) while maintaining backwards compatibility with SU syntax, so to have only one syntax module loaded by default in MT (that does not break anything downstream).

Only thing that is left to redesign is the meaning of arrows. In MT we are supporting many rules types. In the SU syntax => is a DynamicRule (rhs is evaluated as code, regular behaviour of SU). There is another arrow which meaning we should disambiguate and choose. The RewriteRule arrow. This rule type performs symbolic substitution without evaluating the RHS. It is needed in some cases (outside of SU) such as compiler optimization tasks where the expression types that are being rewritten do not support operator-level constructors (such as Expr, contrary to all <:Symbolic types). Other bidirectional rule arrows are unambiguous in both syntaxes (==, !=).

In the NewSyntax module, as you mentioned @peterahrens, the arrows meaning were => for RewriteRule and |> for DynamicRule. Since we are swapping the => arrow meaning for DynamicRule, what could be a binary operator for defining symbolic-substitution RewriteRules?

In MT's SUSyntax module I'm currently using -->. I don't really like it, it's visually confusing.

Another alternative idea could be ditching the difference between => and |> or --> completely. Using only the => and == operators and introducing a macro @srule a => b that imposes that the following rule will perform symbolic substitution only without evaluating code in the rhs. This is backwards compatible and not ambiguous at all. Let me know. I can dedicate a couple of days of work to finalize this release.

cc @shashi

[willow-ahrens]

Thanks for clarifying! Since the syntaxes will be compatible, I think the right thing to do is to merge this PR into SymbolicUtils first, so that there are tests and a well-defined syntax to compare against when testing MT77. @0x0f0f0f or I can copy the code to MT77 (@0x0f0f0f, let me know if you'd like a PR to your PR). Regarding merge conflicts, @0x0f0f0f can simply delete the code this PR introduces when resolving conflicts in https://github.com/JuliaSymbolics/SymbolicUtils.jl/pull/368. That way, https://github.com/JuliaSymbolics/SymbolicUtils.jl/pull/368 and MT/77 can be made simpler (closer to only moving code around).

[willow-ahrens]

Let's move the discussion of the arrows to https://github.com/JuliaSymbolics/Metatheory.jl/issues/68

[0x0f0f0f]

Thanks for clarifying! Since the syntaxes will be compatible, I think the right thing to do is to merge this PR into SymbolicUtils first, so that there are tests and a well-defined syntax to compare against when testing MT77. @0x0f0f0f or I can copy the code to MT77 (@0x0f0f0f, let me know if you'd like a PR to your PR). Regarding merge conflicts, @0x0f0f0f can simply delete the code this PR introduces when resolving conflicts in #368. That way, #368 and MT/77 can be made simpler (closer to only moving code around).

I just ported everything to MT77. I can delete in #368 later or we can close this and port everything that is left (docs and tests) to MT77 and then to #368.

[willow-ahrens]

@shashi After much discussion, this PR is ready for review. Docs and tests have been added.

[shashi]

Looks good! But @0x0f0f0f just merged MT#77 so maybe we should move this there?

[willow-ahrens]

MT#77 includes this change. If you think that #368 will take a while to review or merge, then you can merge this in the meantime, as a partway step. Otherwise, feel free to close this.

[shashi]

Thanks all!