X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataConstraints.ml;h=3e8ac2f7250c3aa29ec3bffa835589c0711fe365;hb=320c0f89a7e31e996b6eff2b4165eb74e8141cec;hp=07fcc738b0b2fee951580106307200b4823f505c;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml index 07fcc738b..3e8ac2f72 100644 --- a/helm/software/components/metadata/metadataConstraints.ml +++ b/helm/software/components/metadata/metadataConstraints.ml @@ -28,8 +28,11 @@ open Printf open MetadataTypes +let debug = false +let debug_print s = if debug then prerr_endline (Lazy.force s) + let critical_value = 7 -let just_factor = 3 +let just_factor = 1 module UriManagerSet = UriManager.UriSet module SetSet = Set.Make (UriManagerSet) @@ -153,7 +156,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 dbtype ~(dbd:HSql.dbd) ?rating (n,from,where) = let from = String.concat ", " from in let where = String.concat " and " where in let query = @@ -165,39 +168,58 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) = 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 + (* debug_print (lazy query); *) + let result = HSql.exec dbtype dbd query in + HSql.map result + ~f:(fun row -> + match row.(0) with Some s -> UriManager.uri_of_string s + | _ -> assert false) +;; + +let at_least dbtype ~(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 dbtype ~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 - (at_least - ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @ - (at_least - ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata) + at_least + HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating + default_tables metadata + @ + at_least + HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating + default_tables metadata + @ + at_least + HSql.User ~dbd ?concl_card ?full_card ?diff ?rating + (current_tables ()) metadata + else at_least - ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata + HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating + default_tables metadata + @ + at_least + HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating + default_tables metadata (** Prefix handling *) @@ -250,8 +272,9 @@ and inspect_conclusion n t = merge n (inspect_conclusion n s) (inspect_conclusion n t) | Cic.Lambda (_, s, t) -> merge n (inspect_conclusion n s) (inspect_conclusion n t) - | Cic.LetIn (_, s, t) -> - merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.LetIn (_, s, ty, t) -> + merge n (inspect_conclusion n s) + (merge n (inspect_conclusion n ty) (inspect_conclusion n t)) | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> add_root (n-1) u l | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> @@ -289,7 +312,7 @@ let rec inspect_term n t = 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.LetIn (_, _, _, t) -> inspect_term n t | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> let childunion = inspect_children (n-1) l in Some u, childunion @@ -358,18 +381,28 @@ and signature_concl = | Cic.Const (u,exp_named_subst) -> UriManagerSet.singleton u | Cic.MutInd (u, t, exp_named_subst) -> + let rec projections_of uris = + List.flatten + (List.map + (fun uri -> + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + projections_of (CicUtil.projections_of_record o uri)) + uris) + in let uri = UriManager.uri_of_uriref u t None in - UriManagerSet.singleton uri + List.fold_right UriManagerSet.add + (projections_of [u]) (UriManagerSet.singleton uri) | Cic.MutConstruct (u, t, c, exp_named_subst) -> let uri = UriManager.uri_of_uriref u t (Some c) in - UriManagerSet.singleton uri + UriManagerSet.singleton uri | Cic.Cast (t, _) -> signature_concl t | Cic.Prod (_, s, t) -> UriManagerSet.union (signature_concl s) (signature_concl t) | Cic.Lambda (_, s, t) -> UriManagerSet.union (signature_concl s) (signature_concl t) - | Cic.LetIn (_, s, t) -> - UriManagerSet.union (signature_concl s) (signature_concl t) + | Cic.LetIn (_, s, ty, t) -> + UriManagerSet.union (signature_concl s) + (UriManagerSet.union (signature_concl ty) (signature_concl t)) | Cic.Appl l -> add l | Cic.MutCase _ | Cic.Fix _ @@ -379,12 +412,12 @@ and signature_concl = let rec signature_of = function | Cic.Cast (t, _) -> signature_of t | Cic.Prod (_, _, t) -> signature_of t - | Cic.LetIn (_, _, t) -> signature_of t + | Cic.LetIn (_, _, _, t) -> signature_of t | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> Some (u, []), add l | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> let suri = UriManager.uri_of_uriref u t None in - if u = HelmLibraryObjects.Logic.eq_URI then + if LibraryObjects.is_eq_URI u 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 *) @@ -400,7 +433,7 @@ let rec signature_of = function 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, []), UriManagerSet.empty + | _ :: tl -> Some (suri, []), add tl | _ -> assert false (* args number must be > 0 *) else Some (suri, []), add l @@ -434,7 +467,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 @@ -443,27 +476,33 @@ let get_constants (dbd:HMysql.dbd) ~where uri = [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos; MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ] in - let query = - 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 - + let pos_predicate = + String.concat " OR " + (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions) + in + let query tbl = + sprintf "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)" + tbl uri pos_predicate + in + let db = [ + HSql.Library, MetadataTypes.library_obj_tbl; + HSql.Legacy, MetadataTypes.library_obj_tbl; + HSql.User, MetadataTypes.obj_tbl ()] in - 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 := UriManagerSet.add (UriManager.uri_of_string uri) !set - | _ -> assert false); + List.iter + (fun (dbtype, table) -> + let result = HSql.exec dbtype dbd (query table) in + HSql.iter result + (fun col -> + match col.(0) with + | Some uri -> + set := UriManagerSet.add (UriManager.uri_of_string uri) !set + | _ -> assert false)) + db; !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 +520,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 +551,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 = @@ -541,14 +580,19 @@ let compute_with_only ~(dbd:HMysql.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 +(* 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 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 +646,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 = @@ -611,29 +655,34 @@ let sigmatch ~(dbd:HMysql.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)); *) + (* debug_print (lazy (("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 + (* let _ = debug_print (lazy (("subsets: ")^ + (string_of_int (List.length subsets)))) in *) + 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 + debug_print (lazy ("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 + (debug_print (lazy ("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 + debug_print (lazy "fine1"); + compute_exactly ~dbd ~facts ~where main subsets) (* match query wrappers *)