Skip to content

Commit 99cdbd8

Browse files
authored
Merge pull request #132 from adharshkamath/invariants-grammar
Added invariants grammar
2 parents efde334 + afac4be commit 99cdbd8

File tree

1 file changed

+48
-0
lines changed

1 file changed

+48
-0
lines changed
Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
start: invariants
2+
3+
invariants: (invariant /\n+/)+ -> multiple_invariants
4+
5+
invariant: "loop" /\s+/ "invariant" /\s+/ pred ";" -> invariant
6+
7+
STRING: /"([^"\\]|\\.)*"/
8+
9+
INTEGER: /[0-9]+/
10+
11+
REAL: /[0-9]+\.[0-9]+/
12+
13+
CHAR: /'([^'\\]|\\.)'/
14+
15+
TRUE: "\true"
16+
17+
FALSE: "\false"
18+
19+
IDENTIFIER: /[a-zA-Z_][a-zA-Z0-9_]*/
20+
21+
unary_logic_op: "~"
22+
23+
bin_logic_op: "&&" | "||" | "=>" | "<=>"
24+
25+
rel_arith_op: "==" | "!=" | "<" | "<=" | ">" | ">="
26+
27+
unary_arith_op: "-"
28+
29+
bin_arith_op: "+" | "-" | "*" | "/" | "%" | "^"
30+
31+
expr: INTEGER
32+
| REAL
33+
| CHAR
34+
| STRING
35+
| IDENTIFIER
36+
| IDENTIFIER /\s+/ "(" /\s+/ expr /\s+/ ("," /\s+/ expr)* /\s+/ ")"
37+
| "(" /\s+/ expr /\s+/ ")"
38+
| unary_arith_op /\s+/ expr
39+
| expr /\s+/ bin_arith_op /\s+/ expr
40+
| expr /\s+/ "?" /\s+/ expr /\s+/ ":" /\s+/ expr
41+
42+
pred: TRUE
43+
| FALSE
44+
| "(" /\s+/ pred /\s+/ ")"
45+
| expr
46+
| unary_logic_op /\s+/ pred
47+
| pred /\s+/ bin_logic_op /\s+/ pred
48+
| expr /\s+/ rel_arith_op /\s+/ expr

0 commit comments

Comments
 (0)