Skip to content
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

Fixes several issues in the new AST term structures #7

Merged
merged 1 commit into from
Oct 23, 2023
Merged

Fixes several issues in the new AST term structures #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
1 change: 0 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/java/Services.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,6 @@ public Services getOverlay(NamespaceSet namespaces) {
return result;
}


/**
* Returns the TypeConverter associated with this Services object.
*/
Expand Down
27 changes: 7 additions & 20 deletions key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
* SPDX-License-Identifier: GPL-2.0-only */
package de.uka.ilkd.key.logic;

import java.util.HashMap;
import java.util.Map;

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

public NamespaceSet(Namespace<QuantifiableVariable> varNS,
Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators,
Namespace<Function> funcNS,
Namespace<Function> funcNS,
Namespace<Sort> sortNS, Namespace<RuleSet> ruleSetNS, Namespace<Choice> choiceNS,
Namespace<IProgramVariable> programVarNS) {
this.varNS = varNS;
Expand All @@ -47,21 +43,21 @@ public NamespaceSet(Namespace<QuantifiableVariable> varNS,
}

public NamespaceSet copy() {
return new NamespaceSet(variables().copy(), new HashMap<>(operators()), functions().copy(),
return new NamespaceSet(variables().copy(), functions().copy(),
sorts().copy(),
ruleSets().copy(), choices().copy(), programVariables().copy());
}

public NamespaceSet shallowCopy() {
return new NamespaceSet(variables(), operators(), functions(), sorts(), ruleSets(),
return new NamespaceSet(variables(), functions(), sorts(), ruleSets(),
choices(),
programVariables());
}

// TODO MU: Rename into sth with wrap or similar
public NamespaceSet copyWithParent() {
return new NamespaceSet(new Namespace<>(variables()),
operators(), new Namespace<>(functions()), new Namespace<>(sorts()),
new Namespace<>(functions()), new Namespace<>(sorts()),
new Namespace<>(ruleSets()), new Namespace<>(choices()),
new Namespace<>(programVariables()));
}
Expand All @@ -82,15 +78,6 @@ public void setProgramVariables(Namespace<IProgramVariable> progVarNS) {
this.progVarNS = progVarNS;
}

public Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators() {
return operators;
}

public void setOperators(
Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> operators) {
this.operators = operators;
}

public Namespace<Function> functions() {
return funcNS;
}
Expand Down Expand Up @@ -218,12 +205,12 @@ public boolean isEmpty() {

// create a namespace
public NamespaceSet simplify() {
return new NamespaceSet(varNS.simplify(), operators, funcNS.simplify(), sortNS.simplify(),
return new NamespaceSet(varNS.simplify(), funcNS.simplify(), sortNS.simplify(),
ruleSetNS.simplify(), choiceNS.simplify(), progVarNS.simplify());
}

public NamespaceSet getCompression() {
return new NamespaceSet(varNS.compress(), operators, funcNS.compress(), sortNS.compress(),
return new NamespaceSet(varNS.compress(), funcNS.compress(), sortNS.compress(),
ruleSetNS.compress(), choiceNS.compress(), progVarNS.compress());
}

Expand All @@ -234,7 +221,7 @@ public void flushToParent() {
}

public NamespaceSet getParent() {
return new NamespaceSet(varNS.parent(), operators, funcNS.parent(), sortNS.parent(),
return new NamespaceSet(varNS.parent(), funcNS.parent(), sortNS.parent(),
ruleSetNS.parent(), choiceNS.parent(), progVarNS.parent());
}

Expand Down
17 changes: 3 additions & 14 deletions key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -423,12 +423,12 @@ public Term func(Function f, Term[] s, ImmutableArray<QuantifiableVariable> boun
// }

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

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

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

// TODO: move?
public Modality modality(Modality.JavaModalityKind kind, JavaBlock jb) {
var pair = new Pair<>(kind, jb.program());
Modality mod = services.getNamespaces().operators().get(pair);
if (mod == null) {
mod = new Modality(jb, kind);
services.getNamespaces().operators().put(pair, mod);
}
return mod;
}

public Term ife(Term cond, Term _then, Term _else) {
return tf.createTerm(IfThenElse.IF_THEN_ELSE, cond, _then, _else);
}
Expand Down Expand Up @@ -1706,7 +1695,7 @@ public Term addLabel(Term term, ImmutableArray<TermLabel> labels) {

for (TermLabel newLabel : labels) {
for (TermLabel oldLabel : newLabelList) {
if (oldLabel.getClass().equals(newLabel.getClass())) {
if (oldLabel.getClass() == newLabel.getClass()) {
newLabelList.remove(oldLabel);
break;
}
Expand Down
37 changes: 19 additions & 18 deletions key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -362,6 +362,10 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
return true;
}

if (t0.sort() != t1.sort() || t0.arity() != t1.arity()) {
return false;
}

final Operator op0 = t0.op();

if (op0 instanceof QuantifiableVariable) {
Expand All @@ -374,24 +378,21 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList<QuantifiableVariable>
if (mod0.kind() != mod1.kind()) {
return false;
}
nat = handleJava(t0, t1, nat);
nat = handleJava(mod0.program(), mod1.program(), nat);
if (nat == FAILED) {
return false;
}
} else if (!(op0 instanceof ProgramVariable) && op0 != op1) {
return false;
}

if (t0.sort() != t1.sort() || t0.arity() != t1.arity()) {
return false;
}

if (!(t0.op() instanceof SchemaVariable) && t0.op() instanceof ProgramVariable) {
if (!(t1.op() instanceof ProgramVariable)) {
return false;
}
nat = checkNat(nat);
if (!((ProgramVariable) t0.op()).equalsModRenaming((ProgramVariable) t1.op(), nat)) {
if (!(op0 instanceof SchemaVariable) && op0 instanceof ProgramVariable pv0) {
if (op1 instanceof ProgramVariable pv1) {
nat = checkNat(nat);
if (!pv0.equalsModRenaming(pv1, nat)) {
return false;
}
} else {
return false;
}
}
Expand All @@ -413,15 +414,13 @@ && compareBoundVariables((QuantifiableVariable) t0.op(),
*/
private static final NameAbstractionTable FAILED = new NameAbstractionTable();

private static NameAbstractionTable handleJava(Term t0, Term t1, NameAbstractionTable nat) {

if (!t0.javaBlock().isEmpty() || !t1.javaBlock().isEmpty()) {
private static NameAbstractionTable handleJava(JavaBlock jb0, JavaBlock jb1, NameAbstractionTable nat) {
if (!jb0.isEmpty() || !jb1.isEmpty()) {
nat = checkNat(nat);
if (!t0.javaBlock().equalsModRenaming(t1.javaBlock(), nat)) {
if (!jb0.equalsModRenaming(jb1, nat)) {
return FAILED;
}
}

return nat;
}

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

return op.equals(t.op) && t.hasLabels() == hasLabels() && subs.equals(t.subs)
&& boundVars.equals(t.boundVars) && javaBlock().equals(t.javaBlock());
&& boundVars.equals(t.boundVars)
// TODO (DD): below is no longer necessary
&& javaBlock().equals(t.javaBlock());
}

@Override
Expand Down Expand Up @@ -709,7 +710,7 @@ public ImmutableArray<TermLabel> getLabels() {
public boolean containsJavaBlockRecursive() {
if (containsJavaBlockRecursive == ThreeValuedTruth.UNKNOWN) {
ThreeValuedTruth result = ThreeValuedTruth.FALSE;
if (javaBlock() != null && !javaBlock().isEmpty()) {
if (!javaBlock().isEmpty()) {
result = ThreeValuedTruth.TRUE;
} else {
for (int i = 0, arity = subs.size(); i < arity; i++) {
Expand Down
27 changes: 26 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/logic/op/Modality.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
import java.util.HashMap;
import java.util.Map;

import de.uka.ilkd.key.java.JavaProgramElement;
import de.uka.ilkd.key.ldt.JavaDLTheory;
import de.uka.ilkd.key.logic.JavaBlock;
import de.uka.ilkd.key.logic.Term;
Expand All @@ -15,12 +16,37 @@

import org.key_project.logic.Name;
import org.key_project.logic.Program;
import org.key_project.util.collection.Pair;

/**
* This class is used to represent a dynamic logic modality like diamond and box (but also
* extensions of DL like preserves and throughout are possible in the future).
*/
public class Modality extends org.key_project.logic.op.Modality<Sort> implements Operator {
/*
keeps track of created modalities
*/
private static Map<Pair<JavaModalityKind, JavaProgramElement>, Modality> operators =
new HashMap<>();


/**
* Returns the knownm modalities
*/
public static Map<Pair<JavaModalityKind, JavaProgramElement>, Modality> operators() {
return operators;
}

public static Modality modality(Modality.JavaModalityKind kind, JavaBlock jb) {
var pair = new Pair<>(kind, jb.program());
Modality mod = Modality.operators().get(pair);
if (mod == null) {
mod = new Modality(jb, kind);
Modality.operators().put(pair, mod);
}
return mod;
}

/**
* creates a modal operator with the given name
*
Expand Down Expand Up @@ -142,7 +168,6 @@ public static class JavaModalityKind extends Kind implements SVSubstitute {
*/
public static final JavaModalityKind TOUT_TRANSACTION =
new JavaModalityKind(new Name("throughout_transaction"));
public static final JavaModalityKind MOD_SV = new JavaModalityKind(new Name("mod_sv"));

public JavaModalityKind(Name name) {
super(name);
Expand Down
5 changes: 3 additions & 2 deletions key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1020,7 +1020,7 @@
Namespace<QuantifiableVariable> orig = variables();
List<QuantifiableVariable> exVars = accept(ctx.bound_variables());
Term condF = accept(ctx.condF);
if (condF.sort() != JavaDLTheory.FORMULA) {

Check warning on line 1023 in key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java

View workflow job for this annotation

GitHub Actions / qodana

Constant conditions & exceptions 

Method invocation `sort` may produce `NullPointerException`
semanticError(ctx, "Condition of an \\ifEx-then-else term has to be a formula.");
}

Expand Down Expand Up @@ -1151,11 +1151,12 @@
* "No schema elements allowed outside taclet declarations (" + sjb.opName + ")"); }
*/
Modality.JavaModalityKind kind = (Modality.JavaModalityKind) schemaVariables().lookup(new Name(sjb.opName));
op = getServices().getTermBuilder().modality(kind, sjb.javaBlock);
op = Modality.modality(kind, sjb.javaBlock);
} else {
op = getServices().getTermBuilder().modality(Modality.JavaModalityKind.getKind(sjb.opName), sjb.javaBlock);
Modality.JavaModalityKind kind = Modality.JavaModalityKind.getKind(sjb.opName);
op = Modality.modality(kind, sjb.javaBlock);
}
if (op == null) {

Check warning on line 1159 in key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java

View workflow job for this annotation

GitHub Actions / qodana

Constant conditions & exceptions 

Condition `op == null` is always `false`
semanticError(ctx, "Unknown modal operator: " + sjb.opName);
}

Expand Down
13 changes: 3 additions & 10 deletions key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,24 +5,19 @@

import java.io.IOException;
import java.io.Reader;
import java.util.Map;

import de.uka.ilkd.key.java.JavaProgramElement;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Namespace;
import de.uka.ilkd.key.logic.NamespaceSet;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.Function;
import de.uka.ilkd.key.logic.op.IProgramVariable;
import de.uka.ilkd.key.logic.op.Modality;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.sort.Sort;
import de.uka.ilkd.key.nparser.KeyIO;
import de.uka.ilkd.key.pp.AbbrevMap;

import org.key_project.util.collection.Pair;

import org.antlr.v4.runtime.CharStreams;
import org.antlr.v4.runtime.RecognitionException;

Expand All @@ -42,18 +37,16 @@ public final class DefaultTermParser {
* ensures, that the term has the specified sort.
*
* @param sort The expected sort of the term.
* @param op_ns
* @return The parsed term of the specified sort.
* @throws ParserException The method throws a ParserException, if the input could not be parsed
* correctly or the term has an invalid sort.
* correctly or the term has an invalid sort.
*/
public Term parse(Reader in, Sort sort, Services services,
Namespace<QuantifiableVariable> var_ns,
Map<Pair<Modality.JavaModalityKind, JavaProgramElement>, Modality> op_ns,
Namespace<Function> func_ns,
Namespace<Function> func_ns,
Namespace<Sort> sort_ns, Namespace<IProgramVariable> progVar_ns, AbbrevMap scm)
throws ParserException {
return parse(in, sort, services, new NamespaceSet(var_ns, op_ns, func_ns, sort_ns,
return parse(in, sort, services, new NamespaceSet(var_ns, func_ns, sort_ns,
new Namespace<>(), new Namespace<>(), progVar_ns), scm);
}

Expand Down
3 changes: 2 additions & 1 deletion key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1667,7 +1667,8 @@ public void printModalityTerm(String left, JavaBlock jb, String right, Term phi,
for (int i = 0; i < phi.arity(); i++) {
ta[i] = phi.sub(i);
}
Modality m = services.getTermBuilder().modality(mod.kind(), mod.program());
JavaBlock jb1 = mod.program();
Modality m = Modality.modality(mod.kind(), jb1);
Term term = services.getTermFactory().createTerm(m, ta,
phi.boundVars(), phi.javaBlock());
notationInfo.getNotation(m).print(term, this);
Expand Down
5 changes: 2 additions & 3 deletions key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -468,11 +468,10 @@ private GoalsConfigurator setUpGoalConfigurator(final StatementBlock block,
final KeYJavaType kjt = getCalleeKeYJavaType();
final TypeRef typeRef = new TypeRef(new ProgramElementName(kjt.getName()), 0, selfVar, kjt);
final ExecutionContext ec = new ExecutionContext(typeRef, getProgramMethod(), selfVar);
// TODO (DD): HACK
final Instantiation inst =
new Instantiation(tb.skip(), tb.tt(),
new Modality(JavaBlock.createJavaBlock(new StatementBlock()),
contract.getModalityKind()),
Modality.modality(contract.getModalityKind(),
JavaBlock.createJavaBlock(new StatementBlock())),
selfTerm, block, ec);
return new GoalsConfigurator(null, new TermLabelState(), inst,
contract.getAuxiliaryContract().getLabels(), variables, null, services, null);
Expand Down
2 changes: 1 addition & 1 deletion key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -940,7 +940,7 @@ public static Term parseTerm(String value, Proof proof, Namespace<QuantifiableVa
Namespace<IProgramVariable> progVarNS, Namespace<Function> functNS) {
try {
return new DefaultTermParser().parse(new StringReader(value), null, proof.getServices(),
varNS, proof.getNamespaces().operators(), functNS, proof.getNamespaces().sorts(),
varNS, functNS, proof.getNamespaces().sorts(),
progVarNS, new AbbrevMap());
} catch (ParserException e) {
throw new RuntimeException(
Expand Down
Loading
Loading