Skip to content

small fixes to datatype handling #3661

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wadoon merged 7 commits into from
Sep 22, 2025
Merged

small fixes to datatype handling #3661

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
554dd80
small fixes to datatype handling
mattulbrich Sep 18, 2025
d20191a
spotlessing
mattulbrich Sep 18, 2025
4b42f41
repaired test case
WolframPfeifer Sep 18, 2025
bc6f3a4
fixed test cases in RunAllFunProofs
WolframPfeifer Sep 19, 2025
204c7f0
adding a test case for datatypes with nonrecursive constructors.
mattulbrich Sep 19, 2025
11024a1
Adding comment to clarify an if-condition
mattulbrich Sep 19, 2025
b425891
spotlessing
mattulbrich Sep 22, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 13 additions & 3 deletions key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,10 @@
import org.key_project.logic.Name;
import org.key_project.logic.Namespace;
import org.key_project.logic.op.Function;
import org.key_project.logic.op.SortedOperator;
import org.key_project.logic.sort.Sort;
import org.key_project.util.collection.ImmutableArray;
import org.key_project.util.collection.ImmutableList;


/**
Expand Down Expand Up @@ -65,11 +67,19 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
Sort argSort = accept(constructorContext.sortId(i));
args[i] = argSort;
var argName = argNames.get(i).getText();
var alreadyDefinedFn = dtNamespace.lookup(argName);
SortedOperator alreadyDefinedFn = dtNamespace.lookup(argName);
if (alreadyDefinedFn == null) {
alreadyDefinedFn = namespaces().functions().lookup(argName);
}
if (alreadyDefinedFn == null) {
alreadyDefinedFn = namespaces().programVariables().lookup(argName);
}
if (alreadyDefinedFn != null
&& (!alreadyDefinedFn.sort().equals(argSort)
|| !alreadyDefinedFn.argSort(0).equals(sort))) {
throw new RuntimeException("Name already in namespace: " + argName);
|| !alreadyDefinedFn.argSorts().equals(ImmutableList.of(sort)))) {
semanticError(argNames.get(i), "Name already in namespace: %s" +
". Identifiers in datatype definitions must be unique (also wrt. global functions).",
argName);
}
Function fn = new JFunction(new Name(argName), argSort, new Sort[] { sort }, null,
false, false);
Expand Down
35 changes: 21 additions & 14 deletions key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -263,7 +263,7 @@ public Object visitDatatype_decl(KeYParser.Datatype_declContext ctx) {
for (int i = 0; i < constructor.sortId().size(); i++) {
var argName = constructor.argName.get(i).getText();

var tbDeconstructor = createDeconstructorTaclet(constructor, argName, i);
var tbDeconstructor = createDeconstructorTaclet(constructor, argName, i, dtSort);
registerTaclet(ctx, tbDeconstructor);

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

private TacletBuilder<? extends Taclet> createDeconstructorTaclet(
KeYParser.Datatype_constructorContext constructor, String argName, int argIndex) {
KeYParser.Datatype_constructorContext constructor, String argName, int argIndex,
Sort dtSort) {
var tacletBuilder = new RewriteTacletBuilder<>();
tacletBuilder
.setName(new Name(String.format("%s_Dec_%s", argName, constructor.name.getText())));
.setName(new Name(String.format("DT_%s#Dec_%s#%s", dtSort.name(), argName,
constructor.name.getText())));
tacletBuilder.setDisplayName(
String.format("%s_Deconstruct_%s", argName, constructor.name.getText()));
String.format("DT %s Deconstructor %s (for %s)", dtSort.name(), argName,
constructor.name.getText()));

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

return tacletBuilder;
}
Expand All @@ -314,9 +318,11 @@ private TacletBuilder<? extends Taclet> createDeconstructorEQTaclet(
Sort dtSort) {
var tacletBuilder = new RewriteTacletBuilder<>();
tacletBuilder.setName(
new Name(String.format("%s_DecEQ_%s", argName, constructor.name.getText())));
new Name(String.format("DT_%s#Dec_%s#%s#EQ", dtSort.name(), argName,
constructor.name.getText())));
tacletBuilder.setDisplayName(
String.format("%s_DeconstructEQ_%s", argName, constructor.name.getText()));
String.format("DT %s Deconstructor %s (for %s)", dtSort.name(), argName,
constructor.name.getText()));

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

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

cases.forEach(tacletBuilder::addTacletGoalTemplate);
tacletBuilder.setDisplayName("Induction_for_" + sort.name());
tacletBuilder.setName(new Name(String.format("DT_%s_Induction", sort.name())));
tacletBuilder.setDisplayName(String.format("DT %s Induction", sort.name()));
return tacletBuilder;
}

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

tacletBuilder.setDisplayName("Axiom_for_" + sort.name());
tacletBuilder.setName(new Name(String.format("DT_%s_Axiom", sort.name())));
tacletBuilder.setDisplayName(String.format("DT %s Axiom", sort.name()));
return tacletBuilder;
}

Expand Down Expand Up @@ -452,7 +459,7 @@ private JTerm createQuantifiedFormula(KeYParser.Datatype_constructorContext cont
}

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

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

var phi = declareSchemaVariable(ctx, "var", sort,
false, false, false,
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationInfo.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ public void addJustification(Rule r, RuleJustification j) {
for (RuleKey key : rule2Justification.keySet()) {
if (key.equals(ruleKey) && r != key.r) {
throw new IllegalArgumentException(
"A rule named " + r.name() + "has already been registered.");
"A rule named " + r.name() + " has already been registered.");
}
}
} else {
Expand Down
14 changes: 7 additions & 7 deletions key.core/src/test/java/de/uka/ilkd/key/nparser/AdtTests.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,17 +20,17 @@
*/
public class AdtTests {
private static final String EXPECTED_PRED_DEC_SUCC = """
pred_Dec_succ {
DT_Nat#Dec_pred#succ {
\\find(pred(succ(pred_sv)))
\\sameUpdateLevel\\replacewith(pred_sv)\s

\\heuristics(simplify)
Choices: true}""";
private static final String EXPECTED_PRED_DECEQ_SUCC = """
pred_DecEQ_succ {
\\assumes ([equals(pred_x,succ(pred_sv))]==>[])\s
DT_Nat#Dec_pred#succ#EQ {
\\assumes ([equals(succ(pred_sv),pred_x)]==>[])\s
\\find(pred(pred_x))
\\sameUpdateLevel\\replacewith(pred_sv)\s

\\heuristics(simplify)
Choices: true}""";

@Test
Expand All @@ -44,8 +44,8 @@ public void destructorTest() throws ProblemLoaderException {
System.out.println(taclet.name());
}

var predDecsucc = get("pred_Dec_succ", taclets);
var predDecEqSucc = get("pred_DecEQ_succ", taclets);
var predDecsucc = get("DT_Nat#Dec_pred#succ", taclets);
var predDecEqSucc = get("DT_Nat#Dec_pred#succ#EQ", taclets);

Assertions.assertEquals(EXPECTED_PRED_DEC_SUCC, predDecsucc.toString());
Assertions.assertEquals(EXPECTED_PRED_DECEQ_SUCC, predDecEqSucc.toString());
Expand Down
Loading