Ajout option Local à Hint, Hints et HintDestruct

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

4 files changed, 59 insertions, 37 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 638f6d727c..c7186e4123 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -278,7 +278,7 @@ let add_hint dbname hintlist =
     let db = Hint_db.add_list hintlist Hint_db.empty in
     searchtable_add (dbname,db)
 
-let cache_autohint (_,(name,hintlist)) = add_hint name hintlist
+let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist
 
 (*  let recalc_hints hintlist =
     let env = Global.env() and sigma = Evd.empty in
@@ -317,7 +317,7 @@ let forward_subst_tactic =
 
 let set_extern_subst_tactic f = forward_subst_tactic := f
 
-let subst_autohint (_,subst,(name,hintlist as obj)) = 
+let subst_autohint (_,subst,(local,name,hintlist as obj)) = 
   let trans_clenv clenv = Clenv.subst_clenv (fun _ a -> a) subst clenv in
   let trans_data data code = 	      
     { data with
@@ -359,14 +359,13 @@ let subst_autohint (_,subst,(name,hintlist as obj)) =
   in
   let hintlist' = list_smartmap subst_hint hintlist in
     if hintlist' == hintlist then obj else
-      (name,hintlist')
+      (local,name,hintlist')
 
-let classify_autohint (_,((name,hintlist) as obj)) =
-  match hintlist with
-      [] -> Dispose   
-    | _ -> Substitute obj
+let classify_autohint (_,((local,name,hintlist) as obj)) =
+  if local or hintlist = [] then Dispose else Substitute obj
 
-let export_autohint x = Some x
+let export_autohint ((local,name,hintlist) as obj) =
+  if local then None else Some obj
 
 let (inAutoHint,outAutoHint) =
   declare_object {(default_object "AUTOHINT") with
@@ -380,12 +379,12 @@ let (inAutoHint,outAutoHint) =
 (**************************************************************************)
 (*                     The "Hint" vernacular command                      *)
 (**************************************************************************)
-let add_resolves env sigma clist dbnames =
+let add_resolves env sigma clist local dbnames =
   List.iter 
     (fun dbname ->
        Lib.add_anonymous_leaf
 	 (inAutoHint
-	    (dbname,
+	    (local,dbname,
      	     List.flatten
 	       (List.map
 		  (fun (name,c) -> 
@@ -397,14 +396,14 @@ let add_resolves env sigma clist dbnames =
     dbnames
 
 
-let add_unfolds l dbnames =
+let add_unfolds l local dbnames =
   List.iter 
     (fun dbname -> Lib.add_anonymous_leaf 
-       (inAutoHint (dbname, List.map make_unfold l)))
+       (inAutoHint (local,dbname, List.map make_unfold l)))
     dbnames
 
 
-let add_extern name pri (patmetas,pat) tacast dbname =
+let add_extern name pri (patmetas,pat) tacast local dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
 (* TODO
@@ -417,16 +416,16 @@ let add_extern name pri (patmetas,pat) tacast dbname =
 	  (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound")
     | []  ->
 	Lib.add_anonymous_leaf
-	  (inAutoHint(dbname, [make_extern name pri pat tacast]))
+	  (inAutoHint(local,dbname, [make_extern name pri pat tacast]))
 
-let add_externs name pri pat tacast dbnames = 
-  List.iter (add_extern name pri pat tacast) dbnames
+let add_externs name pri pat tacast local dbnames = 
+  List.iter (add_extern name pri pat tacast local) dbnames
 
-let add_trivials env sigma l dbnames =
+let add_trivials env sigma l local dbnames =
   List.iter
     (fun dbname ->
        Lib.add_anonymous_leaf (
-	 inAutoHint(dbname, List.map (make_trivial env sigma) l)))
+	 inAutoHint(local,dbname, List.map (make_trivial env sigma) l)))
     dbnames
 
 let forward_intern_tac = 
@@ -434,7 +433,7 @@ let forward_intern_tac =
 
 let set_extern_intern_tac f = forward_intern_tac := f
 
-let add_hints dbnames h =
+let add_hints local dbnames h =
   let dbnames = if dbnames = [] then ["core"] else dbnames in match h with
   | HintsResolve lhints ->	
       let env = Global.env() and sigma = Evd.empty in
@@ -444,7 +443,7 @@ let add_hints dbnames h =
 	  | None -> id_of_global (reference_of_constr c)
 	  | Some n -> n in
 	(n,c) in
-      add_resolves env sigma (List.map f lhints) dbnames
+      add_resolves env sigma (List.map f lhints) local dbnames
   | HintsImmediate lhints ->
       let env = Global.env() and sigma = Evd.empty in
       let f (n,c) = 
@@ -453,7 +452,7 @@ let add_hints dbnames h =
 	  | None -> id_of_global (reference_of_constr c)
 	  | Some n -> n in
 	(n,c) in
-      add_trivials env sigma (List.map f lhints) dbnames
+      add_trivials env sigma (List.map f lhints) local dbnames
   | HintsUnfold lhints ->
       let f (n,locqid) =
 	let r = Nametab.global locqid in
@@ -461,18 +460,18 @@ let add_hints dbnames h =
 	  | None -> id_of_global r
 	  | Some n -> n in
 	(n,r) in
-      add_unfolds (List.map f lhints) dbnames
+      add_unfolds (List.map f lhints) local dbnames
   | HintsConstructors (hintname, qid) ->
       let env = Global.env() and sigma = Evd.empty in
       let isp = global_inductive qid in
       let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
       let lcons = list_tabulate (fun i -> mkConstruct (isp,i+1)) (Array.length consnames) in
       let lcons = List.map2 (fun id c -> (id,c)) (Array.to_list consnames) lcons in
-      add_resolves env sigma lcons dbnames
+      add_resolves env sigma lcons local dbnames
   | HintsExtern (hintname, pri, patcom, tacexp) ->
       let pat =	Constrintern.interp_constrpattern Evd.empty (Global.env()) patcom in
       let tacexp = !forward_intern_tac (fst pat) tacexp in
-      add_externs hintname pri pat tacexp dbnames
+      add_externs hintname pri pat tacexp local dbnames
 
 (**************************************************************************)
 (*                    Functions for printing the hints                    *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a8d8cf1df1..ef2571baa7 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -20,6 +20,7 @@ open Pattern
 open Environ
 open Evd
 open Libnames
+open Vernacexpr
 (*i*)
   
 type auto_tactic = 
@@ -61,7 +62,7 @@ type hint_db_table = Hint_db.t Stringmap.t ref
 
 type hint_db_name = string
 
-val add_hints : hint_db_name list -> Vernacexpr.hints -> unit
+val add_hints : locality_flag -> hint_db_name list -> hints -> unit
 
 val print_searchtable : unit -> unit
 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 313ddabcf1..252e302c2c 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -138,15 +138,25 @@ open Libnames
 type destructor_pattern = {
   d_typ: constr_pattern; 
   d_sort: constr_pattern }
-    
+
+let subst_destructor_pattern subst { d_typ = t; d_sort = s } =
+  { d_typ = subst_pattern subst t; d_sort = subst_pattern subst s }
+
 (* hypothesis patterns might need to do matching on the conclusion, too.
  * conclusion-patterns only need to do matching on the hypothesis *)
 type located_destructor_pattern =
-   (* discadable , pattern for hyp, pattern for concl *)
+   (* discardable, pattern for hyp, pattern for concl *)
    (bool * destructor_pattern * destructor_pattern,
    (* pattern for concl *)
    destructor_pattern) location
 
+let subst_located_destructor_pattern subst = function
+  | HypLocation (b,d,d') -> 
+      HypLocation
+        (b,subst_destructor_pattern subst d, subst_destructor_pattern subst d')
+  | ConclLocation d ->
+      ConclLocation (subst_destructor_pattern subst d)
+
 type destructor_data = {
   d_pat : located_destructor_pattern;
   d_pri : int;
@@ -186,9 +196,14 @@ let _ =
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
       Summary.init_function = init;
-      Summary.survive_section = true }
+      Summary.survive_section = false }
 
-let cache_dd (_,(na,dd)) =
+let forward_subst_tactic = 
+  ref (fun _ -> failwith "subst_tactic is not installed for DHyp")
+
+let set_extern_subst_tactic f = forward_subst_tactic := f
+
+let cache_dd (_,(_,na,dd)) =
   try 
     add (na,dd)
   with _ -> 
@@ -196,16 +211,23 @@ let cache_dd (_,(na,dd)) =
       (str"The code which adds destructor hints broke;" ++ spc () ++ 
 	 str"this is not supposed to happen")
 
-let export_dd x = Some x
+let classify_dd (_,(local,_,_ as o)) =
+  if local then Dispose else Substitute o
+
+let export_dd (local,_,_ as x) = if local then None else Some x
 
-type destructor_data_object = identifier * destructor_data
+let subst_dd (_,subst,(local,na,dd)) =
+  (local,na,
+  { d_pat = subst_located_destructor_pattern subst dd.d_pat;
+    d_pri = dd.d_pri; 
+    d_code = !forward_subst_tactic subst dd.d_code })
 
-let ((inDD : destructor_data_object->obj),
-     (outDD : obj->destructor_data_object)) =
+let (inDD,outDD) =
   declare_object {(default_object "DESTRUCT-HYP-CONCL-DATA") with
                     cache_function = cache_dd;
 		    open_function = (fun i o -> if i=1 then cache_dd o);
-                    (* TODO: substitution *)
+                    subst_function = subst_dd;
+		    classify_function = classify_dd;
                     export_function = export_dd }
 
 let forward_intern_tac = 
@@ -216,7 +238,7 @@ let set_extern_intern_tac f = forward_intern_tac := f
 let catch_all_sort_pattern = PMeta(Some (id_of_string "SORT"))
 let catch_all_type_pattern = PMeta(Some (id_of_string "TYPE"))
     
-let add_destructor_hint na loc pat pri code =
+let add_destructor_hint local na loc pat pri code =
   let code = !forward_intern_tac code in
   let code =
     begin match loc, code with
@@ -236,7 +258,7 @@ let add_destructor_hint na loc pat pri code =
     | ConclLocation () ->
 	ConclLocation({d_typ=pat;d_sort=catch_all_sort_pattern}) in
   Lib.add_anonymous_leaf
-    (inDD (na,{ d_pat = pat; d_pri=pri; d_code=code }))
+    (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))
 
 let match_dpat dp cls gls =
   let cltyp = clause_type cls gls in
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index b4ecfeac87..9a46136f98 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -28,5 +28,5 @@ val h_destructConcl : tactic
 val h_auto_tdb : int option -> tactic
 
 val add_destructor_hint :
-  identifier -> (bool,unit) Tacexpr.location ->
+  Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location ->
     Topconstr.constr_expr -> int -> raw_tactic_expr -> unit