Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
b29b50f2
Commit
b29b50f2
authored
Aug 24, 2017
by
Alexander Weigl
Browse files
Pattern Binder
parent
dbf27dc2
Changes
6
Show whitespace changes
Inline
Side-by-side
src/main/antlr4/edu/kit/formal/psdb/termmatcher/MatchPattern.g4
View file @
b29b50f2
...
...
@@ -32,9 +32,9 @@ termPattern :
//| termPattern EQUIV termPattern already covered by EQ/NEQ
| MINUS termPattern #exprNegate
| NOT termPattern #exprNot
| '(' termPattern ')' #exprParen
| func=ID ( '(' termPattern (',' termPattern)* ')')? #function
| DONTCARE #dontCare
| '(' termPattern ')'
bindClause?
#exprParen
| func=ID ( '(' termPattern (',' termPattern)* ')')?
bindClause?
#function
| DONTCARE
bindClause?
#dontCare
//| STARDONTCARE #starDontCare
| SID #schemaVar
| STARDONTCARE termPattern STARDONTCARE #anywhere
...
...
@@ -46,6 +46,7 @@ termPattern :
f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...)
*/
bindClause : ('\\as' | ':') SID;
ARROW : '⇒' | '==>';
DONTCARE: '?' | '_' | '█';
...
...
src/main/java/edu/kit/formal/psdb/interpreter/assignhook/KeyAssignmentHook.java
View file @
b29b50f2
...
...
@@ -18,7 +18,6 @@ public class KeyAssignmentHook extends DefaultAssignmentHook<KeyData> {
register
(
"MAX_AUTO_STEPS"
,
this
::
setMaxAutosteps
,
this
::
getMaxAutosteps
);
}
public
Value
<
BigInteger
>
getMaxAutosteps
(
KeyData
data
)
{
return
Value
.
from
(
100
);
}
...
...
@@ -26,5 +25,4 @@ public class KeyAssignmentHook extends DefaultAssignmentHook<KeyData> {
public
boolean
setMaxAutosteps
(
KeyData
data
,
Value
<
BigInteger
>
val
)
{
return
true
;
}
}
src/main/java/edu/kit/formal/psdb/termmatcher/MatchPatternDualVisitor.java
View file @
b29b50f2
...
...
@@ -112,9 +112,12 @@ public abstract class MatchPatternDualVisitor<T, S> extends MatchPatternBaseVisi
@Override
public
T
visitExprParen
(
MatchPatternParser
.
ExprParenContext
ctx
)
{
return
accept
(
ctx
.
termPattern
()
,
stack
.
peek
());
return
visitExprParen
(
ctx
,
stack
.
peek
());
}
public
abstract
T
visitExprParen
(
MatchPatternParser
.
ExprParenContext
ctx
,
S
peek
);
@Override
public
T
visitImpl
(
MatchPatternParser
.
ImplContext
ctx
)
{
return
visitImpl
(
ctx
,
stack
.
peek
());
...
...
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherFacade.java
View file @
b29b50f2
...
...
@@ -148,7 +148,7 @@ public class MatcherFacade {
for
(
SequentFormula
form
:
allSequentFormulas
)
{
Matchings
temp
=
matcher
.
accept
(
termPatternContext
,
form
.
formula
());
for
(
Hash
Map
<
String
,
Term
>
match
:
temp
)
{
for
(
Map
<
String
,
Term
>
match
:
temp
)
{
m
.
add
(
new
MatchInfo
(
match
,
Collections
.
singleton
(
form
)));
}
}
...
...
@@ -161,7 +161,9 @@ public class MatcherFacade {
if
(
res
==
null
)
return
NO_MATCH
;
Set
<
HashMap
<
String
,
Term
>>
resMap
=
res
.
stream
().
map
(
el
->
el
.
matching
).
collect
(
Collectors
.
toSet
());
Set
<
Map
<
String
,
Term
>>
resMap
=
res
.
stream
()
.
map
(
el
->
el
.
matching
)
.
collect
(
Collectors
.
toSet
());
//remove dups?
Matchings
resMatchings
=
new
Matchings
();
...
...
src/main/java/edu/kit/formal/psdb/termmatcher/MatcherImpl.java
View file @
b29b50f2
...
...
@@ -53,7 +53,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
return
oneMatch
?
res
:
null
;
}
private
static
HashMap
<
String
,
Term
>
reduceConform
(
Hash
Map
<
String
,
Term
>
h1
,
Hash
Map
<
String
,
Term
>
h2
)
{
private
static
HashMap
<
String
,
Term
>
reduceConform
(
Map
<
String
,
Term
>
h1
,
Map
<
String
,
Term
>
h2
)
{
HashMap
<
String
,
Term
>
h3
=
new
HashMap
<>(
h1
);
...
...
@@ -85,9 +85,9 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
Matchings
m3
=
new
Matchings
();
boolean
oneMatch
=
false
;
for
(
Hash
Map
<
String
,
Term
>
h1
:
m1
)
{
for
(
Hash
Map
<
String
,
Term
>
h2
:
m2
)
{
Hash
Map
<
String
,
Term
>
h3
=
reduceConform
(
h1
,
h2
);
for
(
Map
<
String
,
Term
>
h1
:
m1
)
{
for
(
Map
<
String
,
Term
>
h2
:
m2
)
{
Map
<
String
,
Term
>
h3
=
reduceConform
(
h1
,
h2
);
if
(
h3
!=
null
)
{
//m3.add(h3);
if
(!
m3
.
contains
(
h3
))
m3
.
add
(
h3
);
...
...
@@ -120,7 +120,7 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
@Override
public
Matchings
visitDontCare
(
MatchPatternParser
.
DontCareContext
ctx
,
Term
peek
)
{
if
(
peek
!=
null
)
{
return
EMPTY_MATCH
;
return
handleBindClause
(
ctx
.
bindClause
(),
peek
,
EMPTY_MATCH
)
;
}
else
{
return
NO_MATCH
;
}
...
...
@@ -168,18 +168,40 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
*/
@Override
protected
Matchings
visitFunction
(
MatchPatternParser
.
FunctionContext
ctx
,
Term
peek
)
{
//System.out.format("Match: %25s with %s %n", peek, ctx.toInfoString(new MatchPatternParser(null)));
String
expectedFunction
=
ctx
.
func
.
getText
();
if
(
peek
.
op
().
name
().
toString
().
equals
(
expectedFunction
)
// same name
&&
ctx
.
termPattern
().
size
()
==
peek
.
arity
()
// same arity
)
{
return
IntStream
.
range
(
0
,
peek
.
arity
())
Matchings
m
=
IntStream
.
range
(
0
,
peek
.
arity
())
.
mapToObj
(
i
->
(
Matchings
)
accept
(
ctx
.
termPattern
(
i
),
peek
.
sub
(
i
)))
.
reduce
(
MatcherImpl:
:
reduceConform
)
.
orElse
(
EMPTY_MATCH
);
return
handleBindClause
(
ctx
.
bindClause
(),
peek
,
m
);
}
return
NO_MATCH
;
}
/**
* @param ctx
* @param t
* @param m
* @return
*/
private
Matchings
handleBindClause
(
MatchPatternParser
.
BindClauseContext
ctx
,
Term
t
,
Matchings
m
)
{
if
(
ctx
==
null
)
{
return
m
;
}
if
(
m
.
equals
(
NO_MATCH
))
{
return
m
;
}
final
String
name
=
ctx
.
SID
().
getText
();
Matchings
mNew
=
Matchings
.
singleton
(
name
,
t
);
return
this
.
reduceConform
(
m
,
mNew
);
}
/**
* Trasnform a term that represent a number to int
*
...
...
@@ -339,11 +361,17 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
return
visitUnaryOperation
(
"sub"
,
ctx
.
termPattern
(),
peek
);
}
@Override
public
Matchings
visitExprParen
(
MatchPatternParser
.
ExprParenContext
ctx
,
Term
peek
)
{
return
handleBindClause
(
ctx
.
bindClause
(),
peek
,
accept
(
ctx
.
termPattern
(),
peek
));
}
private
Matchings
visitUnaryOperation
(
String
unaryOp
,
MatchPatternParser
.
TermPatternContext
ctx
,
Term
peek
)
{
MatchPatternParser
.
FunctionContext
func
=
new
MatchPatternParser
.
FunctionContext
(
ctx
);
func
.
termPattern
().
add
(
ctx
);;
func
.
termPattern
().
add
(
ctx
);
;
func
.
func
=
new
CommonToken
(
MatchPatternLexer
.
ID
,
unaryOp
);
return
accept
(
func
,
peek
);
}
...
...
@@ -387,10 +415,10 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
}
public
static
class
MatchInfo
{
public
Hash
Map
<
String
,
Term
>
matching
;
public
Map
<
String
,
Term
>
matching
;
public
Set
<
SequentFormula
>
matchedForms
;
public
MatchInfo
(
Hash
Map
<
String
,
Term
>
m
,
Set
<
SequentFormula
>
f
)
{
public
MatchInfo
(
Map
<
String
,
Term
>
m
,
Set
<
SequentFormula
>
f
)
{
matching
=
m
;
matchedForms
=
f
;
}
...
...
@@ -400,10 +428,10 @@ class MatcherImpl extends MatchPatternDualVisitor<Matchings, Term> {
/**
* Class Matching contains a hashmap of string to term
*/
class
Matchings
extends
ArrayList
<
Hash
Map
<
String
,
Term
>>
{
class
Matchings
extends
ArrayList
<
Map
<
String
,
Term
>>
{
public
static
Matchings
singleton
(
String
name
,
Term
peek
)
{
Matchings
matchings
=
new
Matchings
();
Hash
Map
<
String
,
Term
>
va
=
new
Hash
Map
<>();
Map
<
String
,
Term
>
va
=
new
Tree
Map
<>();
va
.
put
(
name
,
peek
);
matchings
.
add
(
va
);
return
matchings
;
...
...
src/test/java/edu/kit/formal/psdb/termmatcher/MatcherFacadeTest.java
View file @
b29b50f2
...
...
@@ -52,14 +52,21 @@ public class MatcherFacadeTest {
shouldMatch
(
"1*j"
,
"1 + ?Y"
,
"[]"
);
shouldMatch
(
"1*j"
,
"1 * ?Y"
,
"[{?Y=j}]"
);
//shouldMatch("f(a) ==> f(a), f(b)" , "==> 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)");
}
@Test
public
void
testBindContext
()
throws
ParserException
{
//shouldMatch("f(a)", "f(a) : ?Y", "[{?Y=f(a)}]");
//shouldMatch("f(g(a))", "_ \\as ?Y", "[{?Y=f(g(a))}]");
//shouldMatch("i+i+j", "(?X + ?Y) : ?Z", "[{?X=add(i,i), ?Y=j, ?Z=add(add(i,i),j)}]");
shouldMatch
(
"f(f(g(a)))"
,
"f( (... g( (...a...):?Q ) ...) : ?R) : ?Y"
,
"[{?X=add(i,i), ?Y=j, ?Z=add(add(i,i),j)}]"
);
}
private
void
shouldMatch
(
String
key
,
String
pattern
)
throws
ParserException
{
Term
term
=
parseKeyTerm
(
key
);
Matchings
m
=
MatcherFacade
.
matches
(
pattern
,
term
);
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment