diff options
| -rw-r--r-- | tactics/auto.ml | 4 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 14 | ||||
| -rw-r--r-- | tactics/eauto.ml | 6 | ||||
| -rw-r--r-- | tactics/hints.ml | 69 | ||||
| -rw-r--r-- | tactics/hints.mli | 9 |
5 files changed, 88 insertions, 14 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index d7de6c4fb5..65b2615b6b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -416,6 +416,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl = "nocore" amongst the databases. *) let trivial ?(debug=Off) lems dbnames = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -427,6 +428,7 @@ let trivial ?(debug=Off) lems dbnames = end let full_trivial ?(debug=Off) lems = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -501,6 +503,7 @@ let search d n mod_delta db_list local_db = let default_search_depth = ref 5 let delta_auto debug mod_delta n lems dbnames = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in @@ -524,6 +527,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n let default_auto = auto !default_search_depth [] [] let delta_full_auto ?(debug=Off) mod_delta n lems = + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3456d13bbe..2b183a9d37 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -934,6 +934,9 @@ module Search = struct | Some i -> str ", with depth limit " ++ int i)); tac + let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints = + Hints.wrap_hint_warning @@ eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints + let run_on_evars env evm p tac = match evars_to_goals p evm with | None -> None (* This happens only because there's no evar having p *) @@ -1143,15 +1146,19 @@ let resolve_typeclass_evars debug depth unique env evd filter split fail = (initial_select_evars filter) evd split fail let solve_inst env evd filter unique split fail = - resolve_typeclass_evars + let ((), sigma) = Hints.wrap_hint_warning_fun env evd begin fun evd -> + (), resolve_typeclass_evars (get_typeclasses_debug ()) (get_typeclasses_depth ()) unique env evd filter split fail + end in + sigma let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = + let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma -> let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl Store.empty in @@ -1169,7 +1176,9 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = let evd = sig_sig gls' in let t' = mkEvar (ev, Array.of_list subst) in let term = Evarutil.nf_evar evd t' in - evd, term + term, evd + end in + (sigma, term) let _ = Hook.set Typeclasses.solve_one_instance_hook @@ -1205,6 +1214,7 @@ let is_ground c = let autoapply c i = let open Proofview.Notations in + Hints.wrap_hint_warning @@ Proofview.Goal.enter begin fun gl -> let hintdb = try Hints.searchtable_map i with Not_found -> CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ ".")) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 80d07c5c03..5067315d08 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -409,7 +409,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl = (* let e_search_auto = CProfile.profile5 e_search_auto_key e_search_auto *) let eauto_with_bases ?(debug=Off) np lems db_list = - tclTRY (e_search_auto debug np lems db_list) + Proofview.V82.of_tactic (Hints.wrap_hint_warning (Proofview.V82.tactic (tclTRY (e_search_auto debug np lems db_list)))) let eauto ?(debug=Off) np lems dbnames = let db_list = make_db_list dbnames in @@ -420,8 +420,8 @@ let full_eauto ?(debug=Off) n lems gl = tclTRY (e_search_auto debug n lems db_list) gl let gen_eauto ?(debug=Off) np lems = function - | None -> Proofview.V82.tactic (full_eauto ~debug np lems) - | Some l -> Proofview.V82.tactic (eauto ~debug np lems l) + | None -> Hints.wrap_hint_warning (Proofview.V82.tactic (full_eauto ~debug np lems)) + | Some l -> Hints.wrap_hint_warning (Proofview.V82.tactic (eauto ~debug np lems l)) let make_depth = function | None -> !default_search_depth diff --git a/tactics/hints.ml b/tactics/hints.ml index 3835dee299..c0ba363360 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1579,25 +1579,76 @@ let print_mp mp = let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true +let hint_trace = Evd.Store.field () + +let log_hint h = + let open Proofview.Notations in + Proofview.tclEVARMAP >>= fun sigma -> + let store = get_extra_data sigma in + match Store.get store hint_trace with + | None -> + (** All calls to hint logging should be well-scoped *) + assert false + | Some trace -> + let trace = KNmap.add h.uid h trace in + let store = Store.set store hint_trace trace in + Proofview.Unsafe.tclEVARS (set_extra_data store sigma) + let warn_non_imported_hint = CWarnings.create ~name:"non-imported-hint" ~category:"automation" (fun (hint,mp) -> strbrk "Hint used but not imported: " ++ hint ++ print_mp mp) -let warn h x = - let open Proofview in - tclBIND tclENV (fun env -> - tclBIND tclEVARMAP (fun sigma -> - let hint = pr_hint env sigma h in - let (mp, _, _) = KerName.repr h.uid in - warn_non_imported_hint (hint,mp); - Proofview.tclUNIT x)) +let warn env sigma h = + let hint = pr_hint env sigma h in + let (mp, _, _) = KerName.repr h.uid in + warn_non_imported_hint (hint,mp) + +let wrap_hint_warning t = + let open Proofview.Notations in + Proofview.tclEVARMAP >>= fun sigma -> + let store = get_extra_data sigma in + let old = Store.get store hint_trace in + let store = Store.set store hint_trace KNmap.empty in + Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () -> + t >>= fun ans -> + Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> + let store = get_extra_data sigma in + let hints = match Store.get store hint_trace with + | None -> assert false + | Some hints -> hints + in + let () = KNmap.iter (fun _ h -> warn env sigma h) hints in + let store = match old with + | None -> Store.remove store hint_trace + | Some v -> Store.set store hint_trace v + in + Proofview.Unsafe.tclEVARS (set_extra_data store sigma) >>= fun () -> + Proofview.tclUNIT ans + +let wrap_hint_warning_fun env sigma t = + let store = get_extra_data sigma in + let old = Store.get store hint_trace in + let store = Store.set store hint_trace KNmap.empty in + let (ans, sigma) = t (set_extra_data store sigma) in + let store = get_extra_data sigma in + let hints = match Store.get store hint_trace with + | None -> assert false + | Some hints -> hints + in + let () = KNmap.iter (fun _ h -> warn env sigma h) hints in + let store = match old with + | None -> Store.remove store hint_trace + | Some v -> Store.set store hint_trace v + in + (ans, set_extra_data store sigma) let run_hint tac k = match !warn_hint with | `LAX -> k tac.obj | `WARN -> if is_imported tac then k tac.obj - else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x) + else Proofview.tclTHEN (log_hint tac) (k tac.obj) | `STRICT -> if is_imported tac then k tac.obj else Proofview.tclZERO (UserError (None, (str "Tactic failure."))) diff --git a/tactics/hints.mli b/tactics/hints.mli index c49ca2094a..d63efea27d 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -282,6 +282,15 @@ val make_db_list : hint_db_name list -> hint_db list val typeclasses_db : hint_db_name val rewrite_db : hint_db_name +val wrap_hint_warning : 'a Proofview.tactic -> 'a Proofview.tactic +(** Use around toplevel calls to hint-using tactics, to enable the tracking of + non-imported hints. Any tactic calling [run_hint] must be wrapped this + way. *) + +val wrap_hint_warning_fun : env -> evar_map -> + (evar_map -> 'a * evar_map) -> 'a * evar_map +(** Variant of the above for non-tactics *) + (** Printing hints *) val pr_searchtable : env -> evar_map -> Pp.t |