Skip to content

Commit 133f933

Browse files
authored
Merge pull request #192 from adharshkamath/invariants-grammar
Updated the grammar for invariants
2 parents ef4465d + ef35c9d commit 133f933

1 file changed

Lines changed: 18 additions & 16 deletions

File tree

Lines changed: 18 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
start: invariants
1+
start: "```" "\n" invariants "```"
22

3-
invariants: (invariant /\n+/)+ -> multiple_invariants
3+
invariants: invariant+
44

5-
invariant: "loop" /\s+/ "invariant" /\s+/ pred ";" -> invariant
5+
invariant: "loop" "invariant" pred ";" "\n"
66

77
STRING: /"([^"\\]|\\.)*"/
88

@@ -12,15 +12,15 @@ REAL: /[0-9]+\.[0-9]+/
1212

1313
CHAR: /'([^'\\]|\\.)'/
1414

15-
TRUE: "\true"
15+
TRUE: "\\true"
1616

17-
FALSE: "\false"
17+
FALSE: "\\false"
1818

19-
IDENTIFIER: /[a-zA-Z_][a-zA-Z0-9_]*/
19+
IDENTIFIER.-1: /[a-zA-Z_][a-zA-Z0-9_]*/
2020

2121
unary_logic_op: "~"
2222

23-
bin_logic_op: "&&" | "||" | "=>" | "<=>"
23+
bin_logic_op: "&&" | "||" | "==>" | "<==>"
2424

2525
rel_arith_op: "==" | "!=" | "<" | "<=" | ">" | ">="
2626

@@ -33,16 +33,18 @@ expr: INTEGER
3333
| CHAR
3434
| STRING
3535
| 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
36+
| IDENTIFIER "(" expr ("," expr)* ")"
37+
| "(" expr ")"
38+
| unary_arith_op expr
39+
| expr bin_arith_op expr
40+
| expr "?" expr ":" expr
4141

4242
pred: TRUE
4343
| FALSE
44-
| "(" /\s+/ pred /\s+/ ")"
44+
| "(" pred ")"
4545
| expr
46-
| unary_logic_op /\s+/ pred
47-
| pred /\s+/ bin_logic_op /\s+/ pred
48-
| expr /\s+/ rel_arith_op /\s+/ expr
46+
| unary_logic_op pred
47+
| pred bin_logic_op pred
48+
| expr rel_arith_op expr
49+
50+
%ignore /[\t ]/

0 commit comments

Comments
 (0)