These names are only visible under "ensures" but not under "returns".
If the result is named, the special variable "result" is not used.
In a tuple, either each component should be named, or none at all.
Underscores are allowed. Parentheses around the return type are required.
Each name must be given its own type: "f () : (x y: int)" is rejected.
Identifiers without cast are treated as types, not as names.
To name the result without giving its type, use "returns".

fixes issue #57

a new theory relations.WellFounded is introduced for this purpose
(and must be imported whenever one wants to make use of a custom
relation for a variant)

it defines, inductively, a notion of accessibility for a given
predicate R (x is accessible whenever all elements smaller than x for R
are alreay accessible)

whenever one has to prove that a variant decreases, a new VC is also
generated, to show that the old value of the variant is accessible
for the order relation

note: accessibility being defined inductively, proving well-foundedness
is out of reach of SMT solvers; but at least this is sound now

  vstte12_tree_reconstruction

This makes the syntax cleaner and brings us closer to OCaml.

One incompatibility with the previous grammar is that "ghost"
binds stronger than the left arrow of assignment, and thus
ghost assignments have to be written as "ghost (x.f <- v)".

This is unavoidable, because assignment has to be weaker than
the tuple comma (think "x.f, y.g <- y.g, x.f" or "a[i] <- u,v"),
and "ghost" has to be stronger than comma, for consistency with
our patterns and our return types.

The "return" construction is weaker than comma, for "return a,b".
It is also weaker than assignment, though "return x.f <- b" does
not make much sense either way.

This change does not concern type expressions, where a tuple
type must always have its clothes^Wparentheses on: (int, int).
It might be nice to write "constant pair: int, bool", but on
the other hand this would break casts like "42: int, true".

avoid using logical symbols in programs in a few places

also, require to list all write/read effects whenever
at least one is listed

fix hashtbl_impl, mergesort_queue, and unraveling_a_card_trick

- all programs with sessions are in examples/
- all programs without sessions are in examples/in_progress/
  (if you have private sessions for those, just move them there)
- all pure logical problems are in logic/
  (to simplify bench scripts and gallery building; they are few anyway)
- all OCaml programs are in examples/use_api/
- all strange stuff is in examples/misc/
  (most of it should probably go)
- Claude's solutions for Foveoos 2011 are in examples/foveoos11-cm/
  (why do we need two sets of solutions for quite simple problems?)
- hoare_logic, bitvectors, vacid_0_binary_heaps are in examples/

Bench scripts and documentation are updated.
Also, bench/bench is simplified a little bit.