Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
9f657295
Commit
9f657295
authored
Jan 17, 2018
by
Alexander Weigl
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
qv -> term in matcher
parent
a1064f96
Pipeline
#16940
passed with stages
in 8 minutes and 48 seconds
Changes
10
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
90 additions
and
170 deletions
+90
-170
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java
...a/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java
+13
-9
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java
...ava/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java
+15
-11
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java
...va/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java
+1
-1
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java
...u/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java
+8
-8
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java
...edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java
+3
-1
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
.../kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
+1
-2
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
...java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
+13
-80
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
...edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
+32
-44
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
...kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
+3
-13
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
...va/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
+1
-1
No files found.
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacade.java
View file @
9f657295
package
edu.kit.iti.formal.psdbg.termmatcher
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.Semisequent
;
import
de.uka.ilkd.key.logic.Sequent
;
import
de.uka.ilkd.key.logic.Term
;
...
...
@@ -21,8 +22,8 @@ import org.apache.logging.log4j.Logger;
public
class
MatcherFacade
{
private
static
Logger
logger
=
LogManager
.
getLogger
(
MatcherFacade
.
class
);
public
static
Matchings
matches
(
String
pattern
,
Term
keyTerm
)
{
MatcherImpl
matcher
=
new
MatcherImpl
();
public
static
Matchings
matches
(
String
pattern
,
Term
keyTerm
,
Services
services
)
{
MatcherImpl
matcher
=
new
MatcherImpl
(
services
);
matcher
.
setCatchAll
(
false
);
MatchPatternParser
mpp
=
getParser
(
pattern
);
MatchPatternParser
.
TermPatternContext
ctx
=
mpp
.
termPattern
();
...
...
@@ -50,12 +51,13 @@ public class MatcherFacade {
* @param pattern Semisequent pattern e.g. f(x), f(x)
* @param semiSeq Concrete KeY Semisequent
* @param catchAll
* @param services
* @return Matchings
*/
public
static
Matchings
matches
(
String
pattern
,
Semisequent
semiSeq
,
boolean
catchAll
)
{
public
static
Matchings
matches
(
String
pattern
,
Semisequent
semiSeq
,
boolean
catchAll
,
Services
services
)
{
MatchPatternParser
mpp
=
getParser
(
pattern
);
MatchPatternParser
.
SemiSeqPatternContext
ctx
=
mpp
.
semiSeqPattern
();
MatcherImpl
matcher
=
new
MatcherImpl
();
MatcherImpl
matcher
=
new
MatcherImpl
(
services
);
matcher
.
setCatchAll
(
catchAll
);
Matchings
m
=
matcher
.
accept
(
ctx
,
MatchPathFacade
.
createRoot
(
semiSeq
));
return
m
;
...
...
@@ -67,9 +69,10 @@ public class MatcherFacade {
*
* @param pattern e.g., f(x) ==> f(y)
* @param sequent
* @param services
* @return
*/
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
,
boolean
catchAll
)
{
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
,
boolean
catchAll
,
Services
services
)
{
MatchPatternParser
mpp
=
getParser
(
pattern
);
MatchPatternParser
.
SequentPatternContext
ctx
=
mpp
.
sequentPattern
();
logger
.
info
(
"Matching \n"
+
pattern
+
"\n"
+
sequent
.
toString
());
...
...
@@ -78,21 +81,22 @@ public class MatcherFacade {
return
new
Matchings
();
}
MatcherImpl
matcher
=
new
MatcherImpl
();
MatcherImpl
matcher
=
new
MatcherImpl
(
services
);
matcher
.
setCatchAll
(
catchAll
);
Matchings
m
=
matcher
.
accept
(
ctx
,
MatchPathFacade
.
create
(
sequent
));
return
m
;
}
/**
* Like {@link #matches(String, Sequent)} but allows to use
* Like {@link #matches(String, Sequent
, Services
)} but allows to use
* MatcherImpl#isCatchAll.
*
* @param pattern
* @param sequent
* @param services
* @return
*/
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
)
{
return
matches
(
pattern
,
sequent
,
true
);
public
static
Matchings
matches
(
String
pattern
,
Sequent
sequent
,
Services
services
)
{
return
matches
(
pattern
,
sequent
,
true
,
services
);
}
}
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherImpl.java
View file @
9f657295
package
edu.kit.iti.formal.psdbg.termmatcher
;
import
com.google.common.collect.Sets
;
import
de.uka.ilkd.key.logic.Semisequent
;
import
de.uka.ilkd.key.logic.SequentFormula
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.*
;
import
de.uka.ilkd.key.logic.op.QuantifiableVariable
;
import
edu.kit.formal.psdb.termmatcher.MatchPatternLexer
;
import
edu.kit.formal.psdb.termmatcher.MatchPatternParser
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
static
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
mp
.
MatchPathFacade
.*;
import
lombok.Getter
;
import
lombok.RequiredArgsConstructor
;
import
lombok.Setter
;
import
org.antlr.v4.runtime.CommonToken
;
import
org.antlr.v4.runtime.Token
;
...
...
@@ -20,21 +19,24 @@ import java.util.stream.Collectors;
import
java.util.stream.IntStream
;
import
java.util.stream.Stream
;
import
static
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
mp
.
MatchPathFacade
.*;
/**
* Matchpattern visitor visits the matchpatterns of case-statements
*
* @author Alexander Weigl
* @author S. Grebing
*/
@RequiredArgsConstructor
class
MatcherImpl
extends
MatchPatternDualVisitor
<
Matchings
,
MatchPath
>
{
static
final
Matchings
NO_MATCH
=
new
Matchings
();
static
final
Matchings
EMPTY_MATCH
=
Matchings
.
singleton
(
"EMPTY_MATCH"
,
null
);
static
final
Map
<
String
,
MatchPath
>
EMPTY_VARIABLE_ASSIGNMENT
=
EMPTY_MATCH
.
first
();
@Getter
private
final
Services
services
;
Random
random
=
new
Random
(
42L
);
/*
* Reduce two matchinfos
*
...
...
@@ -67,7 +69,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
*/
private
List
<
Integer
>
currentPosition
=
new
ArrayList
<>();
/**
* If true, we assume every term in the pattern has a binder.
* The binding names are generated.
...
...
@@ -466,7 +467,12 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
continue
;
}
if
(
qfPattern
.
getType
()
==
MatchPatternLexer
.
SID
)
{
match
=
reduceConform
(
match
,
Matchings
.
singleton
(
qfPattern
.
getText
(),
new
MatchPath
.
MPQuantifiableVariable
(
peek
,
qv
,
i
)));
TermFactory
tf
=
new
TermFactory
(
new
HashMap
<>());
TermBuilder
tb
=
new
TermBuilder
(
tf
,
services
);
Term
termQVariable
=
tb
.
var
(
qv
);
match
=
reduceConform
(
match
,
Matchings
.
singleton
(
qfPattern
.
getText
(),
new
MatchPath
.
MPTerm
(
peek
,
termQVariable
,
-
i
)));
}
else
{
if
(!
qv
.
name
().
toString
().
equals
(
qfPattern
.
getText
()))
{
return
NO_MATCH
;
...
...
@@ -555,8 +561,6 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
@Override
public
Matchings
visitExprParen
(
MatchPatternParser
.
ExprParenContext
ctx
,
MatchPath
peek
)
{
return
handleBindClause
(
ctx
.
bindClause
(),
peek
,
accept
(
ctx
.
termPattern
(),
peek
));
...
...
@@ -615,7 +619,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, MatchPath> {
}
public
int
getRandomNumber
()
{
return
random
.
nextInt
();
return
Math
.
abs
(
random
.
nextInt
()
)
;
}
}
/* private Matchings reduceConformQuant(Matchings fromTerm, Matchings match) {
...
...
matcher/src/main/java/edu/kit/iti/formal/psdbg/termmatcher/mp/MatchPath.java
View file @
9f657295
...
...
@@ -75,7 +75,7 @@ public abstract class MatchPath<T, P> {
}
public
static
class
MPTerm
extends
MatchPath
<
Term
,
Object
>
{
MPTerm
(
MatchPath
<?
extends
Object
,
?>
parent
,
Term
unit
,
int
pos
)
{
public
MPTerm
(
MatchPath
<?
extends
Object
,
?>
parent
,
Term
unit
,
int
pos
)
{
super
(
parent
,
unit
,
pos
);
}
...
...
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/MatcherFacadeTest.java
View file @
9f657295
...
...
@@ -123,26 +123,26 @@ public class MatcherFacadeTest {
private
void
shouldMatch
(
String
key
,
String
pattern
)
throws
ParserException
{
Term
term
=
parseKeyTerm
(
key
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
,
services
);
System
.
out
.
println
(
m
);
}
private
void
shouldMatch
(
String
key
,
String
pattern
,
String
exp
)
throws
ParserException
{
Term
term
=
parseKeyTerm
(
key
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
private
void
shouldMatchForm
(
String
form
,
String
pattern
)
throws
ParserException
{
Term
formula
=
parserFormula
(
form
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
,
services
);
System
.
out
.
println
(
m
);
}
private
void
shouldMatchForm
(
String
form
,
String
pattern
,
String
exp
)
throws
ParserException
{
Term
formula
=
parserFormula
(
form
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
formula
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
...
...
@@ -197,14 +197,14 @@ public class MatcherFacadeTest {
private
void
shouldMatchSemiSeq
(
String
s
,
String
s1
,
String
exp
)
throws
ParserException
{
Sequent
term
=
parseSeq
(
s
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
exp
,
m
.
toString
());
}
private
void
shouldMatchSemiSeq
(
String
s
,
String
s1
)
throws
ParserException
{
Sequent
term
=
parseSeq
(
s
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
);
Matchings
m
=
MatcherFacade
.
matches
(
s1
,
term
,
services
);
System
.
out
.
println
(
m
);
}
...
...
@@ -294,7 +294,7 @@ public class MatcherFacadeTest {
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
,
String
exp
)
throws
ParserException
{
Sequent
sequent
=
parseSeq
(
seq
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
,
services
);
System
.
out
.
println
(
m
);
Assert
.
assertEquals
(
removeNumbersInBinders
(
m
),
exp
);
}
...
...
@@ -308,7 +308,7 @@ public class MatcherFacadeTest {
private
void
shouldMatchSeq
(
String
seq
,
String
seqPattern
)
throws
ParserException
{
Sequent
sequent
=
parseSeq
(
seq
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
);
Matchings
m
=
MatcherFacade
.
matches
(
seqPattern
,
sequent
,
services
);
System
.
out
.
println
(
m
);
}
}
\ No newline at end of file
matcher/src/test/java/edu/kit/iti/formal/psdbg/termmatcher/TestUpdateMatch.java
View file @
9f657295
...
...
@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.termmatcher;
import
de.uka.ilkd.key.api.KeYApi
;
import
de.uka.ilkd.key.api.ProofApi
;
import
de.uka.ilkd.key.api.ProofManagementApi
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.Sequent
;
import
de.uka.ilkd.key.proof.init.ProofInputException
;
import
de.uka.ilkd.key.proof.io.ProblemLoaderException
;
...
...
@@ -19,7 +20,8 @@ public class TestUpdateMatch {
ProofApi
pa
=
a
.
startProof
(
a
.
getProofContracts
().
get
(
0
));
Sequent
sequent
=
pa
.
getProof
().
root
().
sequent
();
System
.
out
.
println
(
sequent
);
Matchings
result
=
MatcherFacade
.
matches
(
"... update-application(_, ?X) ..."
,
sequent
,
false
);
Matchings
result
=
MatcherFacade
.
matches
(
"... update-application(_, ?X) ..."
,
sequent
,
false
,
null
);
System
.
out
.
println
(
result
);
String
exp
=
normalize
(
"\\<{exc=null;try { result=self.foo(_x)@Test;} catch (java.lang.Throwable e) { exc=e; } }\\> (and(and(and(gt(result,Z(0(#))),java.lang.Object::<inv>(heap,self)),equals(exc,null)),all{f:Field}(all{o:java.lang.Object}(or(or(elementOf(o,f,allLocs),and(not(equals(o,null)),not(equals(boolean::select(heapAtPre,o,java.lang.Object::<created>),TRUE)))),equals(any::select(heap,o,f),any::select(heapAtPre,o,f)))))))"
);
String
x
=
normalize
(
result
.
iterator
().
next
().
get
(
"?X"
).
getUnit
().
toString
().
replace
(
"\n"
,
" "
));
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
View file @
9f657295
...
...
@@ -114,8 +114,7 @@ public class InterpreterBuilder {
}
public
InterpreterBuilder
addKeyMatcher
(
ProofApi
api
)
{
ScriptApi
scriptApi
=
api
.
getScriptApi
();
interpreter
.
setMatcherApi
(
new
KeYMatcher
(
scriptApi
,
interpreter
));
interpreter
.
setMatcherApi
(
new
KeYMatcher
(
api
.
getEnv
().
getServices
()));
return
this
;
}
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYMatcher.java
View file @
9f657295
package
edu.kit.iti.formal.psdbg.interpreter
;
import
de.uka.ilkd.key.api.
Script
Api
;
import
de.uka.ilkd.key.
api.VariableAssignment
s
;
import
de.uka.ilkd.key.api.
Proof
Api
;
import
de.uka.ilkd.key.
java.Service
s
;
import
de.uka.ilkd.key.logic.Name
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.logic.op.SchemaVariable
;
...
...
@@ -18,14 +18,13 @@ 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.parser.ast.Signature
;
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.types.SimpleType
;
import
edu.kit.iti.formal.psdbg.parser.types.TermType
;
import
edu.kit.iti.formal.psdbg.parser.types.Type
;
import
edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade
;
import
edu.kit.iti.formal.psdbg.termmatcher.Matchings
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
lombok.Getter
;
import
org.apache.logging.log4j.LogManager
;
import
org.apache.logging.log4j.Logger
;
import
org.key_project.util.collection.ImmutableList
;
...
...
@@ -44,13 +43,13 @@ public class KeYMatcher implements MatcherApi<KeyData> {
private
static
final
Logger
LOGGER
=
LogManager
.
getLogger
(
KeYMatcher
.
class
);
private
static
final
Name
CUT_TACLET_NAME
=
new
Name
(
"cut"
);
private
ScriptApi
scrapi
;
private
KeyInterpreter
interpreter
;
private
List
<
MatchResult
>
resultsFromLabelMatch
;
public
KeYMatcher
(
ScriptApi
scrapi
,
KeyInterpreter
interpreter
)
{
this
.
scrapi
=
scrapi
;
this
.
interpreter
=
interpreter
;
@Getter
private
Services
services
;
public
KeYMatcher
(
Services
services
)
{
this
.
services
=
services
;
}
/**
...
...
@@ -162,75 +161,6 @@ public class KeYMatcher implements MatcherApi<KeyData> {
return
assignments
.
isEmpty
()?
null
:
assignments
;
}
/**
* Match against a sequent of a goal node
* @param currentState
* @param term
* @param signature
* @return
*/
//@Override
public
List
<
VariableAssignment
>
matchSeqKeY
(
GoalNode
<
KeyData
>
currentState
,
String
term
,
Signature
signature
)
{
VariableAssignment
interpreterAssignments
=
currentState
.
getAssignments
();
VariableAssignments
keyAssignments
=
new
VariableAssignments
(
null
);
interpreterAssignments
.
getTypes
().
forEach
((
k
,
v
)
->
keyAssignments
.
getTypeMap
().
put
(
k
.
getIdentifier
(),
interpreter
.
getTypeConversionBiMap
().
get
(
v
)));
interpreterAssignments
.
getValues
().
forEach
((
k
,
v
)
->
{
try
{
keyAssignments
.
addAssignment
(
k
.
getIdentifier
(),
v
);
}
catch
(
Exception
e
)
{
e
.
printStackTrace
();
}
});
Set
<
Map
.
Entry
<
Variable
,
Type
>>
sigEntrySet
=
signature
.
entrySet
();
sigEntrySet
.
forEach
(
e
->
{
try
{
keyAssignments
.
addType
(
e
.
getKey
().
getIdentifier
(),
interpreter
.
getTypeConversionBiMap
().
get
(
e
.
getValue
()));
}
catch
(
Exception
e1
)
{
e1
.
printStackTrace
();
}
});
// System.out.println("Matching: "+term.toString()+"\n================\n"+currentState.getData().getNode().sequent()+"\n================\n");
List
<
VariableAssignments
>
keyMatchResult
=
scrapi
.
matchPattern
(
term
,
currentState
.
getData
().
getNode
().
sequent
(),
keyAssignments
);
//empty keyassignments
// System.out.println("Matched " + keyMatchResult.size() + " goals from " + currentState.toString() + " with pattern " + term);
List
<
VariableAssignment
>
transformedMatchResults
=
new
ArrayList
<>();
for
(
VariableAssignments
mResult
:
keyMatchResult
)
{
transformedMatchResults
.
add
(
from
(
mResult
,
currentState
.
getData
()));
}
//keyMatchResult.forEach(r -> transformedMatchResults.add(from(r)));
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
);
Map
<
String
,
VariableAssignments
.
VarType
>
keyTypeMap
=
keyAssignments
.
getTypeMap
();
keyTypeMap
.
entrySet
().
forEach
(
e
->
interpreterAssignments
.
declare
(
e
.
getKey
(),
interpreter
.
getTypeConversionBiMap
().
inverse
().
get
(
e
.
getValue
())));
keyTypeMap
.
keySet
().
forEach
(
k
->
{
try
{
interpreterAssignments
.
assign
(
k
,
toValueTerm
(
currentState
,
(
Term
)
keyAssignments
.
getVarValue
(
k
)));
//System.out.println(keyAssignments.getVarValue(k));
}
catch
(
Exception
e
)
{
e
.
printStackTrace
();
}
});
return
interpreterAssignments
;
}
private
Value
<
String
>
toValueTerm
(
KeyData
currentState
,
Term
matched
)
{
String
reprTerm
=
LogicPrinter
.
quickPrintTerm
(
matched
,
currentState
.
getEnv
().
getServices
());
...
...
@@ -241,11 +171,14 @@ public class KeYMatcher implements MatcherApi<KeyData> {
}
@Override
public
List
<
VariableAssignment
>
matchSeq
(
GoalNode
<
KeyData
>
currentState
,
String
data
,
Signature
sig
)
{
public
List
<
VariableAssignment
>
matchSeq
(
GoalNode
<
KeyData
>
currentState
,
String
data
,
Signature
sig
)
{
//System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
//System.out.println("Signature " + sig.toString());
Matchings
m
=
MatcherFacade
.
matches
(
data
,
currentState
.
getData
().
getNode
().
sequent
(),
false
);
Matchings
m
=
MatcherFacade
.
matches
(
data
,
currentState
.
getData
().
getNode
().
sequent
(),
false
,
services
);
if
(
m
.
isEmpty
())
{
LOGGER
.
debug
(
"currentState has no match= "
+
currentState
.
getData
().
getNode
().
sequent
());
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentMatcher.java
View file @
9f657295
package
edu.kit.iti.formal.psdbg.gui.controls
;
import
de.uka.ilkd.key.java.Services
;
import
de.uka.ilkd.key.logic.PosInOccurrence
;
import
de.uka.ilkd.key.logic.Term
;
import
de.uka.ilkd.key.pp.*
;
...
...
@@ -9,7 +10,10 @@ import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
import
edu.kit.iti.formal.psdbg.termmatcher.Matchings
;
import
edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath
;
import
javafx.beans.Observable
;
import
javafx.beans.property.*
;
import
javafx.beans.property.ListProperty
;
import
javafx.beans.property.ObjectProperty
;
import
javafx.beans.property.SimpleListProperty
;
import
javafx.beans.property.SimpleObjectProperty
;
import
javafx.collections.FXCollections
;
import
javafx.collections.ObservableList
;
import
javafx.fxml.FXML
;
...
...
@@ -20,37 +24,37 @@ import javafx.scene.control.ListView;
import
javafx.scene.control.TextArea
;
import
javafx.scene.input.MouseEvent
;
import
javafx.scene.layout.BorderPane
;
import
javafx.scene.layout.Pane
;
import
java.util.Collections
;
import
java.util.HashMap
;
import
java.util.Map
;
public
class
SequentMatcher
extends
BorderPane
{
private
final
Services
services
;
//alle aktuellen nicht geschlossene Ziele -> alle leaves später (open+closed)
private
final
ListProperty
<
GoalNode
<
KeyData
>>
goals
=
new
SimpleListProperty
<>(
this
,
"goals"
,
FXCollections
.
observableArrayList
());
private
final
ListProperty
<
GoalNode
<
KeyData
>>
matchingresults
=
new
SimpleListProperty
<>(
this
,
"matchingresults"
,
FXCollections
.
observableArrayList
());
private
final
ListProperty
<
Map
<
String
,
MatchPath
>>
results
=
new
SimpleListProperty
<>(
this
,
"results"
,
FXCollections
.
observableArrayList
());
//sicht user selected
private
final
ObjectProperty
<
GoalNode
<
KeyData
>>
selectedGoalNodeToShow
=
new
SimpleObjectProperty
<>(
this
,
"selectedGoalNodeToShow"
);
public
GoalOptionsMenu
goalOptionsMenu
=
new
GoalOptionsMenu
();
@FXML
private
SequentView
sequentView
;
@FXML
private
ListView
<
GoalNode
<
KeyData
>>
goalView
;
@FXML
private
TextArea
matchpattern
;
@FXML
private
ListView
<
Map
<
String
,
MatchPath
>>
matchingsView
;
private
ListView
<
Map
<
String
,
MatchPath
>>
matchingsView
;
@FXML
private
Label
nomatchings
;
//only shown when no matchings found, else always hidden
private
Map
<
PosInOccurrence
,
Range
>
cursorPosition
=
new
HashMap
<>();
public
SequentMatcher
()
{
Utils
.
createWithFXML
(
this
)
;
public
SequentMatcher
(
Services
services
)
{
this
.
services
=
services
;
Utils
.
createWithFXML
(
this
);
selectedGoalNodeToShow
.
addListener
((
observable
,
oldValue
,
newValue
)
->
{
sequentView
.
setGoal
(
newValue
.
getData
().
getGoal
());
...
...
@@ -74,7 +78,7 @@ public class SequentMatcher extends BorderPane {
newValue
.
forEach
((
name
,
mp
)
->
{
PosInOccurrence
pio
=
mp
.
pio
();
Range
r
=
cursorPosition
.
get
(
pio
);
sequentView
.
setStyleClass
(
r
.
start
(),
r
.
end
(),
"sequent-highlight"
);
sequentView
.
setStyleClass
(
r
.
start
(),
r
.
end
(),
"sequent-highlight"
);
System
.
out
.
println
(
"Highlight "
+
r
.
start
()
+
" "
+
r
.
end
());
});
...
...
@@ -109,7 +113,8 @@ public class SequentMatcher extends BorderPane {
}
public
void
startMatch
()
{
Matchings
matchings
=
MatcherFacade
.
matches
(
matchpattern
.
getText
(),
getSelectedGoalNodeToShow
().
getData
().
getNode
().
sequent
(),
true
);
Matchings
matchings
=
MatcherFacade
.
matches
(
matchpattern
.
getText
(),
getSelectedGoalNodeToShow
().
getData
().
getNode
().
sequent
(),
true
,
services
);
ObservableList
<
Map
<
String
,
MatchPath
>>
resultlist
=
FXCollections
.
observableArrayList
(
matchings
);
//If no matchings found, add "No matchings found"
...
...
@@ -123,64 +128,51 @@ public class SequentMatcher extends BorderPane {
}
}
//alle aktuellen nicht geschlossene Ziele -> alle leaves später (open+closed)
private
final
ListProperty
<
GoalNode
<
KeyData
>>
goals
=
new
SimpleListProperty
<>(
this
,
"goals"
,
FXCollections
.
observableArrayList
());
private
final
ListProperty
<
GoalNode
<
KeyData
>>
matchingresults
=
new
SimpleListProperty
<>(
this
,
"matchingresults"
,
FXCollections
.
observableArrayList
());
public
ObservableList
<
GoalNode
<
KeyData
>>
getMatchingresults
()
{
return
matchingresults
.
get
();
}
public
void
setMatchingresults
(
ObservableList
<
GoalNode
<
KeyData
>>
matchingresults
)
{
this
.
matchingresults
.
set
(
matchingresults
);
}
public
ObservableList
<
Map
<
String
,
MatchPath
>>
getResults
()
{
return
results
.
get
();
}
public
ListProperty
<
Map
<
String
,
MatchPath
>>
resultsProperty
()
{
return
results
;
}
public
void
setResults
(
ObservableList
<
Map
<
String
,
MatchPath
>>
results
)
{
this
.
results
.
set
(
results
);
}
private
final
ListProperty
<
Map
<
String
,
MatchPath
>>
results
=
new
SimpleListProperty
<>(
this
,
"results"
,
FXCollections
.
observableArrayList
());
//sicht user selected
private
final
ObjectProperty
<
GoalNode
<
KeyData
>>
selectedGoalNodeToShow
=
new
SimpleObjectProperty
<>(
this
,
"selectedGoalNodeToShow"
);
public
ListProperty
<
Map
<
String
,
MatchPath
>>
resultsProperty
()
{
return
results
;
}
public
ObservableList
<
GoalNode
<
KeyData
>>
getGoals
()
{
return
goals
.
get
();
}
public
ListProperty
<
GoalNode
<
KeyData
>>
goalsProperty
()
{
return
goals
;
}
public
void
setGoals
(
ObservableList
<
GoalNode
<
KeyData
>>
goals
)
{
this
.
goals
.
set
(
goals
);
}
public
GoalNode
<
KeyData
>
g
etSelectedGoalNodeToShow
()
{
return
selectedGoalNodeToShow
.
get
()
;
public
ListProperty
<
GoalNode
<
KeyData
>
>
g
oalsProperty
()
{
return
goals
;
}
public
ObjectProperty
<
GoalNode
<
KeyData
>
>
s
electedGoalNodeToShow
Property
()
{
return
selectedGoalNodeToShow
;
public
GoalNode
<
KeyData
>
getS
electedGoalNodeToShow
()
{
return
selectedGoalNodeToShow
.
get
()
;
}
public
void
setSelectedGoalNodeToShow
(
GoalNode
<
KeyData
>
selectedGoalNodeToShow
)
{
this
.
selectedGoalNodeToShow
.
set
(
selectedGoalNodeToShow
);
}
public
ObjectProperty
<
GoalNode
<
KeyData
>>
selectedGoalNodeToShowProperty
()
{
return
selectedGoalNodeToShow
;
}
public
ListView
<
Map
<
String
,
MatchPath
>>
getMatchingsView
()
{
return
matchingsView
;
...
...
@@ -194,10 +186,6 @@ public class SequentMatcher extends BorderPane {
return
matchingresults
;
}
public
void
setMatchingresults
(
ObservableList
<
GoalNode
<
KeyData
>>
matchingresults
)
{
this
.
matchingresults
.
set
(
matchingresults
);
}
/**
* Cells for GoalView
*/
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentOptionsMenu.java
View file @
9f657295
package
edu.kit.iti.formal.psdbg.gui.controls
;