Deprecate debug flags (#1204)

* Deprecate the debug flag 'sum'

After merging sum theory into adt theory, this flag has no effect
anymore. This commit deprecates it and now it has the same effect as the
flag 'adt'.

* Deprecate debug flag `typing`

This flag is unused.

* Deprecated warnings flag

The debug flag `warnings` is only used by legacy parser. We deprecate it
in `v2.6.0` and it will be removed with the legacy parser in `v2.7.0`.

rsc/extra/worker_json_example.json

@@ -13,8 +13,8 @@
     "debug_explanations": false, "debug_fm": false, "debug_fpa": 0,
     "debug_gc": false, "debug_interpretation": false, "debug_ite": false,
     "debug_matching": 0, "debug_sat": false, "debug_split": false,
-    "debug_sum": false, "debug_triggers": false, "debug_types": false,
-    "debug_typing": false, "debug_uf": false, "debug_unsat_core": false,
+    "debug_triggers": false, "debug_types": false,
+    "debug_uf": false, "debug_unsat_core": false,
     "debug_use": false, "debug_warnings": false, "rule": 0,
     "case_split_policy": "AfterTheoryAssume", "enable_adts_cs": false,
     "max_split": 0, "replay": false, "replay_all_used_context": false,

src/bin/common/parse_command.ml

@@ -222,7 +222,12 @@ module Debug = struct
         | Arith -> Options.set_debug_arith true
         | Arrays -> Options.set_debug_arrays true
         | Bitv -> Options.set_debug_bitv true
-        | Sum -> Options.set_debug_sum true
+        | Sum ->
+          Printer.print_wrn
+            "The debug flag 'sum' is deprecated and is replaced by 'adt'. \
+             It has the same effect as 'adt' and will be removed in a future \
+             version.";
+          Options.set_debug_adt true
         | Ite -> Options.set_debug_ite true
         | Cc -> Options.set_debug_cc true
         | Combine -> Options.set_debug_combine true
@@ -238,11 +243,18 @@ module Debug = struct
         | Split -> Options.set_debug_split true
         | Triggers -> Options.set_debug_triggers true
         | Types -> Options.set_debug_types true
-        | Typing -> Options.set_debug_typing true
+        | Typing ->
+          Printer.print_wrn
+            "The debug flag 'typing' has no effect. It will be removed in a \
+             future version."
         | Uf -> Options.set_debug_uf true
         | Unsat_core -> Options.set_debug_unsat_core true
         | Use -> Options.set_debug_use true
-        | Warnings -> Options.set_debug_warnings true
+        | Warnings ->
+          Printer.print_wrn
+            "The debug flag 'warning' is deprecated and will be removed in a \
+             future version.";
+          Options.set_debug_warnings true
         | Commands -> Options.set_debug_commands true
         | Optimize -> Options.set_debug_optimize true
       )

src/bin/js/options_interface.ml

@@ -115,10 +115,8 @@ let set_options r =
   set_options_opt Options.set_debug_matching r.debug_matching;
   set_options_opt Options.set_debug_sat r.debug_sat;
   set_options_opt Options.set_debug_split r.debug_split;
-  set_options_opt Options.set_debug_sum r.debug_sum;
   set_options_opt Options.set_debug_triggers r.debug_triggers;
   set_options_opt Options.set_debug_types r.debug_types;
-  set_options_opt Options.set_debug_typing r.debug_typing;
   set_options_opt Options.set_debug_uf r.debug_uf;
   set_options_opt Options.set_debug_unsat_core r.debug_unsat_core;
   set_options_opt Options.set_debug_use r.debug_use;

src/bin/js/worker_interface.ml

