normalizer: an optimization: drop the environment for simple arguments
normalizer: an optimization: drop the environment for simple arguments

Suppose we are normalizing the following infinite loop

  let rec f (x:unit) : Tot unit = f ()
  in
  f ()

The KAM will repeatedly:

  - Push Arg(e, ()) on stack
  - Unfold f into `fun x -> f ()`
  - Shift `()` to the environment

which looks OK: the stack and environment remain bounded. However, note
that pushing the `()` to the stack is saving the current environment
`e` as well. We then drop the environment when unfolding f (which is
index-closed), that's fine. Finally, we shift the `Arg (e, ())` to
the machine's environment, adding a *closure* that still mentions the
original `e`.

So the old `e` is still reachable and can never be freed. Further, we
have nested it one more level, since the old `e` is now the environment
of the first closure in the new environmente. (Approximately, we have:
`e' = Clos (e, Tm_unit, _, _) :: []`.) So the KAM will continue nesting
its environment infinitely, and use more and more memory.

(This Tot-example will obviously not typecheck, but the same problem
happens for Div and tactics.)

The rather naive solution in this patch is to detect obviously-closed
terms, such as `()` and drop their environment when pushing them to the
stack.

Perhaps the real solution, at least for tactics, is to normalize them in
CBV.

FStarLang/FStar,FStarLang/FStar,FStarLang/FStar