Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl

 No grammar entries for these tactics since coq 8.0

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

6 files changed, 2 insertions, 509 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c650565c0..cfef521c8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -787,8 +787,6 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
       int * (patvar list * constr_pattern) option * glob_tactic_expr
-  | HintsDestructEntry of identifier * int * (bool,unit) location *
-      (patvar list * constr_pattern) * glob_tactic_expr
 
 let h = id_of_string "H"
 
@@ -859,9 +857,6 @@ let interp_hints h =
       let pat =	Option.map fp patcom in
       let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
       HintsExternEntry (pri, pat, tacexp)
-  | HintsDestruct(na,pri,loc,pat,code) ->
-      let (l,_ as pat) = fp pat in
-      HintsDestructEntry (na,pri,loc,pat,!forward_intern_tac l code)
 
 let add_hints local dbnames0 h =
   if List.mem "nocore" dbnames0 then
@@ -877,10 +872,6 @@ let add_hints local dbnames0 h =
       add_transparency lhints b local dbnames
   | HintsExternEntry (pri, pat, tacexp) ->
       add_externs pri pat tacexp local dbnames
-  | HintsDestructEntry (na,pri,loc,pat,code) ->
-      if dbnames0<>[] then
-        warn (str"Database selection not implemented for destruct hints");
-      Dhyp.add_destructor_hint local na loc pat pri code
 
 (**************************************************************************)
 (*                    Functions for printing the hints                    *)
@@ -1392,87 +1383,3 @@ let default_dauto = dauto (None,None) []
 let h_dauto (n,p) lems =
   Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map snd lems))
     (dauto (n,p) lems)
-
-(***************************************)
-(*** A new formulation of Auto *********)
-(***************************************)
-
-let make_resolve_any_hyp env sigma (id,_,ty) =
-  let ents =
-    map_succeed
-      (fun f -> f (mkVar id,ty))
-      [make_exact_entry sigma None; make_apply_entry env sigma (true,true,false) None]
-  in
-  ents
-
-type autoArguments =
-  | UsingTDB
-  | Destructing
-
-let compileAutoArg contac = function
-  | Destructing ->
-      (function g ->
-         let ctx = pf_hyps g in
-	 tclFIRST
-           (List.map
-              (fun (id,_,typ) ->
-                let cl = (strip_prod_assum typ) in
-                 if Hipattern.is_conjunction cl
-		 then
-		   tclTHENSEQ [simplest_elim (mkVar id); clear [id]; contac]
-                 else
-		   tclFAIL 0 (pr_id id ++ str" is not a conjunction"))
-	     ctx) g)
-  | UsingTDB ->
-      (tclTHEN
-         (Tacticals.tryAllHypsAndConcl
-            (function
-               | Some id -> Dhyp.h_destructHyp false id
-               | None    -> Dhyp.h_destructConcl))
-         contac)
-
-let compileAutoArgList contac = List.map (compileAutoArg contac)
-
-let rec super_search n db_list local_db argl gl =
-  if n = 0 then error "BOUND 2";
-  tclFIRST
-    (assumption
-     ::
-     tclTHEN intro
-        (fun g ->
-	   let hintl = pf_apply make_resolve_any_hyp g (pf_last_hyp g) in
-	   super_search n db_list (Hint_db.add_list hintl local_db)
-	     argl g)
-     ::
-     List.map (fun ntac ->
-            tclTHEN ntac
-              (super_search (n-1) db_list local_db argl))
-         (possible_resolve false db_list local_db (pf_concl gl))
-      @
-      compileAutoArgList (super_search (n-1) db_list local_db argl) argl) gl
-
-let search_superauto n to_add argl g =
-  let sigma =
-    List.fold_right
-      (fun (id,c) -> add_named_decl (id, None, pf_type_of g c))
-      to_add empty_named_context in
-  let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
-  let db = Hint_db.add_list db0 (make_local_hint_db false [] g) in
-  super_search n [Hintdbmap.find "core" !searchtable] db argl g
-
-let superauto n to_add argl  =
-  tclTRY (tclCOMPLETE (search_superauto n to_add argl))
-
-let interp_to_add gl r =
-  let r = locate_global_with_alias (qualid_of_reference r) in
-  let id = basename_of_global r in
-  (next_ident_away id (pf_ids_of_hyps gl), constr_of_global r)
-
-let gen_superauto nopt l a b gl =
-  let n = match nopt with Some n -> n | None -> !default_search_depth in
-  let al = (if a then [Destructing] else [])@(if b then [UsingTDB] else []) in
-  superauto n (List.map (interp_to_add gl) l) al gl
-
-let h_superauto no l a b =
-  Refiner.abstract_tactic (TacSuperAuto (no,l,a,b)) (gen_superauto no l a b)
-
diff --git a/tactics/auto.mli b/tactics/auto.mli
index bd425c1de..95de089e0 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -103,8 +103,6 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsExternEntry of
       int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
-  | HintsDestructEntry of identifier * int * (bool,unit) Tacexpr.location *
-      (patvar list * constr_pattern) * Tacexpr.glob_tactic_expr
 
 val searchtable_map : hint_db_name -> hint_db
 
@@ -255,7 +253,7 @@ val h_trivial : open_constr list -> hint_db_name list option -> tactic
 
 val pr_autotactic : 'a auto_tactic -> Pp.std_ppcmds
 
-(** {6 The following is not yet up to date -- Papageno. } *)
+(** Destructing Auto *)
 
 (** DAuto *)
 val dauto : int option * int option -> open_constr list -> tactic
@@ -264,16 +262,6 @@ val default_dauto : tactic
 
 val h_dauto : int option * int option -> open_constr list -> tactic
 
-(** SuperAuto *)
-
-type autoArguments =
-  | UsingTDB
-  | Destructing
-
-(*
-val superauto : int -> (identifier * constr) list -> autoArguments list -> tactic
-*)
-
-val h_superauto : int option -> reference list -> bool -> bool -> tactic
+(** Hook for changing the initialization of auto *)
 
 val add_auto_init : (unit -> unit) -> unit
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
deleted file mode 100644
index e7c4e0676..000000000
--- a/tactics/dhyp.ml
+++ /dev/null
@@ -1,360 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Chet's comments about this tactic :
-
- Programmable destruction of hypotheses and conclusions.
-
-   The idea here is that we are going to store patterns.  These
-   patterns look like:
-
-   TYP=<pattern>
-   SORT=<pattern>
-
-   and from these patterns, we will be able to decide which tactic to
-   execute.
-
-   For hypotheses, we have a vector of 4 patterns:
-
-   HYP[TYP] HYP[SORT] CONCL[TYP] CONCL[SORT]
-
-   and for conclusions, we have 2:
-
-   CONCL[TYP] CONCL[SORT]
-
-   If the user doesn't supply some of these, they are just replaced
-   with empties.
-
-   The process of matching goes like this:
-
-   We use a discrimination net to look for matches between the pattern
-   for HYP[TOP] (CONCL[TOP]) and the type of the chosen hypothesis.
-   Then, we use this to look for the right tactic to apply, by
-   matching the rest of the slots.  Each match is tried, and if there
-   is more than one, this fact is reported, and the one with the
-   lowest priority is taken.  The priority is a parameter of the
-   tactic input.
-
-   The tactic input is an expression to hand to the
-   tactic-interpreter, and its priority.
-
-   For most tactics, the priority should be the number of subgoals
-   generated.
-
-   Matching is compatible with second-order matching of sopattern.
-
-   SYNTAX:
-
-   Hint DHyp <hyp-pattern> pri <tac-pattern>.
-
-   and
-
-   Hint DConcl <concl-pattern> pri <tac-pattern>.
-
-   The bindings at the end allow us to transfer information from the
-   patterns on terms into the patterns on tactics in a safe way - we
-   will perform second-order normalization and conversion to an AST
-   before substitution into the tactic-expression.
-
-   WARNING: The binding mechanism is NOT intended to facilitate the
-   transfer of large amounts of information from the terms to the
-   tactic.  This should be done in a special-purpose tactic.
-
- *)
-
-(*
-
-Example : The tactic "if there is a hypothesis saying that the
-successor of some number is smaller than zero, then invert such
-hypothesis" is defined in this way:
-
-Require DHyp.
-Hint Destruct Hypothesis less_than_zero (le (S ?) O) 1
-  (:tactic:<Inversion $0>).
-
-Then, the tactic is used like this:
-
-Goal (le (S O) O) -> False.
-Intro H.
-DHyp  H.
-Qed.
-
-The name "$0" refers to the matching hypothesis --in this case the
-hypothesis H.
-
-Similarly for the conclusion :
-
-Hint Destruct Conclusion equal_zero  (? = ?) 1 (:tactic:<Reflexivity>).
-
-Goal (plus O O)=O.
-DConcl.
-Qed.
-
-The "Discardable" option clears the hypothesis after using it.
-
-Require DHyp.
-Hint Destruct  Discardable Hypothesis less_than_zero (le (S ?) O) 1
-  (:tactic:<Inversion $0>).
-
-Goal (n:nat)(le (S n) O) -> False.
-Intros n H.
-DHyp  H.
-Qed.
--- Eduardo (9/3/97 )
-
-*)
-
-open Pp
-open Errors
-open Util
-open Names
-open Term
-open Environ
-open Reduction
-open Proof_type
-open Glob_term
-open Tacmach
-open Refiner
-open Tactics
-open Clenv
-open Tactics
-open Tacticals
-open Libobject
-open Library
-open Pattern
-open Matching
-open Pcoq
-open Tacexpr
-open Termops
-open Libnames
-
-(* two patterns - one for the type, and one for the type of the type *)
-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 =
-   (* 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;
-  d_code : identifier option * glob_tactic_expr (* should be of phylum tactic *)
-}
-
-module Dest_data = struct 
-  type t = destructor_data
-  let compare = Pervasives.compare
-    end
-
-module Nbterm_net = Nbtermdn.Make(Dest_data)
-
-type t = identifier Nbterm_net.t
-type frozen_t = identifier Nbterm_net.frozen_t
-
-let tactab = (Nbterm_net.create () : t)
-
-let lookup pat = Nbterm_net.lookup tactab pat
-
-
-let init () = Nbterm_net.empty tactab
-
-let freeze () = Nbterm_net.freeze tactab
-let unfreeze fs = Nbterm_net.unfreeze fs tactab
-
-let add (na,dd) =
-  let pat = match dd.d_pat with
-    | HypLocation(_,p,_) -> p.d_typ
-    | ConclLocation p -> p.d_typ
-  in
-  if Nbterm_net.in_dn tactab na then begin
-    msgnl (str "Warning [Overriding Destructor Entry " ++
-             str (string_of_id na) ++ str"]");
-    Nbterm_net.remap tactab na (pat,dd)
-  end else
-    Nbterm_net.add tactab (na,(pat,dd))
-
-let _ =
-  Summary.declare_summary "destruct-hyp-concl"
-    { Summary.freeze_function = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function = init }
-
-let forward_subst_tactic =
-  ref (fun _ -> failwith "subst_tactic is not installed for DHyp")
-
-let cache_dd (_,(_,na,dd)) =
-  try
-    add (na,dd)
-  with _ ->
-    anomalylabstrm "Dhyp.add"
-      (str"The code which adds destructor hints broke;" ++ spc () ++
-	 str"this is not supposed to happen")
-
-let classify_dd (local,_,_ as o) =
-  if local then Dispose else Substitute o
-
-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 : bool * identifier * destructor_data -> obj =
-  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);
-                    subst_function = subst_dd;
-		    classify_function = classify_dd }
-
-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 local na loc (_,pat) pri code =
-  let code =
-    begin match loc, code with
-      | HypLocation _, TacFun ([id],body) -> (id,body)
-      | ConclLocation _, _ -> (None, code)
-      | _ ->
-	  errorlabstrm "add_destructor_hint"
-          (str "The tactic should be a function of the hypothesis name.") end
-  in
-  let pat = match loc with
-    | HypLocation b ->
-	HypLocation
-	  (b,{d_typ=pat;d_sort=catch_all_sort_pattern},
-	     {d_typ=catch_all_type_pattern;d_sort=catch_all_sort_pattern})
-    | ConclLocation () ->
-	ConclLocation({d_typ=pat;d_sort=catch_all_sort_pattern}) in
-  Lib.add_anonymous_leaf
-    (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code }))
-
-let match_dpat dp cls gls =
-  let onconcl = cls.concl_occs <> no_occurrences_expr in
-  match (cls,dp) with
-    | ({onhyps=lo},HypLocation(_,hypd,concld)) when not onconcl ->
-        let hl = match lo with
-            Some l -> l
-          | None -> List.map (fun id -> ((all_occurrences_expr,id),InHyp))
-	              (pf_ids_of_hyps gls) in
-        if not
-          (List.for_all
-            (fun ((_,id),hl) ->
-              let cltyp = pf_get_hyp_typ gls id in
-              let cl = pf_concl gls in
-              (hl=InHyp) &
-              (is_matching hypd.d_typ cltyp) &
-              (is_matching hypd.d_sort (pf_type_of gls cltyp)) &
-              (is_matching concld.d_typ cl) &
-              (is_matching concld.d_sort (pf_type_of gls cl)))
-            hl)
-        then error "No match."
-    | ({onhyps=Some[]},ConclLocation concld) when onconcl ->
-        let cl = pf_concl gls in
-        if not
-          ((is_matching concld.d_typ cl) &
-           (is_matching concld.d_sort (pf_type_of gls cl)))
-        then error "No match."
-    | _ -> error "ApplyDestructor"
-
-let forward_interp_tactic =
-  ref (fun _ -> failwith "interp_tactic is not installed for DHyp")
-
-let set_extern_interp f = forward_interp_tactic := f
-
-let applyDestructor cls discard dd gls =
-  match_dpat dd.d_pat cls gls;
-  let cll = simple_clause_of cls gls in
-  let tacl =
-    List.map (fun cl ->
-      match cl, dd.d_code with
-        | Some id, (Some x, tac) ->
-	    let arg =
-              ConstrMayEval(ConstrTerm (GRef(dummy_loc,VarRef id),None)) in
-            TacLetIn (false, [(dummy_loc, x), arg], tac)
-        | None, (None, tac) -> tac
-        | _, (Some _,_) -> error "Destructor expects an hypothesis."
-        | _, (None,_) -> error "Destructor is for conclusion.")
-      cll in
-  let discard_0 =
-    List.map (fun cl ->
-      match (cl,dd.d_pat) with
-        | (Some id,HypLocation(discardable,_,_)) ->
-            if discard & discardable then thin [id] else tclIDTAC
-        | (None,ConclLocation _) -> tclIDTAC
-        | _ -> error "ApplyDestructor" ) cll in
-  tclTHEN (tclMAP !forward_interp_tactic tacl) (tclTHENLIST discard_0) gls
-
-
-(* [DHyp id gls]
-
-   will take an identifier, get its type, look it up in the
-   discrimination net, get the destructors stored there, and then try
-   them in order of priority. *)
-
-let destructHyp discard id gls =
-  let hyptyp = pf_get_hyp_typ gls id in
-  let ddl = List.map snd (lookup hyptyp) in
-  let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
-  tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls
-
-let dHyp id gls = destructHyp false id gls
-
-let h_destructHyp b id =
-  abstract_tactic (TacDestructHyp (b,(dummy_loc,id))) (destructHyp b id)
-
-(* [DConcl gls]
-
-   will take a goal, get its concl, look it up in the
-   discrimination net, get the destructors stored there, and then try
-   them in order of priority. *)
-
-let dConcl gls =
-  let ddl = List.map snd (lookup (pf_concl gls)) in
-  let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in
-  tclFIRST (List.map (applyDestructor onConcl false) sorted_ddl) gls
-
-let h_destructConcl = abstract_tactic TacDestructConcl dConcl
-
-let rec search n =
-  if n=0 then error "Search has reached zero.";
-  tclFIRST
-    [intros;
-     assumption;
-     (tclTHEN
-        (Tacticals.tryAllHypsAndConcl
-           (function
-              | Some id -> (dHyp id)
-              | None    ->  dConcl ))
-        (search (n-1)))]
-
-let auto_tdb n = tclTRY (tclCOMPLETE (search n))
-
-let search_depth_tdb = ref(5)
-
-let depth_tdb = function
-  | None -> !search_depth_tdb
-  | Some n -> n
-
-let h_auto_tdb n = abstract_tactic (TacAutoTDB n) (auto_tdb (depth_tdb n))
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
deleted file mode 100644
index 1bdeed6aa..000000000
--- a/tactics/dhyp.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Tacmach
-open Tacexpr
-
-(** Programmable destruction of hypotheses and conclusions. *)
-
-val set_extern_interp : (glob_tactic_expr -> tactic) -> unit
-
-(*
-val dHyp : identifier -> tactic
-val dConcl : tactic
-*)
-val h_destructHyp : bool -> identifier -> tactic
-val h_destructConcl : tactic
-val h_auto_tdb : int option -> tactic
-
-val add_destructor_hint :
-  Vernacexpr.locality_flag -> identifier -> (bool,unit) Tacexpr.location ->
-    Glob_term.patvar list * Pattern.constr_pattern -> int ->
-      glob_tactic_expr -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9da816d90..81c79f931 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -718,10 +718,6 @@ let rec intern_atomic lf ist x =
   | TacAuto (n,lems,l) ->
       TacAuto (Option.map (intern_or_var ist) n,
         List.map (intern_constr ist) lems,l)
