X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=3e9cd9c5a37942e6df4a9c1ebb9c9105d2da5187;hb=03d2302343e8e1b282c1b2afec8db7913413d9d1;hp=32e34a40a1592e8b278aedd0c75093d3d5c9fea1;hpb=a4c02907fcf1c5ef8a4b89832808541fcad172e6;p=helm.git

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