Bugs et simplifications coercions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@487 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 59 insertions, 45 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 7d61c7a82..b4c3a2bbd 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -516,26 +516,41 @@ let prepare_unif_pb typ cs =
     else 
       (* Il faudrait que noccur_between ne regarde pas la subst des Evar *)
       if match p with DOPN(Evar _,_) -> true | _ -> false then lift (-n) p
-      else failwith "TODO4-1" in
+      else
+	 failwith "TODO4-1" in
   let ci = applist
 	     (mkMutConstruct cs.cs_cstr, cs.cs_params@(rel_list (-n) n)) in
 
   (* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p' *)
   (Array.map (lift (-n)) cs.cs_concl_realargs, ci, p')
 
+let abstract_conclusion typ cs =
+  let n = cs.cs_nargs in
+  let (sign,p) = decompose_prod_n n typ in
+  lam_it p sign
+
 let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
   (* Il faudra substituer les isevars a un certain moment *)
   let eqns = array_map2 prepare_unif_pb typs cstrs in
 
   (* First strategy: no dependencies at all *)
   let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
+  let (sign,_) = get_arity env !isevars indf in
   if array_for_all (fun (_,_,typ) -> the_conv_x env isevars typn typ) eqns
   then
-    let (sign,_) = get_arity env !isevars indf in
     let pred = lam_it (lift (List.length sign) typn) sign in
     (false,pred) (* true = dependent -- par défaut *)
   else
-    failwith "TODO4-2"
+    if Array.length typs = 0 then
+      failwith "TODO4-3"
+    else
+      let s = get_sort_of env !isevars typs.(0) in
+      let predpred = lam_it (mkSort s) sign in
+      let caseinfo = make_default_case_info mis in
+      let brs = array_map2 abstract_conclusion typs cstrs in
+      let predbody = mkMutCaseA caseinfo predpred (Rel 1) brs in
+      let pred = lam_it (lift (List.length sign) typn) sign in
+      failwith "TODO4-2"; (true,pred)
 
 (* Propagation of user-provided predicate through compilation steps *)
 
@@ -981,7 +996,7 @@ let prepare_predicate typing_fun isevars env tomatchs = function
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
-let compile_cases (typing_fun,isevars) vtcon env (predopt, tomatchl, eqns) =
+let compile_cases loc (typing_fun,isevars) vtcon env (predopt, tomatchl, eqns)=
 
   (* We build the matrix of patterns and right-hand-side *)
   let matx = matx_of_eqns env eqns in
@@ -1008,5 +1023,7 @@ let compile_cases (typing_fun,isevars) vtcon env (predopt, tomatchl, eqns) =
   let j = compile pb in
   
   match vtcon with
-    | (_,(_,Some p)) -> Coercion.inh_conv_coerce_to env isevars p j
+    | (_,(_,Some p)) ->
+	let p = make_typed p (get_sort_of env !isevars p) in
+	Coercion.inh_conv_coerce_to loc env isevars j p
     | _ -> j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 2beb7441c..03bcbc6ed 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -30,7 +30,7 @@ i*)
 (* Compilation of pattern-matching. *)
 
 val compile_cases :
-  (trad_constraint -> env -> rawconstr -> unsafe_judgment)
+  loc -> (trad_constraint -> env -> rawconstr -> unsafe_judgment)
   * 'a evar_defs -> trad_constraint -> env ->
     rawconstr option * rawconstr list *
     (identifier list * cases_pattern list * rawconstr) list ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 81d8d2cf4..8b9d9bf4d 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -1,4 +1,3 @@
-
 (* $Id$ *)
 
 open Util
@@ -16,7 +15,11 @@ open Retyping
 
 (* Typing operations dealing with coercions *)
 
-let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t)
+exception NoCoercion
+
+let class_of1 env sigma t =
+  try class_of env sigma (nf_ise1 sigma t)
+  with Not_found -> raise NoCoercion
 
 let j_nf_ise env sigma {uj_val=v;uj_type=t} =
   { uj_val = nf_ise1 sigma v; 
@@ -58,8 +61,7 @@ let apply_pcoercion env p hj typ_cl =
 		 jres),
 	      (body_of_type jres.uj_type))
            (hj,typ_cl) p)
