Introducing a notion of evar candidates to be used when an evar is

known in advance to be instantiable by only a finite number of terms.
When an evar with candidates remain unsolved after unification, the
first candidate is taken as a heuristic.

This is used in particular to reduce the number of pending conversion
problems when trying to infer the return clause of a pattern-matching
problem. As an example, this repairs test 2615.v.

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

8 files changed, 62 insertions, 18 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 77007b0ba5..8963ea5ea5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1489,9 +1489,9 @@ let abstract_tycon loc env evdref subst _tycon extenv t =
 	List.map (fun (id,_,_) -> dependent (mkVar id) u)
 	  (named_context extenv) in
       let filter = rel_filter@named_filter in
+      let candidates = u :: List.map mkRel vl in
       let ev =
-	e_new_evar evdref extenv ~src:(loc, CasesType) ~filter:filter ty in
-      evdref := add_conv_pb (Reduction.CONV,extenv,substl inst ev,u) !evdref;
+	e_new_evar evdref extenv ~src:(loc, CasesType) ~filter ~candidates ty in
       lift k ev
     else
       map_constr_with_full_binders push_binder aux x t in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 91b0eacc48..04f86e709e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -764,7 +764,11 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
   Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
 			  |_,ImpossibleCase -> 
 			     Evd.define ev (j_type (coq_unit_judge ())) evd'
-			  |_ -> evd') heuristic_solved_evd heuristic_solved_evd
+			  |_ ->
+                             match ev_info.evar_candidates with
+                             | Some (a::l) -> Evd.define ev a evd'
+                             | Some [] -> error "Unsolvable existential variables"
+                             | None -> evd') heuristic_solved_evd heuristic_solved_evd
 
 (* Main entry points *)
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index bf4c18f918..7d66bee053 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -158,12 +158,12 @@ let new_untyped_evar =
  * functional operations on evar sets *
  *------------------------------------*)
 
-let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter instance =
+let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter ?candidates instance =
   assert
     (let ctxt = named_context_of_val sign in
      list_distinct (ids_of_named_context ctxt));
   let newevk = new_untyped_evar() in
-  let evd = evar_declare sign newevk typ ~src:src ?filter evd in
+  let evd = evar_declare sign newevk typ ~src:src ?filter ?candidates evd in
   (evd,mkEvar (newevk,Array.of_list instance))
 
 (* Expand rels and vars that are bound to other rels or vars so that
@@ -388,22 +388,23 @@ let push_rel_context_to_named_context env typ =
 	let d = (id,Option.map (substl subst) c,substl subst t) in
 	(mkVar id :: subst, id::avoid, push_named d env))
       (rel_context env) ~init:([], ids, env) in
