Pervasives: add norm_debug step to trigger debugging

This is useful to debug specific norm calls in tactics or norm requests
without turning on a "global" flag, which would also trigger debugging
for any request the typechecker does.

src/parser/FStar.Parser.Const.fst

@@ -319,6 +319,7 @@ let steps_zeta_full     = psconst "zeta_full"
 let steps_iota          = psconst "iota"
 let steps_delta         = psconst "delta"
 let steps_reify         = psconst "reify_"
+let steps_norm_debug    = psconst "norm_debug"
 let steps_unfoldonly    = psconst "delta_only"
 let steps_unfoldfully   = psconst "delta_fully"
 let steps_unfoldattr    = psconst "delta_attr"

src/syntax/FStar.Syntax.Embeddings.fst

@@ -632,6 +632,7 @@ let steps_Zeta          = tconst PC.steps_zeta
 let steps_ZetaFull      = tconst PC.steps_zeta_full
 let steps_Iota          = tconst PC.steps_iota
 let steps_Reify         = tconst PC.steps_reify
+let steps_NormDebug     = tconst PC.steps_norm_debug
 let steps_UnfoldOnly    = tconst PC.steps_unfoldonly
 let steps_UnfoldFully   = tconst PC.steps_unfoldonly
 let steps_UnfoldAttr    = tconst PC.steps_unfoldattr
@@ -678,6 +679,8 @@ let e_norm_step : embedding Pervasives.norm_step =
                     steps_Unmeta
                 | Reify ->
                     steps_Reify
+                | NormDebug ->
+                    steps_NormDebug
                 | UnfoldOnly l ->
                     S.mk_Tm_app steps_UnfoldOnly [S.as_arg (embed (e_list e_string) l rng None norm)]
                                 rng
@@ -730,6 +733,8 @@ let e_norm_step : embedding Pervasives.norm_step =
                     Some Unmeta
                 | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_reify ->
                     Some Reify
+                | Tm_fvar fv, [] when S.fv_eq_lid fv PC.steps_norm_debug ->
+                    Some NormDebug
                 | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldonly ->
                     BU.bind_opt (try_unembed (e_list e_string) l norm) (fun ss ->
                     Some <| UnfoldOnly ss)

src/typechecker/FStar.TypeChecker.Cfg.fst

@@ -168,6 +168,7 @@ let fstep_add_one s fs =
     | NBE -> {fs with nbe_step = true }
     | ForExtraction -> {fs with for_extraction = true }
     | Unrefine -> {fs with unrefine = true }
+    | NormDebug -> fs // handled above, affects only dbg flags
 
 let to_fsteps (s : list step) : fsteps =
     List.fold_right fstep_add_one s default_steps
@@ -1437,9 +1438,10 @@ let config' psteps s e =
         | _ -> d in
     let steps = to_fsteps s |> add_nbe in
     let psteps = add_steps (cached_steps ()) psteps in
+    let dbg_flag = List.contains NormDebug s in
     {tcenv = e;
-     debug = if Options.debug_any () then
-            { gen = Env.debug e (Options.Other "Norm")
+     debug = if dbg_flag || Options.debug_any () then
+            { gen = Env.debug e (Options.Other "Norm") || dbg_flag
              ; top = Env.debug e (Options.Other "NormTop")
              ; cfg = Env.debug e (Options.Other "NormCfg")
              ; primop = Env.debug e (Options.Other "Primops")
@@ -1495,6 +1497,7 @@ let translate_norm_step = function
     | Pervasives.HNF  ->    [HNF]
     | Pervasives.Primops -> [Primops]
     | Pervasives.Reify ->   [Reify]
+    | Pervasives.NormDebug -> [NormDebug]
     | Pervasives.UnfoldOnly names ->
         [UnfoldUntil delta_constant; UnfoldOnly (List.map I.lid_of_str names)]
     | Pervasives.UnfoldFully names ->

src/typechecker/FStar.TypeChecker.Env.fsti

@@ -58,6 +58,7 @@ type step =
   | NBE
   | ForExtraction   //marking an invocation of the normalizer for extraction
   | Unrefine
+  | NormDebug       //force debugging
 and steps = list step
 
 val eq_step : step -> step -> bool

ulib/FStar.Pervasives.fst

@@ -54,6 +54,7 @@ type norm_step =
   | Iota // Reduce case analysis (i.e., match)
   | NBE // Use normalization-by-evaluation, instead of interpretation (experimental)
   | Reify // Reify effectful definitions into their representations
+  | NormDebug // Turn on debugging for this call
   | UnfoldOnly : list string -> norm_step // Unlike Delta, unfold definitions for only the given
   // names, each string is a fully qualified name
   // like `A.M.f`
@@ -80,6 +81,9 @@ let primops = Primops
 irreducible
 let delta = Delta
 
+irreducible
+let norm_debug = NormDebug
+
 irreducible
 let zeta = Zeta
 

ulib/FStar.Pervasives.fsti

@@ -174,6 +174,9 @@ val primops : norm_step
 (** Unfold all non-recursive definitions *)
 val delta : norm_step
 
+(** Turn on debugging for this specific call. *)
+val norm_debug : norm_step
+
 (** Unroll recursive calls
 
     Note: Since F*'s termination check is semantic rather than