Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.

1 files changed, 33 insertions, 27 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index b9f14aa43..2d4296fe4 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -53,16 +53,16 @@ let apply_coercion_args env evd check isproj argl funj =
   let rec apply_rec acc typ = function
     | [] ->
       if isproj then
-	let cst = fst (destConst !evdref (EConstr.of_constr (j_val funj))) in
+	let cst = fst (destConst !evdref (j_val funj)) in
 	let p = Projection.make cst false in
 	let pb = lookup_projection p env in
 	let args = List.skipn pb.Declarations.proj_npars argl in
 	let hd, tl = match args with hd :: tl -> hd, tl | [] -> assert false in
-	  { uj_val = EConstr.Unsafe.to_constr (applist (mkProj (p, hd), tl));
-	    uj_type = EConstr.Unsafe.to_constr typ }
+	  { uj_val = applist (mkProj (p, hd), tl);
+	    uj_type = typ }
       else
-	{ uj_val = EConstr.Unsafe.to_constr (applist (EConstr.of_constr (j_val funj),argl));
-	  uj_type = EConstr.Unsafe.to_constr typ }
+	{ uj_val = applist (j_val funj,argl);
+	  uj_type = typ }
     | h::restl -> (* On devrait pouvoir s'arranger pour qu'on n'ait pas a faire hnf_constr *)
       match EConstr.kind !evdref (EConstr.of_constr (whd_all env !evdref typ)) with
       | Prod (_,c1,c2) ->
@@ -71,7 +71,7 @@ let apply_coercion_args env evd check isproj argl funj =
         apply_rec (h::acc) (Vars.subst1 h c2) restl
       | _ -> anomaly (Pp.str "apply_coercion_args")
   in
-  let res = apply_rec [] (EConstr.of_constr funj.uj_type) argl in
+  let res = apply_rec [] funj.uj_type argl in
     !evdref, res
 
 (* appliquer le chemin de coercions de patterns p *)
@@ -367,7 +367,7 @@ let apply_coercion env sigma p hj typ_cl =
         (fun (ja,typ_cl,sigma) i ->
 	  let ((fv,isid,isproj),ctx) = coercion_value i in
 	  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
-	  let argl = (class_args_of env sigma typ_cl)@[EConstr.of_constr ja.uj_val] in
+	  let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 	  let sigma, jres = 
 	    apply_coercion_args env sigma true isproj argl fv 
 	  in
@@ -375,7 +375,7 @@ let apply_coercion env sigma p hj typ_cl =
 	      { uj_val = ja.uj_val; uj_type = jres.uj_type }
 	     else
 	      jres),
-	    EConstr.of_constr jres.uj_type,sigma)
+	    jres.uj_type,sigma)
       (hj,typ_cl,sigma) p
     in evd, j
   with NoCoercion as e -> raise e
