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