aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml74
-rw-r--r--tactics/auto.mli4
-rw-r--r--tactics/btermdn.ml83
-rw-r--r--tactics/btermdn.mli10
-rw-r--r--tactics/cbn.ml2
-rw-r--r--tactics/class_tactics.ml128
-rw-r--r--tactics/dn.ml12
-rw-r--r--tactics/dn.mli8
-rw-r--r--tactics/eauto.ml22
-rw-r--r--tactics/equality.ml10
-rw-r--r--tactics/equality.mli1
-rw-r--r--tactics/hints.ml201
-rw-r--r--tactics/hints.mli17
-rw-r--r--tactics/tactics.ml35
-rw-r--r--tactics/tactics.mli2
15 files changed, 330 insertions, 279 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3287c1c354..784322679f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -12,11 +12,9 @@ open Pp
open Util
open Names
open Termops
-open EConstr
open Environ
open Genredexpr
open Tactics
-open Clenv
open Locus
open Proofview.Notations
open Hints
@@ -69,38 +67,7 @@ let auto_unif_flags =
(* Try unification with the precompiled clause, then use registered Apply *)
-let connect_hint_clenv h gl =
- let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
- (* [clenv] has been generated by a hint-making function, so the only relevant
- data in its evarmap is the set of metas. The [evar_reset_evd] function
- below just replaces the metas of sigma by those coming from the clenv. *)
- let sigma = Tacmach.New.project gl in
- let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
- (* Still, we need to update the universes *)
- let clenv, c =
- if h.hint_poly then
- (* Refresh the instance of the hint *)
- 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 emap evd;
- env = Proofview.Goal.env gl;
- } in
- clenv, emap c
- else
- let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
- { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
- in clenv, c
-
-let unify_resolve flags (h : hint) =
- Proofview.Goal.enter begin fun gl ->
- let clenv, c = connect_hint_clenv h gl in
- Clenv.res_pf ~flags clenv
- end
+let unify_resolve flags h = Hints.hint_res_pf ~flags h
let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
@@ -110,10 +77,10 @@ let unify_resolve_gen = function
let exact h =
Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv h gl in
- Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
- (exact_check c)
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, c = Hints.fresh_hint env sigma h in
+ Proofview.Unsafe.tclEVARS sigma <*> exact_check c
end
(* Util *)
@@ -299,7 +266,7 @@ let flags_of_state st =
let auto_flags_of_state st =
auto_unif_flags_of TransparentState.full st
-let hintmap_of sigma secvars hdc concl =
+let hintmap_of env sigma secvars hdc concl =
match hdc with
| None -> Hint_db.map_none ~secvars
| Some hdc ->
@@ -307,7 +274,7 @@ let hintmap_of sigma secvars hdc concl =
(fun db -> match Hint_db.map_existential sigma ~secvars hdc concl db with
| ModeMatch l -> l
| ModeMismatch -> [])
- else Hint_db.map_auto sigma ~secvars hdc concl
+ else Hint_db.map_auto env sigma ~secvars hdc concl
let exists_evaluable_reference env = function
| EvalConstRef _ -> true
@@ -333,23 +300,24 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
Proofview.Goal.enter begin fun gl ->
let concl = Tacmach.New.pf_concl gl in
let sigma = Tacmach.New.project gl in
+ let env = Proofview.Goal.env gl in
let secvars = compute_secvars gl in
Tacticals.New.tclFIRST
((dbg_assumption dbg)::intro_tac::
(List.map Tacticals.New.tclCOMPLETE
- (trivial_resolve sigma dbg mod_delta db_list local_db secvars concl)))
+ (trivial_resolve env sigma dbg mod_delta db_list local_db secvars concl)))
end
-and my_find_search_nodelta sigma db_list local_db secvars hdc concl =
+and my_find_search_nodelta env sigma db_list local_db secvars hdc concl =
List.map (fun hint -> (None,hint))
- (List.map_append (hintmap_of sigma secvars hdc concl) (local_db::db_list))
+ (List.map_append (hintmap_of env sigma secvars hdc concl) (local_db::db_list))
and my_find_search mod_delta =
if mod_delta then my_find_search_delta
else my_find_search_nodelta
-and my_find_search_delta sigma db_list local_db secvars hdc concl =
- let f = hintmap_of sigma secvars hdc concl in
+and my_find_search_delta env sigma db_list local_db secvars hdc concl =
+ let f = hintmap_of env sigma secvars hdc concl in
if occur_existential sigma concl then
List.map_append
(fun db ->
@@ -373,7 +341,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
| None -> Hint_db.map_none ~secvars db
| Some hdc ->
if TransparentState.is_empty st
- then Hint_db.map_auto sigma ~secvars hdc concl db
+ then Hint_db.map_auto env sigma ~secvars hdc concl db
else match Hint_db.map_existential sigma ~secvars hdc concl db with
| ModeMatch l -> l
| ModeMismatch -> []
@@ -402,8 +370,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) =
let info = Exninfo.reify () in
Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
end
- | Extern tacast ->
- let p = FullHint.pattern h in
+ | Extern (p, tacast) ->
conclPattern concl p tacast
in
let pr_hint env sigma =
@@ -415,7 +382,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) =
in
tclLOG dbg pr_hint (FullHint.run h tactic)
-and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
+and trivial_resolve env sigma dbg mod_delta db_list local_db secvars cl =
try
let head =
try let hdconstr = decompose_app_bound sigma cl in
@@ -424,7 +391,7 @@ and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
in
List.map (tac_of_hint dbg db_list local_db cl)
(priority
- (my_find_search mod_delta sigma db_list local_db secvars head cl))
+ (my_find_search mod_delta env sigma db_list local_db secvars head cl))
with Not_found -> []
(** The use of the "core" database can be de-activated by passing
@@ -464,7 +431,7 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
(* The classical Auto tactic *)
(**************************************************************************)
-let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
+let possible_resolve env sigma dbg mod_delta db_list local_db secvars cl =
try
let head =
try let hdconstr = decompose_app_bound sigma cl in
@@ -472,7 +439,7 @@ let possible_resolve sigma dbg mod_delta db_list local_db secvars cl =
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
- (my_find_search mod_delta sigma db_list local_db secvars head cl)
+ (my_find_search mod_delta env sigma db_list local_db secvars head cl)
with Not_found -> []
let extend_local_db decl db gl =
@@ -507,12 +474,13 @@ let search d n mod_delta db_list local_db =
( Proofview.Goal.enter begin fun gl ->
let concl = Tacmach.New.pf_concl gl in
let sigma = Tacmach.New.project gl in
+ let env = Proofview.Goal.env gl in
let secvars = compute_secvars gl in
let d' = incr_dbg d in
Tacticals.New.tclFIRST
(List.map
(fun ntac -> Tacticals.New.tclTHEN ntac (search d' (n-1) local_db))
- (possible_resolve sigma d mod_delta db_list local_db secvars concl))
+ (possible_resolve env sigma d mod_delta db_list local_db secvars concl))
end))
end []
in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 903da143d2..bc2eee0e4c 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -12,7 +12,6 @@
open Names
open EConstr
-open Clenv
open Pattern
open Hints
open Tactypes
@@ -23,9 +22,6 @@ val default_search_depth : int ref
val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
-val connect_hint_clenv
- : hint -> Proofview.Goal.t -> clausenv * constr
-
(** Try unification with the precompiled clause, then use registered Apply *)
val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index bb062bfc11..bacb5a7b8f 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -49,17 +49,25 @@ let decomp sigma t =
in
decrec [] t
-let constr_val_discr sigma t =
+let evaluable_constant c env =
+ (* This is a hack to work around a broken Print Module implementation, see
+ bug #2668. *)
+ if Environ.mem_constant c env then Environ.evaluable_constant c env
+ else true
+
+let constr_val_discr env sigma t =
let open GlobRef in
let c, l = decomp sigma t in
match EConstr.kind sigma c with
| Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
| Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
| Var id -> Label(GRLabel (VarRef id),l)
- | Const _ -> Everything
+ | Const (c, _) ->
+ if evaluable_constant c env then Everything
+ else Label(GRLabel (ConstRef c),l)
| _ -> Nothing
-let constr_pat_discr t =
+let constr_pat_discr env t =
if not (Patternops.occur_meta_pattern t) then
None
else
@@ -68,16 +76,23 @@ let constr_pat_discr t =
| PRef ((IndRef _) as ref), args
| PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
| PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
+ | PRef ((ConstRef c) as ref), args ->
+ if evaluable_constant c env then None
+ else Some (GRLabel ref, args)
| _ -> None
-let constr_val_discr_st sigma ts t =
+let constr_val_discr_st env sigma ts t =
let c, l = decomp sigma t in
let open GlobRef in
match EConstr.kind sigma c with
- | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
+ | Const (c,u) ->
+ if evaluable_constant c env && TransparentState.is_transparent_constant ts c then Everything
+ else Label(GRLabel (ConstRef c),l)
| Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
| Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
- | Var id -> if TransparentState.is_transparent_variable ts id then Everything else Label(GRLabel (VarRef id),l)
+ | Var id ->
+ if Environ.evaluable_named id env && TransparentState.is_transparent_variable ts id then Everything
+ else Label(GRLabel (VarRef id),l)
| Prod (n, d, c) -> Label(ProdLabel, [d; c])
| Lambda (n, d, c) ->
if List.is_empty l then
@@ -88,52 +103,54 @@ let constr_val_discr_st sigma ts t =
| Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _
| Proj _ | Int _ | Float _ | Array _ -> Nothing
-let constr_pat_discr_st ts t =
+let constr_pat_discr_st env ts t =
let open GlobRef in
match decomp_pat t with
| PRef ((IndRef _) as ref), args
| PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
- | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) ->
- Some(GRLabel ref,args)
+ | PRef ((VarRef v) as ref), args ->
+ if Environ.evaluable_named v env && (TransparentState.is_transparent_variable ts v) then None
+ else Some(GRLabel ref,args)
+ | PRef ((ConstRef c) as ref), args ->
+ if evaluable_constant c env && TransparentState.is_transparent_constant ts c then None
+ else Some (GRLabel ref, args)
| PVar v, args when not (TransparentState.is_transparent_variable ts v) ->
Some(GRLabel (VarRef v),args)
- | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) ->
- Some (GRLabel ref, args)
| PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
| PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c])
| PSort s, [] -> Some (SortLabel, [])
| _ -> None
-let bounded_constr_pat_discr_st st (t,depth) =
+let bounded_constr_pat_discr_st env st (t,depth) =
if Int.equal depth 0 then
None
else
- match constr_pat_discr_st st t with
+ match constr_pat_discr_st env st t with
| None -> None
| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
-let bounded_constr_val_discr_st sigma st (t,depth) =
+let bounded_constr_val_discr_st env sigma st (t,depth) =
if Int.equal depth 0 then
Nothing
else
- match constr_val_discr_st sigma st t with
+ match constr_val_discr_st env sigma st t with
| Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
| Nothing -> Nothing
| Everything -> Everything
-let bounded_constr_pat_discr (t,depth) =
+let bounded_constr_pat_discr env (t,depth) =
if Int.equal depth 0 then
None
else
- match constr_pat_discr t with
+ match constr_pat_discr env t with
| None -> None
| Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l)
-let bounded_constr_val_discr sigma (t,depth) =
+let bounded_constr_val_discr env sigma (t,depth) =
if Int.equal depth 0 then
Nothing
else
- match constr_val_discr sigma t with
+ match constr_val_discr env sigma t with
| Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l)
| Nothing -> Nothing
| Everything -> Everything
@@ -151,31 +168,23 @@ struct
type t = Dn.t
- let empty = Dn.empty
+ type pattern = Dn.pattern
- let add = function
- | None ->
- (fun dn (c,v) ->
- Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v))
- | Some st ->
- (fun dn (c,v) ->
- Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+ let pattern env st pat = match st with
+ | None -> Dn.pattern (bounded_constr_pat_discr env) (pat, !dnet_depth)
+ | Some st -> Dn.pattern (bounded_constr_pat_discr_st env st) (pat, !dnet_depth)
- let rmv = function
- | None ->
- (fun dn (c,v) ->
- Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v))
- | Some st ->
- (fun dn (c,v) ->
- Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v))
+ let empty = Dn.empty
+ let add = Dn.add
+ let rmv = Dn.rmv
- let lookup sigma = function
+ let lookup env sigma = function
| None ->
(fun dn t ->
- Dn.lookup dn (bounded_constr_val_discr sigma) (t,!dnet_depth))
+ Dn.lookup dn (bounded_constr_val_discr env sigma) (t,!dnet_depth))
| Some st ->
(fun dn t ->
- Dn.lookup dn (bounded_constr_val_discr_st sigma st) (t,!dnet_depth))
+ Dn.lookup dn (bounded_constr_val_discr_st env sigma st) (t,!dnet_depth))
let app f dn = Dn.app f dn
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 4358e5a8d9..ab201a1872 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -28,12 +28,16 @@ module Make :
sig
type t
+ type pattern
+
+ val pattern : Environ.env -> TransparentState.t option -> constr_pattern -> pattern
+
val empty : t
- val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
- val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
+ val add : t -> pattern -> Z.t -> t
+ val rmv : t -> pattern -> Z.t -> t
- val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
+ val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
val app : (Z.t -> unit) -> t -> unit
end
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index dfbcc9fbce..8f0966a486 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -571,7 +571,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| None -> fold ())
| Const (c,u as const) ->
Reductionops.reduction_effect_hook env sigma c
- (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
+ (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,fst (Stack.strip_app stack)))));
if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
let u' = EInstance.kind sigma u in
match constant_value_in env (c, u') with
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 63cafbf76d..2f55cc071f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,61 +144,50 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
}
let e_give_exact flags h =
- let { hint_term = c; hint_clnv = clenv } = h in
let open Tacmach.New in
Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
let sigma = project gl in
- let c, sigma =
- if h.hint_poly then
- let clenv', subst = Clenv.refresh_undefined_univs clenv in
- let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
- let c = Vars.subst_univs_level_constr subst c in
- c, evd
- else c, sigma
- in
+ let sigma, c = Hints.fresh_hint env sigma h in
let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
Proofview.Unsafe.tclEVARS sigma <*>
Clenv.unify ~flags t1 <*> exact_no_check c
end
-let unify_e_resolve flags = begin fun gls (h, _) ->
- let clenv', c = connect_hint_clenv h gls in
- Clenv.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
- end
-
-let unify_resolve flags = begin fun gls (h, _) ->
- let clenv', _ = connect_hint_clenv h gls in
- Clenv.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
+let unify_resolve ~with_evars flags h diff = match diff with
+| None ->
+ Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h
+| Some (diff, ty) ->
+ let () = assert (not h.hint_poly) in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let sigma, c = Hints.fresh_hint env sigma h in
+ let clenv = mk_clenv_from_env env sigma (Some diff) (c, ty) in
+ Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv
end
(** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine flags gls (h, n) =
- let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in
+let unify_resolve_refine flags h diff =
+ let len = match diff with None -> None | Some (diff, _) -> Some diff in
+ Proofview.Goal.enter begin fun gls ->
let open Clenv in
let env = Proofview.Goal.env gls in
let concl = Proofview.Goal.concl gls in
Refine.refine ~typecheck:false begin fun sigma ->
- let sigma, term, ty =
- if h.hint_poly then
- 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
- else
- let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- sigma, c, t
- in
- let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
- let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
- let sigma' =
- Evarconv.(unify_leq_delay
- ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
- env sigma' cl.cl_concl concl)
- in (sigma', term) end
-
-let unify_resolve_refine flags gl clenv =
+ let sigma, term = Hints.fresh_hint env sigma h in
+ let ty = Retyping.get_type_of env sigma term in
+ let sigma, cl = Clenv.make_evar_clause env sigma ?len ty in
+ let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
+ let flags = Evarconv.default_flags_of flags.core_unify_flags.modulo_delta in
+ let sigma = Evarconv.unify_leq_delay ~flags env sigma cl.cl_concl concl in
+ (sigma, term)
+ end
+ end
+
+let unify_resolve_refine flags h diff =
Proofview.tclORELSE
- (unify_resolve_refine flags gl clenv)
+ (unify_resolve_refine flags h diff)
(fun (exn,info) ->
match exn with
| Evarconv.UnableToUnify _ ->
@@ -211,35 +200,21 @@ let unify_resolve_refine flags gl clenv =
(** Dealing with goals of the form A -> B and hints of the form
C -> A -> B.
*)
-let clenv_of_prods nprods h gl =
- let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
- if poly || Int.equal nprods 0 then Some (None, clenv)
- else
- let sigma = Tacmach.New.project gl in
- let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
- let diff = nb_prod sigma ty - nprods in
- if (>=) diff 0 then
- (* Was Some clenv... *)
- Some (Some diff,
- mk_clenv_from_n gl (Some diff) (c,ty))
- else None
-
let with_prods nprods h f =
if get_typeclasses_limit_intros () then
Proofview.Goal.enter begin fun gl ->
- try match clenv_of_prods nprods h gl with
- | None ->
- let info = Exninfo.reify () in
- Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
- | Some (diff, clenv') ->
- let h = { h with hint_clnv = clenv' } in
- f gl (h, diff)
- with e when CErrors.noncritical e ->
- let e, info = Exninfo.capture e in
- Proofview.tclZERO ~info e end
+ let { hint_term = c; hint_poly = poly } = h in
+ if poly || Int.equal nprods 0 then f None
+ else
+ let sigma = Tacmach.New.project gl in
+ let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+ let diff = nb_prod sigma ty - nprods in
+ if (>=) diff 0 then f (Some (diff, ty))
+ else Tacticals.New.tclZEROMSG (str"Not enough premisses")
+ end
else Proofview.Goal.enter
begin fun gl ->
- if Int.equal nprods 0 then f gl (h, None)
+ if Int.equal nprods 0 then f None
else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
let matches_pattern concl pat =
@@ -282,13 +257,13 @@ let shelve_dependencies gls =
Feedback.msg_debug (str" shelving dependent subgoals: " ++ pr_gls sigma gls);
shelve_goals gls)
-let hintmap_of sigma hdc secvars concl =
+let hintmap_of env sigma hdc secvars concl =
match hdc with
| None -> fun db -> ModeMatch (Hint_db.map_none ~secvars db)
| Some hdc ->
fun db ->
if Hint_db.use_dn db then (* Using dnet *)
- Hint_db.map_eauto sigma ~secvars hdc concl db
+ Hint_db.map_eauto env sigma ~secvars hdc concl db
else Hint_db.map_existential sigma ~secvars hdc concl db
(** Hack to properly solve dependent evars that are typeclasses *)
@@ -347,25 +322,25 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
if get_typeclasses_filtered_unification () then
let tac =
with_prods nprods h
- (fun gl clenv ->
+ (fun diff ->
matches_pattern concl p <*>
- unify_resolve_refine flags gl clenv)
+ unify_resolve_refine flags h diff)
in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
let tac =
- with_prods nprods h (unify_resolve flags) in
+ with_prods nprods h (unify_resolve ~with_evars:false flags h) in
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| ERes_pf h ->
if get_typeclasses_filtered_unification () then
let tac = (with_prods nprods h
- (fun gl clenv ->
+ (fun diff ->
matches_pattern concl p <*>
- unify_resolve_refine flags gl clenv)) in
+ unify_resolve_refine flags h diff)) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
let tac =
- with_prods nprods h (unify_e_resolve flags) in
+ with_prods nprods h (unify_resolve ~with_evars:true flags h) in
Proofview.tclBIND (Proofview.with_shelf tac)
(fun (gls, ()) -> shelve_dependencies gls)
| Give_exact h ->
@@ -373,18 +348,18 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
let tac =
matches_pattern concl p <*>
Proofview.Goal.enter
- (fun gl -> unify_resolve_refine flags gl (h, None)) in
+ (fun gl -> unify_resolve_refine flags h None) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
e_give_exact flags h
| Res_pf_THEN_trivial_fail h ->
- let fst = with_prods nprods h (unify_e_resolve flags) in
+ let fst = with_prods nprods h (unify_resolve ~with_evars:true flags h) in
let snd = if complete then Tacticals.New.tclIDTAC
else e_trivial_fail_db only_classes db_list local_db secvars in
Tacticals.New.tclTHEN fst snd
| Unfold_nth c ->
Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
- | Extern tacast -> conclPattern concl p tacast
+ | Extern (p, tacast) -> conclPattern concl p tacast
in
let tac = FullHint.run h tac in
let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
@@ -398,7 +373,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
| Extern _ -> (tac, b, true, name, lazy (FullHint.print env sigma h ++ pp))
| _ -> (tac, b, false, name, lazy (FullHint.print env sigma h ++ pp))
in
- let hint_of_db = hintmap_of sigma hdc secvars concl in
+ let hint_of_db = hintmap_of env sigma hdc secvars concl in
let hintl = List.map_filter (fun db -> match hint_of_db db with
| ModeMatch l -> Some (db, l)
| ModeMismatch -> None)
@@ -1235,8 +1210,7 @@ let autoapply c i =
(Hints.Hint_db.transparent_state hintdb) in
let cty = Tacmach.New.pf_get_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
- let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in
- unify_e_resolve flags gl (h, 0) <*>
+ Clenv.res_pf ~with_evars:true ~with_classes:false ~flags ce <*>
Proofview.tclEVARMAP >>= (fun sigma ->
let sigma = Typeclasses.make_unresolvables
(fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
diff --git a/tactics/dn.ml b/tactics/dn.ml
index e1c9b7c0b5..07eb49442a 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -38,6 +38,8 @@ struct
type t = Trie.t
+ type pattern = (Y.t * int) option list
+
let empty = Trie.empty
(* [path_of dna pat] returns the list of nodes of the pattern [pat] read in
@@ -89,11 +91,13 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
in
List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm))
- let add tm dna (pat,inf) =
- let p = path_of dna pat in Trie.add p (ZSet.singleton inf) tm
+ let pattern dna pat = path_of dna pat
+
+ let add tm p inf =
+ Trie.add p (ZSet.singleton inf) tm
- let rmv tm dna (pat,inf) =
- let p = path_of dna pat in Trie.remove p (ZSet.singleton inf) tm
+ let rmv tm p inf =
+ Trie.remove p (ZSet.singleton inf) tm
let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 2a60c3eb82..287aa2b257 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -18,9 +18,13 @@ sig
must decompose any tree into a label characterizing its root node and
the list of its subtree *)
- val add : t -> 'a decompose_fun -> 'a * Z.t -> t
+ type pattern
- val rmv : t -> 'a decompose_fun -> 'a * Z.t -> t
+ val pattern : 'a decompose_fun -> 'a -> pattern
+
+ val add : t -> pattern -> Z.t -> t
+
+ val rmv : t -> pattern -> Z.t -> t
type 'tree lookup_fun = 'tree -> (Y.t * 'tree list) lookup_res
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 686303a2ab..e920093648 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -19,7 +19,6 @@ open Tacticals
open Tacmach
open Evd
open Tactics
-open Clenv
open Auto
open Genredexpr
open Tactypes
@@ -66,12 +65,9 @@ open Auto
(***************************************************************************)
let unify_e_resolve flags h =
- Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv h gl in
- Clenv.res_pf ~with_evars:true ~with_classes:true ~flags clenv'
- end
+ Hints.hint_res_pf ~with_evars:true ~with_classes:true ~flags h
-let hintmap_of sigma secvars concl =
+let hintmap_of env sigma secvars concl =
(* Warning: for computation sharing, we need to return a closure *)
let hdc = try Some (decompose_app_bound sigma concl) with Bound -> None in
match hdc with
@@ -82,15 +78,15 @@ let hintmap_of sigma secvars concl =
match Hint_db.map_existential sigma ~secvars hdc concl db with
| ModeMatch l -> l
| ModeMismatch -> [])
- else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
+ else (fun db -> Hint_db.map_auto env sigma ~secvars hdc concl db)
(* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
let e_exact flags h =
Proofview.Goal.enter begin fun gl ->
- let clenv', c = connect_hint_clenv h gl in
- Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
- (e_give_exact c)
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, c = Hints.fresh_hint env sigma h in
+ Proofview.Unsafe.tclEVARS sigma <*> e_give_exact c
end
let rec e_trivial_fail_db db_list local_db =
@@ -110,7 +106,7 @@ let rec e_trivial_fail_db db_list local_db =
end
and e_my_find_search env sigma db_list local_db secvars concl =
- let hint_of_db = hintmap_of sigma secvars concl in
+ let hint_of_db = hintmap_of env sigma secvars concl in
let hintl =
List.map_append (fun db ->
let flags = auto_flags_of_state (Hint_db.transparent_state db) in
@@ -130,7 +126,7 @@ and e_my_find_search env sigma db_list local_db secvars concl =
Tacticals.New.tclTHEN (unify_e_resolve st h)
(e_trivial_fail_db db_list local_db)
| Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
- | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
+ | Extern (pat, tacast) -> conclPattern concl pat tacast
in
let tac = FullHint.run h tac in
(tac, b, lazy (FullHint.print env sigma h))
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a2325b69cc..b4def7bb51 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1134,6 +1134,7 @@ let make_tuple env sigma (rterm,rty) lind =
assert (not (noccurn sigma lind rty));
let sigdata = find_sigma_data env (get_sort_of env sigma rty) in
let sigma, a = type_of ~refresh:true env sigma (mkRel lind) in
+ let a = simpl env sigma a in
let na = Context.Rel.Declaration.get_annot (lookup_rel lind env) in
(* We move [lind] to [1] and lift other rels > [lind] by 1 *)
let rty = lift (1-lind) (liftn lind (lind+1) rty) in
@@ -1416,6 +1417,11 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
(if l2r then List.rev injectors else injectors)))
(tac (List.length injectors)))
+exception NothingToInject
+let () = CErrors.register_handler (function
+ | NothingToInject -> Some (Pp.str "Nothing to inject.")
+ | _ -> None)
+
let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
let env = eq_clause.env in
@@ -1429,7 +1435,7 @@ let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
" You can try to use option Set Keep Proof Equalities." in
tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
| Inr [([],_,_)] ->
- tclZEROMSG (str"Nothing to inject.")
+ Proofview.tclZERO NothingToInject
| Inr posns ->
inject_at_positions env sigma l2r u eq_clause posns
(tac (clenv_value eq_clause))
@@ -1644,7 +1650,7 @@ let cutSubstClause l2r eqn cls =
let warn_deprecated_cutrewrite =
CWarnings.create ~name:"deprecated-cutrewrite" ~category:"deprecated"
- (fun () -> strbrk"\"cutrewrite\" is deprecated. See documentation for proposed replacement.")
+ (fun () -> strbrk"\"cutrewrite\" is deprecated. Use \"replace\" instead.")
let cutRewriteClause l2r eqn cls =
warn_deprecated_cutrewrite ();
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e252eeab28..fdcbbc0e3c 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -91,6 +91,7 @@ val discr_tac : evars_flag ->
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 *)
+exception NothingToInject
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 ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 386224824f..db4b23705f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -42,21 +42,22 @@ type debug = Debug | Info | Off
exception Bound
-let head_constr_bound sigma t =
- let t = strip_outer_cast sigma t in
- let _,ccl = decompose_prod_assum sigma t in
- let hd,args = decompose_app sigma ccl in
- let open GlobRef in
- match EConstr.kind sigma hd with
- | Const (c, _) -> ConstRef c
- | Ind (i, _) -> IndRef i
- | Construct (c, _) -> ConstructRef c
- | Var id -> VarRef id
- | Proj (p, _) -> ConstRef (Projection.constant p)
- | _ -> raise Bound
+let rec head_bound sigma t = match EConstr.kind sigma t with
+| Prod (_, _, b) -> head_bound sigma b
+| LetIn (_, _, _, b) -> head_bound sigma b
+| App (c, _) -> head_bound sigma c
+| Case (_, _, _, c, _) -> head_bound sigma c
+| Ind (ind, _) -> GlobRef.IndRef ind
+| Const (c, _) -> GlobRef.ConstRef c
+| Construct (c, _) -> GlobRef.ConstructRef c
+| Var id -> GlobRef.VarRef id
+| Proj (p, _) -> GlobRef.ConstRef (Projection.constant p)
+| Cast (c, _, _) -> head_bound sigma c
+| Evar _ | Rel _ | Meta _ | Sort _ | Fix _ | Lambda _
+| CoFix _ | Int _ | Float _ | Array _ -> raise Bound
let head_constr sigma c =
- try head_constr_bound sigma c
+ try head_bound sigma c
with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \
(co)inductive type, (co)inductive type constructor, or projection.")
@@ -105,7 +106,7 @@ type 'a hint_ast =
| Give_exact of 'a
| Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
| Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of Genarg.glob_generic_argument (* Hint Extern *)
+ | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *)
type 'a hints_path_atom_gen =
@@ -237,10 +238,38 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
type stored_data = int * full_hint
(* First component is the index of insertion in the table, to keep most recent first semantics. *)
-module Bounded_net = Btermdn.Make(struct
- type t = stored_data
- let compare = pri_order_int
- end)
+module Bounded_net :
+sig
+ type t
+ val empty : t
+ val add : TransparentState.t option -> t -> Pattern.constr_pattern -> stored_data -> t
+ val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list
+end =
+struct
+ module Data = struct type t = stored_data let compare = pri_order_int end
+ module Bnet = Btermdn.Make(Data)
+
+ type diff = Pattern.constr_pattern * stored_data
+ type data = Bnet of Bnet.t | Diff of diff * data ref
+ type t = data ref
+
+ let empty = ref (Bnet Bnet.empty)
+
+ let add _st net p v = ref (Diff ((p, v), net))
+
+ let rec force env st net = match !net with
+ | Bnet dn -> dn
+ | Diff ((p, v), rem) ->
+ let dn = force env st rem in
+ let p = Bnet.pattern env st p in
+ let dn = Bnet.add dn p v in
+ let () = net := (Bnet dn) in
+ dn
+
+ let lookup env sigma st net p =
+ let dn = force env st net in
+ Bnet.lookup env sigma st dn p
+end
type search_entry = {
sentry_nopat : stored_data list;
@@ -258,27 +287,28 @@ let empty_se = {
let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid
-let add_tac pat t st se =
+let add_tac pat t se =
match pat with
| None ->
if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat }
- | Some pat ->
+ | Some (st, pat) ->
if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
else { se with
sentry_pat = List.insert pri_order t se.sentry_pat;
- sentry_bnet = Bounded_net.add st se.sentry_bnet (pat, t); }
+ sentry_bnet = Bounded_net.add st se.sentry_bnet pat t; }
let rebuild_dn st se =
let dn' =
List.fold_left
- (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
+ (fun dn (id, t) ->
+ Bounded_net.add (Some st) dn (Option.get t.pat) (id, t))
Bounded_net.empty se.sentry_pat
in
{ se with sentry_bnet = dn' }
-let lookup_tacs sigma concl st se =
- let l' = Bounded_net.lookup sigma st se.sentry_bnet concl in
+let lookup_tacs env sigma concl st se =
+ let l' = Bounded_net.lookup env sigma st se.sentry_bnet concl in
let sl' = List.stable_sort pri_order_int l' in
List.merge pri_order_int se.sentry_nopat sl'
@@ -320,8 +350,7 @@ let instantiate_hint env sigma p =
| Res_pf_THEN_trivial_fail c ->
Res_pf_THEN_trivial_fail (mk_clenv c)
| Give_exact c -> Give_exact (mk_clenv c)
- | Unfold_nth e -> Unfold_nth e
- | Extern t -> Extern t
+ | (Unfold_nth _ | Extern _) as h -> h
in
{ p with code = { p.code with obj = code } }
@@ -500,14 +529,14 @@ val map_none : secvars:Id.Pred.t -> 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 ->
(GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
-val map_eauto : evar_map -> secvars:Id.Pred.t ->
+val map_eauto : Environ.env -> evar_map -> secvars:Id.Pred.t ->
(GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
-val map_auto : evar_map -> secvars:Id.Pred.t ->
+val map_auto : Environ.env -> evar_map -> secvars:Id.Pred.t ->
(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 : GlobRef.t -> t -> t
-val remove_list : GlobRef.t list -> t -> t
+val remove_one : Environ.env -> GlobRef.t -> t -> t
+val remove_list : Environ.env -> 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 -> TransparentState.t
@@ -600,10 +629,10 @@ struct
merge_entry secvars db se.sentry_nopat se.sentry_pat
(* Precondition: concl has no existentials *)
- let map_auto sigma ~secvars (k,args) concl db =
+ let map_auto env sigma ~secvars (k,args) concl db =
let se = find k db in
let st = if db.use_dn then (Some db.hintdb_state) else None in
- let pat = lookup_tacs sigma concl st se in
+ let pat = lookup_tacs env sigma concl st se in
merge_entry secvars db [] pat
let map_existential sigma ~secvars (k,args) concl db =
@@ -613,11 +642,11 @@ struct
else ModeMismatch
(* [c] contains an existential *)
- let map_eauto sigma ~secvars (k,args) concl db =
+ let map_eauto env sigma ~secvars (k,args) concl db =
let se = find k db in
if matches_modes sigma args se.sentry_mode then
let st = if db.use_dn then Some db.hintdb_state else None in
- let pat = lookup_tacs sigma concl st se in
+ let pat = lookup_tacs env sigma concl st se in
ModeMatch (merge_entry secvars db [] pat)
else ModeMismatch
@@ -636,8 +665,6 @@ struct
is_unfold v.code.obj then None else Some gr
| None -> None
in
- let dnst = if db.use_dn then Some db.hintdb_state else None in
- let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in
match k with
| None ->
let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
@@ -646,8 +673,14 @@ struct
{ db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
else db
| Some gr ->
+ let pat =
+ if not db.use_dn && is_exact v.code.obj then None
+ else
+ let dnst = if db.use_dn then Some db.hintdb_state else None in
+ Option.map (fun p -> (dnst, p)) v.pat
+ in
let oval = find gr db in
- { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
+ { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map }
let rebuild_db st' db =
let db' =
@@ -687,14 +720,14 @@ struct
if sl1' == se.sentry_nopat && sl2' == se.sentry_pat then se
else rebuild_dn st { se with sentry_nopat = sl1'; sentry_pat = sl2' }
- let remove_list grs db =
+ let remove_list env grs db =
let filter (_, h) =
match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in
let hintmap = GlobRef.Map.map (remove_he db.hintdb_state filter) db.hintdb_map 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
+ let remove_one env gr db = remove_list env [gr] db
let get_entry se =
let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
@@ -769,12 +802,6 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with
(* adding and removing tactics in the search table *)
-let try_head_pattern c =
- try head_pattern_bound c
- with BoundPattern ->
- user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
- an if, case, or let expression, an application, or a projection.")
-
let with_uid c = { obj = c; uid = fresh_key () }
let secvars_of_idset s =
@@ -795,15 +822,15 @@ 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 ~abort_on_undefined_evars:false sigma cty) in
let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_exact_entry"
+ try head_bound sigma cty
+ with Bound -> failwith "make_exact_entry"
in
let pri = match info.hint_priority with None -> 0 | Some p -> p in
let pat = match info.hint_pattern with
| Some pat -> snd pat
- | None -> pat
+ | None ->
+ Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty)
in
(Some hd,
{ pri; pat = Some pat; name;
@@ -817,16 +844,17 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
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 ~abort_on_undefined_evars:false sigma c') in
let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_apply_entry" in
+ try head_bound ce.evd c'
+ with Bound -> failwith "make_apply_entry" in
let miss = 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
- | Some p -> snd p | None -> pat
+ | Some p -> snd p
+ | None ->
+ Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c')
in
if Int.equal nmiss 0 then
(Some hd,
@@ -929,14 +957,21 @@ let make_unfold eref =
code = with_uid (Unfold_nth eref) })
let make_extern pri pat tacast =
- let hdconstr = Option.map try_head_pattern pat in
+ let hdconstr = match pat with
+ | None -> None
+ | Some c ->
+ try Some (head_pattern_bound c)
+ with BoundPattern ->
+ user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
+ an if, case, or let expression, an application, or a projection.")
+ in
(hdconstr,
{ pri = pri;
pat = pat;
name = PathAny;
db = None;
secvars = Id.Pred.empty; (* Approximation *)
- code = with_uid (Extern tacast) })
+ code = with_uid (Extern (pat, tacast)) })
let make_mode ref m =
let open Term in
@@ -1009,8 +1044,9 @@ let add_transparency dbname target b =
in searchtable_add (dbname, Hint_db.set_transparent_state db st')
let remove_hint dbname grs =
+ let env = Global.env () in
let db = get_db dbname in
- let db' = Hint_db.remove_list grs db in
+ let db' = Hint_db.remove_list env grs db in
searchtable_add (dbname, db')
type hint_action =
@@ -1070,7 +1106,7 @@ let subst_autohint (subst, obj) =
match t with
| None -> gr'
| Some t ->
- (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
+ (try head_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
with Bound -> gr')
in
let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
@@ -1100,9 +1136,10 @@ let subst_autohint (subst, obj) =
| Unfold_nth ref ->
let ref' = subst_evaluable_reference subst ref in
if ref==ref' then data.code.obj else Unfold_nth ref'
- | Extern tac ->
+ | Extern (pat, tac) ->
+ let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
let tac' = Genintern.generic_substitute subst tac in
- if tac==tac' then data.code.obj else Extern tac'
+ if pat==pat' && tac==tac' then data.code.obj else Extern (pat', tac')
in
let name' = subst_path_atom subst data.name in
let uid' = subst_kn subst data.code.uid in
@@ -1382,7 +1419,7 @@ let pr_hint env sigma h = match h.obj with
(str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
| Unfold_nth c ->
str"unfold " ++ pr_evaluable_reference c
- | Extern tac ->
+ | Extern (_, tac) ->
str "(*external*) " ++ Pputils.pr_glb_generic env sigma tac
let pr_id_hint env sigma (id, v) =
@@ -1427,7 +1464,7 @@ let pr_hint_term env sigma cl =
(fun db -> match Hint_db.map_existential sigma ~secvars:Id.Pred.full hdc cl db with
| ModeMatch l -> l
| ModeMismatch -> [])
- else Hint_db.map_auto sigma ~secvars:Id.Pred.full hdc cl
+ else Hint_db.map_auto env sigma ~secvars:Id.Pred.full hdc cl
with Bound -> Hint_db.map_none ~secvars:Id.Pred.full
in
let fn db = List.map (fun x -> 0, x) (fn db) in
@@ -1593,3 +1630,45 @@ struct
let repr (h : t) = h.code.obj
end
+
+let connect_hint_clenv h gl =
+ let { hint_uctx = ctx; hint_clnv = clenv } = h in
+ (* [clenv] has been generated by a hint-making function, so the only relevant
+ data in its evarmap is the set of metas. The [evar_reset_evd] function
+ below just replaces the metas of sigma by those coming from the clenv. *)
+ let sigma = Tacmach.New.project gl in
+ let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
+ (* Still, we need to update the universes *)
+ if h.hint_poly then
+ (* Refresh the instance of the hint *)
+ 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. *)
+ {
+ templval = Evd.map_fl emap clenv.templval;
+ templtyp = Evd.map_fl emap clenv.templtyp;
+ evd = Evd.map_metas emap evd;
+ env = Proofview.Goal.env gl;
+ }
+ else
+ let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+ { clenv with evd = evd ; env = Proofview.Goal.env gl }
+
+let fresh_hint env sigma h =
+ let { hint_term = c; hint_uctx = ctx } = h in
+ if h.hint_poly then
+ (* Refresh the instance of the hint *)
+ 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
+ sigma, c
+ else
+ let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+ sigma, c
+
+let hint_res_pf ?with_evars ?with_classes ?flags h =
+ Proofview.Goal.enter begin fun gl ->
+ let clenv = connect_hint_clenv h gl in
+ Clenv.res_pf ?with_evars ?with_classes ?flags clenv
+ end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 8243716624..e061bd7648 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -37,9 +37,9 @@ type 'a hint_ast =
| Give_exact of 'a
| Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
| Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of Genarg.glob_generic_argument (* Hint Extern *)
+ | Extern of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *)
-type hint = {
+type hint = private {
hint_term : constr;
hint_type : types;
hint_uctx : Univ.ContextSet.t;
@@ -134,18 +134,18 @@ module Hint_db :
(** All hints associated to the reference, respecting modes if evars appear in the
arguments and using the discrimination net.
Returns a [ModeMismatch] if there are declared modes and none matches. *)
- val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
+ val map_eauto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
(** All hints associated to the reference.
Precondition: no evars should appear in the arguments, so no modes
are checked. *)
- val map_auto : evar_map -> secvars:Id.Pred.t ->
+ val map_auto : env -> evar_map -> secvars:Id.Pred.t ->
(GlobRef.t * constr array) -> constr -> t -> FullHint.t 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 : GlobRef.t -> t -> t
- val remove_list : GlobRef.t list -> t -> t
+ val remove_one : Environ.env -> GlobRef.t -> t -> t
+ val remove_list : Environ.env -> GlobRef.t list -> t -> t
val iter : (GlobRef.t option ->
hint_mode array list -> FullHint.t list -> unit) -> t -> unit
@@ -239,6 +239,11 @@ val wrap_hint_warning_fun : env -> evar_map ->
(evar_map -> 'a * evar_map) -> 'a * evar_map
(** Variant of the above for non-tactics *)
+val fresh_hint : env -> evar_map -> hint -> evar_map * constr
+
+val hint_res_pf : ?with_evars:bool -> ?with_classes:bool ->
+ ?flags:Unification.unify_flags -> hint -> unit Proofview.tactic
+
(** Printing hints *)
val pr_searchtable : env -> evar_map -> Pp.t
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f553a290f9..70cea89ccb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -117,7 +117,7 @@ let unsafe_intro env decl b =
Refine.refine ~typecheck:false begin fun sigma ->
let ctx = named_context_val env in
let nctx = push_named_context_val decl ctx in
- let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
+ let inst = identity_subst_val (named_context_val env) in
let ninst = mkRel 1 :: inst in
let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
let (sigma, ev) = new_pure_evar nctx sigma nb ~principal:true in
@@ -338,7 +338,7 @@ let rename_hyp repl =
let nhyps = List.map map hyps in
let nconcl = subst concl in
let nctx = val_of_named_context nhyps in
- let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
+ let instance = EConstr.identity_subst_val (Environ.named_context_val env) in
Refine.refine ~typecheck:false begin fun sigma ->
let sigma, ev = Evarutil.new_pure_evar nctx sigma nconcl ~principal:true in
sigma, mkEvar (ev, instance)
@@ -437,11 +437,6 @@ let clear_hyps2 env sigma ids sign t cl =
with Evarutil.ClearDependencyError (id,err,inglobal) ->
error_replacing_dependency env sigma id err inglobal
-let new_evar_from_context ?principal sign evd typ =
- let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
- let (evd, evk) = Evarutil.new_pure_evar sign evd typ in
- (evd, mkEvar (evk, instance))
-
let internal_cut ?(check=true) replace id t =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -449,22 +444,22 @@ let internal_cut ?(check=true) replace id t =
let concl = Proofview.Goal.concl gl in
let sign = named_context_val env in
let r = Retyping.relevance_of_type env sigma t in
- let sign',t,concl,sigma =
+ let env',t,concl,sigma =
if replace then
let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) 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 env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in
- sign',t,concl,sigma
+ Environ.reset_with_named_context sign' env,t,concl,sigma
else
(if check && mem_named_context_val id sign then
user_err (str "Variable " ++ Id.print id ++ str " is already declared.");
- push_named_context_val (LocalAssum (make_annot id r,t)) sign,t,concl,sigma) in
+ push_named (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in
let nf_t = nf_betaiota env sigma t in
Proofview.tclTHEN
(Proofview.Unsafe.tclEVARS sigma)
(Refine.refine ~typecheck:false begin fun sigma ->
- let (sigma, ev) = new_evar_from_context sign sigma nf_t in
- let (sigma, ev') = new_evar_from_context sign' sigma ~principal:true concl in
+ let (sigma, ev) = Evarutil.new_evar env sigma nf_t in
+ let (sigma, ev') = Evarutil.new_evar ~principal:true env' sigma concl in
let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
(sigma, term)
end)
@@ -1049,12 +1044,15 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
end
end
-let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
+let drop_intro_name (_ : Id.t) = Proofview.tclUNIT ()
+
+let intro_gen n m f d = intro_then_gen n m f d drop_intro_name
let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true false
-let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false
+let intro_using_then id = intro_then_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false
+let intro_using id = intro_using_then id drop_intro_name
let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false
-let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false
+let intro = intro_then drop_intro_name
let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false
let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
@@ -1070,6 +1068,11 @@ let rec intros_using = function
| [] -> Proofview.tclUNIT()
| str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l)
+let rec intros_using_then_helper tac acc = function
+ | [] -> tac (List.rev acc)
+ | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l)
+let intros_using_then l tac = intros_using_then_helper tac [] l
+
let intros = Tacticals.New.tclREPEAT intro
let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
@@ -2788,7 +2791,7 @@ let pose_tac na c =
let id = make_annot id Sorts.Relevant in
let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
- let inst = List.map (fun d -> mkVar (get_id d)) (named_context env) in
+ let inst = EConstr.identity_subst_val hyps in
let body = mkEvar (ev, mkRel 1 :: inst) in
(sigma, mkLetIn (map_annot Name.mk_name id, c, t, body))
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5b397b15d0..00739306a7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -65,9 +65,11 @@ val intro_avoiding : Id.Set.t -> unit Proofview.tactic
val intro_replacing : Id.t -> unit Proofview.tactic
val intro_using : Id.t -> unit Proofview.tactic
+val intro_using_then : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val intro_mustbe_force : Id.t -> unit Proofview.tactic
val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val intros_using : Id.t list -> unit Proofview.tactic
+val intros_using_then : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic
val intros_replacing : Id.t list -> unit Proofview.tactic
val intros_possibly_replacing : Id.t list -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:50:27 +0000