juliasymbolics / terminterface.jl

interface for symbolic terms

TermInterface.jl

This package contains definitions for common functions that are useful for symbolic expression manipulation. Its purpose is to provide a shared interface between various symbolic programming Julia packages, for example SymbolicUtils.jl, Symbolics.jl and Metatheory.jl.

Docs

You can read the documentation here.

terminterface.jl's Issues

outdated doc string copies in the README

PRs #35 and #39 failed to update the doc string copies in the README. They need to either:

1. be updated or
2. deleted from the README as redundant, as the doc strings should already be included in the autogenerated JuliaHub docs

base this on AbstractTrees.jl

It seems like it would make a lot of sense to base this package on the AbstractTrees.jl interface. That is, require users to implement the AbstractTrees.jl interface and any additional functions that are required after that. So some of the functions from this package could be made internal, users wouldn't have to add any methods to those functions. That would enable more interoperability across the ecosystem. Also, TBH, I'm not sure if this package is even necessary given that AbstractTrees.jl already exists?

https://juliahub.com/ui/Packages/General/AbstractTrees

request for new functions: `isvariable` and `variablename`

I want to be able to convert any TermInterface.jl expression to one of the expression types defined by my CallableExpressions.jl package. However, I don't think that TermInterface.jl on its own currently makes that possible. The problem is that, for leaves of the expression tree, I'm not able to:

• tell variables apart from constants

• convert a foreign variable type to a native variable type, for that I need to associate the variable with a name, as each variable is determined by a single Symbol value in CallableExpressions.jl

I think it'd make sense for TermInterface.jl to introduce two additional functions:

• isvariable (name subject to bikeshedding, of course): isvariable(x) should be true when x is a single variable, and it should be false when x is a constant or an expression (neither constant expressions nor variable expressions count as "a variable" here)

• variablename(x) should return an object representing a unique name for the variable, ideally convertible to Symbol

Thoughts?

all `maketerm` arguments should be mandatory

Having two optional arguments means each source code method gets triplicated by the compiler.

Given that this package is supposed to be low-level, making the arguments mandatory should be OK.

Register

@JuliaRegistrator register

`unsorted_arguments`

sometimes you don't need the arguments of an associative-commutative operation in a lexicographically ordered form. In such cases there can be a faster accessor for arguments. This function should be in this package so that we can all use it. Most importantly Rewriters.jl can use it.

`istree` on Expr

should not be true in my opinion because terms may want to hold Exprs. As we discussed, MT could use _istree(x) = istree(x) || x isa Expr...

cc @0x0f0f0f

Add `exprhead` function

The exprhead function should return :call if a symbolic expression can be seen as a function call, :ref if it can be seen as a getindex operation etc... It is different from operation, that should return the function operation of the symbolic term This solves the ugly hack and inconsistency that is used in Metatheory.jl to support e-matching on symbolic types where operation is not :call etc...

This should improve and simplify the codebase of SU and MT when:

• generalizing patterns away from the underlying symbolic representation
• parsing patterns
• converting symbolic expressions to Expr
• printing symbolic expressions
• pattern matching against both Expr and Term etc...
• Representation and printing of e-nodes.

Most importantly this improvement will allow for consistent pattern matching in both egraphs and classical rewriting, in order to finalize the integration and solve the Expr inconsistency:
Patterns will have an operation and an exprhead, and should match against both. Currently, SU only uses operation for pattern matching, and MT uses
only the equivalent of exprhead. Combining them together will allow both systems to pattern match and rewrite against both types of expressions. A keyword argument should be added to similarterm.

cc @shashi

TagBot trigger issue

This issue is used to trigger TagBot; feel free to unsubscribe.

If you haven't already, you should update your TagBot.yml to include issue comment triggers.
Please see this post on Discourse for instructions and more details.

If you'd like for me to do this for you, comment TagBot fix on this issue.
I'll open a PR within a few hours, please be patient!

(Possibly) move `wrap` and `unwrap` here

So that packages (like SymbolicSAT) can use them without depending on Symbolics.

What do you think @YingboMa ?

get rid of the fourth argument of `maketerm`, `type`

maketerm(T, head, children, type=nothing, metadata=nothing)

Constructs an expression. [...], type is the type of the S-expression.

