diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-06-09 21:48:30 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
commit | 4b29ca791bdfc810feabb883dc3d96a4ebd130a1 (patch) | |
tree | 0e0825576f6e02fd3d997ee4374dca5cd934226d /tactics | |
parent | 6876a3cd9dd1d7c94f9d387904c6a6f6d88c31f8 (diff) |
Purely refactoring and code/API cleanup.
Fix test-suite files
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/class_tactics.ml | 1646 | ||||
-rw-r--r-- | tactics/class_tactics.mli | 41 |
2 files changed, 843 insertions, 844 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 61a8956e0..0ddb97dbb 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* TODO: +(* TODO: - Find an interface allowing eauto to backtrack when shelved goals remain, - e.g. to force instantiations. + e.g. to force instantiations. - unique solutions *) @@ -34,6 +34,8 @@ open Hints (** Hint database named "typeclass_instances", now created directly in Auto *) +(** Options handling *) + let typeclasses_debug = ref 0 let typeclasses_depth = ref None @@ -69,7 +71,7 @@ let set_typeclasses_unif_compat_string d = set_typeclasses_unif_compat (get_compat_version d) let get_typeclasses_unif_compat_string () = Flags.pr_version (get_typeclasses_unif_compat ()) - + let typeclasses_compat = ref Flags.Current let set_typeclasses_compat d = (:=) typeclasses_compat d let get_typeclasses_compat () = !typeclasses_compat @@ -92,7 +94,7 @@ let set_typeclasses_depth d = (:=) typeclasses_depth d let get_typeclasses_depth () = !typeclasses_depth open Goptions - + let _ = declare_bool_option { optsync = true; @@ -111,7 +113,7 @@ let _ = optkey = ["Typeclasses";"Limit";"Intros"]; optread = get_typeclasses_limit_intros; optwrite = set_typeclasses_limit_intros; } - + let _ = declare_bool_option { optsync = true; @@ -184,44 +186,13 @@ let set_typeclasses_depth = optread = get_typeclasses_depth; optwrite = set_typeclasses_depth; } -let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) - -(** We transform the evars that are concerned by this resolution - (according to predicate p) into goals. - Invariant: function p only manipulates and returns undefined evars *) - -let top_sort evm undefs = - let l' = ref [] in - let tosee = ref undefs in - let rec visit ev evi = - let evs = Evarutil.undefined_evars_of_evar_info evm evi in - Evar.Set.iter (fun ev -> - if Evar.Map.mem ev !tosee then - visit ev (Evar.Map.find ev !tosee)) evs; - tosee := Evar.Map.remove ev !tosee; - l' := ev :: !l'; - in - while not (Evar.Map.is_empty !tosee) do - let ev, evi = Evar.Map.min_binding !tosee in - visit ev evi - done; - List.rev !l' - -let evars_to_goals p evm = - let goals = ref Evar.Map.empty in - let map ev evi = - let evi, goal = p evm ev evi in - let () = if goal then goals := Evar.Map.add ev evi !goals in - evi - in - let evm = Evd.raw_map_undefined map evm in - if Evar.Map.is_empty !goals then None - else Some (!goals, evm) +let pr_ev evs ev = + Printer.pr_constr_env (Goal.V82.env evs ev) evs + (Evarutil.nf_evar evs (Goal.V82.concl evs ev)) (** Typeclasses instance search tactic / eauto *) open Auto - open Unification let auto_core_unif_flags st freeze = { @@ -239,7 +210,7 @@ let auto_core_unif_flags st freeze = { modulo_eta = !typeclasses_modulo_eta; } -let auto_unif_flags freeze st = +let auto_unif_flags freeze st = let fl = auto_core_unif_flags st freeze in { core_unify_flags = fl; merge_unify_flags = fl; @@ -248,25 +219,6 @@ let auto_unif_flags freeze st = resolve_evars = false } -(* TODO: move, exported tactic in g_class *) -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 = - Proofview.Goal.nf_enter { enter = begin fun gl -> - let concl = Proofview.Goal.concl gl in - let check = - Proofview.Goal.nf_enter { enter = begin fun gl' -> - let newconcl = Proofview.Goal.concl gl' in - if eq_constr_mod_evars concl newconcl - then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)") - else Proofview.tclUNIT () - end } - in t <*> check - end } - let e_give_exact flags poly (c,clenv) gl = let (c, _, _) = c in let c, gl = @@ -274,7 +226,7 @@ let e_give_exact flags poly (c,clenv) gl = let clenv', subst = Clenv.refresh_undefined_univs clenv in let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in let c = Vars.subst_univs_level_constr subst c in - c, {gl with sigma = evd} + c, {gl with sigma = evd} else c, gl in let t1 = pf_unsafe_type_of gl c in @@ -292,17 +244,15 @@ let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> Clenvtac.clenv_refine false ~with_classes:false clenv' end } -exception ReachedLimitEx -exception NotApplicableEx - -let unify_resolve_newcl poly flags = - let open Clenv in +(** Application of a lemma using [refine] instead of the old [w_unify] *) +let unify_resolve_refine poly flags = + let open Clenv in { enter = begin fun gls ((c, t, ctx),n,clenv) -> let env = Proofview.Goal.env gls in let concl = Proofview.Goal.concl gls in Refine.refine ~unsafe:true { Sigma.run = fun sigma -> let sigma = Sigma.to_evar_map sigma in - let sigma, term, ty = + let sigma, term, ty = if poly then let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in @@ -319,13 +269,15 @@ let unify_resolve_newcl poly flags = if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta evdref cl.cl_concl concl) then Type_errors.error_actual_type env - {Environ.uj_val = term; Environ.uj_type = cl.cl_concl} - concl; + {Environ.uj_val = term; Environ.uj_type = cl.cl_concl} + concl; !evdref in Sigma.here term (Sigma.Unsafe.of_evar_map sigma') } end } - +(** Dealing with goals of the form A -> B and hints of the form + C -> A -> B. In the +*) let clenv_of_prods poly nprods (c, clenv) gl = let (c, _, _) = c in if poly || Int.equal nprods 0 then Some (None, clenv) @@ -335,7 +287,7 @@ let clenv_of_prods poly nprods (c, clenv) gl = let diff = nb_prod ty - nprods in if Pervasives.(>=) diff 0 then (* Was Some clenv... *) - Some (Some diff, + Some (Some diff, Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl) else None @@ -349,7 +301,7 @@ let with_prods nprods poly (c, clenv) f = { enter = begin fun gl -> if Int.equal nprods 0 then f.enter gl (c, None, clenv) else Tacticals.New.tclZEROMSG (str"Not enough premisses") end } - + let matches_pattern concl pat = let matches env sigma = match pat with @@ -357,8 +309,8 @@ let matches_pattern concl pat = | Some pat -> let sigma = Sigma.to_evar_map sigma in if Constr_matching.is_matching env sigma pat concl then - Proofview.tclUNIT () - else + Proofview.tclUNIT () + else Tacticals.New.tclZEROMSG (str "conclPattern") in Proofview.Goal.enter { enter = fun gl -> @@ -375,7 +327,7 @@ let matches_pattern concl pat = in independent goals or the conclusion are turned into subgoals iff they are of typeclass kind. - The remaining dependent evars not of typeclass type are shelved, - and resolution must fill them for it to succeed, otherwise we + and resolution must fill them for it to succeed, otherwise we backtrack. *) @@ -390,14 +342,13 @@ let shelve_dependencies gls = (if !typeclasses_debug > 1 then Feedback.msg_debug (str" shelving goals: " ++ pr_gls sigma gls); shelve_goals gls) - -(** Hack to properly solve dependent evars that are typeclasses *) +(** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db only_classes db_list local_db = let open Tacticals.New in let open Tacmach.New in let trivial_fail = - Proofview.Goal.nf_enter { enter = + Proofview.Goal.nf_enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -408,13 +359,13 @@ let rec e_trivial_fail_db only_classes db_list local_db = end } in let trivial_resolve = - Proofview.Goal.nf_enter { enter = + Proofview.Goal.nf_enter { enter = begin fun gl -> let tacs = e_trivial_resolve db_list local_db only_classes (project gl) (pf_concl gl) in tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) - end} - in + end} + in let tacl = Eauto.registered_e_assumption :: (tclTHEN Tactics.intro trivial_fail :: [trivial_resolve]) @@ -425,24 +376,24 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = let open Proofview.Notations in let prods, concl = decompose_prod_assum concl in let nprods = List.length prods in - let freeze = + let freeze = try let cl = Typeclasses.class_info (fst hdc) in - if cl.cl_strict then - Evd.evars_of_term concl - else Evar.Set.empty + if cl.cl_strict then + Evd.evars_of_term concl + else Evar.Set.empty with e when Errors.noncritical e -> Evar.Set.empty in let hintl = List.map_append (fun db -> - let tacs = - if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto hdc concl db - else Hint_db.map_existential hdc concl db - in - let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in - List.map (fun x -> (flags, x)) tacs) + let tacs = + if Hint_db.use_dn db then (* Using dnet *) + Hint_db.map_eauto hdc concl db + else Hint_db.map_existential hdc concl db + in + let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in + List.map (fun x -> (flags, x)) tacs) (local_db::db_list) in let tac_of_hint = @@ -454,7 +405,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = with_prods nprods poly (term,cl) ({ enter = fun gl clenv -> (matches_pattern concl p) <*> - ((unify_resolve_newcl poly flags).enter gl clenv)}) + ((unify_resolve_refine poly flags).enter gl clenv)}) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = @@ -469,14 +420,14 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = let tac = (with_prods nprods poly (term,cl) ({ enter = fun gl clenv -> (matches_pattern concl p) <*> - ((unify_resolve_newcl poly flags).enter gl clenv)})) in + ((unify_resolve_refine poly flags).enter gl clenv)})) in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable else let tac = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in if get_typeclasses_compat () = Flags.V8_5 then Tacticals.New.tclTHEN tac Proofview.shelve_unifiable - else + else Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c) @@ -498,9 +449,9 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl = str " with pattern " ++ Printer.pr_constr_pattern pat | _ -> mt () in - match repr_hint t with - | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp)) - | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp)) + match repr_hint t with + | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp)) + | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp)) in List.map tac_of_hint hintl and e_trivial_resolve db_list local_db only_classes sigma concl = @@ -515,37 +466,62 @@ let e_possible_resolve db_list local_db only_classes sigma concl = (decompose_app_bound concl) false only_classes sigma concl with Bound | Not_found -> [] +let cut_of_hints h = + List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h + let catchable = function | Refiner.FailError _ -> true | e -> Logic.catchable_exception e let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l) -type autoinfo = { hints : hint_db; is_evar: existential_key option; - only_classes: bool; unique : 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 failure = NotApplicable | ReachedLimit -type 'ans fk = failure -> '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 +let is_Prop env sigma concl = + let ty = Retyping.get_type_of env sigma concl in + match kind_of_term ty with + | Sort (Prop Null) -> true + | _ -> false -type atac = auto_result tac +let is_unique env concl = + try + let (cl,u), args = dest_class_app env concl in + cl.cl_unique + with e when Errors.noncritical e -> false -(* Some utility types to avoid the need of -rectypes *) +(** Sort the undefined variables from the least-dependent to most dependent. *) +let top_sort evm undefs = + let l' = ref [] in + let tosee = ref undefs in + let rec visit ev evi = + let evs = Evarutil.undefined_evars_of_evar_info evm evi in + Evar.Set.iter (fun ev -> + if Evar.Map.mem ev !tosee then + visit ev (Evar.Map.find ev !tosee)) evs; + tosee := Evar.Map.remove ev !tosee; + l' := ev :: !l'; + in + while not (Evar.Map.is_empty !tosee) do + let ev, evi = Evar.Map.min_binding !tosee in + visit ev evi + done; + List.rev !l' -type 'a optionk = - | Nonek - | Somek of 'a * 'a optionk fk +(** We transform the evars that are concerned by this resolution + (according to predicate p) into goals. + Invariant: function p only manipulates and returns undefined evars +*) -type ('a,'b) optionk2 = - | Nonek2 of failure - | Somek2 of 'a * 'b * ('a,'b) optionk2 fk +let evars_to_goals p evm = + let goals = ref Evar.Map.empty in + let map ev evi = + let evi, goal = p evm ev evi in + let () = if goal then goals := Evar.Map.add ev evi !goals in + evi + in + let evm = Evd.raw_map_undefined map evm in + if Evar.Map.is_empty !goals then None + else Some (!goals, evm) +(** Making local hints *) let make_resolve_hyp env sigma st flags only_classes pri decl = let open Context.Named.Declaration in let id = get_id decl in @@ -556,10 +532,10 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = | 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 (Term.eq_constr ty' ar) then iscl env' ty' - else false + let env' = Environ.push_rel_context ctx env in + let ty' = whd_betadeltaiota env' ar in + if not (Term.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 @@ -567,674 +543,728 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = 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 false - (IsConstr (c,Univ.ContextSet.empty))) - hints) - else [] + 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 false + (IsConstr (c,Univ.ContextSet.empty))) + hints) + else [] in (hints @ List.map_filter - (fun f -> try Some (f (c, cty, Univ.ContextSet.empty)) - with Failure _ | UserError _ -> None) - [make_exact_entry ~name env sigma pri false; - make_apply_entry ~name env sigma flags pri false]) + (fun f -> try Some (f (c, cty, Univ.ContextSet.empty)) + with Failure _ | UserError _ -> None) + [make_exact_entry ~name env sigma pri false; + make_apply_entry ~name env sigma flags pri false]) 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 = + let hintlist = List.fold_left - (fun (paths, hints) hyp -> - let consider = - let open Context.Named.Declaration in - try let t = Global.lookup_named (get_id hyp) |> get_type in - (* Section variable, reindex only if the type changed *) - not (Term.eq_constr t (get_type hyp)) - with Not_found -> true - in - if consider then - let path, hint = - PathEmpty, pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp - in - (PathOr (paths, path), hint @ hints) - else (paths, hints)) - (PathEmpty, []) sign + (fun hints hyp -> + let consider = + let open Context.Named.Declaration in + try let t = Global.lookup_named (get_id hyp) |> get_type in + (* Section variable, reindex only if the type changed *) + not (Term.eq_constr t (get_type hyp)) + with Not_found -> true + in + if consider then + let hint = + pf_apply make_resolve_hyp g st (true,false,false) only_classes None hyp + in hint @ hints + else hints) + ([]) sign in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) -let make_autogoal_hints = - let cache = ref (true, Environ.empty_named_context_val, - Hint_db.empty full_transparent_state true) - in - fun only_classes ?(st=full_transparent_state) g -> - let sign = pf_filtered_hyps g in - let (onlyc, sign', cached_hints) = !cache in - if onlyc == only_classes && - (sign == sign' || Environ.eq_named_context_val sign sign') - && Hint_db.transparent_state cached_hints == st - then - cached_hints - else - let hints = make_hints g st only_classes (Environ.named_context_of_val sign) - in - cache := (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;} -> - let res = try Some (tac {it=gl; sigma=s;}) - with e when catchable e -> None in - match res with - | Some gls -> sk (f gls hints) fk - | None -> fk NotApplicable } - -let intro_tac : atac = - lift_tactic (Proofview.V82.of_tactic Tactics.intro) - (fun {it = gls; sigma = s} 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 env s hint info.hints in - (g', { info with is_evar = None; hints = ldb; - auto_last_tac = lazy (str"intro") })) gls - in {it = gls'; sigma = s;}) - -let normevars_tac : atac = - { skft = fun sk fk {it = (gl, info); sigma = s;} -> - 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';} fk } - -let merge_failures x y = - match x, y with - | _, ReachedLimit - | ReachedLimit, _ -> ReachedLimit - | NotApplicable, NotApplicable -> NotApplicable - -let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft sk - (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls } - -let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft sk - (fun f -> (y f).skft sk fk gls) gls } +(** <= 8.5 resolution *) +module V85 = struct -let is_Prop env sigma concl = - let ty = Retyping.get_type_of env sigma concl in - match kind_of_term ty with - | Sort (Prop Null) -> true - | _ -> false + type autoinfo = { hints : hint_db; is_evar: existential_key option; + only_classes: bool; unique : 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 failure = NotApplicable | ReachedLimit + type 'ans fk = failure -> 'ans + type ('a,'ans) sk = 'a -> 'ans fk -> 'ans + type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans } -let is_unique env concl = - try - let (cl,u), args = dest_class_app env concl in - cl.cl_unique - with e when Errors.noncritical e -> false + type auto_result = autogoal list sigma -let needs_backtrack env evd oev concl = - if Option.is_empty oev || is_Prop env evd concl then - occur_existential concl - else true + type atac = auto_result tac -type newautoinfo = - { search_depth : int list; - last_tac : Pp.std_ppcmds Lazy.t; - search_dep : bool; - search_cut : hints_path; - search_hints : hint_db; } + (* Some utility types to avoid the need of -rectypes *) -let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty, - Hint_db.empty full_transparent_state true) + type 'a optionk = + | Nonek + | Somek of 'a * 'a optionk fk -let make_autogoal_hints' only_classes ?(st=full_transparent_state) g = - let open Proofview in - let open Tacmach.New in - let sign = Goal.hyps g in - let (dir, onlyc, sign', cached_hints) = !autogoal_cache in - let cwd = Lib.cwd () in - if DirPath.equal cwd dir && - (onlyc == only_classes) && - Context.Named.equal sign sign' && - Hint_db.transparent_state cached_hints == st - then cached_hints - else - let hints = make_hints {it = Goal.goal g; sigma = project g} - st only_classes sign + type ('a,'b) optionk2 = + | Nonek2 of failure + | Somek2 of 'a * 'b * ('a,'b) optionk2 fk + + let pf_filtered_hyps gls = + Goal.V82.hyps gls.Evd.sigma (sig_it gls) + + let make_autogoal_hints = + let cache = ref (true, Environ.empty_named_context_val, + Hint_db.empty full_transparent_state true) in - autogoal_cache := (cwd, only_classes, sign, hints); hints - -let make_autogoal' ?(st=full_transparent_state) only_classes dep cut i g = - let hints = make_autogoal_hints' only_classes ~st g in - let info = { search_hints = hints; - search_depth = [i]; last_tac = lazy (str"none"); - search_dep = dep; - search_cut = cut } in - info - -let needs_backtrack' env evd unique concl = - if unique || is_Prop env evd concl then - occur_existential concl - else true - -let merge_exceptions e e' = - match fst e, fst e' with - | ReachedLimitEx, _ -> e - | _, ReachedLimitEx -> e' - | _, _ -> e - -let new_hints_tac_gl only_classes hints info kont gl - : unit Proofview.tactic - = - let open Proofview in - let open Proofview.Notations in - let env = Goal.env gl in - let concl = Goal.concl gl in - let sigma = Goal.sigma gl in - let s = Sigma.to_evar_map sigma in - let unique = not info.search_dep || is_unique env concl in - let backtrack = needs_backtrack' env s unique concl in - if !typeclasses_debug > 0 then - Feedback.msg_debug - (pr_depth info.search_depth ++ str": looking for " ++ - Printer.pr_constr_env (Goal.env gl) s concl ++ - (if backtrack then str" with backtracking" - else str" without backtracking")); - let poss = e_possible_resolve hints info.search_hints only_classes s concl in - (* If no goal depends on the solution of this one or the - instances are irrelevant/assumed to be unique, then - we don't need to backtrack, as long as no evar appears in the goal - This is an overapproximation. Evars could appear in this goal only - and not any other *) - let ortac = if backtrack then Proofview.tclOR else Proofview.tclORELSE in - let idx = ref 1 in - let foundone = ref false in - let rec aux e = function - | (tac, pat, b, name, pp) :: tl -> - let derivs = path_derivate info.search_cut name in - (if !typeclasses_debug > 1 then - Feedback.msg_debug - (pr_depth (!idx :: info.search_depth) ++ str": trying " ++ - Lazy.force pp ++ - (if !foundone != true then - str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl) - else mt ()))); - let tac_of gls i j = Goal.nf_enter { enter = fun gl' -> - let sigma' = Goal.sigma gl' in - let s' = Sigma.to_evar_map sigma' in - let _concl = Goal.concl gl' in - if !typeclasses_debug > 0 then - Feedback.msg_debug - (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ - pr_ev s' (Proofview.Goal.goal gl')); - let hints' = - if b && not (Context.Named.equal (Goal.hyps gl') (Goal.hyps gl)) - then - let st = Hint_db.transparent_state info.search_hints in - make_autogoal_hints' only_classes ~st gl' - else info.search_hints - in - let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal gl') gls in - let info' = - { search_depth = succ j :: i :: info.search_depth; - last_tac = pp; - search_dep = dep'; - search_hints = hints'; - search_cut = derivs } - in - kont info' } - in - let rec result (shelf, ()) i k = - foundone := true; - Proofview.Unsafe.tclGETGOALS >>= fun gls -> - let j = List.length gls in - (if !typeclasses_debug > 0 then - Feedback.msg_debug - (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl) - ++ str", " ++ int j ++ str" subgoal(s)" ++ - (Option.cata (fun k -> str " in addition to the first " ++ int k) - (mt()) k))); + fun only_classes ?(st=full_transparent_state) g -> + let sign = pf_filtered_hyps g in + let (onlyc, sign', cached_hints) = !cache in + if onlyc == only_classes && + (sign == sign' || Environ.eq_named_context_val sign sign') + && Hint_db.transparent_state cached_hints == st + then + cached_hints + else + let hints = make_hints g st only_classes (Environ.named_context_of_val sign) + in + cache := (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;} -> + let res = try Some (tac {it=gl; sigma=s;}) + with e when catchable e -> None in + match res with + | Some gls -> sk (f gls hints) fk + | None -> fk NotApplicable } + + let intro_tac : atac = + let tac {it = gls; sigma = s} 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 env s hint info.hints in + (g', { info with is_evar = None; hints = ldb; + auto_last_tac = lazy (str"intro") })) gls + in {it = gls'; sigma = s;} + in + lift_tactic (Proofview.V82.of_tactic Tactics.intro) tac + + let normevars_tac : atac = + { skft = fun sk fk {it = (gl, info); sigma = s;} -> + 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';} fk } + + let merge_failures x y = + match x, y with + | _, ReachedLimit + | ReachedLimit, _ -> ReachedLimit + | NotApplicable, NotApplicable -> NotApplicable + + let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = + { skft = fun sk fk gls -> x.skft sk + (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls } + + let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac = + { skft = fun sk fk gls -> x.skft sk + (fun f -> (y f).skft sk fk gls) gls } + + let needs_backtrack env evd oev concl = + if Option.is_empty oev || is_Prop env evd concl then + occur_existential concl + else true + + let hints_tac hints sk fk {it = gl,info; sigma = s} = + let env = Goal.V82.env s gl in + let concl = Goal.V82.concl s gl in + let tacgl = {it = gl; sigma = s;} in + let poss = e_possible_resolve hints info.hints info.only_classes s concl in + let unique = is_unique env concl in + let rec aux i foundone = function + | (tac, _, b, name, pp) :: tl -> + let derivs = path_derivate info.auto_cut name in let res = - if j = 0 then tclUNIT () - else tclDISPATCH (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) + try + if path_matches derivs [] then None + else Some (Proofview.V82.of_tactic tac tacgl) + with e when catchable e -> None in - let finish = - tclEVARMAP >>= fun sigma -> - let filter ev = - try - let evi = Evd.find_undefined sigma ev in - if only_classes then - Some (ev, is_class_type sigma (Evd.evar_concl evi)) - else Some (ev, true) - with Not_found -> None - in - let remaining = CList.map_filter filter shelf in - if !typeclasses_debug > 1 then - Feedback.msg_debug - (pr_depth (i :: info.search_depth) ++ - str": after " ++ Lazy.force pp ++ str" finished, " ++ - int (List.length remaining) ++ - str " goals are shelved and unsolved ( " ++ - prlist_with_sep spc - (fun ev -> int (Evar.repr ev) ++ spc () ++ - pr_ev sigma ev) (List.map fst remaining) ++ str")"); - begin - (* Some existentials produced by the original tactic were not solved - in the subgoals, turn them into subgoals now. *) - let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in - let shelved = List.map fst shelved and goals = List.map fst goals in - if !typeclasses_debug > 1 then - Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ - prlist_with_sep spc (pr_ev sigma) goals); - shelve_goals shelved <*> - (if List.is_empty goals then tclUNIT () - else with_shelf (Unsafe.tclNEWGOALS goals) >>= - fun s -> result s i (Some (Option.default 0 k + j))) - end - in res <*> finish + (match res with + | None -> aux i foundone tl + | Some {it = gls; sigma = s';} -> + if !typeclasses_debug > 0 then + Feedback.msg_debug + (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp + ++ str" on" ++ spc () ++ pr_ev s gl); + let sgls = + evars_to_goals + (fun evm ev evi -> + if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) && + (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') -> + if not !typeclasses_dependency_order then + (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s') + else + (* Reorder with dependent subgoals. *) + let evm = List.fold_left + (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in + let gls = top_sort s' evm in + (List.map (fun ev -> Some ev, ev) gls, 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';} + else info.hints; + auto_cut = derivs } + in g, info) 1 newgls in + let glsv = {it = gls'; sigma = s';} in + let fk' = + (fun e -> + let do_backtrack = + if unique then occur_existential concl + else if info.unique then true + else if List.is_empty gls' then + needs_backtrack env s' info.is_evar concl + else true + in + let e' = match foundone with None -> e + | Some e' -> merge_failures e e' in + if !typeclasses_debug > 0 then + Feedback.msg_debug + ((if do_backtrack then str"Backtracking after " + else str "Not backtracking after ") + ++ Lazy.force pp); + if do_backtrack then aux (succ i) (Some e') tl + else fk e') + in + sk glsv fk') + | [] -> + if foundone == None && !typeclasses_debug > 0 then + Feedback.msg_debug + (pr_depth info.auto_depth ++ str": no match for " ++ + Printer.pr_constr_env (Goal.V82.env s gl) s concl ++ + spc () ++ str ", " ++ int (List.length poss) ++ + str" possibilities"); + match foundone with + | Some e -> fk e + | None -> fk NotApplicable + in aux 1 None poss + + let hints_tac hints = + { skft = fun sk fk gls -> hints_tac hints sk fk gls } + + 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 -> + Control.check_for_interrupt (); + (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 fk'' = + if not info.unique && List.is_empty gls' && + not (needs_backtrack (Goal.V82.env s gl) s + info.is_evar (Goal.V82.concl s gl)) + then fk + else fk' + in + aux s' (gls'::acc) fk'' gls) + fk {it = (gl,info); sigma = s; }) + | [] -> Somek2 (List.rev acc, s, fk) + in fun {it = gls; sigma = s; } fk -> + let rec aux' = function + | Nonek2 e -> fk e + | Somek2 (res, s', fk') -> + let goals' = List.concat res in + sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e)) + in aux' (aux s [] (fun e -> Nonek2 e) 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 reason : atac = + { skft = fun sk fk _ -> fk reason } + + 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 ReachedLimit + else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } + + let fix_iterative t = + let rec aux depth = + or_else_tac (fix_limit depth t) + (function + | NotApplicable as e -> fail_tac e + | ReachedLimit -> aux (succ depth)) + in aux 1 + + let fix_iterative_limit limit (t : 'a tac) : 'a tac = + let rec aux depth = + if Int.equal limit depth then fail_tac ReachedLimit + else or_tac (fix_limit depth t) + { skft = fun sk fk -> (aux (succ depth)).skft sk fk } + in aux 1 + + let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) + cut ev g = + let hints = make_autogoal_hints only_classes ~st g in + (g.it, { hints = hints ; is_evar = ev; unique = unique; + only_classes = only_classes; auto_depth = []; + auto_last_tac = lazy (str"none"); + auto_path = []; auto_cut = cut }) + + + let make_autogoals ?(only_classes=true) ?(unique=false) + ?(st=full_transparent_state) hints gs evm' = + let cut = cut_of_hints hints in + let gl i g = + let (gl, auto) = make_autogoal ~only_classes ~unique + ~st cut (Some g) {it = g; sigma = evm'; } in + (gl, { auto with auto_depth = [i]}) + in { it = List.map_i gl 1 gs; sigma = evm' } + + let get_result r = + match r with + | Nonek -> None + | Somek (gls, fk) -> Some (gls.sigma,fk) + + let run_on_evars ?(only_classes=true) ?(unique=false) ?(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 goals = + if !typeclasses_dependency_order then + top_sort evm' goals + else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) in - if path_matches derivs [] then aux e tl - else ortac (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) - (fun e' -> aux (merge_exceptions e e') tl) - | [] -> - if !foundone == false && !typeclasses_debug > 0 then - Feedback.msg_debug - (pr_depth info.search_depth ++ str": no match for " ++ - Printer.pr_constr_env (Goal.env gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ - str" possibilities"); - match e with - | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx - | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx - in - if backtrack then aux (NotApplicableEx,Exninfo.null) poss - else tclONCE (aux (NotApplicableEx,Exninfo.null) poss) - -let new_hints_tac cl hints info kont : unit Proofview.tactic = - Proofview.Goal.nf_enter - { enter = fun gl -> new_hints_tac_gl cl hints info kont gl } - -let cut_of_hints h = - List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h + let res = run_list_tac tac p goals + (make_autogoals ~only_classes ~unique ~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 ~with_univs:false evm' evm, fk) -let intro_tac'' only_classes info kont gl = - let open Proofview in - let open Proofview.Notations in - let env = Goal.env gl in - let sigma = Goal.sigma gl in - let s = Sigma.to_evar_map sigma in - let decl = Tacmach.New.pf_last_hyp gl in - let hint = - make_resolve_hyp env s (Hint_db.transparent_state info.search_hints) - (true,false,false) only_classes None decl in - let ldb = Hint_db.add_list env s hint info.search_hints in - let info' = - { info with search_hints = ldb; last_tac = lazy (str"intro") } - in kont info' - -let intro_tac' only_classes info kont = - Proofview.tclBIND Tactics.intro - (fun _ -> - Proofview.Goal.nf_enter { enter = fun gl -> intro_tac'' only_classes info kont gl }) - -let rec eauto_tac' only_classes hints limit depth = - let kont info = - Proofview.numgoals >>= fun i -> - if !typeclasses_debug > 1 then - Feedback.msg_debug - (str"calling eauto recursively at depth " ++ int (succ depth) - ++ str" on " ++ int i ++ str" subgoals"); - eauto_tac' only_classes hints limit (succ depth) info - in - fun info -> - if Int.equal depth (succ limit) then Proofview.tclZERO ReachedLimitEx - else Proofview.tclOR (new_hints_tac only_classes hints info kont) - (fun e -> Proofview.tclOR (intro_tac' only_classes info kont) - (fun e' -> let (e, info) = merge_exceptions e e' in - Proofview.tclZERO ~info e)) - - -let new_eauto_tac_gl ?st only_classes dep hints limit i sigma gls gl : - unit Proofview.tactic = - let open Proofview in - let open Proofview.Notations in - let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in - let info = make_autogoal' ?st only_classes dep (cut_of_hints hints) i gl in - eauto_tac' only_classes hints limit 1 info + let eauto_tac hints = + then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) -exception HasShelvedGoals - -let new_eauto_tac ?(st=full_transparent_state) only_classes dep hints limit : unit Proofview.tactic = - let open Proofview in - let eautotac sigma gls i = - Goal.nf_enter - { enter = fun gl -> - new_eauto_tac_gl ~st only_classes dep hints limit (succ i) sigma gls gl } - in - Proofview.Unsafe.tclGETGOALS >>= fun gls -> - Proofview.tclEVARMAP >>= fun sigma -> - let j = List.length gls in - (tclDISPATCH - (List.init j (fun i -> eautotac sigma gls i))) - -let fix_iterative t = - let rec aux depth = - Proofview.tclOR (t depth) - (function - | (ReachedLimitEx,_) -> aux (succ depth) - | (e,ie) -> Proofview.tclZERO ~info:ie e) - in aux 1 - -let fix_iterative_limit limit t = - let open Proofview in - let rec aux depth = - if Int.equal depth (succ limit) then tclZERO ReachedLimitEx - else tclOR (t depth) (function (ReachedLimitEx, _) -> aux (succ depth) - | (e,ie) -> Proofview.tclZERO ~info:ie e) - - in aux 1 - -let new_eauto_tac ?(st=full_transparent_state) only_classes ?limit dep hints = - let tac = + let eauto_tac depth hints = if get_typeclasses_iterative_deepening () then - match limit with - | None -> - fix_iterative (new_eauto_tac ~st only_classes dep hints) - | Some l -> - fix_iterative_limit l (new_eauto_tac ~st only_classes dep hints) + match depth with + | None -> fix_iterative (eauto_tac hints) + | Some depth -> fix_iterative_limit depth (eauto_tac hints) else - let limit = match limit with None -> -1 | Some d -> d in - new_eauto_tac ~st only_classes dep hints limit - in - let error (e, ie) = - match e with - | ReachedLimitEx -> - Tacticals.New.tclFAIL 0 (str"Proof search reached its limit") - | NotApplicableEx -> - Tacticals.New.tclFAIL 0 (str"Proof search failed" ++ - (if Option.is_empty limit then mt() - else str" without reaching its limit")) - | e -> Proofview.tclZERO ~info:ie e - in Proofview.tclORELSE tac error - -let run_on_evars ?(unique=false) p evm tac = - match evars_to_goals p evm with - | None -> None (* This happens only because there's no evar having p *) - | Some (goals, evm') -> - let goals = - if !typeclasses_dependency_order then - top_sort evm' goals - else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) + match depth with + | None -> fix (eauto_tac hints) + | Some depth -> fix_limit depth (eauto_tac hints) + + let real_eauto ?depth unique st hints p evd = + let res = + run_on_evars ~st ~unique p evd hints (eauto_tac depth hints) in - let fgoals = Evd.future_goals evm in - let pgoal = Evd.principal_future_goal evm in - let _, pv = Proofview.init evm' [] in - let pv = Proofview.unshelve goals pv in - try - let (), pv', (unsafe, shelved, gaveup), _ = - Proofview.apply (Global.env ()) tac pv - in - if Proofview.finished pv' then - let evm' = Proofview.return pv' in - assert(Evd.fold_undefined (fun ev _ acc -> - let okev = Evd.mem evm ev || List.mem ev shelved in - if not okev then - Feedback.msg_debug - (str "leaking evar " ++ int (Evar.repr ev) ++ - spc () ++ pr_ev evm' ev); - acc && okev) evm' true); - let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in - let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in - Some evm' - else raise Not_found - with Logic_monad.TacticFailure _ -> raise Not_found - -let real_new_eauto ?limit unique st hints p evd = - let eauto_tac = new_eauto_tac ~st true ?limit false hints in - let res = run_on_evars ~unique p evd eauto_tac in match res with | None -> evd - | Some evd' -> evd' - (* TODO treat unique classes, with exactlyonce *) - -let resolve_all_evars_once' debug limit unique p evd = - let db = searchtable_map typeclasses_db in - real_new_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd - -let hints_tac hints = - { skft = fun sk fk {it = gl,info; sigma = s;} -> - let env = Goal.V82.env s gl in - let concl = Goal.V82.concl s gl in - let tacgl = {it = gl; sigma = s;} in - let poss = e_possible_resolve hints info.hints info.only_classes s concl in - let unique = is_unique env 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 (Proofview.V82.of_tactic tac tacgl) - with e when catchable e -> None - in - (match res with - | None -> aux i foundone tl - | Some {it = gls; sigma = s';} -> - if !typeclasses_debug > 0 then - Feedback.msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev s gl); - let sgls = - evars_to_goals - (fun evm ev evi -> - if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) && - (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') -> - if not !typeclasses_dependency_order then - (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s') - else - (* Reorder with dependent subgoals. *) - let evm = List.fold_left - (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in - let gls = top_sort s' evm in - (List.map (fun ev -> Some ev, ev) gls, 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';} - else info.hints; - auto_cut = derivs } - in g, info) 1 newgls in - let glsv = {it = gls'; sigma = s';} in - let fk' = - (fun e -> - let do_backtrack = - if unique then occur_existential concl - else if info.unique then true - else if List.is_empty gls' then - needs_backtrack env s' info.is_evar concl - else true - in - let e' = match foundone with None -> e | Some e' -> merge_failures e e' in - if !typeclasses_debug > 0 then - Feedback.msg_debug - ((if do_backtrack then str"Backtracking after " - else str "Not backtracking after ") - ++ Lazy.force pp); - if do_backtrack then aux (succ i) (Some e') tl - else fk e') - in - sk glsv fk') + | Some (evd', fk) -> + if unique then + (match get_result (fk NotApplicable) with + | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions" + | None -> evd') + else evd' + + let resolve_all_evars_once debug depth unique p evd = + let db = searchtable_map typeclasses_db in + real_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd + + let eauto85 ?(only_classes=true) ?st depth hints g = + let gl = { it = make_autogoal ~only_classes ?st + (cut_of_hints hints) None g; sigma = project g; } in + match run_tac (eauto_tac depth hints) gl with + | None -> raise Not_found + | Some {it = goals; sigma = s; } -> + {it = List.map fst goals; sigma = s;} + +end + +(** 8.6 resolution *) +module Search = struct + type autoinfo = + { search_depth : int list; + last_tac : Pp.std_ppcmds Lazy.t; + search_dep : bool; + search_only_classes : bool; + search_cut : hints_path; + search_hints : hint_db; } + + let autogoal_cache = ref (DirPath.empty, true, Context.Named.empty, + Hint_db.empty full_transparent_state true) + + let make_autogoal_hints only_classes ?(st=full_transparent_state) g = + let open Proofview in + let open Tacmach.New in + let sign = Goal.hyps g in + let (dir, onlyc, sign', cached_hints) = !autogoal_cache in + let cwd = Lib.cwd () in + if DirPath.equal cwd dir && + (onlyc == only_classes) && + Context.Named.equal sign sign' && + Hint_db.transparent_state cached_hints == st + then cached_hints + else + let hints = make_hints {it = Goal.goal g; sigma = project g} + st only_classes sign + in + autogoal_cache := (cwd, only_classes, sign, hints); hints + + let make_autogoal ?(st=full_transparent_state) only_classes dep cut i g = + let hints = make_autogoal_hints only_classes ~st g in + { search_hints = hints; + search_depth = [i]; last_tac = lazy (str"none"); + search_dep = dep; + search_only_classes = only_classes; + search_cut = cut } + + let needs_backtrack env evd unique concl = + if unique || is_Prop env evd concl then + occur_existential concl + else true + + (** In the proof engine failures are represented as exceptions *) + exception ReachedLimitEx + exception NotApplicableEx + + let merge_exceptions e e' = + match fst e, fst e' with + | ReachedLimitEx, _ -> e + | _, ReachedLimitEx -> e' + | _, _ -> e + + let hints_tac_gl hints info kont gl : unit Proofview.tactic = + let open Proofview in + let open Proofview.Notations in + let env = Goal.env gl in + let concl = Goal.concl gl in + let sigma = Goal.sigma gl in + let s = Sigma.to_evar_map sigma in + let unique = not info.search_dep || is_unique env concl in + let backtrack = needs_backtrack env s unique concl in + if !typeclasses_debug > 0 then + Feedback.msg_debug (pr_depth info.search_depth ++ str": looking for " ++ + Printer.pr_constr_env (Goal.env gl) s concl ++ + (if backtrack then str" with backtracking" + else str" without backtracking")); + let poss = + e_possible_resolve hints info.search_hints info.search_only_classes s concl in + (* If no goal depends on the solution of this one or the + instances are irrelevant/assumed to be unique, then + we don't need to backtrack, as long as no evar appears in the goal + This is an overapproximation. Evars could appear in this goal only + and not any other *) + let ortac = if backtrack then Proofview.tclOR else Proofview.tclORELSE in + let idx = ref 1 in + let foundone = ref false in + let rec aux e = function + | (tac, pat, b, name, pp) :: tl -> + let derivs = path_derivate info.search_cut name in + (if !typeclasses_debug > 1 then + Feedback.msg_debug (pr_depth (!idx :: info.search_depth) ++ str": trying " ++ + Lazy.force pp ++ + (if !foundone != true then + str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl) + else mt ()))); + let tac_of gls i j = Goal.nf_enter { enter = fun gl' -> + begin + let sigma' = Goal.sigma gl' in + let s' = Sigma.to_evar_map sigma' in + let _concl = Goal.concl gl' in + if !typeclasses_debug > 0 then + Feedback.msg_debug (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ + pr_ev s' (Proofview.Goal.goal gl')); + let hints' = + if b && not (Context.Named.equal (Goal.hyps gl') (Goal.hyps gl)) + then + let st = Hint_db.transparent_state info.search_hints in + make_autogoal_hints info.search_only_classes ~st gl' + else info.search_hints + in + let dep' = info.search_dep || Proofview.unifiable s' (Goal.goal gl') gls in + let info' = + { search_depth = succ j :: i :: info.search_depth; + last_tac = pp; + search_dep = dep'; + search_only_classes = info.search_only_classes; + search_hints = hints'; + search_cut = derivs } + in + kont info' end } + in + let rec result (shelf, ()) i k = + foundone := true; + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + let j = List.length gls in + (if !typeclasses_debug > 0 then + Feedback.msg_debug + (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp + ++ str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal gl) + ++ str", " ++ int j ++ str" subgoal(s)" ++ + (Option.cata (fun k -> str " in addition to the first " ++ int k) + (mt()) k))); + let res = + if j = 0 then tclUNIT () + else tclDISPATCH + (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) + in + let finish = + tclEVARMAP >>= fun sigma -> + let filter ev = + try + let evi = Evd.find_undefined sigma ev in + if info.search_only_classes then + Some (ev, is_class_type sigma (Evd.evar_concl evi)) + else Some (ev, true) + with Not_found -> None + in + let remaining = CList.map_filter filter shelf in + if !typeclasses_debug > 1 then + Feedback.msg_debug (pr_depth (i :: info.search_depth) ++ + str": after " ++ Lazy.force pp ++ str" finished, " ++ + int (List.length remaining) ++ + str " goals are shelved and unsolved ( " ++ + prlist_with_sep spc + (fun ev -> int (Evar.repr ev) ++ spc () ++ + pr_ev sigma ev) + (List.map fst remaining) ++ str")"); + begin + (* Some existentials produced by the original tactic were not solved + in the subgoals, turn them into subgoals now. *) + let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in + let shelved = List.map fst shelved and goals = List.map fst goals in + if !typeclasses_debug > 1 then + Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ + prlist_with_sep spc (pr_ev sigma) goals); + shelve_goals shelved <*> + (if List.is_empty goals then tclUNIT () + else with_shelf (Unsafe.tclNEWGOALS goals) >>= + fun s -> result s i (Some (Option.default 0 k + j))) + end + in res <*> finish + in + if path_matches derivs [] then aux e tl + else ortac (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) + (fun e' -> aux (merge_exceptions e e') tl) | [] -> - if foundone == None && !typeclasses_debug > 0 then - Feedback.msg_debug (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_constr_env (Goal.V82.env s gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ str" possibilities"); - match foundone with - | Some e -> fk e - | None -> fk NotApplicable - in aux 1 None poss } - -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 -> - Control.check_for_interrupt (); - (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 fk'' = - if not info.unique && List.is_empty gls' && - not (needs_backtrack (Goal.V82.env s gl) s - info.is_evar (Goal.V82.concl s gl)) - then fk - else fk' - in - aux s' (gls'::acc) fk'' gls) - fk {it = (gl,info); sigma = s; }) - | [] -> Somek2 (List.rev acc, s, fk) - in fun {it = gls; sigma = s; } fk -> - let rec aux' = function - | Nonek2 e -> fk e - | Somek2 (res, s', fk') -> - let goals' = List.concat res in - sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e)) - in aux' (aux s [] (fun e -> Nonek2 e) 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 reason : atac = - { skft = fun sk fk _ -> fk reason } - -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 ReachedLimit - else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } - -let fix_iterative t = - let rec aux depth = - or_else_tac (fix_limit depth t) - (function - | NotApplicable as e -> fail_tac e - | ReachedLimit -> aux (succ depth)) - in aux 1 - -let fix_iterative_limit limit (t : 'a tac) : 'a tac = - let rec aux depth = - if Int.equal depth limit then fail_tac ReachedLimit - else or_tac (fix_limit depth t) { skft = fun sk fk -> (aux (succ depth)).skft sk fk } - in aux 1 - -let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) - cut ev g = - let hints = make_autogoal_hints only_classes ~st g in - (g.it, { hints = hints ; is_evar = ev; unique = unique; - only_classes = only_classes; auto_depth = []; - auto_last_tac = lazy (str"none"); - auto_path = []; auto_cut = cut }) - - -let make_autogoals ?(only_classes=true) ?(unique=false) - ?(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 ~unique - ~st cut (Some g) {it = g; sigma = evm'; } in - (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; } - -let get_result r = - match r with - | Nonek -> None - | Somek (gls, fk) -> Some (gls.sigma,fk) - -let run_on_evars ?(only_classes=true) ?(unique=false) ?(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 goals = - if !typeclasses_dependency_order then - top_sort evm' goals - else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) + if !foundone == false && !typeclasses_debug > 0 then + Feedback.msg_debug (pr_depth info.search_depth ++ str": no match for " ++ + Printer.pr_constr_env (Goal.env gl) s concl ++ + spc () ++ str ", " ++ int (List.length poss) ++ + str" possibilities"); + match e with + | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx + | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx in - let res = run_list_tac tac p goals - (make_autogoals ~only_classes ~unique ~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 ~with_univs:false evm' evm, fk) - -let eauto_tac hints = - then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) - -let eauto_tac ?limit hints = - if get_typeclasses_iterative_deepening () then - match limit with - | None -> fix_iterative (eauto_tac hints) - | Some limit -> fix_iterative_limit limit (eauto_tac hints) - else - match limit with - | None -> fix (eauto_tac hints) - | Some limit -> fix_limit limit (eauto_tac hints) - -let real_eauto ?limit unique st hints p evd = - let res = - run_on_evars ~st ~unique p evd hints (eauto_tac ?limit hints) - in + if backtrack then aux (NotApplicableEx,Exninfo.null) poss + else tclONCE (aux (NotApplicableEx,Exninfo.null) poss) + + let hints_tac hints info kont : unit Proofview.tactic = + Proofview.Goal.nf_enter + { enter = fun gl -> hints_tac_gl hints info kont gl } + + let intro_tac info kont gl = + let open Proofview in + let open Proofview.Notations in + let env = Goal.env gl in + let sigma = Goal.sigma gl in + let s = Sigma.to_evar_map sigma in + let decl = Tacmach.New.pf_last_hyp gl in + let hint = + make_resolve_hyp env s (Hint_db.transparent_state info.search_hints) + (true,false,false) info.search_only_classes None decl in + let ldb = Hint_db.add_list env s hint info.search_hints in + let info' = + { info with search_hints = ldb; last_tac = lazy (str"intro") } + in kont info' + + let intro info kont = + Proofview.tclBIND Tactics.intro + (fun _ -> Proofview.Goal.nf_enter { enter = fun gl -> intro_tac info kont gl }) + + let rec search_tac hints limit depth = + let kont info = + Proofview.numgoals >>= fun i -> + if !typeclasses_debug > 1 then + Feedback.msg_debug (str"calling eauto recursively at depth " ++ int (succ depth) + ++ str" on " ++ int i ++ str" subgoals"); + search_tac hints limit (succ depth) info + in + fun info -> + if Int.equal depth (succ limit) then Proofview.tclZERO ReachedLimitEx + else + Proofview.tclOR (hints_tac hints info kont) + (fun e -> Proofview.tclOR (intro info kont) + (fun e' -> let (e, info) = merge_exceptions e e' in + Proofview.tclZERO ~info e)) + + let search_tac_gl ?st only_classes dep hints depth i sigma gls gl : + unit Proofview.tactic = + let open Proofview in + let open Proofview.Notations in + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in + let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in + search_tac hints depth 1 info + + exception HasShelvedGoals + + let search_tac ?(st=full_transparent_state) only_classes dep hints depth = + let open Proofview in + let tac sigma gls i = + Goal.nf_enter + { enter = fun gl -> + search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl } + in + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + Proofview.tclEVARMAP >>= fun sigma -> + let j = List.length gls in + (tclDISPATCH (List.init j (fun i -> tac sigma gls i))) + + let fix_iterative t = + let rec aux depth = + Proofview.tclOR (t depth) + (function + | (ReachedLimitEx,_) -> aux (succ depth) + | (e,ie) -> Proofview.tclZERO ~info:ie e) + in aux 1 + + let fix_iterative_limit limit t = + let open Proofview in + let rec aux depth = + if Int.equal depth (succ limit) then tclZERO ReachedLimitEx + else tclOR (t depth) (function (ReachedLimitEx, _) -> aux (succ depth) + | (e,ie) -> Proofview.tclZERO ~info:ie e) + in aux 1 + + let eauto_tac ?(st=full_transparent_state) ~only_classes ~depth ~dep hints = + let tac = + let search = search_tac ~st only_classes dep hints in + if get_typeclasses_iterative_deepening () then + match depth with + | None -> fix_iterative search + | Some l -> fix_iterative_limit l search + else + let depth = match depth with None -> -1 | Some d -> d in + search depth + in + let error (e, ie) = + match e with + | ReachedLimitEx -> + Tacticals.New.tclFAIL 0 (str"Proof search reached its limit") + | NotApplicableEx -> + Tacticals.New.tclFAIL 0 (str"Proof search failed" ++ + (if Option.is_empty depth then mt() + else str" without reaching its limit")) + | e -> Proofview.tclZERO ~info:ie e + in Proofview.tclORELSE tac error + + let run_on_evars ?(unique=false) p evm tac = + match evars_to_goals p evm with + | None -> None (* This happens only because there's no evar having p *) + | Some (goals, evm') -> + let goals = + if !typeclasses_dependency_order then + top_sort evm' goals + else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) + in + let fgoals = Evd.future_goals evm in + let pgoal = Evd.principal_future_goal evm in + let _, pv = Proofview.init evm' [] in + let pv = Proofview.unshelve goals pv in + try + let (), pv', (unsafe, shelved, gaveup), _ = + Proofview.apply (Global.env ()) tac pv + in + if Proofview.finished pv' then + let evm' = Proofview.return pv' in + assert(Evd.fold_undefined (fun ev _ acc -> + let okev = Evd.mem evm ev || List.mem ev shelved in + if not okev then + Feedback.msg_debug + (str "leaking evar " ++ int (Evar.repr ev) ++ + spc () ++ pr_ev evm' ev); + acc && okev) evm' true); + let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in + let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in + Some evm' + else raise Not_found + with Logic_monad.TacticFailure _ -> raise Not_found + + let eauto depth only_classes unique dep st hints p evd = + let eauto_tac = eauto_tac ~st ~only_classes ~depth ~dep hints in + let res = run_on_evars ~unique p evd eauto_tac in match res with | None -> evd - | Some (evd', fk) -> - if unique then - (match get_result (fk NotApplicable) with - | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions" - | None -> evd') - else evd' - -let resolve_all_evars_once debug limit unique p evd = - let db = searchtable_map typeclasses_db in - real_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd - -let eauto85 ?(only_classes=true) ?st ?limit hints g = - let gl = { it = make_autogoal ~only_classes ?st - (cut_of_hints hints) None g; sigma = project g; } in - match run_tac (eauto_tac ?limit hints) gl with - | None -> raise Not_found - | Some {it = goals; sigma = s; } -> - {it = List.map fst goals; sigma = s;} + | Some evd' -> evd' + (* TODO treat unique solutions *) + + let typeclasses_eauto ?depth unique st hints p evd = + eauto depth true unique false st hints p evd + (** Typeclasses eauto is an eauto which tries to resolve only + goals of typeclass type, and assumes that the initially selected + evars in evd are independent of the rest of the evars *) + + let typeclasses_resolve debug depth unique p evd = + let db = searchtable_map typeclasses_db in + typeclasses_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd +end + +(** Binding to either V85 or Search implementations. *) +let eauto depth ~only_classes ~st ~dep dbs = + Search.eauto_tac ~st ~only_classes ~depth ~dep dbs + +let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) + ~depth dbs = + let dbs = List.map_filter + (fun db -> try Some (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 + let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in + if get_typeclasses_compat () = Flags.V8_5 then + Tacticals.New.tclORELSE (Proofview.V82.tactic + (V85.eauto85 depth ~only_classes ~st dbs)) + (Proofview.Goal.nf_enter ({ enter = fun gl -> + Tacticals.New.tclFAIL 0 (str" typeclasses eauto failed on: " ++ + Goal.pr_goal (Proofview.Goal.goal gl))})) + else eauto depth ~only_classes ~st ~dep:true dbs (** We compute dependencies via a union-find algorithm. Beware of the imperative effects on the partition structure, @@ -1256,24 +1286,6 @@ let evar_dependencies evm p = in Intpart.union_set evars p) evm () -let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = - 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 - let hints = searchtable_map typeclasses_db in - let gls' = eauto85 ?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_instantiation_problem := - (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) - (** [split_evars] returns groups of undefined evars according to dependencies *) let split_evars evm = @@ -1289,9 +1301,9 @@ let is_inference_forced p evd ev = then let (loc, k) = evar_source ev evd in match k with - | Evar_kinds.ImplicitArg (_, _, b) -> b - | Evar_kinds.QuestionMark _ -> false - | _ -> true + | Evar_kinds.ImplicitArg (_, _, b) -> b + | Evar_kinds.QuestionMark _ -> false + | _ -> true else true with Not_found -> assert false @@ -1358,12 +1370,11 @@ let revert_resolvability oevd evd = 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 unique env p oevd do_split fail = +(** If [do_split] is [true], we try to separate the problem in + several components and then solve them separately *) +let resolve_all_evars debug depth unique 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 @@ -1372,20 +1383,20 @@ let resolve_all_evars debug m unique env p oevd do_split fail = | comp :: comps -> let p = select_and_update_evars p oevd (in_comp comp) in try - let evd' = + let evd' = if get_typeclasses_compat () = Flags.Current then - resolve_all_evars_once' debug m unique p evd - else resolve_all_evars_once debug m unique p evd + Search.typeclasses_resolve debug depth unique p evd + else V85.resolve_all_evars_once debug depth unique p evd in - if has_undefined p oevd evd' then raise Unresolved; - docomp evd' comps + 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. *) + if fail && (not do_split || is_mandatory (p evd) comp evd) + then (* Unable to satisfy the constraints. *) let comp = if do_split then Some comp else None in - error_unresolvable env comp evd - else (* Best effort: do nothing on this component *) - docomp evd comps + error_unresolvable env comp evd + else (* Best effort: do nothing on this component *) + docomp evd comps in docomp oevd split let initial_select_evars filter = @@ -1393,13 +1404,14 @@ let initial_select_evars filter = filter ev (snd evi.Evd.evar_source) && Typeclasses.is_class_evar evd evi -let resolve_typeclass_evars debug m unique env evd filter split fail = +let resolve_typeclass_evars debug depth unique 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 unique env (initial_select_evars filter) evd split fail + resolve_all_evars debug depth unique env + (initial_select_evars filter) evd split fail let solve_inst env evd filter unique split fail = resolve_typeclass_evars @@ -1410,22 +1422,24 @@ let solve_inst env evd filter unique split fail = let _ = Typeclasses.solve_instantiations_problem := solve_inst -let eauto ?limit ~only_classes ~st dbs = - new_eauto_tac ~st only_classes ?limit dbs - -let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs = - let dbs = List.map_filter - (fun db -> try Some (searchtable_map db) - with e when Errors.noncritical e -> None) - dbs +let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = + 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 + let hints = searchtable_map typeclasses_db in + let gls' = V85.eauto85 !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 st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in - if get_typeclasses_compat () = Flags.V8_5 then - Tacticals.New.tclORELSE (Proofview.V82.tactic (eauto85 ?limit:!typeclasses_depth ~only_classes ~st dbs)) - (Proofview.Goal.nf_enter ({ enter = fun gl -> - Tacticals.New.tclFAIL 0 (str" typeclasses eauto failed on: " ++ - Goal.pr_goal (Proofview.Goal.goal gl))})) - else eauto ?limit:!typeclasses_depth ~only_classes ~st true dbs + let term = Evarutil.nf_evar evd t' in + evd, term + +let _ = + Typeclasses.solve_instantiation_problem := + (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) (** Take the head of the arity of a constr. Used in the partial application tactic. *) @@ -1449,11 +1463,3 @@ let not_evar c = match kind_of_term c with 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 = auto_unif_flags Evar.Set.empty - (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_unsafe_type_of gl c in - let ce = mk_clenv_from gl (c,cty) in - let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),None,ce) } in - Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 48abba1aa..2fb0bbb04 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -20,10 +20,9 @@ val get_typeclasses_debug : unit -> bool val set_typeclasses_depth : int option -> unit val get_typeclasses_depth : unit -> int option -val progress_evars : unit Proofview.tactic -> unit Proofview.tactic - val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> - Hints.hint_db_name list -> unit Proofview.tactic + depth:(Int.t option) -> + Hints.hint_db_name list -> unit Proofview.tactic val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic @@ -33,24 +32,18 @@ val is_ground : constr -> tactic val autoapply : constr -> Hints.hint_db_name -> tactic -type newautoinfo = - { search_depth : int list; - last_tac : Pp.std_ppcmds Lazy.t; - search_dep : bool; - search_cut : Hints.hints_path; - search_hints : Hints.Hint_db.t } - -val new_hints_tac : bool -> Hints.hint_db list -> - newautoinfo -> - (newautoinfo -> unit Proofview.tactic) -> unit Proofview.tactic - -val make_autogoal' : ?st:Names.transparent_state -> - bool -> bool -> - Hints.hints_path -> int -> ([ `NF ], 'c) Proofview.Goal.t -> newautoinfo - -val new_eauto_tac : ?st:Names.transparent_state -> - bool -> ?limit:Int.t -> - bool -> (* Should the tactic be made backtracking, whatever the dependencies - betwwen initial goals are *) - Hints.hint_db list -> unit Proofview.tactic - +module Search : sig + val eauto_tac : + ?st:Names.transparent_state -> + (** The transparent_state used when working with local hypotheses *) + only_classes:bool -> + (** Should non-class goals be shelved and resolved at the end *) + depth:Int.t option -> + (** Bounded or unbounded search *) + dep:bool -> + (** Should the tactic be made backtracking on the initial goals, + whatever their internal dependencies are. *) + Hints.hint_db list -> + (** The list of hint databases to use *) + unit Proofview.tactic +end |