aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/coretactics.ml461
-rw-r--r--tactics/tacintern.ml6
-rw-r--r--tactics/tacinterp.ml26
-rw-r--r--tactics/tacsubst.ml6
4 files changed, 61 insertions, 38 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 0170b68014..2434d3f453 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -8,6 +8,11 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+open Util
+open Names
+open Tacexpr
+open Tacinterp
+
DECLARE PLUGIN "coretactics"
TACTIC EXTEND reflexivity
@@ -17,3 +22,59 @@ END
TACTIC EXTEND assumption
[ "assumption" ] -> [ Tactics.assumption ]
END
+
+let make_vars len =
+ List.init len (fun i -> Id.of_string (Printf.sprintf "_%i" i))
+
+let dummy_id = Id.of_string "_"
+
+(** Add a tactic that only uses constrs arguments. Such tactics actually do
+ not need to define grammar rules, because tactic arguments are already
+ parsed as constrs. So we add them manually. *)
+(** TODO: do this automagically in TACTIC EXTEND and use it in this file *)
+let add_constr_tactic name len tac =
+ let vars = make_vars len in
+ (** We pass the arguments through the environment rather than through the
+ tactic, to overcome the way tactics arguments are interpreted. *)
+ let tac _ ist = Proofview.Goal.raw_enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let map id =
+ let c = Id.Map.find id ist.lfun in
+ try Taccoerce.coerce_to_closed_constr env c
+ with Taccoerce.CannotCoerceTo ty ->
+ error_ltac_variable Loc.ghost dummy_id (Some env) c ty
+ in
+ let args = List.map map vars in
+ tac args ist
+ end in
+ let () = Tacenv.register_ml_tactic name tac in
+ let ref = Libnames.Ident (Loc.ghost, Id.of_string name) in
+ let args = List.map (fun id -> Some id) vars in
+ let body = TacExtend (Loc.ghost, name, []) in
+ let body = TacFun (args, TacAtom (Loc.ghost, body)) in
+ let obj () = Tacenv.register_ltac false false [ref, false, body] in
+ Mltop.declare_cache_obj obj "coretactics"
+
+let () =
+ let tac args _ = match args with [c] _ -> Tactics.cut c | _ -> assert false in
+ add_constr_tactic "cut" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.exact_no_check c) | _ -> assert false in
+ add_constr_tactic "exact_no_check" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.vm_cast_no_check c) | _ -> assert false in
+ add_constr_tactic "vm_cast_no_check" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.case_type c) | _ -> assert false in
+ add_constr_tactic "casetype" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Proofview.V82.tactic (Tactics.elim_type c) | _ -> assert false in
+ add_constr_tactic "elimtype" 1 tac
+
+let () =
+ let tac args _ = match args with [c] -> Tactics.cut_and_apply c | _ -> assert false in
+ add_constr_tactic "lapply" 1 tac
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index ea3e346853..22ea274cb7 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -456,17 +456,13 @@ let rec intern_atomic lf ist x =
TacIntroMove (Option.map (intern_ident lf ist) ido,
intern_move_location ist hto)
| TacExact c -> TacExact (intern_constr ist c)
- | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
- | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
| TacApply (a,ev,cb,inhyp) ->
TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb,
Option.map (intern_in_hyp_as ist lf) inhyp)
| TacElim (ev,cb,cbo) ->
TacElim (ev,intern_constr_with_bindings ist cb,
Option.map (intern_constr_with_bindings ist) cbo)
- | TacElimType c -> TacElimType (intern_type ist c)
| TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
- | TacCaseType c -> TacCaseType (intern_type ist c)
| TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
| TacMutualFix (id,n,l) ->
let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
@@ -475,7 +471,6 @@ let rec intern_atomic lf ist x =
| TacMutualCofix (id,l) ->
let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
TacMutualCofix (intern_ident lf ist id, List.map f l)
- | TacCut c -> TacCut (intern_type ist c)
| TacAssert (otac,ipat,c) ->
TacAssert (Option.map (intern_pure_tactic ist) otac,
Option.map (intern_intro_pattern lf ist) ipat,
@@ -516,7 +511,6 @@ let rec intern_atomic lf ist x =
| TacDecompose (l,c) -> let l = List.map (intern_inductive ist) l in
TacDecompose (l,intern_constr ist c)
| TacSpecialize (n,l) -> TacSpecialize (n,intern_constr_with_bindings ist l)
- | TacLApply c -> TacLApply (intern_constr ist c)
(* Context management *)
| TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d72a37d33e..4333c5696d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1455,12 +1455,6 @@ and interp_atomic ist tac =
(Tactics.exact_no_check c_interp)
gl
end
- | TacExactNoCheck c ->
- (new_interp_constr ist c)
- (fun c -> Proofview.V82.tactic (Tactics.exact_no_check c))
- | TacVmCastNoCheck c ->
- (new_interp_constr ist c)
- (fun c -> Proofview.V82.tactic (Tactics.vm_cast_no_check c))
| TacApply (a,ev,cb,cl) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1487,14 +1481,6 @@ and interp_atomic ist tac =
let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
Tacticals.New.tclWITHHOLES ev (Tactics.elim ev cb) sigma cbo
end
- | TacElimType c ->
- Proofview.V82.tactic begin fun gl ->
- let (sigma,c_interp) = pf_interp_type ist gl c in
- tclTHEN
- (tclEVARS sigma)
- (Tactics.elim_type c_interp)
- gl
- end
| TacCase (ev,cb) ->
Proofview.Goal.raw_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
@@ -1502,14 +1488,6 @@ and interp_atomic ist tac =
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev) sigma cb
end
- | TacCaseType c ->
- Proofview.V82.tactic begin fun gl ->
- let (sigma,c_interp) = pf_interp_type ist gl c in
- tclTHEN
- (tclEVARS sigma)
- (Tactics.case_type c_interp)
- gl
- end
| TacFix (idopt,n) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1548,8 +1526,6 @@ and interp_atomic ist tac =
(Tactics.mutual_cofix (interp_fresh_ident ist env id) l_interp 0)
gl
end
- | TacCut c ->
- new_interp_type ist c Tactics.cut
| TacAssert (t,ipat,c) ->
Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1670,8 +1646,6 @@ and interp_atomic ist tac =
tclWITHHOLES false (Tactics.specialize n) sigma cb gl
end
end
- | TacLApply c ->
- new_interp_constr ist c Tactics.cut_and_apply
(* Context management *)
| TacClear (b,l) ->
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 31a1b57bc0..4d0b595690 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -135,23 +135,18 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Basic tactics *)
| TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
| TacExact c -> TacExact (subst_glob_constr subst c)
- | TacExactNoCheck c -> TacExactNoCheck (subst_glob_constr subst c)
- | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_glob_constr subst c)
| TacApply (a,ev,cb,cl) ->
TacApply (a,ev,List.map (subst_glob_with_bindings subst) cb,cl)
| TacElim (ev,cb,cbo) ->
TacElim (ev,subst_glob_with_bindings subst cb,
Option.map (subst_glob_with_bindings subst) cbo)
- | TacElimType c -> TacElimType (subst_glob_constr subst c)
| TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
- | TacCaseType c -> TacCaseType (subst_glob_constr subst c)
| TacFix (idopt,n) as x -> x
| TacMutualFix (id,n,l) ->
TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
| TacCofix idopt as x -> x
| TacMutualCofix (id,l) ->
TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
- | TacCut c -> TacCut (subst_glob_constr subst c)
| TacAssert (b,na,c) ->
TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
| TacGeneralize cl ->
@@ -177,7 +172,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
let l = List.map (subst_or_var (subst_ind subst)) l in
TacDecompose (l,subst_glob_constr subst c)
| TacSpecialize (n,l) -> TacSpecialize (n,subst_glob_with_bindings subst l)
- | TacLApply c -> TacLApply (subst_glob_constr subst c)
(* Context management *)
| TacClear _ as x -> x
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 15:37:27 +0000