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