- Documentation of the Program tactics.

- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.



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

1 files changed, 119 insertions, 56 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3b2d85b1ff..841e6b0347 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -40,8 +40,15 @@ module type S = sig
      [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
-    env -> evar_defs -> unsafe_judgment -> types -> evar_defs * unsafe_judgment
+    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
     
+
+  (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+     is coercible to an object of type [t'] adding evar constraints if needed;
+     it fails if no coercion exists *)
+  val inh_conv_coerces_to : loc -> 
+    env -> evar_defs -> types -> type_constraint_type -> evar_defs
+
   (* [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 *)
@@ -136,73 +143,129 @@ module Default = struct
 	| _ ->
 	    inh_tosort_force loc env isevars j
 
-  let inh_coerce_to_fail env isevars c1 hj =
-    let hj' =
+  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) hj.uj_type in
+	let t2,i2 = class_of1 env (evars_of isevars) t in
 	let p = lookup_path_between (i2,i1) in
-	  apply_coercion env p hj t2
+	  match v with
+	      Some v -> 
+		let j = apply_coercion env p {uj_val = v; uj_type = t} t2 in
+		  Some j.uj_val, j.uj_type
+	    | None -> None, t
       with Not_found -> raise NoCoercion 
     in
-      try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+      try (the_conv_x_leq env t' c1 isevars, v', t')
       with Reduction.NotConvertible -> raise NoCoercion
-
-  let rec inh_conv_coerce_to_fail env isevars hj c1 =
-    let {uj_val = v; uj_type = t} = hj in
-      try (the_conv_x_leq env t c1 isevars, hj)
-      with Reduction.NotConvertible ->
-	(try 
-	   inh_coerce_to_fail env isevars c1 hj
+  open Pp
+  let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
+(*     (try *)
+(*        msgnl (str "inh_conv_coerces_to_fail called for " ++ *)
+(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* 	      Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++ *)
+(* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* 	      Termops.print_env env); *)
+(*      with _ -> ()); *)
+    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' = whd_betadeltaiota env (evars_of isevars) v in
+		    let v' = option_app (whd_betadeltaiota env (evars_of isevars)) v in
 		    let (evd',b) =
-		      match kind_of_term v' with
-			| Lambda (_,v1,v2) ->
-			    (try the_conv_x env v1 u1 isevars, true  (* leq v1 u1? *)
-			     with Reduction.NotConvertible -> (isevars, false))
-			| _  -> (isevars,false) in
-		      if b
-		      then 
-			let (x,v1,v2) = destLambda v' in
-			let env1 = push_rel (x,None,v1) env in
-			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
-			  {uj_val = v2; uj_type = t2 } u2 in
-			  (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
-				   uj_type = mkProd (x, v1, h2.uj_type) })
-		      else 
-			(* 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',h1) =
-			  inh_conv_coerce_to_fail env1 isevars
-			    {uj_val = mkRel 1; uj_type = (lift 1 u1) }
-			    (lift 1 t1) in
-			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
-			  { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
-                            uj_type = subst1 h1.uj_val t2 }
-                          u2
-			in
-			  (evd'',
-			   { uj_val = mkLambda (name, u1, h2.uj_val);
-			     uj_type = mkProd (name, u1, h2.uj_type) })
+		      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_app (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_app (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_app (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 t =
-    let (evd',cj') = 
-      try 
-	inh_conv_coerce_to_fail env isevars cj t
-      with NoCoercion ->
-	let sigma = evars_of isevars in
-	  error_actual_type_loc loc env sigma cj t
+  let inh_conv_coerce_to loc env isevars cj (n, t) =
+    if n = 0 then
+      let (evd', val', type') = 
+	try 
+	  inh_conv_coerce_to_fail loc env isevars (Some cj.uj_val) cj.uj_type t
+	with NoCoercion ->
+	  let sigma = evars_of isevars in
+	    error_actual_type_loc loc env sigma cj t
+      in
+      let val' = match val' with Some v -> v | None -> assert(false) in
+	(evd',{ uj_val = val'; uj_type = t })
+    else
+      (isevars, cj)
+
+  open Pp
+  let inh_conv_coerces_to loc env isevars t (abs, t') = isevars
+  (* Still bugguy 
+(*     (try *)
+(*        msgnl (str "inh_conv_coerces_to called for " ++ *)
+(* 	      Termops.print_constr_env env t ++ str " and "++ spc () ++ *)
+(* 	      Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++ *)
+(* 	      Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++ *)
+(* 	      Termops.print_env env); *)
+(*      with _ -> ()); *)
+    try let (rels, rng) = 
+      (* a little more effort to get products is needed *) 
+      try decompose_prod_n abs t
+      with _ -> 
+	raise (Invalid_argument "Coercion.inh_conv_coerces_to")
     in
-      (evd',{ uj_val = cj'.uj_val; uj_type = t })
+      if noccur_between 0 (succ abs) rng then (
+	(* msgnl (str "No occur between 0 and " ++ int (succ abs)); *)
+	let env', t, t' = 
+	  let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+	    env', rng, lift abs t'
+	in
+	  try 
+	    pi1 (inh_conv_coerce_to_fail loc env' isevars None t t')
+	  with NoCoercion ->
+	    isevars) (* Maybe not enough information to unify *)
+	    (*let sigma = evars_of isevars in
+	      error_cannot_coerce env' sigma (t, t'))*)
+      else isevars
+    with Invalid_argument _ -> isevars *)
 end