Remove support for "abstract typing constraints" that requires unicity of solutions to unification.

Only allow bidirectional checking of constructor applications, enabled by a program_mode flag:
it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated
with delta-equivalent but not syntactically equivalent terms.
Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code.

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

6 files changed, 68 insertions, 83 deletions

diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 6893f13513..279e4d87a3 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -413,7 +413,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps) =
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
-		  pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
+		  pb.isevars (make_judge current typ) indt).uj_val in
 	    let sigma =  !(pb.isevars) in
 	    let typ = IsInd (indt,find_rectype pb.env sigma indt) in
 	    ((current,typ),deps))
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 3cbf9fcabe..b55c43d820 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -409,9 +409,9 @@ module Coercion = struct
 
   let inh_coerce_to_prod loc env isevars t =
     let isevars = ref isevars in
-    let typ = hnf env !isevars (snd t) in
+    let typ = hnf env !isevars t in
     let _, typ' = mu env isevars typ in
-      !isevars, (fst t, typ')
+      !isevars, typ'
 
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
@@ -462,50 +462,30 @@ module Coercion = struct
     | _ -> raise NoCoercion
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
-    match n with
-    | None ->
-      let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } 
-      and t = hnf_nodelta env evd t in
-      let (evd', val') =
-	try
-	  inh_conv_coerce_to_fail loc env evd rigidonly
+  let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
+    let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } 
+    and t = hnf_nodelta env evd t in
+    let (evd', val') =
+      try
+	inh_conv_coerce_to_fail loc env evd rigidonly
 	  (Some cj.uj_val) cj.uj_type t
-	with NoCoercion ->
+      with NoCoercion ->
 	(try
 	   coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
 	 with NoSubtacCoercion ->
 	   error_actual_type_loc loc env evd cj t)
-      in
-      let val' = match val' with Some v -> v | None -> assert(false) in
-	(evd',{ uj_val = val'; uj_type = t })
-    | Some (init, cur) ->
-      (evd, cj)
-
+    in
+    let val' = match val' with Some v -> v | None -> assert(false) in
+      (evd',{ uj_val = val'; uj_type = t })
+	
   let inh_conv_coerce_to = inh_conv_coerce_to_gen false
   let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
 
