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

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index f7707f90f..2ebd46c2a 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)
@@ -403,6 +403,8 @@ 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"; 
@@ -411,12 +413,14 @@ let myspeciallist =
    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) 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) ->
@@ -537,15 +549,17 @@ let sigmatch ~(dbd:Mysql.dbd) ?(where = `Conclusion) (main, constants) =
           let types_no = List.length types in
           (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) 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