MatchPattern.g4 2.72 KB
Newer Older
Alexander Weigl's avatar
Alexander Weigl committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
grammar MatchPattern;

/* Examples for testing

f(x)
f(x,y,g(y))
X
?Y
_
...
f(... ?X ...)
f(..., ?X)
f(..., ...?X...)
f(..., ... g(x) ...)
f(_, x, _, y, ... y ...)
*/
17

Alexander Weigl's avatar
Alexander Weigl committed
18 19 20
sequentPattern : antec=semiSeqPattern? ARROW succ=semiSeqPattern? #sequentArrow
               | anywhere=semiSeqPattern #sequentAnywhere
               ;
21

22
semiSeqPattern : termPattern (',' termPattern)*;
23

Alexander Weigl's avatar
Alexander Weigl committed
24
termPattern :
25
   '(' quantifier=(EXISTS|FORALL) boundVars+=(SID|ID|DONTCARE)+  skope=termPattern ')' bindClause?  #quantForm
26
    |  termPattern MUL termPattern                              #mult
27 28 29
    | <assoc=right> termPattern op=(DIV|MOD) termPattern        #divMod
    | termPattern op=(PLUS|MINUS) termPattern                   #plusMinus
    | termPattern op=(LE|GE|LEQ|GEQ) termPattern                #comparison
Sarah Grebing's avatar
Sarah Grebing committed
30
    | termPattern op=(NEQ|EQ) termPattern                       #equality
31 32 33 34
    | termPattern AND termPattern                               #and
    | termPattern OR termPattern                                #or
    | termPattern IMP termPattern                               #impl
    | termPattern XOR termPattern                               #xor
Sarah Grebing's avatar
Sarah Grebing committed
35
    | termPattern EQUIV termPattern                             #equivalence
36 37
    | MINUS termPattern                                         #exprNegate
    | NOT termPattern                                           #exprNot
Alexander Weigl's avatar
Alexander Weigl committed
38 39 40
    | '(' termPattern ')' bindClause?                                      #exprParen
    | func=ID ( '(' termPattern (',' termPattern)* ')')? bindClause?        #function
    |  DONTCARE   bindClause?                                              #dontCare
41 42 43 44 45 46
    //| STARDONTCARE  #starDontCare
    | SID                                                       #schemaVar
    | STARDONTCARE termPattern STARDONTCARE                     #anywhere
    | DIGITS                                                    #number
    // not working because of ambigue | left=termPattern op=(PLUS|MINUS|MUL|LE|GE|LEQ|GEQ|NEQ|EQ| AND|OR|IMP) right=termPattern #binaryOperation
    ;
47

Alexander Weigl's avatar
Alexander Weigl committed
48 49 50
/*
f(x), f(x,y,g(y)), X, ?Y, _, ..., f(... ?X ...), f(..., ?X), f(..., ...?X...), f(..., ... g(x) ...), f(_, x, _, y, ... y ...)
*/
51

Alexander Weigl's avatar
Alexander Weigl committed
52
bindClause : ('\\as' | ':') SID;
Alexander Weigl's avatar
Alexander Weigl committed
53 54

DONTCARE: '?' | '_' | '█';
Alexander Weigl's avatar
Alexander Weigl committed
55 56 57 58
DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ;

ARROW : '⇒' | '==>';
Alexander Weigl's avatar
Alexander Weigl committed
59
STARDONTCARE: '...' | '…';
60 61 62 63 64 65 66 67
PLUS : '+' ;
MINUS : '-' ;
MUL : '*' ;
DIV : '/' ;
EQ : '=' ;
NEQ : '!=' ;
GEQ : '>=' ;
LEQ : '<=' ;
68
EQUIV : '<->';
69 70 71 72
GE : '>' ;
LE : '<' ;
AND : '&' ;
OR: '|' ;
73
IMP: '->';
74 75
MOD:'%';
XOR:'^';
76 77 78 79 80 81 82 83 84 85
NOT :'!';
FORALL: '\\forall' | '∀';
EXISTS: '\\exists';
SID: '?' [_a-zA-Z0-9\\]+ ;
ID : [a-zA-Z\\_] ([_a-zA-Z0-9\\])*
   | 'update-application'
   | 'parallel-upd'
   | 'elem-update'
   ;

86

Alexander Weigl's avatar
Alexander Weigl committed
87
COMMENT: '//' ~[\n\r]* -> channel(HIDDEN);
88
WS: [\n\f\r\t ] -> channel(HIDDEN);