From 1f05de5d4e19867c3425c39999a1f58e12b57657 Mon Sep 17 00:00:00 2001 From: letouzey Date: Sat, 6 Oct 2012 10:08:32 +0000 Subject: Clean-up : removal of Proof_type.tactic_expr This instance of gen_tactic_expr was used only to decorate tactics via Refiner.abstract_tactics and alii, but these expressions are now ignored by the new proof-engine (no "info"...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7 --- grammar/tacextend.ml4 | 2 +- plugins/xml/dumptree.ml4 | 9 ---- printing/pptactic.ml | 15 ------- printing/pptactic.mli | 2 - proofs/proof_type.ml | 33 -------------- proofs/proof_type.mli | 34 -------------- proofs/refiner.ml | 6 +-- proofs/refiner.mli | 7 ++- tactics/auto.ml | 6 +-- tactics/elim.ml | 8 ++-- tactics/eqdecide.ml4 | 2 +- tactics/hiddentac.ml | 112 ++++++++++++++++++----------------------------- tactics/tacinterp.ml | 13 +++--- 13 files changed, 63 insertions(+), 186 deletions(-) diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index f11927e77..8b5b64ffc 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -177,7 +177,7 @@ let declare_tactic loc s cl = let e = make_fun <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ + Refiner.abstract_extended_tactic $make_eval_tactic e p$ >> p in <:str_item< value $lid:stac$ = $e$ >> diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4 index c0c8ada95..1fd829e7a 100644 --- a/plugins/xml/dumptree.ml4 +++ b/plugins/xml/dumptree.ml4 @@ -36,15 +36,6 @@ let thin_sign osign sign = sign ~init:Environ.empty_named_context_val ;; -let pr_tactic_xml = function - | TacArg (_,Tacexp t) -> str "" - | t -> str "" -;; - -let pr_proof_instr_xml instr = - Ppdecl_proof.pr_proof_instr (Global.env()) instr -;; - let pr_var_decl_xml env (id,c,typ) = let ptyp = print_constr_env env typ in match c with diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b790c4ea6..055f08d93 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1035,23 +1035,8 @@ and pr_glob_tactic_level env n (t:glob_tactic_expr) = let pr_constr_or_lconstr_pattern b = if b then pr_lconstr_pattern else pr_constr_pattern -let typed_printers = - (pr_glob_tactic_level, - pr_constr_env, - pr_lconstr_env, - pr_constr_or_lconstr_pattern, - pr_evaluable_reference_env, - pr_inductive, - pr_ltac_constant, - pr_id, - pr_extend, - strip_prod_binders_constr) - -let pr_tactic_level env = fst (make_pr_tac typed_printers env) - let pr_raw_tactic env = pr_raw_tactic_level env ltop let pr_glob_tactic env = pr_glob_tactic_level env ltop -let pr_tactic env = pr_tactic_level env ltop let _ = Tactic_debug.set_tactic_printer (fun x -> pr_glob_tactic (Global.env()) x) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 61acffd08..8973bd6bc 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -92,8 +92,6 @@ val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds -val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds - val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index b84b6db48..e09d72e47 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -46,39 +46,6 @@ type prim_rule = type rule = prim_rule -type tactic_expr = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_tactic_expr - -and atomic_tactic_expr = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_atomic_tactic_expr - -and tactic_arg = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_tactic_arg - (** Ltac traces *) type ltac_call_kind = diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 6688d6e62..95ca33e90 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -70,40 +70,6 @@ type goal = Goal.goal type tactic = goal sigma -> goal list sigma - -type tactic_expr = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_tactic_expr - -and atomic_tactic_expr = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_atomic_tactic_expr - -and tactic_arg = - (constr, - constr_pattern, - evaluable_global_reference, - inductive, - ltac_constant, - identifier, - glob_tactic_expr, - tlevel) - Tacexpr.gen_tactic_arg - (** Ltac traces *) type ltac_call_kind = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 4b5bdcfe9..33b070e76 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -23,9 +23,9 @@ let project x = x.sigma let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls)) let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)) -let abstract_tactic_expr ?(dflt=false) te tacfun = tacfun -let abstract_tactic ?(dflt=false) te tacfun = tacfun -let abstract_extended_tactic ?(dflt=false) s args tacfun = tacfun +let abstract_tactic_expr tacfun = tacfun +let abstract_tactic tacfun = tacfun +let abstract_extended_tactic tacfun = tacfun let refiner pr goal_sigma = let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 6f11e7115..bc47a73c9 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -33,10 +33,9 @@ val apply_sig_tac : (* spiwack: currently here for compatibility, the tactic expression is discarded and we simply return the tactic. *) -val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic -val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic -val abstract_extended_tactic : - ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic +val abstract_tactic : tactic -> tactic +val abstract_tactic_expr : tactic -> tactic +val abstract_extended_tactic : tactic -> tactic val refiner : rule -> tactic diff --git a/tactics/auto.ml b/tactics/auto.ml index 748b608b4..926e65d29 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1017,7 +1017,7 @@ let auto_unif_flags = { (* Try unification with the precompiled clause, then use registered Apply *) let h_clenv_refine ev c clenv = - Refiner.abstract_tactic (TacApply (true,ev,[c,NoBindings],None)) + Refiner.abstract_tactic (Clenvtac.clenv_refine ev clenv) let unify_resolve_nodelta (c,clenv) gl = @@ -1355,7 +1355,7 @@ let gen_trivial ?(debug=Off) lems = function | Some l -> trivial ~debug lems l let h_trivial ?(debug=Off) lems l = - Refiner.abstract_tactic (TacTrivial (debug,List.map snd lems,l)) + Refiner.abstract_tactic (gen_trivial ~debug lems l) (**************************************************************************) @@ -1439,5 +1439,5 @@ let gen_auto ?(debug=Off) n lems dbnames = let inj_or_var = Option.map (fun n -> ArgArg n) let h_auto ?(debug=Off) n lems l = - Refiner.abstract_tactic (TacAuto (debug,inj_or_var n,List.map snd lems,l)) + Refiner.abstract_tactic (gen_auto ~debug n lems l) diff --git a/tactics/elim.ml b/tactics/elim.ml index 32acc5af5..a25a37092 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -123,13 +123,13 @@ let decompose_or c gls = c gls let h_decompose l c = - Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) + Refiner.abstract_tactic (decompose_these c l) let h_decompose_or c = - Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) + Refiner.abstract_tactic (decompose_or c) let h_decompose_and c = - Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) + Refiner.abstract_tactic (decompose_and c) (* The tactic Double performs a double induction *) @@ -175,6 +175,6 @@ let double_ind h1 h2 gls = ([],[]) (mkVar id)))) gls let h_double_induction h1 h2 = - Refiner.abstract_tactic (TacDoubleInduction (h1,h2)) (double_ind h1 h2) + Refiner.abstract_tactic (double_ind h1 h2) diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 5329029a8..89d2a85d8 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -73,7 +73,7 @@ let solveNoteqBranch side = (onLastHypId (fun id -> Extratactics.h_discrHyp id))) let h_solveNoteqBranch side = - Refiner.abstract_extended_tactic "solveNoteqBranch" [] + Refiner.abstract_extended_tactic (solveNoteqBranch side) (* Constructs the type {c1=c2}+{~c1=c2} *) diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index b68b6c545..25106d1ef 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -14,125 +14,97 @@ open Locus open Misctypes (* Basic tactics *) -let h_intro_move x y = - abstract_tactic (TacIntroMove (x, y)) (intro_move x y) +let h_intro_move x y = abstract_tactic (intro_move x y) let h_intro x = h_intro_move (Some x) MoveLast -let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) -let h_assumption = abstract_tactic TacAssumption assumption -let h_exact c = abstract_tactic (TacExact c) (exact_check c) -let h_exact_no_check c = - abstract_tactic (TacExactNoCheck c) (exact_no_check c) -let h_vm_cast_no_check c = - abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c) -let h_apply simple ev cb = - abstract_tactic (TacApply (simple,ev,List.map snd cb,None)) +let h_intros_until x = abstract_tactic (intros_until x) +let h_assumption = abstract_tactic assumption +let h_exact c = abstract_tactic (exact_check c) +let h_exact_no_check c = abstract_tactic (exact_no_check c) +let h_vm_cast_no_check c = abstract_tactic (vm_cast_no_check c) +let h_apply simple ev cb = abstract_tactic (apply_with_bindings_gen simple ev cb) -let h_apply_in simple ev cb (id,ipat as inhyp) = - abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp)) - (apply_in simple ev id cb ipat) -let h_elim ev cb cbo = - abstract_tactic (TacElim (ev,cb,cbo)) - (elim ev cb cbo) -let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c) -let h_case ev cb = abstract_tactic (TacCase (ev,cb)) (general_case_analysis ev cb) -let h_case_type c = abstract_tactic (TacCaseType c) (case_type c) -let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n) -let h_mutual_fix b id n l = - abstract_tactic - (TacMutualFix (b,id,n,l)) - (mutual_fix id n l 0) +let h_apply_in simple ev cb (id,ipat) = + abstract_tactic (apply_in simple ev id cb ipat) +let h_elim ev cb cbo = abstract_tactic (elim ev cb cbo) +let h_elim_type c = abstract_tactic (elim_type c) +let h_case ev cb = abstract_tactic (general_case_analysis ev cb) +let h_case_type c = abstract_tactic (case_type c) +let h_fix ido n = abstract_tactic (fix ido n) +let h_mutual_fix b id n l = abstract_tactic (mutual_fix id n l 0) -let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido) -let h_mutual_cofix b id l = - abstract_tactic - (TacMutualCofix (b,id,l)) - (mutual_cofix id l 0) +let h_cofix ido = abstract_tactic (cofix ido) +let h_mutual_cofix b id l = abstract_tactic (mutual_cofix id l 0) -let h_cut c = abstract_tactic (TacCut c) (cut c) +let h_cut c = abstract_tactic (cut c) let h_generalize_gen cl = - abstract_tactic (TacGeneralize cl) + abstract_tactic (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) let h_generalize cl = h_generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous)) cl) let h_generalize_dep c = - abstract_tactic (TacGeneralizeDep c) (generalize_dep c) + abstract_tactic (generalize_dep c) let h_let_tac b na c cl eqpat = let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in - abstract_tactic (TacLetTac (na,c,cl,b,eqpat)) - (letin_tac with_eq na c None cl) + abstract_tactic (letin_tac with_eq na c None cl) let h_let_pat_tac b na c cl eqpat = let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in - abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat)) - (letin_pat_tac with_eq na c None cl) + abstract_tactic (letin_pat_tac with_eq na c None cl) (* Derived basic tactics *) let h_simple_induction_destruct isrec h = - abstract_tactic (TacSimpleInductionDestruct (isrec,h)) - (if isrec then (simple_induct h) else (simple_destruct h)) + abstract_tactic (if isrec then (simple_induct h) else (simple_destruct h)) let h_simple_induction = h_simple_induction_destruct true let h_simple_destruct = h_simple_induction_destruct false -let out_indarg = function - | ElimOnConstr (_,c) -> ElimOnConstr c - | ElimOnIdent id -> ElimOnIdent id - | ElimOnAnonHyp n -> ElimOnAnonHyp n - let h_induction_destruct isrec ev lcl = - let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in - abstract_tactic (TacInductionDestruct (isrec,ev,lcl')) - (induction_destruct isrec ev lcl) + abstract_tactic (induction_destruct isrec ev lcl) let h_new_induction ev c idl e cl = h_induction_destruct true ev ([c,idl],e,cl) let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl) -let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d) -let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) +let h_specialize n d = abstract_tactic (specialize n d) +let h_lapply c = abstract_tactic (cut_and_apply c) (* Context management *) -let h_clear b l = abstract_tactic (TacClear (b,l)) - ((if b then keep else clear) l) -let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l) -let h_move dep id1 id2 = - abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2) -let h_rename l = - abstract_tactic (TacRename l) (rename_hyp l) -let h_revert l = abstract_tactic (TacRevert l) (revert l) +let h_clear b l = abstract_tactic ((if b then keep else clear) l) +let h_clear_body l = abstract_tactic (clear_body l) +let h_move dep id1 id2 = abstract_tactic (move_hyp dep id1 id2) +let h_rename l = abstract_tactic (rename_hyp l) +let h_revert l = abstract_tactic (revert l) (* Constructors *) -let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_bindings ev l) -let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_bindings ev l) -let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_bindings ev l) +let h_left ev l = abstract_tactic (left_with_bindings ev l) +let h_right ev l = abstract_tactic (right_with_bindings ev l) +let h_split ev l = abstract_tactic (split_with_bindings ev l) (* Moved to tacinterp because of dependencies in Tacinterp.interp let h_any_constructor t = abstract_tactic (TacAnyConstructor t) (any_constructor t) *) let h_constructor ev n l = - abstract_tactic (TacConstructor(ev,ArgArg n,l))(constructor_tac ev None n l) + abstract_tactic (constructor_tac ev None n l) let h_one_constructor n = - abstract_tactic (TacConstructor(false,ArgArg n,NoBindings)) (one_constructor n NoBindings) + abstract_tactic (one_constructor n NoBindings) let h_simplest_left = h_left false NoBindings let h_simplest_right = h_right false NoBindings (* Conversion *) let h_reduce r cl = - abstract_tactic (TacReduce (r,cl)) (reduce r cl) + abstract_tactic (reduce r cl) let h_change op c cl = - abstract_tactic (TacChange (op,c,cl)) (change op c cl) + abstract_tactic (change op c cl) (* Equivalence relations *) -let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity -let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) -let h_transitivity c = - abstract_tactic (TacTransitivity c) - (intros_transitivity c) +let h_reflexivity = abstract_tactic intros_reflexivity +let h_symmetry c = abstract_tactic (intros_symmetry c) +let h_transitivity c = abstract_tactic (intros_transitivity c) let h_simplest_apply c = h_apply false false [Loc.ghost,(c,NoBindings)] let h_simplest_eapply c = h_apply false true [Loc.ghost,(c,NoBindings)] let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) -let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l) +let h_intro_patterns l = abstract_tactic (intro_patterns l) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 12c970d68..2ed054ea1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2380,7 +2380,7 @@ and interp_atomic ist gl tac = let (sigma,c) = (if t=None then interp_constr else interp_type) ist env sigma c in tclTHEN (tclEVARS sigma) - (abstract_tactic (TacAssert (t,ipat,c)) + (abstract_tactic (Tactics.forward (Option.map (interp_tactic ist) t) (Option.map (interp_intro_pattern ist gl) ipat) c)) | TacGeneralize cl -> @@ -2479,7 +2479,7 @@ and interp_atomic ist gl tac = let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in tclWITHHOLES ev (h_split ev) sigma bll | TacAnyConstructor (ev,t) -> - abstract_tactic (TacAnyConstructor (ev,t)) + abstract_tactic (Tactics.any_constructor ev (Option.map (interp_tactic ist) t)) | TacConstructor (ev,n,bl) -> let sigma, bl = interp_bindings ist env sigma bl in @@ -2569,7 +2569,7 @@ and interp_atomic ist gl tac = sigma , a_interp::acc end l (project gl,[]) in - abstract_extended_tactic opn args (tac args) + abstract_extended_tactic (tac args) | TacAlias (loc,s,l,(_,body)) -> fun gl -> let evdref = ref gl.sigma in let f x = match genarg_tag x with @@ -2706,16 +2706,15 @@ let eval_ltac_constr gl t = { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl (intern_tactic_or_tacarg (make_empty_glob_sign ()) t ) -(* Hides interpretation for pretty-print *) +(* Used to hide interpretation for pretty-print, now just launch tactics *) let hide_interp t ot gl = let ist = { ltacvars = ([],[]); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } in let te = intern_tactic true ist t in let t = eval_tactic te in match ot with - | None -> abstract_tactic_expr (TacArg (dloc,Tacexp te)) t gl - | Some t' -> - abstract_tactic_expr ~dflt:true (TacArg (dloc,Tacexp te)) (tclTHEN t t') gl + | None -> abstract_tactic_expr t gl + | Some t' -> abstract_tactic_expr (tclTHEN t t') gl (***************************************************************************) (* Substitution at module closing time *) -- cgit v1.2.3