Lazy conversion add flag to disable first order approximation, use for VM fallback

checker/coqchk_main.ml

@@ -146,11 +146,22 @@ let indices_matter = ref false
 
 let enable_vm = ref false
 
+let warn_no_bytecode =
+  CWarnings.create ~name:"bytecode-compiler-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler
+    Pp.(fun () ->
+        str "Bytecode compiler is disabled," ++ spc() ++
+        str "-bytecode-compiler option ignored.")
+
 let make_senv () =
   let senv = Safe_typing.empty_environment in
   let senv = Safe_typing.set_impredicative_set !impredicative_set senv in
   let senv = Safe_typing.set_indices_matter !indices_matter senv in
-  let senv = Safe_typing.set_VM !enable_vm senv in
+  let senv =
+    if !enable_vm && not Coq_config.bytecode_compiler then begin
+      warn_no_bytecode ();
+      senv
+    end else Safe_typing.set_VM !enable_vm senv
+  in
   let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *)
   Safe_typing.set_native_compiler false senv
 

doc/tools/rocqrst/repl/rocqtop.py

@@ -103,7 +103,7 @@ def sendone(self, sentence):
     def send_initial_options(self):
         """Options to send when starting the toplevel and after a Reset Initial."""
         self.sendone('Set Rocqtop Exit On Error.')
-        self.sendone('Set Warnings "+default".')
+        self.sendone('Set Warnings "+default,-vm-compute-disabled".')
 
 def sendmany(*sentences):
     """A small demo: send each sentence in sentences and print the output"""

kernel/conversion.ml

@@ -119,14 +119,19 @@ let pure_stack lfts stk =
 (*                         Conversion                               *)
 (********************************************************************)
 
+type firstorder_mode =
+  | Eager
+  | L2R
+  | R2L
+
 (* Conversion utility functions *)
 
 (* functions of this type are called from the kernel *)
 type 'a kernel_conversion_function = env -> 'a -> 'a -> (unit, unit) result
 
 (* functions of this type can be called from outside the kernel *)
 type 'a extended_conversion_function =
-  ?l2r:bool -> ?reds:TransparentState.t -> env ->
+  ?l2r:firstorder_mode -> ?reds:TransparentState.t -> env ->
   ?evars:evar_handler ->
   'a -> 'a -> (unit, unit) result
 
@@ -384,7 +389,12 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
 and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Control.check_for_interrupt ();
   (* First head reduce both terms *)
-  let ninfos = infos_with_reds infos.cnv_inf RedFlags.betaiotazeta in
+  let ninfos = match l2r with
+    | Eager ->
+      let all = RedFlags.(red_add_transparent all (red_transparent (info_flags infos.cnv_inf))) in
+      infos_with_reds infos.cnv_inf all
+    | L2R | R2L -> infos_with_reds infos.cnv_inf RedFlags.betaiotazeta
+  in
   let appr1 = whd_stack ninfos infos.lft_tab (fst st1) (snd st1) in
   let appr2 = whd_stack ninfos infos.rgt_tab (fst st2) (snd st2) in
   eqwhnf cv_pb l2r infos (lft1, appr1) (lft2, appr2) cuniv
@@ -466,6 +476,11 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
           let () = Control.check_for_interrupt () in
           (* Determine which constant to unfold first *)
           let unfold_left =
+            let l2r = match l2r with
+              | L2R -> true
+              | R2L -> false
+              | Eager -> assert false
+            in
             let order = Conv_oracle.oracle_compare oracle (to_er fl1) (to_er fl2) in
             match order with
             | Conv_oracle.Left -> true
@@ -1014,7 +1029,7 @@ let () =
       let state = info_univs infos in
       let qual_equal q1 q2 = CClosure.eq_quality infos q1 q2 in
       let infos = { cnv_inf = infos; cnv_typ = true; lft_tab = tab; rgt_tab = tab; err_ret = box; } in
-      let state', _ = ccnv CONV false infos el_id el_id a b (state, checked_universes_gen qual_equal) in
+      let state', _ = ccnv CONV R2L infos el_id el_id a b (state, checked_universes_gen qual_equal) in
       assert (state==state');
       true
     with
@@ -1023,7 +1038,7 @@ let () =
   in
   CClosure.set_conv conv
 
-let gen_conv ~typed cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=default_evar_handler env) t1 t2 =
+let gen_conv ~typed cv_pb ?(l2r=R2L) ?(reds=TransparentState.full) env ?(evars=default_evar_handler env) t1 t2 =
   let univs = Environ.universes env in
   let state = univs in
   let b =

kernel/conversion.mli

@@ -14,9 +14,15 @@ open Environ
 (***********************************************************************
   s conversion functions *)
 
