Remove a lot of Debug.any

src/basic/FStarC.Common.fst

@@ -26,21 +26,23 @@ module List = FStarC.List
 module BU = FStarC.Util
 module SB = FStarC.StringBuffer
 
+let dbg = Debug.get_toggle "Snapshot"
+
 let snapshot msg (push: 'a -> 'b) (stackref: ref (list 'c)) (arg: 'a) : (int & 'b) = BU.atomically (fun () ->
   let len : int = List.length !stackref in
   let arg' = push arg in
-  if FStarC.Debug.any () then Format.print2 "(%s)snapshot %s\n" msg (string_of_int len);
+  if !dbg then Format.print2 "(%s)snapshot %s\n" msg (string_of_int len);
   (len, arg'))
 
 let rollback msg (pop: unit -> 'a) (stackref: ref (list 'c)) (depth: option int) =
-  if FStarC.Debug.any () then Format.print2 "(%s)rollback %s ... " msg (match depth with None -> "None" | Some len ->string_of_int len);
+  if !dbg then Format.print2 "(%s)rollback %s ... " msg (match depth with None -> "None" | Some len ->string_of_int len);
   let rec aux n : 'a =
     if n <= 0 then failwith "(rollback) Too many pops"
     else if n = 1 then pop ()
     else (ignore (pop ()); aux (n - 1)) in
   let curdepth = List.length !stackref in
   let n = match depth with Some d -> curdepth - d | None -> 1 in
-  if FStarC.Debug.any () then Format.print1 " depth is %s\n "(string_of_int (List.length (!stackref)));
+  if !dbg then Format.print1 " depth is %s\n "(string_of_int (List.length (!stackref)));
   BU.atomically (fun () -> aux n)
 
 // This function is separate to make it easier to put breakpoints on it

src/basic/FStarC.Plugins.fst

@@ -28,10 +28,12 @@ open FStarC.Class.Show
 let loaded : ref (list string) = mk_ref []
 let loaded_plugin_lib : ref bool = mk_ref false
 
-let pout  s   = if Debug.any () then Format.print_string s
-let pout1 s x = if Debug.any () then Format.print1 s x
-let perr  s   = if Debug.any () then Format.print_error s
-let perr1 s x = if Debug.any () then Format.print1_error s x
+let dbg_Plugin = Debug.get_toggle "Plugin"
+
+let pout  s   = if !dbg_Plugin then Format.print_string s
+let pout1 s x = if !dbg_Plugin then Format.print1 s x
+let perr  s   = if !dbg_Plugin then Format.print_error s
+let perr1 s x = if !dbg_Plugin then Format.print1_error s x
 
 let do_dynlink (fname:string) : unit =
   try
@@ -122,13 +124,13 @@ if it could find a plugin with the proper name. This will fail hard
 if loading the plugin fails. *)
 let autoload_plugin (ext:string) : bool =
   if Options.Ext.enabled "noautoload" then false else (
-  if Debug.any () then
+  if !dbg_Plugin then
     Format.print1 "Trying to find a plugin for extension %s\n" ext;
   match Find.find_file (ext ^ ".cmxs") with
   | Some fn ->
     if List.mem fn !loaded then false
     else (
-    if Debug.any () then
+    if !dbg_Plugin then
       Format.print1 "Autoloading plugin %s ...\n" fn;
     load_plugin fn;
     true

src/extraction/FStarC.Extraction.ML.Modul.fst

@@ -48,6 +48,7 @@ module Cfg    = FStarC.TypeChecker.Cfg
 module PO     = FStarC.TypeChecker.Primops
 module Print  = FStarC.Syntax.Print
 
+let dbg_Extraction     = Debug.get_toggle "Extraction"
 let dbg_ExtractionReify = Debug.get_toggle "ExtractionReify"
 
 type tydef_declaration = (mlsymbol & FStarC.Extraction.ML.Syntax.metadata & int) //int is the arity
@@ -893,7 +894,7 @@ let extract_iface' (g:env_t) modul =
 let extract_iface (g:env_t) modul =
   let g, iface =
     UF.with_uf_enabled (fun () ->
-      if Debug.any()
+      if !dbg_Extraction
       then FStarC.Util.measure_execution_time
              (Format.fmt1 "Extracted interface of %s" (string_of_lid modul.name))
              (fun () -> extract_iface' g modul)

src/interactive/FStarC.Interactive.Incremental.fst

@@ -332,7 +332,7 @@ let run_full_buffer (st:repl_state)
               run_qst (inspect_repl_stack (!repl_stack) decls push_kind with_symbols write_full_buffer_fragment_progress) qid st
           in
           if request_type <> Cache then log_syntax_issues err_opt;
-          if Debug.any()
+          if !dbg
           then (
             Format.print1 "Generating queries\n%s\n" 
                       (String.concat "\n" (List.map query_to_string queries))

src/parser/FStarC.Parser.Dep.fst

@@ -41,6 +41,10 @@ module F = FStarC.Format
 
 let fd_enabled = mk_ref (None #bool)
 
+let debug_fly_deps =
+  let dbg = FStarC.Debug.get_toggle "fly_deps" in
+  fun () -> !dbg
+
 let fly_deps_enabled () =
     match !fd_enabled with
     | Some b -> b
@@ -53,19 +57,19 @@ let fly_deps_enabled () =
           //so don't change that yet
           || Options.any_dump_module() 
           then (
-            if Debug.any() 
+            if debug_fly_deps ()
             then (
               Format.print_string "Ignoring fly_deps because dep or dump_module is on\n"
             );
             false
           )
           else (
-            if Debug.any() then Format.print_string "fly_deps is on!\n";
+            if debug_fly_deps () then Format.print_string "fly_deps is on!\n";
             true
           )
         )
         else (
-          if Debug.any() then Format.print_string "fly_deps is off!\n";
+          if debug_fly_deps () then Format.print_string "fly_deps is off!\n";
           false
         )
       in
@@ -78,10 +82,6 @@ let with_fly_deps_disabled (f: unit -> 'a) : 'a =
   fd_enabled := Some false;
   FStarC.Util.finally (fun _ -> fd_enabled := v) f
 
-let debug_fly_deps =
-  let dbg = FStarC.Debug.get_toggle "fly_deps" in
-  fun () -> !dbg
-
 (* This is faster than the quadratic BU.remove_dups, since we can use
 the total order. *)
 let remove_dups_fast (#a:Type) {| ord a |} (xs : list a) : list a =

src/smtencoding/FStarC.SMTEncoding.Env.fst

@@ -32,6 +32,7 @@ module BU = FStarC.Util
 open FStarC.Class.Show
 
 let dbg_PartialApp = Debug.get_toggle "PartialApp"
+let dbg_Snapshot = Debug.get_toggle "Snapshot"
 
 let add_fuel x tl = if (Options.unthrottle_inductives()) then tl else x::tl
 let withenv c (a, b) = (a,b,c)
@@ -96,10 +97,10 @@ let varops =
     //the fresh counter is reset after every module
     let reset_fresh () = ctr := initial_ctr in
     let push () =
-      if Debug.any() then Format.print_string "SMTEncoding.scopes.push\n";
+      if !dbg_Snapshot then Format.print_string "SMTEncoding.scopes.push\n";
       scopes := new_scope() :: !scopes in // already signal-atomic
     let pop () = 
-      if Debug.any() then Format.print_string "SMTEncoding.scopes.pop\n";
+      if !dbg_Snapshot then Format.print_string "SMTEncoding.scopes.pop\n";
       scopes := List.tl !scopes in // already signal-atomic
     let snapshot () = FStarC.Common.snapshot "SMTEncoding.scopes" push scopes () in
     let rollback depth = FStarC.Common.rollback "SMTEncoding.scopes" pop scopes depth in
@@ -114,7 +115,7 @@ let varops =
      next_id=next_id;
      mk_unique=mk_unique;
      reset_scope=fun () -> 
-      if Debug.any() then Format.print_string "reset_scope!\n";
+      if !dbg_Snapshot then Format.print_string "reset_scope!\n";
       scopes := [new_scope ()]}
 
 (* ---------------------------------------------------- *)

src/smtencoding/FStarC.SMTEncoding.Solver.fst

@@ -1392,7 +1392,7 @@ let encode_and_ask (can_split:bool) (is_retry:bool) use_env_msg tcenv q : (list
 
       | Assume _ ->
         if (is_retry || Options.split_queries() = Options.Always)
-        && Debug.any()
+        && !dbg_SMTQuery
         then (
           let n = List.length labels in
           if n <> 1
@@ -1452,7 +1452,7 @@ let do_solve (can_split:bool) (is_retry:bool) use_env_msg tcenv q : unit =
     failwith "impossible: bad answer from encode_and_ask"
 
 let split_and_solve (retrying:bool) use_env_msg tcenv q : unit =
-  if retrying && (Debug.any () || Options.query_stats ()) then begin
+  if retrying && (!dbg_SMTQuery || Options.query_stats ()) then begin
     Format.print1 "(%s)\tQuery-stats splitting query because retrying failed query\n"
                    (show (Env.get_range tcenv))
   end;
@@ -1504,7 +1504,7 @@ let do_solve_maybe_split use_env_msg tcenv q : unit =
       end
     | Options.Always ->
       (* Set retrying=false so queries go through the full config list, etc. *)
-      if Debug.any () || Options.query_stats () then
+      if !dbg_SMTQuery || Options.query_stats () then
         Format.print1 "(%s)\tQuery-stats splitting query because --split_queries is always\n"
                       (show (Env.get_range tcenv));
       split_and_solve false use_env_msg tcenv q