Commit 86619428 authored by Alexander Weigl's avatar Alexander Weigl

some fixes, but not for uninstantiated taclets

parent 0430bb2f
package edu.kit.iti.formal.psdbg;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.PosInOccurrence;
import de.uka.ilkd.key.logic.PosInTerm;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.proof.RuleAppIndex;
import de.uka.ilkd.key.proof.rulefilter.TacletFilter;
import de.uka.ilkd.key.rule.*;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableSLList;
import java.util.ArrayList;
import java.util.List;
public class RuleCommandHelper {
private final Proof proof;
private final Services services;
private final Goal g;
private final RuleCommand.Parameters parameters;
public RuleCommandHelper(Goal g, RuleCommand.Parameters parameters) {
this.proof = g.proof();
this.services = proof.getServices();
this.g = g;
this.parameters = parameters;
}
public int getOccurence(TacletApp app) {
List<TacletApp> apps = getTacletApps();
if (apps.isEmpty()) {
return -1;
}
if(apps.size()==1) {
return 0;
}
return 0;
//return apps.indexOf(app);
}
private List<TacletApp> getTacletApps() {
ImmutableList<TacletApp> allApps = findAllTacletApps();
return filterList(allApps);
}
public ImmutableList<TacletApp> findAllTacletApps() {
TacletFilter filter = new TacletNameFilter(parameters.rulename);
RuleAppIndex index = g.ruleAppIndex();
index.autoModeStopped();
ImmutableList<TacletApp> allApps = ImmutableSLList.nil();
for (SequentFormula sf : g.node().sequent().antecedent()) {
if (parameters.formula != null && !sf.formula().equalsModRenaming(parameters.formula)) {
continue;
}
allApps = allApps.append(index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
services));
}
for (SequentFormula sf : g.node().sequent().succedent()) {
if (parameters.formula != null && !sf.formula().equalsModRenaming(parameters.formula)) {
continue;
}
allApps = allApps.append(index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), false),
services));
}
return allApps;
}
/*
* Filter those apps from a list that are according to the parameters.
*/
private List<TacletApp> filterList(ImmutableList<TacletApp> list) {
List<TacletApp> matchingApps = new ArrayList<TacletApp>();
for (TacletApp tacletApp : list) {
if (tacletApp instanceof PosTacletApp) {
PosTacletApp pta = (PosTacletApp) tacletApp;
if (parameters.on == null || pta.posInOccurrence().subTerm()
.equalsModRenaming(parameters.on)) {
matchingApps.add(pta);
}
}
}
return matchingApps;
}
private static class TacletNameFilter extends TacletFilter {
private final Name rulename;
public TacletNameFilter(String rulename) {
this.rulename = new Name(rulename);
}
@Override
protected boolean filter(Taclet taclet) {
return taclet.name().equals(rulename);
}
}
}
......@@ -21,7 +21,6 @@ import org.key_project.util.collection.ImmutableList;
import java.io.File;
import java.util.Collection;
import java.util.Collections;
import java.util.List;
import java.util.stream.Collectors;
......@@ -201,6 +200,9 @@ public class KeYProofFacade {
public void setEnvironment(KeYEnvironment environment) {
this.environment.set(environment);
if (environment != null) {
getEnvironment().getUi().getProofControl().setMinimizeInteraction(true);
}
}
public SimpleObjectProperty<KeYEnvironment> environmentProperty() {
......@@ -233,7 +235,7 @@ public class KeYProofFacade {
ImmutableList<Goal> openGoals = p.getSubtreeGoals(p.root());
List<GoalNode<KeyData>> goals = openGoals.stream().map(g ->
new GoalNode<>(null, new KeyData(g, env, p), false))
.collect(Collectors.toList());
.collect(Collectors.toList());
return goals;
}
......
......@@ -29,7 +29,7 @@ import java.util.Locale;
public class ProofScriptDebugger extends Application {
public static final String NAME = "Proof Script Debugger";
public static final String VERSION = "0.1";
public static final String VERSION = "1.0-FM";
public static final String KEY_VERSION = KeYConstants.VERSION;
......
......@@ -6,13 +6,17 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Node;
import de.uka.ilkd.key.proof.Proof;
import de.uka.ilkd.key.rule.inst.InstantiationEntry;
import edu.kit.iti.formal.psdbg.LabelFactory;
import edu.kit.iti.formal.psdbg.RuleCommandHelper;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
import edu.kit.iti.formal.psdbg.gui.controls.ScriptController;
import edu.kit.iti.formal.psdbg.gui.controls.Utils;
......@@ -27,8 +31,6 @@ import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicabl
import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
import edu.kit.iti.formal.psdbg.parser.ast.*;
import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
import javafx.beans.property.BooleanProperty;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.collections.ObservableList;
......@@ -39,12 +41,11 @@ import lombok.val;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import org.key_project.util.collection.ImmutableMapEntry;
import recoder.util.Debug;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.math.BigInteger;
import java.util.*;
import java.util.stream.Collectors;
@Getter
......@@ -147,19 +148,44 @@ public class InteractiveModeController {
SequentFormula seqForm = tap.getPio().sequentFormula();
//transform term to parsable string representation
Sequent seq = g.sequent();
String term = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
String sfTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
String onTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(tap.getPio().subTerm());
//check whether more than one possibility for match
Matchings matches = MatcherFacade.matches(term, seq, true, keYServices);
//Matchings matches = MatcherFacade.matches(term, seq, true, keYServices);
Parameters params = new Parameters();
/*Parameters params = new Parameters();
params.put(new Variable("formula"), new TermLiteral(term));
if (matches.size() > 1) {
moreThanOneMatch = true;
params.put(new Variable("occ"), new StringLiteral("0"));
}
}*/
RuleCommand.Parameters params = new RuleCommand.Parameters();
params.formula = seqForm.formula();
params.rulename = tap.getApp().taclet().name().toString();
params.on = tap.getPio().subTerm();
RuleCommandHelper rch = new RuleCommandHelper(g, params);
int occ = rch.getOccurence(tap.getApp());
Parameters callp = new Parameters();
callp.put(new Variable("formula"), new TermLiteral(sfTerm));
callp.put(new Variable("occ"), new IntegerLiteral(BigInteger.valueOf(occ)));
callp.put(new Variable("on"), new TermLiteral(onTerm));
VariableAssignment va = new VariableAssignment(null);
CallStatement call = new CallStatement(tapName, params);
CallStatement call = new CallStatement(tapName, callp);
/*
Iterator<ImmutableMapEntry<SchemaVariable, InstantiationEntry<?>>> iter = tap.getApp().instantiations().pairIterator();
while (iter.hasNext()) {
ImmutableMapEntry<SchemaVariable, InstantiationEntry<?>> entry = iter.next();
String p = "inst_" + entry.key().proofToString();
String v = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm((Term) entry.value().getInstantiation());
call.getParameters().put(new Variable(p), new TermLiteral(v));
}*/
try {
......@@ -178,9 +204,14 @@ public class InteractiveModeController {
} catch (ScriptCommandNotApplicableException e) {
Utils.showExceptionDialog("Proof Command was not Applicable",
"Proof Command was not Applicable",
"The script command " + call.getCommand().toString() + " was not applicable. " + e.getMessage(), e);
StringBuilder sb = new StringBuilder("The script command ");
sb.append(call.getCommand()).append(" was not applicable.");
sb.append("\nSequent Formula: formula=").append(sfTerm);
sb.append("\nOn Sub Term: on=").append(onTerm);
Utils.showExceptionDialog("Proof Command was not applicable",
"Proof Command was not applicable.",
sb.toString(), e);
}
......
......@@ -206,6 +206,14 @@ public class TacletContextMenu extends ContextMenu {
toAdd.addAll(noFindTaclets);
}
/*toAdd=toAdd.stream().filter(tapp->{
try{
return tapp.isExecutable(goal.proof().getServices());
}catch (NullPointerException e) {
return false;
}
}).collect(Collectors.toList());*/
if (rulesAvailable) {
createMenuItems(toAdd);
} else {
......
......@@ -191,6 +191,9 @@ public class Utils {
alert.getDialogPane().setExpandableContent(expContent);
alert.setHeight(600);
alert.setWidth(400);
alert.showAndWait();
}
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment