diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 93 | ||||
| -rw-r--r-- | tactics/auto.mli | 16 | ||||
| -rw-r--r-- | tactics/dhyp.ml | 360 | ||||
| -rw-r--r-- | tactics/dhyp.mli | 28 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 13 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 1 |
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 |