Skip to content

Commit 4c7db14

Browse files
wadoonwadoon
committed
get rid of getOrigin() using MetaSpace
* overhaul ContextMenu of InfoTree and clean Extension API
1 parent 8535026 commit 4c7db14

60 files changed

Lines changed: 379 additions & 546 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,6 @@ public Name name() {
3838
return NAME;
3939
}
4040

41-
@Override
42-
public @Nullable String getOrigin() {
43-
return super.getOrigin();
44-
}
4541

4642
protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier {
4743
public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp<?> ruleApp) {

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -762,7 +762,7 @@ public DLEmbeddedExpression convert(EscapeExpression e) {
762762
sortName, e.getStartPosition()));
763763
}
764764

765-
var doc = namespaceSet.docs().find(sort);
765+
var doc = namespaceSet.docs().findDocumentation(sort);
766766

767767
if (doc == null) {
768768
throw new ConvertException(

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

Lines changed: 0 additions & 64 deletions
This file was deleted.

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

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@
1616
import org.key_project.util.collection.ImmutableSet;
1717

1818
import org.jspecify.annotations.NonNull;
19-
import org.jspecify.annotations.Nullable;
2019

2120
/**
2221
* In contrast to the distinction of formulas and terms as made by most of the inductive definitions
@@ -118,9 +117,4 @@ public interface JTerm
118117
* non-empty {@link JavaBlock}, {@code false} no {@link JavaBlock} available.
119118
*/
120119
boolean containsJavaBlockRecursive();
121-
122-
/**
123-
* Returns a human-readable source of this term. For example the filename with line and offset.
124-
*/
125-
default @Nullable String getOrigin() { return null; }
126120
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ public class LabeledTermImpl extends TermImpl {
5252
public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
5353
ImmutableArray<QuantifiableVariable> boundVars,
5454
ImmutableArray<TermLabel> labels, String origin) {
55-
super(op, subs, boundVars, origin);
55+
super(op, subs, boundVars);
5656
assert labels != null : "Term labels must not be null";
5757
assert !labels.isEmpty() : "There must be at least one term label";
5858
this.labels = labels;
@@ -69,7 +69,7 @@ public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
6969
public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
7070
ImmutableArray<QuantifiableVariable> boundVars,
7171
ImmutableArray<TermLabel> labels) {
72-
super(op, subs, boundVars, "");
72+
super(op, subs, boundVars);
7373
assert labels != null : "Term labels must not be null";
7474
assert !labels.isEmpty() : "There must be at least one term label";
7575
this.labels = labels;

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

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.logic;
5+
6+
import java.util.Map;
7+
import java.util.TreeMap;
8+
9+
import org.key_project.logic.HasMeta;
10+
11+
import org.jspecify.annotations.NullMarked;
12+
import org.jspecify.annotations.Nullable;
13+
14+
/// MetaSpace is a namespace for storing additional information
15+
///
16+
/// @author weigl
17+
@NullMarked
18+
public class MetaSpace {
19+
public static final String SPACE_PREFIX_DOC = "doc/";
20+
public static final String SPACE_PREFIX_ORIGIN = "origin/";
21+
22+
private @Nullable MetaSpace parent;
23+
private final Map<String, Object> metadata = new TreeMap<>();
24+
25+
public MetaSpace() {
26+
}
27+
28+
public MetaSpace(Map<String, Object> documentation) {
29+
this.metadata.putAll(documentation);
30+
}
31+
32+
public MetaSpace(MetaSpace parent) {
33+
this.parent = parent;
34+
}
35+
36+
private @Nullable Object findMetadata(String key) {
37+
return metadata.get(key);
38+
}
39+
40+
public @Nullable String findDocumentation(HasMeta entity) {
41+
if (entity.getDocumentation() != null) {
42+
return entity.getDocumentation();
43+
}
44+
return (String) findMetadata(SPACE_PREFIX_DOC + entity.getMetaKey());
45+
}
46+
47+
/**
48+
* Returns a human-readable source of this term. For example the filename with line and offset.
49+
*/
50+
public @Nullable String findOrigin(HasMeta entity) {
51+
return (String) findMetadata(SPACE_PREFIX_ORIGIN + entity.getMetaKey());
52+
}
53+
54+
public void add(MetaSpace space) {
55+
this.metadata.putAll(space.metadata);
56+
}
57+
58+
public @Nullable MetaSpace parent() {
59+
return parent;
60+
}
61+
62+
public void setDocumentation(HasMeta entity, @Nullable String doc) {
63+
setMetadata(SPACE_PREFIX_DOC, entity, doc);
64+
}
65+
66+
public void setOrigin(HasMeta entity, @Nullable String origin) {
67+
setMetadata(SPACE_PREFIX_ORIGIN, entity, origin);
68+
}
69+
70+
private void setMetadata(String prefix, HasMeta entity, @Nullable Object val) {
71+
var key = prefix + entity.getMetaKey();
72+
if (val == null) {
73+
metadata.remove(key);
74+
} else {
75+
metadata.put(key, val);
76+
}
77+
}
78+
79+
80+
public MetaSpace copy() {
81+
return new MetaSpace(metadata);
82+
}
83+
}

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

Lines changed: 10 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@
1919
import org.key_project.logic.sort.Sort;
2020
import org.key_project.prover.rules.RuleSet;
2121

22-
import org.jspecify.annotations.NonNull;
2322
import org.jspecify.annotations.NullMarked;
2423
import org.jspecify.annotations.Nullable;
2524

@@ -33,11 +32,11 @@ public class NamespaceSet {
3332
private Namespace<Function> funcNS = new Namespace<>();
3433
private Namespace<RuleSet> ruleSetNS = new Namespace<>();
3534
private Namespace<Sort> sortNS = new Namespace<>();
36-
private Namespace<@NonNull SortAlias> sortAliases = new Namespace<>();
35+
private Namespace<SortAlias> sortAliases = new Namespace<>();
3736
private Namespace<ParametricSortDecl> parametricSortNS = new Namespace<>();
3837
private Namespace<ParametricFunctionDecl> parametricFuncNS = new Namespace<>();
3938
private Namespace<Choice> choiceNS = new Namespace<>();
40-
private final DocSpace documentation = new DocSpace();
39+
private MetaSpace documentation = new MetaSpace();
4140

4241
public NamespaceSet() {
4342
}
@@ -53,7 +52,7 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
5352
Namespace<IProgramVariable> programVarNS) {
5453
this(varNS, funcNS, sortNS, sortAliases, ruleSetNS,
5554
parametricSortNS, parametricFuncNS,
56-
choiceNS, programVarNS, new DocSpace());
55+
choiceNS, programVarNS, new MetaSpace());
5756
}
5857

5958
public NamespaceSet(Namespace<QuantifiableVariable> varNS,
@@ -65,7 +64,7 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
6564
Namespace<ParametricFunctionDecl> parametricFuncNS,
6665
Namespace<Choice> choiceNS,
6766
Namespace<IProgramVariable> programVarNS,
68-
DocSpace documentation) {
67+
MetaSpace documentation) {
6968
this.varNS = varNS;
7069
this.progVarNS = programVarNS;
7170
this.funcNS = funcNS;
@@ -75,7 +74,7 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
7574
this.choiceNS = choiceNS;
7675
this.parametricSortNS = parametricSortNS;
7776
this.parametricFuncNS = parametricFuncNS;
78-
this.documentation.add(documentation);
77+
this.documentation = documentation;
7978
}
8079

8180

@@ -91,7 +90,7 @@ public NamespaceSet shallowCopy() {
9190
return new NamespaceSet(variables(), functions(), sorts(), sortAliases(), ruleSets(),
9291
parametricSorts(),
9392
parametricFunctions(),
94-
choices(), programVariables(), new DocSpace(documentation));
93+
choices(), programVariables(), new MetaSpace(documentation));
9594
}
9695

9796
// TODO MU: Rename into sth with wrap or similar
@@ -101,7 +100,7 @@ public NamespaceSet copyWithParent() {
101100
new Namespace<>(ruleSets()), new Namespace<>(parametricSorts()),
102101
new Namespace<>(parametricFunctions()), new Namespace<>(choices()),
103102
new Namespace<>(programVariables()),
104-
new DocSpace(documentation));
103+
new MetaSpace(documentation));
105104
}
106105

