X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=7bc92eb66b136c6c2c8ee6b46f4d42f1ad3469f4;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d18663fadcaea3998f1267915967827c0ce83611;hpb=9eee519f40a2cf6dfaaaa0c5e37d23ad8748552c;p=helm.git diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index d18663fad..7bc92eb66 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -27,7 +27,7 @@ open Printf open MetadataTypes let critical_value = 7 -let just_factor = 4 +let just_factor = 3 module UriManagerSet = UriManager.UriSet module SetSet = Set.Make (UriManagerSet) @@ -151,7 +151,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata = in ((n+2), from, where) -let exec ~(dbd:Mysql.dbd) ?rating (n,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 = @@ -163,13 +163,13 @@ let exec ~(dbd:Mysql.dbd) ?rating (n,from,where) = and table0.source = hits.source order by hits.no desc") from where in -(* prerr_endline query; *) - let result = Mysql.exec dbd query in - Mysql.map result + (* 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:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables +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 @@ -185,7 +185,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables exec ~dbd ?rating (n,from,where) let at_least - ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating + ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating (metadata: MetadataTypes.constr list) = if are_tables_ownerized () then @@ -432,7 +432,7 @@ let must_of_prefix ?(where = `Conclusion) m s = let escape = Str.global_replace (Str.regexp_string "\'") "\\'" -let get_constants (dbd:Mysql.dbd) ~where uri = +let get_constants (dbd:HMysql.dbd) ~where uri = let uri = escape (UriManager.string_of_uri uri) in let positions = match where with @@ -452,16 +452,16 @@ let get_constants (dbd:Mysql.dbd) ~where uri = MetadataTypes.library_obj_tbl uri pos_predicate in - let result = Mysql.exec dbd query in + let result = HMysql.exec dbd query in let set = ref UriManagerSet.empty in - Mysql.iter result + HMysql.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:Mysql.dbd) ?(where = `Conclusion) only u = +let at_most ~(dbd:HMysql.dbd) ?(where = `Conclusion) only u = let inconcl = get_constants dbd ~where u in UriManagerSet.subset inconcl only @@ -479,7 +479,7 @@ let myspeciallist = 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) -> @@ -510,7 +510,7 @@ let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main 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 = @@ -523,7 +523,7 @@ 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 @@ -539,13 +539,14 @@ let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 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 -> [] @@ -584,8 +585,10 @@ let power_upto upto consts = 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 = @@ -597,7 +600,7 @@ let power consts = type where = [ `Conclusion | `Statement ] -let sigmatch ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) +let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) (main, constants) = let main,types = @@ -606,9 +609,12 @@ let sigmatch ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) | 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 @@ -616,7 +622,7 @@ let sigmatch ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 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 + compute_with_only ~dbd ~where main subsets all_constants else let subsets = let subsets = power constants in