From cf7d42d1c64e8a8a1c1400f5264c7d9f96757669 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 4 Oct 2013 19:06:02 +0000 Subject: 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 --- tactics/class_tactics.ml | 761 ++++++++++++++++++++++++++++++++++++++++++ tactics/class_tactics.ml4 | 829 ---------------------------------------------- tactics/class_tactics.mli | 32 ++ tactics/g_class.ml4 | 84 +++++ tactics/hightactics.mllib | 1 + 5 files changed, 878 insertions(+), 829 deletions(-) create mode 100644 tactics/class_tactics.ml delete mode 100644 tactics/class_tactics.ml4 create mode 100644 tactics/class_tactics.mli create mode 100644 tactics/g_class.ml4 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 *) +(* + 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 diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 deleted file mode 100644 index 40834be365..0000000000 --- a/tactics/class_tactics.ml4 +++ /dev/null @@ -1,829 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - 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 - -TACTIC EXTEND progress_evars - [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.eval_tactic t) ] -END - -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 - - -(** Options: depth, debug and transparency settings. *) - -open Goptions - -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_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 d = (:=) typeclasses_depth d; - Typeclasses.solve_instanciations_problem := solve_inst !typeclasses_debug !typeclasses_depth - -let get_typeclasses_depth () = !typeclasses_depth - -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 set_transparency cl b = - List.iter (fun r -> - let gr = Smartlocate.global_with_alias r in - let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in - Classes.set_typeclass_transparency ev false b) cl - -VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ - set_transparency cl true ] -END - -VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [ - set_transparency cl false ] -END - -open Genarg - -let pr_debug _prc _prlc _prt b = - if b then Pp.str "debug" else Pp.mt() - -ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug -| [ "debug" ] -> [ true ] -| [ ] -> [ false ] -END - -let pr_depth _prc _prlc _prt = function - Some i -> Pp.int i - | None -> Pp.mt() - -ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth -| [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ] -END - -(* true = All transparent, false = Opaque if possible *) - -VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [ - set_typeclasses_debug d; - set_typeclasses_depth depth - ] -END - -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 - -TACTIC EXTEND typeclasses_eauto -| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ] -| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto ~only_classes:true [typeclasses_db] ] -END - -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 - -TACTIC EXTEND head_of_constr - [ "head_of_constr" ident(h) constr(c) ] -> [ - let c = head_of_constr c in - letin_tac None (Name h) c None Locusops.allHyps - ] -END - -TACTIC EXTEND not_evar - [ "not_evar" constr(ty) ] -> [ - match kind_of_term ty with - | Evar _ -> tclFAIL 0 (str"Evar") - | _ -> tclIDTAC ] -END - -TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ fun gl -> - if Evarutil.is_ground_term (project gl) ty then tclIDTAC gl - else tclFAIL 0 (str"Not ground") gl ] -END - -TACTIC EXTEND autoapply - [ "autoapply" constr(c) "using" preident(i) ] -> [ fun 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 ] -END diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli new file mode 100644 index 0000000000..0b74027c31 --- /dev/null +++ b/tactics/class_tactics.mli @@ -0,0 +1,32 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool + +val set_typeclasses_debug : bool -> unit +val get_typeclasses_debug : unit -> bool + +val set_typeclasses_depth : int option -> unit +val get_typeclasses_depth : unit -> int option + +val progress_evars : tactic -> tactic + +val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> + Auto.hint_db_name list -> tactic + +val head_of_constr : Id.t -> Term.constr -> tactic + +val not_evar : constr -> tactic + +val is_ground : constr -> tactic + +val autoapply : constr -> Auto.hint_db_name -> tactic diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 new file mode 100644 index 0000000000..970f635b73 --- /dev/null +++ b/tactics/g_class.ml4 @@ -0,0 +1,84 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [ progress_evars (Tacinterp.eval_tactic t) ] +END + +(** Options: depth, debug and transparency settings. *) + +open Goptions + +let set_transparency cl b = + List.iter (fun r -> + let gr = Smartlocate.global_with_alias r in + let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in + Classes.set_typeclass_transparency ev false b) cl + +VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF +| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ + set_transparency cl true ] +END + +VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF +| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [ + set_transparency cl false ] +END + +open Genarg + +let pr_debug _prc _prlc _prt b = + if b then Pp.str "debug" else Pp.mt() + +ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug +| [ "debug" ] -> [ true ] +| [ ] -> [ false ] +END + +let pr_depth _prc _prlc _prt = function + Some i -> Pp.int i + | None -> Pp.mt() + +ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth +| [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ] +END + +(* true = All transparent, false = Opaque if possible *) + +VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF + | [ "Typeclasses" "eauto" ":=" debug(d) depth(depth) ] -> [ + set_typeclasses_debug d; + set_typeclasses_depth depth + ] +END + +TACTIC EXTEND typeclasses_eauto +| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ] +| [ "typeclasses" "eauto" ] -> [ typeclasses_eauto ~only_classes:true [Auto.typeclasses_db] ] +END + +TACTIC EXTEND head_of_constr + [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ] +END + +TACTIC EXTEND not_evar + [ "not_evar" constr(ty) ] -> [ not_evar ty ] +END + +TACTIC EXTEND is_ground + [ "is_ground" constr(ty) ] -> [ is_ground ty ] +END + +TACTIC EXTEND autoapply + [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ] +END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 25d630b674..0d6322af61 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -2,6 +2,7 @@ Extraargs Extratactics Eauto Class_tactics +G_class Rewrite G_rewrite Tauto -- cgit v1.2.3