From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- tactics/auto.ml | 9 +- tactics/autorewrite.ml | 26 ++-- tactics/btermdn.ml | 4 +- tactics/class_tactics.ml | 54 +++------ tactics/contradiction.ml | 5 +- tactics/contradiction.mli | 2 +- tactics/eauto.ml | 11 +- tactics/elim.mli | 3 +- tactics/elimschemes.ml | 6 +- tactics/eqdecide.ml | 12 +- tactics/eqschemes.ml | 43 ++++--- tactics/equality.ml | 63 +++++----- tactics/equality.mli | 18 ++- tactics/hints.ml | 241 +++++++++++++++++++++++-------------- tactics/hints.mli | 76 ++++++++---- tactics/hipattern.ml | 12 +- tactics/hipattern.mli | 2 +- tactics/ind_tables.ml | 10 +- tactics/inv.ml | 33 +++--- tactics/inv.mli | 6 +- tactics/leminv.ml | 9 +- tactics/leminv.mli | 2 +- tactics/tacticals.ml | 73 ++++++++---- tactics/tacticals.mli | 11 +- tactics/tactics.ml | 296 +++++++++++++++++++++++++++------------------- tactics/tactics.mli | 44 ++++--- tactics/term_dnet.ml | 4 +- tactics/term_dnet.mli | 2 +- 28 files changed, 630 insertions(+), 447 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 0c0d9bcf..d7de6c4f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Pp open Util open Names @@ -81,15 +79,14 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let clenv, c = if poly then (** Refresh the instance of the hint *) - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in - let map c = CVars.subst_univs_level_constr subst c in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in (** Only metas are mentioning the old universes. *) let clenv = { templval = Evd.map_fl emap clenv.templval; templtyp = Evd.map_fl emap clenv.templtyp; - evd = Evd.map_metas map evd; + evd = Evd.map_metas emap evd; env = Proofview.Goal.env gl; } in clenv, emap c @@ -102,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) = Proofview.Goal.enter begin fun gl -> let clenv, c = connect_hint_clenv poly c clenv gl in let clenv = clenv_unique_resolver ~flags clenv gl in - Clenvtac.clenv_refine false clenv + Clenvtac.clenv_refine clenv end let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c3857e6b..c8fd0b7a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -30,7 +30,7 @@ let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in - let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in + let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; @@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas = let try_rewrite dir ctx c tc = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -228,7 +228,7 @@ let decompose_applied_relation metas env sigma c ctype left2right = if metas then eqclause else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd) in - let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in + let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> @@ -236,17 +236,19 @@ let decompose_applied_relation metas env sigma c ctype left2right = | _ -> raise Not_found in try - let others,(c1,c2) = split_last_two args in - let ty1, ty2 = - Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2) - in - let ty = EConstr.Unsafe.to_constr ty in - let ty1 = EConstr.Unsafe.to_constr ty1 in + let others,(c1,c2) = split_last_two args in + let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in + (* XXX: It looks like mk_clenv_from_env should be fixed instead? *) + let open EConstr in + let hyp_ty = Unsafe.to_constr ty in + let hyp_car = Unsafe.to_constr ty1 in + let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in + let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in + let hyp_left = Unsafe.to_constr @@ c1 in + let hyp_right = Unsafe.to_constr @@ c2 in (* if not (evd_convertible env eqclause.evd ty1 ty2) then None *) (* else *) - Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty; - hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others); - hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; } + Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; } with Not_found -> None in match find_rel ctype with diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 8e50c977..aca7f6c6 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -9,7 +9,7 @@ (************************************************************************) open Util -open Term +open Constr open EConstr open Names open Pattern @@ -22,7 +22,7 @@ open Globnames let dnet_depth = ref 8 type term_label = -| GRLabel of global_reference +| GRLabel of GlobRef.t | ProdLabel | LambdaLabel | SortLabel diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 73b649e5..29797240 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -18,6 +18,7 @@ open CErrors open Util open Names open Term +open Constr open Termops open EConstr open Tacmach @@ -206,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' = try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) with e -> Proofview.tclZERO e in resolve >>= fun clenv' -> - Clenvtac.clenv_refine with_evars ~with_classes:false clenv' + Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv' end let unify_e_resolve poly flags = begin fun gls (c,_,clenv) -> @@ -226,7 +227,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = Refine.refine ~typecheck:false begin fun sigma -> let sigma, term, ty = if poly then - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in sigma, map c, map t @@ -476,7 +477,7 @@ let is_Prop env sigma concl = match EConstr.kind sigma ty with | Sort s -> begin match ESorts.kind sigma s with - | Prop Null -> true + | Prop -> true | _ -> false end | _ -> false @@ -546,12 +547,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = let hints = build_subclasses ~check:false env sigma (VarRef id) empty_hint_info in (List.map_append (fun (path,info,c) -> - let info = - { info with Vernacexpr.hint_pattern = - Option.map (Constrintern.intern_constr_pattern env sigma) - info.Vernacexpr.hint_pattern } - in - make_resolves env sigma ~name:(PathHints path) + make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info false (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty))) hints) @@ -653,17 +649,6 @@ module Search = struct Evd.add sigma gl evi') sigma goals - let fail_if_nonclass info = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - if is_class_type sigma (Proofview.Goal.concl gl) then - Proofview.tclUNIT () - else (if !typeclasses_debug > 1 then - Feedback.msg_debug (pr_depth info.search_depth ++ - str": failure due to non-class subgoal " ++ - pr_ev sigma (Proofview.Goal.goal gl)); - Proofview.tclZERO NoApplicableEx) end - (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined depending on the dependencies of the goal and the unique/Prop @@ -708,8 +693,9 @@ module Search = struct let msg = match fst ie with | Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) -> - str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++ - print_constr_env env evd y + str"Cannot unify " ++ + Printer.pr_econstr_env env evd x ++ str" and " ++ + Printer.pr_econstr_env env evd y | ReachedLimitEx -> str "Proof-search reached its limit." | NoApplicableEx -> str "Proof-search failed." | e -> CErrors.iprint ie @@ -802,13 +788,8 @@ module Search = struct in if path_matches derivs [] then aux e tl else - let filter = - if false (* in 8.6, still allow non-class subgoals - info.search_only_classes *) then fail_if_nonclass info - else Proofview.tclUNIT () - in ortac - (with_shelf (tac <*> filter) >>= fun s -> + (with_shelf tac >>= fun s -> let i = !idx in incr idx; result s i None) (fun e' -> if CErrors.noncritical (fst e') then @@ -872,12 +853,9 @@ module Search = struct let search_tac_gl ?st only_classes dep hints depth i sigma gls gl : unit Proofview.tactic = let open Proofview in - if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then - Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") - else - let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in - let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in - search_tac hints depth 1 info + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in + let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in + search_tac hints depth 1 info let search_tac ?(st=full_transparent_state) only_classes dep hints depth = let open Proofview in @@ -1030,8 +1008,8 @@ module Intpart = Unionfind.Make(Evar.Set)(Evar.Map) let deps_of_constraints cstrs evm p = List.iter (fun (_, _, x, y) -> - let evx = Evarutil.undefined_evars_of_term evm (EConstr.of_constr x) in - let evy = Evarutil.undefined_evars_of_term evm (EConstr.of_constr y) in + let evx = Evarutil.undefined_evars_of_term evm x in + let evy = Evarutil.undefined_evars_of_term evm y in Intpart.union_set (Evar.Set.union evx evy) p) cstrs @@ -1076,7 +1054,7 @@ let error_unresolvable env comp evd = | Some s -> Evar.Set.mem ev s in let fold ev evi (found, accu) = - let ev_class = class_of_constr evd (EConstr.of_constr evi.evar_concl) in + let ev_class = class_of_constr evd evi.evar_concl in if not (Option.is_empty ev_class) && is_part ev then (* focus on one instance if only one was searched for *) if not found then (true, Some ev) @@ -1174,7 +1152,7 @@ let solve_inst env evd filter unique split fail = let _ = Hook.set Typeclasses.solve_all_instances_hook solve_inst -let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = +let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = 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 diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c285f21e..e12063fd 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -8,13 +8,12 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term +open Constr open EConstr open Hipattern open Tactics open Coqlib open Reductionops -open Misctypes open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) = else Proofview.tclORELSE begin - if lbind = NoBindings then + if lbind = Tactypes.NoBindings then filter_hyp (fun c -> is_negation_of env sigma typ c) (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) else diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 2b3a9475..4bb3263f 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -9,7 +9,7 @@ (************************************************************************) open EConstr -open Misctypes +open Tactypes val absurd : constr -> unit Proofview.tactic val contradiction : constr with_bindings option -> unit Proofview.tactic diff --git a/tactics/eauto.ml b/tactics/eauto.ml index dc310c54..80d07c5c 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Termops open EConstr open Proof_type @@ -70,11 +70,10 @@ let first_goal gls = (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) let apply_tac_list tac glls = - let (sigr,lg) = unpackage glls in - match lg with + match glls.it with | (g1::rest) -> - let gl = apply_sig_tac sigr tac g1 in - repackage sigr (gl@rest) + let pack = tac (re_sig g1 glls.sigma) in + re_sig (pack.it @ rest) pack.sigma | _ -> user_err Pp.(str "apply_tac_list") let one_step l gl = @@ -90,7 +89,7 @@ let rec prolog l n gl = let out_term env = function | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr)) + | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr)) let prolog_tac l n = Proofview.V82.tactic begin fun gl -> diff --git a/tactics/elim.mli b/tactics/elim.mli index d6b67e5b..ddfac3f2 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -11,12 +11,11 @@ open Names open EConstr open Tacticals -open Misctypes open Tactypes (** Eliminations tactics. *) -val introCaseAssumsThen : evars_flag -> +val introCaseAssumsThen : Tactics.evars_flag -> (intro_patterns -> branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 6bd4866c..3b69d992 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -44,10 +44,10 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams_rec else mib.mind_nparams in - let sigma, sort = Evd.fresh_sort_in_family env sigma sort in + let sigma, sort = Evd.fresh_sort_in_family sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in - let sigma, nf = Evarutil.nf_evars_and_universes sigma in - (nf c', Evd.evar_universe_context sigma), eff + let sigma = Evd.minimize_universes sigma in + (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index b0deeed1..832014a6 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -17,18 +17,18 @@ open Util open Names open Namegen -open Term +open Constr open EConstr open Declarations open Tactics open Tacticals.New open Auto open Constr_matching -open Misctypes open Hipattern open Proofview.Notations open Tacmach.New open Coqlib +open Tactypes (* This file containts the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the @@ -58,14 +58,14 @@ let clear_last = let choose_eq eqonleft = if eqonleft then - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings else - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings let choose_noteq eqonleft = if eqonleft then - right_with_bindings false Misctypes.NoBindings + right_with_bindings false NoBindings else - left_with_bindings false Misctypes.NoBindings + left_with_bindings false NoBindings (* A surgical generalize which selects the right occurrences by hand *) (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 477de645..ea5ff4a6 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -78,7 +78,7 @@ let build_dependent_inductive ind (mib,mip) = Context.Rel.to_extended_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt @ Context.Rel.to_extended_list mkRel 0 realargs) -let named_hd env t na = named_hd env Evd.empty (EConstr.of_constr t) na +let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na let name_assumption env = function | LocalAssum (na,t) -> LocalAssum (named_hd env t na, t) | LocalDef (na,c,t) -> LocalDef (named_hd env c na, c, t) @@ -102,15 +102,20 @@ let get_coq_eq ctx = let eq = Globnames.destIndRef Coqlib.glob_eq in (* Do not force the lazy if they are not defined *) let eq, ctx = with_context_set ctx - (Universes.fresh_inductive_instance (Global.env ()) eq) in + (UnivGen.fresh_inductive_instance (Global.env ()) eq) in mkIndU eq, mkConstructUi (eq,1), ctx with Not_found -> user_err Pp.(str "eq not found.") let univ_of_eq env eq = - let eq = EConstr.of_constr eq in - match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env Evd.empty eq)) with - | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false) + let open EConstr in + let eq = of_constr eq in + let sigma = Evd.from_env env in + match kind sigma (Retyping.get_type_of env sigma eq) with + | Prod (_,t,_) -> (match kind sigma t with + Sort k -> + (match ESorts.kind sigma k with Type u -> u | _ -> assert false) + | _ -> assert false) | _ -> assert false (**********************************************************************) @@ -192,7 +197,7 @@ let get_non_sym_eq_data env (ind,u) = (**********************************************************************) let build_sym_scheme env ind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n = @@ -241,11 +246,11 @@ let sym_scheme_kind = let const_of_scheme kind env ind ctx = let sym_scheme, eff = (find_scheme kind ind) in let sym, ctx = with_context_set ctx - (Universes.fresh_constant_instance (Global.env()) sym_scheme) in + (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in mkConstU sym, ctx, eff let build_sym_involutive_scheme env ind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let eq,eqrefl,ctx = get_coq_eq ctx in @@ -353,7 +358,7 @@ let sym_involutive_scheme_kind = (**********************************************************************) let build_l2r_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in @@ -392,7 +397,7 @@ let build_l2r_rew_scheme dep env ind kind = rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -469,7 +474,7 @@ let build_l2r_rew_scheme dep env ind kind = (**********************************************************************) let build_l2r_forward_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n p = @@ -495,7 +500,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let realsign_ind_P n aP = name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -561,7 +566,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (**********************************************************************) let build_r2l_forward_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = get_non_sym_eq_data env indu in let cstr n = @@ -573,7 +578,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let realsign_ind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -620,7 +625,9 @@ let build_r2l_forward_rew_scheme dep env ind kind = (**********************************************************************) let fix_r2l_forward_rew_scheme (c, ctx') = - let t = Retyping.get_type_of (Global.env()) Evd.empty (EConstr.of_constr c) in + let env = Global.env () in + let sigma = Evd.from_env env in + let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in let ctx,_ = decompose_prod_assum t in match ctx with @@ -630,7 +637,7 @@ let fix_r2l_forward_rew_scheme (c, ctx') = (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 1) p) (mkLambda_or_LetIn (RelDecl.map_constr (liftn (-1) 2) hp) (mkLambda_or_LetIn (RelDecl.map_constr (lift 2) ind) - (EConstr.Unsafe.to_constr (Reductionops.whd_beta Evd.empty + (EConstr.Unsafe.to_constr (Reductionops.whd_beta sigma (EConstr.of_constr (applist (c, Context.Rel.to_extended_list mkRel 3 indargs @ [mkRel 1;mkRel 3;mkRel 2])))))))) in c', ctx' @@ -755,7 +762,7 @@ let rew_r2l_scheme_kind = let build_congr env (eq,refl,ctx) ind = let (ind,u as indu), ctx = with_context_set ctx - (Universes.fresh_inductive_instance env ind) in + (UnivGen.fresh_inductive_instance env ind) in let (mib,mip) = lookup_mind_specif env ind in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; @@ -778,7 +785,7 @@ let build_congr env (eq,refl,ctx) ind = let varH = fresh env (Id.of_string "H") in let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in - let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt diff --git a/tactics/equality.ml b/tactics/equality.ml index 5821717d..0e392157 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -15,6 +15,7 @@ open Util open Names open Nameops open Term +open Constr open Termops open EConstr open Vars @@ -41,7 +42,7 @@ open Ind_tables open Eqschemes open Locus open Locusops -open Misctypes +open Tactypes open Proofview.Notations open Unification open Context.Named.Declaration @@ -153,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = let c1 = args.(arglen - 2) in let c2 = args.(arglen - 1) in let try_occ (evd', c') = - Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'} + Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'} in let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in let occs = @@ -545,6 +546,12 @@ let apply_special_clear_request clear_flag f = e when catchable_exception e -> tclIDTAC end +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + let general_multi_rewrite with_evars l cl tac = let do1 l2r f = Proofview.Goal.enter begin fun gl -> @@ -935,7 +942,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkSort (Prop Null)) + kont sigma subval (false_0,mkProp) (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the @@ -1036,7 +1043,7 @@ let onEquality with_evars tac (c,lbindc) = let t = type_of c in let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in - let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in + let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in tclTHEN @@ -1108,8 +1115,6 @@ let make_tuple env sigma (rterm,rty) lind = let p = mkLambda (na, a, rty) in let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in let sigma, sig_term = Evd.fresh_global env sigma sigdata.typ in - let exist_term = EConstr.of_constr exist_term in - let sig_term = EConstr.of_constr sig_term in sigma, (applist(exist_term,[a;p;(mkRel lind);rterm]), applist(sig_term,[a;p])) @@ -1178,35 +1183,35 @@ let minimal_free_rels_rec env sigma = let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigdata = find_sigma_data env sort_of_ty in - let evdref = ref (Evd.clear_metas sigma) in - let rec sigrec_clausal_form siglen p_i = + let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) let dflt_typ = unsafe_type_of env sigma dflt in try - let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = - evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in - dflt + let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in + let sigma = + Evarconv.solve_unif_constraints_with_heuristics env sigma in + sigma, dflt with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with + let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in - let ev = Evarutil.e_new_evar env evdref a in + let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in - let tuple_tail = sigrec_clausal_form (siglen-1) rty in - let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in + let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in + let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in match evopt with | Some w -> - let w_type = unsafe_type_of env !evdref w in - if Evarconv.e_cumul env evdref w_type a then - let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in - let exist_term = EConstr.of_constr exist_term in - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - else + let w_type = unsafe_type_of env sigma w in + begin match Evarconv.cumul env sigma w_type a with + | Some sigma -> + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | None -> user_err Pp.(str "Cannot solve a unification problem.") + end | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; @@ -1216,8 +1221,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = unsolved evars would mean not binding rel *) user_err Pp.(str "Cannot solve a unification problem.") in - let scf = sigrec_clausal_form siglen ty in - !evdref, Evarutil.nf_evar !evdref scf + let sigma = Evd.clear_metas sigma in + let sigma, scf = sigrec_clausal_form sigma siglen ty in + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors @@ -1372,7 +1378,6 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = let sigma, (injbody,resty) = build_injector e_env !evdref t1' (mkVar e) cpath in let injfun = mkNamedLambda e t injbody in let sigma,congr = Evd.fresh_global env sigma eq.congr in - let congr = EConstr.of_constr congr in let pf = applist(congr,[t;resty;injfun;t1;t2]) in let sigma, pf_typ = Typing.type_of env sigma pf in let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in @@ -1783,7 +1788,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in let u = EInstance.kind sigma u in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> @@ -1809,9 +1814,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) -> + | Var x', _ when not (Termops.local_occur_var sigma x' y) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) -> + | _, Var y' when not (Termops.local_occur_var sigma y' x) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () @@ -1834,7 +1839,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let u = EInstance.kind sigma u in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then failwith "caught"; diff --git a/tactics/equality.mli b/tactics/equality.mli index c0be917a..6f3e08ea 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -15,8 +15,8 @@ open EConstr open Environ open Ind_tables open Locus -open Misctypes open Tactypes +open Tactics (*i*) type dep_proof_flag = bool (* true = support rewriting dependent proofs *) @@ -61,6 +61,12 @@ val general_rewrite_in : val general_rewrite_clause : orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic +type multi = + | Precisely of int + | UpTo of int + | RepeatStar + | RepeatPlus + val general_multi_rewrite : evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list -> clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic @@ -80,20 +86,20 @@ val discrConcl : unit Proofview.tactic val discrHyp : Id.t -> unit Proofview.tactic val discrEverywhere : evars_flag -> unit Proofview.tactic val discr_tac : evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic (* Below, if flag is [None], it takes the value from the dynamic value of the option *) val inj : inj_flags option -> intro_patterns option -> evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic val injClause : inj_flags option -> intro_patterns option -> evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic val injHyp : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic val injConcl : inj_flags option -> unit Proofview.tactic val simpleInjClause : inj_flags option -> evars_flag -> - constr with_bindings destruction_arg option -> unit Proofview.tactic + constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic -val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic -val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic +val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic +val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings Tactics.destruction_arg option -> unit Proofview.tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr) diff --git a/tactics/hints.ml b/tactics/hints.ml index 500abc5b..43a450ea 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -12,7 +12,7 @@ open Pp open Util open CErrors open Names -open Term +open Constr open Evd open EConstr open Vars @@ -23,17 +23,16 @@ open Libobject open Namegen open Libnames open Smartlocate -open Misctypes open Termops open Inductiveops open Typing open Decl_kinds +open Typeclasses open Pattern open Patternops open Clenv open Tacred open Printer -open Vernacexpr module NamedDecl = Context.Named.Declaration @@ -94,13 +93,14 @@ let secvars_of_hyps hyps = else pred let empty_hint_info = - let open Vernacexpr in { hint_priority = None; hint_pattern = None } (************************************************************************) (* The Type of Constructions Autotactic Hints *) (************************************************************************) +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -115,7 +115,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen @@ -125,11 +125,11 @@ type 'a hints_path_gen = | PathEmpty | PathEpsilon -type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type pre_hints_path = Libnames.qualid hints_path_gen +type hints_path = GlobRef.t hints_path_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type 'a with_uid = { @@ -153,9 +153,33 @@ type 'a with_metadata = { type full_hint = hint with_metadata -type hint_entry = global_reference option * +type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata +type reference_or_constr = + | HintsReference of qualid + | HintsConstr of Constrexpr.constr_expr + +type hint_mode = + | ModeInput (* No evars *) + | ModeNoHeadEvar (* No evar at the head *) + | ModeOutput (* Anything *) + +type 'a hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + +type hints_expr = + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * qualid list * int option + | HintsImmediate of reference_or_constr list + | HintsUnfold of qualid list + | HintsTransparency of qualid hints_transparency_target * bool + | HintsMode of qualid * hint_mode list + | HintsConstructors of qualid list + | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument + type import_level = [ `LAX | `WARN | `STRICT ] let warn_hint : import_level ref = ref `LAX @@ -275,16 +299,16 @@ let strip_params env sigma c = match EConstr.kind sigma c with | App (f, args) -> (match EConstr.kind sigma f with - | Const (p,_) -> - let cb = lookup_constant p env in - (match cb.Declarations.const_proj with - | Some pb -> - let n = pb.Declarations.proj_npars in - if Array.length args > n then - mkApp (mkProj (Projection.make p false, args.(n)), - Array.sub args (n+1) (Array.length args - (n + 1))) - else c - | None -> c) + | Const (cst,_) -> + (match Recordops.find_primitive_projection cst with + | Some p -> + let p = Projection.make p false in + let npars = Projection.npars p in + if Array.length args > npars then + mkApp (mkProj (p, args.(npars)), + Array.sub args (npars+1) (Array.length args - (npars + 1))) + else c + | None -> c) | _ -> c) | _ -> c @@ -308,7 +332,7 @@ let instantiate_hint env sigma p = { 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 +| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2 | PathAny, PathAny -> true | _ -> false @@ -365,7 +389,7 @@ let path_seq p p' = let rec path_derivate hp hint = let rec derivate_atoms hints hints' = match hints, hints' with - | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs' + | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs' | [], [] -> PathEpsilon | [], hints -> PathEmpty | grs, [] -> PathAtom (PathHints grs) @@ -448,7 +472,7 @@ let subst_path_atom subst p = | PathAny -> p | PathHints grs -> let gr' gr = fst (subst_global subst gr) in - let grs' = List.smartmap gr' grs in + let grs' = List.Smart.map gr' grs in if grs' == grs then p else PathHints grs' let rec subst_hints_path subst hp = @@ -474,28 +498,28 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t -val find : global_reference -> t -> search_entry +val find : GlobRef.t -> 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_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_eauto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * 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 remove_one : GlobRef.t -> t -> t +val remove_list : GlobRef.t list -> t -> t +val iter : (GlobRef.t 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 add_mode : GlobRef.t -> 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) -> +val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a end = @@ -510,7 +534,7 @@ 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 : (GlobRef.t option * stored_data) list; hintdb_name : string option; } @@ -654,7 +678,7 @@ struct 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 + let remove_sdl p sdl = List.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -664,9 +688,9 @@ struct let remove_list grs db = let filter (_, h) = - match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in + match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in - let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db @@ -792,7 +816,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = match EConstr.kind sigma cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in + let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -814,12 +838,12 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c 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 pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false 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 nmiss = List.length miss 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 @@ -862,20 +886,6 @@ let pr_hint_term env sigma ctx = function let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in pr_econstr_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 ++ @@ -886,7 +896,7 @@ let fresh_global_or_constr env sigma poly cr = let isgr, (c, ctx) = match cr with | IsGlobRef gr -> - let (c, ctx) = Universes.fresh_global_instance env gr in + let (c, ctx) = UnivGen.fresh_global_instance env gr in true, (EConstr.of_constr c, ctx) | IsConstr (c, ctx) -> false, (c, ctx) in @@ -895,7 +905,7 @@ let fresh_global_or_constr env sigma poly cr = else begin if isgr then warn_polymorphic_hint (pr_hint_term env sigma ctx cr); - Lib.add_anonymous_leaf (input_context_set ctx); + Declare.declare_universe_context false ctx; (c, Univ.ContextSet.empty) end @@ -1005,15 +1015,19 @@ let add_hint dbname hintlist = let db' = Hint_db.add_list env sigma hintlist db in searchtable_add (dbname,db') -let add_transparency dbname grs b = +let add_transparency dbname target b = let db = get_db dbname in - let st = Hint_db.transparent_state db in + let (ids, csts as st) = Hint_db.transparent_state db in let st' = - List.fold_left (fun (ids, csts) gr -> - match gr with - | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts) - | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts) - st grs + match target with + | HintsVariables -> (if b then Id.Pred.full else Id.Pred.empty), csts + | HintsConstants -> ids, if b then Cpred.full else Cpred.empty + | HintsReferences grs -> + List.fold_left (fun (ids, csts) gr -> + match gr with + | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts) + | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts) + st grs in searchtable_add (dbname, Hint_db.set_transparent_state db st') let remove_hint dbname grs = @@ -1023,11 +1037,11 @@ let remove_hint dbname grs = type hint_action = | CreateDB of bool * transparent_state - | AddTransparency of evaluable_global_reference list * bool + | AddTransparency of evaluable_global_reference hints_transparency_target * bool | AddHints of hint_entry list - | RemoveHints of global_reference list + | RemoveHints of GlobRef.t list | AddCut of hints_path - | AddMode of global_reference * hint_mode array + | AddMode of GlobRef.t * hint_mode array let add_cut dbname path = let db = get_db dbname in @@ -1075,8 +1089,8 @@ let subst_autohint (subst, obj) = 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 k' = Option.Smart.map subst_key k in + let pat' = Option.Smart.map (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) -> @@ -1113,14 +1127,22 @@ let subst_autohint (subst, obj) = in let action = match obj.hint_action with | CreateDB _ -> obj.hint_action - | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in - if grs == grs' then obj.hint_action else AddTransparency (grs', b) + | AddTransparency (target, b) -> + let target' = + match target with + | HintsVariables -> target + | HintsConstants -> target + | HintsReferences grs -> + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in + if grs == grs' then target + else HintsReferences grs' + in + if target' == target then obj.hint_action else AddTransparency (target', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in + let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in + let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path in @@ -1228,15 +1250,15 @@ let add_trivials env sigma l local dbnames = type hnf = bool -type hint_info = (patvar list * constr_pattern) hint_info_gen +type nonrec hint_info = hint_info type hints_entry = | 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 * hint_mode list + | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" @@ -1273,20 +1295,53 @@ let prepare_hint check (poly,local) env init (sigma,c) = subst := (evar,mkVar id)::!subst; 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 env = Global.env () in + let empty_sigma = Evd.from_env env in + if check then Pretyping.check_evars env empty_sigma 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 (Lib.add_anonymous_leaf (input_context_set diff); + else (Declare.declare_universe_context false diff; IsConstr (c', Univ.ContextSet.empty)) +let project_hint ~poly pri l2r r = + let open EConstr in + let open Coqlib in + let gr = Smartlocate.global_with_alias r in + let env = Global.env() in + let sigma = Evd.from_env env in + let sigma, c = Evd.fresh_global env sigma gr in + let t = Retyping.get_type_of env sigma c in + let t = + Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) t in + let sign,ccl = decompose_prod_assum sigma t in + let (a,b) = match snd (decompose_app sigma ccl) with + | [a;b] -> (a,b) + | _ -> assert false in + let p = + if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in + let sigma, p = Evd.fresh_global env sigma p in + let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in + let c = it_mkLambda_or_LetIn + (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in + let id = + Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) + in + let ctx = Evd.const_univ_entry ~poly sigma in + let c = EConstr.to_constr sigma c in + let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in + let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in + (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c)) + let interp_hints poly = fun h -> 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 env = Global.env () in + let sigma = Evd.from_env env in + prepare_hint true (poly,false) env sigma (evd,c) in let fref r = let gr = global_with_alias r in Dumpglob.add_glob ?loc:r.CAst.loc gr; @@ -1305,18 +1360,25 @@ let interp_hints poly = let info = { info with hint_pattern = Option.map fp info.hint_pattern } in (info, poly, b, path, gr) in + let ft = function + | HintsVariables -> HintsVariables + | HintsConstants -> HintsConstants + | HintsReferences lhints -> HintsReferences (List.map fr lhints) + in + let fp = Constrintern.intern_constr_pattern (Global.env()) in match h with | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) + | HintsResolveIFF (l2r, lc, n) -> + HintsResolveEntry (List.map (project_hint ~poly n l2r) lc) | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) - | HintsTransparency (lhints, b) -> - HintsTransparencyEntry (List.map fr lhints, b) + | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b) | HintsMode (r, l) -> HintsModeEntry (fref r, l) | HintsConstructors lqid -> let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in @@ -1325,14 +1387,14 @@ let interp_hints poly = 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 pat = Option.map (fp sigma) patcom in let l = match pat with None -> [] | Some (l, _) -> l 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 = +let add_hints ~local dbnames0 h = if String.List.mem "nocore" dbnames0 then 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 @@ -1367,12 +1429,10 @@ let expand_constructor_hints env sigma lems = (* builds a hint database from a constr signature *) (* typically used with (lid, ltyp) = pf_hyps_types *) -let add_hint_lemmas env sigma eapply lems hint_db = +let constructor_hints env sigma eapply lems = let lems = expand_constructor_hints env sigma lems in - let hintlist' = - 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 + List.map_append (fun (poly, lem) -> + make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in @@ -1383,8 +1443,9 @@ let make_local_hint_db env sigma ts eapply lems = | Some ts -> ts in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in - add_hint_lemmas env sigma eapply lems - (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) + Hint_db.empty ts false + |> Hint_db.add_list env sigma hintlist + |> Hint_db.add_list env sigma (constructor_hints env sigma eapply lems) let make_local_hint_db env sigma ?ts eapply lems = make_local_hint_db env sigma ts eapply lems diff --git a/tactics/hints.mli b/tactics/hints.mli index 1811150c..9bf6c175 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -12,29 +12,29 @@ open Util open Names open EConstr open Environ -open Globnames open Decl_kinds open Evd -open Misctypes open Tactypes open Clenv open Pattern -open Vernacexpr +open Typeclasses (** {6 General functions. } *) exception Bound -val decompose_app_bound : evar_map -> constr -> global_reference * constr array +val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array type debug = Debug | Info | Off val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t -val empty_hint_info : 'a hint_info_gen +val empty_hint_info : 'a Typeclasses.hint_info_gen (** Pre-created hint databases *) +type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen + type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -51,7 +51,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type hint_db_name = string type 'a with_metadata = private { @@ -72,6 +72,30 @@ type search_entry type hint_entry +type reference_or_constr = + | HintsReference of Libnames.qualid + | HintsConstr of Constrexpr.constr_expr + +type hint_mode = + | ModeInput (* No evars *) + | ModeNoHeadEvar (* No evar at the head *) + | ModeOutput (* Anything *) + +type 'a hints_transparency_target = + | HintsVariables + | HintsConstants + | HintsReferences of 'a list + +type hints_expr = + | HintsResolve of (hint_info_expr * bool * reference_or_constr) list + | HintsResolveIFF of bool * Libnames.qualid list * int option + | HintsImmediate of reference_or_constr list + | HintsUnfold of Libnames.qualid list + | HintsTransparency of Libnames.qualid hints_transparency_target * bool + | HintsMode of Libnames.qualid * hint_mode list + | HintsConstructors of Libnames.qualid list + | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument + type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen | PathStar of 'a hints_path_gen @@ -80,8 +104,8 @@ type 'a hints_path_gen = | PathEmpty | PathEpsilon -type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type pre_hints_path = Libnames.qualid hints_path_gen +type hints_path = GlobRef.t hints_path_gen val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool @@ -91,15 +115,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t val pp_hints_path : hints_path -> Pp.t val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : - Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen + Libnames.qualid hints_path_atom_gen -> GlobRef.t hints_path_atom_gen val glob_hints_path : - Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen + Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t - val find : global_reference -> t -> search_entry + val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. * [secvars] represent the set of section variables that @@ -107,27 +131,27 @@ module Hint_db : val map_none : secvars:Id.Pred.t -> t -> full_hint list (** All hints associated to the reference *) - val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list + val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list + val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * 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 -> + val remove_one : GlobRef.t -> t -> t + val remove_list : GlobRef.t list -> t -> t + val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool @@ -144,10 +168,8 @@ type hint_db = Hint_db.t type hnf = bool -type hint_info = (patvar list * constr_pattern) hint_info_gen - type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type hints_entry = @@ -156,8 +178,8 @@ type hints_entry = | 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 * hint_mode list + | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument val searchtable_map : hint_db_name -> hint_db @@ -171,7 +193,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit -val remove_hints : bool -> hint_db_name list -> global_reference list -> unit +val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit val current_db_names : unit -> String.Set.t @@ -179,7 +201,7 @@ val current_pure_db : unit -> hint_db list val interp_hints : polymorphic -> hints_expr -> hints_entry -val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit +val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> (bool * bool) (* polymorphic or monomorphic, local or global *) -> @@ -264,7 +286,7 @@ val rewrite_db : hint_db_name val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t @@ -274,3 +296,5 @@ val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) val add_hints_init : (unit -> unit) -> unit +type nonrec hint_info = hint_info +[@@ocaml.deprecated "Use [Typeclasses.hint_info]"] diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b012a7ec..7da059ae 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -12,7 +12,7 @@ open Pp open CErrors open Util open Names -open Term +open Constr open Termops open EConstr open Inductiveops @@ -263,7 +263,9 @@ open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) let mkGApp f args = DAst.make @@ GApp (f, args) let mkGHole = DAst.make @@ - GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None) + GHole (QuestionMark { + Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Define false; + }, Namegen.IntroAnonymous, None) let mkGProd id c1 c2 = DAst.make @@ GProd (Name (Id.of_string id), Explicit, c1, c2) let mkGArrow c1 c2 = DAst.make @@ @@ -294,13 +296,13 @@ let match_with_equation env sigma t = let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if eq_gr (IndRef ind) glob_eq then + if GlobRef.equal (IndRef ind) glob_eq then Some (build_coq_eq_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_identity then + else if GlobRef.equal (IndRef ind) glob_identity then Some (build_coq_identity_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_jmeq then + else if GlobRef.equal (IndRef ind) glob_jmeq then Some (build_coq_jmeq_data()),hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 0697d0f1..f04cda12 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr +val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 62ead57f..e4013152 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) = (subst_ind subst ind,subst_constant subst const) let subst_scheme (subst,(kind,l)) = - (kind,Array.map (subst_one_scheme subst) l) + (kind,Array.Smart.map (subst_one_scheme subst) l) let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> @@ -123,7 +123,7 @@ let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in let ctx = UState.minimize univs in - let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in + let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) @@ -154,7 +154,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define mode id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; - const, Safe_typing.add_private + const, Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = @@ -174,7 +174,7 @@ let define_mutual_scheme_base kind suff f mode names mind = let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, - Safe_typing.add_private + Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) (Array.to_list schemes)) eff @@ -187,7 +187,7 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.add_private + s, Safe_typing.concat_private (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind, s]) Safe_typing.empty_private_constants diff --git a/tactics/inv.ml b/tactics/inv.ml index 067fc894..43786c8e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -14,6 +14,7 @@ open Util open Names open Term open Termops +open Constr open EConstr open Vars open Namegen @@ -25,7 +26,7 @@ open Tacticals.New open Tactics open Elim open Equality -open Misctypes +open Tactypes open Proofview.Notations module NamedDecl = Context.Named.Declaration @@ -64,6 +65,11 @@ let var_occurs_in_pf gl id = type inversion_status = Dep of constr option | NoDep +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + let compute_eqn env sigma n i ai = (mkRel (n-i),get_type_of env sigma (mkRel (n-i))) @@ -88,7 +94,7 @@ let make_inv_predicate env evd indf realargs id status concl = | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> let sort = get_sort_family_of env !evd concl in - let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in + let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in let p = make_arity env !evd true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env !evd p concl (realargs@[mkVar id]) @@ -119,12 +125,10 @@ let make_inv_predicate env evd indf realargs id status concl = in let eq_term = eqdata.Coqlib.eq in let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in - let eq = EConstr.of_constr eq in let eqn = applist (eq,[eqnty;lhs;rhs]) in let eqns = (Anonymous, lift n eqn) :: eqns in let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in - let refl_term = EConstr.of_constr refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in @@ -289,7 +293,7 @@ let error_too_many_names pats = str "Unexpected " ++ str (String.plural (List.length pats) "introduction pattern") ++ str ": " ++ pr_enum (Miscprint.pr_intro_pattern - (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++ + (fun c -> Printer.pr_econstr_env env sigma (snd (c env (Evd.from_env env))))) pats ++ str ".") let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with @@ -328,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function (tacfun (get_names allow_conj a)) (tclMAP_i allow_conj (n-1) tacfun l) -let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id +let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input @@ -371,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = [if as_mode then clear [id] else tclIDTAC; (tclMAP_i (false,false) neqns (function (idopt,_) -> tclTRY (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) @@ -400,7 +404,7 @@ let nLastDecls i tac = let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in - let first_eq = ref MoveLast in + let first_eq = ref Logic.MoveLast in let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in match othin with | Some thin -> @@ -412,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba = (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx))); tclMAP_i (true,false) neqns (fun (idopt,names) -> (tclTHEN - (intro_move_avoid idopt avoid MoveLast) + (intro_move_avoid idopt avoid Logic.MoveLast) (onLastHypId (fun id -> tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) let idopt = if as_mode then Some (NamedDecl.get_id d) else None in - intro_move idopt (if thin then MoveLast else !first_eq)) + intro_move idopt (if thin then Logic.MoveLast else !first_eq)) nodepids; (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)] | None -> (* simple inversion *) if as_mode then tclMAP_i (false,true) neqns (fun (idopt,_) -> - intro_move idopt MoveLast) names + intro_move idopt Logic.MoveLast) names else (tclTHENLIST [tclDO neqns intro; @@ -465,7 +469,7 @@ let raw_inversion inv_kind id status names = make_inv_predicate env evdref indf realargs id status concl in let sigma = !evdref in let (cut_concl,case_tac) = - if status != NoDep && (dependent sigma c concl) then + if status != NoDep && (local_occur_var sigma id concl) then Reductionops.beta_applist sigma (elim_predicate, realargs@[c]), case_then_using else @@ -491,11 +495,12 @@ let raw_inversion inv_kind id status names = (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError - (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Prop Pos as k),i)) -> + (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( (strbrk "Inversion would require case analysis on sort " ++ - pr_sort Evd.empty k ++ + pr_sort sigma k ++ strbrk " which is not allowed for inductive definition " ++ pr_inductive env (fst i) ++ str ".")) | e -> Proofview.tclZERO ~info e diff --git a/tactics/inv.mli b/tactics/inv.mli index c63d57af..bbd1f335 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -10,11 +10,15 @@ open Names open EConstr -open Misctypes open Tactypes type inversion_status = Dep of constr option | NoDep +type inversion_kind = + | SimpleInversion + | FullInversion + | FullInversionClear + val inv_clause : inversion_kind -> or_and_intro_pattern option -> Id.t list -> quantified_hypothesis -> unit Proofview.tactic diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a4cdc159..caf4c1ec 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -12,9 +12,9 @@ open Pp open CErrors open Util open Names -open Term open Termops open Environ +open Constr open EConstr open Vars open Namegen @@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op = let c = fill_holes pfterm in (* warning: side-effect on ownSign *) let invProof = it_mkNamedLambda_or_LetIn c !ownSign in - let invProof = EConstr.Unsafe.to_constr invProof in - let p = Evarutil.nf_evars_universes sigma invProof in - p, sigma + let p = EConstr.to_constr sigma invProof in + p, sigma let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in @@ -252,7 +251,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_type_evars env sigma com in - let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in + let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in try add_inversion_lemma ~poly na env sigma c sort bool tac with diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 2337a790..f42e5a8b 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -11,7 +11,7 @@ open Names open EConstr open Constrexpr -open Misctypes +open Tactypes val lemInv_clause : quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 958a205a..596feeec 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -159,8 +159,6 @@ type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) -open Misctypes - let fix_empty_or_and_pattern nv l = (* 1- The syntax does not distinguish between "[ ]" for one clause with no names and "[ ]" for no clause at all *) @@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns = if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2; if Int.equal p p1 then IntroAndPattern - (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l) + (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l) else names else @@ -225,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function let compute_induction_names = compute_induction_names_gen true (* Compute the let-in signature of case analysis or standard induction scheme *) -let compute_constructor_signatures isrec ((_,k as ity),u) = +let compute_constructor_signatures ~rec_flag ((_,k as ity),u) = let rec analrec c recargs = match Constr.kind c, recargs with | Prod (_,_,c), recarg::rest -> @@ -233,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) = begin match Declareops.dest_recarg recarg with | Norec | Imbr _ -> true :: rest | Mrec (_,j) -> - if isrec && Int.equal j k then true :: true :: rest + if rec_flag && Int.equal j k then true :: true :: rest else true :: rest end | LetIn (_,_,_,c), rest -> false :: analrec c rest @@ -263,7 +261,7 @@ let pf_with_evars glsev k gls = tclTHEN (Refiner.tclEVARS evd) (k a) gls let pf_constr_of_global gr k = - pf_with_evars (fun gls -> on_snd EConstr.of_constr (pf_apply Evd.fresh_global gls gr)) k + pf_with_evars (fun gls -> pf_apply Evd.fresh_global gls gr) k (** Tacticals of Ltac defined directly in term of Proofview *) module New = struct @@ -369,9 +367,36 @@ module New = struct tclTHENSFIRSTn t1 l (tclUNIT()) let tclTHENFIRST t1 t2 = tclTHENFIRSTn t1 [|t2|] + + let tclBINDFIRST t1 t2 = + t1 >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + match gls with + | [] -> tclFAIL 0 (str "Expect at least one goal.") + | hd::tl -> + Proofview.Unsafe.tclSETGOALS [hd] <*> t2 ans >>= fun ans -> + Proofview.Unsafe.tclNEWGOALS tl <*> + Proofview.tclUNIT ans + let tclTHENLASTn t1 l = tclTHENS3PARTS t1 [||] (tclUNIT()) l let tclTHENLAST t1 t2 = tclTHENLASTn t1 [|t2|] + + let option_of_failure f x = try Some (f x) with Failure _ -> None + + let tclBINDLAST t1 t2 = + t1 >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun gls -> + match option_of_failure List.sep_last gls with + | None -> tclFAIL 0 (str "Expect at least one goal.") + | Some (last,firstn) -> + Proofview.Unsafe.tclSETGOALS [last] <*> t2 ans >>= fun ans -> + Proofview.Unsafe.tclGETGOALS >>= fun newgls -> + tclEVARMAP >>= fun sigma -> + let firstn = Proofview.Unsafe.undefined sigma firstn in + Proofview.Unsafe.tclSETGOALS (firstn@newgls) <*> + Proofview.tclUNIT ans + let tclTHENS t l = tclINDEPENDENT begin t <*>Proofview.tclORELSE (* converts the [SizeMismatch] error into an ltac error *) @@ -465,11 +490,13 @@ module New = struct Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) (* Select a subset of the goals *) - let tclSELECT = function - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> fun tac -> tac + let tclSELECT = let open Goal_select in function + | SelectNth i -> Proofview.tclFOCUS i i + | SelectList l -> Proofview.tclFOCUSLIST l + | SelectId id -> Proofview.tclFOCUSID id + | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | SelectAlreadyFocused -> + anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) @@ -479,8 +506,8 @@ module New = struct let evi = Evd.find sigma evk in match Evd.evar_body evi with | Evd.Evar_empty -> Some (evk,evi) - | Evd.Evar_defined c -> match Constr.kind c with - | Term.Evar (evk,l) -> is_undefined_up_to_restriction sigma evk + | Evd.Evar_defined c -> match Constr.kind (EConstr.Unsafe.to_constr c) with + | Evar (evk,l) -> is_undefined_up_to_restriction sigma evk | _ -> (* We make the assumption that there is no way to refine an evar remaining after typing from the initial term given to @@ -607,7 +634,7 @@ module New = struct (* Find the right elimination suffix corresponding to the sort of the goal *) (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim - isrec allnames tac predicate ind (c, t) = + rec_flag allnames tac predicate ind (c, t) = Proofview.Goal.enter begin fun gl -> let sigma, elim = mk_elim ind gl in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in @@ -628,15 +655,14 @@ module New = struct | _ -> let name_elim = match EConstr.kind sigma elim with - | Const (kn, _) -> Constant.to_string kn - | Var id -> Id.to_string id - | _ -> "\b" + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim + | _ -> mt () in user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in - let branchsigns = compute_constructor_signatures isrec ind in + let branchsigns = compute_constructor_signatures ~rec_flag ind in let brnames = compute_induction_names_gen false branchsigns allnames in let flags = Unification.elim_flags () in let elimclause' = @@ -659,7 +685,7 @@ module New = struct in let branchtacs = List.init (Array.length branchsigns) after_tac in Proofview.tclTHEN - (Clenvtac.clenv_refine false clenv') + (Clenvtac.clenv_refine clenv') (Proofview.tclEXTEND [] tclIDTAC branchtacs) end) end @@ -682,7 +708,7 @@ module New = struct let gl_make_elim ind = begin fun gl -> let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in let (sigma, c) = pf_apply Evd.fresh_global gl gr in - (sigma, EConstr.of_constr c) + (sigma, c) end let gl_make_case_dep (ind, u) = begin fun gl -> @@ -726,8 +752,8 @@ module New = struct let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with - | None -> true,gl_make_elim - | Some _ -> false,gl_make_case_dep + | NotRecord -> true,gl_make_elim + | FakeRecord | PrimRecord _ -> false,gl_make_case_dep in general_elim_then_using mkelim isrec None tac None ind (c, t) end @@ -742,7 +768,6 @@ module New = struct Proofview.tclEVARMAP >>= fun sigma -> Proofview.tclENV >>= fun env -> let (sigma, c) = Evd.fresh_global env sigma ref in - let c = EConstr.of_constr c in Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT c end diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index f0ebac78..1e66c2b0 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -14,7 +14,6 @@ open EConstr open Evd open Proof_type open Locus -open Misctypes open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) @@ -124,7 +123,7 @@ val fix_empty_or_and_pattern : int -> delayed_open_constr or_and_intro_pattern_expr -> delayed_open_constr or_and_intro_pattern_expr -val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array +val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool list array (** Useful for [as intro_pattern] modifier *) val compute_induction_names : @@ -135,7 +134,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic -val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic +val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic (** Tacticals defined directly in term of Proofview *) @@ -196,8 +195,10 @@ module New : sig (** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2] to the first resulting subgoal *) val tclTHENFIRST : unit tactic -> unit tactic -> unit tactic + val tclBINDFIRST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic val tclTHENLASTn : unit tactic -> unit tactic array -> unit tactic val tclTHENLAST : unit tactic -> unit tactic -> unit tactic + val tclBINDLAST : 'a tactic -> ('a -> 'b tactic) -> 'b tactic (* [tclTHENS t l = t <*> tclDISPATCH l] *) val tclTHENS : unit tactic -> unit tactic list -> unit tactic (* [tclTHENLIST [t1;…;tn]] is [t1<*>…<*>tn] *) @@ -221,7 +222,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic + val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic @@ -266,5 +267,5 @@ module New : sig val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic + val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dfdd3237..f060e494 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -43,7 +43,7 @@ open Pretype_errors open Unification open Locus open Locusops -open Misctypes +open Tactypes open Proofview.Notations open Context.Named.Declaration @@ -128,14 +128,14 @@ let unsafe_intro env store decl b = (sigma, mkNamedLambda_or_LetIn decl ev) end -let introduction ?(check=true) id = +let introduction id = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in let store = Proofview.Goal.extra gl in let env = Proofview.Goal.env gl in - let () = if check && mem_named_context_val id hyps then + let () = if mem_named_context_val id hyps then user_err ~hdr:"Tactics.introduction" (str "Variable " ++ Id.print id ++ str " is already declared.") in @@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k = let sigma = if check then begin ignore (Typing.unsafe_type_of env sigma ty); - let sigma,b = Reductionops.infer_conv env sigma ty conclty in - if not b then error "Not convertible."; - sigma + match Reductionops.infer_conv env sigma ty conclty with + | None -> error "Not convertible." + | Some sigma -> sigma end else sigma in let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in @@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = Proofview.Goal.enter begin fun gl -> - try - let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in - if b then Proofview.Unsafe.tclEVARS sigma - else Tacticals.New.tclFAIL 0 (str "Not convertible") - with (* Reduction.NotConvertible *) _ -> + match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with + | Some sigma -> Proofview.Unsafe.tclEVARS sigma + | None -> Tacticals.New.tclFAIL 0 (str "Not convertible") + | exception _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") end @@ -198,32 +197,46 @@ end let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y -let clear_dependency_msg env sigma id = function +let clear_in_global_msg = function + | None -> mt () + | Some ref -> str " implicitly in " ++ Printer.pr_global ref + +let clear_dependency_msg env sigma id err inglobal = + let pp = clear_in_global_msg inglobal in + match err with | Evarutil.OccurHypInSimpleClause None -> - Id.print id ++ str " is used in conclusion." + Id.print id ++ str " is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"." + Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." -let error_clear_dependency env sigma id err = - user_err (clear_dependency_msg env sigma id err) +let error_clear_dependency env sigma id err inglobal = + user_err (clear_dependency_msg env sigma id err inglobal) -let replacing_dependency_msg env sigma id = function +let replacing_dependency_msg env sigma id err inglobal = + let pp = clear_in_global_msg inglobal in + match err with | Evarutil.OccurHypInSimpleClause None -> - str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion." + str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> str "Cannot change " ++ Id.print id ++ - strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"." + strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." + | Evarutil.NoCandidatesLeft ev -> + str "Cannot change " ++ Id.print id ++ str " as it would leave the existential " ++ + Printer.pr_existential_key sigma ev ++ str" without candidates." -let error_replacing_dependency env sigma id err = - user_err (replacing_dependency_msg env sigma id err) +let error_replacing_dependency env sigma id err inglobal = + user_err (replacing_dependency_msg env sigma id err inglobal) (* This tactic enables the user to remove hypotheses from the signature. * Some care is taken to prevent him from removing variables that are @@ -239,13 +252,12 @@ let clear_gen fail = function let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let evdref = ref sigma in - let (hyps, concl) = - try clear_hyps_in_evi env evdref (named_context_val env) concl ids - with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err + let (sigma, hyps, concl) = + try clear_hyps_in_evi env sigma (named_context_val env) concl ids + with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal in let env = reset_with_named_context hyps env in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end) @@ -423,11 +435,10 @@ let get_previous_hyp_position env sigma id = let clear_hyps2 env sigma ids sign t cl = try - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency env sigma id err + let sigma = Evd.clear_metas sigma in + Evarutil.clear_hyps2_in_evi env sigma sign t cl ids + with Evarutil.ClearDependencyError (id,err,inglobal) -> + error_replacing_dependency env sigma id err inglobal let internal_cut_gen ?(check=true) dir replace id t = Proofview.Goal.enter begin fun gl -> @@ -439,7 +450,7 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign',t,concl,sigma = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in - let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in + let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma else @@ -557,20 +568,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> end end -let warning_nameless_fix = - CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () -> - str "fix/cofix without a name are deprecated, please use the named version.") - -let fix ido n = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_fix id n [] 0 - end - | Some id -> - mutual_fix id n [] 0 +let fix id n = mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in @@ -613,16 +611,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> end end -let cofix ido = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_cofix id [] 0 - end - | Some id -> - mutual_cofix id [] 0 +let cofix id = mutual_cofix id [] 0 (**************************************************************) (* Reduction and conversion tactics *) @@ -802,9 +791,9 @@ let e_change_in_hyp redfun (id,where) = (convert_hyp c) end -type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr +type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr -let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c) +let make_change_arg c pats env sigma = (sigma, replace_vars (Id.Map.bindings pats) c) let check_types env sigma mayneedglobalcheck deep newc origc = let t1 = Retyping.get_type_of env sigma newc in @@ -812,15 +801,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc = let t2 = Retyping.get_type_of env sigma origc in let sigma, t2 = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t2 in - let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in - if not b then + match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with + | None -> if isSort sigma (whd_all env sigma t1) && isSort sigma (whd_all env sigma t2) then (mayneedglobalcheck := true; sigma) else user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.") - else sigma + | Some sigma -> sigma end else if not (isSort sigma (whd_all env sigma t1)) then @@ -829,11 +818,11 @@ let check_types env sigma mayneedglobalcheck deep newc origc = (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb mayneedglobalcheck deep t env sigma c = - let (sigma, t') = t sigma in + let (sigma, t') = t env sigma in let sigma = check_types env sigma mayneedglobalcheck deep t' c in - let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in - if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible."); - (sigma, t') + match infer_conv ~pb:cv_pb env sigma t' c with + | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible."); + | Some sigma -> (sigma, t') (* Use cumulativity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb deep t where env sigma c = @@ -971,6 +960,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac + | Evar ev when force_flag -> + let sigma, t = Evardefine.define_evar_as_product sigma ev in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (intro_then_gen name_flag move_flag force_flag dep_flag tac) | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) @@ -1108,7 +1102,13 @@ let msg_quantified_hypothesis = function pr_nth n ++ str " non dependent hypothesis" +let warn_deprecated_intros_until_0 = + CWarnings.create ~name:"deprecated-intros-until-0" ~category:"tactics" + (fun () -> + strbrk"\"intros until 0\" is deprecated, use \"intros *\"; instead of \"induction 0\" and \"destruct 0\" use explicitly a name.\"") + let depth_of_quantified_hypothesis red h gl = + if h = AnonHyp 0 then warn_deprecated_intros_until_0 (); match lookup_hypothesis_as_renamed_gen red h gl with | Some depth -> depth | None -> @@ -1159,6 +1159,18 @@ let tactic_infer_flags with_evar = { Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of lident + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> @@ -1251,7 +1263,6 @@ let cut c = end let error_uninstantiated_metas t clenv = - let t = EConstr.Unsafe.to_constr t in let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.") in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".") @@ -1261,7 +1272,7 @@ let check_unresolved_evars_of_metas sigma clenv = (* Refiner.pose_all_metas_as_evars are resolved *) List.iter (fun (mv,b) -> match b with | Clval (_,(c,_),_) -> - (match Constr.kind c.rebus with + (match Constr.kind (EConstr.Unsafe.to_constr c.rebus) with | Evar (evk,_) when Evd.is_undefined clenv.evd evk && not (Evd.mem sigma evk) -> error_uninstantiated_metas (mkMeta mv) clenv @@ -1281,7 +1292,7 @@ let do_replace id = function let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) targetid id sigma0 clenv tac = - let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in + let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in let clenv = if with_classes then { clenv with evd = Typeclasses.resolve_typeclasses @@ -1438,9 +1449,7 @@ let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations let find_ind_eliminator ind s gl = let gr = lookup_eliminator ind s in - let evd, c = Tacmach.New.pf_apply Evd.fresh_global gl gr in - let c = EConstr.of_constr c in - evd, c + Tacmach.New.pf_apply Evd.fresh_global gl gr let find_eliminator c gl = let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in @@ -1572,9 +1581,10 @@ let make_projection env sigma params cstr sign elim i n c u = | Some proj -> let args = Context.Rel.to_extended_vect mkRel 0 sign in let proj = - if Environ.is_projection proj env then + match Recordops.find_primitive_projection proj with + | Some proj -> mkProj (Projection.make proj false, mkApp (c, args)) - else + | None -> mkApp (mkConstU (proj,u), Array.append (Array.of_list params) [|mkApp (c, args)|]) in @@ -1639,13 +1649,11 @@ let tclORELSEOPT t k = Proofview.tclZERO ~info e | Some tac -> tac) -let general_apply with_delta with_destruct with_evars clear_flag - {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = +let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars + clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let flags = - if with_delta then default_unify_flags () else default_no_delta_unify_flags () in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) @@ -1654,7 +1662,12 @@ let general_apply with_delta with_destruct with_evars clear_flag Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - + let ts = + if respect_opaque then Conv_oracle.get_transp_state (oracle env) + else full_transparent_state + in + let flags = + if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in let try_apply thm_ty nprod = try @@ -1720,14 +1733,14 @@ let rec apply_with_bindings_gen b e = function (general_apply b b e k cb) (apply_with_bindings_gen b e cbl) -let apply_with_delayed_bindings_gen b e l = +let apply_with_delayed_bindings_gen b e l = let one k {CAst.loc;v=f} = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let (sigma, cb) = f env sigma in Tacticals.New.tclWITHHOLES e - (general_apply b b e k CAst.(make ?loc cb)) sigma + (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma end in let rec aux = function @@ -1802,14 +1815,12 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) = in aux (make_clenv_binding env sigma (d,thm) lbind) -let apply_in_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,{ CAst.loc; v= d,lbind}) tac = +let apply_in_once ?(respect_opaque = false) sidecond_first with_delta + with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac = let open Context.Rel.Declaration in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let flags = - if with_delta then default_unify_flags () else default_no_delta_unify_flags () in let t' = Tacmach.New.pf_get_hyp_typ id gl in let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in @@ -1817,6 +1828,12 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in + let ts = + if respect_opaque then Conv_oracle.get_transp_state (oracle env) + else full_transparent_state + in + let flags = + if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in try let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in clenv_refine_in ~sidecond_first with_evars targetid id sigma clause @@ -1836,14 +1853,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming aux [] with_destruct d end -let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming - id (clear_flag,{CAst.loc;v=f}) tac = +let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta + with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let (sigma, c) = f env sigma in Tacticals.New.tclWITHHOLES with_evars - (apply_in_once sidecond_first with_delta with_destruct with_evars + (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars naming id (clear_flag,CAst.(make ?loc c)) tac) sigma end @@ -1911,8 +1928,8 @@ let cast_no_check cast c = exact_no_check (mkCast (c, cast, concl)) end -let vm_cast_no_check c = cast_no_check Term.VMcast c -let native_cast_no_check c = cast_no_check Term.NATIVEcast c +let vm_cast_no_check c = cast_no_check VMcast c +let native_cast_no_check c = cast_no_check NATIVEcast c let exact_proof c = let open Tacmach.New in @@ -1935,16 +1952,19 @@ let assumption = let t = NamedDecl.get_type decl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in - let (sigma, is_same_type) = - if only_eq then (sigma, EConstr.eq_constr sigma t concl) + let ans = + if only_eq then + if EConstr.eq_constr sigma t concl then Some sigma + else None else let env = Proofview.Goal.env gl in infer_conv env sigma t concl in - if is_same_type then + match ans with + | Some sigma -> (Proofview.Unsafe.tclEVARS sigma) <*> exact_no_check (mkVar (NamedDecl.get_id decl)) - else arec gl only_eq rest + | None -> arec gl only_eq rest in let assumption_tac gl = let hyps = Proofview.Goal.hyps gl in @@ -1964,24 +1984,22 @@ let on_the_bodies = function exception DependsOnBody of Id.t option let check_is_type env sigma ty = - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - !evdref + let sigma, _ = Typing.sort_of env sigma ty in + sigma with e when CErrors.noncritical e -> raise (DependsOnBody None) let check_decl env sigma decl = let open Context.Named.Declaration in let ty = NamedDecl.get_type decl in - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - let _ = match decl with - | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.e_check env evdref c ty + let sigma, _ = Typing.sort_of env sigma ty in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,c,_) -> Typing.check env sigma c ty in - !evdref + sigma with e when CErrors.noncritical e -> let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) @@ -2252,7 +2270,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = let c = mkVar id in let t = Tacmach.New.pf_unsafe_type_of gl c in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in - let branchsigns = compute_constructor_signatures false ind in + let branchsigns = compute_constructor_signatures ~rec_flag:false ind in let nv_with_let = Array.map List.length branchsigns in let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in let ll = get_and_check_or_and_pattern ?loc ll branchsigns in @@ -2532,11 +2550,11 @@ let assert_as first hd ipat t = (* apply in as *) -let general_apply_in sidecond_first with_delta with_destruct with_evars - id lemmas ipat = +let general_apply_in ?(respect_opaque=false) sidecond_first with_delta + with_destruct with_evars id lemmas ipat = let tac (naming,lemma) tac id = - apply_in_delayed_once sidecond_first with_delta with_destruct with_evars - naming id lemma tac in + apply_in_delayed_once ~respect_opaque sidecond_first with_delta + with_destruct with_evars naming id lemma tac in Proofview.Goal.enter begin fun gl -> let destopt = if with_evars then MoveLast (* evars would depend on the whole context *) @@ -2567,7 +2585,7 @@ let apply_in simple with_evars id lemmas ipat = general_apply_in false simple simple with_evars id lemmas ipat let apply_delayed_in simple with_evars id lemmas ipat = - general_apply_in false simple simple with_evars id lemmas ipat + general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat (*****************************) (* Tactics abstracting terms *) @@ -2605,9 +2623,7 @@ let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in - let eq = EConstr.of_constr eq in let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in - let refl = EConstr.of_constr refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in @@ -2663,9 +2679,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in - let eq = EConstr.of_constr eq in let (sigma, refl) = Evd.fresh_global env sigma eqdata.refl in - let refl = EConstr.of_constr refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in @@ -3003,8 +3017,24 @@ let unfold_body x = end end +let warn_cannot_remove_as_expected = + CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics" + (fun (id,inglobal) -> + let pp = match inglobal with + | None -> mt () + | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in + str "Cannot remove " ++ Id.print id ++ pp ++ str ".") + +let clear_for_destruct ids = + Proofview.tclORELSE + (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids) + (function + | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT () + | e -> iraise e) + (* Either unfold and clear if defined or simply clear if not a definition *) -let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] +let expand_hyp id = + Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id] (*****************************) (* High-level induction *) @@ -3420,7 +3450,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) @@ -3782,7 +3812,10 @@ let specialize_eqs id = let ty = Tacmach.New.pf_get_hyp_typ id gl in let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = - compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 + compare_upto_variables !evars c1 c2 && + (match Evarconv.conv env !evars c1 c2 with + | Some sigma -> evars := sigma; true + | None -> false) in let rec aux in_eqs ctx acc ty = match EConstr.kind !evars ty with @@ -3807,7 +3840,8 @@ let specialize_eqs id = | _ -> if in_eqs then acc, in_eqs, ctx, ty else - let e = e_new_evar (push_rel_context ctx env) evars t in + let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in + evars := sigma; aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in @@ -4176,7 +4210,7 @@ let induction_tac with_evars params indvars elim = let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in - Clenvtac.clenv_refine with_evars resolved + Clenvtac.clenv_refine ~with_evars resolved end (* Apply induction "in place" taking into account dependent @@ -4334,7 +4368,7 @@ let check_expected_type env sigma (elimc,bl) elimt = let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in let (_,u,_) = destProd sigma cl.cl_concl in - fun t -> Evarconv.e_cumul env (ref sigma) t u + fun t -> Option.has_some (Evarconv.cumul env sigma t u) let check_enough_applied env sigma elim = (* A heuristic to decide whether the induction arg is enough applied *) @@ -4927,9 +4961,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd, nf = nf_evars_and_universes !evdref in + let evd = Evd.minimize_universes !evdref in let ctx = Evd.universe_context_set evd in - evd, ctx, nf concl + evd, ctx, Evarutil.nf_evars_universes evd concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in @@ -4973,7 +5007,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd = Evd.set_universe_context evd ectx in let open Safe_typing in let eff = private_con_of_con (Global.safe_env ()) cst in - let effs = add_private eff + let effs = concat_private eff Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> @@ -5007,6 +5041,26 @@ let tclABSTRACT ?(opaque=true) name_op tac = else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in abstract_subproof ~opaque s gk tac +let constr_eq ~strict x y = + let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in + let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + match EConstr.eq_constr_universes env evd x y with + | Some csts -> + let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in + if strict then + if Evd.check_constraints evd csts then Proofview.tclUNIT () + else fail_universes + else + (match Evd.add_constraints evd csts with + | evd -> Proofview.Unsafe.tclEVARS evd + | exception Univ.UniverseInconsistency _ -> + fail_universes) + | None -> fail + end + let unify ?(state=full_transparent_state) x y = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 079baa3e..34b49f3b 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -16,10 +16,8 @@ open Proof_type open Evd open Clenv open Redexpr -open Globnames open Pattern open Unification -open Misctypes open Tactypes open Locus open Ltac_pretype @@ -35,16 +33,16 @@ val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) -val introduction : ?check:bool -> Id.t -> unit Proofview.tactic +val introduction : Id.t -> unit Proofview.tactic val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic -val fix : Id.t option -> int -> unit Proofview.tactic +val fix : Id.t -> int -> unit Proofview.tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic -val cofix : Id.t option -> unit Proofview.tactic +val cofix : Id.t -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic @@ -57,8 +55,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic -val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic -val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic +val intro_move : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) @@ -92,9 +90,22 @@ val intros_clearing : bool list -> unit Proofview.tactic val try_intros_until : (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic +type evars_flag = bool (* true = pose evars false = fail on evars *) +type rec_flag = bool (* true = recursive false = not recursive *) +type advanced_flag = bool (* true = advanced false = basic *) +type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) + (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) +type 'a core_destruction_arg = + | ElimOnConstr of 'a + | ElimOnIdent of lident + | ElimOnAnonHyp of int + +type 'a destruction_arg = + clear_flag * 'a core_destruction_arg + val onInductionArg : (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> constr with_bindings destruction_arg -> unit Proofview.tactic @@ -110,11 +121,11 @@ val use_clear_hyp_by_default : unit -> bool (** {6 Introduction tactics with eliminations. } *) val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic -val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns -> +val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns -> +val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns -> unit Proofview.tactic -val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr -> +val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr -> unit Proofview.tactic (** Implements user-level "intros", with [] standing for "**" *) @@ -134,7 +145,7 @@ val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic type tactic_reduction = Reductionops.reduction_function type e_tactic_reduction = Reductionops.e_reduction_function -type change_arg = patvar_map -> evar_map -> evar_map * constr +type change_arg = patvar_map -> env -> evar_map -> evar_map * constr val make_change_arg : constr -> change_arg val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic @@ -169,7 +180,7 @@ val change : val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic -val unfold_constr : global_reference -> unit Proofview.tactic +val unfold_constr : GlobRef.t -> unit Proofview.tactic (** {6 Modification of the local context. } *) @@ -181,7 +192,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic -val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic +val move_hyp : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic val revert : Id.t list -> unit Proofview.tactic @@ -245,7 +256,7 @@ val apply_delayed_in : type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (** number of parameters *) predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) @@ -398,6 +409,11 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - (** {6 Other tactics. } *) +(** Syntactic equality up to universes. With [strict] the universe + constraints must be already true to succeed, without [strict] they + are added to the evar map. *) +val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic + val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 753c608a..8bdcc632 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -37,7 +37,7 @@ struct type 't t = | DRel | DSort - | DRef of global_reference + | DRef of GlobRef.t | DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *) | DLambda of 't * 't | DApp of 't * 't (* binary app *) @@ -290,7 +290,7 @@ struct | Const (c,u) -> Term (DRef (ConstRef c)) | Ind (i,u) -> Term (DRef (IndRef i)) | Construct (c,u)-> Term (DRef (ConstructRef c)) - | Term.Meta _ -> assert false + | Meta _ -> assert false | Evar (i,_) -> let meta = try Evar.Map.find i !metas diff --git a/tactics/term_dnet.mli b/tactics/term_dnet.mli index 2c748f9c..7bce5778 100644 --- a/tactics/term_dnet.mli +++ b/tactics/term_dnet.mli @@ -26,7 +26,7 @@ open Mod_subst The results returned here are perfect, since post-filtering is done inside here. - See lib/dnet.mli for more details. + See tactics/dnet.mli for more details. *) (** Identifiers to store (right hand side of the association) *) -- cgit v1.2.3