- Fix treatment of globality flag for typeclass instance hints (they

  were all declared as global).
- Add possibility to remove hints (Resolve or Immediate only) based on
  the name of the lemma.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13842 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 101 insertions, 35 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8a05736ca..f4985f40e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -57,6 +57,7 @@ type auto_tactic =
 type pri_auto_tactic = {
   pri  : int;            (* A number between 0 and 4, 4 = lower priority *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
+  name  : global_reference option; (* A potential name to refer to the hint *) 
   code : auto_tactic     (* the tactic to apply when the concl matches pat *)
 }
 
@@ -213,6 +214,20 @@ module Hint_db = struct
 
   let add_list l db = List.fold_right add_one l db
 
+  let remove_sdl p sdl = list_smartfilter p sdl 
+  let remove_he st p (sl1, sl2, dn 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)
+
+  let remove_list grs db =
+    let filter h = match h.name with None -> true | Some gr -> not (List.mem gr grs) 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 snd db.hintdb_nopat);
     Constr_map.iter (fun k (l,l',_) -> f (Some k) (l@l')) db.hintdb_map
@@ -280,7 +295,9 @@ let try_head_pattern c =
 
 let dummy_goal = Goal.V82.dummy_goal
 
-let make_exact_entry sigma pri (c,cty) =
+let name_of_constr c = try Some (global_of_constr c) with Not_found -> None
+
+let make_exact_entry sigma pri ?name (c,cty) =
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
@@ -293,9 +310,10 @@ let make_exact_entry sigma pri (c,cty) =
           (Some hd,
 	  { pri = (match pri with None -> 0 | Some p -> p);
 	    pat = Some pat;
+	    name = name;
 	    code = Give_exact c })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
+let make_apply_entry env sigma (eapply,hnf,verbose) pri ?name (c,cty) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
     match kind_of_term cty with
     | Prod _ ->
@@ -310,6 +328,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
 	  (Some hd,
           { pri = (match pri with None -> nb_hyp cty | Some p -> p);
             pat = Some pat;
+	    name = name;
             code = Res_pf(c,{ce with env=empty_env}) })
 	else begin
 	  if not eapply then failwith "make_apply_entry";
@@ -319,6 +338,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
           (Some hd,
             { pri = (match pri with None -> nb_hyp cty + nmiss | Some p -> p);
               pat = Some pat;
+	      name = name;
               code = ERes_pf(c,{ce with env=empty_env}) })
         end
     | _ -> failwith "make_apply_entry"
@@ -327,12 +347,12 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
    c is a constr
    cty is the type of constr *)
 
-let make_resolves env sigma flags pri c =
+let make_resolves env sigma flags pri ?name c =
   let cty = type_of env sigma c in
   let ents =
     map_succeed
       (fun f -> f (c,cty))
-      [make_exact_entry sigma pri; make_apply_entry env sigma flags pri]
+      [make_exact_entry sigma pri ?name; make_apply_entry env sigma flags pri ?name]
   in
   if ents = [] then
     errorlabstrm "Hint"
@@ -344,7 +364,7 @@ let make_resolves env sigma flags pri c =
 (* 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
+    [make_apply_entry env sigma (true, true, false) None ~name:(VarRef hname)
        (mkVar hname, htyp)]
   with
     | Failure _ -> []
@@ -352,24 +372,28 @@ let make_resolve_hyp env sigma (hname,_,htyp) =
 
 (* REM : in most cases hintname = id *)
 let make_unfold eref =
-  (Some (global_of_evaluable_reference eref),
+  let g = global_of_evaluable_reference eref in
+  (Some g,
    { pri = 4;
      pat = None;
+     name = Some g;
      code = Unfold_nth eref })
 
 let make_extern pri pat tacast =
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
-   { pri=pri;
+   { pri = pri;
      pat = pat;
-     code= Extern tacast })
+     name = None;
+     code = Extern tacast })
 
-let make_trivial env sigma c =
+let make_trivial env sigma ?name c =
   let t = hnf_constr env sigma (type_of env sigma c) in
   let hd = head_of_constr_reference (fst (head_constr t)) in
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
          pat = Some (snd (Pattern.pattern_of_constr sigma (clenv_type ce)));
+	 name = name;
          code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
 
 open Vernacexpr
