From 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 8 Oct 2015 18:06:55 +0200
Subject: Fix #4346 1/2: native casts were not inferring universe constraints.

---
 pretyping/nativenorm.ml    | 20 ++++++++++++++------
 pretyping/nativenorm.mli   |  6 ++++--
 pretyping/pretyping.ml     |  8 +++-----
 pretyping/reductionops.ml  | 11 +++++++----
 pretyping/reductionops.mli |  9 ++++++++-
 5 files changed, 36 insertions(+), 18 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 2432b8d291..949a28a1f4 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 x y =
+  Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma)
+    ~catch_incon:true ~pb env sigma x y
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 746b4000ee..e1e8982e1e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -942,12 +942,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	  | 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..a24773b6e6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1295,8 +1295,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 +1313,17 @@ 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))
+
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1df2a73b2e..b179dbc95e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -266,7 +266,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 +274,13 @@ 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
 
+(** [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
-- 
cgit v1.2.3


From 44817bf722eacb0379bebc7e435bfafa503d574f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Oct 2015 14:21:45 +0200
Subject:  Fix #4346 2/2: VM casts were not inferring universe constraints.

---
 pretyping/nativenorm.ml    |  4 ++--
 pretyping/pretyping.ml     | 11 ++++-------
 pretyping/reductionops.ml  |  3 ---
 pretyping/reductionops.mli |  2 --
 pretyping/vnorm.ml         |  4 ++++
 pretyping/vnorm.mli        |  4 ++++
 6 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 949a28a1f4..dafe88d8db 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -405,6 +405,6 @@ let native_norm env sigma c ty =
 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 x y =
+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 x y
+    ~catch_incon:true ~pb env sigma t1 t2
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e1e8982e1e..f6c1867285 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -929,14 +929,11 @@ 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) = Vnorm.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 ->
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a24773b6e6..d25e273a3e 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
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b179dbc95e..42c2c9c6e6 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 -> universes -> 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
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index f768e4feef..2c6ac7a292 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -312,3 +312,7 @@ 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
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 7dabbc6cb0..99856a8d9a 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -8,7 +8,11 @@
 
 open Term
 open Environ
+open Evd
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr
 
+(** Conversion with inference of universe constraints *)
+val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
+  evar_map * bool
-- 
cgit v1.2.3


From 048b87502eced0a46a654f3f95de8f1968004db1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Oct 2015 18:15:21 +0200
Subject: Avoid dependency of the pretyper on C code.

Using the same hack as in the kernel: VM conversion is a reference to
a function, updated when modules using C code are actually linked.

This hack should one day go away, but always linking C code may produce some
other trouble (with the OCaml debugger for instance), so better be safe
for now.
---
 pretyping/pretyping.ml     | 2 +-
 pretyping/reductionops.ml  | 6 ++++++
 pretyping/reductionops.mli | 7 +++++++
 pretyping/vnorm.ml         | 2 ++
 pretyping/vnorm.mli        | 4 ----
 5 files changed, 16 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f6c1867285..d484df69c1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -929,7 +929,7 @@ 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
-		let (evd,b) = Vnorm.vm_infer_conv env !evdref cty tval in
+		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 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index d25e273a3e..bb1bc7d2ea 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1321,6 +1321,12 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
 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 42c2c9c6e6..d5a844847c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -272,6 +272,13 @@ 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 ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 2c6ac7a292..46af784dda 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -316,3 +316,5 @@ let cbv_vm env c 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 99856a8d9a..9421b2d859 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.mli
@@ -12,7 +12,3 @@ open Evd
 
 (** {6 Reduction functions } *)
 val cbv_vm : env -> constr -> types -> constr
-
-(** Conversion with inference of universe constraints *)
-val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool
-- 
cgit v1.2.3