+(** Which side to unfold first (default: R2L ie unfold right side first) *)
+type firstorder_mode =
+  | Eager
+  | L2R
+  | R2L
+
 type 'a kernel_conversion_function = env -> 'a -> 'a -> (unit, unit) result
 type 'a extended_conversion_function =
-  ?l2r:bool -> ?reds:TransparentState.t -> env ->
+  ?l2r:firstorder_mode -> ?reds:TransparentState.t -> env ->
   ?evars:CClosure.evar_handler ->
   'a -> 'a -> (unit, unit) result
 
@@ -57,7 +63,7 @@ val conv_leq : types extended_conversion_function
 
 (** The failure values depend on the universe state functions
     (for better error messages). *)
-val generic_conv : conv_pb -> l2r:bool
+val generic_conv : conv_pb -> l2r:firstorder_mode
   -> TransparentState.t -> env -> ?evars:CClosure.evar_handler
   -> ('a, 'err) generic_conversion_function
 

kernel/declareops.ml

@@ -19,6 +19,10 @@ let noh hcons x = snd (hcons x)
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
+let configure_enabled_native = match Coq_config.native_compiler with
+  | NativeOff -> false
+  | NativeOn _ -> true
+
 let safe_flags oracle = {
   check_guarded = true;
   check_positive = true;
@@ -27,8 +31,8 @@ let safe_flags oracle = {
   conv_oracle = oracle;
   share_reduction = true;
   unfold_dep_heuristic = false;
-  enable_VM = true;
-  enable_native_compiler = true;
+  enable_VM = Coq_config.bytecode_compiler;
+  enable_native_compiler = configure_enabled_native;
   indices_matter = true;
   impredicative_set = false;
   sprop_allowed = true;

kernel/environ.ml

@@ -598,11 +598,18 @@ let same_flags {
   allow_uip == alt.allow_uip
 [@warning "+9"]
 
+let check_flags c =
+  assert (Coq_config.bytecode_compiler || not c.enable_VM);
+  assert (match Coq_config.native_compiler with
+      | NativeOff -> not c.enable_native_compiler
+      | NativeOn _ -> true)
+
 let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
 
 let set_typing_flags c env =
   if same_flags env.env_typing_flags c then env
   else
+    let () = check_flags c in
     let env = { env with env_typing_flags = c } in
     let env = set_type_in_type (not c.check_universes) env in
     let env = { env with env_qualities = QGraph.set_ignore_constraints (not c.check_eliminations) env.env_qualities } in

kernel/mod_typing.ml

@@ -53,10 +53,10 @@ let rec rebuild_mp mp l =
   | i::r -> rebuild_mp (MPdot(mp,i)) r
 
 let infer_gen_conv state env c1 c2 =
-  Conversion.generic_conv Conversion.CONV ~l2r:false TransparentState.full env state c1 c2
+  Conversion.generic_conv Conversion.CONV ~l2r:R2L TransparentState.full env state c1 c2
 
 let infer_gen_conv_leq state env c1 c2 =
-  Conversion.generic_conv Conversion.CUMUL ~l2r:false TransparentState.full env state c1 c2
+  Conversion.generic_conv Conversion.CUMUL ~l2r:R2L TransparentState.full env state c1 c2
 
 type with_body = {
   w_def : Constr.t;

kernel/subtyping.ml

@@ -89,7 +89,7 @@ let check_conv_error error why state poly pb env a1 a2 =
   if poly then match Conversion.default_conv pb env a1 a2 with
   | Result.Ok () -> fst state
   | Result.Error () ->  error (IncompatiblePolymorphism (env, a1, a2))
-  else match Conversion.generic_conv pb ~l2r:false TransparentState.full env state a1 a2 with
+  else match Conversion.generic_conv pb ~l2r:R2L TransparentState.full env state a1 a2 with
   | Result.Ok state -> state
   | Result.Error None -> error why
   | Result.Error (Some (Univ e)) -> error (IncompatibleUniverses { err = e; env; t1 = a1; t2 = a2 })

kernel/typeops.ml

@@ -528,7 +528,7 @@ let should_invert_case env r ci =
 let type_case_scrutinee env (mib, _mip) (u', largs) u pms (pctx, p) c =
   let (params, realargs) = List.chop mib.mind_nparams largs in
   (* Check that the type of the scrutinee is <= the expected argument type *)
-  let iter p1 p2 = match Conversion.conv ~l2r:true env p1 p2 with
+  let iter p1 p2 = match Conversion.conv ~l2r:L2R env p1 p2 with
   | Result.Ok () -> ()
   | Result.Error () -> raise NotConvertible
   in

kernel/vconv.ml

@@ -220,7 +220,7 @@ let warn_bytecode_compiler_failed =
 
 let vm_conv_gen (type err) cv_pb sigma env univs t1 t2 =
   if not (typing_flags env).Declarations.enable_VM then
-    Conversion.generic_conv cv_pb ~l2r:false ~evars:sigma.Genlambda.evars_val
+    Conversion.generic_conv cv_pb ~l2r:Eager ~evars:sigma.Genlambda.evars_val
       TransparentState.full env univs t1 t2
   else
   let exception Error of err in
@@ -235,7 +235,7 @@ let vm_conv_gen (type err) cv_pb sigma env univs t1 t2 =
   | Error e -> Result.Error (Some e)
   | Not_found | Invalid_argument _ | Vmerrors.CompileError _ ->
     warn_bytecode_compiler_failed ();
-    Conversion.generic_conv cv_pb ~l2r:false ~evars:sigma.Genlambda.evars_val
+    Conversion.generic_conv cv_pb ~l2r:Eager ~evars:sigma.Genlambda.evars_val
       TransparentState.full env univs t1 t2
 
 let vm_conv cv_pb env t1 t2 =

kernel/vmbytegen.ml

@@ -975,6 +975,7 @@ let warn_compile_error =
     Vmerrors.pr_error
 
 let compile ~fail_on_error ~uinstance env sigma c =
+  if not (typing_flags env).enable_VM then None else
   try NewProfile.profile "vm_compile" (fun () -> Some (compile ~uinstance env sigma c)) ()
   with Vmerrors.CompileError msg as exn ->
     let exn = Exninfo.capture exn in

pretyping/reductionops.ml

@@ -1253,7 +1253,7 @@ let is_fconv ?(reds=TransparentState.full) pb env sigma t1 t2 =
     let evars = Evd.evar_handler sigma in
     try
       let env = Environ.set_universes (Evd.universes sigma) env in
-      begin match Conversion.generic_conv ~l2r:false pb ~evars reds env (sigma, CheckUnivs.checked_universes) t1 t2 with
+      begin match Conversion.generic_conv ~l2r:R2L pb ~evars reds env (sigma, CheckUnivs.checked_universes) t1 t2 with
       | Result.Ok (_ : Evd.evar_map) -> true
       | Result.Error None -> false
       | Result.Error (Some e) -> Empty.abort e
@@ -1282,7 +1282,7 @@ let is_conv_nounivs ?(reds=TransparentState.full) env sigma t1 t2 =
         compare_cumul_instances = (fun _ _ _ _ () -> Ok ());
       }
       in
-      begin match Conversion.generic_conv ~l2r:false CONV ~evars reds env ((), ignore_univs) t1 t2 with
+      begin match Conversion.generic_conv ~l2r:R2L CONV ~evars reds env ((), ignore_univs) t1 t2 with
       | Result.Ok () -> true
       | Result.Error None -> false
       | Result.Error (Some e) -> Empty.abort e
@@ -1341,7 +1341,7 @@ let univproblem_univ_state =
     compare_cumul_instances = univproblem_check_inductive_instances; }
 
 type genconv = {
-  genconv : 'a 'err. conv_pb -> l2r:bool -> Evd.evar_map -> TransparentState.t ->
+  genconv : 'a 'err. conv_pb -> l2r:Conversion.firstorder_mode -> Evd.evar_map -> TransparentState.t ->
     Environ.env -> ('a, 'err) Conversion.generic_conversion_function
 }
 
@@ -1371,7 +1371,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL)
            approximation. This may result in unsatisfiable constraints even if
            some unfoldings of the arguments could have been unified, but this
            should be exceedingly rare. *)
-        let ans = match conv_fun.genconv pb ~l2r:false sigma ts env (UnivProblem.Set.empty, univproblem_univ_state) x y with
+        let ans = match conv_fun.genconv pb ~l2r:R2L sigma ts env (UnivProblem.Set.empty, univproblem_univ_state) x y with
         | Result.Ok cstr -> Some cstr
         | Result.Error None ->
           None (* no universe unification can make these terms convertible *)
@@ -1384,7 +1384,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL)
           | sigma -> Some sigma
           | exception UGraph.UniverseInconsistency _ | exception Evd.UniversesDiffer ->
             (* Retry with local universe checking, which may imply constant unfolding *)
