Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about

backtracking on coercion classes when a coercion path fails).



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

11 files changed, 148 insertions, 89 deletions

diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 23c2b14ac3..4b68f1fc78 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -310,8 +310,6 @@ module Coercion = struct
 
   (* Typing operations dealing with coercions *)
 
-  let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
-
   (* Here, funj is a coercion therefore already typed in global context *)
   let apply_coercion_args env argl funj =
     let rec apply_rec acc typ = function
@@ -339,19 +337,17 @@ module Coercion = struct
 
   (* 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
+    let p = lookup_pattern_path_between (ind1,ind2) in
       apply_pattern_coercion loc pat p
 
   (* appliquer le chemin de coercions p à hj *)
 
-  let apply_coercion env p hj typ_cl =
+  let apply_coercion env sigma p hj typ_cl =
     try 
       fst (List.fold_left
              (fun (ja,typ_cl) i -> 
 		let fv,isid = coercion_value i in
-		let argl = (class_args_of typ_cl)@[ja.uj_val] in
+		let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 		let jres = apply_coercion_args env argl fv in
 		  (if isid then 
 		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
@@ -370,9 +366,9 @@ module Coercion = struct
 	      (isevars',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
-      	       let p = lookup_path_to_fun_from i1 in
-		 (isevars,apply_coercion env p j t)
+      	       let t,p =
+		 lookup_path_to_fun_from env (evars_of isevars) j.uj_type in
+		 (isevars,apply_coercion env (evars_of isevars) p j t)
 	     with Not_found ->
 	       try 
 		 let coercef, t = mu env isevars t in
@@ -382,9 +378,8 @@ module Coercion = struct
 
   let inh_tosort_force loc env isevars j =
     try
-      let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
-      let p = lookup_path_to_sort_from i1 in
-      let j1 = apply_coercion env p j t in 
+      let t,p = lookup_path_to_sort_from env (evars_of isevars) j.uj_type in
+      let j1 = apply_coercion env (evars_of isevars) p j t in 
 	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
     with Not_found ->
       error_not_a_type_loc loc env (evars_of isevars) j
@@ -417,12 +412,11 @@ module Coercion = struct
     else
     let v', t' =
       try 
-	let t1,i1 = class_of1 env (evars_of evd) c1 in
-	let t2,i2 = class_of1 env (evars_of evd) t in
-	let p = lookup_path_between (i2,i1) in
+	let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
 	  match v with
 	      Some v -> 
-		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		let j = apply_coercion env (evars_of evd) p
+		  {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
       with Not_found -> raise NoCoercion 
diff --git a/dev/base_include b/dev/base_include
index 398f60d2b7..0b7a0b67d8 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -29,6 +29,7 @@
 #install_printer  (* qualid *)  ppqualid;;
 #install_printer  (* kernel_name *) ppkn;;
 #install_printer  (* constant *) ppcon;;
+#install_printer  (* cl_index *) ppclindex;;
 #install_printer  (* constr *)  print_pure_constr;; 
 #install_printer  (* patch *) ppripos;;
 #install_printer  (* values *) ppvalues;;
diff --git a/dev/db b/dev/db
index 6221462a85..8187857014 100644
--- a/dev/db
+++ b/dev/db
@@ -13,6 +13,7 @@ install_printer Top_printers.ppkn
 install_printer Top_printers.ppcon
 install_printer Top_printers.ppsp
 install_printer Top_printers.ppqualid
+install_printer Top_printers.ppclindex
 install_printer Top_printers.ppbigint
 
 install_printer Top_printers.pppattern
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 3624fe792d..8dc220f65e 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -744,7 +744,7 @@ let print_path_between cls clt =
   let j = index_of_class clt in
   let p = 
     try 
-      lookup_path_between (i,j) 
+      lookup_path_between_class (i,j) 
     with _ -> 
       errorlabstrm "index_cl_of_id"
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 0ffaed3717..548ca7596f 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -128,6 +128,10 @@ let class_exists cl = Bijint.mem cl !class_tab
 
 let class_info_from_index i = Bijint.map i !class_tab
 
+let cl_fun_index = fst(class_info CL_FUN)
+
+let cl_sort_index = fst(class_info CL_SORT)
+
 (* coercion_info : coe_typ -> coe_info_typ *)
 
 let coercion_info coe = Gmap.find coe !coercion_tab
@@ -136,32 +140,10 @@ let coercion_exists coe = Gmap.mem coe !coercion_tab
 
 let coercion_params coe_info = coe_info.coe_param
 
-let lookup_path_between (s,t) =
-  Gmap.find (s,t) !inheritance_graph
-
-let lookup_path_to_fun_from s = 
-  lookup_path_between (s,fst(class_info CL_FUN))
+(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
 
-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 = Gmap.find (s,t) !inheritance_graph in
-  List.map  
-    (fun coe ->
-       let c, _ =
-	 Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty 
-	   coe.coe_value
-       in 
-       match kind_of_term c with
-	 | Construct cstr ->
-	     (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
-	 | _ -> raise Not_found) l
-
-(* find_class_type : constr -> cl_typ * int *)
-
-let find_class_type t =
-  let t', args = decompose_app (Reductionops.whd_betaiotazeta t) in
+let find_class_type env sigma t =
+  let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in
   match kind_of_term t' with
     | Var id -> CL_SECVAR id, args
     | Const sp -> CL_CONST sp, args
@@ -178,7 +160,7 @@ let subst_cl_typ subst ct = match ct with
   | CL_CONST kn -> 
       let kn',t = subst_con subst kn in 
 	if kn' == kn then ct else
-         fst (find_class_type t)
+         fst (find_class_type (Global.env()) Evd.empty t)
   | CL_IND (kn,i) ->
       let kn' = subst_kn subst kn in 
 	if kn' == kn then ct else
@@ -188,19 +170,17 @@ let subst_cl_typ subst ct = match ct with
        to declare any term as a coercion *)
 let subst_coe_typ subst t = fst (subst_global subst t)
 
-(* classe d'un terme *)
-
 (* class_of : Term.constr -> int *)
 
 let class_of env sigma t = 
   let (t, n1, i, args) = 
     try
-      let (cl,args) = find_class_type t in
+      let (cl,args) = find_class_type env sigma t in
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
     with Not_found ->
       let t = Tacred.hnf_constr env sigma t in
-      let (cl, args) = find_class_type t in 
+      let (cl, args) = find_class_type env sigma t in 
       let (i, { cl_param = n1 } ) = class_info cl in
       (t, n1, i, args)
   in
@@ -208,7 +188,7 @@ let class_of env sigma t =
 
 let inductive_class_of ind = fst (class_info (CL_IND ind))
 
-let class_args_of c = snd (find_class_type c)
+let class_args_of env sigma c = snd (find_class_type env sigma c)
 
 let string_of_class = function
   | CL_FUN -> "Funclass"
@@ -222,6 +202,61 @@ let string_of_class = function
 
 let pr_class x = str (string_of_class x)
 
+(* lookup paths *)
+
+let lookup_path_between_class (s,t) =
+  Gmap.find (s,t) !inheritance_graph
+
+let lookup_path_to_fun_from_class s =
+  lookup_path_between_class (s,cl_fun_index)
+
+let lookup_path_to_sort_from_class s =
+  lookup_path_between_class (s,cl_sort_index)
+
+(* advanced path lookup *)
+
+let apply_on_class_of env sigma t cont =
+  try
+    let (cl,args) = find_class_type env sigma t in
+    let (i, { cl_param = n1 } ) = class_info cl in
+    if List.length args <> n1 then raise Not_found;
+    t, cont i
+  with Not_found ->
+    (* Is it worth to be more incremental on the delta steps? *)
+    let t = Tacred.hnf_constr env sigma t in
+    let (cl, args) = find_class_type env sigma t in 
+    let (i, { cl_param = n1 } ) = class_info cl in
+    if List.length args <> n1 then raise Not_found;
+    t, cont i
+
+let lookup_path_between env sigma (s,t) =
+  let (s,(t,p)) =
+    apply_on_class_of env sigma s (fun i ->
+      apply_on_class_of env sigma t (fun j ->
+	lookup_path_between_class (i,j))) in
+  (s,t,p)
+
+let lookup_path_to_fun_from env sigma s =
+  apply_on_class_of env sigma s lookup_path_to_fun_from_class
+
+let lookup_path_to_sort_from env sigma s = 
+  apply_on_class_of env sigma s lookup_path_to_sort_from_class
+
+let get_coercion_constructor coe =
+  let c, _ =
+    Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value
+  in
+  match kind_of_term c with
+  | Construct cstr -> 
+      (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1)
+  | _ ->
+      raise Not_found
+
+let lookup_pattern_path_between (s,t) =
+  let i = inductive_class_of s in
+  let j = inductive_class_of t in
+  List.map get_coercion_constructor (Gmap.find (i,j) !inheritance_graph)
+
 (* coercion_value : coe_index -> unsafe_judgment * bool *)
 
 let coercion_value { coe_value = c; coe_type = t; coe_is_identity = b } =
@@ -255,11 +290,11 @@ let add_coercion_in_graph (ic,source,target) =
     try 
       if i=j then begin
 	if different_class_params i j then begin
-	  let _ = lookup_path_between ij in
+	  let _ = lookup_path_between_class ij in
           ambig_paths := (ij,p)::!ambig_paths
 	end
       end else begin
-        let _ = lookup_path_between (i,j) in
+        let _ = lookup_path_between_class (i,j) in
         ambig_paths := (ij,p)::!ambig_paths
       end;
       false
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c1a62b34fd..a5f139ab11 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -52,17 +52,17 @@ val class_info : cl_typ -> (cl_index * cl_info_typ)
 val class_exists : cl_typ -> bool
 val class_info_from_index : cl_index -> cl_typ * cl_info_typ
 
-(* [find_class_type c] returns the head reference of c and its
+(* [find_class_type env sigma c] returns the head reference of [c] and its
    arguments *)
-val find_class_type : constr -> cl_typ * constr list
+val find_class_type : env -> evar_map -> types -> cl_typ * constr list
 
 (* raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> constr -> constr * cl_index
+val class_of : env -> evar_map -> types -> types * 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 class_args_of : env -> evar_map -> types -> constr list
 
 (*s [declare_coercion] adds a coercion in the graph of coercion paths *)
 val declare_coercion : 
@@ -75,11 +75,16 @@ val coercion_exists : coe_typ -> bool
 val coercion_value : coe_index -> (unsafe_judgment * bool)
 
 (*s Lookup functions for coercion paths *)
-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
+val lookup_path_between_class : cl_index * cl_index -> inheritance_path
+
+val lookup_path_between : env -> evar_map -> types * types -> 
+      types * types * inheritance_path
+val lookup_path_to_fun_from : env -> evar_map -> types ->
+      types * inheritance_path
+val lookup_path_to_sort_from : env -> evar_map -> types -> 
+      types * inheritance_path
+val lookup_pattern_path_between : 
+  inductive * inductive -> (constructor * int) list
 
 (*i Crade *)
 open Pp
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 4ff60b41f2..85e14d482c 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -78,10 +78,6 @@ module Default = struct
       | App (f,l) -> mkApp (whd_evar sigma f,l)
       | _ -> whd_evar sigma t
 
-  let class_of1 env evd t =
-    let sigma = evars_of evd 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 =
     let rec apply_rec acc typ = function
@@ -107,18 +103,16 @@ module Default = struct
 
   (* 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
+    let p = lookup_pattern_path_between (ind1,ind2) in
       apply_pattern_coercion loc pat p
 
   (* appliquer le chemin de coercions p à hj *)
-  let apply_coercion env p hj typ_cl =
+  let apply_coercion env sigma p hj typ_cl =
     try 
       fst (List.fold_left
              (fun (ja,typ_cl) i -> 
 		let fv,isid = coercion_value i in
-		let argl = (class_args_of typ_cl)@[ja.uj_val] in
+		let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 		let jres = apply_coercion_args env argl fv in
 		  (if isid then 
 		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
@@ -137,16 +131,15 @@ module Default = struct
 	      (evd',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
- 	       let t,i1 = class_of1 env evd j.uj_type in
-      	       let p = lookup_path_to_fun_from i1 in
-		 (evd,apply_coercion env p j t)
+      	       let t,p =
+		 lookup_path_to_fun_from env (evars_of evd) j.uj_type in
+		 (evd,apply_coercion env (evars_of evd) p j t)
 	     with Not_found -> (evd,j))
 
   let inh_tosort_force loc env evd j =
     try
-      let t,i1 = class_of1 env evd j.uj_type in
-      let p = lookup_path_to_sort_from i1 in
-      let j1 = apply_coercion env p j t in 
+      let t,p = lookup_path_to_sort_from env (evars_of evd) j.uj_type in
+      let j1 = apply_coercion env (evars_of evd) p j t in 
       let j2 = on_judgment_type (whd_evar (evars_of evd)) j1 in
         (evd,type_judgment env j2)
     with Not_found ->
@@ -173,12 +166,12 @@ module Default = struct
     else
     let v', t' =
       try 
-	let t1,i1 = class_of1 env evd c1 in
-	let t2,i2 = class_of1 env evd t in
-	let p = lookup_path_between (i2,i1) in
+	let t2,t1,p = lookup_path_between env (evars_of evd) (t,c1) in
 	  match v with
 	      Some v -> 
-		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		let j =
+		  apply_coercion env (evars_of evd) p
+		    {uj_val = v; uj_type = t} t2 in
 		  Some j.uj_val, j.uj_type
 	    | None -> None, t
       with Not_found -> raise NoCoercion 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 99c57d084c..57af582a1c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -233,6 +233,7 @@ let evar = mkflags [fevar]
 let betaevar = mkflags [fevar; fbeta]
 let betaiota = mkflags [fiota; fbeta]
 let betaiotazeta = mkflags [fiota; fbeta;fzeta]
+let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar]
 
 (* Contextual *)
 let delta = mkflags [fdelta;fevar]
@@ -483,6 +484,12 @@ let whd_betaiotazeta_stack x =
 let whd_betaiotazeta x =
   app_stack (whd_betaiotazeta_state (x, empty_stack))
 
+let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar
+let whd_betaiotazetaevar_stack env sigma x =
+  appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
+let whd_betaiotazetaevar env sigma x =
+  app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
+
 let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
 let whd_betaiotaevar_stack env sigma x =
   appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 422ee57d47..371a66a9d5 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -98,6 +98,7 @@ val whd_evar :  evar_map -> constr -> constr
 val whd_beta : local_reduction_function
 val whd_betaiota : local_reduction_function
 val whd_betaiotazeta : local_reduction_function
+val whd_betaiotazetaevar : contextual_reduction_function
 val whd_betadeltaiota :  contextual_reduction_function
 val whd_betadeltaiota_nolet :  contextual_reduction_function
 val whd_betaetalet : local_reduction_function
@@ -105,17 +106,17 @@ val whd_betalet : local_reduction_function
 
 val whd_beta_stack : local_stack_reduction_function
 val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazeta_stack : local_stack_reduction_function
-val whd_betadeltaiota_stack :  contextual_stack_reduction_function
-val whd_betadeltaiota_nolet_stack :  contextual_stack_reduction_function
+val whd_betaiotazetaevar_stack : contextual_stack_reduction_function
+val whd_betadeltaiota_stack : contextual_stack_reduction_function
+val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
 val whd_betaetalet_stack : local_stack_reduction_function
 val whd_betalet_stack : local_stack_reduction_function
 
 val whd_beta_state : local_state_reduction_function
 val whd_betaiota_state : local_state_reduction_function
-val whd_betaiotazeta_state : local_state_reduction_function
-val whd_betadeltaiota_state :  contextual_state_reduction_function
-val whd_betadeltaiota_nolet_state :  contextual_state_reduction_function
+val whd_betaiotazetaevar_state : contextual_state_reduction_function
+val whd_betadeltaiota_state : contextual_state_reduction_function
+val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
 val whd_betaetalet_state : local_state_reduction_function
 val whd_betalet_state : local_state_reduction_function
 
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index d652132e49..525348dec9 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -61,3 +61,24 @@ Check fun (H : For_all (fun x => C (f x))) => H : For_all (fun x => D (f x)).
 
 End Q.
 
+(* Combining class lookup and path lookup so that if a lookup fails, another
+   descent in the class can be found (see wish #1934) *)
+
+Record Setoid : Type :=
+{ car :>  Type }.
+
+Record Morphism (X Y:Setoid) : Type :=
+{evalMorphism :> X -> Y}.
+
+Definition extSetoid (X Y:Setoid) : Setoid.
+intros X Y.
+constructor.
+exact (Morphism X Y).
+Defined.
+
+Definition ClaimA := forall (X Y:Setoid) (f: extSetoid X Y) x, f x= f x.
+
+Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
+
+Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
+
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 7ad7c0eda2..f577355d37 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -139,7 +139,7 @@ let get_source lp source =
 	let (cl1,lv1) =
           match lp with
 	    | [] -> raise Not_found
-            | t1::_ -> find_class_type t1
+            | t1::_ -> find_class_type (Global.env()) Evd.empty t1
         in 
 	(cl1,lv1,1)
     | Some cl ->
@@ -147,7 +147,7 @@ let get_source lp source =
 	  | [] -> raise Not_found
 	  | t1::lt ->
 	      try 
-		let cl1,lv1 = find_class_type t1 in
+		let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in
 		if cl = cl1 then cl1,lv1,(List.length lt+1)
 		else raise Not_found
               with Not_found -> aux lt
@@ -157,7 +157,7 @@ let get_target t ind =
   if (ind > 1) then 
     CL_FUN
   else 
-    fst (find_class_type t)
+    fst (find_class_type (Global.env()) Evd.empty t)
 
 let prods_of t = 
   let rec aux acc d = match kind_of_term d with
@@ -225,8 +225,9 @@ let build_id_coercion idf_opt source =
     match idf_opt with
       | Some idf -> idf
       | None ->
+	  let cl,_ = find_class_type (Global.env()) Evd.empty t in
 	  id_of_string ("Id_"^(ident_key_of_class source)^"_"^
-                        (ident_key_of_class (fst (find_class_type t)))) 
+                        (ident_key_of_class cl))
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry