GitLab

this commit changes the way of tracking occurrences of regions
and type variables for the purposes of generalization, effect
filtering, and effect checks. It restricts the previous
implementation in two aspects:

- a psymbol p can be monomorphic (= non-generalizable) in an effect
  only if p depends (= is defined via) a pvsymbol whose type contains
  the affected region. See bench/programs/bad-typing/recfun.mlw
  for an example. This restriction is required for soundness.

- an argument of a psymbol cannot contain a region shared with
  another argument or an external pvsymbol. However, we do not
  require (so far) that the argument's type doesn't contain the same
  region twice and we allow the result type to contain known regions.
  This restriction is not necessary for soundness, and is introduced
  only to avoid some unintentional user errors and reduce the gap
  between the types that can be implemented in a "let" and the types
  that can be declared in a "val".

[GTK sourceview] why.lang renamed to why3.lang

Submitted by Johannes Kanig

This makes unnecessary all checks for ghost exceptions
escaping into the non-ghost code.

In this case, we break the encapsulation and prove the global
exception postcondition directly from the code under "abstract".

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

fix hashtbl_impl, mergesort_queue, and unraveling_a_card_trick

they now live in examples/tests/

also, simplify bench/bench script

a lemma function is introduced with 'let lemma f' or 'let rec lemma f'
it is a ghost function
it must have return type unit and read-only effects
it introduces a goal (its WP), followed by an axiom
  forall args/reads, precondition => postcondition