X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=7bc92eb66b136c6c2c8ee6b46f4d42f1ad3469f4;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=28973af976f9ede65b9386982f308821ce0a4e4a;hpb=a7e03aee7257e05cba4225ee3bde1dbb8a6ee515;p=helm.git

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index 28973af97..7bc92eb66 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -24,18 +24,30 @@
  *)
 
 open Printf
+open MetadataTypes 
 
 let critical_value = 7
-let just_factor = 4
+let just_factor = 3
 
-module StringSet = Set.Make (String)
-module SetSet = Set.Make (StringSet)
+module UriManagerSet = UriManager.UriSet
+module SetSet = Set.Make (UriManagerSet)
 
-type term_signature = (string * string list) option * StringSet.t
+type term_signature = (UriManager.uri * UriManager.uri list) option * UriManagerSet.t
 
 type cardinality_condition =
   | Eq of int
   | Gt of int
+  | Lt of int
+
+type rating_criterion =
+  [ `Hits   (** order by number of hits, most used objects first *)
+  ]
+
+let default_tables =
+   (library_obj_tbl,library_rel_tbl,library_sort_tbl,library_count_tbl)
+
+let current_tables () = 
+  (obj_tbl (),rel_tbl (),sort_tbl (), count_tbl ())
 
 let tbln n = "table" ^ string_of_int n
 
@@ -59,98 +71,143 @@ let mk_positions positions cur_tbl =
         | `MainConclusion None
         | `MainHypothesis None ->
             sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
-        | `MainConclusion (Some d)
-        | `MainHypothesis (Some d) ->
-            sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
-              cur_tbl pos_str cur_tbl d)
+        | `MainConclusion (Some r)
+        | `MainHypothesis (Some r) ->
+            let depth = MetadataPp.pp_relation r in
+            sprintf "(%s.h_position = \"%s\" and %s.h_depth %s)"
+              cur_tbl pos_str cur_tbl depth)
       (positions :> MetadataTypes.position list)) ^
   ")"
 
-let add_card_constr tbl (n,from,where) = function
-  | None -> (n,from,where)
-  | Some (Eq card) ->
-      let cur_tbl = tbln n in
-      (n+1,
-       (sprintf "%s as %s" tbl cur_tbl :: from),
-       (sprintf "%s.no=%d" cur_tbl card ::
-        (if n=0 then []
-        else [sprintf "table0.source = %s.source" cur_tbl]) @
-        where))
-  | Some (Gt card) ->
+let explode_card_constr = function
+  | Eq card -> "=", card
+  | Gt card -> ">", card
+  | Lt card -> "<", card
+
+let add_card_constr tbl col where = function
+  | None -> where
+  | Some constr ->
+      let op, card = explode_card_constr constr in
+      (* count(_utente).hypothesis = 3 *)
+      (sprintf "%s.%s %s %d" tbl col op card :: where)
+
+let add_diff_constr tbl where = function
+  | None -> where
+  | Some constr ->
+      let op, card = explode_card_constr constr in
+      (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where)
+      
+let add_all_constr ?(tbl=library_count_tbl) (n,from,where) concl full diff =
+  match (concl, full, diff) with
+  | None, None, None -> (n,from,where)
+  | _ -> 
       let cur_tbl = tbln n in
-      (n+1,
-       (sprintf "%s as %s" tbl cur_tbl :: from),
-       (sprintf "%s.no>%d" cur_tbl card ::
-        (if n=0 then []
-        else [sprintf "table0.source = %s.source" cur_tbl]) @
-        where))
-
-let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
+      let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
+      let where = add_card_constr cur_tbl "conclusion" where concl in
+      let where = add_card_constr cur_tbl "statement" where full in
+      let where = add_diff_constr cur_tbl where diff in
+      (n+2,from, 
+        (if n > 0 then 
+          sprintf "table0.source = %s.source" cur_tbl :: where 
+        else
+          where))
+      
+
+let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
+  let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables 
+  in
+  let cur_tbl = tbln n in
+  let start_table = tbln start in
+  match metadata with
+  | `Obj (uri, positions) ->
+      let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
+      let where = 
+        (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl (UriManager.string_of_uri uri)) ::
+        mk_positions positions cur_tbl ::
+        (if n=start then []
+        else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ 
+        where
+      in
+      ((n+2), from, where)
+  | `Rel positions ->
+      let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
+      let where =
+        mk_positions positions cur_tbl ::
+        (if n=start then []
+        else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ 
+        where
+      in
+      ((n+2), from, where)
+  | `Sort (sort, positions) ->
+      let sort_str = CicPp.ppsort sort in
+      let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
+      let where =
+        (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
+            mk_positions positions cur_tbl ::
+        (if n=start then 
+          []
+        else 
+          [sprintf "%s.source = %s.source" start_table cur_tbl ]) @ where
+      in
+      ((n+2), from, where)
+
+let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
+  let from = String.concat ", " from in
+  let where = String.concat " and " where in
+  let query =
+    match rating with
+    | None -> sprintf "select distinct table0.source from %s where %s" from where
+    | Some `Hits ->
+        sprintf
+          ("select distinct table0.source from %s, hits where %s
+            and table0.source = hits.source order by hits.no desc")
+          from where 
+  in
+  (* prerr_endline query; *) 
+  let result = HMysql.exec dbd query in
+  HMysql.map result
+    (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
+
+
+let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
   (metadata: MetadataTypes.constr list)
 =
+  let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables 
+  in
   if (metadata = []) && concl_card = None && full_card = None then
     failwith "MetadataQuery.at_least: no constraints given";
-  let add_constraint (n,from,where) metadata =
-    let cur_tbl = tbln n in
-    match metadata with
-    | `Obj (uri, positions) ->
-        let tbl = MetadataTypes.obj_tbl in
-        let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
-        let where =
-          (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) ::
-          mk_positions positions cur_tbl ::
-          (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @
-          where
-        in
-        ((n+1), from, where)
-    | `Rel positions ->
-        let tbl = MetadataTypes.rel_tbl in
-        let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
-        let where =
-          mk_positions positions cur_tbl ::
-          (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @
-          where
-        in
-        ((n+1), from, where)
-    | `Sort (sort, positions) ->
-        let tbl = MetadataTypes.sort_tbl in
-        let sort_str = MetadataPp.pp_sort sort in
-        let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
-        let where =
-          (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
-          mk_positions positions cur_tbl ::
-          (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @
-          where
-        in
-        ((n+1), from, where)
-  in
-  let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
   let (n,from,where) =
-    add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card
+    List.fold_left (add_constraint ~tables) (0,[],[]) metadata
   in
   let (n,from,where) =
-    add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card
+    add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
   in
-  let from = String.concat ", " from in
-  let where = String.concat " and " where in
-  let query = sprintf "select table0.source from %s where %s" from where in
-  let result = Mysql.exec dbd query in
-  Mysql.map result
-    (fun row -> match row.(0) with Some s -> s | _ -> assert false)
-
+  exec ~dbd ?rating (n,from,where)
+    
+let at_least  
+  ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
+      (metadata: MetadataTypes.constr list)
+=
+  if are_tables_ownerized () then
+    (at_least 
+       ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
+    (at_least 
+       ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
+  else
+    at_least 
+      ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata 
+  
+    
   (** Prefix handling *)
 
 let filter_by_card n =
-  SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
+  SetSet.filter (fun t -> (UriManagerSet.cardinal t) <= n)
   
 let merge n a b = 
   let init = SetSet.union a b in
   let merge_single_set s1 b = 
     SetSet.fold 
-      (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
+      (fun s2 res -> SetSet.add (UriManagerSet.union s1 s2) res)
       b SetSet.empty in
   let res = 
     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
@@ -164,11 +221,11 @@ let rec inspect_children n childs =
 
 and add_root n root childs =
   let childunion = inspect_children n childs in
-  let addroot = StringSet.add root in
+  let addroot = UriManagerSet.add root in
     SetSet.fold 
       (fun child newsets -> SetSet.add (addroot child) newsets)
       childunion 
-      (SetSet.singleton (StringSet.singleton root))
+      (SetSet.singleton (UriManagerSet.singleton root))
 
 and inspect_conclusion n t = 
   if n = 0 then SetSet.empty
@@ -179,13 +236,13 @@ and inspect_conclusion n t =
     | Cic.Implicit _ -> SetSet.empty 
     | Cic.Var (u,exp_named_subst) -> SetSet.empty
     | Cic.Const (u,exp_named_subst) -> 
-        SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
+        SetSet.singleton (UriManagerSet.singleton u)
     | Cic.MutInd (u, t, exp_named_subst) -> 
-	SetSet.singleton (StringSet.singleton
-          (UriManager.string_of_uriref (u, [t])))
+	SetSet.singleton (UriManagerSet.singleton
+          (UriManager.uri_of_uriref u t None))
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
-	SetSet.singleton (StringSet.singleton
-          (UriManager.string_of_uriref (u, [t; c])))
+	SetSet.singleton (UriManagerSet.singleton
+          (UriManager.uri_of_uriref u t (Some c)))
     | Cic.Cast (t, _) -> inspect_conclusion n t
     | Cic.Prod (_, s, t) -> 
 	merge n (inspect_conclusion n s) (inspect_conclusion n t)
@@ -194,13 +251,12 @@ and inspect_conclusion n t =
     | Cic.LetIn (_, s, t) ->
 	merge n (inspect_conclusion n s) (inspect_conclusion n t)
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
-        let suri = UriManager.string_of_uri u in
-	add_root (n-1) suri l
+	add_root (n-1) u l
     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
-        let suri = UriManager.string_of_uriref (u, [t]) in
-	add_root (n-1) suri l
+        let uri = UriManager.uri_of_uriref u t None in
+	add_root (n-1) uri l
     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
-	let suri = UriManager.string_of_uriref (u, [t; c]) in
+	let suri = UriManager.uri_of_uriref u t (Some c) in
 	add_root (n-1) suri l
     | Cic.Appl l -> 
 	SetSet.empty
@@ -222,37 +278,35 @@ let rec inspect_term n t =
     | Cic.Implicit _ -> None, SetSet.empty 
     | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
     | Cic.Const (u,exp_named_subst) -> 
-        Some (UriManager.string_of_uri u), SetSet.empty
+        Some u, SetSet.empty
     | Cic.MutInd (u, t, exp_named_subst) -> 
-        let uri = UriManager.string_of_uriref (u, [t]) in
+        let uri = UriManager.uri_of_uriref u t None in
 	Some uri, SetSet.empty
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
-        let uri = UriManager.string_of_uriref (u, [t; c]) in
+        let uri = UriManager.uri_of_uriref u t (Some c) in
 	Some uri, SetSet.empty
     | Cic.Cast (t, _) -> inspect_term n t
     | Cic.Prod (_, _, t) -> inspect_term n t
     | Cic.LetIn (_, _, t) -> inspect_term n t
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
-	let suri = UriManager.string_of_uri u in
 	let childunion = inspect_children (n-1) l in
-	Some suri, childunion
+	Some u, childunion
     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
-	let suri = UriManager.string_of_uriref (u, [t]) in
+	let suri = UriManager.uri_of_uriref u t None in
 	if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
 	  (* equality is handled in a special way: in particular, 
              the type, if defined, is always added to the prefix, 
 	     and n is not decremented - it should have been n-2 *)
 	  match l with
 	      Cic.Const (u1,exp_named_subst1)::l1 ->
-		let suri1 = UriManager.string_of_uri u1 in
-		let inconcl = add_root (n-1) suri1 l1 in
+		let inconcl = add_root (n-1) u1 l1 in
 		Some suri, inconcl
 	    | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
-		let suri1 = UriManager.string_of_uriref (u1, [t1]) in
+		let suri1 = UriManager.uri_of_uriref u1 t1 None in
 		let inconcl = add_root (n-1) suri1 l1 in  
 		Some suri, inconcl
 	    | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
-                let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
+                let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
 		let inconcl = add_root (n-1) suri1 l1 in  
 		Some suri, inconcl
 	    | _ :: _ -> Some suri, SetSet.empty
@@ -261,7 +315,7 @@ let rec inspect_term n t =
 	  let childunion = inspect_children (n-1) l in
 	  Some suri, childunion
     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
-	let suri = UriManager.string_of_uriref (u, [t; c]) in
+	let suri = UriManager.uri_of_uriref u t(Some c) in
 	let childunion = inspect_children (n-1) l in
 	Some suri, childunion
     | _ -> None, SetSet.empty
@@ -271,7 +325,7 @@ let add_cardinality s =
   let res = 
     List.map 
       (fun set -> 
-	 let el = StringSet.elements set in
+	 let el = UriManagerSet.elements set in
 	 (List.length el, el)) l in
     (* ordered by descending cardinality *)
     List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
@@ -285,8 +339,8 @@ let prefixes n t =
 
 let rec add children =
   List.fold_left
-    (fun acc t -> StringSet.union (signature_concl t) acc)
-    (StringSet.empty) children
+    (fun acc t -> UriManagerSet.union (signature_concl t) acc)
+    (UriManagerSet.empty) children
   
 (* this function creates the set of all different constants appearing in 
    the conclusion of the term *)
@@ -295,61 +349,61 @@ and signature_concl =
       Cic.Rel _                    
     | Cic.Meta _                     
     | Cic.Sort _ 
-    | Cic.Implicit _ -> StringSet.empty 
-    | Cic.Var (u,exp_named_subst) -> StringSet.empty
+    | Cic.Implicit _ -> UriManagerSet.empty 
+    | Cic.Var (u,exp_named_subst) ->
+       (*CSC: TODO if the var has a body it must be processed *)
+       UriManagerSet.empty
     | Cic.Const (u,exp_named_subst) -> 
-        StringSet.singleton (UriManager.string_of_uri u)
+        UriManagerSet.singleton u
     | Cic.MutInd (u, t, exp_named_subst) -> 
-        let uri = UriManager.string_of_uriref (u, [t]) in
-	StringSet.singleton uri
+        let uri = UriManager.uri_of_uriref u t None in
+	UriManagerSet.singleton uri
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
-        let uri = UriManager.string_of_uriref (u, [t;c]) in
-	StringSet.singleton uri
+        let uri = UriManager.uri_of_uriref u t (Some c) in
+	UriManagerSet.singleton uri
     | Cic.Cast (t, _) -> signature_concl t
     | Cic.Prod (_, s, t) -> 
-	StringSet.union (signature_concl s) (signature_concl t)
+	UriManagerSet.union (signature_concl s) (signature_concl t)
     | Cic.Lambda (_, s, t) ->
-	StringSet.union (signature_concl s) (signature_concl t)
+	UriManagerSet.union (signature_concl s) (signature_concl t)
     | Cic.LetIn (_, s, t) ->
-	StringSet.union (signature_concl s) (signature_concl t)
+	UriManagerSet.union (signature_concl s) (signature_concl t)
     | Cic.Appl l  -> add l
     | Cic.MutCase _
     | Cic.Fix _
     | Cic.CoFix _ ->
-	StringSet.empty
+	UriManagerSet.empty
 
 let rec signature_of = function
   | Cic.Cast (t, _)      -> signature_of t
   | Cic.Prod (_, _, t)   -> signature_of t               
   | Cic.LetIn (_, _, t) -> signature_of t
   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
-      let suri = UriManager.string_of_uri u in
-      Some (suri, []), add l
+      Some (u, []), add l
   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
-      let suri = UriManager.string_of_uriref (u, [t]) in
+      let suri = UriManager.uri_of_uriref u t None in
       if u = HelmLibraryObjects.Logic.eq_URI then
 	  (* equality is handled in a special way: in particular, 
              the type, if defined, is always added to the prefix, 
 	     and n is not decremented - it should have been n-2 *)
       match l with
 	  Cic.Const (u1,exp_named_subst1)::l1 ->
-	    let suri1 = UriManager.string_of_uri u1 in
-	    let inconcl = StringSet.remove suri1 (add l1) in
-            Some (suri, [suri1]), inconcl
+	    let inconcl = UriManagerSet.remove u1 (add l1) in
+            Some (suri, [u1]), inconcl
 	| Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
-	    let suri1 = UriManager.string_of_uriref (u1, [t1]) in
-	    let inconcl =  StringSet.remove suri1 (add l1) in
+	    let suri1 = UriManager.uri_of_uriref u1 t1 None in
+	    let inconcl =  UriManagerSet.remove suri1 (add l1) in
 	      Some (suri, [suri1]), inconcl
 	| Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
-            let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
-	    let inconcl =  StringSet.remove suri1 (add l1) in
+            let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
+	    let inconcl =  UriManagerSet.remove suri1 (add l1) in
             Some (suri, [suri1]), inconcl
-	| _ :: _ -> Some (suri, []), StringSet.empty
+	| _ :: _ -> Some (suri, []), UriManagerSet.empty
 	| _ -> assert false (* args number must be > 0 *)
       else
 	Some (suri, []), add l
   | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
-      let suri = UriManager.string_of_uriref (u, [t;c]) in
+      let suri = UriManager.uri_of_uriref u t (Some c) in
       Some (suri, []), add l
   | t -> None, signature_concl t
 
@@ -369,71 +423,94 @@ let must_of_prefix ?(where = `Conclusion) m s =
     | `Conclusion -> [`InConclusion]
     | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
   in
-  let s' = List.map (fun u -> `Obj (u, positions)) s in
-  `Obj (m, [`MainConclusion None]) :: s'
+  let positions =
+   if m = None then `MainConclusion None :: positions else positions in
+  let s' = List.map (fun (u:UriManager.uri) -> `Obj (u, positions)) s in
+   match m with
+      None -> s'
+    | Some m -> `Obj (m, [`MainConclusion None]) :: s'
 
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 
-let get_constants (dbd:Mysql.dbd) ~where uri =
-  let uri = escape uri in
+let get_constants (dbd:HMysql.dbd) ~where uri =
+  let uri = escape (UriManager.string_of_uri uri) in
   let positions =
     match where with
-    | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""]
+    | `Conclusion -> [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos ]
     | `Statement ->
-        ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\"";
-         "\"MainHypothesis\""]
+        [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
+          MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
   in
   let query = 
-    sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)"
-      uri (String.concat " or " positions)
+    let pos_predicate =
+      String.concat " OR "
+        (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
+    in
+    sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
+             "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
+      (MetadataTypes.obj_tbl ()) uri pos_predicate
+      MetadataTypes.library_obj_tbl uri pos_predicate
+      
   in
-  let result = Mysql.exec dbd query in
-  let set = ref StringSet.empty in
-  Mysql.iter result
+  let result = HMysql.exec dbd query in
+  let set = ref UriManagerSet.empty in
+  HMysql.iter result
     (fun col ->
       match col.(0) with
-      | Some uri -> set := StringSet.add uri !set
+      | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
       | _ -> assert false);
   !set
 
-let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
+let at_most ~(dbd:HMysql.dbd) ?(where = `Conclusion) only u =
   let inconcl = get_constants dbd ~where u in
-  StringSet.subset inconcl only
+  UriManagerSet.subset inconcl only
 
   (* Special handling of equality. The problem is filtering out theorems just
   * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
   * ad-hoc, no better solution found at the moment *)
 let myspeciallist_of_facts  =
-  [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
+  [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
 let myspeciallist =
-  [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
-   0,"cic:/Coq/Init/Logic/sym_eq.con"; 
-   0,"cic:/Coq/Init/Logic/trans_eq.con";
-   0,"cic:/Coq/Init/Logic/f_equal.con";
-   0,"cic:/Coq/Init/Logic/f_equal2.con";
-   0,"cic:/Coq/Init/Logic/f_equal3.con"]
+  [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
+   (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
+   0,UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con";
+   0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal.con";
+   0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal2.con";
+   0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"]
 
 
-let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
+let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
   List.concat
     (List.map 
       (fun (m,s) -> 
-        if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
+        let is_eq,card =
+         match main with
+            None -> false,m
+          | Some main ->
+             (m = 0 &&
+              UriManager.eq main
+               (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI))),
+             m+1
+        in
+        if m = 0 && is_eq then
           (if facts then myspeciallist_of_facts
 	   else myspeciallist)
         else
           let res =
+           (* this gets rid of the ~750 objects of type Set/Prop/Type *)
+           if card = 0 then []
+           else
             let must = must_of_prefix ~where main s in
             match where with
-            | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
-            | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
+            | `Conclusion -> at_least ~dbd ~concl_card:(Eq card) must
+            | `Statement -> at_least ~dbd ~full_card:(Eq card) must
           in
-          List.map (fun uri -> (m, uri)) res)
+          List.map (fun uri -> (card, uri)) res)
       prefixes)
 
   (* critical value reached, fallback to "only" constraints *)
 
-let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 
+let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) 
   main prefixes constants
 =
   let max_prefix_length = 
@@ -446,43 +523,45 @@ let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion)
       | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
       | _::_-> res in
     filter [] prefixes in
-  let greater_than =
+    let greater_than =
     let all =
       union
         (List.map 
           (fun (m,s) -> 
+            let card = if main = None then m else m + 1 in
             let must = must_of_prefix ~where main s in
             (let res = 
               match where with
-              | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
-              | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
+              | `Conclusion -> at_least ~dbd ~concl_card:(Gt card) must
+              | `Statement -> at_least ~dbd ~full_card:(Gt card) must
             in
             (* we tag the uri with m+1, for sorting purposes *)
-            List.map (fun uri -> (m+1, uri)) res))
+            List.map (fun uri -> (card, uri)) res))
           maximal_prefixes)
     in
+    Printf.fprintf stderr "all: %d\n" (List.length all);flush_all ();
     List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
-    let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
+  let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
     greater_than @ equal_to
 
   (* real match query implementation *)
 
-let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
+let cmatch ~(dbd:HMysql.dbd)  ?(facts=false) t =
   let (main, constants) = signature_of t in
   match main with
   | None -> []
   | Some (main, types) ->
       (* the type of eq is not counted in constants_no *)
       let types_no = List.length types in
-      let constants_no = StringSet.cardinal constants in
+      let constants_no = UriManagerSet.cardinal constants in
       if (constants_no > critical_value) then 
         let prefixes = prefixes just_factor t in
         (match prefixes with
         | Some main, all_concl ->
             let all_constants = 
-              List.fold_right StringSet.add types (StringSet.add main constants)
+              List.fold_right UriManagerSet.add types (UriManagerSet.add main constants)
             in
-            compute_with_only ~dbd ~facts main all_concl all_constants
+            compute_with_only ~dbd ~facts (Some main) all_concl all_constants
          | _, _ -> [])
       else
         (* in this case we compute all prefixes, and we do not need
@@ -498,28 +577,22 @@ let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
         in
         (match prefixes with
            Some main, all_concl ->
-	     compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
-(*
-             List.concat
-               (List.map 
-                  (fun (m,s) -> 
-                    let must = must_of_prefix ~where:`Conclusion main s in
-                    let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
-                    List.map (fun uri -> (m, uri)) res)
-                  all_concl) *)
+	    compute_exactly ~dbd ~facts ~where:`Conclusion (Some main) all_concl
          | _, _ -> [])
 
 let power_upto upto consts =
-  let l = StringSet.elements consts in
+  let l = UriManagerSet.elements consts in
   List.sort (fun (n,_) (m,_) -> m - n)
   (List.fold_left 
     (fun res a ->
-       List.filter (function (n,l) -> n <= upto)
-       res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
+       let res' = 
+	 List.filter (function (n,l) -> n <= upto)
+	   (List.map (function (n,l) -> (n+1,a::l)) res) in
+	 res@res')
      [(0,[])] l)
 
 let power consts =
-  let l = StringSet.elements consts in
+  let l = UriManagerSet.elements consts in
   List.sort (fun (n,_) (m,_) -> m - n)
   (List.fold_left 
     (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res)) 
@@ -527,31 +600,38 @@ let power consts =
 
 type where = [ `Conclusion | `Statement ]
 
-let sigmatch ~(dbd:Mysql.dbd) 
-  ?(facts=false) ?(where = `Conclusion) (main, constants) =
-  match main with
-    None -> []
-  | Some (main, types) ->
-      let constants_no = StringSet.cardinal constants in
-      if (constants_no > critical_value) then 
-        let subsets = 
-          let subsets = power_upto just_factor constants in
-          let types_no = List.length types in
-          List.map (function (n,l) -> (n+types_no,types@l)) subsets
-        in
-        let all_constants = 
-          List.fold_right StringSet.add types (StringSet.add main constants)
-        in
-        compute_with_only ~dbd ~where main subsets all_constants
-      else
-        let subsets = 
-          let subsets = power constants in
-          let types_no = List.length types in
-	  if types_no > 0 then  
-          (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
-	  else subsets
-        in
-        compute_exactly ~dbd ~facts ~where main subsets
+let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+ (main, constants)
+=
+ let main,types =
+   match main with
+     None -> None,[]
+   | Some (main, types) -> Some main,types
+ in
+  let constants_no = UriManagerSet.cardinal constants in
+  (* prerr_endline (("constants_no: ")^(string_of_int constants_no)); *)
+  if (constants_no > critical_value) then 
+    let subsets = 
+      let subsets = power_upto just_factor constants in
+      (* let _ = prerr_endline (("subsets: ")^
+	 (string_of_int (List.length subsets))) in *)
+      let types_no = List.length types in
+      List.map (function (n,l) -> (n+types_no,types@l)) subsets
+    in
+    let all_constants = 
+     let all = match main with None -> types | Some m -> m::types in
+      List.fold_right UriManagerSet.add all constants
+    in
+     compute_with_only ~dbd ~where main subsets all_constants
+  else
+    let subsets = 
+      let subsets = power constants in
+      let types_no = List.length types in
+       if types_no > 0 then  
+        (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
+       else subsets
+      in
+       compute_exactly ~dbd ~facts ~where main subsets
 
   (* match query wrappers *)