Merge pull request #3669 from mtzguido/nit

Tc: prevent reset of -d across modules

src/basic/FStarC.Compiler.Debug.fst

@@ -84,15 +84,17 @@ let set_level_high    () = dbg_level := 3
 let set_level_extreme () = dbg_level := 4
 
 let enable_toggles (keys : list string) : unit =
-  if Cons? keys then enable ();
+  if Cons? keys then
+    enable ();
   keys |> List.iter (fun k ->
-    if k = "Low" then set_level_low ()
-    else if k = "Medium" then set_level_medium ()
-    else if k = "High" then set_level_high ()
-    else if k = "Extreme" then set_level_extreme ()
-    else
-    let t = get_toggle k in
-    t := true
+    match k with
+    | "Low" ->     set_level_low ()
+    | "Medium" ->  set_level_medium ()
+    | "High" ->    set_level_high ()
+    | "Extreme" -> set_level_extreme ()
+    | _ ->
+      let t = get_toggle k in
+      t := true
   )
 
 let disable_all () : unit =

src/typechecker/FStarC.TypeChecker.Tc.fst

@@ -1135,9 +1135,9 @@ let tc_partial_modul env modul =
   if Debug.any () then
     BU.print3 "Now %s %s of %s\n" action label (string_of_lid modul.name);
 
-  Debug.disable_all ();
-  if Options.should_check (string_of_lid modul.name) // || Options.debug_all_modules ()
-  then Debug.enable_toggles (Options.debug_keys ());
+  let dsnap = Debug.snapshot () in
+  if not (Options.should_check (string_of_lid modul.name)) && not (Options.debug_all_modules ())
+  then Debug.disable_all ();
 
   let name = BU.format2 "%s %s" (if modul.is_interface then "interface" else "module") (string_of_lid modul.name) in
   let env = {env with Env.is_iface=modul.is_interface; admit=not verify} in
@@ -1148,6 +1148,7 @@ let tc_partial_modul env modul =
                                     (string_of_lid modul.name)
                                     (if modul.is_interface then " (interface)" else "")) (fun () ->
     let ses, env = tc_decls env modul.declarations in
+    Debug.restore dsnap;
     {modul with declarations=ses}, env
   )
 
@@ -1222,16 +1223,17 @@ let load_checked_module (en:env) (m:modul) :env =
   module. *)
 
   (* Reset debug flags *)
-  if Options.should_check (string_of_lid m.name) // || Options.debug_all_modules ()
-  then Debug.enable_toggles (Options.debug_keys ())
-  else Debug.disable_all ();
+  let dsnap = Debug.snapshot () in
+  if not (Options.should_check (string_of_lid m.name)) && not (Options.debug_all_modules ())
+  then Debug.disable_all ();
 
   let m = deep_compress_modul m in
   let env = load_checked_module_sigelts en m in
   //And then call finish_partial_modul, which is the normal workflow of tc_modul below
   //except with the flag `must_check_exports` set to false, since this is already a checked module
   //the second true flag is for iface_exists, used to determine whether should extract interface or not
   let _, env = finish_partial_modul true true env m in
+  Debug.restore dsnap;
   env
 
 let load_partial_checked_module (en:env) (m:modul) : env =