1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Genarg
open Pp
open Names
open Tacexpr
(** Tactic notations (TacAlias) *)
type alias = KerName.t
let alias_map = Summary.ref ~name:"tactic-alias"
(KNmap.empty : glob_tactic_expr KNmap.t)
let register_alias key tac =
alias_map := KNmap.add key tac !alias_map
let interp_alias key =
try KNmap.find key !alias_map
with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key)
(** ML tactic extensions (TacML) *)
type ml_tactic =
typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic
module MLName =
struct
type t = ml_tactic_name
let compare tac1 tac2 =
let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in
if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin
else c
end
module MLTacMap = Map.Make(MLName)
let pr_tacname t =
t.mltac_plugin ^ "::" ^ t.mltac_tactic
let tac_tab = ref MLTacMap.empty
let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) =
let () =
if MLTacMap.mem s !tac_tab then
if overwrite then
let () = tac_tab := MLTacMap.remove s !tac_tab in
msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s))
else
Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ "."))
in
tac_tab := MLTacMap.add s t !tac_tab
let interp_ml_tactic s =
try
MLTacMap.find s !tac_tab
with Not_found ->
Errors.errorlabstrm ""
(str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
(***************************************************************************)
(* Tactic registration *)
(* Summary and Object declaration *)
open Nametab
open Libobject
let mactab =
Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t)
~name:"tactic-definition"
let interp_ltac r = snd (KNmap.find r !mactab)
let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab)
(* Declaration of the TAC-DEFINITION object *)
let add (kn,td) = mactab := KNmap.add kn td !mactab
let load_md i ((sp, kn), (local, id, b, t)) = match id with
| None ->
let () = if not local then Nametab.push_tactic (Until i) sp kn in
add (kn, (b,t))
| Some kn -> add (kn, (b,t))
let open_md i ((sp, kn), (local, id, b, t)) = match id with
| None ->
let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
add (kn, (b,t))
| Some kn -> add (kn, (b,t))
let cache_md ((sp, kn), (local, id ,b, t)) = match id with
| None ->
let () = Nametab.push_tactic (Until 1) sp kn in
add (kn, (b,t))
| Some kn -> add (kn, (b,t))
let subst_kind subst id = match id with
| None -> None
| Some kn -> Some (Mod_subst.subst_kn subst kn)
let subst_md (subst, (local, id, b, t)) =
(local, subst_kind subst id, b, Tacsubst.subst_tactic subst t)
let classify_md (local, _, _, _ as o) = Substitute o
let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj =
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
open_function = open_md;
subst_function = subst_md;
classify_function = classify_md}
let register_ltac for_ml local id tac =
ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
let redefine_ltac local kn tac =
Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
|
