coqargs: use algebraic datatype for -native-compiler

4 files changed, 21 insertions, 14 deletions

diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index 31656e0b07..3fe6ad0718 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -96,6 +96,9 @@ let compile opts copts ~echo ~f_in ~f_out =
   let iload_path = build_load_path opts in
   let require_libs = require_libs opts in
   let stm_options = opts.stm_flags in
+  let output_native_objects = match opts.native_compiler with
+    | NativeOff -> false | NativeOn {ondemand} -> not ondemand
+  in
   match copts.compilation_mode with
   | BuildVo ->
       Flags.record_aux_file := true;
@@ -125,7 +128,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       let _doc = Stm.join ~doc:state.doc in
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
-      let output_native_objects = opts.output_native_objects in
       Library.save_library_to ~output_native_objects ldir long_f_dot_vo (Global.opaque_tables ());
       Aux_file.record_in_aux_at "vo_compile_time"
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
@@ -169,7 +171,6 @@ let compile opts copts ~echo ~f_in ~f_out =
       let state = Vernac.load_vernac ~echo ~check:false ~interactive:false ~state long_f_dot_v in
       let doc = Stm.finish ~doc:state.doc in
       check_pending_proofs ();
-      let output_native_objects = opts.output_native_objects in
       let () = ignore (Stm.snapshot_vio ~doc ~output_native_objects ldir long_f_dot_vio) in
       Stm.reset_task_queue ()
 
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 25e9177b45..947346efcc 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -33,6 +33,8 @@ let set_type_in_type () =
 
 type color = [`ON | `AUTO | `OFF]
 
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
 type t = {
 
   load_init   : bool;
@@ -54,8 +56,7 @@ type t = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter : bool;
   enable_VM : bool;
-  enable_native_compiler : bool;
-  output_native_objects : bool;
+  native_compiler : native_compiler;
 
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
@@ -80,6 +81,11 @@ type t = {
 
 let default_toplevel = Names.(DirPath.make [Id.of_string "Top"])
 
+let default_native =
+  if Coq_config.native_compiler
+  then NativeOn {ondemand=true}
+  else NativeOff
+
 let default = {
 
   load_init   = true;
@@ -100,8 +106,7 @@ let default = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
   enable_VM = true;
-  enable_native_compiler = Coq_config.native_compiler;
-  output_native_objects = false;
+  native_compiler = default_native;
 
   stm_flags    = Stm.AsyncOpts.default_opts;
   debug        = false;
@@ -417,14 +422,14 @@ let parse_args ~help ~init arglist : t * string list =
       produced artifact(s) (`.vo`, `.vio`, `.coq-native`, ...) should be done by
       a separate flag, and the "ondemand" value removed. Once this is done, use
       [get_bool] here. *)
-      let (enable,precompile) =
+      let native_compiler =
         match (next ()) with
-        | ("yes" | "on") -> true, true
-        | "ondemand" -> true, false
-        | ("no" | "off") -> false, false
+        | ("yes" | "on") -> NativeOn {ondemand=false}
+        | "ondemand" -> NativeOn {ondemand=true}
+        | ("no" | "off") -> NativeOff
         | _ -> prerr_endline ("Error: (yes|no|ondemand) expected after option -native-compiler"); exit 1
       in
-      { oval with output_native_objects = precompile; enable_native_compiler = enable }
+      { oval with native_compiler }
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli
index c603505f8c..b89a88d1f6 100644
--- a/toplevel/coqargs.mli
+++ b/toplevel/coqargs.mli
@@ -12,6 +12,8 @@ type color = [`ON | `AUTO | `OFF]
 
 val default_toplevel : Names.DirPath.t
 
+type native_compiler = NativeOff | NativeOn of { ondemand : bool }
+
 type t = {
 
   load_init   : bool;
@@ -32,8 +34,7 @@ type t = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter : bool;
   enable_VM : bool;
-  enable_native_compiler : bool;
-  output_native_objects : bool;
+  native_compiler : native_compiler;
 
   stm_flags   : Stm.AsyncOpts.stm_opt;
   debug       : bool;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6ef0aa390d..92ac200bc0 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -188,7 +188,7 @@ let init_toplevel ~help ~init custom_init arglist =
   Global.set_engagement opts.impredicative_set;
   Global.set_indices_matter opts.indices_matter;
   Global.set_VM opts.enable_VM;
-  Global.set_native_compiler opts.enable_native_compiler;
+  Global.set_native_compiler (match opts.native_compiler with NativeOff -> false | NativeOn _ -> true);
 
   (* Allow the user to load an arbitrary state here *)
   inputstate opts;