GitLab

The projection is now recorded with its ident which allow us to rewrite
the projections in counterexamples. We use the id_string which is only an
approximation of what can be seen in the task (but it is close enough).

Note that this should have no effect on why3

The declare-datatypes part apparently changes in smtv2.6.

We now use the information inside attributes to correctly associate a
label to each counterexamples. The information is carried inside
attributes which are preserved/collected during ce transformations and
printing to smt2.
The collection filled during the printing of the task is reused during the
printing of counterexamples to add "at label" where needed.

This is solved by collecting names of constructors with no arguments
during printing.

These projections are necessary because records have changed from
old system to new system. Previously, a record was never abstract.
Subsequently, we could always give value to its fields independently.
Now, when a record (or algebraic type, not handled by this commit) is
abstract, we use the function defined for its fields as projections.
So, we need to have several projections per constant in order to represent
those as values.

This patch is also a first step to the necessary cleaning of ce treatment
code.

interrupt is now properly handled by why3server

Instead of erroring out, the behavior is now the same as in git, opam, and
so on.

         allows to remove completely some prover version

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.

Change-Id: I73818d34852ddf6dc271deb287bf4baaf5b2bb95
(cherry picked from commit 8f2af64511e7b2e68f61e4dba4bffbb99cfd9da2)

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.