X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=15177ddb1331d04b118eea1838e8a9dd2cbc9c45;hb=aca103d3c3d740efcc0bcc2932922cff77facb49;hp=3e9cd9c5a37942e6df4a9c1ebb9c9105d2da5187;hpb=71b71ad9ccda0f26a25f3a5ad7e1697025d207a9;p=helm.git diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 3e9cd9c5a..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)) ^ ")" @@ -76,43 +84,48 @@ let explode_card_constr = function | Gt card -> ">", card | Lt card -> "<", card -let add_card_constr tbl (n,from,where) = function - | None -> (n,from,where) +let add_card_constr tbl col where = function + | None -> where | Some constr -> - let cur_tbl = tbln n in let op, card = explode_card_constr constr in - (n+1, - (sprintf "%s as %s" tbl cur_tbl :: from), - (sprintf "%s.no %s %d" cur_tbl op card :: - (if n=0 then [] - else [sprintf "table0.source = %s.source" cur_tbl]) @ - where)) - -let add_diff_constr conclno_tbl hypno_tbl (n,from,where) = function - | None -> (n,from,where) + (* count(_utente).hypothesis = 3 *) + (sprintf "%s.%s %s %d" tbl col op card :: where) + +let add_diff_constr tbl where = function + | None -> where | Some constr -> - let cur_tbl1, cur_tbl2 = tbln n, tbln (n+1) in let op, card = explode_card_constr constr in - (n+2, - (sprintf "%s as %s" conclno_tbl cur_tbl1 :: - sprintf "%s as %s" hypno_tbl cur_tbl2 :: from), - (sprintf "%s.no - %s.no %s %d" cur_tbl2 cur_tbl1 op card :: - (if n=0 then assert false - else [sprintf "table0.source = %s.source" cur_tbl1; - sprintf "table0.source = %s.source" cur_tbl2]) @ - where)) - -let add_constraint tables (n,from,where) metadata = - let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in + (sprintf "%s.hypothesis - %s.conclusion %s %d" tbl tbl op card :: where) + +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 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" cur_tbl :: where + else + where)) + + +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) @@ -120,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) @@ -131,73 +144,58 @@ 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 at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff ?rating tables - (metadata: MetadataTypes.constr list) -= - let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_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_card_constr conclno_tbl (n,from,where) concl_card - in - let (n,from,where) = - add_card_constr fullno_tbl (n,from,where) full_card - in - let (n,from,where) = - add_diff_constr conclno_tbl hypno_tbl (n,from,where) diff - in +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 -(* - sprintf - ("select table0.source from %s, %s where %s and %s.source = table0.source" - ^^ " order by %s.no") - from fullno_tbl where fullno_tbl fullno_tbl - *) | None -> sprintf "select table0.source from %s where %s" from where | Some `Hits -> sprintf - ("select table0.source from %s, hits where %s" - ^^ " and hits.source = table0.source order by hits.no desc") - from where + ("select table0.source from %s, hits where %s + and table0.source = hits.source order by hits.no desc") + from where in -(* prerr_endline query; *) +(* 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) += + 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) + 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.conclno_tbl (),MT.fullno_tbl (),MT.hypno_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_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_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_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) - metadata + at_least + ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata (** Prefix handling *) @@ -473,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";