Commit 3ff04f0c authored by Lulu Luong's avatar Lulu Luong

Merge branch 'master' of C:\Users\Lulu\Desktop\Bachelor\ProofScriptParser with conflicts.

parent a0f432d5
......@@ -33,10 +33,7 @@ import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import java.util.*;
/**
* @author Alexander Weigl
......@@ -77,7 +74,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
try {
for (SequentFormula sf : g.node().sequent().succedent()) {
ImmutableList<TacletApp> apps = index.getTacletAppAtAndBelow(filter,
new PosInOccurrence(sf, PosInTerm.getTopLevel(), false),
new PosInOccurrence(sf, PosInTerm.getTopLevel(), true),
services);
apps.forEach(t -> set.add(t.taclet().name().toString()));
}
......@@ -120,11 +117,13 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
params.asMap().forEach((k, v) -> map.put(k.getIdentifier(), v.getData()));
LOGGER.info("Execute {} with {}", call, map);
RuleCommand.Parameters cc;
try {
map.put("#2", call.getCommand());
EngineState estate = new EngineState(kd.getProof());
estate.setGoal(kd.getNode());
RuleCommand.Parameters cc = new RuleCommand.Parameters();
cc = new RuleCommand.Parameters();
ValueInjector valueInjector = ValueInjector.createDefault(kd.getNode());
cc = valueInjector.inject(c, cc, map);
AbstractUserInterfaceControl uiControl = new DefaultUserInterfaceControl();
......@@ -140,6 +139,37 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
state.getGoals().add(new GoalNode<>(expandedNode, kdn, kdn.getNode().isClosed()));
}
} catch (ScriptException e) {
//TODO: adding UserinteractionWindow
/*TODO: possible cases not applicable, because
command not recognized (can be ignored)
command multiple matches -> need more specification with on + formula
if(e.getMessage().equals("More than one applicable occurrence")) {
//TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 121)
ImmutableList<TacletApp> allApps = c.findAllTacletApps(cc, state);
List<TacletApp> matchingApps = c.filterList(cc, allApps);
//TODO: (re)apply completed TacletApp
//TODO: insert into script
}
command not complete -> missig parameters
solution:
if(e.getMessage().equals("Not a unique \\assumes instantiation")) {
//TODO: open UserinteractionWindow with selectionbox , need (RuleCommand: 56)
ImmutableList<TacletApp> assumesCandidates = theApp.findIfFormulaInstantiations(state.getFirstOpenGoal().sequent(), proof.getServices());
//TODO: (re)apply completed TacletApp
//TODO: insert into script
}
*/
if (interpreter.isStrictMode()) {
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
......
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