@@ -401,15 +425,22 @@ let add_transparency dbname grs b =
       st grs
   in searchtable_add (dbname, Hint_db.set_transparent_state db st')
 
+let remove_hints dbname hintlist 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
-		   | AddTactic of (global_reference option * pri_auto_tactic) list
+		   | AddHints of (global_reference option * pri_auto_tactic) list
+		   | RemoveHints of global_reference list
 
 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
-  | AddTactic hints -> add_hint name hints
+  | AddHints hints -> add_hint name hints
+  | RemoveHints grs -> remove_hints name hints grs
 
 let forward_subst_tactic =
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
@@ -482,13 +513,17 @@ let subst_autohint (subst,(local,name,hintlist as 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))
-    | AddTactic hintlist ->
+    | AddHints hintlist ->
 	let hintlist' = list_smartmap subst_hint hintlist in
 	  if hintlist' == hintlist then obj else
-	    (local,name,AddTactic hintlist')
+	    (local,name,AddHints hintlist')
+    | RemoveHints grs ->
+	let grs' = list_smartmap (fun x -> fst (subst_global subst x)) grs in
+	  if grs==grs' then obj else (local, name, RemoveHints grs')
+
 
 let classify_autohint ((local,name,hintlist) as obj) =
-  if local or hintlist = (AddTactic []) then Dispose else Substitute obj
+  if local or hintlist = (AddHints []) then Dispose else Substitute obj
 
 let inAutoHint =
   declare_object {(default_object "AUTOHINT") with
@@ -501,6 +536,13 @@ let inAutoHint =
 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 dbnames = [] then ["core"] else dbnames in
+    List.iter
+      (fun dbname ->
+	 Lib.add_anonymous_leaf (inAutoHint(local, dbname, RemoveHints grs)))
+      dbnames
+
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
@@ -509,16 +551,16 @@ let add_resolves env sigma clist local dbnames =
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
-	    (local,dbname, AddTactic
-     	      (List.flatten (List.map (fun (x, hnf, y) ->
-		make_resolves env sigma (true,hnf,Flags.is_verbose()) x y) clist)))))
+	    (local,dbname, AddHints
+     	      (List.flatten (List.map (fun (x, hnf, name, y) ->
+		make_resolves env sigma (true,hnf,Flags.is_verbose()) x ?name y) clist)))))
     dbnames
 
 
 let add_unfolds l local dbnames =
   List.iter
     (fun dbname -> Lib.add_anonymous_leaf
-       (inAutoHint (local,dbname, AddTactic (List.map make_unfold l))))
+       (inAutoHint (local,dbname, AddHints (List.map make_unfold l))))
     dbnames
 
 let add_transparency l b local dbnames =
@@ -539,10 +581,10 @@ let add_extern pri pat tacast local dbname =
 	      (str "The meta-variable ?" ++ Ppconstr.pr_patvar i ++ str" is not bound.")
 	| []  ->
 	    Lib.add_anonymous_leaf
-	      (inAutoHint(local,dbname, AddTactic [make_extern pri (Some pat) tacast])))
+	      (inAutoHint(local,dbname, AddHints [make_extern pri (Some pat) tacast])))
     | None ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(local,dbname, AddTactic [make_extern pri None tacast]))
+	  (inAutoHint(local,dbname, AddHints [make_extern pri None tacast]))
 
 let add_externs pri pat tacast local dbnames =
   List.iter (add_extern pri pat tacast local) dbnames
@@ -551,7 +593,7 @@ let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(local,dbname, AddTactic (List.map (make_trivial env sigma) l))))
+	 inAutoHint(local,dbname, AddHints (List.map (fun (name, c) -> make_trivial env sigma ?name c) l))))
     dbnames
 
 let forward_intern_tac =
@@ -560,8 +602,8 @@ let forward_intern_tac =
 let set_extern_intern_tac f = forward_intern_tac := f
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * constr) list
-  | HintsImmediateEntry of constr list
+  | HintsResolveEntry of (int option * bool * global_reference option * constr) list
+  | HintsImmediateEntry of (global_reference option * constr) list
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -602,6 +644,11 @@ let prepare_hint env (sigma,c) =
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   iter c
 
