Mise en place de coercion dans les motifs

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

5 files changed, 82 insertions, 37 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 5b3f3522ac..3152478abb 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -509,25 +509,36 @@ let pattern_status pats =
 
 exception NotAdjustable
 
-let rec adjust_local_defs = function
+let rec adjust_local_defs loc = function
   | (pat :: pats, (_,None,_) :: decls) ->
-      pat :: adjust_local_defs (pats,decls)
+      pat :: adjust_local_defs loc (pats,decls)
   | (pats, (_,Some _,_) :: decls) ->
-      PatVar (dummy_loc, Anonymous) :: adjust_local_defs (pats,decls)
+      PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls)
   | [], [] -> []
   | _ -> raise NotAdjustable
 
-let check_and_adjust_constructor loc (_,j as cstr_sp) mind cstrs pats =
-  (* Check it is constructor of the right type *)
-  if inductive_of_constructor cstr_sp <> mind
-  then error_bad_constructor_loc loc cstr_sp mind;
-  (* Check the constructor has the right number of args *)
-  let nb_args_constr = cstrs.(j-1).cs_nargs in
-  if List.length pats = nb_args_constr then pats
-  else
-    try adjust_local_defs (pats, List.rev cstrs.(j-1).cs_args)
-    with NotAdjustable ->
-      error_wrong_numarg_constructor_loc loc cstr_sp nb_args_constr
+let check_and_adjust_constructor ind cstrs = function 
+  | PatVar _ as pat -> pat
+  | PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
+      (* Check it is constructor of the right type *)
+      let ind' = inductive_of_constructor cstr in
+      if ind' = ind then
+	(* Check the constructor has the right number of args *)
+	let ci = cstrs.(i-1) in
+	let nb_args_constr = ci.cs_nargs in
+	if List.length args = nb_args_constr then pat
+	else
+	  try 
+	    let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
+	    in PatCstr (loc, cstr, args', alias)
+	  with NotAdjustable ->
+	    error_wrong_numarg_constructor_loc loc cstr nb_args_constr
+      else
+	(* Try to insert a coercion *)
+	try
+	  Coercion.inh_pattern_coerce_to loc pat ind' ind
+	with Not_found -> 
+	  error_bad_constructor_loc loc cstr ind
 
 let check_all_variables typ mat =
   List.iter
@@ -1105,7 +1116,8 @@ let group_equations mind current cstrs mat =
     List.fold_right (* To be sure it's from bottom to top *)
       (fun eqn () ->
 	 let rest = remove_current_pattern eqn in
-	 match current_pattern eqn with
+	 let pat = current_pattern eqn in
+	 match check_and_adjust_constructor mind cstrs pat with 
 	   | PatVar (_,name) -> 
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
@@ -1113,12 +1125,10 @@ let group_equations mind current cstrs mat =
 		 let rest = {rest with tag = lower_pattern_status rest.tag} in
 		 brs.(i-1) <- (args, rest) :: brs.(i-1)
 	       done
-	   | PatCstr(loc,((_,i) as cstr),args,alias) ->
+	   | PatCstr (loc,((_,i) as cstr),args,_) as pat ->
 	       (* This is a regular clause *)
-	       let args' =
-		 check_and_adjust_constructor loc cstr mind cstrs args in
 	       only_default := false;
-	       brs.(i-1) <- (args',rest) :: brs.(i-1)) mat () in
+	       brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in
   (brs,!only_default)
 
 (************************************************************************)
@@ -1427,8 +1437,8 @@ let coerce_row typing_fun isevars env cstropt tomatch =
 	   with NotCoercible ->
 	     (* 2 cases : Not the right inductive or not an inductive at all *)
 	     try
-	       let mind,_ = find_mrectype env (evars_of isevars) typ in
-	       error_bad_constructor_loc cloc c mind
+	       IsInd (typ,find_rectype env (evars_of isevars) typ)
+               (* will try to coerce later in check_and_adjust_constructor.. *)
 	     with Induc ->
 	       error_case_not_inductive_loc
 		 (loc_of_rawconstr tomatch) env (evars_of isevars) j)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4220b7b9ee..77dff358b0 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -165,6 +165,19 @@ let lookup_path_to_fun_from s =
 let lookup_path_to_sort_from s = 
   lookup_path_between (s,fst(class_info CL_SORT))
 
+let lookup_pattern_path_between (s,t) =
+  let l = List.assoc (s,t) !inheritance_graph in
+  List.map  
+    (fun i ->
+       let coe = snd (coercion_info_from_index i) in
+       let c, _ =
+	 Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty 
+	   coe.coe_value.uj_val
+       in 
+       match kind_of_term c with
+	 | Construct sp -> (sp, coe.coe_param)
+	 | _ -> raise Not_found) l
+
 (* library, summary *)
 
 (*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
@@ -219,6 +232,8 @@ let class_of env sigma t =
   in
   if List.length args = n1 then t, i else raise Not_found
 
+let inductive_class_of ind = fst (class_info (CL_IND ind))
+
 let class_args_of c = snd (decompose_app c)
 
 let strength_of_cl = function 
@@ -233,7 +248,7 @@ let string_of_class = function
   | CL_IND sp -> string_of_id (id_of_global (Global.env()) (IndRef sp))
   | CL_SECVAR sp -> string_of_id (id_of_global (Global.env()) (VarRef sp))
 
-(* coercion_value : int -> unsafe_judgment * bool *)
+(* coercion_value : coe_index -> unsafe_judgment * bool *)
 
 let coercion_value i = 
   let { coe_value = j; coe_is_identity = b } = snd (coercion_info_from_index i)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 9f8d0cf858..ecdce7543a 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -62,6 +62,9 @@ val find_class_type : constr -> cl_typ * constr list
 (* raises [Not_found] if not convertible to a class *)
 val class_of : env -> evar_map -> constr -> constr * cl_index
 
+(* raises [Not_found] if not mapped to a class *)
+val inductive_class_of : inductive -> cl_index
+
 val class_args_of : constr -> constr list
 
 val strength_of_cl : cl_typ -> strength
@@ -87,9 +90,11 @@ val set_coercion_visibility : bool -> coe_typ -> unit
 val is_coercion_visible : coe_typ -> bool
 
 (*s Lookup functions for coercion paths *)
-val lookup_path_between : (cl_index * cl_index) -> inheritance_path
+val lookup_path_between : cl_index * cl_index -> inheritance_path
 val lookup_path_to_fun_from : cl_index -> inheritance_path
 val lookup_path_to_sort_from : cl_index -> inheritance_path
+val lookup_pattern_path_between :
+  cl_index * cl_index -> (constructor * int) list
 
 (*i Pour le discharge *)
 type coercion = (coe_typ * coe_info_typ) * cl_typ * cl_typ
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5a540353b2..5c6b2c6b79 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -30,19 +30,35 @@ let apply_coercion_args env argl funj =
     | [] -> { uj_val = applist (j_val funj,argl);
               uj_type = typ }
     | h::restl ->
-      (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
+    (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
   	match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
 	  | Prod (_,c1,c2) -> 
-              (* Typage garanti par l'appel a app_coercion*)
+              (* Typage garanti par l'appel à app_coercion*)
 	      apply_rec (h::acc) (subst1 h c2) restl
 	  | _ -> anomaly "apply_coercion_args"
   in 
   apply_rec [] funj.uj_type argl
 
-(* appliquer le chemin de coercions p a` hj *)
-
 exception NoCoercion
 
+(* appliquer le chemin de coercions de patterns p *)
+
+let apply_pattern_coercion loc pat p =
+  List.fold_left
+    (fun pat (co,n) ->
+       let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in
+       Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+    pat p
+
+(* raise Not_found if no coercion found *)
+let inh_pattern_coerce_to loc pat ind1 ind2 =
+  let i1 = inductive_class_of ind1 in
+  let i2 = inductive_class_of ind2 in
+  let p = lookup_pattern_path_between (i1,i2) in
+  apply_pattern_coercion loc pat p
+
+(* appliquer le chemin de coercions p à hj *)
+
 let apply_coercion env p hj typ_cl =
   if !compter then begin
     nbpathc := !nbpathc +1; 
@@ -51,10 +67,10 @@ let apply_coercion env p hj typ_cl =
   try 
     fst (List.fold_left
            (fun (ja,typ_cl) i -> 
-              let fv,b = coercion_value i in
+              let fv,isid = coercion_value i in
               let argl = (class_args_of typ_cl)@[ja.uj_val] in
               let jres = apply_coercion_args env argl fv in
-              (if b then 
+              (if isid then 
 		 { uj_val = ja.uj_val; uj_type = jres.uj_type }
                else 
 		 jres),
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 4ca3ba9875..36c981172b 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -10,10 +10,12 @@
 
 (*i*)
 open Evd
+open Names
 open Term
 open Sign
 open Environ
 open Evarutil
+open Rawterm
 (*i*)
 
 (*s Coercions. *)
@@ -36,11 +38,8 @@ val inh_coerce_to_sort :
 val inh_conv_coerce_to : Rawterm.loc -> 
   env -> evar_defs -> unsafe_judgment -> constr -> unsafe_judgment
 
-(*i
-(* [inh_apply_rel_list loc env isevars args f tycon] tries to type [(f
-   args)] of type [tycon] (if any) by inserting coercions in front of
-   each arg$_i$, if necessary *)
-val inh_apply_rel_list : Rawterm.loc -> env -> 'a evar_defs ->
-  (Rawterm.loc * unsafe_judgment) list ->
-    (Rawterm.loc * unsafe_judgment) -> constr option -> unsafe_judgment
-i*)
+(* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
+   pattern [pat] typed in [ind1] into a pattern typed in [ind2];
+   raises [Not_found] if no coercion found *)
+val inh_pattern_coerce_to :
+  Rawterm.loc  -> cases_pattern -> inductive -> inductive -> cases_pattern