X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=2ebd46c2a69478986d70cb2b47f4082d257dfc08;hb=6e986001aac7cc63b0e7d13447caae3729e0f833;hp=3a0b63d9e5f5948d9fc21b7178b4de68dfaa3e52;hpb=b6658a4a5c874be0223f44c7c1b99900185cbc60;p=helm.git diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 3a0b63d9e..2ebd46c2a 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -25,8 +25,8 @@ open Printf -let critical_value = 6 -let just_factor = 3 +let critical_value = 7 +let just_factor = 4 module StringSet = Set.Make (String) module SetSet = Set.Make (StringSet) @@ -85,7 +85,7 @@ let add_card_constr tbl (n,from,where) = function else [sprintf "table0.source = %s.source" cur_tbl]) @ where)) -let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card +let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card (metadata: MetadataTypes.constr list) = if (metadata = []) && concl_card = None && full_card = None then @@ -137,9 +137,9 @@ let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card 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 query = dbh#prepare query in - query#execute []; - List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ()) + let result = Mysql.exec dbd query in + Mysql.map result + (fun row -> match row.(0) with Some s -> s | _ -> assert false) (** Prefix handling *) @@ -374,7 +374,7 @@ let must_of_prefix ?(where = `Conclusion) m s = let escape = Str.global_replace (Str.regexp_string "\'") "\\'" -let get_constants (dbh:Dbi.connection) ~where uri = +let get_constants (dbd:Mysql.dbd) ~where uri = let uri = escape uri in let positions = match where with @@ -384,24 +384,27 @@ let get_constants (dbh:Dbi.connection) ~where uri = "\"MainHypothesis\""] in let query = - dbh#prepare - (sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)" - uri (String.concat " or " positions)) + sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)" + uri (String.concat " or " positions) in - query#execute []; - query#fold_left (* transform the result in a set *) - (fun set fields -> - let uri = match fields with [`String uri] -> uri | _ -> assert false in - StringSet.add uri set) - StringSet.empty - -let at_most ~(dbh:Dbi.connection) ?(where = `Conclusion) only u = - let inconcl = get_constants dbh ~where u in + let result = Mysql.exec dbd query in + let set = ref StringSet.empty in + Mysql.iter result + (fun col -> + match col.(0) with + | Some uri -> set := StringSet.add uri !set + | _ -> assert false); + !set + +let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u = + let inconcl = get_constants dbd ~where u in StringSet.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)"] let myspeciallist = [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"; 0,"cic:/Coq/Init/Logic/sym_eq.con"; @@ -410,25 +413,28 @@ let myspeciallist = 0,"cic:/Coq/Init/Logic/f_equal2.con"; 0,"cic:/Coq/Init/Logic/f_equal3.con"] -let compute_exactly ~(dbh:Dbi.connection) where main prefixes = + +let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes = List.concat (List.map (fun (m,s) -> - if (m = 0) then - myspeciallist + if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then + (if facts then myspeciallist_of_facts + else myspeciallist) else let res = let must = must_of_prefix ~where main s in match where with - | `Conclusion -> at_least ~dbh ~concl_card:(Eq (m+1)) must - | `Statement -> at_least ~dbh ~full_card:(Eq (m+1)) must + | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must + | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must in List.map (fun uri -> (m, uri)) res) prefixes) (* critical value reached, fallback to "only" constraints *) -let compute_with_only ~(dbh:Dbi.connection) ?(where = `Conclusion) main - prefixes constants + +let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) + main prefixes constants = let max_prefix_length = match prefixes with @@ -448,26 +454,27 @@ let compute_with_only ~(dbh:Dbi.connection) ?(where = `Conclusion) main let must = must_of_prefix ~where main s in (let res = match where with - | `Conclusion -> at_least ~dbh ~concl_card:(Gt (m+1)) must - | `Statement -> at_least ~dbh ~full_card:(Gt (m+1)) must + | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must + | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must in (* we tag the uri with m+1, for sorting purposes *) List.map (fun uri -> (m+1, uri)) res)) maximal_prefixes) in - List.filter (function (_,uri) -> at_most ~dbh ~where constants uri) all in - let equal_to = compute_exactly ~dbh where main prefixes 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 ~(dbh:Dbi.connection) t = + +let cmatch ~(dbd:Mysql.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 + types_no in + let constants_no = StringSet.cardinal constants in if (constants_no > critical_value) then let prefixes = prefixes just_factor t in (match prefixes with @@ -475,26 +482,31 @@ let cmatch ~(dbh:Dbi.connection) t = let all_constants = List.fold_right StringSet.add types (StringSet.add main constants) in - compute_with_only ~dbh main all_concl all_constants + compute_with_only ~dbd ~facts main all_concl all_constants | _, _ -> []) else (* in this case we compute all prefixes, and we do not need to apply the only constraints *) let prefixes = if constants_no = 0 then - Some main, [0, []; types_no, types] + (if types_no = 0 then + Some main, [0, []] + else + Some main, [0, []; types_no, types]) else - prefixes constants_no t + prefixes (constants_no+types_no) 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 ~dbh ~concl_card:(Eq (m+1)) must in + let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in List.map (fun uri -> (m, uri)) res) - all_concl) + all_concl) *) | _, _ -> []) let power_upto upto consts = @@ -515,7 +527,8 @@ let power consts = type where = [ `Conclusion | `Statement ] -let sigmatch ~(dbh:Dbi.connection) ?(where = `Conclusion) (main, constants) = +let sigmatch ~(dbd:Mysql.dbd) + ?(facts=false) ?(where = `Conclusion) (main, constants) = match main with None -> [] | Some (main, types) -> @@ -529,22 +542,24 @@ let sigmatch ~(dbh:Dbi.connection) ?(where = `Conclusion) (main, constants) = let all_constants = List.fold_right StringSet.add types (StringSet.add main constants) in - compute_with_only ~dbh ~where main subsets all_constants + compute_with_only ~dbd ~where main subsets all_constants else let subsets = let subsets = power constants in let types_no = List.length types in (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets in - compute_exactly ~dbh where main subsets + compute_exactly ~dbd ~facts ~where main subsets (* match query wrappers *) -let cmatch' = cmatch -let cmatch ~dbh term = + +let cmatch'= cmatch + +let cmatch ~dbd ?(facts=false) term = List.map snd (List.sort (fun x y -> Pervasives.compare (fst y) (fst x)) - (cmatch' ~dbh term)) + (cmatch' ~dbd ~facts term)) let constants_of = signature_concl