@@ -383,23 +383,23 @@ let apply_coercion env sigma p hj typ_cl =
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =
-  let t = whd_all env evd (EConstr.of_constr j.uj_type) in
+  let t = whd_all env evd j.uj_type in
   let t = EConstr.of_constr t in
     match EConstr.kind evd t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
 	let (evd',t) = Evardefine.define_evar_as_product evd ev in
-	  (evd',{ uj_val = j.uj_val; uj_type = EConstr.Unsafe.to_constr t })
+	  (evd',{ uj_val = j.uj_val; uj_type = t })
     | _ ->
       	try let t,p =
-	  lookup_path_to_fun_from env evd (EConstr.of_constr j.uj_type) in
+	  lookup_path_to_fun_from env evd j.uj_type in
 	    apply_coercion env evd p j t
 	with Not_found | NoCoercion ->
           if Flags.is_program_mode () then
 	  try
 	    let evdref = ref evd in
 	    let coercef, t = mu env evdref t in
-	    let res = { uj_val = EConstr.Unsafe.to_constr (app_opt env evdref coercef (EConstr.of_constr j.uj_val)); uj_type = EConstr.Unsafe.to_constr t } in
+	    let res = { uj_val = app_opt env evdref coercef j.uj_val; uj_type = t } in
 	      (!evdref, res)
 	  with NoSubtacCoercion | NoCoercion ->
 	    (evd,j)
@@ -415,17 +415,23 @@ let inh_app_fun resolve_tc env evd j =
     try inh_app_fun_core env (saturate_evd env evd) j
     with NoCoercion -> (evd, j)
 
+let type_judgment env sigma j =
+  match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma j.uj_type)) with
+    | Sort s -> {utj_val = j.uj_val; utj_type = s }
+    | _ -> error_not_a_type env sigma j
+
 let inh_tosort_force loc env evd j =
   try
-    let t,p = lookup_path_to_sort_from env evd (EConstr.of_constr j.uj_type) in
+    let t,p = lookup_path_to_sort_from env evd j.uj_type in
     let evd,j1 = apply_coercion env evd p j t in
+    let whd_evar evd c = EConstr.of_constr (whd_evar evd (EConstr.Unsafe.to_constr c)) in
     let j2 = on_judgment_type (whd_evar evd) j1 in
-      (evd,type_judgment env j2)
+      (evd,type_judgment env evd j2)
   with Not_found | NoCoercion ->
     error_not_a_type ~loc env evd j
 
 let inh_coerce_to_sort loc env evd j =
-  let typ = whd_all env evd (EConstr.of_constr j.uj_type) in
+  let typ = whd_all env evd j.uj_type in
     match EConstr.kind evd (EConstr.of_constr typ) with
     | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev ->
@@ -437,10 +443,10 @@ let inh_coerce_to_sort loc env evd j =
 let inh_coerce_to_base loc env evd j =
   if Flags.is_program_mode () then
     let evdref = ref evd in
-    let ct, typ' = mu env evdref (EConstr.of_constr j.uj_type) in
+    let ct, typ' = mu env evdref j.uj_type in
     let res =
-      { uj_val = EConstr.Unsafe.to_constr (app_coercion env evdref ct (EConstr.of_constr j.uj_val));
-	uj_type = EConstr.Unsafe.to_constr typ' }
+      { uj_val = (app_coercion env evdref ct j.uj_val);
+	uj_type = typ' }
     in !evdref, res
   else (evd, j)
 
@@ -463,8 +469,8 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
 	  | Some v ->
 	    let evd,j =
 	      apply_coercion env evd p
-		{uj_val = EConstr.Unsafe.to_constr v; uj_type = EConstr.Unsafe.to_constr t} t2 in
-	      evd, Some (EConstr.of_constr j.uj_val), (EConstr.of_constr j.uj_type)
+		{uj_val = v; uj_type = t} t2 in
+	      evd, Some j.uj_val, j.uj_type
 	  | None -> evd, None, t
       with Not_found -> raise NoCoercion
     in
@@ -510,27 +516,27 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
 let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
   let (evd', val') =
     try
-      inh_conv_coerce_to_fail loc env evd rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
     with NoCoercionNoUnifier (best_failed_evd,e) ->
       try
 	if Flags.is_program_mode () then
-	  coerce_itf loc env evd (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+	  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 	else raise NoSubtacCoercion
       with
       | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion ->
-	  error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+	  error_actual_type ~loc env best_failed_evd cj t e
       | NoSubtacCoercion ->
 	let evd' = saturate_evd env evd in
       	  try
 	    if evd' == evd then 
-	      error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+	      error_actual_type ~loc env best_failed_evd cj t e
 	    else 
-      	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some (EConstr.of_constr cj.uj_val)) (EConstr.of_constr cj.uj_type) t
+      	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
 	  with NoCoercionNoUnifier (_evd,_error) ->
-	    error_actual_type ~loc env best_failed_evd cj (EConstr.Unsafe.to_constr t) e
+	    error_actual_type ~loc env best_failed_evd cj t e
   in
   let val' = match val' with Some v -> v | None -> assert(false) in
-    (evd',{ uj_val = EConstr.Unsafe.to_constr val'; uj_type = EConstr.Unsafe.to_constr t })
+    (evd',{ uj_val = val'; uj_type = t })
 
 let inh_conv_coerce_to resolve_tc = inh_conv_coerce_to_gen resolve_tc false
 let inh_conv_coerce_rigid_to resolve_tc = inh_conv_coerce_to_gen resolve_tc true