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 StringSet = Set.Make (String)
  33 module SetSet = Set.Make (StringSet)
  34
  35 type term_signature = (string * string list) option * StringSet.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 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)) ^
  79   ")"
  80
  81 let explode_card_constr = function
  82   | Eq card -> "=", card
  83   | Gt card -> ">", card
  84   | Lt card -> "<", card
  85
  86 let add_card_constr tbl col where = function
  87   | None -> where
  88   | Some constr ->
  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)
  92
  93 let add_diff_constr tbl where = function
  94   | None -> where
  95   | Some constr ->
  96       let op, card = explode_card_constr constr in
  97       (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where)
  98
  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)
 102   | _ ->
 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
 108       (n+2,from,
 109         (if n > 0 then
 110           sprintf "table0.source = %s.source" cur_tbl :: where
 111         else
 112           where))
 113
 114
 115 let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
 116   let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables
 117   in
 118   let cur_tbl = tbln n in
 119   let start_table = tbln start in
 120   match metadata with
 121   | `Obj (uri, positions) ->
 122       let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
 123       let where =
 124         (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
 125         mk_positions positions cur_tbl ::
 126         (if n=start then []
 127         else [sprintf "%s.source = %s.source" start_table cur_tbl]) @
 128         where
 129       in
 130       ((n+2), from, where)
 131   | `Rel positions ->
 132       let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
 133       let where =
 134         mk_positions positions cur_tbl ::
 135         (if n=start then []
 136         else [sprintf "%s.source = %s.source" start_table cur_tbl]) @
 137         where
 138       in
 139       ((n+2), from, where)
 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
 143       let where =
 144         (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
 145             mk_positions positions cur_tbl ::
 146         (if n=start then
 147           []
 148         else
 149           [sprintf "%s.source = %s.source" start_table cur_tbl ]) @ where
 150       in
 151       ((n+2), from, where)
 152
 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
 156   let query =
 157     match rating with
 158     | None -> sprintf "select table0.source from %s where %s" from where
 159     | Some `Hits ->
 160         sprintf
 161           ("select table0.source from %s, hits where %s
 162             and table0.source = hits.source order by hits.no desc")
 163           from where
 164   in
 165   prerr_endline query;
 166   let result = Mysql.exec dbd query in
 167   Mysql.map result
 168     (fun row -> match row.(0) with Some s -> s | _ -> assert false)
 169
 170
 171 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables
 172   (metadata: MetadataTypes.constr list)
 173 =
 174   let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables
 175   in
 176   if (metadata = []) && concl_card = None && full_card = None then
 177     failwith "MetadataQuery.at_least: no constraints given";
 178   let (n,from,where) =
 179     List.fold_left (add_constraint ~tables) (0,[],[]) metadata
 180   in
 181   let (n,from,where) =
 182     add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
 183   in
 184   exec ~dbd ?rating (n,from,where)
 185
 186 let at_least
 187   ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating
 188       (metadata: MetadataTypes.constr list)
 189 =
 190   if are_tables_ownerized () then
 191     (at_least
 192        ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
 193     (at_least
 194        ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
 195   else
 196     at_least
 197       ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata
 198
 199
 200   (** Prefix handling *)
 201
 202 let filter_by_card n =
 203   SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
 204
 205 let merge n a b =
 206   let init = SetSet.union a b in
 207   let merge_single_set s1 b =
 208     SetSet.fold
 209       (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
 210       b SetSet.empty in
 211   let res =
 212     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
 213   in
 214   filter_by_card n res
 215
 216 let rec inspect_children n childs =
 217   List.fold_left
 218     (fun res term -> merge n (inspect_conclusion n term) res)
 219     SetSet.empty childs
 220
 221 and add_root n root childs =
 222   let childunion = inspect_children n childs in
 223   let addroot = StringSet.add root in
 224     SetSet.fold
 225       (fun child newsets -> SetSet.add (addroot child) newsets)
 226       childunion
 227       (SetSet.singleton (StringSet.singleton root))
 228
 229 and inspect_conclusion n t =
 230   if n = 0 then SetSet.empty
 231   else match t with
 232       Cic.Rel _
 233     | Cic.Meta _
 234     | Cic.Sort _
 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
 261     | Cic.Appl l ->
 262         SetSet.empty
 263     | Cic.MutCase (u, t, tt, uu, m) ->
 264         SetSet.empty
 265     | Cic.Fix (_, m) ->
 266         SetSet.empty
 267     | Cic.CoFix (_, m) ->
 268         SetSet.empty
 269
 270 let rec inspect_term n t =
 271   if n = 0 then
 272     assert false
 273   else
 274     match t with
 275       Cic.Rel _
 276     | Cic.Meta _
 277     | Cic.Sort _
 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 *)
 301           match l with
 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
 305                 Some suri, inconcl
 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
 309                 Some suri, inconcl
 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
 313                 Some suri, inconcl
 314             | _ :: _ -> Some suri, SetSet.empty
 315             | _ -> assert false (* args number must be > 0 *)
 316         else
 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
 324
 325 let add_cardinality s =
 326   let l = SetSet.elements s in
 327   let res =
 328     List.map
 329       (fun set ->
 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)
 334
 335 let prefixes n t =
 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
 340
 341
 342 let rec add children =
 343   List.fold_left
 344     (fun acc t -> StringSet.union (signature_concl t) acc)
 345     (StringSet.empty) children
 346
 347 (* this function creates the set of all different constants appearing in
 348    the conclusion of the term *)
 349 and signature_concl =
 350   function
 351       Cic.Rel _
 352     | Cic.Meta _
 353     | Cic.Sort _
 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
 372     | Cic.MutCase _
 373     | Cic.Fix _
 374     | Cic.CoFix _ ->
 375         StringSet.empty
 376
 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 *)
 390       match l with
 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 *)
 405       else
 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
 411
 412 (* takes a list of lists and returns the list of all elements
 413    without repetitions *)
 414 let union l =
 415   let rec drop_repetitions = function
 416       [] -> []
 417     | [a] -> [a]
 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))
 421
 422 let must_of_prefix ?(where = `Conclusion) m s =
 423   let positions =
 424     match where with
 425     | `Conclusion -> [`InConclusion]
 426     | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
 427   in
 428   let s' = List.map (fun u -> `Obj (u, positions)) s in
 429   `Obj (m, [`MainConclusion None]) :: s'
 430
 431 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 432
 433 let get_constants (dbd:Mysql.dbd) ~where uri =
 434   let uri = escape uri in
 435   let positions =
 436     match where with
 437     | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
 438     | `Statement ->
 439         [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
 440           MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
 441   in
 442   let query =
 443     let pos_predicate =
 444       String.concat " OR "
 445         (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
 446     in
 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
 451
 452   in
 453   let result = Mysql.exec dbd query in
 454   let set = ref StringSet.empty in
 455   Mysql.iter result
 456     (fun col ->
 457       match col.(0) with
 458       | Some uri -> set := StringSet.add uri !set
 459       | _ -> assert false);
 460   !set
 461
 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
 465
 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)"]
 471 let myspeciallist =
 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"]
 478
 479
 480 let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
 481   List.concat
 482     (List.map
 483       (fun (m,s) ->
 484         if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
 485           (if facts then myspeciallist_of_facts
 486            else myspeciallist)
 487         else
 488           let res =
 489             let must = must_of_prefix ~where main s in
 490             match where with
 491             | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
 492             | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
 493           in
 494           List.map (fun uri -> (m, uri)) res)
 495       prefixes)
 496
 497   (* critical value reached, fallback to "only" constraints *)
 498
 499 let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
 500   main prefixes constants
 501 =
 502   let max_prefix_length =
 503     match prefixes with
 504     | [] -> assert false
 505     | (max,_)::_ -> max in
 506   let maximal_prefixes =
 507     let rec filter res = function
 508         [] -> res
 509       | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
 510       | _::_-> res in
 511     filter [] prefixes in
 512   let greater_than =
 513     let all =
 514       union
 515         (List.map
 516           (fun (m,s) ->
 517             let must = must_of_prefix ~where main s in
 518             (let res =
 519               match where with
 520               | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
 521               | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
 522             in
 523             (* we tag the uri with m+1, for sorting purposes *)
 524             List.map (fun uri -> (m+1, uri)) res))
 525           maximal_prefixes)
 526     in
 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
 530
 531   (* real match query implementation *)
 532
 533 let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
 534   let (main, constants) = signature_of t in
 535   match main with
 536   | None -> []
 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
 543         (match prefixes with
 544         | Some main, all_concl ->
 545             let all_constants =
 546               List.fold_right StringSet.add types (StringSet.add main constants)
 547             in
 548             compute_with_only ~dbd ~facts main all_concl all_constants
 549          | _, _ -> [])
 550       else
 551         (* in this case we compute all prefixes, and we do not need
 552            to apply the only constraints *)
 553         let prefixes =
 554           if constants_no = 0 then
 555             (if types_no = 0 then
 556                Some main, [0, []]
 557              else
 558                Some main, [0, []; types_no, types])
 559           else
 560             prefixes (constants_no+types_no+1) t
 561         in
 562         (match prefixes with
 563            Some main, all_concl ->
 564              compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
 565 (*
 566              List.concat
 567                (List.map
 568                   (fun (m,s) ->
 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)
 572                   all_concl) *)
 573          | _, _ -> [])
 574
 575 let power_upto upto consts =
 576   let l = StringSet.elements consts in
 577   List.sort (fun (n,_) (m,_) -> m - n)
 578   (List.fold_left
 579     (fun res a ->
 580        List.filter (function (n,l) -> n <= upto)
 581        res@(List.map (function (n,l) -> (n+1,a::l)) res))
 582      [(0,[])] l)
 583
 584 let power consts =
 585   let l = StringSet.elements consts in
 586   List.sort (fun (n,_) (m,_) -> m - n)
 587   (List.fold_left
 588     (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
 589      [(0,[])] l)
 590
 591 type where = [ `Conclusion | `Statement ]
 592
 593 let sigmatch ~(dbd:Mysql.dbd)
 594   ?(facts=false) ?(where = `Conclusion) (main, constants) =
 595   match main with
 596     None -> []
 597   | Some (main, types) ->
 598       let constants_no = StringSet.cardinal constants in
 599       if (constants_no > critical_value) then
 600         let subsets =
 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
 604         in
 605         let all_constants =
 606           List.fold_right StringSet.add types (StringSet.add main constants)
 607         in
 608         compute_with_only ~dbd ~where main subsets all_constants
 609       else
 610         let subsets =
 611           let subsets = power constants in
 612           let types_no = List.length types in
 613           if types_no > 0 then
 614           (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
 615           else subsets
 616         in
 617         compute_exactly ~dbd ~facts ~where main subsets
 618
 619   (* match query wrappers *)
 620
 621 let cmatch'= cmatch
 622
 623 let cmatch ~dbd ?(facts=false) term =
 624   List.map snd
 625     (List.sort
 626       (fun x y -> Pervasives.compare (fst y) (fst x))
 627       (cmatch' ~dbd ~facts term))
 628
 629 let constants_of = signature_concl
 630