X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=15177ddb1331d04b118eea1838e8a9dd2cbc9c45;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=952aa5a575a5ed98d725497fcb41918de92ee787;hpb=5edfd170706c91c5d3a9d3522360b748a2dc034f;p=helm.git diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 952aa5a57..15177ddb1 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -24,6 +24,7 @@ *) open Printf +open MetadataTypes let critical_value = 7 let just_factor = 4 @@ -42,6 +43,12 @@ type rating_criterion = [ `Hits (** order by number of hits, most used objects first *) ] +let default_tables = + (library_obj_tbl,library_rel_tbl,library_sort_tbl,library_count_tbl) + +let current_tables () = + (obj_tbl (),rel_tbl (),sort_tbl (), count_tbl ()) + let tbln n = "table" ^ string_of_int n (* @@ -64,10 +71,11 @@ let mk_positions positions cur_tbl = | `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) + | `MainConclusion (Some r) + | `MainHypothesis (Some r) -> + let depth = MetadataPp.pp_relation r in + sprintf "(%s.h_position = \"%s\" and %s.h_depth %s)" + cur_tbl pos_str cur_tbl depth) (positions :> MetadataTypes.position list)) ^ ")" @@ -89,32 +97,35 @@ let add_diff_constr tbl where = function let op, card = explode_card_constr constr in (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where) -let add_all_constr tbl (n,from,where) concl full diff = +let add_all_constr ?(tbl=library_count_tbl) (n,from,where) concl full diff = match (concl, full, diff) with | None, None, None -> (n,from,where) | _ -> - let where = add_card_constr tbl "conclusion" where concl in - let where = add_card_constr tbl "statement" where full in - let where = add_diff_constr tbl where diff in - (n,tbl :: from, + let cur_tbl = tbln n in + let from = (sprintf "%s as %s" tbl cur_tbl) :: from in + let where = add_card_constr cur_tbl "conclusion" where concl in + let where = add_card_constr cur_tbl "statement" where full in + let where = add_diff_constr cur_tbl where diff in + (n+2,from, (if n > 0 then - sprintf "table0.source = %s.source" tbl :: where + sprintf "table0.source = %s.source" cur_tbl :: where else where)) -let add_constraint tables (n,from,where) metadata = +let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata = let obj_tbl,rel_tbl,sort_tbl,count_tbl = tables in let cur_tbl = tbln n in + let start_table = tbln start in match metadata with | `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]) @ + (if n=start then [] + else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ where in ((n+2), from, where) @@ -122,8 +133,8 @@ let add_constraint tables (n,from,where) metadata = let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in let where = mk_positions positions cur_tbl :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ + (if n=start then [] + else [sprintf "%s.source = %s.source" start_table cur_tbl]) @ where in ((n+2), from, where) @@ -133,13 +144,30 @@ let add_constraint tables (n,from,where) metadata = let where = (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) :: mk_positions positions cur_tbl :: - (if n=0 then + (if n=start then [] else - [sprintf "table0.source = %s.source" cur_tbl ]) @ where + [sprintf "%s.source = %s.source" start_table cur_tbl ]) @ where in ((n+2), from, where) +let exec ~(dbd:Mysql.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 + | Some `Hits -> + sprintf + ("select 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 + (fun row -> match row.(0) with Some s -> s | _ -> assert false) + let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables (metadata: MetadataTypes.constr list) @@ -149,48 +177,25 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables 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 + List.fold_left (add_constraint ~tables) (0,[],[]) metadata in - let selected = if metadata = [] then count_tbl else "table0" in let (n,from,where) = - add_all_constr count_tbl (n,from,where) concl_card full_card diff - in - let from = String.concat ", " from in - let where = String.concat " and " where in - let query = - match rating with - | None -> sprintf "select %s.source from %s where %s" selected from where - | Some `Hits -> - sprintf - ("select %s.source from %s, hits where %s" - ^^ " and hits.source = %s.source order by hits.no desc") - selected from where selected + add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff in - prerr_endline query; - let result = Mysql.exec dbd query in - Mysql.map result - (fun row -> match row.(0) with Some s -> s | _ -> assert false) - + exec ~dbd ?rating (n,from,where) let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating (metadata: MetadataTypes.constr list) = - let module MT = MetadataTypes in - if MT.are_tables_ownerized () then - (at_least ~dbd ?concl_card ?full_card ?diff ?rating - (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (), MT.count_tbl ()) - metadata) - @ - (at_least ~dbd ?concl_card ?full_card ?diff ?rating - (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_count_tbl) - metadata) + 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) else - at_least ~dbd ?concl_card ?full_card ?diff ?rating - (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl, - MT.library_count_tbl) - metadata + at_least + ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata (** Prefix handling *) @@ -466,7 +471,7 @@ 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";