Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 77 insertions, 67 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d0ee913f..cc74b0ad 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: coercion.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: coercion.ml 9257 2006-10-21 17:28:28Z herbelin $ *)
 
 open Util
 open Names
@@ -20,6 +20,7 @@ open Evarutil
 open Evarconv
 open Retyping
 open Evd
+open Termops
 
 module type S = sig
   (*s Coercions. *)
@@ -66,7 +67,14 @@ module Default = struct
   (* Typing operations dealing with coercions *)
   exception NoCoercion
 
-  let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
+  let whd_app_evar sigma t =
+    match kind_of_term t with
+      | App (f,l) -> mkApp (whd_evar sigma f,l)
+      | _ -> whd_evar sigma t
+
+  let class_of1 env isevars t =
+    let sigma = evars_of isevars in
+    class_of env sigma (whd_app_evar sigma t)
 
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
@@ -84,7 +92,6 @@ module Default = struct
       apply_rec [] funj.uj_type argl
 
   (* appliquer le chemin de coercions de patterns p *)
-
   let apply_pattern_coercion loc pat p =
     List.fold_left
       (fun pat (co,n) ->
@@ -100,7 +107,6 @@ module Default = struct
       apply_pattern_coercion loc pat p
 
   (* appliquer le chemin de coercions p à hj *)
-
   let apply_coercion env p hj typ_cl =
     try 
       fst (List.fold_left
@@ -120,22 +126,23 @@ module Default = struct
     let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
       match kind_of_term t with
 	| Prod (_,_,_) -> (isevars,j)
-	| Evar ev when not (is_defined_evar isevars ev) ->
+	| Evar ev ->
 	    let (isevars',t) = define_evar_as_arrow isevars ev in
 	      (isevars',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+ 	       let t,i1 = class_of1 env isevars j.uj_type in
       	       let p = lookup_path_to_fun_from i1 in
 		 (isevars,apply_coercion env p j t)
 	     with Not_found -> (isevars,j))
 
   let inh_tosort_force loc env isevars j =
     try
-      let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+      let t,i1 = class_of1 env isevars j.uj_type in
       let p = lookup_path_to_sort_from i1 in
       let j1 = apply_coercion env p j t in 
-	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+      let j2 = on_judgment_type (whd_evar (evars_of isevars)) j1 in
+        (isevars,type_judgment env j2)
     with Not_found ->
       error_not_a_type_loc loc env (evars_of isevars) j
 
@@ -154,8 +161,8 @@ module Default = struct
   let inh_coerce_to_fail env isevars c1 v t =
     let v', t' =
       try 
-	let t1,i1 = class_of1 env (evars_of isevars) c1 in
-	let t2,i2 = class_of1 env (evars_of isevars) t in
+	let t1,i1 = class_of1 env isevars c1 in
+	let t2,i2 = class_of1 env isevars t in
 	let p = lookup_path_between (i2,i1) in
 	  match v with
 	      Some v -> 
@@ -166,64 +173,68 @@ module Default = struct
     in
       try (the_conv_x_leq env t' c1 isevars, v', t')
       with Reduction.NotConvertible -> raise NoCoercion
-  open Pp
+
   let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
     try (the_conv_x_leq env t c1 isevars, v, t)
     with Reduction.NotConvertible ->
-      (try 
-	 inh_coerce_to_fail env isevars c1 v t
-	 with NoCoercion ->
-	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
-	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
-		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
-		    let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
-		    let (evd',b) =
-		      match v' with 
-			  Some v' ->
-			    (match kind_of_term v' with
-			       | Lambda (x,v1,v2) ->
-				   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)  (* leq v1 u1? *)
-				    with Reduction.NotConvertible -> (isevars, None))
-			       | _  -> (isevars, None))
-			| None -> (isevars, None)
-		    in 
-		      (match b with
-			   Some (x, v1, v2) ->
-			     let env1 = push_rel (x,None,v1) env in
-			     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
-						       (Some v2) t2 u2 in
-			       (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
-				mkProd (x, v1, t2'))
-			 | None ->
-			     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
-			     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
-			     (* has type (name:u1)u2 (with v' recursively obtained) *)
-			     let name = (match name with 
-					   | Anonymous -> Name (id_of_string "x")
-					   | _ -> name) in
-			     let env1 = push_rel (name,None,u1) env in
-			     let (evd', v1', t1') =
-			       inh_conv_coerce_to_fail loc env1 isevars
-				 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) 
-			     in
-			     let (evd'', v2', t2') = 
-			       let v2 =
-				 match v with 
-				     Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1'
-				   | None -> None
-			       and evd', t2 =
-				 match v1' with 
-				     Some v1' -> evd', subst1 v1' t2
-				   | None -> 
-				       let evd', ev = new_evar evd' env ~src:(loc, InternalHole) t1' in
-					 evd', subst1 ev t2
-			       in
-				 inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
-			     in
-			       (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
-				mkProd (name, u1, t2')))
-		| _ -> raise NoCoercion))
-	
+    try inh_coerce_to_fail env isevars c1 v t
+    with NoCoercion ->
+    match
+      kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
+      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1)
+    with
+    | Prod (_,t1,t2), Prod (name,u1,u2) -> 
+	let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in
+	let (evd',b) =
+	  match v' with 
+	  | Some v' ->
+	      (match kind_of_term v' with
+	       | Lambda (x,v1,v2) ->
+		   (* sous-typage non contravariant: pas de "leq v1 u1" *)
+		   (try the_conv_x env v1 u1 isevars, Some (x, v1, v2)
+		   with Reduction.NotConvertible -> (isevars, None))
+	       | _  -> (isevars, None))
+	  | None -> (isevars, None)
+	in
+	(match b with
+	 | Some (x, v1, v2) ->
+	     let env1 = push_rel (x,None,v1) env in
+	     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
+	       (Some v2) t2 u2 in
+	     (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', 
+	     mkProd (x, v1, t2'))
+	 | None ->
+	     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+	     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+	     (* has type (name:u1)u2 (with v' recursively obtained) *)
+	     let name = match name with 
+	       | Anonymous -> Name (id_of_string "x")
+	       | _ -> name
+	     in
+	     let env1 = push_rel (name,None,u1) env in
+	     let (evd', v1', t1') =
+	       inh_conv_coerce_to_fail loc env1 isevars
+		 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
+	     in
+	     let (evd'', v2', t2') = 
+	       let v2 =
+		 match v with 
+		 | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1'
+		 | None -> None
+	       and evd', t2 =
+		 match v1' with 
+		 | Some v1' -> evd', subst_term v1' t2
+		 | None -> 
+		     let evd', ev =
+		       new_evar evd' env ~src:(loc, InternalHole) t1' in
+		     evd', subst_term ev t2
+	       in
+	       inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
+	     in
+	     (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2',
+	     mkProd (name, u1, t2')))
+    | _ -> raise NoCoercion
+
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to loc env isevars cj (n, t) =
     match n with
@@ -236,8 +247,7 @@ module Default = struct
 		error_actual_type_loc loc env sigma cj t
 	  in
 	  let val' = match val' with Some v -> v | None -> assert(false) in
-	  let nf = nf_isevar evd' in
-	    (evd',{ uj_val = nf val'; uj_type = nf t })
+	    (evd',{ uj_val = val'; uj_type = t })
       | Some (init, cur) -> (isevars, cj)
       
     let inh_conv_coerces_to loc env (isevars : evar_defs) t (abs, t') = isevars