]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/metadata/metadataConstraints.ml
aded prifiler factory
[helm.git] / helm / ocaml / metadata / metadataConstraints.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open Printf
27 open MetadataTypes 
28
29 let critical_value = 7
30 let just_factor = 4
31
32 module UriManagerSet = UriManager.UriSet
33 module SetSet = Set.Make (UriManagerSet)
34
35 type term_signature = (UriManager.uri * UriManager.uri list) option * UriManagerSet.t
36
37 type cardinality_condition =
38   | Eq of int
39   | Gt of int
40   | Lt of int
41
42 type rating_criterion =
43   [ `Hits   (** order by number of hits, most used objects first *)
44   ]
45
46 let default_tables =
47    (library_obj_tbl,library_rel_tbl,library_sort_tbl,library_count_tbl)
48
49 let current_tables () = 
50   (obj_tbl (),rel_tbl (),sort_tbl (), count_tbl ())
51
52 let tbln n = "table" ^ string_of_int n
53
54 (*
55 let add_depth_constr depth_opt cur_tbl where =
56   match depth_opt with
57   | None -> where
58   | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
59 *)
60
61 let mk_positions positions cur_tbl =
62   "(" ^
63   String.concat " or "
64     (List.map
65       (fun pos ->
66         let pos_str = MetadataPp.pp_position_tag pos in
67         match pos with
68         | `InBody
69         | `InConclusion
70         | `InHypothesis
71         | `MainConclusion None
72         | `MainHypothesis None ->
73             sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
74         | `MainConclusion (Some r)
75         | `MainHypothesis (Some r) ->
76             let depth = MetadataPp.pp_relation r in
77             sprintf "(%s.h_position = \"%s\" and %s.h_depth %s)"
78               cur_tbl pos_str cur_tbl depth)
79       (positions :> MetadataTypes.position list)) ^
80   ")"
81
82 let explode_card_constr = function
83   | Eq card -> "=", card
84   | Gt card -> ">", card
85   | Lt card -> "<", card
86
87 let add_card_constr tbl col where = function
88   | None -> where
89   | Some constr ->
90       let op, card = explode_card_constr constr in
91       (* count(_utente).hypothesis = 3 *)
92       (sprintf "%s.%s %s %d" tbl col op card :: where)
93
94 let add_diff_constr tbl where = function
95   | None -> where
96   | Some constr ->
97       let op, card = explode_card_constr constr in
98       (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where)
99       
100 let add_all_constr ?(tbl=library_count_tbl) (n,from,where) concl full diff =
101   match (concl, full, diff) with
102   | None, None, None -> (n,from,where)
103   | _ -> 
104       let cur_tbl = tbln n in
105       let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
106       let where = add_card_constr cur_tbl "conclusion" where concl in
107       let where = add_card_constr cur_tbl "statement" where full in
108       let where = add_diff_constr cur_tbl where diff in
109       (n+2,from, 
110         (if n > 0 then 
111           sprintf "table0.source = %s.source" cur_tbl :: where 
112         else
113           where))
114       
115
116 let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
117   let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables 
118   in
119   let cur_tbl = tbln n in
120   let start_table = tbln start in
121   match metadata with
122   | `Obj (uri, positions) ->
123       let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
124       let where = 
125         (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl (UriManager.string_of_uri uri)) ::
126         mk_positions positions cur_tbl ::
127         (if n=start then []
128         else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ 
129         where
130       in
131       ((n+2), from, where)
132   | `Rel positions ->
133       let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
134       let where =
135         mk_positions positions cur_tbl ::
136         (if n=start then []
137         else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ 
138         where
139       in
140       ((n+2), from, where)
141   | `Sort (sort, positions) ->
142       let sort_str = CicPp.ppsort sort in
143       let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
144       let where =
145         (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
146             mk_positions positions cur_tbl ::
147         (if n=start then 
148           []
149         else 
150           [sprintf "%s.source = %s.source" start_table cur_tbl ]) @ where
151       in
152       ((n+2), from, where)
153
154 let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) =
155   let from = String.concat ", " from in
156   let where = String.concat " and " where in
157   let query =
158     match rating with
159     | None -> sprintf "select table0.source from %s where %s" from where
160     | Some `Hits ->
161         sprintf
162           ("select table0.source from %s, hits where %s
163             and table0.source = hits.source order by hits.no desc")
164           from where 
165   in
166 (*  prerr_endline query; *)
167   let result = Mysql.exec dbd query in
168   Mysql.map result
169     (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
170
171
172 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
173   (metadata: MetadataTypes.constr list)
174 =
175   let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables 
176   in
177   if (metadata = []) && concl_card = None && full_card = None then
178     failwith "MetadataQuery.at_least: no constraints given";
179   let (n,from,where) =
180     List.fold_left (add_constraint ~tables) (0,[],[]) metadata
181   in
182   let (n,from,where) =
183     add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
184   in
185   exec ~dbd ?rating (n,from,where)
186     
187 let at_least  
188   ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating
189       (metadata: MetadataTypes.constr list)
190 =
191   if are_tables_ownerized () then
192     (at_least 
193        ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
194     (at_least 
195        ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
196   else
197     at_least 
198       ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata 
199   
200     
201   (** Prefix handling *)
202
203 let filter_by_card n =
204   SetSet.filter (fun t -> (UriManagerSet.cardinal t) <= n)
205   
206 let merge n a b = 
207   let init = SetSet.union a b in
208   let merge_single_set s1 b = 
209     SetSet.fold 
210       (fun s2 res -> SetSet.add (UriManagerSet.union s1 s2) res)
211       b SetSet.empty in
212   let res = 
213     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
214   in
215   filter_by_card n res 
216
217 let string_of_uriref i =
218  UriManager.uri_of_string (UriManager.string_of_uriref i)
219
220 let rec inspect_children n childs =
221   List.fold_left 
222     (fun res term -> merge n (inspect_conclusion n term) res)
223     SetSet.empty childs 
224
225 and add_root n root childs =
226   let childunion = inspect_children n childs in
227   let addroot = UriManagerSet.add root in
228     SetSet.fold 
229       (fun child newsets -> SetSet.add (addroot child) newsets)
230       childunion 
231       (SetSet.singleton (UriManagerSet.singleton root))
232
233 and inspect_conclusion n t = 
234   if n = 0 then SetSet.empty
235   else match t with
236       Cic.Rel _                    
237     | Cic.Meta _                     
238     | Cic.Sort _ 
239     | Cic.Implicit _ -> SetSet.empty 
240     | Cic.Var (u,exp_named_subst) -> SetSet.empty
241     | Cic.Const (u,exp_named_subst) -> 
242         SetSet.singleton (UriManagerSet.singleton u)
243     | Cic.MutInd (u, t, exp_named_subst) -> 
244         SetSet.singleton (UriManagerSet.singleton
245           (string_of_uriref (u, [t])))
246     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
247         SetSet.singleton (UriManagerSet.singleton
248           (string_of_uriref (u, [t; c])))
249     | Cic.Cast (t, _) -> inspect_conclusion n t
250     | Cic.Prod (_, s, t) -> 
251         merge n (inspect_conclusion n s) (inspect_conclusion n t)
252     | Cic.Lambda (_, s, t) ->
253         merge n (inspect_conclusion n s) (inspect_conclusion n t)
254     | Cic.LetIn (_, s, t) ->
255         merge n (inspect_conclusion n s) (inspect_conclusion n t)
256     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
257         let suri = u in
258         add_root (n-1) suri l
259     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
260         let suri = string_of_uriref (u, [t]) in
261         add_root (n-1) suri l
262     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
263         let suri = string_of_uriref (u, [t; c]) in
264         add_root (n-1) suri l
265     | Cic.Appl l -> 
266         SetSet.empty
267     | Cic.MutCase (u, t, tt, uu, m) ->
268         SetSet.empty
269     | Cic.Fix (_, m) -> 
270         SetSet.empty
271     | Cic.CoFix (_, m) -> 
272         SetSet.empty
273
274 let rec inspect_term n t = 
275   if n = 0 then
276     assert false
277   else
278     match t with
279       Cic.Rel _                    
280     | Cic.Meta _                     
281     | Cic.Sort _ 
282     | Cic.Implicit _ -> None, SetSet.empty 
283     | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
284     | Cic.Const (u,exp_named_subst) -> 
285         Some u, SetSet.empty
286     | Cic.MutInd (u, t, exp_named_subst) -> 
287         let uri = string_of_uriref (u, [t]) in
288         Some uri, SetSet.empty
289     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
290         let uri = string_of_uriref (u, [t; c]) in
291         Some uri, SetSet.empty
292     | Cic.Cast (t, _) -> inspect_term n t
293     | Cic.Prod (_, _, t) -> inspect_term n t
294     | Cic.LetIn (_, _, t) -> inspect_term n t
295     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
296         let suri = u in
297         let childunion = inspect_children (n-1) l in
298         Some suri, childunion
299     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
300         let suri = string_of_uriref (u, [t]) in
301         if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
302           (* equality is handled in a special way: in particular, 
303              the type, if defined, is always added to the prefix, 
304              and n is not decremented - it should have been n-2 *)
305           match l with
306               Cic.Const (u1,exp_named_subst1)::l1 ->
307                 let suri1 = u1 in
308                 let inconcl = add_root (n-1) suri1 l1 in
309                 Some suri, inconcl
310             | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
311                 let suri1 = string_of_uriref (u1, [t1]) in
312                 let inconcl = add_root (n-1) suri1 l1 in  
313                 Some suri, inconcl
314             | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
315                 let suri1 = string_of_uriref (u1, [t1; c1]) in
316                 let inconcl = add_root (n-1) suri1 l1 in  
317                 Some suri, inconcl
318             | _ :: _ -> Some suri, SetSet.empty
319             | _ -> assert false (* args number must be > 0 *)
320         else
321           let childunion = inspect_children (n-1) l in
322           Some suri, childunion
323     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
324         let suri = string_of_uriref (u, [t; c]) in
325         let childunion = inspect_children (n-1) l in
326         Some suri, childunion
327     | _ -> None, SetSet.empty
328
329 let add_cardinality s =
330   let l = SetSet.elements s in
331   let res = 
332     List.map 
333       (fun set -> 
334          let el = UriManagerSet.elements set in
335          (List.length el, el)) l in
336     (* ordered by descending cardinality *)
337     List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
338
339 let prefixes n t =
340   match inspect_term n t with
341       Some a, set -> Some a, add_cardinality set
342     | None, set when (SetSet.is_empty set) -> None, []
343     | _, _ -> assert false
344
345
346 let rec add children =
347   List.fold_left
348     (fun acc t -> UriManagerSet.union (signature_concl t) acc)
349     (UriManagerSet.empty) children
350   
351 (* this function creates the set of all different constants appearing in 
352    the conclusion of the term *)
353 and signature_concl = 
354   function
355       Cic.Rel _                    
356     | Cic.Meta _                     
357     | Cic.Sort _ 
358     | Cic.Implicit _ -> UriManagerSet.empty 
359     | Cic.Var (u,exp_named_subst) -> UriManagerSet.empty
360     | Cic.Const (u,exp_named_subst) -> 
361         UriManagerSet.singleton u
362     | Cic.MutInd (u, t, exp_named_subst) -> 
363         let uri = string_of_uriref (u, [t]) in
364         UriManagerSet.singleton uri
365     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
366         let uri = string_of_uriref (u, [t;c]) in
367         UriManagerSet.singleton uri
368     | Cic.Cast (t, _) -> signature_concl t
369     | Cic.Prod (_, s, t) -> 
370         UriManagerSet.union (signature_concl s) (signature_concl t)
371     | Cic.Lambda (_, s, t) ->
372         UriManagerSet.union (signature_concl s) (signature_concl t)
373     | Cic.LetIn (_, s, t) ->
374         UriManagerSet.union (signature_concl s) (signature_concl t)
375     | Cic.Appl l  -> add l
376     | Cic.MutCase _
377     | Cic.Fix _
378     | Cic.CoFix _ ->
379         UriManagerSet.empty
380
381 let rec signature_of = function
382   | Cic.Cast (t, _)      -> signature_of t
383   | Cic.Prod (_, _, t)   -> signature_of t               
384   | Cic.LetIn (_, _, t) -> signature_of t
385   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
386       let suri = u in
387       Some (suri, []), add l
388   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
389       let suri = string_of_uriref (u, [t]) in
390       if u = HelmLibraryObjects.Logic.eq_URI then
391           (* equality is handled in a special way: in particular, 
392              the type, if defined, is always added to the prefix, 
393              and n is not decremented - it should have been n-2 *)
394       match l with
395           Cic.Const (u1,exp_named_subst1)::l1 ->
396             let suri1 = u1 in
397             let inconcl = UriManagerSet.remove suri1 (add l1) in
398             Some (suri, [suri1]), inconcl
399         | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
400             let suri1 = string_of_uriref (u1, [t1]) in
401             let inconcl =  UriManagerSet.remove suri1 (add l1) in
402               Some (suri, [suri1]), inconcl
403         | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
404             let suri1 = string_of_uriref (u1, [t1;c1]) in
405             let inconcl =  UriManagerSet.remove suri1 (add l1) in
406             Some (suri, [suri1]), inconcl
407         | _ :: _ -> Some (suri, []), UriManagerSet.empty
408         | _ -> assert false (* args number must be > 0 *)
409       else
410         Some (suri, []), add l
411   | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
412       let suri = string_of_uriref (u, [t;c]) in
413       Some (suri, []), add l
414   | t -> None, signature_concl t
415
416 (* takes a list of lists and returns the list of all elements
417    without repetitions *)
418 let union l = 
419   let rec drop_repetitions = function
420       [] -> []
421     | [a] -> [a]
422     | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
423     | u::l -> u::(drop_repetitions l) in
424   drop_repetitions (List.sort Pervasives.compare (List.concat l))
425
426 let must_of_prefix ?(where = `Conclusion) m s =
427   let positions =
428     match where with
429     | `Conclusion -> [`InConclusion]
430     | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
431   in
432   let s' = List.map (fun u -> `Obj (u, positions)) s in
433   `Obj (m, [`MainConclusion None]) :: s'
434
435 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
436
437 let get_constants (dbd:Mysql.dbd) ~where uri =
438   let uri = escape (UriManager.string_of_uri uri) in
439   let positions =
440     match where with
441     | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
442     | `Statement ->
443         [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
444           MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
445   in
446   let query = 
447     let pos_predicate =
448       String.concat " OR "
449         (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
450     in
451     sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
452              "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
453       (MetadataTypes.obj_tbl ()) uri pos_predicate
454       MetadataTypes.library_obj_tbl uri pos_predicate
455       
456   in
457   let result = Mysql.exec dbd query in
458   let set = ref UriManagerSet.empty in
459   Mysql.iter result
460     (fun col ->
461       match col.(0) with
462       | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
463       | _ -> assert false);
464   !set
465
466 let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
467   let inconcl = get_constants dbd ~where u in
468   UriManagerSet.subset inconcl only
469
470   (* Special handling of equality. The problem is filtering out theorems just
471   * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
472   * ad-hoc, no better solution found at the moment *)
473 let myspeciallist_of_facts  =
474   [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
475 let myspeciallist =
476   [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
477    (* 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con"; *)
478    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con";
479    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal.con";
480    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal2.con";
481    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"]
482
483
484 let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
485   List.concat
486     (List.map 
487       (fun (m,s) -> 
488         if ((m = 0) && (main = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI)) then
489           (if facts then myspeciallist_of_facts
490            else myspeciallist)
491         else
492           let res =
493             let must = must_of_prefix ~where main s in
494             match where with
495             | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
496             | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
497           in
498           List.map (fun uri -> (m, uri)) res)
499       prefixes)
500
501   (* critical value reached, fallback to "only" constraints *)
502
503 let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 
504   main prefixes constants
505 =
506   let max_prefix_length = 
507     match prefixes with
508     | [] -> assert false 
509     | (max,_)::_ -> max in
510   let maximal_prefixes = 
511     let rec filter res = function 
512         [] -> res
513       | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
514       | _::_-> res in
515     filter [] prefixes in
516   let greater_than =
517     let all =
518       union
519         (List.map 
520           (fun (m,s) -> 
521             let must = must_of_prefix ~where main s in
522             (let res = 
523               match where with
524               | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
525               | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
526             in
527             (* we tag the uri with m+1, for sorting purposes *)
528             List.map (fun uri -> (m+1, uri)) res))
529           maximal_prefixes)
530     in
531     List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
532     let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
533     greater_than @ equal_to
534
535   (* real match query implementation *)
536
537 let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
538   let (main, constants) = signature_of t in
539   match main with
540   | None -> []
541   | Some (main, types) ->
542       (* the type of eq is not counted in constants_no *)
543       let types_no = List.length types in
544       let constants_no = UriManagerSet.cardinal constants in
545       if (constants_no > critical_value) then 
546         let prefixes = prefixes just_factor t in
547         (match prefixes with
548         | Some main, all_concl ->
549             let all_constants = 
550               List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
551             in
552             compute_with_only ~dbd ~facts main all_concl all_constants
553          | _, _ -> [])
554       else
555         (* in this case we compute all prefixes, and we do not need
556            to apply the only constraints *)
557         let prefixes =
558           if constants_no = 0 then
559             (if types_no = 0 then
560                Some main, [0, []]
561              else
562                Some main, [0, []; types_no, types])
563           else
564             prefixes (constants_no+types_no+1) t
565         in
566         (match prefixes with
567            Some main, all_concl ->
568              compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
569 (*
570              List.concat
571                (List.map 
572                   (fun (m,s) -> 
573                     let must = must_of_prefix ~where:`Conclusion main s in
574                     let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
575                     List.map (fun uri -> (m, uri)) res)
576                   all_concl) *)
577          | _, _ -> [])
578
579 let power_upto upto consts =
580   let l = UriManagerSet.elements consts in
581   List.sort (fun (n,_) (m,_) -> m - n)
582   (List.fold_left 
583     (fun res a ->
584        List.filter (function (n,l) -> n <= upto)
585        res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
586      [(0,[])] l)
587
588 let power consts =
589   let l = UriManagerSet.elements consts in
590   List.sort (fun (n,_) (m,_) -> m - n)
591   (List.fold_left 
592     (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
593      [(0,[])] l)
594
595 type where = [ `Conclusion | `Statement ]
596
597 let sigmatch ~(dbd:Mysql.dbd) 
598   ?(facts=false) ?(where = `Conclusion) (main, constants) =
599   match main with
600     None -> []
601   | Some (main, types) ->
602       let constants_no = UriManagerSet.cardinal constants in
603       if (constants_no > critical_value) then 
604         let subsets = 
605           let subsets = power_upto just_factor constants in
606           let types_no = List.length types in
607           List.map (function (n,l) -> (n+types_no,types@l)) subsets
608         in
609         let all_constants = 
610           List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
611         in
612         compute_with_only ~dbd ~where main subsets all_constants
613       else
614         let subsets = 
615           let subsets = power constants in
616           let types_no = List.length types in
617           if types_no > 0 then  
618           (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
619           else subsets
620         in
621         compute_exactly ~dbd ~facts ~where main subsets
622
623   (* match query wrappers *)
624
625 let cmatch'= cmatch 
626
627 let cmatch ~dbd ?(facts=false) term =
628   List.map snd
629     (List.sort
630       (fun x y -> Pervasives.compare (fst y) (fst x))
631       (cmatch' ~dbd ~facts term))
632
633 let constants_of = signature_concl
634