Splitting Class_tactics between code and CAMLP4/5 declarations.

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

1 files changed, 761 insertions, 0 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
new file mode 100644
index 0000000000..d80b7d738a
--- /dev/null
+++ b/tactics/class_tactics.ml
@@ -0,0 +1,761 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Errors
+open Util
+open Names
+open Term
+open Termops
+open Reduction
+open Proof_type
+open Tacticals
+open Tacmach
+open Tactics
+open Patternops
+open Clenv
+open Typeclasses
+open Globnames
+open Evd
+open Locus
+open Misctypes
+
+(** Hint database named "typeclass_instances", now created directly in Auto *)
+
+let typeclasses_db = Auto.typeclasses_db
+
+let typeclasses_debug = ref false
+let typeclasses_depth = ref None
+
+exception Found of evar_map
+
+(** We transform the evars that are concerned by this resolution
+    (according to predicate p) into goals.
+    Invariant: function p only manipulates undefined evars *)
+
+let evars_to_goals p evm =
+  let goals, evm' =
+    Evd.fold_undefined
+      (fun ev evi (gls, evm') ->
+	let evi', goal = p evm ev evi in
+	let gls' = if goal then (ev,Goal.V82.build ev) :: gls else gls in
+	(gls', Evd.add evm' ev evi'))
+      evm ([], Evd.defined_evars evm)
+  in
+  if List.is_empty goals then None else Some (List.rev goals, evm')
+
+(** Typeclasses instance search tactic / eauto *)
+
+open Auto
+
+let e_give_exact flags c gl =
+  let t1 = (pf_type_of gl c) in
+    tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) gl
+
+open Unification
+
+let auto_unif_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
+  use_metas_eagerly_in_conv_on_closed_terms = true;
+  modulo_delta = var_full_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  modulo_delta_in_merge = None;
+  check_applied_meta_types = false;
+  resolve_evars = false;
+  use_pattern_unification = true;
+  use_meta_bound_pattern_unification = true;
+  frozen_evars = Evar.Set.empty;
+  restrict_conv_on_strict_subterms = false; (* ? *)
+  modulo_betaiota = true;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
+}
+
+let rec eq_constr_mod_evars x y =
+  match kind_of_term x, kind_of_term y with
+  | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true
+  | _, _ -> compare_constr eq_constr_mod_evars x y
+
+let progress_evars t gl =
+  let concl = pf_concl gl in
+  let check gl' =
+    let newconcl = pf_concl gl' in
+      if eq_constr_mod_evars concl newconcl
+      then tclFAIL 0 (str"No progress made (modulo evars)") gl'
+      else tclIDTAC gl'
+  in tclTHEN t check gl
+
+let unify_e_resolve flags (c,clenv) gls =
+  let clenv' = connect_clenv gls clenv in
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
+    Clenvtac.clenv_refine true ~with_classes:false clenv' gls
+
+let unify_resolve flags (c,clenv) gls =
+  let clenv' = connect_clenv gls clenv in
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
+    Clenvtac.clenv_refine false ~with_classes:false clenv' gls
+
+let clenv_of_prods nprods (c, clenv) gls =
+  if Int.equal nprods 0 then Some clenv
+  else
+    let ty = pf_type_of gls c in
+    let diff = nb_prod ty - nprods in
+      if diff >= 0 then
+	Some (mk_clenv_from_n gls (Some diff) (c,ty))
+      else None
+
+let with_prods nprods (c, clenv) f gls =
+  match clenv_of_prods nprods (c, clenv) gls with
+  | None -> tclFAIL 0 (str"Not enough premisses") gls
+  | Some clenv' -> f (c, clenv') gls
+
+(** Hack to properly solve dependent evars that are typeclasses *)
+
+let flags_of_state st =
+  {auto_unif_flags with
+    modulo_conv_on_closed_terms = Some st; modulo_delta = st;
+     modulo_delta_types = st;
+     modulo_eta = false}
+
+let rec e_trivial_fail_db db_list local_db goal =
+  let tacl =
+    Eauto.registered_e_assumption ::
+    (tclTHEN Tactics.intro
+       (function g'->
+	  let d = pf_last_hyp g' in
+	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
+          (e_trivial_fail_db db_list
+	      (Hint_db.add_list hintl local_db) g'))) ::
+    (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (pf_concl goal)))
+  in
+  tclFIRST (List.map tclCOMPLETE tacl) goal
+
+and e_my_find_search db_list local_db hdc complete concl =
+  let hdc = head_of_constr_reference hdc in
+  let prods, concl = decompose_prod_assum concl in
+  let nprods = List.length prods in
+  let hintl =
+    List.map_append
+      (fun db ->
+	if Hint_db.use_dn db then
+	  let flags = flags_of_state (Hint_db.transparent_state db) in
+	    List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
+	else
+	  let flags = flags_of_state (Hint_db.transparent_state db) in
+	    List.map (fun x -> (flags, x)) (Hint_db.map_all hdc db))
+      (local_db::db_list)
+  in
+  let tac_of_hint =
+    fun (flags, {pri = b; pat = p; code = t; name = name}) ->
+      let tac =
+	match t with
+	  | Res_pf (term,cl) -> with_prods nprods (term,cl) (unify_resolve flags)
+	  | ERes_pf (term,cl) -> with_prods nprods (term,cl) (unify_e_resolve flags)
+	  | Give_exact (c) -> e_give_exact flags c
+	  | Res_pf_THEN_trivial_fail (term,cl) ->
+              tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags))
+	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
+	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
+	  | Extern tacast ->
+(* 	    tclTHEN *)
+(* 	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) *)
+	      (conclPattern concl p tacast)
+      in
+      let tac = if complete then tclCOMPLETE tac else tac in
+	match t with
+	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
+	| _ ->
+(* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
+	    (tac,b,false, name, lazy (pr_autotactic t))
+  in List.map tac_of_hint hintl
+
+and e_trivial_resolve db_list local_db gl =
+  try
+    e_my_find_search db_list local_db
+    (fst (head_constr_bound gl)) true gl
+  with Bound | Not_found -> []
+
+let e_possible_resolve db_list local_db gl =
+  try
+    e_my_find_search db_list local_db
+      (fst (head_constr_bound gl)) false gl
+  with Bound | Not_found -> []
+
+let rec catchable = function
+  | Refiner.FailError _ -> true
+  | e -> Logic.catchable_exception e
+
+let nb_empty_evars s =
+  Evar.Map.cardinal (undefined_map s)
+
+let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
+
+let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
+
+type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
+		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
+		  auto_path : global_reference option list;
+		  auto_cut : hints_path }
+type autogoal = goal * autoinfo
+type 'ans fk = unit -> 'ans
+type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
+type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans }
+
+type auto_result = autogoal list sigma
+
+type atac = auto_result tac
+
+(* Some utility types to avoid the need of -rectypes *)
+
+type 'a optionk =
+  | Nonek
+  | Somek of 'a * 'a optionk fk
+
+type ('a,'b) optionk2 =
+  | Nonek2
+  | Somek2 of 'a * 'b * ('a,'b) optionk2 fk
+
+let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
+  let cty = Evarutil.nf_evar sigma cty in
+  let rec iscl env ty =
+    let ctx, ar = decompose_prod_assum ty in
+      match kind_of_term (fst (decompose_app ar)) with
+      | Const c -> is_class (ConstRef c)
+      | Ind i -> is_class (IndRef i)
+      | _ ->
+	  let env' = Environ.push_rel_context ctx env in
+	  let ty' = whd_betadeltaiota env' ar in
+	       if not (eq_constr ty' ar) then iscl env' ty'
+	       else false
+  in
+  let is_class = iscl env cty in
+  let keep = not only_classes || is_class in
+    if keep then
+      let c = mkVar id in
+      let name = PathHints [VarRef id] in
+      let hints =
+	if is_class then
+	  let hints = build_subclasses ~check:false env sigma (VarRef id) None in
+	    (List.map_append
+	       (fun (path,pri, c) -> make_resolves env sigma ~name:(PathHints path)
+		  (true,false,Flags.is_verbose()) pri c)
+	       hints)
+	else []
+      in
+        (hints @ List.map_filter
+	 (fun f -> try Some (f (c, cty)) with Failure _ | UserError _ -> None)
+	 [make_exact_entry ~name sigma pri; make_apply_entry ~name env sigma flags pri])
+    else []
+
+let pf_filtered_hyps gls =
+  Goal.V82.hyps gls.Evd.sigma (sig_it gls)
+
+let make_hints g st only_classes sign =
+  let paths, hintlist =
+    List.fold_left
+    (fun (paths, hints) hyp ->
+     if is_section_variable (pi1 hyp) then (paths, hints)
+     else
+       let path, hint =
+	 PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp
+       in
+	 (PathOr (paths, path), hint @ hints))
+    (PathEmpty, []) sign
+  in Hint_db.add_list hintlist (Hint_db.empty st true)
+
+let autogoal_hints_cache
+    : (bool * Environ.named_context_val * hint_db) option ref
+    = Summary.ref None ~name:"autogoal-hints-cache"
+let freeze () = !autogoal_hints_cache
+let unfreeze v = autogoal_hints_cache := v
+
+let make_autogoal_hints =
+  fun only_classes ?(st=full_transparent_state) g ->
+    let sign = pf_filtered_hyps g in
+      match freeze () with
+      | Some (onlyc, sign', hints)
+	  when (onlyc : bool) == only_classes &&
+	    Environ.eq_named_context_val sign sign' -> hints
+      | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in
+	  unfreeze (Some (only_classes, sign, hints)); hints
+
+let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
+  { skft = fun sk fk {it = gl,hints; sigma=s;eff=eff} ->
+    let res = try Some (tac {it=gl; sigma=s;eff=eff})
+              with e when catchable e -> None in
+      match res with
+      | Some gls -> sk (f gls hints) fk
+      | None -> fk () }
+
+let intro_tac : atac =
+  lift_tactic Tactics.intro
+    (fun {it = gls; sigma = s;eff=eff} info ->
+      let gls' =
+	List.map (fun g' ->
+	  let env = Goal.V82.env s g' in
+	  let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
+	  let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
+	    (true,false,false) info.only_classes None (List.hd context) in
+	  let ldb = Hint_db.add_list hint info.hints in
+	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
+      in {it = gls'; sigma = s;eff=eff})
+
+let normevars_tac : atac =
+  { skft = fun sk fk {it = (gl, info); sigma = s; eff=eff} ->
+    let gl', sigma' = Goal.V82.nf_evar s gl in
+    let info' = { info with auto_last_tac = lazy (str"normevars") } in
+      sk {it = [gl', info']; sigma = sigma';eff=eff} fk }
+
+(* Ordering of states is lexicographic on the number of remaining goals. *)
+let compare (pri, _, _, res) (pri', _, _, res') =
+  let nbgoals s =
+    List.length (sig_it s) + nb_empty_evars (sig_sig s)
+  in
+  let pri = pri - pri' in
+    if not (Int.equal pri 0) then pri
+    else nbgoals res - nbgoals res'
+
+let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
+  { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
+
+let hints_tac hints =
+  { skft = fun sk fk {it = gl,info; sigma = s;eff=eff} ->
+      let concl = Goal.V82.concl s gl in
+      let tacgl = {it = gl; sigma = s;eff=eff} in
+      let poss = e_possible_resolve hints info.hints concl in
+      let rec aux i foundone = function
+	| (tac, _, b, name, pp) :: tl ->
+	  let derivs = path_derivate info.auto_cut name in
+	  let res =
+            try
+		if path_matches derivs [] then None else Some (tac tacgl)
+	    with e when catchable e -> None
+	  in
+	    (match res with
+	       | None -> aux i foundone tl
+	       | Some {it = gls; sigma = s';eff=eff} ->
+	    	   if !typeclasses_debug then
+		     msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
+			    ++ str" on" ++ spc () ++ pr_ev s gl);
+		   let fk =
+		     (fun () -> if !typeclasses_debug then msg_debug (str"backtracked after " ++ Lazy.force pp);
+			aux (succ i) true tl)
+		   in
+		   let sgls =
+		     evars_to_goals
+		       (fun evm ev evi ->
+			  if Typeclasses.is_resolvable evi &&
+			    (not info.only_classes || Typeclasses.is_class_evar evm evi)
+			  then Typeclasses.mark_unresolvable evi, true
+			  else evi, false) s'
+		   in
+		   let newgls, s' =
+		     let gls' = List.map (fun g -> (None, g)) gls in
+		       match sgls with
+		       | None -> gls', s'
+		       | Some (evgls, s') ->
+			 (* Reorder with dependent subgoals. *)
+			 (gls' @ List.map (fun (ev, x) -> Some ev, x) evgls, s')
+		   in
+		   let gls' = List.map_i
+		     (fun j (evar, g) ->
+			let info =
+			  { info with auto_depth = j :: i :: info.auto_depth; auto_last_tac = pp;
+			      is_evar = evar;
+			      hints =
+			      if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
+			      then make_autogoal_hints info.only_classes
+				~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';eff=eff}
+			      else info.hints;
+			      auto_cut = derivs }
+			in g, info) 1 newgls in
+		   let glsv = {it = gls'; sigma = s';eff=eff} in
+		     sk glsv fk)
+	| [] ->
+	  if not foundone && !typeclasses_debug then
+	    msg_debug (pr_depth info.auto_depth ++ str": no match for " ++
+		     Printer.pr_constr_env (Goal.V82.env s gl) concl ++
+		     spc () ++ int (List.length poss) ++ str" possibilities");
+	  fk ()
+    in aux 1 false poss }
+
+let isProp env sigma concl =
+  let ty = Retyping.get_type_of env sigma concl in
+  match kind_of_term ty with
+  | Sort (Prop Null) -> true
+  | _ -> false
+
+let needs_backtrack only_classes env evd oev concl =
+  if Option.is_empty oev || isProp env evd concl then
+    not (Evar.Set.is_empty (Evarutil.evars_of_term concl))
+  else true
+
+let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
+  let rec aux s (acc : autogoal list list) fk = function
+    | (gl,info) :: gls ->
+	(match info.is_evar with
+	 | Some ev when Evd.is_defined s ev -> aux s acc fk gls
+	 | _ ->
+	     second.skft
+	       (fun {it=gls';sigma=s'} fk' ->
+		  let needs_backtrack =
+		    if List.is_empty gls' then
+ 		      needs_backtrack info.only_classes
+		        (Goal.V82.env s gl) s' info.is_evar (Goal.V82.concl s gl)
+		    else true
+		  in
+		  let fk'' =
+		    if not needs_backtrack then
+		      (if !typeclasses_debug then
+			  msg_debug (str"no backtrack on " ++ pr_ev s gl ++
+				     str " after " ++ Lazy.force info.auto_last_tac);
+		       fk)
+		    else fk'
+		  in aux s' (gls'::acc) fk'' gls)
+	       fk {it = (gl,info); sigma = s; eff = Declareops.no_seff })
+    | [] -> Somek2 (List.rev acc, s, fk)
+  in fun {it = gls; sigma = s; eff = eff} fk ->
+    let rec aux' = function
+      | Nonek2 -> fk ()
+      | Somek2 (res, s', fk') ->
+	  let goals' = List.concat res in
+	    sk {it = goals'; sigma = s'; eff = eff } (fun () -> aux' (fk' ()))
+    in aux' (aux s [] (fun () -> Nonek2) gls)
+
+let then_tac (first : atac) (second : atac) : atac =
+  { skft = fun sk fk -> first.skft (then_list second sk) fk }
+
+let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
+  t.skft (fun x _ -> Some x) (fun _ -> None) gl
+
+type run_list_res = auto_result optionk
+
+let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
+  (then_list t (fun x fk -> Somek (x, fk)))
+    gl
+    (fun _ -> Nonek)
+
+let fail_tac : atac =
+  { skft = fun sk fk _ -> fk () }
+
+let rec fix (t : 'a tac) : 'a tac =
+  then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
+
+let rec fix_limit limit (t : 'a tac) : 'a tac =
+  if Int.equal limit 0 then fail_tac
+  else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk }
+
+let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) cut ev g =
+  let hints = make_autogoal_hints only_classes ~st g in
+    (g.it, { hints = hints ; is_evar = ev;
+	     only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (str"none");
+	     auto_path = []; auto_cut = cut })
+
+
+let cut_of_hints h =
+  List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h
+
+let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
+  let cut = cut_of_hints hints in
+  { it = List.map_i (fun i g ->
+    let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'; eff = Declareops.no_seff } in
+      (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; eff = Declareops.no_seff }
+
+let get_result r =
+  match r with
+  | Nonek -> None
+  | Somek (gls, fk) -> Some (gls.sigma,fk)
+
+let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm hints tac =
+  match evars_to_goals p evm with
+  | None -> None (* This happens only because there's no evar having p *)
+  | Some (goals, evm') ->
+      let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st hints goals evm') in
+	match get_result res with
+	| None -> raise Not_found
+	| Some (evm', fk) -> Some (evars_reset_evd ~with_conv_pbs:true evm' evm, fk)
+
+let eauto_tac hints =
+  then_tac normevars_tac (or_tac (hints_tac hints) intro_tac)
+
+let eauto_tac ?limit hints =
+  match limit with
+  | None -> fix (eauto_tac hints)
+  | Some limit -> fix_limit limit (eauto_tac hints)
+
+let eauto ?(only_classes=true) ?st ?limit hints g =
+  let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; eff=g.eff } in
+    match run_tac (eauto_tac ?limit hints) gl with
+    | None -> raise Not_found
+    | Some {it = goals; sigma = s; eff=eff} ->
+	{it = List.map fst goals; sigma = s; eff=eff}
+
+let real_eauto st ?limit hints p evd =
+  let rec aux evd fails =
+    let res, fails =
+      try run_on_evars ~st p evd hints (eauto_tac ?limit hints), fails
+      with Not_found ->
+	List.fold_right (fun fk (res, fails) ->
+	  match res with
+	  | Some r -> res, fk :: fails
+	  | None -> get_result (fk ()), fails)
+	  fails (None, [])
+    in
+      match res with
+      | None -> evd
+      | Some (evd', fk) -> aux evd' (fk :: fails)
+  in aux evd []
+
+let resolve_all_evars_once debug limit p evd =
+  let db = searchtable_map typeclasses_db in
+    real_eauto ?limit (Hint_db.transparent_state db) [db] p evd
+
+(** We compute dependencies via a union-find algorithm.
+    Beware of the imperative effects on the partition structure,
+    it should not be shared, but only used locally. *)
+
+module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
+
+let deps_of_constraints cstrs evm p =
+  List.iter (fun (_, _, x, y) ->
+    let evx = Evarutil.undefined_evars_of_term evm x in
+    let evy = Evarutil.undefined_evars_of_term evm y in
+    Intpart.union_set (Evar.Set.union evx evy) p)
+    cstrs
+
+let evar_dependencies evm p =
+  Evd.fold_undefined
+    (fun ev evi _ ->
+      let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
+      in Intpart.union_set evars 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 (gl,t,sigma) =
+    Goal.V82.mk_goal sigma nc gl Store.empty in
+  let gls = { it = gl ; sigma = sigma; eff= Declareops.no_seff } in (* XXX eff *)
+  let hints = searchtable_map typeclasses_db in
+  let gls' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
+  let evd = sig_sig gls' in
+  let t' = let (ev, inst) = destEvar t in
+    mkEvar (ev, Array.of_list subst)
+  in
+  let term = Evarutil.nf_evar evd t' in
+    evd, term
+
+let _ =
+  Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
+
+(** [split_evars] returns groups of undefined evars according to dependencies *)
+
+let split_evars evm =
+  let p = Intpart.create () in
+  evar_dependencies evm p;
+  deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p;
+  Intpart.partition p
+
+(** [evars_in_comp] filters an [evar_map], keeping only evars
+    that belongs to a certain component *)
+
+let evars_in_comp comp evm =
+  try
+    evars_reset_evd
+      (Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev))
+	 comp Evd.empty) evm
+  with Not_found -> assert false
+
+let is_inference_forced p evd ev =
+  try
+    let evi = Evd.find_undefined evd ev in
+    if Typeclasses.is_resolvable evi && snd (p ev evi)
+    then
+      let (loc, k) = evar_source ev evd in
+      match k with
+	| Evar_kinds.ImplicitArg (_, _, b) -> b
+	| Evar_kinds.QuestionMark _ -> false
+	| _ -> true
+    else true
+  with Not_found -> assert false
+
+let is_mandatory p comp evd =
+  Evar.Set.exists (is_inference_forced p evd) comp
+
+(** In case of unsatisfiable constraints, build a nice error message *)
+
+let error_unresolvable env comp do_split evd =
+  let evd = Evarutil.nf_evar_map_undefined evd in
+  let evm = if do_split then evars_in_comp comp evd else evd in
+  let _, ev = Evd.fold_undefined
+    (fun ev evi (b,acc) ->
+      (* focus on one instance if only one was searched for *)
+      if not (Option.is_empty (class_of_constr evi.evar_concl)) then
+	if not b (* || do_split *) then
+	  true, Some ev
+	else b, None
+      else b, acc) evm (false, None)
+  in
+  Typeclasses_errors.unsatisfiable_constraints
+    (Evarutil.nf_env_evar evm env) evm ev
+
+(** Check if an evar is concerned by the current resolution attempt,
+    (and in particular is in the current component), and also update
+    its evar_info.
+    Invariant : this should only be applied to undefined evars,
+    and return undefined evar_info *)
+
+let select_and_update_evars p oevd in_comp evd ev evi =
+  assert (evi.evar_body == Evar_empty);
+  try
+    let oevi = Evd.find_undefined oevd ev in
+    if Typeclasses.is_resolvable oevi then
+      Typeclasses.mark_unresolvable evi,
+      (in_comp ev && p evd ev evi)
+    else evi, false
+  with Not_found ->
+    Typeclasses.mark_unresolvable evi, p evd ev evi
+
+(** Do we still have unresolved evars that should be resolved ? *)
+
+let has_undefined p oevd evd =
+  let check ev evi = snd (p oevd ev evi) in
+  Evar.Map.exists check (Evd.undefined_map evd)
+
+(** Revert the resolvability status of evars after resolution,
+    potentially unprotecting some evars that were set unresolvable
+    just for this call to resolution. *)
+
+let revert_resolvability oevd evd =
+  let map ev evi =
+    try
+      if not (Typeclasses.is_resolvable evi) then
+        let evi' = Evd.find_undefined oevd ev in
+        if Typeclasses.is_resolvable evi' then
+          Typeclasses.mark_resolvable evi
+        else evi
+      else evi
+    with Not_found -> evi
+  in
+  Evd.raw_map_undefined map evd
+
+(** If [do_split] is [true], we try to separate the problem in
+    several components and then solve them separately *)
+
+exception Unresolved
+
+let resolve_all_evars debug m env p oevd do_split fail =
+  let split = if do_split then split_evars oevd else [Evar.Set.empty] in
+  let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
+  in
+  let rec docomp evd = function
+    | [] -> revert_resolvability oevd evd
+    | comp :: comps ->
+      let p = select_and_update_evars p oevd (in_comp comp) in
+      try
+	 let evd' = resolve_all_evars_once debug m p evd in
+	 if has_undefined p oevd evd' then raise Unresolved;
+	 docomp evd' comps
+      with Unresolved | Not_found ->
+	if fail && (not do_split || is_mandatory (p evd) comp evd)
+	then (* Unable to satisfy the constraints. *)
+	  error_unresolvable env comp do_split evd
+	else (* Best effort: do nothing on this component *)
+	  docomp evd comps
+  in docomp oevd split
+
+let initial_select_evars filter =
+  fun evd ev evi ->
+    filter ev (snd evi.Evd.evar_source) &&
+    Typeclasses.is_class_evar evd evi
+
+let resolve_typeclass_evars debug m env evd filter split fail =
+  let evd =
+    try Evarconv.consider_remaining_unif_problems
+      ~ts:(Typeclasses.classes_transparent_state ()) env evd
+    with e when Errors.noncritical e -> evd
+  in
+    resolve_all_evars debug m env (initial_select_evars filter) evd split fail
+
+let solve_inst debug depth env evd filter split fail =
+  resolve_typeclass_evars debug depth env evd filter split fail
+
+let _ =
+  Typeclasses.solve_instanciations_problem :=
+    solve_inst false !typeclasses_depth
+
+let set_typeclasses_debug d = (:=) typeclasses_debug d;
+  Typeclasses.solve_instanciations_problem := solve_inst d !typeclasses_depth
+
+let get_typeclasses_debug () = !typeclasses_debug
+
+let set_typeclasses_depth d = (:=) typeclasses_depth d;
+  Typeclasses.solve_instanciations_problem := solve_inst !typeclasses_debug !typeclasses_depth
+
+let get_typeclasses_depth () = !typeclasses_depth
+
+open Goptions
+
+let set_typeclasses_debug =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "debug output for typeclasses proof search";
+      optkey   = ["Typeclasses";"Debug"];
+      optread  = get_typeclasses_debug;
+      optwrite = set_typeclasses_debug; }
+
+let set_typeclasses_depth =
+  declare_int_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "depth for typeclasses proof search";
+      optkey   = ["Typeclasses";"Depth"];
+      optread  = get_typeclasses_depth;
+      optwrite = set_typeclasses_depth; }
+
+let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
+  try
+    let dbs = List.map_filter
+      (fun db -> try Some (Auto.searchtable_map db)
+        with e when Errors.noncritical e -> None)
+      dbs
+    in
+    let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+      eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
+   with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
+
+let _ = Classes.refine_ref := Refine.refine
+
+(** Take the head of the arity of a constr.
+    Used in the partial application tactic. *)
+
+let rec head_of_constr t =
+  let t = strip_outer_cast(collapse_appl t) in
+    match kind_of_term t with
+    | Prod (_,_,c2)  -> head_of_constr c2
+    | LetIn (_,_,_,c2) -> head_of_constr c2
+    | App (f,args)  -> head_of_constr f
+    | _      -> t
+
+let head_of_constr h c =
+  let c = head_of_constr c in
+  letin_tac None (Name h) c None Locusops.allHyps
+
+let not_evar c = match kind_of_term c with
+| Evar _ -> tclFAIL 0 (str"Evar")
+| _ -> tclIDTAC
+
+let is_ground c gl =
+  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
+  else tclFAIL 0 (str"Not ground") gl
+
+let autoapply c i gl =
+  let flags = flags_of_state (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
+  let cty = pf_type_of gl c in
+  let ce = mk_clenv_from gl (c,cty) in
+  unify_e_resolve flags (c,ce) gl