Overloaded Operators for KeY lang #3032

This MR brings overloaded operators to KeY lang:

1. On function and predicate definitions you can additional add prefix, infix, and postfix notations. \functions { int add(int, int) \infix(+); }

These information are stored inside the Function object.

1. These information also impacts the pretty printing.

2. Operators are now a sequence of symbols [-+*/^<>=|]. Their first character determines the precedence. Following are legal expressions:

a ++ b + c = ( a ++ b ) + c a <|> b <= c a +- b != a + -b This trick avoids an "operator precedence parser", which would also be nice.