107106
public Namespace<QuantifiableVariable> variables() {
@@ -144,11 +143,11 @@ public void setSorts(Namespace<Sort> sortNS) {
144143
this.sortNS = sortNS;
145144
}
146145

147-
public Namespace<@NonNull SortAlias> sortAliases() {
146+
public Namespace<SortAlias> sortAliases() {
148147
return sortAliases;
149148
}
150149

151-
public void setSortAliases(Namespace<@NonNull SortAlias> sortAliases) {
150+
public void setSortAliases(Namespace<SortAlias> sortAliases) {
152151
this.sortAliases = sortAliases;
153152
}
154153

@@ -325,7 +324,7 @@ public NamespaceSet getParent() {
325324
choiceNS.parent(), progVarNS.parent(), documentation.parent());
326325
}
327326

328-
public DocSpace docs() {
327+
public MetaSpace docs() {
329328
return documentation;
330329
}
331330
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ private JTerm doCreateTerm(Operator op, ImmutableArray<JTerm> subs,
121121

122122
final TermImpl newTerm =
123123
(labels == null || labels.isEmpty()
124-
? new TermImpl(op, subs, boundVars, origin)
124+
? new TermImpl(op, subs, boundVars)
125125
: new LabeledTermImpl(op, subs, boundVars, labels, origin));
126126
// Check if caching is possible. It is not possible if a non-empty JavaBlock is available
127127
// in the term or in one of its children because the meta information like PositionInfos

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

Lines changed: 1 addition & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@
2121
import org.key_project.util.collection.ImmutableSet;
2222

2323
import org.jspecify.annotations.NonNull;
24-
import org.jspecify.annotations.Nullable;
2524

2625

2726
/**
@@ -81,10 +80,6 @@ private enum ThreeValuedTruth {
8180
*/
8281
private ThreeValuedTruth containsJavaBlockRecursive = ThreeValuedTruth.UNKNOWN;
8382

84-
// -------------------------------------------------------------------------
85-
// constructors
86-
// -------------------------------------------------------------------------
87-
8883
/**
8984
* Constructs a term for the given operator, with the given sub terms, bounded variables and (if
9085
* applicable) the code block on this term.
@@ -95,37 +90,14 @@ private enum ThreeValuedTruth {
9590
* @param boundVars the bounded variables (if applicable), e.g., for quantifiers
9691
*/
9792
public TermImpl(Operator op, ImmutableArray<JTerm> subs,
98-
ImmutableArray<QuantifiableVariable> boundVars,
99-
String origin) {
93+
ImmutableArray<QuantifiableVariable> boundVars) {
10094
assert op != null;
10195
assert subs != null;
10296
this.op = op;
10397
this.subs = subs.isEmpty() ? EMPTY_TERM_LIST : subs;
10498
this.boundVars = boundVars == null ? EMPTY_VAR_LIST : boundVars;
105-
this.origin = origin;
10699
}
107100

108-
TermImpl(Operator op, ImmutableArray<JTerm> subs,
109-
ImmutableArray<QuantifiableVariable> boundVars) {
110-
this(op, subs, boundVars, "");
111-
}
112-
113-
/**
114-
* For which feature is this information needed?
115-
* What is the difference from {@link de.uka.ilkd.key.logic.label.OriginTermLabel}?
116-
*/
117-
private final String origin;
118-
119-
@Override
120-
public @Nullable String getOrigin() {
121-
return origin;
122-
}
123-
124-
// -------------------------------------------------------------------------
125-
// internal methods
126-
// -------------------------------------------------------------------------
127-
128-
129101
private ImmutableSet<QuantifiableVariable> determineFreeVars() {
130102
ImmutableSet<QuantifiableVariable> localFreeVars =
131103
DefaultImmutableSet.nil();

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@
1616
import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope;
1717
import de.uka.ilkd.key.rule.label.TermLabelUpdate;
1818

19-
import org.key_project.logic.HasDocumentation;
19+
import org.key_project.logic.HasMeta;
2020
import org.key_project.logic.Name;
2121
import org.key_project.logic.Named;
2222
import org.key_project.logic.TerminalSyntaxElement;
@@ -153,7 +153,7 @@
153153
*/
154154
// spotless:on
155155
public interface TermLabel
156-
extends Named, HasDocumentation, /* TODO: Remove */ TerminalSyntaxElement {
156+
extends Named, HasMeta, /* TODO: Remove */ TerminalSyntaxElement {
157157

158158
/**
159159
* Retrieves the i-th parameter object of this term label.
@@ -187,7 +187,7 @@ default boolean isProofRelevant() {
187187
}
188188

189189
@Override
190-
default String getDocumentationKey() {
190+
default String getMetaKey() {
191191
return "termlabel/" + name();
192192
}
193193
}

0 commit comments

Comments
 (0)