+let name_of_constr_expr c =
+  match c with
+  | Topconstr.CRef r -> (try Some (global r) with _ -> None)
+  | _ -> None 
+      
 let interp_hints h =
   let f c =
     let evd,c = Constrintern.interp_open_constr Evd.empty (Global.env()) c in
@@ -613,17 +660,20 @@ let interp_hints h =
     let r' = evaluable_of_global_reference (Global.env()) gr in
     Dumpglob.add_glob (loc_of_reference r) gr;
     r' in
+  let fres (o, b, c) = (o, b, name_of_constr_expr c, f c) in
+  let fi c = name_of_constr_expr c, f c in
   let fp = Constrintern.intern_constr_pattern Evd.empty (Global.env()) in
   match h with
-  | HintsResolve lhints -> HintsResolveEntry (List.map (on_pi3 f) lhints)
-  | HintsImmediate lhints -> HintsImmediateEntry (List.map f lhints)
+  | 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)
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
         let ind = global_inductive_with_alias qid in
-        list_tabulate (fun i -> None, true, mkConstruct (ind,i+1))
+        list_tabulate (fun i -> let c = (ind,i+1) in
+			 None, true, Some (ConstructRef c), mkConstruct c)
 	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 73249d43a..cd8808bff 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -35,6 +35,7 @@ open Glob_term
 type pri_auto_tactic = {
   pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
   pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
+  name  : global_reference option; (** A potential name to refer to the hint *) 
   code  : auto_tactic;    (** the tactic to apply when the concl matches pat *)
 }
 
@@ -56,6 +57,8 @@ module Hint_db :
     val map_auto : global_reference * 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 -> stored_data list -> unit) -> t -> unit
 
     val use_dn : t -> bool
@@ -70,8 +73,8 @@ type hint_db_name = string
 type hint_db = Hint_db.t
 
 type hints_entry =
-  | HintsResolveEntry of (int option * bool * constr) list
-  | HintsImmediateEntry of constr list
+  | HintsResolveEntry of (int option * bool * global_reference option * constr) list
+  | HintsImmediateEntry of (global_reference option * constr) list
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
@@ -90,6 +93,8 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
 
 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 -> hint_db_name list
 
 val interp_hints : hints_expr -> hints_entry
@@ -112,7 +117,7 @@ val print_hint_db : Hint_db.t -> unit
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)
 
-val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
+val make_exact_entry : evar_map -> int option -> ?name:global_reference -> constr * constr -> hint_entry
 
 (** [make_apply_entry (eapply,hnf,verbose) pri (c,cty)].
    [eapply] is true if this hint will be used only with EApply;
@@ -122,8 +127,8 @@ val make_exact_entry : evar_map -> int option -> constr * constr -> hint_entry
    [cty] is the type of [c]. *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> int option -> constr * constr
-      -> hint_entry
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> 
+  constr * constr -> hint_entry
 
 (** A constr which is Hint'ed will be:
    - (1) used as an Exact, if it does not start with a product
@@ -133,8 +138,8 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> int option -> constr ->
-      hint_entry list
+  env -> evar_map -> bool * bool * bool -> int option -> ?name:global_reference -> 
+  constr -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 7b2bf08cb..bbeb9425e 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -187,6 +187,17 @@ END
 
 open Autorewrite
 
+let pr_orient _prc _prlc _prt = function
+  | true -> Pp.mt ()
+  | false -> Pp.str " <-"
+
+let pr_orient_string _prc _prlc _prt (orient, s) =
+  pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s
+
+ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_string
+| [ orient(r) preident(i) ] -> [ r, i ]
+END
+
 TACTIC EXTEND autorewrite
 | [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] ->
     [ auto_multi_rewrite  l (glob_in_arg_hyp_to_clause  cl) ]
@@ -275,7 +286,7 @@ let project_hint pri l2r c =
   let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
-  (pri,true,c)
+  (pri,true,None,c)
 
 let add_hints_iff l2r lc n bl =
   Auto.add_hints true bl
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 89a8a5389..127a61db5 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1342,7 +1342,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance binders instance fields =
-  new_instance binders instance (CRecord (dummy_loc,None,fields)) ~generalize:false None
+  new_instance binders instance (CRecord (dummy_loc,None,fields)) ~global:true ~generalize:false None
 
 let declare_instance_refl binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"