Skip to content

Commit

Permalink
Remove SVSubstitute
Browse files Browse the repository at this point in the history
  • Loading branch information
Drodt committed May 22, 2024
1 parent 4bbd87b commit 87a57de
Show file tree
Hide file tree
Showing 75 changed files with 224 additions and 182 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil;
import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;

import org.key_project.logic.SyntaxElement;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;

Expand Down Expand Up @@ -76,7 +77,7 @@ public abstract class AbstractConditionalBreakpoint extends AbstractHitCountBrea
* A {@link Map} mapping from relevant variables for the condition to their runtime equivalent
* in KeY
*/
private Map<SVSubstitute, SVSubstitute> variableNamingMap;
private Map<SyntaxElement, SyntaxElement> variableNamingMap;

/**
* The list of parameter variables of the method that contains the associated breakpoint
Expand Down Expand Up @@ -162,14 +163,14 @@ private void putValuesFromGlobalVars(ProgramVariable varForCondition, Node node,
*
* @return the cloned map
*/
private Map<SVSubstitute, SVSubstitute> getOldMap() {
Map<SVSubstitute, SVSubstitute> oldMap = new HashMap<>();
for (Entry<SVSubstitute, SVSubstitute> svSubstituteSVSubstituteEntry : getVariableNamingMap()
private Map<SyntaxElement, SyntaxElement> getOldMap() {
Map<SyntaxElement, SyntaxElement> oldMap = new HashMap<>();
for (Entry<SyntaxElement, SyntaxElement> svSubstituteSVSubstituteEntry : getVariableNamingMap()
.entrySet()) {
Entry<?, ?> oldEntry = svSubstituteSVSubstituteEntry;
if (oldEntry.getKey() instanceof SVSubstitute
&& oldEntry.getValue() instanceof SVSubstitute) {
oldMap.put((SVSubstitute) oldEntry.getKey(), (SVSubstitute) oldEntry.getValue());
if (oldEntry.getKey() instanceof SyntaxElement
&& oldEntry.getValue() instanceof SyntaxElement) {
oldMap.put((SyntaxElement) oldEntry.getKey(), (SyntaxElement) oldEntry.getValue());
}
}
return oldMap;
Expand Down Expand Up @@ -200,7 +201,7 @@ private void freeVariablesAfterReturn(Node node, RuleApp ruleApp, boolean inScop
* @param oldMap the oldMap variableNamings
*/
private void putValuesFromRenamings(ProgramVariable varForCondition, Node node, boolean inScope,
Map<SVSubstitute, SVSubstitute> oldMap, RuleApp ruleApp) {
Map<SyntaxElement, SyntaxElement> oldMap, RuleApp ruleApp) {
// look for renamings KeY did
boolean found = false;
// get current renaming tables
Expand All @@ -215,7 +216,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
.getHashMap().entrySet()) {
Entry<?, ?> entry = value;
if (entry.getKey() instanceof LocationVariable
&& entry.getValue() instanceof SVSubstitute) {
&& entry.getValue() instanceof SyntaxElement) {
if ((VariableNamer.getBasename(((LocationVariable) entry.getKey()).name()))
.equals(varForCondition.name())
&& ((LocationVariable) entry.getKey()).name().toString()
Expand All @@ -229,7 +230,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
// add new value
toKeep.add((LocationVariable) entry.getValue());
getVariableNamingMap().put(varForCondition,
(SVSubstitute) entry.getValue());
(SyntaxElement) entry.getValue());
found = true;
break;
} else if (inScope && ((LocationVariable) entry.getKey()).name()
Expand All @@ -242,7 +243,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
// add new value
toKeep.add((LocationVariable) entry.getValue());
getVariableNamingMap().put(varForCondition,
(SVSubstitute) entry.getValue());
(SyntaxElement) entry.getValue());
found = true;
break;
}
Expand All @@ -263,7 +264,7 @@ private void putValuesFromRenamings(ProgramVariable varForCondition, Node node,
protected void refreshVarMaps(RuleApp ruleApp, Node node) {
boolean inScope = isInScope(node);
// collect old values
Map<SVSubstitute, SVSubstitute> oldMap = getOldMap();
Map<SyntaxElement, SyntaxElement> oldMap = getOldMap();
// put values into map which have to be replaced
for (ProgramVariable varForCondition : getVarsForCondition()) {
// put global variables only done when a variable is instantiated by
Expand Down Expand Up @@ -498,14 +499,14 @@ public Set<LocationVariable> getToKeep() {
/**
* @return the variableNamingMap
*/
public Map<SVSubstitute, SVSubstitute> getVariableNamingMap() {
public Map<SyntaxElement, SyntaxElement> getVariableNamingMap() {
return variableNamingMap;
}

/**
* @param variableNamingMap the variableNamingMap to set
*/
public void setVariableNamingMap(Map<SVSubstitute, SVSubstitute> variableNamingMap) {
public void setVariableNamingMap(Map<SyntaxElement, SyntaxElement> variableNamingMap) {
this.variableNamingMap = variableNamingMap;
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@

import de.uka.ilkd.key.rule.MatchConditions;

import org.key_project.logic.SyntaxElement;
import org.key_project.util.ExtList;
import org.key_project.util.collection.ImmutableArray;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
package de.uka.ilkd.key.java;

import de.uka.ilkd.key.java.visitor.Visitor;
import de.uka.ilkd.key.logic.op.SVSubstitute;

import org.key_project.logic.SyntaxElement;

Expand All @@ -14,7 +13,7 @@
* to achieve an immutable structure
*/

public interface SourceElement extends SVSubstitute, SyntaxElement {
public interface SourceElement extends SyntaxElement {


/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.java;

import org.key_project.logic.SyntaxElement;
import org.key_project.logic.TerminalSyntaxElement;

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
package de.uka.ilkd.key.java.declaration;

import de.uka.ilkd.key.java.JavaProgramElement;
import de.uka.ilkd.key.java.TerminalProgramElement;
import de.uka.ilkd.key.java.visitor.Visitor;

import org.key_project.logic.SyntaxElement;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@

import de.uka.ilkd.key.java.declaration.Modifier;

import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.util.ExtList;

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@

import de.uka.ilkd.key.java.LoopInitializer;
import de.uka.ilkd.key.java.NonTerminalProgramElement;
import de.uka.ilkd.key.java.TerminalProgramElement;

import org.key_project.util.collection.ImmutableArray;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
import de.uka.ilkd.key.java.statement.ILoopInit;
import de.uka.ilkd.key.logic.op.IProgramMethod;
import de.uka.ilkd.key.logic.op.IProgramVariable;

import org.key_project.logic.SyntaxElement;

/**
Expand All @@ -31,5 +32,5 @@ public interface ProgramConstruct extends Expression, Statement, ILoopInit, IFor
SyntaxElement getChild(int n);

@Override
int getChildCount() ;
int getChildCount();
}
3 changes: 1 addition & 2 deletions key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
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 de.uka.ilkd.key.logic.op.SVSubstitute;

import org.key_project.logic.Name;
import org.key_project.logic.Visitor;
Expand Down Expand Up @@ -43,7 +42,7 @@
* supported: {@link Term#execPostOrder(Visitor)} and {@link Term#execPreOrder(Visitor)}.
*/
public interface Term
extends SVSubstitute, Sorted, TermEqualsModProperty, org.key_project.logic.Term {
extends Sorted, TermEqualsModProperty, org.key_project.logic.Term {
@Override
Operator op();

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@
* @see TermLabelManager
*/
// spotless:on
public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove*/ TerminalSyntaxElement {
public interface TermLabel extends Named, SyntaxElement, /* TODO: Remove */ TerminalSyntaxElement {

/**
* Retrieves the i-th parameter object of this term label.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -125,7 +125,7 @@ public String toString() {
return super.toString();
}

public static class JavaModalityKind extends Kind implements SVSubstitute {
public static class JavaModalityKind extends Kind {
private static final Map<String, JavaModalityKind> kinds = new HashMap<>();
/**
* The diamond operator of dynamic logic. A formula <alpha;>Phi can be read as after
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
* etc. have to implement this interface.
*/
public interface Operator
extends org.key_project.logic.op.Operator, SVSubstitute, EqualsModProofIrrelevancy {
extends org.key_project.logic.op.Operator, EqualsModProofIrrelevancy {

/**
* comparator to compare operators; for modalities only their kind is compared
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@

import org.key_project.logic.Name;
import org.key_project.logic.SyntaxElement;
import org.key_project.logic.TerminalSyntaxElement;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;

Expand All @@ -34,7 +33,8 @@
* Objects of this class are schema variables matching program constructs within modal operators.
* The particular construct being matched is determined by the ProgramSVSort of the schema variable.
*/
public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator , SyntaxElement {
public final class ProgramSV extends OperatorSV
implements ProgramConstruct, UpdateableOperator, SyntaxElement {
public static final Logger LOGGER = LoggerFactory.getLogger(ProgramSV.class);

private static final ProgramList EMPTY_LIST_INSTANTIATION =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@

import java.util.WeakHashMap;

import org.key_project.logic.SyntaxElement;
import org.key_project.logic.TerminalSyntaxElement;

public class Qualifier<T> implements TerminalSyntaxElement {
Expand Down
12 changes: 0 additions & 12 deletions key.core/src/main/java/de/uka/ilkd/key/logic/op/SVSubstitute.java

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,15 @@
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.rule.inst.SVInstantiations;

import org.key_project.logic.TerminalSyntaxElement;

/**
* TermTransformer perform complex term transformation which cannot be (efficiently or at all)
* described by taclets.
*/
public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator, /*TODO: check*/ TerminalSyntaxElement {
public interface TermTransformer extends org.key_project.logic.op.SortedOperator, Operator,
/* TODO: check */ TerminalSyntaxElement {

/**
* initiates term transformation of <tt>term</tt>. Note the top level operator of of parameter
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,8 @@
/**
* Schema variable that is instantiated with logical variables.
*/
public final class VariableSV extends OperatorSV implements QuantifiableVariable, TerminalSyntaxElement {
public final class VariableSV extends OperatorSV
implements QuantifiableVariable, TerminalSyntaxElement {

/**
* Creates a new SchemaVariable that is used as placeholder for bound(quantified) variables.
Expand Down
12 changes: 6 additions & 6 deletions key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@
import de.uka.ilkd.key.logic.TermFactory;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.op.SVSubstitute;
import de.uka.ilkd.key.util.InfFlowSpec;

import org.key_project.logic.SyntaxElement;
import org.key_project.util.collection.DefaultImmutableSet;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;
Expand All @@ -36,7 +36,7 @@ public class OpReplacer {
/**
* The replacement map.
*/
private final ReplacementMap<? extends SVSubstitute, ? extends SVSubstitute> map;
private final ReplacementMap<? extends SyntaxElement, ? extends SyntaxElement> map;

/**
* <p>
Expand All @@ -53,7 +53,7 @@ public class OpReplacer {
* with
* @param tf a term factory.
*/
public OpReplacer(Map<? extends SVSubstitute, ? extends SVSubstitute> map, TermFactory tf) {
public OpReplacer(Map<? extends SyntaxElement, ? extends SyntaxElement> map, TermFactory tf) {
this(map, tf, null);
}

Expand All @@ -65,12 +65,12 @@ public OpReplacer(Map<? extends SVSubstitute, ? extends SVSubstitute> map, TermF
* @param tf a term factory.
* @param proof the currently loaded proof
*/
public OpReplacer(Map<? extends SVSubstitute, ? extends SVSubstitute> map, TermFactory tf,
public OpReplacer(Map<? extends SyntaxElement, ? extends SyntaxElement> map, TermFactory tf,
Proof proof) {
assert map != null;

this.map = map instanceof ReplacementMap
? (ReplacementMap<? extends SVSubstitute, ? extends SVSubstitute>) map
? (ReplacementMap<? extends SyntaxElement, ? extends SyntaxElement>) map
: ReplacementMap.create(tf, proof, map);

this.tf = tf;
Expand Down Expand Up @@ -234,7 +234,7 @@ public Term replace(Term term) {
return newTerm;
}

for (SVSubstitute svs : map.keySet()) {
for (SyntaxElement svs : map.keySet()) {
if (term.equalsModProperty(svs, TERM_LABELS_PROPERTY)) {
return (Term) map.get(svs);
}
Expand Down
13 changes: 7 additions & 6 deletions key.core/src/main/java/de/uka/ilkd/key/proof/ReplacementMap.java
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,12 @@
import de.uka.ilkd.key.logic.TermFactory;
import de.uka.ilkd.key.logic.label.OriginTermLabel;
import de.uka.ilkd.key.logic.label.TermLabelManager;
import de.uka.ilkd.key.logic.op.SVSubstitute;
import de.uka.ilkd.key.settings.ProofSettings;
import de.uka.ilkd.key.settings.TermLabelSettings;
import de.uka.ilkd.key.util.LinkedHashMap;

import org.key_project.logic.SyntaxElement;

/**
* A map to be used in an {@link OpReplacer}. It maps operators that should be replaced to their
* replacements.
Expand All @@ -25,7 +26,7 @@
* @param <S> the type of the elements to replace.
* @param <T> the type of the replacements.
*/
public interface ReplacementMap<S extends SVSubstitute, T> extends Map<S, T> {
public interface ReplacementMap<S extends SyntaxElement, T> extends Map<S, T> {

/**
* Creates a new replacement map.
Expand All @@ -36,7 +37,7 @@ public interface ReplacementMap<S extends SVSubstitute, T> extends Map<S, T> {
* @param proof the currently loaded proof, or {@code null} if no proof is loaded.
* @return a new replacement map.
*/
static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
static <S extends SyntaxElement, T> ReplacementMap<S, T> create(TermFactory tf,
Proof proof) {
var noIrrelevantTermLabelsMap = proof == null
? ProofSettings.DEFAULT_SETTINGS.getTermLabelSettings().getUseOriginLabels()
Expand All @@ -58,7 +59,7 @@ static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
* @param initialMappings a map whose mapping should be added to the new replacement map.
* @return a new replacement map.
*/
static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
static <S extends SyntaxElement, T> ReplacementMap<S, T> create(TermFactory tf,
Proof proof, Map<S, T> initialMappings) {
ReplacementMap<S, T> result = create(tf, proof);
result.putAll(initialMappings);
Expand All @@ -77,7 +78,7 @@ static <S extends SVSubstitute, T> ReplacementMap<S, T> create(TermFactory tf,
* @param <S> the type of the operators to replace.
* @param <T> the type of the replacements.
*/
class DefaultReplacementMap<S extends SVSubstitute, T> extends LinkedHashMap<S, T>
class DefaultReplacementMap<S extends SyntaxElement, T> extends LinkedHashMap<S, T>
implements ReplacementMap<S, T> {
private static final long serialVersionUID = 6223486569442129676L;
}
Expand All @@ -98,7 +99,7 @@ class DefaultReplacementMap<S extends SVSubstitute, T> extends LinkedHashMap<S,
*
* @see OriginTermLabel
*/
class NoIrrelevantLabelsReplacementMap<S extends SVSubstitute, T>
class NoIrrelevantLabelsReplacementMap<S extends SyntaxElement, T>
implements ReplacementMap<S, T> {

/**
Expand Down
Loading

0 comments on commit 87a57de

Please sign in to comment.