Source file search.ml
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
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
open Pp
open Util
open Names
open Constr
open Declarations
open Libobject
open Environ
open Pattern
open Libnames
open Vernacexpr
module NamedDecl = Context.Named.Declaration
type filter_function =
GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool
type display_function =
GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit
type glob_search_item =
| GlobSearchSubPattern of glob_search_where * bool * constr_pattern
| GlobSearchString of string
| GlobSearchKind of Decls.logical_kind
| GlobSearchFilter of (GlobRef.t -> bool)
type glob_search_request =
| GlobSearchLiteral of glob_search_item
| GlobSearchDisjConj of (bool * glob_search_request) list list
module SearchBlacklist =
Goptions.MakeStringTable
(struct
let key = ["Search";"Blacklist"]
let title = "Current search blacklist : "
let member_message s b =
str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s
end)
let iter_constructors indsp u fn env nconstr =
for i = 1 to nconstr do
let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in
fn (GlobRef.ConstructRef (indsp, i)) None env typ
done
module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end)
let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
| f -> f o
| exception Not_found -> ()
let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) =
List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) None env (NamedDecl.get_type d))
(Environ.named_context env);
let iter_obj prefix lobj = match lobj with
| AtomicObject o ->
let handler =
DynHandle.add Declare.Internal.Constant.tag begin fun (id,obj) ->
let kn = KerName.make prefix.Nametab.obj_mp (Label.of_id id) in
let cst = Global.constant_of_delta_kn kn in
let gr = GlobRef.ConstRef cst in
let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
let kind = Declare.Internal.Constant.kind obj in
fn gr (Some kind) env typ
end @@
DynHandle.add DeclareInd.Internal.objInductive begin fun (id,_) ->
let kn = KerName.make prefix.Nametab.obj_mp (Label.of_id id) in
let mind = Global.mind_of_delta_kn kn in
let mib = Global.lookup_mind mind in
let iter_packet i mip =
let ind = (mind, i) in
let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
let i = (ind, u) in
let typ = Inductiveops.type_of_inductive env i in
let () = fn (GlobRef.IndRef ind) None env typ in
let len = Array.length mip.mind_user_lc in
iter_constructors ind u fn env len
in
Array.iteri iter_packet mib.mind_packets
end @@
DynHandle.empty
in
handle handler o
| _ -> ()
in
try Declaremods.iter_all_segments iter_obj
with Not_found -> ()
(** This module defines a preference on constrs in the form of a
[compare] function (preferred constr must be big for this
functions, so preferences such as small constr must use a reversed
order). This priority will be used to order search results and
propose first results which are more likely to be relevant to the
query, this is why the type [t] contains the other elements
required of a search. *)
module ConstrPriority = struct
type t = GlobRef.t * Decls.logical_kind option * Environ.env * Constr.t * priority
and priority = int
module ConstrSet = CSet.Make(Constr)
(** A measure of the size of a term *)
let rec size t =
Constr.fold (fun s t -> 1 + s + size t) 0 t
(** Set of the "symbols" (definitions, inductives, constructors)
which appear in a term. *)
let rec symbols acc t =
let open Constr in
match kind t with
| Const _ | Ind _ | Construct _ -> ConstrSet.add t acc
| _ -> Constr.fold symbols acc t
(** The number of distinct "symbols" (see {!symbols}) which appear
in a term. *)
let num_symbols t =
ConstrSet.(cardinal (symbols empty t))
let priority gref t : priority =
-(3*(num_symbols t) + size t)
let compare (_,_,_,_,p1) (_,_,_,_,p2) =
pervasives_compare p1 p2
end
module PriorityQueue = Heap.Functional(ConstrPriority)
let rec iter_priority_queue q fn =
match PriorityQueue.maximum q with
| (gref,kind,env,t,_) ->
fn gref kind env t;
iter_priority_queue (PriorityQueue.remove q) fn
| exception Heap.EmptyHeap -> ()
let prioritize_search seq fn =
let acc = ref PriorityQueue.empty in
let iter gref kind env t =
let p = ConstrPriority.priority gref t in
acc := PriorityQueue.add (gref,kind,env,t,p) !acc
in
let () = seq iter in
iter_priority_queue !acc fn
(** Filters *)
(** This function tries to see whether the conclusion matches a pattern.
FIXME: this is quite dummy, we may find a more efficient algorithm. *)
let rec pattern_filter pat ref env sigma typ =
let typ = Termops.strip_outer_cast sigma typ in
if Constr_matching.is_matching env sigma pat typ then true
else match EConstr.kind sigma typ with
| Prod (_, _, typ)
| LetIn (_, _, _, typ) -> pattern_filter pat ref env sigma typ
| _ -> false
let full_name_of_reference ref =
let (dir,id) = repr_path (Nametab.path_of_global ref) in
DirPath.to_string dir ^ "." ^ Id.to_string id
(** Whether a reference is blacklisted *)
let blacklist_filter ref kind env sigma typ =
let name = full_name_of_reference ref in
let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
CString.Set.for_all is_not_bl (SearchBlacklist.v ())
let module_filter (mods, outside) ref kind env sigma typ =
let sp = Nametab.path_of_global ref in
let sl = dirpath sp in
let is_outside md = not (is_dirpath_prefix_of md sl) in
let is_inside md = is_dirpath_prefix_of md sl in
if outside then List.for_all is_outside mods
else List.is_empty mods || List.exists is_inside mods
let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref)
let search_filter query gr kind env sigma typ = match query with
| GlobSearchSubPattern (where,head,pat) ->
let open Context.Rel.Declaration in
let rec collect env hyps typ =
match Constr.kind typ with
| LetIn (na,b,t,c) -> collect (push_rel (LocalDef (na,b,t)) env) ((env,b) :: (env,t) :: hyps) c
| Prod (na,t,c) -> collect (push_rel (LocalAssum (na,t)) env) ((env,t) :: hyps) c
| _ -> (hyps,(env,typ)) in
let typl= match where with
| InHyp -> fst (collect env [] typ)
| InConcl -> [snd (collect env [] typ)]
| Anywhere -> if head then let hyps, ccl = collect env [] typ in ccl :: hyps else [env,typ] in
List.exists (fun (env,typ) ->
let f =
if head then Constr_matching.is_matching_head
else Constr_matching.is_matching_appsubterm ~closed:false in
f env sigma pat (EConstr.of_constr typ)) typl
| GlobSearchString s ->
String.string_contains ~where:(name_of_reference gr) ~what:s
| GlobSearchKind k -> (match kind with None -> false | Some k' -> k = k')
| GlobSearchFilter f -> f gr
(** SearchPattern *)
let search_pattern env sigma pat mods pr_search =
let filter ref kind env typ =
module_filter mods ref kind env sigma typ &&
pattern_filter pat ref env sigma (EConstr.of_constr typ) &&
blacklist_filter ref kind env sigma typ
in
let iter ref kind env typ =
if filter ref kind env typ then pr_search ref kind env typ
in
generic_search env iter
(** SearchRewrite *)
let eq () = Coqlib.(lib_ref "core.eq.type")
let rewrite_pat1 pat =
PApp (PRef (eq ()), [| PMeta None; pat; PMeta None |])
let rewrite_pat2 pat =
PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |])
let search_rewrite env sigma pat mods pr_search =
let pat1 = rewrite_pat1 pat in
let pat2 = rewrite_pat2 pat in
let filter ref kind env typ =
module_filter mods ref kind env sigma typ &&
(pattern_filter pat1 ref env sigma (EConstr.of_constr typ) ||
pattern_filter pat2 ref env sigma (EConstr.of_constr typ)) &&
blacklist_filter ref kind env sigma typ
in
let iter ref kind env typ =
if filter ref kind env typ then pr_search ref kind env typ
in
generic_search env iter
(** Search *)
let search env sigma items mods pr_search =
let filter ref kind env typ =
let eqb b1 b2 = if b1 then b2 else not b2 in
module_filter mods ref kind env sigma typ &&
let rec aux = function
| GlobSearchLiteral i -> search_filter i ref kind env sigma typ
| GlobSearchDisjConj l -> List.exists (List.for_all aux') l
and aux' (b,s) = eqb b (aux s) in
List.for_all aux' items && blacklist_filter ref kind env sigma typ
in
let iter ref kind env typ =
if filter ref kind env typ then pr_search ref kind env typ
in
generic_search env iter
type search_constraint =
| Name_Pattern of Str.regexp
| Type_Pattern of Pattern.constr_pattern
| SubType_Pattern of Pattern.constr_pattern
| In_Module of Names.DirPath.t
| Include_Blacklist
type 'a coq_object = {
coq_object_prefix : string list;
coq_object_qualid : string list;
coq_object_object : 'a;
}
let interface_search env sigma =
let rec name tpe subtpe mods blacklist = function
| [] -> (name, tpe, subtpe, mods, blacklist)
| (Name_Pattern regexp, b) :: l ->
extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
| (Type_Pattern pat, b) :: l ->
extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
| (SubType_Pattern pat, b) :: l ->
extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
| (In_Module id, b) :: l ->
extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
| (Include_Blacklist, b) :: l ->
extract_flags name tpe subtpe mods b l
in
fun flags ->
let (name, tpe, subtpe, mods, blacklist) =
extract_flags [] [] [] [] false flags
in
let filter_function ref env constr =
let id = Names.Id.to_string (Nametab.basename_of_global ref) in
let path = Libnames.dirpath (Nametab.path_of_global ref) in
let toggle x b = if x then b else not b in
let match_name (regexp, flag) =
toggle (Str.string_match regexp id 0) flag
in
let match_type (pat, flag) =
toggle (Constr_matching.is_matching env sigma pat (EConstr.of_constr constr)) flag
in
let match_subtype (pat, flag) =
toggle
(Constr_matching.is_matching_appsubterm ~closed:false
env sigma pat (EConstr.of_constr constr)) flag
in
let match_module (mdl, flag) =
toggle (Libnames.is_dirpath_prefix_of mdl path) flag
in
List.for_all match_name name &&
List.for_all match_type tpe &&
List.for_all match_subtype subtpe &&
List.for_all match_module mods &&
(blacklist || blacklist_filter ref kind env sigma constr)
in
let ans = ref [] in
let print_function ref env constr =
let fullpath = DirPath.repr (Nametab.dirpath_of_global ref) in
let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
let (shortpath, basename) = Libnames.repr_qualid qualid in
let shortpath = DirPath.repr shortpath in
let rec prefix full short accu = match full, short with
| _, [] ->
let full = List.rev_map Id.to_string full in
(full, accu)
| _ :: full, m :: short ->
prefix full short (Id.to_string m :: accu)
| _ -> assert false
in
let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in
let answer = {
coq_object_prefix = prefix;
coq_object_qualid = qualid;
coq_object_object = constr;
} in
ans := answer :: !ans;
in
let iter ref kind env typ =
if filter_function ref env typ then print_function ref env typ
in
let () = generic_search env iter in
!ans