More general equalsModProperty

[tobias-rnh]

Intended Change

Building on top of #3386, the interface EqualsModProperty has now been changed so that it can be used not just with Terms but theoretically any class if a proper Property is implemented. The signature of the method has also been slightly modified so that it is able to handle equality checks that utilize additional parameters (like was the case with equalsModRenaming defined on SourceElements that is also refactored with this PR). To refactor equalsModRenaming of SourceElement, a new Interface TreeWalker and implementing class JavaASTTreeWalker have been introduced that make it possible to move through the tree of SourceElements step by step.

Plan

~~Direct tests for JavaASTTreeWalker (currently only indirectly tested through tests for equalsModProperty)~~ ~~Even more doc comments~~

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: Already existing and new tests

Additional information and contact(s)

EqualsModProperty

The old TermEqualsModProperty

public interface TermEqualsModProperty {
    boolean equalsModProperty(Object o, TermProperty property);
    int hashCodeModProperty(TermProperty property);
}

has now been parameterized with a type T so that it can accommodate other classes than just Term:

public interface EqualsModProperty<T> {
    <V> boolean equalsModProperty(Object o, Property<T> property, V... v);
    int hashCodeModProperty(Property<T> property);
}

equalsModProperty is furthermore parameterized with a type V that can account for additional parameters needed for the equality check.

Properties

public interface TermProperty {
    Boolean equalsModThisProperty(Term term1, Term term2);
    int hashCodeModThisProperty(Term term);
}

is now parameterized with a type T so that it can accommodate other classes than just Term:

public interface Property<T> {
    <V> boolean equalsModThisProperty(T t1, T t2, V... v);
    int hashCodeModThisProperty(T t);
}

equalsModThisProperty is furthermore parameterized with a type V that can account for additional parameters needed for the equality check.

Refactoring of equalsModRenaming

As equals and equalsModRenaming for SourceElements were basically doing the same thing except for a few classes (equals mostly called equalsModRenaming), the idea was that the content of equalsModRenaming is moved to equals entirely. The special cases that did not call equalsModRenaming in equals or made use of the NameAbstractionTable are now handled by a JavaASTTreeWalker.

TreeWalker

The new JavaASTTreeWalker was necessary as the already existing JavaASTWalker recursively walks through the entire tree of SourceElements. That way, we are unable to walk two trees of SourceElements step by step at the same time, which is necessary to add program elements with a name to a NameAbstractionTable. JavaASTTreeWalker is a simple walker that is loosely based on the DOM TreeWalker as filtering is not yet supported.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.