What is the meaning of the type argument here? "Type of the sexp" means nothing to me, sexps don't have type?

Originally posted by @nsajko in #25 (comment)

The fourth argument, type, seems like it's not generally useful for expressions, and redundant with the next argument, metadata. Is there any reason why it should exist in this interface?

I notice that the in-development version of Metatheory.jl that supports the current TermInterface.jl always ignores both type and metadata, and so will my package. EDIT: actually my package does use metadata for some types.

Was type only introduced to make things slightly more convenient for the SymbolicUtils.jl implementation?

Improve docs before bumping new version

I'll work on it

`istree` should only receive objects and not types

Fix broken tests in JuliaSymbolics/SymbolicUtils.jl#432

Relationship to SymbolicUtils etc

Hi,

Documentation for this package says,

Its purpose is to provide a shared interface between various symbolic programming Julia packages, for example SymbolicUtils.jl, Symbolics.jl and Metatheory.jl.

But SymbolicUtils doesn't depend on it, and in fact seems incompatible:

julia> using SymbolicUtils; import TermInterface

julia> @syms x::Int
(x,)

julia> TermInterface.exprhead(x + 1)
ERROR: MethodError: no method matching exprhead(::SymbolicUtils.BasicSymbolic{Int64})

Closest candidates are:
  exprhead(::Expr)
   @ TermInterface ~/.julia/packages/TermInterface/6hcD2/src/expr.jl:5

Stacktrace:
 [1] top-level scope
   @ REPL[2]:1

Digging into this, I came across JuliaSymbolics/SymbolicUtils.jl#505 from a few months ago.

Given this, what is the current and planned relationship of this package to the rest of the ecosystem? Will it be deprecated? If we want to program to an interface to make it easy to use tools from the JuliaSymbolics ecosystem, what's now the "right" way to do that?

Redesign proposal

Interfaces for traversing terms is easy, but similarterm is the main magic of this package. The awkwardness of the current implementation is the use of exprhead as a keyword argument in similarterm. SymbolicUtils only has (mostly) terms that represent function calls, but we couldn't just ignore exprhead because Julia tries to dispatch on it. Also, exprhead is set to :call by default -- a clear sign of abstraction leak. I think it's time to take concept of a "head" seriously...

The proposal is to just make head the first argument to similarterm instead of the reference object in whose image we are trying to build the new term. It then also makes sense to rename similarterm to maketerm. This also allows one to compute the head in other ways than using a reference term.

So the new interface could be:

maketerm(h::H, t; type=Any, metadata=nothing) # -> to be implemented by provider of H
head(t) = h
tail(t) = t

I'm using the word tail because arguments is already in use to mean basically tail[2:end] in the case that the head is a function call. It would presumably have this check programmatically, going forward.

In SymbolicUtils, we would define

struct SUApply end
maketerm(::SUApply, tail; kw...) = term(tail...; kw...)
istree(x::Symbolic) = true # replace Symbolic with concrete types that are tree
head(x::Symbolic) = SUTerm()
tail(x::Symbolic) = (operation(x), arguments(x)...) # or some efficient alternative

So this would stay within the closure of types that represent function calls.

In Metatheory you'd just need to add a MTHead type.

struct MTHead; head::Symbol; end
maketerm(h::MTHead, tail) = Expr(h.head, tail...)
head(::Expr) = MTTerm() # This will be considered piracy, however, so you might want to add a wrapper around Expr in MT eventually

I have thought about this a lot, and I think it's easiest to leave type and metadata as keyword arguments, and not try to cram them into head or something like that, but other arguments are welcome. These are like the stuff after : in a typed language definition.

This should address #10 and answer #15.

@0x0f0f0f @willow-ahrens @YingboMa

Should `issym` take type?

Instances are OK in SU, but what about MT @0x0f0f0f ?

Rethinking exprhead

Not all usages of rewriting are for julia-esque programs, so its not immediately clear what exprhead should be for those applications, and the documentation doesn't make it super clear. Can we make exprhead default to :call so that the operation function defaults to being understood as returning a relevant expression node constructor by default?

expr vs call?

I don't understand the difference between isexpr and iscall. Perhaps give in the docs an example: a type T and x::T such that isexpr(x) != iscall(x)?