-  with _ -> 
-    failwith "apply_pcoercion"
+  with _ -> anomaly "apply_pcoercion"
 
 let inh_app_fun env isevars j = 
   match whd_betadeltaiota env !isevars (body_of_type j.uj_type) with
@@ -69,7 +71,7 @@ let inh_app_fun env isevars j =
  	   let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
       	   let p = lookup_path_to_fun_from i1 in
            apply_pcoercion env p j t
-	 with _ -> j)
+	 with Not_found | NoCoercion -> j)
 (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *)
 
 let inh_tosort_force env isevars j =
@@ -77,7 +79,7 @@ let inh_tosort_force env isevars j =
     let t,i1 = class_of1 env !isevars (body_of_type j.uj_type) in
     let p = lookup_path_to_sort_from i1 in
     apply_pcoercion env p j t 
-  with Not_found -> 
+  with Not_found | NoCoercion -> 
     j
 
 let inh_tosort env isevars j = 
@@ -94,24 +96,24 @@ let inh_ass_of_j env isevars j =
         let j1 = inh_tosort_force env isevars j in 
 	type_judgment env !isevars j1 
 
-let inh_coerce_to env isevars c1 hj =
+let inh_coerce_to_fail env isevars c1 hj =
   let t1,i1 = class_of1 env !isevars c1 in
   let t2,i2 = class_of1 env !isevars (body_of_type hj.uj_type) in
   let p = lookup_path_between (i2,i1) in
   let hj' = apply_pcoercion env p hj t2 in
   if the_conv_x_leq env isevars (body_of_type hj'.uj_type) c1 then 
     hj'
-  else 
-    failwith "inh_coerce_to"
+  else
+    raise NoCoercion
 
-let rec inh_conv_coerce_to env isevars c1 hj =
+let rec inh_conv_coerce_to_fail env isevars c1 hj =
   let {uj_val = v; uj_type = t} = hj in
   let t = body_of_type t in
   if the_conv_x_leq env isevars t c1 then hj
   else 
     try 
-      inh_coerce_to env isevars c1 hj
-    with _ ->  (* try ... with _ -> ... is BAD *)
+      inh_coerce_to_fail env isevars c1 hj
+    with NoCoercion ->  (* try ... with _ -> ... is BAD *)
       (*   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*)
       (match (whd_betadeltaiota env !isevars t,
 	      whd_betadeltaiota env !isevars c1) with
@@ -128,7 +130,7 @@ let rec inh_conv_coerce_to env isevars c1 hj =
 	          let assv1 = assumption_of_judgement env !isevars jv1 in *)
 	       let assv1 = outcast_type v1 in
                let env1 = push_rel (x,assv1) env in
-               let h2 = inh_conv_coerce_to env isevars u2
+               let h2 = inh_conv_coerce_to_fail env isevars u2
 			  {uj_val = v2;
 			   uj_type =
 			     make_typed t2 (get_sort_of env !isevars t2) } in
@@ -145,29 +147,28 @@ let rec inh_conv_coerce_to env isevars c1 hj =
                              | _ -> name) in
                let env1 = push_rel (name,assu1) env in
                let h1 = 
-		 inh_conv_coerce_to env isevars t1
+		 inh_conv_coerce_to_fail env isevars t1
 		   {uj_val = Rel 1; 
 		    uj_type = typed_app (fun _ -> u1) assu1 } in
-               let h2 = inh_conv_coerce_to env isevars u2  
+               let h2 = inh_conv_coerce_to_fail env isevars u2  
 			 { uj_val = DOPN(AppL,[|(lift 1 v);h1.uj_val|]);
                            uj_type =
 			     make_typed (subst1 h1.uj_val t2)
 			       (get_sort_of env !isevars t2) }
 	       in
 	       fst (abs_rel env !isevars name assu1 h2)
-	 | _ -> failwith "inh_coerce_to")
-            
-let inh_cast_rel loc env isevars cj tj =
-  let tj = assumption_of_judgment env !isevars tj in
+	 | _ -> raise NoCoercion)
+
+let inh_conv_coerce_to loc env isevars cj tj =
   let cj' = 
     try 
