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