From 135c872c4a507726a633cc4025d284933fbc6660 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 7 Sep 2008 18:06:41 +0000 Subject: Add the ability to declare [Hint Extern]'s with no pattern. This permits to create a database [relations] in [RelationClasses] with a single extern tactic in it that tries to apply [reflexivity] or [symmetry]. This is then automatically used in [auto with *] and repair backward compatibility. The previous commit broke some scripts which were using [intuition] to do (setoid) [reflexivity] or [symmetry]: this worked only by accident, because the hint database of typeclasses was used. Overrall, this also allows to put a bunch of always-applicable, related tactics in some database or to use [Hint Extern] but match only on hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11384 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/auto.ml | 129 ++++++++++++++++++++++++++++------------------ tactics/auto.mli | 25 +++++---- tactics/class_tactics.ml4 | 3 +- tactics/eauto.ml4 | 6 +-- 4 files changed, 96 insertions(+), 67 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index a5778d45d..58730d5d1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -59,6 +59,8 @@ type pri_auto_tactic = { code : auto_tactic (* the tactic to apply when the concl matches pat *) } +type hint_entry = global_reference option * pri_auto_tactic + let pri_ord {pri=pri1} {pri=pri2} = pri1 - pri2 let pri_order {pri=pri1} {pri=pri2} = pri1 <= pri2 @@ -121,14 +123,15 @@ module Hint_db = struct hintdb_state : Names.transparent_state; use_dn : bool; hintdb_map : search_entry Constr_map.t; - (* A list of unindexed entries starting with an unfoldable constant. *) - hintdb_transp : stored_data list + (* A list of unindexed entries starting with an unfoldable constant + or with no associated pattern. *) + hintdb_nopat : stored_data list } let empty st use_dn = { hintdb_state = st; use_dn = use_dn; hintdb_map = Constr_map.empty; - hintdb_transp = [] } + hintdb_nopat = [] } let find key db = try Constr_map.find key db.hintdb_map @@ -136,12 +139,12 @@ module Hint_db = struct let map_all k db = let (l,l',_) = find k db in - Sort.merge pri_order (db.hintdb_transp @ l) l' + Sort.merge pri_order (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 - Sort.merge pri_order db.hintdb_transp l' + Sort.merge pri_order db.hintdb_nopat l' let is_exact = function | Give_exact _ -> true @@ -160,26 +163,34 @@ module Hint_db = struct | EvalConstRef cst -> (ids, Cpred.add cst csts)), true | _ -> db.hintdb_state, false in - let dnst, db = + let dnst, db, k = if db.use_dn then - let db' = - if rebuild then rebuild_db st' db + let db', k' = + if rebuild then rebuild_db st' db, k else (* not an unfold *) - if is_transparent_gr st' k && not (List.mem v db.hintdb_transp) then - { db with hintdb_transp = v :: db.hintdb_transp } - else db + (match k with + | Some gr -> db, if is_transparent_gr st' gr then None else k + | None -> db, None) in - (Some st', db') - else None, db + (Some st', db', k') + else None, db, k in - let oval = find k db in let pat = if not db.use_dn && is_exact v.code then None else v.pat in - { db with hintdb_map = Constr_map.add k (add_tac pat v dnst oval) db.hintdb_map; - hintdb_state = st' } + match k with + | None -> + if not (List.mem v db.hintdb_nopat) then + { db with hintdb_nopat = v :: db.hintdb_nopat } + else db + | Some gr -> + let oval = find gr db in + { db with hintdb_map = Constr_map.add gr (add_tac pat v dnst oval) db.hintdb_map; + hintdb_state = st' } let add_list l db = List.fold_right add_one l db - let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db.hintdb_map + let iter f db = + f None db.hintdb_nopat; + Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map let transparent_state db = db.hintdb_state @@ -255,7 +266,7 @@ let make_exact_entry pri (c,cty) = let ce = mk_clenv_from dummy_goal (c,cty) in let c' = clenv_type ce in let pat = Pattern.pattern_of_constr c' in - (head_of_constr_reference (List.hd (head_constr cty)), + (Some (head_of_constr_reference (List.hd (head_constr cty))), { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c }) let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = @@ -269,7 +280,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = with BoundPattern -> failwith "make_apply_entry") in let nmiss = List.length (clenv_missing ce) in if nmiss = 0 then - (hd, + (Some hd, { pri = (match pri with None -> nb_hyp cty | Some p -> p); pat = Some pat; code = Res_pf(c,{ce with env=empty_env}) }) @@ -278,7 +289,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) = if verbose then warn (str "the hint: eapply " ++ pr_lconstr c ++ str " will only be used by eauto"); - (hd, + (Some hd, { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p); pat = Some pat; code = ERes_pf(c,{ce with env=empty_env}) }) @@ -314,23 +325,23 @@ let make_resolve_hyp env sigma (hname,_,htyp) = (* REM : in most cases hintname = id *) let make_unfold (ref, eref) = - (ref, + (Some ref, { pri = 4; pat = None; code = Unfold_nth eref }) let make_extern pri pat tacast = - let hdconstr = try_head_pattern pat in + let hdconstr = Option.map try_head_pattern pat in (hdconstr, { pri=pri; - pat = Some pat; + pat = pat; code= Extern tacast }) let make_trivial env sigma c = let t = hnf_constr env sigma (type_of env sigma c) in let hd = head_of_constr_reference (List.hd (head_constr t)) in let ce = mk_clenv_from dummy_goal (c,t) in - (hd, { pri=1; + (Some hd, { pri=1; pat = Some (Pattern.pattern_of_constr (clenv_type ce)); code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) }) @@ -364,7 +375,7 @@ let add_transparency dbname grs b = type hint_action = | CreateDB of bool * transparent_state | AddTransparency of evaluable_global_reference list * bool - | AddTactic of (global_reference * pri_auto_tactic) list + | AddTactic of (global_reference option * pri_auto_tactic) list let cache_autohint (_,(local,name,hints)) = match hints with @@ -385,11 +396,15 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = code = code ; } in - let subst_hint (lab,data as hint) = - let lab',elab' = subst_global subst lab in - let lab' = - try head_of_constr_reference (List.hd (head_constr_bound elab' [])) - with Tactics.Bound -> lab' in + let subst_key gr = + let (lab'', elab') = subst_global subst gr in + let gr' = + (try head_of_constr_reference (List.hd (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 data' = match data.code with | Res_pf (c, clenv) -> let c' = subst_mps subst c in @@ -417,8 +432,8 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = if tac==tac' then data else trans_data data (Extern tac') in - if lab' == lab && data' == data then hint else - (lab',data') + if k' == k && data' == data then hint else + (k',data') in match hintlist with | CreateDB _ -> obj @@ -474,17 +489,22 @@ let add_transparency l b local dbnames = (inAutoHint (local,dbname, AddTransparency (l, b)))) dbnames -let add_extern pri (patmetas,pat) tacast local dbname = +let add_extern pri pat tacast local dbname = (* We check that all metas that appear in tacast have at least one occurence in the left pattern pat *) let tacmetas = [] in - match (list_subtract tacmetas patmetas) with - | i::_ -> - errorlabstrm "add_extern" - (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") - | [] -> + match pat with + | Some (patmetas,pat) -> + (match (list_subtract tacmetas patmetas) with + | i::_ -> + errorlabstrm "add_extern" + (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") + | [] -> + Lib.add_anonymous_leaf + (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast]))) + | None -> Lib.add_anonymous_leaf - (inAutoHint(local,dbname, AddTactic [make_extern pri pat tacast])) + (inAutoHint(local,dbname, AddTactic [make_extern pri None tacast])) let add_externs pri pat tacast local dbnames = List.iter (add_extern pri pat tacast local) dbnames @@ -548,8 +568,8 @@ let add_hints local dbnames0 h = add_resolves env sigma lcons local dbnames in List.iter add_one lqid | HintsExtern (pri, patcom, tacexp) -> - let pat = Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in - let tacexp = !forward_intern_tac (fst pat) tacexp in + let pat = Option.map (Constrintern.interp_constrpattern Evd.empty (Global.env())) patcom in + let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in add_externs pri pat tacexp local dbnames | HintsDestruct(na,pri,loc,pat,code) -> if dbnames0<>[] then @@ -648,9 +668,15 @@ let print_hint_db db = str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ())); Hint_db.iter (fun head hintlist -> - msg (hov 0 - (str "For " ++ pr_global head ++ str " -> " ++ - fmt_hint_list hintlist))) + match head with + | Some head -> + msg (hov 0 + (str "For " ++ pr_global head ++ str " -> " ++ + fmt_hint_list hintlist)) + | None -> + msg (hov 0 + (str "For any goal -> " ++ + fmt_hint_list hintlist))) db let print_hint_db_by_name dbname = @@ -728,10 +754,13 @@ let forward_interp_tactic = let set_extern_interp f = forward_interp_tactic := f let conclPattern concl pat tac gl = - let constr_bindings = - try matches pat concl - with PatternMatchingFailure -> error "conclPattern" in - !forward_interp_tactic constr_bindings tac gl + let constr_bindings = + match pat with + | None -> [] + | Some pat -> + try matches pat concl + with PatternMatchingFailure -> error "conclPattern" in + !forward_interp_tactic constr_bindings tac gl (**************************************************************************) (* The Trivial tactic *) @@ -779,7 +808,7 @@ and my_find_search_nodelta db_list local_db hdc concl = (trivial_fail_db false db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> - conclPattern concl (Option.get p) tacast)) + conclPattern concl p tacast)) tacl and my_find_search mod_delta = @@ -828,7 +857,7 @@ and my_find_search_delta db_list local_db hdc concl = (trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] | Extern tacast -> - conclPattern concl (Option.get p) tacast)) + conclPattern concl p tacast)) tacl and trivial_resolve mod_delta db_list local_db cl = diff --git a/tactics/auto.mli b/tactics/auto.mli index b35f98ec1..0eaa35872 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -44,6 +44,10 @@ type stored_data = pri_auto_tactic type search_entry = stored_data list * stored_data list * stored_data Btermdn.t +(* The head may not be bound. *) + +type hint_entry = global_reference option * pri_auto_tactic + module Hint_db : sig type t @@ -51,9 +55,9 @@ module Hint_db : val find : global_reference -> t -> search_entry val map_all : global_reference -> t -> pri_auto_tactic list val map_auto : global_reference * constr -> t -> pri_auto_tactic list - val add_one : global_reference * pri_auto_tactic -> t -> t - val add_list : (global_reference * pri_auto_tactic) list -> t -> t - val iter : (global_reference -> stored_data list -> unit) -> t -> unit + val add_one : hint_entry -> t -> t + val add_list : (hint_entry) list -> t -> t + val iter : (global_reference option -> stored_data list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state @@ -91,7 +95,7 @@ val print_hint_db_by_name : hint_db_name -> unit [c] is the term given as an exact proof to solve the goal; [ctyp] is the type of [c]. *) -val make_exact_entry : int option -> constr * constr -> global_reference * pri_auto_tactic +val make_exact_entry : int option -> constr * constr -> hint_entry (* [make_apply_entry (eapply,verbose) pri (c,cty)]. [eapply] is true if this hint will be used only with EApply; @@ -102,7 +106,7 @@ val make_exact_entry : int option -> constr * constr -> global_reference * pri_a val make_apply_entry : env -> evar_map -> bool * bool * bool -> int option -> constr * constr - -> global_reference * pri_auto_tactic + -> hint_entry (* A constr which is Hint'ed will be: (1) used as an Exact, if it does not start with a product @@ -113,7 +117,7 @@ val make_apply_entry : val make_resolves : env -> evar_map -> bool * bool * bool -> int option -> constr -> - (global_reference * pri_auto_tactic) list + hint_entry list (* [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; @@ -121,14 +125,13 @@ val make_resolves : If the hyp cannot be used as a Hint, the empty list is returned. *) val make_resolve_hyp : - env -> evar_map -> named_declaration -> - (global_reference * pri_auto_tactic) list + env -> evar_map -> named_declaration -> hint_entry list (* [make_extern pri pattern tactic_expr] *) val make_extern : - int -> constr_pattern -> Tacexpr.glob_tactic_expr - -> global_reference * pri_auto_tactic + int -> constr_pattern option -> Tacexpr.glob_tactic_expr + -> hint_entry val set_extern_interp : (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit @@ -163,7 +166,7 @@ val unify_resolve : Unification.unify_flags -> (constr * clausenv) -> tactic [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the right values to build a tactic *) -val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tactic +val conclPattern : constr -> constr_pattern option -> Tacexpr.glob_tactic_expr -> tactic (* The Auto tactic *) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 3cdf050c4..e803e8dcb 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -143,8 +143,7 @@ and e_my_find_search db_list local_db hdc concl = tclTHEN (unify_e_resolve flags (term,cl)) (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> conclPattern concl - (Option.get p) tacast + | Extern tacast -> conclPattern concl p tacast in (tac,b,fmt_autotactic t) in diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index eae6f5632..dcff75331 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -140,8 +140,7 @@ and e_my_find_search_nodelta db_list local_db hdc concl = tclTHEN (unify_e_resolve_nodelta (term,cl)) (e_trivial_fail_db false db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> conclPattern concl - (Option.get p) tacast + | Extern tacast -> conclPattern concl p tacast in (tac,fmt_autotactic t)) (*i @@ -179,8 +178,7 @@ and e_my_find_search_delta db_list local_db hdc concl = tclTHEN (unify_e_resolve st (term,cl)) (e_trivial_fail_db true db_list local_db) | Unfold_nth c -> unfold_in_concl [all_occurrences,c] - | Extern tacast -> conclPattern concl - (Option.get p) tacast + | Extern tacast -> conclPattern concl p tacast in (tac,fmt_autotactic t)) (*i -- cgit v1.2.3