Skip to content

Commit

Permalink
Remove EqualsModProofIrrelevancy interface
Browse files Browse the repository at this point in the history
  • Loading branch information
Drodt committed Dec 4, 2024
1 parent 3b3738d commit a0d6d50
Show file tree
Hide file tree
Showing 384 changed files with 970 additions and 112 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,13 @@
import java.util.stream.Collectors;

import de.uka.ilkd.key.logic.equality.EqualsModProperty;
import de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty;
import de.uka.ilkd.key.logic.equality.Property;
import de.uka.ilkd.key.logic.equality.RenamingTermProperty;
import de.uka.ilkd.key.logic.label.TermLabel;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;

import org.key_project.logic.Name;
import org.key_project.util.EqualsModProofIrrelevancy;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.java.CollectionUtil;

Expand All @@ -30,12 +28,7 @@
* while ignoring certain
* given properties. E.g. by using {@link RenamingTermProperty#RENAMING_TERM_PROPERTY}, just the
* term structures modulo
* renaming are compared whilst ignoring annotations.
* <p>
* Prior implementations of {@link EqualsModProofIrrelevancy} are now in
* {@link ProofIrrelevancyProperty}.
* </p>
*
* renaming are compared whilst ignoring annotations. *
*
* @see Term
* @see TermImpl
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
import de.uka.ilkd.key.logic.util.EqualityUtils;
import de.uka.ilkd.key.rule.EqualityModuloProofIrrelevancy;

import org.key_project.util.EqualsModProofIrrelevancy;
import org.key_project.util.EqualsModProofIrrelevancyUtil;
import org.key_project.util.collection.ImmutableArray;

Expand Down Expand Up @@ -45,7 +44,7 @@ private ProofIrrelevancyProperty() {}
* Checks if {@code term2} is a term syntactically equal to {@code term1}, except for attributes
* that are not relevant for the purpose of these terms in the proof.
* <p>
* Combines the prior implementations of {@link EqualsModProofIrrelevancy} in TermImpl and
* Combines the prior implementations of {@code EqualsModProofIrrelevancy} in TermImpl and
* LabeledTermImpl.
* </p>
*
Expand Down Expand Up @@ -102,8 +101,6 @@ public <V> boolean equalsModThisProperty(Term term1, Term term2, V... v) {
* <p>
* Computes a hashcode that represents the proof-relevant fields of {@code term}.
* </p>
* Combines the prior implementations of {@link EqualsModProofIrrelevancy} in TermImpl and
* LabeledTermImpl.
*
* @param term the term to compute the hashcode for
* @return the hashcode
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,7 @@
* variables are a
* separate syntactic category, and not a type of function.
* <br>
* <strong>As soon as there is a solution for
* {@link org.key_project.util.EqualsModProofIrrelevancy}, this class
* <strong>As soon as {@link AbstractTermTransformer#METASORT} is generalized, this class
* may be deleted.</strong>
*/
public class JFunction extends Function implements Operator, Sorted {
Expand Down Expand Up @@ -95,8 +94,8 @@ public JFunction(Name name, Sort sort, boolean isSkolemConstant) {
* checks if a given Term could be subterm (at the at'th subterm position) of a term with this
* function at its top level. The validity of the given subterm is NOT checked.
*
* @param at theposition of the term where this method should check the validity.
* @param possibleSub the subterm to be ckecked.
* @param at the position of the term where this method should check the validity.
* @param possibleSub the subterm to be checked.
* @return true iff the given term can be subterm at the indicated position
*/
private boolean possibleSub(int at, Term possibleSub) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -318,7 +318,7 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) {

/**
* Try to find the provided formula in the provided sequent,
* using {@link org.key_project.util.EqualsModProofIrrelevancy} to check for equality.
* using equality modulo proof irrelevancy.
*
* @param oldPos formula to look for
* @param newSequent sequent
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
import org.junit.jupiter.api.Test;

/**
* Tests for {@link org.key_project.util.EqualsModProofIrrelevancy}.
* Tests for equality modulo proof irrelevancy.
*
* @author Arne Keller
*/
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,16 +7,16 @@
import java.util.function.ToIntFunction;

/**
* Wrapper around an object that implements {@link EqualsModProofIrrelevancy}.
* Wrapper around an object that implements alternative equality and hash code methods.
* Forwards calls to {@link #equals(Object)} and {@link #hashCode()} to
* {@link EqualsModProofIrrelevancy#equalsModProofIrrelevancy(Object)} and
* {@link EqualsModProofIrrelevancy#hashCodeModProofIrrelevancy()}.
* {@link #equalityCmp} and
* {@link #hasher}.
*
* @param <T> type to wrap
* @author Arne Keller
*/
@SuppressWarnings("nullness")
public class EqualsModProofIrrelevancyWrapper<T> {
public class EqualsAndHashCodeDelegator<T> {
/**
* The wrapped object.
*/
Expand All @@ -25,12 +25,13 @@ public class EqualsModProofIrrelevancyWrapper<T> {
private final ToIntFunction<T> hasher;

/**
* Construct a new wrapper for the provided object. The provided object must implement
* {@link EqualsModProofIrrelevancy}.
* Construct a new wrapper for the provided object.
*
* @param inner object to wrap
* @param equalityCmp the equality method to be used
* @param hasher the hash method to be used
*/
public EqualsModProofIrrelevancyWrapper(T inner,
public EqualsAndHashCodeDelegator(T inner,
BiPredicate<T, T> equalityCmp,
ToIntFunction<T> hasher) {
this.inner = inner;
Expand All @@ -47,7 +48,7 @@ public boolean equals(Object o) {
return false;
}

EqualsModProofIrrelevancyWrapper<?> that = (EqualsModProofIrrelevancyWrapper<?>) o;
EqualsAndHashCodeDelegator<?> that = (EqualsAndHashCodeDelegator<?>) o;

return inner != null ? equalityCmp.test(inner, (T) that.inner) : that.inner == null;
}
Expand Down

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
import org.key_project.util.collection.ImmutableList;

/**
* Utility methods for the {@link EqualsModProofIrrelevancy} interface.
* Utility methods for the equals mod proof irrelevancy check.
*
* @author Arne Keller
*/
Expand All @@ -21,7 +21,7 @@ private EqualsModProofIrrelevancyUtil() {
}

/**
* Compare two arrays using the elements' {@link EqualsModProofIrrelevancy} implementation.
* Compare two arrays modulo proof irrelevancy.
*
* @param a first array
* @param b second array
Expand All @@ -48,8 +48,7 @@ public static <T> boolean compareImmutableArrays(
}

/**
* Compute the hashcode of an iterable using the elements' {@link EqualsModProofIrrelevancy}
* implementation.
* Compute the hashcode of an iterable modulo proof irrelevancy.
*
* @param iter iterable of elements
* @return combined hashcode
Expand All @@ -70,8 +69,7 @@ public static <T> int hashCodeIterable(Iterable<T> iter, ToIntFunction<T> hasher
}

/**
* Compare two immutable lists using the elements' {@link EqualsModProofIrrelevancy}
* implementation.
* Compare two immutable lists modulo proof irrelevancy.
* A null list is considered equal to a zero-sized list.
*
* @param a first list
Expand Down Expand Up @@ -99,8 +97,7 @@ public static <T> boolean compareImmutableLists(
}

/**
* Compute the hashcode of an immutable list using the elements'
* {@link EqualsModProofIrrelevancy}
* Compute the hashcode of an immutable list modulo proof irrelevancy.
* implementation.
*
* @param list list of elements
Expand Down
1 change: 1 addition & 0 deletions keyext.rusty/rust-wrapper/target/.rustc_info.json
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc_fingerprint":3195307579905410487,"outputs":{"4614504638168534921":{"success":true,"status":"","code":0,"stdout":"rustc 1.84.0-nightly (4f2f477fd 2024-10-23)\nbinary: rustc\ncommit-hash: 4f2f477fded0a47b21ed3f6aeddeafa5db8bf518\ncommit-date: 2024-10-23\nhost: x86_64-unknown-linux-gnu\nrelease: 1.84.0-nightly\nLLVM version: 19.1.1\n","stderr":""},"15729799797837862367":{"success":true,"status":"","code":0,"stdout":"___\nlib___.rlib\nlib___.so\nlib___.so\nlib___.a\nlib___.so\n/home/daniel/.rustup/toolchains/nightly-2024-10-24-x86_64-unknown-linux-gnu\noff\npacked\nunpacked\n___\ndebug_assertions\nfmt_debug=\"full\"\noverflow_checks\npanic=\"unwind\"\nproc_macro\nrelocation_model=\"pic\"\ntarget_abi=\"\"\ntarget_arch=\"x86_64\"\ntarget_endian=\"little\"\ntarget_env=\"gnu\"\ntarget_family=\"unix\"\ntarget_feature=\"fxsr\"\ntarget_feature=\"sse\"\ntarget_feature=\"sse2\"\ntarget_has_atomic\ntarget_has_atomic=\"16\"\ntarget_has_atomic=\"32\"\ntarget_has_atomic=\"64\"\ntarget_has_atomic=\"8\"\ntarget_has_atomic=\"ptr\"\ntarget_has_atomic_equal_alignment=\"16\"\ntarget_has_atomic_equal_alignment=\"32\"\ntarget_has_atomic_equal_alignment=\"64\"\ntarget_has_atomic_equal_alignment=\"8\"\ntarget_has_atomic_equal_alignment=\"ptr\"\ntarget_has_atomic_load_store\ntarget_has_atomic_load_store=\"16\"\ntarget_has_atomic_load_store=\"32\"\ntarget_has_atomic_load_store=\"64\"\ntarget_has_atomic_load_store=\"8\"\ntarget_has_atomic_load_store=\"ptr\"\ntarget_os=\"linux\"\ntarget_pointer_width=\"64\"\ntarget_thread_local\ntarget_vendor=\"unknown\"\nub_checks\nunix\n","stderr":""}},"successes":{}}
3 changes: 3 additions & 0 deletions keyext.rusty/rust-wrapper/target/CACHEDIR.TAG
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Signature: 8a477f597d28d172789f06886806bc55
# This file is a cache directory tag created by cargo.
# For information about cache directory tags see https://bford.info/cachedir/
Empty file.
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
0b482f9d09fe8b0d
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[\"perf-literal\", \"std\"]","declared_features":"[\"default\", \"logging\", \"perf-literal\", \"std\"]","target":9771195463141993919,"profile":10243973527296709326,"path":14341779084064582309,"deps":[[554324495028472449,"memchr",false,17868887934125138260]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/aho-corasick-a4d85f1f7e011e9e/dep-lib-aho_corasick","checksum":false}}],"rustflags":[],"metadata":13904389431191498124,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
a7002f68fbe71a3b
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[\"auto\", \"default\", \"wincon\"]","declared_features":"[\"auto\", \"default\", \"test\", \"wincon\"]","target":1736373845211751465,"profile":7959395715337908301,"path":18094606002502968462,"deps":[[4140584164330467587,"anstyle_parse",false,11562416134763488694],[4841825386763765772,"anstyle",false,11478260539685712771],[8720183142424604966,"utf8parse",false,6090743133543034409],[9119385831240683871,"is_terminal_polyfill",false,7978550353298358848],[11373957721457960839,"colorchoice",false,18290110254355698702],[17875114200413610454,"anstyle_query",false,13548699391446477530]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/anstream-caff7e85907949a9/dep-lib-anstream","checksum":false}}],"rustflags":[],"metadata":7500874485387469444,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
83b3597b25f94a9f
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[\"default\", \"std\"]","declared_features":"[\"default\", \"std\"]","target":4691279112367741833,"profile":7959395715337908301,"path":8204611676237499787,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/anstyle-3c24e018428cb281/dep-lib-anstyle","checksum":false}}],"rustflags":[],"metadata":14064844656010464607,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
b6a5d2d936f475a0
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[\"default\", \"utf8\"]","declared_features":"[\"core\", \"default\", \"utf8\"]","target":985948777999996156,"profile":7959395715337908301,"path":16849024412998873167,"deps":[[8720183142424604966,"utf8parse",false,6090743133543034409]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/anstyle-parse-3162f58a267a82d1/dep-lib-anstyle_parse","checksum":false}}],"rustflags":[],"metadata":9799137552285937175,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
daeab7fb4fa606bc
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[]","declared_features":"[]","target":2663518930196293257,"profile":7959395715337908301,"path":7615581767548581255,"deps":[],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/anstyle-query-ba85be343c043f10/dep-lib-anstyle_query","checksum":false}}],"rustflags":[],"metadata":10674566383365303417,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
9b8478a962427c0a
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[]","declared_features":"[]","target":11387529161390985894,"profile":5601947868832436996,"path":6772842809225066263,"deps":[[3474499548496471852,"env_logger",false,2262794480653654029],[6476581561599070667,"serde",false,14906573397576289421],[10793036991674847345,"key_wrapper",false,1832139669109492188],[12448247148799001525,"serde_json",false,4315822061808735760],[12992322993666529830,"clap",false,14688045012722537339],[16779514855709104956,"toml",false,17698180167813265972]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/cargo-key-219c860c787ca185/dep-lib-cargo_key","checksum":false}}],"rustflags":[],"metadata":2376146922787978900,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
b42ab0fda6d3d9b4
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[]","declared_features":"[]","target":9695809817815701792,"profile":11983525691607113661,"path":1874893257148842004,"deps":[[3474499548496471852,"env_logger",false,2262794480653654029],[6476581561599070667,"serde",false,14906573397576289421],[10793036991674847345,"key_wrapper",false,1832139669109492188],[12448247148799001525,"serde_json",false,4315822061808735760],[12992322993666529830,"clap",false,14688045012722537339],[15139195121139870255,"cargo_key",false,755551829008876699],[16779514855709104956,"toml",false,17698180167813265972]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/cargo-key-49f78e16ef565d93/dep-test-bin-cargo-key","checksum":false}}],"rustflags":[],"metadata":2376146922787978900,"config":2202906307356721367,"compile_kind":0}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
7401b17da8589bbe
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[]","declared_features":"[]","target":9695809817815701792,"profile":5601947868832436996,"path":1874893257148842004,"deps":[[3474499548496471852,"env_logger",false,2262794480653654029],[6476581561599070667,"serde",false,14906573397576289421],[10793036991674847345,"key_wrapper",false,1832139669109492188],[12448247148799001525,"serde_json",false,4315822061808735760],[12992322993666529830,"clap",false,14688045012722537339],[15139195121139870255,"cargo_key",false,755551829008876699],[16779514855709104956,"toml",false,17698180167813265972]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/cargo-key-aa2e81a5cf2902af/dep-bin-cargo-key","checksum":false}}],"rustflags":[],"metadata":2376146922787978900,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
b02c57a54f05e8d5
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[]","declared_features":"[]","target":14295905777831417870,"profile":11983525691607113661,"path":1193460770330799409,"deps":[[3474499548496471852,"env_logger",false,2262794480653654029],[6476581561599070667,"serde",false,14906573397576289421],[10793036991674847345,"key_wrapper",false,1832139669109492188],[12448247148799001525,"serde_json",false,4315822061808735760],[12992322993666529830,"clap",false,14688045012722537339],[15139195121139870255,"cargo_key",false,755551829008876699],[16779514855709104956,"toml",false,17698180167813265972]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/cargo-key-c7392722823c1423/dep-test-bin-key-rustc","checksum":false}}],"rustflags":[],"metadata":2376146922787978900,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
b604369eaf18de2e
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[]","declared_features":"[]","target":11387529161390985894,"profile":11983525691607113661,"path":6772842809225066263,"deps":[[3474499548496471852,"env_logger",false,2262794480653654029],[6476581561599070667,"serde",false,14906573397576289421],[10793036991674847345,"key_wrapper",false,1832139669109492188],[12448247148799001525,"serde_json",false,4315822061808735760],[12992322993666529830,"clap",false,14688045012722537339],[16779514855709104956,"toml",false,17698180167813265972]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/cargo-key-e46a9c72d6da4be7/dep-test-lib-cargo_key","checksum":false}}],"rustflags":[],"metadata":2376146922787978900,"config":2202906307356721367,"compile_kind":0}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
95655c203530f9cb
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
{"rustc":9739624705989529557,"features":"[]","declared_features":"[]","target":14295905777831417870,"profile":5601947868832436996,"path":1193460770330799409,"deps":[[3474499548496471852,"env_logger",false,2262794480653654029],[6476581561599070667,"serde",false,14906573397576289421],[10793036991674847345,"key_wrapper",false,1832139669109492188],[12448247148799001525,"serde_json",false,4315822061808735760],[12992322993666529830,"clap",false,14688045012722537339],[15139195121139870255,"cargo_key",false,755551829008876699],[16779514855709104956,"toml",false,17698180167813265972]],"local":[{"CheckDepInfo":{"dep_info":"debug/.fingerprint/cargo-key-f423f6b8b580290c/dep-bin-key-rustc","checksum":false}}],"rustflags":[],"metadata":2376146922787978900,"config":2202906307356721367,"compile_kind":0}
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Binary file not shown.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
This file has an mtime of when this was started.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
7b5346541e6bd6cb
Loading

0 comments on commit a0d6d50

Please sign in to comment.