Commit 3890f721 authored by Alexander Weigl's avatar Alexander Weigl
Browse files

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

* 'master' of git.scc.kit.edu:xt9634/ProofScriptParser:
  BUGFIX IndexOutOfRange+NullPointerExc
  merge
  Bugfix for emptyMatch on sequent
parents 74bfe221 183a4cdd
Pipeline #12996 failed with stage
in 2 minutes and 37 seconds
...@@ -112,10 +112,14 @@ public class ScriptArea extends CodeArea { ...@@ -112,10 +112,14 @@ public class ScriptArea extends CodeArea {
textProperty().addListener((prop, oldValue, newValue) -> { textProperty().addListener((prop, oldValue, newValue) -> {
dirty.set(true); dirty.set(true);
updateMainScriptMarker(); if (newValue.isEmpty()) {
updateHighlight(); System.err.println("text cleared");
highlightProblems(); } else {
highlightNonExecutionArea(); updateMainScriptMarker();
updateHighlight();
highlightProblems();
highlightNonExecutionArea();
}
}); });
...@@ -192,13 +196,14 @@ public class ScriptArea extends CodeArea { ...@@ -192,13 +196,14 @@ public class ScriptArea extends CodeArea {
clearStyle(0, newValue.length()); clearStyle(0, newValue.length());
StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue); StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue);
if (spans != null) setStyleSpans(0, spans); if (spans != null) setStyleSpans(0, spans);
markedRegions.forEach(reg -> {
Collection<String> list = new HashSet<>();
list.add(reg.clazzName);
setStyle(reg.start, reg.stop, list);
});
} }
markedRegions.forEach(reg -> {
Collection<String> list = new HashSet<>();
list.add(reg.clazzName);
setStyle(reg.start, reg.stop, list);
});
} }
private void highlightProblems() { private void highlightProblems() {
......
...@@ -289,9 +289,10 @@ public class ScriptController { ...@@ -289,9 +289,10 @@ public class ScriptController {
private ScriptArea.RegionStyle asRegion(ASTNode node) { private ScriptArea.RegionStyle asRegion(ASTNode node) {
assert node != null; assert node != null;
if (node.getRuleContext() != null)
return new ScriptArea.RegionStyle(node.getRuleContext().getStart().getStartIndex(), return new ScriptArea.RegionStyle(node.getRuleContext().getStart().getStartIndex(),
node.getRuleContext().getStop().getStopIndex(), clazzName); node.getRuleContext().getStop().getStopIndex(), clazzName);
else return new ScriptArea.RegionStyle(0, 1, "");
} }
} }
} }
...@@ -106,7 +106,7 @@ public class ProofTreeController { ...@@ -106,7 +106,7 @@ public class ProofTreeController {
//set value of newly computed node //set value of newly computed node
nextComputedNode.setValue(nodeAddedEvent.getAddedNode()); nextComputedNode.setValue(nodeAddedEvent.getAddedNode());
//setNewState(this.statePointer.getState()); //setNewState(this.statePointer.getState());
//Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt())); Events.fire(new Events.NewNodeExecuted(nodeAddedEvent.getAddedNode().getScriptstmt()));
} }
}; };
......
...@@ -47,6 +47,13 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -47,6 +47,13 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return scripts; return scripts;
} }
@Override
public List<ProofScript> visitStart(ScriptLanguageParser.StartContext ctx) {
ctx.script().forEach(s ->
scripts.add((ProofScript) s.accept(this)));
return scripts;
}
@Override @Override
public ProofScript visitScript(ScriptLanguageParser.ScriptContext ctx) { public ProofScript visitScript(ScriptLanguageParser.ScriptContext ctx) {
ProofScript s = new ProofScript(); ProofScript s = new ProofScript();
...@@ -58,13 +65,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -58,13 +65,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return s; return s;
} }
@Override
public List<ProofScript> visitStart(ScriptLanguageParser.StartContext ctx) {
ctx.script().forEach(s ->
scripts.add((ProofScript) s.accept(this)));
return scripts;
}
@Override @Override
public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) { public Signature visitArgList(ScriptLanguageParser.ArgListContext ctx) {
Signature signature = new Signature(); Signature signature = new Signature();
...@@ -72,6 +72,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -72,6 +72,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
signature.put(new Variable(decl.name), signature.put(new Variable(decl.name),
TypeFacade.findType(decl.type.getText())); TypeFacade.findType(decl.type.getText()));
} }
signature.setRuleContext(ctx);
return signature; return signature;
} }
...@@ -133,12 +134,9 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -133,12 +134,9 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return be; return be;
} }
private UnaryExpression createUnaryExpression(ParserRuleContext ctx, ScriptLanguageParser.ExpressionContext expression, Operator op) { @Override
UnaryExpression ue = new UnaryExpression(); public Object visitExprNot(ScriptLanguageParser.ExprNotContext ctx) {
ue.setRuleContext(ctx); return createUnaryExpression(ctx, ctx.expression(), Operator.NOT);
ue.setExpression((Expression<ParserRuleContext>) expression.accept(this));
ue.setOperator(op);
return ue;
} }
@Override @Override
...@@ -146,9 +144,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -146,9 +144,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return createUnaryExpression(ctx, ctx.expression(), Operator.NEGATE); return createUnaryExpression(ctx, ctx.expression(), Operator.NEGATE);
} }
@Override private UnaryExpression createUnaryExpression(ParserRuleContext ctx, ScriptLanguageParser.ExpressionContext expression, Operator op) {
public Object visitExprNot(ScriptLanguageParser.ExprNotContext ctx) { UnaryExpression ue = new UnaryExpression();
return createUnaryExpression(ctx, ctx.expression(), Operator.NOT); ue.setRuleContext(ctx);
ue.setExpression((Expression<ParserRuleContext>) expression.accept(this));
ue.setOperator(op);
return ue;
} }
@Override @Override
...@@ -214,15 +215,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -214,15 +215,6 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return ctx.literals().accept(this); return ctx.literals().accept(this);
} }
@Override
public Object visitExprDivision(ScriptLanguageParser.ExprDivisionContext ctx) {
return createBinaryExpression(ctx, ctx.expression(), Operator.DIVISION);
}
//TODO implement
@Override @Override
public Object visitExprSubst(ScriptLanguageParser.ExprSubstContext ctx) { public Object visitExprSubst(ScriptLanguageParser.ExprSubstContext ctx) {
SubstituteExpression se = new SubstituteExpression(); SubstituteExpression se = new SubstituteExpression();
...@@ -232,6 +224,14 @@ public class TransformAst implements ScriptLanguageVisitor<Object> { ...@@ -232,6 +224,14 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return se; return se;
} }
//TODO implement
@Override
public Object visitExprDivision(ScriptLanguageParser.ExprDivisionContext ctx) {
return createBinaryExpression(ctx, ctx.expression(), Operator.DIVISION);
}
@Override @Override
public Map<String, Expression> visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) { public Map<String, Expression> visitSubstExpressionList(ScriptLanguageParser.SubstExpressionListContext ctx) {
Map<String, Expression> map = new LinkedHashMap<>(); Map<String, Expression> map = new LinkedHashMap<>();
......
...@@ -4,6 +4,7 @@ import de.uka.ilkd.key.logic.SequentFormula; ...@@ -4,6 +4,7 @@ import de.uka.ilkd.key.logic.SequentFormula;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import org.antlr.v4.runtime.CommonToken; import org.antlr.v4.runtime.CommonToken;
import org.apache.commons.lang.NotImplementedException; import org.apache.commons.lang.NotImplementedException;
import org.key_project.util.collection.ImmutableArray;
import java.util.*; import java.util.*;
import java.util.stream.IntStream; import java.util.stream.IntStream;
...@@ -19,6 +20,8 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -19,6 +20,8 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
static final Matchings NO_MATCH = new Matchings(); static final Matchings NO_MATCH = new Matchings();
static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null); static final Matchings EMPTY_MATCH = Matchings.singleton("EMPTY_MATCH", null);
private Stack<Term> termStack = new Stack<>();
protected static List<MatchInfo> reduceConform(List<MatchInfo> m1, List<MatchInfo> m2) { protected static List<MatchInfo> reduceConform(List<MatchInfo> m1, List<MatchInfo> m2) {
if (m1 == null || m2 == null) return null; //"null" is equivalent to NO_MATCH if (m1 == null || m2 == null) return null; //"null" is equivalent to NO_MATCH
...@@ -56,6 +59,58 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -56,6 +59,58 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
return h3; return h3;
} }
/*@Override
protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) {
if (peek != null) {
return EMPTY_MATCH;
} else {
return NO_MATCH;
}
}*/
/**
* Reduce the matchings by eliminating non-compatible matchings.
* For example:
* m1: <X, f(y)>, <Y,g> and m2: <X, g> <Y, f(x)>
*
* @param m1
* @param m2
* @return
*/
protected static Matchings reduceConform(Matchings m1, Matchings m2) {
//shortcuts
if (m1 == NO_MATCH || m2 == NO_MATCH) return NO_MATCH;
if (m1 == EMPTY_MATCH) return m2;
if (m2 == EMPTY_MATCH) return m1;
Matchings m3 = new Matchings();
boolean oneMatch = false;
for (HashMap<String, Term> h1 : m1) {
for (HashMap<String, Term> h2 : m2) {
HashMap<String, Term> h3 = reduceConform(h1, h2);
if (h3 != null) {
m3.add(h3);
oneMatch = true;
}
}
}
return oneMatch ? m3 : NO_MATCH;
}
/**
* Visit a semisequent pattern f(x), f(y)
*
* @param ctx
* @param peek
* @return
*/
@Override
protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, Term peek) {
return null;
}
/** /**
* Visit '_' * Visit '_'
* *
...@@ -72,15 +127,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -72,15 +127,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
} }
} }
/*@Override
protected Matchings visitStartDontCare(MatchPatternParser.StarDontCareContext ctx, Term peek) {
if (peek != null) {
return EMPTY_MATCH;
} else {
return NO_MATCH;
}
}*/
/** /**
* Visit a Schema Variable * Visit a Schema Variable
* *
...@@ -114,74 +160,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -114,74 +160,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
return m; return m;
} }
protected Matchings visitBinaryOperation(String keyOpName, MatchPatternParser.TermPatternContext right, MatchPatternParser.TermPatternContext left, Term peek) {
MatchPatternParser.FunctionContext func = new MatchPatternParser.FunctionContext(left);
func.func = new CommonToken(MatchPatternLexer.ID, keyOpName);
func.termPattern().add(left);
func.termPattern().add(right);
return accept(func, peek);
}
private String convert(int op) {
switch (op) {
case MatchPatternParser.PLUS:
return "add";
case MatchPatternParser.MINUS:
return "sub";
case MatchPatternParser.MUL:
return "mul";
case MatchPatternParser.DIV:
return "div";
case MatchPatternParser.LE:
return "lt";
case MatchPatternParser.LEQ:
return "leq";
case MatchPatternParser.EQ:
return "equals";
case MatchPatternParser.GE:
return "gt";
case MatchPatternParser.GEQ:
return "geq";
case MatchPatternParser.IMP:
return "imp";
case MatchPatternParser.AND:
return "and";
case MatchPatternParser.OR:
return "or";
default:
throw new UnsupportedOperationException("The operator " + op + "is not known");
}
}
/**
* Reduce the matchings by eliminating non-compatible matchings.
* For example:
* m1: <X, f(y)>, <Y,g> and m2: <X, g> <Y, f(x)>
*
* @param m1
* @param m2
* @return
*/
protected static Matchings reduceConform(Matchings m1, Matchings m2) {
//shortcuts
if (m1 == NO_MATCH || m2 == NO_MATCH) return NO_MATCH;
if (m1 == EMPTY_MATCH) return m2;
if (m2 == EMPTY_MATCH) return m1;
Matchings m3 = new Matchings();
boolean oneMatch = false;
for (HashMap<String, Term> h1 : m1) {
for (HashMap<String, Term> h2 : m2) {
HashMap<String, Term> h3 = reduceConform(h1, h2);
if (h3 != null) {
m3.add(h3);
oneMatch = true;
}
}
}
return oneMatch ? m3 : NO_MATCH;
}
/** /**
* Visit a function and predicate symbol without a sequent arrow * Visit a function and predicate symbol without a sequent arrow
* *
...@@ -203,22 +181,25 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -203,22 +181,25 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
return NO_MATCH; return NO_MATCH;
} }
/**
* Visit a semisequent pattern f(x), f(y)
*
* @param ctx
* @param peek
* @return
*/
@Override @Override
protected Matchings visitSemiSeqPattern(MatchPatternParser.SemiSeqPatternContext ctx, Term peek) { protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, Term peek) {
return null; //we are at a natural number
if (peek.op().name().toString().equals("Z")) {
ImmutableArray<Term> subs = peek.subs();
int transformedString = transformToNumber(peek.sub(0));
return EMPTY_MATCH;
} else {
return NO_MATCH;
}
} }
@Override private int transformToNumber(Term sub) {
protected Matchings visitNumber(MatchPatternParser.NumberContext ctx, Term peek) { int number = 0;
return null; return 0;
} }
/** /**
...@@ -240,6 +221,66 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> { ...@@ -240,6 +221,66 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
ctx.termPattern(0), ctx.termPattern(1), peek); ctx.termPattern(0), ctx.termPattern(1), peek);
} }
protected Matchings visitBinaryOperation(String keyOpName, MatchPatternParser.TermPatternContext right, MatchPatternParser.TermPatternContext left, Term peek) {
MatchPatternParser.FunctionContext func = new MatchPatternParser.FunctionContext(left);
func.func = new CommonToken(MatchPatternLexer.ID, keyOpName);
func.termPattern().add(left);
func.termPattern().add(right);
return accept(func, peek);
}
private String convert(int op) {
switch (op) {
case MatchPatternParser.PLUS:
return "add";
case MatchPatternParser.MINUS:
return "sub";
case MatchPatternParser.MUL:
return "mul";
case MatchPatternParser.DIV:
return "div";
case MatchPatternParser.LE:
return "lt";
case MatchPatternParser.LEQ:
return "leq";
case MatchPatternParser.EQ:
return "equals";
case MatchPatternParser.GE:
return "gt";
case MatchPatternParser.GEQ:
return "geq";
case MatchPatternParser.IMP:
return "imp";
case MatchPatternParser.AND:
return "and";
case MatchPatternParser.OR:
return "or";
default:
throw new UnsupportedOperationException("The operator " + op + "is not known");
}
}
@Override @Override
protected Matchings visitMult(MatchPatternParser.MultContext ctx, Term peek) { protected Matchings visitMult(MatchPatternParser.MultContext ctx, Term peek) {
return visitBinaryOperation("mul", ctx.termPattern(0), ctx.termPattern(1), peek); return visitBinaryOperation("mul", ctx.termPattern(0), ctx.termPattern(1), peek);
......
...@@ -46,17 +46,16 @@ public class MatcherFacadeTest { ...@@ -46,17 +46,16 @@ public class MatcherFacadeTest {
shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]"); shouldMatch("i+j", "add(?X,?Y)", "[{?X=i, ?Y=j}]");
shouldMatch("i+j", "?X+?Y", "[{?X=i, ?Y=j}]"); shouldMatch("i+j", "?X+?Y", "[{?X=i, ?Y=j}]");
shouldMatchForm("p & q", "p & ?X", "[{?X=q}]"); shouldMatchForm("p & q", "p & ?X", "[{?X=q}]");
//shouldMatchForm("p & q", "?X & q", "[{?X=p}]"); shouldMatchForm("p & q", "?X & q", "[{?X=p}]");
//shouldMatch("1*j", "add(1,?Y)", "[{?Y=j}]"); System.out.println(parseKeyTerm("12004"));
shouldMatch("1", "1");
// shouldMatch("1*j", "1 + ?Y", "[]");
//shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]); //shouldMatch("f(a) ==> f(a), f(b)" , "==> f(?X)", [{?X=a}]);
//shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]); //shouldMatch("f(a) ==> f(a), f(b)" , "f(a) ==> f(?X)", [{?X=a}]);
//shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)"); //shouldNotMatch("f(a) ==> f(a), f(b)" , "f(?X) ==> f(?X), f(a)");
//shouldMatch("f(a) ==> f(a), f(b)" , "==>");
//shouldMatch("f(a) ==> f(a), f(b)" , "_ ==> _");
//shouldMatch("f(a) ==> f(a), f(b)" , " ==> _");
//shouldMatch("f(a) ==> f(a), f(b)" , "_ ==> ");
} }
...@@ -163,6 +162,13 @@ public class MatcherFacadeTest { ...@@ -163,6 +162,13 @@ public class MatcherFacadeTest {
shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]"); shouldMatchSeq("==> pred(a)", "==>", "[{EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]"); shouldMatchSeq("pred(a) ==> ", "==>", "[{EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "==>", "[{EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> ", "[{EMPTY_MATCH=null}]");
//these two need to be checked I think
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", "_ ==> _", "[{EMPTY_MATCH=null}, {EMPTY_MATCH=null}]");
shouldMatchSeq("pred(a) ==> pred(a), pred(b)", " ==> _", "[{EMPTY_MATCH=null}, {EMPTY_MATCH=null}]");
} }
private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException { private void shouldMatchSeq(String seq, String seqPattern, String exp) throws ParserException {
......
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