Skip to content

Commit e53d245

Browse files
wadoonwadoon
authored
small fixes to datatype handling (#3661)
2 parents bb8f016 + b425891 commit e53d245

File tree

10 files changed

+99
-36
lines changed

10 files changed

+99
-36
lines changed

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

Lines changed: 19 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,10 @@
1717
import org.key_project.logic.Name;
1818
import org.key_project.logic.Namespace;
1919
import org.key_project.logic.op.Function;
20+
import org.key_project.logic.op.SortedOperator;
2021
import org.key_project.logic.sort.Sort;
2122
import org.key_project.util.collection.ImmutableArray;
23+
import org.key_project.util.collection.ImmutableList;
2224

2325

2426
/**
@@ -65,11 +67,25 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
6567
Sort argSort = accept(constructorContext.sortId(i));
6668
args[i] = argSort;
6769
var argName = argNames.get(i).getText();
68-
var alreadyDefinedFn = dtNamespace.lookup(argName);
70+
SortedOperator alreadyDefinedFn = dtNamespace.lookup(argName);
71+
if (alreadyDefinedFn == null) {
72+
alreadyDefinedFn = namespaces().functions().lookup(argName);
73+
}
74+
if (alreadyDefinedFn == null) {
75+
alreadyDefinedFn = namespaces().programVariables().lookup(argName);
76+
}
6977
if (alreadyDefinedFn != null
7078
&& (!alreadyDefinedFn.sort().equals(argSort)
71-
|| !alreadyDefinedFn.argSort(0).equals(sort))) {
72-
throw new RuntimeException("Name already in namespace: " + argName);
79+
|| !alreadyDefinedFn.argSorts().equals(ImmutableList.of(sort)))) {
80+
// The condition checks whether there is already a function with the same name
81+
// but different signature. This is necessarily true if there is a globally
82+
// defined function
83+
// of the same name and may or may not be true if there is another constructor
84+
// argument of the
85+
// same name.
86+
semanticError(argNames.get(i), "Name already in namespace: %s" +
87+
". Identifiers in datatype definitions must be unique (also wrt. global functions).",
88+
argName);
7389
}
7490
Function fn = new JFunction(new Name(argName), argSort, new Sort[] { sort }, null,
7591
false, false);

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

Lines changed: 21 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
263263
for (int i = 0; i < constructor.sortId().size(); i++) {
264264
var argName = constructor.argName.get(i).getText();
265265

266-
var tbDeconstructor = createDeconstructorTaclet(constructor, argName, i);
266+
var tbDeconstructor = createDeconstructorTaclet(constructor, argName, i, dtSort);
267267
registerTaclet(ctx, tbDeconstructor);
268268

269269
var tbDeconsEq = createDeconstructorEQTaclet(constructor, argName, i, dtSort);
@@ -275,12 +275,15 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
275275
}
276276

277277
private TacletBuilder<? extends Taclet> createDeconstructorTaclet(
278-
KeYParser.Datatype_constructorContext constructor, String argName, int argIndex) {
278+
KeYParser.Datatype_constructorContext constructor, String argName, int argIndex,
279+
Sort dtSort) {
279280
var tacletBuilder = new RewriteTacletBuilder<>();
280281
tacletBuilder
281-
.setName(new Name(String.format("%s_Dec_%s", argName, constructor.name.getText())));
282+
.setName(new Name(String.format("DT_%s#Dec_%s#%s", dtSort.name(), argName,
283+
constructor.name.getText())));
282284
tacletBuilder.setDisplayName(
283-
String.format("%s_Deconstruct_%s", argName, constructor.name.getText()));
285+
String.format("DT %s Deconstructor %s (for %s)", dtSort.name(), argName,
286+
constructor.name.getText()));
284287

285288
var schemaVariables = new JOperatorSV[constructor.argName.size()];
286289
var args = new JTerm[constructor.argName.size()];
@@ -305,6 +308,7 @@ private TacletBuilder<? extends Taclet> createDeconstructorTaclet(
305308
new RewriteTacletGoalTemplate(tb.var(schemaVariables[argIndex])));
306309
tacletBuilder.setApplicationRestriction(
307310
new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL));
311+
tacletBuilder.addRuleSet(ruleSets().lookup(new Name("simplify")));
308312

309313
return tacletBuilder;
310314
}
@@ -314,9 +318,11 @@ private TacletBuilder<? extends Taclet> createDeconstructorEQTaclet(
314318
Sort dtSort) {
315319
var tacletBuilder = new RewriteTacletBuilder<>();
316320
tacletBuilder.setName(
317-
new Name(String.format("%s_DecEQ_%s", argName, constructor.name.getText())));
321+
new Name(String.format("DT_%s#Dec_%s#%s#EQ", dtSort.name(), argName,
322+
constructor.name.getText())));
318323
tacletBuilder.setDisplayName(
319-
String.format("%s_DeconstructEQ_%s", argName, constructor.name.getText()));
324+
String.format("DT %s Deconstructor %s (for %s)", dtSort.name(), argName,
325+
constructor.name.getText()));
320326

321327
var schemaVariables = new JOperatorSV[constructor.argName.size()];
322328
var args = new JTerm[constructor.argName.size()];
@@ -342,10 +348,11 @@ private TacletBuilder<? extends Taclet> createDeconstructorEQTaclet(
342348
tacletBuilder.setFind(tb.func(function, tb.var(x)));
343349
tacletBuilder.setIfSequent(JavaDLSequentKit.createAnteSequent(
344350
ImmutableSLList
345-
.singleton(new SequentFormula(tb.equals(tb.var(x), tb.func(consFn, args))))));
351+
.singleton(new SequentFormula(tb.equals(tb.func(consFn, args), tb.var(x))))));
346352
tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(tb.var(res)));
347353
tacletBuilder.setApplicationRestriction(
348354
new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL));
355+
tacletBuilder.addRuleSet(ruleSets().lookup(new Name("simplify")));
349356

350357
return tacletBuilder;
351358
}
@@ -354,7 +361,6 @@ private TacletBuilder<? extends Taclet> createDeconstructorEQTaclet(
354361
private TacletBuilder<? extends Taclet> createInductionTaclet(
355362
KeYParser.Datatype_declContext ctx) {
356363
var tacletBuilder = new NoFindTacletBuilder();
357-
tacletBuilder.setName(new Name(String.format("%s_Ind", ctx.name.getText())));
358364
final var sort = sorts().lookup(ctx.name.getText());
359365
var phi = declareSchemaVariable(ctx, "phi", JavaDLTheory.FORMULA, true,
360366
false, false, new SchemaVariableModifierSet.FormulaSV());
@@ -376,7 +382,8 @@ private TacletBuilder<? extends Taclet> createInductionTaclet(
376382
cases.add(useCase);
377383

378384
cases.forEach(tacletBuilder::addTacletGoalTemplate);
379-
tacletBuilder.setDisplayName("Induction_for_" + sort.name());
385+
tacletBuilder.setName(new Name(String.format("DT_%s_Induction", sort.name())));
386+
tacletBuilder.setDisplayName(String.format("DT %s Induction", sort.name()));
380387
return tacletBuilder;
381388
}
382389

@@ -395,7 +402,6 @@ private TacletGoalTemplate createGoalDtConstructor(KeYParser.Datatype_constructo
395402
private TacletBuilder<NoFindTaclet> createAxiomTaclet(
396403
KeYParser.Datatype_declContext ctx) {
397404
var tacletBuilder = new NoFindTacletBuilder();
398-
tacletBuilder.setName(new Name(String.format("%s_Axiom", ctx.name.getText())));
399405
final var sort = sorts().lookup(ctx.name.getText());
400406
var phi = declareSchemaVariable(ctx, "phi", JavaDLTheory.FORMULA, true,
401407
false, false, new SchemaVariableModifierSet.FormulaSV());
@@ -417,7 +423,8 @@ private TacletBuilder<NoFindTaclet> createAxiomTaclet(
417423
ImmutableSLList.nil());
418424
tacletBuilder.addTacletGoalTemplate(goal);
419425

420-
tacletBuilder.setDisplayName("Axiom_for_" + sort.name());
426+
tacletBuilder.setName(new Name(String.format("DT_%s_Axiom", sort.name())));
427+
tacletBuilder.setDisplayName(String.format("DT %s Axiom", sort.name()));
421428
return tacletBuilder;
422429
}
423430

@@ -452,7 +459,7 @@ private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext cont
452459
}
453460

454461
if (ind.isEmpty()) {
455-
return tb.all(qvs, tb.func(fn, args));
462+
return tb.all(qvs, tb.subst(qvX, tb.func(fn, args), phi));
456463
} else {
457464
var base = tb.and(ind);
458465
return tb.all(qvs, tb.imp(base, tb.subst(qvX, tb.func(fn, args), phi)));
@@ -482,8 +489,8 @@ private RewriteTacletBuilder<RewriteTaclet> createConstructorSplit(
482489
new ApplicationRestriction(ApplicationRestriction.SAME_UPDATE_LEVEL));
483490
final var sort = sorts().lookup(ctx.name.getText());
484491

485-
b.setName(new Name(sort.name() + "_ctor_split"));
486-
b.setDisplayName("case distinction of " + sort.name());
492+
b.setName(new Name("DT_" + sort.name() + "_ctor_split"));
493+
b.setDisplayName(String.format("DT %s case distinction ", sort.name()));
487494

488495
var phi = declareSchemaVariable(ctx, "var", sort,
489496
false, false, false,

‎key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ public void addJustification(Rule r, RuleJustification j) {
2929
for (RuleKey key : rule2Justification.keySet()) {
3030
if (key.equals(ruleKey) && r != key.r) {
3131
throw new IllegalArgumentException(
32-
"A rule named " + r.name() + "has already been registered.");
32+
"A rule named " + r.name() + " has already been registered.");
3333
}
3434
}
3535
} else {

‎key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java‎

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

6+
import java.io.IOException;
7+
import java.nio.file.Files;
68
import java.nio.file.Paths;
79
import java.util.Collection;
810

@@ -20,17 +22,17 @@
2022
*/
2123
public class AdtTests {
2224
private static final String EXPECTED_PRED_DEC_SUCC = """
23-
pred_Dec_succ {
25+
DT_Nat#Dec_pred#succ {
2426
\\find(pred(succ(pred_sv)))
2527
\\sameUpdateLevel\\replacewith(pred_sv)\s
26-
28+
\\heuristics(simplify)
2729
Choices: true}""";
2830
private static final String EXPECTED_PRED_DECEQ_SUCC = """
29-
pred_DecEQ_succ {
30-
\\assumes ([equals(pred_x,succ(pred_sv))]==>[])\s
31+
DT_Nat#Dec_pred#succ#EQ {
32+
\\assumes ([equals(succ(pred_sv),pred_x)]==>[])\s
3133
\\find(pred(pred_x))
3234
\\sameUpdateLevel\\replacewith(pred_sv)\s
33-
35+
\\heuristics(simplify)
3436
Choices: true}""";
3537

3638
@Test
@@ -44,14 +46,35 @@ public void destructorTest() throws ProblemLoaderException {
4446
System.out.println(taclet.name());
4547
}
4648

47-
var predDecsucc = get("pred_Dec_succ", taclets);
48-
var predDecEqSucc = get("pred_DecEQ_succ", taclets);
49+
var predDecsucc = get("DT_Nat#Dec_pred#succ", taclets);
50+
var predDecEqSucc = get("DT_Nat#Dec_pred#succ#EQ", taclets);
4951

5052
Assertions.assertEquals(EXPECTED_PRED_DEC_SUCC, predDecsucc.toString());
5153
Assertions.assertEquals(EXPECTED_PRED_DECEQ_SUCC, predDecEqSucc.toString());
5254

5355
}
5456

57+
/*
58+
* Test for a non-recursive constructor. The generated taclet must not contain an induction
59+
* hypothesis.
60+
* See #3661
61+
*/
62+
@Test
63+
public void nonRecursiveConstructorTest() throws ProblemLoaderException, IOException {
64+
var path = Paths.get("../key.ui/examples/standard_key/adt/dt_nonrec.key");
65+
var env = KeYEnvironment.load(path);
66+
var taclets = env.getInitConfig().activatedTaclets();
67+
String expected = Files.lines(path)
68+
.filter(l -> l.startsWith("//!"))
69+
.map(l -> l.substring(4))
70+
.collect(java.util.stream.Collectors.joining("\n"));
71+
72+
var consTaclet = get("DT_NonRec#Dec_nonrecarg#b", taclets);
73+
// There are spaces before linebreaks. Better remove them for the comparison.
74+
Assertions.assertEquals(expected, consTaclet.toString().replaceAll(" +\n", "\n"));
75+
}
76+
77+
5578
private Taclet get(String name, Collection<Taclet> taclets) {
5679
var n = new Name(name);
5780
var t = taclets.stream().filter(it -> n.equals(it.name())).findAny().orElse(null);

‎key.ui/examples/standard_key/adt/dt_color.proof‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@
5656

5757
(branch "dummy ID"
5858
(rule "allRight" (formula "1") (inst "sk=l_0") (userinteraction))
59-
(rule "Color_ctor_split" (formula "1") (term "0,0,0") (userinteraction))
59+
(rule "DT_Color_ctor_split" (formula "1") (term "0,0,0") (userinteraction))
6060
(branch "l_0 = Red"
6161
(rule "orRight" (formula "2"))
6262
(rule "orRight" (formula "2"))

‎key.ui/examples/standard_key/adt/dt_list_appnil.proof‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@
9595
(autoModeTime "105")
9696

9797
(branch "dummy ID"
98-
(rule "List_Ind" (inst "phi=(app(l, Nil) = l)<<origin(\"User_Interaction @ node 0 (Induction_for_List)\",\"[]\")>>") (inst "x=l") (userinteraction))
98+
(rule "DT_List_Induction" (inst "phi=(app(l, Nil) = l)<<origin(\"User_Interaction @ node 0 (Induction_for_List)\",\"[]\")>>") (inst "x=l") (userinteraction))
9999
(branch "Nil"
100100
(rule "concat_base" (formula "1") (term "0") (userinteraction))
101101
(builtin "One Step Simplification" (formula "1"))

‎key.ui/examples/standard_key/adt/dt_list_deconstruct.key‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
\datatypes {
2-
List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail);
2+
List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail2);
33
}
44

55
\functions {
66
List x;
77
}
88

99
\problem {
10-
Nil = tail(Cons(0, Nil)) & Nil = tail(Cons2(0, Nil)) & (x = Cons(0, Cons(1, Nil)) -> head(x) = 0)
10+
Nil = tail(Cons(0, Nil)) & Nil = tail2(Cons2(0, Nil)) & (Cons(0, Cons(1, Nil)) = x -> head(x) = 0)
1111
}

‎key.ui/examples/standard_key/adt/dt_list_deconstruct.proof‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -73,16 +73,16 @@
7373
}
7474

7575
\datatypes {
76-
List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail);
76+
List = Nil | Cons(any head, List tail) | Cons2(any head2, List tail2);
7777
}
7878

7979
\functions {
8080
List x;
8181
}
8282
\problem {
8383
Nil = tail(Cons(Z(0(#)), Nil))
84-
& Nil = tail(Cons2(Z(0(#)), Nil))
85-
& ( x = Cons(Z(0(#)), Cons(Z(1(#)), Nil))
84+
& Nil = tail2(Cons2(Z(0(#)), Nil))
85+
& ( Cons(Z(0(#)), Cons(Z(1(#)), Nil)) = x
8686
-> head(x) = Z(0(#)))
8787
}
8888

@@ -96,19 +96,19 @@
9696
(branch "Case 1"
9797
(rule "andRight" (formula "1") (userinteraction))
9898
(branch "Case 1"
99-
(rule "tail_Dec_Cons" (formula "1") (term "1") (userinteraction))
99+
(rule "DT_List#Dec_tail#Cons" (formula "1") (term "1") (userinteraction))
100100
(rule "equalUnique" (formula "1") (userinteraction))
101101
(rule "closeTrue" (formula "1") (userinteraction))
102102
)
103103
(branch "Case 2"
104-
(rule "tail_Dec_Cons2" (formula "1") (term "1") (userinteraction))
104+
(rule "DT_List#Dec_tail2#Cons2" (formula "1") (term "1") (userinteraction))
105105
(rule "equalUnique" (formula "1") (userinteraction))
106106
(rule "closeTrue" (formula "1") (userinteraction))
107107
)
108108
)
109109
(branch "Case 2"
110110
(rule "impRight" (formula "1") (userinteraction))
111-
(rule "head_DecEQ_Cons" (formula "2") (term "0") (ifseqformula "1") (userinteraction))
111+
(rule "DT_List#Dec_head#Cons#EQ" (formula "2") (term "0") (ifseqformula "1") (userinteraction))
112112
(rule "equal_literals" (formula "2") (userinteraction))
113113
(rule "closeTrue" (formula "2") (userinteraction))
114114
)

‎key.ui/examples/standard_key/adt/dt_list_revrev.proof‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,7 @@
110110
(autoModeTime "22638")
111111

112112
(branch "dummy ID"
113-
(rule "List_Ind" (inst "phi=(rev(rev(l)) = l)<<origin(\"User_Interaction @ node 0 (InductionforList)\",\"[]\")>>") (inst "x=l") (userinteraction))
113+
(rule "DT_List_Induction" (inst "phi=(rev(rev(l)) = l)<<origin(\"User_Interaction @ node 0 (InductionforList)\",\"[]\")>>") (inst "x=l") (userinteraction))
114114
(branch "Nil"
115115
(rule "allRight" (formula "2") (inst "sk=l_0"))
116116
(rule "revert_base" (formula "1") (term "0,0") (userinteraction))

‎key.ui/examples/standard_key/adt/dt_nonrec.key‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
/*
2+
There was a bug in the handling of datatypes with constructors that have no recursive arguments. #3661
3+
*/
4+
5+
// Expected selector taclet is as follows:
6+
//! DT_NonRec#Dec_nonrecarg#b {
7+
//! \find(nonrecarg(b(nonrecarg_sv)))
8+
//! \sameUpdateLevel\replacewith(nonrecarg_sv)
9+
//! \heuristics(simplify)
10+
//! Choices: true}
11+
12+
\datatypes {
13+
NonRec = a | b(int nonrecarg);
14+
}
15+
16+
\problem { true }
17+

0 commit comments

Comments
 (0)