X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=7bc92eb66b136c6c2c8ee6b46f4d42f1ad3469f4;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=602ee49b93966cac2868be492445bc42b52441d7;hpb=a458a3e72fd374b106481a7e98f4000369c6ae61;p=helm.git diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 602ee49b9..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,25 +151,25 @@ 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 = match rating with - | None -> sprintf "select table0.source from %s where %s" from where + | None -> sprintf "select distinct table0.source from %s where %s" from where | Some `Hits -> sprintf - ("select table0.source from %s, hits where %s + ("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 = 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 @@ -350,7 +350,9 @@ and signature_concl = | Cic.Meta _ | Cic.Sort _ | Cic.Implicit _ -> UriManagerSet.empty - | Cic.Var (u,exp_named_subst) -> 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) -> UriManagerSet.singleton u | Cic.MutInd (u, t, exp_named_subst) -> @@ -421,12 +423,16 @@ let must_of_prefix ?(where = `Conclusion) m s = | `Conclusion -> [`InConclusion] | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None] in + 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 - `Obj (m, [`MainConclusion None]) :: s' + 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 get_constants (dbd:HMysql.dbd) ~where uri = let uri = escape (UriManager.string_of_uri uri) in let positions = match where with @@ -446,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 @@ -473,26 +479,38 @@ 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) -> - if ((m = 0) && (UriManager.eq main (UriManager.uri_of_string (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 = @@ -505,28 +523,30 @@ 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 -> [] @@ -541,7 +561,7 @@ let cmatch ~(dbd:Mysql.dbd) ?(facts=false) t = let all_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 @@ -557,15 +577,7 @@ 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 = @@ -573,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 = @@ -586,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 = UriManagerSet.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 UriManagerSet.add types (UriManagerSet.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 *)