diff options
author | 2015-11-13 11:31:34 +0100 | |
---|---|---|
committer | 2015-11-13 11:31:34 +0100 | |
commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
tree | 074182834cb406d1304aec4233718564a9c06ba1 /tactics/hints.ml | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'tactics/hints.ml')
-rw-r--r-- | tactics/hints.ml | 292 |
1 files changed, 193 insertions, 99 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 55d62e15..5630d20b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -68,7 +68,7 @@ let decompose_app_bound t = (* The Type of Constructions Autotactic Hints *) (************************************************************************) -type 'a auto_tactic_ast = +type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -92,23 +92,66 @@ type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set -type 'a auto_tactic = 'a auto_tactic_ast +type 'a with_uid = { + obj : 'a; + uid : KerName.t; +} + +type raw_hint = constr * types * Univ.universe_context_set -type 'a gen_auto_tactic = { +type hint = (raw_hint * clausenv) hint_ast with_uid + +type 'a with_metadata = { pri : int; (* A number lower is higher priority *) poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (* A pattern for the concl of the Goal *) name : hints_path_atom; (* A potential name to refer to the hint *) - code : 'a (* the tactic to apply when the concl matches pat *) + code : 'a; (* the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic +type full_hint = hint with_metadata type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic - -let run_auto_tactic tac k = k tac -let repr_auto_tactic tac = tac + raw_hint hint_ast with_uid with_metadata + +type import_level = [ `LAX | `WARN | `STRICT ] + +let warn_hint : import_level ref = ref `LAX +let read_warn_hint () = match !warn_hint with +| `LAX -> "Lax" +| `WARN -> "Warn" +| `STRICT -> "Strict" + +let write_warn_hint = function +| "Lax" -> warn_hint := `LAX +| "Warn" -> warn_hint := `WARN +| "Strict" -> warn_hint := `STRICT +| _ -> error "Only the following flags are accepted: Lax, Warn, Strict." + +let _ = + Goptions.declare_string_option + { Goptions.optsync = true; + Goptions.optdepr = false; + Goptions.optname = "behavior of non-imported hints"; + Goptions.optkey = ["Loose"; "Hint"; "Behavior"]; + Goptions.optread = read_warn_hint; + Goptions.optwrite = write_warn_hint; + } + +let fresh_key = + let id = Summary.ref ~name:"HINT-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) let eq_hints_path_atom p1 p2 = match p1, p2 with | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2 @@ -125,7 +168,7 @@ let eq_auto_tactic t1 t2 = match t1, t2 with | (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _ | Unfold_nth _ | Extern _), _ -> false -let eq_gen_auto_tactic t1 t2 = +let eq_hint_metadata t1 t2 = Int.equal t1.pri t2.pri && Option.equal constr_pattern_eq t1.pat t2.pat && eq_hints_path_atom t1.name t2.name && @@ -153,7 +196,7 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0 - un discrimination net borné (Btermdn.t) constitué de tous les patterns de la seconde liste de tactiques *) -type stored_data = int * pri_auto_tactic +type stored_data = int * full_hint (* First component is the index of insertion in the table, to keep most recent first semantics. *) module Bounded_net = Btermdn.Make(struct @@ -175,21 +218,7 @@ let empty_se = { sentry_mode = []; } -let eq_pri_auto_tactic (_, x) (_, y) = - if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then - match x.code,y.code with - | Res_pf (cstr,_),Res_pf (cstr1,_) -> - Term.eq_constr cstr cstr1 - | ERes_pf (cstr,_),ERes_pf (cstr1,_) -> - Term.eq_constr cstr cstr1 - | Give_exact (cstr,_),Give_exact (cstr1,_) -> - Term.eq_constr cstr cstr1 - | Res_pf_THEN_trivial_fail (cstr,_) - ,Res_pf_THEN_trivial_fail (cstr1,_) -> - Term.eq_constr cstr cstr1 - | _,_ -> false - else - false +let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid let add_tac pat t st se = match pat with @@ -239,24 +268,24 @@ let strip_params env c = | _ -> c) | _ -> c -let instantiate_hint p = - let mk_clenv c cty ctx = - let env = Global.env () in - let sigma = Evd.merge_context_set univ_flexible (Evd.from_env env) ctx in - let cl = mk_clenv_from_env (Global.env()) sigma None (c,cty) in +let instantiate_hint env sigma p = + let mk_clenv (c, cty, ctx) = + let sigma = Evd.merge_context_set univ_flexible sigma ctx in + let cl = mk_clenv_from_env env sigma None (c,cty) in {cl with templval = { cl.templval with rebus = strip_params env cl.templval.rebus }; env = empty_env} in - let code = match p.code with - | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx) - | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx) - | Res_pf_THEN_trivial_fail (c, cty, ctx) -> - Res_pf_THEN_trivial_fail (c, mk_clenv c cty ctx) - | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx) + let code = match p.code.obj with + | Res_pf c -> Res_pf (c, mk_clenv c) + | ERes_pf c -> ERes_pf (c, mk_clenv c) + | Res_pf_THEN_trivial_fail c -> + Res_pf_THEN_trivial_fail (c, mk_clenv c) + | Give_exact c -> Give_exact (c, mk_clenv c) | Unfold_nth e -> Unfold_nth e | Extern t -> Extern t - in { pri = p.pri; poly = p.poly; name = p.name; pat = p.pat; code = code } + in + { p with code = { p.code with obj = code } } let hints_path_atom_eq h1 h2 = match h1, h2 with | PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2 @@ -353,15 +382,19 @@ let rec normalize_path h = let path_derivate hp hint = normalize_path (path_derivate hp hint) +let pp_hints_path_atom a = + match a with + | PathAny -> str"*" + | PathHints grs -> pr_sequence pr_global grs + let rec pp_hints_path = function - | PathAtom (PathAny) -> str"." - | PathAtom (PathHints grs) -> pr_sequence pr_global grs - | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" + | PathAtom pa -> pp_hints_path_atom pa + | PathStar p -> str "!(" ++ pp_hints_path p ++ str")" | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p' | PathOr (p, p') -> str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")" - | PathEmpty -> str"Ø" - | PathEpsilon -> str"ε" + | PathEmpty -> str"emp" + | PathEpsilon -> str"eps" let subst_path_atom subst p = match p with @@ -429,7 +462,9 @@ module Hint_db = struct else List.exists (matches_mode args) modes let merge_entry db nopat pat = - let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in + let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in + let h = List.merge pri_order_int h nopat in + let h = List.merge pri_order_int h pat in List.map realize_tac h let map_none db = @@ -473,15 +508,14 @@ module Hint_db = struct let idv = id, v in let k = match gr with | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && - is_unfold v.code then None else Some gr + is_unfold v.code.obj then None else Some gr | None -> None in let dnst = if db.use_dn then Some db.hintdb_state else None in - let pat = if not db.use_dn && is_exact v.code then None else v.pat in + let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in match k with | None -> - (** ppedrot: this equality here is dubious. Maybe we can remove it? *) - let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in + let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in if not (List.exists is_present db.hintdb_nopat) then (** FIXME *) { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat } @@ -497,10 +531,10 @@ module Hint_db = struct in List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat - let add_one (k, v) db = - let v = instantiate_hint v in + let add_one env sigma (k, v) db = + let v = instantiate_hint env sigma v in let st',db,rebuild = - match v.code with + match v.code.obj with | Unfold_nth egr -> let addunf (ids,csts) (ids',csts') = match egr with @@ -515,7 +549,7 @@ module Hint_db = struct let db, id = next_hint_id db in addkv k id v db - let add_list l db = List.fold_left (fun db k -> add_one k db) db l + let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l let remove_sdl p sdl = List.smartfilter p sdl @@ -534,7 +568,9 @@ module Hint_db = struct let remove_one gr db = remove_list [gr] db - let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat) + let get_entry se = + let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in + List.map realize_tac h let iter f db = let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in @@ -586,6 +622,7 @@ let auto_init_db = Hintdbmap.empty) let searchtable : hint_db_table = ref auto_init_db +let statustable = ref KNmap.empty let searchtable_map name = Hintdbmap.find name !searchtable @@ -598,7 +635,7 @@ let current_pure_db () = List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable)) let error_no_such_hint_database x = - error ("No such Hint database: "^x^".") + errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".") (**************************************************************************) (* Definition of the summary *) @@ -609,9 +646,10 @@ let add_hints_init f = let init = !hints_init in hints_init := (fun () -> init (); f ()) -let init () = searchtable := auto_init_db; !hints_init () -let freeze _ = !searchtable -let unfreeze fs = searchtable := fs +let init () = + searchtable := auto_init_db; statustable := KNmap.empty; !hints_init () +let freeze _ = (!searchtable, !statustable) +let unfreeze (fs, st) = searchtable := fs; statustable := st let _ = Summary.declare_summary "search" { Summary.freeze_function = freeze; @@ -632,6 +670,8 @@ let try_head_pattern c = try head_pattern_bound c with BoundPattern -> error "Bound head variable." +let with_uid c = { obj = c; uid = fresh_key () } + let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = let cty = strip_outer_cast cty in match kind_of_term cty with @@ -647,7 +687,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = poly = poly; pat = Some pat; name = name; - code = Give_exact (c, cty, ctx) }) + code = with_uid (Give_exact (c, cty, ctx)); }) let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in @@ -667,7 +707,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; - code = Res_pf(c,cty,ctx) }) + code = with_uid (Res_pf(c,cty,ctx)); }) else begin if not eapply then failwith "make_apply_entry"; if verbose then @@ -678,7 +718,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, poly = poly; pat = Some pat; name = name; - code = ERes_pf(c,cty,ctx) }) + code = with_uid (ERes_pf(c,cty,ctx)); }) end | _ -> failwith "make_apply_entry" @@ -724,7 +764,7 @@ let make_unfold eref = poly = false; pat = None; name = PathHints [g]; - code = Unfold_nth eref }) + code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = let hdconstr = Option.map try_head_pattern pat in @@ -733,7 +773,7 @@ let make_extern pri pat tacast = poly = false; pat = pat; name = PathAny; - code = Extern tacast }) + code = with_uid (Extern tacast) }) let make_mode ref m = let ty = Global.type_of_global_unsafe ref in @@ -749,14 +789,14 @@ let make_mode ref m = let make_trivial env sigma poly ?(name=PathAny) r = let c,ctx = fresh_global_or_constr env sigma poly r in let sigma = Evd.merge_context_set univ_flexible sigma ctx in - let t = hnf_constr env sigma (type_of env sigma c) in + let t = hnf_constr env sigma (unsafe_type_of env sigma c) in let hd = head_of_constr_reference (head_constr t) in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); name = name; - code=Res_pf_THEN_trivial_fail(c,t,ctx) }) + code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -771,9 +811,19 @@ let get_db dbname = try searchtable_map dbname with Not_found -> Hint_db.empty empty_transparent_state false -let add_hint dbname hintlist = +let add_hint dbname hintlist = + let check (_, h) = + let () = if KNmap.mem h.code.uid !statustable then + error "Conflicting hint keys. This can happen when including \ + twice the same module." + in + statustable := KNmap.add h.code.uid false !statustable + in + let () = List.iter check hintlist in let db = get_db dbname in - let db' = Hint_db.add_list hintlist db in + let env = Global.env () in + let sigma = Evd.from_env env in + let db' = Hint_db.add_list env sigma hintlist db in searchtable_add (dbname,db') let add_transparency dbname grs b = @@ -816,7 +866,7 @@ type hint_obj = { hint_action : hint_action; } -let cache_autohint (_, h) = +let load_autohint _ (kn, h) = let name = h.hint_name in match h.hint_action with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b) @@ -826,6 +876,16 @@ let cache_autohint (_, h) = | AddCut path -> add_cut name path | AddMode (l, m) -> add_mode name l m +let open_autohint i (kn, h) = + if Int.equal i 1 then match h.hint_action with + | AddHints hints -> + let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in + List.iter add hints + | _ -> () + +let cache_autohint (kn, obj) = + load_autohint 1 (kn, obj); open_autohint 1 (kn, obj) + let subst_autohint (subst, obj) = let subst_key gr = let (lab'', elab') = subst_global subst gr in @@ -837,34 +897,36 @@ let subst_autohint (subst, obj) = let subst_hint (k,data as hint) = let k' = Option.smartmap subst_key k in let pat' = Option.smartmap (subst_pattern subst) data.pat in - let code' = match data.code with + let code' = match data.code.obj with | Res_pf (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'==t then data.code else Res_pf (c', t',ctx) + if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx) | ERes_pf (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'==t then data.code else ERes_pf (c',t',ctx) + if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx) | Give_exact (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t'== t then data.code else Give_exact (c',t',ctx) + if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx) | Res_pf_THEN_trivial_fail (c,t,ctx) -> let c' = subst_mps subst c in let t' = subst_mps subst t in - if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t',ctx) + if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx) | Unfold_nth ref -> let ref' = subst_evaluable_reference subst ref in - if ref==ref' then data.code else Unfold_nth ref' + if ref==ref' then data.code.obj else Unfold_nth ref' | Extern tac -> let tac' = Tacsubst.subst_tactic subst tac in - if tac==tac' then data.code else Extern tac' + if tac==tac' then data.code.obj else Extern tac' in let name' = subst_path_atom subst data.name in + let uid' = subst_kn subst data.code.uid in let data' = - if data.pat==pat' && data.name == name' && data.code==code' then data - else { data with pat = pat'; name = name'; code = code' } + if data.code.uid == uid' && data.pat == pat' && + data.name == name' && data.code.obj == code' then data + else { data with pat = pat'; name = name'; code = { obj = code'; uid = uid' } } in if k' == k && data' == data then hint else (k',data') in @@ -896,7 +958,8 @@ let classify_autohint obj = let inAutoHint : hint_obj -> obj = declare_object {(default_object "AUTOHINT") with cache_function = cache_autohint; - load_function = (fun _ -> cache_autohint); + load_function = load_autohint; + open_function = open_autohint; subst_function = subst_autohint; classify_function = classify_autohint; } @@ -999,7 +1062,7 @@ let default_prepare_hint_ident = Id.of_string "H" exception Found of constr * types -let prepare_hint check env init (sigma,c) = +let prepare_hint check (poly,local) env init (sigma,c) = let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in (* We re-abstract over uninstantiated evars. It is actually a bit stupid to generalize over evars since the first @@ -1012,7 +1075,7 @@ let prepare_hint check env init (sigma,c) = (* We skip the test whether args is the identity or not *) let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in - if not (Int.Set.is_empty (free_rels t)) then + if not (closed0 c) then error "Hints with holes dependent on a bound variable not supported."; if occur_existential t then (* Not clever enough to construct dependency graph of evars *) @@ -1029,13 +1092,18 @@ let prepare_hint check env init (sigma,c) = let c' = iter c in if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in - IsConstr (c', diff) + if poly then IsConstr (c', diff) + else if local then IsConstr (c', diff) + else (Global.push_context_set false diff; + IsConstr (c', Univ.ContextSet.empty)) let interp_hints poly = fun h -> - let f c = - let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in - prepare_hint true (Global.env()) Evd.empty (evd,c) in + let env = (Global.env()) in + let sigma = Evd.from_env env in + let f poly c = + let evd,c = Constrintern.interp_open_constr env sigma c in + prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in let fref r = let gr = global_with_alias r in Dumpglob.add_glob (loc_of_reference r) gr; @@ -1048,7 +1116,7 @@ let interp_hints poly = | HintsReference c -> let gr = global_with_alias c in (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> (PathAny, poly, f c) + | HintsConstr c -> (PathAny, poly, f poly c) in let fres (pri, b, r) = let path, poly, gr = fi r in @@ -1083,7 +1151,8 @@ let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then error "The hint database \"nocore\" is meant to stay empty."; let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames @@ -1103,7 +1172,7 @@ let expand_constructor_hints env sigma lems = (fun i -> IsConstr (mkConstructU ((ind,i+1),u), Univ.ContextSet.empty)) | _ -> - [prepare_hint false env sigma (evd,lem)]) lems + [prepare_hint false (false,true) env sigma (evd,lem)]) lems (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) @@ -1111,8 +1180,8 @@ let expand_constructor_hints env sigma lems = let add_hint_lemmas env sigma eapply lems hint_db = let lems = expand_constructor_hints env sigma lems in let hintlist' = - List.map_append (make_resolves env sigma (eapply,true,false) None true) lems in - Hint_db.add_list hintlist' hint_db + List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in + Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = let sign = Environ.named_context env in @@ -1122,7 +1191,7 @@ let make_local_hint_db env sigma ts eapply lems = in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in add_hint_lemmas env sigma eapply lems - (Hint_db.add_list hintlist (Hint_db.empty ts false)) + (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) let make_local_hint_db = if Flags.profile then @@ -1146,13 +1215,14 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_autotactic = - function - | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c) - | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c) - | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c) - | Res_pf_THEN_trivial_fail (c,clenv) -> - (str"apply " ++ pr_constr c ++ str" ; trivial") +let pr_hint_elt (c, _, _) = pr_constr c + +let pr_hint h = match h.obj with + | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c) + | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c) + | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c) + | Res_pf_THEN_trivial_fail (c, _) -> + (str"apply " ++ pr_hint_elt c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> let env = @@ -1163,11 +1233,11 @@ let pr_autotactic = in (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) -let pr_hint (id, v) = - (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) +let pr_id_hint (id, v) = + (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) let pr_hint_list hintlist = - (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ()) + (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) let pr_hints_db (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ @@ -1266,3 +1336,27 @@ let pr_searchtable () = in Hintdbmap.fold fold !searchtable (mt ()) +let print_mp mp = + try + let qid = Nametab.shortest_qualid_of_module mp in + str " from " ++ pr_qualid qid + with Not_found -> mt () + +let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true + +let warn h x = + let hint = pr_hint h in + let (mp, _, _) = KerName.repr h.uid in + let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in + Proofview.tclUNIT x + +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) +| `STRICT -> + if is_imported tac then k tac.obj + else Proofview.tclZERO (UserError ("", (str "Tactic failure."))) + +let repr_hint h = h.obj |