Skip to content

Commit

Permalink
Clean up for syntactical replace visitors
Browse files Browse the repository at this point in the history
  • Loading branch information
@unp1
unp1 committed Jan 15, 2025
1 parent 7cc5c77 commit 56a2b8f
Show file tree
Hide file tree
Showing 2 changed files with 44 additions and 66 deletions.
52 changes: 16 additions & 36 deletions key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import de.uka.ilkd.key.strategy.quantifierHeuristics.ConstraintAwareSyntacticalReplaceVisitor;

import org.key_project.logic.op.sv.SchemaVariable;
import org.key_project.logic.sort.Sort;
Expand All @@ -37,7 +36,7 @@
*
* @author Dominic Steinhoefel
*/
public class LightweightSyntacticalReplaceVisitor implements DefaultVisitor {
public final class LightweightSyntacticalReplaceVisitor implements DefaultVisitor {
private final SVInstantiations svInst;
private final Services services;
private final TermBuilder tb;
Expand Down Expand Up @@ -67,10 +66,6 @@ public LightweightSyntacticalReplaceVisitor(SVInstantiations svInst, Services se
subStack = new Stack<>(); // of Term
}

public LightweightSyntacticalReplaceVisitor(Services services) {
this(SVInstantiations.EMPTY_SVINSTANTIATIONS, services);
}

private JavaProgramElement addContext(StatementBlock pe) {
final ContextStatementBlockInstantiation cie = svInst.getContextInstantiation();
if (cie == null) {
Expand All @@ -91,11 +86,10 @@ private JavaBlock replacePrg(SVInstantiations svInst, JavaBlock jb) {
}

ProgramReplaceVisitor trans;
ProgramElement result = null;

if (jb.program() instanceof ContextStatementBlock) {
ProgramElement result;
if (jb.program() instanceof ContextStatementBlock csb) {
trans = new ProgramReplaceVisitor(
new StatementBlock(((ContextStatementBlock) jb.program()).getBody()), // TODO
new StatementBlock(csb.getBody()), // TODO
services, svInst);
trans.start();
result = addContext((StatementBlock) trans.result());
Expand Down Expand Up @@ -131,14 +125,6 @@ protected void pushNew(Object t) {
subStack.push(t);
}

/**
* the method is only still invoked to allow the
* {@link ConstraintAwareSyntacticalReplaceVisitor} to recursively replace meta variables
*/
protected Term toTerm(Term o) {
return o;
}

private ElementaryUpdate instantiateElementaryUpdate(ElementaryUpdate op) {
final UpdateableOperator originalLhs = op.lhs();
if (originalLhs instanceof SchemaVariable originalLhsAsSV) {
Expand All @@ -147,10 +133,7 @@ private ElementaryUpdate instantiateElementaryUpdate(ElementaryUpdate op) {
lhsInst = ((Term) lhsInst).op();
}

final UpdateableOperator newLhs;
if (lhsInst instanceof UpdateableOperator) {
newLhs = (UpdateableOperator) lhsInst;
} else {
if (!(lhsInst instanceof final UpdateableOperator newLhs)) {
assert false : "not updateable: " + lhsInst;
throw new IllegalStateException("Encountered non-updateable operator " + lhsInst
+ " on left-hand side of update.");
Expand All @@ -174,12 +157,11 @@ private Operator instantiateModality(Modality op, JavaBlock jb) {

protected Operator instantiateOperator(Operator p_operatorToBeInstantiated, JavaBlock jb) {
Operator instantiatedOp = p_operatorToBeInstantiated;
if (p_operatorToBeInstantiated instanceof SortDependingFunction) {
instantiatedOp =
handleSortDependingSymbol((SortDependingFunction) p_operatorToBeInstantiated);
} else if (p_operatorToBeInstantiated instanceof ElementaryUpdate) {
if (p_operatorToBeInstantiated instanceof SortDependingFunction sortDependingFunction) {
instantiatedOp =
instantiateElementaryUpdate((ElementaryUpdate) p_operatorToBeInstantiated);
handleSortDependingSymbol(sortDependingFunction);
} else if (p_operatorToBeInstantiated instanceof ElementaryUpdate elementaryUpdate) {
instantiatedOp = instantiateElementaryUpdate(elementaryUpdate);
} else if (p_operatorToBeInstantiated instanceof Modality mod) {
instantiatedOp = instantiateModality(mod, jb);
} else if (p_operatorToBeInstantiated instanceof SchemaVariable sv) {
Expand All @@ -205,13 +187,11 @@ private ImmutableArray<QuantifiableVariable> instantiateBoundVariables(Term visi
if (boundVar instanceof SchemaVariable boundSchemaVariable) {
final Term instantiationForBoundSchemaVariable =
(Term) svInst.getInstantiation(boundSchemaVariable);
// instantiation might be null in case of PO generation for taclets
if (instantiationForBoundSchemaVariable != null) {
boundVar = (QuantifiableVariable) instantiationForBoundSchemaVariable.op();
} else {
// this case may happen for PO generation of taclets
boundVar = (QuantifiableVariable) boundSchemaVariable;
varsChanged = true;
}
varsChanged = true;
}
newVars[j] = boundVar;
}
Expand All @@ -233,8 +213,8 @@ public void visit(final Term visited) {
if (visitedOp instanceof SchemaVariable visitedSV && visitedOp.arity() == 0
&& svInst.isInstantiated(visitedSV)
&& (!(visitedOp instanceof ProgramSV visitedPSV && visitedPSV.isListSV()))) {
final Term newTerm = toTerm(svInst.getTermInstantiation(visitedSV,
svInst.getExecutionContext(), services));
final Term newTerm = svInst.getTermInstantiation(visitedSV,
svInst.getExecutionContext(), services);
pushNew(newTerm);
} else {
// instantiation of java block
Expand Down Expand Up @@ -285,8 +265,8 @@ private Operator handleSortDependingSymbol(SortDependingFunction depOp) {
}

private Term resolveSubst(Term t) {
if (t.op() instanceof SubstOp) {
Term resolved = ((SubstOp) t.op()).apply(t, tb);
if (t.op() instanceof SubstOp substOp) {
final Term resolved = substOp.apply(t, tb);
return tb.label(resolved, t.sub(1).getLabels());
} else {
return t;
Expand Down Expand Up @@ -322,7 +302,7 @@ public void subtreeEntered(Term subtreeRoot) {
/**
* this method is called in execPreOrder and execPostOrder in class Term when leaving the
* subtree rooted in the term subtreeRoot. Default implementation is to do nothing. Subclasses
* can override this method when the visitor behaviour depends on informations bound to
* can override this method when the visitor behaviour depends on information bound to
* subtrees.
*
* @param subtreeRoot root of the subtree which the visitor leaves.
Expand Down
58 changes: 28 additions & 30 deletions key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,8 +24,8 @@
import de.uka.ilkd.key.rule.Taclet.TacletLabelHint;
import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import de.uka.ilkd.key.strategy.quantifierHeuristics.ConstraintAwareSyntacticalReplaceVisitor;

import org.key_project.logic.Visitor;
import org.key_project.logic.op.sv.SchemaVariable;
import org.key_project.logic.sort.Sort;
import org.key_project.prover.rules.Rule;
Expand All @@ -34,15 +34,16 @@
import org.key_project.util.collection.ImmutableArray;

/**
* visitor for <t> execPostOrder </t> of {@link de.uka.ilkd.key.logic.Term}. Called with that method
* visitor for method {@link de.uka.ilkd.key.logic.Term#execPostOrder(Visitor)}. Called with that
* method
* on a term, the visitor builds a new term replacing SchemaVariables with their instantiations that
* are given as a SVInstantiations object.
*/
public class SyntacticalReplaceVisitor implements DefaultVisitor {
public static final String SUBSTITUTION_WITH_LABELS_HINT = "SUBSTITUTION_WITH_LABELS";
protected final SVInstantiations svInst;
protected final Services services;
/** the termbuilder used to construct terms */
/** the term builder used to construct terms */
protected final TermBuilder tb;
private Term computedResult = null;
protected final PosInOccurrence applicationPosInOccurrence;
Expand Down Expand Up @@ -91,13 +92,13 @@ private SyntacticalReplaceVisitor(TermLabelState termLabelState, TacletLabelHint
this.labelHint = labelHint;
this.goal = goal;
subStack = new Stack<>(); // of Term
if (labelHint instanceof TacletLabelHint) {
if (labelHint != null) {
labelHint.setTacletTermStack(tacletTermStack);
}
}

/**
* ONLY TO BE USED BZ ConstraintAwareSyntacticalReplaceVisitor (HACK)
* ONLY TO BE USED BY ConstraintAwareSyntacticalReplaceVisitor (HACK)
* constructs a term visitor replacing any occurrence of a schemavariable found in
* {@code svInst} by its instantiation
*
Expand All @@ -124,7 +125,7 @@ public SyntacticalReplaceVisitor(TermLabelState termLabelState, TacletLabelHint
this.labelHint = labelHint;
this.goal = null;
subStack = new Stack<>(); // of Term
if (labelHint instanceof TacletLabelHint) {
if (labelHint != null) {
labelHint.setTacletTermStack(tacletTermStack);
}
}
Expand Down Expand Up @@ -152,9 +153,10 @@ public SyntacticalReplaceVisitor(TermLabelState termLabelState, TacletLabelHint
/**
* ONLY used by {@link de.uka.ilkd.key.strategy.termgenerator.TriggeredInstantiations}
*
* @param termLabelState
* @param svInst
* @param services
* @param termLabelState the termlabel state
* @param svInst mapping of schemavariables to their instantiation
* @param services the Services with information about the logic signature, access to term
* construction etc.
*/
public SyntacticalReplaceVisitor(TermLabelState termLabelState, SVInstantiations svInst,
Services services) {
Expand Down Expand Up @@ -190,7 +192,7 @@ private JavaBlock replacePrg(SVInstantiations svInst, JavaBlock jb) {
}

ProgramReplaceVisitor trans;
ProgramElement result = null;
ProgramElement result;

if (jb.program() instanceof ContextStatementBlock) {
trans = new ProgramReplaceVisitor(
Expand Down Expand Up @@ -233,7 +235,9 @@ protected void pushNew(Object t) {

/**
* the method is only still invoked to allow the
* {@link ConstraintAwareSyntacticalReplaceVisitor} to recursively replace meta variables
* {@link de.uka.ilkd.key.strategy.quantifierHeuristics.ConstraintAwareSyntacticalReplaceVisitor}
* to recursively
* replace meta variables
*/
protected Term toTerm(Term o) {
return o;
Expand All @@ -244,8 +248,8 @@ private ElementaryUpdate instantiateElementaryUpdate(ElementaryUpdate op) {
final UpdateableOperator originalLhs = op.lhs();
if (originalLhs instanceof SchemaVariable originalLhsAsSV) {
Object lhsInst = svInst.getInstantiation(originalLhsAsSV);
if (lhsInst instanceof Term) {
lhsInst = ((Term) lhsInst).op();
if (lhsInst instanceof Term lhsInstAsTerm) {
lhsInst = lhsInstAsTerm.op();
}

final UpdateableOperator newLhs;
Expand Down Expand Up @@ -276,12 +280,10 @@ private Operator instantiateModality(Modality op, JavaBlock jb) {

private Operator instantiateOperator(Operator p_operatorToBeInstantiated, JavaBlock jb) {
Operator instantiatedOp = p_operatorToBeInstantiated;
if (p_operatorToBeInstantiated instanceof SortDependingFunction) {
instantiatedOp =
handleSortDependingSymbol((SortDependingFunction) p_operatorToBeInstantiated);
} else if (p_operatorToBeInstantiated instanceof ElementaryUpdate) {
instantiatedOp =
instantiateElementaryUpdate((ElementaryUpdate) p_operatorToBeInstantiated);
if (p_operatorToBeInstantiated instanceof SortDependingFunction sortDependingFunction) {
instantiatedOp = handleSortDependingSymbol(sortDependingFunction);
} else if (p_operatorToBeInstantiated instanceof ElementaryUpdate elementaryUpdate) {
instantiatedOp = instantiateElementaryUpdate(elementaryUpdate);
} else if (p_operatorToBeInstantiated instanceof Modality mod) {
instantiatedOp = instantiateModality(mod, jb);
} else if (p_operatorToBeInstantiated instanceof SchemaVariable opAsSV) {
Expand All @@ -305,13 +307,11 @@ private ImmutableArray<QuantifiableVariable> instantiateBoundVariables(Term visi
if (boundVar instanceof SchemaVariable boundSchemaVariable) {
final Term instantiationForBoundSchemaVariable =
(Term) svInst.getInstantiation(boundSchemaVariable);
// instantiation might be null in case of PO generation for taclets
if (instantiationForBoundSchemaVariable != null) {
boundVar = (QuantifiableVariable) instantiationForBoundSchemaVariable.op();
} else {
// this case may happen for PO generation of taclets
boundVar = (QuantifiableVariable) boundSchemaVariable;
varsChanged = true;
}
varsChanged = true;
}
newVars[j] = boundVar;
}
Expand Down Expand Up @@ -389,8 +389,7 @@ private ImmutableArray<TermLabel> instantiateLabels(Term tacletTerm, Operator ne
ImmutableArray<TermLabel> newTermOriginalLabels) {
return TermLabelManager.instantiateLabels(termLabelState, services,
applicationPosInOccurrence, rule, ruleApp, goal, labelHint, tacletTerm,
tb.tf().createTerm(newTermOp, newTermSubs, newTermBoundVars,
newTermOriginalLabels));
tb.tf().createTerm(newTermOp, newTermSubs, newTermBoundVars, newTermOriginalLabels));
}

private Operator handleSortDependingSymbol(SortDependingFunction depOp) {
Expand Down Expand Up @@ -425,21 +424,20 @@ private Term resolveSubst(Term t) {
*/
public Term getTerm() {
if (computedResult == null) {
Object o = null;
Object o;
do {
o = subStack.pop();
} while (o == newMarker);
Term t = (Term) o;
// Term t = (Term) o;
// CollisionDeletingSubstitutionTermApplier substVisit
// = new CollisionDeletingSubstitutionTermApplier();
// t.execPostOrder(substVisit);
// t=substVisit.getTerm();
computedResult = t;
computedResult = (Term) o;
}
return computedResult;
}


public SVInstantiations getSVInstantiations() {
return svInst;
}
Expand All @@ -455,7 +453,7 @@ public void subtreeEntered(Term subtreeRoot) {
/**
* this method is called in execPreOrder and execPostOrder in class Term when leaving the
* subtree rooted in the term subtreeRoot. Default implementation is to do nothing. Subclasses
* can override this method when the visitor behaviour depends on informations bound to
* can override this method when the visitor behaviour depends on information bound to
* subtrees.
*
* @param subtreeRoot root of the subtree which the visitor leaves.
Expand Down

0 comments on commit 56a2b8f

Please sign in to comment.