Skip to content

Commit 2fb102b

Browse files
unp1unp1
authored
Merge pull request #7 from Drodt/severalFixes
Fixes several issues in the new AST term structures
2 parents b3f376f + fc3e614 commit 2fb102b

19 files changed

+100
-98
lines changed

‎key.core/src/main/java/de/uka/ilkd/key/java/Services.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -147,7 +147,6 @@ public Services getOverlay(NamespaceSet namespaces) {
147147
return result;
148148
}
149149

150-
151150
/**
152151
* Returns the TypeConverter associated with this Services object.
153152
*/

‎key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java

Lines changed: 7 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.logic;
55

6-
import java.util.HashMap;
76
import java.util.Map;
87

98
import de.uka.ilkd.key.java.JavaProgramElement;
@@ -23,8 +22,6 @@ public class NamespaceSet {
2322
private Namespace<QuantifiableVariable> varNS = new Namespace<>();
2423
private Namespace<IProgramVariable> progVarNS = new Namespace<>();
2524
// TODO: Operators should not be local to goals
26-
private Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators =
27-
new HashMap<>();
2825
private Namespace<Function> funcNS = new Namespace<>();
2926
private Namespace<RuleSet> ruleSetNS = new Namespace<>();
3027
private Namespace<Sort> sortNS = new Namespace<>();
@@ -34,8 +31,7 @@ public NamespaceSet() {
3431
}
3532

3633
public NamespaceSet(Namespace<QuantifiableVariable> varNS,
37-
Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators,
38-
Namespace<Function> funcNS,
34+
Namespace<Function> funcNS,
3935
Namespace<Sort> sortNS, Namespace<RuleSet> ruleSetNS, Namespace<Choice> choiceNS,
4036
Namespace<IProgramVariable> programVarNS) {
4137
this.varNS = varNS;
@@ -47,21 +43,21 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
4743
}
4844

4945
public NamespaceSet copy() {
50-
return new NamespaceSet(variables().copy(), new HashMap<>(operators()), functions().copy(),
46+
return new NamespaceSet(variables().copy(), functions().copy(),
5147
sorts().copy(),
5248
ruleSets().copy(), choices().copy(), programVariables().copy());
5349
}
5450

5551
public NamespaceSet shallowCopy() {
56-
return new NamespaceSet(variables(), operators(), functions(), sorts(), ruleSets(),
52+
return new NamespaceSet(variables(), functions(), sorts(), ruleSets(),
5753
choices(),
5854
programVariables());
5955
}
6056

6157
// TODO MU: Rename into sth with wrap or similar
6258
public NamespaceSet copyWithParent() {
6359
return new NamespaceSet(new Namespace<>(variables()),
64-
operators(), new Namespace<>(functions()), new Namespace<>(sorts()),
60+
new Namespace<>(functions()), new Namespace<>(sorts()),
6561
new Namespace<>(ruleSets()), new Namespace<>(choices()),
6662
new Namespace<>(programVariables()));
6763
}
@@ -82,15 +78,6 @@ public void setProgramVariables(Namespace<IProgramVariable> progVarNS) {
8278
this.progVarNS = progVarNS;
8379
}
8480

85-
public Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators() {
86-
return operators;
87-
}
88-
89-
public void setOperators(
90-
Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators) {
91-
this.operators = operators;
92-
}
93-
9481
public Namespace<Function> functions() {
9582
return funcNS;
9683
}
@@ -218,12 +205,12 @@ public boolean isEmpty() {
218205

219206
// create a namespace
220207
public NamespaceSet simplify() {
221-
return new NamespaceSet(varNS.simplify(), operators, funcNS.simplify(), sortNS.simplify(),
208+
return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(),
222209
ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify());
223210
}
224211

225212
public NamespaceSet getCompression() {
226-
return new NamespaceSet(varNS.compress(), operators, funcNS.compress(), sortNS.compress(),
213+
return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(),
227214
ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress());
228215
}
229216

@@ -234,7 +221,7 @@ public void flushToParent() {
234221
}
235222

236223
public NamespaceSet getParent() {
237-
return new NamespaceSet(varNS.parent(), operators, funcNS.parent(), sortNS.parent(),
224+
return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(),
238225
ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent());
239226
}
240227

‎key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java

Lines changed: 3 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -423,12 +423,12 @@ public Term func(Function f, Term[] s, ImmutableArray<QuantifiableVariable> boun
423423
// }
424424

425425
public Term prog(Modality.JavaModalityKind modKind, JavaBlock jb, Term t) {
426-
return tf.createTerm(modality(modKind, jb), new Term[] { t }, null, jb);
426+
return tf.createTerm(Modality.modality(modKind, jb), new Term[] { t }, null, jb);
427427
}
428428

429429
public Term prog(Modality.JavaModalityKind modKind, JavaBlock jb, Term t,
430430
ImmutableArray<TermLabel> labels) {
431-
return tf.createTerm(modality(modKind, jb), new Term[] { t }, null, jb, labels);
431+
return tf.createTerm(Modality.modality(modKind, jb), new Term[] { t }, null, jb, labels);
432432
}
433433

434434
public Term box(JavaBlock jb, Term t) {
@@ -439,17 +439,6 @@ public Term dia(JavaBlock jb, Term t) {
439439
return prog(Modality.JavaModalityKind.DIA, jb, t);
440440
}
441441

442-
// TODO: move?
443-
public Modality modality(Modality.JavaModalityKind kind, JavaBlock jb) {
444-
var pair = new Pair<>(kind, jb.program());
445-
Modality mod = services.getNamespaces().operators().get(pair);
446-
if (mod == null) {
447-
mod = new Modality(jb, kind);
448-
services.getNamespaces().operators().put(pair, mod);
449-
}
450-
return mod;
451-
}
452-
453442
public Term ife(Term cond, Term _then, Term _else) {
454443
return tf.createTerm(IfThenElse.IF_THEN_ELSE, cond, _then, _else);
455444
}
@@ -1706,7 +1695,7 @@ public Term addLabel(Term term, ImmutableArray<TermLabel> labels) {
17061695

17071696
for (TermLabel newLabel : labels) {
17081697
for (TermLabel oldLabel : newLabelList) {
1709-
if (oldLabel.getClass().equals(newLabel.getClass())) {
1698+
if (oldLabel.getClass() == newLabel.getClass()) {
17101699
newLabelList.remove(oldLabel);
17111700
break;
17121701
}

‎key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java

Lines changed: 19 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -362,6 +362,10 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
362362
return true;
363363
}
364364

365+
if (t0.sort() != t1.sort() || t0.arity() != t1.arity()) {
366+
return false;
367+
}
368+
365369
final Operator op0 = t0.op();
366370

367371
if (op0 instanceof QuantifiableVariable) {
@@ -374,24 +378,21 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
374378
if (mod0.kind() != mod1.kind()) {
375379
return false;
376380
}
377-
nat = handleJava(t0, t1, nat);
381+
nat = handleJava(mod0.program(), mod1.program(), nat);
378382
if (nat == FAILED) {
379383
return false;
380384
}
381385
} else if (!(op0 instanceof ProgramVariable) && op0 != op1) {
382386
return false;
383387
}
384388

385-
if (t0.sort() != t1.sort() || t0.arity() != t1.arity()) {
386-
return false;
387-
}
388-
389-
if (!(t0.op() instanceof SchemaVariable) && t0.op() instanceof ProgramVariable) {
390-
if (!(t1.op() instanceof ProgramVariable)) {
391-
return false;
392-
}
393-
nat = checkNat(nat);
394-
if (!((ProgramVariable) t0.op()).equalsModRenaming((ProgramVariable) t1.op(), nat)) {
389+
if (!(op0 instanceof SchemaVariable) && op0 instanceof ProgramVariable pv0) {
390+
if (op1 instanceof ProgramVariable pv1) {
391+
nat = checkNat(nat);
392+
if (!pv0.equalsModRenaming(pv1, nat)) {
393+
return false;
394+
}
395+
} else {
395396
return false;
396397
}
397398
}
@@ -413,15 +414,13 @@ && compareBoundVariables((QuantifiableVariable) t0.op(),
413414
*/
414415
private static final NameAbstractionTable FAILED = new NameAbstractionTable();
415416

416-
private static NameAbstractionTable handleJava(Term t0, Term t1, NameAbstractionTable nat) {
417-
418-
if (!t0.javaBlock().isEmpty() || !t1.javaBlock().isEmpty()) {
417+
private static NameAbstractionTable handleJava(JavaBlock jb0, JavaBlock jb1, NameAbstractionTable nat) {
418+
if (!jb0.isEmpty() || !jb1.isEmpty()) {
419419
nat = checkNat(nat);
420-
if (!t0.javaBlock().equalsModRenaming(t1.javaBlock(), nat)) {
420+
if (!jb0.equalsModRenaming(jb1, nat)) {
421421
return FAILED;
422422
}
423423
}
424-
425424
return nat;
426425
}
427426

@@ -484,7 +483,9 @@ public boolean equals(Object o) {
484483
final TermImpl t = (TermImpl) o;
485484

486485
return op.equals(t.op) && t.hasLabels() == hasLabels() && subs.equals(t.subs)
487-
&& boundVars.equals(t.boundVars) && javaBlock().equals(t.javaBlock());
486+
&& boundVars.equals(t.boundVars)
487+
// TODO (DD): below is no longer necessary
488+
&& javaBlock().equals(t.javaBlock());
488489
}
489490

490491
@Override
@@ -709,7 +710,7 @@ public ImmutableArray<TermLabel> getLabels() {
709710
public boolean containsJavaBlockRecursive() {
710711
if (containsJavaBlockRecursive == ThreeValuedTruth.UNKNOWN) {
711712
ThreeValuedTruth result = ThreeValuedTruth.FALSE;
712-
if (javaBlock() != null && !javaBlock().isEmpty()) {
713+
if (!javaBlock().isEmpty()) {
713714
result = ThreeValuedTruth.TRUE;
714715
} else {
715716
for (int i = 0, arity = subs.size(); i < arity; i++) {

‎key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java

Lines changed: 26 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
import java.util.HashMap;
77
import java.util.Map;
88

9+
import de.uka.ilkd.key.java.JavaProgramElement;
910
import de.uka.ilkd.key.ldt.JavaDLTheory;
1011
import de.uka.ilkd.key.logic.JavaBlock;
1112
import de.uka.ilkd.key.logic.Term;
@@ -15,12 +16,37 @@
1516

1617
import org.key_project.logic.Name;
1718
import org.key_project.logic.Program;
19+
import org.key_project.util.collection.Pair;
1820

1921
/**
2022
* This class is used to represent a dynamic logic modality like diamond and box (but also
2123
* extensions of DL like preserves and throughout are possible in the future).
2224
*/
2325
public class Modality extends org.key_project.logic.op.Modality<Sort> implements Operator {
26+
/*
27+
keeps track of created modalities
28+
*/
29+
private static Map<Pair<JavaModalityKind, JavaProgramElement>, Modality> operators =
30+
new HashMap<>();
31+
32+
33+
/**
34+
* Returns the knownm modalities
35+
*/
36+
public static Map<Pair<JavaModalityKind, JavaProgramElement>, Modality> operators() {
37+
return operators;
38+
}
39+
40+
public static Modality modality(Modality.JavaModalityKind kind, JavaBlock jb) {
41+
var pair = new Pair<>(kind, jb.program());
42+
Modality mod = Modality.operators().get(pair);
43+
if (mod == null) {
44+
mod = new Modality(jb, kind);
45+
Modality.operators().put(pair, mod);
46+
}
47+
return mod;
48+
}
49+
2450
/**
2551
* creates a modal operator with the given name
2652
*
@@ -142,7 +168,6 @@ public static class JavaModalityKind extends Kind implements SVSubstitute {
142168
*/
143169
public static final JavaModalityKind TOUT_TRANSACTION =
144170
new JavaModalityKind(new Name("throughout_transaction"));
145-
public static final JavaModalityKind MOD_SV = new JavaModalityKind(new Name("mod_sv"));
146171

147172
public JavaModalityKind(Name name) {
148173
super(name);

‎key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1151,9 +1151,10 @@ public Object visitModality_term(KeYParser.Modality_termContext ctx) {
11511151
* "No schema elements allowed outside taclet declarations (" + sjb.opName + ")"); }
11521152
*/
11531153
Modality.JavaModalityKind kind = (Modality.JavaModalityKind) schemaVariables().lookup(new Name(sjb.opName));
1154-
op = getServices().getTermBuilder().modality(kind, sjb.javaBlock);
1154+
op = Modality.modality(kind, sjb.javaBlock);
11551155
} else {
1156-
op = getServices().getTermBuilder().modality(Modality.JavaModalityKind.getKind(sjb.opName), sjb.javaBlock);
1156+
Modality.JavaModalityKind kind = Modality.JavaModalityKind.getKind(sjb.opName);
1157+
op = Modality.modality(kind, sjb.javaBlock);
11571158
}
11581159
if (op == null) {
11591160
semanticError(ctx, "Unknown modal operator: " + sjb.opName);

‎key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java

Lines changed: 3 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -5,24 +5,19 @@
55

66
import java.io.IOException;
77
import java.io.Reader;
8-
import java.util.Map;
98

10-
import de.uka.ilkd.key.java.JavaProgramElement;
119
import de.uka.ilkd.key.java.Services;
1210
import de.uka.ilkd.key.logic.Namespace;
1311
import de.uka.ilkd.key.logic.NamespaceSet;
1412
import de.uka.ilkd.key.logic.Sequent;
1513
import de.uka.ilkd.key.logic.Term;
1614
import de.uka.ilkd.key.logic.op.Function;
1715
import de.uka.ilkd.key.logic.op.IProgramVariable;
18-
import de.uka.ilkd.key.logic.op.Modality;
1916
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
2017
import de.uka.ilkd.key.logic.sort.Sort;
2118
import de.uka.ilkd.key.nparser.KeyIO;
2219
import de.uka.ilkd.key.pp.AbbrevMap;
2320

24-
import org.key_project.util.collection.Pair;
25-
2621
import org.antlr.v4.runtime.CharStreams;
2722
import org.antlr.v4.runtime.RecognitionException;
2823

@@ -42,18 +37,16 @@ public final class DefaultTermParser {
4237
* ensures, that the term has the specified sort.
4338
*
4439
* @param sort The expected sort of the term.
45-
* @param op_ns
4640
* @return The parsed term of the specified sort.
4741
* @throws ParserException The method throws a ParserException, if the input could not be parsed
48-
* correctly or the term has an invalid sort.
42+
* correctly or the term has an invalid sort.
4943
*/
5044
public Term parse(Reader in, Sort sort, Services services,
5145
Namespace<QuantifiableVariable> var_ns,
52-
Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> op_ns,
53-
Namespace<Function> func_ns,
46+
Namespace<Function> func_ns,
5447
Namespace<Sort> sort_ns, Namespace<IProgramVariable> progVar_ns, AbbrevMap scm)
5548
throws ParserException {
56-
return parse(in, sort, services, new NamespaceSet(var_ns, op_ns, func_ns, sort_ns,
49+
return parse(in, sort, services, new NamespaceSet(var_ns, func_ns, sort_ns,
5750
new Namespace<>(), new Namespace<>(), progVar_ns), scm);
5851
}
5952

‎key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1667,7 +1667,8 @@ public void printModalityTerm(String left, JavaBlock jb, String right, Term phi,
16671667
for (int i = 0; i < phi.arity(); i++) {
16681668
ta[i] = phi.sub(i);
16691669
}
1670-
Modality m = services.getTermBuilder().modality(mod.kind(), mod.program());
1670+
JavaBlock jb1 = mod.program();
1671+
Modality m = Modality.modality(mod.kind(), jb1);
16711672
Term term = services.getTermFactory().createTerm(m, ta,
16721673
phi.boundVars(), phi.javaBlock());
16731674
notationInfo.getNotation(m).print(term, this);

‎key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -468,11 +468,10 @@ private GoalsConfigurator setUpGoalConfigurator(final StatementBlock block,
468468
final KeYJavaType kjt = getCalleeKeYJavaType();
469469
final TypeRef typeRef = new TypeRef(new ProgramElementName(kjt.getName()), 0, selfVar, kjt);
470470
final ExecutionContext ec = new ExecutionContext(typeRef, getProgramMethod(), selfVar);
471-
// TODO (DD): HACK
472471
final Instantiation inst =
473472
new Instantiation(tb.skip(), tb.tt(),
474-
new Modality(JavaBlock.createJavaBlock(new StatementBlock()),
475-
contract.getModalityKind()),
473+
Modality.modality(contract.getModalityKind(),
474+
JavaBlock.createJavaBlock(new StatementBlock())),
476475
selfTerm, block, ec);
477476
return new GoalsConfigurator(null, new TermLabelState(), inst,
478477
contract.getAuxiliaryContract().getLabels(), variables, null, services, null);

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -940,7 +940,7 @@ public static Term parseTerm(String value, Proof proof, Namespace<QuantifiableVa
940940
Namespace<IProgramVariable> progVarNS, Namespace<Function> functNS) {
941941
try {
942942
return new DefaultTermParser().parse(new StringReader(value), null, proof.getServices(),
943-
varNS, proof.getNamespaces().operators(), functNS, proof.getNamespaces().sorts(),
943+
varNS, functNS, proof.getNamespaces().sorts(),
944944
progVarNS, new AbbrevMap());
945945
} catch (ParserException e) {
946946
throw new RuntimeException(

0 commit comments

Comments
 (0)