-  | TacAutoTDB n -> TacAutoTDB n
-  | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
-  | TacDestructConcl -> TacDestructConcl
-  | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
   | TacDAuto (n,p,lems) ->
       TacDAuto (Option.map (intern_or_var ist) n,p,
         List.map (intern_constr ist) lems)
@@ -2285,10 +2281,6 @@ and interp_atomic ist gl tac =
       Auto.h_auto (Option.map (interp_int_or_var ist) n)
 	(interp_auto_lemmas ist env sigma lems)
 	(Option.map (List.map (interp_hint_base ist)) l)
-  | TacAutoTDB n -> Dhyp.h_auto_tdb n
-  | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
-  | TacDestructConcl -> Dhyp.h_destructConcl
-  | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
   | TacDAuto (n,p,lems) ->
       Auto.h_dauto (Option.map (interp_int_or_var ist) n,p)
       (interp_auto_lemmas ist env sigma lems)
@@ -2656,10 +2648,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   (* Automation tactics *)
   | TacTrivial (lems,l) -> TacTrivial (List.map (subst_glob_constr subst) lems,l)
   | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_glob_constr subst) lems,l)
-  | TacAutoTDB n -> TacAutoTDB n
-  | TacDestructHyp (b,id) -> TacDestructHyp(b,id)
-  | TacDestructConcl -> TacDestructConcl
-  | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
   | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_glob_constr subst) lems)
 
   (* Derived basic tactics *)
@@ -3004,4 +2992,3 @@ let _ = Auto.set_extern_intern_tac
     Flags.with_option strict_check
     (intern_pure_tactic {(make_empty_glob_sign()) with ltacvars=(l,[])}))
 let _ = Auto.set_extern_subst_tactic subst_tactic
-let _ = Dhyp.set_extern_interp eval_tactic
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 333d6a3a2..f1324809a 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -10,7 +10,6 @@ Elimschemes
 Tactics
 Hiddentac
 Elim
-Dhyp
 Auto
 Equality
 Contradiction