Commit 53a01a49 authored by Sarah Grebing's avatar Sarah Grebing

Interim

parent a8009ced
Pipeline #10724 failed with stage
in 2 minutes and 25 seconds
...@@ -16,7 +16,7 @@ ...@@ -16,7 +16,7 @@
<developers> <developers>
<developer> <developer>
<name>Sarah Grebing</name> <name>Sarah Grebing</name>
<email>sarah.grebing@ira.uka.de</email> <email>sarah.grebing@kit.edu</email>
<organization>Karlruhe Institute of Technology</organization> <organization>Karlruhe Institute of Technology</organization>
</developer> </developer>
...@@ -141,7 +141,21 @@ ...@@ -141,7 +141,21 @@
<artifactId>key.core</artifactId> <artifactId>key.core</artifactId>
<version>2.7</version> <version>2.7</version>
<scope>system</scope> <scope>system</scope>
<systemPath>${basedir}/lib/key.core.jar</systemPath> <systemPath>${basedir}/lib/components/key.core.jar</systemPath>
</dependency>
<dependency>
<groupId>org.key-project</groupId>
<artifactId>key.ui</artifactId>
<version>2.7</version>
<scope>system</scope>
<systemPath>${basedir}/lib/components/key.ui.jar</systemPath>
</dependency>
<dependency>
<groupId>org.key-project</groupId>
<artifactId>key.util</artifactId>
<version>2.7</version>
<scope>system</scope>
<systemPath>${basedir}/lib/components/key.util.jar</systemPath>
</dependency> </dependency>
<dependency> <dependency>
<groupId>org.antlr</groupId> <groupId>org.antlr</groupId>
......
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.EngineState;
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;
import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.Visitor;
import edu.kit.formal.proofscriptparser.ast.*; import edu.kit.formal.proofscriptparser.ast.*;
import lombok.Getter; import lombok.Getter;
import lombok.Setter; import lombok.Setter;
import org.antlr.v4.runtime.ParserRuleContext;
import java.util.*; import java.util.*;
import java.util.logging.Logger; import java.util.logging.Logger;
...@@ -22,10 +21,9 @@ import java.util.logging.Logger; ...@@ -22,10 +21,9 @@ import java.util.logging.Logger;
public class Interpreter extends DefaultASTVisitor<Void> public class Interpreter extends DefaultASTVisitor<Void>
implements ScopeObservable { implements ScopeObservable {
private static final int MAX_ITERATIONS = 5; private static final int MAX_ITERATIONS = 5;
private static Logger logger = Logger.getLogger("interpreter");
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes) //TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
private Stack<AbstractState> stateStack = new Stack<>(); private Stack<AbstractState> stateStack = new Stack<>();
private static Logger logger = Logger.getLogger("interpreter");
@Getter @Getter
private List<Visitor> entryListeners = new ArrayList<>(), private List<Visitor> entryListeners = new ArrayList<>(),
exitListeners = new ArrayList<>(); exitListeners = new ArrayList<>();
...@@ -248,15 +246,28 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -248,15 +246,28 @@ public class Interpreter extends DefaultASTVisitor<Void>
* *
* @param matchExpression * @param matchExpression
* @param goal * @param goal
* @return * @return null, if match was false, return teh first Assignment when match was true
*/ */
private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode goal) { private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode goal) {
enterScope(matchExpression); enterScope(matchExpression);
Evaluator eval = new Evaluator(goal.getAssignments(), goal); MatchEvaluator mEval = new MatchEvaluator(goal.getAssignments(), goal, matcherApi);
mEval.getEntryListeners().addAll(entryListeners);
mEval.getExitListeners().addAll(exitListeners);
exitScope(matchExpression);
List<VariableAssignment> matchResult = mEval.eval(matchExpression);
if (matchResult.isEmpty()) {
return null;
} else {
return matchResult.get(0);
}
/*Evaluator eval = new Evaluator(goal.getAssignments(), goal);
eval.setMatcher(matcherApi); eval.setMatcher(matcherApi);
eval.getEntryListeners().addAll(entryListeners); eval.getEntryListeners().addAll(entryListeners);
eval.getExitListeners().addAll(exitListeners); eval.getExitListeners().addAll(exitListeners);
exitScope(matchExpression); exitScope(matchExpression);
Value v = eval.eval(matchExpression); Value v = eval.eval(matchExpression);
if (v.getData().equals(Value.TRUE)) { if (v.getData().equals(Value.TRUE)) {
if (eval.getMatchedVariables().size() == 0) { if (eval.getMatchedVariables().size() == 0) {
...@@ -265,7 +276,7 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -265,7 +276,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
return eval.getMatchedVariables().get(0); return eval.getMatchedVariables().get(0);
} }
} }
return null; return null;*/
} }
/** /**
...@@ -298,12 +309,12 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -298,12 +309,12 @@ public class Interpreter extends DefaultASTVisitor<Void>
* @param caseStatement * @param caseStatement
* @return * @return
*/ */
@Override /* @Override
public Void visit(CaseStatement caseStatement) { public Void visit(CaseStatement caseStatement) {
enterScope(caseStatement); enterScope(caseStatement);
exitScope(caseStatement); exitScope(caseStatement);
return null; return null;
} }*/
/** /**
* Visiting a call statement results in: * Visiting a call statement results in:
...@@ -428,12 +439,7 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -428,12 +439,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
return getCurrentGoals().get(0); return getCurrentGoals().get(0);
} }
} }
/* @Override
public T visit(Parameters parameters) {
parameters.entrySet();
System.out.println("Params " + parameters.toString());
return null;
}*/
public AbstractState getCurrentState() { public AbstractState getCurrentState() {
return stateStack.peek(); return stateStack.peek();
...@@ -484,5 +490,7 @@ public class Interpreter extends DefaultASTVisitor<Void> ...@@ -484,5 +490,7 @@ public class Interpreter extends DefaultASTVisitor<Void>
public ScriptApi getScriptApi() { public ScriptApi getScriptApi() {
return scriptApi; return scriptApi;
} }
//endregion //endregion
} }
package edu.kit.formal.interpreter; package edu.kit.formal.interpreter;
import de.uka.ilkd.key.api.*;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
import edu.kit.formal.interpreter.funchdl.BuiltinCommands; import edu.kit.formal.interpreter.funchdl.BuiltinCommands;
import edu.kit.formal.interpreter.funchdl.CommandLookup;
import edu.kit.formal.interpreter.funchdl.DefaultLookup; import edu.kit.formal.interpreter.funchdl.DefaultLookup;
import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
import java.io.File; import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.util.HashMap;
import java.util.List; import java.util.List;
import java.util.Map;
/** /**
* Test Main, will be replaced * Test Main, will be replaced
*/ */
public class Main { public class Main {
static ProofManagementApi api;
//This hard coded link is only for the first testing will be removed later on //This hard coded link is only for the first testing will be removed later on
private static File testFile = new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/proofscriptparser/scripts/test.txt"); private static File testFile = new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/proofscriptparser/scripts/test.txt");
private static File testFile1 = new File("/home/sarah/Documents/KIT_Mitarbeiter/ProofScriptingLanguage/src/test/resources/edu/kit/formal/proofscriptparser/scripts/contraposition.key");
public static void main(String[] args) { public static void main(String[] args) {
try {
System.out.println(testFile1.exists());
api = KeYApi.loadFromKeyFile(testFile1);
ProofApi papi = api.getLoadedProof();
ScriptApi scrapi = papi.getScriptApi();
System.out.println(papi.getFirstOpenGoal().getSequent().toString());
ProjectedNode openGoal = papi.getFirstOpenGoal();
RuleCommand rc = (RuleCommand) KeYApi.getScriptCommandApi().getScriptCommands("rule");
Map cArgs = new HashMap();
VariableAssignments va = new VariableAssignments();
cArgs.put("#2", "impRight");
ProofScriptCommandCall impRight = scrapi.instantiateCommand(rc, cArgs);
scrapi.executeScriptCommand(impRight, openGoal, va);
VariableAssignments va2 = new VariableAssignments(va);
va2.addType("X", VariableAssignments.VarType.FORMULA);
va2.addType("Y", VariableAssignments.VarType.FORMULA);
List<VariableAssignments> matches = scrapi.matchPattern("==> X -> Y", openGoal.getSequent(), va2);
for (VariableAssignments match : matches) {
System.out.println(match);
}
if (matches.isEmpty()) {
System.out.println("No match found");
} else {
List<VariableAssignments> matches2 = scrapi.matchPattern("==> X -> Y", openGoal.getSequent(), va2);
}
} catch (ProblemLoaderException e) {
System.out.println("Could not load file");
e.printStackTrace();
} catch (Exception e) {
e.printStackTrace();
}
//Erzeuge Parser //Erzeuge Parser
//lese P ein //lese P ein
//Erzeuge Interpreter //Erzeuge Interpreter
......
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