Clean and fix definitions of options.

- Provide new helper functions in `Goptions` on the model of
  `declare_bool_option_and_ref`;

- Use these helper functions in many parts of the code base
  (encapsulates the corresponding references);

- Move almost all options from `declare_string_option` to
  `declare_stringopt_option` (only "Warnings" continue to use the
  former).  This means that these options now support `Unset` to get
  back to the default setting.  Note that there is a naming
  misalignment since `declare_int_option` is similar to
  `declare_stringopt_option` and supports `Unset`.  When "Warning" is
  eventually migrated to support `Unset` as well, we can remove
  `declare_string_option` and rename `declare_stringopt_option` to
  `declare_string_option`.

- For some vernac options and flags that have an equivalent
  command-line option or flag, implement it like the standard `-set`
  and `-unset`.

3 files changed, 37 insertions, 80 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 1958fff4cc..9eeba614c7 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -27,7 +27,13 @@ open NumCompat
 open Q.Notations
 open Mutils
 
-let use_simplex = ref true
+let use_simplex =
+  Goptions.declare_bool_option_and_ref ~depr:false ~key:["Simplex"] ~value:true
+
+(* If set to some [file], arithmetic goals are dumped in [file].v *)
+
+let dump_file =
+  Goptions.declare_stringopt_option_and_ref ~depr:false ~key:["Dump"; "Arith"]
 
 type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
 type zres = (Mc.zArithProof, int * Mc.z list) res
@@ -203,19 +209,19 @@ let fourier_linear_prover l =
   | Inl _ -> None
 
 let direct_linear_prover l =
-  if !use_simplex then Simplex.find_unsat_certificate l
+  if use_simplex () then Simplex.find_unsat_certificate l
   else fourier_linear_prover l
 
 let find_point l =
   let open Util in
-  if !use_simplex then Simplex.find_point l
+  if use_simplex () then Simplex.find_point l
   else
     match Mfourier.Fourier.find_point l with
     | Inr _ -> None
     | Inl cert -> Some cert
 
 let optimise v l =
-  if !use_simplex then Simplex.optimise v l else Mfourier.Fourier.optimise v l
+  if use_simplex () then Simplex.optimise v l else Mfourier.Fourier.optimise v l
 
 let dual_raw_certificate l =
   if debug then begin
@@ -981,13 +987,11 @@ let xlia_simplex env red sys =
   with FoundProof prf -> compile_prf sys (Step (0, prf, Done))
 
 let xlia env0 en red sys =
-  if !use_simplex then xlia_simplex env0 red sys else xlia en red sys
-
-let dump_file = ref None
+  if use_simplex () then xlia_simplex env0 red sys else xlia en red sys
 
 let gen_bench (tac, prover) can_enum prfdepth sys =
   let res = prover can_enum prfdepth sys in
