X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmetadata%2FmetadataConstraints.ml;h=1b28e44d0b03632ffaec79d66b37f4948d679e58;hb=51d9b14ac63f4d4f045772ccd006b49e87d8f4bc;hp=f7707f90fbb441e7c8fd4a02c67816ad8ba113bd;hpb=282f371ba8533ea0e4e667265f9e4b04856bf972;p=helm.git

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index f7707f90f..1b28e44d0 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -25,8 +25,8 @@
 
 open Printf
 
-let critical_value = 6
-let just_factor = 3
+let critical_value = 7
+let just_factor = 4
 
 module StringSet = Set.Make (String)
 module SetSet = Set.Make (StringSet)
@@ -116,7 +116,7 @@ let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
         ((n+1), from, where)
     | `Sort (sort, positions) ->
         let tbl = MetadataTypes.sort_tbl in
-        let sort_str = MetadataPp.pp_sort sort in
+        let sort_str = CicPp.ppsort sort in
         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
         let where =
           (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
@@ -403,20 +403,24 @@ let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
   (* Special handling of equality. The problem is filtering out theorems just
   * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
   * ad-hoc, no better solution found at the moment *)
+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";
    0,"cic:/Coq/Init/Logic/f_equal3.con"]
 
-let compute_exactly ~(dbd:Mysql.dbd) where main prefixes =
+
+let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
   List.concat
     (List.map 
       (fun (m,s) -> 
-        if (m = 0) then
-          myspeciallist
+        if ((m = 0) && (main = HelmLibraryObjects.Logic.eq_XURI)) then
+          (if facts then myspeciallist_of_facts
+	   else myspeciallist)
         else
           let res =
             let must = must_of_prefix ~where main s in
@@ -428,8 +432,9 @@ let compute_exactly ~(dbd:Mysql.dbd) where main prefixes =
       prefixes)
 
   (* critical value reached, fallback to "only" constraints *)
-let compute_with_only ~(dbd:Mysql.dbd) ?(where = `Conclusion) main
-  prefixes constants
+
+let compute_with_only ~(dbd:Mysql.dbd) ?(facts=false) ?(where = `Conclusion) 
+  main prefixes constants
 =
   let max_prefix_length = 
     match prefixes with
@@ -457,18 +462,19 @@ let compute_with_only ~(dbd:Mysql.dbd) ?(where = `Conclusion) main
           maximal_prefixes)
     in
     List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
-    let equal_to = compute_exactly ~dbd where main prefixes in
+    let equal_to = compute_exactly ~dbd ~facts ~where main prefixes in
     greater_than @ equal_to
 
   (* real match query implementation *)
-let cmatch ~(dbd:Mysql.dbd) t =
+
+let cmatch ~(dbd:Mysql.dbd)  ?(facts=false) t =
   let (main, constants) = signature_of t in
   match main with
   | None -> []
   | Some (main, types) ->
       (* the type of eq is not counted in constants_no *)
       let types_no = List.length types in
-      let constants_no = StringSet.cardinal constants + types_no in
+      let constants_no = StringSet.cardinal constants in
       if (constants_no > critical_value) then 
         let prefixes = prefixes just_factor t in
         (match prefixes with
@@ -476,26 +482,31 @@ let cmatch ~(dbd:Mysql.dbd) t =
             let all_constants = 
               List.fold_right StringSet.add types (StringSet.add main constants)
             in
-            compute_with_only ~dbd main all_concl all_constants
+            compute_with_only ~dbd ~facts main all_concl all_constants
          | _, _ -> [])
       else
         (* in this case we compute all prefixes, and we do not need
            to apply the only constraints *)
         let prefixes =
-          if constants_no = types_no then
-            Some main, [0, []; types_no, types]
+          if constants_no = 0 then
+	    (if types_no = 0 then
+	       Some main, [0, []]
+	     else
+	       Some main, [0, []; types_no, types])
           else
-            prefixes constants_no t
+            prefixes (constants_no+types_no+1) t
         in
         (match prefixes with
            Some main, all_concl ->
+	     compute_exactly ~dbd ~facts ~where:`Conclusion main all_concl
+(*
              List.concat
                (List.map 
                   (fun (m,s) -> 
                     let must = must_of_prefix ~where:`Conclusion main s in
                     let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
                     List.map (fun uri -> (m, uri)) res)
-                  all_concl)
+                  all_concl) *)
          | _, _ -> [])
 
 let power_upto upto consts =
@@ -516,7 +527,8 @@ let power consts =
 
 type where = [ `Conclusion | `Statement ]
 
-let sigmatch ~(dbd:Mysql.dbd) ?(where = `Conclusion) (main, constants) =
+let sigmatch ~(dbd:Mysql.dbd) 
+  ?(facts=false) ?(where = `Conclusion) (main, constants) =
   match main with
     None -> []
   | Some (main, types) ->
@@ -535,17 +547,21 @@ let sigmatch ~(dbd:Mysql.dbd) ?(where = `Conclusion) (main, constants) =
         let subsets = 
           let subsets = power constants in
           let types_no = List.length types in
+	  if types_no > 0 then  
           (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
+	  else subsets
         in
-        compute_exactly ~dbd where main subsets
+        compute_exactly ~dbd ~facts ~where main subsets
 
   (* match query wrappers *)
-let cmatch' = cmatch
-let cmatch ~dbd term =
+
+let cmatch'= cmatch 
+
+let cmatch ~dbd ?(facts=false) term =
   List.map snd
     (List.sort
       (fun x y -> Pervasives.compare (fst y) (fst x))
-      (cmatch' ~dbd term))
+      (cmatch' ~dbd ~facts term))
 
 let constants_of = signature_concl