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