Commit a77f70a0 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add support for operators to why3doc.

parent 721efb49
......@@ -886,8 +886,9 @@ ident_rich:
lident_rich:
| lident { $1 }
| LEFTPAR lident_op RIGHTPAR { mk_id $2 (floc ()) }
| LEFTPAR lident_op RIGHTPAR { mk_id $2 (floc_i 2) }
| LEFTPAR_STAR_RIGHTPAR { mk_id (infix "*") (floc ()) }
/* FIXME: use location of operator star rather than left parenthesis */
;
lident_op:
......
......@@ -83,8 +83,29 @@
}
let op_char_1 = ['=' '<' '>' '~']
let op_char_2 = ['+' '-']
let op_char_3 = ['*' '/' '%']
let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
let op_char_34 = op_char_3 | op_char_4
let op_char_234 = op_char_2 | op_char_34
let op_char_1234 = op_char_1 | op_char_234
let op_char_pref = ['!' '?']
let prefix_op =
op_char_1234* op_char_1 op_char_1234*
| op_char_234* op_char_2 op_char_234*
| op_char_34* op_char_3 op_char_34*
| op_char_4+
let operator =
op_char_pref op_char_4*
| prefix_op
| prefix_op '_'
| "[]"
| "[<-]"
| "[]<-"
let space = [' ' '\t']
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*
let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
let special = ['<' '>' '&']
rule scan fmt = parse
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment