Add normalization step for tactics.

[gebner]

#1969 added normalization for impure lets in tactic execution, but this was gated on the reify step. The reify step is however also enabled in extraction, and then this heuristic can incorrectly remove effectful lets.

This PR adds a new tactics step in the normalizer, which is only enabled in tactic execution. The heuristic from #1969 is only enabled when this step is set, and no longer applies during extraction.

@mtzguido did pretty much all the work here, thank you!

[mtzguido]

I thought this maybe only happened since we were bypassing the typechecker with the terms we were creating, but this was actually terrible:

$ cat X.fst
module X

let rec g () : Dv nat = g ()

let f () : Dv nat =
  let y = g () in
  42
$ ./bin/fstar.exe X.fst --codegen OCaml
Extracted module FStar.Pervasives.Native
Extracted module X
Verified module: X
All verification conditions discharged successfully

$ cat X.ml
open Prims
let rec (g : unit -> Prims.nat) = fun uu___ -> g ()
let (f : unit -> Prims.nat) = fun uu___ -> (Prims.of_int (42))

I'll add a bunch of tests for this later, it's a pretty serious mistake to not notice.

[gebner]

Wow, this was even happening in F* itself (see last commit--I did another bootstrapping round):

-let rec unexpected : 'a . Prims.string -> 'a = fun s -> unexpected s
-let rec unreachable : 'a . Prims.string -> 'a = fun s -> unreachable s
+let rec unexpected : 'a . Prims.string -> 'a =
+  fun s ->
+    let uu___ =
+      FStar_IO.debug_print_string
+        (Prims.strcat "Platform.Error.unexpected: " s) in
+    unexpected s
+let rec unreachable : 'a . Prims.string -> 'a =
+  fun s ->
+    let uu___ =
+      FStar_IO.debug_print_string
+        (Prims.strcat "Platform.Error.unreachable: " s) in
+    unreachable s

[mtzguido]

I added a test to check that a thing like the snippet above actually diverges (== reaches a 1s timeout).