Main changes are:
- Real constants now offer a normalized representation usable for internal
computations.
- Constants are no longer stored in textual form.
Program functions can be declared as partial with "let/val partial".
Similarly to "diverges", partial code cannot be ghost, however it does not need to be
explicitly specified as partial.
Fixes#184.
It is possible to append an arbitary number of quote symbols
at the end of an prefix/infix/mixfix operator:
applied form standalone form
-' 42 (-'_)
x +' y (+')
a[0]' <- 1 ([]'<-)
Pretty-printing will use the quote symbols for disambiguation.
The derived symbols can be produced by Why3 by appending
a suffix of the form "_toto" or "'toto". These symbols can
be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
This commit removes all hard-coded "infix ..", "prefix ..",
and "mixfix .." from the rest of the code, and handles the
symbolic notation entirely inside Ident. It does not change
the notation itself.
