Added a new boolean parameter "facts" (default=false) to most of the

methods. The idea is that when facts=true search should be restricted
to facts (theorems without hypothesis). To be used at the maximum
depth of automatic tactcis.

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index f7707f90fbb441e7c8fd4a02c67816ad8ba113bd..2ebd46c2a69478986d70cb2b47f4082d257dfc08 100644 (file)
--- 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
 

diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli
index 3de99469c51cef9e31f6866ad305406dcf1ecf41..72f808efbc80ea7396a407704ee11e30696428f6 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.mli
+++ b/helm/ocaml/metadata/metadataConstraints.mli
@@ -35,18 +35,20 @@ type term_signature = (string * string list) option * StringSet.t
 
   (** @return sorted list of theorem URIs, first URIs in the least have higher
   * relevance *)
-val cmatch: dbd:Mysql.dbd -> Cic.term -> string list
+val cmatch: dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> string list
 
   (** as cmatch, but returned list is not sorted but rather tagged with
   * relevance information: higher the tag, higher the relevance *)
-val cmatch': dbd:Mysql.dbd -> Cic.term -> (int * string) list
+val cmatch': dbd:Mysql.dbd -> ?facts:bool -> Cic.term -> (int * string) list
 
 type where = [ `Conclusion | `Statement ] (** signature matching extent *)
 
   (** @param where defaults to `Conclusion *)
 val sigmatch:
   dbd:Mysql.dbd ->
-  ?where:where -> term_signature ->
+  ?facts:bool ->
+  ?where:where -> 
+  term_signature ->
     (int * string) list
 
 (** {2 Constraint engine} *)