checked in new version of matita from svn

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 180091c0a871053bcd49c1b997f6ab2bb36421b0..0e86d8ccecf56b8a9005cec598b0e5d585cd875b 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -28,15 +28,31 @@ open Printf
 module Constr = MetadataConstraints
 module PET = ProofEngineTypes 
 
+  (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
+  * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
+let sqlpat_of_shellglob =
+  let star_RE, qmark_RE, percent_RE, uscore_RE =
+    Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_"
+  in
+  fun shellglob ->
+    Pcre.replace ~rex:star_RE ~templ:"%"
+      (Pcre.replace ~rex:qmark_RE ~templ:"_"
+        (Pcre.replace ~rex:percent_RE ~templ:"\\%"
+          (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
+            shellglob)))
+
 let nonvar s =
   let len = String.length s in
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) name =
+let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
+  let sql_pat = sqlpat_of_shellglob pat in
   let query =
-    sprintf "SELECT source FROM %s WHERE value = \"%s\""
-      MetadataTypes.name_tbl name
+        sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
+                 "SELECT source FROM %s WHERE value LIKE \"%s\"")
+          (MetadataTypes.name_tbl ()) sql_pat
+           MetadataTypes.library_name_tbl sql_pat
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar
@@ -44,13 +60,47 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) name =
       (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
 
 let match_term ~(dbd:Mysql.dbd) ty =
+(*   prerr_endline (CicPp.ppterm ty); *)
   let metadata = MetadataExtractor.compute ~body:None ~ty in
   let constants_no =
     MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
   in
+  let full_card, diff =
+    if CicUtil.is_meta_closed ty then
+      Some (MetadataConstraints.Eq constants_no), None
+    else
+      let diff_no =
+        let (hyp_constants, concl_constants) =
+          (* collect different constants in hypotheses and conclusions *)
+          List.fold_left
+            (fun ((hyp, concl) as acc) metadata ->
+               match (metadata: MetadataTypes.metadata) with
+               | `Sort _ | `Rel _ -> acc
+               | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
+                 when not (List.mem uri concl) -> (hyp, uri :: concl)
+               | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
+                 when not (List.mem uri hyp) -> (uri :: hyp, concl)
+               | `Obj _ -> acc)
+            ([], [])
+            metadata
+        in
+        List.length hyp_constants - List.length concl_constants
+      in
+      let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
+      let diff =
+        if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
+          Some (MetadataConstraints.Eq diff_no)
+        else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
+          Some (MetadataConstraints.Gt (diff_no - 1))
+        else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
+          Some (MetadataConstraints.Lt (diff_no + 1))
+        else
+          None
+      in
+      None, diff
+  in
   let constraints = List.map MetadataTypes.constr_of_metadata metadata in
-  Constr.at_least ~dbd ~full_card:(MetadataConstraints.Eq constants_no)
-    constraints
+  Constr.at_least ~dbd ?full_card ?diff constraints
 
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
 
@@ -138,7 +188,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-Constr.StringSet.iter prerr_endline hyp_constants;
+(* Constr.StringSet.iter prerr_endline hyp_constants; *)
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
@@ -209,7 +259,7 @@ let experimental_hint
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-Constr.StringSet.iter prerr_endline hyp_constants;
+(* Constr.StringSet.iter prerr_endline hyp_constants; *)
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
     let pow = 2 ** (Constr.StringSet.cardinal other_constants) in