From: Stefano Zacchiroli <zack@upsilon.cc>
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