Commit 490a1bc0 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

key handler

parent ffb9d946
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.macros.scripts.EngineState;
import edu.kit.formal.interpreter.funchdl.CommandCall; import edu.kit.formal.interpreter.funchdl.CommandCall;
import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.interpreter.funchdl.CommandLookup;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
...@@ -38,6 +40,8 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -38,6 +40,8 @@ public class Interpreter extends DefaultASTVisitor<Void>
@Getter @Getter
@Setter @Setter
private boolean scrictSelectedGoalMode = false; private boolean scrictSelectedGoalMode = false;
private EngineState engineState;
private ScriptApi scriptApi;
public Interpreter(CommandLookup lookup) { public Interpreter(CommandLookup lookup) {
functionLookup = lookup; functionLookup = lookup;
...@@ -403,5 +407,13 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -403,5 +407,13 @@ public class Interpreter extends DefaultASTVisitor<Void>
public List<GoalNode> getCurrentGoals() { public List<GoalNode> getCurrentGoals() {
return getCurrentState().getGoals(); return getCurrentState().getGoals();
} }
public EngineState getEngineState() {
return engineState;
}
public ScriptApi getScriptApi() {
return scriptApi;
}
//endregion //endregion
} }
package edu.kit.formal.interpreter;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
import de.uka.ilkd.key.proof.Proof;
import edu.kit.formal.interpreter.funchdl.*;
import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
import java.io.File;
import java.io.IOException;
import java.util.Arrays;
import java.util.List;
/**
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
public class InterpreterBuilder {
private ProofScriptHandler psh = new ProofScriptHandler();
private MacroCommandHandler pmh = new MacroCommandHandler();
private RuleCommandHandler pmr = new RuleCommandHandler();
private ProofScriptCommandBuilder pmc = new ProofScriptCommandBuilder();
public Interpreter build(File file) throws IOException {
return build(Facade.getAST(file));
}
private Interpreter build(List<ProofScript> ast) {
psh.addScripts(ast);
DefaultLookup lookup = new DefaultLookup(psh, pmh, pmr, pmc);
return new Interpreter(lookup);
}
public InterpreterBuilder scriptSearchPath(File... paths) {
}
public InterpreterBuilder keyRules(Proof proof) {
}
public InterpreterBuilder defaultScriptCommands(List<ProofScriptCommand> commands) {
}
public InterpreterBuilder defaultKeyMacros(List<ProofMacro> macros) {
}
public InterpreterBuilder register(ProofScript... script) {
psh.addScripts(Arrays.asList(script));
return this;
}
public InterpreterBuilder onEntry(Visitor v) {
return this;
}
public InterpreterBuilder onExit(Visitor v) {
return this;
}
public InterpreterBuilder captureHistory() {
return this;
}
public InterpreterBuilder log(String prefix) {
return this;
}
}
...@@ -18,6 +18,10 @@ public class DefaultLookup implements CommandLookup { ...@@ -18,6 +18,10 @@ public class DefaultLookup implements CommandLookup {
public DefaultLookup() { public DefaultLookup() {
} }
public DefaultLookup(CommandHandler... cmdh) {
builders.addAll(Arrays.asList(cmdh));
}
public void callCommand(Interpreter interpreter, public void callCommand(Interpreter interpreter,
CallStatement call, CallStatement call,
VariableAssignment params) { VariableAssignment params) {
......
...@@ -12,6 +12,7 @@ import edu.kit.formal.proofscriptparser.ast.Variable; ...@@ -12,6 +12,7 @@ import edu.kit.formal.proofscriptparser.ast.Variable;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import java.lang.reflect.Parameter; import java.lang.reflect.Parameter;
import java.util.HashMap;
import java.util.Map; import java.util.Map;
/** /**
...@@ -22,6 +23,10 @@ import java.util.Map; ...@@ -22,6 +23,10 @@ import java.util.Map;
public class MacroCommandHandler implements CommandHandler { public class MacroCommandHandler implements CommandHandler {
private final Map<String, ProofMacro> macros; private final Map<String, ProofMacro> macros;
public MacroCommandHandler() {
macros = new HashMap<>();
}
@Override @Override
public boolean handles(CallStatement call) throws IllegalArgumentException { public boolean handles(CallStatement call) throws IllegalArgumentException {
......
...@@ -8,6 +8,7 @@ import edu.kit.formal.interpreter.VariableAssignment; ...@@ -8,6 +8,7 @@ import edu.kit.formal.interpreter.VariableAssignment;
import edu.kit.formal.proofscriptparser.ast.CallStatement; import edu.kit.formal.proofscriptparser.ast.CallStatement;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import java.util.HashMap;
import java.util.Map; import java.util.Map;
/** /**
...@@ -18,6 +19,10 @@ import java.util.Map; ...@@ -18,6 +19,10 @@ import java.util.Map;
public class ProofScriptCommandBuilder implements CommandHandler { public class ProofScriptCommandBuilder implements CommandHandler {
private final Map<String, ProofScriptCommand> scripts; private final Map<String, ProofScriptCommand> scripts;
public ProofScriptCommandBuilder() {
this(new HashMap<>());
}
@Override @Override
public boolean handles(CallStatement call) { public boolean handles(CallStatement call) {
return scripts.containsKey(call.getCommand()); return scripts.containsKey(call.getCommand());
......
...@@ -28,6 +28,10 @@ public class ProofScriptHandler implements CommandHandler { ...@@ -28,6 +28,10 @@ public class ProofScriptHandler implements CommandHandler {
@Getter @Getter
private final List<File> searchPath = new ArrayList<>(); private final List<File> searchPath = new ArrayList<>();
public ProofScriptHandler() {
scripts = new HashMap<>();
}
public ProofScriptHandler(List<ProofScript> proofScripts) { public ProofScriptHandler(List<ProofScript> proofScripts) {
scripts = new HashMap<>(); scripts = new HashMap<>();
proofScripts.forEach(s -> scripts.put(s.getName(), s)); proofScripts.forEach(s -> scripts.put(s.getName(), s));
...@@ -86,4 +90,8 @@ public class ProofScriptHandler implements CommandHandler { ...@@ -86,4 +90,8 @@ public class ProofScriptHandler implements CommandHandler {
//TODO create new context/introduce signature //TODO create new context/introduce signature
ps.accept(interpreter); ps.accept(interpreter);
} }
public void addScripts(List<ProofScript> ast) {
ast.forEach(script -> scripts.put(script.getName(), script));
}
} }
package edu.kit.formal.interpreter.funchdl;
import de.uka.ilkd.key.api.ProjectedNode;
import de.uka.ilkd.key.api.ProofScriptCommandCall;
import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.api.VariableAssignments;
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.rule.Rule;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.VariableAssignment;
import edu.kit.formal.proofscriptparser.ast.CallStatement;
import edu.kit.formal.proofscriptparser.ast.Parameters;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import java.util.HashMap;
import java.util.Map;
/**
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
@RequiredArgsConstructor
public class RuleCommandHandler implements CommandHandler {
@Getter
private final Map<String, Rule> rules;
public RuleCommandHandler() {
this(new HashMap<>());
}
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
return rules.containsKey(call.getCommand());
}
@Override
public void evaluate(Interpreter interpreter,
CallStatement call,
VariableAssignment params) {
Rule r = rules.get(call.getCommand());
RuleCommand rc = new RuleCommand();
RuleCommand.Parameters rcp = new RuleCommand.Parameters();
//TODO fill in rcp
EngineState es = interpreter.getEngineState();
ScriptApi sa = interpreter.getScriptApi();
VariableAssignments assignments = new VariableAssignments();
ProjectedNode onNode = null;
try {
sa.executeScriptCommand(
new ProofScriptCommandCall<RuleCommand.Parameters>(rc, rcp),
onNode, assignments);
} catch (ScriptException e) {
e.printStackTrace();
} catch (InterruptedException e) {
e.printStackTrace();
}
}
}
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