X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataConstraints.ml;h=c2dee6f5edb40cdc839ea5df43f1d8f56e96f800;hb=7dbc6d6fe71f6967f5ad31528a629dc89e6d8160;hp=6cab493fce46d067aa46c33f93d58d27e0a5d7f7;hpb=765e519a1c3326ba72315cf7942eea1330b25e4d;p=helm.git

diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml
index 6cab493fc..c2dee6f5e 100644
--- a/helm/software/components/metadata/metadataConstraints.ml
+++ b/helm/software/components/metadata/metadataConstraints.ml
@@ -29,7 +29,7 @@ open Printf
 open MetadataTypes 
 
 let critical_value = 7
-let just_factor = 3
+let just_factor = 1
 
 module UriManagerSet = UriManager.UriSet
 module SetSet = Set.Make (UriManagerSet)
@@ -153,7 +153,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
       in
       ((n+2), from, where)
 
-let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
+let exec ~(dbd:HSql.dbd) ?rating (n,from,where) =
   let from = String.concat ", " from in
   let where = String.concat " and " where in
   let query =
@@ -166,28 +166,32 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
           from where 
   in
   (* prerr_endline query; *) 
-  let result = HMysql.exec dbd query in
-  HMysql.map result
+  let result = HSql.exec dbd query in
+  HSql.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
+let at_least ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
   (metadata: MetadataTypes.constr list)
 =
-  let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables 
-  in
+  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 (n,from,where) =
-    List.fold_left (add_constraint ~tables) (0,[],[]) metadata
-  in
-  let (n,from,where) =
-    add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
-  in
-  exec ~dbd ?rating (n,from,where)
+    begin
+      HLog.warn "MetadataConstraints.at_least: no constraints given";
+      []
+    end
+  else
+    let (n,from,where) =
+      List.fold_left (add_constraint ~tables) (0,[],[]) metadata
+    in
+    let (n,from,where) =
+      add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
+    in
+    exec ~dbd ?rating (n,from,where)
+;;
     
 let at_least  
-  ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
+  ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating
       (metadata: MetadataTypes.constr list)
 =
   if are_tables_ownerized () then
@@ -434,7 +438,7 @@ let must_of_prefix ?(where = `Conclusion) m s =
 
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 
-let get_constants (dbd:HMysql.dbd) ~where uri =
+let get_constants (dbd:HSql.dbd) ~where uri =
   let uri = escape (UriManager.string_of_uri uri) in
   let positions =
     match where with
@@ -454,16 +458,16 @@ let get_constants (dbd:HMysql.dbd) ~where uri =
       MetadataTypes.library_obj_tbl uri pos_predicate
       
   in
-  let result = HMysql.exec dbd query in
+  let result = HSql.exec dbd query in
   let set = ref UriManagerSet.empty in
-  HMysql.iter result
+  HSql.iter result
     (fun col ->
       match col.(0) with
       | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
       | _ -> assert false);
   !set
 
-let at_most ~(dbd:HMysql.dbd) ?(where = `Conclusion) only u =
+let at_most ~(dbd:HSql.dbd) ?(where = `Conclusion) only u =
   let inconcl = get_constants dbd ~where u in
   UriManagerSet.subset inconcl only
 
@@ -481,7 +485,7 @@ let myspeciallist =
    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"]
 
 
-let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
+let compute_exactly ~(dbd:HSql.dbd) ?(facts=false) ~where main prefixes =
   List.concat
     (List.map 
       (fun (m,s) -> 
@@ -512,7 +516,7 @@ let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
 
   (* critical value reached, fallback to "only" constraints *)
 
-let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) 
+let compute_with_only ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion) 
   main prefixes constants
 =
   let max_prefix_length = 
@@ -542,13 +546,18 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
           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
+(*
+    List.filter (function (_,uri) -> 
+      at_most ~dbd ~where constants uri) 
+*)
+    all 
+    in
   let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
     greater_than @ equal_to
 
   (* real match query implementation *)
 
-let cmatch ~(dbd:HMysql.dbd)  ?(facts=false) t =
+let cmatch ~(dbd:HSql.dbd)  ?(facts=false) t =
   let (main, constants) = signature_of t in
   match main with
   | None -> []
@@ -602,7 +611,7 @@ let power consts =
 
 type where = [ `Conclusion | `Statement ]
 
-let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let sigmatch ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion)
  (main, constants)
 =
  let main,types =
@@ -617,23 +626,28 @@ let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
       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
+      let types_no = List.length types in 
+	if types_no > 0 then  
+          List.map (function (n,l) -> (n+types_no,types@l)) subsets
+	else subsets
     in
+    prerr_endline ("critical_value exceded..." ^ string_of_int constants_no);
     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
+    (prerr_endline ("all subsets..." ^ string_of_int constants_no);
     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
+    in
+       prerr_endline "fine1";
+       compute_exactly ~dbd ~facts ~where main subsets)
 
   (* match query wrappers *)