Variant of compute_in_goal that rewrite only the specified set of rules.

  This is to prevent quantified records from being decomposed by
  eval_match. e.g, assert { forall x:t. ... } was previously
  transformed to assert { forall x1:t1, x2:t2, x3:t3. ... } if x was
  a record type with fields x1,x2,x3. This changed the
  instantiation pattern, which could be harmful.

We do not want to generate distinct liftings for every single
partial application of a function or predicate symbol. Canonical
closures have an easily recognizable shape, thus we can detect
them and replace them with a unique constant "f_closure".

Currently, the builtin theory why3.HighOrd (or just HighOrd) must
be explicitly "use"-d. However, the type (HighOrd.func 'a 'b) can
be written ('a -> 'b), and the type (HighOrd.pred 'a) can be written
('a -> bool), and the application operation (HighOrd.(@)) can be
written as the usual juxtaposition. Thus, normally, you do not have
to write the qualifiers. The builtin theory why3.Bool (or just Bool)
is needed for "bool". The names "HighOrd", "func", "pred", and "(@)"
are not yet fixed and may change.

"eliminate_epsilon" tries to be smart when a lambda (or some other
comprehension form) occurs under equality or at the top of a definition.
We could go even further and replace (\ x . t) s with t[x <- s], without
lifting the lambda. I'm not sure it's worth it: we rarely write redexes
manually. They can and will appear through inlining, though.

Anyone who wants to construct epsilon-terms directly using the API
should remember that these are not Hilbert's epsilons: by writing
an epsilon term, you postulate the existence (though not necessarily
uniqueness) of the described object, and "eliminate_epsilon" will
happily convert it to an axiom expressing this existence. We only
use epsilons to write comprehensions whose soundness is guaranteed
by a background theory, e.g. lambda-calculus.

lskept: the old selection check required at least one non-variable
non-closed type in the lsymbol's signature. This is too permissive,
because (list_match : list 'a -> 'b -> 'b) is allowed and will produce
an instance for every type in the "inst" set. The new check requires
that all freely standing type variables occur under a type constructor
elsewhere in the lsymbol's signature.

lsinst: accept any monomorphic instance of any polymorphic symbol
except equality. The old procedure applied the same restrictions
as for the "lskept" set which serve no real purpose for "lsinst".

Sharing is caring, right?

also, avoid the "encoding_sort" transformation, if it can be done
directly in the printer.

On the same example as in the previous commits, this gives 5x
acceleration together with some memory usage reduction.

feel free to revert, if you think we might want to make again the
distinction between t_equal and t_equal_alpha in future or just
don't feel like breaking the API.

we still keep bv_vars in the binders, so calculating the set
of free variables only has to descend to the topmost binders.
The difference on an example from BWare is quite striking:

/usr/bin/time why3-replayer : with t_vars

505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k

/usr/bin/time why3-replayer : without t_vars

242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k

Not only we take 2/3 of memory, but we also gain in speed (less work
for the GC, most probably).

This patch should be tested on big WhyML examples,
since src/whyml/mlw_*.ml are big users of t_vars.

Thanks to Guillaume for the suggestion.

In pattern compilation, we only need to know the full list of
constructors for a given type, whenever
1. we want to check that a symbol used in a pattern is indeed
   a constructor;
2. we want to check for non-exhaustive matching and return an
   example of a non-covered pattern, if any.
Thus, we need to give Pattern.compile access to the current
known_map whenever we check new declarations in Decl or Mlw_decl.
However, once we have checked the patterns, we do not need the
full constructor lists just to compile the match expressions.
Just knowing the number of constructors (provided in ls_constr)
is enough to detect non-exhaustive matching during compilation.