diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 508 |
1 files changed, 339 insertions, 169 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 42e5067c..9a96b738 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -8,7 +8,7 @@ open Pp open Util -open Errors +open CErrors open Names open Vars open Term @@ -33,6 +33,8 @@ open Pfedit open Tacred open Printer open Vernacexpr +open Sigma.Notations +open Context.Named.Declaration (****************************************) (* General functions *) @@ -64,6 +66,28 @@ let decompose_app_bound t = | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args | _ -> raise Bound +(** Compute the set of section variables that remain in the named context. + Starts from the top to the bottom of the context, stops at the first + different declaration between the named hyps and the section context. *) +let secvars_of_hyps hyps = + let secctx = Global.named_context () in + let pred, all = + List.fold_left (fun (pred,all) decl -> + try let _ = Context.Named.lookup (get_id decl) hyps in + (* Approximation, it might be an hypothesis reintroduced with same name and unconvertible types, + we must allow it currently, as comparing the declarations for syntactic equality is too + strong a check (e.g. an unfold in a section variable would make it unusable). *) + (Id.Pred.add (get_id decl) pred, all) + with Not_found -> (pred, false)) + (Id.Pred.empty,true) secctx + in + if all then Id.Pred.full (* If the whole section context is available *) + else pred + +let empty_hint_info = + let open Vernacexpr in + { hint_priority = None; hint_pattern = None } + (************************************************************************) (* The Type of Constructions Autotactic Hints *) (************************************************************************) @@ -74,20 +98,27 @@ type 'a hint_ast = | Give_exact of 'a | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *) | Unfold_nth of evaluable_global_reference (* Hint Unfold *) - | Extern of glob_tactic_expr (* Hint Extern *) + | Extern of Genarg.glob_generic_argument (* Hint Extern *) -type hints_path_atom = - | PathHints of global_reference list + +type 'a hints_path_atom_gen = + | PathHints of 'a list + (* For forward hints, their names is the list of projections *) | PathAny -type hints_path = - | PathAtom of hints_path_atom - | PathStar of hints_path - | PathSeq of hints_path * hints_path - | PathOr of hints_path * hints_path +type hints_path_atom = global_reference hints_path_atom_gen + +type 'a hints_path_gen = + | PathAtom of 'a hints_path_atom_gen + | PathStar of 'a hints_path_gen + | PathSeq of 'a hints_path_gen * 'a hints_path_gen + | PathOr of 'a hints_path_gen * 'a hints_path_gen | PathEmpty | PathEpsilon +type pre_hints_path = Libnames.reference hints_path_gen +type hints_path = global_reference hints_path_gen + type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set @@ -102,11 +133,13 @@ type raw_hint = constr * types * Univ.universe_context_set 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 *) + 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 *) + db : string option; (** The database from which the hint comes *) + secvars : Id.Pred.t; (* The set of section variables the hint depends on *) + code : 'a; (* the tactic to apply when the concl matches pat *) } type full_hint = hint with_metadata @@ -153,27 +186,6 @@ let fresh_key = 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 -| PathAny, PathAny -> true -| (PathHints _ | PathAny), _ -> false - -let eq_auto_tactic t1 t2 = match t1, t2 with -| Res_pf (c1, _), Res_pf (c2, _) -> Constr.equal c1 c2 -| ERes_pf (c1, _), ERes_pf (c2, _) -> Constr.equal c1 c2 -| Give_exact (c1, _), Give_exact (c2, _) -> Constr.equal c1 c2 -| Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> Constr.equal c1 c2 -| Unfold_nth gr1, Unfold_nth gr2 -> eq_egr gr1 gr2 -| Extern tac1, Extern tac2 -> tac1 == tac2 (** May cause redundancy in addkv *) -| (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _ - | Unfold_nth _ | Extern _), _ -> false - -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 && - eq_auto_tactic t1.code t2.code - let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) = let d = pri1 - pri2 in if Int.equal d 0 then id2 - id1 @@ -208,7 +220,7 @@ type search_entry = { sentry_nopat : stored_data list; sentry_pat : stored_data list; sentry_bnet : Bounded_net.t; - sentry_mode : bool array list; + sentry_mode : hint_mode array list; } let empty_se = { @@ -336,6 +348,12 @@ let rec is_empty = function | PathEmpty -> true | PathEpsilon -> false +let path_seq p p' = + match p, p' with + | PathEpsilon, p' -> p' + | p, PathEpsilon -> p + | p, p' -> PathSeq (p, p') + let rec path_derivate hp hint = let rec derivate_atoms hints hints' = match hints, hints' with @@ -343,26 +361,26 @@ let rec path_derivate hp hint = | [], [] -> PathEpsilon | [], hints -> PathEmpty | grs, [] -> PathAtom (PathHints grs) - | _, _ -> PathEmpty + | _, _ -> PathEmpty in - match hp with - | PathAtom PathAny -> PathEpsilon - | PathAtom (PathHints grs) -> - (match grs, hint with - | h :: hints, PathAny -> PathEmpty - | hints, PathHints hints' -> derivate_atoms hints hints' - | _, _ -> assert false) - | PathStar p -> if path_matches p [hint] then hp else PathEpsilon - | PathSeq (hp, hp') -> - let hpder = path_derivate hp hint in - if matches_epsilon hp then - PathOr (PathSeq (hpder, hp'), path_derivate hp' hint) - else if is_empty hpder then PathEmpty - else PathSeq (hpder, hp') - | PathOr (hp, hp') -> - PathOr (path_derivate hp hint, path_derivate hp' hint) - | PathEmpty -> PathEmpty - | PathEpsilon -> PathEmpty + match hp with + | PathAtom PathAny -> PathEpsilon + | PathAtom (PathHints grs) -> + (match grs, hint with + | h :: _, PathAny -> PathEmpty + | hints, PathHints hints' -> derivate_atoms hints hints' + | _, _ -> assert false) + | PathStar p -> if path_matches p [hint] then hp else PathEpsilon + | PathSeq (hp, hp') -> + let hpder = path_derivate hp hint in + if matches_epsilon hp then + PathOr (path_seq hpder hp', path_derivate hp' hint) + else if is_empty hpder then PathEmpty + else path_seq hpder hp' + | PathOr (hp, hp') -> + PathOr (path_derivate hp hint, path_derivate hp' hint) + | PathEmpty -> PathEmpty + | PathEpsilon -> PathEmpty let rec normalize_path h = match h with @@ -382,19 +400,40 @@ let rec normalize_path h = let path_derivate hp hint = normalize_path (path_derivate hp hint) -let pp_hints_path_atom a = +let pp_hints_path_atom prg a = match a with - | PathAny -> str"*" - | PathHints grs -> pr_sequence pr_global grs - -let rec pp_hints_path = function - | 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 ")" + | PathAny -> str"_" + | PathHints grs -> pr_sequence prg grs + +let pp_hints_path_gen prg = + let rec aux = function + | PathAtom pa -> pp_hints_path_atom prg pa + | PathStar (PathAtom PathAny) -> str"_*" + | PathStar p -> str "(" ++ aux p ++ str")*" + | PathSeq (p, p') -> aux p ++ spc () ++ aux p' + | PathOr (p, p') -> + str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++ + aux p' ++ str ")" | PathEmpty -> str"emp" | PathEpsilon -> str"eps" + in aux + +let pp_hints_path = pp_hints_path_gen pr_global + +let glob_hints_path_atom p = + match p with + | PathHints g -> PathHints (List.map Nametab.global g) + | PathAny -> PathAny + +let glob_hints_path = + let rec aux = function + | PathAtom pa -> PathAtom (glob_hints_path_atom pa) + | PathStar p -> PathStar (aux p) + | PathSeq (p, p') -> PathSeq (aux p, aux p') + | PathOr (p, p') -> PathOr (aux p, aux p') + | PathEmpty -> PathEmpty + | PathEpsilon -> PathEpsilon + in aux let subst_path_atom subst p = match p with @@ -421,7 +460,38 @@ let rec subst_hints_path subst hp = if p' == p && q' == q then hp else PathOr (p', q') | _ -> hp -module Hint_db = struct +type hint_db_name = string + +module Hint_db : +sig +type t +val empty : ?name:hint_db_name -> transparent_state -> bool -> t +val find : global_reference -> t -> search_entry +val map_none : secvars:Id.Pred.t -> t -> full_hint list +val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list +val map_existential : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list +val map_eauto : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list +val map_auto : secvars:Id.Pred.t -> + (global_reference * constr array) -> constr -> t -> full_hint list +val add_one : env -> evar_map -> hint_entry -> t -> t +val add_list : env -> evar_map -> hint_entry list -> t -> t +val remove_one : global_reference -> t -> t +val remove_list : global_reference list -> t -> t +val iter : (global_reference option -> hint_mode array list -> full_hint list -> unit) -> t -> unit +val use_dn : t -> bool +val transparent_state : t -> transparent_state +val set_transparent_state : t -> transparent_state -> t +val add_cut : hints_path -> t -> t +val add_mode : global_reference -> hint_mode array -> t -> t +val cut : t -> hints_path +val unfolds : t -> Id.Set.t * Cset.t +val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> + t -> 'a -> 'a + +end = +struct type t = { hintdb_state : Names.transparent_state; @@ -432,69 +502,83 @@ module Hint_db = struct hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant or with no associated pattern. *) - hintdb_nopat : (global_reference option * stored_data) list + hintdb_nopat : (global_reference option * stored_data) list; + hintdb_name : string option; } let next_hint_id db = let h = db.hintdb_max_id in { db with hintdb_max_id = succ db.hintdb_max_id }, h - let empty st use_dn = { hintdb_state = st; + let empty ?name st use_dn = { hintdb_state = st; hintdb_cut = PathEmpty; hintdb_unfolds = (Id.Set.empty, Cset.empty); hintdb_max_id = 0; use_dn = use_dn; hintdb_map = Constr_map.empty; - hintdb_nopat = [] } + hintdb_nopat = []; + hintdb_name = name; } let find key db = try Constr_map.find key db.hintdb_map with Not_found -> empty_se - let realize_tac (id,tac) = tac - + let realize_tac secvars (id,tac) = + if Id.Pred.subset tac.secvars secvars then Some tac + else + (** Warn about no longer typable hint? *) + None + + let match_mode m arg = + match m with + | ModeInput -> not (occur_existential arg) + | ModeNoHeadEvar -> + Evarutil.(try ignore(head_evar arg); false + with NoHeadEvar -> true) + | ModeOutput -> true + let matches_mode args mode = - Array.length args == Array.length mode && - Array.for_all2 (fun arg m -> not (m && occur_existential arg)) args mode + Array.length mode == Array.length args && + Array.for_all2 match_mode mode args let matches_modes args modes = if List.is_empty modes then true else List.exists (matches_mode args) modes - let merge_entry db nopat pat = + let merge_entry secvars db nopat pat = 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 + List.map_filter (realize_tac secvars) h - let map_none db = - merge_entry db [] [] + let map_none ~secvars db = + merge_entry secvars db [] [] - let map_all k db = + let map_all ~secvars k db = let se = find k db in - merge_entry db se.sentry_nopat se.sentry_pat + merge_entry secvars db se.sentry_nopat se.sentry_pat (** Precondition: concl has no existentials *) - let map_auto (k,args) concl db = + let map_auto ~secvars (k,args) concl db = let se = find k db in let st = if db.use_dn then (Some db.hintdb_state) else None in let pat = lookup_tacs concl st se in - merge_entry db [] pat + merge_entry secvars db [] pat - let map_existential (k,args) concl db = + let map_existential ~secvars (k,args) concl db = let se = find k db in if matches_modes args se.sentry_mode then - merge_entry db se.sentry_nopat se.sentry_pat - else merge_entry db [] [] + merge_entry secvars db se.sentry_nopat se.sentry_pat + else merge_entry secvars db [] [] (* [c] contains an existential *) - let map_eauto (k,args) concl db = + let map_eauto ~secvars (k,args) concl db = let se = find k db in if matches_modes args se.sentry_mode then let st = if db.use_dn then Some db.hintdb_state else None in let pat = lookup_tacs concl st se in - merge_entry db [] pat - else merge_entry db [] [] + merge_entry secvars db [] pat + else merge_entry secvars db [] [] let is_exact = function | Give_exact _ -> true @@ -505,7 +589,7 @@ module Hint_db = struct | _ -> false let addkv gr id v db = - let idv = id, v in + let idv = id, { v with db = db.hintdb_name } in let k = match gr with | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr && is_unfold v.code.obj then None else Some gr @@ -570,11 +654,11 @@ module Hint_db = struct let get_entry se = let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in - List.map realize_tac h + List.map snd h let iter f db = let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in - f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat); + f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat); Constr_map.iter iter_se db.hintdb_map let fold f db accu = @@ -609,8 +693,6 @@ type hint_db = Hint_db.t type hint_db_table = hint_db Hintdbmap.t ref -type hint_db_name = string - (** Initially created hint databases, for typeclasses and rewrite *) let typeclasses_db = "typeclass_instances" @@ -631,8 +713,7 @@ let searchtable_add (name,db) = let current_db_names () = Hintdbmap.domain !searchtable let current_db () = Hintdbmap.bindings !searchtable -let current_pure_db () = - List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable)) +let current_pure_db () = List.map snd (current_db ()) let error_no_such_hint_database x = errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".") @@ -672,7 +753,20 @@ let try_head_pattern c = let with_uid c = { obj = c; uid = fresh_key () } -let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = +let secvars_of_idset s = + Id.Set.fold (fun id p -> + if is_section_variable id then + Id.Pred.add id p + else p) s Id.Pred.empty + +let secvars_of_constr env c = + secvars_of_idset (global_vars_set env c) + +let secvars_of_global env gr = + secvars_of_idset (vars_of_global_reference env gr) + +let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = + let secvars = secvars_of_constr env c in let cty = strip_outer_cast cty in match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" @@ -682,14 +776,17 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" in - (Some hd, - { pri = (match pri with None -> 0 | Some p -> p); - poly = poly; - pat = Some pat; - name = name; - code = with_uid (Give_exact (c, cty, ctx)); }) + let pri = match info.hint_priority with None -> 0 | Some p -> p in + let pat = match info.hint_pattern with + | Some pat -> snd pat + | None -> pat + in + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; secvars; + 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 make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) = let cty = if hnf then hnf_constr env sigma cty else cty in match kind_of_term cty with | Prod _ -> @@ -701,23 +798,25 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in let nmiss = List.length (clenv_missing ce) in + let secvars = secvars_of_constr env c in + let pri = match info.hint_priority with None -> nb_hyp cty + nmiss | Some p -> p in + let pat = match info.hint_pattern with + | Some p -> snd p | None -> pat + in if Int.equal nmiss 0 then (Some hd, - { pri = (match pri with None -> nb_hyp cty | Some p -> p); - poly = poly; - pat = Some pat; - name = name; + { pri; poly; pat = Some pat; name; + db = None; + secvars; code = with_uid (Res_pf(c,cty,ctx)); }) else begin if not eapply then failwith "make_apply_entry"; if verbose then - msg_warning (str "the hint: eapply " ++ pr_lconstr c ++ + Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); (Some hd, - { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); - poly = poly; - pat = Some pat; - name = name; + { pri; poly; pat = Some pat; name; + db = None; secvars; code = with_uid (ERes_pf(c,cty,ctx)); }) end | _ -> failwith "make_apply_entry" @@ -726,18 +825,56 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, c is a constr cty is the type of constr *) -let fresh_global_or_constr env sigma poly cr = - match cr with - | IsGlobRef gr -> Universes.fresh_global_instance env gr - | IsConstr (c, ctx) -> (c, ctx) +let pr_hint_term env sigma ctx = function + | IsGlobRef gr -> pr_global gr + | IsConstr (c, ctx) -> + let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in + pr_constr_env env sigma c + +(** We need an object to record the side-effect of registering + global universes associated with a hint. *) +let cache_context_set (_,c) = + Global.push_context_set false c + +let input_context_set : Univ.ContextSet.t -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Global universe context") with + cache_function = cache_context_set; + load_function = (fun _ -> cache_context_set); + discharge_function = (fun (_,a) -> Some a); + classify_function = (fun a -> Keep a) } + +let warn_polymorphic_hint = + CWarnings.create ~name:"polymorphic-hint" ~category:"automation" + (fun hint -> strbrk"Using polymorphic hint " ++ hint ++ + str" monomorphically" ++ + strbrk" use Polymorphic Hint to use it polymorphically.") -let make_resolves env sigma flags pri poly ?name cr = +let fresh_global_or_constr env sigma poly cr = + let isgr, (c, ctx) = + match cr with + | IsGlobRef gr -> + true, Universes.fresh_global_instance env gr + | IsConstr (c, ctx) -> false, (c, ctx) + in + if poly then (c, ctx) + else if Univ.ContextSet.is_empty ctx then (c, ctx) + else begin + if isgr then + warn_polymorphic_hint (pr_hint_term env sigma ctx cr); + Lib.add_anonymous_leaf (input_context_set ctx); + (c, Univ.ContextSet.empty) + end + +let make_resolves env sigma flags info poly ?name cr = let c, ctx = fresh_global_or_constr env sigma poly cr in let cty = Retyping.get_type_of env sigma c in let try_apply f = try Some (f (c, cty, ctx)) with Failure _ -> None in let ents = List.map_filter try_apply - [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name] + [make_exact_entry env sigma info poly ?name; + make_apply_entry env sigma flags info poly ?name] in if List.is_empty ents then errorlabstrm "Hint" @@ -747,16 +884,19 @@ let make_resolves env sigma flags pri poly ?name cr = ents (* used to add an hypothesis to the local hint database *) -let make_resolve_hyp env sigma (hname,_,htyp) = +let make_resolve_hyp env sigma decl = + let hname = get_id decl in + let c = mkVar hname in try - [make_apply_entry env sigma (true, true, false) None false + [make_apply_entry env sigma (true, true, false) empty_hint_info false ~name:(PathHints [VarRef hname]) - (mkVar hname, htyp, Univ.ContextSet.empty)] + (c, get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") (* REM : in most cases hintname = id *) + let make_unfold eref = let g = global_of_evaluable_reference eref in (Some g, @@ -764,15 +904,20 @@ let make_unfold eref = poly = false; pat = None; name = PathHints [g]; + db = None; + secvars = secvars_of_global (Global.env ()) g; code = with_uid (Unfold_nth eref) }) let make_extern pri pat tacast = + let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri = pri; poly = false; pat = pat; name = PathAny; + db = None; + secvars = Id.Pred.empty; (* Approximation *) code = with_uid (Extern tacast) }) let make_mode ref m = @@ -796,6 +941,8 @@ let make_trivial env sigma poly ?(name=PathAny) r = poly = poly; pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce)); name = name; + db = None; + secvars = secvars_of_constr env c; code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -809,7 +956,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let get_db dbname = try searchtable_map dbname - with Not_found -> Hint_db.empty empty_transparent_state false + with Not_found -> Hint_db.empty ~name:dbname empty_transparent_state false let add_hint dbname hintlist = let check (_, h) = @@ -848,7 +995,7 @@ type hint_action = | AddHints of hint_entry list | RemoveHints of global_reference list | AddCut of hints_path - | AddMode of global_reference * bool array + | AddMode of global_reference * hint_mode array let add_cut dbname path = let db = get_db dbname in @@ -869,7 +1016,7 @@ type hint_obj = { 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) + | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b) | AddTransparency (grs, b) -> add_transparency name grs b | AddHints hints -> add_hint name hints | RemoveHints grs -> remove_hint name grs @@ -918,7 +1065,7 @@ let subst_autohint (subst, obj) = let ref' = subst_evaluable_reference subst ref in if ref==ref' then data.code.obj else Unfold_nth ref' | Extern tac -> - let tac' = Tacsubst.subst_tactic subst tac in + let tac' = Genintern.generic_substitute subst tac in if tac==tac' then data.code.obj else Extern tac' in let name' = subst_path_atom subst data.name in @@ -1025,16 +1172,17 @@ let add_transparency l b local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_extern pri pat tacast local dbname = - let pat = match pat with +let add_extern info tacast local dbname = + let pat = match info.hint_pattern with | None -> None | Some (_, pat) -> Some pat in - let hint = make_hint ~local dbname (AddHints [make_extern pri pat tacast]) in + let hint = make_hint ~local dbname + (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in Lib.add_anonymous_leaf (inAutoHint hint) -let add_externs pri pat tacast local dbnames = - List.iter (add_extern pri pat tacast local) dbnames +let add_externs info tacast local dbnames = + List.iter (add_extern info tacast local) dbnames let add_trivials env sigma l local dbnames = List.iter @@ -1048,15 +1196,16 @@ let (forward_intern_tac, extern_intern_tac) = Hook.make () type hnf = bool +type hint_info = (patvar list * constr_pattern) hint_info_gen + type hints_entry = - | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list + | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * bool list - | HintsExternEntry of - int * (patvar list * constr_pattern) option * glob_tactic_expr + | HintsModeEntry of global_reference * hint_mode list + | HintsExternEntry of hint_info * glob_tactic_expr let default_prepare_hint_ident = Id.of_string "H" @@ -1064,10 +1213,12 @@ exception Found of constr * types 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. + (* We re-abstract over uninstantiated evars and universes. It is actually a bit stupid to generalize over evars since the first thing make_resolves will do is to re-instantiate the products *) - let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in + let sigma, subst = Evd.nf_univ_variables sigma in + let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in + let c = drop_extra_implicit_args c in let vars = ref (collect_vars c) in let subst = ref [] in let rec find_next_evar c = match kind_of_term c with @@ -1081,7 +1232,7 @@ let prepare_hint check (poly,local) env init (sigma,c) = (* Not clever enough to construct dependency graph of evars *) error "Not clever enough to deal with evars dependent in other evars."; raise (Found (c,t)) - | _ -> iter_constr find_next_evar c in + | _ -> Constr.iter find_next_evar c in let rec iter c = try find_next_evar c; c with Found (evar,t) -> @@ -1090,11 +1241,11 @@ let prepare_hint check (poly,local) env init (sigma,c) = subst := (evar,mkVar id)::!subst; mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in let c' = iter c in - if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c'; + if check then Pretyping.check_evars (Global.env()) Evd.empty sigma c'; let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in if poly then IsConstr (c', diff) else if local then IsConstr (c', diff) - else (Global.push_context_set false diff; + else (Lib.add_anonymous_leaf (input_context_set diff); IsConstr (c', Univ.ContextSet.empty)) let interp_hints poly = @@ -1118,11 +1269,12 @@ let interp_hints poly = (PathHints [gr], poly, IsGlobRef gr) | HintsConstr c -> (PathAny, poly, f poly c) in - let fres (pri, b, r) = + let fp = Constrintern.intern_constr_pattern (Global.env()) in + let fres (info, b, r) = let path, poly, gr = fi r in - (pri, poly, b, path, gr) + let info = { info with hint_pattern = Option.map fp info.hint_pattern } in + (info, poly, b, path, gr) in - let fp = Constrintern.intern_constr_pattern (Global.env()) in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) @@ -1138,14 +1290,14 @@ let interp_hints poly = List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - None, mib.Declarations.mind_polymorphic, true, + empty_hint_info, mib.Declarations.mind_polymorphic, true, PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> let pat = Option.map fp patcom in let l = match pat with None -> [] | Some (l, _) -> l in let tacexp = Hook.get forward_intern_tac l tacexp in - HintsExternEntry (pri, pat, tacexp) + HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then @@ -1161,29 +1313,41 @@ let add_hints local dbnames0 h = | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames | HintsTransparencyEntry (lhints, b) -> add_transparency lhints b local dbnames - | HintsExternEntry (pri, pat, tacexp) -> - add_externs pri pat tacexp local dbnames + | HintsExternEntry (info, tacexp) -> + add_externs info tacexp local dbnames let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> match kind_of_term lem with | Ind (ind,u) -> List.init (nconstructors ind) - (fun i -> IsConstr (mkConstructU ((ind,i+1),u), - Univ.ContextSet.empty)) + (fun i -> + let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd) + (Evd.universe_context_set sigma) in + not (Univ.ContextSet.is_empty ctx), + IsConstr (mkConstructU ((ind,i+1),u),ctx)) | _ -> - [prepare_hint false (false,true) env sigma (evd,lem)]) lems - + [match prepare_hint false (false,true) env sigma (evd,lem) with + | IsConstr (c, ctx) -> + not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx) + | IsGlobRef _ -> assert false (* Impossible return value *) ]) lems (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *) 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 false) lems in + List.map_append (fun (poly, lem) -> + make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems in Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = + let map c = + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (c, sigma, _) = c.delayed env sigma in + (Sigma.to_evar_map sigma, c) + in + let lems = List.map map lems in let sign = Environ.named_context env in let ts = match ts with | None -> Hint_db.transparent_state (searchtable_map "core") @@ -1193,12 +1357,6 @@ let make_local_hint_db env sigma ts eapply lems = add_hint_lemmas env sigma eapply lems (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) -let make_local_hint_db = - if Flags.profile then - let key = Profile.declare_profile "make_local_hint_db" in - Profile.profile4 key make_local_hint_db - else make_local_hint_db - let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems @@ -1218,23 +1376,25 @@ let make_db_list dbnames = 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) + | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c) + | ERes_pf (c, _) -> (str"simple 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") + (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial") | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) | Extern tac -> let env = try let (_, env) = Pfedit.get_current_goal_context () in env - with e when Errors.noncritical e -> Global.env () + with e when CErrors.noncritical e -> Global.env () in - (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac) + (str "(*external*) " ++ Pptactic.pr_glb_generic env tac) let pr_id_hint (id, v) = - (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ()) + let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in + (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat + ++ str", id " ++ int id ++ str ")" ++ spc ()) let pr_hint_list hintlist = (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ()) @@ -1248,7 +1408,7 @@ let pr_hints_db (name,db,hintlist) = let pr_hint_list_for_head c = let dbs = current_db () in let validate (name, db) = - let hints = List.map (fun v -> 0, v) (Hint_db.map_all c db) in + let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in (name, db, hints) in let valid_dbs = List.map validate dbs in @@ -1270,9 +1430,9 @@ let pr_hint_term cl = let fn = try let hdc = decompose_app_bound cl in if occur_existential cl then - Hint_db.map_existential hdc cl - else Hint_db.map_auto hdc cl - with Bound -> Hint_db.map_none + Hint_db.map_existential ~secvars:Id.Pred.full hdc cl + else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl + with Bound -> Hint_db.map_none ~secvars:Id.Pred.full in let fn db = List.map (fun x -> 0, x) (fn db) in List.map (fun (name, db) -> (name, db, fn db)) dbs @@ -1290,13 +1450,18 @@ let pr_applicable_hint () = let pts = get_pftreestate () in let glss = Proof.V82.subgoals pts in match glss.Evd.it with - | [] -> Errors.error "No focused goal." + | [] -> CErrors.error "No focused goal." | g::_ -> pr_hint_term (Goal.V82.concl glss.Evd.sigma g) +let pp_hint_mode = function + | ModeInput -> str"+" + | ModeNoHeadEvar -> str"!" + | ModeOutput -> str"-" + (* displays the whole hint database db *) let pr_hint_db db = - let pr_mode = prvect_with_sep spc (fun x -> if x then str"+" else str"-") in + let pr_mode = prvect_with_sep spc pp_hint_mode in let pr_modes l = if List.is_empty l then mt () else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")" @@ -1344,10 +1509,15 @@ let print_mp mp = let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true +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 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 + warn_non_imported_hint (hint,mp); Proofview.tclUNIT x let run_hint tac k = match !warn_hint with |