Handling of qualified operations

[olynch]

This is me adding my two cents about qualified operations, as related to #209.

I think that the behavior of maybe_quote_operation in Metatheory.jl is confusing, and breaks lexical scoping.

I would prefer to have something like:

struct FuncRef
  # Fully-qualified module name
  fqmn::Vector{Symbol}
  name::Symbol
end

struct TypeRef
  fqmn::Vector{Symbol}
  name::Symbol
end

maybe_quote_operation(x::Function) = FuncRef([fullname(parentmodule(x))...], nameof(x))
maybe_quote_operation(x::DataType) = TypeRef([fullname(parentmodule(x))...], nameof(x))

Similarly, I think that the @rule macro should work differently. Rather than fully constructing the rule at macro-expansion time, the macro

@rule (~x + ~y) == (~y + ~x)

should expand to something like

Rule(App(+, [Var(1, :x), Var(2, :y)]) == App(+, [Var(2, :y), Var(1, :x)]))

Thus, the identity of + is given by whatever it is bound to in the current lexical scope, rather than simply treating it as :(+). This would be more in line with how SymbolicUtils works, and it would naturally solve #209.

[olynch]

Or really, why are we even quoting? Couldn't we just store the functions in the constant table directly? It seems like functions/types actually hash reasonably well.

[olynch]

OK, I see the problem: rewriting of Exprs would break with this approach.

How many things downstream rely on rewriting Exprs vs. rewriting TermInterface stuff?

[olynch]

Ah, I didn't carefully read src/Syntax.jl; I didn't understand that you do in fact resolve symbols in the current module! Neat. I'm going to close this.

[0x0f0f0f]

OK, I see the problem: rewriting of Exprs would break with this approach.

How many things downstream rely on rewriting Exprs vs. rewriting TermInterface stuff?

@olynch They are both TermInterface. This was already discussed a while ago and it took us ages with the Symbolics.jl team to find a decent TermInterface that supported both quoted and unquoted operations :)