aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/cList.ml8
-rw-r--r--lib/cList.mli4
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--plugins/firstorder/sequent.mli2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--tactics/auto.ml1208
-rw-r--r--tactics/auto.mli206
-rw-r--r--tactics/class_tactics.ml7
-rw-r--r--tactics/class_tactics.mli4
-rw-r--r--tactics/eauto.ml413
-rw-r--r--tactics/eauto.mli3
-rw-r--r--tactics/extratactics.ml46
-rw-r--r--tactics/g_class.ml42
-rw-r--r--tactics/rewrite.ml6
-rw-r--r--tactics/tacintern.ml2
-rw-r--r--tactics/tactics.ml30
-rw-r--r--tactics/tactics.mli5
-rw-r--r--tactics/tactics.mllib1
-rw-r--r--toplevel/classes.ml16
-rw-r--r--toplevel/obligations.ml8
-rw-r--r--toplevel/vernacentries.ml14
22 files changed, 79 insertions, 1472 deletions
diff --git a/lib/cList.ml b/lib/cList.ml
index 93ba0637e..3115826c6 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -61,6 +61,7 @@ sig
val except : 'a eq -> 'a -> 'a list -> 'a list
val remove : 'a eq -> 'a -> 'a list -> 'a list
val remove_first : ('a -> bool) -> 'a list -> 'a list
+ val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val sep_last : 'a list -> 'a * 'a list
val find_map : ('a -> 'b option) -> 'a list -> 'b
@@ -442,6 +443,13 @@ let rec remove_first p = function
| b::l -> b::remove_first p l
| [] -> raise Not_found
+let insert p v l =
+ let rec insrec = function
+ | [] -> [v]
+ | h::tl -> if p v h then v::h::tl else h::insrec tl
+ in
+ insrec l
+
let add_set cmp x l = if mem_f cmp x l then l else x :: l
(** List equality up to permutation (but considering multiple occurrences) *)
diff --git a/lib/cList.mli b/lib/cList.mli
index 01ae83960..aa888679c 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -119,6 +119,10 @@ sig
val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)
+ val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
+ (** Insert at the (first) position so that if the list is ordered wrt to the
+ total order given as argument, the order is preserved *)
+
val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val sep_last : 'a list -> 'a * 'a list
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 6d4d8792f..f0afa2ec5 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -204,7 +204,7 @@ let extend_with_ref_list l seq gl =
(add_formula Hyp gr typ seq gl,gl) in
List.fold_right f l (seq,gl)
-open Auto
+open Hints
let extend_with_auto_hints l seq gl=
let seqref=ref seq in
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 40aa169ab..6462fe9d3 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -56,7 +56,7 @@ val empty_seq : int -> t
val extend_with_ref_list : global_reference list ->
t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
-val extend_with_auto_hints : Auto.hint_db_name list ->
+val extend_with_auto_hints : Hints.hint_db_name list ->
t -> Proof_type.goal sigma -> t * Proof_type.goal sigma
val print_cmap: global_reference list CM.t -> Pp.std_ppcmds
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 700f67a74..cd3f1a5d4 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1454,7 +1454,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
Eauto.eauto_with_bases
(true,5)
[Evd.empty,Lazy.force refl_equal]
- [Auto.Hint_db.empty empty_transparent_state false]
+ [Hints.Hint_db.empty empty_transparent_state false]
)
)
)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9f52258ed..8014abf65 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1312,7 +1312,7 @@ let open_new_goal build_proof ctx using_lemmas ref_ goal_name (gls_type,decompos
Eauto.eauto_with_bases
(true,5)
[Evd.empty,Lazy.force refl_equal]
- [Auto.Hint_db.empty empty_transparent_state false]
+ [Hints.Hint_db.empty empty_transparent_state false]
]
)
)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e06c2b7e0..056b781e1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,1153 +6,24 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(*
+*)
open Pp
-open Errors
open Util
+open Errors
open Names
-open Namegen
-open Term
open Vars
open Termops
-open Inductiveops
open Environ
-open Evd
-open Typing
-open Pattern
-open Patternops
open Tacmach
-open Pfedit
open Genredexpr
-open Tacred
open Tactics
open Tacticals
open Clenv
-open Libnames
-open Globnames
-open Smartlocate
-open Libobject
-open Printer
open Tacexpr
-open Mod_subst
open Locus
open Proofview.Notations
-open Decl_kinds
-
-(****************************************************************************)
-(* The Type of Constructions Autotactic Hints *)
-(****************************************************************************)
-
-type 'a auto_tactic =
- | Res_pf of 'a (* Hint Apply *)
- | ERes_pf of 'a (* Hint EApply *)
- | Give_exact of 'a
- | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
- | Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of glob_tactic_expr (* Hint Extern *)
-
-type hints_path_atom =
- | PathHints of global_reference list
- | PathAny
-
-type hints_path =
- | PathAtom of hints_path_atom
- | PathStar of hints_path
- | PathSeq of hints_path * hints_path
- | PathOr of hints_path * hints_path
- | PathEmpty
- | PathEpsilon
-
-type hint_term =
- | IsGlobRef of global_reference
- | IsConstr of constr * Univ.universe_context_set
-
-type 'a gen_auto_tactic = {
- pri : int; (* A number lower is higher priority *)
- poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *)
- pat : constr_pattern option; (* A pattern for the concl of the Goal *)
- name : hints_path_atom; (* A potential name to refer to the hint *)
- code : 'a auto_tactic (* the tactic to apply when the concl matches pat *)
-}
-
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
-
-type hint_entry = global_reference option *
- (constr * types * Univ.universe_context_set) gen_auto_tactic
-
-let eq_hints_path_atom p1 p2 = match p1, p2 with
-| PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
-| PathAny, PathAny -> true
-| (PathHints _ | PathAny), _ -> false
-
-let eq_auto_tactic t1 t2 = match t1, t2 with
-| Res_pf (c1, _), Res_pf (c2, _) -> Constr.equal c1 c2
-| ERes_pf (c1, _), ERes_pf (c2, _) -> Constr.equal c1 c2
-| Give_exact (c1, _), Give_exact (c2, _) -> Constr.equal c1 c2
-| Res_pf_THEN_trivial_fail (c1, _), Res_pf_THEN_trivial_fail (c2, _) -> Constr.equal c1 c2
-| Unfold_nth gr1, Unfold_nth gr2 -> eq_egr gr1 gr2
-| Extern tac1, Extern tac2 -> tac1 == tac2 (** May cause redundancy in addkv *)
-| (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
- | Unfold_nth _ | Extern _), _ -> false
-
-let eq_gen_auto_tactic t1 t2 =
- Int.equal t1.pri t2.pri &&
- Option.equal constr_pattern_eq t1.pat t2.pat &&
- eq_hints_path_atom t1.name t2.name &&
- eq_auto_tactic t1.code t2.code
-
-let pri_order_int (id1, {pri=pri1}) (id2, {pri=pri2}) =
- let d = pri1 - pri2 in
- if Int.equal d 0 then id2 - id1
- else d
-
-let pri_order t1 t2 = pri_order_int t1 t2 <= 0
-
-let insert v l =
- let rec insrec = function
- | [] -> [v]
- | h::tl -> if pri_order v h then v::h::tl else h::(insrec tl)
- in
- insrec l
-
-(* Nov 98 -- Papageno *)
-(* Les Hints sont ré-organisés en plusieurs databases.
-
- La table impérative "searchtable", de type "hint_db_table",
- associe une database (hint_db) à chaque nom.
-
- Une hint_db est une table d'association fonctionelle constr -> search_entry
- Le constr correspond à la constante de tête de la conclusion.
-
- Une search_entry est un triplet comprenant :
- - la liste des tactiques qui n'ont pas de pattern associé
- - la liste des tactiques qui ont un pattern
- - un discrimination net borné (Btermdn.t) constitué de tous les
- patterns de la seconde liste de tactiques *)
-
-type stored_data = int * pri_auto_tactic
- (* 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)
-
-type search_entry = stored_data list * stored_data list * Bounded_net.t * bool array list
-
-
-let empty_se = ([],[],Bounded_net.create (),[])
-
-let eq_pri_auto_tactic (_, x) (_, y) =
- if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
- match x.code,y.code with
- | Res_pf (cstr,_),Res_pf (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | ERes_pf (cstr,_),ERes_pf (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | Give_exact (cstr,_),Give_exact (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | Res_pf_THEN_trivial_fail (cstr,_)
- ,Res_pf_THEN_trivial_fail (cstr1,_) ->
- Term.eq_constr cstr cstr1
- | _,_ -> false
- else
- false
-
-let add_tac pat t st (l,l',dn,m) =
- match pat with
- | None ->
- if not (List.exists (eq_pri_auto_tactic t) l) then (insert t l, l', dn, m)
- else (l, l', dn, m)
- | Some pat ->
- if not (List.exists (eq_pri_auto_tactic t) l')
- then (l, insert t l', Bounded_net.add st dn (pat,t), m) else (l, l', dn, m)
-
-let rebuild_dn st ((l,l',dn,m) : search_entry) =
- let dn' =
- List.fold_left
- (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
- (Bounded_net.create ()) l'
- in
- (l, l', dn', m)
-
-let lookup_tacs concl st (l,l',dn) =
- let l' = Bounded_net.lookup st dn concl in
- let sl' = List.stable_sort pri_order_int l' in
- List.merge pri_order_int l sl'
-
-module Constr_map = Map.Make(RefOrdered)
-
-let is_transparent_gr (ids, csts) = function
- | VarRef id -> Id.Pred.mem id ids
- | ConstRef cst -> Cpred.mem cst csts
- | IndRef _ | ConstructRef _ -> false
-
-let strip_params env c =
- match kind_of_term c with
- | App (f, args) ->
- (match kind_of_term 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)
- | _ -> c)
- | _ -> c
-
-let instantiate_hint p =
- let mk_clenv c cty ctx =
- let env = Global.env () in
- let sigma = Evd.merge_context_set univ_flexible (Evd.from_env env) ctx in
- let cl = mk_clenv_from_env (Global.env()) sigma None (c,cty) in
- {cl with templval =
- { cl.templval with rebus = strip_params env cl.templval.rebus };
- env = empty_env}
- in
- let code = match p.code with
- | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx)
- | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx)
- | Res_pf_THEN_trivial_fail (c, cty, ctx) ->
- Res_pf_THEN_trivial_fail (c, mk_clenv c cty ctx)
- | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx)
- | Unfold_nth e -> Unfold_nth e
- | Extern t -> Extern t
- in { pri = p.pri; poly = p.poly; name = p.name; pat = p.pat; code = code }
-
-let hints_path_atom_eq h1 h2 = match h1, h2 with
-| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
-| PathAny, PathAny -> true
-| _ -> false
-
-let rec hints_path_eq h1 h2 = match h1, h2 with
-| PathAtom h1, PathAtom h2 -> hints_path_atom_eq h1 h2
-| PathStar h1, PathStar h2 -> hints_path_eq h1 h2
-| PathSeq (l1, r1), PathSeq (l2, r2) ->
- hints_path_eq l1 l2 && hints_path_eq r1 r2
-| PathOr (l1, r1), PathOr (l2, r2) ->
- hints_path_eq l1 l2 && hints_path_eq r1 r2
-| PathEmpty, PathEmpty -> true
-| PathEpsilon, PathEpsilon -> true
-| _ -> false
-
-let path_matches hp hints =
- let rec aux hp hints k =
- match hp, hints with
- | PathAtom _, [] -> false
- | PathAtom PathAny, (_ :: hints') -> k hints'
- | PathAtom p, (h :: hints') ->
- if hints_path_atom_eq p h then k hints' else false
- | PathStar hp', hints ->
- k hints || aux hp' hints (fun hints' -> aux hp hints' k)
- | PathSeq (hp, hp'), hints ->
- aux hp hints (fun hints' -> aux hp' hints' k)
- | PathOr (hp, hp'), hints ->
- aux hp hints k || aux hp' hints k
- | PathEmpty, _ -> false
- | PathEpsilon, hints -> k hints
- in aux hp hints (fun hints' -> true)
-
-let rec matches_epsilon = function
- | PathAtom _ -> false
- | PathStar _ -> true
- | PathSeq (p, p') -> matches_epsilon p && matches_epsilon p'
- | PathOr (p, p') -> matches_epsilon p || matches_epsilon p'
- | PathEmpty -> false
- | PathEpsilon -> true
-
-let rec is_empty = function
- | PathAtom _ -> false
- | PathStar _ -> false
- | PathSeq (p, p') -> is_empty p || is_empty p'
- | PathOr (p, p') -> matches_epsilon p && matches_epsilon p'
- | PathEmpty -> true
- | PathEpsilon -> false
-
-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'
- | [], [] -> PathEpsilon
- | [], hints -> PathEmpty
- | grs, [] -> PathAtom (PathHints grs)
- | _, _ -> PathEmpty
- in
- match hp with
- | PathAtom PathAny -> PathEpsilon
- | PathAtom (PathHints grs) ->
- (match grs, hint with
- | h :: hints, PathAny -> PathEmpty
- | hints, PathHints hints' -> derivate_atoms hints hints'
- | _, _ -> assert false)
- | PathStar p -> if path_matches p [hint] then hp else PathEpsilon
- | PathSeq (hp, hp') ->
- let hpder = path_derivate hp hint in
- if matches_epsilon hp then
- PathOr (PathSeq (hpder, hp'), path_derivate hp' hint)
- else if is_empty hpder then PathEmpty
- else PathSeq (hpder, hp')
- | PathOr (hp, hp') ->
- PathOr (path_derivate hp hint, path_derivate hp' hint)
- | PathEmpty -> PathEmpty
- | PathEpsilon -> PathEmpty
-
-let rec normalize_path h =
- match h with
- | PathStar PathEpsilon -> PathEpsilon
- | PathSeq (PathEmpty, _) | PathSeq (_, PathEmpty) -> PathEmpty
- | PathSeq (PathEpsilon, p) | PathSeq (p, PathEpsilon) -> normalize_path p
- | PathOr (PathEmpty, p) | PathOr (p, PathEmpty) -> normalize_path p
- | PathOr (p, q) ->
- let p', q' = normalize_path p, normalize_path q in
- if hints_path_eq p p' && hints_path_eq q q' then h
- else normalize_path (PathOr (p', q'))
- | PathSeq (p, q) ->
- let p', q' = normalize_path p, normalize_path q in
- if hints_path_eq p p' && hints_path_eq q q' then h
- else normalize_path (PathSeq (p', q'))
- | _ -> h
-
-let path_derivate hp hint = normalize_path (path_derivate hp hint)
-
-let rec pp_hints_path = function
- | PathAtom (PathAny) -> str"."
- | PathAtom (PathHints grs) -> pr_sequence pr_global grs
- | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
- | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
- | PathOr (p, p') ->
- str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
- | PathEmpty -> str"Ø"
- | PathEpsilon -> str"ε"
-
-let subst_path_atom subst p =
- match p with
- | PathAny -> p
- | PathHints grs ->
- let gr' gr = fst (subst_global subst gr) in
- let grs' = List.smartmap gr' grs in
- if grs' == grs then p else PathHints grs'
-
-let rec subst_hints_path subst hp =
- match hp with
- | PathAtom p ->
- let p' = subst_path_atom subst p in
- if p' == p then hp else PathAtom p'
- | PathStar p -> let p' = subst_hints_path subst p in
- if p' == p then hp else PathStar p'
- | PathSeq (p, q) ->
- let p' = subst_hints_path subst p in
- let q' = subst_hints_path subst q in
- if p' == p && q' == q then hp else PathSeq (p', q')
- | PathOr (p, q) ->
- let p' = subst_hints_path subst p in
- let q' = subst_hints_path subst q in
- if p' == p && q' == q then hp else PathOr (p', q')
- | _ -> hp
-
-module Hint_db = struct
-
- type t = {
- hintdb_state : Names.transparent_state;
- hintdb_cut : hints_path;
- hintdb_unfolds : Id.Set.t * Cset.t;
- mutable hintdb_max_id : int;
- use_dn : bool;
- 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
- }
-
- let next_hint_id t =
- let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h
-
- let empty st use_dn = { hintdb_state = st;
- hintdb_cut = PathEmpty;
- hintdb_unfolds = (Id.Set.empty, Cset.empty);
- hintdb_max_id = 0;
- use_dn = use_dn;
- hintdb_map = Constr_map.empty;
- hintdb_nopat = [] }
-
- let find key db =
- try Constr_map.find key db.hintdb_map
- with Not_found -> empty_se
-
- let realize_tac (id,tac) = tac
-
- let matches_mode args mode =
- Array.length args == Array.length mode &&
- Array.for_all2 (fun arg m -> not (m && occur_existential arg)) args mode
-
- let matches_modes args modes =
- if List.is_empty modes then true
- else List.exists (matches_mode args) modes
-
- let map_none db =
- List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) [])
-
- let map_all k db =
- let (l,l',_,_) = find k db in
- List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
-
- (** Precondition: concl has no existentials *)
- let map_auto (k,args) concl db =
- let (l,l',dn,m) = find k db in
- let st = if db.use_dn then (Some db.hintdb_state) else None in
- let l' = lookup_tacs concl st (l,l',dn) in
- List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
-
- let map_existential (k,args) concl db =
- let (l,l',_,m) = find k db in
- if matches_modes args m then
- List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
- else List.map realize_tac (List.map snd db.hintdb_nopat)
-
- (* [c] contains an existential *)
- let map_eauto (k,args) concl db =
- let (l,l',dn,m) = find k db in
- if matches_modes args m then
- let st = if db.use_dn then Some db.hintdb_state else None in
- let l' = lookup_tacs concl st (l,l',dn) in
- List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat) l')
- else List.map realize_tac (List.map snd db.hintdb_nopat)
-
- let is_exact = function
- | Give_exact _ -> true
- | _ -> false
-
- let is_unfold = function
- | Unfold_nth _ -> true
- | _ -> false
-
- let addkv gr id v db =
- let idv = id, v in
- let k = match gr with
- | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
- is_unfold v.code 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 then None else v.pat in
- match k with
- | None ->
- (** ppedrot: this equality here is dubious. Maybe we can remove it? *)
- let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in
- if not (List.exists is_present db.hintdb_nopat) then
- (** FIXME *)
- { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
- 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 }
-
- let rebuild_db st' db =
- let db' =
- { db with hintdb_map = Constr_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
-
- let add_one (k, v) db =
- let v = instantiate_hint v in
- let st',db,rebuild =
- match v.code with
- | Unfold_nth egr ->
- let addunf (ids,csts) (ids',csts') =
- match egr with
- | EvalVarRef id -> (Id.Pred.add id ids, csts), (Id.Set.add id ids', csts')
- | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
- in
- let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
- state, { db with hintdb_unfolds = unfs }, true
- | _ -> db.hintdb_state, db, false
- in
- let db = if db.use_dn && rebuild then rebuild_db st' db else db
- in addkv k (next_hint_id db) v db
-
- let add_list l db = List.fold_left (fun db k -> add_one k db) db l
-
- let remove_sdl p sdl = List.smartfilter p sdl
- let remove_he st p (sl1, sl2, dn, m as he) =
- let sl1' = remove_sdl p sl1 and sl2' = remove_sdl p sl2 in
- if sl1' == sl1 && sl2' == sl2 then he
- else rebuild_dn st (sl1', sl2', dn, m)
-
- let remove_list grs db =
- let filter (_, h) =
- match h.name with PathHints [gr] -> not (List.mem_f eq_gr 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
- { db with hintdb_map = hintmap; hintdb_nopat = hintnopat }
-
- let remove_one gr db = remove_list [gr] db
-
- let iter f db =
- f None [] (List.map (fun x -> realize_tac (snd x)) db.hintdb_nopat);
- Constr_map.iter (fun k (l,l',_,m) -> f (Some k) m (List.map realize_tac (l@l'))) 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 (l,l',_,m) -> f (Some k) m (List.map snd (l@l'))) db.hintdb_map accu
-
- let transparent_state db = db.hintdb_state
-
- let set_transparent_state db st =
- if db.use_dn then rebuild_db st db
- else { db with hintdb_state = st }
-
- let add_cut path db =
- { db with hintdb_cut = normalize_path (PathOr (db.hintdb_cut, path)) }
-
- let add_mode gr m db =
- let (l,l',dn,ms) = find gr db in
- { db with hintdb_map = Constr_map.add gr (l,l',dn,m :: ms) db.hintdb_map }
-
- let cut db = db.hintdb_cut
-
- let unfolds db = db.hintdb_unfolds
-
- let use_dn db = db.use_dn
-
-end
-
-module Hintdbmap = String.Map
-
-type hint_db = Hint_db.t
-
-type hint_db_table = hint_db Hintdbmap.t ref
-
-type hint_db_name = string
-
-(** Initially created hint databases, for typeclasses and rewrite *)
-
-let typeclasses_db = "typeclass_instances"
-let rewrite_db = "rewrite"
-
-let auto_init_db =
- Hintdbmap.add typeclasses_db (Hint_db.empty full_transparent_state true)
- (Hintdbmap.add rewrite_db (Hint_db.empty cst_full_transparent_state true)
- Hintdbmap.empty)
-
-let searchtable : hint_db_table = ref auto_init_db
-
-let searchtable_map name =
- Hintdbmap.find name !searchtable
-let searchtable_add (name,db) =
- searchtable := Hintdbmap.add name db !searchtable
-let current_db_names () = Hintdbmap.domain !searchtable
-let current_db () = Hintdbmap.bindings !searchtable
-
-(**************************************************************************)
-(* Definition of the summary *)
-(**************************************************************************)
-
-let auto_init : (unit -> unit) ref = ref (fun () -> ())
-let add_auto_init f =
- let init = !auto_init in
- auto_init := (fun () -> init (); f ())
-
-let init () = searchtable := auto_init_db; !auto_init ()
-let freeze _ = !searchtable
-let unfreeze fs = searchtable := fs
-
-let _ = Summary.declare_summary "search"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
-
-
-(**************************************************************************)
-(* Auxiliary functions to prepare AUTOHINT objects *)
-(**************************************************************************)
-
-let rec nb_hyp c = match kind_of_term c with
- | Prod(_,_,c2) -> if noccurn 1 c2 then 1+(nb_hyp c2) else nb_hyp c2
- | _ -> 0
-
-(* adding and removing tactics in the search table *)
-
-let try_head_pattern c =
- try head_pattern_bound c
- with BoundPattern -> error "Bound head variable."
-
-let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
- let cty = strip_outer_cast cty in
- match kind_of_term cty with
- | Prod _ -> failwith "make_exact_entry"
- | _ ->
- let pat = snd (Patternops.pattern_of_constr env sigma cty) in
- let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_exact_entry"
- in
- (Some hd,
- { pri = (match pri with None -> 0 | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
- code = Give_exact (c, cty, ctx) })
-
-let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
- let cty = if hnf then hnf_constr env sigma cty else cty in
- match kind_of_term cty with
- | Prod _ ->
- let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
- let ce = mk_clenv_from_env env sigma' None (c,cty) in
- let c' = clenv_type (* ~reduce:false *) ce in
- let pat = snd (Patternops.pattern_of_constr env ce.evd c') in
- let hd =
- try head_pattern_bound pat
- with BoundPattern -> failwith "make_apply_entry" in
- let nmiss = List.length (clenv_missing ce) in
- if Int.equal nmiss 0 then
- (Some hd,
- { pri = (match pri with None -> nb_hyp cty | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
- code = Res_pf(c,cty,ctx) })
- else begin
- if not eapply then failwith "make_apply_entry";
- if verbose then
- msg_warning (str "the hint: eapply " ++ pr_lconstr c ++
- str " will only be used by eauto");
- (Some hd,
- { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
- poly = poly;
- pat = Some pat;
- name = name;
- code = ERes_pf(c,cty,ctx) })
- end
- | _ -> failwith "make_apply_entry"
-
-(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose
- c is a constr
- cty is the type of constr *)
-
-let fresh_global_or_constr env sigma poly cr =
- match cr with
- | IsGlobRef gr -> Universes.fresh_global_instance env gr
- | IsConstr (c, ctx) -> (c, ctx)
-
-let make_resolves env sigma flags pri poly ?name cr =
- let c, ctx = fresh_global_or_constr env sigma poly cr in
- let cty = Retyping.get_type_of env sigma c in
- let try_apply f =
- try Some (f (c, cty, ctx)) with Failure _ -> None in
- let ents = List.map_filter try_apply
- [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name]
- in
- if List.is_empty ents then
- errorlabstrm "Hint"
- (pr_lconstr c ++ spc() ++
- (if pi1 flags then str"cannot be used as a hint."
- else str "can be used as a hint only for eauto."));
- ents
-
-(* used to add an hypothesis to the local hint database *)
-let make_resolve_hyp env sigma (hname,_,htyp) =
- try
- [make_apply_entry env sigma (true, true, false) None false
- ~name:(PathHints [VarRef hname])
- (mkVar hname, htyp, Univ.ContextSet.empty)]
- with
- | Failure _ -> []
- | e when Logic.catchable_exception e -> anomaly (Pp.str "make_resolve_hyp")
-
-(* REM : in most cases hintname = id *)
-let make_unfold eref =
- let g = global_of_evaluable_reference eref in
- (Some g,
- { pri = 4;
- poly = false;
- pat = None;
- name = PathHints [g];
- code = Unfold_nth eref })
-
-let make_extern pri pat tacast =
- let hdconstr = Option.map try_head_pattern pat in
- (hdconstr,
- { pri = pri;
- poly = false;
- pat = pat;
- name = PathAny;
- code = Extern tacast })
-
-let make_mode ref m =
- let ty = Global.type_of_global_unsafe ref in
- let ctx, t = decompose_prod ty in
- let n = List.length ctx in
- let m' = Array.of_list m in
- if not (n == Array.length m') then
- errorlabstrm "Hint"
- (pr_global ref ++ str" has " ++ int n ++
- str" arguments while the mode declares " ++ int (Array.length m'))
- else m'
-
-let make_trivial env sigma poly ?(name=PathAny) r =
- let c,ctx = fresh_global_or_constr env sigma poly r in
- let sigma = Evd.merge_context_set univ_flexible sigma ctx in
- let t = hnf_constr env sigma (type_of env sigma c) in
- let hd = head_of_constr_reference (head_constr t) in
- let ce = mk_clenv_from_env env sigma None (c,t) in
- (Some hd, { pri=1;
- poly = poly;
- pat = Some (snd (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
- name = name;
- code=Res_pf_THEN_trivial_fail(c,t,ctx) })
-
-open Vernacexpr
-
-(**************************************************************************)
-(* declaration of the AUTOHINT library object *)
-(**************************************************************************)
-
-(* If the database does not exist, it is created *)
-(* TODO: should a warning be printed in this case ?? *)
-
-let get_db dbname =
- try searchtable_map dbname
- with Not_found -> Hint_db.empty empty_transparent_state false
-
-let add_hint dbname hintlist =
- let db = get_db dbname in
- let db' = Hint_db.add_list hintlist db in
- searchtable_add (dbname,db')
-
-let add_transparency dbname grs b =
- let db = get_db dbname in
- let 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
- in searchtable_add (dbname, Hint_db.set_transparent_state db st')
-
-let remove_hint dbname grs =
- let db = get_db dbname in
- let db' = Hint_db.remove_list grs db in
- searchtable_add (dbname, db')
-
-type hint_action =
- | CreateDB of bool * transparent_state
- | AddTransparency of evaluable_global_reference list * bool
- | AddHints of hint_entry list
- | RemoveHints of global_reference list
- | AddCut of hints_path
- | AddMode of global_reference * bool array
-
-let add_cut dbname path =
- let db = get_db dbname in
- let db' = Hint_db.add_cut path db in
- searchtable_add (dbname, db')
-
-let add_mode dbname l m =
- let db = get_db dbname in
- let db' = Hint_db.add_mode l m db in
- searchtable_add (dbname, db')
-
-type hint_obj = bool * string * hint_action (* locality, name, action *)
-
-let cache_autohint (_,(local,name,hints)) =
- match hints with
- | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
- | AddTransparency (grs, b) -> add_transparency name grs b
- | AddHints hints -> add_hint name hints
- | RemoveHints grs -> remove_hint name grs
- | AddCut path -> add_cut name path
- | AddMode (l, m) -> add_mode name l m
-
-let subst_autohint (subst,(local,name,hintlist as obj)) =
- let subst_key gr =
- let (lab'', elab') = subst_global subst gr in
- let gr' =
- (try head_of_constr_reference (head_constr_bound elab')
- with Tactics.Bound -> lab'')
- in if gr' == gr then gr else gr'
- in
- let subst_hint (k,data as hint) =
- let k' = Option.smartmap subst_key k in
- let pat' = Option.smartmap (subst_pattern subst) data.pat in
- let code' = match data.code with
- | Res_pf (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'==t then data.code else Res_pf (c', t',ctx)
- | ERes_pf (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'==t then data.code else ERes_pf (c',t',ctx)
- | Give_exact (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t'== t then data.code else Give_exact (c',t',ctx)
- | Res_pf_THEN_trivial_fail (c,t,ctx) ->
- let c' = subst_mps subst c in
- let t' = subst_mps subst t in
- if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t',ctx)
- | Unfold_nth ref ->
- let ref' = subst_evaluable_reference subst ref in
- if ref==ref' then data.code else Unfold_nth ref'
- | Extern tac ->
- let tac' = Tacsubst.subst_tactic subst tac in
- if tac==tac' then data.code else Extern tac'
- in
- let name' = subst_path_atom subst data.name in
- let data' =
- if data.pat==pat' && data.name == name' && data.code==code' then data
- else { data with pat = pat'; name = name'; code = code' }
- in
- if k' == k && data' == data then hint else (k',data')
- in
- match hintlist with
- | CreateDB _ -> obj
- | AddTransparency (grs, b) ->
- let grs' = List.smartmap (subst_evaluable_reference subst) grs in
- if grs==grs' then obj else (local, name, AddTransparency (grs', b))
- | AddHints hintlist ->
- let hintlist' = List.smartmap subst_hint hintlist in
- if hintlist' == hintlist then obj else
- (local,name,AddHints hintlist')
- | RemoveHints grs ->
- let grs' = List.smartmap (subst_global_reference subst) grs in
- if grs==grs' then obj else (local, name, RemoveHints grs')
- | AddCut path ->
- let path' = subst_hints_path subst path in
- if path' == path then obj else (local, name, AddCut path')
- | AddMode (l,m) ->
- let l' = subst_global_reference subst l in
- (local, name, AddMode (l', m))
-
-let classify_autohint ((local,name,hintlist) as obj) =
- match hintlist with
- | AddHints [] -> Dispose
- | _ -> if local then Dispose else Substitute obj
-
-let inAutoHint : hint_obj -> obj =
- declare_object {(default_object "AUTOHINT") with
- cache_function = cache_autohint;
- load_function = (fun _ -> cache_autohint);
- subst_function = subst_autohint;
- classify_function = classify_autohint; }
-
-let create_hint_db l n st b =
- Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB (b, st)))
-
-let remove_hints local dbnames grs =
- let dbnames = if List.is_empty dbnames then ["core"] else dbnames in
- List.iter
- (fun dbname ->
- Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
- dbnames
-
-open Misctypes
-
-(**************************************************************************)
-(* The "Hint" vernacular command *)
-(**************************************************************************)
-let add_resolves env sigma clist local dbnames =
- List.iter
- (fun dbname ->
- Lib.add_anonymous_leaf
- (inAutoHint
- (local,dbname, AddHints
- (List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
- make_resolves env sigma (true,hnf,Flags.is_verbose())
- pri poly ~name:path gr) clist)))))
- dbnames
-
-let add_unfolds l local dbnames =
- List.iter
- (fun dbname -> Lib.add_anonymous_leaf
- (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
- dbnames
-
-let add_cuts l local dbnames =
- List.iter
- (fun dbname -> Lib.add_anonymous_leaf
- (inAutoHint (local,dbname, AddCut l)))
- dbnames
-
-let add_mode l m local dbnames =
- List.iter
- (fun dbname -> Lib.add_anonymous_leaf
- (let m' = make_mode l m in
- (inAutoHint (local,dbname, AddMode (l,m')))))
- dbnames
-
-let add_transparency l b local dbnames =
- List.iter
- (fun dbname -> Lib.add_anonymous_leaf
- (inAutoHint (local,dbname, AddTransparency (l, b))))
- dbnames
-
-let add_extern pri pat tacast local dbname =
- let pat = match pat with
- | None -> None
- | Some (_, pat) -> Some pat
- in
- let hint = local, dbname, AddHints [make_extern pri pat tacast] in
- Lib.add_anonymous_leaf (inAutoHint hint)
-
-let add_externs pri pat tacast local dbnames =
- List.iter (add_extern pri pat tacast local) dbnames
-
-let add_trivials env sigma l local dbnames =
- List.iter
- (fun dbname ->
- Lib.add_anonymous_leaf (
- inAutoHint(local,dbname,
- AddHints (List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l))))
- dbnames
-
-let (forward_intern_tac, extern_intern_tac) = Hook.make ()
-
-type hnf = bool
-
-type hints_entry =
- | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * hint_term) list
- | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
- | HintsCutEntry of hints_path
- | HintsUnfoldEntry of evaluable_global_reference list
- | HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * bool list
- | HintsExternEntry of
- int * (patvar list * constr_pattern) option * glob_tactic_expr
-
-let default_prepare_hint_ident = Id.of_string "H"
-
-exception Found of constr * types
-
-let prepare_hint check env init (sigma,c) =
- let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
- (* We re-abstract over uninstantiated evars.
- It is actually a bit stupid to generalize over evars since the first
- thing make_resolves will do is to re-instantiate the products *)
- let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in
- let vars = ref (collect_vars c) in
- let subst = ref [] in
- let rec find_next_evar c = match kind_of_term c with
- | Evar (evk,args as ev) ->
- (* We skip the test whether args is the identity or not *)
- let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
- let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
- if not (Int.Set.is_empty (free_rels t)) then
- error "Hints with holes dependent on a bound variable not supported.";
- if occur_existential t then
- (* Not clever enough to construct dependency graph of evars *)
- error "Not clever enough to deal with evars dependent in other evars.";
- raise (Found (c,t))
- | _ -> iter_constr find_next_evar c in
- let rec iter c =
- try find_next_evar c; c
- with Found (evar,t) ->
- let id = next_ident_away_from default_prepare_hint_ident (fun id -> Id.Set.mem id !vars) in
- vars := Id.Set.add id !vars;
- subst := (evar,mkVar id)::!subst;
- mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
- let c' = iter c in
- if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
- let diff = Evd.diff sigma init in
- IsConstr (c', Evd.universe_context_set diff)
-
-let interp_hints poly =
- fun h ->
- let f c =
- let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in
- prepare_hint true (Global.env()) Evd.empty (evd,c) in
- let fref r =
- let gr = global_with_alias r in
- Dumpglob.add_glob (loc_of_reference r) gr;
- gr in
- let fr r =
- evaluable_of_global_reference (Global.env()) (fref r)
- in
- let fi c =
- match c with
- | HintsReference c ->
- let gr = global_with_alias c in
- (PathHints [gr], poly, IsGlobRef gr)
- | HintsConstr c -> (PathAny, poly, f c)
- in
- let fres (pri, b, r) =
- let path, poly, gr = fi r in
- (pri, poly, b, path, gr)
- in
- let fp = Constrintern.intern_constr_pattern (Global.env()) in
- match h with
- | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
- | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
- | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
- | HintsTransparency (lhints, b) ->
- HintsTransparencyEntry (List.map fr lhints, 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 (fst (qualid_of_reference qid)) "<>" (string_of_reference qid) "ind";
- List.init (nconstructors ind)
- (fun i -> let c = (ind,i+1) in
- let gr = ConstructRef c in
- None, mib.Declarations.mind_polymorphic, true,
- PathHints [gr], IsGlobRef gr)
- in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
- | HintsExtern (pri, patcom, tacexp) ->
- let pat = Option.map fp patcom in
- let l = match pat with None -> [] | Some (l, _) -> l in
- let tacexp = Hook.get forward_intern_tac l tacexp in
- HintsExternEntry (pri, pat, tacexp)
-
-let add_hints local dbnames0 h =
- if String.List.mem "nocore" dbnames0 then
- error "The hint database \"nocore\" is meant to stay empty.";
- let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
- let env = Global.env() and sigma = Evd.empty in
- match h with
- | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
- | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
- | HintsCutEntry lhints -> add_cuts lhints local dbnames
- | HintsModeEntry (l,m) -> add_mode l m local dbnames
- | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames
- | HintsTransparencyEntry (lhints, b) ->
- add_transparency lhints b local dbnames
- | HintsExternEntry (pri, pat, tacexp) ->
- add_externs pri pat tacexp local dbnames
-
-(**************************************************************************)
-(* Functions for printing the hints *)
-(**************************************************************************)
-
-let pr_autotactic =
- function
- | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
- | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
- | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c)
- | Res_pf_THEN_trivial_fail (c,clenv) ->
- (str"apply " ++ pr_constr c ++ str" ; trivial")
- | Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
- | Extern tac ->
- let env =
- try
- let (_, env) = Pfedit.get_current_goal_context () in
- env
- with e when Errors.noncritical e -> Global.env ()
- in
- (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
-
-let pr_hint (id, v) =
- (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
-
-let pr_hint_list hintlist =
- (str " " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ())
-
-let pr_hints_db (name,db,hintlist) =
- (str "In the database " ++ str name ++ str ":" ++
- if List.is_empty hintlist then (str " nothing" ++ fnl ())
- else (fnl () ++ pr_hint_list hintlist))
-
-(* Print all hints associated to head c in any database *)
-let pr_hint_list_for_head c =
- let dbs = current_db () in
- let validate (name, db) =
- let hints = List.map (fun v -> 0, v) (Hint_db.map_all c db) in
- (name, db, hints)
- in
- let valid_dbs = List.map validate dbs in
- if List.is_empty valid_dbs then
- (str "No hint declared for :" ++ pr_global c)
- else
- hov 0
- (str"For " ++ pr_global c ++ str" -> " ++ fnl () ++
- hov 0 (prlist pr_hints_db valid_dbs))
-
-let pr_hint_ref ref = pr_hint_list_for_head ref
-
-(* Print all hints associated to head id in any database *)
-
-let pr_hint_term cl =
- try
- let dbs = current_db () in
- let valid_dbs =
- let fn = try
- let hdc = decompose_app_bound cl in
- if occur_existential cl then
- Hint_db.map_existential hdc cl
- else Hint_db.map_auto hdc cl
- with Bound -> Hint_db.map_none
- in
- let fn db = List.map (fun x -> 0, x) (fn db) in
- List.map (fun (name, db) -> (name, db, fn db)) dbs
- in
- if List.is_empty valid_dbs then
- (str "No hint applicable for current goal")
- else
- (str "Applicable Hints :" ++ fnl () ++
- hov 0 (prlist pr_hints_db valid_dbs))
- with Match_failure _ | Failure _ ->
- (str "No hint applicable for current goal")
-
-let error_no_such_hint_database x =
- error ("No such Hint database: "^x^".")
-
-(* print all hints that apply to the concl of the current goal *)
-let pr_applicable_hint () =
- let pts = get_pftreestate () in
- let glss = Proof.V82.subgoals pts in
- match glss.Evd.it with
- | [] -> Errors.error "No focused goal."
- | g::_ ->
- let gl = { Evd.it = g; sigma = glss.Evd.sigma; } in
- pr_hint_term (pf_concl gl)
-
-(* displays the whole hint database db *)
-let pr_hint_db db =
- let pr_mode = prvect_with_sep spc (fun x -> if x then str"+" else str"-") in
- let pr_modes l =
- if List.is_empty l then mt ()
- else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")"
- in
- let content =
- let fold head modes hintlist accu =
- let goal_descr = match head with
- | None -> str "For any goal"
- | Some head -> str "For " ++ pr_global head ++ pr_modes modes
- in
- let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in
- let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in
- accu ++ hint_descr
- in
- Hint_db.fold fold db (mt ())
- in
- let (ids, csts) = Hint_db.transparent_state db in
- hov 0
- ((if Hint_db.use_dn db then str"Discriminated database"
- else str"Non-discriminated database")) ++ fnl () ++
- hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids) ++ fnl () ++
- hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts) ++ fnl () ++
- hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
- content
-
-let pr_hint_db_by_name dbname =
- try
- let db = searchtable_map dbname in pr_hint_db db
- with Not_found ->
- error_no_such_hint_database dbname
-
-(* displays all the hints of all databases *)
-let pr_searchtable () =
- let fold name db accu =
- accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++
- pr_hint_db db ++ fnl ()
- in
- Hintdbmap.fold fold !searchtable (mt ())
+open Hints
(**************************************************************************)
(* Automatic tactics *)
@@ -1233,44 +104,6 @@ let exact poly (c,clenv) =
(* Util *)
-let expand_constructor_hints env sigma lems =
- List.map_append (fun (evd,lem) ->
- match kind_of_term lem with
- | Ind (ind,u) ->
- List.init (nconstructors ind)
- (fun i -> IsConstr (mkConstructU ((ind,i+1),u),
- Univ.ContextSet.empty))
- | _ ->
- [prepare_hint false env sigma (evd,lem)]) lems
-
-(* builds a hint database from a constr signature *)
-(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
-
-let add_hint_lemmas eapply lems hint_db gl =
- let lems = expand_constructor_hints (pf_env gl) (project gl) lems in
- let hintlist' =
- List.map_append (pf_apply make_resolves gl (eapply,true,false) None true) lems in
- Hint_db.add_list hintlist' hint_db
-
-let make_local_hint_db ts eapply lems gl =
- let sign = pf_hyps gl in
- let ts = match ts with
- | None -> Hint_db.transparent_state (searchtable_map "core")
- | Some ts -> ts
- in
- let hintlist = List.map_append (pf_apply make_resolve_hyp gl) sign in
- add_hint_lemmas eapply lems
- (Hint_db.add_list hintlist (Hint_db.empty ts false)) gl
-
-let make_local_hint_db =
- if Flags.profile then
- let key = Profile.declare_profile "make_local_hint_db" in
- Profile.profile4 key make_local_hint_db
- else make_local_hint_db
-
-let make_local_hint_db ?ts eapply lems gl =
- make_local_hint_db ts eapply lems gl
-
(* Serait-ce possible de compiler d'abord la tactique puis de faire la
substitution sans passer par bdize dont l'objectif est de préparer un
terme pour l'affichage ? (HH) *)
@@ -1557,31 +390,24 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
(** The use of the "core" database can be de-activated by passing
"nocore" amongst the databases. *)
-let make_db_list dbnames =
- let use_core = not (List.mem "nocore" dbnames) in
- let dbnames = List.remove String.equal "nocore" dbnames in
- let dbnames = if use_core then "core"::dbnames else dbnames in
- let lookup db =
- try searchtable_map db with Not_found -> error_no_such_hint_database db
- in
- List.map lookup dbnames
-
let trivial ?(debug=Off) lems dbnames =
Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let db_list = make_db_list dbnames in
let d = mk_trivial_dbg debug in
- let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(trivial_fail_db d false db_list hints)
end
let full_trivial ?(debug=Off) lems =
Proofview.Goal.nf_enter begin fun gl ->
- let dbs = !searchtable in
- let dbs = String.Map.remove "v62" dbs in
- let db_list = List.map snd (String.Map.bindings dbs) in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let db_list = current_pure_db () in
let d = mk_trivial_dbg debug in
- let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(trivial_fail_db d false db_list hints)
end
@@ -1647,9 +473,11 @@ let default_search_depth = ref 5
let delta_auto debug mod_delta n lems dbnames =
Proofview.Goal.nf_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
let db_list = make_db_list dbnames in
let d = mk_auto_dbg debug in
- let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(search d n mod_delta db_list hints)
end
@@ -1668,11 +496,11 @@ let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems =
Proofview.Goal.nf_enter begin fun gl ->
- let dbs = !searchtable in
- let dbs = String.Map.remove "v62" dbs in
- let db_list = List.map snd (String.Map.bindings dbs) in
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let db_list = current_pure_db () in
let d = mk_auto_dbg debug in
- let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
+ let hints = make_local_hint_db env sigma false lems in
tclTRY_dbg d
(search d n mod_delta db_list hints)
end
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 26dcee8cc..fd24846d8 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,208 +6,19 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
open Names
open Term
-open Context
open Proof_type
-open Tacmach
open Clenv
open Pattern
-open Environ
open Evd
-open Globnames
-open Vernacexpr
-open Mod_subst
-open Misctypes
-open Pp
open Decl_kinds
-
-(** Auto and related automation tactics *)
-
-type 'a auto_tactic =
- | Res_pf of 'a (* Hint Apply *)
- | ERes_pf of 'a (* Hint EApply *)
- | Give_exact of 'a
- | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
- | Unfold_nth of evaluable_global_reference (* Hint Unfold *)
- | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *)
-
-type hints_path_atom =
- | PathHints of global_reference list
- | PathAny
-
-type 'a gen_auto_tactic = {
- pri : int; (** A number between 0 and 4, 4 = lower priority *)
- poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *)
- pat : constr_pattern option; (** A pattern for the concl of the Goal *)
- name : hints_path_atom; (** A potential name to refer to the hint *)
- code : 'a auto_tactic; (** the tactic to apply when the concl matches pat *)
-}
-
-type pri_auto_tactic = (constr * clausenv) gen_auto_tactic
-
-type search_entry
-
-(** The head may not be bound. *)
-
-type hint_entry = global_reference option *
- (constr * types * Univ.universe_context_set) gen_auto_tactic
-
-type hints_path =
- | PathAtom of hints_path_atom
- | PathStar of hints_path
- | PathSeq of hints_path * hints_path
- | PathOr of hints_path * hints_path
- | PathEmpty
- | PathEpsilon
-
-val normalize_path : hints_path -> hints_path
-val path_matches : hints_path -> hints_path_atom list -> bool
-val path_derivate : hints_path -> hints_path_atom -> hints_path
-val pp_hints_path : hints_path -> Pp.std_ppcmds
-
-module Hint_db :
- sig
- type t
- val empty : transparent_state -> bool -> t
- val find : global_reference -> t -> search_entry
- val map_none : t -> pri_auto_tactic list
-
- (** All hints associated to the reference *)
- val map_all : global_reference -> t -> pri_auto_tactic list
-
- (** All hints associated to the reference, respecting modes if evars appear in the
- arguments, _not_ using the discrimination net. *)
- val map_existential : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
-
- (** All hints associated to the reference, respecting modes if evars appear in the
- arguments and using the discrimination net. *)
- val map_eauto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
-
- (** All hints associated to the reference, respecting modes if evars appear in the
- arguments. *)
- val map_auto : (global_reference * constr array) -> constr -> t -> pri_auto_tactic list
-
- val add_one : hint_entry -> t -> t
- val add_list : (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 -> bool array list -> pri_auto_tactic 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 cut : t -> hints_path
-
- val unfolds : t -> Id.Set.t * Cset.t
- end
-
-type hint_db_name = string
-
-type hint_db = Hint_db.t
-
-type hnf = bool
-
-type hint_term =
- | IsGlobRef of global_reference
- | IsConstr of constr * Univ.universe_context_set
-
-type hints_entry =
- | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom *
- hint_term) list
- | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
- | HintsCutEntry of hints_path
- | HintsUnfoldEntry of evaluable_global_reference list
- | HintsTransparencyEntry of evaluable_global_reference list * bool
- | HintsModeEntry of global_reference * bool list
- | HintsExternEntry of
- int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
-
-val searchtable_map : hint_db_name -> hint_db
-
-val searchtable_add : (hint_db_name * hint_db) -> unit
-
-(** [create_hint_db local name st use_dn].
- [st] is a transparency state for unification using this db
- [use_dn] switches the use of the discrimination net for all hints
- and patterns. *)
-
-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 current_db_names : unit -> String.Set.t
-
-val interp_hints : polymorphic -> hints_expr -> hints_entry
-
-val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit
-
-val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map ->
- open_constr -> hint_term
-
-val pr_searchtable : unit -> std_ppcmds
-val pr_applicable_hint : unit -> std_ppcmds
-val pr_hint_ref : global_reference -> std_ppcmds
-val pr_hint_db_by_name : hint_db_name -> std_ppcmds
-val pr_hint_db : Hint_db.t -> std_ppcmds
-
-(** [make_exact_entry pri (c, ctyp)].
- [c] is the term given as an exact proof to solve the goal;
- [ctyp] is the type of [c]. *)
-
-val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom ->
- (constr * types * Univ.universe_context_set) -> hint_entry
-
-(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)].
- [eapply] is true if this hint will be used only with EApply;
- [hnf] should be true if we should expand the head of cty before searching for
- products;
- [c] is the term given as an exact proof to solve the goal;
- [cty] is the type of [c]. *)
-
-val make_apply_entry :
- env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom ->
- (constr * types * Univ.universe_context_set) -> hint_entry
-
-(** A constr which is Hint'ed will be:
- - (1) used as an Exact, if it does not start with a product
- - (2) used as an Apply, if its HNF starts with a product, and
- has no missing arguments.
- - (3) used as an EApply, if its HNF starts with a product, and
- has missing arguments. *)
-
-val make_resolves :
- env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom ->
- hint_term -> hint_entry list
-
-(** [make_resolve_hyp hname htyp].
- used to add an hypothesis to the local hint database;
- Never raises a user exception;
- If the hyp cannot be used as a Hint, the empty list is returned. *)
-
-val make_resolve_hyp :
- env -> evar_map -> named_declaration -> hint_entry list
-
-(** [make_extern pri pattern tactic_expr] *)
-
-val make_extern :
- int -> constr_pattern option -> Tacexpr.glob_tactic_expr
- -> hint_entry
+open Hints
val extern_interp :
(patvar_map -> Tacexpr.glob_tactic_expr -> unit Proofview.tactic) Hook.t
-val extern_intern_tac :
- (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
-
-(** Create a Hint database from the pairs (name, constr).
- Useful to take the current goal hypotheses as hints;
- Boolean tells if lemmas with evars are allowed *)
-
-val make_local_hint_db : ?ts:transparent_state -> bool -> open_constr list -> goal sigma -> hint_db
+(** Auto and related automation tactics *)
val priority : ('a * pri_auto_tactic) list -> ('a * pri_auto_tactic) list
@@ -232,8 +43,6 @@ val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -
(** The use of the "core" database can be de-activated by passing
"nocore" amongst the databases. *)
-val make_db_list : hint_db_name list -> hint_db list
-
val auto : ?debug:Tacexpr.debug ->
int -> open_constr list -> hint_db_name list -> unit Proofview.tactic
@@ -276,14 +85,3 @@ val full_trivial : ?debug:Tacexpr.debug ->
open_constr list -> unit Proofview.tactic
val h_trivial : ?debug:Tacexpr.debug ->
open_constr list -> hint_db_name list option -> unit Proofview.tactic
-
-val pr_autotactic : (constr * 'a) auto_tactic -> Pp.std_ppcmds
-
-(** Hook for changing the initialization of auto *)
-
-val add_auto_init : (unit -> unit) -> unit
-
-(** Pre-created hint databases *)
-
-val typeclasses_db : hint_db_name
-val rewrite_db : hint_db_name
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d9f90b02e..38f1114b5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -25,6 +25,7 @@ open Evd
open Locus
open Misctypes
open Proofview.Notations
+open Hints
(** Hint database named "typeclass_instances", now created directly in Auto *)
@@ -215,7 +216,7 @@ let pr_ev evs ev = Printer.pr_constr_env (Goal.V82.env evs ev) evs (Evarutil.nf_
let pr_depth l = prlist_with_sep (fun () -> str ".") int (List.rev l)
-type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
+type autoinfo = { hints : hint_db; is_evar: existential_key option;
only_classes: bool; unique : bool;
auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t;
auto_path : global_reference option list;
@@ -750,7 +751,7 @@ let set_typeclasses_depth =
let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
try
let dbs = List.map_filter
- (fun db -> try Some (Auto.searchtable_map db)
+ (fun db -> try Some (searchtable_map db)
with e when Errors.noncritical e -> None)
dbs
in
@@ -787,7 +788,7 @@ let is_ground c gl =
let autoapply c i gl =
let flags = auto_unif_flags Evar.Set.empty
- (Auto.Hint_db.transparent_state (Auto.searchtable_map i)) in
+ (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
let cty = pf_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
unify_e_resolve false flags (c,ce) gl
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index f64f708de..00c601d28 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -21,7 +21,7 @@ val get_typeclasses_depth : unit -> int option
val progress_evars : unit Proofview.tactic -> unit Proofview.tactic
val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
- Auto.hint_db_name list -> tactic
+ Hints.hint_db_name list -> tactic
val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic
@@ -29,4 +29,4 @@ val not_evar : constr -> unit Proofview.tactic
val is_ground : constr -> tactic
-val autoapply : constr -> Auto.hint_db_name -> tactic
+val autoapply : constr -> Hints.hint_db_name -> tactic
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 711ae92b0..334e0c22a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -27,6 +27,7 @@ open Tacexpr
open Misctypes
open Locus
open Locusops
+open Hints
DECLARE PLUGIN "eauto"
@@ -196,8 +197,8 @@ type search_state = {
depth : int; (*r depth of search before failing *)
tacres : goal list sigma;
last_tactic : std_ppcmds Lazy.t;
- dblist : Auto.hint_db list;
- localdb : Auto.hint_db list;
+ dblist : hint_db list;
+ localdb : hint_db list;
prev : prev_search_state
}
@@ -289,7 +290,7 @@ module SearchProblem = struct
let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
let hyps' = pf_hyps gls in
if hyps' == hyps then List.hd s.localdb
- else make_local_hint_db ~ts:full_transparent_state true [] gls)
+ else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true [])
(List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
in
{ depth = pred s.depth; tacres = res;
@@ -369,7 +370,7 @@ let make_initial_state dbg n gl dblist localdb =
}
let e_search_auto debug (in_depth,p) lems db_list gl =
- let local_db = make_local_hint_db ~ts:full_transparent_state true lems gl in
+ let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:full_transparent_state true lems in
let d = mk_eauto_dbg debug in
let tac = match in_depth,d with
| (true,Debug) -> Search.debug_depth_first
@@ -505,7 +506,7 @@ let autounfold db cls gl =
let autounfold_tac db cls gl =
let dbs = match db with
- | None -> String.Set.elements (Auto.current_db_names ())
+ | None -> String.Set.elements (current_db_names ())
| Some [] -> ["core"]
| Some l -> l
in
@@ -661,6 +662,6 @@ END
VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
let entry = HintsCutEntry p in
- Auto.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
+ Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
(match dbnames with None -> ["core"] | Some l -> l) entry ]
END
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e2da23aaa..488bc037c 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -10,6 +10,7 @@ open Term
open Proof_type
open Auto
open Evd
+open Hints
val hintbases : hint_db_name list option Pcoq.Gram.entry
@@ -33,6 +34,6 @@ val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> open_constr list ->
val eauto_with_bases :
?debug:Tacexpr.debug ->
bool * int ->
- open_constr list -> Auto.hint_db list -> Proof_type.tactic
+ open_constr list -> hint_db list -> Proof_type.tactic
val autounfold : hint_db_name list -> Locus.clause -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cb15bb94c..342e65cba 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -325,11 +325,11 @@ let project_hint pri l2r r =
in
let ctx = Evd.universe_context_set sigma in
let c = Declare.declare_definition ~internal:Declare.KernelSilent id (c,ctx) in
- (pri,false,true,Auto.PathAny, Auto.IsGlobRef (Globnames.ConstRef c))
+ (pri,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
let add_hints_iff l2r lc n bl =
- Auto.add_hints true bl
- (Auto.HintsResolveEntry (List.map (project_hint n l2r) lc))
+ Hints.add_hints true bl
+ (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc))
VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
[ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4
index 1e666e5a5..a49c76f14 100644
--- a/tactics/g_class.ml4
+++ b/tactics/g_class.ml4
@@ -64,7 +64,7 @@ END
TACTIC EXTEND typeclasses_eauto
| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ Proofview.V82.tactic (typeclasses_eauto l) ]
-| [ "typeclasses" "eauto" ] -> [ Proofview.V82.tactic (typeclasses_eauto ~only_classes:true [Auto.typeclasses_db]) ]
+| [ "typeclasses" "eauto" ] -> [ Proofview.V82.tactic (typeclasses_eauto ~only_classes:true [Hints.typeclasses_db]) ]
END
TACTIC EXTEND head_of_constr
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index fbcd9ee2d..63885318c 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -517,12 +517,12 @@ let rewrite_db = "rewrite"
let conv_transparent_state = (Id.Pred.empty, Cpred.full)
let _ =
- Auto.add_auto_init
+ Hints.add_hints_init
(fun () ->
- Auto.create_hint_db false rewrite_db conv_transparent_state true)
+ Hints.create_hint_db false rewrite_db conv_transparent_state true)
let rewrite_transparent_state () =
- Auto.Hint_db.transparent_state (Auto.searchtable_map rewrite_db)
+ Hints.Hint_db.transparent_state (Hints.searchtable_map rewrite_db)
let rewrite_core_unif_flags = {
Unification.modulo_conv_on_closed_terms = None;
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 08dd0dff4..3f27d0b91 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -825,4 +825,4 @@ let _ =
Flags.with_option strict_check
(intern_pure_tactic { (make_empty_glob_sign()) with ltacvars })
in
- Hook.set Auto.extern_intern_tac f
+ Hook.set Hints.extern_intern_tac f
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c40dc4078..68aac55c8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -44,8 +44,6 @@ open Locusops
open Misctypes
open Proofview.Notations
-exception Bound
-
let nb_prod x =
let rec count n c =
match kind_of_term c with
@@ -114,34 +112,6 @@ let _ =
(* Tactics *)
(*********************************************)
-(****************************************)
-(* General functions *)
-(****************************************)
-
-let head_constr_bound t =
- let t = strip_outer_cast t in
- let _,ccl = decompose_prod_assum t in
- let hd,args = decompose_app ccl in
- match kind_of_term hd with
- | Const _ | Ind _ | Construct _ | Var _ -> hd
- | Proj (p, _) -> mkConst (Projection.constant p)
- | _ -> raise Bound
-
-let head_constr c =
- try head_constr_bound c with Bound -> error "Bound head variable."
-
-let decompose_app_bound t =
- let t = strip_outer_cast t in
- let _,ccl = decompose_prod_assum t in
- let hd,args = decompose_app_vect ccl in
- match kind_of_term hd with
- | Const (c,u) -> ConstRef c, args
- | Ind (i,u) -> IndRef i, args
- | Construct (c,u) -> ConstructRef c, args
- | Var id -> VarRef id, args
- | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args
- | _ -> raise Bound
-
(******************************************)
(* Primitive tactics *)
(******************************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 398a90ba3..6ecb48101 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,11 +26,6 @@ open Locus
(** {6 General functions. } *)
-exception Bound
-
-val head_constr : constr -> constr
-val head_constr_bound : constr -> constr
-val decompose_app_bound : constr -> global_reference * constr array
val is_quantified_hypothesis : Id.t -> goal sigma -> bool
(** {6 Primitive tactics. } *)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index e2c0f40fb..46f2abd7f 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -17,6 +17,7 @@ Leminv
Tacsubst
Taccoerce
Tacenv
+Hints
Auto
Tacintern
TacticMatching
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 8f36fc79f..4d23a4181 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -28,22 +28,22 @@ open Entries
let typeclasses_db = "typeclass_instances"
let set_typeclass_transparency c local b =
- Auto.add_hints local [typeclasses_db]
- (Auto.HintsTransparencyEntry ([c], b))
+ Hints.add_hints local [typeclasses_db]
+ (Hints.HintsTransparencyEntry ([c], b))
let _ =
Hook.set Typeclasses.add_instance_hint_hook
(fun inst path local pri poly ->
- let inst' = match inst with IsConstr c -> Auto.IsConstr (c, Univ.ContextSet.empty)
- | IsGlobal gr -> Auto.IsGlobRef gr
+ let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
+ | IsGlobal gr -> Hints.IsGlobRef gr
in
Flags.silently (fun () ->
- Auto.add_hints local [typeclasses_db]
- (Auto.HintsResolveEntry
- [pri, poly, false, Auto.PathHints path, inst'])) ());
+ Hints.add_hints local [typeclasses_db]
+ (Hints.HintsResolveEntry
+ [pri, poly, false, Hints.PathHints path, inst'])) ());
Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
Hook.set Typeclasses.classes_transparent_state_hook
- (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
+ (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
(** TODO: add subinstances *)
let existing_instance glob g pri =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 2ac4339c1..b303533e4 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -632,8 +632,8 @@ let declare_obligation prg obl body ty uctx =
(DefinitionEntry ce,IsProof Property)
in
if not opaque then
- Auto.add_hints false [Id.to_string prg.prg_name]
- (Auto.HintsUnfoldEntry [EvalConstRef constant]);
+ Hints.add_hints false [Id.to_string prg.prg_name]
+ (Hints.HintsUnfoldEntry [EvalConstRef constant]);
definition_message obl.obl_name;
{ obl with obl_body =
if poly then
@@ -813,8 +813,8 @@ let rec solve_obligation prg num tac =
else DefinedObl cst
in
if transparent then
- Auto.add_hints true [Id.to_string prg.prg_name]
- (Auto.HintsUnfoldEntry [EvalConstRef cst]);
+ Hints.add_hints true [Id.to_string prg.prg_name]
+ (Hints.HintsUnfoldEntry [EvalConstRef cst]);
{ obl with obl_body = Some body }
in
let obls = Array.copy obls in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 63253d54e..f6bc8bbeb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -967,15 +967,15 @@ let vernac_declare_tactic_definition locality (x,def) =
let vernac_create_hintdb locality id b =
let local = make_module_locality locality in
- Auto.create_hint_db local id full_transparent_state b
+ Hints.create_hint_db local id full_transparent_state b
let vernac_remove_hints locality dbs ids =
let local = make_module_locality locality in
- Auto.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
+ Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
let vernac_hints locality poly local lb h =
let local = enforce_module_locality locality local in
- Auto.add_hints local lb (Auto.interp_hints poly h)
+ Hints.add_hints local lb (Hints.interp_hints poly h)
let vernac_syntactic_definition locality lid x local y =
Dumpglob.dump_definition lid false "syndef";
@@ -1528,11 +1528,11 @@ let vernac_print = function
let univ = if b then Univ.sort_universes univ else univ in
msg_notice (Univ.pr_universes univ)
| PrintUniverses (b, Some s) -> dump_universes b s
- | PrintHint r -> msg_notice (Auto.pr_hint_ref (smart_global r))
- | PrintHintGoal -> msg_notice (Auto.pr_applicable_hint ())
- | PrintHintDbName s -> msg_notice (Auto.pr_hint_db_by_name s)
+ | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
+ | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
+ | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
| PrintRewriteHintDbName s -> msg_notice (Autorewrite.print_rewrite_hintdb s)
- | PrintHintDb -> msg_notice (Auto.pr_searchtable ())
+ | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
| PrintScopes ->
msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
| PrintScope s ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 14:14:56 +0000