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

4 files changed, 96 insertions, 67 deletions

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