-  (named_context_val env, substl subst typ, inst_rels@inst_vars)
+  (named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 
-let new_evar evd env ?(src=(dummy_loc,InternalHole)) ?filter typ =
-  let sign,typ',instance = push_rel_context_to_named_context env typ in
+let new_evar evd env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates typ =
+  let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
+  let candidates = Option.map (List.map (substl subst)) candidates in
   let instance =
     match filter with
     | None -> instance
     | Some filter -> snd (list_filter2 (fun b c -> b) (filter,instance)) in
-  new_evar_instance sign evd typ' ~src:src ?filter instance
+  new_evar_instance sign evd typ' ~src:src ?filter ?candidates instance
 
   (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty =
-  let (evd',ev) = new_evar !evdref env ~src:src ?filter ty in
+let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty =
+  let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
   evdref := evd';
   ev
 
@@ -919,6 +920,7 @@ let do_restrict_hyps evd evk projs =
 (* [postpone_evar_term] postpones an equation of the form ?e[σ] = c *)
 
 let postpone_evar_term env evd (evk,argsv) rhs =
+  assert (isVar rhs or isRel rhs);
   let rhs = expand_vars_in_term env rhs in
   let evi = Evd.find evd evk in
   let evd,evk,args =
@@ -1054,6 +1056,35 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
   let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
     Evd.add_conv_pb pb evd
 
+(* If the evar can be instantiated by a finite set of candidates known
+   in advance, we check which of them apply *)
+
+exception NoCandidates
+
+let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
+  let evi = Evd.find evd evk in
+  let args = Array.to_list argsv in
+  match evi.evar_candidates with
+  | None -> raise NoCandidates
+  | Some l ->
+      let l' = list_map_filter (fun c ->
+        let c' = instantiate_evar (evar_filtered_context evi) c args in
+        let evd, b = conv_algo env evd Reduction.CONV c' rhs in
+        if b then Some (c,evd) else None) l in
+      match l' with
+      | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
+      | [c,evd] -> Evd.define evk c evd
+      | l when List.length l < List.length l' ->
+          let candidates = List.map fst l in
+          let filter = evar_filter evi in
+          let sign = evar_hyps evi in
+          let ids = List.map pi1 (named_context_of_val sign) in
+          let inst_in_sign =
+            List.map mkVar (snd (list_filter2 (fun b id -> b) (filter,ids))) in
+          let evd,evar = new_evar_instance (evar_hyps evi) evd (evar_concl evi)
+            ~filter ~candidates inst_in_sign in
+          Evd.define evk evar evd
+      | l -> evd
 
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
@@ -1202,6 +1233,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
       if evk = evk2 then solve_refl conv_algo env evd evk argsv argsv2
       else solve_evar_evar (evar_define conv_algo) env evd ev ev2
   | _ ->
+  try solve_candidates conv_algo env evd ev rhs
+  with NoCandidates ->
   try
     let (evd',body) = invert_definition conv_algo choose env evd ev rhs in
     if occur_meta body then error "Meta cannot occur in evar body.";
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 78898aaa7c..61f503c7dc 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -28,11 +28,13 @@ val new_untyped_evar : unit -> existential_key
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_map * constr
+  evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list ->
+  ?candidates:constr list -> types -> evar_map * constr
 
 (** the same with side-effects *)
 val e_new_evar :
-  evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr
+  evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list ->
+  ?candidates:constr list -> types -> constr
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
@@ -46,7 +48,7 @@ val new_type_evar :
    of [inst] are typed in the occurrence context and their type (seen
    as a telescope) is [sign] *)
 val new_evar_instance :
- named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_map * constr
+ named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
 
 val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
 
@@ -219,7 +221,7 @@ val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
   identifier list -> named_context_val * types
 
 val push_rel_context_to_named_context : Environ.env -> types ->
-  named_context_val * types * constr list
+  named_context_val * types * constr list * constr list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 552e8aba33..44d25f626e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -49,6 +49,7 @@ type evar_info = {
   evar_body : evar_body;
   evar_filter : bool list;
   evar_source : hole_kind located;
+  evar_candidates : constr list option; (* if not None, list of allowed instances *)
   evar_extra : Store.t }
 
 let make_evar hyps ccl = {
@@ -57,6 +58,7 @@ let make_evar hyps ccl = {
   evar_body = Evar_empty;
   evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
   evar_source = (dummy_loc,InternalHole);
+  evar_candidates = None;
   evar_extra = Store.empty
 }
 
@@ -429,7 +431,7 @@ let define evk body evd =
 	| [] ->  evd.last_mods
         | _ -> ExistentialSet.add evk evd.last_mods }
 
-let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
+let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter ?candidates evd =
   let filter =
     if filter = None then
       List.map (fun _ -> true) (named_context_of_val hyps)
@@ -445,6 +447,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
        evar_body = Evar_empty;
        evar_filter = filter;
        evar_source = src;
+       evar_candidates = candidates;
        evar_extra = Store.empty } }
 
 let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index feddb908ea..55c54f2c6e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -117,6 +117,7 @@ type evar_info = {
   evar_body : evar_body;
   evar_filter : bool list;
   evar_source : hole_kind located;
+  evar_candidates : constr list option;
   evar_extra : Store.t }
 
 val eq_evar_info : evar_info -> evar_info -> bool
@@ -195,7 +196,7 @@ val defined_evars : evar_map -> evar_map
 val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
 val evar_declare :
   named_context_val -> evar -> types -> ?src:loc * hole_kind ->
-      ?filter:bool list -> evar_map -> evar_map
+      ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
 val evar_source : existential_key -> evar_map -> hole_kind located
 
 (* spiwack: this function seems to somewhat break the abstraction. 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index b50177eeae..1542267e36 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -500,6 +500,7 @@ module V82 = struct
 	                                                        (Environ.named_context_of_val hyps);
 		     Evd.evar_body = Evd.Evar_empty; 
 		     Evd.evar_source = (Util.dummy_loc,Evd.GoalEvar);
+		     Evd.evar_candidates = None;
 		     Evd.evar_extra = extra }
     in
     let evi = Typeclasses.mark_unresolvable evi in
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 82b4267759..e219bbff09 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -542,7 +542,7 @@ let evar_dependencies evm p =
     evm ()
 
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
-  let nc, gl, subst = Evarutil.push_rel_context_to_named_context env gl in
+  let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) = 
     Goal.V82.mk_goal sigma nc gl Store.empty in
   let gls = { it = gl ; sigma = sigma } in