Commit e1fa86bc authored by Sarah Grebing's avatar Sarah Grebing

Merge branch 'master' of git.scc.kit.edu:xt9634/ProofScriptParser

parents 1010040d 77f055d3
Pipeline #14322 failed with stage
in 2 minutes and 39 seconds
...@@ -10,6 +10,8 @@ ...@@ -10,6 +10,8 @@
</content> </content>
<orderEntry type="inheritedJdk" /> <orderEntry type="inheritedJdk" />
<orderEntry type="sourceFolder" forTests="false" /> <orderEntry type="sourceFolder" forTests="false" />
<orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-api:2.6" level="project" />
<orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-core:2.6" level="project" />
<orderEntry type="library" scope="TEST" name="Maven: junit:junit:4.12" level="project" /> <orderEntry type="library" scope="TEST" name="Maven: junit:junit:4.12" level="project" />
<orderEntry type="library" scope="TEST" name="Maven: org.hamcrest:hamcrest-core:1.3" level="project" /> <orderEntry type="library" scope="TEST" name="Maven: org.hamcrest:hamcrest-core:1.3" level="project" />
<orderEntry type="library" scope="PROVIDED" name="Maven: org.projectlombok:lombok:1.16.16" level="project" /> <orderEntry type="library" scope="PROVIDED" name="Maven: org.projectlombok:lombok:1.16.16" level="project" />
...@@ -21,7 +23,7 @@ ...@@ -21,7 +23,7 @@
<orderEntry type="library" name="Maven: org.codehaus.mojo:animal-sniffer-annotations:1.14" level="project" /> <orderEntry type="library" name="Maven: org.codehaus.mojo:animal-sniffer-annotations:1.14" level="project" />
<orderEntry type="library" name="Maven: commons-io:commons-io:2.5" level="project" /> <orderEntry type="library" name="Maven: commons-io:commons-io:2.5" level="project" />
<orderEntry type="library" name="Maven: commons-lang:commons-lang:2.6" level="project" /> <orderEntry type="library" name="Maven: commons-lang:commons-lang:2.6" level="project" />
<orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-api:2.8" level="project" /> <orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-api:2.6" level="project" />
<orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-core:2.8" level="project" /> <orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-core:2.6" level="project" />
</component> </component>
</module> </module>
\ No newline at end of file
# Execute this in this folder. # Execute this in this folder.
# Set to key/key/deployment/components/ # Set to key/key/deployment/components/
COMPONENTS=~/work/key/key/deployment/components/ COMPONENTS=${COMPONENTS:-~/work/key/key/deployment/components/}
mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \ mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \
......
# Execute this in this folder. # Execute this in this folder.
# Set to key/key/deployment/components/ # Set to key/key/deployment/components/
COMPONENTS=~/work/key/key/deployment/components/ COMPONENTS=${COMPONENTS:-~/work/key/key/deployment/components/}
mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \ mvn install:install-file -Dfile=$COMPONENTS/key.core.jar \
......
...@@ -7,17 +7,17 @@ ...@@ -7,17 +7,17 @@
<snapshot> <snapshot>
<localCopy>true</localCopy> <localCopy>true</localCopy>
</snapshot> </snapshot>
<lastUpdated>20170911152346</lastUpdated> <lastUpdated>20170912105152</lastUpdated>
<snapshotVersions> <snapshotVersions>
<snapshotVersion> <snapshotVersion>
<extension>jar</extension> <extension>jar</extension>
<value>2.7-SNAPSHOT</value> <value>2.7-SNAPSHOT</value>
<updated>20170911152346</updated> <updated>20170912105152</updated>
</snapshotVersion> </snapshotVersion>
<snapshotVersion> <snapshotVersion>
<extension>pom</extension> <extension>pom</extension>
<value>2.7-SNAPSHOT</value> <value>2.7-SNAPSHOT</value>
<updated>20170911152346</updated> <updated>20170912103022</updated>
</snapshotVersion> </snapshotVersion>
</snapshotVersions> </snapshotVersions>
</versioning> </versioning>
......
...@@ -6,6 +6,6 @@ ...@@ -6,6 +6,6 @@
<versions> <versions>
<version>2.7-SNAPSHOT</version> <version>2.7-SNAPSHOT</version>
</versions> </versions>
<lastUpdated>20170911152346</lastUpdated> <lastUpdated>20170912105152</lastUpdated>
</versioning> </versioning>
</metadata> </metadata>
...@@ -7,17 +7,17 @@ ...@@ -7,17 +7,17 @@
<snapshot> <snapshot>
<localCopy>true</localCopy> <localCopy>true</localCopy>
</snapshot> </snapshot>
<lastUpdated>20170911152349</lastUpdated> <lastUpdated>20170912105155</lastUpdated>
<snapshotVersions> <snapshotVersions>
<snapshotVersion> <snapshotVersion>
<extension>jar</extension> <extension>jar</extension>
<value>2.7-SNAPSHOT</value> <value>2.7-SNAPSHOT</value>
<updated>20170911152349</updated> <updated>20170912105155</updated>
</snapshotVersion> </snapshotVersion>
<snapshotVersion> <snapshotVersion>
<extension>pom</extension> <extension>pom</extension>
<value>2.7-SNAPSHOT</value> <value>2.7-SNAPSHOT</value>
<updated>20170911152349</updated> <updated>20170912103024</updated>
</snapshotVersion> </snapshotVersion>
</snapshotVersions> </snapshotVersions>
</versioning> </versioning>
......
...@@ -6,6 +6,6 @@ ...@@ -6,6 +6,6 @@
<versions> <versions>
<version>2.7-SNAPSHOT</version> <version>2.7-SNAPSHOT</version>
</versions> </versions>
<lastUpdated>20170911152349</lastUpdated> <lastUpdated>20170912105155</lastUpdated>
</versioning> </versioning>
</metadata> </metadata>
...@@ -7,17 +7,17 @@ ...@@ -7,17 +7,17 @@
<snapshot> <snapshot>
<localCopy>true</localCopy> <localCopy>true</localCopy>
</snapshot> </snapshot>
<lastUpdated>20170911152351</lastUpdated> <lastUpdated>20170912105158</lastUpdated>
<snapshotVersions> <snapshotVersions>
<snapshotVersion> <snapshotVersion>
<extension>jar</extension> <extension>jar</extension>
<value>2.7-SNAPSHOT</value> <value>2.7-SNAPSHOT</value>
<updated>20170911152351</updated> <updated>20170912105158</updated>
</snapshotVersion> </snapshotVersion>
<snapshotVersion> <snapshotVersion>
<extension>pom</extension> <extension>pom</extension>
<value>2.7-SNAPSHOT</value> <value>2.7-SNAPSHOT</value>
<updated>20170911152351</updated> <updated>20170912103027</updated>
</snapshotVersion> </snapshotVersion>
</snapshotVersions> </snapshotVersions>
</versioning> </versioning>
......
...@@ -6,6 +6,6 @@ ...@@ -6,6 +6,6 @@
<versions> <versions>
<version>2.7-SNAPSHOT</version> <version>2.7-SNAPSHOT</version>
</versions> </versions>
<lastUpdated>20170911152351</lastUpdated> <lastUpdated>20170912105158</lastUpdated>
</versioning> </versioning>
</metadata> </metadata>
...@@ -7,6 +7,6 @@ ...@@ -7,6 +7,6 @@
<versions> <versions>
<version>2.7</version> <version>2.7</version>
</versions> </versions>
<lastUpdated>20170911152354</lastUpdated> <lastUpdated>20170912105201</lastUpdated>
</versioning> </versioning>
</metadata> </metadata>
...@@ -19,9 +19,26 @@ import java.util.stream.Collectors; ...@@ -19,9 +19,26 @@ import java.util.stream.Collectors;
* @version 1 (11.09.17) * @version 1 (11.09.17)
*/ */
public class GenDoc { public class GenDoc {
private static final Set<String> FORBBIDEN = new TreeSet<>();
static {
FORBBIDEN.add("exit");
FORBBIDEN.add("focus");
FORBBIDEN.add("javascript");
FORBBIDEN.add("leave");
FORBBIDEN.add("let \n");
/*TODO
script
schemaVar
select
set
skip
*/
}
private static File basedir = new File(".."); private static File basedir = new File("..");
private static File propertiesFile = new File(basedir, "rt-key/src/main/resources/edu/kit/iti/formal/psdbg/taclets.properties.xml"); private static File propertiesFile = new File(basedir, "rt-key/src/main/resources/edu/kit/iti/formal/psdbg/taclets.properties.xml");
private static File dummyFile = new File(basedir, "rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key"); private static File dummyFile = new File(".", "rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/contraposition.key");
private static File websiteDoc = new File(basedir, "website/docs/"); private static File websiteDoc = new File(basedir, "website/docs/");
...@@ -58,7 +75,7 @@ public class GenDoc { ...@@ -58,7 +75,7 @@ public class GenDoc {
"\n\nCovering the *default* taclets of [KeY](http://key-project.org)."); "\n\nCovering the *default* taclets of [KeY](http://key-project.org).");
for (Taclet t : taclets) { for (Taclet t : taclets) {
stream.write("\n\n## ${t.displayName()}\n\n"); stream.write("\n\n## " + t.displayName() + "\n\n");
stream.write("```\n" + t.toString() + "\n```"); stream.write("```\n" + t.toString() + "\n```");
} }
...@@ -143,7 +160,8 @@ public class GenDoc { ...@@ -143,7 +160,8 @@ public class GenDoc {
commands.sort(Comparator.comparing(ProofScriptCommand::getName)); commands.sort(Comparator.comparing(ProofScriptCommand::getName));
for (ProofScriptCommand t : commands) { for (ProofScriptCommand t : commands) {
stream.write(helpForCommand(t) + "\n\n"); if (!FORBBIDEN.contains(t.getName()))
stream.write(helpForCommand(t) + "\n\n");
} }
stream.close(); stream.close();
} catch (IOException e) { } catch (IOException e) {
......
...@@ -69,8 +69,8 @@ expression ...@@ -69,8 +69,8 @@ expression
substExpressionList substExpressionList
: :
(scriptVar '/' expression (scriptVar '\\' expression
(',' scriptVar '/' expression)* (',' scriptVar '\\' expression)*
)? )?
; ;
......
...@@ -41,6 +41,10 @@ import java.util.Map; ...@@ -41,6 +41,10 @@ import java.util.Map;
* @version 1 (27.04.17) * @version 1 (27.04.17)
*/ */
public class TransformAst implements ScriptLanguageVisitor<Object> { public class TransformAst implements ScriptLanguageVisitor<Object> {
/**
* Start Index for positional arguments for command calls
*/
public static final int KEY_START_INDEX_PARAMETER = 2;
private List<ProofScript> scripts = new ArrayList<>(10); private List<ProofScript> scripts = new ArrayList<>(10);
...@@ -380,7 +384,9 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -380,7 +384,9 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override @Override
public Object visitParameters(ScriptLanguageParser.ParametersContext ctx) { public Object visitParameters(ScriptLanguageParser.ParametersContext ctx) {
Parameters params = new Parameters(); Parameters params = new Parameters();
int i = 1;
int i = KEY_START_INDEX_PARAMETER;
for (ScriptLanguageParser.ParameterContext pc : ctx.parameter()) { for (ScriptLanguageParser.ParameterContext pc : ctx.parameter()) {
Expression expr = (Expression) pc.expr.accept(this); Expression expr = (Expression) pc.expr.accept(this);
Variable key = pc.pname != null ? new Variable(pc.pname) : new Variable("#" + (i++)); Variable key = pc.pname != null ? new Variable(pc.pname) : new Variable("#" + (i++));
......
...@@ -5,6 +5,7 @@ import lombok.Data; ...@@ -5,6 +5,7 @@ import lombok.Data;
import lombok.NoArgsConstructor; import lombok.NoArgsConstructor;
import java.util.ArrayList; import java.util.ArrayList;
import java.util.Arrays;
import java.util.List; import java.util.List;
/** /**
...@@ -17,6 +18,10 @@ import java.util.List; ...@@ -17,6 +18,10 @@ import java.util.List;
public class TermType implements Type { public class TermType implements Type {
private List<Type> argTypes = new ArrayList<>(); private List<Type> argTypes = new ArrayList<>();
public TermType(Type... sortType) {
this(Arrays.asList(sortType));
}
@Override @Override
public String symbol() { public String symbol() {
return "Term<" + return "Term<" +
......
...@@ -31,7 +31,7 @@ termPattern : ...@@ -31,7 +31,7 @@ termPattern :
| termPattern OR termPattern #or | termPattern OR termPattern #or
| termPattern IMP termPattern #impl | termPattern IMP termPattern #impl
| termPattern XOR termPattern #xor | termPattern XOR termPattern #xor
//| termPattern EQUIV termPattern already covered by EQ/NEQ | termPattern EQUIV termPattern #equivalence
| MINUS termPattern #exprNegate | MINUS termPattern #exprNegate
| NOT termPattern #exprNot | NOT termPattern #exprNot
| '(' termPattern ')' bindClause? #exprParen | '(' termPattern ')' bindClause? #exprParen
...@@ -61,6 +61,7 @@ EQ : '=' ; ...@@ -61,6 +61,7 @@ EQ : '=' ;
NEQ : '!=' ; NEQ : '!=' ;
GEQ : '>=' ; GEQ : '>=' ;
LEQ : '<=' ; LEQ : '<=' ;
EQUIV : '<->';
GE : '>' ; GE : '>' ;
LE : '<' ; LE : '<' ;
AND : '&' ; AND : '&' ;
......
...@@ -85,6 +85,7 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi ...@@ -85,6 +85,7 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
return visitPlusMinus(ctx, stack.peek()); return visitPlusMinus(ctx, stack.peek());
} }
protected abstract T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx, S peek); protected abstract T visitPlusMinus(MatchPatternParser.PlusMinusContext ctx, S peek);
@Override @Override
...@@ -164,6 +165,13 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi ...@@ -164,6 +165,13 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
} }
protected abstract T visitEquality(MatchPatternParser.EqualityContext ctx, S peek); protected abstract T visitEquality(MatchPatternParser.EqualityContext ctx, S peek);
@Override
public T visitEquivalence(MatchPatternParser.EquivalenceContext ctx) {
return visitEquivalence(ctx, stack.peek());
}
protected abstract T visitEquivalence(MatchPatternParser.EquivalenceContext ctx, S peek);
} }
......
...@@ -7,6 +7,7 @@ import de.uka.ilkd.key.logic.Term; ...@@ -7,6 +7,7 @@ import de.uka.ilkd.key.logic.Term;
import edu.kit.formal.psdb.termmatcher.MatchPatternLexer; import edu.kit.formal.psdb.termmatcher.MatchPatternLexer;
import edu.kit.formal.psdb.termmatcher.MatchPatternParser; import edu.kit.formal.psdb.termmatcher.MatchPatternParser;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath; import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
import static edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade.*;
import lombok.Getter; import lombok.Getter;
import lombok.Setter; import lombok.Setter;
import org.antlr.v4.runtime.CommonToken; import org.antlr.v4.runtime.CommonToken;
...@@ -17,8 +18,6 @@ import java.util.stream.Collectors; ...@@ -17,8 +18,6 @@ import java.util.stream.Collectors;
import java.util.stream.IntStream; import java.util.stream.IntStream;
import java.util.stream.Stream; import java.util.stream.Stream;
import static edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade.*;
/** /**
* Matchpattern visitor visits the matchpatterns of case-statements * Matchpattern visitor visits the matchpatterns of case-statements
* *
...@@ -520,6 +519,11 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> { ...@@ -520,6 +519,11 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
return visitBinaryOperation("equals", ctx.termPattern(0), ctx.termPattern(1), peek); return visitBinaryOperation("equals", ctx.termPattern(0), ctx.termPattern(1), peek);
} }
@Override
protected Matchings visitEquivalence(MatchPatternParser.EquivalenceContext ctx, MatchPath peek) {
return visitBinaryOperation("equiv", ctx.termPattern(0), ctx.termPattern(1), peek);
}
private Stream<MatchPath.MPTerm> subTerms(MatchPath.MPTerm peek) { private Stream<MatchPath.MPTerm> subTerms(MatchPath.MPTerm peek) {
ArrayList<MatchPath.MPTerm> list = new ArrayList<>(); ArrayList<MatchPath.MPTerm> list = new ArrayList<>();
subTerms(list, peek); subTerms(list, peek);
......
package edu.kit.iti.formal.psdbg.termmatcher;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.Equality;
import de.uka.ilkd.key.logic.op.Junctor;
import de.uka.ilkd.key.logic.op.Operator;
public class Utils {
/**
* Rewrite toString() representation of Term to a parsable version
*
* @param formula
* @return parsable Stringversion of Term
*/
@Deprecated
public static String toPrettyTerm(Term formula) {
StringBuilder sb = new StringBuilder();
Operator op = formula.op();
//ugly if/else
if (op.equals(Junctor.IMP)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") -> (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Junctor.AND)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") && (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Junctor.OR)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") || (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Equality.EQV)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") <-> (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Equality.EQUALS)) {
sb.append("(" + toPrettyTerm(formula.sub(0)) + ") == (" + toPrettyTerm(formula.sub(1)) + ")");
} else {
if (op.equals(Junctor.NOT)) {
sb.append("(!" + toPrettyTerm(formula.sub(0)) + ")");
} else {
sb.append(formula.toString());
}
}
}
}
}
}
return sb.toString();
}
}
...@@ -216,7 +216,9 @@ public class MatcherFacadeTest { ...@@ -216,7 +216,9 @@ public class MatcherFacadeTest {
"fint2(1,2), fint2(2,3), !p ==> pred(a), p", "fint2(1,2), fint2(2,3), !p ==> pred(a), p",
"fint2(1, ?X), fint2(?X, ?Y) ==> p", "fint2(1, ?X), fint2(?X, ?Y) ==> p",
"[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]"); "[{EMPTY_MATCH=null, ?X=Z(2(#)), ?Y=Z(3(#))}]");
shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X= h2(2,3)}]"); shouldMatchSeq("2 >= 1, h2(1,2) = h2(2,3), h2(2,3) = 0 ==> p, !p", "?X=0 ==>", "[{?X=h2(Z(2(#)),Z(3(#)))}]");
shouldMatchSeq("pred(a) <-> pred(b), pred(a), pred(b) ==> p", "?X <-> ?Y ==> ", "[{?X=pred(a), ?Y=pred(b)}]");
} }
private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException { private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException {
......
...@@ -50,6 +50,7 @@ ...@@ -50,6 +50,7 @@
<project.build.sourceEncoding>UTF-8</project.build.sourceEncoding> <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
<maven.compiler.target>1.8</maven.compiler.target> <maven.compiler.target>1.8</maven.compiler.target>
<maven.compiler.source>1.8</maven.compiler.source> <maven.compiler.source>1.8</maven.compiler.source>
<skipTests>true</skipTests>
</properties> </properties>
<modules> <modules>
...@@ -218,13 +219,13 @@ ...@@ -218,13 +219,13 @@
<dependency> <dependency>
<groupId>org.apache.logging.log4j</groupId> <groupId>org.apache.logging.log4j</groupId>
<artifactId>log4j-api</artifactId> <artifactId>log4j-api</artifactId>
<version>2.8</version> <version>2.6</version>
</dependency> </dependency>
<dependency> <dependency>
<groupId>org.apache.logging.log4j</groupId> <groupId>org.apache.logging.log4j</groupId>
<artifactId>log4j-core</artifactId> <artifactId>log4j-core</artifactId>
<version>2.8</version> <version>2.6</version>
</dependency> </dependency>
</dependencies> </dependencies>
......
...@@ -51,7 +51,7 @@ public class InterpreterBuilder { ...@@ -51,7 +51,7 @@ public class InterpreterBuilder {
@Getter @Getter
private ScopeLogger logger; private ScopeLogger logger;
@Getter @Getter
private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmr, pmc); private DefaultLookup lookup = new DefaultLookup(psh, pmh, pmc, pmr);
private KeyInterpreter interpreter = new KeyInterpreter(lookup); private KeyInterpreter interpreter = new KeyInterpreter(lookup);
@Getter @Getter
......
...@@ -3,9 +3,9 @@ package edu.kit.iti.formal.psdbg.interpreter; ...@@ -3,9 +3,9 @@ package edu.kit.iti.formal.psdbg.interpreter;
import de.uka.ilkd.key.api.ScriptApi; import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.api.VariableAssignments; import de.uka.ilkd.key.api.VariableAssignments;
import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.ApplyStrategy; import de.uka.ilkd.key.proof.ApplyStrategy;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
...@@ -15,9 +15,9 @@ import de.uka.ilkd.key.rule.Taclet; ...@@ -15,9 +15,9 @@ import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.SortType;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.ast.Signature; import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.ast.TermLiteral;
import edu.kit.iti.formal.psdbg.parser.ast.Variable; import edu.kit.iti.formal.psdbg.parser.ast.Variable;
import edu.kit.iti.formal.psdbg.parser.data.Value; import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType; import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
...@@ -196,13 +196,46 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -196,13 +196,46 @@ public class KeYMatcher implements MatcherApi<KeyData> {
// System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term); // System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term);
List<VariableAssignment> transformedMatchResults = new ArrayList<>(); List<VariableAssignment> transformedMatchResults = new ArrayList<>();
for (VariableAssignments mResult : keyMatchResult) { for (VariableAssignments mResult : keyMatchResult) {
transformedMatchResults.add(from(mResult)); transformedMatchResults.add(from(mResult, currentState.getData()));
} }
//keyMatchResult.forEach(r -> transformedMatchResults.add(from(r))); //keyMatchResult.forEach(r -> transformedMatchResults.add(from(r)));
return transformedMatchResults; return transformedMatchResults;
} }
/**
* Transforms a KeY Variable Assignment into an assignment for the interpreter
*
* @param keyAssignments
* @param currentState
* @return
*/
public VariableAssignment from(VariableAssignments keyAssignments, KeyData currentState) {
VariableAssignment interpreterAssignments = new VariableAssignment(null);