-            match conv_fun.genconv pb ~l2r:false sigma ts env (sigma, sigma_univ_state) x y with
+            match conv_fun.genconv pb ~l2r:R2L sigma ts env (sigma, sigma_univ_state) x y with
             | Result.Ok sigma -> Some sigma
             | Result.Error None -> None
             | Result.Error (Some e) -> raise (UGraph.UniverseInconsistency e)

pretyping/reductionops.mli

@@ -273,7 +273,7 @@ val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
   evar_map option
 
 type genconv = {
-  genconv : 'a 'err. conv_pb -> l2r:bool -> Evd.evar_map -> TransparentState.t ->
+  genconv : 'a 'err. conv_pb -> l2r:Conversion.firstorder_mode -> Evd.evar_map -> TransparentState.t ->
     Environ.env -> ('a, 'err) Conversion.generic_conversion_function
 }
 

sysinit/coqargs.ml

@@ -41,6 +41,7 @@ type require_injection = { lib: string; prefix: string option; export: export_fl
 type injection_command =
   | OptionInjection of (string list * option_command)
   | RequireInjection of require_injection
+  | WarnNoBytecode
   | WarnNoNative of string
   | WarnNativeDeprecated
 
@@ -106,8 +107,6 @@ type t = {
 
 let default_toplevel = "Top"
 
-let default_native = Coq_config.native_compiler
-
 let default_logic_config = {
   impredicative_set = false;
   indices_matter = false;
@@ -120,8 +119,8 @@ let default_config = {
   logic        = default_logic_config;
   rcfile       = None;
   coqlib       = None;
-  enable_VM    = true;
-  native_compiler = default_native;
+  enable_VM    = Coq_config.bytecode_compiler;
+  native_compiler = Coq_config.native_compiler;
   native_output_dir = ".coq-native";
   native_include_dirs = [];
   output_directory = None;
@@ -229,6 +228,10 @@ let parse_option_set opt =
     let v = String.sub opt (eqi+1) (len - eqi - 1) in
     to_opt_key (String.sub opt 0 eqi), Some v
 
+let get_bytecode_compiler_warns b =
+  if b && not Coq_config.bytecode_compiler then [WarnNoBytecode]
+  else []
+
 let get_native_compiler s =
   (* We use two boolean flags because the four states make sense, even if
      only three are accessible to the user at the moment. The selection of the
@@ -345,7 +348,10 @@ let parse_args ~init arglist : t * string list =
     |"-w" | "-W" -> add_set_warnings oval (next())
 
     |"-bytecode-compiler" ->
-      { oval with config = { oval.config with enable_VM = get_bool ~opt (next ()) }}
+      let b = get_bool ~opt (next ()) in
+      let warn = get_bytecode_compiler_warns b in
+      { oval with config = { oval.config with enable_VM = b };
+                  pre = { oval.pre with injections = warn @ oval.pre.injections }}
 
     |"-native-compiler" ->
       let native_compiler, warn = get_native_compiler (next ()) in

sysinit/coqargs.mli

@@ -30,6 +30,7 @@ type injection_command =
   | RequireInjection of require_injection
   (** Require libraries before the initial state is
       ready. *)
+  | WarnNoBytecode
   | WarnNoNative of string
   (** Used so that "-w -native-compiler-disabled -native-compiler yes"
      does not cause a warning. The native option must be processed

sysinit/coqinit.ml

@@ -219,6 +219,11 @@ let require_file ~intern ~prefix ~lib ~export ~allow_failure =
   with (Synterp.UnmappedLibrary _ | Synterp.NotFoundLibrary _) when allow_failure ->
     warn_require_not_found (mfrom, mp)
 
+let warn_no_bytecode =
+  CWarnings.create ~name:"bytecode-compiler-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler
+    Pp.(fun () -> str "Bytecode compiler is disabled," ++ spc() ++
+                  str "-bytecode-compiler option ignored.")
+
 let warn_no_native_compiler =
   CWarnings.create_in Nativeconv.w_native_disabled
     Pp.(fun s -> strbrk "Native compiler is disabled," ++
@@ -253,6 +258,7 @@ let handle_injection ~intern = let open Coqargs in function
   | RequireInjection {lib;prefix;export;allow_failure} ->
     require_file ~intern ~lib ~prefix ~export ~allow_failure
   | OptionInjection o -> set_option o
+  | WarnNoBytecode -> warn_no_bytecode ()
   | WarnNoNative s -> warn_no_native_compiler s
   | WarnNativeDeprecated -> warn_deprecated_native_compiler ()
 

theories/Corelib/Numbers/Cyclic/Int63/Sint63Axioms.v

@@ -20,7 +20,7 @@ Local Infix "^" := Z.pow : Z_scope.
 Local Notation "x <= y" := (Z.compare x y <> Gt) : Z_scope.
 Local Notation "x < y" := (Z.compare x y = Lt) : Z_scope.
 
-Definition min_int := Eval vm_compute in (lsl 1 62).
+Definition min_int := Eval lazy in (lsl 1 62).
 
 (** Translation to and from Z *)
 Definition to_Z (i : int) :=

theories/Corelib/Numbers/Cyclic/Int63/Uint63Axioms.v

@@ -32,7 +32,7 @@ Definition size := 63%nat.
 Definition digits := 63%uint63.
 
 (** The biggest int *)
-Definition max_int := Eval vm_compute in sub 0 1.
+Definition max_int := Eval lazy in sub 0 1.
 
 (** Access to the nth digits *)
 Definition get_digit x p := ltb 0 (land x (lsl 1 p)).