1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 let critical_value = 7
31 module StringSet = Set.Make (String)
32 module SetSet = Set.Make (StringSet)
34 type term_signature = (string * string list) option * StringSet.t
36 type cardinality_condition =
40 let tbln n = "table" ^ string_of_int n
43 let add_depth_constr depth_opt cur_tbl where =
46 | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
49 let mk_positions positions cur_tbl =
54 let pos_str = MetadataPp.pp_position_tag pos in
59 | `MainConclusion None
60 | `MainHypothesis None ->
61 sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
62 | `MainConclusion (Some d)
63 | `MainHypothesis (Some d) ->
64 sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
65 cur_tbl pos_str cur_tbl d)
66 (positions :> MetadataTypes.position list)) ^
69 let add_card_constr tbl (n,from,where) = function
70 | None -> (n,from,where)
72 let cur_tbl = tbln n in
74 (sprintf "%s as %s" tbl cur_tbl :: from),
75 (sprintf "%s.no=%d" cur_tbl card ::
77 else [sprintf "table0.source = %s.source" cur_tbl]) @
80 let cur_tbl = tbln n in
82 (sprintf "%s as %s" tbl cur_tbl :: from),
83 (sprintf "%s.no>%d" cur_tbl card ::
85 else [sprintf "table0.source = %s.source" cur_tbl]) @
88 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
89 (metadata: MetadataTypes.constr list)
91 if (metadata = []) && concl_card = None && full_card = None then
92 failwith "MetadataQuery.at_least: no constraints given";
93 let add_constraint (n,from,where) metadata =
94 let cur_tbl = tbln n in
95 let cur_ltbl = tbln (n+1) in
97 | `Obj (uri, positions) ->
98 let tbl = MetadataTypes.obj_tbl () in
99 let ltbl = MetadataTypes.library_obj_tbl in
101 (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from
104 (sprintf "(%s.h_occurrence = \"%s\" OR %s.h_occurrence = \"%s\")"
105 cur_tbl uri cur_ltbl uri) ::
106 mk_positions positions cur_tbl ::
109 "(table0.source = %s.source OR table0.source = %s.source)"
110 cur_tbl cur_ltbl]) @ where
114 let tbl = MetadataTypes.rel_tbl () in
115 let ltbl = MetadataTypes.library_rel_tbl in
117 (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from
120 mk_positions positions cur_tbl ::
123 "(table0.source = %s.source OR table0.source = %s.source)"
124 cur_tbl cur_ltbl]) @ where
127 | `Sort (sort, positions) ->
128 let tbl = MetadataTypes.sort_tbl () in
129 let ltbl = MetadataTypes.library_sort_tbl in
130 let sort_str = CicPp.ppsort sort in
132 (sprintf "%s AS %s, %s AS %s" tbl cur_tbl ltbl cur_ltbl) :: from
135 (sprintf "(%s.h_sort = \"%s\" OR %s.h_sort = \"%s\")"
136 cur_tbl sort_str cur_ltbl sort_str) ::
137 mk_positions positions cur_tbl ::
142 "(table0.source = %s.source OR table0.source = %s.source)"
143 cur_tbl cur_ltbl]) @ where
147 let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
149 add_card_constr (MetadataTypes.conclno_tbl ()) (n,from,where) concl_card
152 add_card_constr (MetadataTypes.conclno_hyp_tbl ()) (n,from,where) full_card
154 let from = String.concat ", " from in
155 let where = String.concat " and " where in
156 let query = sprintf "select table0.source from %s where %s" from where in
157 let result = Mysql.exec dbd query in
159 (fun row -> match row.(0) with Some s -> s | _ -> assert false)
161 (** Prefix handling *)
163 let filter_by_card n =
164 SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
167 let init = SetSet.union a b in
168 let merge_single_set s1 b =
170 (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
173 SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
177 let rec inspect_children n childs =
179 (fun res term -> merge n (inspect_conclusion n term) res)
182 and add_root n root childs =
183 let childunion = inspect_children n childs in
184 let addroot = StringSet.add root in
186 (fun child newsets -> SetSet.add (addroot child) newsets)
188 (SetSet.singleton (StringSet.singleton root))
190 and inspect_conclusion n t =
191 if n = 0 then SetSet.empty
196 | Cic.Implicit _ -> SetSet.empty
197 | Cic.Var (u,exp_named_subst) -> SetSet.empty
198 | Cic.Const (u,exp_named_subst) ->
199 SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
200 | Cic.MutInd (u, t, exp_named_subst) ->
201 SetSet.singleton (StringSet.singleton
202 (UriManager.string_of_uriref (u, [t])))
203 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
204 SetSet.singleton (StringSet.singleton
205 (UriManager.string_of_uriref (u, [t; c])))
206 | Cic.Cast (t, _) -> inspect_conclusion n t
207 | Cic.Prod (_, s, t) ->
208 merge n (inspect_conclusion n s) (inspect_conclusion n t)
209 | Cic.Lambda (_, s, t) ->
210 merge n (inspect_conclusion n s) (inspect_conclusion n t)
211 | Cic.LetIn (_, s, t) ->
212 merge n (inspect_conclusion n s) (inspect_conclusion n t)
213 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
214 let suri = UriManager.string_of_uri u in
215 add_root (n-1) suri l
216 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
217 let suri = UriManager.string_of_uriref (u, [t]) in
218 add_root (n-1) suri l
219 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
220 let suri = UriManager.string_of_uriref (u, [t; c]) in
221 add_root (n-1) suri l
224 | Cic.MutCase (u, t, tt, uu, m) ->
228 | Cic.CoFix (_, m) ->
231 let rec inspect_term n t =
239 | Cic.Implicit _ -> None, SetSet.empty
240 | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
241 | Cic.Const (u,exp_named_subst) ->
242 Some (UriManager.string_of_uri u), SetSet.empty
243 | Cic.MutInd (u, t, exp_named_subst) ->
244 let uri = UriManager.string_of_uriref (u, [t]) in
245 Some uri, SetSet.empty
246 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
247 let uri = UriManager.string_of_uriref (u, [t; c]) in
248 Some uri, SetSet.empty
249 | Cic.Cast (t, _) -> inspect_term n t
250 | Cic.Prod (_, _, t) -> inspect_term n t
251 | Cic.LetIn (_, _, t) -> inspect_term n t
252 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
253 let suri = UriManager.string_of_uri u in
254 let childunion = inspect_children (n-1) l in
255 Some suri, childunion
256 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
257 let suri = UriManager.string_of_uriref (u, [t]) in
258 if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
259 (* equality is handled in a special way: in particular,
260 the type, if defined, is always added to the prefix,
261 and n is not decremented - it should have been n-2 *)
263 Cic.Const (u1,exp_named_subst1)::l1 ->
264 let suri1 = UriManager.string_of_uri u1 in
265 let inconcl = add_root (n-1) suri1 l1 in
267 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
268 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
269 let inconcl = add_root (n-1) suri1 l1 in
271 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
272 let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
273 let inconcl = add_root (n-1) suri1 l1 in
275 | _ :: _ -> Some suri, SetSet.empty
276 | _ -> assert false (* args number must be > 0 *)
278 let childunion = inspect_children (n-1) l in
279 Some suri, childunion
280 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
281 let suri = UriManager.string_of_uriref (u, [t; c]) in
282 let childunion = inspect_children (n-1) l in
283 Some suri, childunion
284 | _ -> None, SetSet.empty
286 let add_cardinality s =
287 let l = SetSet.elements s in
291 let el = StringSet.elements set in
292 (List.length el, el)) l in
293 (* ordered by descending cardinality *)
294 List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
297 match inspect_term n t with
298 Some a, set -> Some a, add_cardinality set
299 | None, set when (SetSet.is_empty set) -> None, []
300 | _, _ -> assert false
303 let rec add children =
305 (fun acc t -> StringSet.union (signature_concl t) acc)
306 (StringSet.empty) children
308 (* this function creates the set of all different constants appearing in
309 the conclusion of the term *)
310 and signature_concl =
315 | Cic.Implicit _ -> StringSet.empty
316 | Cic.Var (u,exp_named_subst) -> StringSet.empty
317 | Cic.Const (u,exp_named_subst) ->
318 StringSet.singleton (UriManager.string_of_uri u)
319 | Cic.MutInd (u, t, exp_named_subst) ->
320 let uri = UriManager.string_of_uriref (u, [t]) in
321 StringSet.singleton uri
322 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
323 let uri = UriManager.string_of_uriref (u, [t;c]) in
324 StringSet.singleton uri
325 | Cic.Cast (t, _) -> signature_concl t
326 | Cic.Prod (_, s, t) ->
327 StringSet.union (signature_concl s) (signature_concl t)
328 | Cic.Lambda (_, s, t) ->
329 StringSet.union (signature_concl s) (signature_concl t)
330 | Cic.LetIn (_, s, t) ->
331 StringSet.union (signature_concl s) (signature_concl t)
332 | Cic.Appl l -> add l
338 let rec signature_of = function
339 | Cic.Cast (t, _) -> signature_of t
340 | Cic.Prod (_, _, t) -> signature_of t
341 | Cic.LetIn (_, _, t) -> signature_of t
342 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
343 let suri = UriManager.string_of_uri u in
344 Some (suri, []), add l
345 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
346 let suri = UriManager.string_of_uriref (u, [t]) in
347 if u = HelmLibraryObjects.Logic.eq_URI then
348 (* equality is handled in a special way: in particular,
349 the type, if defined, is always added to the prefix,
350 and n is not decremented - it should have been n-2 *)
352 Cic.Const (u1,exp_named_subst1)::l1 ->
353 let suri1 = UriManager.string_of_uri u1 in
354 let inconcl = StringSet.remove suri1 (add l1) in
355 Some (suri, [suri1]), inconcl
356 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
357 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
358 let inconcl = StringSet.remove suri1 (add l1) in
359 Some (suri, [suri1]), inconcl
360 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
361 let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
362 let inconcl = StringSet.remove suri1 (add l1) in
363 Some (suri, [suri1]), inconcl
364 | _ :: _ -> Some (suri, []), StringSet.empty
365 | _ -> assert false (* args number must be > 0 *)
367 Some (suri, []), add l
368 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
369 let suri = UriManager.string_of_uriref (u, [t;c]) in
370 Some (suri, []), add l
371 | t -> None, signature_concl t
373 (* takes a list of lists and returns the list of all elements
374 without repetitions *)
376 let rec drop_repetitions = function
379 | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
380 | u::l -> u::(drop_repetitions l) in
381 drop_repetitions (List.sort Pervasives.compare (List.concat l))
383 let must_of_prefix ?(where = `Conclusion) m s =
386 | `Conclusion -> [`InConclusion]
387 | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
389 let s' = List.map (fun u -> `Obj (u, positions)) s in
390 `Obj (m, [`MainConclusion None]) :: s'
392 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
394 let get_constants (dbd:Mysql.dbd) ~where uri =
395 let uri = escape uri in
398 | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""]
400 ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\"";
401 "\"MainHypothesis\""]
404 sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION"^^
405 "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
406 (MetadataTypes.obj_tbl ()) uri (String.concat " OR " positions)
407 MetadataTypes.library_obj_tbl uri (String.concat " OR " positions)
410 let result = Mysql.exec dbd query in
411 let set = ref StringSet.empty in
415 | Some uri -> set := StringSet.add uri !set
416 | _ -> assert false);
419 let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
420 let inconcl = get_constants dbd ~where u in
421 StringSet.subset inconcl only
423 (* Special handling of equality. The problem is filtering out theorems just
424 * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
425 * ad-hoc, no better solution found at the moment *)
426 let myspeciallist_of_facts =
427 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
429 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
430 (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
431 0,"cic:/Coq/Init/Logic/trans_eq.con";
432 0,"cic:/Coq/Init/Logic/f_equal.con";
433 0,"cic:/Coq/Init/Logic/f_equal2.con";
434 0,"cic:/Coq/Init/Logic/f_equal3.con"]
437 let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
441 if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
442 (if facts then myspeciallist_of_facts
446 let must = must_of_prefix ~where main s in
448 | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
449 | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
451 List.map (fun uri -> (m, uri)) res)
454 (* critical value reached, fallback to "only" constraints *)
456 let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
457 main prefixes constants
459 let max_prefix_length =
462 | (max,_)::_ -> max in
463 let maximal_prefixes =
464 let rec filter res = function
466 | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
468 filter [] prefixes in
474 let must = must_of_prefix ~where main s in
477 | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
478 | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
480 (* we tag the uri with m+1, for sorting purposes *)
481 List.map (fun uri -> (m+1, uri)) res))
484 List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
485 let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
486 greater_than @ equal_to
488 (* real match query implementation *)
490 let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t =
491 let (main, constants) = signature_of t in
494 | Some (main, types) ->
495 (* the type of eq is not counted in constants_no *)
496 let types_no = List.length types in
497 let constants_no = StringSet.cardinal constants in
498 if (constants_no > critical_value) then
499 let prefixes = prefixes just_factor t in
501 | Some main, all_concl ->
503 List.fold_right StringSet.add types (StringSet.add main constants)
505 compute_with_only ~dbd ~facts main all_concl all_constants
508 (* in this case we compute all prefixes, and we do not need
509 to apply the only constraints *)
511 if constants_no = 0 then
512 (if types_no = 0 then
515 Some main, [0, []; types_no, types])
517 prefixes (constants_no+types_no+1) t
520 Some main, all_concl ->
521 compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
526 let must = must_of_prefix ~where:`Conclusion main s in
527 let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
528 List.map (fun uri -> (m, uri)) res)
532 let power_upto upto consts =
533 let l = StringSet.elements consts in
534 List.sort (fun (n,_) (m,_) -> m - n)
537 List.filter (function (n,l) -> n <= upto)
538 res@(List.map (function (n,l) -> (n+1,a::l)) res))
542 let l = StringSet.elements consts in
543 List.sort (fun (n,_) (m,_) -> m - n)
545 (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
548 type where = [ `Conclusion | `Statement ]
550 let sigmatch ~(dbd:Mysql.dbd)
551 ?(facts=false) ?(where = `Conclusion) (main, constants) =
554 | Some (main, types) ->
555 let constants_no = StringSet.cardinal constants in
556 if (constants_no > critical_value) then
558 let subsets = power_upto just_factor constants in
559 let types_no = List.length types in
560 List.map (function (n,l) -> (n+types_no,types@l)) subsets
563 List.fold_right StringSet.add types (StringSet.add main constants)
565 compute_with_only ~dbd ~where main subsets all_constants
568 let subsets = power constants in
569 let types_no = List.length types in
571 (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
574 compute_exactly ~dbd ~facts ~where main subsets
576 (* match query wrappers *)
580 let cmatch ~dbd ?(facts=false) term =
583 (fun x y -> Pervasives.compare (fst y) (fst x))
584 (cmatch' ~dbd ~facts term))
586 let constants_of = signature_concl