aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml58
-rw-r--r--tactics/class_tactics.mli19
-rw-r--r--tactics/hints.ml31
-rw-r--r--tactics/hints.mli3
-rw-r--r--tactics/tactics.ml22
5 files changed, 82 insertions, 51 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c1ac7d201a..160e4f164e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -548,7 +548,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
make_apply_entry ~name env sigma flags pri false])
else []
-let make_hints g st only_classes sign =
+let make_hints g (modes,st) only_classes sign =
let hintlist =
List.fold_left
(fun hints hyp ->
@@ -565,7 +565,9 @@ let make_hints g st only_classes sign =
in hint @ hints
else hints)
([]) sign
- in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
+ in
+ let db = Hint_db.add_modes modes @@ Hint_db.empty st true in
+ Hint_db.add_list (pf_env g) (project g) hintlist db
module Search = struct
type autoinfo =
@@ -578,29 +580,29 @@ module Search = struct
(** Local hints *)
let autogoal_cache = Summary.ref ~name:"autogoal_cache"
- (DirPath.empty, true, Context.Named.empty,
+ (DirPath.empty, true, Context.Named.empty, GlobRef.Map.empty,
Hint_db.empty TransparentState.full true)
- let make_autogoal_hints only_classes ?(st=TransparentState.full) g =
+ let make_autogoal_hints only_classes (modes,st as mst) g =
let open Proofview in
let open Tacmach.New in
let sign = Goal.hyps g in
- let (dir, onlyc, sign', cached_hints) = !autogoal_cache in
+ let (dir, onlyc, sign', cached_modes, cached_hints) = !autogoal_cache in
let cwd = Lib.cwd () in
let eq c1 c2 = EConstr.eq_constr (project g) c1 c2 in
if DirPath.equal cwd dir &&
(onlyc == only_classes) &&
Context.Named.equal eq sign sign' &&
- Hint_db.transparent_state cached_hints == st
+ cached_modes == modes
then cached_hints
else
let hints = make_hints {it = Goal.goal g; sigma = project g}
- st only_classes sign
+ mst only_classes sign
in
- autogoal_cache := (cwd, only_classes, sign, hints); hints
+ autogoal_cache := (cwd, only_classes, sign, modes, hints); hints
- let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g =
- let hints = make_autogoal_hints only_classes ~st g in
+ let make_autogoal mst only_classes dep cut i g =
+ let hints = make_autogoal_hints only_classes mst g in
{ search_hints = hints;
search_depth = [i]; last_tac = lazy (str"none");
search_dep = dep;
@@ -695,7 +697,8 @@ module Search = struct
if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
then
let st = Hint_db.transparent_state info.search_hints in
- make_autogoal_hints info.search_only_classes ~st gl'
+ let modes = Hint_db.modes info.search_hints in
+ make_autogoal_hints info.search_only_classes (modes,st) gl'
else info.search_hints
in
let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in
@@ -830,19 +833,19 @@ module Search = struct
(fun e' -> let (e, info) = merge_exceptions e e' in
Proofview.tclZERO ~info e))
- let search_tac_gl ?st only_classes dep hints depth i sigma gls gl :
+ let search_tac_gl mst only_classes dep hints depth i sigma gls gl :
unit Proofview.tactic =
let open Proofview in
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
+ let info = make_autogoal mst only_classes dep (cut_of_hints hints) i gl in
search_tac hints depth 1 info
- let search_tac ?(st=TransparentState.full) only_classes dep hints depth =
+ let search_tac mst only_classes dep hints depth =
let open Proofview in
let tac sigma gls i =
Goal.enter
begin fun gl ->
- search_tac_gl ~st only_classes dep hints depth (succ i) sigma gls gl end
+ search_tac_gl mst only_classes dep hints depth (succ i) sigma gls gl end
in
Proofview.Unsafe.tclGETGOALS >>= fun gls ->
let gls = CList.map Proofview.drop_state gls in
@@ -867,11 +870,11 @@ module Search = struct
| (e,ie) -> Proofview.tclZERO ~info:ie e)
in aux 1
- let eauto_tac ?(st=TransparentState.full) ?(unique=false)
+ let eauto_tac mst ?(unique=false)
~only_classes ?strategy ~depth ~dep hints =
let open Proofview in
let tac =
- let search = search_tac ~st only_classes dep hints in
+ let search = search_tac mst only_classes dep hints in
let dfs =
match strategy with
| None -> not (get_typeclasses_iterative_deepening ())
@@ -915,8 +918,8 @@ module Search = struct
| Some i -> str ", with depth limit " ++ int i));
tac
- let eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints =
- Hints.wrap_hint_warning @@ eauto_tac ?st ?unique ~only_classes ?strategy ~depth ~dep hints
+ let eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints =
+ Hints.wrap_hint_warning @@ eauto_tac mst ?unique ~only_classes ?strategy ~depth ~dep hints
let run_on_evars env evm p tac =
match evars_to_goals p evm with
@@ -968,8 +971,8 @@ module Search = struct
else raise Not_found
with Logic_monad.TacticFailure _ -> raise Not_found
- let evars_eauto env evd depth only_classes unique dep st hints p =
- let eauto_tac = eauto_tac ~st ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
+ let evars_eauto env evd depth only_classes unique dep mst hints p =
+ let eauto_tac = eauto_tac mst ~unique ~only_classes ~depth ~dep:(unique || dep) hints in
let res = run_on_evars env evd p eauto_tac in
match res with
| None -> evd
@@ -983,11 +986,11 @@ module Search = struct
let typeclasses_resolve env evd debug depth unique p =
let db = searchtable_map typeclasses_db in
- typeclasses_eauto env evd ?depth unique (Hint_db.transparent_state db) [db] p
+ let st = Hint_db.transparent_state db in
+ let modes = Hint_db.modes db in
+ typeclasses_eauto env evd ?depth unique (modes,st) [db] p
end
-(** Binding to either V85 or Search implementations. *)
-
let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
?strategy ~depth dbs =
let dbs = List.map_filter
@@ -996,8 +999,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
dbs
in
let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+ let modes = List.map Hint_db.modes dbs in
+ let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in
let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
- Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs
+ Search.eauto_tac (modes,st) ~only_classes ?strategy ~depth ~dep:true dbs
(** We compute dependencies via a union-find algorithm.
Beware of the imperative effects on the partition structure,
@@ -1140,11 +1145,12 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
let gls = { it = gl ; sigma = sigma; } in
let hints = searchtable_map typeclasses_db in
let st = Hint_db.transparent_state hints in
+ let modes = Hint_db.modes hints in
let depth = get_typeclasses_depth () in
let gls' =
try
Proofview.V82.of_tactic
- (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
+ (Search.eauto_tac (modes,st) ~only_classes:true ~depth [hints] ~dep:true) gls
with Refiner.FailError _ -> raise Not_found
in
let evd = sig_sig gls' in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index c950e3de3d..b9291f6124 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -27,9 +27,18 @@ type search_strategy = Dfs | Bfs
val set_typeclasses_strategy : search_strategy -> unit
-val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy ->
- depth:(Int.t option) ->
- Hints.hint_db_name list -> unit Proofview.tactic
+val typeclasses_eauto :
+ ?only_classes:bool
+ (** Should non-class goals be shelved and resolved at the end *)
+ -> ?st:TransparentState.t
+ (** The transparent_state used when working with local hypotheses *)
+ -> ?strategy:search_strategy
+ (** Is a traversing-strategy specified? *)
+ -> depth:(Int.t option)
+ (** Bounded or unbounded search *)
+ -> Hints.hint_db_name list
+ (** The list of hint databases to use *)
+ -> unit Proofview.tactic
val head_of_constr : Id.t -> constr -> unit Proofview.tactic
@@ -41,8 +50,8 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
module Search : sig
val eauto_tac :
- ?st:TransparentState.t
- (** The transparent_state used when working with local hypotheses *)
+ Hints.hint_mode array list GlobRef.Map.t * TransparentState.t
+ (** The transparent_state and modes used when working with local hypotheses *)
-> ?unique:bool
(** Should we force a unique solution *)
-> only_classes:bool
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 11a8816159..cc56c1c425 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -289,8 +289,6 @@ let lookup_tacs sigma concl st se =
let sl' = List.stable_sort pri_order_int l' in
List.merge pri_order_int se.sentry_nopat sl'
-module Constr_map = Map.Make(GlobRef.Ordered)
-
let is_transparent_gr ts = function
| VarRef id -> TransparentState.is_transparent_variable ts id
| ConstRef cst -> TransparentState.is_transparent_constant ts cst
@@ -520,6 +518,8 @@ val add_cut : hints_path -> 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 add_modes : hint_mode array list GlobRef.Map.t -> t -> t
+val modes : t -> hint_mode array list GlobRef.Map.t
val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) ->
t -> 'a -> 'a
@@ -532,7 +532,7 @@ struct
hintdb_unfolds : Id.Set.t * Cset.t;
hintdb_max_id : int;
use_dn : bool;
- hintdb_map : search_entry Constr_map.t;
+ hintdb_map : search_entry GlobRef.Map.t;
(* A list of unindexed entries starting with an unfoldable constant
or with no associated pattern. *)
hintdb_nopat : (GlobRef.t option * stored_data) list;
@@ -548,12 +548,12 @@ struct
hintdb_unfolds = (Id.Set.empty, Cset.empty);
hintdb_max_id = 0;
use_dn = use_dn;
- hintdb_map = Constr_map.empty;
+ hintdb_map = GlobRef.Map.empty;
hintdb_nopat = [];
hintdb_name = name; }
let find key db =
- try Constr_map.find key db.hintdb_map
+ try GlobRef.Map.find key db.hintdb_map
with Not_found -> empty_se
let realize_tac secvars (id,tac) =
@@ -650,11 +650,11 @@ struct
else db
| Some gr ->
let oval = find gr db in
- { db with hintdb_map = Constr_map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
+ { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv dnst oval) db.hintdb_map }
let rebuild_db st' db =
let db' =
- { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map;
+ { db with hintdb_map = GlobRef.Map.map (rebuild_dn st') db.hintdb_map;
hintdb_state = st'; hintdb_nopat = [] }
in
List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
@@ -693,7 +693,7 @@ struct
let remove_list grs db =
let filter (_, h) =
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 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 }
@@ -706,11 +706,11 @@ struct
let iter f db =
let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat);
- Constr_map.iter iter_se db.hintdb_map
+ GlobRef.Map.iter iter_se db.hintdb_map
let fold f db accu =
let accu = f None [] (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in
- Constr_map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
+ GlobRef.Map.fold (fun k se -> f (Some k) se.sentry_mode (get_entry se)) db.hintdb_map accu
let transparent_state db = db.hintdb_state
@@ -724,12 +724,21 @@ struct
let add_mode gr m db =
let se = find gr db in
let se = { se with sentry_mode = m :: se.sentry_mode } in
- { db with hintdb_map = Constr_map.add gr se db.hintdb_map }
+ { db with hintdb_map = GlobRef.Map.add gr se db.hintdb_map }
let cut db = db.hintdb_cut
let unfolds db = db.hintdb_unfolds
+ let add_modes modes db =
+ let f gr e me =
+ Some { e with sentry_mode = me.sentry_mode @ e.sentry_mode }
+ in
+ let mode_entries = GlobRef.Map.map (fun m -> { empty_se with sentry_mode = m }) modes in
+ { db with hintdb_map = GlobRef.Map.union f db.hintdb_map mode_entries }
+
+ let modes db = GlobRef.Map.map (fun se -> se.sentry_mode) db.hintdb_map
+
let use_dn db = db.use_dn
end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 90a8b7fe52..7b8f96cdd8 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -162,6 +162,9 @@ module Hint_db :
val cut : t -> hints_path
val unfolds : t -> Id.Set.t * Cset.t
+
+ val add_modes : hint_mode array list GlobRef.Map.t -> t -> t
+ val modes : t -> hint_mode array list GlobRef.Map.t
end
type hint_db = Hint_db.t
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 16bede0d1b..5e8869f9b0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -833,7 +833,7 @@ let change_in_hyp ?(check=true) occl t id =
(* FIXME: we set the [check] flag only to reorder hypotheses in case of
introduction of dependencies in new variables. We should separate this
check from the conversion function. *)
- e_change_in_hyp ~check:true (fun x -> change_on_subterm check Reduction.CONV x t occl) id
+ e_change_in_hyp ~check (fun x -> change_on_subterm check Reduction.CONV x t occl) id
let concrete_clause_of enum_hyps cl = match cl.onhyps with
| None ->
@@ -855,7 +855,7 @@ let change ?(check=true) chg c cls =
let redfun deep env sigma t = change_on_subterm check Reduction.CONV deep c occl env sigma t in
(redfun, id, where)
in
- e_change_in_hyps ~check:true f hyps
+ e_change_in_hyps ~check f hyps
end
let change_concl t =
@@ -2863,17 +2863,21 @@ let generalize_dep ?(with_let=false) c =
| _ -> tothin
in
let cl' = it_mkNamedProd_or_LetIn (pf_concl gl) to_quantify in
- let body =
- if with_let then
- match EConstr.kind sigma c with
- | Var id -> id |> (fun id -> pf_get_hyp id gl) |> NamedDecl.get_value
- | _ -> None
- else None
+ let is_var, body = match EConstr.kind sigma c with
+ | Var id ->
+ let body = NamedDecl.get_value (pf_get_hyp id gl) in
+ let is_var = Option.is_empty body && not (List.mem id init_ids) in
+ if with_let then is_var, body else is_var, None
+ | _ -> false, None
in
let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
(cl',project gl) in
(* Check that the generalization is indeed well-typed *)
- let (evd, _) = Typing.type_of env evd cl'' in
+ let evd =
+ (* No need to retype for variables, term is statically well-typed *)
+ if is_var then evd
+ else fst (Typing.type_of env evd cl'')
+ in
let args = Context.Named.to_instance mkVar to_quantify_rev in
tclTHENLIST
[ Proofview.Unsafe.tclEVARS evd;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 06:57:11 +0000