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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Errors
open Util
open Names
open Libobject
open Pcoq
open Egramml
open Egramcoq
open Vernacexpr
(**********************************************************************)
(* Tactic Notation *)
let interp_prod_item lev = function
| TacTerm s -> GramTerminal s
| TacNonTerm (loc, nt, (_, sep)) ->
let EntryName (etyp, e) = interp_entry_name lev nt sep in
GramNonTerminal (loc, etyp, e)
let make_terminal_status = function
| GramTerminal s -> Some s
| GramNonTerminal _ -> None
let make_fresh_key =
let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
fun () ->
let cur = incr id; !id in
let lbl = Id.of_string ("_" ^ string_of_int cur) in
let kn = Lib.make_kn lbl in
let (mp, dir, _) = KerName.repr kn in
(** We embed the full path of the kernel name in the label so that the
identifier should be unique. This ensures that including two modules
together won't confuse the corresponding labels. *)
let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
(ModPath.to_string mp) (DirPath.to_string dir) cur)
in
KerName.make mp dir (Label.of_id lbl)
type tactic_grammar_obj = {
tacobj_key : KerName.t;
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
tacobj_tacpp : Pptactic.pp_tactic;
tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
}
let check_key key =
if Tacenv.check_alias key then
error "Conflicting tactic notations keys. This can happen when including \
twice the same module."
let cache_tactic_notation (_, tobj) =
let key = tobj.tacobj_key in
let () = check_key key in
Tacenv.register_alias key tobj.tacobj_body;
Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
let open_tactic_notation i (_, tobj) =
let key = tobj.tacobj_key in
if Int.equal i 1 && not tobj.tacobj_local then
Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
let load_tactic_notation i (_, tobj) =
let key = tobj.tacobj_key in
let () = check_key key in
(** Only add the printing and interpretation rules. *)
Tacenv.register_alias key tobj.tacobj_body;
Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
if Int.equal i 1 && not tobj.tacobj_local then
Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
let (ids, body) = tobj.tacobj_body in
{ tobj with
tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
tacobj_body = (ids, Tacsubst.subst_tactic subst body);
}
let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
open_function = open_tactic_notation;
load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
classify_function = classify_tactic_notation}
let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, _, (id, _)) -> Some id
let add_tactic_notation (local,n,prods,e) =
let ids = List.map_filter cons_production_parameter prods in
let prods = List.map (interp_prod_item n) prods in
let pprule = {
Pptactic.pptac_level = n;
pptac_prods = prods;
} in
let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
let parule = {
tacgram_level = n;
tacgram_prods = prods;
} in
let tacobj = {
tacobj_key = make_fresh_key ();
tacobj_local = local;
tacobj_tacgram = parule;
tacobj_tacpp = pprule;
tacobj_body = (ids, tac);
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
(**********************************************************************)
(* ML Tactic entries *)
type ml_tactic_grammar_obj = {
mltacobj_name : Tacexpr.ml_tactic_name;
(** ML-side unique name *)
mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list;
(** Grammar rules generating the ML tactic. *)
}
exception NonEmptyArgument
(** ML tactic notations whose use can be restricted to an identifier are added
as true Ltac entries. *)
let extend_atomic_tactic name entries =
let open Tacexpr in
let map_prod prods =
let (hd, rem) = match prods with
| GramTerminal s :: rem -> (s, rem)
| _ -> assert false (** Not handled by the ML extension syntax *)
in
let empty_value = function
| GramTerminal s -> raise NonEmptyArgument
| GramNonTerminal (_, typ, e) ->
let Genarg.Rawwit wit = typ in
let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
| Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
in
try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
in
let entries = List.map map_prod entries in
let add_atomic i args = match args with
| None -> ()
| Some (id, args) ->
let args = List.map (fun a -> Tacexp a) args in
let entry = { mltac_name = name; mltac_index = i } in
let body = TacML (Loc.ghost, entry, args) in
Tacenv.register_ltac false false (Names.Id.of_string id) body
in
List.iteri add_atomic entries
let cache_ml_tactic_notation (_, obj) =
extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod
let open_ml_tactic_notation i obj =
if Int.equal i 1 then cache_ml_tactic_notation obj
let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
declare_object { (default_object "MLTacticGrammar") with
open_function = open_ml_tactic_notation;
cache_function = cache_ml_tactic_notation;
classify_function = (fun o -> Substitute o);
subst_function = (fun (_, o) -> o);
}
let add_ml_tactic_notation name prods =
let obj = {
mltacobj_name = name;
mltacobj_prod = prods;
} in
Lib.add_anonymous_leaf (inMLTacticGrammar obj);
extend_atomic_tactic name prods
|
