An external printer/argument parser can now be registered. This changes
args_wrapper and Trans so that transformation now takes the Env.fformat
representing the language as argument.
Function lang of session_itp now uses file_format.
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.
