Skip to content

Commit 573c60e

Browse files
wadoonwadoon
committed
Test for taclet option
* fixed activeTacletOption in InitConfig to forbid multiple choices for the same category * enh Info window to show current taclet options for the active proof * refactor Info window * enh Documentation system: Using now the doc_comments instead of XML files.
1 parent 8e2d966 commit 573c60e

64 files changed

Lines changed: 1022 additions & 992 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.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,6 @@
2727
import de.uka.ilkd.key.rule.BuiltInRule;
2828
import de.uka.ilkd.key.rule.OneStepSimplifier;
2929
import de.uka.ilkd.key.rule.Taclet;
30-
import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder;
3130
import de.uka.ilkd.key.settings.ProofSettings;
3231
import de.uka.ilkd.key.strategy.StrategyProperties;
3332
import de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile;
@@ -817,9 +816,7 @@ protected ImmutableList<TermLabelConfiguration> computeTermLabelConfiguration()
817816
? new ProofSettings(sourceInitConfig.getSettings())
818817
: null;
819818
initConfig.setSettings(clonedSettings);
820-
initConfig.setTaclet2Builder(
821-
(HashMap<Taclet, TacletBuilder<? extends Taclet>>) sourceInitConfig.getTaclet2Builder()
822-
.clone());
819+
initConfig.setTaclet2Builder(new HashMap<>(sourceInitConfig.getTaclet2Builder()));
823820
initConfig.setTaclets(sourceInitConfig.getTaclets());
824821
// Create new ProofEnvironment and initialize it with values from initial one.
825822
ProofEnvironment env = new ProofEnvironment(initConfig);

‎key.core/src/main/antlr4/KeYParser.g4‎

Lines changed: 22 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -90,11 +90,11 @@ one_sort_decl
9090
:
9191
doc=DOC_COMMENT?
9292
(
93-
GENERIC sortIds=simple_ident_dots_comma_list
93+
GENERIC sortIds=simple_ident_dots_comma_list_with_docs
9494
(ONEOF sortOneOf = oneof_sorts)?
9595
(EXTENDS sortExt = extends_sorts)? SEMI
96-
| PROXY sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI
97-
| ABSTRACT? (sortIds=simple_ident_dots_comma_list | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)? SEMI
96+
| PROXY sortIds=simple_ident_dots_comma_list_with_docs (EXTENDS sortExt=extends_sorts)? SEMI
97+
| ABSTRACT? (sortIds=simple_ident_dots_comma_list_with_docs | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)? SEMI
9898
| ALIAS simple_ident_dots EQUALS sortId SEMI
9999
)
100100
;
@@ -116,6 +116,13 @@ simple_ident_dots_comma_list
116116
simple_ident_dots (COMMA simple_ident_dots)*
117117
;
118118

119+
simple_ident_dots_comma_list_with_docs
120+
:
121+
simple_ident_dots_with_docs (COMMA simple_ident_dots_with_docs)*
122+
;
123+
124+
simple_ident_dots_with_docs: DOC_COMMENT? simple_ident_dots;
125+
119126

120127
extends_sorts
121128
:
@@ -140,7 +147,7 @@ prog_var_decls
140147
LBRACE
141148
(
142149
kjt = keyjavatype
143-
var_names = simple_ident_comma_list
150+
var_names = simple_ident_comma_list_with_docs
144151
SEMI
145152
)*
146153
RBRACE
@@ -162,6 +169,10 @@ simple_ident_comma_list
162169
id = simple_ident (COMMA id = simple_ident )*
163170
;
164171

172+
simple_ident_comma_list_with_docs
173+
:
174+
id+=simple_ident_with_doc (COMMA id+=simple_ident_with_doc)*
175+
;
165176

166177
schema_var_decls :
167178
SCHEMAVARIABLES LBRACE
@@ -260,6 +271,7 @@ datatype_decl:
260271
;
261272

