aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/vernacexpr.mli1
-rw-r--r--parsing/g_proofs.ml44
-rw-r--r--plugins/firstorder/sequent.ml2
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--printing/ppvernac.ml3
-rw-r--r--tactics/auto.ml173
-rw-r--r--tactics/auto.mli19
-rw-r--r--tactics/class_tactics.ml20
-rw-r--r--tactics/eauto.ml412
-rw-r--r--tactics/tactics.ml12
-rw-r--r--tactics/tactics.mli5
-rw-r--r--test-suite/success/auto.v21
-rw-r--r--test-suite/typeclasses/backtrack.v6
13 files changed, 198 insertions, 82 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 009ec543c..e670f68c2 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -125,6 +125,7 @@ type hints_expr =
| HintsImmediate of reference_or_constr list
| HintsUnfold of reference list
| HintsTransparency of reference list * bool
+ | HintsMode of reference * bool list
| HintsConstructors of reference list
| HintsExtern of int * constr_expr option * raw_tactic_expr
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 212d4af6d..2c8eb85b8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -146,6 +146,7 @@ GEXTEND Gram
| IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
| IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
| IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false)
+ | IDENT "Mode"; l = global; m = mode -> HintsMode (l, m)
| IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
| IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
| IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
@@ -156,4 +157,7 @@ GEXTEND Gram
[ [ ":="; c = lconstr -> c
| ":"; t = lconstr; ":="; c = lconstr -> CCast(!@loc,c,CastConv t) ] ]
;
+ mode:
+ [ [ l = LIST1 ["+" -> true | "-" -> false] -> l ] ]
+ ;
END
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index afa178832..6d4d8792f 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -218,7 +218,7 @@ let extend_with_auto_hints l seq gl=
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
| _-> () in
- let g _ l = List.iter f l in
+ let g _ _ l = List.iter f l in
let h dbname=
let hdb=
try
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 420666356..5828e7f43 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -157,7 +157,7 @@ let pattern_of_constr sigma t =
| Evar_kinds.MatchingVar (b,id) ->
ctx := (id,None,existential_type sigma ev)::!ctx;
assert (not b); PMeta (Some id)
- | Evar_kinds.GoalEvar _ -> PEvar (evk,Array.map pattern_of_constr ctxt)
+ | Evar_kinds.GoalEvar -> PEvar (evk,Array.map pattern_of_constr ctxt)
| _ -> PMeta None)
| Case (ci,p,a,br) ->
let cip =
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b7ac274b7..a075265cc 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -172,6 +172,9 @@ let pr_hints db h pr_c pr_pat =
| HintsTransparency (l, b) ->
str (if b then "Transparent " else "Opaque ") ++ prlist_with_sep sep
pr_reference l
+ | HintsMode (m, l) ->
+ str "Mode " ++ pr_reference m ++ spc() ++ prlist_with_sep spc
+ (fun b -> if b then str"+" else str"-") l
| HintsConstructors c ->
str"Constructors" ++ spc() ++ prlist_with_sep spc pr_reference c
| HintsExtern (n,c,tac) ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e386728fe..0f1d7cb02 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -137,9 +137,10 @@ module Bounded_net = Btermdn.Make(struct
let compare = pri_order_int
end)
-type search_entry = stored_data list * stored_data list * Bounded_net.t
+type search_entry = stored_data list * stored_data list * Bounded_net.t * bool array list
-let empty_se = ([],[],Bounded_net.create ())
+
+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
@@ -157,20 +158,25 @@ let eq_pri_auto_tactic (_, x) (_, y) =
else
false
-let add_tac pat t st (l,l',dn) =
+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) else (l, l', dn)
+ | 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)) else (l, l', dn)
-
-let rebuild_dn st ((l,l',dn) : search_entry) =
- (l, l', List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t)))
- (Bounded_net.create ()) l')
-
+ 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 (hdc,c) st (l,l',dn) =
- let l' = Bounded_net.lookup st dn c in
+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'
@@ -378,18 +384,43 @@ module Hint_db = struct
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
+ let (l,l',_,_) = find k db in
List.map realize_tac (Sort.merge pri_order (List.map snd db.hintdb_nopat @ l) l')
-
- let map_auto (k,c) db =
- let st = if db.use_dn then Some db.hintdb_state else None in
- let l' = lookup_tacs (k,c) st (find k db) in
+
+ (** 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
@@ -446,10 +477,10 @@ module Hint_db = struct
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 as he) =
+ 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)
+ else rebuild_dn st (sl1', sl2', dn, m)
let remove_list grs db =
let filter (_, h) =
@@ -461,12 +492,12 @@ module Hint_db = struct
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',_) -> f (Some k) (List.map realize_tac (l@l'))) db.hintdb_map
+ 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',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map 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
@@ -477,6 +508,10 @@ module Hint_db = struct
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
@@ -648,6 +683,17 @@ let make_extern pri pat tacast =
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 t = hnf_constr env sigma (type_of env sigma c) in
@@ -699,12 +745,18 @@ type hint_action =
| 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)) =
@@ -714,19 +766,10 @@ let cache_autohint (_,(local,name,hints)) =
| 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 (forward_subst_tactic, extern_subst_tactic) = Hook.make ()
- (* let subst_mps_or_ref subst cr = *)
- (* match cr with *)
- (* | IsConstr c -> let c' = subst_mps subst c in *)
- (* if c' == c then cr *)
- (* else IsConstr c' *)
- (* | IsGlobal r -> let r' = subst_global_reference subst r in *)
- (* if r' == r then cr *)
- (* else IsGlobal r' *)
- (* in *)
-
let subst_autohint (subst,(local,name,hintlist as obj)) =
let subst_key gr =
let (lab'', elab') = subst_global subst gr in
@@ -779,11 +822,14 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
if hintlist' == hintlist then obj else
(local,name,AddHints hintlist')
| RemoveHints grs ->
- let grs' = List.smartmap (fun x -> fst (subst_global subst x)) grs in
+ 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
@@ -835,6 +881,13 @@ let add_cuts l local dbnames =
(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
@@ -870,6 +923,7 @@ type hints_entry =
| 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
@@ -914,22 +968,19 @@ let interp_hints poly =
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 fr r =
+ let fref r =
let gr = global_with_alias r in
- let r' = evaluable_of_global_reference (Global.env()) gr in
Dumpglob.add_glob (loc_of_reference r) gr;
- r' in
+ 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 ->
- (* if poly then *)
- (* errorlabstrm "Hint" (Ppconstr.pr_constr_expr c ++ spc () ++ *)
- (* str" is a term and cannot be made a polymorphic hint," ++ *)
- (* str" only global references can be polymorphic hints.") *)
- (* else *) (PathAny, poly, f c)
+ | HintsConstr c -> (PathAny, poly, f c)
in
let fres (pri, b, r) =
let path, poly, gr = fi r in
@@ -942,6 +993,7 @@ let interp_hints poly =
| 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
@@ -968,6 +1020,7 @@ let add_hints local dbnames0 h =
| 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
@@ -1030,11 +1083,10 @@ let pr_hint_term cl =
let dbs = current_db () in
let valid_dbs =
let fn = try
- let hdc = head_constr_bound cl in
- let hd = head_of_constr_reference hdc in
+ let hdc = decompose_app_bound cl in
if occur_existential cl then
- Hint_db.map_all hd
- else Hint_db.map_auto (hd, cl)
+ 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
@@ -1063,11 +1115,16 @@ let pr_applicable_hint () =
(* 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 hintlist accu =
+ let fold head modes hintlist accu =
let goal_descr = match head with
| None -> str "For any goal"
- | Some head -> str "For " ++ pr_global head
+ | 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
@@ -1395,8 +1452,8 @@ let hintmap_of hdc concl =
match hdc with
| None -> Hint_db.map_none
| Some hdc ->
- if occur_existential concl then Hint_db.map_all hdc
- else Hint_db.map_auto (hdc,concl)
+ if occur_existential concl then Hint_db.map_existential hdc concl
+ else Hint_db.map_auto hdc concl
let exists_evaluable_reference env = function
| EvalConstRef _ -> true
@@ -1458,8 +1515,8 @@ and my_find_search_delta db_list local_db hdc concl =
match hdc with None -> Hint_db.map_none db
| Some hdc ->
if (Id.Pred.is_empty ids && Cpred.is_empty csts)
- then Hint_db.map_auto (hdc,concl) db
- else Hint_db.map_all hdc db
+ then Hint_db.map_auto hdc concl db
+ else Hint_db.map_existential hdc concl db
in auto_flags_of_state st, l
in List.map (fun x -> (Some flags,x)) l)
(local_db::db_list)
@@ -1489,8 +1546,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly}))
and trivial_resolve dbg mod_delta db_list local_db cl =
try
let head =
- try let hdconstr = head_constr_bound cl in
- Some (head_of_constr_reference hdconstr)
+ try let hdconstr = decompose_app_bound cl in
+ Some hdconstr
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
@@ -1543,8 +1600,8 @@ let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
let possible_resolve dbg mod_delta db_list local_db cl =
try
let head =
- try let hdconstr = head_constr_bound cl in
- Some (head_of_constr_reference hdconstr)
+ try let hdconstr = decompose_app_bound cl in
+ Some hdconstr
with Bound -> None
in
List.map (tac_of_hint dbg db_list local_db cl)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 3c916af73..5fde1d2de 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -73,13 +73,27 @@ module Hint_db :
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
- val map_auto : global_reference * constr -> 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 -> pri_auto_tactic list -> unit) -> t -> unit
+ 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
@@ -108,6 +122,7 @@ type hints_entry =
| 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
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 77101c70e..7de9330ba 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -151,12 +151,11 @@ let rec e_trivial_fail_db db_list local_db goal =
tclFIRST (List.map tclCOMPLETE tacl) goal
and e_my_find_search db_list local_db hdc complete sigma concl =
- let hdc = head_of_constr_reference hdc in
let prods, concl = decompose_prod_assum concl in
let nprods = List.length prods in
let freeze =
try
- let cl = Typeclasses.class_info hdc in
+ let cl = Typeclasses.class_info (fst hdc) in
if cl.cl_strict then
Evarutil.evars_of_term concl
else Evar.Set.empty
@@ -165,12 +164,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
let hintl =
List.map_append
(fun db ->
- if Hint_db.use_dn db then
- let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
- List.map (fun x -> (flags, x)) (Hint_db.map_auto (hdc,concl) db)
- else
- let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
- List.map (fun x -> (flags, x)) (Hint_db.map_all hdc db))
+ let tacs =
+ if Hint_db.use_dn db then (* Using dnet *)
+ Hint_db.map_eauto hdc concl db
+ else Hint_db.map_existential hdc concl db
+ in
+ let flags = auto_unif_flags freeze (Hint_db.transparent_state db) in
+ List.map (fun x -> (flags, x)) tacs)
(local_db::db_list)
in
let tac_of_hint =
@@ -198,13 +198,13 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
and e_trivial_resolve db_list local_db sigma concl =
try
e_my_find_search db_list local_db
- (head_constr_bound concl) true sigma concl
+ (decompose_app_bound concl) true sigma concl
with Bound | Not_found -> []
let e_possible_resolve db_list local_db sigma concl =
try
e_my_find_search db_list local_db
- (head_constr_bound concl) false sigma concl
+ (decompose_app_bound concl) false sigma concl
with Bound | Not_found -> []
let catchable = function
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 5676a3b58..7a4639967 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -141,19 +141,19 @@ let rec e_trivial_fail_db db_list local_db goal =
(Hint_db.add_list hintl local_db) g'))) ::
(List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
in
- tclFIRST (List.map tclCOMPLETE tacl) goal
+ tclFIRST (List.map tclCOMPLETE tacl) goal
and e_my_find_search db_list local_db hdc concl =
- let hdc = head_of_constr_reference hdc in
let hintl =
if occur_existential concl then
List.map_append (fun db ->
let flags = auto_flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
+ List.map (fun x -> flags, x) (Hint_db.map_existential hdc concl db)
+ (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)) (local_db::db_list)
else
List.map_append (fun db ->
let flags = auto_flags_of_state (Hint_db.transparent_state db) in
- List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+ List.map (fun x -> flags, x) (Hint_db.map_auto hdc concl db)) (local_db::db_list)
in
let tac_of_hint =
fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
@@ -177,13 +177,13 @@ and e_trivial_resolve db_list local_db gl =
try
priority
(e_my_find_search db_list local_db
- (head_constr_bound gl) gl)
+ (decompose_app_bound gl) gl)
with Bound | Not_found -> []
let e_possible_resolve db_list local_db gl =
try List.map snd
(e_my_find_search db_list local_db
- (head_constr_bound gl) gl)
+ (decompose_app_bound gl) gl)
with Bound | Not_found -> []
let find_first_goal gls =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 48bfeb86e..36a297c81 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -130,6 +130,18 @@ let head_constr_bound t =
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 p, Array.cons c args
+ | _ -> raise Bound
+
(******************************************)
(* Primitive tactics *)
(******************************************)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d6e648b9b..c076efb1f 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,12 +26,13 @@ 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
-exception Bound
-
(** {6 Primitive tactics. } *)
val introduction : Id.t -> tactic
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index fb9f8c218..db3b19af5 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -24,3 +24,24 @@ auto using (pair O).
Undo.
eauto using (pair O).
Qed.
+
+Create HintDb test discriminated.
+
+Parameter foo : forall x, x = x + 0.
+Hint Resolve foo : test.
+
+Variable C : nat -> Type -> Prop.
+
+Variable c_inst : C 0 nat.
+
+Hint Resolve c_inst : test.
+
+Hint Mode C - + : test.
+Hint Resolve c_inst : test2.
+Hint Mode C + + : test2.
+
+Goal exists n, C n nat.
+Proof.
+ eexists. Fail progress debug eauto with test2.
+ progress eauto with test.
+Qed.
diff --git a/test-suite/typeclasses/backtrack.v b/test-suite/typeclasses/backtrack.v
index 112112f0c..fff740edd 100644
--- a/test-suite/typeclasses/backtrack.v
+++ b/test-suite/typeclasses/backtrack.v
@@ -1,5 +1,3 @@
-Set Typeclasses Strict Resolution.
-
(* Set Typeclasses Unique Instances *)
(** This lets typeclass search assume that instance heads are unique,
so if one matches no other need to be tried,
@@ -14,6 +12,10 @@ Set Typeclasses Unique Instances.
(* Unique *)
Class D.
Class C (A : Type) := c : A.
+
+Hint Mode C +.
+Fail Definition test := c.
+
Unset Typeclasses Unique Instances.
Instance : B -> D -> C nat := fun _ _ => 0.
Instance : A -> D -> C nat := fun _ _ => 0.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 13:25:26 +0000