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