Permalink
Browse files

remove Refiner.abstract_tactic and similar

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
1 parent f975575 commit e1bdb515ee2f701bfc56f1bcf4a8e404f759a38a letouzey committed Oct 6, 2012
Showing with 61 additions and 111 deletions.
  1. +1 −6 grammar/tacextend.ml4
  2. +0 −4 proofs/refiner.ml
  3. +0 −11 proofs/refiner.mli
  4. +4 −12 tactics/auto.ml
  5. +4 −8 tactics/elim.ml
  6. +1 −5 tactics/eqdecide.ml4
  7. +43 −55 tactics/hiddentac.ml
  8. +2 −2 tactics/hiddentac.mli
  9. +6 −8 tactics/tacinterp.ml
View
7 grammar/tacextend.ml4
@@ -174,12 +174,7 @@ let declare_tactic loc s cl =
let hide_tac (p,e) =
(* reste a definir les fonctions cachees avec des noms frais *)
let stac = "h_"^s in
- let e =
- make_fun
- <:expr<
- Refiner.abstract_extended_tactic $make_eval_tactic e p$
- >>
- p in
+ let e = make_fun (make_eval_tactic e p) p in
<:str_item< value $lid:stac$ = $e$ >>
in
let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
View
4 proofs/refiner.ml
@@ -23,10 +23,6 @@ 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 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
{it=sgl; sigma = sigma'}
View
11 proofs/refiner.mli
@@ -26,17 +26,6 @@ val repackage : evar_map ref -> 'a -> 'a sigma
val apply_sig_tac :
evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
-(** {6 Hiding the implementation of tactics. } *)
-
-(** [abstract_tactic tac] hides the (partial) proof produced by [tac] under
- a single proof node. The boolean tells if the default tactic is used. *)
-(* spiwack: currently here for compatibility, the tactic expression
- is discarded and we simply return the tactic. *)
-
-val abstract_tactic : tactic -> tactic
-val abstract_tactic_expr : tactic -> tactic
-val abstract_extended_tactic : tactic -> tactic
-
val refiner : rule -> tactic
(** {6 Tacticals. } *)
View
16 tactics/auto.ml
@@ -1016,19 +1016,15 @@ let auto_unif_flags = {
(* Try unification with the precompiled clause, then use registered Apply *)
-let h_clenv_refine ev c clenv =
- Refiner.abstract_tactic
- (Clenvtac.clenv_refine ev clenv)
-
let unify_resolve_nodelta (c,clenv) gl =
let clenv' = connect_clenv gl clenv in
let clenv'' = clenv_unique_resolver ~flags:auto_unif_flags clenv' gl in
- h_clenv_refine false c clenv'' gl
+ Clenvtac.clenv_refine false clenv'' gl
let unify_resolve flags (c,clenv) gl =
let clenv' = connect_clenv gl clenv in
let clenv'' = clenv_unique_resolver ~flags clenv' gl in
- h_clenv_refine false c clenv'' gl
+ Clenvtac.clenv_refine false clenv'' gl
let unify_resolve_gen = function
| None -> unify_resolve_nodelta
@@ -1354,9 +1350,7 @@ let gen_trivial ?(debug=Off) lems = function
| None -> full_trivial ~debug lems
| Some l -> trivial ~debug lems l
-let h_trivial ?(debug=Off) lems l =
- Refiner.abstract_tactic
- (gen_trivial ~debug lems l)
+let h_trivial ?(debug=Off) lems l = gen_trivial ~debug lems l
(**************************************************************************)
(* The classical Auto tactic *)
@@ -1438,6 +1432,4 @@ 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
- (gen_auto ~debug n lems l)
+let h_auto ?(debug=Off) n lems l = gen_auto ~debug n lems l
View
12 tactics/elim.ml
@@ -122,14 +122,11 @@ let decompose_or c gls =
(fun (_,t) -> is_disjunction t)
c gls
-let h_decompose l c =
- Refiner.abstract_tactic (decompose_these c l)
+let h_decompose l c = decompose_these c l
-let h_decompose_or c =
- Refiner.abstract_tactic (decompose_or c)
+let h_decompose_or = decompose_or
-let h_decompose_and c =
- Refiner.abstract_tactic (decompose_and c)
+let h_decompose_and = decompose_and
(* The tactic Double performs a double induction *)
@@ -174,7 +171,6 @@ let double_ind h1 h2 gls =
(introElimAssumsThen (induction_trailer abs_i abs_j))
([],[]) (mkVar id)))) gls
-let h_double_induction h1 h2 =
- Refiner.abstract_tactic (double_ind h1 h2)
+let h_double_induction = double_ind
View
6 tactics/eqdecide.ml4
@@ -72,10 +72,6 @@ let solveNoteqBranch side =
(tclTHEN introf
(onLastHypId (fun id -> Extratactics.h_discrHyp id)))
-let h_solveNoteqBranch side =
- Refiner.abstract_extended_tactic
- (solveNoteqBranch side)
-
(* Constructs the type {c1=c2}+{~c1=c2} *)
let mkDecideEqGoal eqonleft op rectype c1 c2 g =
@@ -151,7 +147,7 @@ let decideGralEquality g =
in
(tclTHEN
(mkBranches c1 c2)
- (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+ (tclORELSE (solveNoteqBranch eqonleft) (solveEqBranch rectype)))
g
with PatternMatchingFailure ->
error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."
View
98 tactics/hiddentac.ml
@@ -14,97 +14,85 @@ open Locus
open Misctypes
(* Basic tactics *)
-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 (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) =
- 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_intro_move = intro_move
+let h_intro x = h_intro_move (Some x) MoveLast
+let h_intros_until = intros_until
+let h_assumption = assumption
+let h_exact = exact_check
+let h_exact_no_check = exact_no_check
+let h_vm_cast_no_check = vm_cast_no_check
+let h_apply = apply_with_bindings_gen
+let h_apply_in simple ev cb (id,ipat) = apply_in simple ev id cb ipat
+let h_elim = elim
+let h_elim_type = elim_type
+let h_case = general_case_analysis
+let h_case_type = case_type
+let h_fix = fix
+let h_mutual_fix b id n l = mutual_fix id n 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_cofix = cofix
+let h_mutual_cofix b id l = mutual_cofix id l 0
-let h_cut c = abstract_tactic (cut c)
+let h_cut = cut
let h_generalize_gen cl =
- abstract_tactic
- (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl))
+ 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 (generalize_dep c)
+let h_generalize_dep = generalize_dep
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 (letin_tac with_eq na c None cl)
+ 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 (letin_pat_tac with_eq na c None cl)
+ letin_pat_tac with_eq na c None cl
(* Derived basic tactics *)
let h_simple_induction_destruct isrec h =
- abstract_tactic (if isrec then (simple_induct h) else (simple_destruct h))
+ 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 h_induction_destruct isrec ev lcl =
- abstract_tactic (induction_destruct isrec ev lcl)
+let h_induction_destruct = induction_destruct
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 (specialize n d)
-let h_lapply c = abstract_tactic (cut_and_apply c)
+let h_specialize = specialize
+let h_lapply = cut_and_apply
(* Context management *)
-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)
+let h_clear b l = (if b then keep else clear) l
+let h_clear_body = clear_body
+let h_move = move_hyp
+let h_rename = rename_hyp
+let h_revert = revert
(* Constructors *)
-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 (constructor_tac ev None n l)
-let h_one_constructor n =
- abstract_tactic (one_constructor n NoBindings)
+let h_left = left_with_bindings
+let h_right = right_with_bindings
+let h_split = split_with_bindings
+
+let h_constructor ev n l = constructor_tac ev None n l
+let h_one_constructor n = 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 (reduce r cl)
-let h_change op c cl =
- abstract_tactic (change op c cl)
+let h_reduce = reduce
+let h_change = change
(* Equivalence relations *)
-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_reflexivity = intros_reflexivity
+let h_symmetry = intros_symmetry
+let h_transitivity = intros_transitivity
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 (intro_patterns l)
+let h_intro_patterns = intro_patterns
View
4 tactics/hiddentac.mli
@@ -20,7 +20,7 @@ open Clenv
open Termops
open Misctypes
-(** Tactics for the interpreter. They left a trace in the proof tree
+(** Tactics for the interpreter. They used to left a trace in the proof tree
when they are called. *)
(** Basic tactics *)
@@ -56,7 +56,7 @@ val h_cofix : identifier option -> tactic
val h_cut : constr -> tactic
val h_generalize : constr list -> tactic
val h_generalize_gen : (constr Locus.with_occurrences * name) list -> tactic
-val h_generalize_dep : constr -> tactic
+val h_generalize_dep : ?with_let:bool -> constr -> tactic
val h_let_tac : letin_flag -> name -> constr -> Locus.clause ->
intro_pattern_expr located option -> tactic
val h_let_pat_tac : letin_flag -> name -> evar_map * constr ->
View
14 tactics/tacinterp.ml
@@ -2394,9 +2394,8 @@ 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
- (Tactics.forward (Option.map (interp_tactic ist) t)
- (Option.map (interp_intro_pattern ist gl) ipat) c))
+ (Tactics.forward (Option.map (interp_tactic ist) t)
+ (Option.map (interp_intro_pattern ist gl) ipat) c)
| TacGeneralize cl ->
let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
tclWITHHOLES false (h_generalize_gen) sigma cl
@@ -2493,8 +2492,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
- (Tactics.any_constructor ev (Option.map (interp_tactic ist) t))
+ Tactics.any_constructor ev (Option.map (interp_tactic ist) t)
| TacConstructor (ev,n,bl) ->
let sigma, bl = interp_bindings ist env sigma bl in
tclWITHHOLES ev (h_constructor ev (interp_int_or_var ist n)) sigma bl
@@ -2583,7 +2581,7 @@ and interp_atomic ist gl tac =
sigma , a_interp::acc
end l (project gl,[])
in
- abstract_extended_tactic (tac args)
+ tac args
| TacAlias (loc,s,l,(_,body)) -> fun gl ->
let evdref = ref gl.sigma in
let f x = match genarg_tag x with
@@ -2727,8 +2725,8 @@ let hide_interp t ot gl =
let te = intern_tactic true ist t in
let t = eval_tactic te in
match ot with
- | None -> abstract_tactic_expr t gl
- | Some t' -> abstract_tactic_expr (tclTHEN t t') gl
+ | None -> t gl
+ | Some t' -> (tclTHEN t t') gl
(***************************************************************************)
(* Substitution at module closing time *)

0 comments on commit e1bdb51

Please sign in to comment.