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