-  let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
-    let nabsinit, nabs =
-      match abs with
-	  None -> 0, 0
-	| Some (init, cur) -> init, cur
-    in
-      try
-	let rels, rng = Reductionops.splay_prod_n env ( isevars) nabs t in
-	(* The final range free variables must have been replaced by evars, we accept only that evars
-	   in rng are applied to free vars. *)
-	if noccur_with_meta 1 (succ nabs) rng then (
-	  let env', t, t' =
-	    let env' = push_rel_context rels env in
-	      env', rng, lift nabs t'
-	  in
-	    try
-	      fst (try inh_conv_coerce_to_fail loc env' isevars false None t t'
-		   with NoCoercion ->
-		     coerce_itf loc env' isevars None t t')
-	    with NoSubtacCoercion ->
-	      error_cannot_coerce env' isevars (t, t'))
-	else isevars
-      with _ -> isevars
+
+  let inh_conv_coerces_to loc env evd t t' =
+    try
+      fst (inh_conv_coerce_to_fail loc env evd true None t t')
+    with NoCoercion ->
+      evd (* Maybe not enough information to unify *)
+
 end
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index c8acf7e0bb..b83057ac8b 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -126,7 +126,7 @@ let subtac_process ?(is_type=false) env isevars id bl c tycon =
   in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars !isevars in
-  let ty = nf_evar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+  let ty = nf_evar !isevars (match tycon with Some c -> c | _ -> ctyp) in
     evm, coqc, ty, imps
 
 open Subtac_obligations
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index fbeed381d3..43182765df 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -177,13 +177,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     in
       match tycon with
       | None -> evd,(Anonymous,None,None)
-      | Some (abs, c) ->
-	  (match abs with
-	   | None ->
-	       let evd', (n, dom, rng) = real_split evd c in
-		 evd', (n, mk_tycon dom, mk_tycon rng)
-	   | Some (init, cur) ->
-	       evd, (Anonymous, None, Some (Some (init, succ cur), c)))
+      | Some c ->
+	  let evd', (n, dom, rng) = real_split evd c in
+	    evd', (n, mk_tycon dom, mk_tycon rng)
 	    
 	    
   (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
@@ -222,8 +218,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     | GHole (loc,k) ->
 	let ty =
           match tycon with
-            | Some (None, ty) -> ty
-            | None | Some _ ->
+            | Some ty -> ty
+            | None ->
 		e_new_evar evdref env ~src:(loc, InternalHole) (Termops.new_Type ()) in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
@@ -312,43 +308,52 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env evdref s' tycon
 
     | GApp (loc,f,args) ->
+	let fj = pretype empty_tycon env evdref lvar f in
+ 	let floc = loc_of_glob_constr f in
 	let length = List.length args in
-	let ftycon =
-	  let ty =
-	    if length > 0 then
-	      match tycon with
-	      | None -> None
-	      | Some (None, ty) -> mk_abstr_tycon length ty
-	      | Some (Some (init, cur), ty) ->
-		  Some (Some (length + init, length + cur), ty)
- 	    else tycon
-	  in
-	    match ty with
-	    | Some (_, t) ->
-	      if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty
-	      else None
-	    | _ -> None
+	let candargs =
+	  (* Bidirectional typechecking hint: 
+	     parameters of a constructor are completely determined
+	     by a typing constraint *)
+	  if length > 0 && isConstruct fj.uj_val then
+	    match tycon with
+	    | None -> []
+	    | Some ty -> 
+		let (ind, i) = destConstruct fj.uj_val in
+		let npars = inductive_nparams ind in
+		  if npars = 0 then []
+		  else
+		    try 
+		      (* Does not treat partially applied constructors. *)
+		      let IndType (indf, args) = find_rectype env !evdref ty in
+		      let (ind',pars) = dest_ind_family indf in
+			if ind = ind' then pars
+			else (* Let the usual code throw an error *) []
+		    with Not_found -> []
+ 	  else []
 	in
-	let fj = pretype ftycon env evdref lvar f in
- 	let floc = loc_of_glob_constr f in
-	let rec apply_rec env n resj tycon = function
+	let rec apply_rec env n resj candargs = function
 	  | [] -> resj
 	  | c::rest ->
 	      let argloc = loc_of_glob_constr c in
 	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
               let resty = whd_betadeltaiota env !evdref resj.uj_type in
       		match kind_of_term resty with
-		  | Prod (na,c1,c2) ->
-		      Option.iter (fun ty -> evdref :=
-			Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon;
-		      let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in
-		      evdref := evd;
-		      let hj = pretype (mk_tycon c1) env evdref lvar c in
-		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
-			apply_rec env (n+1)
+		| Prod (na,c1,c2) ->
+		    let hj = pretype (mk_tycon c1) env evdref lvar c in
+		    let candargs, ujval =
+		      match candargs with
+		      | [] -> [], j_val hj
+		      | arg :: args -> 
+			  if e_conv env evdref (j_val hj) arg then
+			    args, nf_evar !evdref (j_val hj)
+			  else [], j_val hj
+		    in
+		    let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
+		      apply_rec env (n+1)
 			{ uj_val = value;
 			  uj_type = typ }
-			  (Option.map (fun (abs, c) -> abs, c) tycon) rest
+			candargs rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
@@ -356,7 +361,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env !evdref
 	      		  resj [hj]
 	in
-	let resj = apply_rec env 1 fj ftycon args in
+	let resj = apply_rec env 1 fj candargs args in
 	let resj =
 	  match kind_of_term (whd_evar !evdref resj.uj_val) with
 	  | App (f,args) when isInd f or isConst f ->
@@ -503,8 +508,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  jtyp.uj_val, jtyp.uj_type
 	    | None ->
 		let p = match tycon with
-		  | Some (None, ty) -> ty
-		  | None | Some _ ->
+		  | Some ty -> ty
+		  | None ->
                       e_new_evar evdref env ~src:(loc,InternalHole) (Termops.new_Type ())
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 0ed78a23b6..cb1c9f8e1f 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -114,7 +114,7 @@ let my_print_env = Termops.print_env
 let my_print_glob_constr = Printer.pr_glob_constr_env
 let my_print_evardefs = Evd.pr_evar_map None
 
-let my_print_tycon_type = Evarutil.pr_tycon_type
+let my_print_tycon = Evarutil.pr_tycon
 
 let debug_level = 2
 
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 70ad0bcc82..719b87952a 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -70,7 +70,7 @@ val my_print_rel_context : env -> rel_context -> std_ppcmds
 val my_print_named_context : env -> std_ppcmds
 val my_print_env : env -> std_ppcmds
 val my_print_glob_constr : env -> glob_constr -> std_ppcmds
-val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
+val my_print_tycon : env -> type_constraint -> std_ppcmds
 
 
 val debug : int -> std_ppcmds -> unit