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