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

7 files changed, 97 insertions, 144 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3ef14f7e12..2883df6d7a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -390,7 +390,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
 		current
 	      else
 		(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
-		  pb.evdref (make_judge current typ) (mk_tycon_type indt)).uj_val in
+		  pb.evdref (make_judge current typ) indt).uj_val in
 	    let sigma =  !(pb.evdref) in
 	    (current,try_find_ind pb.env sigma indt names))
   | _ -> (current,tmtyp)
@@ -1743,7 +1743,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
   let preds =
     match pred, tycon with
     (* No type annotation *)
-    | None, Some (None, t) when not (noccur_with_meta 0 max_int t) ->
+    | None, Some t when not (noccur_with_meta 0 max_int t) ->
 	(* If the tycon is not closed w.r.t real variables, we try *)
         (* two different strategies *)
 	(* First strategy: we abstract the tycon wrt to the dependencies *)
@@ -1756,8 +1756,8 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
 	(* No dependent type constraint, or no constraints at all: *)
 	(* we use two strategies *)
         let sigma,t = match tycon with
-	| Some (None, t) -> sigma,t
-	| _ -> new_type_evar sigma env ~src:(loc, CasesType) in
+	| Some t -> sigma,t
+	| None -> new_type_evar sigma env ~src:(loc, CasesType) in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Second strategy: we directly use the evar as a non dependent pred *)
@@ -1770,12 +1770,13 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
       let sigma, newt = new_sort_variable sigma in
       let evdref = ref sigma in
       let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
-      let sigma = Option.cata (fun tycon ->
-          let na = Name (id_of_string "x") in
-          let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in
-          let predinst = extract_predicate predcclj.uj_val tms in
-          Coercion.inh_conv_coerces_to loc env !evdref predinst tycon)
-        !evdref tycon in
+      let sigma = !evdref in
+      (* let sigma = Option.cata (fun tycon -> *)
+      (*     let na = Name (id_of_string "x") in *)
+      (*     let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in *)
+      (*     let predinst = extract_predicate predcclj.uj_val tms in *)
+      (*     Coercion.inh_conv_coerce_to loc env !evdref predinst tycon) *)
+      (*   !evdref tycon in *)
       let predccl = (j_nf_evar sigma predcclj).uj_val in
       [sigma, predccl]
   in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0c340f9ed0..eb014af464 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -54,22 +54,22 @@ module type S = sig
 
   (* [inh_coerce_to_prod env evars t] coerces [t] to a product type *)
   val inh_coerce_to_prod : loc ->
