From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 3 Dec 2004 16:04:01 +0000 (+0000)
Subject: changed "locate" so that it supports shell-like pattern matching with
X-Git-Tag: V_0_1_0~170
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6c6530f435e82cc7688c3f76c4d61b4e0bd7a0e5;p=helm.git

changed "locate" so that it supports shell-like pattern matching with
'*' and '?' wildcards
---

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 180091c0a..f65318896 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -28,15 +28,29 @@ 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\""
+      MetadataTypes.name_tbl sql_pat
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar
diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli
index b3b506de9..0d32e4835 100644
--- a/helm/ocaml/tactics/metadataQuery.mli
+++ b/helm/ocaml/tactics/metadataQuery.mli
@@ -24,7 +24,9 @@
  *)
 
   (** @param vars if set variables (".var" URIs) are considered. Defaults to
-  * false *)
+  * false
+  * @param pat shell like pattern matching over object names, a string where "*"
+  * is interpreted as 0 or more characters and "?" as exactly one character *)
 val locate:
   dbd:Mysql.dbd ->
   ?vars:bool -> string -> string list