@@ -194,10 +194,8 @@ type options = {
   debug_matching : int option;
   debug_sat : bool option;
   debug_split : bool option;
-  debug_sum : bool option;
   debug_triggers : bool option;
   debug_types : bool option;
-  debug_typing : bool option;
   debug_uf : bool option;
   debug_unsat_core : bool option;
   debug_use : bool option;
@@ -297,10 +295,8 @@ let init_options () = {
   debug_matching = None;
   debug_sat = None;
   debug_split = None;
-  debug_sum = None;
   debug_triggers = None;
   debug_types = None;
-  debug_typing = None;
   debug_uf = None;
   debug_unsat_core = None;
   debug_use = None;
@@ -403,7 +399,7 @@ let opt_dbg2_encoding =
   conv
     (fun dbg2 -> dbg2)
     (fun dbg2 -> dbg2)
-    (obj10
+    (obj9
        (opt "debug_fm" bool)
        (opt "debug_fpa" int31)
        (opt "debug_gc" bool)
@@ -412,17 +408,15 @@ let opt_dbg2_encoding =
        (opt "debug_matching" int31)
        (opt "debug_sat" bool)
        (opt "debug_split" bool)
-       (opt "debug_sum" bool)
        (opt "debug_triggers" bool)
     )
 
 let opt_dbg3_encoding =
   conv
     (fun dbg3 -> dbg3)
     (fun dbg3 -> dbg3)
-    (obj6
+    (obj5
        (opt "debug_types" bool)
-       (opt "debug_typing" bool)
        (opt "debug_uf" bool)
        (opt "debug_unsat_core" bool)
        (opt "debug_use" bool)
@@ -572,12 +566,10 @@ let options_to_json opt =
      opt.debug_matching,
      opt.debug_sat,
      opt.debug_split,
-     opt.debug_sum,
      opt.debug_triggers)
   in
   let dbg_opt3 =
     (opt.debug_types,
-     opt.debug_typing,
      opt.debug_uf,
      opt.debug_unsat_core,
      opt.debug_use,
@@ -703,10 +695,8 @@ let options_from_json options =
          debug_matching,
          debug_sat,
          debug_split,
-         debug_sum,
          debug_triggers) = dbg_opt2 in
     let (debug_types,
-         debug_typing,
          debug_uf,
          debug_unsat_core,
          debug_use,
@@ -790,10 +780,8 @@ let options_from_json options =
       debug_matching;
       debug_sat;
       debug_split;
-      debug_sum;
       debug_triggers;
       debug_types;
-      debug_typing;
       debug_uf;
       debug_unsat_core;
       debug_use;

src/bin/js/worker_interface.mli

@@ -77,10 +77,8 @@ type options = {
   debug_matching : int option;
   debug_sat : bool option;
   debug_split : bool option;
-  debug_sum : bool option;
   debug_triggers : bool option;
   debug_types : bool option;
-  debug_typing : bool option;
   debug_uf : bool option;
   debug_unsat_core : bool option;
   debug_use : bool option;

src/lib/util/options.ml

@@ -155,10 +155,8 @@ let debug_ite = ref false
 let debug_matching = ref 0
 let debug_sat = ref false
 let debug_split = ref false
-let debug_sum = ref false
 let debug_triggers = ref false
 let debug_types = ref false
-let debug_typing = ref false
 let debug_uf = ref false
 let debug_unsat_core = ref false
 let debug_use = ref false
@@ -186,10 +184,8 @@ let set_debug_ite b = debug_ite := b
 let set_debug_matching i = debug_matching := i
 let set_debug_sat b = debug_sat := b
 let set_debug_split b = debug_split := b
-let set_debug_sum b = debug_sum := b
 let set_debug_triggers b = debug_triggers := b
 let set_debug_types b = debug_types := b
-let set_debug_typing b = debug_typing := b
 let set_debug_uf b = debug_uf := b
 let set_debug_unsat_core b = debug_unsat_core := b
 let set_debug_use b = debug_use := b
@@ -217,10 +213,8 @@ let get_debug_ite () = !debug_ite
 let get_debug_matching () = !debug_matching
 let get_debug_sat () = !debug_sat
 let get_debug_split () = !debug_split
-let get_debug_sum () = !debug_sum
 let get_debug_triggers () = !debug_triggers
 let get_debug_types () = !debug_types
-let get_debug_typing () = !debug_typing
 let get_debug_uf () = !debug_uf
 let get_debug_unsat_core () = !debug_unsat_core
 let get_debug_use () = !debug_use

src/lib/util/options.mli

@@ -158,18 +158,12 @@ val set_debug_sat : bool -> unit
 (** Set [debug_split] accessible with {!val:get_debug_split} *)
 val set_debug_split : bool -> unit
 
-(** Set [debug_sum] accessible with {!val:get_debug_sum} *)
-val set_debug_sum : bool -> unit
-
 (** Set [debug_triggers] accessible with {!val:get_debug_triggers} *)
 val set_debug_triggers : bool -> unit
 
 (** Set [debug_types] accessible with {!val:get_debug_types} *)
 val set_debug_types : bool -> unit
 
-(** Set [debug_typing] accessible with {!val:get_debug_typing} *)
-val set_debug_typing : bool -> unit
-
 (** Set [debug_uf] accessible with {!val:get_debug_uf} *)
 val set_debug_uf : bool -> unit
 
@@ -514,9 +508,6 @@ val get_debug_intervals : unit -> bool
 val get_debug_fpa : unit -> int
 (** Default to [0]. *)
 
-(** Get the debugging flag of Sum. *)
-val get_debug_sum : unit -> bool
-
 (** Get the debugging flag of ADTs. *)
 val get_debug_adt : unit -> bool
 
@@ -532,9 +523,6 @@ val get_debug_ac : unit -> bool
 (** Get the debugging flag of SAT. *)
 val get_debug_sat : unit -> bool
 
-(** Get the debugging flag of typing. *)
-val get_debug_typing : unit -> bool
-
 (** Get the debugging flag of constructors. *)
 val get_debug_constr : unit -> bool