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