-      inh_conv_coerce_to env isevars (body_of_type tj) cj 
-    with Not_found | Failure _ -> 
+      inh_conv_coerce_to_fail env isevars (body_of_type tj) cj 
+    with NoCoercion -> 
       let rcj = j_nf_ise env !isevars cj in
-      let atj = nf_ise1 !isevars (body_of_type tj) in
-      error_actual_type_loc loc env rcj.uj_val (body_of_type rcj.uj_type) atj
+      let at = nf_ise1 !isevars (body_of_type tj) in
+      error_actual_type_loc loc env rcj.uj_val (body_of_type rcj.uj_type) at
   in
-  { uj_val = mkCast cj'.uj_val (body_of_type tj);
+  { uj_val = (* mkCast *) cj'.uj_val (* (body_of_type tj) *);
     uj_type = tj }
 
 let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
@@ -179,8 +180,8 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
       	in
       	(match vtcon with 
 	   | (_,(_,Some typ')) ->
-               (try inh_conv_coerce_to env isevars typ' resj
-          	with _ -> resj) (* try ... with _ -> ... is BAD *)
+               (try inh_conv_coerce_to_fail env isevars typ' resj
+          	with NoCoercion -> resj) (* try ... with _ -> ... is BAD *)
 	   | (_,(_,None)) -> resj)
 
     | hj::restjl ->
@@ -191,9 +192,9 @@ let inh_apply_rel_list nocheck apploc env isevars argjl funj vtcon =
 		  hj 
 		else 
 		  (try 
-		     inh_conv_coerce_to env isevars c1 hj 
-		   with Failure _ | Not_found ->
-                     error_cant_apply_bad_type_loc apploc env (n,c1,(body_of_type hj.uj_type))
+		     inh_conv_coerce_to_fail env isevars c1 hj 
+		   with NoCoercion ->
+                     error_cant_apply_bad_type_loc apploc env (n,c1,body_of_type hj.uj_type)
 		       (j_nf_ise env !isevars funj)
 		       (jl_nf_ise env !isevars argjl)) 
 	      in
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index ec1ab927b..5051f96db 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -19,13 +19,9 @@ val inh_tosort :
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment
 val inh_ass_of_j : 
   env -> 'a evar_defs -> unsafe_judgment -> unsafe_type_judgment
-val inh_coerce_to : 
-  env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment
-val inh_conv_coerce_to : 
-  env -> 'a evar_defs -> constr -> unsafe_judgment -> unsafe_judgment
 
-val inh_cast_rel : Rawterm.loc ->
-  env -> 'a evar_defs -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+val inh_conv_coerce_to : Rawterm.loc ->
+  env -> 'a evar_defs -> unsafe_judgment -> typed_type -> unsafe_judgment
 
 val inh_apply_rel_list : bool -> Rawterm.loc -> env -> 'a evar_defs ->
   unsafe_judgment list -> unsafe_judgment -> trad_constraint
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 23e7b5682..2d72b43f1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -440,17 +440,17 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
      uj_type = make_typed rsty s }
 
 | RCases (loc,prinfo,po,tml,eqns) ->
-    Cases.compile_cases
+    Cases.compile_cases loc
       ((fun vtyc env -> pretype vtyc env isevars lvar lmeta),isevars)
       vtcon env (* loc *) (po,tml,eqns)
 
 | RCast(loc,c,t) ->
   let tj = pretype def_vty_con env isevars lvar lmeta t in
   let tj = inh_tosort_force env isevars tj in
+  let tj = assumption_of_judgment env !isevars tj in
   let cj =
-    pretype (mk_tycon2 vtcon (body_of_type (assumption_of_judgment env !isevars
-      tj))) env isevars lvar lmeta c in
-  inh_cast_rel loc env isevars cj tj
+    pretype (mk_tycon2 vtcon (body_of_type tj)) env isevars lvar lmeta c in
+  inh_conv_coerce_to loc env isevars cj tj
 
 (* Maintenant, tout s'exécute... 
   | _ -> error_cant_execute CCI env (nf_ise1 env !isevars cstr)