262273
datatype_constructor:
274+
doc=DOC_COMMENT?
263275
name=simple_ident
264276
(
265277
LPAREN
@@ -342,7 +354,12 @@ where_to_bind:
342354

343355
ruleset_decls
344356
:
345-
HEURISTICSDECL LBRACE (doc+=DOC_COMMENT? id+=simple_ident SEMI)* RBRACE
357+
HEURISTICSDECL LBRACE (id+=simple_ident_with_doc SEMI)* RBRACE
358+
;
359+
360+
simple_ident_with_doc
361+
:
362+
doc=DOC_COMMENT? id=simple_ident
346363
;
347364

348365
sortId

‎key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,7 @@ public TermLabelVisibilityManagerListener[] getTermLabelVisibilityManagerListene
157157

158158
/**
159159
* Fires the event
160-
* {@link TermLabelVisibilityManagerListener#visibleLabelsChanged( TermLabelVisibilityManagerEvent)}
160+
* {@link TermLabelVisibilityManagerListener#visibleLabelsChanged(TermLabelVisibilityManagerEvent)}
161161
* to all listeners.
162162
*
163163
* @param e The event object.

‎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 = sort.getDocumentation();
765+
var doc = namespaceSet.docs().find(sort);
766766

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

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

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,6 @@ public DocSpace(DocSpace parent) {
2626
this.parent = parent;
2727
}
2828

29-
public DocSpace(@Nullable DocSpace parent, Map<String, String> documentation) {
30-
this(documentation);
31-
this.parent = parent;
32-
}
33-
3429
public @Nullable String find(String key) {
3530
var value = documentation.get(key);
3631
if (value != null)
@@ -64,6 +59,6 @@ public void describe(HasDocumentation entity, @Nullable String doc) {
6459
}
6560

6661
public DocSpace copy() {
67-
return new DocSpace(parent, documentation);
62+
return new DocSpace(documentation);
6863
}
6964
}

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
package de.uka.ilkd.key.logic;
55

66

7-
import java.util.Objects;
87

98
import de.uka.ilkd.key.logic.op.IProgramVariable;
109
import de.uka.ilkd.key.logic.op.ParametricFunctionDecl;
@@ -24,6 +23,7 @@
2423
import org.jspecify.annotations.NullMarked;
2524
import org.jspecify.annotations.Nullable;
2625

26+
2727
@NullMarked
2828
public class NamespaceSet {
2929

@@ -37,7 +37,7 @@ public class NamespaceSet {
3737
private Namespace<ParametricSortDecl> parametricSortNS = new Namespace<>();
3838
private Namespace<ParametricFunctionDecl> parametricFuncNS = new Namespace<>();
3939
private Namespace<Choice> choiceNS = new Namespace<>();
40-
private DocSpace documentation = new DocSpace();
40+
private final DocSpace documentation = new DocSpace();
4141

4242
public NamespaceSet() {
4343
}
@@ -75,7 +75,7 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
7575
this.choiceNS = choiceNS;
7676
this.parametricSortNS = parametricSortNS;
7777
this.parametricFuncNS = parametricFuncNS;
78-
this.documentation = Objects.requireNonNull(documentation);
78+
this.documentation.add(documentation);
7979
}
8080

8181

@@ -302,7 +302,7 @@ public NamespaceSet simplify() {
302302
return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(),
303303
sortAliases.simplify(),
304304
ruleSetNS.simplify(), parametricSortNS.simplify(), parametricFuncNS.simplify(),
305-
choiceNS.simplify(), progVarNS.simplify(), documentation);
305+
choiceNS.simplify(), progVarNS.simplify());
306306
}
307307

308308
public NamespaceSet getCompression() {

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

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -59,12 +59,12 @@ public class OriginTermLabel implements TermLabel {
5959
/**
6060
* Display name for {@link OriginTermLabel}s.
6161
*/
62-
public final static Name NAME = new Name("origin");
62+
public static final Name NAME = new Name("origin");
6363

6464
/**
6565
* @see #getTLChildCount()
6666
*/
67-
public final static int CHILD_COUNT = 2;
67+
public static final int CHILD_COUNT = 2;
6868
public static final Sort[] EMPTY_SORTS = new Sort[0];
6969

7070

@@ -559,9 +559,13 @@ private static SubTermOriginData getSubTermOriginData(final ImmutableArray<JTerm
559559
*
560560
*/
561561
private static class SubTermOriginData {
562-
/** All collected sub-terms */
562+
/**
563+
* All collected sub-terms
564+
*/
563565
public final JTerm[] terms;
564-
/** All collected origins */
566+
/**
567+
* All collected origins
568+
*/
565569
public final Set<Origin> origins;
566570

567571
/**
@@ -775,6 +779,18 @@ public boolean equals(Object obj) {
775779
}
776780
}
777781

782+
@Override
783+
public @Nullable String getDocumentation() {
784+
return """
785+
This label saves a term's origin in the JML specification as well as the origins of all of its subterms and former subterms.
786+
787+
For example, if the file "Example.java" contains the clause "requires R" at line 20, then every JavaDL term that is generated from R will have the origin
788+
"requires @ Example.java @ line 20".
789+
790+
Origin labels are not printed in the sequent view. To see a term's origin, you can mouse over it while holding the ALT button. If you want more detailed information, left click on the term and then on "Show Origin".
791+
""";
792+
}
793+
778794
/**
779795
* A {@code SpecType} is any type of JML specification which gets translated into JavaDL.
780796
*

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

Lines changed: 25 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77

88
import org.key_project.logic.Name;
99

10+
import org.jspecify.annotations.Nullable;
11+
1012
/**
1113
* The Class {@link ParameterlessTermLabel} can be used to define labels without parameters.
1214
*
@@ -56,12 +58,22 @@ public final class ParameterlessTermLabel implements TermLabel {
5658
*/
5759
public static final Name SHORTCUT_EVALUATION_LABEL_NAME = new Name("SC");
5860

61+
public static final String SHORTCUT_EVALUATION_LABEL_DOC =
62+
"""
63+
The term label SC is used to indicate that a logical operator has originally been "shortcut" operator.
64+
65+
For instance, both conjunction operators in JML (i.e., &amp;&amp; and &amp;) are translated to the same function in JavaDL. To differentiate between the two, the translation of &amp;&amp; adds the label SC.
66+
67+
This is relevant for welldefinedness checks.
68+
""";
69+
5970
/**
6071
* Label attached to a term with the logical operator '{@literal ||}' or '{@literal &&}' to
6172
* distinguish from '{@literal |}' or '{@literal &}' respectively.
6273
*/
6374
public static final TermLabel SHORTCUT_EVALUATION_LABEL =
64-
new ParameterlessTermLabel(SHORTCUT_EVALUATION_LABEL_NAME);
75+
new ParameterlessTermLabel(SHORTCUT_EVALUATION_LABEL_NAME,
76+
SHORTCUT_EVALUATION_LABEL_DOC);
6577

6678
/**
6779
* Name of {@link #UNDEFINED_VALUE_LABEL}.
@@ -115,15 +127,22 @@ public final class ParameterlessTermLabel implements TermLabel {
115127
*/
116128
private final Name name;
117129

130+
private final @Nullable String documentation;
131+
118132
/**
119133
* Instantiates a new simple term label.
120134
*
121135
* @param name the name, not <code>null</code> The fixed associated instantiator, may be
122136
* <code>null</code>.
123137
*/
124138
public ParameterlessTermLabel(Name name) {
139+
this(name, null);
140+
}
141+
142+
public ParameterlessTermLabel(Name name, @Nullable String doc) {
125143
assert name != null;
126144
this.name = name;
145+
this.documentation = doc;
127146
}
128147

129148
@Override
@@ -181,4 +200,9 @@ public boolean equals(Object obj) {
181200
public int hashCode() {
182201
return name.hashCode();
183202
}
203+
204+
@Override
205+
public @Nullable String getDocumentation() {
206+
return documentation;
207+
}
184208
}

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77

88
import de.uka.ilkd.key.logic.TermServices;
99

10+
import org.jspecify.annotations.Nullable;
11+
1012
/**
1113
* A factory for creating singleton {@link TermLabel}.
1214
*
@@ -33,6 +35,11 @@ public SingletonLabelFactory(T singletonLabel) {
3335
this.singletonLabel = singletonLabel;
3436
}
3537

38+
@Override
39+
public @Nullable String getDocumentation() {
40+
return singletonLabel.getDocumentation();
41+
}
42+
3643
/**
3744
* {@inheritDoc}
3845
*

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

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +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;
1920
import org.key_project.logic.Name;
2021
import org.key_project.logic.Named;
2122
import org.key_project.logic.TerminalSyntaxElement;
@@ -151,7 +152,8 @@
151152
* @see TermLabelManager
152153
*/
153154
// spotless:on
154-
public interface TermLabel extends Named, /* TODO: Remove */ TerminalSyntaxElement {
155+
public interface TermLabel
156+
extends Named, HasDocumentation, /* TODO: Remove */ TerminalSyntaxElement {
155157

156158
/**
157159
* Retrieves the i-th parameter object of this term label.
@@ -183,4 +185,9 @@ public interface TermLabel extends Named, /* TODO: Remove */ TerminalSyntaxEleme
183185
default boolean isProofRelevant() {
184186
return true;
185187
}
188+
189+
@Override
190+
default String getDocumentationKey() {
191+
return "termlabel/" + name();
192+
}
186193
}

0 commit comments

Comments
 (0)