diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 421 |
1 files changed, 227 insertions, 194 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 9a96b738..500abc5b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1,17 +1,21 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp open Util open CErrors open Names -open Vars open Term +open Evd +open EConstr +open Vars open Environ open Mod_subst open Globnames @@ -20,45 +24,49 @@ open Namegen open Libnames open Smartlocate open Misctypes -open Evd open Termops open Inductiveops open Typing -open Tacexpr open Decl_kinds open Pattern open Patternops open Clenv -open Pfedit open Tacred open Printer open Vernacexpr -open Sigma.Notations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (****************************************) (* General functions *) (****************************************) -exception Bound +type debug = Debug | Info | Off -let head_constr_bound t = - let t = strip_outer_cast t in - let _,ccl = decompose_prod_assum t in - let hd,args = decompose_app ccl in - match kind_of_term hd with - | Const _ | Ind _ | Construct _ | Var _ -> hd - | Proj (p, _) -> mkConst (Projection.constant p) - | _ -> raise Bound - -let head_constr c = - try head_constr_bound c with Bound -> error "Bound head variable." +exception Bound -let decompose_app_bound t = - let t = strip_outer_cast t in - let _,ccl = decompose_prod_assum t in - let hd,args = decompose_app_vect ccl in - match kind_of_term hd with +let head_constr_bound sigma t = + let t = strip_outer_cast sigma t in + let _,ccl = decompose_prod_assum sigma t in + let hd,args = decompose_app sigma ccl in + match EConstr.kind sigma hd with + | Const (c, _) -> ConstRef c + | Ind (i, _) -> IndRef i + | Construct (c, _) -> ConstructRef c + | Var id -> VarRef id + | Proj (p, _) -> ConstRef (Projection.constant p) + | _ -> raise Bound + +let head_constr sigma c = + try head_constr_bound sigma c + with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \ + (co)inductive type, (co)inductive type constructor, or projection.") + +let decompose_app_bound sigma t = + let t = strip_outer_cast sigma t in + let _,ccl = decompose_prod_assum sigma t in + let hd,args = decompose_app_vect sigma ccl in + match EConstr.kind sigma hd with | Const (c,u) -> ConstRef c, args | Ind (i,u) -> IndRef i, args | Construct (c,u) -> ConstructRef c, args @@ -71,6 +79,7 @@ let decompose_app_bound t = different declaration between the named hyps and the section context. *) let secvars_of_hyps hyps = let secctx = Global.named_context () in + let open Context.Named.Declaration in let pred, all = List.fold_left (fun (pred,all) decl -> try let _ = Context.Named.lookup (get_id decl) hyps in @@ -121,14 +130,14 @@ type hints_path = global_reference hints_path_gen type hint_term = | IsGlobRef of global_reference - | IsConstr of constr * Univ.universe_context_set + | IsConstr of constr * Univ.ContextSet.t type 'a with_uid = { obj : 'a; uid : KerName.t; } -type raw_hint = constr * types * Univ.universe_context_set +type raw_hint = constr * types * Univ.ContextSet.t type hint = (raw_hint * clausenv) hint_ast with_uid @@ -159,12 +168,11 @@ 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." +| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.") let _ = Goptions.declare_string_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "behavior of non-imported hints"; Goptions.optkey = ["Loose"; "Hint"; "Behavior"]; Goptions.optread = read_warn_hint; @@ -251,8 +259,8 @@ let rebuild_dn st se = in { se with sentry_bnet = dn' } -let lookup_tacs concl st se = - let l' = Bounded_net.lookup st se.sentry_bnet concl in +let lookup_tacs sigma concl st se = + let l' = Bounded_net.lookup sigma st se.sentry_bnet concl in let sl' = List.stable_sort pri_order_int l' in List.merge pri_order_int se.sentry_nopat sl' @@ -263,10 +271,10 @@ let is_transparent_gr (ids, csts) = function | ConstRef cst -> Cpred.mem cst csts | IndRef _ | ConstructRef _ -> false -let strip_params env c = - match kind_of_term c with +let strip_params env sigma c = + match EConstr.kind sigma c with | App (f, args) -> - (match kind_of_term f with + (match EConstr.kind sigma f with | Const (p,_) -> let cb = lookup_constant p env in (match cb.Declarations.const_proj with @@ -285,7 +293,7 @@ let instantiate_hint env sigma p = 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 }; + { cl.templval with rebus = strip_params env sigma cl.templval.rebus }; env = empty_env} in let code = match p.code.obj with @@ -469,11 +477,11 @@ 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 -> +val map_existential : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list -val map_eauto : secvars:Id.Pred.t -> +val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list -val map_auto : secvars:Id.Pred.t -> +val map_auto : evar_map -> 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 @@ -529,21 +537,32 @@ struct (** Warn about no longer typable hint? *) None - let match_mode m arg = + let head_evar sigma c = + let rec hrec c = match EConstr.kind sigma c with + | Evar (evk,_) -> evk + | Case (_,_,c,_) -> hrec c + | App (c,_) -> hrec c + | Cast (c,_,_) -> hrec c + | Proj (p, c) -> hrec c + | _ -> raise Evarutil.NoHeadEvar + in + hrec c + + let match_mode sigma m arg = match m with - | ModeInput -> not (occur_existential arg) + | ModeInput -> not (occur_existential sigma arg) | ModeNoHeadEvar -> - Evarutil.(try ignore(head_evar arg); false - with NoHeadEvar -> true) + (try ignore(head_evar sigma arg); false + with Evarutil.NoHeadEvar -> true) | ModeOutput -> true - let matches_mode args mode = + let matches_mode sigma args mode = Array.length mode == Array.length args && - Array.for_all2 match_mode mode args + Array.for_all2 (match_mode sigma) mode args - let matches_modes args modes = + let matches_modes sigma args modes = if List.is_empty modes then true - else List.exists (matches_mode args) modes + else List.exists (matches_mode sigma args) modes let merge_entry secvars db nopat pat = let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in @@ -559,24 +578,24 @@ struct merge_entry secvars db se.sentry_nopat se.sentry_pat (** Precondition: concl has no existentials *) - let map_auto ~secvars (k,args) concl db = + let map_auto sigma ~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 + let pat = lookup_tacs sigma concl st se in merge_entry secvars db [] pat - let map_existential ~secvars (k,args) concl db = + let map_existential sigma ~secvars (k,args) concl db = let se = find k db in - if matches_modes args se.sentry_mode then + if matches_modes sigma args se.sentry_mode then merge_entry secvars db se.sentry_nopat se.sentry_pat else merge_entry secvars db [] [] (* [c] contains an existential *) - let map_eauto ~secvars (k,args) concl db = + let map_eauto sigma ~secvars (k,args) concl db = let se = find k db in - if matches_modes args se.sentry_mode then + if matches_modes sigma 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 + let pat = lookup_tacs sigma concl st se in merge_entry secvars db [] pat else merge_entry secvars db [] [] @@ -716,7 +735,7 @@ let current_db () = Hintdbmap.bindings !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 ".") + user_err ~hdr:"Hints" (str "No such Hint database: " ++ str x ++ str ".") (**************************************************************************) (* Definition of the summary *) @@ -741,15 +760,17 @@ let _ = Summary.declare_summary "search" (* Auxiliary functions to prepare AUTOHINT objects *) (**************************************************************************) -let rec nb_hyp c = match kind_of_term c with - | Prod(_,_,c2) -> if noccurn 1 c2 then 1+(nb_hyp c2) else nb_hyp c2 +let rec nb_hyp sigma c = match EConstr.kind sigma c with + | Prod(_,_,c2) -> if noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2 | _ -> 0 (* adding and removing tactics in the search table *) let try_head_pattern c = try head_pattern_bound c - with BoundPattern -> error "Bound head variable." + with BoundPattern -> + user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \ + an if, case, or let expression, an application, or a projection.") let with_uid c = { obj = c; uid = fresh_key () } @@ -759,19 +780,19 @@ let secvars_of_idset s = 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_constr env sigma c = + secvars_of_idset (Termops.global_vars_set env sigma 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 + let secvars = secvars_of_constr env sigma c in + let cty = strip_outer_cast sigma cty in + match EConstr.kind sigma cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = Patternops.pattern_of_constr env sigma cty in + let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -788,38 +809,48 @@ let make_exact_entry env sigma info 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 _ -> - let sigma' = Evd.merge_context_set univ_flexible sigma ctx in - let ce = mk_clenv_from_env env sigma' None (c,cty) in - let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd c' in - let hd = - 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; 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 - Feedback.msg_info (str "the hint: eapply " ++ pr_lconstr c ++ - str " will only be used by eauto"); - (Some hd, - { pri; poly; pat = Some pat; name; - db = None; secvars; - code = with_uid (ERes_pf(c,cty,ctx)); }) - end - | _ -> failwith "make_apply_entry" + match EConstr.kind sigma cty with + | Prod _ -> + let sigma' = Evd.merge_context_set univ_flexible sigma ctx in + let ce = mk_clenv_from_env env sigma' None (c,cty) in + let c' = clenv_type (* ~reduce:false *) ce in + let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in + let hd = + try head_pattern_bound pat + with BoundPattern -> failwith "make_apply_entry" in + let miss = clenv_missing ce in + let nmiss = List.length (clenv_missing ce) in + let secvars = secvars_of_constr env sigma c in + let pri = match info.hint_priority with None -> nb_hyp sigma' 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; 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 begin + let variables = str (CString.plural nmiss "variable") in + Feedback.msg_info ( + strbrk "The hint " ++ + pr_leconstr_env env sigma' c ++ + strbrk " will only be used by eauto, because applying " ++ + pr_leconstr_env env sigma' c ++ + strbrk " would leave " ++ variables ++ Pp.spc () ++ + Pp.prlist_with_sep Pp.pr_comma Name.print (List.map (Evd.meta_name ce.evd) miss) ++ + strbrk " as unresolved existential " ++ variables ++ str "." + ) + end; + (Some hd, + { pri; poly; pat = Some pat; name; + db = None; secvars; + code = with_uid (ERes_pf(c,cty,ctx)); }) + end + | _ -> failwith "make_apply_entry" (* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose c is a constr @@ -829,7 +860,7 @@ 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 + pr_econstr_env env sigma c (** We need an object to record the side-effect of registering global universes associated with a hint. *) @@ -855,7 +886,8 @@ 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 + let (c, ctx) = Universes.fresh_global_instance env gr in + true, (EConstr.of_constr c, ctx) | IsConstr (c, ctx) -> false, (c, ctx) in if poly then (c, ctx) @@ -877,23 +909,23 @@ let make_resolves env sigma flags info poly ?name cr = make_apply_entry env sigma flags info poly ?name] in if List.is_empty ents then - errorlabstrm "Hint" - (pr_lconstr c ++ spc() ++ + user_err ~hdr:"Hint" + (pr_leconstr_env env sigma c ++ spc() ++ (if pi1 flags then str"cannot be used as a hint." else str "can be used as a hint only for eauto.")); ents (* used to add an hypothesis to the local hint database *) let make_resolve_hyp env sigma decl = - let hname = get_id decl in + let hname = NamedDecl.get_id decl in let c = mkVar hname in try [make_apply_entry env sigma (true, true, false) empty_hint_info false ~name:(PathHints [VarRef hname]) - (c, get_type decl, Univ.ContextSet.empty)] + (c, NamedDecl.get_type decl, Univ.ContextSet.empty)] with | Failure _ -> [] - | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp") + | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp.") (* REM : in most cases hintname = id *) @@ -909,7 +941,6 @@ let make_unfold eref = 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; @@ -921,12 +952,13 @@ let make_extern pri pat tacast = code = with_uid (Extern tacast) }) let make_mode ref m = - let ty = Global.type_of_global_unsafe ref in + let open Term in + let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in let ctx, t = decompose_prod ty in let n = List.length ctx in let m' = Array.of_list m in if not (n == Array.length m') then - errorlabstrm "Hint" + user_err ~hdr:"Hint" (pr_global ref ++ str" has " ++ int n ++ str" arguments while the mode declares " ++ int (Array.length m')) else m' @@ -935,14 +967,14 @@ 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 (unsafe_type_of env sigma c) in - let hd = head_of_constr_reference (head_constr t) in + let hd = head_constr sigma t in let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce)); + pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce))); name = name; db = None; - secvars = secvars_of_constr env c; + secvars = secvars_of_constr env sigma c; code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) @@ -961,8 +993,8 @@ let get_db dbname = 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." + user_err Pp.(str "Conflicting hint keys. This can happen when including \ + twice the same module.") in statustable := KNmap.add h.code.uid false !statustable in @@ -1036,14 +1068,16 @@ let cache_autohint (kn, obj) = let subst_autohint (subst, obj) = let subst_key gr = let (lab'', elab') = subst_global subst gr in + let elab' = EConstr.of_constr elab' in let gr' = - (try head_of_constr_reference (head_constr_bound elab') + (try head_constr_bound Evd.empty elab' with Bound -> lab'') in if gr' == gr then gr else gr' in 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 subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> let c' = subst_mps subst c in @@ -1136,7 +1170,7 @@ let add_resolves env sigma clist local dbnames = (fun dbname -> let r = List.flatten (List.map (fun (pri, poly, hnf, path, gr) -> - make_resolves env sigma (true,hnf,Flags.is_verbose()) + make_resolves env sigma (true,hnf,not !Flags.quiet) pri poly ~name:path gr) clist) in let hint = make_hint ~local dbname (AddHints r) in @@ -1192,8 +1226,6 @@ let add_trivials env sigma l local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let (forward_intern_tac, extern_intern_tac) = Hook.make () - type hnf = bool type hint_info = (patvar list * constr_pattern) hint_info_gen @@ -1205,7 +1237,7 @@ type hints_entry = | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool | HintsModeEntry of global_reference * hint_mode list - | HintsExternEntry of hint_info * glob_tactic_expr + | HintsExternEntry of hint_info * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" @@ -1216,30 +1248,30 @@ let prepare_hint check (poly,local) env init (sigma,c) = (* 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 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 sigma, _ = Evd.nf_univ_variables sigma in + let c = Evarutil.nf_evar sigma c in + let c = drop_extra_implicit_args sigma c in + let vars = ref (collect_vars sigma c) in let subst = ref [] in - let rec find_next_evar c = match kind_of_term c with + let rec find_next_evar c = match EConstr.kind sigma c with | Evar (evk,args as ev) -> (* 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 (closed0 c) then - error "Hints with holes dependent on a bound variable not supported."; - if occur_existential t then + let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in + if not (closed0 sigma c) then + user_err Pp.(str "Hints with holes dependent on a bound variable not supported."); + if occur_existential sigma t then (* Not clever enough to construct dependency graph of evars *) - error "Not clever enough to deal with evars dependent in other evars."; + user_err Pp.(str "Not clever enough to deal with evars dependent in other evars."); raise (Found (c,t)) - | _ -> Constr.iter find_next_evar c in + | _ -> EConstr.iter sigma find_next_evar c in let rec iter c = try find_next_evar c; c with Found (evar,t) -> let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in vars := Id.Set.add id !vars; subst := (evar,mkVar id)::!subst; - mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in + mkNamedLambda id t (iter (replace_term sigma evar (mkVar id) c)) in let c' = iter c in 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 @@ -1250,18 +1282,16 @@ let prepare_hint check (poly,local) env init (sigma,c) = let interp_hints poly = fun h -> - let env = (Global.env()) 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; + Dumpglob.add_glob ?loc:r.CAst.loc gr; gr in - let fr r = - evaluable_of_global_reference (Global.env()) (fref r) - in + let fr r = evaluable_of_global_reference env (fref r) in let fi c = match c with | HintsReference c -> @@ -1269,7 +1299,7 @@ let interp_hints poly = (PathHints [gr], poly, IsGlobRef gr) | HintsConstr c -> (PathAny, poly, f poly c) in - let fp = Constrintern.intern_constr_pattern (Global.env()) in + let fp = Constrintern.intern_constr_pattern env sigma in let fres (info, b, r) = let path, poly, gr = fi r in let info = { info with hint_pattern = Option.map fp info.hint_pattern } in @@ -1286,22 +1316,25 @@ let interp_hints poly = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - empty_hint_info, mib.Declarations.mind_polymorphic, true, + empty_hint_info, + (Declareops.inductive_is_polymorphic mib), 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 + let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in + let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in + let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) let add_hints local dbnames0 h = if String.List.mem "nocore" dbnames0 then - error "The hint database \"nocore\" is meant to stay empty."; + user_err Pp.(str "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() in let sigma = Evd.from_env env in @@ -1318,7 +1351,7 @@ let add_hints local dbnames0 h = let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> - match kind_of_term lem with + match EConstr.kind sigma lem with | Ind (ind,u) -> List.init (nconstructors ind) (fun i -> @@ -1342,13 +1375,9 @@ let add_hint_lemmas env sigma eapply lems hint_db = 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 map c = c env sigma in let lems = List.map map lems in - let sign = Environ.named_context env in + let sign = EConstr.named_context env in let ts = match ts with | None -> Hint_db.transparent_state (searchtable_map "core") | Some ts -> ts @@ -1373,42 +1402,37 @@ let make_db_list dbnames = (* Functions for printing the hints *) (**************************************************************************) -let pr_hint_elt (c, _, _) = pr_constr c +let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c -let pr_hint h = match h.obj with - | 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) +let pr_hint env sigma h = match h.obj with + | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c) + | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c) + | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail (c, _) -> - (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial") - | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c) + (str"simple apply " ++ pr_hint_elt env sigma 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 CErrors.noncritical e -> Global.env () - in - (str "(*external*) " ++ Pptactic.pr_glb_generic env tac) + str "(*external*) " ++ Pputils.pr_glb_generic env tac -let pr_id_hint (id, v) = - 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 +let pr_id_hint env sigma (id, v) = + let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in + (pr_hint env sigma 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 ()) +let pr_hint_list env sigma hintlist = + (str " " ++ hov 0 (prlist (pr_id_hint env sigma) hintlist) ++ fnl ()) -let pr_hints_db (name,db,hintlist) = +let pr_hints_db env sigma (name,db,hintlist) = (str "In the database " ++ str name ++ str ":" ++ if List.is_empty hintlist then (str " nothing" ++ fnl ()) - else (fnl () ++ pr_hint_list hintlist)) + else (fnl () ++ pr_hint_list env sigma hintlist)) (* Print all hints associated to head c in any database *) -let pr_hint_list_for_head c = +let pr_hint_list_for_head env sigma c = let dbs = current_db () in let validate (name, db) = - let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in + let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in (name, db, hints) in let valid_dbs = List.map validate dbs in @@ -1417,21 +1441,21 @@ let pr_hint_list_for_head c = else hov 0 (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) let pr_hint_ref ref = pr_hint_list_for_head ref (* Print all hints associated to head id in any database *) -let pr_hint_term cl = +let pr_hint_term env sigma cl = try let dbs = current_db () in let valid_dbs = let fn = try - let hdc = decompose_app_bound cl in - if occur_existential cl then - Hint_db.map_existential ~secvars:Id.Pred.full hdc cl - else Hint_db.map_auto ~secvars:Id.Pred.full hdc cl + let hdc = decompose_app_bound sigma cl in + if occur_existential sigma cl then + Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl + else Hint_db.map_auto sigma ~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 @@ -1441,18 +1465,19 @@ let pr_hint_term cl = (str "No hint applicable for current goal") else (str "Applicable Hints :" ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) + hov 0 (prlist (pr_hints_db env sigma) valid_dbs)) with Match_failure _ | Failure _ -> (str "No hint applicable for current goal") (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint () = - let pts = get_pftreestate () in - let glss = Proof.V82.subgoals pts in - match glss.Evd.it with - | [] -> CErrors.error "No focused goal." + let env = Global.env () in + let pts = Proof_global.give_me_the_proof () in + let glss,_,_,_,sigma = Proof.proof pts in + match glss with + | [] -> CErrors.user_err Pp.(str "No focused goal.") | g::_ -> - pr_hint_term (Goal.V82.concl glss.Evd.sigma g) + pr_hint_term env sigma (Goal.V82.concl sigma g) let pp_hint_mode = function | ModeInput -> str"+" @@ -1460,9 +1485,9 @@ let pp_hint_mode = function | ModeOutput -> str"-" (* displays the whole hint database db *) -let pr_hint_db db = +let pr_hint_db_env env sigma db = let pr_mode = prvect_with_sep spc pp_hint_mode in - let pr_modes l = + let pr_modes l = if List.is_empty l then mt () else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")" in @@ -1472,7 +1497,7 @@ let pr_hint_db db = | None -> str "For any goal" | Some head -> str "For " ++ pr_global head ++ pr_modes modes in - let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in + let hints = pr_hint_list env sigma (List.map (fun x -> (0, x)) hintlist) in let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in accu ++ hint_descr in @@ -1487,17 +1512,22 @@ let pr_hint_db db = hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ content -let pr_hint_db_by_name dbname = +(* Deprecated in the mli *) +let pr_hint_db db = + let sigma, env = Pfedit.get_current_context () in + pr_hint_db_env env sigma db + +let pr_hint_db_by_name env sigma dbname = try - let db = searchtable_map dbname in pr_hint_db db + let db = searchtable_map dbname in pr_hint_db_env env sigma db with Not_found -> error_no_such_hint_database dbname (* displays all the hints of all databases *) -let pr_searchtable () = +let pr_searchtable env sigma = let fold name db accu = accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++ - pr_hint_db db ++ fnl () + pr_hint_db_env env sigma db ++ fnl () in Hintdbmap.fold fold !searchtable (mt ()) @@ -1515,10 +1545,13 @@ let warn_non_imported_hint = 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 - warn_non_imported_hint (hint,mp); - Proofview.tclUNIT 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 run_hint tac k = match !warn_hint with | `LAX -> k tac.obj @@ -1527,6 +1560,6 @@ let run_hint tac k = match !warn_hint with 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."))) + else Proofview.tclZERO (UserError (None, (str "Tactic failure."))) let repr_hint h = h.obj |