Merge branch 'v8.5' into trunk

7 files changed, 60 insertions, 31 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2432b8d291..dafe88d8db 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -22,11 +22,6 @@ open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-let evars_of_evar_map evd =
-  { evars_val = Evd.existential_opt_value evd;
-    evars_typ = Evd.existential_type evd;
-    evars_metas = Evd.meta_type evd }
-
 exception Find_at of int
 
 let invert_tag cst tag reloc_tbl =
@@ -375,11 +370,17 @@ and  nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_type env v
 
+let evars_of_evar_map sigma =
+  { Nativelambda.evars_val = Evd.existential_opt_value sigma;
+    Nativelambda.evars_typ = Evd.existential_type sigma;
+    Nativelambda.evars_metas = Evd.meta_type sigma }
+
 let native_norm env sigma c ty =  
   if Coq_config.no_native_compiler then
     error "Native_compute reduction has been disabled at configure time."
   else
-  let penv = Environ.pre_env env in 
+  let penv = Environ.pre_env env in
+  let sigma = evars_of_evar_map sigma in
   (*
   Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
   Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
@@ -400,3 +401,10 @@ let native_norm env sigma c ty =
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         res
     | _ -> anomaly (Pp.str "Compilation failure") 
+
+let native_conv_generic pb sigma t =
+  Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
+
+let native_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
+  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma)
+    ~catch_incon:true ~pb env sigma t1 t2
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index c854e8c9c5..0352038385 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -12,6 +12,8 @@ open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val evars_of_evar_map : evar_map -> evars
+val native_norm : env -> evar_map -> constr -> types -> constr
 
-val native_norm : env -> evars -> constr -> types -> constr
+(** Conversion with inference of universe constraints *)
+val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bb21b87d37..c2cf1f83d5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -929,25 +929,20 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 	      if not (occur_existential cty || occur_existential tval) then
-		begin 
-		  try
-		    let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in 
-		    ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
-		  with Reduction.NotConvertible -> 
-		    error_actual_type_loc loc env !evdref cj tval 
+		let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in
+		if b then (evdref := evd; cj)
+		else
+		  error_actual_type_loc loc env !evdref cj tval 
                       (ConversionFailed (env,cty,tval))
-		end
 	      else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
-            let evars = Nativenorm.evars_of_evar_map !evdref in
-	    let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in 
             begin
-              try
-                ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj
-              with Reduction.NotConvertible -> 
+	      let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in
+	      if b then (evdref := evd; cj)
+	      else
                 error_actual_type_loc loc env !evdref cj tval 
                   (ConversionFailed (env,cty,tval))
             end
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dc70f36ccf..bb1bc7d2ea 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1251,9 +1251,6 @@ let pb_equal = function
   | Reduction.CUMUL -> Reduction.CONV
   | Reduction.CONV -> Reduction.CONV
 
-let sort_cmp cv_pb s1 s2 u = 
-  Reduction.check_sort_cmp_universes cv_pb s1 s2 u
-
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   try
     let evars ev = safe_evar_value sigma ev in
@@ -1295,8 +1292,8 @@ let sigma_univ_state =
   { Reduction.compare = sigma_compare_sorts;
     Reduction.compare_instances = sigma_compare_instances }
 
-let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) 
-    env sigma x y = 
+let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
+    ?(ts=full_transparent_state) env sigma x y =
   try 
     let b, sigma = 
       let b, cstrs = 
@@ -1313,14 +1310,23 @@ let infer_conv ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_s
       if b then sigma, true
       else
 	let sigma' = 
-	  Reduction.generic_conv pb false (safe_evar_value sigma) ts 
+	  conv_fun pb ~l2r:false sigma ts
 	    env (sigma, sigma_univ_state) x y in
 	  sigma', true
   with
   | Reduction.NotConvertible -> sigma, false
   | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
   | e when is_anomaly e -> error "Conversion test raised an anomaly"
-    
+
+let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
+      Reduction.generic_conv pb ~l2r (safe_evar_value sigma))
+
+(* This reference avoids always having to link C code with the kernel *)
+let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:full_transparent_state)
+let set_vm_infer_conv f = vm_infer_conv := f
+let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
+  !vm_infer_conv ~pb env t1 t2
+
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5e1c467c82..d5a844847c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -251,8 +251,6 @@ type conversion_test = constraints -> constraints
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val sort_cmp : env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit
-
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
 val is_fconv : conv_pb -> env ->  evar_map -> constr -> constr -> bool
@@ -266,7 +264,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env ->  evar_map -> constr
  *)
 val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> constr -> constr -> bool
 
-(** [infer_fconv] Adds necessary universe constraints to the evar map.
+(** [infer_conv] Adds necessary universe constraints to the evar map.
     pb defaults to CUMUL and ts to a full transparent state.
     @raises UniverseInconsistency iff catch_incon is set to false, 
     otherwise returns false in that case.
@@ -274,6 +272,20 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
   env -> evar_map -> constr -> constr -> evar_map * bool
 
+(** Conversion with inference of universe constraints *)
+val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool) -> unit
+val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
+
+
+(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
+conversion function. Used to pretype vm and native casts. *)
+val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
+    (constr, evar_map) Reduction.generic_conversion_function) ->
+  ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
+  evar_map -> constr -> constr -> evar_map * bool
+
 (** {6 Special-Purpose Reduction Functions } *)
 
 val whd_meta : evar_map -> constr -> constr
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index f768e4feef..46af784dda 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -312,3 +312,9 @@ and nf_cofix env cf =
 let cbv_vm env c t  =
   let v = Vconv.val_of_constr env c in
   nf_val env v t
+
+let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
+  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb)
+    ~catch_incon:true ~pb env sigma t1 t2
+
+let _ = Reductionops.set_vm_infer_conv vm_infer_conv
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 7dabbc6cb0..9421b2d859 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -8,7 +8,7 @@
 
 open Term
 open Environ
+open Evd
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr
-