From: Stefano Zacchiroli Date: Fri, 29 Apr 2005 08:04:17 +0000 (+0000) Subject: added rating parameter to at_least (used by elim) X-Git-Tag: single_binding~142 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=71b71ad9ccda0f26a25f3a5ad7e1697025d207a9;p=helm.git added rating parameter to at_least (used by elim) --- diff --git a/helm/ocaml/metadata/.depend b/helm/ocaml/metadata/.depend index bb47a0559..e2a4669b3 100644 --- a/helm/ocaml/metadata/.depend +++ b/helm/ocaml/metadata/.depend @@ -7,11 +7,11 @@ metadataExtractor.cmo: metadataTypes.cmi metadataExtractor.cmi metadataExtractor.cmx: metadataTypes.cmx metadataExtractor.cmi metadataPp.cmo: metadataTypes.cmi metadataPp.cmi metadataPp.cmx: metadataTypes.cmx metadataPp.cmi -metadataDb.cmo: metadataExtractor.cmi metadataPp.cmi metadataTypes.cmi \ +metadataDb.cmo: metadataTypes.cmi metadataPp.cmi metadataExtractor.cmi \ metadataDb.cmi -metadataDb.cmx: metadataExtractor.cmx metadataPp.cmx metadataTypes.cmx \ +metadataDb.cmx: metadataTypes.cmx metadataPp.cmx metadataExtractor.cmx \ metadataDb.cmi -metadataConstraints.cmo: metadataPp.cmi metadataTypes.cmi \ +metadataConstraints.cmo: metadataTypes.cmi metadataPp.cmi \ metadataConstraints.cmi -metadataConstraints.cmx: metadataPp.cmx metadataTypes.cmx \ +metadataConstraints.cmx: metadataTypes.cmx metadataPp.cmx \ metadataConstraints.cmi diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml index 32e34a40a..3e9cd9c5a 100644 --- a/helm/ocaml/metadata/metadataConstraints.ml +++ b/helm/ocaml/metadata/metadataConstraints.ml @@ -38,6 +38,10 @@ type cardinality_condition = | Gt of int | Lt of int +type rating_criterion = + [ `Hits (** order by number of hits, most used objects first *) + ] + let tbln n = "table" ^ string_of_int n (* @@ -134,7 +138,7 @@ let add_constraint tables (n,from,where) metadata = in ((n+2), from, where) -let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff tables +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 @@ -155,13 +159,19 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff tables 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 *) - sprintf "select table0.source from %s where %s" from where + | 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 in (* prerr_endline query; *) let result = Mysql.exec dbd query in @@ -169,22 +179,22 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff tables (fun row -> match row.(0) with Some s -> s | _ -> assert false) let at_least - ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff + ~(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 + (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 + (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) else - at_least ~dbd ?concl_card ?full_card ?diff + 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 diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli index 48143490f..ddf672b7f 100644 --- a/helm/ocaml/metadata/metadataConstraints.mli +++ b/helm/ocaml/metadata/metadataConstraints.mli @@ -59,6 +59,10 @@ type cardinality_condition = | Gt of int | Lt of int +type rating_criterion = + [ `Hits (** order by number of hits, most used objects first *) + ] + (** @param concl_card cardinality condition on conclusion only * @param full_card cardinality condition on the whole statement * @param diff required difference between the number of different constants in @@ -69,6 +73,7 @@ val at_least: ?concl_card:cardinality_condition -> ?full_card:cardinality_condition -> ?diff:cardinality_condition -> + ?rating:rating_criterion -> MetadataTypes.constr list -> string list diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 0e86d8cce..3bc3c566e 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -304,5 +304,5 @@ let elim ~dbd uri = `Obj (uri,[`InHypothesis]); ] in - MetadataConstraints.at_least ~dbd constraints + MetadataConstraints.at_least ~rating:`Hits ~dbd constraints