-    env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
+    env -> evar_map -> types -> evar_map * types
 
   (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type
      [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_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
   val inh_conv_coerce_rigid_to : loc ->
-    env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
-  (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t]
+  (** [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_map -> types -> type_constraint_type -> evar_map
+    env -> evar_map -> types -> types -> evar_map
 
   (* [inh_pattern_coerce_to loc env evd pat ind1 ind2] coerces the Cases
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
@@ -223,63 +223,27 @@ module Default = 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) =
-    match n with
-	None ->
-	  let (evd', val') =
-	    try
-	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-	    with NoCoercion ->
-	      let evd = saturate_evd env evd in
-		try
-		  inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-		with NoCoercion ->
-		  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)
+  let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
+    let (evd', val') =
+      try
+	inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+      with NoCoercion ->
+	let evd = saturate_evd env evd in
+	  try
+	    inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+	  with NoCoercion ->
+	    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 })
 
   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 (evd : evar_map) t (abs, t') =
-      if abs = None then
-	try
-	  fst (inh_conv_coerce_to_fail loc env evd true None t t')
-	with NoCoercion ->
-	  evd (* Maybe not enough information to unify *)
-      else
-        evd
-      (* Still problematic, as it changes unification
-      let nabsinit, nabs =
-	match abs with
-	    None -> 0, 0
-	  | Some (init, cur) -> init, cur
-      in
-	try
-	  let (rels, rng) =
-	    (* a little more effort to get products is needed *)
-	    try decompose_prod_n nabs t
-	    with _ ->
-	      if !Flags.debug then
-		msg_warning (str "decompose_prod_n failed");
-	      raise (Invalid_argument "Coercion.inh_conv_coerces_to")
-	  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 0 (succ nabsinit) rng then (
-	      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 nabs t'
-	      in
-		try
-		  pi1 (inh_conv_coerce_to_fail loc env' evd None t t')
-		with NoCoercion ->
-		  evd) (* Maybe not enough information to unify *)
-	      (*let sigma =  evd in
-		error_cannot_coerce env' sigma (t, t'))*)
-	    else evd
-	with Invalid_argument _ -> evd	  *)
+  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/pretyping/coercion.mli b/pretyping/coercion.mli
index f312802a89..91cb693abf 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -39,22 +39,22 @@ module type S = sig
 
   (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
   val inh_coerce_to_prod : loc ->
-    env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
+    env -> evar_map -> types -> evar_map * types
 
   (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
      [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_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
 
   val inh_conv_coerce_rigid_to : loc ->
-    env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
+    env -> evar_map -> unsafe_judgment -> types -> evar_map * 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_map -> types -> type_constraint_type -> evar_map
+    env -> evar_map -> types -> types -> evar_map
 
   (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
      pattern [pat] typed in [ind1] into a pattern typed in [ind2];
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5faa86cb02..8da1270727 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1632,8 +1632,7 @@ open Glob_term
 
 (* Operations on value/type constraints *)
 
-type type_constraint_type = (int * int) option * constr
-type type_constraint = type_constraint_type option
+type type_constraint = types option
 
 type val_constraint = constr option
 
@@ -1654,14 +1653,8 @@ type val_constraint = constr option
 (* The empty type constraint *)
 let empty_tycon = None
 
-let mk_tycon_type c = (None, c)
-let mk_abstr_tycon_type n c = (Some (n, n), c) (* First component is initial abstraction, second
-						  is current abstraction *)
-
 (* Builds a type constraint *)
-let mk_tycon ty = Some (mk_tycon_type ty)
-
-let mk_abstr_tycon n ty = Some (mk_abstr_tycon_type n ty)
+let mk_tycon ty = Some ty
 
 (* Constrains the value of a type *)
 let empty_valcon = None
@@ -1669,7 +1662,6 @@ let empty_valcon = None
 (* Builds a value constraint *)
 let mk_valcon c = Some c
 
-
 let new_type_evar ?src ?filter evd env =
   let evd', s = new_sort_variable evd in
     new_evar evd' env ?src ?filter (mkSort s)
@@ -1765,10 +1757,6 @@ let judge_of_new_Type evd =
    constraint on its domain and codomain. If the input constraint is
    an evar instantiate it with the product of 2 new evars. *)
 
-let unlift_tycon init cur c =
-  if cur = 1 then None, c
-  else Some (init, pred cur), c
-
 let split_tycon loc env evd tycon =
   let rec real_split evd c =
     let t = whd_betadeltaiota env evd c in
@@ -1785,35 +1773,13 @@ let split_tycon loc env evd tycon =
   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 (unlift_tycon init cur c)))
-
-let valcon_of_tycon x =
-  match x with
-    | Some (None, t) -> Some t
-    | _ -> None
-
-let lift_abstr_tycon_type n (abs, t) =
-  match abs with
-      None -> raise (Invalid_argument "lift_abstr_tycon_type: not an abstraction")
-    | Some (init, abs) ->
-	let abs' = abs + n in
-	  if abs' < 0 then raise (Invalid_argument "lift_abstr_tycon_type")
-	  else (Some (init, abs'), t)
-
-let lift_tycon_type n (abs, t) = (abs, lift n t)
-let lift_tycon n = Option.map (lift_tycon_type n)
+      | Some c ->
+	  let evd', (n, dom, rng) = real_split evd c in
+	    evd', (n, mk_tycon dom, mk_tycon rng)
 
-let pr_tycon_type env (abs, t) =
-  match abs with
-      None -> Termops.print_constr_env env t
-    | Some (init, cur) -> str "Abstract (" ++ int init ++ str ","  ++ int cur ++ str ") " ++ Termops.print_constr_env env t
+let valcon_of_tycon x = x
+let lift_tycon n = Option.map (lift n)
 
 let pr_tycon env = function
     None -> str "None"
-  | Some t -> pr_tycon_type env t
+  | Some t -> Termops.print_constr_env env t
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 82205c91f6..fb0c481ef1 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -146,16 +146,11 @@ val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t
 
 val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
 
-type type_constraint_type = (int * int) option * constr
-type type_constraint = type_constraint_type option
-
+type type_constraint = types option
 type val_constraint = constr option
 
 val empty_tycon : type_constraint
-val mk_tycon_type : constr -> type_constraint_type
-val mk_abstr_tycon_type : int -> constr -> type_constraint_type
 val mk_tycon : constr -> type_constraint
-val mk_abstr_tycon : int -> constr -> type_constraint
 val empty_valcon : val_constraint
 val mk_valcon : constr -> val_constraint
 
@@ -164,10 +159,6 @@ val split_tycon :
     evar_map * (name * type_constraint * type_constraint)
 
 val valcon_of_tycon : type_constraint -> val_constraint
-
-val lift_abstr_tycon_type : int -> type_constraint_type -> type_constraint_type
-
-val lift_tycon_type : int -> type_constraint_type -> type_constraint_type
 val lift_tycon : int -> type_constraint -> type_constraint
 
 (***********************************************************)
@@ -202,7 +193,6 @@ val expand_vars_in_term : env -> constr -> constr
 
 (** {6 debug pretty-printer:} *)
 
-val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
 val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b1419c47b4..4f286efe7a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -219,6 +219,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
   let allow_anonymous_refs = ref false
 
+  let program_mode = ref false
+
   let evd_comb0 f evdref =
     let (evd',x) = f !evdref in
       evdref := evd';
@@ -355,16 +357,16 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | GPatVar (loc,(someta,n)) ->
 	let ty =
           match tycon with
-            | Some (None, ty) -> ty
-            | None | Some _ -> new_type_evar evdref env loc in
+            | Some ty -> ty
+            | None -> new_type_evar evdref env loc in
         let k = MatchingVar (someta,n) in
 	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
     | GHole (loc,k) ->
 	let ty =
           match tycon with
-            | Some (None, ty) -> ty
-            | None | Some _ ->
+            | Some ty -> ty
+            | None ->
 		new_type_evar evdref env loc in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
@@ -438,27 +440,58 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     | GApp (loc,f,args) ->
 	let fj = pretype empty_tycon env evdref lvar f in
  	let floc = loc_of_glob_constr f in
-	let rec apply_rec env n resj = function
+	let length = List.length args in
+	let candargs =
+	  (* Bidirectional typechecking hint: 
+	     parameters of a constructor are completely determined
+	     by a typing constraint *)
+	  if !program_mode && 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 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) ->
-		      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)
-			  { uj_val = value;
-			    uj_type = typ }
-			  rest
+		| 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 }
+			candargs rest
+
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
 			error_cant_apply_not_functional_loc
 			  (join_loc floc argloc) env !evdref
 	      		  resj [hj]
 	in
-	let resj = apply_rec env 1 fj args in
+	let resj = apply_rec env 1 fj candargs args in
 	let resj =
 	  match evar_kind_of_term !evdref resj.uj_val with
 	  | App (f,args) ->
@@ -612,8 +645,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	        pred, typ
 	    | None ->
 		let p = match tycon with
-		  | Some (None, ty) -> ty
-		  | None | Some _ -> new_type_evar evdref env loc
+		  | Some ty -> ty
+		  | None -> new_type_evar evdref env loc
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
 	  let pred = nf_evar !evdref pred in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 48a2c8c425..be6d90a264 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -795,8 +795,7 @@ let try_to_coerce env evd c cty tycon =
     (evd',j'.uj_val)
 
 let w_coerce_to_type env evd c cty mvty =
-  let evd,mvty = pose_all_metas_as_evars env evd mvty in
-  let tycon = mk_tycon_type mvty in
+  let evd,tycon = pose_all_metas_as_evars env evd mvty in
     try try_to_coerce env evd c cty tycon
     with e when precatchable_exception e ->
     (* inh_conv_coerce_rigid_to should have reasoned modulo reduction