X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=73e6f288dfd3b4e3b5815842684177d929a92717;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=3a985deb9304c34537029fab103294cc9648198a;hpb=7403c949ea3a84624f8c05deee00de53336937ba;p=helm.git diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 3a985deb9..73e6f288d 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) @@ -39,91 +39,128 @@ type cardinality_condition = let tbln n = "table" ^ string_of_int n +(* let add_depth_constr depth_opt cur_tbl where = match depth_opt with | None -> where | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where +*) + +let mk_positions positions cur_tbl = + "(" ^ + String.concat " or " + (List.map + (fun pos -> + let pos_str = MetadataPp.pp_position_tag pos in + match pos with + | `InBody + | `InConclusion + | `InHypothesis + | `MainConclusion None + | `MainHypothesis None -> + sprintf "%s.h_position = \"%s\"" cur_tbl pos_str + | `MainConclusion (Some d) + | `MainHypothesis (Some d) -> + sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)" + cur_tbl pos_str cur_tbl d) + (positions :> MetadataTypes.position list)) ^ + ")" let add_card_constr tbl (n,from,where) = function | None -> (n,from,where) | Some (Eq card) -> + let cur_tbl = tbln n in (n+1, - (sprintf "%s as %s" tbl (tbln n) :: from), - (sprintf "no=%d" card :: + (sprintf "%s as %s" tbl cur_tbl :: from), + (sprintf "%s.no=%d" cur_tbl card :: (if n=0 then [] - else [sprintf "table0.source = %s.source" (tbln n)]) @ + else [sprintf "table0.source = %s.source" cur_tbl]) @ where)) | Some (Gt card) -> + let cur_tbl = tbln n in (n+1, - (sprintf "%s as %s" tbl (tbln n) :: from), - (sprintf "no>%d" card :: + (sprintf "%s as %s" tbl cur_tbl :: from), + (sprintf "%s.no>%d" cur_tbl card :: (if n=0 then [] - else [sprintf "table0.source = %s.source" (tbln n)]) @ + else [sprintf "table0.source = %s.source" cur_tbl]) @ where)) -let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card - (metadata: MetadataTypes.metadata list) +let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card tables + (metadata: MetadataTypes.constr list) = if (metadata = []) && concl_card = None && full_card = None then failwith "MetadataQuery.at_least: no constraints given"; + let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,conclno_hyp_tbl = tables in let add_constraint (n,from,where) metadata = let cur_tbl = tbln n in match metadata with - | `Obj (uri, pos, depth_opt) -> - let tbl = MetadataTypes.obj_tbl in - let pos_str = MetadataPp.pp_position pos in - let from = (sprintf "%s as %s" tbl cur_tbl) :: from in - let where = - (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: - (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) :: + | `Obj (uri, positions) -> + let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in + let where = + (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) :: + mk_positions positions cur_tbl :: (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ + else [sprintf "table0.source = %s.source" cur_tbl]) @ where in - let where = add_depth_constr depth_opt cur_tbl where in - ((n+1), from, where) - | `Rel (pos, depth) -> - let tbl = MetadataTypes.rel_tbl in - let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in - let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + ((n+2), from, where) + | `Rel positions -> + let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in let where = - (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: + mk_positions positions cur_tbl :: (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ + else [sprintf "table0.source = %s.source" cur_tbl]) @ where in - let where = add_depth_constr (Some depth) cur_tbl where in - ((n+1), from, where) - | `Sort (sort, pos, depth) -> - let tbl = MetadataTypes.sort_tbl in - let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in - let sort_str = MetadataPp.pp_sort sort in - let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + ((n+2), from, where) + | `Sort (sort, positions) -> + let sort_str = CicPp.ppsort sort in + let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in let where = - (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) :: - (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where + (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) :: + mk_positions positions cur_tbl :: + (if n=0 then + [] + else + [sprintf "table0.source = %s.source" cur_tbl ]) @ where in - let where = add_depth_constr (Some depth) cur_tbl where in - ((n+1), from, where) + ((n+2), from, where) in let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in let (n,from,where) = - add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card + add_card_constr conclno_tbl (n,from,where) concl_card in let (n,from,where) = - add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card + add_card_constr conclno_hyp_tbl (n,from,where) full_card in 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 -prerr_endline query; - 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) +let at_least + ~(dbd:Mysql.dbd) ?concl_card ?full_card (metadata: MetadataTypes.constr list) += + let module MT = MetadataTypes in + if MT.are_tables_ownerized () then + (at_least ~dbd ?concl_card ?full_card + (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), + MT.conclno_tbl (),MT.conclno_hyp_tbl ()) + metadata) + @ + (at_least ~dbd ?concl_card ?full_card + (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, + MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) + metadata) + else + at_least ~dbd ?concl_card ?full_card + (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, + MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) + metadata + + (** Prefix handling *) let filter_by_card n = @@ -154,8 +191,8 @@ and add_root n root childs = (SetSet.singleton (StringSet.singleton root)) and inspect_conclusion n t = -if n = 0 then SetSet.empty -else match t with + if n = 0 then SetSet.empty + else match t with Cic.Rel _ | Cic.Meta _ | Cic.Sort _ @@ -346,55 +383,82 @@ let union l = | u::l -> u::(drop_repetitions l) in drop_repetitions (List.sort Pervasives.compare (List.concat l)) -let must_of_prefix m s = - let s' = List.map (fun u -> `Obj (u, `InConclusion, None)) s in - `Obj (m, `MainConclusion, None) :: s' +let must_of_prefix ?(where = `Conclusion) m s = + let positions = + match where with + | `Conclusion -> [`InConclusion] + | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None] + in + let s' = List.map (fun u -> `Obj (u, positions)) s in + `Obj (m, [`MainConclusion None]) :: s' let escape = Str.global_replace (Str.regexp_string "\'") "\\'" -let get_inconcl (dbh:Dbi.connection) uri = +let get_constants (dbd:Mysql.dbd) ~where uri = let uri = escape uri in + let positions = + match where with + | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""] + | `Statement -> + ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\""; + "\"MainHypothesis\""] + in let query = - dbh#prepare (sprintf "select h_occurrence from refObj where source=\"%s\" and (h_position=\"MainConclusion\" or h_position=\"InConclusion\")" - uri) + 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 (String.concat " OR " positions) + MetadataTypes.library_obj_tbl 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 test_only ~(dbh:Dbi.connection) only u = - let inconcl = get_inconcl dbh 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"; +(* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *) 0,"cic:/Coq/Init/Logic/trans_eq.con"; 0,"cic:/Coq/Init/Logic/f_equal.con"; 0,"cic:/Coq/Init/Logic/f_equal2.con"; 0,"cic:/Coq/Init/Logic/f_equal3.con"] -let compute_exactly ~(dbh:Dbi.connection) 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 = - at_least ~dbh ~concl_card:(Eq (m+1)) (must_of_prefix main s) + 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 in List.map (fun uri -> (m, uri)) res) prefixes) (* critical value reached, fallback to "only" constraints *) -let compute_with_only ~(dbh:Dbi.connection) main prefixes constants = + +let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) + main prefixes constants += let max_prefix_length = match prefixes with | [] -> assert false @@ -410,24 +474,29 @@ let compute_with_only ~(dbh:Dbi.connection) main prefixes constants = union (List.map (fun (m,s) -> + let must = must_of_prefix ~where main s in (let res = - at_least ~dbh ~concl_card:(Gt (m+1)) (must_of_prefix main s) + match where with + | `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) -> test_only ~dbh constants uri) all in - let equal_to = compute_exactly ~dbh 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 in if (constants_no > critical_value) then let prefixes = prefixes just_factor t in @@ -436,25 +505,32 @@ 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 if constants_no = 0 then [] else (* in this case we compute all prefixes, and we do not need to apply the only constraints *) - let prefixes = prefixes constants_no t in + let prefixes = + if constants_no = 0 then + (if types_no = 0 then + Some main, [0, []] + else + Some main, [0, []; types_no, types]) + else + prefixes (constants_no+types_no+1) t + in (match prefixes with - Some main, all_concl -> - List.concat - (List.map - (fun (m,s) -> - (let res = - at_least ~dbh ~concl_card:(Eq (m+1)) - (must_of_prefix main s) - in - List.map (fun uri -> (m, uri)) res)) - all_concl) - | _, _ -> []) + 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) *) + | _, _ -> []) let power_upto upto consts = let l = StringSet.elements consts in @@ -472,7 +548,10 @@ let power consts = (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res)) [(0,[])] l) -let sigmatch ~(dbh:Dbi.connection) (main, constants) = +type where = [ `Conclusion | `Statement ] + +let sigmatch ~(dbd:Mysql.dbd) + ?(facts=false) ?(where = `Conclusion) (main, constants) = match main with None -> [] | Some (main, types) -> @@ -486,22 +565,26 @@ let sigmatch ~(dbh:Dbi.connection) (main, constants) = let all_constants = List.fold_right StringSet.add types (StringSet.add main constants) in - compute_with_only ~dbh 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 - List.map (function (n,l) -> (n+types_no,types@l)) subsets + if types_no > 0 then + (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets + else subsets in - compute_exactly ~dbh 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