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/
29 let critical_value = 7
32 module StringSet = Set.Make (String)
33 module SetSet = Set.Make (StringSet)
35 type term_signature = (string * string list) option * StringSet.t
37 type cardinality_condition =
42 type rating_criterion =
43 [ `Hits (** order by number of hits, most used objects first *)
47 (library_obj_tbl,library_rel_tbl,library_sort_tbl,library_count_tbl)
49 let current_tables () =
50 (obj_tbl (),rel_tbl (),sort_tbl (), count_tbl ())
52 let tbln n = "table" ^ string_of_int n
55 let add_depth_constr depth_opt cur_tbl where =
58 | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
61 let mk_positions positions cur_tbl =
66 let pos_str = MetadataPp.pp_position_tag pos in
71 | `MainConclusion None
72 | `MainHypothesis None ->
73 sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
74 | `MainConclusion (Some d)
75 | `MainHypothesis (Some d) ->
76 sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
77 cur_tbl pos_str cur_tbl d)
78 (positions :> MetadataTypes.position list)) ^
81 let explode_card_constr = function
82 | Eq card -> "=", card
83 | Gt card -> ">", card
84 | Lt card -> "<", card
86 let add_card_constr tbl col where = function
89 let op, card = explode_card_constr constr in
90 (* count(_utente).hypothesis = 3 *)
91 (sprintf "%s.%s %s %d" tbl col op card :: where)
93 let add_diff_constr tbl where = function
96 let op, card = explode_card_constr constr in
97 (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where)
99 let add_all_constr ?(tbl=library_count_tbl) (n,from,where) concl full diff =
100 match (concl, full, diff) with
101 | None, None, None -> (n,from,where)
103 let cur_tbl = tbln n in
104 let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
105 let where = add_card_constr cur_tbl "conclusion" where concl in
106 let where = add_card_constr cur_tbl "statement" where full in
107 let where = add_diff_constr cur_tbl where diff in
110 sprintf "table0.source = %s.source" cur_tbl :: where
115 let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
116 let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables
118 let cur_tbl = tbln n in
119 let start_table = tbln start in
121 | `Obj (uri, positions) ->
122 let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
124 (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
125 mk_positions positions cur_tbl ::
127 else [sprintf "%s.source = %s.source" start_table cur_tbl]) @
132 let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
134 mk_positions positions cur_tbl ::
136 else [sprintf "%s.source = %s.source" start_table cur_tbl]) @
140 | `Sort (sort, positions) ->
141 let sort_str = CicPp.ppsort sort in
142 let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
144 (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
145 mk_positions positions cur_tbl ::
149 [sprintf "%s.source = %s.source" start_table cur_tbl ]) @ where
153 let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) =
154 let from = String.concat ", " from in
155 let where = String.concat " and " where in
158 | None -> sprintf "select table0.source from %s where %s" from where
161 ("select table0.source from %s, hits where %s
162 and table0.source = hits.source order by hits.no desc")
166 let result = Mysql.exec dbd query in
168 (fun row -> match row.(0) with Some s -> s | _ -> assert false)
171 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
172 (metadata: MetadataTypes.constr list)
174 let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables
176 if (metadata = []) && concl_card = None && full_card = None then
177 failwith "MetadataQuery.at_least: no constraints given";
179 List.fold_left (add_constraint ~tables) (0,[],[]) metadata
182 add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
184 exec ~dbd ?rating (n,from,where)
187 ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating
188 (metadata: MetadataTypes.constr list)
190 if are_tables_ownerized () then
192 ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
194 ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
197 ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata
200 (** Prefix handling *)
202 let filter_by_card n =
203 SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
206 let init = SetSet.union a b in
207 let merge_single_set s1 b =
209 (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
212 SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
216 let rec inspect_children n childs =
218 (fun res term -> merge n (inspect_conclusion n term) res)
221 and add_root n root childs =
222 let childunion = inspect_children n childs in
223 let addroot = StringSet.add root in
225 (fun child newsets -> SetSet.add (addroot child) newsets)
227 (SetSet.singleton (StringSet.singleton root))
229 and inspect_conclusion n t =
230 if n = 0 then SetSet.empty
235 | Cic.Implicit _ -> SetSet.empty
236 | Cic.Var (u,exp_named_subst) -> SetSet.empty
237 | Cic.Const (u,exp_named_subst) ->
238 SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
239 | Cic.MutInd (u, t, exp_named_subst) ->
240 SetSet.singleton (StringSet.singleton
241 (UriManager.string_of_uriref (u, [t])))
242 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
243 SetSet.singleton (StringSet.singleton
244 (UriManager.string_of_uriref (u, [t; c])))
245 | Cic.Cast (t, _) -> inspect_conclusion n t
246 | Cic.Prod (_, s, t) ->
247 merge n (inspect_conclusion n s) (inspect_conclusion n t)
248 | Cic.Lambda (_, s, t) ->
249 merge n (inspect_conclusion n s) (inspect_conclusion n t)
250 | Cic.LetIn (_, s, t) ->
251 merge n (inspect_conclusion n s) (inspect_conclusion n t)
252 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
253 let suri = UriManager.string_of_uri u in
254 add_root (n-1) suri l
255 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
256 let suri = UriManager.string_of_uriref (u, [t]) in
257 add_root (n-1) suri l
258 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
259 let suri = UriManager.string_of_uriref (u, [t; c]) in
260 add_root (n-1) suri l
263 | Cic.MutCase (u, t, tt, uu, m) ->
267 | Cic.CoFix (_, m) ->
270 let rec inspect_term n t =
278 | Cic.Implicit _ -> None, SetSet.empty
279 | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
280 | Cic.Const (u,exp_named_subst) ->
281 Some (UriManager.string_of_uri u), SetSet.empty
282 | Cic.MutInd (u, t, exp_named_subst) ->
283 let uri = UriManager.string_of_uriref (u, [t]) in
284 Some uri, SetSet.empty
285 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
286 let uri = UriManager.string_of_uriref (u, [t; c]) in
287 Some uri, SetSet.empty
288 | Cic.Cast (t, _) -> inspect_term n t
289 | Cic.Prod (_, _, t) -> inspect_term n t
290 | Cic.LetIn (_, _, t) -> inspect_term n t
291 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
292 let suri = UriManager.string_of_uri u in
293 let childunion = inspect_children (n-1) l in
294 Some suri, childunion
295 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
296 let suri = UriManager.string_of_uriref (u, [t]) in
297 if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
298 (* equality is handled in a special way: in particular,
299 the type, if defined, is always added to the prefix,
300 and n is not decremented - it should have been n-2 *)
302 Cic.Const (u1,exp_named_subst1)::l1 ->
303 let suri1 = UriManager.string_of_uri u1 in
304 let inconcl = add_root (n-1) suri1 l1 in
306 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
307 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
308 let inconcl = add_root (n-1) suri1 l1 in
310 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
311 let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
312 let inconcl = add_root (n-1) suri1 l1 in
314 | _ :: _ -> Some suri, SetSet.empty
315 | _ -> assert false (* args number must be > 0 *)
317 let childunion = inspect_children (n-1) l in
318 Some suri, childunion
319 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
320 let suri = UriManager.string_of_uriref (u, [t; c]) in
321 let childunion = inspect_children (n-1) l in
322 Some suri, childunion
323 | _ -> None, SetSet.empty
325 let add_cardinality s =
326 let l = SetSet.elements s in
330 let el = StringSet.elements set in
331 (List.length el, el)) l in
332 (* ordered by descending cardinality *)
333 List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
336 match inspect_term n t with
337 Some a, set -> Some a, add_cardinality set
338 | None, set when (SetSet.is_empty set) -> None, []
339 | _, _ -> assert false
342 let rec add children =
344 (fun acc t -> StringSet.union (signature_concl t) acc)
345 (StringSet.empty) children
347 (* this function creates the set of all different constants appearing in
348 the conclusion of the term *)
349 and signature_concl =
354 | Cic.Implicit _ -> StringSet.empty
355 | Cic.Var (u,exp_named_subst) -> StringSet.empty
356 | Cic.Const (u,exp_named_subst) ->
357 StringSet.singleton (UriManager.string_of_uri u)
358 | Cic.MutInd (u, t, exp_named_subst) ->
359 let uri = UriManager.string_of_uriref (u, [t]) in
360 StringSet.singleton uri
361 | Cic.MutConstruct (u, t, c, exp_named_subst) ->
362 let uri = UriManager.string_of_uriref (u, [t;c]) in
363 StringSet.singleton uri
364 | Cic.Cast (t, _) -> signature_concl t
365 | Cic.Prod (_, s, t) ->
366 StringSet.union (signature_concl s) (signature_concl t)
367 | Cic.Lambda (_, s, t) ->
368 StringSet.union (signature_concl s) (signature_concl t)
369 | Cic.LetIn (_, s, t) ->
370 StringSet.union (signature_concl s) (signature_concl t)
371 | Cic.Appl l -> add l
377 let rec signature_of = function
378 | Cic.Cast (t, _) -> signature_of t
379 | Cic.Prod (_, _, t) -> signature_of t
380 | Cic.LetIn (_, _, t) -> signature_of t
381 | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
382 let suri = UriManager.string_of_uri u in
383 Some (suri, []), add l
384 | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
385 let suri = UriManager.string_of_uriref (u, [t]) in
386 if u = HelmLibraryObjects.Logic.eq_URI then
387 (* equality is handled in a special way: in particular,
388 the type, if defined, is always added to the prefix,
389 and n is not decremented - it should have been n-2 *)
391 Cic.Const (u1,exp_named_subst1)::l1 ->
392 let suri1 = UriManager.string_of_uri u1 in
393 let inconcl = StringSet.remove suri1 (add l1) in
394 Some (suri, [suri1]), inconcl
395 | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
396 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
397 let inconcl = StringSet.remove suri1 (add l1) in
398 Some (suri, [suri1]), inconcl
399 | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
400 let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
401 let inconcl = StringSet.remove suri1 (add l1) in
402 Some (suri, [suri1]), inconcl
403 | _ :: _ -> Some (suri, []), StringSet.empty
404 | _ -> assert false (* args number must be > 0 *)
406 Some (suri, []), add l
407 | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) ->
408 let suri = UriManager.string_of_uriref (u, [t;c]) in
409 Some (suri, []), add l
410 | t -> None, signature_concl t
412 (* takes a list of lists and returns the list of all elements
413 without repetitions *)
415 let rec drop_repetitions = function
418 | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
419 | u::l -> u::(drop_repetitions l) in
420 drop_repetitions (List.sort Pervasives.compare (List.concat l))
422 let must_of_prefix ?(where = `Conclusion) m s =
425 | `Conclusion -> [`InConclusion]
426 | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
428 let s' = List.map (fun u -> `Obj (u, positions)) s in
429 `Obj (m, [`MainConclusion None]) :: s'
431 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
433 let get_constants (dbd:Mysql.dbd) ~where uri =
434 let uri = escape uri in
437 | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
439 [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
440 MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
445 (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
447 sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
448 "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
449 (MetadataTypes.obj_tbl ()) uri pos_predicate
450 MetadataTypes.library_obj_tbl uri pos_predicate
453 let result = Mysql.exec dbd query in
454 let set = ref StringSet.empty in
458 | Some uri -> set := StringSet.add uri !set
459 | _ -> assert false);
462 let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
463 let inconcl = get_constants dbd ~where u in
464 StringSet.subset inconcl only
466 (* Special handling of equality. The problem is filtering out theorems just
467 * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
468 * ad-hoc, no better solution found at the moment *)
469 let myspeciallist_of_facts =
470 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
472 [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
473 (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
474 0,"cic:/Coq/Init/Logic/trans_eq.con";
475 0,"cic:/Coq/Init/Logic/f_equal.con";
476 0,"cic:/Coq/Init/Logic/f_equal2.con";
477 0,"cic:/Coq/Init/Logic/f_equal3.con"]
480 let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
484 if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
485 (if facts then myspeciallist_of_facts
489 let must = must_of_prefix ~where main s in
491 | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
492 | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
494 List.map (fun uri -> (m, uri)) res)
497 (* critical value reached, fallback to "only" constraints *)
499 let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
500 main prefixes constants
502 let max_prefix_length =
505 | (max,_)::_ -> max in
506 let maximal_prefixes =
507 let rec filter res = function
509 | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
511 filter [] prefixes in
517 let must = must_of_prefix ~where main s in
520 | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
521 | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
523 (* we tag the uri with m+1, for sorting purposes *)
524 List.map (fun uri -> (m+1, uri)) res))
527 List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
528 let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
529 greater_than @ equal_to
531 (* real match query implementation *)
533 let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t =
534 let (main, constants) = signature_of t in
537 | Some (main, types) ->
538 (* the type of eq is not counted in constants_no *)
539 let types_no = List.length types in
540 let constants_no = StringSet.cardinal constants in
541 if (constants_no > critical_value) then
542 let prefixes = prefixes just_factor t in
544 | Some main, all_concl ->
546 List.fold_right StringSet.add types (StringSet.add main constants)
548 compute_with_only ~dbd ~facts main all_concl all_constants
551 (* in this case we compute all prefixes, and we do not need
552 to apply the only constraints *)
554 if constants_no = 0 then
555 (if types_no = 0 then
558 Some main, [0, []; types_no, types])
560 prefixes (constants_no+types_no+1) t
563 Some main, all_concl ->
564 compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
569 let must = must_of_prefix ~where:`Conclusion main s in
570 let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
571 List.map (fun uri -> (m, uri)) res)
575 let power_upto upto consts =
576 let l = StringSet.elements consts in
577 List.sort (fun (n,_) (m,_) -> m - n)
580 List.filter (function (n,l) -> n <= upto)
581 res@(List.map (function (n,l) -> (n+1,a::l)) res))
585 let l = StringSet.elements consts in
586 List.sort (fun (n,_) (m,_) -> m - n)
588 (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
591 type where = [ `Conclusion | `Statement ]
593 let sigmatch ~(dbd:Mysql.dbd)
594 ?(facts=false) ?(where = `Conclusion) (main, constants) =
597 | Some (main, types) ->
598 let constants_no = StringSet.cardinal constants in
599 if (constants_no > critical_value) then
601 let subsets = power_upto just_factor constants in
602 let types_no = List.length types in
603 List.map (function (n,l) -> (n+types_no,types@l)) subsets
606 List.fold_right StringSet.add types (StringSet.add main constants)
608 compute_with_only ~dbd ~where main subsets all_constants
611 let subsets = power constants in
612 let types_no = List.length types in
614 (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
617 compute_exactly ~dbd ~facts ~where main subsets
619 (* match query wrappers *)
623 let cmatch ~dbd ?(facts=false) term =
626 (fun x y -> Pervasives.compare (fst y) (fst x))
627 (cmatch' ~dbd ~facts term))
629 let constants_of = signature_concl