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

Author: SkySkimmer

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
 
@@ -385,7 +390,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
@@ -467,6 +477,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
@@ -1010,7 +1025,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
@@ -1019,7 +1034,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/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 =

pretyping/reductionops.ml

@@ -1251,7 +1251,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
@@ -1315,7 +1315,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
 }
 
@@ -1345,7 +1345,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 *)
@@ -1358,7 +1358,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)
@@ -1388,7 +1388,7 @@ let infer_conv_ustate ?(catch_incon=true) ?(pb=Conversion.CUMUL)
         let y = EConstr.Unsafe.to_constr y in
         let env = Environ.set_universes (Evd.universes sigma) env in
         match
-          Conversion.generic_conv pb ~l2r:false ~evars:(Evd.evar_handler sigma) ts
+          Conversion.generic_conv pb ~l2r:R2L ~evars:(Evd.evar_handler sigma) ts
             env (UnivProblem.Set.empty, univproblem_univ_state) x y
         with
         | Result.Ok cstr -> Some cstr

pretyping/reductionops.mli

@@ -274,7 +274,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
 }