-  ( match !dump_file with
+  ( match dump_file () with
   | None -> ()
   | Some file ->
     let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in
diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli
index cabd36ebb7..5b215549b0 100644
--- a/plugins/micromega/certificate.mli
+++ b/plugins/micromega/certificate.mli
@@ -12,16 +12,12 @@ module Mc = Micromega
 
 (** [use_simplex] is bound to the Coq option Simplex.
     If set, use the Simplex method, otherwise use Fourier *)
-val use_simplex : bool ref
+val use_simplex : unit -> bool
 
 type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
 type zres = (Mc.zArithProof, int * Mc.z list) res
 type qres = (Mc.q Mc.psatz, int * Mc.q list) res
 
-(** [dump_file] is bound to the Coq option Dump Arith.
-    If set to some [file], arithmetic goals are dumped in filexxx.v *)
-val dump_file : string option ref
-
 (** [q_cert_of_pos prf] converts a Sos proof into a rational Coq proof *)
 val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 43f6f5a35e..7e4c4ce5c6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -37,74 +37,31 @@ let debug = false
 let max_depth = max_int
 
 (* Search limit for provers over Q R *)
-let lra_proof_depth = ref max_depth
+let lra_proof_depth =
+  declare_int_option_and_ref ~depr:false ~key:["Lra"; "Depth"] ~value:max_depth
 
 (* Search limit for provers over Z *)
-let lia_enum = ref true
-let lia_proof_depth = ref max_depth
-let get_lia_option () = (!Certificate.use_simplex, !lia_enum, !lia_proof_depth)
-let get_lra_option () = !lra_proof_depth
+let lia_enum =
+  declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Enum"] ~value:true
+
+let lia_proof_depth =
+  declare_int_option_and_ref ~depr:false ~key:["Lia"; "Depth"] ~value:max_depth
+
+let get_lia_option () =
+  (Certificate.use_simplex (), lia_enum (), lia_proof_depth ())
 
 (* Enable/disable caches *)
 
-let use_lia_cache = ref true
-let use_nia_cache = ref true
-let use_nra_cache = ref true
-let use_csdp_cache = ref true
-
-let () =
-  let int_opt l vref =
-    { optdepr = false
-    ; optkey = l
-    ; optread = (fun () -> Some !vref)
-    ; optwrite =
-        (fun x -> vref := match x with None -> max_depth | Some v -> v) }
-  in
-  let lia_enum_opt =
-    { optdepr = false
-    ; optkey = ["Lia"; "Enum"]
-    ; optread = (fun () -> !lia_enum)
-    ; optwrite = (fun x -> lia_enum := x) }
-  in
-  let solver_opt =
-    { optdepr = false
-    ; optkey = ["Simplex"]
-    ; optread = (fun () -> !Certificate.use_simplex)
-    ; optwrite = (fun x -> Certificate.use_simplex := x) }
-  in
-  let dump_file_opt =
-    { optdepr = false
-    ; optkey = ["Dump"; "Arith"]
-    ; optread = (fun () -> !Certificate.dump_file)
-    ; optwrite = (fun x -> Certificate.dump_file := x) }
-  in
-  let lia_cache_opt =
-    { optdepr = false
-    ; optkey = ["Lia"; "Cache"]
-    ; optread = (fun () -> !use_lia_cache)
-    ; optwrite = (fun x -> use_lia_cache := x) }
-  in
-  let nia_cache_opt =
-    { optdepr = false
-    ; optkey = ["Nia"; "Cache"]
-    ; optread = (fun () -> !use_nia_cache)
-    ; optwrite = (fun x -> use_nia_cache := x) }
-  in
-  let nra_cache_opt =
-    { optdepr = false
-    ; optkey = ["Nra"; "Cache"]
-    ; optread = (fun () -> !use_nra_cache)
-    ; optwrite = (fun x -> use_nra_cache := x) }
-  in
-  let () = declare_bool_option solver_opt in
-  let () = declare_bool_option lia_cache_opt in
-  let () = declare_bool_option nia_cache_opt in
-  let () = declare_bool_option nra_cache_opt in
-  let () = declare_stringopt_option dump_file_opt in
-  let () = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
-  let () = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in
-  let () = declare_bool_option lia_enum_opt in
-  ()
+let use_lia_cache =
+  declare_bool_option_and_ref ~depr:false ~key:["Lia"; "Cache"] ~value:true
+
+let use_nia_cache =
+  declare_bool_option_and_ref ~depr:false ~key:["Nia"; "Cache"] ~value:true
+
+let use_nra_cache =
+  declare_bool_option_and_ref ~depr:false ~key:["Nra"; "Cache"] ~value:true
+
+let use_csdp_cache () = true
 
 (**
   * Initialize a tag type to the Tag module declaration (see Mutils).
@@ -2101,7 +2058,7 @@ struct
 
   let memo_opt use_cache cache_file f =
     let memof = memo cache_file f in
-    fun x -> if !use_cache then memof x else f x
+    fun x -> if use_cache () then memof x else f x
 end
 
 module CacheCsdp = MakeCache (struct
@@ -2281,7 +2238,7 @@ let memo_nra =
 
 let linear_prover_Q =
   { name = "linear prover"
-  ; get_option = get_lra_option
+  ; get_option = lra_proof_depth
   ; prover =
       (fun (o, l) ->
         lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2292,7 +2249,7 @@ let linear_prover_Q =
 
 let linear_prover_R =
   { name = "linear prover"
-  ; get_option = get_lra_option
+  ; get_option = lra_proof_depth
   ; prover =
       (fun (o, l) ->
         lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
@@ -2303,7 +2260,7 @@ let linear_prover_R =
 
 let nlinear_prover_R =
   { name = "nra"
-  ; get_option = get_lra_option
+  ; get_option = lra_proof_depth
   ; prover = memo_nra
   ; hyps = hyps_of_cone
   ; compact = compact_cone